ASTIS mathematical exposition

Prove the selected-test entropy bound by exponential tilting

AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight · theorem · Teaching coverage

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}}.\]

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 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

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.

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

/-- One-sided DV inequality for a SALD-style scaled selected test.

This packages the theorem-instance side conditions for tests of the form
`Z = alpha * q`.  The `alpha0` exponential-moment assumption supplies the
finite-log-mgf hypothesis by `dvFiniteLogMgfOfLeAlpha`, and the remaining
absolute-continuity, selected-test integrability, and log-likelihood
integrability hypotheses are kept explicit.  The Boucheron supremum equality
from `appendix.tex:73-79` remains source-cited.
-/

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.

Source and reuse

ASTIS 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

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.isProbabilityMeasure_tilted — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.absolutelyContinuous_tilted — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.integrable_llr_tilted_right — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
InformationTheory.integral_llr_add_sub_measure_univ_nonneg — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.integral_llr_tilted_right — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
InformationTheory.toReal_klDiv_of_measure_eq — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

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