feat: binomial random variables (leanprover-community#28248)

Define the binomial distribution and compute the expectation, variance, conditional variance of a binomial random variable.

From MiscYD

Author: YaelDillies

Mathlib.lean

@@ -5964,6 +5964,7 @@ public import Mathlib.Probability.Decision.Risk.Basic
 public import Mathlib.Probability.Decision.Risk.Defs
 public import Mathlib.Probability.Density
 public import Mathlib.Probability.Distributions.Beta
+public import Mathlib.Probability.Distributions.Binomial
 public import Mathlib.Probability.Distributions.Cauchy
 public import Mathlib.Probability.Distributions.Exponential
 public import Mathlib.Probability.Distributions.Fernique
@@ -5984,6 +5985,7 @@ public import Mathlib.Probability.Distributions.Pareto
 public import Mathlib.Probability.Distributions.Poisson.Basic
 public import Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
 public import Mathlib.Probability.Distributions.SetBernoulli
+public import Mathlib.Probability.Distributions.TwoValued
 public import Mathlib.Probability.Distributions.Uniform
 public import Mathlib.Probability.HasLaw
 public import Mathlib.Probability.HasLawExists

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -276,6 +276,7 @@ theorem condExp_bot_ae_eq (f : α → E) :
   · rw [ae_zero]; exact eventually_bot
   · exact Eventually.of_forall <| congr_fun (condExp_bot' f)
 
+@[simp]
 theorem condExp_bot [IsProbabilityMeasure μ] (f : α → E) : μ[f | ⊥] = fun _ => ∫ x, f x ∂μ := by
   refine (condExp_bot' f).trans ?_
   rw [probReal_univ, inv_one, one_smul]

Mathlib/MeasureTheory/Integral/Bochner/Set.lean

@@ -144,6 +144,10 @@ theorem setIntegral_empty : ∫ x in ∅, f x ∂μ = 0 := by
 
 theorem setIntegral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [Measure.restrict_univ]
 
+lemma integral_eq_setIntegral (hs : ∀ᵐ x ∂μ, x ∈ s) (f : X → E) :
+    ∫ x, f x ∂μ = ∫ x in s, f x ∂μ := by
+  rw [← setIntegral_univ, ← setIntegral_congr_set]; rwa [ae_eq_univ]
+
 theorem integral_add_compl₀ (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) :
     ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ := by
   have := setIntegral_union₀ disjoint_compl_right.aedisjoint

Mathlib/Order/Filter/Germ/Basic.lean

@@ -66,7 +66,7 @@ variable {α β γ δ : Type*} {l : Filter α} {f g h : α → β}
 theorem const_eventuallyEq' [NeBot l] {a b : β} : (∀ᶠ _ in l, a = b) ↔ a = b :=
   eventually_const
 
-theorem const_eventuallyEq [NeBot l] {a b : β} : ((fun _ => a) =ᶠ[l] fun _ => b) ↔ a = b :=
+@[simp] theorem const_eventuallyEq [NeBot l] {a b : β} : ((fun _ => a) =ᶠ[l] fun _ => b) ↔ a = b :=
   @const_eventuallyEq' _ _ _ _ a b
 
 /-- Setoid used to define the space of germs. -/

Mathlib/Probability/CondVar.lean

@@ -155,6 +155,7 @@ lemma condVar_bot_ae_eq (X : Ω → ℝ) :
     exact eventually_bot
   · exact .of_forall <| congr_fun (condVar_bot' X)
 
+@[simp]
 lemma condVar_bot [IsProbabilityMeasure μ] (hX : AEMeasurable X μ) :
     Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ] := by
   simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

Mathlib/Probability/Distributions/Binomial.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2025 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Probability.CondVar
+public import Mathlib.Probability.Distributions.SetBernoulli
+public import Mathlib.Probability.Moments.Variance
+public import Mathlib.Probability.HasLaw
+
+import Mathlib.MeasureTheory.MeasurableSpace.NCard
+import Mathlib.Order.Interval.Set.Nat
+import Mathlib.Probability.Distributions.TwoValued
+import Mathlib.Probability.Notation
+
+/-!
+# Binomial random variables
+
+This file defines the binomial distribution and binomial random variables,
+and computes their expectation and variance.
+
+## Main definitions
+
+* `ProbabilityTheory.binomial`:
+  Binomial distribution on an arbitrary semiring with parameters `n` and `p`.
+
+## Notation
+
+`Bin(n, p)` is the binomial distribution with parameters `n` and `p` in `ℕ`.
+`Bin(R, n, p)` is the binomial distribution with parameters `n` and `p` in `R`.
+-/
+
+public section
+
+open MeasureTheory
+open scoped NNReal ProbabilityTheory unitInterval
+
+namespace ProbabilityTheory
+variable {R Ω : Type*} [MeasurableSpace R] [AddMonoidWithOne R] {m : MeasurableSpace Ω}
+  {P : Measure Ω} {X : Ω → R} {n : ℕ} {p : I}
+
+/-- The binomial probability distribution with parameter `p`. -/
+@[expose]
+noncomputable def binomial (n : ℕ) (p : I) : Measure ℕ := setBer(Set.Iio n, p).map Set.ncard
+
+/-- The binomial probability distribution with parameter `p`. -/
+scoped notation3 "Bin(" n ", " p ")" => binomial n p
+
+/-- The binomial probability distribution with parameter `p` valued in the semiring `R`. -/
+scoped notation3 "Bin(" R ", " n ", " p ")" => (binomial n p).map (Nat.cast : ℕ → R)
+
+instance isProbabilityMeasure_binomial : IsProbabilityMeasure Bin(n, p) :=
+  Measure.isProbabilityMeasure_map <| by fun_prop
+
+lemma ae_le_of_hasLaw_binomial {X : Ω → ℕ} (hX : HasLaw X Bin(n, p) P) : ∀ᵐ ω ∂P, X ω ≤ n := by
+  rw [hX.ae_iff (p := (· ≤ n)) <| by fun_prop, binomial,
+    ae_map_iff (by fun_prop) (Set.finite_Iic _).measurableSet]
+  filter_upwards [setBernoulli_ae_subset] with s hs
+  simpa using Set.ncard_le_ncard hs
+
+/-! ### Binomial random variables -/
+
+variable {X : Ω → ℝ}
+
+/-- **Expectation of a binomial random variable**.
+
+The expectation of a binomial random variable with parameters `n` and `p` is `pn`. -/
+proof_wanted integral_of_hasLaw_binomial (hX : HasLaw X Bin(ℝ, n, p) P) : P[X] = p.val * n
+
+/-- **Variance of a binomial random variable**.
+
+The variance of a binomial random variable with parameters `n` and `p` is `p(1 - p)n`. -/
+proof_wanted variance_of_hasLaw_binomial (hX : HasLaw X Bin(ℝ, n, p) P) :
+    Var[X; P] = p * (1 - p) * n
+
+/-- **Conditional variance of a binomial random variable**.
+
+The conditional variance of a binomial random variable is the product of the conditional
+probabilities that it's equal to `0` and that it's equal to `1`. -/
+proof_wanted condVar_of_hasLaw_binomial {m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) {P : Measure[m₀] Ω}
+    (hX : HasLaw X Bin(ℝ, n, p) P) :
+    Var[X; P | m] =ᵐ[P] P[X | m] * P[1 - X | m]
+
+end ProbabilityTheory

Mathlib/Probability/Distributions/TwoValued.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2024 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.Probability.CondVar
+
+import Mathlib.Probability.Notation
+
+/-!
+# Distributions on two values
+
+This file proves a few lemmas about random variables that take at most two values.
+-/
+
+public section
+
+open MeasureTheory
+open scoped ProbabilityTheory
+
+namespace MeasureTheory
+variable {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω}
+
+/-- If an `AEMeasurable` function is ae equal to `0` or `1`, then its integral is equal to the
+measure of the set where it equals `1`. -/
+lemma integral_of_ae_eq_zero_or_one (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ ω ∂μ, X ω = 0 ∨ X ω = 1) :
+    μ[X] = μ.real {ω | X ω = 1} := by
+  refine (integral_map (f := id) hXmeas <| by fun_prop).symm.trans ?_
+  rw [(Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac hXmeas zero_ne_one).1 hX]
+  by_cases h : μ {ω | X ω = 1} = ⊤
+  · simp [h, Measure.real, Set.preimage, integral_undef, Integrable, HasFiniteIntegral]
+  rw [integral_add_measure ⟨by fun_prop, by simp [HasFiniteIntegral]⟩ <|
+    .smul_measure (by simp [integrable_dirac]) h]
+  simp [Measure.real, Set.preimage]
+
+/-- If a random variable is ae equal to `0` or `1`, then one minus its expectation is equal to the
+probability that it equals `0`. -/
+lemma integral_one_sub_of_ae_eq_zero_or_one (hXmeas : AEMeasurable X μ)
+    (hX : ∀ᵐ ω ∂μ, X ω = 0 ∨ X ω = 1) : ∫ ω, 1 - X ω ∂μ = μ.real {ω | X ω = 0} := by
+  calc
+    _ = μ.real {ω | 1 - X ω = 1} :=
+      integral_of_ae_eq_zero_or_one (aemeasurable_const (b := 1).sub hXmeas)
+        (by simpa [sub_eq_zero, or_comm, eq_comm (a := (1 : ℝ))] using hX)
+    _ = μ.real {ω | X ω = 0} := by simp
+
+end MeasureTheory
+
+
+namespace ProbabilityTheory
+variable {Ω : Type*} {m : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : Measure ℝ} {P : Measure Ω}
+
+/-- If a random variable is ae equal to `0` or `1`, then its conditional variance is the product of
+the conditional probabilities that it's equal to `0` and that it's equal to `1`. -/
+lemma condVar_of_ae_eq_zero_or_one {m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) {μ : Measure[m₀] Ω}
+    [IsFiniteMeasure μ] (hXmeas : AEMeasurable[m₀] X μ) (hX : ∀ᵐ ω ∂μ, X ω = 0 ∨ X ω = 1) :
+    Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
+  wlog hXmeas : Measurable[m₀] X
+  · obtain ⟨Y, hYmeas, hXY⟩ := ‹AEMeasurable[m₀] X μ›
+    calc
+      Var[X; μ | m]
+      _ =ᵐ[μ] Var[Y; μ | m] := condVar_congr_ae hXY
+      _ =ᵐ[μ] μ[Y | m] * μ[1 - Y | m] := by
+        refine this hm hYmeas.aemeasurable ?_ hYmeas
+        filter_upwards [hX, hXY] with ω hXω hXYω
+        simp [hXω, ← hXYω]
+      _ =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
+        refine .mul ?_ ?_ <;>
+          exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]
+  calc
+    _ =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 :=
+      condVar_ae_eq_condExp_sq_sub_sq_condExp hm <| .of_bound hXmeas.aestronglyMeasurable 1 <| by
+        filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
+    _ =ᵐ[μ] μ[X | m] - μ[X | m] ^ 2 := by
+      refine .sub ?_ ae_eq_rfl
+      exact condExp_congr_ae <| by filter_upwards [hX]; rintro ω (hω | hω) <;> simp [hω]
+    _ =ᵐ[μ] μ[X | m] * μ[1 - X | m] := by
+      rw [sq, ← one_sub_mul, mul_comm]
+      refine .mul ae_eq_rfl ?_
+      calc
+        1 - μ[X | m]
+        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
+        _ =ᵐ[μ] μ[1 - X | m] := by
+          refine (condExp_sub (integrable_const _)
+            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
+          filter_upwards [hX]
+          rintro ω (hω | hω) <;> simp [hω]
+
+/-- If a random variable is ae equal to `0` or `1`, then its variance is the product of
+the probabilities that it's equal to `0` and that it's equal to `1`. -/
+lemma variance_of_ae_eq_zero_or_one {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ]
+    (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ ω ∂μ, X ω = 0 ∨ X ω = 1) :
+    Var[X; μ] = μ.real {ω | X ω = 0} * μ.real {ω | X ω = 1} := by
+  obtain rfl | hμ := eq_zero_or_isProbabilityMeasure μ
+  · simp
+  simpa [Pi.mul_def, integral_of_ae_eq_zero_or_one, integral_one_sub_of_ae_eq_zero_or_one, mul_comm,
+    *] using condVar_of_ae_eq_zero_or_one bot_le hXmeas hX
+
+end ProbabilityTheory