D

formal source

 123    simp only [Function.comp_apply]
 124    exact hρ_eq _
 125
 126private noncomputable def D : ℕ → ℕ := fun n => CE f c R hf n n
 127
 128private theorem D_succ_gt (n : ℕ) : D f c R hf n < D f c R hf (n + 1) := by
 129  show CE f c R hf n n < CE f c R hf (n + 1) (n + 1)
 130  rw [CE_succ]
 131  show CE f c R hf n n < CE f c R hf n (LE f c R hf n (n + 1))
 132  exact CE_strictMono f c R hf n
 133    (lt_of_lt_of_le (Nat.lt_succ_of_le le_rfl)
 134      (strictMono_id_le (LE_strictMono f c R hf n) (n + 1)))
 135
 136private theorem D_strictMono : StrictMono (D f c R hf) :=
 137  strictMono_nat_of_lt_succ (fun n => D_succ_gt f c R hf n)
 138
 139private theorem D_converges (m : ℕ) :
 140    Tendsto (fun n => f (D f c R hf n) m) atTop (𝓝 (CL f c R hf m)) := by
 141  rw [Metric.tendsto_atTop]
 142  intro ε hε
 143  have h_base := CE_conv_at f c R hf m
 144  rw [Metric.tendsto_atTop] at h_base
 145  obtain ⟨K, hK⟩ := h_base ε hε
 146  refine ⟨max m K, fun n hn => ?_⟩
 147  have hm : m ≤ n := le_of_max_le_left hn
 148  have hK_le : K ≤ n := le_of_max_le_right hn
 149  obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hm
 150  obtain ⟨ρ, _hρ_mono, hρ_ge, hρ_eq⟩ := CE_factor f c R hf m p
 151  show dist (f (CE f c R hf (m + p) (m + p)) m) (CL f c R hf m) < ε
 152  rw [hρ_eq (m + p)]
 153  exact hK (ρ (m + p)) (le_trans hK_le (hρ_ge (m + p)))
 154
 155end Diagonal
 156