feat(MeasureTheory.MeasurableSpace.CountablyGenerated): add Separates…

…Points and related theorems (#11048)

the goal of the PR is to clarify the relationship between the following closely related assumptions on a measurable space:
* Being countably generated (`CountablyGenerated`)
* Separating points (`SeparatesPoints`)
* Having a countable separating family of measurable sets (`HasCountableSeparatingOn _ MeasurableSet univ`) 
* Having singletons be measurable (`MeasurableSingletonClass`)

It defines `SeparatesPoints` and registers all implications between combinations of these properties as instances (or rather a minimal set needed to deduce all others). 

It also proves an optimal theorem regarding when a measurable space appears as an induced subspace of the Cantor Space `Nat -> Bool`. This will be used to generalize topological assumptions to measure theoretic ones in some theorems in `MeasureTheory.Constructions.Polish`.



Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -1007,7 +1007,8 @@ noncomputable def measurableEquivNatBoolOfNotCountable (h : ¬Countable α) : α
   obtain ⟨f, -, fcts, finj⟩ :=
     isClosed_univ.exists_nat_bool_injection_of_not_countable
       (by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff])
-  obtain ⟨g, gmeas, ginj⟩ := MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated α
+  obtain ⟨g, gmeas, ginj⟩ :=
+    MeasurableSpace.measurable_injection_nat_bool_of_hasCountableSeparatingOn α
   exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩
 #align polish_space.measurable_equiv_nat_bool_of_not_countable PolishSpace.measurableEquivNatBoolOfNotCountable
 

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -2033,9 +2033,9 @@ lemma measurableSet_tendsto {_ : MeasurableSpace β} [MeasurableSpace γ]
     (v_meas n).2.preimage (hf i)
 
 /-- We say that a collection of sets is countably spanning if a countable subset spans the
-  whole type. This is a useful condition in various parts of measure theory. For example, it is
-  a needed condition to show that the product of two collections generate the product sigma algebra,
-  see `generateFrom_prod_eq`. -/
+whole type. This is a useful condition in various parts of measure theory. For example, it is
+a needed condition to show that the product of two collections generate the product sigma algebra,
+see `generateFrom_prod_eq`. -/
 def IsCountablySpanning (C : Set (Set α)) : Prop :=
   ∃ s : ℕ → Set α, (∀ n, s n ∈ C) ∧ ⋃ n, s n = univ
 #align is_countably_spanning IsCountablySpanning

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -23,19 +23,23 @@ the space such that the measurable space is generated by the union of all partit
 * `MeasurableSpace.countablePartition`: sequences of finer and finer partitions of
   a countably generated space, defined by taking the `memPartion` of an enumeration of the sets in
   `countableGeneratingSet`.
+* `MeasurableSpace.SeparatesPoints` : class stating that a measurable space separates points.
 
 ## Main statements
 
-* `MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated`: if a measurable space is
-  countably generated and separates points, it admits a measurable injection into the Cantor space
+* `MeasurableSpace.measurable_equiv_nat_bool_of_countablyGenerated`: if a measurable space is
+  countably generated and separates points, it is measure equivalent to a subset of the Cantor Space
+  `ℕ → Bool` (equipped with the product sigma algebra).
+* `MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated`: If a measurable space
+  admits a countable sequence of measurable sets separating points,
+  it admits a measurable injection into the Cantor space `ℕ → Bool`
   `ℕ → Bool` (equipped with the product sigma algebra).
 
 The file also contains measurability results about `memPartition`, from which the properties of
 `countablePartition` are deduced.
 
 -/
 
-
 open Set MeasureTheory
 
 namespace MeasurableSpace
@@ -55,7 +59,7 @@ def countableGeneratingSet (α : Type*) [MeasurableSpace α] [h : CountablyGener
   insert ∅ h.isCountablyGenerated.choose
 
 lemma countable_countableGeneratingSet [MeasurableSpace α] [h : CountablyGenerated α] :
-    Countable (countableGeneratingSet α) :=
+    Set.Countable (countableGeneratingSet α) :=
   Countable.insert _ h.isCountablyGenerated.choose_spec.1
 
 lemma generateFrom_countableGeneratingSet [m : MeasurableSpace α] [h : CountablyGenerated α] :
@@ -75,6 +79,20 @@ lemma measurableSet_countableGeneratingSet [MeasurableSpace α] [CountablyGenera
   rw [← generateFrom_countableGeneratingSet (α := α)]
   exact measurableSet_generateFrom hs
 
+/-- A countable sequence of sets generating the measurable space. -/
+def natGeneratingSequence (α : Type*) [MeasurableSpace α] [CountablyGenerated α] : ℕ → (Set α) :=
+  enumerateCountable (countable_countableGeneratingSet (α := α)) ∅
+
+lemma generateFrom_natGeneratingSequence (α : Type*) [m : MeasurableSpace α]
+    [CountablyGenerated α] : generateFrom (range (natGeneratingSequence _)) = m := by
+  rw [natGeneratingSequence, range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
+    generateFrom_countableGeneratingSet]
+
+lemma measurableSet_natGeneratingSequence [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
+    MeasurableSet (natGeneratingSequence α n) :=
+  measurableSet_countableGeneratingSet $ Set.enumerateCountable_mem _
+    empty_mem_countableGeneratingSet n
+
 theorem CountablyGenerated.comap [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) :
     @CountablyGenerated α (.comap f m) := by
   rcases h with ⟨⟨b, hbc, rfl⟩⟩
@@ -99,6 +117,140 @@ instance [MeasurableSpace α] [CountablyGenerated α] [MeasurableSpace β] [Coun
     CountablyGenerated (α × β) :=
   .sup (.comap Prod.fst) (.comap Prod.snd)
 
+section SeparatesPoints
+
+/-- We say that a measurable space separates points if for any two distinct points,
+there is a measurable set containing one but not the other. -/
+class SeparatesPoints (α : Type*) [m : MeasurableSpace α] : Prop where
+  separates : ∀ x y : α, (∀ s, MeasurableSet s → (x ∈ s → y ∈ s)) → x = y
+
+theorem separatesPoints_def [MeasurableSpace α] [hs : SeparatesPoints α] {x y : α}
+    (h : ∀ s, MeasurableSet s → (x ∈ s → y ∈ s)) : x = y := hs.separates _ _ h
+
+theorem exists_measurableSet_of_ne [MeasurableSpace α] [SeparatesPoints α] {x y : α}
+    (h : x ≠ y) : ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s := by
+  contrapose! h
+  exact separatesPoints_def h
+
+/-- If the measurable space generated by `S` separates points,
+then this is witnessed by sets in `S`. -/
+theorem separating_of_generateFrom (S : Set (Set α))
+    [h : @SeparatesPoints α (generateFrom S)] :
+    ∀ x y : α, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y := by
+  letI := generateFrom S
+  intros x y hxy
+  rw [← forall_generateFrom_mem_iff_mem_iff] at hxy
+  exact separatesPoints_def $ fun _ hs => (hxy _ hs).mp
+
+theorem SeparatesPoints.mono {m m' : MeasurableSpace α} [hsep : @SeparatesPoints _ m] (h : m ≤ m') :
+    @SeparatesPoints _ m' := @SeparatesPoints.mk _ m' fun _ _ hxy ↦
+    @SeparatesPoints.separates _ m hsep _ _ fun _ hs ↦ hxy _ (h _ hs)
+
+instance (priority := 100) Subtype.separatesPoints [MeasurableSpace α] [h : SeparatesPoints α]
+    {s : Set α} : SeparatesPoints s :=
+  ⟨fun _ _ hxy ↦ Subtype.val_injective $ h.1 _ _ fun _ ht ↦ hxy _ $ measurable_subtype_coe ht⟩
+
+instance (priority := 100) separatesPoints_of_measurableSingletonClass [MeasurableSpace α]
+    [MeasurableSingletonClass α] : SeparatesPoints α := by
+  refine ⟨fun x y h ↦ ?_⟩
+  specialize h _ (MeasurableSet.singleton x)
+  simp_rw [mem_singleton_iff, forall_true_left] at h
+  exact h.symm
+
+instance (priority := 100) [MeasurableSpace α] {s : Set α}
+    [h : CountablyGenerated s] [SeparatesPoints s] :
+    HasCountableSeparatingOn α MeasurableSet s := by
+  suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
+  rcases h.1 with ⟨b, hbc, hb⟩
+  refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
+  rw [hb] at ‹SeparatesPoints s›
+  convert separating_of_generateFrom b
+  simp
+
+variable (α)
+
+/-- If a measurable space admits a countable separating family of measurable sets,
+there is a countably generated coarser space which still separates points. -/
+theorem exists_countablyGenerated_le_of_hasCountableSeparatingOn [m : MeasurableSpace α]
+    [h : HasCountableSeparatingOn α MeasurableSet univ] :
+    ∃ m' : MeasurableSpace α, @CountablyGenerated _ m' ∧ @SeparatesPoints _ m' ∧ m' ≤ m := by
+  rcases h.1 with ⟨b, bct, hbm, hb⟩
+  refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
+  · use b
+  refine @SeparatesPoints.mk _ (generateFrom b) fun x y hxy ↦ hb _ trivial _ trivial ?_
+  intro s hs
+  use hxy _ (measurableSet_generateFrom hs)
+  contrapose
+  exact hxy _ (measurableSet_generateFrom hs).compl
+
+open scoped Classical
+
+open Function
+
+/-- A map from a measurable space to the Cantor space `ℕ → Bool` induced by a countable
+sequence of sets generating the measurable space. -/
+noncomputable
+def mapNatBool [MeasurableSpace α] [CountablyGenerated α] (x : α) (n : ℕ) :
+    Bool := x ∈ natGeneratingSequence α n
+
+theorem measurable_mapNatBool [MeasurableSpace α] [CountablyGenerated α] :
+    Measurable (mapNatBool α) := by
+  rw [measurable_pi_iff]
+  refine fun n ↦ measurable_to_bool ?_
+  simp only [preimage, mem_singleton_iff, mapNatBool,
+    Bool.decide_iff, setOf_mem_eq]
+  apply measurableSet_natGeneratingSequence
+
+theorem injective_mapNatBool [MeasurableSpace α] [CountablyGenerated α]
+    [SeparatesPoints α] : Injective (mapNatBool α) := by
+  intro x y hxy
+  rw [← generateFrom_natGeneratingSequence α] at *
+  apply separating_of_generateFrom (range (natGeneratingSequence _))
+  rintro - ⟨n, rfl⟩
+  rw [← decide_eq_decide]
+  exact congr_fun hxy n
+
+/-- If a measurable space is countably generated and separates points, it is measure equivalent
+to some some subset of the Cantor space `ℕ → Bool` (equipped with the product sigma algebra).
+Note: `s` need not be measurable, so this map need not be a `MeasurableEmbedding` to
+the Cantor Space. -/
+theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α]
+    [CountablyGenerated α] [SeparatesPoints α] :
+    ∃ s : Set (ℕ → Bool), Nonempty (α ≃ᵐ s) := by
+  use range (mapNatBool α), Equiv.ofInjective _ $
+    injective_mapNatBool _,
+    Measurable.subtype_mk $ measurable_mapNatBool _
+  simp_rw [← generateFrom_natGeneratingSequence α]
+  apply measurable_generateFrom
+  rintro _ ⟨n, rfl⟩
+  rw [← Equiv.image_eq_preimage _ _]
+  refine ⟨{y | y n}, by measurability, ?_⟩
+  rw [← Equiv.preimage_eq_iff_eq_image]
+  simp[mapNatBool]
+
+/-- If a measurable space admits a countable sequence of measurable sets separating points,
+it admits a measurable injection into the Cantor space `ℕ → Bool`
+(equipped with the product sigma algebra). -/
+theorem measurable_injection_nat_bool_of_hasCountableSeparatingOn [MeasurableSpace α]
+    [HasCountableSeparatingOn α MeasurableSet univ] :
+    ∃ f : α → ℕ → Bool, Measurable f ∧ Injective f := by
+  rcases exists_countablyGenerated_le_of_hasCountableSeparatingOn α with ⟨m', _, _, m'le⟩
+  refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩
+  exact (measurable_mapNatBool _).mono m'le le_rfl
+
+variable {α}
+
+--TODO: Make this an instance
+theorem measurableSingletonClass_of_hasCountableSeparatingOn
+    [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet univ] :
+    MeasurableSingletonClass α := by
+  rcases measurable_injection_nat_bool_of_hasCountableSeparatingOn α with ⟨f, fmeas, finj⟩
+  refine ⟨fun x ↦ ?_⟩
+  rw [← finj.preimage_image {x}, image_singleton]
+  exact fmeas $ MeasurableSet.singleton _
+
+end SeparatesPoints
+
 instance [MeasurableSpace α] {s : Set α} [h : CountablyGenerated s] [MeasurableSingletonClass s] :
     HasCountableSeparatingOn α MeasurableSet s := by
   suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
@@ -307,21 +459,4 @@ lemma measurableSet_countablePartitionSet (n : ℕ) (a : α) :
     MeasurableSet (countablePartitionSet n a) :=
   measurableSet_countablePartition n (countablePartitionSet_mem n a)
 
-variable (α)
-
-open scoped Classical
-
-/-- If a measurable space is countably generated and separates points, it admits a measurable
-injection into the Cantor space `ℕ → Bool` (equipped with the product sigma algebra). -/
-theorem measurable_injection_nat_bool_of_countablyGenerated [MeasurableSpace α]
-    [HasCountableSeparatingOn α MeasurableSet univ] :
-    ∃ f : α → ℕ → Bool, Measurable f ∧ Function.Injective f := by
-  rcases exists_seq_separating α MeasurableSet.empty univ with ⟨e, hem, he⟩
-  refine ⟨(· ∈ e ·), ?_, ?_⟩
-  · rw [measurable_pi_iff]
-    refine fun n ↦ measurable_to_bool ?_
-    simpa only [preimage, mem_singleton_iff, Bool.decide_iff, setOf_mem_eq] using hem n
-  · exact fun x y h ↦ he x trivial y trivial fun n ↦ decide_eq_decide.1 <| congr_fun h _
-#align measurable_space.measurable_injection_nat_bool_of_countably_generated MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated
-
 end MeasurableSpace