TODO: Add doc-string.

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

A complex place gaussian used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.complexPlaceGaussian K x q = Complex.exp (-↑(2 * Real.pi * ∑ w : NumberField.InfinitePlace K, w x ^ 2 * q w ^ 2))

theorem NumberField.Odlyzko.complexPlaceMellinGaussian_eq_prod_cpow_mul_gaussian (K : Type u_1) [Field K] [NumberField K] (x : K) (s : ℂ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), 0 ≤ q w) : complexPlaceMellinGaussian K x s q = ↑(∏ w : InfinitePlace K, q w) ^ (2 * s - 1) * complexPlaceGaussian K x q

theorem NumberField.Odlyzko.prod_complexPlace_eq_prod_infinitePlace (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (f : InfinitePlace K → ℝ) : ∏ w : { w : InfinitePlace K // w.IsComplex }, f ↑w = ∏ w : InfinitePlace K, f w

theorem NumberField.Odlyzko.prod_infinitePlace_sq_eq_norm_mixedSpaceOfRealSpace (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), 0 ≤ q w) : (∏ w : InfinitePlace K, q w) ^ 2 = mixedEmbedding.norm (mixedEmbedding.mixedSpaceOfRealSpace q)

theorem NumberField.Odlyzko.prod_expMapBasis_eq_exp_half_finrank (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (y : mixedEmbedding.realSpace K) : ∏ w : InfinitePlace K, ↑mixedEmbedding.fundamentalCone.expMapBasis y w = Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K) / 2)

theorem NumberField.Odlyzko.ofReal_exp_cpow (a : ℝ) (s : ℂ) : ↑(Real.exp a) ^ s = Complex.exp (↑a * s)

theorem NumberField.Odlyzko.complexPlaceRadialJacobian_eq_prod (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), 0 < q w) : complexPlaceRadialJacobian K q = (∏ w : InfinitePlace K, q w) * (2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K)

theorem NumberField.Odlyzko.radialMellinGaussian_eq_prod_cpow_mul_gaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : K) (s : ℂ) (y : mixedEmbedding.realSpace K) : radialMellinGaussian K x s y = (2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) • (↑(∏ w : InfinitePlace K, ↑mixedEmbedding.fundamentalCone.expMapBasis y w) ^ (2 * s) * complexPlaceGaussian K x (↑mixedEmbedding.fundamentalCone.expMapBasis y))

theorem NumberField.Odlyzko.radialMellinGaussian_eq_exp_mul_gaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : K) (s : ℂ) (y : mixedEmbedding.realSpace K) : radialMellinGaussian K x s y = (2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) • (Complex.exp (↑(y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s) * complexPlaceGaussian K x (↑mixedEmbedding.fundamentalCone.expMapBasis y))

theorem NumberField.Odlyzko.fundamentalConeZeta_eq_integral_tsum_nonzeroIdealElement_radial (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K J s = ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, ∑' (x : nonzeroIdealElement K J), radialMellinGaussian K (↑↑x) s y

noncomputable def NumberField.Odlyzko.nonzeroIdealShapeTheta (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (y : mixedEmbedding.realSpace K) : ℂ

A nonzero ideal shape theta used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.tsum_nonzeroIdealElement_radialMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) (y : mixedEmbedding.realSpace K) : ∑' (x : nonzeroIdealElement K J), radialMellinGaussian K (↑↑x) s y = ↑(2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) * Complex.exp (↑(y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s) * nonzeroIdealShapeTheta K J y

theorem NumberField.Odlyzko.integrableOn_logarithmicMellinWeight_mul_nonzeroIdealShapeTheta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : MeasureTheory.IntegrableOn (fun (y : mixedEmbedding.realSpace K) => Complex.exp (↑(y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s) * nonzeroIdealShapeTheta K J y) (unitFundamentalParamSet K) MeasureTheory.volume

theorem NumberField.Odlyzko.fundamentalConeZeta_eq_integral_nonzeroIdealShapeTheta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K J s = ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, ↑(2⁻¹ ^ InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * Units.regulator K) * Complex.exp (↑(y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * s) * nonzeroIdealShapeTheta K J y