Theorems · Theorem · number theory

ModularFormClass.differentiableAt_cuspFunction

∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k],
  0 < h → h ∈ Γ.strictPeriods → ∀ {q : ℂ}, ‖q‖ < 1 → DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) q

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeModularFormClass