Bounded changes of measure: the finite-integral entropy and energy core
Classical Holley–Stroock mechanism; source exposition by Sinho Chewi. These generic library interfaces are not a claim that the complete geometric proposition has been formalized.
August20 2026 · §2.3.1, Proposition2.3.1 proof and entropy-cost display, printed pp60–61 · licensed original
Complete source statement (Samplinglib restatement)
For a fixed class of finite-integral tests and a fixed nonnegative energy density, bounded comparison of probability laws transfers entropy and its energy inequality. A bounded exponential tilt has exact transfer factor exp(u-l); normalization and target-law integrability are proved. Geometric base inequalities and extension to larger functional domains remain separate.
- Both laws in the comparison theorem are probability measures.
- All real entropy tests and energy tests use precisely the finite-integral domain of the displayed definition.
- The energy density and test predicate remain fixed as the measure changes.
entropy comparison
\[\nu\le b\mu\quad\Longrightarrow\quad\operatorname{Ent}_\nu(g)\le b\operatorname{Ent}_\mu(g).\]
energy inequality transfer
\[\mu\le a\nu,\quad\nu\le b\mu\quad\Longrightarrow\quad C_\nu\le abC_\mu.\]
exponential factor
\[\nu=Z^{-1}e^B\mu,\quad l\le B\le u\quad\Longrightarrow\quad C_\nu\le C_\mu e^{u-l}.\]
Read the formalized proofs
Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.
Samplinglib mathematical lesson
Finite-integral function entropy
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.entropy · def · Teaching coverage
Read this first
Mathematical statement
For a measurable space X, a measure m, and a real function g, define its real function entropy by the difference of the integral of g log g and the mean of g times the logarithm of that mean. Applications below impose integrability explicitly; this literal real formula is not an extended-real entropy.
\[\operatorname{Ent}_\mu(g)=\int g\log g\,d\mu-m\log m,\qquad m=\int g\,d\mu.\]
Lean statement · entropy
For a measurable space X, a measure m, and a real function g, define its real function entropy by the difference of the integral of g log g and the mean of g times the logarithm of that mean. Applications below impose integrability explicitly; this literal real formula is not an extended-real entropy.
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.
noncomputable def entropy (μ : Measure X) (g : X → ℝ) : ℝ
Exact module and namespace context
Proof roadmap
- 1Use the literal real formula
For a measurable space X, a measure m, and a real function g, define its real function entropy by the difference of the integral of g log g and the mean of g times the logarithm of that mean. Applications below impose integrability explicitly; this literal real formula is not an extended-real entropy.
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.
Construction and meaning
1. Use the literal real formula
For a measurable space X, a measure m, and a real function g, define its real function entropy by the difference of the integral of g log g and the mean of g times the logarithm of that mean. Applications below impose integrability explicitly; this literal real formula is not an extended-real entropy.
\[\operatorname{Ent}_\mu(g)=\int g\log g\,d\mu-m\log m,\qquad m=\int g\,d\mu.\]
Corresponding Lean step
The complete definition body is displayed in the adjacent folded Lean disclosure.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · entropy
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.
noncomputable def entropy (μ : Measure X) (g : X → ℝ) : ℝ :=
(∫ x, g x * Real.log (g x) ∂μ) - (∫ x, g x ∂μ) * Real.log (∫ x, g x ∂μ)
Exact module and namespace context
Source assumptions versus formal assumptions
Canonical finite-integral interface only. Full geometric test-class and Sobolev extension remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: Identifying this totalized expression with classical function entropy requires the intended nonnegative finite-integral domain. This node alone proves no infimum identity or entropy comparison. — Current canonical source statement, full implementation, independent reconstruction, and candidate prose explicitly limit the claim to the supporting finite-integral core. The separate geometric-source-application obligation has no proof binding.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
No direct Mathlib call recorded; see the Samplinglib parents.
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.
Samplinglib mathematical lesson
An energy LSI on a fixed class of finite-integral tests
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.EnergyLogSobolev · def · Teaching coverage
Read this first
Mathematical statement
Fix a measurable space X, a measure m, a real energy density Γ(f)(x), a test-function predicate D(f), and C. The finite-integral energy LSI means: every D-test f for which f², f² log(f²), and Γ(f) are integrable, with Γ(f) nonnegative almost everywhere, satisfies Ent_m(f²) ≤ 2 C ∫Γ(f) dm. It asserts no integrability outside those tests.
\[\operatorname{Ent}_\mu(f^2)\le 2C\int\Gamma(f)\,d\mu,\qquad f\in D\text{ in the finite-integral domain}.\]
Lean statement · EnergyLogSobolev
Fix a measurable space X, a measure m, a real energy density Γ(f)(x), a test-function predicate D(f), and C. The finite-integral energy LSI means: every D-test f for which f², f² log(f²), and Γ(f) are integrable, with Γ(f) nonnegative almost everywhere, satisfies Ent_m(f²) ≤ 2 C ∫Γ(f) dm. It asserts no integrability outside those tests.
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.
def EnergyLogSobolev (μ : Measure X) (Γ : (X → ℝ) → X → ℝ)
(admissible : (X → ℝ) → Prop) (C : ℝ) : Prop
Exact module and namespace context
Proof roadmap
- 1Use the literal real formula
Fix a measurable space X, a measure m, a real energy density Γ(f)(x), a test-function predicate D(f), and C. The finite-integral energy LSI means: every D-test f for which f², f² log(f²), and Γ(f) are integrable, with Γ(f) nonnegative almost everywhere, satisfies Ent_m(f²) ≤ 2 C ∫Γ(f) dm. It asserts no integrability outside those tests.
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.
Construction and meaning
1. Use the literal real formula
Fix a measurable space X, a measure m, a real energy density Γ(f)(x), a test-function predicate D(f), and C. The finite-integral energy LSI means: every D-test f for which f², f² log(f²), and Γ(f) are integrable, with Γ(f) nonnegative almost everywhere, satisfies Ent_m(f²) ≤ 2 C ∫Γ(f) dm. It asserts no integrability outside those tests.
\[\operatorname{Ent}_\mu(f^2)\le 2C\int\Gamma(f)\,d\mu,\qquad f\in D\text{ in the finite-integral domain}.\]
Corresponding Lean step
The complete definition body is displayed in the adjacent folded Lean disclosure.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · EnergyLogSobolev
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.
def EnergyLogSobolev (μ : Measure X) (Γ : (X → ℝ) → X → ℝ)
(admissible : (X → ℝ) → Prop) (C : ℝ) : Prop :=
∀ f : X → ℝ,
admissible f →
Integrable (fun x => (f x) ^ 2) μ →
Integrable (fun x => (f x) ^ 2 * Real.log ((f x) ^ 2)) μ →
Integrable (Γ f) μ →
(0 ≤ᵐ[μ] Γ f) →
entropy μ (fun x => (f x) ^ 2) ≤ 2 * C * ∫ x, Γ f x ∂μ
Exact module and namespace context
Source assumptions versus formal assumptions
Canonical finite-integral interface only. Full geometric test-class and Sobolev extension remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: Nonvacuity, a specific gradient energy, a useful test class, and equivalence or extension to a Sobolev-domain LSI require separate results. — Current canonical source statement, full implementation, independent reconstruction, and candidate prose explicitly limit the claim to the supporting finite-integral core. The separate geometric-source-application obligation has no proof binding.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
No direct Mathlib call recorded; see the Samplinglib parents.
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.
Samplinglib mathematical lesson
Compare entropy under a bounded change of probability law
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation.entropy_le_mul_of_measure_le · theorem · Teaching coverage
Read this first
Mathematical statement
Let μ and ν be probability measures on the same measurable space. If b ≥ 0, ν ≤ b μ, and g is nonnegative μ-almost everywhere with g and g log g μ-integrable, then Ent_ν(g) ≤ b Ent_μ(g). Integrability under ν is derived, including the zero-mean case.
\[\nu\le b\mu\quad\Longrightarrow\quad\operatorname{Ent}_\nu(g)\le b\operatorname{Ent}_\mu(g).\]
Lean statement · entropy_le_mul_of_measure_le
Let μ and ν be probability measures on the same measurable space. If b ≥ 0, ν ≤ b μ, and g is nonnegative μ-almost everywhere with g and g log g μ-integrable, then Ent_ν(g) ≤ b Ent_μ(g). Integrability under ν is derived, including the zero-mean case.
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 entropy_le_mul_of_measure_le {μ ν : Measure X}
[IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {g : X → ℝ} {b : ℝ}
(hb : 0 ≤ b) (hν : ν ≤ ENNReal.ofReal b • μ)
(hg0 : 0 ≤ᵐ[μ] g) (hg : Integrable g μ)
(hlog : Integrable (fun x => g x * Real.log (g x)) μ) :
entropy ν g ≤ b * entropy μ g
Exact module and namespace context
Proof roadmap
- 1Use a nonnegative scalar cost
For s ≥ 0 and t > 0, the logarithm inequality gives Φ_t(s) = s log(s/t)-s+t ≥ 0. The case s=0 is handled separately, so no strict positivity of the test is assumed.
- 2Separate entropy from the cost at the mean
Linearity of the integrable terms and probability mass one give an exact identity. The cost at the target mean is nonnegative, hence every positive t is an upper bound on entropy.
- 3Compare the nonnegative costs under the two laws
Measure domination transports integrability and compares the integral of the nonnegative cost. Choose t equal to the positive reference mean; its reference cost at the mean vanishes.
- 4Discharge zero mean
A nonnegative integrable function with zero integral vanishes almost everywhere. Absolute continuity transfers this to the target law, so both displayed real entropies equal zero.
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. Use a nonnegative scalar cost
For s ≥ 0 and t > 0, the logarithm inequality gives Φ_t(s) = s log(s/t)-s+t ≥ 0. The case s=0 is handled separately, so no strict positivity of the test is assumed.
\[\Phi_t(s)=s\log(s/t)-s+t\ge0.\]
Corresponding Lean step
cost_nonneg uses Real.log_le_sub_one_of_pos and a zero split.
2. Separate entropy from the cost at the mean
Linearity of the integrable terms and probability mass one give an exact identity. The cost at the target mean is nonnegative, hence every positive t is an upper bound on entropy.
\[\int\Phi_t(g)\,d\mu=\operatorname{Ent}_\mu(g)+\Phi_t\!\left(\int g\,d\mu\right).\]
Corresponding Lean step
integrable_cost, integral_cost and entropy_le_integral_cost are private providers.
3. Compare the nonnegative costs under the two laws
Measure domination transports integrability and compares the integral of the nonnegative cost. Choose t equal to the positive reference mean; its reference cost at the mean vanishes.
\[\operatorname{Ent}_\nu(g)\le\int\Phi_m(g)\,d\nu\le b\int\Phi_m(g)\,d\mu=b\operatorname{Ent}_\mu(g).\]
Corresponding Lean step
Use integral_mono_measure after Integrable.smul_measure and mono_measure.
4. Discharge zero mean
A nonnegative integrable function with zero integral vanishes almost everywhere. Absolute continuity transfers this to the target law, so both displayed real entropies equal zero.
\[\int g\,d\mu=0\quad\Longrightarrow\quad g=0\quad\mu\text{-a.e. and }\nu\text{-a.e.}\]
Corresponding Lean step
Use integral_eq_zero_iff_of_nonneg_ae and absolutelyContinuous_of_le_smul.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · entropy_le_mul_of_measure_le
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.
theorem entropy_le_mul_of_measure_le {μ ν : Measure X}
[IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {g : X → ℝ} {b : ℝ}
(hb : 0 ≤ b) (hν : ν ≤ ENNReal.ofReal b • μ)
(hg0 : 0 ≤ᵐ[μ] g) (hg : Integrable g μ)
(hlog : Integrable (fun x => g x * Real.log (g x)) μ) :
entropy ν g ≤ b * entropy μ g := by
have hνμ : ν ≪ μ := Measure.absolutelyContinuous_of_le_smul hν
have hgn : Integrable g ν := (hg.smul_measure ENNReal.ofReal_ne_top).mono_measure hν
have hln : Integrable (fun x => g x * Real.log (g x)) ν :=
(hlog.smul_measure ENNReal.ofReal_ne_top).mono_measure hν
have hgn0 : 0 ≤ᵐ[ν] g := hνμ.ae_le hg0
have hm0 : 0 ≤ ∫ x, g x ∂μ := integral_nonneg_of_ae hg0
rcases hm0.eq_or_lt with hm | hm
· have hgzero : g =ᵐ[μ] 0 := (integral_eq_zero_iff_of_nonneg_ae hg0 hg).1 hm.symm
have hgnzero : g =ᵐ[ν] 0 := hνμ.ae_le hgzero
have hlogzero : (fun x => g x * Real.log (g x)) =ᵐ[μ] 0 :=
hgzero.mono fun x hx => by simp [hx]
have hlognzero : (fun x => g x * Real.log (g x)) =ᵐ[ν] 0 :=
hgnzero.mono fun x hx => by simp [hx]
simp [entropy, integral_congr_ae hgzero, integral_congr_ae hgnzero,
integral_congr_ae hlogzero, integral_congr_ae hlognzero]
· calc
entropy ν g ≤ ∫ x, cost (g x) (∫ y, g y ∂μ) ∂ν :=
entropy_le_integral_cost hgn0 hgn hln hm
_ ≤ ∫ x, cost (g x) (∫ y, g y ∂μ) ∂(ENNReal.ofReal b • μ) :=
integral_mono_measure hν
(by filter_upwards [Measure.ae_smul_measure hg0 (ENNReal.ofReal b)] with x hx
exact cost_nonneg hx hm)
((integrable_cost hg hlog hm).smul_measure ENNReal.ofReal_ne_top)
_ = b * entropy μ g := by
rw [integral_smul_measure, ENNReal.toReal_ofReal hb, smul_eq_mul,
integral_cost hg hlog hm]
simp [cost]
/- The energy functional is held fixed while the probability law changes.
For the usual gradient form choose Γ f = ‖∇f‖². -/
Exact module and namespace context
Source assumptions versus formal assumptions
Canonical finite-integral interface only. Full geometric test-class and Sobolev extension remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: Only the finite-integral entropy comparison is asserted; the complete displayed infimum formula in arbitrary extended-real cases is not formalized here. — Current canonical source statement, full implementation, independent reconstruction, and candidate prose explicitly limit the claim to the supporting finite-integral core. The separate geometric-source-application obligation has no proof binding.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
- Real.log_le_sub_one_of_pos
- MeasureTheory.integral_mono_measure
- MeasureTheory.integral_eq_zero_iff_of_nonneg_ae
- MeasureTheory.Measure.absolutelyContinuous_of_le_smul
- MeasureTheory.Integrable.smul_measure
- MeasureTheory.Integrable.mono_measure
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.
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
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.
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 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.
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 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
Source assumptions versus formal assumptions
Canonical finite-integral interface only. Full geometric test-class and Sobolev extension remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: A useful geometric source LSI must already be established on the intended interface. The theorem does not prove all admissible tests are integrable or identify a best constant. — Current canonical source statement, full implementation, independent reconstruction, and candidate prose explicitly limit the claim to the supporting finite-integral core. The separate geometric-source-application obligation has no proof binding.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.integral_mono_measure
- MeasureTheory.Integrable.smul_measure
- MeasureTheory.Integrable.mono_measure
- MeasureTheory.Measure.absolutelyContinuous_of_le_smul
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.
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.
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
- 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.
- 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.
- 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.
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
Source assumptions versus formal assumptions
Canonical finite-integral interface only. Full geometric test-class and Sobolev extension remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: This needs explicit valid finite bounds l,u. Passing from an oscillation hypothesis to such bounds, identifying a geometric base/test interface, and any Sobolev or extended-domain extension remain separate. — Current canonical source statement, full implementation, independent reconstruction, and candidate prose explicitly limit the claim to the supporting finite-integral core. The separate geometric-source-application obligation has no proof binding.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.
Which proof obligations and prerequisites are covered?
- Formalized proof edge; source adapter/review separate Canonical finite-integral entropy comparison
- Formalized proof edge; source adapter/review separate Fixed-test-class energy inequality under comparable laws
- Formalized proof edge; source adapter/review separate Normalized exponential perturbation with exact factor exp(u-l)
- TODO — not closed by these contributions Remaining source application: identify the geometric reference LSI and intended smooth/Sobolev test domain