Upper Semicontinuity Of Legendre Conjugate Mass

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

1. $\psi$ is finite-valued in the extended-real sense on $K$.
2. $\phi_j(x)\to\psi(x)$ for every $x\in K$.
3. $\psi(tx)\to\psi(x)$ as $t\to1$ from below for every $x$.
4. $\psi(x)=+\infty$ whenever $x\notin\overline K$.

Then

$$\operatorname{mass}(dx,\psi^*)\ne+\infty$$

and

$$\limsup_{j\to\infty}\operatorname{mass}(dx,\phi_j^*)\le\operatorname{mass}(dx,\psi^*).$$

No finiteness of the individual source masses is assumed, and the conclusion permits zero mass.

Original Lean declaration header

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

theorem limsup_mass_legendre_le
    (dx : Measure E) [dx.IsAddHaarMeasure]
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hK : IsOpen K) (hKconv : Convex ℝ K) (h0 : (0 : E) ∈ K)
    (hfin : ∀ x ∈ K, ψ x ≠ ⊤ ∧ ψ x ≠ ⊥)
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x)))
    (hrad : ∀ x, Tendsto (fun t : ℝ => ψ (t • x)) (𝓝[<] 1) (𝓝 (ψ x)))
    (hoff : ∀ x ∉ closure K, ψ x = ⊤) :
    mass dx (legendre ψ) ≠ ⊤ ∧
      limsup (fun j => mass dx (legendre (φ j))) atTop ≤ mass dx (legendre ψ)

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

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

Supporting theorems: legendre_eq_interior_sup, exists_integrable_exponential_domination, limsup_density_legendre_le.

Previous: exists_integrable_exponential_domination · Next: log_sub_ge_of_integral_limits.

Source excerpt, lines 156–165 · Frozen source 408915f.

Literature

This formalizes Lemma 17 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited as “Compactness of normalised potentials,” in a partial form.

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.limsup_mass_legendre_le_readable
    (dx : Measure E) [dx.IsAddHaarMeasure]
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hK : IsOpen K) (hKconv : Convex ℝ K) (h0 : (0 : E) ∈ K)
    (hfin : ∀ x ∈ K, ψ x ≠ ⊤ ∧ ψ x ≠ ⊥)
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x)))
    (hrad : ∀ x, Tendsto (fun t : ℝ => ψ (t • x)) (𝓝[<] 1) (𝓝 (ψ x)))
    (hoff : ∀ x ∉ closure K, ψ x = ⊤) :
    mass dx (legendre ψ) ≠ ⊤ ∧
      limsup (fun j => mass dx (legendre (φ j))) atTop ≤ mass dx (legendre ψ) := by sorry