theorem KolmogorovThreeSeries.eLpNorm_one_le_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm f 1 μ ≤ MeasureTheory.eLpNorm f 2 μ

On a probability space, the L¹ norm is dominated by the L² norm: ‖f‖₁ ≤ ‖f‖₂.

theorem KolmogorovThreeSeries.eLpNorm_one_le_sqrt_integral_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 μ) {C : ℝ} (h_int_sq : ∫ (x : Ω), ‖f x‖ ^ 2 ∂μ ≤ C) : MeasureTheory.eLpNorm f 1 μ ≤ ENNReal.ofReal √C

If ∫ ‖f‖² dμ ≤ C for an L² function on a probability space, then ‖f‖₁ ≤ √C.

theorem KolmogorovThreeSeries.ae_tendsto_sum_of_indep_centered_L1bdd {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : ℕ → Ω → ℝ} (hZ_sm : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (Z n)) (hZ_indep : ProbabilityTheory.iIndepFun Z μ) (hZ_mean : ∀ (n : ℕ), ∫ (ω : Ω), Z n ω ∂μ = 0) (hZ_int : ∀ (n : ℕ), MeasureTheory.Integrable (Z n) μ) {R : NNReal} (hZ_L1_bdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (fun (ω : Ω) => ∑ k ∈ Finset.range (n + 1), Z k ω) 1 μ ≤ ↑R) : ∀ᵐ (ω : Ω) ∂μ, ∃ (c : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), Z k ω) Filter.atTop (nhds c)

Key step toward the Kolmogorov three-series theorem: if the Zₙ are independent centered (mean zero) integrable random variables whose partial sums Sₙ = ∑_{k≤n} Zₖ are uniformly bounded in L¹, then Sₙ converges almost surely. This is proved by realizing Sₙ as a martingale and applying the L¹-bounded martingale convergence theorem.