TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.radialLogVector (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : mixedEmbedding.realSpace K

A radial log vector used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.radialLogVector K t w = if w = NumberField.Units.dirichletUnitTheorem.w₀ then t else 0

@[simp]

theorem NumberField.Odlyzko.radialLogVector_apply_w₀ (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : radialLogVector K t Units.dirichletUnitTheorem.w₀ = t

theorem NumberField.Odlyzko.radialLogVector_neg (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : radialLogVector K (-t) = -radialLogVector K t

theorem NumberField.Odlyzko.fractionalShapeCovolumeConstant_pos (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : 0 < fractionalShapeCovolumeConstant K I

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

A fractional shape covolume center used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fractionalShapeCovolumeCenter K I = -Real.log (NumberField.Odlyzko.fractionalShapeCovolumeConstant K I) / ↑(Module.finrank ℚ K)

theorem NumberField.Odlyzko.fractionalShapeCovolumeCenter_traceDual (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : fractionalShapeCovolumeCenter K (traceDualIdealUnit K I) = -fractionalShapeCovolumeCenter K I

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

A centered fractional shape coordinates used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredFractionalShapeCoordinates K I y = y + NumberField.Odlyzko.radialLogVector K (NumberField.Odlyzko.fractionalShapeCovolumeCenter K I)

theorem NumberField.Odlyzko.centeredFractionalShapeCoordinates_traceDual_neg (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) : centeredFractionalShapeCoordinates K (traceDualIdealUnit K I) (-y) = -centeredFractionalShapeCoordinates K I y

theorem NumberField.Odlyzko.covolume_shapeIdealLattice_centered (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 (centeredFractionalShapeCoordinates K I y)) ⋯) MeasureTheory.volume = Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))

theorem NumberField.Odlyzko.fractionalShapeIdealTheta_centered_poisson (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 (centeredFractionalShapeCoordinates K I y)) ⋯ = (Real.exp (y Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))).toNNReal⁻¹ • fractionalShapeIdealTheta K (traceDualIdealUnit K I) (↑mixedEmbedding.fundamentalCone.expMapBasis (centeredFractionalShapeCoordinates K (traceDualIdealUnit K I) (-y))) ⋯