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 → ℤ) => ‖eisSummand k x z‖

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

The norm of the restricted sum is less than the full sum of the norms.

theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A ⇑(eisensteinSeriesSIF a k))

Eisenstein series are bounded at infinity.

@[deprecated EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF (since := "2026-02-10")]

theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k A ⇑(eisensteinSeriesSIF a k))

Alias of EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF.

---

Eisenstein series are bounded at infinity.