is a Dirichlet series with nonnegative coefficients and (Davenport §21)
ProvedDavenport.zeta_LFunction_prod_LSeries_nonnegThe Dirichlet series of (Davenport §21). Let and be real (quadratic) Dirichlet characters modulo and respectively, and let denote their product, a character modulo (both characters lifted to the modulus ). Then there are real numbers with such that
the series converging absolutely for .
The coefficients are (Dirichlet convolution); is multiplicative, and at a prime power its value is the coefficient of in , which is nonnegative because (equivalently, has nonnegative coefficients). This is the function of Davenport §21 and the function of the second case of the proof of Siegel's theorem in Montgomery–Vaughan; the nonnegativity of its coefficients is what Estermann's lemma requires.
Formalization Note. Neither character is required to be primitive or non-principal; is formed as the product of the two characters after changing both levels to (Mathlib's changeLevel), so its value at is for every integer .
import Mathlib.NumberTheory.LSeries.DirichletContinuation import Mathlib.NumberTheory.LSeries.Nonvanishing import Mathlib.NumberTheory.LSeries.Positivity import Mathlib.NumberTheory.LSeries.Convolution import Mathlib.NumberTheory.DirichletCharacter.Basic import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.Pow.Complex import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.Exp open Finset DirichletCharacter
namespace Davenport
theorem zeta_LFunction_prod_LSeries_nonneg (q₁ q₂ : ℕ) [NeZero q₁] [NeZero q₂]
(χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂)
(h₁ : χ₁.IsQuadratic) (h₂ : χ₂.IsQuadratic) :
∃ a : ℕ → ℝ, a 1 = 1 ∧ (∀ n, 0 ≤ a n) ∧
(∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (a n : ℂ)) s) ∧
∀ s : ℂ, 1 < s.re →
riemannZeta s * DirichletCharacter.LFunction χ₁ s * DirichletCharacter.LFunction χ₂ s *
DirichletCharacter.LFunction
(changeLevel (Nat.dvd_mul_right q₁ q₂) χ₁ * changeLevel (Nat.dvd_mul_left q₂ q₁) χ₂) s
= LSeries (fun n => (a n : ℂ)) s := by sorry
end Davenport