English
For every z ∈ ℂ, the sequence a_n = ∑_{m=0}^{n-1} | z^m / m! | is a Cauchy sequence (with respect to the real absolute value norm).
Русский
Для каждого z ∈ ℂ последовательность a_n = ∑_{m=0}^{n-1} | z^m / m! | является последовательностью Коши (по норме абсолютного значения).
LaTeX
$$$\\forall z\\in\\mathbb{C},\\; IsCauSeq\\; |\\cdot|\\ \\bigl(n \\mapsto \\sum_{m=0}^{n-1} \\frac{|z|^m}{m!}\\bigr)$$$
Lean4
theorem isCauSeq_norm_exp (z : ℂ) : IsCauSeq abs fun n => ∑ m ∈ range n, ‖z ^ m / m.factorial‖ :=
let ⟨n, hn⟩ := exists_nat_gt ‖z‖
have hn0 : (0 : ℝ) < n := lt_of_le_of_lt (norm_nonneg _) hn
IsCauSeq.series_ratio_test n (‖z‖ / n) (div_nonneg (norm_nonneg _) (le_of_lt hn0)) (by rwa [div_lt_iff₀ hn0, one_mul])
fun m hm =>
by
rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul, ← div_div, mul_div_assoc,
mul_div_right_comm, Complex.norm_mul, Complex.norm_div, norm_natCast]
gcongr
exact le_trans hm (Nat.le_succ _)
