The Fricke functional equation of a cusp form

For a cusp form f of positive integral weight, the level-N completion is the Mellin transform of the restriction of f to the rescaled imaginary axis,

Λ_N(s, f) = Mellin (t ↦ f(i t / √N)) s.

If g is the Petersson-normalized Fricke companion g = (√N)^(2-k) • (f ∣[k] W_N), then

Λ_N(k - s, f) = i^k Λ_N(s, g).

The rescaling identity for Mellin transforms identifies Λ_N with (√N)^s times Mathlib's entire ModularForm.Λ, so the completed function is entire. On Γ₁(N), Tau Ceti's bundled normalizedFrickeOperatorCusp supplies the companion without an additional hypothesis.

Main results

• UpperHalfPlane.resToImagAxis_slash_frickeGL: the Fricke slash on the rescaled imaginary axis.
• CuspForm.frickeCompletedL: the level-N completed L-function.
• CuspForm.frickeCompletedL_eq_cpow_mul_Λ: its expression as N^(s/2) · ModularForm.Λ.
• CuspForm.frickeCompletedL_sub_eq_I_zpow_mul: Λ_N(k - s, f) = i^k Λ_N(s, g) for any Fricke companion g, without weight or width hypotheses.
• CuspForm.frickeCompletedL_functional_equation: the two-form Fricke functional equation.
• CuspForm.frickeCompletedL_functional_equation_gamma1: the functional equation on Γ₁(N) with the bundled normalized Fricke companion.

Provenance

Adapted from the AINTLIB LeanModularForms project (Apache-2.0, commit 112d12d95), LeanModularForms/Modularforms/LFunctionFEqN.lean. This version reuses Mathlib's completed L-function and Mellin change-of-variables API instead of rebuilding the analytic-continuation argument.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, Theorem 5.10.2.
• G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Section 3.6.
• T. Miyake, Modular Forms, Theorem 4.3.5.

theorem UpperHalfPlane.resToImagAxis_slash_frickeGL {N : ℕ} [NeZero N] {k : ℤ} (F : UpperHalfPlane → ℂ) {t : ℝ} (ht : 0 < t) : resToImagAxis (SlashAction.map k (TauCeti.frickeGL ℝ N) F) (t / √↑N) = ↑√↑N ^ (k - 2) * Complex.I ^ (-k) * ↑t ^ (-k) * resToImagAxis F (1 / t / √↑N)

The Fricke slash on the rescaled imaginary axis. For t > 0,

(F ∣[k] W_N)(i t / √N) = (√N)^(k-2) i^(-k) t^(-k) F(i / (t√N)).

The power of √N is exactly cancelled by the Petersson normalization of the Fricke operator.

noncomputable def CuspForm.frickeCompletedL {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (f : CuspForm Γ k) (N : ℕ+) (s : ℂ) : ℂ

The level-N completed L-function of a cusp form, for a positive level N, defined as the Mellin transform of its restriction to the rescaled imaginary axis t ↦ i t / √N.

Equations

• f.frickeCompletedL N s = mellin (fun (t : ℝ) => UpperHalfPlane.resToImagAxis (⇑f) (t / √↑↑N)) s

@[simp]

theorem CuspForm.frickeCompletedL_apply {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (f : CuspForm Γ k) (N : ℕ+) (s : ℂ) : f.frickeCompletedL N s = mellin (fun (t : ℝ) => UpperHalfPlane.resToImagAxis (⇑f) (t / √↑↑N)) s

The defining equation for the level-N completed L-function.

theorem CuspForm.frickeCompletedL_smul {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (c : ℂ) (f : CuspForm Γ k) (N : ℕ+) (s : ℂ) : (c • f).frickeCompletedL N s = c * f.frickeCompletedL N s

The level-N completed L-function is linear in the form: Λ_N(s, c • f) = c Λ_N(s, f).

theorem CuspForm.frickeCompletedL_eq_cpow_mul_Λ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] (f : CuspForm Γ k) (N : ℕ+) (hk : 0 < k) (s : ℂ) : f.frickeCompletedL N s = ↑↑N ^ (s / 2) * ModularForm.Λ hk f s

The level-N completed L-function is N^(s/2) times Mathlib's completed L-function ModularForm.Λ. Thus this definition has the classical completion N^(s/2) (2π)^(-s) Γ(s) L(s, f) on the Dirichlet-series half-plane.

theorem CuspForm.differentiable_frickeCompletedL {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] (f : CuspForm Γ k) (N : ℕ+) (hk : 0 < k) : Differentiable ℂ (f.frickeCompletedL N)

The level-N completed L-function of a positive-weight cusp form is entire.

theorem CuspForm.frickeCompletedL_sub_eq_I_zpow_mul {k : ℤ} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℝ)} (f : CuspForm Γ₁ k) (g : CuspForm Γ₂ k) (N : ℕ) [NeZero N] (hg : ⇑g = ↑√↑N ^ (2 - k) • SlashAction.map k (TauCeti.frickeGL ℝ N) ⇑f) (s : ℂ) : f.frickeCompletedL (N.toPNat ⋯) (↑k - s) = Complex.I ^ k * g.frickeCompletedL (N.toPNat ⋯) s

The identity underlying Hecke's two-form functional equation. If g is the Petersson-normalized Fricke companion of f, then Λ_N(k - s, f) = i^k Λ_N(s, g), without additional weight or width hypotheses; this follows from Mellin change of variables alone.

theorem CuspForm.frickeCompletedL_functional_equation {k : ℤ} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℝ)} (f : CuspForm Γ₁ k) (g : CuspForm Γ₂ k) (N : ℕ) [NeZero N] (_hw₁ : Γ₁.strictWidthInfty = 1) (_hw₂ : Γ₂.strictWidthInfty = 1) (_hk : 0 < k) (hg : ⇑g = ↑√↑N ^ (2 - k) • SlashAction.map k (TauCeti.frickeGL ℝ N) ⇑f) (s : ℂ) : f.frickeCompletedL (N.toPNat ⋯) (↑k - s) = Complex.I ^ k * g.frickeCompletedL (N.toPNat ⋯) s

Hecke's two-form functional equation. If f and g are positive-weight, width-one cusp forms and g is the Petersson-normalized Fricke companion of f, then Λ_N(k - s, f) = i^k Λ_N(s, g). The two forms may live on different carriers, but both have weight k. This is the classical hypothesis-bearing interface; for the stronger underlying Mellin identity, use frickeCompletedL_sub_eq_I_zpow_mul.

theorem CuspForm.frickeCompletedL_functional_equation_gamma1 {N : ℕ} [NeZero N] {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (hk : 0 < k) (s : ℂ) : f.frickeCompletedL (N.toPNat ⋯) (↑k - s) = Complex.I ^ k * ((TauCeti.normalizedFrickeOperatorCusp k) f).frickeCompletedL (N.toPNat ⋯) s

Hecke's functional equation for a positive-weight cusp form on Γ₁(N), with the normalized Fricke operator providing the companion cusp form.