The abstract analytic world of the quasi-Riemann hypothesis
DefinitionQRH_worldThe reduction from the key mean-square estimate to the zero-free half-plane Re s > 11/12, packaged as an abstract interface. A world consists of four types with their data: a type of finite-order Hecke characters, each with its L-function rendered as a total complex-valued function and a pole predicate whose only possible pole is the trivial character at s = 1, the pole of the zeta function; a type of rows u, parametrizing the sextic-twisted sum family A_u(D) together with the untwisted sum A_1(D), with the row ranges, the good rows p^6 — the sixth powers of primary primes in a norm range — with a weakened form of Landau's prime ideal theorem as the row-count lower bound (at least a constant times Y^(1-delta) good rows at every scale Y), the sextic-twist comparison bounding the difference between A_{p^6}(D) and A_1(D) by a constant times D/Y, and the key mean-square estimate of Proposition 2.1: for every 0 < theta <= 1/10 and epsilon > 0 the mean square of the family over rows of height at most D^(1+theta) is at most a constant times D^(2+theta+epsilon), carried as an interface hypothesis; a type of smooth test weights, with their Mellin transforms, the Mellin integral of the untwisted sum, the existence for every point of the half-plane of a weight whose Mellin transform does not vanish there, and the conditional Mellin identity asserting that a power saving for (nu, W) implies L(s, nu) M_W(s) = Mellin(W)(s) throughout the half-plane away from poles — this packages termwise integration for Re s > 1, Hecke's meromorphic continuation, and the identity theorem; and the Dirichlet side: the trivial Dirichlet character, the nontrivial quadratic character modulo 3, the twist involution, the Dirichlet L-functions with their pole data, the quadratic base change attaching to every Dirichlet character the Hecke character chi o N with its factorization into the two Dirichlet L-functions times Euler factors that are nonzero in the half-plane, and Dirichlet's nonvanishing theorem at s = 1 for the quadratic character modulo 3. The deep unformalized inputs — Poisson summation over the Eisenstein integers, the Gauss-Jacobi identities, Patterson's cubic theta coefficients, the theta transformation, the quadratic large sieve, and the recursive transfer and descent — enter only through these fields; every field asserting an estimate or an identity is a hypothesis of every statement built on the world. The module also defines the power saving property of the untwisted sum: A_1(D) is O(D^(11/12 + epsilon)) for every epsilon > 0.
import Mathlib
/-!
# The Quasi-Riemann Hypothesis: the abstract analytic world
An abstract interface for the source's reduction from the key mean-square
estimate for sextic-twisted Mobius sums to the zero-free half-plane
Re s > 11/12 for finite-order Hecke L-functions over K = Q(sqrt(-3)), and
onward, by quadratic base change, to every Dirichlet L-function, including
the Riemann zeta function.
The interface carries the characters with their L-functions and a pole
predicate, the rows with the twisted sum family and the key estimate of
Proposition 2.1 (rendered as an interface hypothesis), the test weights
with their Mellin transforms and the conditional Mellin identity that
packages termwise integration and the identity theorem, and the
Dirichlet-side data with the base-change factorization and Dirichlet's
nonvanishing theorem. The deep unformalized inputs of the source -- Poisson
summation, cubic theta transformation, the quadratic large sieve, and the
recursive descent -- are carried as interface hypotheses.
-/
namespace QRH
/-- The abstract world of the quasi-Riemann hypothesis: characters with
their L-functions, rows with the sextic-twisted sum family, test weights
with Mellin transforms, and Dirichlet characters with the quadratic base
change. Every field asserting an estimate or an identity is a hypothesis
of every statement built on the world. -/
structure World where
/-- the finite-order Hecke characters of the source -/
Char : Type
/-- the rows u: elements of K, parametrizing the twisted sum family -/
U : Type
/-- the smooth compactly supported test weights -/
Test : Type
/-- the Dirichlet characters of the base change -/
DirCh : Type
/-- the rows of height at most r -/
rowsBelow : ℝ → Finset U
/-- the row ranges are increasing -/
rowsBelow_mono : ∀ (r s : ℝ), r ≤ s → rowsBelow r ⊆ rowsBelow s
/-- the good rows p^6: sixth powers of primary primes with norm in
(Y/2, Y] -/
goodRows : ℝ → Finset U
/-- every good row at scale Y has height at most Y^6 -/
goodRows_sub : ∀ Y : ℝ, 1 ≤ Y → goodRows Y ⊆ rowsBelow (Y ^ 6)
/-- Landau's prime ideal theorem, weakened: for every delta > 0 there
is c > 0 with at least c * Y^(1-delta) good rows at every scale Y >= 1 -/
goodCount : ∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧
∀ Y : ℝ, 1 ≤ Y → c * Y ^ (1 - δ) ≤ ((goodRows Y).card : ℝ)
/-- the twisted sum family A_u(D) of the source -/
A : Char → Test → U → ℝ → ℂ
/-- the untwisted sum A_1(D) -/
A1 : Char → Test → ℝ → ℂ
/-- the sextic-twist comparison: a good row p^6 at scale Y satisfies
|A_{p^6}(D) - A_1(D)| <= C * D / Y -/
approx : ∀ (ν : Char) (W : Test), ∃ C : ℝ, 0 < C ∧
∀ (D Y : ℝ) (u : U), 2 ≤ D → 1 ≤ Y → u ∈ goodRows Y →
‖A1 ν W D - A ν W u D‖ ≤ C * D / Y
/-- the key mean-square estimate (Proposition 2.1 of the source): for
every 0 < theta <= 1/10 and epsilon > 0 there is C > 0 such that the
mean square of the family over rows of height at most D^(1+theta) is
at most C * D^(2+theta+epsilon) -/
key : ∀ (ν : Char) (W : Test) (θ ε : ℝ), 0 < θ → θ ≤ 1 / 10 → 0 < ε →
∃ C : ℝ, 0 < C ∧ ∀ D : ℝ, 2 ≤ D →
∑ u ∈ rowsBelow (D ^ (1 + θ)), (‖A ν W u D‖) ^ 2 ≤
C * D ^ (2 + θ + ε)
/-- the L-function of a character, as a total function -/
L : Char → ℂ → ℂ
/-- the pole predicate for L -/
isPole : Char → ℂ → Prop
/-- the trivial character -/
trivChar : Char
/-- the only possible pole in the plane: the trivial character at 1 --
the pole of the zeta function, which is not a zero -/
pole_only : ∀ (ν : Char) (s : ℂ), isPole ν s → ν = trivChar ∧ s = 1
/-- the Mellin transform of a test weight -/
mellin : Test → ℂ → ℂ
/-- the Mellin integral of the untwisted sum -/
Mfun : Char → Test → ℂ → ℂ
/-- for every rho in the half-plane there is a test weight whose
Mellin transform does not vanish at rho -/
mellin_nonzero : ∀ ρ : ℂ, 11 / 12 < ρ.re → ∃ W : Test, mellin W ρ ≠ 0
/-- the Mellin identity, conditional on the power saving for (nu, W):
L(s, nu) * M_W(s) = Mellin(W)(s) throughout the half-plane away from
poles; this packages termwise integration for Re s > 1, the meromorphic
continuation, and the identity theorem -/
mellin_identity : ∀ (ν : Char) (W : Test),
(∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∀ D : ℝ, 2 ≤ D →
‖A1 ν W D‖ ≤ C * D ^ (11 / 12 + ε)) →
∀ s : ℂ, 11 / 12 < s.re → ¬isPole ν s →
L ν s * Mfun ν W s = mellin W s
/-- the trivial Dirichlet character -/
trivD : DirCh
/-- the nontrivial quadratic character modulo 3 -/
chi_m3 : DirCh
/-- the twist chi -> chi * chi_{-3} -/
twist : DirCh → DirCh
/-- twisting twice is the identity -/
twist_twist : ∀ χ : DirCh, twist (twist χ) = χ
/-- the twist of the trivial character is the quadratic character -/
twist_triv : twist trivD = chi_m3
/-- the quadratic character modulo 3 is nontrivial -/
chi_m3_nontriv : chi_m3 ≠ trivD
/-- the Dirichlet L-functions, as total functions -/
Ldir : DirCh → ℂ → ℂ
/-- the pole predicate for the Dirichlet side -/
isPoleD : DirCh → ℂ → Prop
/-- the only possible pole on the Dirichlet side: the trivial character
at 1 -- the pole of the zeta function -/
poleD_only : ∀ (χ : DirCh) (s : ℂ), isPoleD χ s → χ = trivD ∧ s = 1
/-- the trivial character has a pole at 1 -/
poleD_triv : isPoleD trivD 1
/-- a pole is not a zero: at a pole the total rendering carries a
designated nonzero value -/
poleD_not_zero : ∀ (χ : DirCh) (s : ℂ), isPoleD χ s → Ldir χ s ≠ 0
/-- the quadratic base change chi -> chi o N -/
bc : DirCh → Char
/-- the base change of the trivial character is trivial -/
bc_triv : bc trivD = trivChar
/-- only the trivial character has trivial base change -/
bc_nontriv_iff : ∀ χ : DirCh, bc χ = trivChar ↔ χ = trivD
/-- the Euler factors of the base change, nonzero in the half-plane -/
ef : DirCh → ℂ → ℂ
ef_nonzero : ∀ (χ : DirCh) (s : ℂ), 11 / 12 < s.re → ef χ s ≠ 0
/-- the base-change factorization: away from poles of the two Dirichlet
factors, L_K(s, chi o N) equals L(s, chi) * L(s, chi chi_{-3}) up to the
nonzero Euler factors -/
base_change : ∀ (χ : DirCh) (s : ℂ), 11 / 12 < s.re →
¬isPoleD χ s → ¬isPoleD (twist χ) s →
L (bc χ) s = Ldir χ s * Ldir (twist χ) s * ef χ s
/-- Dirichlet's nonvanishing theorem for the quadratic character
modulo 3 -/
dirichlet_nonvanishing : Ldir chi_m3 1 ≠ 0
/-- The power saving for the untwisted sum (display (2.5) of the source):
A_1(D) is O(D^(11/12 + epsilon)) for every epsilon > 0. -/
def PowerSaving (F : World) (ν : F.Char) (W : F.Test) : Prop :=
∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∀ D : ℝ, 2 ≤ D →
‖F.A1 ν W D‖ ≤ C * D ^ (11 / 12 + ε)
end QRH