AveragingDerivation
plain-language theorem explainer
A typeclass equips a real function F with the symmetric-unit axioms plus agreement of F(exp t) with the J-cost on the exponential image. Log-domain cost derivations cite the class to obtain equality between the composed log function and Jlog. The declaration is a direct class extension adjoining one agreement axiom.
Claim. A function $F:ℝ→ℝ$ satisfies the averaging derivation property when it extends the symmetric unit axioms ($F(x)=F(x^{-1})$ for $x>0$ and $F(1)=0$) and obeys the agreement condition $F(e^t)=J_{cost}(e^t)$ for every real $t$.
background
The module works in the log domain by composing cost functions with the exponential map. The auxiliary definition Flog F t := F(exp t) converts a function on the positive reals into one on the additive group of reals. SymmUnit supplies the two axioms that any admissible cost function must obey: invariance under inversion and vanishing at unity. The upstream JcostCore.AveragingDerivation supplies the same class in the original domain, while the present version is specialized for the log-domain setting.
proof idea
The declaration is the class definition itself; it directly extends SymmUnit F by adjoining the single agreement axiom that equates F(exp t) with Jcost(exp t) for all t.
why it matters
This class is the key interface that lets downstream lemmas such as Flog_eq_Jlog and F_eq_J_on_pos_of_derivation conclude that Flog coincides with Jlog and that F agrees with Jcost on positives. It closes the bridge between the original JcostCore formulation and the log-domain FlogEL development, supporting the derivation of zero-derivative and non-negativity properties for Flog.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.