English
If q lies in the unit disk, then HasSum holds for the q-expansion of f with coefficients of qExpansion n f; i.e., the q-expansion converges to cuspFunction.
Русский
Для |q|<1 сумма ряда с коэффициентами qExpansion сходится к cuspFunction.
LaTeX
$$$HasSum( m \mapsto (qExpansion n f).coeff m \cdot q^m ) (cuspFunction n f q)$ при $|q|<1$$$
Lean4
theorem hasSum_qExpansion_of_abs_lt [NeZero n] [ModularFormClass F Γ(n) k] {q : ℂ} (hq : ‖q‖ < 1) :
HasSum (fun m : ℕ ↦ (qExpansion n f).coeff m • q ^ m) (cuspFunction n f q) :=
by
simp only [qExpansion_coeff]
have hdiff : DifferentiableOn ℂ (cuspFunction n f) (Metric.ball 0 1) :=
by
refine fun z hz ↦ (differentiableAt_cuspFunction n f ?_).differentiableWithinAt
simpa using hz
have qmem : q ∈ Metric.ball 0 1 := by simpa using hq
convert hasSum_taylorSeries_on_ball hdiff qmem using 2 with m
rw [sub_zero, smul_eq_mul, smul_eq_mul, mul_right_comm, smul_eq_mul, mul_assoc]
