Finite sums of rational slashes at the cusps

A slash is zero at c exactly when the original function is zero at g • c (OnePoint.IsZeroAt.smul_iff), and for a rational g the point g • c is again a cusp of an arithmetic subgroup (IsCusp.smul_map_ratCast). So a function vanishing, or bounded, at every cusp keeps that property after any finite sum of rational slashes.

Nothing here is specific to Hecke operators: the index type is arbitrary and the matrices are unconstrained apart from rationality. The Hecke sums are corollaries, obtained by supplying their own index and representatives.

Main results

• OnePoint.isZeroAt_rat_slash, OnePoint.isBoundedAt_rat_slash: a single rational slash inherits vanishing, resp. boundedness, at the cusps.
• OnePoint.isZeroAt_sum_rat_slash, OnePoint.isBoundedAt_sum_rat_slash: the same for a finite sum, obtained by closing the summand-wise statements under OnePoint.IsZeroAt.sum and OnePoint.IsBoundedAt.sum respectively.

Provenance

No code is transcribed. The argument is the one the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0) uses for its specific representative sum in LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08 (heckeT_p_ut_zero_at_cusps, lines 62-70), where it is open-coded per call site. Here it is stated once, for an arbitrary finite family of rational matrices, so that each Hecke sum specialises it instead of repeating it.

theorem OnePoint.isZeroAt_rat_slash (k : ℤ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {f : UpperHalfPlane → ℂ} {c : OnePoint ℝ} (g : GL (Fin 2) ℚ) (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsZeroAt f k) (hc : IsCusp c Γ) : c.IsZeroAt (SlashAction.map k g f) k

A rational slash vanishes at every cusp when the function does. The matrix is unconstrained: only its rationality is used, via IsCusp.smul_map_ratCast.

theorem OnePoint.isZeroAt_sum_rat_slash (k : ℤ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {ι : Type u_1} {f : UpperHalfPlane → ℂ} {c : OnePoint ℝ} (s : Finset ι) (g : ι → GL (Fin 2) ℚ) (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsZeroAt f k) (hc : IsCusp c Γ) : c.IsZeroAt (∑ i ∈ s, SlashAction.map k (g i) f) k

A finite sum of rational slashes vanishes at every cusp — the summand-wise statement isZeroAt_rat_slash closed under OnePoint.IsZeroAt.sum.

theorem OnePoint.isBoundedAt_rat_slash (k : ℤ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {f : UpperHalfPlane → ℂ} {c : OnePoint ℝ} (g : GL (Fin 2) ℚ) (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsBoundedAt f k) (hc : IsCusp c Γ) : c.IsBoundedAt (SlashAction.map k g f) k

A rational slash is bounded at every cusp when the function is.

theorem OnePoint.isBoundedAt_sum_rat_slash (k : ℤ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {ι : Type u_1} {f : UpperHalfPlane → ℂ} {c : OnePoint ℝ} (s : Finset ι) (g : ι → GL (Fin 2) ℚ) (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsBoundedAt f k) (hc : IsCusp c Γ) : c.IsBoundedAt (∑ i ∈ s, SlashAction.map k (g i) f) k

A finite sum of rational slashes is bounded at every cusp — the summand-wise statement isBoundedAt_rat_slash closed under OnePoint.IsBoundedAt.sum.