Preserve an external nonnegative coefficient in the energy bound

AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff · theorem · Teaching coverage

Statement

Under the complete scaled-energy assumptions below, let c≥0 be any real coefficient. Then c∫q dν≤(cα⁻¹)(klDiv ν μ).toReal+c e_α. The coefficient may be zero and is independent of the integration variable.

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.
• c=coeff is a real scalar with hcoeff:0≤c.

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 dvVariationalScaledTestEnergyBoundWithCoeff {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha coeff : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hcoeff : 0 ≤ coeff)
    (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)) :
    coeff * (∫ x, q x ∂nu) ≤
      (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha

theorem dvVariationalScaledTestEnergyBoundWithCoeff {Ω : Type*} [MeasurableSpace Ω]
    (nu mu : Measure Ω) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (q : Ω → Real) {alpha alpha0 eAlpha coeff : Real}
    (hAlpha_pos : 0 < alpha) (hAlpha_le : alpha ≤ alpha0)
    (hcoeff : 0 ≤ coeff)
    (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)) :
    coeff * (∫ x, q x ∂nu) ≤
      (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha := by
  have hbase := dvVariationalScaledTestEnergyBound (nu := nu) (mu := mu)
    (q := q) hAlpha_pos hAlpha_le hnu_mu hq_nu hexp_alpha0_mu hllr heAlpha
  have hmul :
      coeff * (∫ x, q x ∂nu) ≤
        coeff * (alpha⁻¹ * (klDiv nu mu).toReal + eAlpha) := by
    exact mul_le_mul_of_nonneg_left hbase hcoeff
  calc
    coeff * (∫ x, q x ∂nu) ≤
        coeff * (alpha⁻¹ * (klDiv nu mu).toReal + eAlpha) := hmul
    _ = (coeff * alpha⁻¹) * (klDiv nu mu).toReal + coeff * eAlpha := by
      ring

/-- One-sided Donsker--Varadhan consequence from the tilted backend.

This is the form consumed by SALD after a selected test has supplied the
explicit Mathlib hypotheses.  It remains a one-sided theorem only; the
Boucheron supremum equality in `appendix.tex:73-79` stays 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.
• A scalar coefficient such as a time-change factor must have its sign established by the caller. No Grönwall, convergence or time-change theorem is proved here.