TODO: Add doc-string.

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

noncomputable def NumberField.Odlyzko.idealCompletedThetaIntegral (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) : ℂ

An ideal 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.idealCompletedThetaIntegral_eq_fundamentalConeZeta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : idealCompletedThetaIntegral K J s = CompletedZeta.discriminantFactor K s * (↑(Units.torsionOrder K))⁻¹ * ↑(Ideal.absNorm ↑J) ^ s * (CompletedZeta.complexPlaceGammaFactor s ^ InfinitePlace.nrComplexPlaces K * fundamentalConeZeta K J s)

theorem NumberField.Odlyzko.idealCompletedThetaIntegral_eq_centered (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) : idealCompletedThetaIntegral K J s = (↑(Units.torsionOrder K))⁻¹ * 2 ^ InfinitePlace.nrComplexPlaces K * ↑(shapeThetaIntegralConstant K) * ∫ (y : mixedEmbedding.realSpace K) in unitFundamentalParamSet K, centeredNonzeroFractionalShapeThetaMellinKernel K ((FractionalIdeal.mk0 K) J) s y

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

A centered fractional class contribution used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.centeredFractionalClassContribution_eq_partialDedekindZeta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (C : ClassGroup (RingOfIntegers K)) (hI : (ClassGroup.mk K) I = C⁻¹) {s : ℂ} (hs : 1 < s.re) : centeredFractionalClassContribution K I s = CompletedZeta.discriminantFactor K s * CompletedZeta.complexPlaceGammaFactor s ^ InfinitePlace.nrComplexPlaces K * partialDedekindZeta K C s

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

A pole cleared centered fractional class contribution used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.differentiable_poleClearedCenteredFractionalClassContribution (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : Differentiable ℂ (poleClearedCenteredFractionalClassContribution K I)

theorem NumberField.Odlyzko.poleClearedCenteredFractionalClassContribution_eq_of_mk_eq_of_one_lt_re (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I J : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (hIJ : (ClassGroup.mk K) I = (ClassGroup.mk K) J) {s : ℂ} (hs : 1 < s.re) : poleClearedCenteredFractionalClassContribution K I s = poleClearedCenteredFractionalClassContribution K J s

theorem NumberField.Odlyzko.poleClearedCenteredFractionalClassContribution_eq_of_mk_eq (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (I J : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (hIJ : (ClassGroup.mk K) I = (ClassGroup.mk K) J) : poleClearedCenteredFractionalClassContribution K I = poleClearedCenteredFractionalClassContribution K J

theorem NumberField.Odlyzko.poleClearedCenteredClassThetaIntegral_functionalEquation (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : poleClearedCenteredClassThetaIntegral K I s = poleClearedCenteredClassThetaIntegral K (traceDualIdealUnit K I) (1 - s)

theorem NumberField.Odlyzko.poleClearedCenteredFractionalClassContribution_functionalEquation (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (s : ℂ) : poleClearedCenteredFractionalClassContribution K I s = poleClearedCenteredFractionalClassContribution K (traceDualIdealUnit K I) (1 - s)

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

A pole cleared completed dedekind zeta continuation used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.differentiable_poleClearedCompletedDedekindZetaContinuation (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : Differentiable ℂ (poleClearedCompletedDedekindZetaContinuation K)

theorem NumberField.Odlyzko.mk_traceDual_inverseClassIdealRepresentative_eq_reindexed (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) : (ClassGroup.mk K) (traceDualIdealUnit K ((FractionalIdeal.mk0 K) (inverseClassIdealRepresentative K C))) = (ClassGroup.mk K) ((FractionalIdeal.mk0 K) (inverseClassIdealRepresentative K ((traceDualInverseClassEquiv K) C)))

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation_functionalEquation (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (s : ℂ) : poleClearedCompletedDedekindZetaContinuation K s = poleClearedCompletedDedekindZetaContinuation K (1 - s)

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation_eq_completedDedekindZeta (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : 1 < s.re) : poleClearedCompletedDedekindZetaContinuation K s = ↑(Module.finrank ℚ K) * s * (1 - s) * CompletedZeta.completed K s