2.1 · Book p. 48 · PDF p. 60
Overview of the Inequalities
Places Poincaré, log-Sobolev, transport, concentration, and isoperimetric inequalities in one comparison map.
Open this section in the canonical August 9 source ↗Section 2.1 overview
The chapter organizes Poincaré, log-Sobolev, transport, and concentration inequalities in a common measure-theoretic language.
The principal inequalities compare variance, entropy, transport distance, and boundary or tail behavior. Their implications and preservation rules provide reusable routes from geometric assumptions to quantitative sampling convergence.
Why is this valid?
Each inequality needs an explicit function class and finite terms; extension beyond a smooth compactly supported core requires a closure or density argument.
Source assumptions
- probability reference law
- regular test functions or densities
Formal assumptions
- explicit measure
- probability normalization for the Poincare interface
- finite entropy/energy terms
- explicit function class
View Lean formalization
ASTIS separates the probability-law and density prerequisites from the analytic inequality and its semigroup consumers.
AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
{α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
{r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
(hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
(hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
(hr : ∀ᵐ x ∂mu, 0 < r x)
(hdSqrt : ∀ᵐ x ∂mu,
∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
(hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
dirichlet = (1 / 4) * fisher := by
rw [hdirichlet, hfisher]
rw [← integral_const_mul]
exact lsiKlFiSqrtDensityFisherChainIntegralFiniteSum mu hr hdSqrt hdLog
/-- Scalar rearrangement behind the one-sided use of the cited DV formula.
This is not a proof of Donsker--Varadhan. It starts after a cited or
eventually formalized entropy-duality theorem has supplied the variational
upper bound for an admissible test.
-/Imports
- Mathlib.Data.Real.Basic
- Mathlib.Algebra.Order.Archimedean.Real.Basic
- Mathlib.Analysis.Real.Sqrt
- Mathlib.Analysis.Calculus.ParametricIntegral
- Mathlib.Analysis.SpecialFunctions.Log.Basic
- Mathlib.InformationTheory.KullbackLeibler.Basic
- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
- Mathlib.MeasureTheory.Measure.Tilted
- Mathlib.Probability.Kernel.Condexp
- Mathlib.Probability.Moments.IntegrableExpMul
- AutoSamplingTheory.Core
Local dependencies
No Registry dependency inferred.
Downstream consumers
- semigroup convergence
- sampling complexity