Level one modular forms

This file contains results specific to modular forms of level one, i.e. 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 {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k] (hk : k ≤ 0) (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 (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k] {f : F} {c : ℂ} (hf : ⇑f = Function.const UpperHalfPlane c) : k = 0 ∨ c = 0

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

theorem ModularFormClass.one_mem_strictPeriods_SL2Z : 1 ∈ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)).strictPeriods

theorem ModularFormClass.levelOne_neg_weight_eq_zero {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k] (hk : k < 0) (f : F) : ⇑f = 0

theorem ModularFormClass.levelOne_weight_zero_const {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 0] (f : F) : ∃ (c : ℂ), ⇑f = Function.const UpperHalfPlane c

theorem ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 0) = 1

theorem ModularForm.levelOne_neg_weight_rank_zero {k : ℤ} (hk : k < 0) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 0