Problem 1.3: Finite expectation of supremum with decaying variance proxies

Let X₁, X₂, ... be an infinite sequence of sub-Gaussian random variables with variance proxy σᵢ² = C(log i)^{-1/2} = C / √(log i). For C large enough, we have E[sup_{i≥2} Xᵢ] < ∞.

The conclusion is formalized as integrability of the pointwise supremum ω ↦ ⨆ (i : {n : ℕ // 2 ≤ n}) X_{i}(ω), which implies that the Bochner integral E[sup_{i≥2} Xᵢ] is well-defined and finite.

Note: The index starts at i ≥ 2 since log 1 = 0 would make the variance proxy undefined.

theorem problem_1_3_sup_decaying_variance : ∃ (C : ℝ), 0 < C ∧ ∀ (Ω : Type) [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ), (∀ (i : ℕ), 2 ≤ i → IsSubGaussian (X i) (C / √(Real.log ↑i)) μ) → (∀ (i : ℕ), 2 ≤ i → Measurable (X i)) → (∀ (ω : Ω), BddAbove (Set.range fun (i : { n : ℕ // 2 ≤ n }) => X (↑i) ω)) → MeasureTheory.Integrable (fun (ω : Ω) => ⨆ (i : { n : ℕ // 2 ≤ n }), X (↑i) ω) μ

Problem 1.3: There exists a constant C > 0 such that for any sequence of sub-Gaussian random variables Xᵢ with variance proxy σᵢ² = C / √(log i), the pointwise supremum over i ≥ 2 is integrable, i.e., E[sup_{i≥2} Xᵢ] < ∞.

Hypotheses include measurability of each Xᵢ and pointwise boundedness above of the supremum (needed for iSup in the conditionally complete lattice ℝ).