UniformResidue.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

From separated zeros and Hadamard's identity to a uniform residue comparison

This is the downstream argument in the manuscript's residue lemma. The zero coordinates, their separation, the baseline zero-sum bound, and Hadamard's identity are explicit hypotheses. Their number-field instances come from Stark (1974), Lemmas 3 and 8 and equation (9), together with the Euler product.

theorem OAI.DukePrimeDegree.residue_comparison_from_separated_zeros line 22

Source documentation

The constants in the residue comparison depend only on the uniform zero-separation, baseline sum, and gamma-factor bounds, not on L or h.

theorem residue_comparison_from_separated_zeros {ι : Type*}
    (F G : ℝ → ℝ) (X Y : ι → ℝ) (L c A B h : ℝ)
    (hL : 1 ≤ L) (hc : 0 < c) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hh : 0 < h) (hlen : h ≤ 4 / L)
    (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)))
    (hbaseline : (∑' i, (X i + 1) / ((X i + 1) ^ 2 + Y i ^ 2)) ≤ A)
    (hgamma : ∀ σ, 1 < σ → σ ≤ 1 + 4 / L → |G σ| ≤ B)
    (hhadamard : ∀ σ, 1 < σ → σ ≤ 1 + 4 / L →
      deriv (fun s => Real.log (F s)) σ =
        L * (∑' i, (X i + L * (σ - 1)) /
          ((X i + L * (σ - 1)) ^ 2 + Y i ^ 2)) - 1 / σ - L / 2 - G σ)
…