Theorems · Theorem · number theory

ModularForm.hasSum_L

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : ModularFormClass F Γ k],
  ↑k + 1 < s.re →
    HasSum (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑n ^ s)
      (↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s)

Defined in

Mathlib.NumberTheory.ModularForms.LFunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass