Preserve an external nonnegative coefficient in the energy bound
AutoSamplingTheory.dvVariationalScaledTestEnergyBoundWithCoeff · theorem · Teaching coverage
Mathematical 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.
Lean statement · dvVariationalScaledTestEnergyBoundWithCoeff
The new coefficient is a real number with an explicit nonnegative sign proof. No inverse of c is used, so c=0 is allowed.
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 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 * eAlphaProof roadmap
- 1Reuse the unweighted energy inequality
All measure-theoretic hypotheses are passed unchanged to the existing positive-scale result.
- 2Multiply by a nonnegative scalar
The sign assumption on c ensures multiplication preserves the order.
- 3Distribute while keeping the coefficient visible
Associativity and distributivity give the desired coefficient grouping.
Full assumptions and notation
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
1. Reuse the unweighted energy inequality
All measure-theoretic hypotheses are passed unchanged to the existing positive-scale result.
Corresponding Lean step
dvVariationalScaledTestEnergyBound ...
2. Multiply by a nonnegative scalar
The sign assumption on c ensures multiplication preserves the order.
Corresponding Lean step
mul_le_mul_of_nonneg_left hbase hcoeff
3. Distribute while keeping the coefficient visible
Associativity and distributivity give the desired coefficient grouping.
Corresponding Lean step
ring
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · dvVariationalScaledTestEnergyBoundWithCoeff
The proof invokes the already proved energy bound, multiplies its two sides, then normalizes the algebraic grouping.
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 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
ringScope 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- mul_le_mul_of_nonneg_left
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
- AutoSamplingTheory.dvVariationalScaledTestEnergyBound — 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.