noncomputable def ProbabilityTheory.standardizedBinomial (n : ℕ) (p : ↑unitInterval) : MeasureTheory.Measure ℝ

Standardized binomial distribution.

The law of (Sₙ − np) / √(np(1−p)) where Sₙ ~ Binomial(n, p). This is the standardized sum appearing in the DeMoivre–Laplace limit theorem.

instance ProbabilityTheory.isProbabilityMeasure_Bin_real (n : ℕ) (p : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map Nat.cast (binomial n p))

The real-valued binomial measure Bin(ℝ, n, p) is a probability measure.

instance ProbabilityTheory.isProbabilityMeasure_standardizedBinomial (n : ℕ) (p : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (standardizedBinomial n p)

The standardized binomial measure is a probability measure (pushforward of a probability measure under a measurable affine map).

noncomputable def ProbabilityTheory.standardizedBinomialProb (n : ℕ) (p : ↑unitInterval) : MeasureTheory.ProbabilityMeasure ℝ

Bundled ProbabilityMeasure wrapper around standardizedBinomial n p.

noncomputable def ProbabilityTheory.stdNormalProb : MeasureTheory.ProbabilityMeasure ℝ

The standard normal distribution N(0, 1) packaged as a ProbabilityMeasure ℝ.

theorem ProbabilityTheory.charFun_stdNormal (t : ℝ) : MeasureTheory.charFun (gaussianReal 0 1) t = Complex.exp (-(↑t ^ 2 / 2))

Characteristic function of the standard normal: φ_Z(t) = exp(−t² / 2).

theorem ProbabilityTheory.charFun_map_affine (μ : MeasureTheory.Measure ℝ) (a s t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (x : ℝ) => (x - a) / s) μ) t = MeasureTheory.charFun μ (t * s⁻¹) * Complex.exp (↑(-(a * (t * s⁻¹))) * Complex.I)

Affine transformation of a characteristic function.

If Y = (X − a)/s then φ_Y(t) = φ_X(t/s) · exp(−i a t / s).

theorem ProbabilityTheory.binomial_singleton (n k : ℕ) (p : ↑unitInterval) (hk : k ≤ n) : (binomial n p) {k} = ↑(n.choose k) * ↑(unitInterval.toNNReal p) ^ k * ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ (n - k)

Point mass formula for the binomial distribution.

For k ≤ n, Binomial(n, p)({k}) = C(n, k) · pᵏ · (1−p)ⁿ⁻ᵏ.

theorem ProbabilityTheory.binomial_singleton_of_gt (n k : ℕ) (p : ↑unitInterval) (hk : n < k) : (binomial n p) {k} = 0

The binomial distribution Binomial(n, p) assigns mass zero to any k > n.

theorem ProbabilityTheory.integrable_binomial (n : ℕ) (p : ↑unitInterval) (f : ℕ → ℂ) : MeasureTheory.Integrable f (binomial n p)

Every function f : ℕ → ℂ is integrable against Binomial(n, p) since the distribution is supported on the finite set {0, …, n}.

theorem ProbabilityTheory.binomial_singleton_toReal (n k : ℕ) (p : ↑unitInterval) (hk : k ≤ n) : ((binomial n p) {k}).toReal = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Real-valued version of the binomial point mass formula: Binomial(n, p)({k}) = C(n, k) · pᵏ · (1−p)ⁿ⁻ᵏ as a real number.

theorem ProbabilityTheory.integral_binomial_eq_sum (n : ℕ) (p : ↑unitInterval) (f : ℕ → ℂ) : ∫ (x : ℕ), f x ∂binomial n p = ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑↑p ^ k * ↑(1 - ↑p) ^ (n - k) * f k

Integrals against the binomial measure are finite sums: ∫ f d(Binomial(n, p)) = ∑_{k=0}^{n} C(n,k) · pᵏ · (1−p)ⁿ⁻ᵏ · f(k).

theorem ProbabilityTheory.charFun_binomial_real (n : ℕ) (p : ↑unitInterval) (t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map Nat.cast (binomial n p)) t = (1 - ↑↑p + ↑↑p * Complex.exp (↑t * Complex.I)) ^ n

Characteristic function of the real-valued binomial distribution.

φ_{Bin(n, p)}(t) = ((1 − p) + p · e^{it})ⁿ.

theorem ProbabilityTheory.charFun_standardizedBinomial (n : ℕ) (p : ↑unitInterval) (t : ℝ) : have s := √(↑n * ↑p * (1 - ↑p)); MeasureTheory.charFun (standardizedBinomial n p) t = MeasureTheory.charFun (MeasureTheory.Measure.map Nat.cast (binomial n p)) (t * s⁻¹) * Complex.exp (↑(-(↑n * ↑p * (t * s⁻¹))) * Complex.I)

Characteristic function of the standardized binomial as a rescaling of the characteristic function of Bin(n, p). Specialization of charFun_map_affine to the shift np and scale s = √(np(1−p)).

theorem ProbabilityTheory.exp_taylor2_err (z : ℂ) (hz : ‖z‖ ≤ 1) : ‖Complex.exp z - 1 - z - z ^ 2 / 2‖ ≤ 2 * ‖z‖ ^ 3

Second-order Taylor remainder bound for exp.

For ‖z‖ ≤ 1, the remainder after the degree-2 Taylor polynomial of exp satisfies ‖e^z − 1 − z − z²/2‖ ≤ 2 ‖z‖³. Used in the proof of the DeMoivre–Laplace CLT.

theorem ProbabilityTheory.tendsto_charFun_standardizedBinomial (p : ↑unitInterval) (hp₀ : 0 < ↑p) (hp₁ : ↑p < 1) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.charFun (standardizedBinomial n p) t) Filter.atTop (nhds (Complex.exp (-(↑t ^ 2 / 2))))

Convergence of characteristic functions in DeMoivre–Laplace.

For 0 < p < 1 and every t ∈ ℝ, the characteristic function of the standardized binomial converges to the characteristic function of the standard normal: φ_{standardizedBinomial n p}(t) → exp(−t² / 2).

This is the key analytic step in proving deMoivreLaplace_clt via Lévy's continuity theorem.

theorem ProbabilityTheory.deMoivreLaplace_clt (p : ↑unitInterval) (hp₀ : 0 < ↑p) (hp₁ : ↑p < 1) : Filter.Tendsto (fun (n : ℕ) => standardizedBinomialProb n p) Filter.atTop (nhds stdNormalProb)

DeMoivre–Laplace limit theorem (Lecture 12).

Let Xᵢ be i.i.d. Bernoulli(p) and Sₙ = X₁ + ⋯ + Xₙ so that Sₙ ~ Binomial(n, p). For 0 < p < 1, the standardized sums (Sₙ − np)/√(np(1−p)) converge in distribution to the standard normal: P{a ≤ (Sₙ − np)/√(np(1−p)) ≤ b} → Φ(b) − Φ(a) as n → ∞.

The proof combines tendsto_charFun_standardizedBinomial with Lévy's continuity theorem (ProbabilityMeasure.tendsto_iff_tendsto_charFun).