TODO: Add doc-string.

@[reducible, inline]

abbrev NumberField.Odlyzko.complexPlacePositiveOrthant (K : Type u_1) [Field K] : Set (InfinitePlace K → ℝ)

A complex place positive orthant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.complexPlacePositiveOrthant K = Set.univ.pi fun (x : NumberField.InfinitePlace K) => Set.Ioi 0

theorem NumberField.Odlyzko.expMapBasis_image_univ (K : Type u_1) [Field K] [NumberField K] : ↑mixedEmbedding.fundamentalCone.expMapBasis '' Set.univ = complexPlacePositiveOrthant K

theorem NumberField.Odlyzko.pi_restrict_Ioi_eq_volume_restrict_positiveOrthant (K : Type u_1) [Field K] [NumberField K] : (MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = MeasureTheory.volume.restrict (complexPlacePositiveOrthant K)

noncomputable def NumberField.Odlyzko.complexPlaceRadialJacobian (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) : ℝ

A complex place radial jacobian used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.complexPlaceRadialJacobian_expMapBasis (K : Type u_1) [Field K] [NumberField K] (y : mixedEmbedding.realSpace K) : complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis y) = Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * (∏ w : { w : InfinitePlace K // w.IsComplex }, ↑mixedEmbedding.fundamentalCone.expMapBasis y ↑w)⁻¹ * 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K

theorem NumberField.Odlyzko.integral_positiveOrthant_eq_expMapBasis (K : Type u_1) [Field K] [NumberField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (InfinitePlace K → ℝ) → E) : (∫ (q : InfinitePlace K → ℝ), f q ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = ∫ (y : mixedEmbedding.realSpace K), complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis y) • f (↑mixedEmbedding.fundamentalCone.expMapBasis y)

theorem NumberField.Odlyzko.integral_complexPlaceMellinGaussian_eq_expMapBasis (K : Type u_1) [Field K] [NumberField K] (x : K) (s : ℂ) : (∫ (q : InfinitePlace K → ℝ), complexPlaceMellinGaussian K x s q ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = ∫ (y : mixedEmbedding.realSpace K), complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis y) • complexPlaceMellinGaussian K x s (↑mixedEmbedding.fundamentalCone.expMapBasis y)

theorem NumberField.Odlyzko.complexPlaceRadialJacobian_expMapBasis_pos (K : Type u_1) [Field K] [NumberField K] (y : mixedEmbedding.realSpace K) : 0 < complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis y)

noncomputable def NumberField.Odlyzko.radialMellinGaussian (K : Type u_1) [Field K] [NumberField K] (x : K) (s : ℂ) (y : mixedEmbedding.realSpace K) : ℂ

A radial mellin gaussian used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.integrable_complexPlaceRadialJacobian_smul_mellinGaussian (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : MeasureTheory.Integrable (radialMellinGaussian K x s) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_norm_radialMellinGaussian (K : Type u_1) [Field K] [NumberField K] (x : K) (s : ℂ) : ∫ (y : mixedEmbedding.realSpace K), ‖radialMellinGaussian K x s y‖ = ∫ (q : InfinitePlace K → ℝ), ‖complexPlaceMellinGaussian K x s q‖ ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)

theorem NumberField.Odlyzko.prod_complexPlace_apply_unit_eq_one (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (u : (RingOfIntegers K)ˣ) : ∏ w : { w : InfinitePlace K // w.IsComplex }, ↑w ↑↑u = 1

theorem NumberField.Odlyzko.complexPlaceRadialJacobian_expMapBasis_add_unitCoordinateShift (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (y : mixedEmbedding.realSpace K) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis (y + unitCoordinateShift z)) = complexPlaceRadialJacobian K (↑mixedEmbedding.fundamentalCone.expMapBasis y)

theorem NumberField.Odlyzko.radialMellinGaussian_add_unitCoordinateShift (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : K) (s : ℂ) (y : mixedEmbedding.realSpace K) (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) : radialMellinGaussian K x s (y + unitCoordinateShift z) = radialMellinGaussian K (↑↑(fundamentalUnitForShift z) * x) s y

theorem NumberField.Odlyzko.integral_radialMellinGaussian_eq_tsum_unitSlab (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : ∫ (y : mixedEmbedding.realSpace K), radialMellinGaussian K x s y = ∑' (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ), ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, radialMellinGaussian K (↑↑(fundamentalUnitForShift z) * x) s y