Summability of Eisenstein series

We gather results about the summability of Eisenstein series, particularly the summability of the Eisenstein series summands, which are used in the proof of the boundedness of Eisenstein series at infinity.

theorem EisensteinSeries.norm_eq_max_natAbs (x : Fin 2 → ℤ) : ‖x‖ = ↑(max (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) : r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

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

theorem EisensteinSeries.r1_aux_bound (z : UpperHalfPlane) (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : 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 = min z.im √(EisensteinSeries.r1 z)

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

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

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

theorem EisensteinSeries.auxbound2 (z : UpperHalfPlane) (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : r z ≤ ‖↑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) : r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

theorem EisensteinSeries.summand_bound (z : UpperHalfPlane) {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) : ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ 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) : ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ 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.