English
The Eisenstein series converges locally uniformly on the upper half-plane for weights k ≥ 3 and level N with congruence data a.
Русский
Эйзенштейнов ряд сходится локально равномерно на верхней полуплоскости для веса k ≥ 3 и уровня N с данными сравнения a.
LaTeX
$$$\\forall k \\in \\mathbb{Z},\\; k \\ge 3,\\; \\forall N \\in \\mathbb{N},\\; \\forall a: \\text{Fin } 2 \\to \\mathbb{Z}/N\\mathbb{Z},\\; \\ TendstoLocallyUniformly(\\text{eisSummand},\\ eisensteinSeries, k, a)$$$
Lean4
/-- 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_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : ℕ} (a : Fin 2 → ZMod N) :
TendstoLocallyUniformly (fun (s : Finset (gammaSet N 1 a)) ↦ (∑ x ∈ s, eisSummand k x ·)) (eisensteinSeries a k ·)
Filter.atTop :=
by
have hk' : (2 : ℝ) < k := by norm_cast
have p_sum : Summable fun x : gammaSet N 1 a ↦ ‖x.val‖ ^ (-k) :=
mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N 1 a)
simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]
intro K hK
obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact hK
refine (tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ)) (fun p z hz ↦ ?_)).mono HABK
simpa only [eisSummand, one_div, ← zpow_neg, norm_zpow, ← Real.rpow_intCast, Int.cast_neg] using
summand_bound_of_mem_verticalStrip (by positivity) p hB hz
