English
For NeZero n, the q-expansion of a level-n modular form f converges to f on the upper half-plane; equivalently, the series with coefficients (qExpansion n f).coeff m converges to f(τ) for τ ∈ ℍ.
Русский
Сходима q-разложения mодулярной формы уровня n к самой форме на верхней полуплоскости; сумма коэффициентов дает f(τ).
LaTeX
$$$\text{HasSum}\left( m \mapsto (qExpansion\, n\, f).\text{coeff}\, m \cdot q^m \right) (f(\tau))$, где $q = \mathbf{q}_n(\tau)$$$
Lean4
theorem differentiableAt_cuspFunction [NeZero n] [ModularFormClass F Γ(n) k] {q : ℂ} (hq : ‖q‖ < 1) :
DifferentiableAt ℂ (cuspFunction n f) q :=
by
have npos : 0 < (n : ℝ) := mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _))
rcases eq_or_ne q 0 with rfl | hq'
·
exact
(periodic_comp_ofComplex n f).differentiableAt_cuspFunction_zero npos
(eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0)) (fun _ ↦ differentiableAt_comp_ofComplex f))
(bounded_at_infty_comp_ofComplex f)
·
exact
Periodic.qParam_right_inv npos.ne' hq' ▸ (periodic_comp_ofComplex n f).differentiableAt_cuspFunction npos.ne' <|
differentiableAt_comp_ofComplex _ <| Periodic.im_invQParam_pos_of_norm_lt_one npos hq hq'
