Pointwise Subsequence Compactness For Nonnegative Convex Functions

This is the finite-dimensional pointwise compactness theorem for convex functions, used in the compactness argument for Lemma 17 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited as a partial formalization.

Let $E$ be finite-dimensional over $\mathbb R$, let $K\subseteq E$ be open, and let $f_j:E\to\mathbb R$. Assume:

1. Each $f_j$ is convex on $K$.
2. $f_j(x)\ge0$ for every $x\in K$.
3. For each $x\in K$, the set $\{f_j(x):j\in\mathbb N\}$ is bounded above.

Then there exist a strictly increasing sequence $s:\mathbb N\to\mathbb N$ and a function $g:E\to\mathbb R$ such that $g$ is convex on $K$ and, for every $x\in K$,

The conclusion also applies when $K$ is empty.

Original Lean declaration header

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

theorem exists_subseq_tendsto_of_convexOn_of_bddAbove {K : Set E} (hK : IsOpen K)
    (f : ℕ → E → ℝ) (hf : ∀ ℓ, ConvexOn ℝ K (f ℓ)) (hnn : ∀ ℓ, ∀ x ∈ K, 0 ≤ f ℓ x)
    (hbdd : ∀ x ∈ K, BddAbove (Set.range fun ℓ => f ℓ x)) :
    ∃ (s : ℕ → ℕ) (g : E → ℝ), StrictMono s ∧ ConvexOn ℝ K g ∧
      ∀ x ∈ K, Filter.Tendsto (fun j => f (s j) x) Filter.atTop (nhds (g x))

Module navigation

Module: Analysis/Convex/PointwiseCompactness.

Source excerpt, lines 132–136 · Frozen source 408915f.