norm_exp_le_exp_norm

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Complex.norm_exp_le_exp_norm

English

For all x ∈ ℂ, the modulus of exp(x) does not exceed exp(||x||).

Русский

Для любого x ∈ ℂ модуль exp(x) не превосходит exp(||x||).

LaTeX

$$$\\|e^{x}\\| \\leq e^{\\|x\\|}.$$$

Lean4

theorem norm_exp_le_exp_norm (x : ℂ) : ‖exp x‖ ≤ Real.exp ‖x‖ := by
  convert norm_exp_sub_sum_le_exp_norm_sub_sum x 0 using 1 <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru