feat(probability/independence): Independence of singletons (#18506)

Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence.

Also add supporting `measurable_space` and `set.preimage` lemmas

Author: YaelDillies

src/data/set/basic.lean

@@ -1906,3 +1906,6 @@ lemma subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : disjoint s t) : s
 hab.left_le_of_le_sup_left h
 
 end disjoint
+
+@[simp] lemma Prop.compl_singleton (p : Prop) : ({p}ᶜ : set Prop) = {¬ p} :=
+ext $ λ q, by simpa [@iff.comm q] using not_iff

src/data/set/image.lean

@@ -71,6 +71,9 @@ theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _
 @[simp] theorem preimage_diff (f : α → β) (s t : set β) :
   f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t := rfl
 
+@[simp] lemma preimage_symm_diff (f : α → β) (s t : set β) :
+  f ⁻¹' (s ∆ t) = (f ⁻¹' s) ∆ (f ⁻¹' t) := rfl
+
 @[simp] theorem preimage_ite (f : α → β) (s t₁ t₂ : set β) :
   f ⁻¹' (s.ite t₁ t₂) = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂) :=
 rfl
@@ -120,6 +123,10 @@ lemma nonempty_of_nonempty_preimage {s : set β} {f : α → β} (hf : (f ⁻¹'
   s.nonempty :=
 let ⟨x, hx⟩ := hf in ⟨f x, hx⟩
 
+@[simp] lemma preimage_singleton_true (p : α → Prop) : p ⁻¹' {true} = {a | p a} := by { ext, simp }
+@[simp] lemma preimage_singleton_false (p : α → Prop) : p ⁻¹' {false} = {a | ¬ p a} :=
+by { ext, simp }
+
 lemma preimage_subtype_coe_eq_compl {α : Type*} {s u v : set α} (hsuv : s ⊆ u ∪ v)
   (H : s ∩ (u ∩ v) = ∅) : (coe : s → α) ⁻¹' u = (coe ⁻¹' v)ᶜ :=
 begin
@@ -1003,6 +1010,9 @@ lemma left_inverse.preimage_preimage {g : β → α} (h : left_inverse g f) (s :
   f ⁻¹' (g ⁻¹' s) = s :=
 by rw [← preimage_comp, h.comp_eq_id, preimage_id]
 
+protected lemma involutive.preimage {f : α → α} (hf : involutive f) : involutive (preimage f) :=
+hf.right_inverse.preimage_preimage
+
 end function
 
 namespace equiv_like

src/measure_theory/measurable_space.lean

@@ -7,6 +7,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import data.prod.tprod
 import group_theory.coset
 import logic.equiv.fin
+import logic.lemmas
 import measure_theory.measurable_space_def
 import order.filter.small_sets
 import order.liminf_limsup
@@ -136,6 +137,12 @@ lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _
 
 end functors
 
+@[simp] lemma map_const {m} (b : β) : measurable_space.map (λ a : α, b) m = ⊤ :=
+eq_top_iff.2 $ by { rintro s hs, by_cases b ∈ s; change measurable_set (preimage _ _); simp [*] }
+
+@[simp] lemma comap_const {m} (b : β) : measurable_space.comap (λ a : α, b) m = ⊥ :=
+eq_bot_iff.2 $ by { rintro _ ⟨s, -, rfl⟩, by_cases b ∈ s; simp [*] }
+
 lemma comap_generate_from {f : α → β} {s : set (set β)} :
   (generate_from s).comap f = generate_from (preimage f '' s) :=
 le_antisymm
@@ -291,13 +298,15 @@ section constructions
 instance : measurable_space empty := ⊤
 instance : measurable_space punit := ⊤ -- this also works for `unit`
 instance : measurable_space bool := ⊤
+instance Prop.measurable_space : measurable_space Prop := ⊤
 instance : measurable_space ℕ := ⊤
 instance : measurable_space ℤ := ⊤
 instance : measurable_space ℚ := ⊤
 
 instance : measurable_singleton_class empty := ⟨λ _, trivial⟩
 instance : measurable_singleton_class punit := ⟨λ _, trivial⟩
 instance : measurable_singleton_class bool := ⟨λ _, trivial⟩
+instance Prop.measurable_singleton_class : measurable_singleton_class Prop := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℕ := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℤ := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℚ := ⟨λ _, trivial⟩
@@ -340,6 +349,15 @@ begin
   exact h,
 end
 
+lemma measurable_to_prop {f : α → Prop} (h : measurable_set (f⁻¹' {true})) : measurable f :=
+begin
+  refine measurable_to_countable' (λ x, _),
+  by_cases hx : x,
+  { simpa [hx] using h },
+  { simpa only [hx, ←preimage_compl, Prop.compl_singleton, not_true, preimage_singleton_false]
+      using h.compl }
+end
+
 lemma measurable_find_greatest' {p : α → ℕ → Prop} [∀ x, decidable_pred (p x)]
   {N : ℕ} (hN : ∀ k ≤ N, measurable_set {x | nat.find_greatest (p x) N = k}) :
   measurable (λ x, nat.find_greatest (p x) N) :=
@@ -860,8 +878,38 @@ end sum
 instance {α} {β : α → Type*} [m : Πa, measurable_space (β a)] : measurable_space (sigma β) :=
 ⨅a, (m a).map (sigma.mk a)
 
+section prop
+variables {p : α → Prop}
+
+variables [measurable_space α]
+
+@[simp] lemma measurable_set_set_of : measurable_set {a | p a} ↔ measurable p :=
+⟨λ h, measurable_to_prop $ by simpa only [preimage_singleton_true], λ h,
+  by simpa using h (measurable_set_singleton true)⟩
+
+@[simp] lemma measurable_mem : measurable (∈ s) ↔ measurable_set s := measurable_set_set_of.symm
+
+alias measurable_set_set_of ↔ _ measurable.set_of
+alias measurable_mem ↔ _ measurable_set.mem
+
+end prop
 end constructions
 
+namespace measurable_space
+
+/-- The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`. -/
+@[simp] lemma generate_from_singleton (s : set α) :
+  generate_from {s} = measurable_space.comap (∈ s) ⊤ :=
+begin
+  classical,
+  letI : measurable_space α := generate_from {s},
+  refine le_antisymm (generate_from_le $ λ t ht, ⟨{true}, trivial, by simp [ht.symm]⟩) _,
+  rintro _ ⟨u, -, rfl⟩,
+  exact (show measurable_set s, from generate_measurable.basic _ $ mem_singleton s).mem trivial,
+end
+
+end measurable_space
+
 /-- A map `f : α → β` is called a *measurable embedding* if it is injective, measurable, and sends
 measurable sets to measurable sets. The latter assumption can be replaced with “`f` has measurable
 inverse `g : range f → α`”, see `measurable_embedding.measurable_range_splitting`,
@@ -1052,6 +1100,9 @@ e.to_equiv.image_eq_preimage s
   measurable_set (e '' s) ↔ measurable_set s :=
 by rw [image_eq_preimage, measurable_set_preimage]
 
+@[simp] lemma map_eq (e : α ≃ᵐ β) : measurable_space.map e ‹_› = ‹_› :=
+e.measurable.le_map.antisymm' $ λ s, e.measurable_set_preimage.1
+
 /-- A measurable equivalence is a measurable embedding. -/
 protected lemma measurable_embedding (e : α ≃ᵐ β) : measurable_embedding e :=
 { injective := e.injective,
@@ -1277,12 +1328,41 @@ def sum_compl {s : set α} [decidable_pred s] (hs : measurable_set s) : s ⊕ (s
   measurable_to_fun := by {apply measurable.sum_elim; exact measurable_subtype_coe},
   measurable_inv_fun :=  measurable.dite measurable_inl measurable_inr hs }
 
+/-- Convert a measurable involutive function `f` to a measurable permutation with
+`to_fun = inv_fun = f`. See also `function.involutive.to_perm`. -/
+@[simps to_equiv] def of_involutive (f : α → α) (hf : involutive f) (hf' : measurable f) : α ≃ᵐ α :=
+{ measurable_to_fun := hf',
+  measurable_inv_fun := hf',
+  ..hf.to_perm _ }
+
+@[simp] lemma of_involutive_apply (f : α → α) (hf : involutive f) (hf' : measurable f) (a : α) :
+  of_involutive f hf hf' a = f a := rfl
+
+@[simp] lemma of_involutive_symm (f : α → α) (hf : involutive f) (hf' : measurable f) :
+  (of_involutive f hf hf').symm = of_involutive f hf hf' := rfl
+
 end measurable_equiv
 
 namespace measurable_embedding
 
 variables [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β} {g : β → α}
 
+@[simp] lemma comap_eq (hf : measurable_embedding f) : measurable_space.comap f ‹_› = ‹_› :=
+hf.measurable.comap_le.antisymm $ λ s h,
+  ⟨_, hf.measurable_set_image' h, hf.injective.preimage_image _⟩
+
+lemma iff_comap_eq :
+  measurable_embedding f ↔
+    injective f ∧ measurable_space.comap f ‹_› = ‹_› ∧ measurable_set (range f) :=
+⟨λ hf, ⟨hf.injective, hf.comap_eq, hf.measurable_set_range⟩, λ hf,
+  { injective := hf.1,
+    measurable := by { rw ←hf.2.1, exact comap_measurable f },
+    measurable_set_image' := begin
+      rw ←hf.2.1,
+      rintro _ ⟨s, hs, rfl⟩,
+      simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2,
+    end }⟩
+
 /-- A set is equivalent to its image under a function `f` as measurable spaces,
   if `f` is a measurable embedding -/
 noncomputable def equiv_image (s : set α) (hf : measurable_embedding f) :
@@ -1377,6 +1457,19 @@ end
 
 end measurable_embedding
 
+lemma measurable_space.comap_compl {m' : measurable_space β} [boolean_algebra β]
+  (h : measurable (compl : β → β)) (f : α → β) :
+  measurable_space.comap (λ a, (f a)ᶜ) infer_instance = measurable_space.comap f infer_instance :=
+begin
+  rw ←measurable_space.comap_comp,
+  congr',
+  exact (measurable_equiv.of_involutive _ compl_involutive h).measurable_embedding.comap_eq,
+end
+
+@[simp] lemma measurable_space.comap_not (p : α → Prop) :
+  measurable_space.comap (λ a, ¬ p a) infer_instance = measurable_space.comap p infer_instance :=
+measurable_space.comap_compl (λ _ _, trivial) _
+
 section countably_generated
 
 namespace measurable_space

src/measure_theory/measurable_space_def.lean

@@ -196,7 +196,7 @@ by { cases i, exacts [h₂, h₁] }
   measurable_set (disjointed f n) :=
 disjointed_rec (λ t i ht, measurable_set.diff ht $ h _) (h n)
 
-@[simp] lemma measurable_set.const (p : Prop) : measurable_set {a : α | p} :=
+lemma measurable_set.const (p : Prop) : measurable_set {a : α | p} :=
 by { by_cases p; simp [h, measurable_set.empty]; apply measurable_set.univ }
 
 /-- Every set has a measurable superset. Declare this as local instance as needed. -/
@@ -377,10 +377,10 @@ begin
   { exact measurable_set_generate_from ht, },
 end
 
-@[simp] lemma generate_from_singleton_empty : generate_from {∅} = (⊥ : measurable_space α) :=
+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 α) :=
+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) :=

src/probability/independence/basic.lean

@@ -64,7 +64,7 @@ when defining `μ` in the example above, the measurable space used is the last o
 Part A, Chapter 4.
 -/
 
-open measure_theory measurable_space
+open measure_theory measurable_space set
 open_locale big_operators measure_theory ennreal
 
 namespace probability_theory
@@ -577,7 +577,8 @@ We prove the following equivalences on `indep_set`, for measurable sets `s, t`.
 * `indep_set s t μ ↔ indep_sets {s} {t} μ`.
 -/
 
-variables {s t : set Ω} (S T : set (set Ω))
+variables {s t : set Ω} (S T : set (set Ω)) {π : ι → set (set Ω)} {f : ι → set Ω}
+  {m0 : measurable_space Ω} {μ : measure Ω}
 
 lemma indep_set_iff_indep_sets_singleton {m0 : measurable_space Ω}
   (hs_meas : measurable_set s) (ht_meas : measurable_set t)
@@ -624,6 +625,40 @@ lemma indep_iff_forall_indep_set (m₁ m₂ : measurable_space Ω) {m0 : measura
   λ h s t hs ht, h s t hs ht s t (measurable_set_generate_from (set.mem_singleton s))
     (measurable_set_generate_from (set.mem_singleton t))⟩
 
+lemma Indep_sets.meas_Inter [fintype ι] (h : Indep_sets π μ) (hf : ∀ i, f i ∈ π i) :
+  μ (⋂ i, f i) = ∏ i, μ (f i) :=
+by simp [← h _ (λ i _, hf _)]
+
+lemma Indep_comap_mem_iff : Indep (λ i, measurable_space.comap (∈ f i) ⊤) μ ↔ Indep_set f μ :=
+by { simp_rw ←generate_from_singleton, refl }
+
+alias Indep_comap_mem_iff ↔ _ Indep_set.Indep_comap_mem
+
+lemma Indep_sets_singleton_iff :
+  Indep_sets (λ i, {f i}) μ ↔ ∀ t, μ (⋂ i ∈ t, f i) = ∏ i in t, μ (f i) :=
+forall_congr $ λ t,
+  ⟨λ h, h $ λ _ _, mem_singleton _,
+  λ h f hf, begin
+    refine eq.trans _ (h.trans $ finset.prod_congr rfl $ λ i hi, congr_arg _ $ (hf i hi).symm),
+    rw Inter₂_congr hf,
+  end⟩
+
+variables [is_probability_measure μ]
+
+lemma Indep_set_iff_Indep_sets_singleton (hf : ∀ i, measurable_set (f i)) :
+  Indep_set f μ ↔ Indep_sets (λ i, {f i}) μ :=
+⟨Indep.Indep_sets $ λ _, rfl, Indep_sets.Indep _
+  (λ i, generate_from_le $ by { rintro t (rfl : t = _), exact hf _}) _
+    (λ _, is_pi_system.singleton _) $ λ _, rfl⟩
+
+lemma Indep_set_iff_measure_Inter_eq_prod (hf : ∀ i, measurable_set (f i)) :
+  Indep_set f μ ↔ ∀ s, μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) :=
+(Indep_set_iff_Indep_sets_singleton hf).trans Indep_sets_singleton_iff
+
+lemma Indep_sets.Indep_set_of_mem (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, measurable_set (f i))
+  (hπ : Indep_sets π μ) : Indep_set f μ :=
+(Indep_set_iff_measure_Inter_eq_prod hf).2 $ λ t, hπ _ $ λ i _, hfπ _
+
 end indep_set
 
 section indep_fun