im_invQParam_pos_of_norm_lt_one — Mathlib

English

Let h > 0 and q ∈ C with |q| < 1 and q ≠ 0. Then the imaginary part of invQParam(h, q) is strictly positive.

Русский

Пусть h > 0 и q ∈ ℂ так, что |q| < 1 и q ≠ 0. Тогда мнимая часть invQParam(h, q) положительна.

LaTeX

$$$\forall h \in \mathbb{R}, h > 0 \; \forall q \in \mathbb{C}, \|q\| < 1, q \neq 0 \; \Rightarrow \Im\big(\operatorname{Periodic.invQParam}(h,q)\big) > 0$$$

Lean4

theorem im_invQParam_pos_of_norm_lt_one {h : ℝ} (hh : 0 < h) {q : ℂ} (hq : ‖q‖ < 1) (hq_ne : q ≠ 0) :
    0 < im (Periodic.invQParam h q) :=
  im_invQParam .. ▸
    mul_pos_of_neg_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) Real.two_pi_pos)
      ((Real.log_neg_iff (norm_pos_iff.mpr hq_ne)).mpr hq)

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