norm_jacobiTheta₂_term — Mathlib

English

The norm of jacobiTheta₂_term is given by exp( -π n^2 Im τ - 2π n Im z ).

Русский

Норма jacobiTheta₂_term равна exp(-π n^2 Im τ - 2π n Im z).

LaTeX

$$$\|\jacobiTheta_2\_term(n,z,\tau)\| = e^{ -\pi \; n^{2} \Im(\tau) - 2\pi n \Im(z) }$$$

Lean4

theorem norm_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) :
    ‖jacobiTheta₂_term n z τ‖ = rexp (-π * n ^ 2 * τ.im - 2 * π * n * z.im) :=
  by
  rw [jacobiTheta₂_term, Complex.norm_exp,
    (by push_cast; ring :
      (2 * π : ℂ) * I * n * z + π * I * n ^ 2 * τ = (π * (2 * n) :) * z * I + (π * n ^ 2 :) * τ * I),
    add_re, mul_I_re, im_ofReal_mul, mul_I_re, im_ofReal_mul]
  ring_nf

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