AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher

No declaration docstring.

abbrev State := EuclideanSpace ℝ ι

/-- The canonical density/log-ratio pair is in the generator integration-by-
parts domain needed to invoke Chewi Theorem 1.2.14.

The fields are exactly the three integrability terms, stationarity of the
product observable, and generator symmetry for this pair.  This is a local
pair contract, not a global reversibility claim. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:50published source at 0e31a3cda412

- The canonical density/log-ratio pair is in the generator integration-by- parts domain needed to invoke Chewi Theorem 1.2.14. The fields are exactly the three integrability terms, stationarity of the product observable, and generator symmetry for this pair. This is a local pair contract, not a global reversibility claim.

structure DirichletPairDomain
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop where
  generator_product_integrable :
    Integrable
      (generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi)) pi
  density_mul_generator_logRatio_integrable :
    Integrable
      (fun x => RNLogRatio.density mu pi x *
        generator (RNLogRatio.logRatio mu pi) x) pi
  logRatio_mul_generator_density_integrable :
    Integrable
      (fun x => RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x) pi
  stationary_product :
    (∫ x,
      generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi) x ∂pi) = 0
  symmetric_pair :
    (∫ x, RNLogRatio.density mu pi x *
      generator (RNLogRatio.logRatio mu pi) x ∂pi) =
      ∫ x, RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x ∂pi

/-- The concrete carré-du-champ identification required to turn the abstract
Dirichlet form into canonical relative Fisher information.

For overdamped Langevin this is the measure-domain version of
`Gamma(f,g)=inner (grad f) (grad g)` together with the score chain rule for the
canonical density.  It is kept as a separate contract because absolute
continuity alone gives no differentiability of an RN representative. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:58published source at 0e31a3cda412

- The concrete carré-du-champ identification required to turn the abstract Dirichlet form into canonical relative Fisher information. For overdamped Langevin this is the measure-domain version of `Gamma(f,g)=inner (grad f) (grad g)` together with the score chain rule for the canonical density. It is kept as a separate contract because absolute continuity alone gives no differentiability of an RN representative.

def HasCanonicalFisherGamma
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop :=
  ∀ᵐ x ∂pi,
    StochasticProcesses.CarreDuChamp.carreDuChamp generator
      (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) x =
      RNLogRatio.density mu pi x *
        CanonicalRelativeFisher.scoreSq mu pi x

/-- Chewi Theorem 1.2.14 plus the concrete Gamma/score identification gives
exactly the canonical relative Fisher information:

`E_pi(dmu/dpi, log(dmu/dpi)) = FI(mu || pi)`.

This is the reusable Dirichlet--Fisher edge consumed by KL dissipation and by
the generator form of log-Sobolev inequalities. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:91published source at 0e31a3cda412

- Chewi Theorem 1.2.14 plus the concrete Gamma/score identification gives exactly the canonical relative Fisher information: `E_pi(dmu/dpi, log(dmu/dpi)) = FI(mu || pi)`. This is the reusable Dirichlet--Fisher edge consumed by KL dissipation and by the generator form of log-Sobolev inequalities.

theorem dirichletForm_density_logRatio_eq_information
    (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) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      CanonicalRelativeFisher.information mu pi hscore := by
  have hibp :=
    StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts
      pi generator (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)
      hpair.generator_product_integrable
      hpair.density_mul_generator_logRatio_integrable
      hpair.logRatio_mul_generator_density_integrable
      hpair.stationary_product hpair.symmetric_pair
  rw [hibp.2]
  rw [CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq
    mu pi hscore]
  exact integral_congr_ae hgamma

/-- Equivalent source-facing integral form of the same bridge. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:108published source at 0e31a3cda412

- Equivalent source-facing integral form of the same bridge.

theorem dirichletForm_density_logRatio_eq_integral_scoreSq
    (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) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      ∫ x, CanonicalRelativeFisher.scoreSq mu pi x ∂mu := by
  rw [dirichletForm_density_logRatio_eq_information
    mu pi generator hscore hpair hgamma]
  exact CanonicalRelativeFisher.information_eq_integral_scoreSq mu pi hscore

/-- A supplied KL derivative written as minus the canonical density/log-ratio
Dirichlet form immediately becomes the standard dissipation rate `-FI`.

This theorem intentionally starts *after* the analytic law-evolution /
differentiation-under-the-integral step.  The next topology node must prove that
step for the Langevin measure flow rather than hiding it inside this algebraic
handoff. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:132published source at 0e31a3cda412

- A supplied KL derivative written as minus the canonical density/log-ratio Dirichlet form immediately becomes the standard dissipation rate `-FI`. This theorem intentionally starts *after* the analytic law-evolution / differentiation-under-the-integral step. The next topology node must prove that step for the Langevin measure flow rather than hiding it inside this algebraic handoff.

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

AutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean:154published source at 0e31a3cda412