Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Exponential perturbation with the exact oscillation factor

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

Read this first

Mathematical statement

Let μ be a probability measure on any measurable space, B an almost-everywhere measurable real function, and l,u finite real bounds with l ≤ B ≤ u μ-almost everywhere. If C ≥ 0 and the finite-integral energy LSI holds under μ for fixed Γ,D with constant C, it holds for the normalized tilt dν = exp(B)/Z dμ with constant C exp(u-l). The proof derives integrability and positivity of Z, normalization, and both measure comparisons; it does not assume the perturbed LSI.

\[\nu=Z^{-1}e^B\mu,\quad l\le B\le u\quad\Longrightarrow\quad C_\nu\le C_\mu e^{u-l}.\]
Lean statement · energyLogSobolev_tilted

Let μ be a probability measure on any measurable space, B an almost-everywhere measurable real function, and l,u finite real bounds with l ≤ B ≤ u μ-almost everywhere. If C ≥ 0 and the finite-integral energy LSI holds under μ for fixed Γ,D with constant C, it holds for the normalized tilt dν = exp(B)/Z dμ with constant C exp(u-l). The proof derives integrability and positivity of Z, normalization, and both measure comparisons; it does not assume the perturbed LSI.

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_tilted {μ : Measure X} [IsProbabilityMeasure μ]
    {Γ : (X → ℝ) → X → ℝ} {admissible : (X → ℝ) → Prop} {C l u : ℝ} {B : X → ℝ}
    (hC : 0 ≤ C) (hB : AEMeasurable B μ)
    (hl : ∀ᵐ x ∂μ, l ≤ B x) (hu : ∀ᵐ x ∂μ, B x ≤ u)
    (hLS : EnergyLogSobolev μ Γ admissible C) :
    EnergyLogSobolev (μ.tilted B) Γ admissible (C * Real.exp (u - l))

Exact module and namespace context

Proof roadmap

  1. 1Construct the normalized probability law

    The upper bound B ≤ u bounds exp B by the integrable constant exp u. Measurability gives integrability, and the strictly positive exponential has positive integral, so Z is finite and positive and the normalized tilt is a probability measure.

  2. 2Prove both density comparisons

    The same Z occurs in both bounds. The upper density is exp u / Z; multiplying the tilted density by Z / exp l makes it at least one. Both comparisons follow by monotonicity of withDensity.

  3. 3Cancel the normalization constant

    Apply the general measure-comparison transfer. Its factor is the product of the two proved bounds; Z cancels exactly, leaving exp(u-l). The test class and energy density are unchanged.

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. Construct the normalized probability law

The upper bound B ≤ u bounds exp B by the integrable constant exp u. Measurability gives integrability, and the strictly positive exponential has positive integral, so Z is finite and positive and the normalized tilt is a probability measure.

\[0<Z=\int e^B\,d\mu<\infty.\]
Corresponding Lean step

Use Integrable.mono', integral_exp_pos and isProbabilityMeasure_tilted.

2. Prove both density comparisons

The same Z occurs in both bounds. The upper density is exp u / Z; multiplying the tilted density by Z / exp l makes it at least one. Both comparisons follow by monotonicity of withDensity.

\[\nu\le\frac{e^u}{Z}\mu,\qquad\mu\le\frac{Z}{e^l}\nu.\]
Corresponding Lean step

Use withDensity_mono, withDensity_const, withDensity_one and withDensity_smul'.

3. Cancel the normalization constant

Apply the general measure-comparison transfer. Its factor is the product of the two proved bounds; Z cancels exactly, leaving exp(u-l). The test class and energy density are unchanged.

\[C\frac Z{e^l}\frac{e^u}Z=Ce^{u-l}.\]
Corresponding Lean step

Apply energyLogSobolev_of_measure_comparison; use Real.exp_sub and field_simp with Z ≠ 0.

Lean verification

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

Lean proof · energyLogSobolev_tilted

See the adjacent exact source and the stepwise mathematical proof.

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_tilted {μ : Measure X} [IsProbabilityMeasure μ]
    {Γ : (X → ℝ) → X → ℝ} {admissible : (X → ℝ) → Prop} {C l u : ℝ} {B : X → ℝ}
    (hC : 0 ≤ C) (hB : AEMeasurable B μ)
    (hl : ∀ᵐ x ∂μ, l ≤ B x) (hu : ∀ᵐ x ∂μ, B x ≤ u)
    (hLS : EnergyLogSobolev μ Γ admissible C) :
    EnergyLogSobolev (μ.tilted B) Γ admissible (C * Real.exp (u - l)) := by
  have hExp : Integrable (fun x => Real.exp (B x)) μ :=
    (integrable_const (Real.exp u)).mono'
      (Real.measurable_exp.comp_aemeasurable hB).aestronglyMeasurable (by
        filter_upwards [hu] with x hx
        simpa only [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] using Real.exp_le_exp.mpr hx)
  have := isProbabilityMeasure_tilted hExp
  let Z := ∫ x, Real.exp (B x) ∂μ
  have hZ : 0 < Z := integral_exp_pos hExp
  have hupper : μ.tilted B ≤ ENNReal.ofReal (Real.exp u / Z) • μ := by
    rw [Measure.tilted, ← withDensity_const]
    apply withDensity_mono
    filter_upwards [hu] with x hx
    exact ENNReal.ofReal_le_ofReal (div_le_div_of_nonneg_right (Real.exp_le_exp.mpr hx) hZ.le)
  have hlower : μ ≤ ENNReal.ofReal (Z / Real.exp l) • μ.tilted B := by
    calc
      μ = μ.withDensity (fun _ => 1) := withDensity_one.symm
      _ ≤ μ.withDensity (fun x => ENNReal.ofReal (Z / Real.exp l) *
          ENNReal.ofReal (Real.exp (B x) / Z)) := by
        apply withDensity_mono
        filter_upwards [hl] with x hx
        rw [← ENNReal.ofReal_mul (by positivity)]
        have heq : (Z / Real.exp l) * (Real.exp (B x) / Z) =
            Real.exp (B x) / Real.exp l := by field_simp
        rw [heq, ← ENNReal.ofReal_one]
        exact ENNReal.ofReal_le_ofReal
          ((one_le_div (Real.exp_pos _)).2 (Real.exp_le_exp.mpr hx))
      _ = ENNReal.ofReal (Z / Real.exp l) • μ.tilted B :=
        withDensity_smul' _ _ ENNReal.ofReal_ne_top
  have hconst : C * (Z / Real.exp l) * (Real.exp u / Z) = C * Real.exp (u - l) := by
    rw [Real.exp_sub]
    field_simp [ne_of_gt hZ]
  rw [← hconst]
  exact energyLogSobolev_of_measure_comparison hC (by positivity) (by positivity)
    hlower hupper hLS

end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation

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

Mathlib API called (external library)

  • MeasureTheory.Integrable.mono'
  • MeasureTheory.integral_exp_pos
  • MeasureTheory.isProbabilityMeasure_tilted
  • MeasureTheory.withDensity_mono
  • MeasureTheory.withDensity_smul'
  • Real.exp_sub

Mathematical sources

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