The nonnegative quadratic convolution in Siegel's elementary argument

For a quadratic character χ, this file packages the coefficients of ζ(s) L(s, χ) as the real divisor sum

aχ(n) = ∑ d ∣ n, Re χ(d).

The coefficients are nonnegative, and every nonzero square contributes at least one. Consequently their summatory function is at least ⌊√X⌋. The last theorem combines this arithmetic lower bound with the explicit Pólya--Vinogradov harmonic tail. Its remaining discrepancy is kept as an explicit term; no unproved upper estimate for that term is assumed.

noncomputable def DirichletCharacter.quadraticSiegelConvolution {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : ℝ

The real coefficient of ζ(s) L(s, χ).

Equations

• χ.quadraticSiegelConvolution n = (χ.zetaMul n).re

theorem DirichletCharacter.quadraticSiegelConvolution_eq_divisorSum {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : χ.quadraticSiegelConvolution n = ∑ d ∈ n.divisors, (χ ↑d).re

The convolution coefficient is literally the real quadratic divisor sum.

theorem DirichletCharacter.zetaMul_im_eq_zero_of_sq_eq_one {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (n : ℕ) : (χ.zetaMul n).im = 0

The complex convolution coefficient lies on the real axis.

theorem DirichletCharacter.quadraticSiegelConvolution_nonneg {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (n : ℕ) : 0 ≤ χ.quadraticSiegelConvolution n

Quadratic convolution coefficients are nonnegative real numbers.

theorem DirichletCharacter.one_le_zetaMul_prime_even_pow {q : ℕ} {χ : DirichletCharacter ℂ q} (hquad : χ ^ 2 = 1) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : 1 ≤ χ.zetaMul (p ^ (2 * k))

At every even prime-power exponent the quadratic Euler coefficient is at least one.

theorem DirichletCharacter.one_le_quadraticSiegelConvolution_sq {q : ℕ} {χ : DirichletCharacter ℂ q} (hquad : χ ^ 2 = 1) {m : ℕ} (hm : m ≠ 0) : 1 ≤ χ.quadraticSiegelConvolution (m ^ 2)

Every nonzero square has quadratic convolution coefficient at least one.

noncomputable def DirichletCharacter.quadraticSiegelConvolutionSummatory {q : ℕ} (χ : DirichletCharacter ℂ q) (X : ℕ) : ℝ

The summatory quadratic convolution up to X.

Equations

• χ.quadraticSiegelConvolutionSummatory X = ∑ n ∈ Finset.Icc 1 X, χ.quadraticSiegelConvolution n

theorem DirichletCharacter.quadraticSiegelConvolutionSummatory_eq_divisorDoubleSum {q : ℕ} (χ : DirichletCharacter ℂ q) (X : ℕ) : χ.quadraticSiegelConvolutionSummatory X = ∑ n ∈ Finset.Icc 1 X, ∑ d ∈ n.divisors, (χ ↑d).re

Dirichlet-convolution / divisor-double-sum identity.

theorem DirichletCharacter.sqrt_le_quadraticSiegelConvolutionSummatory {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (X : ℕ) : ↑X.sqrt ≤ χ.quadraticSiegelConvolutionSummatory X

Siegel's square lower-bound chain: ⌊√X⌋ ≤ ∑_{1 ≤ n ≤ X} aχ(n).

noncomputable def DirichletCharacter.quadraticSiegelConvolutionDiscrepancy {q : ℕ} (χ : DirichletCharacter ℂ q) (X m : ℕ) : ℝ

The exact residual between the convolution summatory function and X times the finite harmonic truncation. Later hyperbola estimates should bound this quantity rather than postulate an unknown error bound.

Equations

• χ.quadraticSiegelConvolutionDiscrepancy X m = χ.quadraticSiegelConvolutionSummatory X - ↑X * χ.quadraticHarmonicTruncation m

theorem DirichletCharacter.quadraticSiegelConvolutionDiscrepancy_eq_divisorDoubleSum_sub {q : ℕ} (χ : DirichletCharacter ℂ q) (X m : ℕ) : χ.quadraticSiegelConvolutionDiscrepancy X m = ∑ n ∈ Finset.Icc 1 X, ∑ d ∈ n.divisors, (χ ↑d).re - ↑X * χ.quadraticHarmonicTruncation m

Expansion of the residual as the divisor double sum minus the harmonic main term.

theorem DirichletCharacter.sqrt_sub_convolutionDiscrepancy_sub_polyaVinogradovError_le {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hprimitive : χ.IsPrimitive) (hquad : χ ^ 2 = 1) (hnonprincipal : χ ≠ 1) (hq : 1 < q) (X : ℕ) {m : ℕ} (hm : 1 ≤ m) : ↑X.sqrt - χ.quadraticSiegelConvolutionDiscrepancy X m - ↑X * (8 * √↑q * (1 + Real.log ↑q) / ↑m) ≤ ↑X * (LFunction χ 1).re

The first load-bearing inequality in the elementary convolution route. The square lower bound and the explicit Pólya--Vinogradov tail force a lower bound for X * Re L(1,χ) up to the exact convolution discrepancy.