Rewrite a supplied negative-Dirichlet derivative as negative Fisher

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.hasDerivAt_eq_neg_information_of_eq_neg_dirichlet · theorem · Teaching coverage

Statement

Let μ and π, L, and the three domain/Γ witnesses satisfy all hypotheses of the Dirichlet–Fisher bridge, including μ σ-finiteness and a Lebesgue-decomposition instance. Let K:ℝ→ℝ be any real function and t∈ℝ. If K has a two-sided derivative at t with value −Eπ^L(ρ,r), then K has a derivative there with value −I_hscore(μ∥π). The derivative assumption is supplied; K is not required by the formal statement to be a KL-divergence path.

All objects and hypotheses

• ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
• μ and π are arbitrary measures on E. No probability, finite-total-mass, or normalization hypothesis is present.
• Use the exact selected functions ρ(x) = (μ.rnDeriv π x).toReal and r(x) = RNLogRatio.logRatio μ π x = MeasureTheory.llr μ π x = Real.log(ρ(x)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
• μ is σ-finite, and the typeclass HaveLebesgueDecomposition μ π is supplied. π need not be assumed σ-finite. These are in addition to μ ≪ π in the score-domain witness.
• L is a real-linear map from all functions E → ℝ to all functions E → ℝ. Its linearity alone does not say that it generates a Markov semigroup, preserves a measure, or is a diffusion.
• The supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).
• The supplied witness hpair proves, for the fixed functions ρ and r, that L(ρr), x ↦ ρ(x)Lr(x), and x ↦ r(x)Lρ(x) are π-integrable, that ∫ L(ρr) dπ = 0, and that ∫ ρ Lr dπ = ∫ r Lρ dπ.
• The supplied hgamma asserts Γ_L(ρ,r)(x) = ρ(x)q(x) for π-almost every x, where Γ_L(f,g) = ½[L(fg) − f Lg − g Lf]. It is not required pointwise everywhere.
• K is an arbitrary function ℝ → ℝ and t is an arbitrary real time. hK is the full HasDerivAt assertion for K at t with derivative −Eπ^L(ρ,r), using the ordinary two-sided neighborhood filter, not a one-sided derivative on t≥0.
• The measures μ and π are fixed parameters in this declaration. No time-dependent law μ_t or equation relating K to entropy is assumed.

Mathematical proof

theorem hasDerivAt_eq_neg_information_of_eq_neg_dirichlet
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator)
    {K : ℝ → ℝ} {t : ℝ}
    (hK : HasDerivAt K
      (-FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)) t) :
    HasDerivAt K (-CanonicalRelativeFisher.information mu pi hscore) t

theorem hasDerivAt_eq_neg_information_of_eq_neg_dirichlet
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator)
    {K : ℝ → ℝ} {t : ℝ}
    (hK : HasDerivAt K
      (-FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)) t) :
    HasDerivAt K (-CanonicalRelativeFisher.information mu pi hscore) t := by
  simpa [dirichletForm_density_logRatio_eq_information
    mu pi generator hscore hpair hgamma] using hK

end

end CanonicalDirichletFisher
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Scope and omitted-condition boundaries

• This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
• These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
• No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
• No KL identity, entropy finiteness, evolving family of measures, PDE/semigroup equation, or differentiation under the integral is proved. The function K and its derivative are supplied as inputs.
• A finite-entropy neighborhood, differentiability of an actual KL path, source-law normalization, and an endpoint one-sided-to-two-sided adapter are not supplied.
• This is an algebraic handoff after a derivative proof; it is not a new entropy-dissipation theorem.