The twisted slash sum at the cusps

HeckeSlash/Cusps.lean proves isZeroAt_heckeSlashSum and isBoundedAt_heckeSlashSum for the unweighted sum. This file is the nebentypus-twisted counterpart.

As in HeckeSlash/Nebentypus/Holomorphic.lean, the summands are the unweighted ones scaled by the constant nebentypusWeight χ D v, so nothing about the character is used — only that its value is a scalar. The summand-wise statements are the existing OnePoint.isZeroAt_rat_slash and OnePoint.isBoundedAt_rat_slash, closed under OnePoint.IsZeroAt.const_smul and OnePoint.IsBoundedAt.const_smul for the weight and then under OnePoint.IsZeroAt.sum and OnePoint.IsBoundedAt.sum for the sum.

Main results

• HeckeRing.GL2.isZeroAt_twistedHeckeSlashSum: the twisted slash sum vanishes at every cusp when the function does.
• HeckeRing.GL2.isBoundedAt_twistedHeckeSlashSum: the twisted slash sum is bounded at every cusp when the function is.

theorem HeckeRing.GL2.isZeroAt_twistedHeckeSlashSum {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) [NeZero N] {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {f : UpperHalfPlane → ℂ} (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsZeroAt f k) {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsZeroAt (twistedHeckeSlashSum k χ D f) k

The twisted slash sum vanishes at every cusp when the function does.

theorem HeckeRing.GL2.isBoundedAt_twistedHeckeSlashSum {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) [NeZero N] {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {f : UpperHalfPlane → ℂ} (hf : ∀ (c : OnePoint ℝ), IsCusp c Γ → c.IsBoundedAt f k) {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsBoundedAt (twistedHeckeSlashSum k χ D f) k

The twisted slash sum is bounded at every cusp when the function is.