English
Let x be a complex number with |x| ≤ 1. Then the remainder of the exponential series after the first two terms satisfies ||e^x − 1 − x|| ≤ ||x||^2.
Русский
Пусть x — комплексное число с |x| ≤ 1. Тогда остаток ряда экспоненты после первых двух слагаемых удовлетворяет неравенству ||e^x − 1 − x|| ≤ |x|^2.
LaTeX
$$$\\|e^x - 1 - x\\| \\leq \\|x\\|^2 \\quad$ для $x \\in \\mathbb{C}$ с $\\|x\\| \\le 1$.$$
Lean4
theorem norm_exp_sub_one_sub_id_le {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖exp x - 1 - x‖ ≤ ‖x‖ ^ 2 :=
calc
‖exp x - 1 - x‖ = ‖exp x - ∑ m ∈ range 2, x ^ m / m.factorial‖ := by
simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc, Nat.factorial]
_ ≤ ‖x‖ ^ 2 * ((Nat.succ 2 : ℝ) * (Nat.factorial 2 * (2 : ℕ) : ℝ)⁻¹) := (exp_bound hx (by decide))
_ ≤ ‖x‖ ^ 2 * 1 := by gcongr; norm_num [Nat.factorial]
_ = ‖x‖ ^ 2 := by rw [mul_one]
