def definition def or abbrev

`additiveQuadratic`

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

formal statement (Lean)

  14noncomputable def additiveQuadratic {n : ℕ} (ε : Vec n) : ℝ :=

Definition body.

  15  (1 / 2 : ℝ) * ∑ i : Fin n, (ε i) ^ 2
  16
  17/-- Quadratic multiplicative approximation `1/2 * (Σ αᵢ εᵢ)²`. -/

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

additive_decomposition in IndisputableMonolith.Cost.Ndim.Bridge decl_use
compensatoryQuadratic in IndisputableMonolith.Cost.Ndim.Bridge decl_use
multiplicative_le_additive_of_sqNorm_le_one in IndisputableMonolith.Cost.Ndim.Bridge decl_use

Lean names referenced from this declaration's body.