English
Let x ∈ C and n ∈ N with |x| ≤ 1. The bound on the remainder of the exponential series after n terms is of the form 2·|x|^n/n!.
Русский
Пусть x ∈ C и n ∈ N с условием |x| ≤ 1. Оценка остатка экспоненты после n членов имеет вид 2·|x|^n/n!.
LaTeX
$$$\|\exp x - \sum_{m=0}^{n-1} \frac{x^m}{m!}\| \le 2 \cdot \frac{|x|^n}{n!}$$$
Lean4
theorem exp_bound' {x : ℂ} {n : ℕ} (hx : ‖x‖ / n.succ ≤ 1 / 2) :
‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ ‖x‖ ^ n / n.factorial * 2 :=
by
rw [← lim_const (abv := norm) (∑ m ∈ range n, _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_norm]
refine lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
simp_rw [← sub_eq_add_neg]
change ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ ‖x‖ ^ n / n.factorial * 2
let k := j - n
have hj : j = n + k := (add_tsub_cancel_of_le hj).symm
rw [hj, sum_range_add_sub_sum_range]
calc
‖∑ i ∈ range k, x ^ (n + i) / ((n + i).factorial : ℂ)‖ ≤ ∑ i ∈ range k, ‖x ^ (n + i) / ((n + i).factorial : ℂ)‖ :=
IsAbsoluteValue.abv_sum _ _ _
_ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / (n + i).factorial := by simp [norm_natCast, Complex.norm_pow]
_ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ((n.factorial : ℝ) * (n.succ : ℝ) ^ i) := ?_
_ = ∑ i ∈ range k, ‖x‖ ^ n / n.factorial * (‖x‖ ^ i / (n.succ : ℝ) ^ i) := ?_
_ ≤ ‖x‖ ^ n / ↑n.factorial * 2 := ?_
· gcongr
exact mod_cast Nat.factorial_mul_pow_le_factorial
· simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]
· rw [← mul_sum]
gcongr
simp_rw [← div_pow]
rw [geom_sum_eq, div_le_iff_of_neg]
· trans (-1 : ℝ)
· linarith
· simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
positivity
· linarith
· linarith
