StarkZeros.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform residues from completed-zeta zero separation

The completed zeta function, its functional equation and its convergent real Hadamard sum give the uniform residue estimate from a uniform zero gap. Uniqueness of a near-one zero reduces this gap to real-zero exclusion.

lemma OAI.DukePrimeDegree.realZeroPole_le_of_scaled_gap line 26

Source documentation

Comparison of the actual multiplicity-weighted zero terms.

lemma realZeroPole_le_of_scaled_gap {f : ℂ → ℂ}
    (hf : Differentiable ℂ f) (hzero : f 0 ≠ 0)
    (hstrip : ∀ z, f z = 0 → z.re ≤ 1)
    {L c h : ℝ} (hL : 0 < L) (hc : 0 < c) (hh : 0 < h) (hh4 : h ≤ 4 / L)
    (hgap : ∀ z, f z = 0 →
      c ^ 2 ≤ (L * (1 - z.re)) ^ 2 + (L * z.im) ^ 2) (z : ℂ) :
    realZeroPole f (1 + h) z ≤
      (4 * (1 + 3 / c) ^ 2) * realZeroPole f (1 + 1 / L) z := by
…

theorem OAI.DukePrimeDegree.logRegularized_deriv_bound_of_completedXi_gap line 51

Source documentation

The analytic estimate uses the proved completed-zeta Hadamard sum, with no zero-sum or summability hypothesis.

theorem logRegularized_deriv_bound_of_completedXi_gap
    {d : ℕ} {K : Type*} [Field K] [NumberField K] [NumberField.IsTotallyReal K]
    (σ : OrderedEmbeddings (d + 1) K) (hn : Module.finrank ℚ K = d + 1)
    {c B L : ℝ} (hc : 0 < c) (hB : 0 < B)
    (hL : L = Real.log |(NumberField.discr K : ℝ)|) (hL4 : 4 ≤ L)
    (harch : ∀ s ∈ Icc (1 : ℝ) 2, |archimedeanZetaTerm (d + 1) s| ≤ B)
    (hgap : ∀ z, completedThetaXi σ hn z = 0 →
      c ^ 2 ≤ (L * (1 - z.re)) ^ 2 + (L * z.im) ^ 2) :
    ∀ h ∈ Ioc (0 : ℝ) (4 / L),
      |deriv (logRegularizedDedekindZeta K) h| ≤
        (4 * (1 + 3 / c) ^ 2 * (3 + B) + B + 2) * L := by
…

def OAI.DukePrimeDegree.CompletedXiGap line 111
Source documentation
Uniform separation of completed-zeta zeros on the discriminant scale.
```
def CompletedXiGap (d : ℕ) : Prop :=
…
```
def OAI.DukePrimeDegree.ExceptionalRealZeroExclusion line 122
Source documentation
The real exceptional-zero assertion in Stark's Lemma 8, after excluding quadratic subfields.
```
def ExceptionalRealZeroExclusion (d : ℕ) : Prop :=
…
```
theorem OAI.DukePrimeDegree.completedXiGap_of_exceptionalRealZeroExclusion line 132
Source documentation
Uniqueness of a near-one zero reduces complex zero separation to real-zero exclusion.
```
theorem completedXiGap_of_exceptionalRealZeroExclusion (d : ℕ)
    (H : ExceptionalRealZeroExclusion.{u} d) : CompletedXiGap.{u} d := by
…
```
theorem OAI.DukePrimeDegree.uniformZetaScaleBound_of_completedXiGap line 180
Source documentation
The completed-zeta zero gap gives the uniform zeta scale bound.
```
theorem uniformZetaScaleBound_of_completedXiGap (d : ℕ)
    (H : CompletedXiGap.{u} d) : UniformZetaScaleBound.{u} (d + 1) := by
…
```