Theorems · Theorem · number theory

ModularForm.hasSum_qExpansion

∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F),
  0 < h →
    ∀ {k : ℤ} [ModularFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)],
      h ∈ Γ.strictPeriods →
        ∀ (τ : UpperHalfPlane),
          HasSum (fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f) * Function.Periodic.qParam h ↑τ ^ m)
            (f τ)

Specialized version of UpperHalfPlane.hasSum_qExpansion for modular forms, with many arguments filled in automatically.

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

0 results in Mathlib

Foundations

Depth 293 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeModularFormClassFact