dot
plain-language theorem explainer
The dot product supplies the inner product for n-dimensional vectors inside the reciprocal cost construction. Workers on multi-component J-cost aggregates cite it when deriving quadratic bounds and compensatory nonnegativity results. The definition is introduced as a direct finite sum of componentwise products.
Claim. For vectors $α, t ∈ ℝ^n$ the weighted dot product is $∑_{i=1}^n α_i t_i$.
background
The module defines core operations for the N-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vectors appear as coordinate functions from the finite set Fin n to the reals. The dot product furnishes the bilinear form required for the subsequent quadratic and norm constructions.
proof idea
The definition is given explicitly by the summation over the index set Fin n. It requires no lemmas or tactics and functions as the base operation for unfolding sqNorm and the quadratic cost expressions.
why it matters
This pairing is the common ingredient in the Bridge theorems on compensatory nonnegativity under squared-norm bounds and on the comparison of multiplicative and additive quadratic costs. It likewise appears in the squared-norm uniform-weight calibration. In the Recognition framework it carries the scalar J-cost structure into the vector setting while preserving the relations needed for the composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.