Samplinglib mathematical lesson

Evaluate canonical KL with an explicit normalized tilt ratio

AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedKL.finite_klDiv_and_toReal_eq_integral_normalizedLogRatio · theorem · Teaching coverage

Read this first

Mathematical statement

Let mu be a nonzero sigma-finite measure and let f and g define integrable exponential tilts. If their displayed normalized log-density ratio is integrable under the left tilt, then the canonical KL divergence from the left tilt to the right tilt is finite, and its real value is exactly the left-tilt integral of that displayed ratio.

\[\mathrm{KL}(\mu_f\|\mu_g)<\infty,\qquad \mathrm{KL}(\mu_f\|\mu_g)=\int\!\left(f-\log Z_f-g+\log Z_g\right)\,d\mu_f.\]

Lean statement · finite_klDiv_and_toReal_eq_integral_normalizedLogRatio

The conclusion contains both the ENNReal finiteness certificate and the exact real integral identity. Its explicit integrability premise prevents toReal from silently collapsing infinity to zero.

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_eq_integral_normalizedLogRatio
    (mu : Measure X) [SigmaFinite mu] [NeZero mu] (f g : X → ℝ)
    (hf : Measurable f)
    (hfi : Integrable (fun x => Real.exp (f x)) mu)
    (hgi : Integrable (fun x => Real.exp (g x)) mu)
    (hrep : Integrable
      (fun x =>
        f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
          Real.log (∫ z, Real.exp (g z) ∂mu))
      (mu.tilted f)) :
    InformationTheory.klDiv (mu.tilted f) (mu.tilted g) ≠ ⊤ ∧
      (InformationTheory.klDiv (mu.tilted f) (mu.tilted g)).toReal =
        ∫ x,
          (f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
            Real.log (∫ z, Real.exp (g z) ∂mu)) ∂(mu.tilted f)

Exact module and namespace context

Proof roadmap

1Normalize the two tilts and obtain absolute continuity
Integrability of both exponential weights makes each tilt a probability measure. The left tilt is absolutely continuous with respect to the common base, and the base is absolutely continuous with respect to the right tilt; composing gives the KL direction.
2Transfer integrability only at the value level
The previously compiled representative theorem identifies Mathlib's canonical llr with the explicit normalized ratio almost everywhere under the left tilt. Therefore the assumed integrability of the explicit ratio implies integrability of the canonical llr.
3Certify finite canonical KL
Mathlib's finite-KL criterion requires precisely absolute continuity in the KL direction and integrability of its canonical llr. Both have now been proved.
4Replace the canonical llr integral by the smooth representative
Because both tilted measures have mass one, Mathlib's equal-mass KL formula has no extra mass correction. Almost-everywhere equality then changes the integrand without changing the integral.

Full assumptions and notation

All objects and hypotheses

The common base measure is sigma-finite and nonzero.
The left exponent f is measurable, and exp(f) and exp(g) are integrable under the base measure, so both normalized tilts are probability measures.
The explicit normalized ratio f-log Z_f-g+log Z_g is integrable under the left tilt. This real analytic obligation is not inferred merely from normalization.
No differentiability or gradient statement is used.

Mathematical proof

1. Normalize the two tilts and obtain absolute continuity

Integrability of both exponential weights makes each tilt a probability measure. The left tilt is absolutely continuous with respect to the common base, and the base is absolutely continuous with respect to the right tilt; composing gives the KL direction.

\[\mu_f\ll\mu\ll\mu_g\quad\Longrightarrow\quad\mu_f\ll\mu_g,\qquad \mu_f(X)=\mu_g(X)=1.\]

Corresponding Lean step

Use isProbabilityMeasure_tilted, tilted_absolutelyContinuous, absolutelyContinuous_tilted and trans.

2. Transfer integrability only at the value level

The previously compiled representative theorem identifies Mathlib's canonical llr with the explicit normalized ratio almost everywhere under the left tilt. Therefore the assumed integrability of the explicit ratio implies integrability of the canonical llr.

\[\operatorname{llr}(\mu_f,\mu_g)=f-\log Z_f-g+\log Z_g\quad\mu_f\text{-a.e.}\]

Corresponding Lean step

Apply Integrable.congr to TiltedLogRatio.llr_tilted_tilted_ae in the reverse direction.

3. Certify finite canonical KL

Mathlib's finite-KL criterion requires precisely absolute continuity in the KL direction and integrability of its canonical llr. Both have now been proved.

\[\mu_f\ll\mu_g\ \wedge\ \operatorname{llr}(\mu_f,\mu_g)\in L^1(\mu_f)\quad\Longrightarrow\quad\mathrm{KL}(\mu_f\|\mu_g)\ne\infty.\]

Corresponding Lean step

Invoke InformationTheory.klDiv_ne_top.

4. Replace the canonical llr integral by the smooth representative

Because both tilted measures have mass one, Mathlib's equal-mass KL formula has no extra mass correction. Almost-everywhere equality then changes the integrand without changing the integral.

\[\mathrm{KL}(\mu_f\|\mu_g)=\int\operatorname{llr}(\mu_f,\mu_g)\,d\mu_f=\int(f-\log Z_f-g+\log Z_g)\,d\mu_f.\]

Corresponding Lean step

Use InformationTheory.toReal_klDiv_of_measure_eq and integral_congr_ae.

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_eq_integral_normalizedLogRatio

Build probability instances for both tilts, compose absolute continuity, transfer L1 integrability through the existing a.e. representative theorem, then apply Mathlib's KL theorems and integral congruence.

Download module (.lean)

theorem finite_klDiv_and_toReal_eq_integral_normalizedLogRatio
    (mu : Measure X) [SigmaFinite mu] [NeZero mu] (f g : X → ℝ)
    (hf : Measurable f)
    (hfi : Integrable (fun x => Real.exp (f x)) mu)
    (hgi : Integrable (fun x => Real.exp (g x)) mu)
    (hrep : Integrable
      (fun x =>
        f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
          Real.log (∫ z, Real.exp (g z) ∂mu))
      (mu.tilted f)) :
    InformationTheory.klDiv (mu.tilted f) (mu.tilted g) ≠ ⊤ ∧
      (InformationTheory.klDiv (mu.tilted f) (mu.tilted g)).toReal =
        ∫ x,
          (f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
            Real.log (∫ z, Real.exp (g z) ∂mu)) ∂(mu.tilted f) := by
  let _ : IsProbabilityMeasure (mu.tilted f) := isProbabilityMeasure_tilted hfi
  let _ : IsProbabilityMeasure (mu.tilted g) := isProbabilityMeasure_tilted hgi
  have hae := TiltedLogRatio.llr_tilted_tilted_ae mu f g hf hfi hgi
  have hac : mu.tilted f ≪ mu.tilted g :=
    (tilted_absolutelyContinuous mu f).trans (absolutelyContinuous_tilted hgi)
  have hllr : Integrable (MeasureTheory.llr (mu.tilted f) (mu.tilted g))
      (mu.tilted f) :=
    hrep.congr hae.symm
  constructor
  · exact InformationTheory.klDiv_ne_top hac hllr
  · rw [InformationTheory.toReal_klDiv_of_measure_eq hac (by simp)]
    exact integral_congr_ae hae

end

end AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedKL

Exact module and namespace context

Scope and omitted-condition boundaries

The explicit ratio's integrability under the left fiber is an input, not a consequence of exponential-weight integrability alone.
Almost-everywhere equality is used for values, integrability and integrals only; it is not used to transport classical gradients.
The theorem does not prove the restricted-fiber score formula, relative Fisher energy, log-Sobolev inequality, Talagrand inequality, W2 contraction or SPHMC main theorem.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedLogRatio.llr_tilted_tilted_ae

Mathlib API called (external library)

MeasureTheory.isProbabilityMeasure_tilted
MeasureTheory.tilted_absolutelyContinuous
MeasureTheory.absolutelyContinuous_tilted
MeasureTheory.Integrable.congr
InformationTheory.klDiv_ne_top
InformationTheory.toReal_klDiv_of_measure_eq
MeasureTheory.integral_congr_ae

Mathematical sources

Lee, Shen and Tian, Lemma 2 — The entropy/LSI proof uses the explicit restricted-fiber log ratio and then computes its score; ASTIS isolates the canonical-KL representative interface.
Chen, Chewi, Lu and Zhang, SPHMC v1, Lemma 4.17 — The restricted-Gaussian contraction cites the prior argument. This declaration supplies only its KL representative bridge.

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