compensatoryQuadratic
plain-language theorem explainer
The definition supplies the residual term reconciling additive and multiplicative quadratic cost approximations in n dimensions. Analysts of the quadratic bridge in the Recognition cost model cite it when decomposing the total quadratic cost. It is realized directly as the difference between the additive quadratic form and the multiplicative quadratic form.
Claim. For vectors $α, ε ∈ ℝ^n$, the compensatory quadratic term is $Q_a(ε) - Q_m(α, ε)$, where $Q_a(ε) = ½ ∑ ε_i²$ is the additive quadratic approximation and $Q_m(α, ε) = ½ (α · ε)²$ is the multiplicative quadratic approximation.
background
The module establishes the additive-multiplicative quadratic bridge. Vectors are coordinate functions from Fin n to reals. The additive quadratic approximates cost by half the sum of squared components. The multiplicative quadratic approximates cost by half the square of the weighted dot product. These two forms are the immediate dependencies of the residual term.
proof idea
The definition is a one-line subtraction of the multiplicative quadratic approximation from the additive quadratic approximation.
why it matters
This term completes the decomposition identity that equates the additive quadratic to the sum of the multiplicative quadratic and the compensatory term. It is invoked in the nonnegativity theorem under the condition that the squared norm of α is at most one. The construction supports quadratic cost analysis inside the N-dimensional bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.