q-expansions of modular forms

We show that a modular form of level Γ(n) can be written as τ ↦ F (𝕢 n τ) where F is analytic on the open unit disc, and 𝕢 n is the parameter τ ↦ exp (2 * I * π * τ / n). As an application, we show that cusp forms decay exponentially to 0 as im τ → ∞.

We also define the q-expansion of a modular form, either as a power series or as a FormalMultilinearSeries, and show that it converges to f on the upper half plane.

Main definitions and results

• SlashInvariantFormClass.cuspFunction: for a level n slash-invariant form, this is the function F such that f τ = F (exp (2 * π * I * τ / n)), extended by a choice of limit at 0.
• ModularFormClass.differentiableAt_cuspFunction: when f is a modular form, its cuspFunction is differentiable on the open unit disc (including at 0).
• ModularFormClass.qExpansion: the q-expansion of a modular form (defined as the Taylor series of its cuspFunction), bundled as a PowerSeries.
• ModularFormClass.hasSum_qExpansion: the q-expansion evaluated at 𝕢 n τ sums to f τ, for τ in the upper half plane.
• qExpansionRingHom defines the ring homomorphism from the graded ring of modular forms to power series given by taking q-expansions.
• qExpansion_coeff_unique shows that q-expansion coefficients are uniquely determined.

def UpperHalfPlane.valueAtInfty (f : UpperHalfPlane → ℂ) : ℂ

The value of f at the cusp ∞ (or an arbitrary choice of value if this limit is not well-defined).

theorem UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) : valueAtInfty f = 0

theorem UpperHalfPlane.qParam_tendsto_atImInfty {h : ℝ} (hh : 0 < h) : Filter.Tendsto (fun (τ : UpperHalfPlane) => Function.Periodic.qParam h ↑τ) atImInfty (nhds 0)

theorem SlashInvariantFormClass.periodic_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [SlashInvariantFormClass F Γ k] (hΓ : h ∈ Γ.strictPeriods) : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h

def SlashInvariantFormClass.cuspFunction (h : ℝ) (f : UpperHalfPlane → ℂ) : ℂ → ℂ

The analytic function F such that f τ = F (exp (2 * π * I * τ / h)), extended by a choice of limit at 0.

theorem SlashInvariantFormClass.eq_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [SlashInvariantFormClass F Γ k] (τ : UpperHalfPlane) (hΓ : h ∈ Γ.strictPeriods) (hh : h ≠ 0) : cuspFunction h (⇑f) (Function.Periodic.qParam h ↑τ) = f τ

theorem ModularFormClass.differentiableAt_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] {z : ℂ} (hz : 0 < z.im) : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) z

theorem ModularFormClass.bounded_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] (hi : IsCusp OnePoint.infty Γ) : (Filter.comap Complex.im Filter.atTop).BoundedAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem ModularFormClass.differentiableAt_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {q : ℂ} (hq : ‖q‖ < 1) : DifferentiableAt ℂ (SlashInvariantFormClass.cuspFunction h ⇑f) q

theorem ModularFormClass.differentiableOn_cuspFunction_ball {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : DifferentiableOn ℂ (SlashInvariantFormClass.cuspFunction h ⇑f) (Metric.ball 0 1)

theorem ModularFormClass.analyticAt_cuspFunction_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : AnalyticAt ℂ (SlashInvariantFormClass.cuspFunction h ⇑f) 0

theorem ModularFormClass.cuspFunction_apply_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : SlashInvariantFormClass.cuspFunction h (⇑f) 0 = UpperHalfPlane.valueAtInfty ⇑f

def ModularFormClass.qExpansion (h : ℝ) (f : UpperHalfPlane → ℂ) : PowerSeries ℂ

The q-expansion of a level n modular form, bundled as a PowerSeries.

theorem ModularFormClass.qExpansion_coeff {h : ℝ} (f : UpperHalfPlane → ℂ) (m : ℕ) : (PowerSeries.coeff m) (qExpansion h f) = (↑m.factorial)⁻¹ * iteratedDeriv m (SlashInvariantFormClass.cuspFunction h f) 0

theorem ModularFormClass.qExpansion_coeff_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : (PowerSeries.coeff 0) (qExpansion h ⇑f) = UpperHalfPlane.valueAtInfty ⇑f

theorem ModularFormClass.hasSum_qExpansion_of_norm_lt {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {q : ℂ} (hq : ‖q‖ < 1) : HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (qExpansion h ⇑f) • q ^ m) (SlashInvariantFormClass.cuspFunction h (⇑f) q)

@[deprecated ModularFormClass.hasSum_qExpansion_of_norm_lt (since := "2025-12-04")]

theorem ModularFormClass.hasSum_qExpansion_of_abs_lt {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {q : ℂ} (hq : ‖q‖ < 1) : HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (qExpansion h ⇑f) • q ^ m) (SlashInvariantFormClass.cuspFunction h (⇑f) q)

Alias of ModularFormClass.hasSum_qExpansion_of_norm_lt.

theorem ModularFormClass.hasSum_qExpansion {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (τ : UpperHalfPlane) : HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (qExpansion h ⇑f) • Function.Periodic.qParam h ↑τ ^ m) (f τ)

def ModularFormClass.qExpansionFormalMultilinearSeries {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (h : ℝ) (f : F) : FormalMultilinearSeries ℂ ℂ ℂ

The q-expansion of a modular form, bundled as a FormalMultilinearSeries.

TODO: Maybe get rid of this and instead define a general API for converting PowerSeries to FormalMultilinearSeries.

@[simp]

theorem ModularFormClass.qExpansionFormalMultilinearSeries_coeff {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ) : (qExpansionFormalMultilinearSeries h f).coeff m = (PowerSeries.coeff m) (qExpansion h ⇑f)

theorem ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ) : ‖qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

theorem ModularFormClass.qExpansionFormalMultilinearSeries_radius {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : 1 ≤ (qExpansionFormalMultilinearSeries h f).radius

theorem ModularFormClass.hasFPowerSeries_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : HasFPowerSeriesOnBall (SlashInvariantFormClass.cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

The q-expansion of f is an FPowerSeries representing cuspFunction n f.

theorem ModularFormClass.qExpansion_coeff_eq_circleIntegral {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (n : ℕ) {R : ℝ} (hR : 0 < R) (hR' : R < 1) : (PowerSeries.coeff n) (qExpansion h ⇑f) = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), SlashInvariantFormClass.cuspFunction h (⇑f) z / z ^ (n + 1)

The q-expansion coefficient can be expressed as a circleIntegral for any radius 0 < R < 1.

theorem ModularFormClass.qExpansion_coeff_eq_intervalIntegral {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (n : ℕ) {t : ℝ} (ht : 0 < t) : (PowerSeries.coeff n) (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 := ⋯ }

If h is a positive strict period of f, then the q-expansion coefficient can be expressed as an integral along a horizontal line in the upper half-plane from t * I to h + t * I, for any 0 < t.

theorem ModularFormClass.exp_decay_sub_atImInfty {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : (fun (τ : UpperHalfPlane) => f τ - UpperHalfPlane.valueAtInfty ⇑f) =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem ModularFormClass.exp_decay_sub_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] : ∃ c > 0, (fun (τ : UpperHalfPlane) => f τ - UpperHalfPlane.valueAtInfty ⇑f) =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

Version of exp_decay_sub_atImInfty stating a less precise result but easier to apply in practice (not specifying the growth rate precisely).

Note that the Fact hypothesis is automatically synthesized for arithmetic subgroups. The discreteness hypothesis may be unnecessary, but it is satisfied in the cases of interest.

theorem UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (f ∘ ↑ofComplex)

theorem UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) (hh : 0 < h) : SlashInvariantFormClass.cuspFunction h f 0 = 0

theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {f : F} [ModularFormClass F Γ k] (hf : IsZeroAtImInfty ⇑f) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : ⇑f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {f : F} [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] (hf : IsZeroAtImInfty ⇑f) : ∃ c > 0, ⇑f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

Version of exp_decay_atImInfty stating a less precise result but easier to apply in practice (not specifying the growth rate precisely). Note that the Fact hypothesis is automatically synthesized for arithmetic subgroups.

theorem CuspFormClass.zero_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)] : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem CuspFormClass.cuspFunction_apply_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [CuspFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : SlashInvariantFormClass.cuspFunction h (⇑f) 0 = 0

theorem CuspFormClass.exp_decay_atImInfty {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [CuspFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : ⇑f =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem CuspFormClass.exp_decay_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] : ∃ c > 0, ⇑f =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

theorem cuspFunction_mul_zero {h : ℝ} {f g : ℂ → ℂ} (hfcts : ContinuousAt (Function.Periodic.cuspFunction h f) 0) (hgcts : ContinuousAt (Function.Periodic.cuspFunction h g) 0) : Function.Periodic.cuspFunction h (f * g) 0 = Function.Periodic.cuspFunction h f 0 * Function.Periodic.cuspFunction h g 0

theorem qExpansion_mul_coeff_zero {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) (hgcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h g) 0) : (PowerSeries.coeff 0) (ModularFormClass.qExpansion h (f * g)) = (PowerSeries.coeff 0) (ModularFormClass.qExpansion h f) * (PowerSeries.coeff 0) (ModularFormClass.qExpansion h g)

theorem cuspFunction_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) (hgcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h g) 0) : SlashInvariantFormClass.cuspFunction h (f * g) = SlashInvariantFormClass.cuspFunction h f * SlashInvariantFormClass.cuspFunction h g

theorem ModularForm.cuspFunction_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : SlashInvariantFormClass.cuspFunction h ⇑(f.mul g) = SlashInvariantFormClass.cuspFunction h ⇑f * SlashInvariantFormClass.cuspFunction h ⇑g

theorem cuspFunction_smul {h : ℝ} {f : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) (a : ℂ) : SlashInvariantFormClass.cuspFunction h (a • f) = a • SlashInvariantFormClass.cuspFunction h f

theorem cuspFunction_neg {h : ℝ} {f : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) : SlashInvariantFormClass.cuspFunction h (-f) = -SlashInvariantFormClass.cuspFunction h f

theorem cuspFunction_add {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) (hgcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h g) 0) : SlashInvariantFormClass.cuspFunction h (f + g) = SlashInvariantFormClass.cuspFunction h f + SlashInvariantFormClass.cuspFunction h g

theorem cuspFunction_sub {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h f) 0) (hgcts : ContinuousAt (SlashInvariantFormClass.cuspFunction h g) 0) : SlashInvariantFormClass.cuspFunction h (f - g) = SlashInvariantFormClass.cuspFunction h f - SlashInvariantFormClass.cuspFunction h g

theorem qExpansion_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (SlashInvariantFormClass.cuspFunction h f) 0) (hg : AnalyticAt ℂ (SlashInvariantFormClass.cuspFunction h g) 0) : ModularFormClass.qExpansion h (f * g) = ModularFormClass.qExpansion h f * ModularFormClass.qExpansion h g

theorem ModularForm.qExpansion_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : ModularFormClass.qExpansion h ⇑(f.mul g) = ModularFormClass.qExpansion h ⇑f * ModularFormClass.qExpansion h ⇑g

theorem qExpansion_add {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] : ModularFormClass.qExpansion h (⇑f + ⇑g) = ModularFormClass.qExpansion h ⇑f + ModularFormClass.qExpansion h ⇑g

theorem qExpansion_smul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] : ModularFormClass.qExpansion h (a • ⇑f) = a • ModularFormClass.qExpansion h ⇑f

theorem qExpansion_neg {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : F) [ModularFormClass F Γ k] : ModularFormClass.qExpansion h (-⇑f) = -ModularFormClass.qExpansion h ⇑f

theorem qExpansion_sub {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : ModularFormClass.qExpansion h (⇑f - ⇑g) = ModularFormClass.qExpansion h ⇑f - ModularFormClass.qExpansion h ⇑g

theorem qExpansion_zero (h : ℝ) : ModularFormClass.qExpansion h 0 = 0

theorem qExpansion_eq_zero_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {k : ℤ} (f : ModularForm Γ k) : ModularFormClass.qExpansion h ⇑f = 0 ↔ f = 0

def qExpansionAddHom {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) : ModularForm Γ k →+ PowerSeries ℂ

The qExpansion map as an additive group hom. to power series over ℂ.

theorem qExpansion_one {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] : ModularFormClass.qExpansion h ⇑1 = 1

def qExpansionRingHom {Γ : Subgroup (GL (Fin 2) ℝ)} (h : ℝ) [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : (DirectSum ℤ fun (k : ℤ) => ModularForm Γ k) →+* PowerSeries ℂ

The qExpansion map as a map from the graded ring of modular forms to power series over ℂ.

@[simp]

theorem qExpansionRingHom_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) (f : ModularForm Γ k) : (qExpansionRingHom h hh hΓ) ((DirectSum.of (ModularForm Γ) k) f) = ModularFormClass.qExpansion h ⇑f

theorem qExpansion_of_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a b : ℤ) (f : ModularForm Γ a) (g : ModularForm Γ b) : ModularFormClass.qExpansion h ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) = ModularFormClass.qExpansion h ⇑f * ModularFormClass.qExpansion h ⇑g

theorem qExpansion_of_pow {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : ModularForm Γ k) (n : ℕ) : ModularFormClass.qExpansion h ⇑(((DirectSum.of (ModularForm Γ) k) f ^ n) (↑n * k)) = ModularFormClass.qExpansion h ⇑f ^ n

theorem hasFPowerSeriesOnBall_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {c : ℕ → ℂ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {f : F} [ModularFormClass F Γ k] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) : HasFPowerSeriesOnBall (SlashInvariantFormClass.cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

theorem qExpansion_coeff_unique {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {c : ℕ → ℂ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {f : F} [ModularFormClass F Γ k] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) (m : ℕ) : c m = (PowerSeries.coeff m) (ModularFormClass.qExpansion h ⇑f)