feat(probability/independence): lemmas about pi_Union_Inter of a sequ…

…ence of singletons (#17013)

Co-authored-by: Kexing Ying



Co-authored-by: JasonKYi <kexing.ying19@imperial.ac.uk>

src/measure_theory/pi_system.lean

@@ -325,18 +325,79 @@ end
 
 section Union_Inter
 
+variables {α ι : Type*}
+
 /-! ### π-system generated by finite intersections of sets of a π-system family -/
 
 /-- From a set of indices `S : set ι` and a family of sets of sets `π : ι → set (set α)`,
 define the set of sets that can be written as `⋂ x ∈ t, f x` for some finset `t ⊆ S` and sets
 `f x ∈ π x`. If `π` is a family of π-systems, then it is a π-system. -/
-def pi_Union_Inter {α ι} (π : ι → set (set α)) (S : set ι) : set (set α) :=
+def pi_Union_Inter (π : ι → set (set α)) (S : set ι) : set (set α) :=
 {s : set α | ∃ (t : finset ι) (htS : ↑t ⊆ S) (f : ι → set α) (hf : ∀ x, x ∈ t → f x ∈ π x),
   s = ⋂ x ∈ t, f x}
 
-/-- If `S` is union-closed and `π` is a family of π-systems, then `pi_Union_Inter π S` is a
-π-system. -/
-lemma is_pi_system_pi_Union_Inter {α ι} (π : ι → set (set α))
+lemma pi_Union_Inter_singleton (π : ι → set (set α)) (i : ι) :
+  pi_Union_Inter π {i} = π i ∪ {univ} :=
+begin
+  ext1 s,
+  simp only [pi_Union_Inter, exists_prop, mem_union],
+  refine ⟨_, λ h, _⟩,
+  { rintros ⟨t, hti, f, hfπ, rfl⟩,
+    simp only [subset_singleton_iff, finset.mem_coe] at hti,
+    by_cases hi : i ∈ t,
+    { have ht_eq_i : t = {i},
+      { ext1 x, rw finset.mem_singleton, exact ⟨λ h, hti x h, λ h, h.symm ▸ hi⟩, },
+      simp only [ht_eq_i, finset.mem_singleton, Inter_Inter_eq_left],
+      exact or.inl (hfπ i hi), },
+     { have ht_empty : t = ∅,
+      { ext1 x,
+        simp only [finset.not_mem_empty, iff_false],
+        exact λ hx, hi (hti x hx ▸ hx), },
+      simp only [ht_empty, Inter_false, Inter_univ, set.mem_singleton univ, or_true], }, },
+  { cases h with hs hs,
+    { refine ⟨{i}, _, λ _, s, ⟨λ x hx, _, _⟩⟩,
+      { rw finset.coe_singleton, },
+      { rw finset.mem_singleton at hx,
+        rwa hx, },
+      { simp only [finset.mem_singleton, Inter_Inter_eq_left], }, },
+    { refine ⟨∅, _⟩,
+      simpa only [finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, is_empty.forall_iff,
+        implies_true_iff, finset.not_mem_empty, Inter_false, Inter_univ, true_and, exists_const]
+        using hs, }, },
+end
+
+lemma pi_Union_Inter_singleton_left (s : ι → set α) (S : set ι) :
+  pi_Union_Inter (λ i, ({s i} : set (set α))) S
+    = {s' : set α | ∃ (t : finset ι) (htS : ↑t ⊆ S), s' = ⋂ i ∈ t, s i} :=
+begin
+  ext1 s',
+  simp_rw [pi_Union_Inter, set.mem_singleton_iff, exists_prop, set.mem_set_of_eq],
+  refine ⟨λ h, _, λ ⟨t, htS, h_eq⟩, ⟨t, htS, s, λ _ _, rfl, h_eq⟩⟩,
+  obtain ⟨t, htS, f, hft_eq, rfl⟩ := h,
+  refine ⟨t, htS, _⟩,
+  congr' with i x,
+  simp_rw set.mem_Inter,
+  exact ⟨λ h hit, by { rw ← hft_eq i hit, exact h hit, },
+    λ h hit, by { rw hft_eq i hit, exact h hit, }⟩,
+end
+
+lemma generate_from_pi_Union_Inter_singleton_left (s : ι → set α) (S : set ι) :
+  generate_from (pi_Union_Inter (λ k, {s k}) S) = generate_from {t | ∃ k ∈ S, s k = t} :=
+begin
+  refine le_antisymm (generate_from_le _) (generate_from_mono _),
+  { rintro _ ⟨I, hI, f, hf, rfl⟩,
+    refine finset.measurable_set_bInter _ (λ m hm, measurable_set_generate_from _),
+    exact ⟨m, hI hm, (hf m hm).symm⟩, },
+  { rintro _ ⟨k, hk, rfl⟩,
+    refine ⟨{k}, λ m hm, _, s, λ i hi, _, _⟩,
+    { rw [finset.mem_coe, finset.mem_singleton] at hm,
+      rwa hm, },
+    { exact set.mem_singleton _, },
+    { simp only [finset.mem_singleton, set.Inter_Inter_eq_left], }, },
+end
+
+/-- If `π` is a family of π-systems, then `pi_Union_Inter π S` is a π-system. -/
+lemma is_pi_system_pi_Union_Inter (π : ι → set (set α))
   (hpi : ∀ x, is_pi_system (π x)) (S : set ι) :
   is_pi_system (pi_Union_Inter π S) :=
 begin
@@ -377,15 +438,15 @@ begin
   { exact absurd hn (by simp [hn1, h]), },
 end
 
-lemma pi_Union_Inter_mono_left {α ι} {π π' : ι → set (set α)} (h_le : ∀ i, π i ⊆ π' i)
-  (S : set ι) :
+lemma pi_Union_Inter_mono_left {π π' : ι → set (set α)} (h_le : ∀ i, π i ⊆ π' i) (S : set ι) :
   pi_Union_Inter π S ⊆ pi_Union_Inter π' S :=
-begin
-  rintros s ⟨t, ht_mem, ft, hft_mem_pi, rfl⟩,
-  exact ⟨t, ht_mem, ft, λ x hxt, h_le x (hft_mem_pi x hxt), rfl⟩,
-end
+λ s ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩, ⟨t, ht_mem, ft, λ x hxt, h_le x (hft_mem_pi x hxt), h_eq⟩
+
+lemma pi_Union_Inter_mono_right {π : ι → set (set α)} {S T : set ι} (hST : S ⊆ T) :
+  pi_Union_Inter π S ⊆ pi_Union_Inter π T :=
+λ s ⟨t, ht_mem, ft, hft_mem_pi, h_eq⟩, ⟨t, ht_mem.trans hST, ft, hft_mem_pi, h_eq⟩
 
-lemma generate_from_pi_Union_Inter_le {α ι} {m : measurable_space α}
+lemma generate_from_pi_Union_Inter_le {m : measurable_space α}
   (π : ι → set (set α)) (h : ∀ n, generate_from (π n) ≤ m) (S : set ι) :
   generate_from (pi_Union_Inter π S) ≤ m :=
 begin
@@ -395,28 +456,27 @@ begin
   exact measurable_set_generate_from (hft_mem_pi x hx_mem),
 end
 
-lemma subset_pi_Union_Inter {α ι} {π : ι → set (set α)} {S : set ι} {i : ι} (his : i ∈ S) :
+lemma subset_pi_Union_Inter {π : ι → set (set α)} {S : set ι} {i : ι} (his : i ∈ S) :
   π i ⊆ pi_Union_Inter π S :=
 begin
-  refine λ t ht_pii, ⟨{i}, _, (λ j, t), ⟨λ m h_pm, _, _⟩⟩,
-  { simp only [his, finset.coe_singleton, singleton_subset_iff], },
-  { rw finset.mem_singleton at h_pm,
-    rwa h_pm, },
-  { simp only [finset.mem_singleton, Inter_Inter_eq_left], },
+  have h_ss : {i} ⊆ S,
+  { intros j hj, rw mem_singleton_iff at hj, rwa hj, },
+  refine subset.trans _ (pi_Union_Inter_mono_right h_ss),
+  rw pi_Union_Inter_singleton,
+  exact subset_union_left _ _,
 end
 
-lemma mem_pi_Union_Inter_of_measurable_set {α ι} (m : ι → measurable_space α)
+lemma mem_pi_Union_Inter_of_measurable_set (m : ι → measurable_space α)
   {S : set ι} {i : ι} (hiS : i ∈ S) (s : set α)
   (hs : measurable_set[m i] s) :
   s ∈ pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S :=
 subset_pi_Union_Inter hiS hs
 
-lemma le_generate_from_pi_Union_Inter {α ι} {π : ι → set (set α)}
-  (S : set ι) {x : ι} (hxS : x ∈ S) :
+lemma le_generate_from_pi_Union_Inter {π : ι → set (set α)} (S : set ι) {x : ι} (hxS : x ∈ S) :
   generate_from (π x) ≤ generate_from (pi_Union_Inter π S) :=
 generate_from_mono (subset_pi_Union_Inter hxS)
 
-lemma measurable_set_supr_of_mem_pi_Union_Inter {α ι} (m : ι → measurable_space α)
+lemma measurable_set_supr_of_mem_pi_Union_Inter (m : ι → measurable_space α)
   (S : set ι) (t : set α) (ht : t ∈ pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S) :
   measurable_set[⨆ i ∈ S, m i] t :=
 begin
@@ -427,7 +487,7 @@ begin
   exact le_supr₂ i hi',
 end
 
-lemma generate_from_pi_Union_Inter_measurable_set {α ι} (m : ι → measurable_space α) (S : set ι) :
+lemma generate_from_pi_Union_Inter_measurable_set (m : ι → measurable_space α) (S : set ι) :
   generate_from (pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S) = ⨆ i ∈ S, m i :=
 begin
   refine le_antisymm _ _,

src/probability/independence.lean

@@ -132,12 +132,12 @@ end definitions
 
 section indep
 
-lemma indep_sets.symm {s₁ s₂ : set (set Ω)} [measurable_space Ω] {μ : measure Ω}
+@[symm] lemma indep_sets.symm {s₁ s₂ : set (set Ω)} [measurable_space Ω] {μ : measure Ω}
   (h : indep_sets s₁ s₂ μ) :
   indep_sets s₂ s₁ μ :=
 by { intros t1 t2 ht1 ht2, rw [set.inter_comm, mul_comm], exact h t2 t1 ht2 ht1, }
 
-lemma indep.symm {m₁ m₂ : measurable_space Ω} [measurable_space Ω] {μ : measure Ω}
+@[symm] lemma indep.symm {m₁ m₂ : measurable_space Ω} [measurable_space Ω] {μ : measure Ω}
   (h : indep m₁ m₂ μ) :
   indep m₂ m₁ μ :=
 indep_sets.symm h
@@ -215,6 +215,16 @@ begin
   exact hyp n t1 t2 ht1 ht2,
 end
 
+lemma indep_sets.bUnion [measurable_space Ω] {s : ι → set (set Ω)} {s' : set (set Ω)}
+  {μ : measure Ω} {u : set ι} (hyp : ∀ n ∈ u, indep_sets (s n) s' μ) :
+  indep_sets (⋃ n ∈ u, s n) s' μ :=
+begin
+  intros t1 t2 ht1 ht2,
+  simp_rw set.mem_Union at ht1,
+  rcases ht1 with ⟨n, hpn, ht1⟩,
+  exact hyp n hpn t1 t2 ht1 ht2,
+end
+
 lemma indep_sets.inter [measurable_space Ω] {s₁ s' : set (set Ω)} (s₂ : set (set Ω))
   {μ : measure Ω} (h₁ : indep_sets s₁ s' μ) :
   indep_sets (s₁ ∩ s₂) s' μ :=
@@ -225,6 +235,15 @@ lemma indep_sets.Inter [measurable_space Ω] {s : ι → set (set Ω)} {s' : set
   indep_sets (⋂ n, s n) s' μ :=
 by {intros t1 t2 ht1 ht2, cases h with n h, exact h t1 t2 (set.mem_Inter.mp ht1 n) ht2 }
 
+lemma indep_sets.bInter [measurable_space Ω] {s : ι → set (set Ω)} {s' : set (set Ω)}
+  {μ : measure Ω} {u : set ι} (h : ∃ n ∈ u, indep_sets (s n) s' μ) :
+  indep_sets (⋂ n ∈ u, s n) s' μ :=
+begin
+  intros t1 t2 ht1 ht2,
+  rcases h with ⟨n, hn, h⟩,
+  exact h t1 t2 (set.bInter_subset_of_mem hn ht1) ht2,
+end
+
 lemma indep_sets_singleton_iff [measurable_space Ω] {s t : set Ω} {μ : measure Ω} :
   indep_sets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t :=
 ⟨λ h, h s t rfl rfl,
@@ -346,6 +365,13 @@ begin
   exact indep_sets.indep_aux h2 hp2 hpm2 hyp ht ht2,
 end
 
+lemma indep_sets.indep' {m : measurable_space Ω}
+  {μ : measure Ω} [is_probability_measure μ] {p1 p2 : set (set Ω)}
+  (hp1m : ∀ s ∈ p1, measurable_set s) (hp2m : ∀ s ∈ p2, measurable_set s)
+  (hp1 : is_pi_system p1) (hp2 : is_pi_system p2) (hyp : indep_sets p1 p2 μ) :
+  indep (generate_from p1) (generate_from p2) μ :=
+hyp.indep (generate_from_le hp1m) (generate_from_le hp2m) hp1 hp2 rfl rfl
+
 variables {m0 : measurable_space Ω} {μ : measure Ω}
 
 lemma indep_sets_pi_Union_Inter_of_disjoint [is_probability_measure μ]
@@ -386,6 +412,24 @@ begin
     finset.union_inter_cancel_right, ht1_eq, ← h_indep p1 ht1_m, ht2_eq, ← h_indep p2 ht2_m],
 end
 
+lemma Indep_set.indep_generate_from_of_disjoint [is_probability_measure μ] {s : ι → set Ω}
+  (hsm : ∀ n, measurable_set (s n)) (hs : Indep_set s μ) (S T : set ι) (hST : disjoint S T) :
+  indep (generate_from {t | ∃ n ∈ S, s n = t}) (generate_from {t | ∃ k ∈ T, s k = t}) μ :=
+begin
+  rw [← generate_from_pi_Union_Inter_singleton_left,
+    ← generate_from_pi_Union_Inter_singleton_left],
+  refine indep_sets.indep'
+    (λ t ht, generate_from_pi_Union_Inter_le _ _ _ _ (measurable_set_generate_from ht))
+    (λ t ht, generate_from_pi_Union_Inter_le _ _ _ _ (measurable_set_generate_from ht))
+    _ _ _,
+  { exact λ k, generate_from_le $ λ t ht, (set.mem_singleton_iff.1 ht).symm ▸ hsm k, },
+  { exact λ k, generate_from_le $ λ t ht, (set.mem_singleton_iff.1 ht).symm ▸ hsm k, },
+  { exact is_pi_system_pi_Union_Inter _ (λ k, is_pi_system.singleton _) _, },
+  { exact is_pi_system_pi_Union_Inter _ (λ k, is_pi_system.singleton _) _, },
+  { classical,
+    exact indep_sets_pi_Union_Inter_of_disjoint (Indep.Indep_sets (λ n, rfl) hs) hST, },
+end
+
 lemma indep_supr_of_disjoint [is_probability_measure μ] {m : ι → measurable_space Ω}
   (h_le : ∀ i, m i ≤ m0) (h_indep : Indep m μ) {S T : set ι} (hST : disjoint S T) :
   indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ :=
@@ -435,7 +479,7 @@ lemma indep_supr_of_antitone [semilattice_inf ι] {Ω} {m : ι → measurable_sp
   indep (⨆ i, m i) m' μ :=
 indep_supr_of_directed_le h_indep h_le h_le' (directed_of_inf hm)
 
-lemma Indep_sets.pi_Union_Inter_singleton {π : ι → set (set Ω)} {a : ι} {S : finset ι}
+lemma Indep_sets.pi_Union_Inter_of_not_mem {π : ι → set (set Ω)} {a : ι} {S : finset ι}
   (hp_ind : Indep_sets π μ) (haS : a ∉ S) :
   indep_sets (pi_Union_Inter π S) (π a) μ :=
 begin
@@ -490,7 +534,7 @@ begin
     have h_le' : ∀ i, generate_from (π i) ≤ m0 := λ i, (h_generate i).symm.trans_le (h_le i),
     have hm_p : m_p ≤ m0 := generate_from_pi_Union_Inter_le π h_le' S,
     exact indep_sets.indep hm_p (h_le a) hp (h_pi a) hS_eq_generate (h_generate a)
-      (h_ind.pi_Union_Inter_singleton ha_notin_S), },
+      (h_ind.pi_Union_Inter_of_not_mem ha_notin_S), },
   refine h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (finset.mem_insert_self a S)) _,
   have h_le_p : ∀ i ∈ S, m i ≤ m_p,
   { intros n hn,
@@ -620,7 +664,7 @@ begin
   { rwa ← indep_set_iff_measure_inter_eq_mul (hf hs) (hg ht) μ, },
 end
 
-lemma indep_fun.symm {mβ : measurable_space β} {f g : Ω → β} (hfg : indep_fun f g μ) :
+@[symm] lemma indep_fun.symm {mβ : measurable_space β} {f g : Ω → β} (hfg : indep_fun f g μ) :
   indep_fun g f μ :=
 hfg.symm