AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinKLDissipation

- Source-facing smooth finite-domain Langevin entropy dissipation: `d/dt KL(mu_t || pi) = - FI(mu_t || pi)`. Every non-algebraic obligation remains explicit in the three domain contracts. This is the Chapter 1.2 join node consumed later by functional-inequality and sampling-convergence arguments.

theorem kl_hasDerivAt_eq_neg_information
    {n : ℕ}
    (V : EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
    (mu : ℝ → Measure (EuclideanSpace ℝ (Fin (n + 1))))
    (pi : Measure (EuclideanSpace ℝ (Fin (n + 1))))
    (generator :
      (EuclideanSpace ℝ (Fin (n + 1)) → ℝ) →ₗ[ℝ]
        (EuclideanSpace ℝ (Fin (n + 1)) → ℝ))
    (rhoDot : EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
    (t : ℝ)
    [SigmaFinite (mu t)] [Measure.HaveLebesgueDecomposition (mu t) pi]
    (hscore :
      InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain
        (mu t) pi)
    (hflow :
      InformationTheory.CanonicalKLDissipation.FlowDerivativeDomain
        mu pi generator rhoDot t)
    (hpair :
      InformationTheory.CanonicalDirichletFisher.DirichletPairDomain
        (mu t) pi generator)
    (hlangevin :
      LangevinCanonicalFisherGamma.SmoothCanonicalPairDomain
        V (mu t) pi generator) :
    HasDerivAt
      (fun s => (_root_.InformationTheory.klDiv (mu s) pi).toReal)
      (-InformationTheory.CanonicalRelativeFisher.information
        (mu t) pi hscore) t := by
  exact
    InformationTheory.CanonicalKLDissipation.kl_hasDerivAt_eq_neg_information
      mu pi generator rhoDot t hscore hflow hpair
      (LangevinCanonicalFisherGamma.hasCanonicalFisherGamma
        V (mu t) pi generator hlangevin)

end

end LangevinKLDissipation
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LangevinKLDissipation.lean:39published source at 0e31a3cda412