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.

TO DO:

• define the q-expansion map on modular form spaces as a linear map (or even a ring hom from the graded ring of all modular forms?)

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).

Equations

• UpperHalfPlane.valueAtInfty f = limUnder UpperHalfPlane.atImInfty f

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.

Equations

• SlashInvariantFormClass.cuspFunction h f = Function.Periodic.cuspFunction h (f ∘ ↑UpperHalfPlane.ofComplex)

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 {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (h : ℝ) (f : F) : PowerSeries ℂ

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

Equations

• ModularFormClass.qExpansion h f = PowerSeries.mk fun (m : ℕ) => (↑m.factorial)⁻¹ * iteratedDeriv m (SlashInvariantFormClass.cuspFunction h ⇑f) 0

theorem ModularFormClass.qExpansion_coeff {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (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.

Equations

• ModularFormClass.qExpansionFormalMultilinearSeries h f m = (PowerSeries.coeff m) (ModularFormClass.qExpansion h f) • ContinuousMultilinearMap.mkPiAlgebraFin ℂ m ℂ

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)