Flog_eq_Jlog
Under the averaging derivation hypothesis on F, the log-domain cost function defined by Flog F coincides exactly with the canonical Jlog. Researchers deriving properties of cost functions in the Recognition framework cite this to interchange the two representations without further work. The proof is a one-line wrapper that applies function extensionality to the already-established pointwise equality.
claimLet $F : {R} {to} {R}$ satisfy the averaging derivation property, i.e., $F({exp} t) = J_{cost}({exp} t)$ for every real $t$. Then the function $t {mapsto} F({exp} t)$ equals the function $t {mapsto} J_{cost}({exp} t)$.
background
The module works in the log-domain obtained by composing the base Jcost with the exponential map. AveragingDerivation is the typeclass that records the agreement condition $F({exp} t) = J_{cost}({exp} t)$ together with the symmetry-unit axioms. Jlog is the fixed definition $J_{cost} {circ} {exp}$, while Flog F is the same composition but using the supplied function F. The upstream pointwise lemma Flog_eq_Jlog_pt already shows equality at each fixed t by direct appeal to the agrees field of the typeclass.
proof idea
The proof is a one-line wrapper: it applies funext to reduce the functional equality to the pointwise statement, then invokes the lemma Flog_eq_Jlog_pt (F:=F) t whose body is the direct unfolding of the agrees axiom.
why it matters in Recognition Science
The equality is used by hasDerivAt_Flog_of_derivation to transfer the known derivative of Jlog to the Flog form. It therefore closes the identification between a generic averaging derivation and the canonical log-domain cost inside the cost module, enabling all subsequent derivative, non-negativity and zero-set results that depend on the derivation assumption.
scope and limits
- Does not establish the equality for an arbitrary function F.
- Does not compute explicit numerical values of the cost.
- Does not address differentiability or monotonicity on its own.
- Does not extend the identification beyond real variables.
Lean usage
have hfun := Flog_eq_Jlog (F:=F)formal statement (Lean)
54lemma Flog_eq_Jlog {F : ℝ → ℝ} [AveragingDerivation F] :
55 (fun t => Flog F t) = Jlog := by
proof body
Term-mode proof.
56 funext t; simpa using (Flog_eq_Jlog_pt (F:=F) t)
57