CE_zero

formal source

  62  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  63    (fun n => hf (CE f c R hf m n) (m + 1))).choose
  64
  65private theorem CE_zero : CE f c R hf 0 =
  66    (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose := rfl
  67
  68private theorem CE_succ (m : ℕ) : CE f c R hf (m + 1) = CE f c R hf m ∘ LE f c R hf m := rfl
  69
  70private theorem LE_strictMono (m : ℕ) : StrictMono (LE f c R hf m) :=
  71  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  72    (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.1
  73
  74private theorem CE_strictMono : ∀ m, StrictMono (CE f c R hf m) := by
  75  intro m; induction m with
  76  | zero =>
  77    exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.1
  78  | succ k ih =>
  79    rw [CE_succ]; exact ih.comp (LE_strictMono f c R hf k)
  80
  81private theorem LE_conv (m : ℕ) :
  82    Tendsto (fun n => f (CE f c R hf m (LE f c R hf m n)) (m + 1)) atTop
  83      (𝓝 (CL f c R hf (m + 1))) :=
  84  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  85    (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.2
  86
  87private theorem CE_conv_at : ∀ m, Tendsto (fun n => f (CE f c R hf m n) m)
  88    atTop (𝓝 (CL f c R hf m)) := by
  89  intro m; cases m with
  90  | zero =>
  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