Komlos lemmas

theorem komlos_convex {E : Type u_1} (R : Type u_3) [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommMonoid E] [Module R E] {f : ℕ → E} {φ : E → ℝ} (hφ_nonneg : 0 ≤ φ) (hφ_bdd : ∃ (M : ℝ), ∀ (n : ℕ), φ (f n) ≤ M) : ∃ (g : ℕ → E), (∀ (n : ℕ), g n ∈ (convexHull R) (Set.range fun (m : ℕ) => f (n + m))) ∧ ∀ δ > 0, ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → 2⁻¹ * φ (g n) + 2⁻¹ * φ (g m) - φ (2⁻¹ • (g n + g m)) < δ

theorem komlos_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : ℕ → E} (h_bdd : ∃ (M : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ M) : ∃ (g : ℕ → E), (∀ (n : ℕ), g n ∈ (convexHull ℝ) (Set.range fun (m : ℕ) => f (n + m))) ∧ ∃ (x : E), Filter.Tendsto g Filter.atTop (nhds x)

theorem exists_stdSimplex_of_mem_convexHull {E : Type u_1} {M : Type u_3} {ι : Type u_4} [AddCommGroup E] [Field M] [LinearOrder M] [IsStrictOrderedRing M] [Module M E] {s : ι → E} {x : E} (hx : x ∈ (convexHull M) (Set.range s)) : ∃ (w : Convexity.StdSimplex M ι), x = w.sum fun (i : ι) (wi : M) => wi • s i

def convexTail {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x : ℕ → E) : Set (ℕ → E)

We define the convexTail of a sequence x to be the set of sequences y with the property that every y n can be written as a convex combination of elements x k with k ≥ n.

Equations

• convexTail x = {y : ℕ → E | ∀ (n : ℕ), y n ∈ (convexHull ℝ) (Set.range fun (m : ℕ) => x (n + m))}

theorem convexTail_self {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x : ℕ → E) : x ∈ convexTail x

theorem weights_sum_mem_convexTail {E : Type u_1} [AddCommGroup E] [Module ℝ E] {x y : ℕ → E} (hy : y ∈ convexTail x) {w : ℕ → Convexity.StdSimplex ℝ ℕ} (hw : ∀ (n m : ℕ), m < n → (w n).weights m = 0) : (fun (n : ℕ) => (w n).sum fun (m : ℕ) (r : ℝ) => r • y m) ∈ convexTail x

convexTail x is stable under convex combinations whose weights at step n are supported on indices at least n.

theorem exists_stdSimplex_of_mem_convexTail_reindexed {E : Type u_1} [AddCommGroup E] [Module ℝ E] {x g : ℕ → E} (hg : g ∈ convexTail x) (n : ℕ) : ∃ (w : Convexity.StdSimplex ℝ ℕ), (g n = w.sum fun (i : ℕ) (wi : ℝ) => wi • x i) ∧ ∀ m < n, w.weights m = 0

theorem convex_combination_bounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : ℕ → E} {w : ℕ → Convexity.StdSimplex ℝ ℕ} {M : ℝ} (hx : ∀ (n : ℕ), ‖x n‖ ≤ M) (n : ℕ) : ‖(w n).sum fun (i : ℕ) (wi : ℝ) => wi • x i‖ ≤ M

noncomputable def komlosFormula {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : ℕ → ℕ → E) (cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ) (k i n : ℕ) : E

komlosFormula x cw k n is the convex combination of the stage-k vectors x k m, weighted by iteratedComb cw k n. It is the sequence whose convergence is established at each stage of the Komlós construction.

Equations

• komlosFormula x cw k i n = (Convexity.iteratedComb cw k n).sum fun (m : ℕ) (cwm : ℝ) => cwm • x i m

theorem komlosFormula_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : ℕ → ℕ → E) {cw1 cw2 : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ} {k : ℕ} (h : ∀ k' ≤ k, cw1 k' = cw2 k') : komlosFormula x cw1 k = komlosFormula x cw2 k

theorem komlosFormula_succ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : ℕ → ℕ → E) (cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ) (k i n : ℕ) : komlosFormula x cw (k + 1) i n = (cw (k + 1) n).sum fun (j : ℕ) (c : ℝ) => c • komlosFormula x cw k i j

theorem komlosFormula_mem_convexTail {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : ℕ → ℕ → E) {cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ} (hcw : ∀ (k n m : ℕ), m < n → (cw k n).weights m = 0) {i k : ℕ} (hik : i ≤ k) : komlosFormula x cw k i ∈ convexTail (komlosFormula x cw i i)

For i ≤ k, the stage-k combination of the row x i lies in the convex tail of the stage-i combination of that row.

theorem komlos_base {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : ℕ → ℕ → E} (hx : ∀ (i : ℕ), ∃ (M : ℝ), ∀ (n : ℕ), ‖x i n‖ ≤ M) : ∃ (cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ), (∃ (glim : E), Filter.Tendsto (komlosFormula x cw 0 0) Filter.atTop (nhds glim)) ∧ ∀ (n m : ℕ), m < n → (cw 0 n).weights m = 0

theorem komlos_step {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : ℕ → ℕ → E} (hx : ∀ (i : ℕ), ∃ (M : ℝ), ∀ (n : ℕ), ‖x i n‖ ≤ M) (k : ℕ) (cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ) : ∃ (cw_new : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ), (∃ (glim : E), Filter.Tendsto (komlosFormula x cw_new (k + 1) (k + 1)) Filter.atTop (nhds glim)) ∧ (∀ i ≤ k, cw_new i = cw i) ∧ ∀ (n m : ℕ), m < n → (cw_new (k + 1) n).weights m = 0

theorem komlos_convex_weights {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : ℕ → ℕ → E} (hx : ∀ (i : ℕ), ∃ (M : ℝ), ∀ (n : ℕ), ‖x i n‖ ≤ M) : ∃ (cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ), (∀ (k : ℕ), ∃ (glim : E), Filter.Tendsto (komlosFormula x cw k k) Filter.atTop (nhds glim)) ∧ ∀ (k n m : ℕ), m < n → (cw k n).weights m = 0

theorem TendstoUniformly_convexTail {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : ℕ → E} {xlim : E} (hx : Filter.Tendsto x Filter.atTop (nhds xlim)) : TendstoUniformly (fun (n : ℕ) (y : ↑(convexTail x)) => ↑y n) (fun (x : ↑(convexTail x)) => xlim) Filter.atTop

theorem Tendsto_convexTail {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : ℕ → E} {xlim : E} (hx : Filter.Tendsto x Filter.atTop (nhds xlim)) (y : ℕ → E) : y ∈ convexTail x → Filter.Tendsto y Filter.atTop (nhds xlim)

theorem tendsto_weights_sum_of_forall_lt_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : ℕ → E} {xlim : E} (hx : Filter.Tendsto x Filter.atTop (nhds xlim)) {w : ℕ → Convexity.StdSimplex ℝ ℕ} (hw : ∀ (n m : ℕ), m < n → (w n).weights m = 0) : Filter.Tendsto (fun (n : ℕ) => (w n).sum fun (m : ℕ) (r : ℝ) => r • x m) Filter.atTop (nhds xlim)

Convex combinations of a convergent sequence, given at step n by weights supported on indices at least n, converge to the same limit.

theorem komlos_uniform_convergence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : ℕ → ℕ → E) {cw : ℕ → ℕ → Convexity.StdSimplex ℝ ℕ} (hcw : ∀ (k n m : ℕ), m < n → (cw k n).weights m = 0) {i : ℕ} {lim : E} (hlim : Filter.Tendsto (komlosFormula x cw i i) Filter.atTop (nhds lim)) (ε : ℝ) : ε > 0 → ∃ (N : ℕ), ∀ n ≥ N, ∀ k ≥ i, dist (komlosFormula x cw k i n) lim < ε

If the stage-i combinations komlosFormula x cw i i converge to lim, then for every k ≥ i the stage-k combinations of the row x i converge to lim as well, uniformly in k.

theorem komlos_convex_weights_diagonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : ℕ → ℕ → E} (hx : ∀ (i : ℕ), ∃ (M : ℝ), ∀ (n : ℕ), ‖x i n‖ ≤ M) : ∃ (η : ℕ → Convexity.StdSimplex ℝ ℕ), (∀ (n m : ℕ), m < n → (η n).weights m = 0) ∧ ∀ (i : ℕ), ∃ (glim : E), Filter.Tendsto (fun (n : ℕ) => (η n).sum fun (m : ℕ) (ηm : ℝ) => ηm • x i m) Filter.atTop (nhds glim)

theorem komlos_convergence_L2 {E : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : ℕ → Ω → E) {P : MeasureTheory.Measure Ω} : have f' := fun (i n : ℕ) => {ω : Ω | ‖f n ω‖ ≤ ↑i}.indicator (f n); ∃ (cw : ℕ → Convexity.StdSimplex ℝ ℕ), ∀ (i : ℕ), ∃ (lim : Ω → E), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (ω : Ω) => (cw n).sum (fun (i : ℕ) (wi : ℝ) => wi • f' i n) ω - lim ω) 2 P) Filter.atTop (nhds 0)

theorem komlos_L1 {E : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (hf : MeasureTheory.UniformIntegrable f 1 P) : ∃ (g : ℕ → Ω → E) (glim : Ω → E), MeasureTheory.MemLp glim 1 P ∧ (∀ (n : ℕ), g n ∈ (convexHull ℝ) (Set.range fun (m : ℕ) => f (n + m))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (g n - glim) 1 P) Filter.atTop (nhds 0)

theorem komlos_ennreal {Ω : Type u_2} {mΩ : MeasurableSpace Ω} (X : ℕ → Ω → ENNReal) (hX : ∀ (n : ℕ), Measurable (X n)) {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] : ∃ (Y : ℕ → Ω → ENNReal) (Y_lim : Ω → ENNReal), (∀ (n : ℕ), Y n ∈ (convexHull ENNReal) (Set.range fun (m : ℕ) => X (n + m))) ∧ Measurable Y_lim ∧ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ℕ) => Y x ω) Filter.atTop (nhds (Y_lim ω))