TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.nonzeroShapeThetaMellinKernel (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) (y : mixedEmbedding.realSpace K) : ℂ

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

Equations

• NumberField.Odlyzko.nonzeroShapeThetaMellinKernel K J s y = NumberField.Odlyzko.logarithmicMellinWeight K s y * NumberField.Odlyzko.nonzeroIdealShapeTheta K J y

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

A 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.

theorem NumberField.Odlyzko.integrableOn_nonzeroShapeThetaMellinKernel (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : MeasureTheory.IntegrableOn (nonzeroShapeThetaMellinKernel K J s) (unitFundamentalParamSet K) MeasureTheory.volume