exp_bound_sq — Mathlib

English

For complex numbers x,z with |z| ≤ 1, the bound holds: ||exp(x+z) − exp(x) − z·exp(x)|| ≤ ||exp(x)|| · ||z||^2.

Русский

Для комплексных чисел x,z при |z| ≤ 1 выполняется неравенство: ||e^{x+z} − e^{x} − z e^{x}|| ≤ ||e^{x}|| · ||z||^2.

LaTeX

$$$\\|e^{x+z}-e^{x}-z\\,e^{x}\\| \\leq \\|e^{x}\\| \\cdot \\|z\\|^{2}$$$

Lean4

theorem exp_bound_sq (x z : ℂ) (hz : ‖z‖ ≤ 1) : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 :=
  calc
    ‖exp (x + z) - exp x - z * exp x‖ = ‖exp x * (exp z - 1 - z)‖ :=
      by
      congr
      rw [exp_add]
      ring
    _ = ‖exp x‖ * ‖exp z - 1 - z‖ := (norm_mul _ _)
    _ ≤ ‖exp x‖ * ‖z‖ ^ 2 := mul_le_mul_of_nonneg_left (norm_exp_sub_one_sub_id_le hz) (norm_nonneg _)

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