Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

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 = (max (x 0).natAbs (x 1).natAbs)

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

Equations
Instances For
    theorem EisensteinSeries.r1_eq (z : UpperHalfPlane) :
    EisensteinSeries.r1 z = 1 / ((z.re / z.im) ^ 2 + 1)
    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.

    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
    Instances For
      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 2ZMod N) :
      TendstoLocallyUniformly (fun (s : Finset (EisensteinSeries.gammaSet N a)) (x : UpperHalfPlane) => x_1s, 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 .

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