refactor(MeasureTheory/MeasurableSpace/Card): avoid Ordinal.toType (leanprover-community#18199)

vihdzp · vihdzp · commit 42f07b979f97 · 2024-11-19T00:05:26.000Z
We redefine `generateMeasurableRec` so that it's indexed by an ordinal, rather than being indexed by `ω₁.toType`. We also employ `ω₁` and its new API throughout the file.
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Card.lean b/Mathlib/MeasureTheory/MeasurableSpace/Card.lean
@@ -25,147 +25,188 @@ indeed generates this sigma-algebra.
 -/
 
 
-universe u
+universe u v
 
 variable {α : Type u}
 
-open Cardinal Set
-
--- Porting note: fix universe below, not here
-local notation "ω₁" => (Ordinal.toType <| Cardinal.ord (aleph 1))
+open Cardinal Ordinal Set MeasureTheory
 
 namespace MeasurableSpace
 
 /-- 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.
+countable unions of already constructed sets.
+
+We index this construction by an arbitrary ordinal for simplicity, but by `ω₁` we will have
+generated all the sets in the sigma-algebra.
 
 This construction is very similar to that of the Borel hierarchy. -/
-def generateMeasurableRec (s : Set (Set α)) (i : (ω₁ : Type u)) : Set (Set α) :=
-  let S := ⋃ j : Iio i, generateMeasurableRec s (j.1)
+def generateMeasurableRec (s : Set (Set α)) (i : Ordinal) : Set (Set α) :=
+  let S := ⋃ j < i, generateMeasurableRec s j
   s ∪ {∅} ∪ compl '' S ∪ Set.range fun f : ℕ → S => ⋃ n, (f n).1
 termination_by i
-decreasing_by exact j.2
 
-theorem self_subset_generateMeasurableRec (s : Set (Set α)) (i : ω₁) :
+theorem self_subset_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) :
     s ⊆ generateMeasurableRec s i := by
   unfold generateMeasurableRec
   apply_rules [subset_union_of_subset_left]
   exact subset_rfl
 
-theorem empty_mem_generateMeasurableRec (s : Set (Set α)) (i : ω₁) :
+theorem empty_mem_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) :
     ∅ ∈ generateMeasurableRec s i := by
   unfold generateMeasurableRec
   exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))
 
-theorem compl_mem_generateMeasurableRec {s : Set (Set α)} {i j : ω₁} (h : j < i) {t : Set α}
+theorem compl_mem_generateMeasurableRec {s : Set (Set α)} {i j : Ordinal} (h : j < i) {t : Set α}
     (ht : t ∈ generateMeasurableRec s j) : tᶜ ∈ generateMeasurableRec s i := by
   unfold generateMeasurableRec
-  exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion.2 ⟨⟨j, h⟩, ht⟩, rfl⟩)
+  exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)
 
-theorem iUnion_mem_generateMeasurableRec {s : Set (Set α)} {i : ω₁} {f : ℕ → Set α}
+theorem iUnion_mem_generateMeasurableRec {s : Set (Set α)} {i : Ordinal} {f : ℕ → Set α}
     (hf : ∀ n, ∃ j < i, f n ∈ generateMeasurableRec s j) :
-    (⋃ n, f n) ∈ generateMeasurableRec s i := by
+    ⋃ n, f n ∈ generateMeasurableRec s i := by
   unfold generateMeasurableRec
-  exact mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion.2 ⟨⟨j, hj⟩, hf⟩⟩, rfl⟩
+  exact mem_union_right _ ⟨fun n => ⟨f n, let ⟨j, hj, hf⟩ := hf n; mem_iUnion₂.2 ⟨j, hj, hf⟩⟩, rfl⟩
 
-theorem generateMeasurableRec_subset (s : Set (Set α)) {i j : ω₁} (h : i ≤ j) :
-    generateMeasurableRec s i ⊆ generateMeasurableRec s j := fun x hx => by
-  rcases eq_or_lt_of_le h with (rfl | h)
+theorem generateMeasurableRec_mono (s : Set (Set α)) : Monotone (generateMeasurableRec s) := by
+  intro i j h x hx
+  rcases h.eq_or_lt with (rfl | h)
   · exact hx
   · convert iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩
     exact (iUnion_const x).symm
 
-/-- At each step of the inductive construction, the cardinality bound `≤ (max #s 2) ^ ℵ₀` holds. -/
-theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : ω₁) :
+/-- An inductive principle for the elements of `generateMeasurableRec`. -/
+@[elab_as_elim]
+theorem generateMeasurableRec_induction {s : Set (Set α)} {i : Ordinal} {t : Set α}
+    {p : Set α → Prop} (hs : ∀ t ∈ s, p t) (h0 : p ∅)
+    (hc : ∀ u, p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ)
+    (hn : ∀ f : ℕ → Set α,
+      (∀ n, p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)) :
+    t ∈ generateMeasurableRec s i → p t := by
+  suffices H : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t from H i le_rfl t
+  intro k
+  apply WellFoundedLT.induction k
+  intro k IH hk t
+  replace IH := fun j hj => IH j hj (hj.le.trans hk)
+  unfold generateMeasurableRec
+  rintro (((ht | rfl) | ht) | ⟨f, rfl⟩)
+  · exact hs t ht
+  · exact h0
+  · simp_rw [mem_image, mem_iUnion₂] at ht
+    obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht
+    exact hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩
+  · apply hn
+    intro n
+    obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2
+    use IH j hj _ hj', j, hj.trans_le hk
+
+theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
+    generateMeasurableRec s (ω₁ : Ordinal.{v}) =
+      ⋃ i < (ω₁ : Ordinal.{v}), generateMeasurableRec s i := by
+  apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'
+  intro t ht
+  rw [mem_iUnion₂]
+  refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
+  · intro t ht
+    exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩
+  · exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩
+  · rintro u - ⟨j, hj, hj'⟩
+    exact ⟨_, (isLimit_omega 1).succ_lt hj,
+      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩
+  · intro f H
+    choose I hI using fun n => (H n).1
+    simp_rw [exists_prop] at hI
+    refine ⟨_, Ordinal.lsub_lt_ord_lift ?_ fun n => (hI n).1,
+      iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_lsub I n, (hI n).2⟩⟩
+    rw [mk_nat, lift_aleph0, isRegular_aleph_one.cof_omega_eq]
+    exact aleph0_lt_aleph_one
+
+theorem generateMeasurableRec_subset (s : Set (Set α)) (i : Ordinal) :
+    generateMeasurableRec s i ⊆ { t | GenerateMeasurable s t } := by
+  apply WellFoundedLT.induction i
+  exact fun i IH t ht => generateMeasurableRec_induction .basic .empty
+    (fun u _ ⟨j, hj, hj'⟩ => .compl _ (IH j hj hj')) (fun f H => .iUnion _ fun n => (H n).1) ht
+
+/-- `generateMeasurableRec s ω₁` generates precisely the smallest sigma-algebra containing `s`. -/
+theorem generateMeasurable_eq_rec (s : Set (Set α)) :
+    { t | GenerateMeasurable s t } = generateMeasurableRec s ω₁ := by
+  apply (generateMeasurableRec_subset s _).antisymm'
+  intro t ht
+  induction' ht with u hu u _ IH f _ IH
+  · exact self_subset_generateMeasurableRec s _ hu
+  · exact empty_mem_generateMeasurableRec s _
+  · rw [generateMeasurableRec_omega1, mem_iUnion₂] at IH
+    obtain ⟨i, hi, hi'⟩ := IH
+    exact generateMeasurableRec_mono _ ((isLimit_omega 1).succ_lt hi).le
+      (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')
+  · simp_rw [generateMeasurableRec_omega1, mem_iUnion₂, exists_prop] at IH
+    exact iUnion_mem_generateMeasurableRec IH
+
+/-- `generateMeasurableRec` is constant for ordinals `≥ ω₁`. -/
+theorem generateMeasurableRec_of_omega1_le (s : Set (Set α)) {i : Ordinal.{v}} (hi : ω₁ ≤ i) :
+    generateMeasurableRec s i = generateMeasurableRec s (ω₁ : Ordinal.{v}) := by
+  apply (generateMeasurableRec_mono s hi).antisymm'
+  rw [← generateMeasurable_eq_rec]
+  exact generateMeasurableRec_subset s i
+
+/-- At each step of the inductive construction, the cardinality bound `≤ #s ^ ℵ₀` holds. -/
+theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
     #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ := by
+  suffices ∀ i ≤ ω₁, #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ by
+    obtain hi | hi := le_or_lt i ω₁
+    · exact this i hi
+    · rw [generateMeasurableRec_of_omega1_le s hi.le]
+      exact this _ le_rfl
+  intro i
   apply WellFoundedLT.induction i
-  intro i IH
-  have A := aleph0_le_aleph 1
-  have B : aleph 1 ≤ max #s 2 ^ ℵ₀ :=
-    aleph_one_le_continuum.trans (power_le_power_right (le_max_right _ _))
-  have C : ℵ₀ ≤ max #s 2 ^ ℵ₀ := A.trans B
-  have J : #(⋃ j : Iio i, generateMeasurableRec s j.1) ≤ max #s 2 ^ ℵ₀ := by
-    refine (mk_iUnion_le _).trans ?_
-    have D : ⨆ j : Iio i, #(generateMeasurableRec s j) ≤ _ := ciSup_le' fun ⟨j, hj⟩ => IH j hj
-    apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_toType.le) D).trans
-    rw [mul_eq_max A C]
-    exact max_le B le_rfl
+  intro i IH hi
+  have A : 𝔠 ≤ max #s 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)
+  have B := aleph0_le_continuum.trans A
+  have C : #(⋃ j < i, generateMeasurableRec s j) ≤ max #s 2 ^ ℵ₀ := by
+    apply mk_iUnion_Ordinal_lift_le_of_le _ B _
+    · intro j hj
+      exact IH j hj (hj.trans_le hi).le
+    · rw [lift_power, lift_aleph0]
+      rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
+      have H := card_le_of_le_ord hi
+      rw [← Ordinal.lift_card] at H
+      apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
+      rw [lift_max, Cardinal.lift_ofNat]
+      exact le_max_right _ _
   rw [generateMeasurableRec]
-  apply_rules [(mk_union_le _ _).trans, add_le_of_le C, mk_image_le.trans]
-  · exact (le_max_left _ _).trans (self_le_power _ one_lt_aleph0.le)
+  apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
+    mk_image_le.trans]
+  · exact (self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))
   · rw [mk_singleton]
-    exact one_lt_aleph0.le.trans C
+    exact one_lt_aleph0.le.trans B
   · apply mk_range_le.trans
-    simp only [mk_pi, prod_const, lift_uzero, mk_denumerable, lift_aleph0]
-    have := @power_le_power_right _ _ ℵ₀ J
+    simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]
+    have := @power_le_power_right _ _ ℵ₀ C
     rwa [← power_mul, aleph0_mul_aleph0] at this
 
-/-- `generateMeasurableRec s` generates precisely the smallest sigma-algebra containing `s`. -/
-theorem generateMeasurable_eq_rec (s : Set (Set α)) :
-    { t | GenerateMeasurable s t } =
-        ⋃ (i : (aleph 1).ord.toType), generateMeasurableRec s i := by
-  ext t; refine ⟨fun ht => ?_, fun ht => ?_⟩
-  · inhabit ω₁
-    induction ht with
-    | basic u hu => exact mem_iUnion.2 ⟨default, self_subset_generateMeasurableRec s _ hu⟩
-    | empty => exact mem_iUnion.2 ⟨default, empty_mem_generateMeasurableRec s _⟩
-    | compl _ _ IH =>
-      rcases mem_iUnion.1 IH with ⟨i, hi⟩
-      obtain ⟨j, hj⟩ := exists_gt i
-      exact mem_iUnion.2 ⟨j, compl_mem_generateMeasurableRec hj hi⟩
-    | iUnion f _ IH =>
-      have : ∀ n, ∃ i, f n ∈ generateMeasurableRec s i := fun n => by simpa using IH n
-      choose I hI using this
-      refine mem_iUnion.2 ⟨Ordinal.enum (α := ω₁) (· < ·)
-        ⟨Ordinal.lsub fun n => Ordinal.typein.{u} (α := ω₁) (· < ·) (I n), ?_⟩,
-          iUnion_mem_generateMeasurableRec fun n => ⟨I n, ?_, hI n⟩⟩
-      · rw [Ordinal.type_toType]
-        refine Ordinal.lsub_lt_ord_lift ?_ fun i => Ordinal.typein_lt_self _
-        rw [mk_denumerable, lift_aleph0, isRegular_aleph_one.cof_eq]
-        exact aleph0_lt_aleph_one
-      · rw [← Ordinal.typein_lt_typein (· < ·), Ordinal.typein_enum]
-        apply Ordinal.lt_lsub fun n : ℕ => _
-  · rcases ht with ⟨t, ⟨i, rfl⟩, hx⟩
-    revert t
-    apply WellFoundedLT.induction i
-    intro j H t ht
-    unfold generateMeasurableRec at ht
-    rcases ht with (((h | (rfl : t = ∅)) | ⟨u, ⟨-, ⟨⟨k, hk⟩, rfl⟩, hu⟩, rfl⟩) | ⟨f, rfl⟩)
-    · exact .basic t h
-    · exact .empty
-    · exact .compl u (H k hk u hu)
-    · refine .iUnion _ @fun n => ?_
-      obtain ⟨-, ⟨⟨k, hk⟩, rfl⟩, hf⟩ := (f n).prop
-      exact H k hk _ hf
-
 /-- If a sigma-algebra is generated by a set of sets `s`, then the sigma-algebra has cardinality at
-most `(max #s 2) ^ ℵ₀`. -/
+most `max #s 2 ^ ℵ₀`. -/
 theorem cardinal_generateMeasurable_le (s : Set (Set α)) :
     #{ t | GenerateMeasurable s t } ≤ max #s 2 ^ ℵ₀ := by
-  rw [generateMeasurable_eq_rec]
-  apply (mk_iUnion_le _).trans
-  rw [(aleph 1).mk_ord_toType]
-  refine le_trans (mul_le_mul' aleph_one_le_continuum
-      (ciSup_le' fun i => cardinal_generateMeasurableRec_le s i)) ?_
-  refine (mul_le_max_of_aleph0_le_left aleph0_le_continuum).trans (max_le ?_ le_rfl)
-  exact power_le_power_right (le_max_right _ _)
+  rw [generateMeasurable_eq_rec.{u, 0}]
+  exact cardinal_generateMeasurableRec_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 cardinalMeasurableSet_le (s : Set (Set α)) :
+algebra has cardinality at most `max #s 2 ^ ℵ₀`. -/
+theorem cardinal_measurableSet_le (s : Set (Set α)) :
     #{ t | @MeasurableSet α (generateFrom s) t } ≤ max #s 2 ^ ℵ₀ :=
   cardinal_generateMeasurable_le s
 
+@[deprecated cardinal_measurableSet_le (since := "2024-08-30")]
+alias cardinalMeasurableSet_le := cardinal_measurableSet_le
+
 /-- 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_generateMeasurable_le_continuum {s : Set (Set α)} (hs : #s ≤ 𝔠) :
-    #{ t | GenerateMeasurable s t } ≤ 𝔠 :=
-  (cardinal_generateMeasurable_le s).trans
-    (by
-      rw [← continuum_power_aleph0]
-      exact mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le))
+    #{ t | GenerateMeasurable s t } ≤ 𝔠 := by
+  apply (cardinal_generateMeasurable_le s).trans
+  rw [← continuum_power_aleph0]
+  exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)
 
 /-- 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. -/
diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -437,10 +437,6 @@ theorem isLimit_omega (o : Ordinal) : Ordinal.IsLimit (ω_ o) := by
 theorem ord_aleph_isLimit (o : Ordinal) : (ℵ_ o).ord.IsLimit :=
   isLimit_ord <| aleph0_le_aleph _
 
--- TODO: get rid of this instance where it's used.
-instance (o : Ordinal) : NoMaxOrder (ℵ_ o).ord.toType :=
-  toType_noMax_of_succ_lt (isLimit_ord <| aleph0_le_aleph o).2
-
 @[simp]
 theorem range_aleph : range aleph = Set.Ici ℵ₀ := by
   ext c
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean
@@ -899,6 +899,9 @@ theorem IsRegular.aleph0_le {c : Cardinal} (H : c.IsRegular) : ℵ₀ ≤ c :=
 theorem IsRegular.cof_eq {c : Cardinal} (H : c.IsRegular) : c.ord.cof = c :=
   (cof_ord_le c).antisymm H.2
 
+theorem IsRegular.cof_omega_eq {o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o := by
+  rw [← ord_aleph, H.cof_eq]
+
 theorem IsRegular.pos {c : Cardinal} (H : c.IsRegular) : 0 < c :=
   aleph0_pos.trans_le H.1
 
