Cusps #
Auxiliary lemmas about cusps used in the modular forms development.
theorem
zero_at_cusps_of_zero_at_infty
{f : UpperHalfPlane → ℂ}
{c : OnePoint ℝ}
{k : ℤ}
{𝒢 : Subgroup (GL (Fin 2) ℝ)}
[𝒢.IsArithmetic]
(hc : IsCusp c 𝒢)
(hb : ∀ A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k A f))
:
c.IsZeroAt f k
theorem
bounded_at_cusps_of_bounded_at_infty
{f : UpperHalfPlane → ℂ}
{c : OnePoint ℝ}
{k : ℤ}
{𝒢 : Subgroup (GL (Fin 2) ℝ)}
[𝒢.IsArithmetic]
(hc : IsCusp c 𝒢)
(hb : ∀ A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A f))
:
c.IsBoundedAt f k