norm_cexp_neg_mul_sq_add_mul_I — Mathlib

English

Reciprocal reflection: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.

Русский

Обратная отражательная формула: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.

LaTeX

$$$$ (\Gamma_{\mathbb{R}}(1 - s))^{-1} = \Gamma_{\mathbb{C}}(s) \cos\left(\frac{\pi s}{2}\right) \big( \Gamma_{\mathbb{R}}(s)\big)^{-1}. $$$$

Lean4

/-- Explicit formula for the norm of the Gaussian function along the vertical
edges. -/
theorem norm_cexp_neg_mul_sq_add_mul_I (b : ℂ) (c T : ℝ) :
    ‖cexp (-b * (T + c * I) ^ 2)‖ = exp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2)) :=
  by
  rw [Complex.norm_exp, neg_mul, neg_re, ← re_add_im b]
  simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]
  ring_nf

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