Exponential Lemmas

Auxiliary lemmas about the complex exponential.

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

theorem exp_upperHalfPlane_lt_one_nat (z : UpperHalfPlane) (n : ℕ) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)‖ < 1