The q-expansion as a linear map, and uniqueness of coefficients for raw functions

The q-expansion of modular forms for a determinant-one subgroup of GL(2, ℝ), bundled as a ℂ-linear map into power series, refining Mathlib's additive ModularForm.qExpansionAddHom.

Alongside it, the raw-function form of Mathlib's coefficient-uniqueness statement. Mathlib's UpperHalfPlane.qExpansion_coeff_unique is stated for a bundled f : F with [FunLike F ℍ ℂ], and ℍ → ℂ carries no such instance, so an operator built as a plain function on ℍ — every Hecke-style slash sum before it is packaged as a ModularForm — cannot invoke it. The proof is Mathlib's, run through UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction, which is stated for {f : ℍ → ℂ}, with qExpansionFormalMultilinearSeries spelled out inline for the same reason.

Alongside them, the n-th coefficient bundled as a ℂ-linear functional on cusp forms, CuspForm.qExpansionCoeffₗ — the linear map above, composed with the inclusion of cusp forms and with PowerSeries.coeff n. It is what a coefficient computation on a linear combination of cusp forms is run through, and CuspForm.qExpansion_injective turns the resulting coefficient identity back into an identity of cusp forms.

Alongside those, the effect of a 1 / d translation on the q-powers a support condition leaves alive: shifting the argument by 1 / d scales the n-th q-power by a d-th root of unity raised to n, so a coefficient function supported on the multiples of d does not see the shift. That is what a q-support hypothesis is spent on when descending along V_d, and it is stated here rather than at the descent because it mentions only coefficients, divisibility and Function.Periodic.qParam.

Finally, the q-parameter as a function on ℍ: it is periodic, its own q-expansion is X, and a periodic function whose q-expansion has no constant term is asymptotic at i∞ to its q-coefficient times q. These are what a function with a pole at the cusp, such as j, is expanded through: one multiplies by q and divides the expansion of the product by q.

Main declarations

• TauCeti.ModularForm.qExpansionLinearMap.
• TauCeti.UpperHalfPlane.qExpansion_coeff_unique.
• CuspForm.qExpansionCoeffₗ (at root, so dot notation on CuspForm elaborates): the n-th coefficient as a ℂ-linear functional on cusp forms.
• CuspForm.qExpansion_injective: a cusp form is determined by its q-expansion.
• TauCeti.smul_qParam_pow_shift_eq: a shift by 1 / d fixes every q-power that a d-supported coefficient function leaves alive.
• TauCeti.UpperHalfPlane.qExpansion_qParam: the q-expansion of q is X.
• TauCeti.UpperHalfPlane.tendsto_div_qParam_atImInfty: f / q tends to the q-coefficient of f when the constant coefficient vanishes.

References

• Mathlib PR #39000 (Chris Birkbeck) — the upstream draft this file ports onto the current Mathlib pin.

noncomputable def TauCeti.ModularForm.qExpansionLinearMap {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) : ModularForm Γ k →ₗ[ℂ] PowerSeries ℂ

The q-expansion map as a ℂ-linear map to power series over ℂ, refining the additive ModularForm.qExpansionAddHom.

Equations

• TauCeti.ModularForm.qExpansionLinearMap hh hΓ k = { toAddHom := ↑(ModularForm.qExpansionAddHom hh hΓ k), map_smul' := ⋯ }

@[simp]

theorem TauCeti.ModularForm.qExpansionLinearMap_apply {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {k : ℤ} (f : ModularForm Γ k) : (qExpansionLinearMap hh hΓ k) f = UpperHalfPlane.qExpansion h ⇑f

theorem TauCeti.UpperHalfPlane.qExpansion_coeff_unique {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0) (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) (m : ℕ) : c m = (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f)

Uniqueness of q-expansion coefficients, for a raw function on ℍ. If f is given by a convergent expansion f τ = ∑' m, c m * 𝕢 h τ ^ m and its cusp function is analytic at 0, then the c m are the coefficients of qExpansion h f.

This is Mathlib's UpperHalfPlane.qExpansion_coeff_unique with the [FunLike F ℍ ℂ] bundling removed: ℍ → ℂ has no FunLike instance, so the bundled statement does not apply to an operator that is still a plain function.

theorem TauCeti.UpperHalfPlane.periodic_qParam_comp_ofComplex {h : ℝ} (hh : h ≠ 0) : Function.Periodic ((fun (τ : UpperHalfPlane) => Function.Periodic.qParam h ↑τ) ∘ ↑UpperHalfPlane.ofComplex) ↑h

The q-parameter of width h is h-periodic, read on ℂ through ofComplex.

theorem TauCeti.UpperHalfPlane.qExpansion_qParam {h : ℝ} (hh : 0 < h) : (UpperHalfPlane.qExpansion h fun (τ : UpperHalfPlane) => Function.Periodic.qParam h ↑τ) = PowerSeries.X

The q-expansion of the q-parameter itself is the variable X.

theorem TauCeti.UpperHalfPlane.tendsto_div_qParam_atImInfty {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hfdiff : DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h f) 0) (hf0 : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h f) = 0) : Filter.Tendsto (fun (τ : UpperHalfPlane) => f τ / Function.Periodic.qParam h ↑τ) UpperHalfPlane.atImInfty (nhds ((PowerSeries.coeff 1) (UpperHalfPlane.qExpansion h f)))

A periodic function whose q-expansion has no constant term is asymptotic to its first coefficient times q at i∞: f τ / q tends to the coefficient of q.

noncomputable def CuspForm.qExpansionCoeffₗ {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) (n : ℕ) : CuspForm Γ k →ₗ[ℂ] ℂ

The n-th q-expansion coefficient as a ℂ-linear functional on cusp forms. f ↦ (qExpansion h f).coeff n, bundled: the coefficient of a linear combination of cusp forms is that combination of their coefficients, by map_add, map_sub and map_smul.

Equations

• CuspForm.qExpansionCoeffₗ hh hΓ k n = PowerSeries.coeff n ∘ₗ TauCeti.ModularForm.qExpansionLinearMap hh hΓ k ∘ₗ CuspForm.toModularFormₗ

@[simp]

theorem CuspForm.qExpansionCoeffₗ_apply {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {k : ℤ} (n : ℕ) (f : CuspForm Γ k) : (qExpansionCoeffₗ hh hΓ k n) f = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f)

theorem CuspForm.qExpansion_injective {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {k : ℤ} : Function.Injective fun (f : CuspForm Γ k) => UpperHalfPlane.qExpansion h ⇑f

A cusp form is determined by its q-expansion. The cusp-form counterpart of Mathlib's ModularForm.qExpansion_injective: a cusp form and its image under the injective inclusion CuspForm.toModularFormₗ have the same underlying function.

theorem TauCeti.smul_qParam_pow_shift_eq {d : ℕ} [NeZero d] {c : ℕ → ℂ} (hc : ∀ (n : ℕ), ¬d ∣ n → c n = 0) (σ : UpperHalfPlane) (n : ℕ) : c n • Function.Periodic.qParam 1 ↑(1 / ↑d +ᵥ σ) ^ n = c n • Function.Periodic.qParam 1 ↑σ ^ n

A shift by 1 / d fixes every q-power the support condition leaves alive. Translating the argument by 1 / d scales the n-th q-power by a d-th root of unity raised to n, which is trivial exactly on the multiples of d — and a coefficient function supported there kills every other index. This is what a q-support hypothesis is spent on when descending along V_d.