norm_exp_sub_one_le — Mathlib

English

If |x| ≤ 1, then the norm of exp(x) − 1 is bounded by 2|x|.

Русский

Если |x| ≤ 1, то нормa экспоненты минус единица удовлетворяет неравенству ≤ 2|x|.

LaTeX

$$$\|e^x - 1\| \le 2 \cdot \|x\|$$$

Lean4

theorem norm_exp_sub_one_le {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖exp x - 1‖ ≤ 2 * ‖x‖ :=
  calc
    ‖exp x - 1‖ = ‖exp x - ∑ m ∈ range 1, x ^ m / m.factorial‖ := by simp
    _ ≤ ‖x‖ ^ 1 * ((Nat.succ 1 : ℝ) * ((Nat.factorial 1) * (1 : ℕ) : ℝ)⁻¹) := (exp_bound hx (by decide))
    _ = 2 * ‖x‖ := by simp [mul_two, mul_add, mul_comm, Nat.factorial]

Похожие утверждения