TODO: Add doc-string.

@[reducible, inline]

abbrev NumberField.Odlyzko.unitFundamentalParamSet (K : Type u_2) [Field K] [NumberField K] : Set (mixedEmbedding.realSpace K)

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

Equations

• NumberField.Odlyzko.unitFundamentalParamSet K = Set.univ.pi fun (w : NumberField.InfinitePlace K) => if w = NumberField.Units.dirichletUnitTheorem.w₀ then Set.univ else Set.Ico 0 1

theorem NumberField.Odlyzko.measurableSet_unitFundamentalParamSet {K : Type u_1} [Field K] [NumberField K] : MeasurableSet (unitFundamentalParamSet K)

theorem NumberField.Odlyzko.mem_unitFundamentalParamSet_iff {K : Type u_1} [Field K] [NumberField K] (x : mixedEmbedding.realSpace K) : x ∈ unitFundamentalParamSet K ↔ ∀ (w : InfinitePlace K), w ≠ Units.dirichletUnitTheorem.w₀ → x w ∈ Set.Ico 0 1

noncomputable def NumberField.Odlyzko.unitFloor {K : Type u_1} [Field K] [NumberField K] (x : mixedEmbedding.realSpace K) : InfinitePlace K → ℤ

An unit floor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unitFloor x w = if w = NumberField.Units.dirichletUnitTheorem.w₀ then 0 else ⌊x w⌋

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

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

Equations

• NumberField.Odlyzko.unitCoordinateShift z w = if hw : w = NumberField.Units.dirichletUnitTheorem.w₀ then 0 else ↑(z ⟨w, hw⟩)

noncomputable def NumberField.Odlyzko.fundamentalUnitForShift {K : Type u_1} [Field K] [NumberField K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : (RingOfIntegers K)ˣ

A fundamental unit for shift used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.expMapBasis_add_unitCoordinateShift {K : Type u_1} [Field K] [NumberField K] (x : mixedEmbedding.realSpace K) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : ↑mixedEmbedding.fundamentalCone.expMapBasis (x + unitCoordinateShift z) = (fun (w : InfinitePlace K) => w ((algebraMap (RingOfIntegers K) K) ↑(fundamentalUnitForShift z))) * ↑mixedEmbedding.fundamentalCone.expMapBasis x

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.measurableSet_unitFundamentalTranslate {K : Type u_1} [Field K] [NumberField K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : MeasurableSet (unitFundamentalTranslate z)

theorem NumberField.Odlyzko.mem_unitFundamentalTranslate_iff {K : Type u_1} [Field K] [NumberField K] (x : mixedEmbedding.realSpace K) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : x ∈ unitFundamentalTranslate z ↔ (fun (i : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ }) => unitFloor x ↑i) = z

theorem NumberField.Odlyzko.pairwise_disjoint_unitFundamentalTranslate {K : Type u_1} [Field K] [NumberField K] : Pairwise fun (z z' : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) => Disjoint (unitFundamentalTranslate z) (unitFundamentalTranslate z')

theorem NumberField.Odlyzko.iUnion_unitFundamentalTranslate {K : Type u_1} [Field K] [NumberField K] : ⋃ (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ), unitFundamentalTranslate z = Set.univ

theorem NumberField.Odlyzko.unitFundamentalTranslate_eq_image {K : Type u_1} [Field K] [NumberField K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : unitFundamentalTranslate z = (fun (x : mixedEmbedding.realSpace K) => x + unitCoordinateShift z) '' unitFundamentalParamSet K

theorem NumberField.Odlyzko.setIntegral_unitFundamentalTranslate {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalTranslate z, f x = ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f (x + unitCoordinateShift z)

theorem NumberField.Odlyzko.integral_eq_tsum_setIntegral_unitFundamentalTranslate {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : mixedEmbedding.realSpace K), f x = ∑' (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ), ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalTranslate z, f x

theorem NumberField.Odlyzko.integral_eq_tsum_setIntegral_add_unitCoordinateShift {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : mixedEmbedding.realSpace K → E) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : mixedEmbedding.realSpace K), f x = ∑' (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ), ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, f (x + unitCoordinateShift z)

theorem NumberField.Odlyzko.integral_comp_expMapBasis_eq_tsum_unitSlab {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : mixedEmbedding.realSpace K → E) (hg : MeasureTheory.Integrable (fun (x : mixedEmbedding.realSpace K) => g (↑mixedEmbedding.fundamentalCone.expMapBasis x)) MeasureTheory.volume) : ∫ (x : mixedEmbedding.realSpace K), g (↑mixedEmbedding.fundamentalCone.expMapBasis x) = ∑' (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ), ∫ (x : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, g ((fun (w : InfinitePlace K) => w ((algebraMap (RingOfIntegers K) K) ↑(fundamentalUnitForShift z))) * ↑mixedEmbedding.fundamentalCone.expMapBasis x)

theorem NumberField.Odlyzko.setIntegral_expMapBasis_image {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set (mixedEmbedding.realSpace K)} (hs : MeasurableSet s) (f : mixedEmbedding.realSpace K → E) : ∫ (q : mixedEmbedding.realSpace K) in ↑mixedEmbedding.fundamentalCone.expMapBasis '' s, f q = ∫ (x : mixedEmbedding.realSpace K) in s, (Real.exp (x Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * (∏ w : { w : InfinitePlace K // w.IsComplex }, ↑mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) • f (↑mixedEmbedding.fundamentalCone.expMapBasis x)

theorem NumberField.Odlyzko.integrableOn_expMapBasis_image_iff {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set (mixedEmbedding.realSpace K)} (hs : MeasurableSet s) (f : mixedEmbedding.realSpace K → E) : MeasureTheory.IntegrableOn f (↑mixedEmbedding.fundamentalCone.expMapBasis '' s) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (x : mixedEmbedding.realSpace K) => (Real.exp (x Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * (∏ w : { w : InfinitePlace K // w.IsComplex }, ↑mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) • f (↑mixedEmbedding.fundamentalCone.expMapBasis x)) s MeasureTheory.volume