Uniform convergence of Eisenstein series

We show that the sum of eisSummand converges locally uniformly on ℍ to the Eisenstein series of weight k and level Γ(N) with congruence condition a : Fin 2 → ZMod N.

Outline of argument

The key lemma r_mul_max_le shows that, for z ∈ ℍ and c, d ∈ ℤ (not both zero), |c z + d| is bounded below by r z * max (|c|, |d|), where r z is an explicit function of z (independent of c, d) satisfying 0 < r z < 1 for all z.

We then show in summable_one_div_rpow_max that the sum of max (|c|, |d|) ^ (-k) over (c, d) ∈ ℤ × ℤ is convergent for 2 < k. This is proved by decomposing ℤ × ℤ using the Finset.box lemmas.

theorem EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : ℕ} (a : Fin 2 → ZMod N) : TendstoLocallyUniformly (fun (s : Finset ↑(gammaSet N a)) (x : UpperHalfPlane) => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun (x : UpperHalfPlane) => eisensteinSeries a k x) Filter.atTop

The sum defining the Eisenstein series (of weight k and level Γ(N) with congruence condition a : Fin 2 → ZMod N) converges locally uniformly on ℍ.

theorem EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset ↑(gammaSet N a)) => (fun (z : UpperHalfPlane) => ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑UpperHalfPlane.ofComplex) ((eisensteinSeries_SIF a k).toFun ∘ ↑UpperHalfPlane.ofComplex) Filter.atTop {z : ℂ | 0 < z.im}

Variant of eisensteinSeries_tendstoLocallyUniformly formulated with maps ℂ → ℂ, which is nice to have for holomorphicity later.