Samplinglib mathematical lesson

Transfer the same energy inequality between comparable probability laws

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.energyLogSobolev_of_measure_comparison · theorem · Teaching coverage

Read this first

Mathematical statement

Let μ and ν be probability measures on the same measurable space, with μ ≤ a ν and ν ≤ b μ for nonnegative finite real a,b. For the same energy density Γ and fixed test class D, an energy LSI under μ with C ≥ 0 transfers to ν with constant C a b. The conclusion covers exactly the finite-integral domain in the definition; reference-law test integrability is derived from target-law integrability.

\[\mu\le a\nu,\quad\nu\le b\mu\quad\Longrightarrow\quad C_\nu\le abC_\mu.\]

Lean statement · energyLogSobolev_of_measure_comparison

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.

Download module (.lean)

theorem energyLogSobolev_of_measure_comparison {μ ν : Measure X}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    {Γ : (X → ℝ) → X → ℝ} {admissible : (X → ℝ) → Prop} {C a b : ℝ}
    (hC : 0 ≤ C) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hμ : μ ≤ ENNReal.ofReal a • ν) (hν : ν ≤ ENNReal.ofReal b • μ)
    (hLS : EnergyLogSobolev μ Γ admissible C) :
    EnergyLogSobolev ν Γ admissible (C * a * b)

Exact module and namespace context

Proof roadmap

1Keep the test class and energy fixed
Start with any target-law finite-integral test in D. Domination μ ≤ a ν derives all three reference-law integrability conditions, and absolute continuity transports nonnegativity of the energy.
2Transfer entropy and energy in opposite directions
Apply the compiled entropy comparison, the reference LSI, and the integral comparison of the nonnegative energy. Nonnegativity of b and C licenses multiplication of inequalities.

Full assumptions and notation

All objects and hypotheses

Objects, quantifiers, constants and all finite-integral restrictions are stated in the adjacent statement and exact Lean.
The test predicate and energy density are fixed before changing the measure; no differential operator is transported.

Mathematical proof

1. Keep the test class and energy fixed

Start with any target-law finite-integral test in D. Domination μ ≤ a ν derives all three reference-law integrability conditions, and absolute continuity transports nonnegativity of the energy.

\[\mu\le a\nu\quad\Longrightarrow\quad L^1(\nu)\subseteq L^1(\mu).\]

Corresponding Lean step

Apply Integrable.smul_measure, mono_measure and AbsolutelyContinuous.ae_le.

2. Transfer entropy and energy in opposite directions

Apply the compiled entropy comparison, the reference LSI, and the integral comparison of the nonnegative energy. Nonnegativity of b and C licenses multiplication of inequalities.

\[\operatorname{Ent}_\nu(f^2)\le b\operatorname{Ent}_\mu(f^2)\le2bC\int\Gamma(f)\,d\mu\le2abC\int\Gamma(f)\,d\nu.\]

Corresponding Lean step

Call entropy_le_mul_of_measure_le and integral_mono_measure; the remaining rearrangement is ring arithmetic.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · energyLogSobolev_of_measure_comparison

See the adjacent exact source and the stepwise mathematical proof.

Download module (.lean)

theorem energyLogSobolev_of_measure_comparison {μ ν : Measure X}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    {Γ : (X → ℝ) → X → ℝ} {admissible : (X → ℝ) → Prop} {C a b : ℝ}
    (hC : 0 ≤ C) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hμ : μ ≤ ENNReal.ofReal a • ν) (hν : ν ≤ ENNReal.ofReal b • μ)
    (hLS : EnergyLogSobolev μ Γ admissible C) :
    EnergyLogSobolev ν Γ admissible (C * a * b) := by
  intro f hfAd hf hflog hΓ hΓ0
  have hfμ := (hf.smul_measure ENNReal.ofReal_ne_top).mono_measure hμ
  have hflogμ := (hflog.smul_measure ENNReal.ofReal_ne_top).mono_measure hμ
  have hΓμ := (hΓ.smul_measure ENNReal.ofReal_ne_top).mono_measure hμ
  have hΓμ0 : 0 ≤ᵐ[μ] Γ f :=
    (Measure.absolutelyContinuous_of_le_smul hμ).ae_le hΓ0
  have hE : (∫ x, Γ f x ∂μ) ≤ a * ∫ x, Γ f x ∂ν := by
    calc
      _ ≤ ∫ x, Γ f x ∂(ENNReal.ofReal a • ν) :=
        integral_mono_measure hμ (Measure.ae_smul_measure hΓ0 _)
          (hΓ.smul_measure ENNReal.ofReal_ne_top)
      _ = _ := by rw [integral_smul_measure, ENNReal.toReal_ofReal ha, smul_eq_mul]
  calc
    entropy ν (fun x => (f x) ^ 2) ≤ b * entropy μ (fun x => (f x) ^ 2) :=
      entropy_le_mul_of_measure_le hb hν (Eventually.of_forall fun x => sq_nonneg _)
        hfμ hflogμ
    _ ≤ b * (2 * C * ∫ x, Γ f x ∂μ) :=
      mul_le_mul_of_nonneg_left (hLS f hfAd hfμ hflogμ hΓμ hΓμ0) hb
    _ ≤ b * (2 * C * (a * ∫ x, Γ f x ∂ν)) :=
      mul_le_mul_of_nonneg_left
        (mul_le_mul_of_nonneg_left hE (by positivity)) hb
    _ = 2 * (C * a * b) * ∫ x, Γ f x ∂ν := by ring

Exact module and namespace context

Scope and omitted-condition boundaries

Real-integral domain only; the extended-real entropy and arbitrary Sobolev closure are not supplied.
No geometric base LSI, gradient identification, PI, T2, diffusion, or model theorem is supplied.
No public manuscript identity or private application data is part of this contribution.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.entropy_le_mul_of_measure_le

Mathlib API called (external library)

MeasureTheory.integral_mono_measure
MeasureTheory.Integrable.smul_measure
MeasureTheory.Integrable.mono_measure
MeasureTheory.Measure.absolutelyContinuous_of_le_smul

Mathematical sources

Chewi, Log-Concave Sampling, August20 2026, §2.3.1 — Classical variational-cost and bounded-perturbation proof background; only the displayed canonical finite-integral core is asserted.

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