TODO: Add doc-string.

theorem NumberField.Odlyzko.hasSum_integral_norm_radialMellinGaussian_unitSlab (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) : HasSum (fun (z : unitShiftIndex K) => ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, ‖radialMellinGaussian K (↑↑(fundamentalUnitForShift z) * idealSetElement K J a) s y‖) (∫ (y : mixedEmbedding.realSpace K), ‖radialMellinGaussian K (idealSetElement K J a) s y‖)

theorem NumberField.Odlyzko.summable_prod_integral_norm_radialMellinGaussian_unitSlab (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : Summable fun (p : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K) => ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, ‖radialMellinGaussian K (↑↑(fundamentalUnitForShift p.2) * idealSetElement K J p.1) s y‖

theorem NumberField.Odlyzko.summable_prod_integral_radialMellinGaussian_unitSlab (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : Summable fun (p : ↑(mixedEmbedding.fundamentalCone.idealSet K J) × unitShiftIndex K) => ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, radialMellinGaussian K (↑↑(fundamentalUnitForShift p.2) * idealSetElement K J p.1) s y

theorem NumberField.Odlyzko.fundamentalConeZeta_eq_tsum_nonzeroIdealElement_radialIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K J s = ∑' (x : nonzeroIdealElement K J), ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, radialMellinGaussian K (↑↑x) s y