English
For all x ∈ ℂ and n ∈ ℕ, the difference between exp(x) and the nth partial sum ∑_{m=0}^{n-1} x^m/m! is bounded by exp(‖x‖) − ∑_{m=0}^{n-1} ‖x‖^m/m!.
Русский
Для всех x ∈ ℂ и n ∈ ℕ разность между exp(x) и первым частичным суммированием ∑_{m=0}^{n-1} x^m/m! ограничена: ∥e^x − ∑_{m=0}^{n-1} x^m/m!∥ ≤ exp(∥x∥) − ∑_{m=0}^{n-1} ∥x∥^m/m!.
LaTeX
$$$\\|e^{x} - \\sum_{m=0}^{n-1} \\frac{x^{m}}{m!}\\| \\\\leq e^{\\|x\\|} - \\sum_{m=0}^{n-1} \\frac{\\|x\\|^{m}}{m!}.$$$
Lean4
theorem norm_exp_sub_sum_le_exp_norm_sub_sum (x : ℂ) (n : ℕ) :
‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial :=
by
rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg, ← CauSeq.lim_neg,
CauSeq.lim_add, ← lim_norm]
refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
simp_rw [← sub_eq_add_neg]
calc
‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
_ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial :=
by
rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
congr with i
simp [Complex.norm_pow, Complex.norm_natCast]
_ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial :=
by
gcongr
exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _
