dot_sq_le_sqNorm_mul
plain-language theorem explainer
This inequality supplies a Cauchy-Schwarz bound on the squared weighted dot product in terms of the quadratic form on α and the squared Euclidean norm on ε. Researchers deriving norm-controlled relations between multiplicative and additive quadratic costs cite it when closing the bridge in the N-dimensional cost model. The proof is a term-mode one-liner that unfolds dot and invokes the standard Finset.sum_mul_sq_le_sq_mul_sq lemma.
Claim. For vectors α, ε : ℝ^n, (∑_{i=1}^n α_i ε_i)^2 ≤ (∑_{i=1}^n α_i^2) ⋅ (∑_{i=1}^n ε_i^2).
background
The module develops the additive-multiplicative quadratic bridge. Vec n is the abbreviation for n-component real vectors realized as functions Fin n → ℝ. The dot product is the weighted sum dot α ε := ∑_{i:Fin n} α i ⋅ ε i used by the logarithmic aggregate.
proof idea
The proof is a term-mode one-liner. It unfolds the dot definition, applies simpa with pow_two, and reduces the goal to an instance of Finset.sum_mul_sq_le_sq_mul_sq over the finite set Fin n.
why it matters
The lemma is invoked inside the proof of multiplicative_le_additive_of_sqNorm_le_one to obtain the bound multiplicativeQuadratic α ε ≤ additiveQuadratic ε whenever dot α α ≤ 1. It therefore supplies the key algebraic step that lets the quadratic bridge relate the two cost families under the unit-norm constraint on α, feeding the larger program that connects J-cost functionals to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.