Hadamard Summability Bridge

This file builds the clean bridge from Hadamard order-≤ 1 hypotheses for riemannXi to the genus-one summability statements used by the Li-criterion development.

noncomputable def LiCriterion.xiZeroSet : Hadamard.ZeroSet riemannXi

The nontrivial zeros of ζ viewed as a Hadamard.ZeroSet for riemannXi.

Equations

• LiCriterion.xiZeroSet = { Zero := LiCriterion.NontrivialZero, z := fun (ρ : LiCriterion.NontrivialZero) => ↑ρ, isZero := LiCriterion.xiZeroSet._proof_1 }

theorem LiCriterion.xi_weighted_genus_one_of_hadamard_order_one (hfinite : Hadamard.hasFiniteOrder riemannXi) (horder : Hadamard.order riemannXi ≤ 1) : Summable fun (ρ : NontrivialZero) => ↑(analyticOrderNatAt riemannXi ↑ρ) / ‖↑ρ‖ ^ 2

Genus-1 summability from the order-≤ 1 Hadamard hypotheses for riemannXi.

This is the clean replacement path for the old zero-counting bridge: use the multiplicity-aware Hadamard summability theorem and then compare termwise with the unweighted series, noting that every zero has multiplicity at least 1.

theorem LiCriterion.xi_genus_one_of_hadamard_order_one (hfinite : Hadamard.hasFiniteOrder riemannXi) (horder : Hadamard.order riemannXi ≤ 1) : Summable fun (ρ : NontrivialZero) => 1 / ‖↑ρ‖ ^ 2