theorem StrongLaw.strong_law_of_large_numbers_real {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

Strong law of large numbers (Lecture 6): if X 0, X 1, … are pairwise independent, identically distributed, integrable real-valued random variables, then the empirical means A_n = n⁻¹ ∑_{i < n} X i converge μ-almost surely to the common expectation ∫ X 0 dμ.

theorem StrongLaw.textbook_strong_law_ae {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → ℝ) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (X i) (X j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

Textbook restatement of the strong law of large numbers: a direct alias of strong_law_of_large_numbers_real matching the formulation from Lecture 6.