Poitou Estimate

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.sq_abs_mul_norm_poitouTransform_regularized_eq_norm_fourier_second {δ : ℝ} (hδ : 0 < δ) (y σ t : ℝ) : |t| ^ 2 * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖ = ‖FourierTransform.fourier (poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ) (-t / (2 * Real.pi))‖

theorem NumberField.Odlyzko.tendsto_sq_abs_mul_norm_poitouTransform_regularized_atTop {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : Filter.Tendsto (fun (t : ℝ) => |t| ^ 2 * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖) Filter.atTop (nhds 0)

theorem NumberField.Odlyzko.tendsto_sq_abs_mul_norm_poitouTransform_regularized_atBot {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : Filter.Tendsto (fun (t : ℝ) => |t| ^ 2 * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖) Filter.atBot (nhds 0)

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

A regularized poitou profile second derivative majorant used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.regularizedPoitouStripQuadraticDecayConstant (y δ a b : ℝ) : ℝ

A regularized poitou strip quadratic decay constant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.regularizedPoitouStripQuadraticDecayConstant y δ a b = ∫ (x : ℝ), NumberField.Odlyzko.regularizedPoitouProfileSecondDerivativeMajorant y δ (max |a - 1 / 2| |b - 1 / 2|) x

theorem NumberField.Odlyzko.regularizedPoitouProfileSecondDerivativeMajorant_integrable {δ : ℝ} (hδ : 0 < δ) (y M : ℝ) : MeasureTheory.Integrable (regularizedPoitouProfileSecondDerivativeMajorant y δ M) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_poitouVerticalProfileSecondDerivative_regularized_le_majorant {δ M : ℝ} (hδ : 0 < δ) (_hM : 0 ≤ M) (y : ℝ) {σ : ℝ} (hσ : |σ - 1 / 2| ≤ M) (x : ℝ) : ‖poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x‖ ≤ regularizedPoitouProfileSecondDerivativeMajorant y δ M x

theorem NumberField.Odlyzko.sq_abs_mul_norm_poitouTransform_regularized_le_strip {δ a b : ℝ} (hδ : 0 < δ) (y t : ℝ) {σ : ℝ} (hσ : σ ∈ Set.Icc a b) : |t| ^ 2 * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖ ≤ ∫ (x : ℝ), regularizedPoitouProfileSecondDerivativeMajorant y δ (max |a - 1 / 2| |b - 1 / 2|) x

noncomputable def NumberField.Odlyzko.completedDedekindZetaZeroAbsoluteOrdinatesInBands (K : Type u_1) [Field K] [NumberField K] (a b U V : ℝ) : Finset ℝ

Absolute ordinates, in prescribed bands, of zeros of the completed Dedekind zeta function.

Equations

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

theorem NumberField.Odlyzko.exists_completedZeta_height_separated_from_zeros_in_bands (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (a b U : ℝ) {A L V : ℝ} (hA : 0 ≤ A) (hL : 0 < L) : ∃ (T : ℝ), A < T ∧ T < A + L ∧ ∀ (z : ℂ), z.re ∈ Set.Icc a b → |z.im| ∈ Set.Icc U V → poleClearedCompletedDedekindZetaContinuation K z = 0 → finiteSetAvoidanceRadiusOnLength L (completedDedekindZetaZeroAbsoluteOrdinatesInBands K a b U V) ≤ |T - z.im| ∧ finiteSetAvoidanceRadiusOnLength L (completedDedekindZetaZeroAbsoluteOrdinatesInBands K a b U V) ≤ |-T - z.im|

noncomputable def NumberField.Odlyzko.completedZetaSelectedHeightOrdinates (K : Type u_1) [Field K] [NumberField K] (A : ℝ) : Finset ℝ

A completed zeta selected height ordinates used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightOrdinates K A = NumberField.Odlyzko.completedDedekindZetaZeroAbsoluteOrdinatesInBands K (-3) 7 (A - 5) (A + 6)

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

A completed zeta selected height separation used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightSeparation K A = NumberField.Odlyzko.finiteSetAvoidanceRadiusOnLength 1 (NumberField.Odlyzko.completedZetaSelectedHeightOrdinates K A)

theorem NumberField.Odlyzko.completedZetaSelectedHeightSeparation_pos (K : Type u_1) [Field K] [NumberField K] (A : ℝ) : 0 < completedZetaSelectedHeightSeparation K A

theorem NumberField.Odlyzko.exists_height_norm_logDeriv_poleClearedCompletedZeta_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {A : ℝ} (hA : 6 ≤ A) : ∃ (T : ℝ), A < T ∧ T < A + 1 ∧ ∀ x ∈ Set.Icc (-1) 5, (poleClearedCompletedDedekindZetaContinuation K (↑x + ↑T * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x + ↑T * Complex.I)‖ ≤ completedZetaCenterLogLinearBound K T * completedZetaCanonicalJensenCoefficient / completedZetaSelectedHeightSeparation K A + completedZetaCenterLogLinearBound K T * completedZetaCanonicalJensenCoefficient + 32 * completedZetaCenterLogLinearBound K T) ∧ poleClearedCompletedDedekindZetaContinuation K (↑x - ↑T * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x - ↑T * Complex.I)‖ ≤ completedZetaCenterLogLinearBound K (-T) * completedZetaCanonicalJensenCoefficient / completedZetaSelectedHeightSeparation K A + completedZetaCenterLogLinearBound K (-T) * completedZetaCanonicalJensenCoefficient + 32 * completedZetaCenterLogLinearBound K (-T)

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

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

Equations

• NumberField.Odlyzko.completedZetaMovingVerticalCoefficient K R = max 1 (NumberField.Odlyzko.poleClearedCompletedDedekindZetaVerticalBound K (2 - |R|) (2 + |R|))

theorem NumberField.Odlyzko.one_le_completedZetaMovingVerticalCoefficient (K : Type u_1) [Field K] [NumberField K] (R : ℝ) : 1 ≤ completedZetaMovingVerticalCoefficient K R

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

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

Equations

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

theorem NumberField.Odlyzko.log_completedZetaMovingCircleBound_le (K : Type u_1) [Field K] [NumberField K] (R t : ℝ) : Real.log (completedZetaMovingCircleBound K R t) ≤ completedZetaMovingVerticalCoefficient K R + 2 * (1 + |t| + |R|)

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

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

A completed zeta moving center constant part used in the Odlyzko-bound argument.

Equations

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

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

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

Equations

• NumberField.Odlyzko.completedZetaMovingCenterSlope K = 2 + ↑(NumberField.InfinitePlace.nrComplexPlaces K) / 2 * Real.pi

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

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

Equations

• NumberField.Odlyzko.completedZetaMovingCenterLinearCoefficient K R = 1 + NumberField.Odlyzko.completedZetaMovingCenterConstantPart K R + NumberField.Odlyzko.completedZetaMovingCenterSlope K

theorem NumberField.Odlyzko.one_le_completedZetaMovingCenterLinearCoefficient (K : Type u_1) [Field K] [NumberField K] (R : ℝ) : 1 ≤ completedZetaMovingCenterLinearCoefficient K R

theorem NumberField.Odlyzko.completedZetaMovingCenterLogLinearBound_le (K : Type u_1) [Field K] [NumberField K] (R t : ℝ) : completedZetaMovingCenterLogLinearBound K R t ≤ completedZetaMovingCenterLinearCoefficient K R * (1 + |t|)

theorem NumberField.Odlyzko.completedZetaCenterLogLinearBound_eq_moving (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : completedZetaCenterLogLinearBound K t = completedZetaMovingCenterLogLinearBound K 6 t

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

A completed zeta selected height zero count bound used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightZeroCountBound K A = 2 * NumberField.Odlyzko.completedZetaMovingCenterLogLinearBound K 9 (A + 1 / 2) / Real.log (9 / 8)

theorem NumberField.Odlyzko.card_completedZetaSelectedHeightOrdinates_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {A : ℝ} (hA : 6 ≤ A) : ↑(completedZetaSelectedHeightOrdinates K A).card ≤ completedZetaSelectedHeightZeroCountBound K A

theorem NumberField.Odlyzko.inv_completedZetaSelectedHeightSeparation_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {A : ℝ} (hA : 6 ≤ A) : (completedZetaSelectedHeightSeparation K A)⁻¹ ≤ 4 * (completedZetaSelectedHeightZeroCountBound K A + 1)

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

The linear coefficient controlling the completed-zeta zero count at a selected height.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightZeroCountLinearCoefficient K = 4 * NumberField.Odlyzko.completedZetaMovingCenterLinearCoefficient K 9 / Real.log (9 / 8)

theorem NumberField.Odlyzko.completedZetaSelectedHeightZeroCountBound_le_linear (K : Type u_1) [Field K] [NumberField K] {A : ℝ} (hA : 6 ≤ A) : completedZetaSelectedHeightZeroCountBound K A ≤ completedZetaSelectedHeightZeroCountLinearCoefficient K * (A + 1)

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

The linear coefficient controlling inverse zero separation at a selected height.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightSeparationInvLinearCoefficient K = 4 * (NumberField.Odlyzko.completedZetaSelectedHeightZeroCountLinearCoefficient K + 1)

theorem NumberField.Odlyzko.inv_completedZetaSelectedHeightSeparation_le_linear (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {A : ℝ} (hA : 6 ≤ A) : (completedZetaSelectedHeightSeparation K A)⁻¹ ≤ completedZetaSelectedHeightSeparationInvLinearCoefficient K * (A + 1)

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

The linear coefficient controlling the completed zeta function at a selected center.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeightCenterLinearCoefficient K = 2 * NumberField.Odlyzko.completedZetaMovingCenterLinearCoefficient K 6

theorem NumberField.Odlyzko.completedZetaSelectedHeightCenterLinearCoefficient_nonneg (K : Type u_1) [Field K] [NumberField K] : 0 ≤ completedZetaSelectedHeightCenterLinearCoefficient K

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

The quadratic coefficient controlling the completed-zeta logarithmic derivative at a selected height.

Equations

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

theorem NumberField.Odlyzko.completedZetaSelectedHeightLogDerivativeQuadraticCoefficient_nonneg (K : Type u_1) [Field K] [NumberField K] : 0 ≤ completedZetaSelectedHeightLogDerivativeQuadraticCoefficient K

theorem NumberField.Odlyzko.exists_height_norm_logDeriv_poleClearedCompletedZeta_le_quadratic (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {A : ℝ} (hA : 6 ≤ A) : ∃ (T : ℝ), A < T ∧ T < A + 1 ∧ ∀ x ∈ Set.Icc (-1) 5, (poleClearedCompletedDedekindZetaContinuation K (↑x + ↑T * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x + ↑T * Complex.I)‖ ≤ completedZetaSelectedHeightLogDerivativeQuadraticCoefficient K * (A + 1) ^ 2) ∧ poleClearedCompletedDedekindZetaContinuation K (↑x - ↑T * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x - ↑T * Complex.I)‖ ≤ completedZetaSelectedHeightLogDerivativeQuadraticCoefficient K * (A + 1) ^ 2

noncomputable def NumberField.Odlyzko.completedZetaSelectedHeight (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (n : ℕ) : ℝ

A completed zeta selected height used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.completedZetaSelectedHeight K n = Classical.choose ⋯

theorem NumberField.Odlyzko.completedZetaSelectedHeight_spec (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (n : ℕ) : ↑n + 6 < completedZetaSelectedHeight K n ∧ completedZetaSelectedHeight K n < ↑n + 7 ∧ ∀ x ∈ Set.Icc (-1) 5, (poleClearedCompletedDedekindZetaContinuation K (↑x + ↑(completedZetaSelectedHeight K n) * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x + ↑(completedZetaSelectedHeight K n) * Complex.I)‖ ≤ completedZetaSelectedHeightLogDerivativeQuadraticCoefficient K * (↑n + 7) ^ 2) ∧ poleClearedCompletedDedekindZetaContinuation K (↑x - ↑(completedZetaSelectedHeight K n) * Complex.I) ≠ 0 ∧ ‖logDeriv (poleClearedCompletedDedekindZetaContinuation K) (↑x - ↑(completedZetaSelectedHeight K n) * Complex.I)‖ ≤ completedZetaSelectedHeightLogDerivativeQuadraticCoefficient K * (↑n + 7) ^ 2

theorem NumberField.Odlyzko.completedZetaSelectedHeight_pos (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (n : ℕ) : 0 < completedZetaSelectedHeight K n

theorem NumberField.Odlyzko.tendsto_completedZetaSelectedHeight_atTop (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : Filter.Tendsto (completedZetaSelectedHeight K) Filter.atTop Filter.atTop

theorem NumberField.Odlyzko.tendsto_selected_positive_horizontalIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ : ℝ} (hδ : 0 < δ) : Filter.Tendsto (fun (n : ℕ) => horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s)) (-1) 2 (completedZetaSelectedHeight K n)) Filter.atTop (nhds 0)

theorem NumberField.Odlyzko.tendsto_selected_negative_horizontalIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y δ : ℝ} (hδ : 0 < δ) : Filter.Tendsto (fun (n : ℕ) => horizontalIntegral (fun (s : ℂ) => poitouTransform (regularizedScaledTartar y δ) s * (logDeriv (poleClearedCompletedDedekindZetaContinuation K) s - completedZetaPoleLogDeriv s)) (-1) 2 (-completedZetaSelectedHeight K n)) Filter.atTop (nhds 0)

theorem NumberField.Odlyzko.regularizedSubtractedHorizontalVanishing_two (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (y : ℝ) {δ : ℝ} (hδ : 0 < δ) : RegularizedSubtractedHorizontalVanishing K y δ 2

theorem NumberField.Odlyzko.regularizedRightVerticalLowerBound_two (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {y : ℝ} (hy : y ≠ 0) : RegularizedRightVerticalLowerBound K y 2

theorem NumberField.Odlyzko.totallyComplexPoitouEstimate (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : TotallyComplexPoitouEstimate K

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