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

AutoSamplingTheory.dvVariationalOneSidedOfScaledTest · theorem · Teaching coverage

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.

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

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

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

/-- Energy form of the one-sided DV bound for a scaled selected test.

For SALD use sites, `q` is a squared velocity or residual norm.  This theorem
starts after the selected-test hypotheses have been supplied, applies the
compiled one-sided backend for `Z=alpha*q`, divides by `alpha > 0`, and
rewrites the log-mgf quotient as the supplied alpha-complexity density
`eAlpha`.  The Boucheron supremum equality from `appendix.tex:73-79` remains
source-cited.
-/

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.