TODO: Add doc-string.

def NumberField.Odlyzko.nonnegativeRadialHalfSpace {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A nonnegative radial half space used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.nonnegativeRadialHalfSpace = {y : NumberField.mixedEmbedding.realSpace K | 0 ≤ y NumberField.Units.dirichletUnitTheorem.w₀}

def NumberField.Odlyzko.negativeRadialHalfSpace {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A negative radial half space used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.negativeRadialHalfSpace = {y : NumberField.mixedEmbedding.realSpace K | y NumberField.Units.dirichletUnitTheorem.w₀ < 0}

def NumberField.Odlyzko.positiveRadialHalfSpace {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A positive radial half space used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.positiveRadialHalfSpace = {y : NumberField.mixedEmbedding.realSpace K | 0 < y NumberField.Units.dirichletUnitTheorem.w₀}

def NumberField.Odlyzko.nonnegativeUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A nonnegative unit fundamental param set used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.nonnegativeUnitFundamentalParamSet = NumberField.Odlyzko.unitFundamentalParamSet K ∩ NumberField.Odlyzko.nonnegativeRadialHalfSpace

def NumberField.Odlyzko.negativeUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A negative unit fundamental param set used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.negativeUnitFundamentalParamSet = NumberField.Odlyzko.unitFundamentalParamSet K ∩ NumberField.Odlyzko.negativeRadialHalfSpace

def NumberField.Odlyzko.positiveUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A positive unit fundamental param set used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.positiveUnitFundamentalParamSet = NumberField.Odlyzko.unitFundamentalParamSet K ∩ NumberField.Odlyzko.positiveRadialHalfSpace

theorem NumberField.Odlyzko.measurableSet_negativeRadialHalfSpace {K : Type u_1} [Field K] [NumberField K] : MeasurableSet negativeRadialHalfSpace

theorem NumberField.Odlyzko.measurableSet_positiveRadialHalfSpace {K : Type u_1} [Field K] [NumberField K] : MeasurableSet positiveRadialHalfSpace

theorem NumberField.Odlyzko.measurableSet_negativeUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : MeasurableSet negativeUnitFundamentalParamSet

theorem NumberField.Odlyzko.measurableSet_positiveUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : MeasurableSet positiveUnitFundamentalParamSet

theorem NumberField.Odlyzko.nonnegativeRadialHalfSpace_ae_eq_positive {K : Type u_1} [Field K] [NumberField K] : nonnegativeRadialHalfSpace =ᵐ[MeasureTheory.volume] positiveRadialHalfSpace

theorem NumberField.Odlyzko.nonnegativeUnitFundamentalParamSet_ae_eq_positive {K : Type u_1} [Field K] [NumberField K] : nonnegativeUnitFundamentalParamSet =ᵐ[MeasureTheory.volume] positiveUnitFundamentalParamSet

theorem NumberField.Odlyzko.setIntegral_nonnegativeUnitFundamentalParamSet_eq_positive {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) : ∫ (y : mixedEmbedding.realSpace K) in nonnegativeUnitFundamentalParamSet, f y = ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f y

theorem NumberField.Odlyzko.disjoint_nonnegative_negativeUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : Disjoint nonnegativeUnitFundamentalParamSet negativeUnitFundamentalParamSet

theorem NumberField.Odlyzko.union_nonnegative_negativeUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : nonnegativeUnitFundamentalParamSet ∪ negativeUnitFundamentalParamSet = unitFundamentalParamSet K

theorem NumberField.Odlyzko.setIntegral_unitFundamentalParamSet_eq_add_radialHalves {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : MeasureTheory.IntegrableOn f (unitFundamentalParamSet K) MeasureTheory.volume) : ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f y = (∫ (y : mixedEmbedding.realSpace K) in nonnegativeUnitFundamentalParamSet, f y) + ∫ (y : mixedEmbedding.realSpace K) in negativeUnitFundamentalParamSet, f y

theorem NumberField.Odlyzko.setIntegral_unitFundamentalParamSet_eq_add_openRadialHalves {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : MeasureTheory.IntegrableOn f (unitFundamentalParamSet K) MeasureTheory.volume) : ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f y = (∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f y) + ∫ (y : mixedEmbedding.realSpace K) in negativeUnitFundamentalParamSet, f y

def NumberField.Odlyzko.negUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

A neg unit fundamental param set used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.negUnitFundamentalParamSet = (fun (y : NumberField.mixedEmbedding.realSpace K) => -y) ⁻¹' NumberField.Odlyzko.unitFundamentalParamSet K

theorem NumberField.Odlyzko.measurableSet_negUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : MeasurableSet negUnitFundamentalParamSet

theorem NumberField.Odlyzko.isAddFundamentalDomain_negUnitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : MeasureTheory.IsAddFundamentalDomain (↥unitCoordinateLattice) negUnitFundamentalParamSet MeasureTheory.volume

theorem NumberField.Odlyzko.setIntegral_negUnitFundamentalParamSet_eq {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : ∀ (g : ↥unitCoordinateLattice) (x : mixedEmbedding.realSpace K), f (↑g + x) = f x) : ∫ (y : mixedEmbedding.realSpace K) in negUnitFundamentalParamSet, f y = ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f y

theorem NumberField.Odlyzko.setIntegral_positive_comp_neg_eq_negSlab_negative {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) : ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f (-y) = ∫ (y : mixedEmbedding.realSpace K) in negUnitFundamentalParamSet ∩ negativeRadialHalfSpace, f y

theorem NumberField.Odlyzko.setIntegral_negative_eq_positive_comp_neg {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : ∀ (g : ↥unitCoordinateLattice) (x : mixedEmbedding.realSpace K), f (↑g + x) = f x) : ∫ (y : mixedEmbedding.realSpace K) in negativeUnitFundamentalParamSet, f y = ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f (-y)

theorem NumberField.Odlyzko.integrableOn_negative_iff_positive_comp_neg {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] (f : mixedEmbedding.realSpace K → E) (hf : ∀ (g : ↥unitCoordinateLattice) (x : mixedEmbedding.realSpace K), f (↑g + x) = f x) : MeasureTheory.IntegrableOn f negativeUnitFundamentalParamSet MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (y : mixedEmbedding.realSpace K) => f (-y)) positiveUnitFundamentalParamSet MeasureTheory.volume

theorem NumberField.Odlyzko.setIntegral_positiveUnitFundamentalParamSet_add_eq {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : ∀ (g : ↥unitCoordinateLattice) (x : mixedEmbedding.realSpace K), f (↑g + x) = f x) (a : mixedEmbedding.realSpace K) (ha : a Units.dirichletUnitTheorem.w₀ = 0) : ∫ (x : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f (x + a) = ∫ (x : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, f x