Limit Assembly for Logarithmic Mass Comparison

This is an auxiliary limit-assembly statement related to Proposition 12 of Cordero–Klartag (arXiv:1304.0630v1).

Let $a:\mathbb{N}\to[0,\infty]$, $m:\mathbb{N}\to\mathbb{R}$, $Z\in[0,\infty]$, and $r,S,M\in\mathbb{R}$. Assume:

1. $0\le m_j$ for every $j$.
2. $\log a_j-m_j$ converges in the extended real line to $S$.
3. $m_j$ converges to $M$.
4. $\operatorname{ofReal}(r)\le\liminf_j\operatorname{ofReal}(m_j)$ in $[0,\infty]$.
5. $\limsup_j a_j\le Z$.

Then $Z>0$ and

The declaration is a technical assembly lemma for passing from sequence limits and liminf/limsup bounds to a functional comparison; it is not an attainment statement.

Formalization Note. The quantities involving $a_j$ and $Z$ use ENNReal.log, while the subtraction and the comparison with $S$ and $r$ take place in EReal; the conclusion is expressed with the corresponding coercions.

Original Lean declaration header

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

theorem log_sub_ge_of_integral_limits
    (a : ℕ → ℝ≥0∞) (m : ℕ → ℝ) (Z : ℝ≥0∞) (r S M : ℝ)
    (hnn : ∀ j, 0 ≤ m j)
    (hF : Tendsto (fun j => ENNReal.log (a j) - (m j : EReal)) atTop (𝓝 (S : EReal)))
    (hm : Tendsto m atTop (𝓝 M))
    (hfirst : ENNReal.ofReal r ≤ liminf (fun j => ENNReal.ofReal (m j)) atTop)
    (hsecond : limsup a atTop ≤ Z) :
    0 < Z ∧ (S : EReal) ≤ ENNReal.log Z - (r : EReal)

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

Previous: limsup_mass_legendre_le · Next: real_legendre_normalization.

Source excerpt, lines 211–218 · Frozen source 408915f.