Regularized Poitou Contour Limit

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.verticalSegmentIntegral_one_sub_of_antiInvariant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hf : ∀ (z : ℂ), f (1 - z) = -f z) (b T : ℝ) : verticalSegmentIntegral f (1 - b) (-T) T = -verticalSegmentIntegral f b (-T) T

theorem NumberField.Odlyzko.rectangleIntegral_eq_horizontal_sub_add_two_vertical_of_antiInvariant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hf : ∀ (z : ℂ), f (1 - z) = -f z) (b T : ℝ) : rectangleIntegral f (↑(1 - b) + -↑T * Complex.I) (↑b + ↑T * Complex.I) = horizontalIntegral f (1 - b) b (-T) - horizontalIntegral f (1 - b) b T + 2 • verticalSegmentIntegral f b (-T) T

theorem NumberField.Odlyzko.mul_antiInvariant_of_invariant_of_antiInvariant {h g : ℂ → ℂ} (hh : ∀ (z : ℂ), h (1 - z) = h z) (hg : ∀ (z : ℂ), g (1 - z) = -g z) (z : ℂ) : h (1 - z) * g (1 - z) = -(h z * g z)

noncomputable def NumberField.Odlyzko.fermiDiracKernel (x : ℝ) : ℝ

A fermi dirac kernel used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fermiDiracKernel x = 1 / (Real.exp x + 1)

noncomputable def NumberField.Odlyzko.inverseGaussKernel (f : ℝ → ℝ) (x : ℝ) : ℝ

An inverse gauss kernel used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.inverseGaussKernel f x = (Real.exp (-x) - 2 * f x / (Real.exp x + 1)) / (1 - Real.exp (-x))

theorem NumberField.Odlyzko.inverseGaussKernel_eq {f : ℝ → ℝ} {x : ℝ} (hx : 0 < x) : inverseGaussKernel f x = (1 - f x) / Real.sinh x - fermiDiracKernel x

theorem NumberField.Odlyzko.integrableOn_fermiDiracKernel_Ioi : MeasureTheory.IntegrableOn fermiDiracKernel (Set.Ioi 0) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_fermiDiracKernel : ∫ (x : ℝ) in Set.Ioi 0, fermiDiracKernel x = Real.log 2

theorem NumberField.Odlyzko.exp_sub_poitouKernel_mul_exp_neg_half_div_eq_inverseGaussKernel (f : ℝ → ℝ) {x : ℝ} (_hx : 0 < x) : (Real.exp (-x) - poitouKernel f x * Real.exp (-x / 2)) / (1 - Real.exp (-x)) = inverseGaussKernel f x

theorem NumberField.Odlyzko.exp_sub_regularizedPoitouKernel_mul_exp_neg_half_div (y δ : ℝ) {x : ℝ} (hx : 0 < x) : (Real.exp (-x) - poitouKernel (regularizedScaledTartar y δ) x * Real.exp (-x / 2)) / (1 - Real.exp (-x)) = inverseGaussKernel (regularizedScaledTartar y δ) x

theorem NumberField.Odlyzko.norm_gaussDigammaIntegrand_vertical_le (σ t : ℝ) {x : ℝ} (hx : 0 < x) : ‖gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x‖ ≤ (Real.exp (-x) + Real.exp (-σ * x)) / (1 - Real.exp (-x))

theorem NumberField.Odlyzko.integrable_poitouTransform_regularized_mul_cexp_neg {δ : ℝ} (hδ : 0 < δ) (y σ x : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * Complex.exp (-(↑σ + ↑t * Complex.I) * ↑x)) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_gaussDigammaIntegrand {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) {x : ℝ} (hx : 0 < x) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x = ↑(2 * Real.pi * inverseGaussKernel (regularizedScaledTartar y δ) x)

theorem NumberField.Odlyzko.regularizedScaledTartar_integrable {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 ≤ δ) : MeasureTheory.Integrable (regularizedScaledTartar y δ) MeasureTheory.volume

theorem NumberField.Odlyzko.poitouTransformIntegrand_regularizedScaledTartar_eq (y δ : ℝ) (s : ℂ) (x : ℝ) : poitouTransformIntegrand (regularizedScaledTartar y δ) s x = ↑(Real.exp (-δ * x ^ 2)) * poitouTransformIntegrand (scaledTartarTestFunction y) s x

theorem NumberField.Odlyzko.norm_poitouTransformIntegrand_regularized_le_scaled {y δ : ℝ} (hδ : 0 ≤ δ) (s : ℂ) (x : ℝ) : ‖poitouTransformIntegrand (regularizedScaledTartar y δ) s x‖ ≤ ‖poitouTransformIntegrand (scaledTartarTestFunction y) s x‖

theorem NumberField.Odlyzko.tendsto_poitouTransform_regularizedScaledTartar_nhdsGT_zero {y : ℝ} (hy : y ≠ 0) {s : ℂ} (hs : s.re ∈ Set.Icc 0 1) : Filter.Tendsto (fun (δ : ℝ) => poitouTransform (regularizedScaledTartar y δ) s) (nhdsWithin 0 (Set.Ioi 0)) (nhds (poitouTransform (scaledTartarTestFunction y) s))

noncomputable def NumberField.Odlyzko.completedZetaPoleFactor (s : ℂ) : ℂ

A completed zeta pole factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaPoleFactor s = s * (s - 1)

noncomputable def NumberField.Odlyzko.completedZetaPoleLogDeriv (s : ℂ) : ℂ

A completed zeta pole log deriv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaPoleLogDeriv s = 1 / s + 1 / (s - 1)

theorem NumberField.Odlyzko.completedZetaPoleLogDeriv_one_sub (s : ℂ) : completedZetaPoleLogDeriv (1 - s) = -completedZetaPoleLogDeriv s

theorem NumberField.Odlyzko.meromorphicOrderAt_completedZetaPoleFactor_zero : meromorphicOrderAt completedZetaPoleFactor 0 = 1

theorem NumberField.Odlyzko.meromorphicOrderAt_completedZetaPoleFactor_one : meromorphicOrderAt completedZetaPoleFactor 1 = 1

theorem NumberField.Odlyzko.logDeriv_completedZetaPoleFactor_eq {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1) : logDeriv completedZetaPoleFactor s = completedZetaPoleLogDeriv s

theorem NumberField.Odlyzko.rectangleIntegral_mul_completedZetaPoleLogDeriv {h : ℂ → ℂ} {a b u v : ℝ} (ha : a < 0) (hb : 1 < b) (hu : u < 0) (hv : 0 < v) (hh : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ h z) : rectangleIntegral (fun (s : ℂ) => h s * completedZetaPoleLogDeriv s) (↑a + ↑u * Complex.I) (↑b + ↑v * Complex.I) = 2 * ↑Real.pi * Complex.I * (h 0 + h 1)

def NumberField.Odlyzko.poitouCriticalStrip : Set ℂ

A poitou critical strip used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouCriticalStrip = Complex.re ⁻¹' Set.Ioo 0 1

def NumberField.Odlyzko.poitouClosedCriticalStrip : Set ℂ

A poitou closed critical strip used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouClosedCriticalStrip = Complex.re ⁻¹' Set.Icc 0 1

theorem NumberField.Odlyzko.rectangleBorderIntegrable_of_continuousAt_boundary {E : Type u} [NormedAddCommGroup E] {f : ℂ → E} {a b u v : ℝ} (hab : a ≤ b) (huv : u ≤ v) (hf : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, z.re = a ∨ z.re = b ∨ z.im = u ∨ z.im = v → ContinuousAt f z) : RectangleBorderIntegrable f (↑a + ↑u * Complex.I) (↑b + ↑v * Complex.I)

theorem NumberField.Odlyzko.rectangleIntegral_sub {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {z w : ℂ} (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : rectangleIntegral (fun (s : ℂ) => f s - g s) z w = rectangleIntegral f z w - rectangleIntegral g z w

theorem NumberField.Odlyzko.scaledTartarTestFunction_eq_integral_weightConvolution_cos (y x : ℝ) : scaledTartarTestFunction y x = 9 / 16 * ∫ (v : ℝ), tartarWeightConvolution v * Real.cos (v * y * x)

theorem NumberField.Odlyzko.integral_exp_neg_mul_sq_mul_cos_nonneg {δ : ℝ} (hδ : 0 < δ) (a : ℝ) : 0 ≤ ∫ (x : ℝ), Real.exp (-δ * x ^ 2) * Real.cos (a * x)

theorem NumberField.Odlyzko.cosineTransform_regularizedScaledTartar_nonneg {δ : ℝ} (hδ : 0 < δ) (y t : ℝ) : 0 ≤ Poitou.cosineTransform (regularizedScaledTartar y δ) t

theorem NumberField.Odlyzko.regularizedScaledTartar_poitouAdmissible {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) : Poitou.Admissible (regularizedScaledTartar y δ)

noncomputable def NumberField.Odlyzko.regularizedPoitouCriticalStripMajorant (δ x : ℝ) : ℝ

A regularized poitou critical strip majorant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.regularizedPoitouCriticalStripMajorant δ x = Real.exp ((1 / 2) ^ 2 / (2 * δ)) * Real.exp (-(δ / 2) * x ^ 2)

theorem NumberField.Odlyzko.norm_poitouTransformIntegrand_regularized_le_criticalStripMajorant {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {s : ℂ} (hs : s ∈ poitouClosedCriticalStrip) (x : ℝ) : ‖poitouTransformIntegrand (regularizedScaledTartar y δ) s x‖ ≤ regularizedPoitouCriticalStripMajorant δ x

theorem NumberField.Odlyzko.norm_poitouTransform_regularized_le_criticalStripIntegral {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {s : ℂ} (hs : s ∈ poitouClosedCriticalStrip) : ‖poitouTransform (regularizedScaledTartar y δ) s‖ ≤ ∫ (x : ℝ), regularizedPoitouCriticalStripMajorant δ x

theorem NumberField.Odlyzko.diffContOnCl_poitouTransform_regularized {δ : ℝ} (hδ : 0 < δ) (y : ℝ) : DiffContOnCl ℂ (poitouTransform (regularizedScaledTartar y δ)) poitouCriticalStrip

noncomputable def NumberField.Odlyzko.negativeExpRegularizedPoitouTransform (y δ : ℝ) (s : ℂ) : ℂ

A negative exp regularized poitou transform used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.negativeExpRegularizedPoitouTransform y δ s = Complex.exp (-NumberField.Odlyzko.poitouTransform (NumberField.Odlyzko.regularizedScaledTartar y δ) s)

theorem NumberField.Odlyzko.diffContOnCl_negativeExpRegularizedPoitouTransform {δ : ℝ} (hδ : 0 < δ) (y : ℝ) : DiffContOnCl ℂ (negativeExpRegularizedPoitouTransform y δ) poitouCriticalStrip

theorem NumberField.Odlyzko.norm_negativeExpRegularizedPoitouTransform_le {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {s : ℂ} (hs : s ∈ poitouClosedCriticalStrip) : ‖negativeExpRegularizedPoitouTransform y δ s‖ ≤ Real.exp (∫ (x : ℝ), regularizedPoitouCriticalStripMajorant δ x)

theorem NumberField.Odlyzko.negativeExpRegularizedPoitouTransform_growth {δ : ℝ} (hδ : 0 < δ) (y : ℝ) : ∃ c < Real.pi / (1 - 0), ∃ (B : ℝ), negativeExpRegularizedPoitouTransform y δ =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo 0 1)] fun (z : ℂ) => Real.exp (B * Real.exp (c * |z.im|))

theorem NumberField.Odlyzko.norm_negativeExpRegularizedPoitouTransform_le_one_of_re_zero {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) {s : ℂ} (hs : s.re = 0) : ‖negativeExpRegularizedPoitouTransform y δ s‖ ≤ 1

theorem NumberField.Odlyzko.norm_negativeExpRegularizedPoitouTransform_le_one_of_re_one {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) {s : ℂ} (hs : s.re = 1) : ‖negativeExpRegularizedPoitouTransform y δ s‖ ≤ 1

theorem NumberField.Odlyzko.re_poitouTransform_regularizedScaledTartar_nonneg {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) {s : ℂ} (hs : s ∈ poitouClosedCriticalStrip) : 0 ≤ (poitouTransform (regularizedScaledTartar y δ) s).re

theorem NumberField.Odlyzko.completedDedekindZetaZeroDivisor_support_re_mem_Icc (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : s ∈ (completedDedekindZetaZeroDivisor K).support) : s.re ∈ Set.Icc 0 1

theorem NumberField.Odlyzko.re_sum_mul_completedDedekindZetaZeroDivisor_nonneg_of_re_nonneg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (Φ : ℂ → ℂ) {S : Finset ℂ} (hΦ : ∀ s ∈ S, 0 ≤ (Φ s).re) : 0 ≤ (∑ s ∈ S, Φ s * ↑((completedDedekindZetaZeroDivisor K) s)).re

theorem NumberField.Odlyzko.re_poitouTransform_regularized_nonneg_of_completedZetaZero (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) {s : ℂ} (hs : s ∈ (completedDedekindZetaZeroDivisor K).support) : 0 ≤ (poitouTransform (regularizedScaledTartar y δ) s).re

theorem NumberField.Odlyzko.re_sum_poitouTransform_regularized_mul_completedZetaZeroDivisor_nonneg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) {S : Finset ℂ} (hS : ∀ s ∈ S, s ∈ (completedDedekindZetaZeroDivisor K).support) : 0 ≤ (∑ s ∈ S, poitouTransform (regularizedScaledTartar y δ) s * ↑((completedDedekindZetaZeroDivisor K) s)).re

theorem NumberField.Odlyzko.re_sum_poitouTransform_regularized_completedZetaZerosInClosedRectangle_nonneg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) (a b u v : ℝ) : 0 ≤ (∑ s ∈ completedDedekindZetaZerosInClosedRectangle K a b u v, poitouTransform (regularizedScaledTartar y δ) s * ↑((completedDedekindZetaZeroDivisor K) s)).re

theorem NumberField.Odlyzko.regularizedPoitou_mul_completedZetaLogDeriv_one_sub (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (y δ : ℝ) (s : ℂ) : poitouTransform (regularizedScaledTartar y δ) (1 - s) * logDeriv (poleClearedCompletedDedekindZetaContinuation K) (1 - s) = -(poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s)

theorem NumberField.Odlyzko.regularizedPoitou_centeredRectangle_identity (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ b T : ℝ} (hδ : 0 < δ) (hb : 1 / 2 ≤ b) (hT : 0 ≤ T) (hboundary : ∀ z ∈ Set.Icc (1 - b) b ×ℂ Set.Icc (-T) T, z.re = 1 - b ∨ z.re = b ∨ z.im = -T ∨ z.im = T → poleClearedCompletedDedekindZetaContinuation K z ≠ 0) : horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (1 - b) b (-T) - horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (1 - b) b T + 2 • verticalSegmentIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) b (-T) T = 2 * ↑Real.pi * Complex.I * ∑ p ∈ completedDedekindZetaZerosInClosedRectangle K (1 - b) b (-T) T, poitouTransform (regularizedScaledTartar y δ) p * ↑((completedDedekindZetaZeroDivisor K) p)

theorem NumberField.Odlyzko.regularizedPoitou_zeroFreeRectangle_identity (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ ε T : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (hT : 0 ≤ T) (hboundary : ∀ z ∈ Set.Icc (-ε) (1 + ε) ×ℂ Set.Icc (-T) T, z.re = -ε ∨ z.re = 1 + ε ∨ z.im = -T ∨ z.im = T → poleClearedCompletedDedekindZetaContinuation K z ≠ 0) : horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (-ε) (1 + ε) (-T) - horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (-ε) (1 + ε) T + 2 • verticalSegmentIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (1 + ε) (-T) T = 2 * ↑Real.pi * Complex.I * ∑ p ∈ completedDedekindZetaZerosInClosedRectangle K (-ε) (1 + ε) (-T) T, poitouTransform (regularizedScaledTartar y δ) p * ↑((completedDedekindZetaZeroDivisor K) p)

theorem NumberField.Odlyzko.regularizedPoitou_zeroFreeRectangle_im_nonneg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ ε T : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) (hε : 0 < ε) (hT : 0 ≤ T) (hboundary : ∀ z ∈ Set.Icc (-ε) (1 + ε) ×ℂ Set.Icc (-T) T, z.re = -ε ∨ z.re = 1 + ε ∨ z.im = -T ∨ z.im = T → poleClearedCompletedDedekindZetaContinuation K z ≠ 0) : 0 ≤ (horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (-ε) (1 + ε) (-T) - horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (-ε) (1 + ε) T + 2 • verticalSegmentIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * logDeriv (poleClearedCompletedDedekindZetaContinuation K) s) (1 + ε) (-T) T).im

theorem NumberField.Odlyzko.regularizedPoitou_completedZetaPole_centeredRectangle_identity {y δ b T : ℝ} (hδ : 0 < δ) (hb : 1 < b) (hT : 0 < T) : horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * completedZetaPoleLogDeriv s) (1 - b) b (-T) - horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * completedZetaPoleLogDeriv s) (1 - b) b T + 2 • verticalSegmentIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * completedZetaPoleLogDeriv s) b (-T) T = 4 * ↑Real.pi * Complex.I * poitouTransform (regularizedScaledTartar y δ) 1

theorem NumberField.Odlyzko.regularizedPoitou_subtracted_centeredRectangle_im_lowerBound (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ b T : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) (hb : 1 < b) (hT : 0 < T) (hboundary : ∀ z ∈ Set.Icc (1 - b) b ×ℂ Set.Icc (-T) T, z.re = 1 - b ∨ z.re = b ∨ z.im = -T ∨ z.im = T → poleClearedCompletedDedekindZetaContinuation K z ≠ 0) : -4 * Real.pi * (poitouTransform (regularizedScaledTartar y δ) 1).re ≤ (horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s)) (1 - b) b (-T) - horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s)) (1 - b) b T + 2 • verticalSegmentIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s)) b (-T) T).im

theorem NumberField.Odlyzko.numericalCertificate_of_integral_le {J : ℝ} (hJ : J ≤ 2 / 5) : Real.log (33 / 4) ≤ Real.eulerMascheroniConstant + Real.log (4 * Real.pi) - J - 20 * Real.pi / 123

noncomputable def NumberField.Odlyzko.gaussDigammaVerticalMajorant (σ x : ℝ) : ℝ

A gauss digamma vertical majorant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussDigammaVerticalMajorant σ x = (Real.exp (-x) + Real.exp (-σ * x)) / (1 - Real.exp (-x))

noncomputable def NumberField.Odlyzko.regularizedArchimedeanIntegrand (y δ x : ℝ) : ℝ

A regularized archimedean integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.regularizedArchimedeanIntegrand y δ x = (1 - NumberField.Odlyzko.regularizedScaledTartar y δ x) / Real.sinh x

theorem NumberField.Odlyzko.one_sub_regularizedScaledTartar_le_sq {δ : ℝ} (hδ : 0 ≤ δ) (y x : ℝ) : 1 - regularizedScaledTartar y δ x ≤ (y ^ 2 / 5 + δ) * x ^ 2

theorem NumberField.Odlyzko.regularizedArchimedeanIntegrand_nonneg {δ x : ℝ} (hδ : 0 ≤ δ) (hx : 0 < x) (y : ℝ) : 0 ≤ regularizedArchimedeanIntegrand y δ x

theorem NumberField.Odlyzko.regularizedArchimedeanIntegrand_le_linear {δ x : ℝ} (hδ : 0 ≤ δ) (hx : 0 < x) (y : ℝ) : regularizedArchimedeanIntegrand y δ x ≤ (y ^ 2 / 5 + δ) * x

theorem NumberField.Odlyzko.integrableOn_regularizedArchimedeanIntegrand_Ioc_zero_one {δ : ℝ} (hδ : 0 ≤ δ) (y : ℝ) : MeasureTheory.IntegrableOn (regularizedArchimedeanIntegrand y δ) (Set.Ioc 0 1) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_regularizedArchimedeanIntegrand_Ioi_one {δ : ℝ} (hδ : 0 ≤ δ) (y : ℝ) : MeasureTheory.IntegrableOn (regularizedArchimedeanIntegrand y δ) (Set.Ioi 1) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_regularizedArchimedeanIntegrand_Ioi {δ : ℝ} (hδ : 0 ≤ δ) (y : ℝ) : MeasureTheory.IntegrableOn (regularizedArchimedeanIntegrand y δ) (Set.Ioi 0) MeasureTheory.volume

noncomputable def NumberField.Odlyzko.regularizedArchimedeanMajorant (y x : ℝ) : ℝ

A regularized archimedean majorant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.regularizedArchimedeanMajorant y x = if x ≤ 1 then (y ^ 2 / 5 + 1) * x else 8 / 3 * Real.exp (-x)

theorem NumberField.Odlyzko.integrableOn_regularizedArchimedeanMajorant_Ioi (y : ℝ) : MeasureTheory.IntegrableOn (regularizedArchimedeanMajorant y) (Set.Ioi 0) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_regularizedArchimedeanIntegrand_le_majorant {δ x : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hx : 0 < x) (y : ℝ) : ‖regularizedArchimedeanIntegrand y δ x‖ ≤ regularizedArchimedeanMajorant y x

theorem NumberField.Odlyzko.tendsto_integral_regularizedArchimedeanIntegrand_nhdsGT_zero (y : ℝ) : Filter.Tendsto (fun (δ : ℝ) => ∫ (x : ℝ) in Set.Ioi 0, regularizedArchimedeanIntegrand y δ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (archimedeanIntegral y))

theorem NumberField.Odlyzko.tendsto_integral_inverseGaussKernel_regularizedScaledTartar_nhdsGT_zero (y : ℝ) : Filter.Tendsto (fun (δ : ℝ) => ∫ (x : ℝ) in Set.Ioi 0, inverseGaussKernel (regularizedScaledTartar y δ) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (archimedeanIntegral y - Real.log 2))

theorem NumberField.Odlyzko.norm_gaussDigammaIntegrand_vertical_le_four_div {σ t x : ℝ} (hσ : 0 ≤ σ) (hx : 0 < x) (hx1 : x ≤ 1) : ‖gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x‖ ≤ 4 / x

theorem NumberField.Odlyzko.norm_gaussDigammaIntegrand_vertical_le_sqrt {σ t x : ℝ} (hσ : 0 ≤ σ) (hx : 0 < x) (hx1 : x ≤ 1) : ‖gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x‖ ≤ 4 * √(‖↑σ + ↑t * Complex.I - 1‖ / x)

theorem NumberField.Odlyzko.integrable_sqrt_add_abs_mul_norm_poitouTransform_regularized {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => √(|σ - 1| + |t|) * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_uncurry_poitouTransform_regularized_mul_gaussDigammaIntegrand_Ioi {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 0 < σ) : MeasureTheory.Integrable (Function.uncurry fun (t x : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_integral_gaussDigammaIntegrand_Ioi {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 0 < σ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand (↑σ + ↑t * Complex.I) x = ∫ (x : ℝ) in Set.Ioi 0, ↑(2 * Real.pi * inverseGaussKernel (regularizedScaledTartar y δ) x)

theorem NumberField.Odlyzko.integral_gaussDigammaIntegrand_eq_digamma_add_euler {s : ℂ} (hs : 0 < s.re) : ∫ (x : ℝ) in Set.Ioi 0, gaussDigammaIntegrand s x = s.digamma + ↑Real.eulerMascheroniConstant

theorem NumberField.Odlyzko.integrable_poitouTransform_regularized_mul_digamma_add_euler {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 0 < σ) : MeasureTheory.Integrable (fun (t : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * ((↑σ + ↑t * Complex.I).digamma + ↑Real.eulerMascheroniConstant)) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_digamma_add_euler {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 0 < σ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * ((↑σ + ↑t * Complex.I).digamma + ↑Real.eulerMascheroniConstant) = ∫ (x : ℝ) in Set.Ioi 0, ↑(2 * Real.pi * inverseGaussKernel (regularizedScaledTartar y δ) x)

theorem NumberField.Odlyzko.logDeriv_poleClearedContinuation_sub_poles (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s = ↑(Real.log |↑(discr K)|) / 2 + ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi)) - ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), primePowerLogTerm K pe.1 pe.2 s

theorem NumberField.Odlyzko.logDeriv_poleClearedContinuation_sub_poles_eq_logDeriv_dedekindZeta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s = ↑(Real.log |↑(discr K)|) / 2 + ↑(InfinitePlace.nrComplexPlaces K) * (s.digamma - Complex.log (2 * ↑Real.pi)) + logDeriv (dedekindZeta K) s

theorem NumberField.Odlyzko.integrable_poitouTransform_regularized_mul_neg_logDeriv_dedekindZeta (K : Type u_1) [Field K] [NumberField K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : MeasureTheory.Integrable (fun (t : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * -logDeriv (dedekindZeta K) (↑σ + ↑t * Complex.I)) MeasureTheory.volume

theorem NumberField.Odlyzko.integrable_poitouTransform_regularized_mul_logDeriv_sub_poles (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : MeasureTheory.Integrable (fun (t : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑σ + ↑t * Complex.I) - completedZetaPoleLogDeriv (↑σ + ↑t * Complex.I))) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_logDeriv_sub_poles (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑σ + ↑t * Complex.I) - completedZetaPoleLogDeriv (↑σ + ↑t * Complex.I)) = 2 * ↑Real.pi * (↑(Real.log |↑(discr K)|) / 2) + ↑(InfinitePlace.nrComplexPlaces K) * ((∫ (x : ℝ) in Set.Ioi 0, ↑(2 * Real.pi * inverseGaussKernel (regularizedScaledTartar y δ) x)) - 2 * ↑Real.pi * (↑Real.eulerMascheroniConstant + Complex.log (2 * ↑Real.pi))) - ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), ↑(2 * Real.pi * regularizedPrimePowerPoitouWeight K y δ pe.1 pe.2)

theorem NumberField.Odlyzko.re_integral_poitouTransform_regularized_mul_logDeriv_sub_poles (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : (∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑σ + ↑t * Complex.I) - completedZetaPoleLogDeriv (↑σ + ↑t * Complex.I))).re = 2 * Real.pi * (Real.log |↑(discr K)| / 2 + ↑(InfinitePlace.nrComplexPlaces K) * ((∫ (x : ℝ) in Set.Ioi 0, inverseGaussKernel (regularizedScaledTartar y δ) x) - Real.eulerMascheroniConstant - Real.log (2 * Real.pi)) - ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), regularizedPrimePowerPoitouWeight K y δ pe.1 pe.2)

theorem NumberField.Odlyzko.le_rootDiscr_of_log_le_logDiscr_div_finrank (K : Type u_1) [Field K] [NumberField K] {c : ℝ} (hc : 0 < c) (h : Real.log c ≤ Real.log |↑(discr K)| / ↑(Module.finrank ℚ K)) : c ≤ rootDiscr K

def NumberField.Odlyzko.TotallyComplexPoitouEstimate (K : Type u_1) [Field K] [NumberField K] : Prop

A totally complex poitou estimate used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.target_le_rootDiscr_of_poitouEstimate (K : Type u_1) [Field K] [NumberField K] (hdim : 18 ≤ Module.finrank ℚ K) (hP : TotallyComplexPoitouEstimate K) : 8.25 ≤ rootDiscr K

theorem NumberField.Odlyzko.odlyzkoBound_of_poitouEstimate (K : Type u_1) [Field K] [NumberField K] (hdim : 18 ≤ Module.finrank ℚ K) (hP : TotallyComplexPoitouEstimate K) : |↑(discr K)| ≥ 8.25 ^ Module.finrank ℚ K

def NumberField.Odlyzko.RegularizedRightVerticalLowerBound (K : Type u_1) [Field K] [NumberField K] (y σ : ℝ) : Prop

A regularized right vertical lower bound used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.poitouEstimate_of_regularizedRightVerticalLowerBound (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y σ : ℝ} (hy : 0 < y) (hσ : 1 < σ) (hbound : RegularizedRightVerticalLowerBound K y σ) : Real.log |↑(discr K)| / ↑(Module.finrank ℚ K) ≥ Real.eulerMascheroniConstant + Real.log (4 * Real.pi) - archimedeanIntegral y - 12 * Real.pi / (5 * ↑(Module.finrank ℚ K) * y)

theorem NumberField.Odlyzko.totallyComplexPoitouEstimate_of_regularizedRightVerticalLowerBound (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {σ : ℝ} (hσ : 1 < σ) (hbound : RegularizedRightVerticalLowerBound K odlyzkoScale σ) : TotallyComplexPoitouEstimate K

def NumberField.Odlyzko.RegularizedSubtractedHorizontalVanishing (K : Type u_1) [Field K] [NumberField K] (y δ b : ℝ) : Prop

A regularized subtracted horizontal vanishing used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.regularizedRightVerticalLowerBound_of_horizontalVanishing (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ b : ℝ} (hy : y ≠ 0) (hδ : 0 < δ) (hb : 1 < b) (hvanish : RegularizedSubtractedHorizontalVanishing K y δ b) : -(2 * Real.pi) * (poitouTransform (regularizedScaledTartar y δ) 1).re ≤ (∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑b + ↑t * Complex.I) * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑b + ↑t * Complex.I) - completedZetaPoleLogDeriv (↑b + ↑t * Complex.I))).re

theorem NumberField.Odlyzko.regularizedRightVerticalLowerBound_of_forall_horizontalVanishing (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y b : ℝ} (hy : y ≠ 0) (hb : 1 < b) (hvanish : ∀ (δ : ℝ), 0 < δ → RegularizedSubtractedHorizontalVanishing K y δ b) : RegularizedRightVerticalLowerBound K y b