Komlos lemmas

theorem komlos_convex {E : Type u_1} [AddCommMonoid E] [Module NNReal E] {f : ℕ → E} {φ : E → ℝ} (hφ_nonneg : 0 ≤ φ) (hφ_bdd : ∃ (M : ℝ), ∀ (n : ℕ), φ (f n) ≤ M) : ∃ (g : ℕ → E), (∀ (n : ℕ), g n ∈ (convexHull NNReal) (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] {f : ℕ → E} (h_bdd : ∃ (M : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ M) : ∃ (g : ℕ → E) (x : E), (∀ (n : ℕ), g n ∈ (convexHull ℝ) (Set.range fun (m : ℕ) => f (n + m))) ∧ Filter.Tendsto g Filter.atTop (nhds x)

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 ω))