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 → Int) : Eq (Norm.norm x) (Max.max (x 0).natAbs (x 1).natAbs).cast

def EisensteinSeries.r1 (z : UpperHalfPlane) : Real

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

Equations

• Eq (EisensteinSeries.r1 z) (HDiv.hDiv (HPow.hPow z.im 2) (HAdd.hAdd (HPow.hPow z.re 2) (HPow.hPow z.im 2)))

theorem EisensteinSeries.r1_eq (z : UpperHalfPlane) : Eq (r1 z) (HDiv.hDiv 1 (HAdd.hAdd (HPow.hPow (HDiv.hDiv z.re z.im) 2) 1))

theorem EisensteinSeries.r1_pos (z : UpperHalfPlane) : LT.lt 0 (r1 z)

theorem EisensteinSeries.r1_aux_bound (z : UpperHalfPlane) (c : Real) {d : Real} (hd : LE.le 1 (HPow.hPow d 2)) : LE.le (r1 z) (HAdd.hAdd (HPow.hPow (HAdd.hAdd (HMul.hMul c z.re) d) 2) (HPow.hPow (HMul.hMul c z.im) 2))

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

def EisensteinSeries.r (z : UpperHalfPlane) : Real

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

• Eq (EisensteinSeries.r z) (Min.min z.im (EisensteinSeries.r1 z).sqrt)

theorem EisensteinSeries.r_pos (z : UpperHalfPlane) : LT.lt 0 (r z)

theorem EisensteinSeries.r_lower_bound_on_verticalStrip (z : UpperHalfPlane) {A B : Real} (h : LT.lt 0 B) (hz : Membership.mem (UpperHalfPlane.verticalStrip A B) z) : LE.le (r ⟨{ re := A, im := B }, h⟩) (r z)

theorem EisensteinSeries.auxbound1 (z : UpperHalfPlane) {c : Real} (d : Real) (hc : LE.le 1 (HPow.hPow c 2)) : LE.le (r z) (Norm.norm (HAdd.hAdd (HMul.hMul (Complex.ofReal c) z.coe) (Complex.ofReal d)))

theorem EisensteinSeries.auxbound2 (z : UpperHalfPlane) (c : Real) {d : Real} (hd : LE.le 1 (HPow.hPow d 2)) : LE.le (r z) (Norm.norm (HAdd.hAdd (HMul.hMul (Complex.ofReal c) z.coe) (Complex.ofReal d)))

theorem EisensteinSeries.div_max_sq_ge_one (x : Fin 2 → Int) (hx : Ne x 0) : Or (LE.le 1 (HPow.hPow (HDiv.hDiv (x 0).cast (Norm.norm x)) 2)) (LE.le 1 (HPow.hPow (HDiv.hDiv (x 1).cast (Norm.norm x)) 2))

theorem EisensteinSeries.r_mul_max_le (z : UpperHalfPlane) {x : Fin 2 → Int} (hx : Ne x 0) : LE.le (HMul.hMul (r z) (Norm.norm x)) (Norm.norm (HAdd.hAdd (HMul.hMul (x 0).cast z.coe) (x 1).cast))

theorem EisensteinSeries.summand_bound (z : UpperHalfPlane) {k : Real} (hk : LE.le 0 k) (x : Fin 2 → Int) : LE.le (HPow.hPow (Norm.norm (HAdd.hAdd (HMul.hMul (x 0).cast z.coe) (x 1).cast)) (Neg.neg k)) (HMul.hMul (HPow.hPow (r z) (Neg.neg k)) (HPow.hPow (Norm.norm x) (Neg.neg 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 : Real} (hk : LE.le 0 k) (x : Fin 2 → Int) {A B : Real} (hB : LT.lt 0 B) (hz : Membership.mem (UpperHalfPlane.verticalStrip A B) z) : LE.le (HPow.hPow (Norm.norm (HAdd.hAdd (HMul.hMul (x 0).cast z.coe) (x 1).cast)) (Neg.neg k)) (HMul.hMul (HPow.hPow (r ⟨{ re := A, im := B }, hB⟩) (Neg.neg k)) (HPow.hPow (Norm.norm x) (Neg.neg k)))

theorem EisensteinSeries.summable_one_div_norm_rpow {k : Real} (hk : LT.lt 2 k) : Summable fun (x : Fin 2 → Int) => HPow.hPow (Norm.norm x) (Neg.neg 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 : Int} (hk : LE.le 3 k) {N : Nat} (a : Fin 2 → ZMod N) : TendstoLocallyUniformly (fun (s : Finset (gammaSet N a).Elem) (x : UpperHalfPlane) => s.sum fun (x_1 : (gammaSet N a).Elem) => eisSummand k x_1.val 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 : Int} {N : Nat} (hk : LE.le 3 k) (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N a).Elem) => Function.comp (fun (z : UpperHalfPlane) => s.sum fun (x : (gammaSet N a).Elem) => eisSummand k x.val z) UpperHalfPlane.ofComplex.toFun') (Function.comp (eisensteinSeries_SIF a k).toFun UpperHalfPlane.ofComplex.toFun') Filter.atTop (setOf fun (z : Complex) => LT.lt 0 z.im)

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