E₂ is Bounded At Im Infty

lemma E₂_isBoundedAtImInfty : IsBoundedAtImInfty E₂ := by  rw [UpperHalfPlane.isBoundedAtImInfty_iff]  set r₀ : ℝ := Real.exp (-2 * π)  have hr₀_lt_one : r₀ < 1 := Real.exp_lt_one_iff.mpr (by linarith [Real.pi_pos])  refine ⟨1 + 24 * (r₀ / (1 - r₀) ^ 3), 1, fun z hz => ?_⟩  rw [E₂_eq]  set q : ℂ := cexp (2 * π * Complex.I * z)  have hq_bound : ‖q‖ ≤ r₀ := norm_exp_two_pi_I_le_exp_neg_two_pi z hz  -- Rewrite sum in terms of q^n  set S := ∑' n : ℕ+, (n : ℂ) * q ^ (n : ℕ) / (1 - q ^ (n : ℕ))  have hS_eq : ∑' n : ℕ+, ↑n * cexp (2 * π * Complex.I * ↑n * ↑z) /      (1 - cexp (2 * π * Complex.I * ↑n * ↑z)) = S := by    congr 1; ext n    have : cexp (2 * π * Complex.I * n * z) = q ^ (n : ℕ) := by      change _ = (cexp (2 * π * Complex.I * z)) ^ (n : ℕ)      rw [← Complex.exp_nat_mul]; ring_nf    simp [this]  calc ‖1 - 24 * ∑' n : ℕ+, ↑n * cexp (2 * π * Complex.I * ↑n * ↑z) /          (1 - cexp (2 * π * Complex.I * ↑n * ↑z))‖      = ‖1 - 24 * S‖ := by rw [hS_eq]    _ ≤ 1 + 24 * ‖S‖ := by        calc _ ≤ ‖(1 : ℂ)‖ + ‖24 * S‖ := norm_sub_le _ _          _ = _ := by simp    _ ≤ 1 + 24 * (r₀ / (1 - r₀) ^ 3) := by        gcongr; exact norm_tsum_logDeriv_expo_le_of_norm_le hq_bound hr₀_lt_one