Finite high-convolution arithmetic for the quadratic Siegel amplifier

For a quadratic character χ, the arithmetic function χ.zetaMul is the coefficient sequence of ζ(s) L(s, χ). This file forms its genuine Dirichlet-convolution powers. It proves, without an analytic producer, that all coefficients are nonnegative and that every nonzero even perfect power has coefficient at least one at every positive convolution depth.

In particular, if the convolution depth r and an even exponent e are positive, the summatory function through M ^ e is at least M. Taking e = r (with even r) is the finite, scan-free X^(1/r) support layer of the classical high-power amplifier.

This arithmetic layer does not by itself improve the existing q^(-1/2)-scale one-fold estimate. To deduce the genuine large-conductor Siegel bound from this module, one still needs an analytic estimate of the following quantified strength for arbitrarily large even r:

S_r(X) ≤ C_r X (log X)^(r-1) L(1,χ)^r + E_r(q,X)

at a choice X = q ^ A_r, with E_r(q,X) ≤ (1/2) X^(1/r) and A_r * (r-1) / r^2 → 0 (constants may depend on r, hence ultimately on η). The currently formalized one-fold Pólya--Vinogradov discrepancy gives no such high-power remainder. We therefore expose no conclusion-shaped "source predicate" and make no claim of a large-q endpoint here.

noncomputable def DirichletCharacter.quadraticSiegelPowerCoefficient {q : ℕ} (χ : DirichletCharacter ℂ q) (r n : ℕ) : ℂ

The r-fold Dirichlet-convolution coefficient of ζ(s)L(s,χ).

Equations

• χ.quadraticSiegelPowerCoefficient r n = (χ.zetaMul ^ r) n

theorem DirichletCharacter.quadraticSiegelPowerCoefficient_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : χ.quadraticSiegelPowerCoefficient 0 n = if n = 1 then 1 else 0

The coefficient at depth zero is the convolution identity.

theorem DirichletCharacter.quadraticSiegelPowerCoefficient_succ {q : ℕ} (χ : DirichletCharacter ℂ q) (r n : ℕ) : χ.quadraticSiegelPowerCoefficient (r + 1) n = ∑ x ∈ n.divisorsAntidiagonal, χ.quadraticSiegelPowerCoefficient r x.1 * χ.zetaMul x.2

Exact antidiagonal recursion for the genuine convolution power.

theorem DirichletCharacter.quadraticSiegelPowerCoefficient_one {q : ℕ} (χ : DirichletCharacter ℂ q) (r : ℕ) : χ.quadraticSiegelPowerCoefficient r 1 = 1

Every convolution power is normalized to one at n = 1.

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

Quadraticity makes every coefficient of every convolution power nonnegative (in the real-axis order on ℂ).

theorem DirichletCharacter.zetaMul_le_quadraticSiegelPowerCoefficient_succ {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (r : ℕ) {n : ℕ} (hn : n ≠ 0) : χ.zetaMul n ≤ χ.quadraticSiegelPowerCoefficient (r + 1) n

At every positive depth the high convolution dominates the original coefficient, by retaining the antidiagonal cell (1,n).

theorem DirichletCharacter.one_le_quadraticSiegelPowerCoefficient_evenPow {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (r : ℕ) {m e : ℕ} (hm : m ≠ 0) (he : ∃ (t : ℕ), e = 2 * t) : 1 ≤ χ.quadraticSiegelPowerCoefficient (r + 1) (m ^ e)

Every nonzero even perfect power has high-convolution coefficient at least one. The exponent is quantified; no finite scan is involved.

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

The real summatory function of the r-fold quadratic amplifier.

Equations

• χ.quadraticSiegelPowerSummatory r X = ∑ n ∈ Finset.Icc 1 X, (χ.quadraticSiegelPowerCoefficient r n).re

theorem DirichletCharacter.quadraticSiegelPowerCoefficient_re_nonneg {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (r n : ℕ) : 0 ≤ (χ.quadraticSiegelPowerCoefficient r n).re

All summands of the real high-convolution summatory function are nonnegative.

theorem DirichletCharacter.le_quadraticSiegelPowerSummatory_pow {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (r : ℕ) {e : ℕ} (hepos : 0 < e) (heven : ∃ (t : ℕ), e = 2 * t) (M : ℕ) : ↑M ≤ χ.quadraticSiegelPowerSummatory (r + 1) (M ^ e)

Perfect-power support lower bound. At positive convolution depth and any positive even exponent e, the sum through M^e is at least M.

theorem DirichletCharacter.le_quadraticSiegelPowerSummatory_selfPow {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) {r : ℕ} (hrpos : 0 < r) (hreven : ∃ (t : ℕ), r = 2 * t) (M : ℕ) : ↑M ≤ χ.quadraticSiegelPowerSummatory r (M ^ r)

The requested scan-free X^(1/r) specialization: at even positive depth r, the summatory function through the perfect r-th power M^r is at least M.