TODO: Add doc-string.

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

A centered numerator translation used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.fractionalShapeCovolumeConstant_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : fractionalShapeCovolumeConstant K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) = fractionalShapeCovolumeConstant K I * Real.exp (denominatorLogCoordinates K I Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))

theorem NumberField.Odlyzko.fractionalShapeCovolumeCenter_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : fractionalShapeCovolumeCenter K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) = fractionalShapeCovolumeCenter K I - denominatorLogCoordinates K I Units.dirichletUnitTheorem.w₀

theorem NumberField.Odlyzko.centeredNumeratorTranslation_apply_w₀ (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : centeredNumeratorTranslation K I Units.dirichletUnitTheorem.w₀ = 0

theorem NumberField.Odlyzko.centeredFractionalShapeCoordinates_numerator (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (y : mixedEmbedding.realSpace K) : centeredFractionalShapeCoordinates K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) (y + centeredNumeratorTranslation K I) = centeredFractionalShapeCoordinates K I y - denominatorLogCoordinates K I

theorem NumberField.Odlyzko.centeredNonzeroFractionalShapeThetaMellinKernel_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (y : mixedEmbedding.realSpace K) : centeredNonzeroFractionalShapeThetaMellinKernel K I s y = centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) s (y + centeredNumeratorTranslation K I)

theorem NumberField.Odlyzko.centeredPositiveClassThetaIntegral_eq_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : centeredPositiveClassThetaIntegral K I s = centeredPositiveClassThetaIntegral K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) s

theorem NumberField.Odlyzko.setIntegral_centeredNonzeroFractionalShapeThetaMellinKernel_eq_numerator (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, centeredNonzeroFractionalShapeThetaMellinKernel K I s y = ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) (fractionalIdealNumerator K I)) s y

theorem NumberField.Odlyzko.integrableOn_centeredNonzeroFractionalShapeThetaMellinKernel (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {s : ℂ} (hs : 1 < s.re) : MeasureTheory.IntegrableOn (centeredNonzeroFractionalShapeThetaMellinKernel K I s) (unitFundamentalParamSet K) MeasureTheory.volume