TODO: Add doc-string.

theorem NumberField.Odlyzko.norm_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] (x : K) (s : ℂ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), 0 < q w) : ↑‖complexPlaceMellinGaussian K x s q‖ = complexPlaceMellinGaussian K x (↑s.re) q

theorem NumberField.Odlyzko.idealSetElement_injective (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Function.Injective (idealSetElement K J)

theorem NumberField.Odlyzko.integral_norm_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : (∫ (q : InfinitePlace K → ℝ), ‖complexPlaceMellinGaussian K x s q‖ ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = ‖(2⁻¹ * CompletedZeta.complexPlaceGammaFactor ↑s.re) ^ InfinitePlace.nrComplexPlaces K * ↑↑|(Algebra.norm ℚ) x| ^ (-↑s.re)‖

theorem NumberField.Odlyzko.summable_integral_norm_idealSet_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : Summable 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)