Theorems · Theorem · number theory

UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction

∀ {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        HasFPowerSeriesOnBall (UpperHalfPlane.cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

2 results in Mathlib

Foundations

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