Common Exponential Domination Of Conjugate Densities

This is the common-dominator construction used for the upper semicontinuity result associated with Lemma 17 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited there as a partial formalization.

Let $E$ be finite-dimensional with an additive Haar measure $dx$. Let $\phi_j:E\to\overline{\mathbb R}$, $\psi:E\to\overline{\mathbb R}$, and let $K\subseteq E$ be open with $0\in K$. Assume:

1. For every $x\in K$, $\psi(x)$ is neither $+\infty$ nor $-\infty$.
2. For every $x\in K$, $\phi_j(x)\to\psi(x)$ as $j\to\infty$.

Then there exist $c,M\in\mathbb R$ and $N\in\mathbb N$ with $c>0$ such that

$$\int_E\operatorname{ENNReal.ofReal}\!\left(\exp(M-c\|y\|)\right)\,dx(y)\ne+\infty,$$

while, for every $y\in E$,

$$\operatorname{density}(\psi^*)(y)\le\operatorname{ENNReal.ofReal}\!\left(\exp(M-c\|y\|)\right),$$

and for every $j\ge N$ the same bound holds with $\psi$ replaced by $\phi_j$.

This supplies a single integrable exponential envelope for the limiting and eventually indexed conjugate densities.

Original Lean declaration header

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

theorem exists_integrable_exponential_domination
    (dx : Measure E) [dx.IsAddHaarMeasure]
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hK : IsOpen K) (h0 : (0 : E) ∈ K)
    (hfin : ∀ x ∈ K, ψ x ≠ ⊤ ∧ ψ x ≠ ⊥)
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x))) :
    ∃ (c M : ℝ) (N : ℕ), 0 < c ∧
      (∫⁻ y, ENNReal.ofReal (Real.exp (M - c * ‖y‖)) ∂dx) ≠ ⊤ ∧
      (∀ y, density (legendre ψ) y ≤ ENNReal.ofReal (Real.exp (M - c * ‖y‖))) ∧
      ∀ j, N ≤ j → ∀ y,
        density (legendre (φ j)) y ≤ ENNReal.ofReal (Real.exp (M - c * ‖y‖))

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

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

Supporting theorems: affineMaximum_coercive, eventually_affineMaximum_sub_le_legendre, integrable_exp_sub_norm.

Previous: limsup_density_legendre_le · Next: limsup_mass_legendre_le.

Source excerpt, lines 118–128 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_ConjugateMass

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

theorem FunctionalInequalities.Probability.MomentMeasure.exists_integrable_exponential_domination_readable
    (dx : Measure E) [dx.IsAddHaarMeasure]
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hK : IsOpen K) (h0 : (0 : E) ∈ K)
    (hfin : ∀ x ∈ K, ψ x ≠ ⊤ ∧ ψ x ≠ ⊥)
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x))) :
    ∃ (c M : ℝ) (N : ℕ), 0 < c ∧
      (∫⁻ y, ENNReal.ofReal (Real.exp (M - c * ‖y‖)) ∂dx) ≠ ⊤ ∧
      (∀ y, density (legendre ψ) y ≤ ENNReal.ofReal (Real.exp (M - c * ‖y‖))) ∧
      ∀ j, N ≤ j → ∀ y,
        density (legendre (φ j)) y ≤ ENNReal.ofReal (Real.exp (M - c * ‖y‖)) := by sorry