TODO: Add doc-string.

theorem NumberField.Odlyzko.logarithmicMellinWeight_covolumeCenter (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : logarithmicMellinWeight K s (radialLogVector K (fractionalShapeCovolumeCenter K I)) = ↑(fractionalShapeCovolumeConstant K I) ^ (-s)

theorem NumberField.Odlyzko.ofReal_sqrt_cpow {x : ℝ} (hx : 0 < x) (s : ℂ) : ↑√x ^ s = ↑x ^ (s / 2)

theorem NumberField.Odlyzko.fractionalShapeCovolumeConstant_mk0_cpow (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) : ↑(fractionalShapeCovolumeConstant K ((FractionalIdeal.mk0 K) J)) ^ s = CompletedZeta.discriminantFactor K s * ↑(Ideal.absNorm ↑J) ^ s

theorem NumberField.Odlyzko.centeredNonzeroFractionalShapeThetaMellinKernel_eq_covolume_mul (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (y : mixedEmbedding.realSpace K) : centeredNonzeroFractionalShapeThetaMellinKernel K I s y = ↑(fractionalShapeCovolumeConstant K I) ^ s * nonzeroFractionalShapeThetaMellinKernel K I s (centeredFractionalShapeCoordinates K I y)

theorem NumberField.Odlyzko.nonzeroFractionalShapeThetaMellinKernel_vadd_unitCoordinateLattice (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) (g : ↥unitCoordinateLattice) (y : mixedEmbedding.realSpace K) : nonzeroFractionalShapeThetaMellinKernel K I s (↑g + y) = nonzeroFractionalShapeThetaMellinKernel K I s y

theorem NumberField.Odlyzko.nonzeroFractionalShapeThetaMellinKernel_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) (y : mixedEmbedding.realSpace K) : nonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) J) s y = nonzeroShapeThetaMellinKernel K J s y

theorem NumberField.Odlyzko.setIntegral_centeredNonzeroFractionalShapeThetaMellinKernel (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 = ↑(fractionalShapeCovolumeConstant K I) ^ s * ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, nonzeroFractionalShapeThetaMellinKernel K I s y

theorem NumberField.Odlyzko.integrableOn_centeredNonzeroFractionalShapeThetaMellinKernel_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : MeasureTheory.IntegrableOn (centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) J) s) (unitFundamentalParamSet K) MeasureTheory.volume

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

A centered class 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_centered (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (C : ClassGroup (RingOfIntegers K)) (s : ℂ) : classCompletedThetaIntegral K C s = centeredClassThetaIntegral K C s

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

noncomputable def NumberField.Odlyzko.centeredPositiveClassThetaIntegral (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : ℂ

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

Equations

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

noncomputable def NumberField.Odlyzko.centeredClassThetaPoleTerm (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℂ

A centered class theta pole term used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.centeredClassThetaPoleTerm K s = -1 / (↑(Module.finrank ℚ K) * (1 - s)) - 1 / (↑(Module.finrank ℚ K) * s)

noncomputable def NumberField.Odlyzko.centeredRadiallyContinuedClassThetaIntegral (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : ℂ

A centered radially continued class theta integral used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.setIntegral_negative_centeredNonzeroFractionalShapeThetaMellinKernel (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : ∫ (y : mixedEmbedding.realSpace K) in negativeUnitFundamentalParamSet, centeredNonzeroFractionalShapeThetaMellinKernel K I s y = ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, centeredNonzeroFractionalShapeThetaMellinKernel K (traceDualIdealUnit K I) (1 - s) y + centeredClassThetaPoissonCorrection K s y

theorem NumberField.Odlyzko.setIntegral_centeredClassThetaPoissonCorrection_eq_poleTerm (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∫ (y : mixedEmbedding.realSpace K) in positiveUnitFundamentalParamSet, centeredClassThetaPoissonCorrection K s y = centeredClassThetaPoleTerm K s

theorem NumberField.Odlyzko.setIntegral_centered_eq_radiallyContinued_mk0 (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) J) s y = centeredRadiallyContinuedClassThetaIntegral K ((FractionalIdeal.mk0 K) J) s

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

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

Equations

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

theorem NumberField.Odlyzko.centeredClassThetaIntegral_eq_continued (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (C : ClassGroup (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : centeredClassThetaIntegral K C s = centeredContinuedClassThetaIntegral K C s

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