Evaluate canonical KL with an explicit normalized tilt ratio
AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedKL.finite_klDiv_and_toReal_eq_integral_normalizedLogRatio · theorem · Teaching coverage
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.
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.
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)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.
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.
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.
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.
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.
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.
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.TiltedKLSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The source entropy/score proof manipulates normalized restricted-Gaussian density ratios. | A generic nonzero sigma-finite base, integrable exponential weights, measurable left exponent and explicit left-law L1 ratio. | source-implicit | These hypotheses make normalization, absolute continuity, canonical llr integrability and the real KL integral formula valid. |
| The source differentiates a displayed smooth representative. | This theorem uses a.e. equality only for integrability and integral congruence; it contains no derivative conclusion. | mathematically-necessary | Classical derivatives cannot be transported through arbitrary a.e. equality. |
Finite-KL and exact explicit integral only. Restricted-fiber integrability, score differentiation, LSI, Fisher, T2 and W2 contraction remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Lean proves the bridge for arbitrary normalized exponential tilts over a nonzero sigma-finite base rather than only restricted-Gaussian fibers. — Independent source review classification: domain-generalization; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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
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.