English
Let x ∈ C with |x| ≤ 1 and n > 0. The remainder of truncating exp at n terms is bounded by |x|^n / n! times 2.
Русский
Пусть x ∈ C и |x| ≤ 1, n > 0. Остаток после аппроксимации экспоненты суммой до n−го слагаемого удовлетворяет неравенству ≤ 2·|x|^n / n!.
LaTeX
$$$\|\exp x - \sum_{m=0}^{n-1} \frac{x^m}{m!}\| \le \|x\|^n / n! \cdot 2$$$
Lean4
theorem exp_bound {x : ℂ} (hx : ‖x‖ ≤ 1) {n : ℕ} (hn : 0 < n) :
‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ ‖x‖ ^ n * ((n.succ : ℝ) * (n.factorial * n : ℝ)⁻¹) :=
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.succ : ℝ) * (n.factorial * n : ℝ)⁻¹)
rw [sum_range_sub_sum_range hj]
calc
‖∑ m ∈ range j with n ≤ m, (x ^ m / m.factorial : ℂ)‖ =
‖∑ m ∈ range j with n ≤ m, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ :=
by
refine congr_arg norm (sum_congr rfl fun m hm => ?_)
rw [mem_filter, mem_range] at hm
rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
_ ≤ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ := IsAbsoluteValue.abv_sum norm ..
_ ≤ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / m.factorial) :=
by
simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
gcongr
rw [Complex.norm_pow]
exact pow_le_one₀ (norm_nonneg _) hx
_ = ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, (1 / m.factorial : ℝ) := by simp [← mul_sum]
_ ≤ ‖x‖ ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by
gcongr
exact sum_div_factorial_le _ _ hn
