Flog_eq_Jlog_pt
plain-language theorem explainer
The lemma equates the log-domain cost Flog derived from any averaging derivation F with the canonical Jlog at each real t. Cost modelers in Recognition Science cite it to transfer identities between equivalent representations of the same quantity. The proof reduces the definitions of Flog and Jlog then invokes the agrees axiom supplied by the AveragingDerivation typeclass.
Claim. Let $F : ℝ → ℝ$ be an averaging derivation. Then for every real $t$, $F(e^t) = Jcost(e^t)$.
background
In the log-domain cost setting, Jlog is the composition of Jcost with the exponential, yielding a cost function on the additive reals. Flog is defined identically but for a general map F. The AveragingDerivation typeclass extends SymmUnit and requires that F(exp t) equals Jcost(exp t) for all real t, supplying the bridge between the two compositions.
proof idea
The term proof first applies dsimp to unfold the definitions of Flog and Jlog, then uses the agrees field of the AveragingDerivation instance at the given t.
why it matters
This pointwise equality is the base step for the module's follow-on lemmas Flog_eq_Jlog, Flog_eq_zero_iff_of_derivation, and Flog_nonneg_of_derivation. It identifies the log-domain cost for any averaging derivation with the standard Jlog, supporting transfer of non-negativity and zero-set results within the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.