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_norm_lt_one {h : ℝ} (hh : 0 < h) {q : ℂ} (hq : ‖q‖ < 1) (hq_ne : q ≠ 0) : 0 < (invQParam h q).im

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

theorem UpperHalfPlane.norm_qParam_lt_one (n : ℕ) [NeZero n] (τ : UpperHalfPlane) : ‖Function.Periodic.qParam ↑n ↑τ‖ < 1

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

@[deprecated Function.Periodic.im_invQParam_pos_of_norm_lt_one (since := "2025-02-17")]

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

Alias of Function.Periodic.im_invQParam_pos_of_norm_lt_one.

@[deprecated Function.Periodic.norm_qParam_le_of_one_half_le_im (since := "2025-02-17")]

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

Alias of Function.Periodic.norm_qParam_le_of_one_half_le_im.

@[deprecated UpperHalfPlane.norm_qParam_lt_one (since := "2025-02-17")]

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

Alias of UpperHalfPlane.norm_qParam_lt_one.

@[deprecated UpperHalfPlane.norm_exp_two_pi_I_lt_one (since := "2025-02-17")]

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

Alias of UpperHalfPlane.norm_exp_two_pi_I_lt_one.