Theorem Definition:

        theorem ProbabilityTheory.strong_law_ae {Ω : Type u_1}  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}  {E : Type u_2}  [NormedAddCommGroup E]  [NormedSpace ℝ E] [CompleteSpace E]  [MeasurableSpace E]  [BorelSpace E]  (X : ℕ → Ω → E) (hint : MeasureTheory.Integrable (X 0) μ) (hindep : Pairwise (Function.onFun (fun (x1 x2 : Ω → E) => IndepFun x1 x2 μ) X)) (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ) : ∀ᵐ (ω : Ω) ∂μ,   Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ)) :=