norm_qParam_lt_one — Mathlib

English

For every natural n with n ≠ 0 and every τ in the upper half-plane, the norm of qParam(n, τ) is strictly less than 1.

Русский

Для каждого натурального n ≠ 0 и каждого τ в верхней полуплоскости выполняется, что норма qParam(n, τ) строго меньше 1.

LaTeX

$$$\forall n \in \mathbb{N}, n \neq 0, \forall \tau \in \mathbb{H}, \; \|\mathsf{qParam}(n, \tau)\| < 1$$$

Lean4

theorem norm_qParam_lt_one (n : ℕ) [NeZero n] (τ : ℍ) : ‖𝕢 n τ‖ < 1 :=
  by
  rw [Periodic.norm_qParam, Real.exp_lt_one_iff, neg_mul, coe_im, neg_mul, neg_div, neg_lt_zero,
    div_pos_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero <| NeZero.ne _)]
  positivity

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