Boundedness of Eisenstein series

We show that Eisenstein series of weight k and level Γ(N) with congruence condition a : Fin 2 → ZMod N are bounded at infinity.

Outline of argument

We need to bound the value of the Eisenstein series (acted on by A : SL(2,ℤ)) at a given point z in the upper half plane. Since these are modular forms of level Γ(N), it suffices to prove this for z ∈ verticalStrip N z.im.

We can then, first observe that the slash action just changes our a to (a ᵥ* A) and we then use our bounds for Eisenstein series in these vertical strips to get the result.

theorem EisensteinSeries.summable_norm_eisSummand {k : ℤ} (hk : 3 ≤ k) (z : UpperHalfPlane) : Summable fun (x : Fin 2 → ℤ) => ‖EisensteinSeries.eisSummand k x z‖

theorem EisensteinSeries.abs_le_tsum_abs (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k) (z : UpperHalfPlane) : Complex.abs (eisensteinSeries a k z) ≤ ∑' (x : Fin 2 → ℤ), Complex.abs (EisensteinSeries.eisSummand k x z)

The absolute value of the restricted sum is less than the full sum of the absolute values.

theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ+} (a : Fin 2 → ZMod ↑N) {k : ℤ} (hk : 3 ≤ k) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A (EisensteinSeries.eisensteinSeries_SIF a k).toFun)

Eisenstein series are bounded at infinity.