norm_cexp_neg_mul_sq_add_mul_I' — Mathlib

English

The norm of the complex exponential e^{−b (T+c i)^2} is given by a closed form in terms of b and c.

Русский

Норма экспоненты e^{−b (T+ci)^2} задаётся явной формулой через b и c.

LaTeX

$$$$ \| \mathrm{cexp}(-b (T + c i)^2) \| = \exp\big(-\Re(b) T^2 + 2 \Im(b) c T - \Re(b) c^2\big). $$$$

Lean4

theorem norm_cexp_neg_mul_sq_add_mul_I' (hb : b.re ≠ 0) (c T : ℝ) :
    ‖cexp (-b * (T + c * I) ^ 2)‖ = exp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re))) :=
  by
  have :
    b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 =
      b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re) :=
    by field_simp; ring
  rw [norm_cexp_neg_mul_sq_add_mul_I, this]

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