Identities of ModularForms and SlashInvariantForms

Collection of useful identities of modular forms.

theorem SlashInvariantForm.vAdd_apply_of_mem_strictPeriods {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (τ : UpperHalfPlane) {h : ℝ} (hH : h ∈ Γ.strictPeriods) : f (h +ᵥ τ) = f τ

theorem SlashInvariantForm.vAdd_width_periodic (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k) (z : UpperHalfPlane) : f (↑N * ↑n +ᵥ z) = f z

theorem SlashInvariantForm.T_zpow_width_invariant (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k) (z : UpperHalfPlane) : f (ModularGroup.T ^ (↑N * n) • z) = f z

theorem SlashInvariantForm.slash_S_apply (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane) : SlashAction.map k ModularGroup.S f z = f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

theorem SlashInvariantForm.slash_action_generators {f : UpperHalfPlane → ℂ} {Γ : Subgroup (GL (Fin 2) ℝ)} {s : Set (GL (Fin 2) ℝ)} (hΓ : Γ = Subgroup.closure s) {k : ℤ} : (∀ γ ∈ Γ, SlashAction.map k γ f = f) ↔ ∀ γ ∈ s, SlashAction.map k γ f = f