dot_log_hadamardInv
plain-language theorem explainer
The weighted dot product of a vector alpha with the componentwise logarithm of the inverse of x equals the negative of the dot product with the logarithm of x. Researchers deriving N-dimensional cost functions in Recognition Science cite this when establishing invariance under inversion. The proof unfolds the definitions then applies the log inversion identity followed by ring and simp to factor the negative sign.
Claim. For vectors $α, x ∈ ℝ^n$, the weighted dot product satisfies $∑_{i=1}^n α_i log((x_i)^{-1}) = -∑_{i=1}^n α_i log(x_i)$.
background
The module defines N-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vec n is the type of n-component real vectors as functions Fin n → ℝ. The weighted dot product is ∑ α_i t_i. logVec applies Real.log componentwise and hadamardInv applies inversion componentwise. The local theoretical setting is the core definitions for multi-component reciprocal cost.
proof idea
Tactic-mode proof that unfolds dot, logVec, and hadamardInv, then proceeds via calc. The first step uses Finset.sum_congr with Real.log_inv to replace each log of an inverse by the negative log. The second step applies ring to distribute the negative sign inside the sum. The final step uses simp to pull the negative outside the sum.
why it matters
This result is invoked in JcostN_reciprocal to prove JcostN α (hadamardInv x) = JcostN α x after rewriting with JcostN_eq_cosh_logsum and applying Real.cosh_neg. It supplies the reciprocity step needed for the N-dimensional cost to respect componentwise inversion, consistent with the Recognition Composition Law and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.