geometricMean
plain-language theorem explainer
geometricMean encodes the geometric mean of a list of reals as the exponential of the average logarithm. It is cited by proofs establishing that the geometric mean minimizes total J-cost in the F1 log-domain geometry. Researchers working on simultaneous versus sequential descent in bond costs reference it. The definition is a direct one-line implementation of the standard formula.
Claim. For a list $ns = [n_1, ..., n_k]$ of positive real numbers the geometric mean is defined by $g = e^{(1/k) sum log n_i}$.
background
The module develops log-domain J-cost geometry from the canonical reciprocal cost $J(x) = 1/2(x + x^{-1}) - 1$. Geometric-mean optimality is listed among the main results, together with the distinction between simultaneous and sequential descent. The definition extends core identities imported from JcostCore on the positive reals.
proof idea
This is a one-line definition that directly encodes the geometric mean as the exponential of the average of the logarithms of the list elements.
why it matters
The definition supplies the object used by the parent theorem geometricMean_pos that proves positivity of the mean. It realizes the geometric-mean optimality step required by the F1 paper for J-cost minimization. In the Recognition framework it supplies the log-domain fixed point that feeds into RCL identities and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.