ASTIS mathematical exposition

Divide the scaled entropy bound by its positive scale

AutoSamplingTheory.dvVariationalScaledTestEnergyBound · theorem · Teaching coverage

Statement

Under the probability, absolute-continuity and integrability assumptions below, let 0<α≤α₀ and let e_α=α⁻¹log∫exp(αq)dμ. Then ∫q dν≤α⁻¹(klDiv ν μ).toReal+e_α. Although q may represent an energy in an application, this theorem does not require q≥0.

\[\int q\,d\nu\le\alpha^{-1}K+e_\alpha,\qquad e_\alpha=\alpha^{-1}\log\int e^{\alpha q}\,d\mu.\]

All objects and hypotheses

Ω is measurable; ν and μ are probability measures with explicit SigmaFinite μ and SigmaFinite ν instances.
q:Ω→ℝ is ν-integrable; α,α₀,e_α∈ℝ with 0<α≤α₀; ν≪μ.
exp(α₀q) is μ-integrable and llr(ν,μ) is ν-integrable.
The supplied named value e_α equals α⁻¹ log∫exp(αq)dμ. Write K=(klDiv ν μ).toReal.

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. Make the scaled test integrable

A constant multiple of the ν-integrable q is integrable, so αq satisfies the selected-test input.

\[q\in L^1(\nu)\Longrightarrow\alpha q\in L^1(\nu).\]

Corresponding Lean step

hq_nu.const_mul alpha; hZ_nu

2. Apply the selected scaled-test bound

The preceding theorem gives the variational inequality for αq, using the upper-scale exponential moment.

\[\int\alpha q\,d\nu-L_\alpha\le K.\]

Corresponding Lean step

dvVariationalOneSidedOfScaledTest

3. Move the constant and rearrange

Pull α out of the integral and move the log-mgf to the right.

\[\alpha\int q\,d\nu\le K+L_\alpha.\]

Corresponding Lean step

integral_const_mul; sub_le_iff_le_add.mp

4. Multiply by the positive inverse

Since α>0, its inverse is nonnegative, so multiplication preserves the inequality and α⁻¹α cancels.

\[\int q\,d\nu=\alpha^{-1}\alpha\int q\,d\nu\le\alpha^{-1}(K+L_\alpha).\]

Corresponding Lean step

mul_le_mul_of_nonneg_left; inv_nonneg; field_simp [ne_of_gt hAlpha_pos]

5. Identify the named log-mgf contribution

Distribute the inverse and replace its log-mgf term by the supplied e_α.

\[\alpha^{-1}(K+L_\alpha)=\alpha^{-1}K+e_\alpha.\]

Corresponding Lean step

rw [heAlpha]; ring

Lean statement · dvVariationalScaledTestEnergyBound

Strict positivity of α distinguishes this division theorem from the preceding α≥0 result. The value e_α is a real parameter tied to the log-mgf by an explicit equality.

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 dvVariationalScaledTestEnergyBound {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    (∫ x, q x ∂nu) ≤ alpha⁻¹ * (klDiv nu mu).toReal + eAlpha

Exact module and namespace context

Lean proof · dvVariationalScaledTestEnergyBound

The proof obtains the selected-test bound, uses linearity for one constant, divides by a verified positive scale, and rewrites the named complexity term.

theorem dvVariationalScaledTestEnergyBound {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hnu_mu : nu ≪ mu)
    (hq_nu : Integrable q nu)
    (hexp_alpha0_mu : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hllr : Integrable (llr nu mu) nu)
    (heAlpha : eAlpha =
      alpha⁻¹ * Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) :
    (∫ x, q x ∂nu) ≤ alpha⁻¹ * (klDiv nu mu).toReal + eAlpha := by
  have hZ_nu : Integrable (fun x ↦ alpha * q x) nu := by
    simpa [smul_eq_mul] using hq_nu.const_mul alpha
  have hdv := dvVariationalOneSidedOfScaledTest (nu := nu) (mu := mu)
    (q := q) hAlpha_pos.le hAlpha_le hnu_mu hZ_nu hexp_alpha0_mu hllr
  have hscaledIntegral :
      (∫ x, alpha * q x ∂nu) = alpha * ∫ x, q x ∂nu := by
    rw [integral_const_mul]
  have hscaled :
      alpha * (∫ x, q x ∂nu) ≤
        (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (alpha * q x) ∂mu) := by
    have hvar :
        alpha * (∫ x, q x ∂nu) -
            Real.log (∫ x, Real.exp (alpha * q x) ∂mu) ≤
          (klDiv nu mu).toReal := by
      simpa [hscaledIntegral] using hdv
    exact sub_le_iff_le_add.mp hvar
  have hdiv :
      alpha⁻¹ * (alpha * (∫ x, q x ∂nu)) ≤
        alpha⁻¹ * ((klDiv nu mu).toReal +
          Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) := by
    exact mul_le_mul_of_nonneg_left hscaled (inv_nonneg.mpr hAlpha_pos.le)
  calc
    (∫ x, q x ∂nu) = alpha⁻¹ * (alpha * (∫ x, q x ∂nu)) := by
      field_simp [ne_of_gt hAlpha_pos]
    _ ≤ alpha⁻¹ * ((klDiv nu mu).toReal +
          Real.log (∫ x, Real.exp (alpha * q x) ∂mu)) := hdiv
    _ = alpha⁻¹ * (klDiv nu mu).toReal + eAlpha := by
      rw [heAlpha]
      ring

/-- Coefficient-preserving energy form of the selected scaled-test DV bound.

This is the local algebraic shape used before Gronwall in SALD proofs after a
nonnegative prefactor, such as `(1/2)*dot{s}(t)^(-1)`, multiplies the
post-DV energy estimate.
-/

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 nonnegativity of q is required. It does not construct a complexity bound or prove a later Grönwall estimate.

Source and reuse

ASTIS parents called

AutoSamplingTheory.dvVariationalOneSidedOfScaledTest

Mathlib API called (external library)

MeasureTheory.Integrable.const_mul
MeasureTheory.integral_const_mul
sub_le_iff_le_add
mul_le_mul_of_nonneg_left
inv_nonneg

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.integral_const_mul — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
AutoSamplingTheory.dvVariationalOneSidedOfScaledTest — Existing root ASTIS dependency; use its own adjacent teaching unit.

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