TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.unitCoordinateShiftHom {K : Type u_1} [Field K] [NumberField K] : ({ w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) →+ mixedEmbedding.realSpace K

An unit coordinate shift hom used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitCoordinateShiftHom = { toFun := NumberField.Odlyzko.unitCoordinateShift, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NumberField.Odlyzko.unitCoordinateShiftHom_apply {K : Type u_1} [Field K] [NumberField K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : unitCoordinateShiftHom z = unitCoordinateShift z

noncomputable def NumberField.Odlyzko.unitCoordinateLattice {K : Type u_1} [Field K] [NumberField K] : AddSubgroup (mixedEmbedding.realSpace K)

An unit coordinate lattice used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitCoordinateLattice = NumberField.Odlyzko.unitCoordinateShiftHom.range

theorem NumberField.Odlyzko.unitCoordinateShift_mem_lattice {K : Type u_1} [Field K] [NumberField K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : unitCoordinateShift z ∈ unitCoordinateLattice

theorem NumberField.Odlyzko.unitCoordinateLattice_apply_w₀ {K : Type u_1} [Field K] [NumberField K] (g : ↥unitCoordinateLattice) : ↑g Units.dirichletUnitTheorem.w₀ = 0

instance NumberField.Odlyzko.countable_unitCoordinateLattice {K : Type u_1} [Field K] [NumberField K] : Countable ↥unitCoordinateLattice

theorem NumberField.Odlyzko.existsUnique_vadd_mem_unitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] (x : mixedEmbedding.realSpace K) : ∃! g : ↥unitCoordinateLattice, ↑g + x ∈ unitFundamentalParamSet K

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

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

An unit fundamental real translate used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitFundamentalRealTranslate a = (fun (x : NumberField.mixedEmbedding.realSpace K) => x - a) ⁻¹' NumberField.Odlyzko.unitFundamentalParamSet K

theorem NumberField.Odlyzko.unitFundamentalRealTranslate_eq_image {K : Type u_1} [Field K] [NumberField K] (a : mixedEmbedding.realSpace K) : unitFundamentalRealTranslate a = (fun (x : mixedEmbedding.realSpace K) => x + a) '' unitFundamentalParamSet K

theorem NumberField.Odlyzko.measurableSet_unitFundamentalRealTranslate {K : Type u_1} [Field K] [NumberField K] (a : mixedEmbedding.realSpace K) : MeasurableSet (unitFundamentalRealTranslate a)

theorem NumberField.Odlyzko.isAddFundamentalDomain_unitFundamentalRealTranslate {K : Type u_1} [Field K] [NumberField K] (a : mixedEmbedding.realSpace K) : MeasureTheory.IsAddFundamentalDomain (↥unitCoordinateLattice) (unitFundamentalRealTranslate a) MeasureTheory.volume

theorem NumberField.Odlyzko.setIntegral_add_unitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (a : mixedEmbedding.realSpace K) : ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f (x + a) = ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalRealTranslate a, f x

theorem NumberField.Odlyzko.setIntegral_unitFundamentalParamSet_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) : ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f (x + a) = ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f x

theorem NumberField.Odlyzko.integrableOn_unitFundamentalParamSet_comp_add_iff {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) (a : mixedEmbedding.realSpace K) : MeasureTheory.IntegrableOn (fun (x : mixedEmbedding.realSpace K) => f (x + a)) (unitFundamentalParamSet K) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (unitFundamentalParamSet K) MeasureTheory.volume