Exp on the upper half plane

This file contains lemmas about the exponential function on the upper half plane. Useful for q-expansions of modular forms.

theorem Function.Periodic.im_invQParam_pos_of_abs_lt_one {h : ℝ} (hh : 0 < h) {q : ℂ} (hq : Complex.abs q < 1) (hq_ne : q ≠ 0) : 0 < (invQParam h q).im

theorem Function.Periodic.abs_qParam_le_of_one_half_le_im {ξ : ℂ} (hξ : 1 / 2 ≤ ξ.im) : ‖qParam 1 ξ‖ ≤ Real.exp (-Real.pi)

theorem UpperHalfPlane.abs_qParam_lt_one (n : ℕ) [NeZero n] (τ : UpperHalfPlane) : Complex.abs (Function.Periodic.qParam ↑n ↑τ) < 1

theorem UpperHalfPlane.abs_exp_two_pi_I_lt_one (τ : UpperHalfPlane) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑τ)‖ < 1