Dirichlet series of modular forms

Mathlib's Mathlib/NumberTheory/ModularForms/LFunction.lean defines the completed L-function ModularForm.Λ and the L-function ModularForm.L of a modular form for an arithmetic level, with the Dirichlet-series identities ModularForm.hasSum_L and CuspForm.hasSum_L on their convergence half-planes, and — for cusp forms — entire continuation (CuspForm.differentiable_L). This file supplies the interface between that API and Mathlib's LSeries of the q-expansion coefficients:

• Hecke's abscissa-of-absolute-convergence bounds for the coefficient series, and
• the identification of LSeries of the coefficients with ModularForm.L on the convergence half-plane, in both the modular and the cuspidal ranges.

Main results

• ModularForm.abscissaOfAbsConv_qExpansion_coeff_le: for a modular form of weight k ≥ 0, the abscissa of absolute convergence of the coefficient series is at most k + 1 (from aₙ = O(nᵏ)).
• CuspForm.abscissaOfAbsConv_qExpansion_coeff_le: for a cusp form, at most k/2 + 1 (from Hecke's aₙ = O(n^{k/2})).
• ModularForm.LSeries_qExpansion_coeff_eq, CuspForm.LSeries_qExpansion_coeff_eq: on the respective half-planes, LSeries of the coefficients is (Γ.strictWidthInfty : ℂ) ^ (-s) * L hk f s for Mathlib's ModularForm.L.
• CuspForm.hasEntireExtension_qExpansion_coeff: the coefficient series of a cusp form of positive weight has an entire extension (the Layer-7 continuation milestone).
• CuspForm.L_ne_zero_of_qExpansion_coeff_ne_zero: a nonzero positive-index coefficient makes the entire L-function nonzero.
• CuspForm.eq_strictWidthInfty_cpow_mul_L: uniqueness of the width-normalized entire continuation.

The non-cuspidal abscissa bound k + 1 is weaker than Diamond–Shurman Prop. 5.9.1 (which gives convergence for Re s > k via aₙ = O(n^{k-1})); tightening it is a separate milestone of the roadmap's Layer 7. The entire continuation of the cusp-form series is CuspForm.hasEntireExtension_qExpansion_coeff below.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/LFunction.lean), rebuilt to consume Mathlib's ModularForm.L rather than defining a parallel Dirichlet series.

References

• [DS] Diamond–Shurman, A First Course in Modular Forms, §5.9
• [Miy] Miyake, Modular Forms, Thm 4.5.16
• The AINTLIB LeanModularForms project, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms (Modularforms/LFunction.lean)

theorem ModularForm.abscissaOfAbsConv_qExpansion_coeff_le {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (hk : 0 ≤ k) [ModularFormClass F Γ k] (f : F) : (LSeries.abscissaOfAbsConv fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) ≤ ↑↑k + 1

Hecke's abscissa bound for modular forms: for weight k ≥ 0, the Dirichlet series of the q-expansion coefficients converges absolutely for Re s > k + 1 (from aₙ = O(nᵏ)).

theorem ModularForm.LSeries_qExpansion_coeff_eq {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {s : ℂ} (hk : 0 < k) [ModularFormClass F Γ k] (f : F) (hs : ↑k + 1 < s.re) : LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) s = ↑Γ.strictWidthInfty ^ (-s) * L hk f s

On the half-plane Re s > k + 1, the Dirichlet series of the q-expansion coefficients is Mathlib's ModularForm.L, up to the width factor. Not @[simp]: the positivity witness hk occurs in the right-hand side L hk f s, so the rewrite cannot fire from the left-hand side alone (simpNF rejects it).

theorem CuspForm.abscissaOfAbsConv_qExpansion_coeff_le {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) : (LSeries.abscissaOfAbsConv fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) ≤ ↑(↑k / 2) + 1

Hecke's abscissa bound for cusp forms: the Dirichlet series of the q-expansion coefficients converges absolutely for Re s > k/2 + 1 (from Hecke's aₙ = O(n^{k/2})).

theorem CuspForm.LSeries_qExpansion_coeff_eq {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {s : ℂ} (hk : 0 < k) [CuspFormClass F Γ k] (f : F) (hs : ↑k / 2 + 1 < s.re) : LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) s = ↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s

On the half-plane Re s > k/2 + 1, the Dirichlet series of the q-expansion coefficients of a cusp form is Mathlib's ModularForm.L, up to the width factor. Not @[simp]: as with the modular-form version, hk occurs in the right-hand side.

theorem CuspForm.hasEntireExtension_qExpansion_coeff {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (hk : 0 < k) [CuspFormClass F Γ k] (f : F) : LSeries.HasEntireExtension fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)

Entire continuation of the L-series of a cusp form — the roadmap's Layer-7 continuation milestone: the Dirichlet series of the q-expansion coefficients of a cusp form of positive weight has an entire extension, namely s ↦ (Γ.strictWidthInfty : ℂ) ^ (-s) * L hk f s.

theorem CuspForm.L_ne_zero_of_qExpansion_coeff_ne_zero {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) (hk : 0 < k) {n : ℕ} (hn : n ≠ 0) (hcoeff : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) ≠ 0) : ModularForm.L hk f ≠ 0

The entire L-function of a positive-weight cusp form is nonzero if one of its positive-index coefficients is nonzero. This ensures that its analytic order is finite.

theorem CuspForm.analyticOrderAt_L_ne_top_of_qExpansion_coeff_ne_zero {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) (hk : 0 < k) (s : ℂ) {n : ℕ} (hn : n ≠ 0) (hcoeff : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) ≠ 0) : analyticOrderAt (ModularForm.L hk f) s ≠ ⊤

A positive-weight cusp form with a nonzero positive-index coefficient has finite analytic order at every point.

theorem CuspForm.eq_strictWidthInfty_cpow_mul_L {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) (hk : 0 < k) {G : ℂ → ℂ} (hG : Differentiable ℂ G) (hGL : ∀ {s : ℂ}, ↑k / 2 + 1 < s.re → G s = LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) s) : G = fun (s : ℂ) => ↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s

Any entire function agreeing with the coefficient Dirichlet series of a positive-weight cusp form on its convergence half-plane is the width-normalized entire L-function.