English
For hk with hk ≥ 3 and any A ∈ SL(2,Z), the SL-action-transformed Eisenstein series SIF is bounded at infinity.
Русский
При hk ≥ 3 и любом A∈SL(2,Z, преобразованный по SL) ряд Эйзенштейна-форма SIF ограничен на бесконечности.
LaTeX
$$$\text{IsBoundedAtImInfty}(((\mathrm{eisensteinSeries\_SIF}(a,k)).toFun \mid[ k] A))$ for all A ∈ SL(2,ℤ).$$
Lean4
/-- Eisenstein series are bounded at infinity. -/
theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ} [NeZero N] (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k)
(A : SL(2, ℤ)) : IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A) :=
by
simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeries_SIF] at *
refine ⟨∑' (x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
intro z hz
obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z (NeZero.pos N))
rw [eisensteinSeries_slash_apply, ← eisensteinSeries_SIF_apply, ←
T_zpow_width_invariant N k n (eisensteinSeries_SIF (a ᵥ* A) k) z]
apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)
have hk' : (2 : ℝ) < k := by norm_cast
apply (summable_norm_eisSummand hk _).tsum_le_tsum _
· exact_mod_cast (summable_one_div_norm_rpow hk').mul_left <| r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k)
· intro x
simp_rw [eisSummand, norm_zpow]
exact_mod_cast
summand_bound_of_mem_verticalStrip (lt_trans two_pos hk').le x two_pos (verticalStrip_anti_right N hz hn)
