ASTIS mathematical exposition

An integrable exponential moment remains integrable at a smaller nonnegative scale

AutoSamplingTheory.dvFiniteLogMgfOfLeAlpha · theorem · Teaching coverage

Statement

Let μ be a finite measure on measurable Ω and q:Ω→ℝ any function. If exp(α₀q) is μ-integrable and 0≤α≤α₀, then exp(αq) is μ-integrable. No nonnegativity of q, probability normalization, or separate measurability premise for q is assumed.

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

All objects and hypotheses

Ω is measurable and μ is finite, possibly zero or unnormalized.
q:Ω→ℝ and α,α₀∈ℝ; the exponential at α₀ is integrable, and 0≤α≤α₀.

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. Use the zero-scale endpoint

For a finite measure the constant exponential at scale zero is integrable.

\[e^{0q}=1\in L^1(\mu).\]

Corresponding Lean step

zero endpoint supplied inside integrable_exp_mul_of_nonneg_of_le

2. Control all intermediate scales

The imported interval theorem bounds exp(αq) by 1+exp(α₀q): use the upper endpoint where q≥0 and the zero endpoint where q≤0. Its proof also derives the needed a.e. measurability from the endpoint hypotheses, treating the zero-length interval separately.

\[e^{\alpha q(\omega)}\le1+e^{\alpha_0q(\omega)}\qquad(0\le\alpha\le\alpha_0).\]

Corresponding Lean step

ProbabilityTheory.integrable_exp_mul_of_le_of_le: inspected proof background

3. Reuse the packaged moment theorem

Specialize the imported nonnegative-scale monotonicity result to q, upper scale α₀ and selected scale α.

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

Corresponding Lean step

ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le hAlpha0 hAlpha_nonneg hAlpha_le

Lean statement · dvFiniteLogMgfOfLeAlpha

The actual conclusion is integrability of an exponential. The theorem's name does not additionally assert a positive logarithm normalizer when μ is zero.

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 dvFiniteLogMgfOfLeAlpha {Ω : Type*} [MeasurableSpace Ω]
    {mu : Measure Ω} [IsFiniteMeasure mu]
    {q : Ω → Real} {alpha alpha0 : Real}
    (hAlpha0 : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0) :
    Integrable (fun x ↦ Real.exp (alpha * q x)) mu

Exact module and namespace context

Lean proof · dvFiniteLogMgfOfLeAlpha

The ASTIS body directly calls the imported moment theorem; the endpoint and domination steps explain its mathematical mechanism rather than a new local proof.

theorem dvFiniteLogMgfOfLeAlpha {Ω : Type*} [MeasurableSpace Ω]
    {mu : Measure Ω} [IsFiniteMeasure mu]
    {q : Ω → Real} {alpha alpha0 : Real}
    (hAlpha0 : Integrable (fun x ↦ Real.exp (alpha0 * q x)) mu)
    (hAlpha_nonneg : 0 ≤ alpha) (hAlpha_le : alpha ≤ alpha0) :
    Integrable (fun x ↦ Real.exp (alpha * q x)) mu := by
  exact ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le (X := q) (u := alpha0)
    (t := alpha) hAlpha0 hAlpha_nonneg hAlpha_le

/-- Mathlib-backed one-sided Donsker--Varadhan inequality via exponential tilting.

This proves only the admissible-test upper bound
`E_nu[Z] - log E_mu[exp Z] <= KL(nu || mu)` under explicit Mathlib
measure-theoretic hypotheses.  It is not the Boucheron supremum equality from
`appendix.tex:73-79`.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

This result establishes exponential integrability at an intermediate nonnegative scale, not a Donsker–Varadhan inequality or a variational supremum formula. Its later use in a selected-test bound is a separate consumer; no source-fidelity verdict is made.
For a probability target this supports a finite, positive exponential normalizer. For the allowed zero measure, the normalizer is zero, so do not read the title as an unqualified ordinary log-mgf statement.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le — 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.