TODO: Add doc-string.

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

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

Equations

• NumberField.Odlyzko.traceToEuclidean K = (NumberField.Odlyzko.traceToMixed K).trans (NumberField.mixedEmbedding.euclidean.toMixed K).symm

theorem NumberField.Odlyzko.traceIdealLattice_eq_comap_euclideanIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : traceIdealLattice K I = ZLattice.comap ℝ (euclideanIdealLattice K I) ↑↑(traceToEuclidean K)

theorem NumberField.Odlyzko.covolume_comap_continuousLinearEquiv {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (e : E ≃L[ℝ] E) : ZLattice.covolume (ZLattice.comap ℝ L ↑↑e) μ = |LinearMap.det ↑↑e|⁻¹ * ZLattice.covolume L μ

theorem NumberField.Odlyzko.covolume_traceIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ZLattice.covolume (traceIdealLattice K I) MeasureTheory.volume = ↑(FractionalIdeal.absNorm ↑I) * √|↑(discr K)|

noncomputable def NumberField.Odlyzko.radialMixedSpaceUnit (K : Type u_1) [Field K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : (mixedEmbedding.mixedSpace K)ˣ

A radial mixed space unit used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.radialMixedSpaceUnit_val (K : Type u_1) [Field K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ↑(radialMixedSpaceUnit K q hq) = mixedEmbedding.mixedSpaceOfRealSpace q

noncomputable def NumberField.Odlyzko.traceRadialScale (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : mixedEmbedding.euclidean.mixedSpace K ≃L[ℝ] mixedEmbedding.euclidean.mixedSpace K

A trace radial scale used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.traceToMixed_traceRadialScale (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v : mixedEmbedding.euclidean.mixedSpace K) : (traceToMixed K) ((traceRadialScale K q hq) v) = mixedEmbedding.mixedSpaceOfRealSpace q * (traceToMixed K) v

theorem NumberField.Odlyzko.inner_traceRadialScale (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v z : mixedEmbedding.euclidean.mixedSpace K) : inner ℝ ((traceRadialScale K q hq) v) z = inner ℝ v ((traceRadialScale K q hq) z)

theorem NumberField.Odlyzko.traceRadialScale_symm_apply (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v : mixedEmbedding.euclidean.mixedSpace K) : (traceRadialScale K q hq).symm v = (traceRadialScale K (fun (w : InfinitePlace K) => (q w)⁻¹) ⋯) v

theorem NumberField.Odlyzko.traceConjugation_traceRadialScale (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v : mixedEmbedding.euclidean.mixedSpace K) : (traceConjugation K) ((traceRadialScale K q hq) v) = (traceRadialScale K q hq) ((traceConjugation K) v)

noncomputable def NumberField.Odlyzko.shapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : Submodule ℤ (mixedEmbedding.euclidean.mixedSpace K)

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

Equations

• NumberField.Odlyzko.shapeIdealLattice K I q hq = ZLattice.comap ℝ (NumberField.Odlyzko.traceIdealLattice K I) ↑↑(NumberField.Odlyzko.traceRadialScale K q hq).symm

instance NumberField.Odlyzko.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntShapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : DiscreteTopology ↥(shapeIdealLattice K I q hq)

instance NumberField.Odlyzko.instIsZLatticeRealMixedSpaceShapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : IsZLattice ℝ (shapeIdealLattice K I q hq)

noncomputable def NumberField.Odlyzko.conjugateShapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : Submodule ℤ (mixedEmbedding.euclidean.mixedSpace K)

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

Equations

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

theorem NumberField.Odlyzko.mem_conjugateShapeIdealLattice_iff (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v : mixedEmbedding.euclidean.mixedSpace K) : v ∈ conjugateShapeIdealLattice K I q hq ↔ (traceConjugation K) v ∈ shapeIdealLattice K I q hq

theorem NumberField.Odlyzko.mem_conjugateTraceIdealLattice_iff (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (v : mixedEmbedding.euclidean.mixedSpace K) : v ∈ conjugateTraceIdealLattice K I ↔ (traceConjugation K) v ∈ traceIdealLattice K I

theorem NumberField.Odlyzko.mem_dualLattice_shapeIdealLattice_iff (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (v : mixedEmbedding.euclidean.mixedSpace K) : v ∈ dualLattice (shapeIdealLattice K I q hq) ↔ (traceRadialScale K q hq) v ∈ dualLattice (traceIdealLattice K I)

theorem NumberField.Odlyzko.dualLattice_shapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : dualLattice (shapeIdealLattice K I q hq) = conjugateShapeIdealLattice K (traceDualIdealUnit K I) (fun (w : InfinitePlace K) => (q w)⁻¹) ⋯

theorem NumberField.Odlyzko.traceRadialScale_traceEmbedding_mem_shapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : K) : (traceRadialScale K q hq) (traceEmbedding K x) ∈ shapeIdealLattice K I q hq ↔ x ∈ ↑I

theorem NumberField.Odlyzko.norm_sq_traceRadialScale_traceEmbedding (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : K) : ‖(traceRadialScale K q hq) (traceEmbedding K x)‖ ^ 2 = 2 * ∑ w : InfinitePlace K, w x ^ 2 * q w ^ 2

theorem NumberField.Odlyzko.complexPlaceGaussian_eq_latticeGaussian (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : K) : complexPlaceGaussian K x q = latticeGaussian Real.pi ((traceRadialScale K q hq) (traceEmbedding K x))

noncomputable def NumberField.Odlyzko.idealElementShapeMap (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : ↥↑J) : ↥(shapeIdealLattice K ((FractionalIdeal.mk0 K) J) q hq)

An ideal element shape map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealElementShapeMap K J q hq x = ⟨(NumberField.Odlyzko.traceRadialScale K q hq) (NumberField.Odlyzko.traceEmbedding K ↑↑x), ⋯⟩

theorem NumberField.Odlyzko.idealElementShapeMap_bijective (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : Function.Bijective (idealElementShapeMap K J q hq)

noncomputable def NumberField.Odlyzko.idealElementShapeEquiv (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ↥↑J ≃ ↥(shapeIdealLattice K ((FractionalIdeal.mk0 K) J) q hq)

An ideal element shape equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealElementShapeEquiv K J q hq = Equiv.ofBijective (NumberField.Odlyzko.idealElementShapeMap K J q hq) ⋯

@[simp]

theorem NumberField.Odlyzko.idealElementShapeEquiv_coe (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : ↥↑J) : ↑((idealElementShapeEquiv K J q hq) x) = (traceRadialScale K q hq) (traceEmbedding K ↑↑x)

noncomputable def NumberField.Odlyzko.shapeIdealTheta (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ℂ

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

Equations

• NumberField.Odlyzko.shapeIdealTheta K J q hq = NumberField.Odlyzko.latticeTheta (NumberField.Odlyzko.shapeIdealLattice K ((FractionalIdeal.mk0 K) J) q hq) Real.pi

theorem NumberField.Odlyzko.shapeIdealTheta_eq_tsum (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : shapeIdealTheta K J q hq = ∑' (x : ↥↑J), complexPlaceGaussian K (↑↑x) q

theorem NumberField.Odlyzko.dualLatticeTheta_shapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : dualLatticeTheta (shapeIdealLattice K I q hq) Real.pi = latticeTheta (shapeIdealLattice K (traceDualIdealUnit K I) (fun (w : InfinitePlace K) => (q w)⁻¹) ⋯) Real.pi

def NumberField.Odlyzko.nonzeroIdealElementEquivSingletonCompl (K : Type u_1) [Field K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : nonzeroIdealElement K J ≃ { x : ↥↑J // x ∉ {0} }

A nonzero ideal element equiv singleton compl used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.shapeIdealTheta_eq_one_add_nonzero (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : shapeIdealTheta K J q hq = 1 + ∑' (x : nonzeroIdealElement K J), complexPlaceGaussian K (↑↑x) q

theorem NumberField.Odlyzko.nonzeroIdealShapeTheta_eq_shapeIdealTheta_sub_one (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (y : mixedEmbedding.realSpace K) : nonzeroIdealShapeTheta K J y = shapeIdealTheta K J (↑mixedEmbedding.fundamentalCone.expMapBasis y) ⋯ - 1

theorem NumberField.Odlyzko.det_radialMixedSpaceUnit (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : LinearMap.det ↑((Units.mulLeftLinearEquiv ℝ (mixedEmbedding.mixedSpace K)) (radialMixedSpaceUnit K q hq)) = (∏ w : { w : InfinitePlace K // w.IsReal }, q ↑w) * ∏ w : { w : InfinitePlace K // w.IsComplex }, q ↑w ^ 2

theorem NumberField.Odlyzko.det_traceRadialScale (K : Type u_1) [Field K] [NumberField K] (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : LinearMap.det ↑↑(traceRadialScale K q hq) = (∏ w : { w : InfinitePlace K // w.IsReal }, q ↑w) * ∏ w : { w : InfinitePlace K // w.IsComplex }, q ↑w ^ 2

theorem NumberField.Odlyzko.covolume_shapeIdealLattice (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ZLattice.covolume (shapeIdealLattice K I q hq) MeasureTheory.volume = |(∏ w : { w : InfinitePlace K // w.IsReal }, q ↑w) * ∏ w : { w : InfinitePlace K // w.IsComplex }, q ↑w ^ 2| * (↑(FractionalIdeal.absNorm ↑I) * √|↑(discr K)|)

theorem NumberField.Odlyzko.expMapBasis_neg (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (y : mixedEmbedding.realSpace K) (w : InfinitePlace K) : ↑mixedEmbedding.fundamentalCone.expMapBasis (-y) w = (↑mixedEmbedding.fundamentalCone.expMapBasis y w)⁻¹

theorem NumberField.Odlyzko.covolume_shapeIdealLattice_expMapBasis (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) : ZLattice.covolume (shapeIdealLattice K I (↑mixedEmbedding.fundamentalCone.expMapBasis y) ⋯) MeasureTheory.volume = Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * (↑(FractionalIdeal.absNorm ↑I) * √|↑(discr K)|)

noncomputable def NumberField.Odlyzko.fractionalIdealElementShapeMap (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : ↥↑↑I) : ↥(shapeIdealLattice K I q hq)

A fractional ideal element shape map used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalIdealElementShapeMap K I q hq x = ⟨(NumberField.Odlyzko.traceRadialScale K q hq) (NumberField.Odlyzko.traceEmbedding K ↑x), ⋯⟩

theorem NumberField.Odlyzko.fractionalIdealElementShapeMap_bijective (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : Function.Bijective (fractionalIdealElementShapeMap K I q hq)

noncomputable def NumberField.Odlyzko.fractionalIdealElementShapeEquiv (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ↥↑↑I ≃ ↥(shapeIdealLattice K I q hq)

A fractional ideal element shape equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalIdealElementShapeEquiv K I q hq = Equiv.ofBijective (NumberField.Odlyzko.fractionalIdealElementShapeMap K I q hq) ⋯

@[simp]

theorem NumberField.Odlyzko.fractionalIdealElementShapeEquiv_coe (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (x : ↥↑↑I) : ↑((fractionalIdealElementShapeEquiv K I q hq) x) = (traceRadialScale K q hq) (traceEmbedding K ↑x)

noncomputable def NumberField.Odlyzko.fractionalShapeIdealTheta (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : ℂ

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

Equations

• NumberField.Odlyzko.fractionalShapeIdealTheta K I q hq = NumberField.Odlyzko.latticeTheta (NumberField.Odlyzko.shapeIdealLattice K I q hq) Real.pi

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_eq_tsum (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : fractionalShapeIdealTheta K I q hq = ∑' (x : ↥↑↑I), complexPlaceGaussian K (↑x) q

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_poissonSummation (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : fractionalShapeIdealTheta K I q hq = (ZLattice.covolume (shapeIdealLattice K I q hq) MeasureTheory.volume).toNNReal⁻¹ • fractionalShapeIdealTheta K (traceDualIdealUnit K I) (fun (w : InfinitePlace K) => (q w)⁻¹) ⋯

noncomputable def NumberField.Odlyzko.fractionalIdealNumerator (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))

A fractional ideal numerator used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalIdealNumerator K I = ⟨(↑I).num, ⋯⟩

theorem NumberField.Odlyzko.mk0_fractionalIdealNumerator (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ClassGroup.mk0 (fractionalIdealNumerator K I) = (ClassGroup.mk K) I

theorem NumberField.Odlyzko.fractionalIdeal_den_ne_zero (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ↑(↑I).den ≠ 0

noncomputable def NumberField.Odlyzko.numeratorRadii (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) : InfinitePlace K → ℝ

A numerator radii used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.numeratorRadii K I q w = q w / w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(↑I).den)

theorem NumberField.Odlyzko.numeratorRadii_ne_zero (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) (w : InfinitePlace K) : numeratorRadii K I q w ≠ 0

theorem NumberField.Odlyzko.complexPlaceGaussian_equivNum (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (x : ↥↑↑I) : complexPlaceGaussian K (↑x) q = complexPlaceGaussian K (↑↑((FractionalIdeal.equivNum ⋯) x)) (numeratorRadii K I q)

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_eq_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (q : InfinitePlace K → ℝ) (hq : ∀ (w : InfinitePlace K), q w ≠ 0) : fractionalShapeIdealTheta K I q hq = shapeIdealTheta K (fractionalIdealNumerator K I) (numeratorRadii K I q) ⋯

noncomputable def NumberField.Odlyzko.denominatorLogCoordinates (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : mixedEmbedding.realSpace K

A denominator log coordinates used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.expMapBasis_denominatorLogCoordinates (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ↑mixedEmbedding.fundamentalCone.expMapBasis (denominatorLogCoordinates K I) = fun (w : InfinitePlace K) => w ((algebraMap (RingOfIntegers K) K) ↑(↑I).den)

theorem NumberField.Odlyzko.expMapBasis_add (K : Type u_1) [Field K] [NumberField K] (x y : mixedEmbedding.realSpace K) : ↑mixedEmbedding.fundamentalCone.expMapBasis (x + y) = ↑mixedEmbedding.fundamentalCone.expMapBasis x * ↑mixedEmbedding.fundamentalCone.expMapBasis y

theorem NumberField.Odlyzko.numeratorRadii_expMapBasis (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) : numeratorRadii K I (↑mixedEmbedding.fundamentalCone.expMapBasis y) = ↑mixedEmbedding.fundamentalCone.expMapBasis (y - denominatorLogCoordinates K I)

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_expMapBasis_eq_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) : fractionalShapeIdealTheta K I (↑mixedEmbedding.fundamentalCone.expMapBasis y) ⋯ = shapeIdealTheta K (fractionalIdealNumerator K I) (↑mixedEmbedding.fundamentalCone.expMapBasis (y - denominatorLogCoordinates K I)) ⋯