The twisted slash sum of a holomorphic function is holomorphic

HeckeSlash/Holomorphic.lean proves mdifferentiable_heckeSlashSum for the unweighted sum. This file is the nebentypus-twisted counterpart.

The twisted sum runs over the same slashes as the unweighted one, each scaled by the constant nebentypusWeight χ D v. Holomorphy is closed under scaling by a constant, so no property of the character is used here — only that its value is a scalar — and the proof is the untwisted one with MDifferentiable.const_smul inserted at the summand.

Main results

• HeckeRing.GL2.mdifferentiable_twistedHeckeSlashSum: the twisted slash sum of a holomorphic function is holomorphic.

theorem HeckeRing.GL2.mdifferentiable_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] {f : UpperHalfPlane → ℂ} (hf : MDiff f) : MDiff (twistedHeckeSlashSum k χ D f)

The twisted slash sum of a holomorphic function is holomorphic. Together with the twisted invariance of HeckeSlash/Nebentypus/Invariance.lean this supplies one of the two extra conditions a ModularForm carries over a SlashInvariantForm; boundedness at the cusps is isBoundedAt_twistedHeckeSlashSum.