feat(measure_theory/card_measurable_space): generate_measurable_rec s gives precisely the generated sigma-algebra (#12462)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: vihdzp

src/measure_theory/card_measurable_space.lean

@@ -20,7 +20,8 @@ In particular, if `#s ≤ 𝔠`, then the generated sigma-algebra has cardinalit
 For the proof, we rely on an explicit inductive construction of the sigma-algebra generated by
 `s` (instead of the inductive predicate `generate_measurable`). This transfinite inductive
 construction is parameterized by an ordinal `< ω₁`, and the cardinality bound is preserved along
-each step of the construction.
+each step of the construction. We show in `measurable_space.generate_measurable_eq_rec` that this
+indeed generates this sigma-algebra.
 -/
 
 universe u
@@ -29,21 +30,61 @@ variables {α : Type u}
 open_locale cardinal
 open cardinal set
 
-local notation `ω₁`:= (aleph 1 : cardinal.{u}).ord.out.α
+local notation `ω₁` := (aleph 1 : cardinal.{u}).ord.out.α
 
 namespace measurable_space
 
 /-- Transfinite induction construction of the sigma-algebra generated by a set of sets `s`. At each
 step, we add all elements of `s`, the empty set, the complements of already constructed sets, and
 countable unions of already constructed sets. We index this construction by an ordinal `< ω₁`, as
-this will be enough to generate all sets in the sigma-algebra. -/
+this will be enough to generate all sets in the sigma-algebra.
+
+This construction is very similar to that of the Borel hierarchy. -/
 def generate_measurable_rec (s : set (set α)) : ω₁ → set (set α)
 | i := let S := ⋃ j : {j // j < i}, generate_measurable_rec j.1 in
-    s ∪ {∅} ∪ compl '' S ∪ (set.range (λ (f : ℕ → S), ⋃ n, (f n).1))
+    s ∪ {∅} ∪ compl '' S ∪ set.range (λ (f : ℕ → S), ⋃ n, (f n).1)
 using_well_founded {dec_tac := `[exact j.2]}
 
-/-- At each step of the inductive construction, the cardinality bound `≤ (max (#s) 2) ^ ω`
-holds. -/
+theorem self_subset_generate_measurable_rec (s : set (set α)) (i : ω₁) :
+  s ⊆ generate_measurable_rec s i :=
+begin
+  unfold generate_measurable_rec,
+  apply_rules [subset_union_of_subset_left],
+  exact subset_rfl
+end
+
+theorem empty_mem_generate_measurable_rec (s : set (set α)) (i : ω₁) :
+  ∅ ∈ generate_measurable_rec s i :=
+begin
+  unfold generate_measurable_rec,
+  exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))
+end
+
+theorem compl_mem_generate_measurable_rec {s : set (set α)} {i j : ω₁} (h : j < i) {t : set α}
+  (ht : t ∈ generate_measurable_rec s j) : tᶜ ∈ generate_measurable_rec s i :=
+begin
+  unfold generate_measurable_rec,
+  exact mem_union_left _ (mem_union_right _ ⟨t, mem_Union.2 ⟨⟨j, h⟩, ht⟩, rfl⟩)
+end
+
+theorem Union_mem_generate_measurable_rec {s : set (set α)} {i : ω₁}
+  {f : ℕ → set α} (hf : ∀ n, ∃ j < i, f n ∈ generate_measurable_rec s j) :
+  (⋃ n, f n) ∈ generate_measurable_rec s i :=
+begin
+  unfold generate_measurable_rec,
+  exact mem_union_right _ ⟨λ n, ⟨f n, let ⟨j, hj, hf⟩ := hf n in mem_Union.2 ⟨⟨j, hj⟩, hf⟩⟩, rfl⟩
+end
+
+theorem generate_measurable_rec_subset (s : set (set α)) {i j : ω₁} (h : i ≤ j) :
+  generate_measurable_rec s i ⊆ generate_measurable_rec s j :=
+λ x hx, begin
+  rcases eq_or_lt_of_le h with rfl | h,
+  { exact hx },
+  { convert Union_mem_generate_measurable_rec (λ n, ⟨i, h, hx⟩),
+    exact (Union_const x).symm }
+end
+
+/-- At each step of the inductive construction, the cardinality bound `≤ (max (#s) 2) ^ ω` holds. -/
 lemma cardinal_generate_measurable_rec_le (s : set (set α)) (i : ω₁) :
   #(generate_measurable_rec s i) ≤ (max (#s) 2) ^ omega.{u} :=
 begin
@@ -52,14 +93,12 @@ begin
   have A := omega_le_aleph 1,
   have B : aleph 1 ≤ (max (#s) 2) ^ omega.{u} :=
     aleph_one_le_continuum.trans (power_le_power_right (le_max_right _ _)),
-  have C : omega.{u} ≤ (max (#s) 2) ^ omega.{u} := A.trans B,
+  have C : ω ≤ (max (#s) 2) ^ omega.{u} := A.trans B,
   have J : #(⋃ (j : {j // j < i}), generate_measurable_rec s j.1) ≤ (max (#s) 2) ^ omega.{u},
   { apply (mk_Union_le _).trans,
-    have D : # {j // j < i} ≤ aleph 1 := (mk_subtype_le _).trans (le_of_eq (aleph 1).mk_ord_out),
-    have E : cardinal.sup.{u u}
-      (λ (j : {j // j < i}), #(generate_measurable_rec s j.1)) ≤ (max (#s) 2) ^ omega.{u} :=
-    cardinal.sup_le (λ ⟨j, hj⟩, IH j hj),
-    apply (mul_le_mul' D E).trans,
+    have D : cardinal.sup.{u u} (λ (j : {j // j < i}), #(generate_measurable_rec s j.1)) ≤ _ :=
+      cardinal.sup_le (λ ⟨j, hj⟩, IH j hj),
+    apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_out.le) D).trans,
     rw mul_eq_max A C,
     exact max_le B le_rfl },
   rw [generate_measurable_rec],
@@ -69,70 +108,61 @@ begin
     exact one_lt_omega.le.trans C },
   { apply mk_range_le.trans,
     simp only [mk_pi, subtype.val_eq_coe, prod_const, lift_uzero, mk_denumerable, lift_omega],
-    have := @power_le_power_right _ _ omega.{u} J,
+    have := @power_le_power_right _ _ ω J,
     rwa [← power_mul, omega_mul_omega] at this }
 end
 
-lemma cardinal_Union_generate_measurable_rec_le (s : set (set α)) :
-  #(⋃ i, generate_measurable_rec s i) ≤ (max (#s) 2) ^ omega.{u} :=
+/-- `generate_measurable_rec s` generates precisely the smallest sigma-algebra containing `s`. -/
+theorem generate_measurable_eq_rec (s : set (set α)) :
+  {t | generate_measurable s t} = ⋃ i, generate_measurable_rec s i :=
 begin
+  ext t, refine ⟨λ ht, _, λ ht, _⟩,
+  { inhabit ω₁,
+    induction ht with u hu u hu IH f hf IH,
+    { exact mem_Union.2 ⟨default, self_subset_generate_measurable_rec s _ hu⟩ },
+    { exact mem_Union.2 ⟨default, empty_mem_generate_measurable_rec s _⟩ },
+    { rcases mem_Union.1 IH with ⟨i, hi⟩,
+      obtain ⟨j, hj⟩ := exists_gt i,
+      exact mem_Union.2 ⟨j, compl_mem_generate_measurable_rec hj hi⟩ },
+    { have : ∀ n, ∃ i, f n ∈ generate_measurable_rec s i := λ n, by simpa using IH n,
+      choose I hI using this,
+      refine mem_Union.2 ⟨ordinal.enum (<) (ordinal.lsub (λ n, ordinal.typein.{u} (<) (I n))) _,
+        Union_mem_generate_measurable_rec (λ n, ⟨I n, _, hI n⟩)⟩,
+      { rw ordinal.type_lt,
+        refine ordinal.lsub_lt_ord_lift _ (λ i, ordinal.typein_lt_self _),
+        rw [mk_denumerable, lift_omega, is_regular_aleph_one.2],
+        exact omega_lt_aleph_one },
+      { rw [←ordinal.typein_lt_typein (<), ordinal.typein_enum],
+        apply ordinal.lt_lsub (λ n : ℕ, _) } } },
+  { rcases ht with ⟨t, ⟨i, rfl⟩, hx⟩,
+    revert t,
+    apply (aleph 1).ord.out.wo.wf.induction i,
+    intros j H t ht,
+    unfold generate_measurable_rec at ht,
+    rcases ht with (((h | h) | ⟨u, ⟨-, ⟨⟨k, hk⟩, rfl⟩, hu⟩, rfl⟩) | ⟨f, rfl⟩),
+    { exact generate_measurable.basic t h },
+    { convert generate_measurable.empty },
+    { exact generate_measurable.compl u (H k hk u hu) },
+    { apply generate_measurable.union _ (λ n, _),
+      obtain ⟨-, ⟨⟨k, hk⟩, rfl⟩, hf⟩ := (f n).prop,
+      exact H k hk _ hf } }
+end
+
+/-- If a sigma-algebra is generated by a set of sets `s`, then the sigma-algebra has cardinality at
+most `(max (#s) 2) ^ ω`. -/
+theorem cardinal_generate_measurable_le (s : set (set α)) :
+  #{t | generate_measurable s t} ≤ (max (#s) 2) ^ omega.{u} :=
+begin
+  rw generate_measurable_eq_rec,
   apply (mk_Union_le _).trans,
-  rw [(aleph 1).mk_ord_out],
+  rw (aleph 1).mk_ord_out,
   refine le_trans (mul_le_mul' aleph_one_le_continuum
     (cardinal.sup_le (λ i, cardinal_generate_measurable_rec_le s i))) _,
   have := power_le_power_right (le_max_right (#s) 2),
   rw mul_eq_max omega_le_continuum (omega_le_continuum.trans this),
   exact max_le this le_rfl
 end
 
-/-- A set in the sigma-algebra generated by a set of sets `s` is constructed at some step of the
-transfinite induction defining `generate_measurable_rec`.
-The other inclusion is also true, but not proved here as it is not needed for the cardinality
-bounds.-/
-theorem generate_measurable_subset_rec (s : set (set α)) ⦃t : set α⦄
-  (ht : generate_measurable s t) :
-  t ∈ ⋃ i, generate_measurable_rec s i :=
-begin
-  inhabit ω₁,
-  induction ht with u hu u hu IH f hf IH,
-  { refine mem_Union.2 ⟨default, _⟩,
-    rw generate_measurable_rec,
-    simp only [hu, mem_union_eq, true_or] },
-  { refine mem_Union.2 ⟨default, _⟩,
-    rw generate_measurable_rec,
-    simp only [union_singleton, mem_union_eq, mem_insert_iff, eq_self_iff_true, true_or] },
-  { rcases mem_Union.1 IH with ⟨i, hi⟩,
-    obtain ⟨j, hj⟩ : ∃ j, i < j := ordinal.has_succ_of_type_succ_lt
-      (by { rw ordinal.type_lt, exact (ord_aleph_is_limit 1).2 }) _,
-    apply mem_Union.2 ⟨j, _⟩,
-    rw generate_measurable_rec,
-    have : ∃ a, (a < j) ∧ u ∈ generate_measurable_rec s a := ⟨i, hj, hi⟩,
-    simp [this] },
-  { have : ∀ n, ∃ i, f n ∈ generate_measurable_rec s i := λ n, by simpa using IH n,
-    choose I hI using this,
-    obtain ⟨j, hj⟩ : ∃ j, ∀ k, k ∈ range I → (k < j),
-    { apply ordinal.lt_cof_type,
-      simp only [is_regular_aleph_one.2, mk_singleton, ordinal.type_lt],
-      have : #(range I) = lift.{0} (#(range I)), by simp only [lift_uzero],
-      rw this,
-      apply mk_range_le_lift.trans_lt _,
-      simp [omega_lt_aleph_one] },
-    apply mem_Union.2 ⟨j, _⟩,
-    rw generate_measurable_rec,
-    have : ∃ (g : ℕ → (↥⋃ (i : {i // i < j}), generate_measurable_rec s i.1)),
-      (⋃ (n : ℕ), ↑(g n)) = (⋃ n, f n),
-    { refine ⟨λ n, ⟨f n, _⟩, rfl⟩,
-      exact mem_Union.2 ⟨⟨I n, hj (I n) (mem_range_self _)⟩, hI n⟩ },
-    simp [this] }
-end
-
-/-- If a sigma-algebra is generated by a set of sets `s`, then the sigma
-algebra has cardinality at most `(max (#s) 2) ^ ω`. -/
-theorem cardinal_generate_measurable_le (s : set (set α)) :
-  #{t | generate_measurable s t} ≤ (max (#s) 2) ^ omega.{u} :=
-(mk_subtype_le_of_subset (generate_measurable_subset_rec s)).trans
-  (cardinal_Union_generate_measurable_rec_le s)
-
 /-- If a sigma-algebra is generated by a set of sets `s`, then the sigma
 algebra has cardinality at most `(max (#s) 2) ^ ω`. -/
 theorem cardinal_measurable_set_le (s : set (set α)) :
@@ -143,17 +173,15 @@ cardinal_generate_measurable_le s
 then the sigma algebra has the same cardinality bound. -/
 theorem cardinal_generate_measurable_le_continuum {s : set (set α)} (hs : #s ≤ 𝔠) :
   #{t | generate_measurable s t} ≤ 𝔠 :=
-calc
-#{t | generate_measurable s t}
-    ≤ (max (#s) 2) ^ omega.{u} : cardinal_generate_measurable_le s
-... ≤ 𝔠 ^ omega.{u} :
-  by exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)
-... = 𝔠 : continuum_power_omega
+(cardinal_generate_measurable_le s).trans begin
+  rw ←continuum_power_omega,
+  exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)
+end
 
 /-- If a sigma-algebra is generated by a set of sets `s` with cardinality at most the continuum,
 then the sigma algebra has the same cardinality bound. -/
-theorem cardinal_measurable_set_le_continuum {s : set (set α)} (hs : #s ≤ 𝔠) :
-  #{t | @measurable_set α (generate_from s) t} ≤ 𝔠 :=
-cardinal_generate_measurable_le_continuum hs
+theorem cardinal_measurable_set_le_continuum {s : set (set α)} :
+  #s ≤ 𝔠 → #{t | @measurable_set α (generate_from s) t} ≤ 𝔠 :=
+cardinal_generate_measurable_le_continuum
 
 end measurable_space

src/set_theory/cardinal_ordinal.lean

@@ -229,6 +229,9 @@ end
 theorem ord_aleph_is_limit (o : ordinal) : is_limit (aleph o).ord :=
 ord_is_limit $ omega_le_aleph _
 
+instance (o : ordinal) : no_max_order (aleph o).ord.out.α :=
+ordinal.out_no_max_of_succ_lt (ord_aleph_is_limit o).2
+
 theorem exists_aleph {c : cardinal} : ω ≤ c ↔ ∃ o, c = aleph o :=
 ⟨λ h, ⟨aleph_idx c - ordinal.omega,
   by rw [aleph, ordinal.add_sub_cancel_of_le, aleph'_aleph_idx];