Pointwise Convex Potential Bound By Its Integral

Let $E$ be finite-dimensional with a real inner product and Borel measurable structure. Let $\mu$ be a finite measure and let $x_0$ belong to the interior of the convex hull of $\operatorname{supp}(\mu)$. Then there exists $C\in\mathbb R$ with $C>0$ such that, for every $\phi:E\to\overline{\mathbb R}$ satisfying:

1. $\phi(x)\ge0$ for every $x$.
2. Its real epigraph is convex.
3. $x\mapsto\phi(x).\operatorname{toENNReal}$ is a.e. measurable with respect to $\mu$.
4. Its lower integral is finite:

$$\int^- \phi(x).\operatorname{toENNReal}\,d\mu\ne+\infty.$$

one has

$$\phi(x_0)\le\left(C\left(\int^- \phi(x).\operatorname{toENNReal}\,d\mu\right).\operatorname{toReal}:\mathbb R\right).$$

The constant is selected from $\mu$ and $x_0$ before the potential $\phi$; this is the principal point-control estimate reused in the coercivity arguments.

Formalization Note The integral is an ENNReal lower integral, and .toReal converts it to $\mathbb R$ before the product is coerced back to the extended reals.

Original Lean declaration header

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

theorem exists_pos_le_mul_lintegral_toReal_of_convex_epigraph [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E]
    (μ : Measure E) [IsFiniteMeasure μ] (x₀ : E) :
    x₀ ∈ interior (convexHull ℝ μ.support) →
      ∃ C : ℝ, 0 < C ∧ ∀ φ : E → EReal,
        (∀ x, 0 ≤ φ x) → Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)} →
        AEMeasurable (fun x => (φ x).toENNReal) μ →
        (∫⁻ x, (φ x).toENNReal ∂μ) ≠ ⊤ →
          φ x₀ ≤ ((C * (∫⁻ x, (φ x).toENNReal ∂μ).toReal : ℝ) : EReal)

Module navigation

Module: Probability/ConvexSupport.

Supporting theorems: exists_pos_le_measure_halfspace_of_mem_interior_convexHull_support_of_isFiniteMeasure, mem_interior_setOf_ne_top_of_lintegral_ne_top, strict_sublevel_convex_and_interior.

Previous: strict_sublevel_convex_and_interior · Next: zero_mem_interior_convexHull_support_of_integral_eq_zero.

Source excerpt, lines 654–661 · Frozen source 408915f.

Literature

This formalizes Lemma 16 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited as “Pointwise bound by the integral.”

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_ConvexSupport

open MeasureTheory
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]

theorem FunctionalInequalities.Probability.exists_pos_le_mul_lintegral_toReal_of_convex_epigraph_readable [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E]
    (μ : Measure E) [IsFiniteMeasure μ] (x₀ : E) :
    x₀ ∈ interior (convexHull ℝ μ.support) →
      ∃ C : ℝ, 0 < C ∧ ∀ φ : E → EReal,
        (∀ x, 0 ≤ φ x) → Convex ℝ {p : E × ℝ | φ p.1 ≤ (p.2 : EReal)} →
        AEMeasurable (fun x => (φ x).toENNReal) μ →
        (∫⁻ x, (φ x).toENNReal ∂μ) ≠ ⊤ →
          φ x₀ ≤ ((C * (∫⁻ x, (φ x).toENNReal ∂μ).toReal : ℝ) : EReal) := by sorry