CE_conv_le

formal source

  91    exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.2
  92  | succ k => exact LE_conv f c R hf k
  93
  94private theorem CE_conv_le : ∀ m j, j ≤ m →
  95    Tendsto (fun n => f (CE f c R hf m n) j) atTop (𝓝 (CL f c R hf j)) := by
  96  intro m j hj
  97  induction m with
  98  | zero =>
  99    have hj0 : j = 0 := Nat.le_zero.mp hj
 100    subst hj0; exact CE_conv_at f c R hf 0
 101  | succ k ih =>
 102    rcases eq_or_lt_of_le hj with hjk | hjk
 103    · subst hjk; exact CE_conv_at f c R hf (k + 1)
 104    · rw [CE_succ]
 105      exact tendsto_comp_strictMono (ih (Nat.lt_succ_iff.mp hjk)) (LE_strictMono f c R hf k)
 106
 107/-- Factoring: CE(m+p) = CE(m) ∘ ρ with ρ strictly increasing and ρ(k) ≥ k. -/
 108private theorem CE_factor (m p : ℕ) :
 109    ∃ ρ : ℕ → ℕ, StrictMono ρ ∧ (∀ k, k ≤ ρ k) ∧
 110      ∀ k, CE f c R hf (m + p) k = CE f c R hf m (ρ k) := by
 111  induction p with
 112  | zero => exact ⟨id, strictMono_id, fun k => le_refl k, fun _ => rfl⟩
 113  | succ q ih =>
 114    obtain ⟨ρ, hρ_mono, hρ_ge, hρ_eq⟩ := ih
 115    refine ⟨ρ ∘ LE f c R hf (m + q),
 116      hρ_mono.comp (LE_strictMono f c R hf (m + q)),
 117      fun k => le_trans (strictMono_id_le (LE_strictMono f c R hf (m + q)) k)
 118        (hρ_ge (LE f c R hf (m + q) k)),
 119      fun k => ?_⟩
 120    show CE f c R hf (m + (q + 1)) k = CE f c R hf m ((ρ ∘ LE f c R hf (m + q)) k)
 121    have h1 : m + (q + 1) = (m + q) + 1 := by omega
 122    rw [h1, CE_succ]
 123    simp only [Function.comp_apply]
 124    exact hρ_eq _