feat(probability/independence): Kolmogorov's 0-1 law (#16648)

We prove that any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

docs/undergrad.yaml

@@ -536,7 +536,7 @@ Probability Theory:
     independent events: 'probability_theory.Indep_set'
     sigma-algebra: 'measurable_space'
     independent sigma-algebra: 'probability_theory.Indep'
-    $0$-$1$ law: ''
+    $0$-$1$ law: 'probability_theory.measure_zero_or_one_of_measurable_set_limsup_at_top'
     Borel-Cantelli lemma (easy direction): 'measure_theory.measure_limsup_eq_zero'
     Borel-Cantelli lemma (difficult direction): ''
     conditional probability: 'probability_theory.cond'

src/algebra/big_operators/basic.lean

@@ -821,6 +821,11 @@ lemma prod_extend_by_one [decidable_eq α] (s : finset α) (f : α → β) :
   ∏ i in s, (if i ∈ s then f i else 1) = ∏ i in s, f i :=
 prod_congr rfl $ λ i hi, if_pos hi
 
+@[simp, to_additive]
+lemma prod_ite_mem [decidable_eq α] (s t : finset α) (f : α → β) :
+  ∏ i in s, (if i ∈ t then f i else 1) = ∏ i in (s ∩ t), f i :=
+by rw [← finset.prod_filter, finset.filter_mem_eq_inter]
+
 @[simp, to_additive]
 lemma prod_dite_eq [decidable_eq α] (s : finset α) (a : α) (b : Π x : α, a = x → β) :
   (∏ x in s, (if h : a = x then b x h else 1)) = ite (a ∈ s) (b a rfl) 1 :=

src/data/set/basic.lean

@@ -1232,6 +1232,24 @@ ext $ λ s, subset_empty_iff
 @[simp] theorem powerset_univ : 𝒫 (univ : set α) = univ :=
 eq_univ_of_forall subset_univ
 
+/-! ### Sets defined as an if-then-else -/
+
+lemma mem_dite_univ_right (p : Prop) [decidable p] (t : p → set α) (x : α) :
+  (x ∈ if h : p then t h else univ) ↔ (∀ h : p, x ∈ t h) :=
+by split_ifs; simp [h]
+
+@[simp] lemma mem_ite_univ_right (p : Prop) [decidable p] (t : set α) (x : α) :
+  x ∈ ite p t set.univ ↔ (p → x ∈ t) :=
+mem_dite_univ_right p (λ _, t) x
+
+lemma mem_dite_univ_left (p : Prop) [decidable p] (t : ¬ p → set α) (x : α) :
+  (x ∈ if h : p then univ else t h) ↔ (∀ h : ¬ p, x ∈ t h)  :=
+by split_ifs; simp [h]
+
+@[simp] lemma mem_ite_univ_left (p : Prop) [decidable p] (t : set α) (x : α) :
+  x ∈ ite p set.univ t ↔ (¬ p → x ∈ t) :=
+mem_dite_univ_left p (λ _, t) x
+
 /-! ### If-then-else for sets -/
 
 /-- `ite` for sets: `set.ite t s s' ∩ t = s ∩ t`, `set.ite t s s' ∩ tᶜ = s' ∩ tᶜ`.

src/measure_theory/measurable_space_def.lean

@@ -182,6 +182,11 @@ h₁.inter h₂.compl
   measurable_set (t.ite s₁ s₂) :=
 (h₁.inter ht).union (h₂.diff ht)
 
+lemma measurable_set.ite' {s t : set α} {p : Prop}
+  (hs : p → measurable_set s) (ht : ¬ p → measurable_set t) :
+  measurable_set (ite p s t) :=
+by { split_ifs, exacts [hs h, ht h], }
+
 @[simp] lemma measurable_set.cond {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂)
   {i : bool} : measurable_set (cond i s₁ s₂) :=
 by { cases i, exacts [h₂, h₁] }
@@ -371,6 +376,12 @@ begin
   { exact measurable_set_generate_from ht, },
 end
 
+@[simp] lemma generate_from_singleton_empty : generate_from {∅} = (⊥ : measurable_space α) :=
+by { rw [eq_bot_iff, generate_from_le_iff], simp, }
+
+@[simp] lemma generate_from_singleton_univ : generate_from {set.univ} = (⊥ : measurable_space α) :=
+by { rw [eq_bot_iff, generate_from_le_iff], simp, }
+
 lemma measurable_set_bot_iff {s : set α} : @measurable_set α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
 let b : measurable_space α :=
 { measurable_set'      := λ s, s = ∅ ∨ s = univ,
@@ -419,12 +430,12 @@ theorem measurable_set_supr {ι} {m : ι → measurable_space α} {s : set α} :
 by simp only [supr, measurable_set_Sup, exists_range_iff]
 
 lemma measurable_space_supr_eq (m : ι → measurable_space α) :
-  (⨆ n, m n) = measurable_space.generate_from {s | ∃ n, measurable_set[m n] s} :=
-begin
-  ext s,
-  rw measurable_space.measurable_set_supr,
-  refl,
-end
+  (⨆ n, m n) = generate_from {s | ∃ n, measurable_set[m n] s} :=
+by { ext s, rw measurable_set_supr, refl, }
+
+lemma generate_from_Union_measurable_set (m : ι → measurable_space α) :
+  generate_from (⋃ n, {t | measurable_set[m n] t}) = ⨆ n, m n :=
+(@gi_generate_from α).l_supr_u m
 
 end complete_lattice
 

src/measure_theory/pi_system.lean

@@ -113,6 +113,23 @@ begin
   simpa using hst,
 end
 
+lemma is_pi_system_Union_of_directed_le {α ι} (p : ι → set (set α))
+  (hp_pi : ∀ n, is_pi_system (p n)) (hp_directed : directed (≤) p) :
+  is_pi_system (⋃ n, p n) :=
+begin
+  intros t1 ht1 t2 ht2 h,
+  rw set.mem_Union at ht1 ht2 ⊢,
+  cases ht1 with n ht1,
+  cases ht2 with m ht2,
+  obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m,
+  exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩,
+end
+
+lemma is_pi_system_Union_of_monotone {α ι} [semilattice_sup ι] (p : ι → set (set α))
+  (hp_pi : ∀ n, is_pi_system (p n)) (hp_mono : monotone p) :
+  is_pi_system (⋃ n, p n) :=
+is_pi_system_Union_of_directed_le p hp_pi (monotone.directed_le hp_mono)
+
 section order
 
 variables {α : Type*} {ι ι' : Sort*} [linear_order α]
@@ -435,6 +452,26 @@ begin
     exact generate_from_mono (mem_pi_Union_Inter_of_measurable_set m hpS hpi), },
 end
 
+lemma generate_from_pi_Union_Inter_subsets {α ι} (m : ι → measurable_space α) (S : set ι) :
+  generate_from (pi_Union_Inter (λ i, {t | measurable_set[m i] t}) {t : finset ι | ↑t ⊆ S})
+    = ⨆ i ∈ S, m i :=
+begin
+  rw generate_from_pi_Union_Inter_measurable_space,
+  simp only [set.mem_set_of_eq, exists_prop, supr_exists],
+  congr' 1,
+  ext1 i,
+  by_cases hiS : i ∈ S,
+  { simp only [hiS, csupr_pos],
+    refine le_antisymm (supr₂_le (λ t ht, le_rfl)) _,
+    rw le_supr_iff,
+    intros m' hm',
+    specialize hm' {i},
+    simpa only [hiS, finset.coe_singleton, set.singleton_subset_iff, finset.mem_singleton,
+      eq_self_iff_true, and_self, csupr_pos] using hm', },
+  { simp only [hiS, supr_false, supr₂_eq_bot, and_imp],
+    exact λ t htS hit, absurd (htS hit) hiS, },
+end
+
 end Union_Inter
 
 namespace measurable_space