Integral Bounds From An Eventual Functional Lower Bound

This is the normalized-sequence integral-control statement corresponding to estimate (62) in the coercivity framework.

Let $E$ be finite-dimensional with additive Haar measure $dx$, and let $\mu$ be a probability measure satisfying:

1. Every linear subspace with full $\mu$-measure equals $E$.
2. The identity map is $\mu$-integrable.
3. $\int x\,d\mu(x)=0$.

Let $\phi_j:E\to\overline{\mathbb R}$ be a sequence such that every $\phi_j\ge0$, $\phi_j(0)=0$, ConvexPotential (φ j), and PotentialIntegrable (φ j) μ. If, for some $b\in\mathbb R$, eventually in $j$,

$$b\le\operatorname{variationalFunctional}(dx,\mu,\phi_j),$$

then there exists $B\ge0$ such that

$$\int_E(\phi_j(x)).\operatorname{toReal}\,d\mu(x)\le B\quad\text{for every }j,$$

and

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

The bound includes the finite initial segment of the sequence.

Original Lean declaration header

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

theorem exists_integral_bound_of_eventual_functional_lower
    (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)
    (φ : ℕ → E → EReal) (hnn : ∀ j x, 0 ≤ φ j x) (hφ0 : ∀ j, φ j 0 = 0)
    (hconv : ∀ j, ConvexPotential (φ j)) (hφ : ∀ j, PotentialIntegrable (φ j) μ)
    (b : ℝ) (hlower : ∀ᶠ j in atTop, (b : EReal) ≤ variationalFunctional dx μ (φ j)) :
    ∃ B : ℝ, 0 ≤ B ∧ (∀ j, (∫ x, (φ j x).toReal ∂μ) ≤ B) ∧
      (⨆ j, ∫⁻ x, (φ j x).toENNReal ∂μ) ≠ ⊤

Module navigation

Module: Probability/MomentMeasure/Coercivity.

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

Supporting theorems: exists_bound_of_log_lower, exists_coercivity_of_centered_probability.

Previous: exists_bound_of_log_lower · Next: real_coercivity_le_uniform.

Source excerpt, lines 246–254 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Coercivity

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

theorem FunctionalInequalities.Probability.MomentMeasure.exists_integral_bound_of_eventual_functional_lower_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)
    (φ : ℕ → E → EReal) (hnn : ∀ j x, 0 ≤ φ j x) (hφ0 : ∀ j, φ j 0 = 0)
    (hconv : ∀ j, ConvexPotential (φ j)) (hφ : ∀ j, PotentialIntegrable (φ j) μ)
    (b : ℝ) (hlower : ∀ᶠ j in atTop, (b : EReal) ≤ variationalFunctional dx μ (φ j)) :
    ∃ B : ℝ, 0 ≤ B ∧ (∀ j, (∫ x, (φ j x).toReal ∂μ) ≤ B) ∧
      (⨆ j, ∫⁻ x, (φ j x).toENNReal ∂μ) ≠ ⊤ := by sorry