Elementary theory of the binomial distribution

This file develops the moments, transforms, convolution law, and independent-sum characterization of Mathlib's binomial measure. The native law remains ProbabilityTheory.binomial n p on ℕ; real-valued moments and transforms use its cast pushforward Bin(ℝ, n, p). Its variance is n * p * (1 - p).

Main results

• TauCeti.Probability.pgf_binomial computes the probability-generating function on the native carrier;
• TauCeti.Probability.variance_id_map_cast_binomial computes the variance of the cast law;
• TauCeti.Probability.integral_sq_id_map_cast_binomial computes its second raw moment;
• TauCeti.Probability.mgf_id_map_cast_binomial and TauCeti.Probability.cgf_id_map_cast_binomial compute its moment and cumulant generating functions;
• TauCeti.Probability.charFun_map_cast_binomial computes its characteristic function;
• TauCeti.Probability.binomial_conv_binomial proves additivity of the native binomial laws;
• TauCeti.Probability.iIndepFun.hasLaw_sum_bernoulli identifies a finite sum of independent Bernoulli variables with a binomial law.

References

• N. L. Johnson, A. W. Kemp, S. Kotz, Univariate Discrete Distributions, 3rd ed., Wiley, 2005, Chapter 3.
• TauCetiRoadmap/StandardDistributions/README.md, Layer 1, "Bernoulli and binomial".

@[simp]

theorem TauCeti.Probability.pgf_binomial (n : ℕ) (p : ↑unitInterval) (t : ℝ) : pgf id (ProbabilityTheory.binomial n p) t = (1 - ↑p + ↑p * t) ^ n

The probability-generating function of a binomial distribution.

theorem TauCeti.Probability.mgf_id_map_cast_binomial (n : ℕ) (p : ↑unitInterval) (t : ℝ) : ProbabilityTheory.mgf id (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) t = (1 - ↑p + ↑p * Real.exp t) ^ n

The moment generating function of the real-valued binomial law.

theorem TauCeti.Probability.cgf_id_map_cast_binomial (n : ℕ) (p : ↑unitInterval) (t : ℝ) : ProbabilityTheory.cgf id (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) t = Real.log ((1 - ↑p + ↑p * Real.exp t) ^ n)

The cumulant generating function of the real-valued binomial law.

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

The characteristic function of the real-valued binomial law.

theorem TauCeti.Probability.binomial_conv_binomial (n m : ℕ) (p : ↑unitInterval) : (ProbabilityTheory.binomial n p).conv (ProbabilityTheory.binomial m p) = ProbabilityTheory.binomial (n + m) p

The convolution of two native binomial laws with the same success probability is binomial, with the numbers of trials added.

theorem TauCeti.Probability.iIndepFun.hasLaw_sum_bernoulli {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {p : ↑unitInterval} {X : ι → Ω → ℕ} (hindep : ProbabilityTheory.iIndepFun X P) (hX : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) (ProbabilityTheory.bernoulliMeasure 1 0 p) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => ∑ i : ι, X i ω) (ProbabilityTheory.binomial (Fintype.card ι) p) P

A finite sum of independent Bernoulli variables with common success probability p has the native binomial law, with as many trials as the index type has elements.

Variance

theorem TauCeti.Probability.variance_id_map_cast_binomial (n : ℕ) (p : ↑unitInterval) : ProbabilityTheory.variance id (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) = ↑p * (1 - ↑p) * ↑n

The variance of the real-valued binomial measure itself.

theorem TauCeti.Probability.variance_of_hasLaw_binomial {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {n : ℕ} {p : ↑unitInterval} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) P) : ProbabilityTheory.variance X P = ↑p * (1 - ↑p) * ↑n

The variance of a real-valued binomial random variable with parameters n and p is p(1-p)n.

theorem TauCeti.Probability.integral_sq_id_map_cast_binomial (n : ℕ) (p : ↑unitInterval) : ∫ (x : ℝ), x ^ 2 ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p) = ↑p * (1 - ↑p) * ↑n + (↑p * ↑n) ^ 2

The second raw moment of a real-valued binomial law.