logVec
plain-language theorem explainer
Componentwise logarithm on n-vectors. Researchers extending scalar J-cost to multi-component forms cite this when constructing the weighted log aggregate for n-dimensional reciprocal cost. The definition applies the real logarithm directly to each coordinate of the input vector.
Claim. For an n-dimensional vector $x$ with real components, the map $x_i$ to the vector whose $i$-th entry is the real logarithm of $x_i$.
background
The module defines n-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vectors are coordinate functions from Fin n to the reals. This supplies the pointwise logarithm required to convert componentwise multiplication and division into addition and subtraction inside the dot product.
proof idea
One-line definition that applies Real.log to each coordinate via the function abstraction fun i => Real.log (x i).
why it matters
It supplies the coordinate logarithm used by aggregate, JcostN, and the three hadamard log theorems. These in turn feed the n-dimensional cost that generalizes the scalar J-uniqueness and the phi-ladder mass formula to multiple components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.