TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.shapeThetaIntegralConstant (K : Type u_1) [Field K] [NumberField K] : ℝ

A shape theta integral constant used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.shapeThetaIntegralConstant K = 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * NumberField.Units.regulator K

noncomputable def NumberField.Odlyzko.classCompletedThetaIntegral (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) (s : ℂ) : ℂ

A class completed theta integral used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.classCompletedThetaIntegral_eq_fundamentalConeZeta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (C : ClassGroup (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : classCompletedThetaIntegral K C s = CompletedZeta.discriminantFactor K s * (↑(Units.torsionOrder K))⁻¹ * ↑(Ideal.absNorm ↑(inverseClassIdealRepresentative K C)) ^ s * (CompletedZeta.complexPlaceGammaFactor s ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K (inverseClassIdealRepresentative K C) s)

theorem NumberField.Odlyzko.sum_classCompletedThetaIntegral (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : ∑ C : ClassGroup (RingOfIntegers K), classCompletedThetaIntegral K C s = CompletedZeta.completed K s