norm_cexp_neg_mul_sq — Mathlib

English

For any complex b and real x, the magnitude of e^{-b x^2} equals e^{-Re(b) x^2}.

Русский

Для комплексного b и действительного x модуль e^{-b x^2} равен e^{-Re(b) x^2}.

LaTeX

$$$$\\|e^{-b x^2}\\| = e^{-\\Re(b)\\, x^2}.$$$

Lean4

theorem norm_cexp_neg_mul_sq (b : ℂ) (x : ℝ) : ‖Complex.exp (-b * (x : ℂ) ^ 2)‖ = exp (-b.re * x ^ 2) := by
  rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]

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