TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.euclideanIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule ℤ (mixedEmbedding.euclidean.mixedSpace K)

An euclidean ideal lattice used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.euclideanIdealLattice K I = ZLattice.comap ℝ (NumberField.mixedEmbedding.idealLattice K I) ↑↑(NumberField.mixedEmbedding.euclidean.toMixed K)

instance NumberField.Odlyzko.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntEuclideanIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : DiscreteTopology ↥(euclideanIdealLattice K I)

instance NumberField.Odlyzko.instIsZLatticeRealMixedSpaceEuclideanIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : IsZLattice ℝ (euclideanIdealLattice K I)

theorem NumberField.Odlyzko.covolume_euclideanIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ZLattice.covolume (euclideanIdealLattice K I) MeasureTheory.volume = ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ InfinitePlace.nrComplexPlaces K * √|↑(discr K)|

noncomputable def NumberField.Odlyzko.mixedTracePairing (K : Type u_1) [Field K] [NumberField K] (x y : mixedEmbedding.mixedSpace K) : ℝ

A mixed trace pairing used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.mixedTracePairing_mixedEmbedding (K : Type u_1) [Field K] [NumberField K] (x y : K) : mixedTracePairing K ((mixedEmbedding K) x) ((mixedEmbedding K) y) = ↑((Algebra.trace ℚ K) (x * y))

noncomputable def NumberField.Odlyzko.divideBySqrtTwo : ℂ ≃L[ℝ] ℂ

A divide by sqrt two used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.divideBySqrtTwo = ContinuousLinearEquiv.smulLeft (Units.mk0 (√2)⁻¹ NumberField.Odlyzko.divideBySqrtTwo._proof_4)

@[simp]

theorem NumberField.Odlyzko.divideBySqrtTwo_symm_apply (z : ℂ) : divideBySqrtTwo.symm z = √2 • z

noncomputable def NumberField.Odlyzko.unscaleComplexCoordinates (K : Type u_1) [Field K] : ({ w : InfinitePlace K // w.IsComplex } → ℂ) ≃L[ℝ] { w : InfinitePlace K // w.IsComplex } → ℂ

An unscale complex coordinates used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.unscaleComplexCoordinates K = ContinuousLinearEquiv.piCongrRight fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => NumberField.Odlyzko.divideBySqrtTwo

noncomputable def NumberField.Odlyzko.traceToMixed (K : Type u_1) [Field K] [NumberField K] : mixedEmbedding.euclidean.mixedSpace K ≃L[ℝ] mixedEmbedding.mixedSpace K

A trace to mixed used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.traceEmbedding (K : Type u_1) [Field K] [NumberField K] (x : K) : mixedEmbedding.euclidean.mixedSpace K

A trace embedding used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.traceEmbedding K x = (NumberField.Odlyzko.traceToMixed K).symm ((NumberField.mixedEmbedding K) x)

noncomputable def NumberField.Odlyzko.traceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule ℤ (mixedEmbedding.euclidean.mixedSpace K)

A trace ideal lattice used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.traceIdealLattice K I = ZLattice.comap ℝ (NumberField.mixedEmbedding.idealLattice K I) ↑↑(NumberField.Odlyzko.traceToMixed K)

instance NumberField.Odlyzko.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntTraceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : DiscreteTopology ↥(traceIdealLattice K I)

instance NumberField.Odlyzko.instIsZLatticeRealMixedSpaceTraceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : IsZLattice ℝ (traceIdealLattice K I)

theorem NumberField.Odlyzko.traceEmbedding_mem_traceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {x : K} : traceEmbedding K x ∈ traceIdealLattice K I ↔ x ∈ ↑I

theorem NumberField.Odlyzko.exists_traceEmbedding_eq_of_mem_traceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {v : mixedEmbedding.euclidean.mixedSpace K} (hv : v ∈ traceIdealLattice K I) : ∃ x ∈ ↑I, traceEmbedding K x = v

noncomputable def NumberField.Odlyzko.traceConjugation (K : Type u_1) [Field K] [NumberField K] : mixedEmbedding.euclidean.mixedSpace K ≃ₗᵢ[ℝ] mixedEmbedding.euclidean.mixedSpace K

A trace conjugation used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.traceConjugation_involutive (K : Type u_1) [Field K] [NumberField K] (x : mixedEmbedding.euclidean.mixedSpace K) : (traceConjugation K) ((traceConjugation K) x) = x

theorem NumberField.Odlyzko.inner_traceEmbedding_traceConjugation (K : Type u_1) [Field K] [NumberField K] (x y : K) : inner ℝ (traceEmbedding K x) ((traceConjugation K) (traceEmbedding K y)) = ↑((Algebra.trace ℚ K) (x * y))

noncomputable def NumberField.Odlyzko.traceIdealRealBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℝ (mixedEmbedding.euclidean.mixedSpace K)

A trace ideal real basis used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.traceIdealRealBasis K I = (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I).map ↑(NumberField.Odlyzko.traceToMixed K).symm

@[simp]

theorem NumberField.Odlyzko.traceIdealRealBasis_apply (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : (traceIdealRealBasis K I) i = traceEmbedding K ((basisOfFractionalIdeal K I) i)

theorem NumberField.Odlyzko.span_traceIdealRealBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule.span ℤ (Set.range ⇑(traceIdealRealBasis K I)) = traceIdealLattice K I

theorem NumberField.Odlyzko.innerDualBasis_traceIdealRealBasis_apply (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I) : (LinearMap.BilinForm.dualBasis (innerₗ (mixedEmbedding.euclidean.mixedSpace K)) ⋯ (traceIdealRealBasis K I)) i = (traceConjugation K) (traceEmbedding K ((basisOfFractionalIdeal K I).traceDual i))

theorem NumberField.Odlyzko.span_traceDual_basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I).traceDual) = Submodule.restrictScalars ℤ ↑↑(traceDualIdealUnit K I)

noncomputable def NumberField.Odlyzko.traceEmbeddingIntLinearMap (K : Type u_1) [Field K] [NumberField K] : K →ₗ[ℤ] mixedEmbedding.euclidean.mixedSpace K

A trace embedding int linear map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.traceEmbeddingIntLinearMap K = ↑ℤ ↑↑(NumberField.Odlyzko.traceToMixed K).symm ∘ₗ (NumberField.mixedEmbedding K).toIntAlgHom.toLinearMap

@[simp]

theorem NumberField.Odlyzko.traceEmbeddingIntLinearMap_apply (K : Type u_1) [Field K] [NumberField K] (x : K) : (traceEmbeddingIntLinearMap K) x = traceEmbedding K x

noncomputable def NumberField.Odlyzko.conjugateTraceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule ℤ (mixedEmbedding.euclidean.mixedSpace K)

A conjugate trace ideal lattice used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.map_traceEmbeddingIntLinearMap_fractionalIdeal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule.map (traceEmbeddingIntLinearMap K) (Submodule.restrictScalars ℤ ↑↑I) = traceIdealLattice K I

theorem NumberField.Odlyzko.span_conjugate_traceDual_basisOfFractionalIdeal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Submodule.span ℤ (Set.range fun (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I) => (traceConjugation K) (traceEmbedding K ((basisOfFractionalIdeal K I).traceDual i))) = conjugateTraceIdealLattice K (traceDualIdealUnit K I)

theorem NumberField.Odlyzko.dualLattice_traceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : dualLattice (traceIdealLattice K I) = conjugateTraceIdealLattice K (traceDualIdealUnit K I)