def definition def or abbrev

`compensatoryQuadratic`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  22noncomputable def compensatoryQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=

Definition body.

  23  additiveQuadratic ε - multiplicativeQuadratic α ε
  24

From the project-wide theorem graph. These declarations reference this one in their body.

additive_decomposition in IndisputableMonolith.Cost.Ndim.Bridge decl_use
compensatory_nonneg_of_sqNorm_le_one in IndisputableMonolith.Cost.Ndim.Bridge decl_use

Lean names referenced from this declaration's body.