The two-character Rankin layer in Tatuzawa's argument

For quadratic characters χ₁ and χ₂ (possibly of different moduli), this module forms the genuine Dirichlet-convolution coefficient sequence

(ζ * χ₁) * (ζ * χ₂).

Its coefficients are nonnegative, every nonzero square has coefficient at least one, and in Re s > 1 its L-series factors exactly as

(ζ(s)L(s,χ₁)) (ζ(s)L(s,χ₂)).

Consequently the square support gives a source-free lower bound for the product |L(σ,χ₁)L(σ,χ₂)|. This is the two-character positivity/Rankin bearing layer used before any Deuring--Heilbronn transfer to s = 1. It deliberately does not postulate that missing transfer as a source.

noncomputable def DirichletCharacter.tatuzawaPairCoefficient {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) : ArithmeticFunction ℂ

The biquadratic Rankin coefficient sequence (ζ * χ₁) * (ζ * χ₂).

Equations

• χ₁.tatuzawaPairCoefficient χ₂ = χ₁.zetaMul * χ₂.zetaMul

theorem DirichletCharacter.tatuzawaPairCoefficient_nonneg {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (n : ℕ) : 0 ≤ (χ₁.tatuzawaPairCoefficient χ₂) n

Quadraticity makes every coefficient of the two-character product nonnegative in the real-axis order on ℂ.

theorem DirichletCharacter.one_le_tatuzawaPairCoefficient_sq {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) {m : ℕ} (hm : m ≠ 0) : 1 ≤ (χ₁.tatuzawaPairCoefficient χ₂) (m ^ 2)

Every nonzero square occurs with coefficient at least one. The proof retains the antidiagonal cell (m²,1) and uses the square lower bound in the first quadratic factor.

theorem DirichletCharacter.tatuzawaPairCoefficient_summable {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (⇑(χ₁.tatuzawaPairCoefficient χ₂)) s

Absolute convergence of the two-character Rankin series in Re s > 1.

theorem DirichletCharacter.tatuzawaPairCoefficient_factorization {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) [NeZero q₁] [NeZero q₂] {s : ℂ} (hs : 1 < s.re) : LSeries (⇑(χ₁.tatuzawaPairCoefficient χ₂)) s = riemannZeta s * LFunction χ₁ s * (riemannZeta s * LFunction χ₂ s)

Exact two-character factorization in the half-plane of absolute convergence.

theorem DirichletCharacter.tatuzawaPair_term_re_eq {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) {σ : ℝ} {n : ℕ} (hn : n ≠ 0) : (LSeries.term (⇑(χ₁.tatuzawaPairCoefficient χ₂)) (↑σ) n).re = ((χ₁.tatuzawaPairCoefficient χ₂) n).re / ↑n ^ σ

theorem DirichletCharacter.tatuzawaPair_term_re_nonneg {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) {σ : ℝ} (n : ℕ) : 0 ≤ (LSeries.term (⇑(χ₁.tatuzawaPairCoefficient χ₂)) (↑σ) n).re

theorem DirichletCharacter.tatuzawaPair_square_lower {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) [NeZero q₁] [NeZero q₂] (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (M : ℕ) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ 2) ^ σ ≤ (LSeries ⇑(χ₁.tatuzawaPairCoefficient χ₂) ↑σ).re

The finite square-support Rankin lower bound for the genuine pair coefficient.

theorem DirichletCharacter.tatuzawaPair_square_le_zeta_sq_mul_valueProduct {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) [NeZero q₁] [NeZero q₂] (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (M : ℕ) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ 2) ^ σ ≤ ‖riemannZeta ↑σ‖ ^ 2 * (‖LFunction χ₁ ↑σ‖ * ‖LFunction χ₂ ↑σ‖)

The load-bearing two-character value-product inequality in σ > 1. It is unconditional and contains the exact zeta-pole loss that a subsequent Deuring--Heilbronn argument must overcome when transferring to s = 1.

theorem DirichletCharacter.tatuzawaPair_square_le_zetaMajorant_sq_mul_valueProduct {q₁ q₂ : ℕ} (χ₁ : DirichletCharacter ℂ q₁) (χ₂ : DirichletCharacter ℂ q₂) [NeZero q₁] [NeZero q₂] (h₁ : χ₁ ^ 2 = 1) (h₂ : χ₂ ^ 2 = 1) (M : ℕ) {σ : ℝ} (hσ : 1 < σ) : ↑M / ↑(M ^ 2) ^ σ ≤ (1 + 1 / (σ - 1)) ^ 2 * (‖LFunction χ₁ ↑σ‖ * ‖LFunction χ₂ ↑σ‖)

The same pair lower bound after paying the elementary zeta-pole majorant. The right side now displays precisely the (σ-1)⁻² loss which a genuine Deuring--Heilbronn/value-transfer step must beat.