The slash sum preserves holomorphy

heckeSlashSum is a finite sum of slashes, so it is holomorphic whenever its argument is. This is one of the two conditions separating SlashInvariantForm from ModularForm; the other, boundedness at the cusps, is not addressed here.

Holomorphy is one of the two conditions a ModularForm carries over a SlashInvariantForm. A consumer building the descent needs this together with boundedness at the cusps; only the former is available here, and nothing in this file assumes f is slash-invariant, so it applies to any holomorphic f : ℍ → ℂ.

Main results

• HeckeRing.GL2.mdifferentiable_heckeSlashSum: heckeSlashSum k D f is holomorphic when f is.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4.

theorem HeckeRing.GL2.mdifferentiable_heckeSlashSum (k : ℤ) {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset Δ Γ₁ Γ₂) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] {f : UpperHalfPlane → ℂ} (hf : MDiff f) : MDiff (heckeSlashSum k D f)

The slash sum of a holomorphic function is holomorphic. Together with slash-invariance (heckeSlashSum_slash_invariant) this supplies one of the two extra conditions a ModularForm carries over a SlashInvariantForm; boundedness at the cusps is separate and is not proved here.