norm_qParam — Mathlib

English

The norm of qParam is exp(-2π im(z)/h).

Русский

Норма qParam равна exp(-2π im(z)/h).

LaTeX

$$$\|\mathrm{qParam}(h,z)\| = \exp\left(-\frac{2\pi\, \mathrm{im}(z)}{h}\right)$$$

Lean4

theorem norm_qParam (z : ℂ) : ‖𝕢 h z‖ = Real.exp (-2 * π * im z / h) := by
  simp only [qParam, norm_exp, div_ofReal_re, mul_re, re_ofNat, ofReal_re, im_ofNat, ofReal_im, mul_zero, sub_zero,
    I_re, mul_im, zero_mul, add_zero, I_im, mul_one, sub_self, zero_sub, neg_mul]

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