multiplicative_le_additive_of_sqNorm_le_one
plain-language theorem explainer
When the squared norm of the weight vector alpha is at most one, the multiplicative quadratic cost is bounded above by the additive quadratic cost for any error vector epsilon. Cost modelers comparing quadratic approximations in the N-dimensional setting would cite this bound to control the gap between the two forms. The proof applies a Cauchy-Schwarz inequality to the squared dot product, replaces the resulting factor by the unit bound on alpha, scales by one half, and simplifies.
Claim. If $||α||^2 ≤ 1$ for $α, ε ∈ ℝ^n$, then $½(α · ε)^2 ≤ ½ ∑_i ε_i².
background
The Cost.Ndim.Bridge module develops relations between additive and multiplicative quadratic approximations. Vec n is the type of n-component real vectors, written as functions Fin n → ℝ. The dot product is the standard sum ∑ α_i ε_i. Additive quadratic is defined as (1/2) ∑ (ε_i)^2. Multiplicative quadratic is defined as (1/2) (dot α ε)^2. The result depends on the upstream Cauchy-Schwarz form dot_sq_le_sqNorm_mul, which states (dot α ε)^2 ≤ (dot α α) · ∑ (ε_i)^2.
proof idea
Apply dot_sq_le_sqNorm_mul to obtain (dot α ε)^2 ≤ (dot α α) · ∑ (ε_i)^2. Use the hypothesis dot α α ≤ 1 together with nonnegativity of the sum of squares to replace the product by 1 · ∑ (ε_i)^2. Multiply both sides by the nonnegative constant 1/2 and unfold the two quadratic definitions to reach the target inequality.
why it matters
The theorem is invoked directly by compensatory_nonneg_of_sqNorm_le_one to establish nonnegativity of the residual compensatory term under the same norm bound. It belongs to the additive-multiplicative quadratic bridge in the Ndim cost layer and supports comparisons of the two quadratic forms when weights are normalized. In the Recognition Science setting it helps bound the difference between multiplicative and additive approximations inside the cost analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.