theorem
proved
term proof
CE_conv_le
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/