Samplinglib mathematical lesson

Use an upper-scale exponential moment for the selected scaled test

AutoSamplingTheory.dvVariationalOneSidedOfScaledTest · theorem · Teaching coverage

Read this first

Mathematical statement

For the probability measures and hypotheses below, including integrability of the selected test αq under ν and an exponential moment at α₀ with 0≤α≤α₀, the selected-test DV bound holds at scale α. No positivity of q or strict positivity of α is needed.

\[\int\alpha q\,d\nu-\log\int e^{\alpha q}\,d\mu\le K.\]

Lean statement · dvVariationalOneSidedOfScaledTest

Integrability is assumed for αq itself, not for q. The scale may be zero, so those are genuinely different 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 dvVariationalOneSidedOfScaledTest {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 : Real}
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable (fun x ↦ alpha * q x) nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, alpha * q x ∂nu) - Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
      (klDiv nu mu).toReal

Exact module and namespace context

Proof roadmap

1Supply the selected exponential moment
The finite-measure moment theorem reduces the scale from α₀ to α.
2Apply the tilted selected-test theorem
Use Z=αq with the explicitly supplied absolute continuity, selected-test integrability and likelihood integrability.

Full assumptions and notation

All objects and hypotheses

Ω is measurable; ν and μ are probability measures with explicit SigmaFinite μ and SigmaFinite ν instances.
q:Ω→ℝ and α,α₀∈ℝ satisfy 0≤α≤α₀; ν≪μ.
The selected test αq is ν-integrable, exp(α₀q) is μ-integrable, and llr(ν,μ) is ν-integrable.
Write K=(klDiv ν μ).toReal and L_α=log∫exp(αq)dμ.

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. Supply the selected exponential moment

The finite-measure moment theorem reduces the scale from α₀ to α.

\[e^{\alpha_0q}\in L^1(\mu)\Longrightarrow e^{\alpha q}\in L^1(\mu).\]

Corresponding Lean step

dvFiniteLogMgfOfLeAlpha hexp_alpha0_mu hAlpha_nonneg hAlpha_le

2. Apply the tilted selected-test theorem

Use Z=αq with the explicitly supplied absolute continuity, selected-test integrability and likelihood integrability.

\[\mathbb E_\nu[\alpha q]-L_\alpha\le K.\]

Corresponding Lean step

dvVariationalOneSidedOfTiltedRight ... (Z := fun x ↦ alpha*q x)

Lean verification

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

Lean proof · dvVariationalOneSidedOfScaledTest

One reused theorem supplies the missing selected exponential moment and the other proves the one-sided inequality for that particular test.

Download module (.lean)

theorem dvVariationalOneSidedOfScaledTest {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 : Real}
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable (fun x ↦ alpha * q x) nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, alpha * q x ∂nu) - Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
      (klDiv nu mu).toReal := by
  have hexp_mu : Integrable (fun x ↦ Real.exp (alpha * q x)) mu :=
    dvFiniteLogMgfOfLeAlpha (mu := mu) (q := q) hexp_alpha0_mu hAlpha_nonneg
      hAlpha_le
  exact dvVariationalOneSidedOfTiltedRight (nu := nu) (mu := mu)
    (Z := fun x ↦ alpha * q x) hnu_mu hZ_nu hexp_mu hllr

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 q≥0 or α>0 hypothesis is added. No arbitrary-test supremum is taken.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha — Existing root ASTIS dependency; use its own adjacent teaching unit.
AutoSamplingTheory.dvVariationalOneSidedOfTiltedRight — Existing root ASTIS dependency; use its own adjacent teaching unit.

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