English
A variant of uniform convergence formulated with maps ℂ → ℂ, suitable for holomorphicity, holds on the upper half-plane with Im(z) > 0.
Русский
Вариант локальной равномерности формулирован для отображений ℂ → ℂ подходит для голоморфности на верхней полуплоскости, где Im(z) > 0.
LaTeX
$$$\\forall k\\in \\mathbb{Z},\\; \\forall N\\in \\mathbb{N},\\; \\ TendstoLocallyUniformlyOn(\\dots)\\; (\\text{upper half-plane with } \\operatorname{Im} z > 0)$$$
Lean4
/-- Variant of `eisensteinSeries_tendstoLocallyUniformly` formulated with maps `ℂ → ℂ`, which is
nice to have for holomorphicity later. -/
theorem eisensteinSeries_tendstoLocallyUniformlyOn {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N 1 a)) ↦ ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z))
(↑ₕ(eisensteinSeries_SIF a k).toFun) Filter.atTop {z : ℂ | 0 < z.im} :=
by
rw [← Subtype.coe_image_univ {z : ℂ | 0 < z.im}]
apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)
· simp only [SlashInvariantForm.toFun_eq_coe, Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]
apply eisensteinSeries_tendstoLocallyUniformly hk
·
simp only [IsOpenEmbedding.toOpenPartialHomeomorph_target, Set.top_eq_univ, mapsTo_range_iff, Set.mem_univ,
forall_const]
