English
The HasSum property extends to the qExpansionFormalMultilinearSeries in the setting of modular forms, reflecting the Taylor expansion around 0 for the cusp function.
Русский
Свойство HasSum распространяется на qExpansionFormalMultilinearSeries в контексте модулярных форм; аналог Taylor-разложения около 0.
LaTeX
$$$HasSum\bigl( m \mapsto (qExpansionFormalMultilinearSeries\; n\; f)\, m \cdot q^m \bigr) = \text{cuspFunction } n\, f\, q$$$
Lean4
/-- The `q`-expansion of `f` is an `FPowerSeries` representing `cuspFunction n f`. -/
theorem hasFPowerSeries_cuspFunction [NeZero n] [ModularFormClass F Γ(n) k] :
HasFPowerSeriesOnBall (cuspFunction n f) (qExpansionFormalMultilinearSeries n f) 0 1 :=
by
refine ⟨qExpansionFormalMultilinearSeries_radius n f, zero_lt_one, fun hy ↦ ?_⟩
rw [EMetric.mem_ball, edist_zero_right, enorm_eq_nnnorm, ENNReal.coe_lt_one_iff, ← NNReal.coe_lt_one,
coe_nnnorm] at hy
simpa [qExpansionFormalMultilinearSeries] using hasSum_qExpansion_of_abs_lt n f hy
