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.norm_eq_max_natAbs (x : Fin 2 → ℤ) : ‖x‖ = ↑((x 0).natAbs ⊔ (x 1).natAbs)

def EisensteinSeries.r1 (z : UpperHalfPlane) : ℝ

Auxiliary function used for bounding Eisenstein series, defined as z.im ^ 2 / (z.re ^ 2 + z.im ^ 2).

Equations

• EisensteinSeries.r1 z = z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)

theorem EisensteinSeries.r1_eq (z : UpperHalfPlane) : EisensteinSeries.r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

theorem EisensteinSeries.r1_pos (z : UpperHalfPlane) : 0 < EisensteinSeries.r1 z

theorem EisensteinSeries.r1_aux_bound (z : UpperHalfPlane) (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : EisensteinSeries.r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

For c, d ∈ ℝ with 1 ≤ d ^ 2, we have r1 z ≤ |c * z + d| ^ 2.

def EisensteinSeries.r (z : UpperHalfPlane) : ℝ

This function is used to give an upper bound on the summands in Eisenstein series; it is defined by z ↦ min z.im √(z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)).

Equations

• EisensteinSeries.r z = z.im ⊓ √(EisensteinSeries.r1 z)

theorem EisensteinSeries.r_pos (z : UpperHalfPlane) : 0 < EisensteinSeries.r z

theorem EisensteinSeries.r_lower_bound_on_verticalStrip (z : UpperHalfPlane) {A B : ℝ} (h : 0 < B) (hz : z ∈ UpperHalfPlane.verticalStrip A B) : EisensteinSeries.r ⟨{ re := A, im := B }, h⟩ ≤ EisensteinSeries.r z

theorem EisensteinSeries.auxbound1 (z : UpperHalfPlane) {c : ℝ} (d : ℝ) (hc : 1 ≤ c ^ 2) : EisensteinSeries.r z ≤ Complex.abs (↑c * ↑z + ↑d)

theorem EisensteinSeries.auxbound2 (z : UpperHalfPlane) (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : EisensteinSeries.r z ≤ Complex.abs (↑c * ↑z + ↑d)

theorem EisensteinSeries.div_max_sq_ge_one (x : Fin 2 → ℤ) (hx : x ≠ 0) : 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

theorem EisensteinSeries.r_mul_max_le (z : UpperHalfPlane) {x : Fin 2 → ℤ} (hx : x ≠ 0) : EisensteinSeries.r z * ‖x‖ ≤ Complex.abs (↑(x 0) * ↑z + ↑(x 1))

theorem EisensteinSeries.summand_bound (z : UpperHalfPlane) {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) : Complex.abs (↑(x 0) * ↑z + ↑(x 1)) ^ (-k) ≤ EisensteinSeries.r z ^ (-k) * ‖x‖ ^ (-k)

Upper bound for the summand |c * z + d| ^ (-k), as a product of a function of z and a function of c, d.

theorem EisensteinSeries.summand_bound_of_mem_verticalStrip {z : UpperHalfPlane} {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) {A B : ℝ} (hB : 0 < B) (hz : z ∈ UpperHalfPlane.verticalStrip A B) : Complex.abs (↑(x 0) * ↑z + ↑(x 1)) ^ (-k) ≤ EisensteinSeries.r ⟨{ re := A, im := B }, hB⟩ ^ (-k) * ‖x‖ ^ (-k)

theorem EisensteinSeries.summable_one_div_norm_rpow {k : ℝ} (hk : 2 < k) : Summable fun (x : Fin 2 → ℤ) => ‖x‖ ^ (-k)

The function ℤ ^ 2 → ℝ given by x ↦ ‖x‖ ^ (-k) is summable if 2 < k. We prove this by splitting into boxes using Finset.box.

theorem EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : ℕ} (a : Fin 2 → ZMod N) : TendstoLocallyUniformly (fun (s : Finset ↑(EisensteinSeries.gammaSet N a)) (x : UpperHalfPlane) => ∑ x_1 ∈ s, EisensteinSeries.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 ↑(EisensteinSeries.gammaSet N a)) => (fun (z : UpperHalfPlane) => ∑ x ∈ s, EisensteinSeries.eisSummand k (↑x) z) ∘ ↑UpperHalfPlane.ofComplex) ((EisensteinSeries.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.