feat: variance of the binomial distribution

Mathlib/Analysis/MeanInequalitiesPow.lean

@@ -333,6 +333,10 @@ theorem LpAddConst_zero : LpAddConst 0 = 1 := by
   intro h
   exact lt_irrefl _ h.1
 
+theorem LpAddConst_ne_zero {p : ℝ≥0∞} : LpAddConst p ≠ 0 := by
+  rw [LpAddConst]
+  split_ifs <;> positivity
+
 theorem LpAddConst_lt_top (p : ℝ≥0∞) : LpAddConst p < ∞ := by
   rw [LpAddConst]
   split_ifs with h

Mathlib/MeasureTheory/Function/EssSup.lean

@@ -57,6 +57,14 @@ theorem essSup_congr_ae {f g : α → β} (hfg : f =ᵐ[μ] g) : essSup f μ = e
 theorem essInf_congr_ae {f g : α → β} (hfg : f =ᵐ[μ] g) : essInf f μ = essInf g μ :=
   @essSup_congr_ae α βᵒᵈ _ _ _ _ _ hfg
 
+@[simp]
+lemma essSup_dirac [MeasurableSingletonClass α] (a : α) : essSup f (Measure.dirac a) = f a := by
+  simp [essSup]
+
+@[simp]
+lemma essInf_dirac [MeasurableSingletonClass α] (a : α) : essInf f (Measure.dirac a) = f a := by
+  simp [essInf]
+
 @[simp]
 theorem essSup_const' [NeZero μ] (c : β) : essSup (fun _ : α => c) μ = c :=
   limsup_const _

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -10,6 +10,9 @@ public import Mathlib.MeasureTheory.Function.AEEqFun
 public import Mathlib.MeasureTheory.Function.LpSeminorm.Defs
 public import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
 
+import Mathlib.Analysis.MeanInequalitiesPow
+import Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
+
 /-!
 # Basic theorems about ℒp space
 -/
@@ -142,6 +145,17 @@ variable {ε : Type*} [TopologicalSpace ε] [ContinuousENorm ε]
 @[simp] lemma memLp_measure_zero {f : α → ε} : MemLp f p (0 : Measure α) := by
   simp [MemLp]
 
+@[simp]
+lemma memLp_dirac [MeasurableSingletonClass α] {a : α} {f : α → ε} (hf : ‖f a‖ₑ < ∞) :
+    MemLp f p (Measure.dirac a) := by
+  refine ⟨aestronglyMeasurable_dirac, ?_⟩
+  rw [eLpNorm]
+  split_ifs with hq hq'
+  · simp
+  · simpa
+  · simp [eLpNorm']
+    finiteness
+
 end ContinuousENorm
 
 end Zero
@@ -701,6 +715,10 @@ theorem MemLp.smul_measure {f : α → ε} {c : ℝ≥0∞} (hf : MemLp f p μ)
     MemLp f p (c • μ) :=
   hf.of_measure_le_smul hc le_rfl
 
+theorem MemLp.smul_measure_nnreal {f : α → ε} {c : ℝ≥0} (hf : MemLp f p μ) :
+    MemLp f p (c • μ) :=
+  hf.of_measure_le_smul (by simp) le_rfl
+
 variable {ε : Type*} [ENorm ε] in
 theorem eLpNorm_one_add_measure (f : α → ε) (μ ν : Measure α) :
     eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν := by
@@ -838,6 +856,38 @@ theorem eLpNorm_eq_zero_iff {f : α → ε} (hf : AEStronglyMeasurable f μ) (h0
   rw [eLpNorm_eq_eLpNorm' h0 h_top]
   exact eLpNorm'_eq_zero_iff (ENNReal.toReal_pos h0 h_top) hf
 
+lemma eLpNormEssSup_add_measure {ε : Type*} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} :
+    eLpNormEssSup f (μ + ν) = max (eLpNormEssSup f μ) (eLpNormEssSup f ν) := by
+  refine le_antisymm (eLpNormEssSup_le_of_ae_enorm_bound ?_) ?_
+  · rw [ae_add_measure_iff]
+    constructor
+    · filter_upwards [enorm_ae_le_eLpNormEssSup f μ] with x hx
+      grw [hx, ← le_max_left]
+    · filter_upwards [enorm_ae_le_eLpNormEssSup f ν] with x hx
+      grw [hx, ← le_max_right]
+  · exact max_le_iff.2 ⟨eLpNormEssSup_mono_measure _ (.add_right .rfl _),
+      eLpNormEssSup_mono_measure _ (.add_right' .rfl _)⟩
+
+lemma MemLp.add_measure (h1 : MemLp f p μ) (h2 : MemLp f p ν) : MemLp f p (μ + ν) := by
+  refine ⟨h1.aestronglyMeasurable.add_measure h2.aestronglyMeasurable, ?_⟩
+  rw [eLpNorm]
+  split_ifs with hp hp'
+  · simp
+  · rw [hp'] at h1 h2
+    grw [eLpNormEssSup_add_measure, max_le_add_of_nonneg (by simp) (by simp),
+      ← eLpNorm_exponent_top, ← eLpNorm_exponent_top, h1.2, top_add]
+    exact h2.2.ne
+  · grw [eLpNorm', lintegral_add_measure, ENNReal.rpow_add_le_mul_rpow_add_rpow' _ _ (by simp),
+      ← eLpNorm', ← eLpNorm', ← eLpNorm_eq_eLpNorm' hp hp', ← eLpNorm_eq_eLpNorm' hp hp', h1.2]
+    · simp
+    · exact h2.2.ne
+    · exact ENNReal.LpAddConst_ne_zero
+    · exact (ENNReal.LpAddConst_lt_top _).ne
+
+lemma memLp_add_measure : MemLp f p (μ + ν) ↔ MemLp f p μ ∧ MemLp f p ν where
+  mp h := ⟨h.left_of_add_measure, h.right_of_add_measure⟩
+  mpr h := h.1.add_measure h.2
+
 end ENormedAddMonoid
 
 section MapMeasure

Mathlib/MeasureTheory/Function/LpSeminorm/Defs.lean

@@ -80,6 +80,11 @@ def eLpNormEssSup (f : α → ε) (μ : Measure α) :=
 lemma eLpNormEssSup_eq_essSup_enorm (f : α → ε) (μ : Measure α) :
     eLpNormEssSup f μ = essSup (‖f ·‖ₑ) μ := rfl
 
+@[simp]
+lemma eLpNormEssSup_dirac [MeasurableSingletonClass α] (f : α → ε) (a : α) :
+    eLpNormEssSup f (Measure.dirac a) = ‖f a‖ₑ := by
+  simp [eLpNormEssSup]
+
 /-- `ℒp` seminorm, equal to `0` for `p=0`, to `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and to
 `essSup ‖f‖ μ` for `p = ∞`. -/
 def eLpNorm {_ : MeasurableSpace α}

Mathlib/MeasureTheory/Measure/Dirac.lean

@@ -70,6 +70,10 @@ theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1 := by
   rw [← dirac_apply' a MeasurableSet.univ]
   exact measure_mono (subset_univ s)
 
+@[simp]
+theorem dirac_real_apply_of_mem {a : α} (h : a ∈ s) : (dirac a).real s = 1 := by
+  simp [measureReal_def, h]
+
 @[simp]
 theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
     dirac a s = s.indicator 1 a := by
@@ -79,6 +83,12 @@ theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
     dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
     _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
 
+@[simp]
+theorem dirac_real_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
+    (dirac a).real s = s.indicator 1 a := by
+  simp [measureReal_def, Set.indicator]
+  split_ifs <;> simp
+
 @[simp] lemma dirac_ne_zero : dirac a ≠ 0 :=
   fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a)
 

Mathlib/Order/LiminfLimsup.lean

@@ -59,6 +59,16 @@ def limsSup (f : Filter α) : α :=
 def limsInf (f : Filter α) : α :=
   sSup { a | ∀ᶠ n in f, a ≤ n }
 
+@[simp]
+lemma limsSup_pure (a : α) : limsSup (pure a) = a := by
+  simp only [limsSup, eventually_pure]
+  exact csInf_Ici
+
+@[simp]
+lemma limsInf_pure (a : α) : limsInf (pure a) = a := by
+  simp only [limsInf, eventually_pure]
+  exact csSup_Iic
+
 /-- The `limsup` of a function `u` along a filter `f` is the infimum of the `a` such that
 the inequality `u x ≤ a` eventually holds for `f`. -/
 def limsup (u : β → α) (f : Filter β) : α :=
@@ -83,6 +93,14 @@ section
 
 variable {f : Filter β} {u : β → α} {p : β → Prop}
 
+@[simp]
+lemma limsup_pure (b : β) : limsup u (pure b) = u b := by
+  simp [limsup]
+
+@[simp]
+lemma liminf_pure (b : β) : liminf u (pure b) = u b := by
+  simp [liminf]
+
 theorem limsup_eq : limsup u f = sInf { a | ∀ᶠ n in f, u n ≤ a } :=
   rfl
 

Mathlib/Probability/Distributions/Bernoulli.lean

@@ -6,6 +6,7 @@ Authors: Etienne Marion, David Ledvinka
 module
 
 public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.Probability.HasLaw
 public import Mathlib.Topology.UnitInterval
 
 /-!
@@ -161,14 +162,28 @@ theorem map_bernoulliMeasure' (x y : X) {f : X → Y} (hf : Measurable f) (p : I
     Ber(x, y, p).map f = bernoulliMeasure (f x) (f y) p := by
   simp [bernoulliMeasure_def, Measure.map_add _ _ hf, Measure.map_smul, map_dirac' hf]
 
+lemma eq_bernoulliMeasure {μ : Measure X}
+    (h1 : ∀ s, MeasurableSet s → x ∈ s → y ∈ s → μ s = 1)
+    (h2 : ∀ s, MeasurableSet s → x ∈ s → y ∉ s → μ s = toNNReal p)
+    (h3 : ∀ s, MeasurableSet s → x ∉ s → y ∈ s → μ s = toNNReal (σ p))
+    (h4 : ∀ s, MeasurableSet s → x ∉ s → y ∉ s → μ s = 0) :
+    μ = Ber(x, y, p) := by
+  ext s hs
+  by_cases hx : x ∈ s <;> by_cases hy : y ∈ s <;> simp_all
+
 section Integral
 
 variable {E : Type*} [NormedAddCommGroup E]
 
+@[simp]
+lemma memLp_bernoulliMeasure [MeasurableSingletonClass X] (x y : X) (p : I) (f : X → E) (q : ℝ≥0∞) :
+    MemLp f q Ber(x, y, p) := by
+  simp [bernoulliMeasure_def, memLp_add_measure, MemLp.smul_measure_nnreal]
+
+@[simp]
 lemma integrable_bernoulliMeasure [MeasurableSingletonClass X] (x y : X) (p : I) (f : X → E) :
-    Integrable f Ber(x, y, p) := by
-  simp [bernoulliMeasure_def, integrable_add_measure, integrable_dirac,
-    Integrable.smul_measure_nnreal]
+    Integrable f Ber(x, y, p) :=
+  memLp_one_iff_integrable.1 (memLp_bernoulliMeasure ..)
 
 variable [NormedSpace ℝ E] [CompleteSpace E]
 
@@ -178,6 +193,58 @@ lemma integral_bernoulliMeasure [MeasurableSingletonClass X] (x y : X) (p : I) (
   · simp [NNReal.smul_def]
   all_goals exact (integrable_dirac (by simp)).smul_measure_nnreal
 
+lemma integral_id_bernoulliMeasure : ∫ x : ℝ, x ∂Ber(1, 0, p) = p := by
+  simp [integral_bernoulliMeasure]
+
+lemma variance_id_bernoulliMeasure : Var[id; Ber(1, 0, p)] = p * (1 - p) := by
+  rw [variance_eq_integral (by fun_prop)]
+  simp [integral_bernoulliMeasure]
+  ring
+
 end Integral
 
+section HasLaw
+
+/-! ### Bernoulli random variables -/
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
+
+lemma HasLaw.memLp_comp_bernoulliMeasure {E : Type*} [NormedAddCommGroup E]
+    [MeasurableSingletonClass X] {f : Ω → X} (g : X → E) (q : ℝ≥0∞) (hf : HasLaw f Ber(x, y, p) P) :
+    MemLp (g ∘ f) q P :=
+  hf.memLp_comp (by simp)
+
+lemma HasLaw.memLp_bernoulliMeasure [NormedAddCommGroup X] [MeasurableSingletonClass X] {f : Ω → X}
+    (q : ℝ≥0∞) (hf : HasLaw f Ber(x, y, p) P) :
+    MemLp f q P := hf.memLp_comp_bernoulliMeasure id q
+
+lemma HasLaw.integrable_comp_bernoulliMeasure {E : Type*} [NormedAddCommGroup E]
+    [MeasurableSingletonClass X] {f : Ω → X} (g : X → E) (hf : HasLaw f Ber(x, y, p) P) :
+    Integrable (g ∘ f) P :=
+  hf.integrable_comp (by simp)
+
+lemma HasLaw.integrable_bernoulliMeasure [NormedAddCommGroup X] [MeasurableSingletonClass X]
+    {f : Ω → X} (hf : HasLaw f Ber(x, y, p) P) :
+    Integrable f  P := hf.integrable_comp_bernoulliMeasure id
+
+/-- The constant indicator of a set follows a Bernoulli distribution. -/
+theorem hasLaw_indicator_bernoulliMeasure [IsProbabilityMeasure P] {M : Type*} [Zero M]
+    [MeasurableSpace M] (c : M) {s : Set Ω} (hs : NullMeasurableSet s P) :
+    HasLaw (s.indicator (fun _ ↦ c)) Ber(c, 0, ⟨P.real s, by simp⟩) P := by
+  classical
+  have h : AEMeasurable (s.indicator fun _ ↦ c) P := aemeasurable_const.indicator₀ hs
+  refine ⟨h, eq_bernoulliMeasure ?_ ?_ ?_ ?_⟩
+  all_goals
+    intro t ht h1 h2
+    simp_all [map_apply_of_aemeasurable h ht, Set.indicator_const_preimage_eq_union,
+      measure_compl₀ hs, ENNReal.coe_nnreal_eq, ENNReal.ofReal_sub]
+
+/-- The constant indicator of a set follows a Bernoulli distribution. -/
+theorem hasLaw_indicator_one_bernoulliMeasure [IsProbabilityMeasure P] {M : Type*} [Zero M] [One M]
+    [MeasurableSpace M] {s : Set Ω} (hs : NullMeasurableSet s P) :
+    HasLaw (s.indicator (1 : Ω → M)) Ber(1, 0, ⟨P.real s, by simp⟩) P :=
+  hasLaw_indicator_bernoulliMeasure 1 hs
+
+end HasLaw
+
 end ProbabilityTheory