CE_factor

formal source

 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 _
 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