im_invQParam — Mathlib

English

The imaginary part of invQParam is −h/(2π) · log ||q||.

Русский

m-часть invQParam равна −h/(2π) · log ||q||.

LaTeX

$$$\mathrm{Im}(\mathrm{invQParam}(h,q)) = -\dfrac{h}{2\pi}\,\log \|q\|$$$

Lean4

theorem im_invQParam (q : ℂ) : im (invQParam h q) = -h / (2 * π) * Real.log ‖q‖ := by
  simp only [invQParam, ← div_div, div_I, neg_mul, neg_im, mul_im, mul_re, div_ofReal_re, div_ofNat_re, ofReal_re, I_re,
    mul_zero, div_ofReal_im, div_ofNat_im, ofReal_im, zero_div, I_im, mul_one, sub_self, zero_mul, add_zero, log_re,
    zero_add, neg_div]

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