Jlog
plain-language theorem explainer
Jlog composes the base cost with the exponential map to shift recognition cost into additive log coordinates. Analysts deriving stationary points or minima for the cost function cite this definition when moving from multiplicative to logarithmic variables. The declaration is a direct one-line composition that immediately enables rewriting via hyperbolic identities.
Claim. Define $J_ {log}(t) := J_{cost}(e^t)$ for $t$ real, where $J_{cost}(x) = (x + x^{-1})/2 - 1$.
background
The Cost module defines Jcost as the elementary recognition cost $J_{cost}(x) = (x + x^{-1})/2 - 1$. Jlog applies this cost after the exponential map, converting the argument to logarithmic scale. Upstream siblings supply the equivalent closed form $J_{log}(t) = (e^t + e^{-t})/2 - 1$, which matches cosh(t) - 1 and supports derivative calculations.
proof idea
The declaration is a one-line wrapper that applies Jcost to Real.exp t.
why it matters
Jlog supplies the log-domain interface used by hasDerivAt_Jlog, EL_global_min, and EL_stationary_at_zero. It realizes the shift from multiplicative J-cost to additive form that aligns with J-uniqueness in the forcing chain. The definition is referenced in forty downstream results that establish the global minimum at zero and the derivative vanishing there.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.