dot_log_hadamardMul
plain-language theorem explainer
The theorem shows that the weighted dot product of alpha with the componentwise logarithm of a Hadamard product equals the sum of the separate dot products with each logarithm. Researchers extending the scalar J-cost to N dimensions cite it when decomposing multiplicative structures inside the logarithmic aggregate. The proof unfolds the three core definitions then applies the real logarithm product rule inside a finite sum, followed by distributivity and sum splitting.
Claim. For vectors $α, x, y ∈ ℝ^n$ with $x_i > 0$ and $y_i > 0$ for every index $i$, $∑_i α_i log(x_i y_i) = ∑_i α_i log x_i + ∑_i α_i log y_i$.
background
The module lifts the scalar reciprocal cost to n dimensions by replacing the single logarithm with a weighted aggregate over componentwise logs. Vec n is the type of functions from Fin n to ℝ. The dot operation is the sum over i of α_i times the i-th component of the second vector. logVec applies the natural logarithm to each component, while hadamardMul multiplies corresponding components.
proof idea
The tactic proof unfolds dot, logVec and hadamardMul, then enters a calc block. It first invokes Finset.sum_congr and Real.log_mul (under the positivity hypotheses) to replace each log(x_i y_i) by log x_i + log y_i. A second sum_congr plus ring distributes the factor α_i, after which Finset.sum_add_distrib splits the sum into the two desired terms.
why it matters
The identity is used directly in JcostN_dAlembert to establish the N-dimensional form of the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). It supplies the additive property required to lift the scalar kernel to the phi-ladder and eight-tick octave constructions that appear in the forcing chain T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.