TODO: Add doc-string.

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

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

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

theorem NumberField.Odlyzko.integrableOn_positive_logarithmicMellinWeight_neg (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 0 < s.re) : MeasureTheory.IntegrableOn (fun (y : mixedEmbedding.realSpace K) => logarithmicMellinWeight K s (-y)) positiveUnitFundamentalParamSet MeasureTheory.volume