multiplicativeQuadratic
plain-language theorem explainer
multiplicativeQuadratic supplies the term (1/2)(α · ε)^2 as the multiplicative quadratic approximation for n-dimensional vectors α and ε. Cost analysts in the Recognition framework cite it when decomposing total quadratic cost into multiplicative and compensatory parts. The definition is a direct one-line expression built from the dot product.
Claim. For vectors $α, ε ∈ ℝ^n$, the multiplicative quadratic approximation is defined by $½(α · ε)^2$, where the dot product is the sum $∑_i α_i ε_i$.
background
The Cost.Ndim.Bridge module develops the additive-multiplicative quadratic bridge for cost calculations. Vec n is the abbreviation for n-component real vectors, realized as maps from Fin n to ℝ. The dot operation from Core computes the weighted sum ∑ α_i ε_i and is described as the weighted dot product used by the logarithmic aggregate. This definition isolates the multiplicative contribution within the quadratic cost structure.
proof idea
The definition is a direct algebraic expression: it applies dot to α and ε, squares the result, and multiplies by 1/2.
why it matters
This definition is used by the additive_decomposition theorem, which states additiveQuadratic ε equals multiplicativeQuadratic α ε plus compensatoryQuadratic α ε. It also supports the bound in multiplicative_le_additive_of_sqNorm_le_one when dot α α ≤ 1. In the Recognition framework it contributes to the quadratic bridge in the N-dimensional cost analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.