Level one modular forms

This file contains results specific to modular forms of level one, ie. modular forms for SL(2, ℤ).

TODO: Add finite-dimensionality of these spaces of modular forms.

theorem SlashInvariantForm.exists_one_half_le_im_and_norm_le {k : ℤ} (hk : k ≤ 0) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F ⊤ k] (f : F) (τ : UpperHalfPlane) : ∃ (ξ : UpperHalfPlane), 1 / 2 ≤ ξ.im ∧ ‖f τ‖ ≤ ‖f ξ‖

theorem SlashInvariantForm.wt_eq_zero_of_eq_const {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (k : ℤ) [SlashInvariantFormClass F ⊤ k] {f : F} {c : ℂ} (hf : ∀ (τ : UpperHalfPlane), f τ = c) : k = 0 ∨ c = 0

If a constant function is modular of weight k, then either k = 0, or the constant is 0.