TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.idealSetElement (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : K

An ideal set element used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealSetElement K J a = ↑↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet ↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J) a))

theorem NumberField.Odlyzko.idealSetElement_ne_zero (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : idealSetElement K J a ≠ 0

theorem NumberField.Odlyzko.absNorm_idealSetElement (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : ↑|(Algebra.norm ℚ) (idealSetElement K J a)| = ↑(idealSetIntNorm K J a)

theorem NumberField.Odlyzko.integral_idealSet_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) {s : ℂ} (hs : 0 < s.re) : (∫ (q : InfinitePlace K → ℝ), complexPlaceMellinGaussian K (idealSetElement K J a) s q ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * ↑(idealSetIntNorm K J a) ^ (-s)

theorem NumberField.Odlyzko.hasSum_integral_idealSet_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) => ∫ (q : InfinitePlace K → ℝ), complexPlaceMellinGaussian K (idealSetElement K J a) s q ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) ((2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K J s)