feat(measure_theory/constructions): add the Borel isomorphism theorem. (

#18864)

Add a file `measure_theory/constructions/borel_isomorphism.lean` with several versions of the Borel isomorphism theorem. Also add fairly small supporting lemmas in several other files. Most notable here is the addition of a type class for measurable_spaces whose sigma-algebras are generated by some countable set, and a theorem that such spaces admit measurable injections to the Cantor space.



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

src/measure_theory/constructions/borel_space.lean

@@ -258,6 +258,16 @@ instance subtype.opens_measurable_space {α : Type*} [topological_space α] [mea
   opens_measurable_space s :=
 ⟨by { rw [borel_comap], exact comap_mono h.1 }⟩
 
+@[priority 100]
+instance borel_space.countably_generated {α : Type*} [topological_space α] [measurable_space α]
+  [borel_space α] [second_countable_topology α] : countably_generated α :=
+begin
+  obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α,
+  refine ⟨⟨b, bct, _⟩⟩,
+  borelize α,
+  exact hb.borel_eq_generate_from,
+end
+
 theorem _root_.measurable_set.induction_on_open [topological_space α] [measurable_space α]
   [borel_space α] {C : set α → Prop} (h_open : ∀ U, is_open U → C U)
   (h_compl : ∀ t, measurable_set t → C t → C tᶜ)

src/measure_theory/constructions/polish.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Sébastien Gouëzel, Felix Weilacher
 -/
-import topology.metric_space.polish
+import topology.perfect
 import measure_theory.constructions.borel_space
 
 /-!
@@ -29,7 +29,7 @@ Then, we show Lusin's theorem that two disjoint analytic sets can be separated b
 * `analytic_set.measurably_separable` shows that two disjoint analytic sets are separated by a
   Borel set.
 
-Finally, we prove the Lusin-Souslin theorem that a continuous injective image of a Borel subset of
+We then prove the Lusin-Souslin theorem that a continuous injective image of a Borel subset of
 a Polish space is Borel. The proof of this nontrivial result relies on the above results on
 analytic sets.
 
@@ -43,6 +43,11 @@ analytic sets.
   to a second-countable topological space is a measurable embedding.
 * `is_clopenable_iff_measurable_set`: in a Polish space, a set is clopenable (i.e., it can be made
   open and closed by using a finer Polish topology) if and only if it is Borel-measurable.
+
+We use this to prove several versions of the Borel isomorphism theorem.
+
+* `measurable_equiv_of_not_countable` : Any two uncountable Polish spaces are Borel isomorphic.
+* `equiv.measurable_equiv` : Any two Polish spaces of the same cardinality are Borel. isomorphic.
 -/
 
 open set function polish_space pi_nat topological_space metric filter
@@ -709,3 +714,70 @@ begin
 end
 
 end measure_theory
+
+/-! ### The Borel Isomorphism Theorem -/
+
+/-Note: Move to topology/metric_space/polish when porting. -/
+@[priority 50]
+instance polish_of_countable [h : countable α] [discrete_topology α] : polish_space α :=
+begin
+  obtain ⟨f, hf⟩ := h.exists_injective_nat,
+  have : closed_embedding f,
+  { apply closed_embedding_of_continuous_injective_closed continuous_of_discrete_topology hf,
+    exact λ t _, is_closed_discrete _, },
+  exact this.polish_space,
+end
+
+/-Note: This is to avoid a loop in TC inference. When ported to Lean 4, this will not
+be necessary, and `second_countable_of_polish` should probably
+just be added as an instance soon after the definition of `polish_space`.-/
+private lemma second_countable_of_polish [h : polish_space α] : second_countable_topology α :=
+h.second_countable
+
+local attribute [-instance] polish_space_of_complete_second_countable
+local attribute [instance] second_countable_of_polish
+
+namespace polish_space
+
+variables {β : Type*} [topological_space β] [polish_space α] [polish_space β]
+variables [measurable_space α] [measurable_space β] [borel_space α] [borel_space β]
+
+noncomputable theory
+
+/-- If two Polish spaces admit Borel measurable injections to one another,
+then they are Borel isomorphic.-/
+def borel_schroeder_bernstein
+  {f : α → β} {g : β → α}
+  (fmeas : measurable f) (finj : function.injective f)
+  (gmeas : measurable g) (ginj : function.injective g) :
+  α ≃ᵐ β :=
+(fmeas.measurable_embedding finj).schroeder_bernstein (gmeas.measurable_embedding ginj)
+
+/-- Any uncountable Polish space is Borel isomorphic to the Cantor space `ℕ → bool`.-/
+def measurable_equiv_nat_bool_of_not_countable (h : ¬ countable α) : α ≃ᵐ (ℕ → bool) :=
+begin
+  apply nonempty.some,
+  obtain ⟨f, -, fcts, finj⟩ := is_closed_univ.exists_nat_bool_injection_of_not_countable
+    (by rwa [← countable_coe_iff, (equiv.set.univ _).countable_iff]),
+  obtain ⟨g, gmeas, ginj⟩ := measurable_space.measurable_injection_cantor_of_countably_generated α,
+  exact ⟨borel_schroeder_bernstein gmeas ginj fcts.measurable finj⟩,
+end
+
+/-- The **Borel Isomorphism Theorem**: Any two uncountable Polish spaces are Borel isomorphic.-/
+def measurable_equiv_of_not_countable (hα : ¬ countable α) (hβ : ¬ countable β ) : α ≃ᵐ β :=
+(measurable_equiv_nat_bool_of_not_countable hα).trans
+  (measurable_equiv_nat_bool_of_not_countable hβ).symm
+
+/-- The **Borel Isomorphism Theorem**: If two Polish spaces have the same cardinality,
+they are Borel isomorphic.-/
+def equiv.measurable_equiv (e : α ≃ β) : α ≃ᵐ β :=
+begin
+  by_cases h : countable α,
+  { letI := h,
+    letI := countable.of_equiv α e,
+    use e; apply measurable_of_countable, },
+  refine measurable_equiv_of_not_countable h _,
+  rwa e.countable_iff at h,
+end
+
+end polish_space

src/measure_theory/measurable_space.lean

@@ -315,6 +315,10 @@ begin
   { simp only [preimage_singleton_eq_empty.2 hyf, measurable_set.empty] }
 end
 
+lemma measurable_to_countable' [measurable_space α] [countable α] [measurable_space β] {f : β → α}
+  (h : ∀ x, measurable_set (f ⁻¹' {x})) : measurable f :=
+measurable_to_countable (λ y, h (f y))
+
 @[measurability] lemma measurable_unit [measurable_space α] (f : unit → α) : measurable f :=
 measurable_from_top
 
@@ -327,6 +331,15 @@ measurable_from_top
 lemma measurable_to_nat {f : α → ℕ} : (∀ y, measurable_set (f ⁻¹' {f y})) → measurable f :=
 measurable_to_countable
 
+lemma measurable_to_bool {f : α → bool} (h : measurable_set (f⁻¹' {tt})) : measurable f :=
+begin
+  apply measurable_to_countable',
+  rintros (-|-),
+  { convert h.compl,
+    rw [← preimage_compl, bool.compl_singleton, bool.bnot_tt] },
+  exact h,
+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) :=
@@ -1364,6 +1377,57 @@ end
 
 end measurable_embedding
 
+section countably_generated
+
+namespace measurable_space
+
+variable (α)
+
+/-- We say a measurable space is countably generated
+if can be generated by a countable set of sets.-/
+class countably_generated [m : measurable_space α] : Prop :=
+  (is_countably_generated : ∃ b : set (set α), b.countable ∧ m = generate_from b)
+
+open_locale classical
+
+/-- If a measurable space is countably generated, it admits a measurable injection
+into the Cantor space `ℕ → bool` (equipped with the product sigma algebra). -/
+theorem measurable_injection_cantor_of_countably_generated
+[measurable_space α] [h : countably_generated α] [measurable_singleton_class α] :
+∃ f : α → (ℕ → bool), measurable f ∧ function.injective f :=
+begin
+  obtain ⟨b, bct, hb⟩ := h.is_countably_generated,
+  obtain ⟨e, he⟩ := set.countable.exists_eq_range (bct.insert ∅) (insert_nonempty _ _),
+  rw [← generate_from_insert_empty, he] at hb,
+  refine ⟨λ x n, to_bool (x ∈ e n), _, _⟩,
+  { rw measurable_pi_iff,
+    intro n,
+    apply measurable_to_bool,
+    simp only [preimage, mem_singleton_iff, to_bool_iff, set_of_mem_eq],
+    rw hb,
+    apply measurable_set_generate_from,
+    use n, },
+  intros x y hxy,
+  have : ∀ s : set α, measurable_set s → (x ∈ s ↔ y ∈ s) := λ s, by
+  { rw hb,
+    apply generate_from_induction,
+    { rintros - ⟨n, rfl⟩,
+      rw ← bool.to_bool_eq,
+      rw funext_iff at hxy,
+      exact hxy n },
+    { tauto },
+    { intro t,
+      tauto },
+    intros t ht,
+    simp_rw [mem_Union, ht], },
+  specialize this {y} measurable_set_eq,
+  simpa only [mem_singleton, iff_true],
+end
+
+end measurable_space
+
+end countably_generated
+
 namespace filter
 
 variables [measurable_space α]

src/topology/perfect.lean

@@ -3,8 +3,7 @@ Copyright (c) 2022 Felix Weilacher. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Felix Weilacher
 -/
-import topology.separation
-import topology.bases
+import topology.metric_space.polish
 import topology.metric_space.cantor_scheme
 
 /-!
@@ -223,7 +222,7 @@ end
 end kernel
 end basic
 
-section cantor_inj
+section cantor_inj_metric
 
 open function
 open_locale ennreal
@@ -324,4 +323,16 @@ begin
   simpa only [← subtype.val_inj] using hdisj'.map_injective hxy,
 end
 
-end cantor_inj
+end cantor_inj_metric
+
+/-- Any closed uncountable subset of a Polish space admits a continuous injection
+from the Cantor space `ℕ → bool`.-/
+theorem is_closed.exists_nat_bool_injection_of_not_countable {α : Type*}
+  [topological_space α] [polish_space α] {C : set α} (hC : is_closed C) (hunc : ¬ C.countable) :
+  ∃ f : (ℕ → bool) → α, (range f) ⊆ C ∧ continuous f ∧ function.injective f :=
+begin
+  letI := upgrade_polish_space α,
+  obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_is_closed_of_not_countable hC hunc,
+  obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty,
+  exact ⟨f, hfD.trans hDC, hf⟩,
+end