The genuine two-character convolution

This is a modern arithmetic proof of positivity for the coefficients of ζ(s) L(s, χ) L(s, ψ) L(s, χψ). Both characters have a common arbitrary modulus. No primitivity or coprimality of conductors is used.

The local argument regroups the four actual factors using a character twist of χ.zetaMul. The exceptional local case, where both character values are -1, is controlled by the alternating geometric sum. These are identities of the actual coefficients, not estimates by a positive majorant.

noncomputable def DirichletCharacter.twoCharacterConvolution {q : ℕ} (χ ψ : DirichletCharacter ℂ q) : ArithmeticFunction ℂ

The actual arithmetic convolution with Dirichlet series ζ(s) L(s, χ) L(s, ψ) L(s, χψ).

Equations

• χ.twoCharacterConvolution ψ = (χ.zetaMul * toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => (χ * ψ) ↑x

theorem DirichletCharacter.isMultiplicative_twoCharacterConvolution {q : ℕ} (χ ψ : DirichletCharacter ℂ q) : (χ.twoCharacterConvolution ψ).IsMultiplicative

Multiplicativity is inherited from the four genuine factors.

theorem DirichletCharacter.twoCharacterConvolution_one {q : ℕ} (χ ψ : DirichletCharacter ℂ q) : (χ.twoCharacterConvolution ψ) 1 = 1

Normalization of the fourfold convolution.

theorem DirichletCharacter.twoCharacterConvolution_comm {q : ℕ} (χ ψ : DirichletCharacter ℂ q) : χ.twoCharacterConvolution ψ = ψ.twoCharacterConvolution χ

Exchanging the two characters leaves the actual convolution unchanged.

theorem DirichletCharacter.character_mul_product_apply {q : ℕ} (χ ψ : DirichletCharacter ℂ q) (n : ℕ) : ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => (χ * ψ) ↑x) n = ψ ↑n * χ.zetaMul n

The convolution of ψ and χψ is the pointwise ψ-twist of ζ * χ.

theorem DirichletCharacter.twoCharacterConvolution_apply {q : ℕ} (χ ψ : DirichletCharacter ℂ q) (n : ℕ) : (χ.twoCharacterConvolution ψ) n = ∑ x ∈ n.divisorsAntidiagonal, χ.zetaMul x.1 * (ψ ↑x.2 * χ.zetaMul x.2)

An exact divisor-antidiagonal formula obtained by twisting one pair of factors.

theorem DirichletCharacter.twoCharacterConvolution_prime_pow_nonneg {q : ℕ} {χ ψ : DirichletCharacter ℂ q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : 0 ≤ (χ.twoCharacterConvolution ψ) (p ^ k)

Positivity at every prime power, by structural casework on the two local quadratic character values.

theorem DirichletCharacter.twoCharacterConvolution_nonneg {q : ℕ} {χ ψ : DirichletCharacter ℂ q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) (n : ℕ) : 0 ≤ (χ.twoCharacterConvolution ψ) n

Every coefficient is a nonnegative real number, expressed in the real-axis order on ℂ.

theorem DirichletCharacter.twoCharacterConvolution_im_eq_zero {q : ℕ} {χ ψ : DirichletCharacter ℂ q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) (n : ℕ) : ((χ.twoCharacterConvolution ψ) n).im = 0

The imaginary part vanishes; positivity is not merely a bound on the real part.

theorem DirichletCharacter.twoCharacterConvolution_re_nonneg {q : ℕ} {χ ψ : DirichletCharacter ℂ q} (hχ : χ ^ 2 = 1) (hψ : ψ ^ 2 = 1) (n : ℕ) : 0 ≤ ((χ.twoCharacterConvolution ψ) n).re

The real part of every coefficient is nonnegative.

theorem DirichletCharacter.characterArithmeticFunction_LSeriesSummable {q : ℕ} (χ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (⇑(toArithmeticFunction fun (x : ℕ) => χ ↑x)) s

theorem DirichletCharacter.LSeriesSummable_twoCharacterConvolution {q : ℕ} (χ ψ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (⇑(χ.twoCharacterConvolution ψ)) s

Absolute convergence of the genuine fourfold convolution on Re s > 1; quadraticity is not needed for convergence.

theorem DirichletCharacter.LSeries_twoCharacterConvolution {q : ℕ} (χ ψ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeries (⇑(χ.twoCharacterConvolution ψ)) s = riemannZeta s * LSeries (fun (n : ℕ) => χ ↑n) s * LSeries (fun (n : ℕ) => ψ ↑n) s * LSeries (fun (n : ℕ) => (χ * ψ) ↑n) s

The actual Dirichlet-series product identity, valid even at modulus zero. The character series here are the raw, absolutely convergent Dirichlet series.

theorem DirichletCharacter.LSeries_twoCharacterConvolution_eq_LFunction_product {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeries (⇑(χ.twoCharacterConvolution ψ)) s = riemannZeta s * LFunction χ s * LFunction ψ s * LFunction (χ * ψ) s

The analytic product of the Riemann zeta function and the three Dirichlet L-functions is represented by the genuine convolution on Re s > 1.

theorem DirichletCharacter.LSeriesHasSum_twoCharacterConvolution {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeriesHasSum (⇑(χ.twoCharacterConvolution ψ)) s (riemannZeta s * LFunction χ s * LFunction ψ s * LFunction (χ * ψ) s)

Absolute convergence and the actual analytic value, in one HasSum statement.