TODO: Add doc-string.

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

A centered nonzero fractional shape theta mellin kernel used in the Odlyzko-bound argument.

Equations

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

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

A centered class theta poisson correction used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.logarithmicMellinWeight_neg_mul_centered_invCovolume (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))).toNNReal)⁻¹ = logarithmicMellinWeight K (1 - s) y

theorem NumberField.Odlyzko.centeredNonzeroFractionalShapeThetaMellinKernel_neg_poisson (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (y : mixedEmbedding.realSpace K) : centeredNonzeroFractionalShapeThetaMellinKernel K I s (-y) = centeredNonzeroFractionalShapeThetaMellinKernel K (traceDualIdealUnit K I) (1 - s) y + centeredClassThetaPoissonCorrection K s y

theorem NumberField.Odlyzko.centeredNonzeroFractionalShapeThetaMellinKernel_vadd_unitCoordinateLattice (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (g : ↥unitCoordinateLattice) (y : mixedEmbedding.realSpace K) : centeredNonzeroFractionalShapeThetaMellinKernel K I s (↑g + y) = centeredNonzeroFractionalShapeThetaMellinKernel K I s y

theorem NumberField.Odlyzko.centeredClassThetaPoissonCorrection_eq (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (y : mixedEmbedding.realSpace K) : centeredClassThetaPoissonCorrection K s y = logarithmicMellinWeight K (1 - s) y - logarithmicMellinWeight K s (-y)

theorem NumberField.Odlyzko.integrableOn_centeredClassThetaPoissonCorrection (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : MeasureTheory.IntegrableOn (centeredClassThetaPoissonCorrection K s) positiveUnitFundamentalParamSet MeasureTheory.volume

theorem NumberField.Odlyzko.setIntegral_centeredClassThetaPoissonCorrection (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, centeredClassThetaPoissonCorrection K s y = -1 / (↑(Module.finrank ℚ K) * (1 - s)) - 1 / (↑(Module.finrank ℚ K) * s)