feat(MeasureTheory/Constructions/Polish): generalize topological assu…

…mptions to measurable ones. (#12069)

Several theorems in MeasureTheory/Constructions/Polish.lean about measurable sets, functions, etc. assume that a space is a `BorelSpace` or `OpensMeasurableSpace` for some nice topology. This PR removes the topological data from such theorems when possible, replacing them with sufficient and natural assumptions on `MeasurableSpace`'s.

The old versions of the theorems still work automatically thanks to TC inference. 

*TODO*: Add `CountablySeparated` typeclass abbreviating `HasCountableSeparatingOn _ MeasurableSet univ`. 



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

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -418,6 +418,14 @@ theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {s : Set α} (hs : Measur
   Filter.inf_isMeasurablyGenerated _ _
 #align measurable_set.nhds_within_is_measurably_generated MeasurableSet.nhdsWithin_isMeasurablyGenerated
 
+instance (priority := 100) OpensMeasurableSpace.separatesPoints [T0Space α] :
+    SeparatesPoints α := by
+  rw [separatesPoints_iff]
+  intro x y hxy
+  apply Inseparable.eq
+  rw [inseparable_iff_forall_open]
+  exact fun s hs => hxy _ hs.measurableSet
+
 -- see Note [lower instance priority]
 instance (priority := 100) OpensMeasurableSpace.toMeasurableSingletonClass [T1Space α] :
     MeasurableSingletonClass α :=
@@ -1895,6 +1903,27 @@ theorem tendsto_measure_cthickening_of_isCompact [MetricSpace α] [MeasurableSpa
     ⟨1, zero_lt_one, hs.isBounded.cthickening.measure_lt_top.ne⟩ hs.isClosed
 #align tendsto_measure_cthickening_of_is_compact tendsto_measure_cthickening_of_isCompact
 
+/-- If a measurable space is countably generated and separates points, it arises as
+the borel sets of some second countable t4 topology (i.e. a separable metrizable one). -/
+theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type*)
+    [m : MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] :
+    ∃ τ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α := by
+  rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩
+  letI := induced f inferInstance
+  let F := f.toEquiv.toHomeomorphOfInducing $ inducing_induced _
+  exact ⟨inferInstance, F.secondCountableTopology, F.symm.t4Space,
+    MeasurableEmbedding.borelSpace f.measurableEmbedding F.inducing⟩
+
+/-- If a measurable space on `α` is countably generated and separates points, there is some
+second countable t4 topology on `α` (i.e. a separable metrizable one) for which every
+open set is measurable. -/
+theorem exists_opensMeasurableSpace_of_hasCountableSeparatingOn (α : Type*)
+    [m : MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet univ] :
+    ∃ τ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α := by
+  rcases exists_countablyGenerated_le_of_hasCountableSeparatingOn α with ⟨m', _, _, m'le⟩
+  rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩
+  exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩
+
 namespace Real
 
 open MeasurableSpace MeasureTheory

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Felix Weilacher
 import Mathlib.Data.Real.Cardinality
 import Mathlib.Topology.MetricSpace.Perfect
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+import Mathlib.Topology.CountableSeparatingOn
 
 #align_import measure_theory.constructions.polish from "leanprover-community/mathlib"@"9f55d0d4363ae59948c33864cbc52e0b12e0e8ce"
 
@@ -533,27 +534,30 @@ end MeasureTheory
 
 namespace Measurable
 
-variable {X Y β : Type*} [MeasurableSpace X] [StandardBorelSpace X]
-  [TopologicalSpace Y] [T2Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [MeasurableSpace β]
+variable {X Y Z β : Type*} [MeasurableSpace X] [StandardBorelSpace X]
+  [TopologicalSpace Y] [T0Space Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] [MeasurableSpace β]
+  [MeasurableSpace Z]
 
-/-- If `f : X → Y` is a surjective Borel measurable map from a standard Borel space
-to a topological space with second countable topology, then the preimage of a set `s`
+/-- If `f : X → Z` is a surjective Borel measurable map from a standard Borel space
+to a countably separated measurable space, then the preimage of a set `s`
 is measurable if and only if the set is measurable.
 One implication is the definition of measurability, the other one heavily relies on `X` being a
 standard Borel space. -/
-theorem measurableSet_preimage_iff_of_surjective [SecondCountableTopology Y] {f : X → Y}
-    (hf : Measurable f) (hsurj : Surjective f) {s : Set Y} :
+theorem measurableSet_preimage_iff_of_surjective [HasCountableSeparatingOn Z MeasurableSet univ]
+    {f : X → Z} (hf : Measurable f) (hsurj : Surjective f) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s := by
   refine ⟨fun h => ?_, fun h => hf h⟩
+  rcases exists_opensMeasurableSpace_of_hasCountableSeparatingOn Z with ⟨τ, _, _, _⟩
   apply AnalyticSet.measurableSet_of_compl
   · rw [← image_preimage_eq s hsurj]
     exact h.analyticSet_image hf
   · rw [← image_preimage_eq sᶜ hsurj]
     exact h.compl.analyticSet_image hf
 #align measurable.measurable_set_preimage_iff_of_surjective Measurable.measurableSet_preimage_iff_of_surjective
 
-theorem map_measurableSpace_eq [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f)
-    (hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = ‹MeasurableSpace Y› :=
+theorem map_measurableSpace_eq  [HasCountableSeparatingOn Z MeasurableSet univ]
+    {f : X → Z} (hf : Measurable f)
+    (hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = ‹MeasurableSpace Z› :=
   MeasurableSpace.ext fun _ => hf.measurableSet_preimage_iff_of_surjective hsurj
 #align measurable.map_measurable_space_eq Measurable.map_measurableSpace_eq
 
@@ -569,64 +573,68 @@ theorem borelSpace_codomain [SecondCountableTopology Y] {f : X → Y} (hf : Meas
   ⟨(hf.map_measurableSpace_eq hsurj).symm.trans <| hf.map_measurableSpace_eq_borel hsurj⟩
 #align measurable.borel_space_codomain Measurable.borelSpace_codomain
 
-/-- If `f : X → Y` is a Borel measurable map from a standard Borel space to a topological space
-with second countable topology, then the preimage of a set `s` is measurable if and only if
-the set is measurable in `Set.range f`. -/
-theorem measurableSet_preimage_iff_preimage_val {f : X → Y} [SecondCountableTopology (range f)]
-    (hf : Measurable f) {s : Set Y} :
+/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
+countably separated measurable space then the preimage of a set `s` is measurable
+if and only if the set is measurable in `Set.range f`. -/
+theorem measurableSet_preimage_iff_preimage_val {f : X → Z}
+    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+    (hf : Measurable f) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet ((↑) ⁻¹' s : Set (range f)) :=
   have hf' : Measurable (rangeFactorization f) := hf.subtype_mk
   hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s) surjective_onto_range
 #align measurable.measurable_set_preimage_iff_preimage_coe Measurable.measurableSet_preimage_iff_preimage_val
 
-/-- If `f : X → Y` is a Borel measurable map from a standard Borel space to a
-topological space with second countable topology and the range of `f` is measurable,
+/-- If `f : X → Z` is a Borel measurable map from a standard Borel space to a
+countably separated measurable space and the range of `f` is measurable,
 then the preimage of a set `s` is measurable
 if and only if the intesection with `Set.range f` is measurable. -/
-theorem measurableSet_preimage_iff_inter_range {f : X → Y} [SecondCountableTopology (range f)]
-    (hf : Measurable f) (hr : MeasurableSet (range f)) {s : Set Y} :
+theorem measurableSet_preimage_iff_inter_range {f : X → Z}
+    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+    (hf : Measurable f) (hr : MeasurableSet (range f)) {s : Set Z} :
     MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f) := by
   rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
     ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
 #align measurable.measurable_set_preimage_iff_inter_range Measurable.measurableSet_preimage_iff_inter_range
 
-/-- If `f : X → Y` is a Borel measurable map from a standard Borel space
-to a topological space with second countable topology,
-then for any measurable space `β` and `g : Y → β`, the composition `g ∘ f` is
+/-- If `f : X → Z` is a Borel measurable map from a standard Borel space
+to a countably separated measurable space,
+then for any measurable space `β` and `g : Z → β`, the composition `g ∘ f` is
 measurable if and only if the restriction of `g` to the range of `f` is measurable. -/
-theorem measurable_comp_iff_restrict {f : X → Y} [SecondCountableTopology (range f)]
-    (hf : Measurable f) {g : Y → β} : Measurable (g ∘ f) ↔ Measurable (restrict (range f) g) :=
+theorem measurable_comp_iff_restrict {f : X → Z}
+    [HasCountableSeparatingOn (range f) MeasurableSet univ]
+    (hf : Measurable f) {g : Z → β} : Measurable (g ∘ f) ↔ Measurable (restrict (range f) g) :=
   forall₂_congr fun s _ => measurableSet_preimage_iff_preimage_val hf (s := g ⁻¹' s)
 #align measurable.measurable_comp_iff_restrict Measurable.measurable_comp_iff_restrict
 
-/-- If `f : X → Y` is a surjective Borel measurable map from a standard Borel space
-to a topological space with second countable topology,
-then for any measurable space `α` and `g : Y → α`, the composition
+/-- If `f : X → Z` is a surjective Borel measurable map from a standard Borel space
+to a countably separated measurable space,
+then for any measurable space `α` and `g : Z → α`, the composition
 `g ∘ f` is measurable if and only if `g` is measurable. -/
-theorem measurable_comp_iff_of_surjective [SecondCountableTopology Y] {f : X → Y}
-    (hf : Measurable f) (hsurj : Surjective f) {g : Y → β} : Measurable (g ∘ f) ↔ Measurable g :=
+theorem measurable_comp_iff_of_surjective [HasCountableSeparatingOn Z MeasurableSet univ]
+    {f : X → Z} (hf : Measurable f) (hsurj : Surjective f)
+    {g : Z → β} : Measurable (g ∘ f) ↔ Measurable g :=
   forall₂_congr fun s _ => measurableSet_preimage_iff_of_surjective hf hsurj (s := g ⁻¹' s)
 #align measurable.measurable_comp_iff_of_surjective Measurable.measurable_comp_iff_of_surjective
 
 end Measurable
 
 theorem Continuous.map_eq_borel {X Y : Type*} [TopologicalSpace X] [PolishSpace X]
-    [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T2Space Y] [SecondCountableTopology Y]
+    [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y]
     {f : X → Y} (hf : Continuous f) (hsurj : Surjective f) :
     MeasurableSpace.map f ‹MeasurableSpace X› = borel Y := by
   borelize Y
   exact hf.measurable.map_measurableSpace_eq hsurj
 #align continuous.map_eq_borel Continuous.map_eq_borel
 
 theorem Continuous.map_borel_eq {X Y : Type*} [TopologicalSpace X] [PolishSpace X]
-    [TopologicalSpace Y] [T2Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f)
+    [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f)
     (hsurj : Surjective f) : MeasurableSpace.map f (borel X) = borel Y := by
   borelize X
   exact hf.map_eq_borel hsurj
 #align continuous.map_borel_eq Continuous.map_borel_eq
 
 instance Quotient.borelSpace {X : Type*} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X]
-    [BorelSpace X] {s : Setoid X} [T2Space (Quotient s)] [SecondCountableTopology (Quotient s)] :
+    [BorelSpace X] {s : Setoid X} [T0Space (Quotient s)] [SecondCountableTopology (Quotient s)] :
     BorelSpace (Quotient s) :=
   ⟨continuous_quotient_mk'.map_eq_borel (surjective_quotient_mk' _)⟩
 #align quotient.borel_space Quotient.borelSpace
@@ -822,7 +830,8 @@ theorem _root_.IsClosed.measurableSet_image_of_continuousOn_injOn
   · rwa [injOn_iff_injective] at f_inj
 #align is_closed.measurable_set_image_of_continuous_on_inj_on IsClosed.measurableSet_image_of_continuousOn_injOn
 
-variable {β : Type*} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β]
+variable {α β : Type*} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β]
+  [MeasurableSpace α]
   {s : Set γ} {f : γ → β}
 
 /-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under
@@ -841,26 +850,28 @@ theorem _root_.MeasurableSet.image_of_continuousOn_injOn [OpensMeasurableSpace 
 
 /-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a standard Borel space,
 then its image under a measurable injective map taking values in a
-second-countable topological space is also Borel-measurable. -/
-theorem _root_.MeasurableSet.image_of_measurable_injOn [OpensMeasurableSpace β]
-    [MeasurableSpace γ] [StandardBorelSpace γ] [SecondCountableTopology β]
+countably separate measurable space is also Borel-measurable. -/
+theorem _root_.MeasurableSet.image_of_measurable_injOn {f : γ → α}
+    [HasCountableSeparatingOn α MeasurableSet univ]
+    [MeasurableSpace γ] [StandardBorelSpace γ]
     (hs : MeasurableSet s) (f_meas : Measurable f) (f_inj : InjOn f s) :
     MeasurableSet (f '' s) := by
   letI := upgradeStandardBorel γ
   let tγ : TopologicalSpace γ := inferInstance
+  rcases exists_opensMeasurableSpace_of_hasCountableSeparatingOn α with ⟨τ, _, _, _⟩
   -- for a finer Polish topology, `f` is continuous. Therefore, one may apply the corresponding
   -- result for continuous maps.
   obtain ⟨t', t't, f_cont, t'_polish⟩ :
-      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ β t' tβ f ∧ @PolishSpace γ t' :=
+      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
     f_meas.exists_continuous
   have M : MeasurableSet[@borel γ t'] s :=
     @Continuous.measurable γ γ t' (@borel γ t')
       (@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl))
       tγ _ _ _ (continuous_id_of_le t't) s hs
   exact
     @MeasurableSet.image_of_continuousOn_injOn γ
-      β _ _ _  s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)
-      M (@Continuous.continuousOn γ β t' tβ f s f_cont) f_inj
+      _ _ _ _  s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)
+      M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj
 #align measurable_set.image_of_measurable_inj_on MeasurableSet.image_of_measurable_injOn
 
 /-- An injective continuous function on a Polish space is a measurable embedding. -/
@@ -893,9 +904,10 @@ theorem _root_.ContinuousOn.measurableEmbedding [BorelSpace β]
 #align continuous_on.measurable_embedding ContinuousOn.measurableEmbedding
 
 /-- An injective measurable function from a standard Borel space to a
-second-countable topological space is a measurable embedding. -/
-theorem _root_.Measurable.measurableEmbedding [OpensMeasurableSpace β]
-    [MeasurableSpace γ] [StandardBorelSpace γ] [SecondCountableTopology β]
+countably separated measurable space is a measurable embedding. -/
+theorem _root_.Measurable.measurableEmbedding {f : γ → α}
+    [HasCountableSeparatingOn α MeasurableSet univ]
+    [MeasurableSpace γ] [StandardBorelSpace γ]
     (f_meas : Measurable f) (f_inj : Injective f) : MeasurableEmbedding f :=
   { injective := f_inj
     measurable := f_meas

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -146,6 +146,12 @@ theorem exists_measurableSet_of_ne [MeasurableSpace α] [SeparatesPoints α] {x
   contrapose! h
   exact separatesPoints_def h
 
+theorem separatesPoints_iff [MeasurableSpace α] : SeparatesPoints α ↔
+    ∀ x y : α, (∀ s, MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y :=
+  ⟨fun h => fun _ _ hxy => h.separates _ _ fun _ hs xs => (hxy _ hs).mp xs,
+    fun h => ⟨fun _ _ hxy => h _ _ fun _ hs =>
+    ⟨fun xs => hxy _ hs xs, not_imp_not.mp fun xs => hxy _ hs.compl xs⟩⟩⟩
+
 /-- If the measurable space generated by `S` separates points,
 then this is witnessed by sets in `S`. -/
 theorem separating_of_generateFrom (S : Set (Set α))
@@ -191,11 +197,8 @@ theorem exists_countablyGenerated_le_of_hasCountableSeparatingOn [m : Measurable
   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
+  rw [@separatesPoints_iff]
+  exact fun x y hxy => hb _ trivial _ trivial fun _ hs => hxy _ $ measurableSet_generateFrom hs
 
 open scoped Classical