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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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 ⟨↑u + ↑t * Complex.I, ⋯⟩

If h is a positivie 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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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.

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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] (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)