Completed Zeta Rectangle

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.analyticOnNhd_poleClearedCompletedDedekindZetaContinuation (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : AnalyticOnNhd ℂ (poleClearedCompletedDedekindZetaContinuation K) Set.univ

theorem NumberField.Odlyzko.meromorphicOrderAt_poleClearedCompletedDedekindZetaContinuation_ne_top (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : meromorphicOrderAt (poleClearedCompletedDedekindZetaContinuation K) s ≠ ⊤

theorem NumberField.Odlyzko.meromorphicOrderAt_poleClearedCompletedDedekindZetaContinuation_nonneg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : 0 ≤ meromorphicOrderAt (poleClearedCompletedDedekindZetaContinuation K) s

noncomputable def NumberField.Odlyzko.completedDedekindZetaZeroDivisor (K : Type u_1) [Field K] [NumberField K] : Function.locallyFinsuppWithin Set.univ ℤ

A completed dedekind zeta zero divisor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedDedekindZetaZeroDivisor K = MeromorphicOn.divisor (NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation K) Set.univ

theorem NumberField.Odlyzko.completedDedekindZetaZeroDivisor_support_inter_compact_finite (K : Type u_1) [Field K] [NumberField K] {S : Set ℂ} (hS : IsCompact S) : (S ∩ (completedDedekindZetaZeroDivisor K).support).Finite

theorem NumberField.Odlyzko.mem_completedDedekindZetaZeroDivisor_support_of_eq_zero (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {z : ℂ} (hz : poleClearedCompletedDedekindZetaContinuation K z = 0) : z ∈ (completedDedekindZetaZeroDivisor K).support

theorem NumberField.Odlyzko.meromorphicOrderAt_poleClearedCompletedDedekindZetaContinuation_eq_divisor (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (z : ℂ) : meromorphicOrderAt (poleClearedCompletedDedekindZetaContinuation K) z = ↑((completedDedekindZetaZeroDivisor K) z)

noncomputable def NumberField.Odlyzko.completedDedekindZetaZerosInClosedRectangle (K : Type u_1) [Field K] [NumberField K] (a b u v : ℝ) : Finset ℂ

A completed dedekind zeta zeros in closed rectangle used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedDedekindZetaZerosInClosedRectangle K a b u v = ⋯.toFinset

theorem NumberField.Odlyzko.mem_completedDedekindZetaZerosInClosedRectangle_iff (K : Type u_1) [Field K] [NumberField K] {a b u v : ℝ} {z : ℂ} : z ∈ completedDedekindZetaZerosInClosedRectangle K a b u v ↔ z ∈ Set.Icc a b ×ℂ Set.Icc u v ∧ z ∈ (completedDedekindZetaZeroDivisor K).support

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation_eq_zero_of_mem_support (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {z : ℂ} (hz : z ∈ (completedDedekindZetaZeroDivisor K).support) : poleClearedCompletedDedekindZetaContinuation K z = 0

theorem NumberField.Odlyzko.rectangleIntegral_mul_logDeriv_poleClearedCompletedDedekindZetaContinuation (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {h : ℂ → ℂ} {a b u v : ℝ} (hab : a ≤ b) (huv : u ≤ v) (hh : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ h z) (hboundary : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, z.re = a ∨ z.re = b ∨ z.im = u ∨ z.im = v → poleClearedCompletedDedekindZetaContinuation K z ≠ 0) : rectangleIntegral (fun (z : ℂ) => h z * logDeriv (poleClearedCompletedDedekindZetaContinuation K) z) (↑a + ↑u * Complex.I) (↑b + ↑v * Complex.I) = 2 * ↑Real.pi * Complex.I * ∑ p ∈ completedDedekindZetaZerosInClosedRectangle K a b u v, h p * ↑((completedDedekindZetaZeroDivisor K) p)