noncomputable def stdNormalDensity (t : ℝ) : ℝ

The density of the standard normal distribution: stdNormalDensity t = (2π)^{-1/2} exp(-t²/2).

noncomputable def standardNormalCDF (x : ℝ) : ℝ

The cumulative distribution function of the standard normal: Φ(x) = ∫_{-∞}^{x} (2π)^{-1/2} e^{-t²/2} dt.

theorem berry_esseen {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) (hmean : ∫ (ω : Ω), X 0 ω ∂P = 0) (hσ_pos : 0 < ∫ (ω : Ω), X 0 ω ^ 2 ∂P) (hρ : MeasureTheory.Integrable (fun (ω : Ω) => |X 0 ω| ^ 3) P) (n : ℕ) : 0 < n → ∀ (x : ℝ), |(MeasureTheory.Measure.map (fun (ω : Ω) => (√(∫ (ω' : Ω), X 0 ω' ^ 2 ∂P) * √↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P).real (Set.Iic x) - standardNormalCDF x| ≤ (3 * ∫ (ω : Ω), |X 0 ω| ^ 3 ∂P) / (√(∫ (ω : Ω), X 0 ω ^ 2 ∂P) ^ 3 * √↑n)

Berry-Esseen theorem. Let X_1, X_2, … be i.i.d. real-valued random variables with mean zero, finite variance σ² > 0, and finite third absolute moment ρ = E|X_1|^3 < ∞. Let F_n be the distribution function of (X_1 + … + X_n)/(σ √n). Then for every x ∈ ℝ, |F_n(x) - Φ(x)| ≤ 3ρ/(σ³ √n), where Φ is the standard normal CDF (Durrett, Lecture 16).