hasSum_qExpansion — Mathlib

English

For NeZero n and modular form data, cuspFunction n f is differentiable at every point with positive imaginary part and certain decay conditions near 0; in particular, cuspFunction is differentiable on the unit disk away from 0.

Русский

Для непустого n и данных формы, cuspFunction n f дифференцируема в точках с Im > 0 и в окрестности 0 с учётом условий распада; в частности, на единичной окружности вне 0.

LaTeX

$$$\text{DifferentiableAt}_{\mathbb{C}}(\text{cuspFunction } n\, f, z) \text{ for } z \text{ with } \Im z > 0$$$

Lean4

theorem hasSum_qExpansion [NeZero n] [ModularFormClass F Γ(n) k] (τ : ℍ) :
    HasSum (fun m : ℕ ↦ (qExpansion n f).coeff m • 𝕢 n τ ^ m) (f τ) := by
  simpa only [eq_cuspFunction n f] using hasSum_qExpansion_of_abs_lt n f (τ.norm_qParam_lt_one n)

Похожие утверждения