hadamardDiv
plain-language theorem explainer
Componentwise division of n-vectors is supplied by this definition. Researchers extending the scalar J-cost to multiple dimensions cite it when decomposing logarithmic aggregates into differences. The definition is introduced as a direct pointwise operation on coordinate functions from Fin n to the reals.
Claim. For vectors $x, y : Vec n$ with $Vec n := Fin n → ℝ$, the componentwise division is the vector whose $i$-th entry equals $x_i / y_i$.
background
The module Cost.Ndim.Core defines n-dimensional vectors as coordinate functions Vec n := Fin n → ℝ. These vectors carry the weighted dot product and the exponential aggregate R(x) = exp(∑ α_i log x_i), which lifts the scalar reciprocal cost kernel through a log-weighted sum. The local setting is the construction of multi-component reciprocal cost by componentwise operations on these vectors.
proof idea
This is a direct definition that maps each index i : Fin n to the real division x i / y i. No lemmas are invoked; the construction is the primitive pointwise operation on which later log identities rest.
why it matters
The definition is invoked by dot_log_hadamardDiv to obtain the log-aggregate identity dot α (logVec (hadamardDiv x y)) = dot α (logVec x) - dot α (logVec y). It likewise supplies the division term in JcostN_dAlembert (the n-dimensional d'Alembert identity) and in the submultiplicativity lemma JcostN_submult. It thereby extends the Recognition Composition Law to the n-dimensional setting required for the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.