Documentation

TauCeti.NumberTheory.ModularForms.LFunction.EulerProduct

Euler products of full Hecke eigenforms and newforms #

The Fourier coefficients of a normalized full Hecke eigenform are multiplicative at coprime indices and obey the quadratic Hecke recurrence at every prime. These are precisely the hypotheses of TauCeti.LSeries.LSeries_eulerProduct_tprod_of_recurrence. The character is extended by zero at primes dividing the level, so the quadratic Euler factor becomes linear there.

This gives the Euler product for the coefficient L-series and, through the width-one normalization, for Mathlib's ModularForm.L. The full eigenform structure of a newform, including its bad-prime eigenrelations, gives the newform Euler product.

References #

source
theorem HeckeRing.GL2.Eigenform.LSeries_eulerProduct_hasProd {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
HasProd (fun (p : Nat.Primes) => (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹) (LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s)

The quadratic Euler factors of a normalized full Hecke eigenform have product equal to its coefficient L-series on Re s > k/2 + 1. The zero-extended character makes the factors linear at bad primes.

source
theorem HeckeRing.GL2.Eigenform.LSeries_eulerProduct_tprod {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
∏' (p : Nat.Primes), (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹ = LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s

Euler product of a normalized full Hecke eigenform, as a tprod equality on Re s > k/2 + 1.

source
theorem HeckeRing.GL2.Eigenform.LSeries_eulerProduct {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑p * ↑p ^ (k - 1) * ↑p ^ (-2 * s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s))

Finite products of the quadratic Euler factors converge to the coefficient L-series.

source
theorem HeckeRing.GL2.Eigenform.L_eulerProduct_tprod {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
∏' (p : Nat.Primes), (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹ = ModularForm.L hk f.toCuspForm s

The Euler product in Mathlib's ModularForm.L normalization. At level Γ₁(N) the width at infinity is one, so its Dirichlet series is the coefficient L-series above.

source
theorem HeckeRing.GL2.Eigenform.L_eulerProduct_hasProd {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
HasProd (fun (p : Nat.Primes) => (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹) (ModularForm.L hk f.toCuspForm s)

The quadratic Euler factors have product equal to Mathlib's ModularForm.L for a normalized full Hecke eigenform.

source
theorem HeckeRing.GL2.Eigenform.L_eulerProduct {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑p ^ (-s) + (MulChar.ofUnitHom f.χ) ↑p * ↑p ^ (k - 1) * ↑p ^ (-2 * s))⁻¹) Filter.atTop (nhds (ModularForm.L hk f.toCuspForm s))

Finite products of the quadratic Euler factors converge to Mathlib's ModularForm.L.

source
theorem HeckeRing.GL2.Newform.LSeries_eulerProduct_hasProd {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
HasProd (fun (p : Nat.Primes) => (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + f.dirichletLift ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹) (LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s)

The Euler factors of a newform have product equal to its coefficient L-series on Re s > k/2 + 1. The character is zero-extended at primes dividing the level.

source
theorem HeckeRing.GL2.Newform.LSeries_eulerProduct_tprod {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
∏' (p : Nat.Primes), (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + f.dirichletLift ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹ = LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s

The coefficient L-series of a newform equals its Euler product on Re s > k/2 + 1.

source
theorem HeckeRing.GL2.Newform.LSeries_eulerProduct {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑p ^ (-s) + f.dirichletLift ↑p * ↑p ^ (k - 1) * ↑p ^ (-2 * s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s))

Finite Euler products converge to the coefficient L-series of a newform.

source
theorem HeckeRing.GL2.Newform.L_eulerProduct_hasProd {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
HasProd (fun (p : Nat.Primes) => (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + f.dirichletLift ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹) (ModularForm.L hk f.toCuspForm s)

The Euler factors of a newform have product equal to Mathlib's ModularForm.L.

source
theorem HeckeRing.GL2.Newform.L_eulerProduct_tprod {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
∏' (p : Nat.Primes), (1 - (PowerSeries.coeff ↑p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑↑p ^ (-s) + f.dirichletLift ↑↑p * ↑↑p ^ (k - 1) * ↑↑p ^ (-2 * s))⁻¹ = ModularForm.L hk f.toCuspForm s

The L-function of a newform equals its Euler product on Re s > k/2 + 1.

source
theorem HeckeRing.GL2.Newform.L_eulerProduct {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑p ^ (-s) + f.dirichletLift ↑p * ↑p ^ (k - 1) * ↑p ^ (-2 * s))⁻¹) Filter.atTop (nhds (ModularForm.L hk f.toCuspForm s))

Finite Euler products converge to Mathlib's ModularForm.L for a newform.