Euler products with quadratic local factors

Let a : ℕ → ℂ be multiplicative on coprime arguments with a 1 = 1, and suppose that along the powers of every prime p its values obey the second-order recurrence

a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - c p * a (p ^ r).

Wherever the L-series of a converges absolutely, it is then the Euler product

L(a, s) = ∏_p (1 - a p * p ^ (-s) + c p * p ^ (-2 s))⁻¹.

At each prime, the quadratic factor times the sum of the prime-power terms is 1. Thus each factor is nonzero, and its inverse is the local contribution to the Euler product.

This is the shape of the L-function of a normalized Hecke eigenform, where c p = χ(p) p^(k-1) (Diamond–Shurman, Theorem 5.9.2), and it covers the completely multiplicative case c = 0.

Main results

• TauCeti.LSeries.localFactor_mul_tsum_term_prime_pow_eq_one_of_recurrence: the factor identity.
• TauCeti.LSeries.tsum_term_prime_pow_eq_inv_of_recurrence: the prime-power sum is the inverse factor.
• TauCeti.LSeries.localFactor_ne_zero_of_recurrence: each quadratic factor is nonzero.
• TauCeti.LSeries.LSeries_eulerProduct_hasProd_of_recurrence: the Euler product, as a HasProd.
• TauCeti.LSeries.LSeries_eulerProduct_tprod_of_recurrence: the same, as an equality with ∏'.
• TauCeti.LSeries.LSeries_eulerProduct_of_recurrence: the same, as convergence of the finite partial products over Nat.primesBelow n.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.9.

theorem TauCeti.LSeries.term_pow {a : ℕ → ℂ} {s : ℂ} (p : ℕ) (hp : p ≠ 0) (e : ℕ) : LSeries.term a s (p ^ e) = a (p ^ e) * (↑p ^ (-s)) ^ e

An L-series term at a power of a nonzero index, written as a coefficient times a power of the index's Dirichlet weight.

theorem TauCeti.LSeries.localFactor_mul_tsum_term_prime_pow_eq_one_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (p : Nat.Primes) (hrec : ∀ (r : ℕ), a (↑p ^ (r + 2)) = a ↑p * a (↑p ^ (r + 1)) - c ↑p * a (↑p ^ r)) (hs : Summable fun (e : ℕ) => LSeries.term a s (↑p ^ e)) : (1 - a ↑p * ↑↑p ^ (-s) + c ↑p * ↑↑p ^ (-2 * s)) * ∑' (e : ℕ), LSeries.term a s (↑p ^ e) = 1

The quadratic factor times the sum over powers of a prime is 1 whenever the prime-power coefficients satisfy the second-order recurrence.

theorem TauCeti.LSeries.tsum_term_prime_pow_eq_inv_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (p : Nat.Primes) (hrec : ∀ (r : ℕ), a (↑p ^ (r + 2)) = a ↑p * a (↑p ^ (r + 1)) - c ↑p * a (↑p ^ r)) (hs : Summable fun (e : ℕ) => LSeries.term a s (↑p ^ e)) : ∑' (e : ℕ), LSeries.term a s (↑p ^ e) = (1 - a ↑p * ↑↑p ^ (-s) + c ↑p * ↑↑p ^ (-2 * s))⁻¹

The sum over powers of a prime is the inverse quadratic Euler factor.

theorem TauCeti.LSeries.localFactor_ne_zero_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (p : Nat.Primes) (hrec : ∀ (r : ℕ), a (↑p ^ (r + 2)) = a ↑p * a (↑p ^ (r + 1)) - c ↑p * a (↑p ^ r)) (hs : Summable fun (e : ℕ) => LSeries.term a s (↑p ^ e)) : 1 - a ↑p * ↑↑p ^ (-s) + c ↑p * ↑↑p ^ (-2 * s) ≠ 0

Each quadratic Euler factor is nonzero when its prime-power series converges.

theorem TauCeti.LSeries.term_mul_of_coprime {a : ℕ → ℂ} {s : ℂ} (hmul : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → a (m * n) = a m * a n) {m n : ℕ} (hmn : m.Coprime n) : LSeries.term a s (m * n) = LSeries.term a s m * LSeries.term a s n

The L-series terms of a coefficient sequence multiplicative on nonzero coprime arguments are themselves multiplicative on coprime arguments.

theorem TauCeti.LSeries.LSeries_eulerProduct_hasProd_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (hmul : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → a (m * n) = a m * a n) (hrec : ∀ (p : ℕ), Nat.Prime p → ∀ (r : ℕ), a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - c p * a (p ^ r)) (hs : LSeriesSummable a s) : HasProd (fun (p : Nat.Primes) => (1 - a ↑p * ↑↑p ^ (-s) + c ↑p * ↑↑p ^ (-2 * s))⁻¹) (LSeries a s)

The Euler product with quadratic local factors. Let a : ℕ → ℂ satisfy a 1 = 1, be multiplicative on nonzero coprime arguments, and obey the recurrence a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - c p * a (p ^ r) along the powers of every prime p. Where its L-series converges absolutely,

∏_p (1 - a p * p ^ (-s) + c p * p ^ (-2 s))⁻¹ = L(a, s).

theorem TauCeti.LSeries.LSeries_eulerProduct_tprod_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (hmul : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → a (m * n) = a m * a n) (hrec : ∀ (p : ℕ), Nat.Prime p → ∀ (r : ℕ), a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - c p * a (p ^ r)) (hs : LSeriesSummable a s) : ∏' (p : Nat.Primes), (1 - a ↑p * ↑↑p ^ (-s) + c ↑p * ↑↑p ^ (-2 * s))⁻¹ = LSeries a s

The Euler product with quadratic local factors, as an equality with ∏': under the hypotheses of TauCeti.LSeries.LSeries_eulerProduct_hasProd_of_recurrence, ∏' p, (1 - a p * p ^ (-s) + c p * p ^ (-2 s))⁻¹ = L(a, s).

theorem TauCeti.LSeries.LSeries_eulerProduct_of_recurrence {a c : ℕ → ℂ} {s : ℂ} (h₁ : a 1 = 1) (hmul : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → a (m * n) = a m * a n) (hrec : ∀ (p : ℕ), Nat.Prime p → ∀ (r : ℕ), a (p ^ (r + 2)) = a p * a (p ^ (r + 1)) - c p * a (p ^ r)) (hs : LSeriesSummable a s) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - a p * ↑p ^ (-s) + c p * ↑p ^ (-2 * s))⁻¹) Filter.atTop (nhds (LSeries a s))

The Euler product with quadratic local factors, as convergence of the finite partial products: under the hypotheses of TauCeti.LSeries.LSeries_eulerProduct_hasProd_of_recurrence, ∏_{p < n} (1 - a p * p ^ (-s) + c p * p ^ (-2 s))⁻¹ → L(a, s) as n → ∞.