Samplinglib mathematical lesson
Prove the selected-test entropy bound by exponential tilting
AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight · theorem · Teaching coverage
Read this first
Mathematical statement
For probability measures ν≪μ on a common measurable space, retain the explicit sigma-finiteness hypotheses and assume Z∈L¹(ν), exp Z∈L¹(μ), and llr(ν,μ)∈L¹(ν). Then ∫Z dν−log∫exp Z dμ≤(klDiv ν μ).toReal. These assumptions keep the selected normalizer positive and finite and put KL in its finite branch.
\[\int Z\,d\nu-\log\int e^Z\,d\mu\le K,\qquad K=(\mathrm{klDiv}(\nu,\mu))_{\mathrm{toReal}}.\]
Lean statement · dvVariationalOneSidedOfTiltedRight
The target is a real inequality using toReal of the extended KL divergence. The test and likelihood integrability assumptions are essential analytic hypotheses, not metadata.
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 dvVariationalOneSidedOfTiltedRight {α : Type*} [MeasurableSpace α]
(nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
[SigmaFinite mu] [SigmaFinite nu]
(Z : α → Real)
(hnu_mu : nu ≪ mu)
(hZ_nu : Integrable Z nu)
(hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
(hllr : Integrable (llr nu mu) nu) :
(∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
(klDiv nu mu).toReal
Exact module and namespace context
Proof roadmap
- 1Build a genuine tilted probability measure
Define μ_Z by density exp Z/M_Z against μ. Because μ is nonzero and exp Z is integrable and strictly positive, its normalizer is positive and finite, and Mathlib proves μ_Z is a probability measure.
- 2Transfer absolute continuity to the tilted target
The positive exponential tilt dominates μ in the absolute-continuity sense; combine μ≪μ_Z with ν≪μ.
- 3Check integrability and use entropy nonnegativity
The original test and log-likelihood integrability imply llr(ν,μ_Z) is ν-integrable. Gibbs' inequality includes total-mass correction terms; they cancel because ν and μ_Z are both probability measures.
- 4Rewrite the tilted log-likelihood integral
The imported tilt identity subtracts the test expectation and adds the logarithm of its normalizer to the original log-likelihood integral.
- 5Rearrange the nonnegative expression
The previous two lines imply the test's variational value is at most the original log-likelihood integral.
- 6Identify the real KL value
Absolute continuity and equal total masses give the toReal KL identity; substitute it into the bound. The explicit integrability hypotheses prevent this application from concealing infinite KL behind toReal(∞)=0.
Full assumptions and notation
All objects and hypotheses
- α (or Ω) is an arbitrary measurable space; ν and μ are probability measures on that same space.
- Both SigmaFinite μ and SigmaFinite ν are explicitly present in the Lean signature; probability already supplies them, but they are not omitted here.
- ν≪μ; the chosen real test Z is ν-integrable; exp Z is μ-integrable; llr(ν,μ) is ν-integrable.
- Notation: ℓ=llr(ν,μ)=log((dν/dμ).toReal), M_Z=∫exp Z dμ, and K=(InformationTheory.klDiv ν μ).toReal.
- Z is an arbitrary real-valued function on the common space; no pointwise boundedness or smoothness is assumed.
Notation and interpretation
- A.e. and strong measurability
A.e. means outside a μ-null set. AEMeasurable means equality a.e. to a measurable map; AEStronglyMeasurable (abbreviated AESM) means equality a.e. to a strongly measurable function, which is approximable by simple functions.
\[f=g\quad\mu\text{-a.e.}\]
- Integrability and Bochner integrals
L¹ in the teaching formulas means Integrable, not a newly defined quotient-space element. ∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
\[f\in L^1(\mu)\quad\Longleftrightarrow\quad f\text{ is a.e. strongly measurable and }\int^{\!-}\|f\|\,d\mu<\infty\]
Mathematical proof
1. Build a genuine tilted probability measure
Define μ_Z by density exp Z/M_Z against μ. Because μ is nonzero and exp Z is integrable and strictly positive, its normalizer is positive and finite, and Mathlib proves μ_Z is a probability measure.
\[d\mu_Z=M_Z^{-1}e^Z\,d\mu,\qquad0<M_Z<\infty,\qquad\mu_Z(\alpha)=1.\]
Corresponding Lean step
isProbabilityMeasure_tilted hexp_mu
2. Transfer absolute continuity to the tilted target
The positive exponential tilt dominates μ in the absolute-continuity sense; combine μ≪μ_Z with ν≪μ.
\[\nu\ll\mu\ll\mu_Z\Longrightarrow\nu\ll\mu_Z.\]
Corresponding Lean step
absolutelyContinuous_tilted hexp_mu; hnu_mu.trans hmu_tilted
3. Check integrability and use entropy nonnegativity
The original test and log-likelihood integrability imply llr(ν,μ_Z) is ν-integrable. Gibbs' inequality includes total-mass correction terms; they cancel because ν and μ_Z are both probability measures.
\[0\le\int\ell_{\nu,\mu_Z}\,d\nu+\mu_Z(\alpha)-\nu(\alpha)=\int\ell_{\nu,\mu_Z}\,d\nu.\]
Corresponding Lean step
integrable_llr_tilted_right; integral_llr_add_sub_measure_univ_nonneg; simpa
4. Rewrite the tilted log-likelihood integral
The imported tilt identity subtracts the test expectation and adds the logarithm of its normalizer to the original log-likelihood integral.
\[\int\ell_{\nu,\mu_Z}\,d\nu=\int\ell_{\nu,\mu}\,d\nu-\int Z\,d\nu+\log M_Z.\]
Corresponding Lean step
integral_llr_tilted_right hnu_mu hZ_nu hexp_mu hllr
5. Rearrange the nonnegative expression
The previous two lines imply the test's variational value is at most the original log-likelihood integral.
\[\int Z\,d\nu-\log M_Z\le\int\ell_{\nu,\mu}\,d\nu.\]
Corresponding Lean step
hnonneg_rewrite; linarith
6. Identify the real KL value
Absolute continuity and equal total masses give the toReal KL identity; substitute it into the bound. The explicit integrability hypotheses prevent this application from concealing infinite KL behind toReal(∞)=0.
\[K=\int\ell_{\nu,\mu}\,d\nu,\qquad\int Z\,d\nu-\log M_Z\le K.\]
Corresponding Lean step
toReal_klDiv_of_measure_eq hnu_mu (by simp); simpa [hkl] using hineq
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · dvVariationalOneSidedOfTiltedRight
The proof introduces the tilted probability instance, proves absolute continuity to it, applies nonnegativity of the tilted log-likelihood integral, expands that integral, and rearranges before identifying KL.
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 dvVariationalOneSidedOfTiltedRight {α : Type*} [MeasurableSpace α]
(nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
[SigmaFinite mu] [SigmaFinite nu]
(Z : α → Real)
(hnu_mu : nu ≪ mu)
(hZ_nu : Integrable Z nu)
(hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
(hllr : Integrable (llr nu mu) nu) :
(∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
(klDiv nu mu).toReal := by
let : IsProbabilityMeasure (mu.tilted Z) := isProbabilityMeasure_tilted hexp_mu
have hmu_tilted : mu ≪ mu.tilted Z := absolutelyContinuous_tilted hexp_mu
have hnu_tilted : nu ≪ mu.tilted Z := hnu_mu.trans hmu_tilted
have hllr_tilted : Integrable (llr nu (mu.tilted Z)) nu :=
integrable_llr_tilted_right (μ := nu) (ν := mu) (f := Z) hnu_mu hZ_nu hllr
hexp_mu
have hnonneg := integral_llr_add_sub_measure_univ_nonneg (μ := nu) (ν := mu.tilted Z)
hnu_tilted hllr_tilted
have hnonneg_llr : 0 ≤ ∫ x, llr nu (mu.tilted Z) x ∂nu := by
simpa using hnonneg
have htilted :=
integral_llr_tilted_right (μ := nu) (ν := mu) (f := Z) hnu_mu hZ_nu hexp_mu
hllr
have hnonneg_rewrite :
0 ≤ (∫ x, llr nu mu x ∂nu) - (∫ x, Z x ∂nu) +
Real.log (∫ x, Real.exp (Z x) ∂mu) := by
simpa [htilted] using hnonneg_llr
have hineq :
(∫ x, Z x ∂nu) - Real.log (∫ x, Real.exp (Z x) ∂mu) ≤
∫ x, llr nu mu x ∂nu := by
linarith
have hkl : (klDiv nu mu).toReal = ∫ x, llr nu mu x ∂nu := by
simpa using toReal_klDiv_of_measure_eq (μ := nu) (ν := mu) hnu_mu (by simp)
simpa [hkl] using hineq
Exact module and namespace context
Scope and omitted-condition boundaries
- Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
- No supremum equality, optimizer characterization or equality case is proved. The assumptions are not replaceable by merely finite-looking totalized integrals.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.isProbabilityMeasure_tilted
- MeasureTheory.absolutelyContinuous_tilted
- MeasureTheory.Measure.AbsolutelyContinuous.trans
- MeasureTheory.integrable_llr_tilted_right
- InformationTheory.integral_llr_add_sub_measure_univ_nonneg
- MeasureTheory.integral_llr_tilted_right
- InformationTheory.toReal_klDiv_of_measure_eq
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.