chore(measure_theory/function/uniform_integrable): replace ℕ by a type verifying enough assumptions (#12242)

This PR does not generalize the results of the `uniform_integrable` file much, but using a generic type instead of `ℕ` makes clear where we need assumptions like `encodable`.

Author: RemyDegenne

src/measure_theory/function/uniform_integrable.lean

@@ -35,88 +35,95 @@ section
 
 namespace egorov
 
-/-- Given a sequence of functions `f` and a function `g`, `not_convergent_seq f g i j` is the
-set of elements such that `f k x` and `g x` are separated by at least `1 / (i + 1)` for some
+/-- Given a sequence of functions `f` and a function `g`, `not_convergent_seq f g n j` is the
+set of elements such that `f k x` and `g x` are separated by at least `1 / (n + 1)` for some
 `k ≥ j`.
 
 This definition is useful for Egorov's theorem. -/
-def not_convergent_seq (f : ℕ → α → β) (g : α → β) (i j : ℕ) : set α :=
-⋃ k (hk : j ≤ k), {x | (1 / (i + 1 : ℝ)) < dist (f k x) (g x)}
+def not_convergent_seq [preorder ι] (f : ι → α → β) (g : α → β) (n : ℕ) (j : ι) : set α :=
+⋃ k (hk : j ≤ k), {x | (1 / (n + 1 : ℝ)) < dist (f k x) (g x)}
 
-variables {i j : ℕ} {s : set α} {ε : ℝ} {f : ℕ → α → β} {g : α → β}
+variables {n : ℕ} {i j : ι} {s : set α} {ε : ℝ} {f : ι → α → β} {g : α → β}
 
-lemma mem_not_convergent_seq_iff {x : α} : x ∈ not_convergent_seq f g i j ↔
-  ∃ k (hk : j ≤ k), (1 / (i + 1 : ℝ)) < dist (f k x) (g x) :=
+lemma mem_not_convergent_seq_iff [preorder ι] {x : α} : x ∈ not_convergent_seq f g n j ↔
+  ∃ k (hk : j ≤ k), (1 / (n + 1 : ℝ)) < dist (f k x) (g x) :=
 by { simp_rw [not_convergent_seq, mem_Union], refl }
 
-lemma not_convergent_seq_antitone :
-  antitone (not_convergent_seq f g i) :=
+lemma not_convergent_seq_antitone [preorder ι] :
+  antitone (not_convergent_seq f g n) :=
 λ j k hjk, Union₂_mono' $ λ l hl, ⟨l, le_trans hjk hl, subset.rfl⟩
 
-lemma measure_inter_not_convergent_seq_eq_zero
-  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (i : ℕ) :
-  μ (s ∩ ⋂ j, not_convergent_seq f g i j) = 0 :=
+lemma measure_inter_not_convergent_seq_eq_zero [semilattice_sup ι] [nonempty ι]
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (n : ℕ) :
+  μ (s ∩ ⋂ j, not_convergent_seq f g n j) = 0 :=
 begin
   simp_rw [metric.tendsto_at_top, ae_iff] at hfg,
   rw [← nonpos_iff_eq_zero, ← hfg],
   refine measure_mono (λ x, _),
   simp only [mem_inter_eq, mem_Inter, ge_iff_le, mem_not_convergent_seq_iff],
   push_neg,
   rintro ⟨hmem, hx⟩,
-  refine ⟨hmem, 1 / (i + 1 : ℝ), nat.one_div_pos_of_nat, λ N, _⟩,
+  refine ⟨hmem, 1 / (n + 1 : ℝ), nat.one_div_pos_of_nat, λ N, _⟩,
   obtain ⟨n, hn₁, hn₂⟩ := hx N,
   exact ⟨n, hn₁, hn₂.le⟩
 end
 
 variables [second_countable_topology β] [measurable_space β] [borel_space β]
 
-lemma not_convergent_seq_measurable_set
+lemma not_convergent_seq_measurable_set [preorder ι] [encodable ι]
   (hf : ∀ n, measurable[m] (f n)) (hg : measurable g) :
-  measurable_set (not_convergent_seq f g i j) :=
+  measurable_set (not_convergent_seq f g n j) :=
 measurable_set.Union (λ k, measurable_set.Union_Prop $ λ hk,
   measurable_set_lt measurable_const $ (hf k).dist hg)
 
-lemma measure_not_convergent_seq_tendsto_zero
+lemma measure_not_convergent_seq_tendsto_zero [semilattice_sup ι] [encodable ι]
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
-  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (i : ℕ) :
-  tendsto (λ j, μ (s ∩ not_convergent_seq f g i j)) at_top (𝓝 0) :=
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (n : ℕ) :
+  tendsto (λ j, μ (s ∩ not_convergent_seq f g n j)) at_top (𝓝 0) :=
 begin
-  rw [← measure_inter_not_convergent_seq_eq_zero hfg, inter_Inter],
-  exact tendsto_measure_Inter (λ n, hsm.inter $ not_convergent_seq_measurable_set hf hg)
+  casesI is_empty_or_nonempty ι,
+  { have : (λ j, μ (s ∩ not_convergent_seq f g n j)) = λ j, 0,
+      by simp only [eq_iff_true_of_subsingleton],
+    rw this,
+    exact tendsto_const_nhds, },
+  rw [← measure_inter_not_convergent_seq_eq_zero hfg n, inter_Inter],
+  refine tendsto_measure_Inter (λ n, hsm.inter $ not_convergent_seq_measurable_set hf hg)
     (λ k l hkl, inter_subset_inter_right _ $ not_convergent_seq_antitone hkl)
-    ⟨0, (lt_of_le_of_lt (measure_mono $ inter_subset_left _ _) (lt_top_iff_ne_top.2 hs)).ne⟩
+    ⟨h.some, (lt_of_le_of_lt (measure_mono $ inter_subset_left _ _) (lt_top_iff_ne_top.2 hs)).ne⟩,
 end
 
+variables [semilattice_sup ι] [nonempty ι] [encodable ι]
+
 lemma exists_not_convergent_seq_lt (hε : 0 < ε)
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
-  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (i : ℕ) :
-  ∃ j : ℕ, μ (s ∩ not_convergent_seq f g i j) ≤ ennreal.of_real (ε * 2⁻¹ ^ i) :=
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (n : ℕ) :
+  ∃ j : ι, μ (s ∩ not_convergent_seq f g n j) ≤ ennreal.of_real (ε * 2⁻¹ ^ n) :=
 begin
   obtain ⟨N, hN⟩ := (ennreal.tendsto_at_top ennreal.zero_ne_top).1
-    (measure_not_convergent_seq_tendsto_zero hf hg hsm hs hfg i)
-    (ennreal.of_real (ε * 2⁻¹ ^ i)) _,
+    (measure_not_convergent_seq_tendsto_zero hf hg hsm hs hfg n)
+    (ennreal.of_real (ε * 2⁻¹ ^ n)) _,
   { rw zero_add at hN,
     exact ⟨N, (hN N le_rfl).2⟩ },
   { rw [gt_iff_lt, ennreal.of_real_pos],
-    exact mul_pos hε (pow_pos (by norm_num) _) }
+    exact mul_pos hε (pow_pos (by norm_num) n), }
 end
 
 /-- Given some `ε > 0`, `not_convergent_seq_lt_index` provides the index such that
 `not_convergent_seq` (intersected with a set of finite measure) has measure less than
-`ε * 2⁻¹ ^ i`.
+`ε * 2⁻¹ ^ n`.
 
 This definition is useful for Egorov's theorem. -/
 def not_convergent_seq_lt_index (hε : 0 < ε)
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
-  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (i : ℕ) : ℕ :=
-classical.some $ exists_not_convergent_seq_lt hε hf hg hsm hs hfg i
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (n : ℕ) : ι :=
+classical.some $ exists_not_convergent_seq_lt hε hf hg hsm hs hfg n
 
 lemma not_convergent_seq_lt_index_spec (hε : 0 < ε)
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
-  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (i : ℕ) :
-  μ (s ∩ not_convergent_seq f g i (not_convergent_seq_lt_index hε hf hg hsm hs hfg i)) ≤
-  ennreal.of_real (ε * 2⁻¹ ^ i) :=
-classical.some_spec $ exists_not_convergent_seq_lt hε hf hg hsm hs hfg i
+  (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) (n : ℕ) :
+  μ (s ∩ not_convergent_seq f g n (not_convergent_seq_lt_index hε hf hg hsm hs hfg n)) ≤
+  ennreal.of_real (ε * 2⁻¹ ^ n) :=
+classical.some_spec $ exists_not_convergent_seq_lt hε hf hg hsm hs hfg n
 
 /-- Given some `ε > 0`, `Union_not_convergent_seq` is the union of `not_convergent_seq` with
 specific indicies such that `Union_not_convergent_seq` has measure less equal than `ε`.
@@ -125,7 +132,7 @@ This definition is useful for Egorov's theorem. -/
 def Union_not_convergent_seq (hε : 0 < ε)
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
   (hfg : ∀ᵐ x ∂μ, x ∈ s → tendsto (λ n, f n x) at_top (𝓝 (g x))) : set α :=
-⋃ i, s ∩ not_convergent_seq f g i (not_convergent_seq_lt_index (half_pos hε) hf hg hsm hs hfg i)
+⋃ n, s ∩ not_convergent_seq f g n (not_convergent_seq_lt_index (half_pos hε) hf hg hsm hs hfg n)
 
 lemma Union_not_convergent_seq_measurable_set (hε : 0 < ε)
   (hf : ∀ n, measurable (f n)) (hg : measurable g) (hsm : measurable_set s) (hs : μ s ≠ ∞)
@@ -181,13 +188,14 @@ end
 
 end egorov
 
-variables [second_countable_topology β] [measurable_space β] [borel_space β]
-  {f : ℕ → α → β} {g : α → β} {s : set α}
-
+variables [semilattice_sup ι] [nonempty ι] [encodable ι]
+  [second_countable_topology β] [measurable_space β] [borel_space β]
+  {f : ι → α → β} {g : α → β} {s : set α}
 
-/-- **Egorov's theorem**: If `f : ℕ → α → β` is a sequence of measurable functions that converges
+/-- **Egorov's theorem**: If `f : ι → α → β` is a sequence of measurable functions that converges
 to `g : α → β` almost everywhere on a measurable set `s` of finite measure, then for all `ε > 0`,
 there exists a subset `t ⊆ s` such that `μ t ≤ ε` and `f` converges to `g` uniformly on `s \ t`.
+We require the index type `ι` to be encodable, and usually `ι = ℕ`.
 
 In other words, a sequence of almost everywhere convergent functions converges uniformly except on
 an arbitrarily small set. -/