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 ↗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