AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CanonicalLogSobolev

Samplinglib mathematical lesson

A canonical generator LSI gives finite KL and a Fisher bound

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CanonicalLogSobolev.finite_klDiv_and_toReal_le_half_mul_information · theorem · Teaching coverage

Read this first

Mathematical statement

Let mu be a probability law and pi a reference law on finite-dimensional Euclidean space. Assume pi satisfies the density-form generator log-Sobolev inequality with constant C. If the canonical density dmu/dpi is admissible, its canonical log-ratio has a finite smooth score, and the generator integration-by-parts and carré-du-champ identities identify its Dirichlet form with Fisher information, then KL(mu||pi) is finite and KL(mu||pi) ≤ (C/2) FI(mu||pi).

\[\mathrm{KL}(\mu\|\pi)<\infty,\qquad \mathrm{KL}(\mu\|\pi)\le \frac{C}{2}\,\mathrm{FI}(\mu\|\pi).\]

Lean statement · finite_klDiv_and_toReal_le_half_mul_information

The Lean theorem returns klDiv mu pi != infinity together with the toReal inequality. It keeps density admissibility, canonical score regularity, generator-domain integration by parts and the gamma/score identity as separate hypotheses.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem finite_klDiv_and_toReal_le_half_mul_information
    (mu pi : Measure (EuclideanSpace ℝ ι)) [IsProbabilityMeasure mu]
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (EuclideanSpace ℝ ι → ℝ) →ₗ[ℝ] (EuclideanSpace ℝ ι → ℝ))
    {C : ℝ}
    (hLSI : Generator.SatisfiesLogSobolev pi generator C)
    (hAdmissible : Generator.LogSobolevAdmissible pi generator
      (InformationTheory.RNLogRatio.density mu pi))
    (hScore :
      InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hPair :
      InformationTheory.CanonicalDirichletFisher.DirichletPairDomain
        mu pi generator)
    (hGamma :
      InformationTheory.CanonicalDirichletFisher.HasCanonicalFisherGamma
        mu pi generator) :
    _root_.InformationTheory.klDiv mu pi ≠ ∞ ∧
      (_root_.InformationTheory.klDiv mu pi).toReal ≤
        (C / 2) *
          InformationTheory.CanonicalRelativeFisher.information mu pi hScore

Exact module and namespace context

Proof roadmap

1Extract genuine KL finiteness
Entropy admissibility gives integrability of rho log rho under pi. Mathlib transports this to integrability of the canonical log-likelihood ratio under mu, which together with absolute continuity proves that the ENNReal KL divergence is not infinity.
2Apply LSI to the canonical density
The supplied LSI is specialized to rho=dmu/dpi. Its entropy side is a genuine finite integral because admissibility was stated before applying the inequality.
3Identify entropy with canonical KL
The Radon--Nikodym change-of-measure identity rewrites the density entropy as the integral of Mathlib's canonical log-ratio under mu, hence as klDiv.toReal.
4Identify Dirichlet energy with Fisher information
The already verified integration-by-parts and carré-du-champ bridge turns the generator Dirichlet form into the canonical squared-score integral.

Full assumptions and notation

All objects and hypotheses

mu is a probability measure; hLSI supplies that pi is a probability measure and C>0.
The canonical Radon--Nikodym density is nonnegative, normalized and integrable, with integrable rho log rho and rho L(log rho).
mu is absolutely continuous with respect to pi; the canonical log-ratio is differentiable mu-almost everywhere and its squared score is integrable.
The density/log-density pair lies in the generator integration-by-parts domain and its carré-du-champ is rho times the squared score.
Chewi uses C. SALD and Lee--Shen--Tian use the reciprocal rate c_LSI=lambda=C^{-1}.

Mathematical proof

1. Extract genuine KL finiteness

Entropy admissibility gives integrability of rho log rho under pi. Mathlib transports this to integrability of the canonical log-likelihood ratio under mu, which together with absolute continuity proves that the ENNReal KL divergence is not infinity.

\[\rho\log\rho\in L^1(\pi)\Longrightarrow \log(d\mu/d\pi)\in L^1(\mu)\Longrightarrow \mathrm{KL}(\mu\|\pi)<\infty.\]

Corresponding Lean step

integrable_rnDeriv_mul_log_iff; InformationTheory.klDiv_ne_top

2. Apply LSI to the canonical density

The supplied LSI is specialized to rho=dmu/dpi. Its entropy side is a genuine finite integral because admissibility was stated before applying the inequality.

\[\operatorname{Ent}_{\pi}(\rho)\le \frac C2\,\mathcal E_{\pi}(\rho,\log\rho).\]

Corresponding Lean step

Generator.SatisfiesLogSobolev; Generator.LogSobolevAdmissible

3. Identify entropy with canonical KL

The Radon--Nikodym change-of-measure identity rewrites the density entropy as the integral of Mathlib's canonical log-ratio under mu, hence as klDiv.toReal.

\[\int \rho\log\rho\,d\pi=\int\log(d\mu/d\pi)\,d\mu=\mathrm{KL}(\mu\|\pi).\]

Corresponding Lean step

integral_rnDeriv_mul_log; RNLogRatio.toReal_klDiv_eq_integral_logRatio_of_probability

4. Identify Dirichlet energy with Fisher information

The already verified integration-by-parts and carré-du-champ bridge turns the generator Dirichlet form into the canonical squared-score integral.

\[\mathcal E_{\pi}(\rho,\log\rho)=\int\|\nabla\log(d\mu/d\pi)\|^2\,d\mu=\mathrm{FI}(\mu\|\pi).\]

Corresponding Lean step

CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_information

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · finite_klDiv_and_toReal_le_half_mul_information

The proof first derives integrability of the canonical llr from the admissible RN entropy integrand. It then applies the generator LSI to the canonical density and rewrites its two sides using Mathlib's RN/KL theorem and ASTIS's compiled Dirichlet--Fisher theorem.

Download module (.lean)

theorem finite_klDiv_and_toReal_le_half_mul_information
    (mu pi : Measure (EuclideanSpace ℝ ι)) [IsProbabilityMeasure mu]
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (EuclideanSpace ℝ ι → ℝ) →ₗ[ℝ] (EuclideanSpace ℝ ι → ℝ))
    {C : ℝ}
    (hLSI : Generator.SatisfiesLogSobolev pi generator C)
    (hAdmissible : Generator.LogSobolevAdmissible pi generator
      (InformationTheory.RNLogRatio.density mu pi))
    (hScore :
      InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hPair :
      InformationTheory.CanonicalDirichletFisher.DirichletPairDomain
        mu pi generator)
    (hGamma :
      InformationTheory.CanonicalDirichletFisher.HasCanonicalFisherGamma
        mu pi generator) :
    _root_.InformationTheory.klDiv mu pi ≠ ∞ ∧
      (_root_.InformationTheory.klDiv mu pi).toReal ≤
        (C / 2) *
          InformationTheory.CanonicalRelativeFisher.information mu pi hScore := by
  let _ : IsProbabilityMeasure pi := hLSI.1
  have hLogRatioIntegrable : Integrable (MeasureTheory.llr mu pi) mu := by
    rw [← MeasureTheory.integrable_rnDeriv_mul_log_iff
      hScore.absolutelyContinuous]
    simpa [InformationTheory.RNLogRatio.density] using
      hAdmissible.2.2.2.1
  have hFinite : _root_.InformationTheory.klDiv mu pi ≠ ∞ :=
    _root_.InformationTheory.klDiv_ne_top
      hScore.absolutelyContinuous hLogRatioIntegrable
  refine ⟨hFinite, ?_⟩
  have hApplied := hLSI.2.2
    (InformationTheory.RNLogRatio.density mu pi) hAdmissible
  have hEntropy :
      Generator.densityEntropy pi
          (InformationTheory.RNLogRatio.density mu pi) =
        (_root_.InformationTheory.klDiv mu pi).toReal := by
    unfold Generator.densityEntropy
    change
      (∫ x, (mu.rnDeriv pi x).toReal *
        Real.log (mu.rnDeriv pi x).toReal ∂pi) =
        (_root_.InformationTheory.klDiv mu pi).toReal
    rw [MeasureTheory.integral_rnDeriv_mul_log
      hScore.absolutelyContinuous]
    simpa [InformationTheory.RNLogRatio.logRatio] using
      (InformationTheory.RNLogRatio.toReal_klDiv_eq_integral_logRatio_of_probability
        mu pi hScore.absolutelyContinuous).symm
  have hDirichlet :
      Generator.dirichletForm pi generator
          (InformationTheory.RNLogRatio.density mu pi)
          (fun x => Real.log
            (InformationTheory.RNLogRatio.density mu pi x)) =
        InformationTheory.CanonicalRelativeFisher.information mu pi hScore := by
    rw [show
      (fun x => Real.log (InformationTheory.RNLogRatio.density mu pi x)) =
        InformationTheory.RNLogRatio.logRatio mu pi by
      funext x
      exact (InformationTheory.RNLogRatio.logRatio_apply mu pi x).symm]
    exact
      InformationTheory.CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_information
        mu pi generator hScore hPair hGamma
  rw [hEntropy, hDirichlet] at hApplied
  exact hApplied

end

end CanonicalLogSobolev
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

This theorem does not prove that any concrete Gibbs measure satisfies LSI.
It does not prove Bakry--Emery, Talagrand T2, Wasserstein contraction or an SPHMC/PBPS main theorem.
It does not derive canonical score differentiability from almost-everywhere agreement with an explicit representative.
KL finiteness comes from hAdmissible and is returned explicitly; toReal of infinity is never accepted as evidence.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integrable_rnDeriv_mul_log_iff
MeasureTheory.integral_rnDeriv_mul_log
InformationTheory.klDiv_ne_top

Mathematical sources

Sinho Chewi, Log-Concave Sampling, Definition 1.2.25 — Density-form generator log-Sobolev convention with coefficient C/2.
Lee--Shen--Tian, Lemma 2 — Uses the reciprocal curvature rate lambda, so C=lambda^{-1}; its Talagrand step is not part of this theorem.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

CanonicalLogSobolev: mathematical reading route

A canonical generator LSI gives finite KL and a Fisher bound

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Extract genuine KL finiteness

2. Apply LSI to the canonical density

3. Identify entropy with canonical KL

4. Identify Dirichlet energy with Fisher information

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources