TODO: Add doc-string.

theorem NumberField.Odlyzko.cpow_prod_of_nonneg {ι : Type u_1} (t : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ t, 0 ≤ a i) (s : ℂ) : ↑(∏ i ∈ t, a i) ^ s = ∏ i ∈ t, ↑(a i) ^ s

theorem NumberField.Odlyzko.integrableOn_cpow_mul_cexp_neg_mul_sq_Ioi {s : ℂ} (hs : 0 < s.re) {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑x ^ (2 * s - 1) * Complex.exp (-(↑r * ↑x ^ 2))) (Set.Ioi 0) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_cpow_mul_cexp_neg_mul_sq_Ioi {s : ℂ} (hs : 0 < s.re) {r : ℝ} (hr : 0 < r) : ∫ (x : ℝ) in Set.Ioi 0, ↑x ^ (2 * s - 1) * Complex.exp (-(↑r * ↑x ^ 2)) = 2⁻¹ * (1 / ↑r) ^ s * Complex.Gamma s

theorem NumberField.Odlyzko.integral_complexPlaceGaussian {s : ℂ} (hs : 0 < s.re) {a : ℝ} (ha : 0 < a) : ∫ (x : ℝ) in Set.Ioi 0, ↑x ^ (2 * s - 1) * Complex.exp (-(↑(2 * Real.pi * a) * ↑x ^ 2)) = 2⁻¹ * ↑a ^ (-s) * CompletedZeta.complexPlaceGammaFactor s

theorem NumberField.Odlyzko.integral_pi_complexPlaceGaussian_eq_prod {ι : Type u_1} [Fintype ι] (a : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) {s : ℂ} (hs : 0 < s.re) : (∫ (x : ι → ℝ), ∏ i : ι, ↑(x i) ^ (2 * s - 1) * Complex.exp (-(↑(2 * Real.pi * a i) * ↑(x i) ^ 2)) ∂MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume.restrict (Set.Ioi 0)) = ∏ i : ι, 2⁻¹ * ↑(a i) ^ (-s) * CompletedZeta.complexPlaceGammaFactor s

theorem NumberField.Odlyzko.integral_totallyComplexGaussian_eq_prod (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : (∫ (q : InfinitePlace K → ℝ), ∏ w : InfinitePlace K, ↑(q w) ^ (2 * s - 1) * Complex.exp (-(↑(2 * Real.pi * w x ^ 2) * ↑(q w) ^ 2)) ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = ∏ w : InfinitePlace K, 2⁻¹ * ↑(w x ^ 2) ^ (-s) * CompletedZeta.complexPlaceGammaFactor s

theorem NumberField.Odlyzko.prod_infinitePlace_sq_cpow_eq_absNorm_cpow (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : K) (s : ℂ) : ∏ w : InfinitePlace K, ↑(w x ^ 2) ^ s = ↑↑|(Algebra.norm ℚ) x| ^ s

theorem NumberField.Odlyzko.prod_complexPlaceGaussian_eq_absNorm (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : K) (s : ℂ) : ∏ w : InfinitePlace K, 2⁻¹ * ↑(w x ^ 2) ^ (-s) * CompletedZeta.complexPlaceGammaFactor s = (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ Fintype.card (InfinitePlace K) * ↑↑|(Algebra.norm ℚ) x| ^ (-s)

theorem NumberField.Odlyzko.integral_totallyComplexGaussian_eq_absNorm (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : (∫ (q : InfinitePlace K → ℝ), ∏ w : InfinitePlace K, ↑(q w) ^ (2 * s - 1) * Complex.exp (-(↑(2 * Real.pi * w x ^ 2) * ↑(q w) ^ 2)) ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * ↑↑|(Algebra.norm ℚ) x| ^ (-s)

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

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

Equations

• NumberField.Odlyzko.complexPlaceMellinGaussian K x s q = ∏ w : NumberField.InfinitePlace K, ↑(q w) ^ (2 * s - 1) * Complex.exp (-(↑(2 * Real.pi * w x ^ 2) * ↑(q w) ^ 2))

theorem NumberField.Odlyzko.integrable_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : MeasureTheory.Integrable (complexPlaceMellinGaussian K x s) (MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0))

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

theorem NumberField.Odlyzko.prod_infinitePlace_apply_unit_cpow_eq_one (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (u : (RingOfIntegers K)ˣ) (s : ℂ) : ∏ w : InfinitePlace K, ↑(w ↑↑u) ^ s = 1

theorem NumberField.Odlyzko.complexPlaceMellinGaussian_unit_mul (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (u : (RingOfIntegers K)ˣ) (x : K) (s : ℂ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), 0 ≤ q w) : complexPlaceMellinGaussian K (↑↑u * x) s q = complexPlaceMellinGaussian K x s ((fun (w : InfinitePlace K) => w ↑↑u) * q)

theorem NumberField.Odlyzko.integral_complexPlaceMellinGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {x : K} (hx : x ≠ 0) {s : ℂ} (hs : 0 < s.re) : (∫ (q : InfinitePlace K → ℝ), complexPlaceMellinGaussian K x s q ∂MeasureTheory.Measure.pi fun (x : InfinitePlace K) => MeasureTheory.volume.restrict (Set.Ioi 0)) = (2⁻¹ * CompletedZeta.complexPlaceGammaFactor s) ^ InfinitePlace.nrComplexPlaces K * ↑↑|(Algebra.norm ℚ) x| ^ (-s)

theorem NumberField.Odlyzko.complexPlaceMellinGaussian_fundamentalUnitForShift (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (z : { w : InfinitePlace K // w ≠ Units.dirichletUnitTheorem.w₀ } → ℤ) (x : K) (s : ℂ) (y : mixedEmbedding.realSpace K) : complexPlaceMellinGaussian K x s ((fun (w : InfinitePlace K) => w ↑↑(fundamentalUnitForShift z)) * ↑mixedEmbedding.fundamentalCone.expMapBasis y) = complexPlaceMellinGaussian K (↑↑(fundamentalUnitForShift z) * x) s (↑mixedEmbedding.fundamentalCone.expMapBasis y)