Completed Zeta Center Log Bound

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.norm_finsum_div_sub_le_finsum_div {D : ℂ → ℤ} (hfin : (Function.support D).Finite) (hD : ∀ (u : ℂ), 0 ≤ D u) {z : ℂ} {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ u ∈ Function.support D, δ ≤ ‖z - u‖) : ‖∑ᶠ (u : ℂ), ↑(D u) / (z - u)‖ ≤ ↑(∑ᶠ (u : ℂ), D u) / δ

noncomputable def NumberField.Odlyzko.canonicalZeroFactor (R : ℝ) (u : ℂ) : ℂ → ℂ

A canonical zero factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.canonicalZeroFactor R u z = (Complex.canonicalFactor R u z)⁻¹

theorem NumberField.Odlyzko.norm_canonicalZeroFactor_eq_one {R : ℝ} {u z : ℂ} (hu : u ∈ Metric.ball 0 R) (hz : z ∈ Metric.sphere 0 R) : ‖canonicalZeroFactor R u z‖ = 1

theorem NumberField.Odlyzko.canonicalZeroFactor_eq_zero_iff {R : ℝ} {u z : ℂ} (hu : u ∈ Metric.ball 0 R) (hz : z ∈ Metric.ball 0 R) : canonicalZeroFactor R u z = 0 ↔ z = u

theorem NumberField.Odlyzko.canonicalZeroFactor_apply (R : ℝ) (u z : ℂ) : canonicalZeroFactor R u z = (z - u) * ↑R / (-(starRingEnd ℂ) u * z + ↑R ^ 2)

theorem NumberField.Odlyzko.logDeriv_canonicalZeroFactor {R : ℝ} {u z : ℂ} (hR : R ≠ 0) (hzu : z ≠ u) (hreflect : ↑R ^ 2 - (starRingEnd ℂ) u * z ≠ 0) : logDeriv (canonicalZeroFactor R u) z = 1 / (z - u) + (starRingEnd ℂ) u / (↑R ^ 2 - (starRingEnd ℂ) u * z)

noncomputable def NumberField.Odlyzko.centeredCanonicalZeroFactor (c : ℂ) (R : ℝ) (u : ℂ) : ℂ → ℂ

A centered canonical zero factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredCanonicalZeroFactor c R u z = NumberField.Odlyzko.canonicalZeroFactor R (u - c) (z - c)

theorem NumberField.Odlyzko.norm_centeredCanonicalZeroFactor_eq_one {c u z : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.sphere c R) : ‖centeredCanonicalZeroFactor c R u z‖ = 1

theorem NumberField.Odlyzko.centeredCanonicalZeroFactor_eq_zero_iff {c u z : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.ball c R) : centeredCanonicalZeroFactor c R u z = 0 ↔ z = u

theorem NumberField.Odlyzko.canonicalReflectedDenominator_ne_zero_on_closedBall {c u z : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c R) : ↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c) ≠ 0

theorem NumberField.Odlyzko.analyticOnNhd_centeredCanonicalZeroFactor {c u : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) : AnalyticOnNhd ℂ (centeredCanonicalZeroFactor c R u) (Metric.closedBall c R)

theorem NumberField.Odlyzko.differentiableAt_centeredCanonicalZeroFactor {c u z : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.ball c R) (hzu : z ≠ u) : DifferentiableAt ℂ (centeredCanonicalZeroFactor c R u) z

theorem NumberField.Odlyzko.canonicalReflectedDenominator_ne_zero {c u z : ℂ} {R : ℝ} (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.ball c R) (hzu : z ≠ u) : ↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c) ≠ 0

theorem NumberField.Odlyzko.logDeriv_centeredCanonicalZeroFactor {c u z : ℂ} {R : ℝ} (hR : R ≠ 0) (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.ball c R) (hzu : z ≠ u) (hreflect : ↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c) ≠ 0) : logDeriv (centeredCanonicalZeroFactor c R u) z = 1 / (z - u) + (starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c))

theorem NumberField.Odlyzko.norm_conj_div_reflected_centered_le {c u z : ℂ} {r R : ℝ} (hR : 0 < R) (_hr : 0 ≤ r) (hrR : r < R) (hu : u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c r) : ‖(starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c))‖ ≤ 1 / (R - r)

theorem NumberField.Odlyzko.norm_finprod_centeredCanonicalZeroFactor_zpow_eq_one {c : ℂ} {R : ℝ} (D : ℂ → ℤ) (hfin : (Function.support D).Finite) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) {z : ℂ} (hz : z ∈ Metric.sphere c R) : ‖(∏ᶠ (u : ℂ), centeredCanonicalZeroFactor c R u ^ D u) z‖ = 1

theorem NumberField.Odlyzko.norm_finsum_reflected_centered_le {D : ℂ → ℤ} (hfin : (Function.support D).Finite) (hD : ∀ (u : ℂ), 0 ≤ D u) {c z : ℂ} {r R : ℝ} (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c r) : ‖∑ᶠ (u : ℂ), ↑(D u) * ((starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c)))‖ ≤ ↑(∑ᶠ (u : ℂ), D u) / (R - r)

theorem NumberField.Odlyzko.norm_finsum_canonicalLogDeriv_le {D : ℂ → ℤ} (hfin : (Function.support D).Finite) (hD : ∀ (u : ℂ), 0 ≤ D u) {c z : ℂ} {δ r R : ℝ} (hδ : 0 < δ) (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c r) (hsep : ∀ u ∈ Function.support D, δ ≤ ‖z - u‖) : ‖∑ᶠ (u : ℂ), ↑(D u) * (1 / (z - u) + (starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c)))‖ ≤ ↑(∑ᶠ (u : ℂ), D u) / δ + ↑(∑ᶠ (u : ℂ), D u) / (R - r)

theorem NumberField.Odlyzko.norm_finsum_canonicalLogDeriv_le_of_finsum_le {D : ℂ → ℤ} (hfin : (Function.support D).Finite) (hD : ∀ (u : ℂ), 0 ≤ D u) {c z : ℂ} {δ r R B : ℝ} (hδ : 0 < δ) (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c r) (hsep : ∀ u ∈ Function.support D, δ ≤ ‖z - u‖) (hmass : ↑(∑ᶠ (u : ℂ), D u) ≤ B) : ‖∑ᶠ (u : ℂ), ↑(D u) * (1 / (z - u) + (starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c)))‖ ≤ B / δ + B / (R - r)

noncomputable def NumberField.Odlyzko.centeredCanonicalZeroProduct (c : ℂ) (R : ℝ) (D : ℂ → ℤ) : ℂ → ℂ

A centered canonical zero product used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredCanonicalZeroProduct c R D = ∏ᶠ (u : ℂ), NumberField.Odlyzko.centeredCanonicalZeroFactor c R u ^ D u

theorem NumberField.Odlyzko.analyticOnNhd_centeredCanonicalZeroProduct {D : ℂ → ℤ} (hD : ∀ (u : ℂ), 0 ≤ D u) {c : ℂ} {R : ℝ} (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) : AnalyticOnNhd ℂ (centeredCanonicalZeroProduct c R D) (Metric.closedBall c R)

theorem NumberField.Odlyzko.norm_centeredCanonicalZeroProduct_eq_one {D : ℂ → ℤ} (hfin : (Function.support D).Finite) {c z : ℂ} {R : ℝ} (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.sphere c R) : ‖centeredCanonicalZeroProduct c R D z‖ = 1

theorem NumberField.Odlyzko.norm_centeredCanonicalZeroProduct_le_one {D : ℂ → ℤ} (hfin : (Function.support D).Finite) (hD : ∀ (u : ℂ), 0 ≤ D u) {c z : ℂ} {R : ℝ} (hR : 0 < R) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.closedBall c R) : ‖centeredCanonicalZeroProduct c R D z‖ ≤ 1

theorem NumberField.Odlyzko.logDeriv_centeredCanonicalZeroProduct {D : ℂ → ℤ} (hfin : (Function.support D).Finite) {c z : ℂ} {R : ℝ} (hR : 0 < R) (hinside : ∀ u ∈ Function.support D, u ∈ Metric.ball c R) (hz : z ∈ Metric.ball c R) (hzD : z ∉ Function.support D) : logDeriv (centeredCanonicalZeroProduct c R D) z = ∑ᶠ (u : ℂ), ↑(D u) * (1 / (z - u) + (starRingEnd ℂ) (u - c) / (↑R ^ 2 - (starRingEnd ℂ) (u - c) * (z - c)))

theorem NumberField.Odlyzko.divisor_eq_zero_of_analyticOnNhd_of_ne_zero {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) (hne : ∀ z ∈ U, f z ≠ 0) : MeromorphicOn.divisor f U = 0

theorem NumberField.Odlyzko.divisor_ball_support_subset {f : ℂ → ℂ} {c : ℂ} {R : ℝ} : (MeromorphicOn.divisor f (Metric.ball c R)).support ⊆ Metric.ball c R

theorem NumberField.Odlyzko.divisor_ball_eq_divisor_closedBall_of_boundary_ne {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hboundary : ∀ z ∈ Metric.sphere c R, f z ≠ 0) (z : ℂ) : (MeromorphicOn.divisor f (Metric.ball c R)) z = (MeromorphicOn.divisor f (Metric.closedBall c R)) z

theorem NumberField.Odlyzko.AnalyticOnNhd.exists_canonicalZeroFactor_on_ball_zero {f : ℂ → ℂ} {R : ℝ} (hR : 0 < R) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) (hc : f 0 ≠ 0) (hboundary : ∀ z ∈ Metric.sphere 0 R, f z ≠ 0) : ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g (Metric.closedBall 0 R) ∧ (∀ z ∈ Metric.closedBall 0 R, g z ≠ 0) ∧ Set.EqOn f (centeredCanonicalZeroProduct 0 R ⇑(MeromorphicOn.divisor f (Metric.ball 0 R)) * g) (Metric.closedBall 0 R) ∧ (∀ z ∈ Metric.sphere 0 R, ‖g z‖ = ‖f z‖) ∧ ‖f 0‖ ≤ ‖g 0‖

theorem NumberField.Odlyzko.AnalyticOnNhd.exists_zeroFree_sphere {f : ℂ → ℂ} {c : ℂ} {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c b)) (hc : f c ≠ 0) : ∃ R ∈ Set.Ioo a b, ∀ z ∈ Metric.sphere c R, f z ≠ 0

theorem NumberField.Odlyzko.card_le_finsum_of_subset_support_of_nonneg {α : Type u_1} (D : α → ℤ) (hfin : (Function.support D).Finite) (S : Finset α) (hS : ↑S ⊆ Function.support D) (hD : ∀ (x : α), 0 ≤ D x) : ↑S.card ≤ ↑(∑ᶠ (x : α), D x)

theorem NumberField.Odlyzko.AnalyticOnNhd.card_zeros_le {c : ℂ} {r R M : ℝ} {f : ℂ → ℂ} (hr : 0 < |r|) (hrR : |r| < |R|) (hM : 1 ≤ M) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c |R|)) (hc : f c ≠ 0) (f_bound : ∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ M) (S : Finset ℂ) (hSsupport : ∀ z ∈ S, z ∈ Function.support ⇑(MeromorphicOn.divisor f (Metric.closedBall c |r|))) : ↑S.card ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

theorem NumberField.Odlyzko.mem_divisor_closedBall_of_mem_completedZetaZeroDivisor_support (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {c z : ℂ} {r : ℝ} (hzball : z ∈ Metric.closedBall c |r|) (hz : z ∈ (completedDedekindZetaZeroDivisor K).support) : z ∈ Function.support ⇑(MeromorphicOn.divisor (poleClearedCompletedDedekindZetaContinuation K) (Metric.closedBall c |r|))

theorem NumberField.Odlyzko.card_completedDedekindZetaZerosInClosedRectangle_le_jensen (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {a b u v : ℝ} {c : ℂ} {r R M : ℝ} (hr : 0 < |r|) (hrR : |r| < |R|) (hM : 1 ≤ M) (hc : poleClearedCompletedDedekindZetaContinuation K c ≠ 0) (f_bound : ∀ z ∈ Metric.sphere c |R|, ‖poleClearedCompletedDedekindZetaContinuation K z‖ ≤ M) (hrect : Set.Icc a b ×ℂ Set.Icc u v ⊆ Metric.closedBall c |r|) : ↑(completedDedekindZetaZerosInClosedRectangle K a b u v).card ≤ Real.log (M / ‖poleClearedCompletedDedekindZetaContinuation K c‖) / Real.log (R / r)

noncomputable def NumberField.Odlyzko.completedZetaMovingCircleBound (K : Type u_1) [Field K] [NumberField K] (R t : ℝ) : ℝ

A completed zeta moving circle bound used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaMovingCircleBound K R t = max 1 (NumberField.Odlyzko.poleClearedCompletedDedekindZetaVerticalBound K (2 - |R|) (2 + |R|) * (1 + |t| + |R|) ^ 2)

theorem NumberField.Odlyzko.one_le_completedZetaMovingCircleBound (K : Type u_1) [Field K] [NumberField K] (R t : ℝ) : 1 ≤ completedZetaMovingCircleBound K R t

theorem NumberField.Odlyzko.norm_poleClearedCompletedZeta_le_movingCircleBound (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (R t : ℝ) {z : ℂ} (hz : z ∈ Metric.sphere (2 + ↑t * Complex.I) |R|) : ‖poleClearedCompletedDedekindZetaContinuation K z‖ ≤ completedZetaMovingCircleBound K R t

theorem NumberField.Odlyzko.card_completedDedekindZetaZerosInClosedRectangle_le_movingJensen (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {a b u v r R t : ℝ} (hr : 0 < |r|) (hrR : |r| < |R|) (hc : poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I) ≠ 0) (hrect : Set.Icc a b ×ℂ Set.Icc u v ⊆ Metric.closedBall (2 + ↑t * Complex.I) |r|) : ↑(completedDedekindZetaZerosInClosedRectangle K a b u v).card ≤ Real.log (completedZetaMovingCircleBound K R t / ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖) / Real.log (R / r)

theorem NumberField.Odlyzko.norm_le_on_closedBall_of_norm_le_on_sphere {f : ℂ → ℂ} {c : ℂ} {R M : ℝ} (hR : 0 < R) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hbound : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall c R) : ‖f z‖ ≤ M

theorem NumberField.Odlyzko.norm_deriv_le_of_re_le_on_ball {F : ℂ → ℂ} {R r A : ℝ} (hR : 0 < R) (_hr : 0 ≤ r) (hrR : r < R) (hA : 0 < A) (hF : DifferentiableOn ℂ F (Metric.ball 0 R)) (hFre : ∀ z ∈ Metric.ball 0 R, (F z).re ≤ A) (hF0 : F 0 = 0) {w : ℂ} (hw : w ∈ Metric.closedBall 0 r) : ‖deriv F w‖ ≤ 4 * A * (R + r) / (R - r) ^ 2

theorem NumberField.Odlyzko.AnalyticOnNhd.exists_analyticLog_on_ball {g : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hg : AnalyticOnNhd ℂ g (Metric.ball c R)) (hgn : ∀ z ∈ Metric.ball c R, g z ≠ 0) : ∃ (L : ℂ → ℂ), L c = Complex.log (g c) ∧ (∀ z ∈ Metric.ball c R, HasDerivAt L (logDeriv g z) z) ∧ ∀ z ∈ Metric.ball c R, Complex.exp (L z) = g z

theorem NumberField.Odlyzko.norm_logDeriv_le_of_zeroFree_on_ball {g : ℂ → ℂ} {c z : ℂ} {R r M A : ℝ} (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hM : 0 < M) (hA : 0 < A) (hg : AnalyticOnNhd ℂ g (Metric.ball c R)) (hgn : ∀ w ∈ Metric.ball c R, g w ≠ 0) (hbound : ∀ w ∈ Metric.ball c R, ‖g w‖ ≤ M) (hcenter : Real.log M - Real.log ‖g c‖ ≤ A) (hz : z ∈ Metric.closedBall c r) : ‖logDeriv g z‖ ≤ 4 * A * (R + r) / (R - r) ^ 2

theorem NumberField.Odlyzko.norm_logDeriv_le_of_canonical_factorization {f : ℂ → ℂ} {z : ℂ} {r R δ M A B : ℝ} (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hδ : 0 < δ) (hM : 0 < M) (hA : 0 < A) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) (hc : f 0 ≠ 0) (hboundary : ∀ w ∈ Metric.sphere 0 R, f w ≠ 0) (hbound : ∀ w ∈ Metric.sphere 0 R, ‖f w‖ ≤ M) (hcenter : Real.log M - Real.log ‖f 0‖ ≤ A) (hz : z ∈ Metric.closedBall 0 r) (hfz : f z ≠ 0) (hsep : ∀ u ∈ (MeromorphicOn.divisor f (Metric.ball 0 R)).support, δ ≤ ‖z - u‖) (hmass : ↑(∑ᶠ (u : ℂ), (MeromorphicOn.divisor f (Metric.ball 0 R)) u) ≤ B) : ‖logDeriv f z‖ ≤ B / δ + B / (R - r) + 4 * A * (R + r) / (R - r) ^ 2

theorem NumberField.Odlyzko.norm_logDeriv_le_of_canonical_factorization_centered {f : ℂ → ℂ} {c z : ℂ} {r R δ M A B : ℝ} (hR : 0 < R) (hr : 0 ≤ r) (hrR : r < R) (hδ : 0 < δ) (hM : 0 < M) (hA : 0 < A) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hc : f c ≠ 0) (hboundary : ∀ w ∈ Metric.sphere c R, f w ≠ 0) (hbound : ∀ w ∈ Metric.sphere c R, ‖f w‖ ≤ M) (hcenter : Real.log M - Real.log ‖f c‖ ≤ A) (hz : z ∈ Metric.closedBall c r) (hfz : f z ≠ 0) (hsep : ∀ u ∈ (MeromorphicOn.divisor (fun (w : ℂ) => f (c + w)) (Metric.ball 0 R)).support, δ ≤ ‖z - c - u‖) (hmass : ↑(∑ᶠ (u : ℂ), (MeromorphicOn.divisor (fun (w : ℂ) => f (c + w)) (Metric.ball 0 R)) u) ≤ B) : ‖logDeriv f z‖ ≤ B / δ + B / (R - r) + 4 * A * (R + r) / (R - r) ^ 2

theorem NumberField.Odlyzko.AnalyticOnNhd.eq_zero_of_mem_divisor_support {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hf : AnalyticOnNhd ℂ f U) (hz : z ∈ (MeromorphicOn.divisor f U).support) : f z = 0

theorem NumberField.Odlyzko.AnalyticOnNhd.sum_divisor_ball_le {f : ℂ → ℂ} {c : ℂ} {r R M : ℝ} (hr : 0 < r) (hrR : r < R) (hM : 1 ≤ M) (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hc : f c ≠ 0) (hboundary : ∀ z ∈ Metric.sphere c r, f z ≠ 0) (f_bound : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ M) : ↑(∑ᶠ (z : ℂ), (MeromorphicOn.divisor f (Metric.ball c r)) z) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

noncomputable def NumberField.Odlyzko.completedZetaCanonicalJensenCoefficient : ℝ

A completed zeta canonical jensen coefficient used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaCanonicalJensenCoefficient = 1 / Real.log (6 / 5)

theorem NumberField.Odlyzko.completedZetaCanonicalJensenCoefficient_pos : 0 < completedZetaCanonicalJensenCoefficient

theorem NumberField.Odlyzko.norm_logDeriv_poleClearedCompletedZeta_le_of_local_separation (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {t δ A : ℝ} (hδ : 0 < δ) (hA : 0 < A) (hcenter : Real.log (completedZetaMovingCircleBound K 6 t) - Real.log ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖ ≤ A) {z : ℂ} (hz : z ∈ Metric.closedBall (2 + ↑t * Complex.I) 3) (hfz : poleClearedCompletedDedekindZetaContinuation K z ≠ 0) (hsep : ∀ p ∈ Metric.ball (2 + ↑t * Complex.I) 5, poleClearedCompletedDedekindZetaContinuation K p = 0 → δ ≤ ‖z - p‖) : ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) z‖ ≤ A * completedZetaCanonicalJensenCoefficient / δ + A * completedZetaCanonicalJensenCoefficient + 32 * A

noncomputable def NumberField.Odlyzko.completedZetaRadiusSixVerticalCoefficient (K : Type u_1) [Field K] [NumberField K] : ℝ

A completed zeta radius six vertical coefficient used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaRadiusSixVerticalCoefficient K = max 1 (NumberField.Odlyzko.poleClearedCompletedDedekindZetaVerticalBound K (-4) 8)

noncomputable def NumberField.Odlyzko.completedZetaCenterLogLinearExpression (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : ℝ

A completed zeta center log linear expression used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NumberField.Odlyzko.completedZetaCenterLogLinearBound (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : ℝ

A completed zeta center log linear bound used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaCenterLogLinearBound K t = max 1 (NumberField.Odlyzko.completedZetaCenterLogLinearExpression K t)

theorem NumberField.Odlyzko.one_le_completedZetaCenterLogLinearBound (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : 1 ≤ completedZetaCenterLogLinearBound K t

theorem NumberField.Odlyzko.neg_log_norm_poleClearedCompletedZeta_two_add_mul_I_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {t : ℝ} (ht : 1 ≤ |t|) : -Real.log ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖ ≤ Real.log (dedekindZetaInverseVerticalMajorant K) - ↑(InfinitePlace.nrComplexPlaces K) / 2 * Real.log complexPlaceGammaVerticalLowerConstant + ↑(InfinitePlace.nrComplexPlaces K) / 2 * Real.pi * |t|

theorem NumberField.Odlyzko.log_completedZetaMovingCircleBound_six_le (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : Real.log (completedZetaMovingCircleBound K 6 t) ≤ completedZetaRadiusSixVerticalCoefficient K + 2 * (7 + |t|)

theorem NumberField.Odlyzko.completedZeta_center_log_gap_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {t : ℝ} (ht : 1 ≤ |t|) : Real.log (completedZetaMovingCircleBound K 6 t) - Real.log ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖ ≤ completedZetaCenterLogLinearBound K t