hasDerivAt_Jlog
plain-language theorem explainer
Analysts working with the free energy principle bridge cite this result to obtain the first derivative of the log-domain cost in additive coordinates. The claim asserts that this derivative equals the hyperbolic sine at every real argument. The tactic proof reduces the statement to the standard derivative of the hyperbolic cosine after a pointwise rewriting.
Claim. For every real number $t$, the log-domain cost function defined by $J(t) = J_0(e^t)$ is differentiable at $t$ with derivative equal to $sinh(t)$.
background
The Cost module introduces the log-domain cost as the composition of the base cost function with the exponential, converting the original multiplicative structure into an additive one on the reals. A supporting identity shows that this log-domain cost equals the hyperbolic cosine minus one, obtained by direct substitution of the exponential into the explicit form of the cost. The present lemma therefore inherits differentiability from the hyperbolic functions supplied by the ambient library.
proof idea
The tactic proof first proves an extensional equality between the log-domain cost and the map sending $t$ to cosh($t$) minus one, invoking the auxiliary identity lemma. It then obtains the known derivative of cosh, subtracts the zero derivative of the constant function one, and simplifies the resulting expression to reach the target derivative.
why it matters
This derivative is invoked by the zero-case lemma and by the free-energy-principle bridge theorem to establish that the second derivative of the log-domain cost at equilibrium equals one. It also enables derivative calculations for averaged cost functions in the FlogEL submodule. The result supplies the first-order local information required for equilibrium analysis of the cost, consistent with the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.