TODO: Add doc-string.

def NumberField.Odlyzko.torusQuotientMap {ι : Type u_1} (x : ι → ℝ) : UnitAddTorus ι

A torus quotient map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.torusQuotientMap x i = ↑(x i)

theorem NumberField.Odlyzko.isOpenQuotientMap_torusQuotientMap {ι : Type u_1} : IsOpenQuotientMap torusQuotientMap

theorem NumberField.Odlyzko.surjective_torusQuotientMap {ι : Type u_1} : Function.Surjective torusQuotientMap

theorem NumberField.Odlyzko.exists_intPi_add_of_torusQuotientMap_eq {ι : Type u_1} {x y : ι → ℝ} (h : torusQuotientMap x = torusQuotientMap y) : ∃ (n : ι → ℤ), y = x + fun (i : ι) => ↑(n i)

theorem NumberField.Odlyzko.torusQuotientMap_add_intPi {ι : Type u_1} (x : ι → ℝ) (n : ι → ℤ) : torusQuotientMap (x + fun (i : ι) => ↑(n i)) = torusQuotientMap x

noncomputable def NumberField.Odlyzko.intPeriodization {ι : Type u_1} (f : (ι → ℝ) → ℂ) (x : ι → ℝ) : ℂ

An int periodization used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.intPeriodization f x = ∑' (n : ι → ℤ), f (x + fun (i : ι) => ↑(n i))

theorem NumberField.Odlyzko.intPeriodization_add_intPi {ι : Type u_1} (f : (ι → ℝ) → ℂ) (x : ι → ℝ) (k : ι → ℤ) : intPeriodization f (x + fun (i : ι) => ↑(k i)) = intPeriodization f x

theorem NumberField.Odlyzko.intPeriodization_eq_of_torusQuotientMap_eq {ι : Type u_1} (f : (ι → ℝ) → ℂ) {x y : ι → ℝ} (h : torusQuotientMap x = torusQuotientMap y) : intPeriodization f x = intPeriodization f y

noncomputable def NumberField.Odlyzko.torusLift {ι : Type u_1} {A : Type u_2} (f : (ι → ℝ) → A) : UnitAddTorus ι → A

A torus lift used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.torusLift f x = f (Function.surjInv ⋯ x)

theorem NumberField.Odlyzko.torusLift_comp_torusQuotientMap {ι : Type u_1} {A : Type u_2} (f : (ι → ℝ) → A) (hf : ∀ (x y : ι → ℝ), torusQuotientMap x = torusQuotientMap y → f x = f y) : torusLift f ∘ torusQuotientMap = f

theorem NumberField.Odlyzko.continuous_torusLift {ι : Type u_1} {A : Type u_2} [TopologicalSpace A] (f : (ι → ℝ) → A) (hfc : Continuous f) (hf : ∀ (x y : ι → ℝ), torusQuotientMap x = torusQuotientMap y → f x = f y) : Continuous (torusLift f)

noncomputable def NumberField.Odlyzko.torusContinuousMap {ι : Type u_1} {A : Type u_2} [TopologicalSpace A] (f : (ι → ℝ) → A) (hfc : Continuous f) (hf : ∀ (x y : ι → ℝ), torusQuotientMap x = torusQuotientMap y → f x = f y) : C(UnitAddTorus ι, A)

A torus continuous map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.torusContinuousMap f hfc hf = { toFun := NumberField.Odlyzko.torusLift f, continuous_toFun := ⋯ }

@[simp]

theorem NumberField.Odlyzko.torusContinuousMap_comp_torusQuotientMap {ι : Type u_1} {A : Type u_2} [TopologicalSpace A] (f : (ι → ℝ) → A) (hfc : Continuous f) (hf : ∀ (x y : ι → ℝ), torusQuotientMap x = torusQuotientMap y → f x = f y) (x : ι → ℝ) : (torusContinuousMap f hfc hf) (torusQuotientMap x) = f x

noncomputable def NumberField.Odlyzko.torusPeriodization {ι : Type u_1} (f : (ι → ℝ) → ℂ) (hf : Continuous (intPeriodization f)) : C(UnitAddTorus ι, ℂ)

A torus periodization used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.torusPeriodization f hf = NumberField.Odlyzko.torusContinuousMap (NumberField.Odlyzko.intPeriodization f) hf ⋯

@[simp]

theorem NumberField.Odlyzko.torusPeriodization_apply_quotient {ι : Type u_1} (f : (ι → ℝ) → ℂ) (hf : Continuous (intPeriodization f)) (x : ι → ℝ) : (torusPeriodization f hf) (torusQuotientMap x) = intPeriodization f x

theorem NumberField.Odlyzko.mFourier_torusQuotientMap {ι : Type u_1} [Fintype ι] (n : ι → ℤ) (x : ι → ℝ) : (UnitAddTorus.mFourier n) (torusQuotientMap x) = Complex.exp (2 * ↑Real.pi * Complex.I * ∑ i : ι, ↑(n i) * ↑(x i))

theorem NumberField.Odlyzko.mFourier_neg_torusQuotientMap {ι : Type u_1} [Fintype ι] (n : ι → ℤ) (x : ι → ℝ) : (UnitAddTorus.mFourier (-n)) (torusQuotientMap x) = Complex.exp (-2 * ↑Real.pi * Complex.I * ∑ i : ι, ↑(n i) * ↑(x i))

@[simp]

theorem NumberField.Odlyzko.norm_mFourier_torusQuotientMap {ι : Type u_1} [Fintype ι] (n : ι → ℤ) (x : ι → ℝ) : ‖(UnitAddTorus.mFourier n) (torusQuotientMap x)‖ = 1

theorem NumberField.Odlyzko.innerBilin_nondegenerate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : (innerₗ E).Nondegenerate

noncomputable def NumberField.Odlyzko.dualRealBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) : Module.Basis ι ℝ E

A dual real basis used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dualRealBasis L b = LinearMap.BilinForm.dualBasis (innerₗ E) ⋯ (Module.Basis.ofZLatticeBasis ℝ L b)

theorem NumberField.Odlyzko.inner_dualRealBasis_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (i : ι) (x : E) : inner ℝ ((dualRealBasis L b) i) x = ((Module.Basis.ofZLatticeBasis ℝ L b).repr x) i

noncomputable def NumberField.Odlyzko.dualLattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : Submodule ℤ E

A dual lattice used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dualLattice L = LinearMap.BilinForm.dualSubmodule (innerₗ E) L

theorem NumberField.Odlyzko.mem_dualLattice_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (y : E) : y ∈ dualLattice L ↔ ∀ (x : ↥L), ∃ (n : ℤ), inner ℝ y ↑x = ↑n

theorem NumberField.Odlyzko.span_range_dualRealBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) : Submodule.span ℤ (Set.range ⇑(dualRealBasis L b)) = dualLattice L

instance NumberField.Odlyzko.dualLattice.instDiscreteTopology {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] : DiscreteTopology ↥(dualLattice L)

noncomputable def NumberField.Odlyzko.dualLatticeBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) : Module.Basis ι ℤ ↥(dualLattice L)

A dual lattice basis used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.dualLatticeBasis_apply_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (i : ι) : ↑((dualLatticeBasis L b) i) = (dualRealBasis L b) i

noncomputable def NumberField.Odlyzko.latticeGaussian {E : Type u_1} [NormedAddCommGroup E] (a : ℝ) (x : E) : ℂ

A lattice gaussian used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.latticeGaussian a x = Complex.exp (-↑a * ↑‖x‖ ^ 2)

theorem NumberField.Odlyzko.norm_latticeGaussian {E : Type u_1} [NormedAddCommGroup E] (a : ℝ) (x : E) : ‖latticeGaussian a x‖ = Real.exp (-a * ‖x‖ ^ 2)

theorem NumberField.Odlyzko.norm_latticeGaussian_add_le {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} (ha : 0 ≤ a) (y z : E) : ‖latticeGaussian a (y + z)‖ ≤ Real.exp (a * ‖y‖ ^ 2) * ‖latticeGaussian (a / 2) z‖

theorem NumberField.Odlyzko.summable_latticeGaussian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {a : ℝ} (ha : 0 < a) : Summable fun (x : ↥L) => latticeGaussian a ↑x

noncomputable def NumberField.Odlyzko.latticeTheta {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (a : ℝ) : ℂ

A lattice theta used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.latticeTheta L a = ∑' (x : ↥L), NumberField.Odlyzko.latticeGaussian a ↑x

theorem NumberField.Odlyzko.latticeTheta_map_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) (e : E ≃ₗᵢ[ℝ] E) (a : ℝ) : latticeTheta (Submodule.map (↑(LinearEquiv.restrictScalars ℤ e.toLinearEquiv)) L) a = latticeTheta L a

theorem NumberField.Odlyzko.summable_latticeTheta {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {a : ℝ} (ha : 0 < a) : Summable fun (x : ↥L) => latticeGaussian a ↑x

noncomputable def NumberField.Odlyzko.dualLatticeTheta {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (a : ℝ) : ℂ

A dual lattice theta used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dualLatticeTheta L a = NumberField.Odlyzko.latticeTheta (NumberField.Odlyzko.dualLattice L) a

noncomputable def NumberField.Odlyzko.latticePoint {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] (L : Submodule ℤ E) (b : Module.Basis ι ℤ ↥L) (n : ι → ℤ) : E

A lattice point used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.latticePoint L b n = ↑(b.equivFun.symm n)

noncomputable def NumberField.Odlyzko.dualLatticePoint {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (n : ι → ℤ) : E

A dual lattice point used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.dualLatticePoint L b n = ↑((NumberField.Odlyzko.dualLatticeBasis L b).equivFun.symm n)

theorem NumberField.Odlyzko.inner_dualLatticePoint_ofZLatticeBasis_equivFun_symm {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (n : ι → ℤ) (x : ι → ℝ) : inner ℝ (dualLatticePoint L b n) ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm x) = ∑ i : ι, ↑(n i) * x i

theorem NumberField.Odlyzko.latticeTheta_eq_tsum_coordinates {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] (L : Submodule ℤ E) (b : Module.Basis ι ℤ ↥L) (a : ℝ) : latticeTheta L a = ∑' (n : ι → ℤ), latticeGaussian a (latticePoint L b n)

theorem NumberField.Odlyzko.dualLatticeTheta_eq_tsum_coordinates {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (a : ℝ) : dualLatticeTheta L a = ∑' (n : ι → ℤ), latticeGaussian a (dualLatticePoint L b n)

noncomputable def NumberField.Odlyzko.coordinateGaussian {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (x : ι → ℝ) : ℂ

A coordinate gaussian used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateGaussian L b a x = NumberField.Odlyzko.latticeGaussian a ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm x)

noncomputable def NumberField.Odlyzko.coordinateBasisMap {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) : C(ι → ℝ, E)

A coordinate basis map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateBasisMap L b = { toFun := ⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm.toContinuousLinearEquiv, continuous_toFun := ⋯ }

theorem NumberField.Odlyzko.continuous_coordinateGaussian {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) : Continuous (coordinateGaussian L b a)

theorem NumberField.Odlyzko.ofZLatticeBasis_equivFun_symm_intCast {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (n : ι → ℤ) : ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm fun (i : ι) => ↑(n i)) = latticePoint L b n

noncomputable def NumberField.Odlyzko.coordinateGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n : ι → ℤ) : C(ι → ℝ, ℂ)

A coordinate gaussian translate used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateGaussianTranslate L b a n = { toFun := fun (x : ι → ℝ) => NumberField.Odlyzko.coordinateGaussian L b a (x + fun (i : ι) => ↑(n i)), continuous_toFun := ⋯ }

theorem NumberField.Odlyzko.summable_norm_latticeGaussian_latticePoint {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) : Summable fun (n : ι → ℤ) => ‖latticeGaussian a (latticePoint L b n)‖

theorem NumberField.Odlyzko.norm_coordinateGaussianTranslate_apply_le {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (x : ι → ℝ) (n : ι → ℤ) : ‖(coordinateGaussianTranslate L b a n) x‖ ≤ Real.exp (a * ‖(coordinateBasisMap L b) x‖ ^ 2) * ‖latticeGaussian (a / 2) (latticePoint L b n)‖

theorem NumberField.Odlyzko.norm_restrict_coordinateGaussianTranslate_le {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (K : TopologicalSpace.Compacts (ι → ℝ)) (n : ι → ℤ) : ‖ContinuousMap.restrict (↑K) (coordinateGaussianTranslate L b a n)‖ ≤ Real.exp (a * ‖ContinuousMap.restrict (↑K) (coordinateBasisMap L b)‖ ^ 2) * ‖latticeGaussian (a / 2) (latticePoint L b n)‖

theorem NumberField.Odlyzko.summable_norm_restrict_coordinateGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (K : TopologicalSpace.Compacts (ι → ℝ)) : Summable fun (n : ι → ℤ) => ‖ContinuousMap.restrict (↑K) (coordinateGaussianTranslate L b a n)‖

theorem NumberField.Odlyzko.continuous_intPeriodization_coordinateGaussian {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) : Continuous (intPeriodization (coordinateGaussian L b a))

noncomputable def NumberField.Odlyzko.gaussianTorusPeriodization {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (ha : 0 < a) : C(UnitAddTorus ι, ℂ)

A gaussian torus periodization used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.gaussianTorusPeriodization L b a ha = NumberField.Odlyzko.torusPeriodization (NumberField.Odlyzko.coordinateGaussian L b a) ⋯

theorem NumberField.Odlyzko.gaussianTorusPeriodization_zero {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) : (gaussianTorusPeriodization L b a ha) 0 = latticeTheta L a

noncomputable def NumberField.Odlyzko.coordinateIntLattice {ι : Type u_1} [Fintype ι] : Submodule ℤ (ι → ℝ)

A coordinate int lattice used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateIntLattice = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

noncomputable def NumberField.Odlyzko.coordinateIntBasis {ι : Type u_1} [Fintype ι] : Module.Basis ι ℤ ↥coordinateIntLattice

A coordinate int basis used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateIntBasis = Module.Basis.restrictScalars ℤ (Pi.basisFun ℝ ι)

noncomputable def NumberField.Odlyzko.coordinateIntPoint {ι : Type u_1} [Fintype ι] (n : ι → ℤ) : ↥coordinateIntLattice

A coordinate int point used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateIntPoint n = NumberField.Odlyzko.coordinateIntBasis.equivFun.symm n

@[simp]

theorem NumberField.Odlyzko.coordinateIntPoint_apply {ι : Type u_1} [Fintype ι] (n : ι → ℤ) (i : ι) : ↑(coordinateIntPoint n) i = ↑(n i)

theorem NumberField.Odlyzko.pi_Ioc_ae_eq_pi_Ico {ι : Type u_1} [Fintype ι] : {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ioc 0 1} =ᵐ[MeasureTheory.volume] {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ico 0 1}

theorem NumberField.Odlyzko.integral_eq_tsum_integral_pi_Ico {ι : Type u_1} [Fintype ι] {A : Type u_2} [NormedAddCommGroup A] [NormedSpace ℝ A] (f : (ι → ℝ) → A) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : ι → ℝ), f x = ∑' (n : ι → ℤ), ∫ (x : ι → ℝ) in {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ico 0 1}, f ((fun (i : ι) => ↑(n i)) + x)

theorem NumberField.Odlyzko.integral_eq_tsum_integral_pi_Ioc {ι : Type u_1} [Fintype ι] {A : Type u_2} [NormedAddCommGroup A] [NormedSpace ℝ A] (f : (ι → ℝ) → A) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : ι → ℝ), f x = ∑' (n : ι → ℤ), ∫ (x : ι → ℝ) in {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ioc 0 1}, f ((fun (i : ι) => ↑(n i)) + x)

noncomputable def NumberField.Odlyzko.coordinateFourierCharacter {ι : Type u_2} [Fintype ι] (n : ι → ℤ) (x : ι → ℝ) : ℂ

A coordinate fourier character used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateFourierCharacter n x = (UnitAddTorus.mFourier (-n)) (NumberField.Odlyzko.torusQuotientMap x)

theorem NumberField.Odlyzko.measurableSet_pi_Ioc {κ : Type u_3} [Finite κ] : MeasurableSet {x : κ → ℝ | ∀ (i : κ), x i ∈ Set.Ioc 0 1}

@[simp]

theorem NumberField.Odlyzko.norm_coordinateFourierCharacter {ι : Type u_2} [Fintype ι] (n : ι → ℤ) (x : ι → ℝ) : ‖coordinateFourierCharacter n x‖ = 1

noncomputable def NumberField.Odlyzko.coordinateFourierGaussian {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n : ι → ℤ) (x : ι → ℝ) : ℂ

A coordinate fourier gaussian used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateFourierGaussian L b a n x = NumberField.Odlyzko.coordinateFourierCharacter n x * NumberField.Odlyzko.coordinateGaussian L b a x

noncomputable def NumberField.Odlyzko.coordinateFourierGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n k : ι → ℤ) (x : ι → ℝ) : ℂ

A coordinate fourier gaussian translate used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.coordinateFourierGaussianTranslate L b a n k x = NumberField.Odlyzko.coordinateFourierCharacter n x * (NumberField.Odlyzko.coordinateGaussianTranslate L b a k) x

theorem NumberField.Odlyzko.continuous_coordinateFourierGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n k : ι → ℤ) : Continuous (coordinateFourierGaussianTranslate L b a n k)

theorem NumberField.Odlyzko.coordinateFourierGaussian_add_intPi {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n k : ι → ℤ) (x : ι → ℝ) : coordinateFourierGaussian L b a n ((fun (i : ι) => ↑(k i)) + x) = coordinateFourierGaussianTranslate L b a n k x

theorem NumberField.Odlyzko.summable_integral_norm_coordinateFourierGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (n : ι → ℤ) : Summable fun (k : ι → ℤ) => ∫ (x : ι → ℝ) in {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ioc 0 1}, ‖coordinateFourierGaussianTranslate L b a n k x‖

theorem NumberField.Odlyzko.integral_tsum_coordinateFourierGaussianTranslate {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (n : ι → ℤ) : ∫ (x : ι → ℝ) in {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ioc 0 1}, ∑' (k : ι → ℤ), coordinateFourierGaussianTranslate L b a n k x = ∑' (k : ι → ℤ), ∫ (x : ι → ℝ) in {x : ι → ℝ | ∀ (i : ι), x i ∈ Set.Ioc 0 1}, coordinateFourierGaussianTranslate L b a n k x

theorem NumberField.Odlyzko.mFourierCoeff_gaussianTorusPeriodization {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (n : ι → ℤ) (hint : MeasureTheory.Integrable (coordinateFourierGaussian L b a n) MeasureTheory.volume) : UnitAddTorus.mFourierCoeff (⇑(gaussianTorusPeriodization L b a ha)) n = ∫ (x : ι → ℝ), coordinateFourierGaussian L b a n x

theorem NumberField.Odlyzko.map_ofZLatticeBasis_equivFun_symm_volume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) : MeasureTheory.Measure.map (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm) MeasureTheory.volume = (Module.Basis.ofZLatticeBasis ℝ L b).addHaar

theorem NumberField.Odlyzko.covolume_eq_volumeReal_parallelepiped {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) : ZLattice.covolume L MeasureTheory.volume = MeasureTheory.volume.real ↑(Module.Basis.ofZLatticeBasis ℝ L b).parallelepiped

theorem NumberField.Odlyzko.volume_parallelepiped_ofZLatticeBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) : MeasureTheory.volume ↑(Module.Basis.ofZLatticeBasis ℝ L b).parallelepiped = ENNReal.ofReal (ZLattice.covolume L MeasureTheory.volume)

theorem NumberField.Odlyzko.addHaar_ofZLatticeBasis_eq_inv_covolume_smul_volume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) : (Module.Basis.ofZLatticeBasis ℝ L b).addHaar = (ZLattice.covolume L MeasureTheory.volume).toNNReal⁻¹ • MeasureTheory.volume

theorem NumberField.Odlyzko.integral_comp_ofZLatticeBasis_equivFun_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) (f : E → ℂ) : ∫ (x : ι → ℝ), f ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm x) = (ZLattice.covolume L MeasureTheory.volume).toNNReal⁻¹ • ∫ (y : E), f y

theorem NumberField.Odlyzko.integrable_comp_ofZLatticeBasis_equivFun_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) {f : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ι → ℝ) => f ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm x)) MeasureTheory.volume

noncomputable def NumberField.Odlyzko.ambientFourierGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : ℝ) (w y : E) : ℂ

An ambient fourier gaussian used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.ambientFourierGaussian a w y = Complex.exp (-↑a * ↑‖y‖ ^ 2 + -2 * ↑Real.pi * Complex.I * ↑(inner ℝ w y))

theorem NumberField.Odlyzko.integrable_ambientFourierGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {a : ℝ} (ha : 0 < a) (w : E) : MeasureTheory.Integrable (ambientFourierGaussian a w) MeasureTheory.volume

theorem NumberField.Odlyzko.coordinateFourierGaussian_eq_ambient {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (a : ℝ) (n : ι → ℤ) (x : ι → ℝ) : coordinateFourierGaussian L b a n x = ambientFourierGaussian a (dualLatticePoint L b n) ((Module.Basis.ofZLatticeBasis ℝ L b).equivFun.symm x)

theorem NumberField.Odlyzko.integrable_coordinateFourierGaussian {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (n : ι → ℤ) : MeasureTheory.Integrable (coordinateFourierGaussian L b a n) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_ambientFourierGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {a : ℝ} (ha : 0 < a) (w : E) : ∫ (y : E), ambientFourierGaussian a w y = (↑Real.pi / ↑a) ^ (↑(Module.finrank ℝ E) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖w‖ ^ 2 / ↑a)

theorem NumberField.Odlyzko.mFourierCoeff_gaussianTorusPeriodization_eq {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [Fintype ι] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) (n : ι → ℤ) : UnitAddTorus.mFourierCoeff (⇑(gaussianTorusPeriodization L b a ha)) n = (ZLattice.covolume L MeasureTheory.volume).toNNReal⁻¹ • ((↑Real.pi / ↑a) ^ (↑(Module.finrank ℝ E) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖dualLatticePoint L b n‖ ^ 2 / ↑a))

theorem NumberField.Odlyzko.exp_fourierGaussian_eq_latticeGaussian {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} (_ha : 0 < a) (w : E) : Complex.exp (-↑Real.pi ^ 2 * ↑‖w‖ ^ 2 / ↑a) = latticeGaussian (Real.pi ^ 2 / a) w

theorem NumberField.Odlyzko.summable_mFourierCoeff_gaussianTorusPeriodization {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [Fintype ι] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) : Summable (UnitAddTorus.mFourierCoeff ⇑(gaussianTorusPeriodization L b a ha))

theorem NumberField.Odlyzko.latticeGaussian_poissonSummation_of_basis {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [Finite ι] (b : Module.Basis ι ℤ ↥L) {a : ℝ} (ha : 0 < a) : latticeTheta L a = (ZLattice.covolume L MeasureTheory.volume).toNNReal⁻¹ • ((↑Real.pi / ↑a) ^ (↑(Module.finrank ℝ E) / 2) * dualLatticeTheta L (Real.pi ^ 2 / a))

theorem NumberField.Odlyzko.latticeGaussian_poissonSummation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {a : ℝ} (ha : 0 < a) : latticeTheta L a = (ZLattice.covolume L MeasureTheory.volume).toNNReal⁻¹ • ((↑Real.pi / ↑a) ^ (↑(Module.finrank ℝ E) / 2) * dualLatticeTheta L (Real.pi ^ 2 / a))