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