Write the tilted-backend test bound in additive form

AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence · theorem · Teaching coverage

Statement

For probability measures ν≪μ with the explicit sigma-finiteness hypotheses, if Z is ν-integrable, exp Z is μ-integrable and llr(ν,μ) is ν-integrable, then ∫Z dν≤(klDiv ν μ).toReal+log∫exp Z dμ. This is the additive form of the already proved selected-test inequality.

All objects and hypotheses

• α (or Ω) is an arbitrary measurable space; ν and μ are probability measures on that same space.
• Both SigmaFinite μ and SigmaFinite ν are explicitly present in the Lean signature; probability already supplies them, but they are not omitted here.
• ν≪μ; the chosen real test Z is ν-integrable; exp Z is μ-integrable; llr(ν,μ) is ν-integrable.
• Notation: ℓ=llr(ν,μ)=log((dν/dμ).toReal), M_Z=∫exp Z dμ, and K=(InformationTheory.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

theorem dvVariationalTiltedRightOneSidedConsequence {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) ≤
      (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (Z x) ∂mu)

theorem dvVariationalTiltedRightOneSidedConsequence {α : Type*} [MeasurableSpace α]
    (nu mu : Measure α) [IsProbabilityMeasure nu] [IsProbabilityMeasure mu]
    [SigmaFinite mu] [SigmaFinite nu]
    (Z : α → Real)
    (hnu_mu : nu ≪ mu)
    (hZ_nu : Integrable Z nu)
    (hexp_mu : Integrable (fun x ↦ Real.exp (Z x)) mu)
    (hllr : Integrable (llr nu mu) nu) :
    (∫ x, Z x ∂nu) ≤
      (klDiv nu mu).toReal + Real.log (∫ x, Real.exp (Z x) ∂mu) := by
  exact dvVariationalOneSidedConsequenceScalar
    (dvVariationalOneSidedOfTiltedRight (nu := nu) (mu := mu) (Z := Z)
      hnu_mu hZ_nu hexp_mu hllr)

/-- Log-Sobolev implies KL-FI comparison as a reusable proof target. -/

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.
• Additive-form reuse wrapper, not a new variational principle.