def definition def or abbrev

`multiplicativeQuadratic`

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

formal statement (Lean)

  18noncomputable def multiplicativeQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=

Definition body.

  19  (1 / 2 : ℝ) * (dot α ε) ^ 2
  20
  21/-- Residual compensatory quadratic term. -/

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.