Theorems · Theorem · number theory

ModularFormClass.qExpansion_coeff_eq_intervalIntegral

∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (n : ℕ) {t : ℝ} (ht : 0 < t),
        (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) =
          1 / ↑h *
            ∫ (u : ℝ) in 0..h,
              1 / Function.Periodic.qParam h (↑u + ↑t * Complex.I) ^ n *
                f { coe := ↑u + ↑t * Complex.I, coe_im_pos := ⋯ }

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeModularFormClass