Vertical Growth

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.norm_centeredPositiveClassThetaIntegral_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {s : ℂ} {b : ℝ} (hsb : s.re ≤ b) : ‖centeredPositiveClassThetaIntegral K I s‖ ≤ ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, ‖centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) (↑b) y‖

theorem NumberField.Odlyzko.abs_le_max_abs_endpoints {a b σ : ℝ} (hσ : σ ∈ Set.Icc a b) : |σ| ≤ max |a| |b|

noncomputable def NumberField.Odlyzko.centeredClassThetaVerticalRadius (a b : ℝ) : ℝ

A centered class theta vertical radius used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredClassThetaVerticalRadius a b = max (max |a| |b|) (max |1 - b| |1 - a|) + 1

theorem NumberField.Odlyzko.one_le_centeredClassThetaVerticalRadius (a b : ℝ) : 1 ≤ centeredClassThetaVerticalRadius a b

theorem NumberField.Odlyzko.norm_vertical_pole_factors_le {a b σ t : ℝ} (hσ : σ ∈ Set.Icc a b) : ‖↑σ + ↑t * Complex.I‖ ≤ centeredClassThetaVerticalRadius a b * (1 + |t|) ∧ ‖1 - (↑σ + ↑t * Complex.I)‖ ≤ centeredClassThetaVerticalRadius a b * (1 + |t|)

noncomputable def NumberField.Odlyzko.centeredPositiveClassThetaNormBound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (b : ℝ) : ℝ

A centered positive class theta norm bound used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.centeredPositiveClassThetaNormBound_nonneg (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (b : ℝ) : 0 ≤ centeredPositiveClassThetaNormBound K I b

noncomputable def NumberField.Odlyzko.poleClearedCenteredClassThetaVerticalBound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (a b : ℝ) : ℝ

A pole cleared centered class theta vertical bound used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.poleClearedCenteredClassThetaVerticalBound_nonneg (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (a b : ℝ) : 0 ≤ poleClearedCenteredClassThetaVerticalBound K I a b

theorem NumberField.Odlyzko.norm_poleClearedCenteredClassThetaIntegral_vertical_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {a b σ t : ℝ} (hσ : σ ∈ Set.Icc a b) : ‖poleClearedCenteredClassThetaIntegral K I (↑σ + ↑t * Complex.I)‖ ≤ poleClearedCenteredClassThetaVerticalBound K I a b * (1 + |t|) ^ 2

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

A centered fractional class normalization norm used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.poleClearedCompletedDedekindZetaVerticalBound (K : Type u_1) [Field K] [NumberField K] (a b : ℝ) : ℝ

A pole cleared completed dedekind zeta vertical bound used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaVerticalBound_nonneg (K : Type u_1) [Field K] [NumberField K] (a b : ℝ) : 0 ≤ poleClearedCompletedDedekindZetaVerticalBound K a b

theorem NumberField.Odlyzko.norm_poleClearedCompletedDedekindZetaContinuation_vertical_le (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {a b σ t : ℝ} (hσ : σ ∈ Set.Icc a b) : ‖poleClearedCompletedDedekindZetaContinuation K (↑σ + ↑t * Complex.I)‖ ≤ poleClearedCompletedDedekindZetaVerticalBound K a b * (1 + |t|) ^ 2