ZeroSum.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the separated-zero comparison

The rescaled zero coordinates in the manuscript are Xρ = L (1 - Re ρ) and Yρ = L Im ρ. A uniform zero-free disk gives c² ≤ Xρ² + Yρ². Summing the elementary pointwise comparison controls the real Hadamard sum throughout the discriminant-scaled interval.

theorem OAI.DukePrimeDegree.zero_sum_comparison line 19

Source documentation

Control the whole zero sum at every 0 < U ≤ 4 by its value at U = 1. Convergence at U = 1 implies convergence throughout this range.

theorem zero_sum_comparison {ι : Type*}
    (X Y : ι → ℝ) (c U : ℝ) (hc : 0 < c) (hU : 0 < U) (hU4 : U ≤ 4)
    (hX : ∀ i, 0 ≤ X i) (hgap : ∀ i, c ^ 2 ≤ X i ^ 2 + Y i ^ 2)
    (hsum : Summable (fun i => (X i + 1) / ((X i + 1) ^ 2 + Y i ^ 2))) :
    Summable (fun i => (X i + U) / ((X i + U) ^ 2 + Y i ^ 2)) ∧
      (∑' i, (X i + U) / ((X i + U) ^ 2 + Y i ^ 2)) ≤
        (8 + 8 / c ^ 2) * ∑' i, (X i + 1) / ((X i + 1) ^ 2 + Y i ^ 2) := by
…