Level one modular forms

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

Finite-dimensionality of these spaces is proved in a later file (Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean).

theorem SlashInvariantForm.exists_one_half_le_im_and_norm_le {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range 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 (Matrix.SpecialLinearGroup.mapGL ℝ).range 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 SlashInvariantForm.slash_action_generators_SL2Z {f : UpperHalfPlane → ℂ} {k : ℤ} (hS : SlashAction.map k ModularGroup.S f = f) (hT : SlashAction.map k ModularGroup.T f = f) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map k γ f = f

theorem one_mem_strictPeriods_SL : 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

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

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

theorem ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) = 1

theorem ModularForm.levelOne_neg_weight_rank_zero {k : ℤ} (hk : k < 0) : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0