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)

theorem EisensteinSeries.norm_symm (x y : ℤ) : ‖![x, y]‖ = ‖![y, x]‖

theorem EisensteinSeries.abs_le_left_of_norm (m n : ℤ) : ↑|n| ≤ ‖![n, m]‖

theorem EisensteinSeries.abs_le_right_of_norm (m n : ℤ) : ↑|m| ≤ ‖![n, m]‖

theorem EisensteinSeries.abs_norm_eq_max_natAbs (n : ℕ) : ‖![1, ↑n + 1]‖ = ↑n + 1

theorem EisensteinSeries.abs_norm_eq_max_natAbs_neg (n : ℕ) : ‖![1, -(↑n + 1)]‖ = ↑n + 1

noncomputable def EisensteinSeries.r1 (z : UpperHalfPlane) : ℝ

Auxiliary function used for bounding Eisenstein series, defined as 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.

noncomputable 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)).

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 { coe := { re := A, im := B }, coe_im_pos := 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 { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-k) * ‖x‖ ^ (-k)

theorem EisensteinSeries.linear_isTheta_right_add (c e : ℤ) (z : ℂ) : (fun (d : ℤ) => ↑c * z + ↑d + ↑e) =Θ[Filter.cofinite] fun (n : ℤ) => ↑n

@[deprecated EisensteinSeries.linear_isTheta_right_add (since := "2025-12-27")]

theorem EisensteinSeries.linear_isTheta_right (c : ℤ) (z : ℂ) : (fun (d : ℤ) => ↑c * z + ↑d) =Θ[Filter.cofinite] fun (n : ℤ) => ↑n

theorem EisensteinSeries.linear_isTheta_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) : (fun (c : ℤ) => ↑c * z + ↑d) =Θ[Filter.cofinite] fun (n : ℤ) => ↑n

theorem EisensteinSeries.linear_inv_isBigO_right_add (c e : ℤ) (z : ℂ) : (fun (d : ℤ) => (↑c * z + ↑d + ↑e)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (↑n)⁻¹

theorem EisensteinSeries.linear_inv_isBigO_right (c : ℤ) (z : ℂ) : (fun (d : ℤ) => (↑c * z + ↑d)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (↑n)⁻¹

theorem EisensteinSeries.linear_inv_isBigO_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) : (fun (c : ℤ) => (↑c * z + ↑d)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (↑n)⁻¹

theorem EisensteinSeries.tendsto_zero_inv_linear (z : ℂ) (b : ℤ) : Filter.Tendsto (fun (d : ℕ) => 1 / (↑b * z + ↑d)) Filter.atTop (nhds 0)

theorem EisensteinSeries.tendsto_zero_inv_linear_sub (z : ℂ) (b : ℤ) : Filter.Tendsto (fun (d : ℕ) => 1 / (↑b * z - ↑d)) Filter.atTop (nhds 0)

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.summable_inv_of_isBigO_rpow_inv {α : Type u_1} [NormedField α] [CompleteSpace α] {f : ℤ → α} {a : ℝ} (hab : 1 < a) (hf : (fun (n : ℤ) => (f n)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (|↑n| ^ a)⁻¹) : Summable fun (n : ℤ) => (f n)⁻¹

If the inverse of a function isBigO to (|(n : ℝ)| ^ a)⁻¹ for 1 < a, then the function is Summable.

theorem EisensteinSeries.linear_right_summable (z : ℂ) (c : ℤ) {k : ℤ} (hk : 2 ≤ k) : Summable fun (d : ℤ) => ((↑c * z + ↑d) ^ k)⁻¹

For z : ℂ the function d : ℤ ↦ ((c z + d) ^ k)⁻¹ is Summable for 2 ≤ k.

theorem EisensteinSeries.linear_left_summable {z : ℂ} (hz : z ≠ 0) (d : ℤ) {k : ℤ} (hk : 2 ≤ k) : Summable fun (c : ℤ) => ((↑c * z + ↑d) ^ k)⁻¹

For z : ℂ the function c : ℤ ↦ ((c z + d) ^ k)⁻¹ is Summable for 2 ≤ k.

theorem EisensteinSeries.summable_linear_sub_mul_linear_add (z : ℂ) (c₁ c₂ : ℤ) : Summable fun (n : ℤ) => ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹

theorem EisensteinSeries.summable_linear_right_add_one_mul_linear_right (z : ℂ) (c₁ c₂ : ℤ) : Summable fun (n : ℤ) => ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹

theorem EisensteinSeries.summable_linear_left_mul_linear_left {z : ℂ} (hz : z ≠ 0) (c₁ c₂ : ℤ) : Summable fun (n : ℤ) => ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹

theorem EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology {α : Type u_1} (a : α) [NormedAddCommGroup α] [DiscreteTopology α] [ProperSpace α] : (fun (x : α) => a) =o[Filter.cofinite] fun (x : α) => ‖x‖

theorem EisensteinSeries.vec_add_const_isTheta (a b : ℤ) : (fun (m : Fin 2 → ℤ) => ‖![m 0 + a, m 1 + b]‖⁻¹) =Θ[Filter.cofinite] fun (m : Fin 2 → ℤ) => ‖m‖⁻¹

theorem EisensteinSeries.isBigO_linear_add_const_vec (z : UpperHalfPlane) (a b : ℤ) : (fun (m : Fin 2 → ℤ) => ((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹) =O[Filter.cofinite] fun (m : Fin 2 → ℤ) => ‖m‖⁻¹

theorem EisensteinSeries.summable_of_isBigO_rpow_norm {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] {f : (Fin 2 → ℤ) → E} {a : ℝ} (hab : 2 < a) (hf : f =O[Filter.cofinite] fun (n : Fin 2 → ℤ) => (‖n‖ ^ a)⁻¹) : Summable f

If a function ℤ² → ℂ is O (‖n‖ ^ a)⁻¹ for 2 < a, then the function is summable.