TODO: Add doc-string.

theorem NumberField.Odlyzko.norm_logarithmicMellinWeight (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (y : mixedEmbedding.realSpace K) : ‖logarithmicMellinWeight K s y‖ = Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K) * s.re)

theorem NumberField.Odlyzko.norm_logarithmicMellinWeight_mono (K : Type u_1) [Field K] [NumberField K] {s : ℂ} {b : ℝ} {y : mixedEmbedding.realSpace K} (hy : 0 ≤ y Units.dirichletUnitTheorem.w₀) (hsb : s.re ≤ b) : ‖logarithmicMellinWeight K s y‖ ≤ ‖logarithmicMellinWeight K (↑b) y‖

theorem NumberField.Odlyzko.norm_centeredNonzeroFractionalShapeThetaMellinKernel_mono (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {s : ℂ} {b : ℝ} {y : mixedEmbedding.realSpace K} (hy : 0 ≤ y Units.dirichletUnitTheorem.w₀) (hsb : s.re ≤ b) : ‖centeredNonzeroFractionalShapeThetaMellinKernel K I s y‖ ≤ ‖centeredNonzeroFractionalShapeThetaMellinKernel K I (↑b) y‖

noncomputable def NumberField.Odlyzko.centeredMellinRadialCoefficient (K : Type u_1) [Field K] [NumberField K] (y : mixedEmbedding.realSpace K) : ℂ

A centered mellin radial coefficient used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredMellinRadialCoefficient K y = ↑(y NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))

theorem NumberField.Odlyzko.hasDerivAt_centeredNonzeroFractionalShapeThetaMellinKernel (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (y : mixedEmbedding.realSpace K) : HasDerivAt (fun (z : ℂ) => centeredNonzeroFractionalShapeThetaMellinKernel K I z y) (centeredMellinRadialCoefficient K y * centeredNonzeroFractionalShapeThetaMellinKernel K I s y) s

theorem NumberField.Odlyzko.norm_centeredMellinRadialCoefficient_mul_kernel_le (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {s : ℂ} {b : ℝ} {y : mixedEmbedding.realSpace K} (hy : 0 ≤ y Units.dirichletUnitTheorem.w₀) (hsb : s.re + 1 ≤ b) : ‖centeredMellinRadialCoefficient K y * centeredNonzeroFractionalShapeThetaMellinKernel K I s y‖ ≤ ‖centeredNonzeroFractionalShapeThetaMellinKernel K I (↑b) y‖

theorem NumberField.Odlyzko.integrableOn_positive_centeredNonzeroFractionalShapeThetaMellinKernel_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) : MeasureTheory.IntegrableOn (centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) J) s) positiveUnitFundamentalParamSet MeasureTheory.volume

theorem NumberField.Odlyzko.differentiableAt_centeredPositiveClassThetaIntegral_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s₀ : ℂ) : DifferentiableAt ℂ (centeredPositiveClassThetaIntegral K ((FractionalIdeal.mk0 K) J)) s₀

theorem NumberField.Odlyzko.differentiable_centeredPositiveClassThetaIntegral_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Differentiable ℂ (centeredPositiveClassThetaIntegral K ((FractionalIdeal.mk0 K) J))

theorem NumberField.Odlyzko.differentiable_centeredPositiveClassThetaIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Differentiable ℂ (centeredPositiveClassThetaIntegral K I)

noncomputable def NumberField.Odlyzko.poleClearedCenteredClassThetaIntegral (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : ℂ

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

Equations

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

theorem NumberField.Odlyzko.differentiable_poleClearedCenteredClassThetaIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Differentiable ℂ (poleClearedCenteredClassThetaIntegral K I)

theorem NumberField.Odlyzko.poleClearedCenteredClassThetaIntegral_eq_mul_continued (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1) : poleClearedCenteredClassThetaIntegral K I s = ↑(Module.finrank ℚ K) * s * (1 - s) * centeredRadiallyContinuedClassThetaIntegral K I s