Coercivity From Centering And Full-Dimensional Support

This formalizes the coercivity support associated with Proposition 12 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited as a stronger related statement.

Let $E$ be finite-dimensional with a real inner product, let $dx$ be an additive Haar measure, and let $\mu$ be a probability measure. Assume:

1. Every linear subspace carrying full $\mu$-measure is all of $E$:

$$\mu(V^c)=0\implies V=E.$$

2. The identity map $x\mapsto x$ is $\mu$-integrable.
3. The barycenter is zero:

$$\int_E x\,d\mu(x)=0.$$

Then there exists $A>0$ such that every nonnegative ConvexPotential $\phi$ with $\phi(0)=0$ and PotentialIntegrable φ μ satisfies both

$$\operatorname{mass}(dx,\phi^*)\le\operatorname{ENNReal.ofReal}\!\left(A\left(\max\left\{\int\phi.\operatorname{toReal}\,d\mu,1\right\}\right)^{\dim E}\right)$$

and

$$\operatorname{variationalFunctional}(dx,\mu,\phi)\le\left(\log A+\dim(E)\log\max\left\{\int\phi.\operatorname{toReal}\,d\mu,1\right\}-\int\phi.\operatorname{toReal}\,d\mu\right).$$

This is a uniform coercivity estimate, not an existence theorem for a maximizer or a claim about a particular numerical constant.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem exists_coercivity_of_centered_probability (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hint : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ A : ℝ, 0 < A ∧ ∀ φ : E → EReal,
      (∀ x, 0 ≤ φ x) → φ 0 = 0 → ConvexPotential φ → PotentialIntegrable φ μ →
      (mass dx (legendre φ) ≤ ENNReal.ofReal
        (A * (max (∫ x, (φ x).toReal ∂μ) 1) ^ Module.finrank ℝ E)) ∧
      variationalFunctional dx μ φ ≤
        ((Real.log A + (Module.finrank ℝ E : ℝ) * Real.log (max (∫ x, (φ x).toReal ∂μ) 1) -
          (∫ x, (φ x).toReal ∂μ) : ℝ) : EReal)

Module navigation

Module: Probability/MomentMeasure/Coercivity.

Definition modules: Probability/MomentMeasure/Basic, Analysis/Convex/Legendre.

Supporting theorems: exists_uniform_mass_bound, zero_mem_interior_convexHull_support_of_integral_eq_zero.

Previous: exists_uniform_mass_bound · Next: exists_bound_of_log_lower.

Source excerpt, lines 188–198 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Coercivity

open FunctionalInequalities.Analysis
open MeasureTheory Filter Set
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.Probability.MomentMeasure.exists_coercivity_of_centered_probability_readable (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hint : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ A : ℝ, 0 < A ∧ ∀ φ : E → EReal,
      (∀ x, 0 ≤ φ x) → φ 0 = 0 → ConvexPotential φ → PotentialIntegrable φ μ →
      (mass dx (legendre φ) ≤ ENNReal.ofReal
        (A * (max (∫ x, (φ x).toReal ∂μ) 1) ^ Module.finrank ℝ E)) ∧
      variationalFunctional dx μ φ ≤
        ((Real.log A + (Module.finrank ℝ E : ℝ) * Real.log (max (∫ x, (φ x).toReal ∂μ) 1) -
          (∫ x, (φ x).toReal ∂μ) : ℝ) : EReal) := by sorry