TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.classIdealNormCount (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) (n : ℕ) : ℕ

A class ideal norm count used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.classIdealNormCount K C n = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ClassGroup.mk0 I = C ∧ Ideal.absNorm ↑I = n }

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

A partial dedekind zeta used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.partialDedekindZeta K C s = LSeries (fun (n : ℕ) => ↑(NumberField.Odlyzko.classIdealNormCount K C n)) s

theorem NumberField.Odlyzko.sum_classIdealNormCount (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : n ≠ 0) : ∑ C : ClassGroup (RingOfIntegers K), classIdealNormCount K C n = idealNormCount K n

theorem NumberField.Odlyzko.classIdealNormCount_le_idealNormCount (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) (n : ℕ) : classIdealNormCount K C n ≤ idealNormCount K n

theorem NumberField.Odlyzko.lSeriesSummable_classIdealNormCount (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(classIdealNormCount K C n)) s

theorem NumberField.Odlyzko.hasSum_inverseIdealClass_inverseNormPower (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (I : { I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K))) // ClassGroup.mk0 I = C }) => ↑(Ideal.absNorm ↑↑I) ^ (-s)) (partialDedekindZeta K C s)

theorem NumberField.Odlyzko.sum_partialDedekindZeta (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∑ C : ClassGroup (RingOfIntegers K), partialDedekindZeta K C s = dedekindZeta K s

@[reducible, inline]

abbrev NumberField.Odlyzko.PrincipalIdealAbove (K : Type u_1) [Field K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Type u_1

A principal ideal above used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.PrincipalIdealAbove K J = { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I }

@[reducible, inline]

abbrev NumberField.Odlyzko.InverseIdealClass (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : Type u_1

An inverse ideal class used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.InverseIdealClass K J = { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ }

noncomputable def NumberField.Odlyzko.inverseIdealClassEquivPrincipalIdealAbove (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : InverseIdealClass K J ≃ PrincipalIdealAbove K J

An inverse ideal class equiv principal ideal above used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.absNorm_inverseIdealClassEquivPrincipalIdealAbove (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (I : InverseIdealClass K J) : Ideal.absNorm ↑↑((inverseIdealClassEquivPrincipalIdealAbove K J) I) = Ideal.absNorm ↑J * Ideal.absNorm ↑↑I

theorem NumberField.Odlyzko.hasSum_principalIdealAbove_inverseNormPower (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (I : PrincipalIdealAbove K J) => ↑(Ideal.absNorm ↑↑I) ^ (-s)) (principalIdealZeta K J s)

theorem NumberField.Odlyzko.principalIdealZeta_eq_inverseNormPower_mul_partialDedekindZeta (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : principalIdealZeta K J s = ↑(Ideal.absNorm ↑J) ^ (-s) * partialDedekindZeta K (ClassGroup.mk0 J)⁻¹ s

noncomputable def NumberField.Odlyzko.inverseClassIdealRepresentative (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))

An inverse class ideal representative used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.inverseClassIdealRepresentative K C = Classical.choose ⋯

@[simp]

theorem NumberField.Odlyzko.mk0_inverseClassIdealRepresentative (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) : ClassGroup.mk0 (inverseClassIdealRepresentative K C) = C⁻¹

theorem NumberField.Odlyzko.partialDedekindZeta_eq_normalized_fundamentalConeZeta_of_mk0 (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (hJ : ClassGroup.mk0 J = C⁻¹) {s : ℂ} (hs : 1 < s.re) : partialDedekindZeta K C s = (↑(Units.torsionOrder K))⁻¹ * ↑(Ideal.absNorm ↑J) ^ s * fundamentalConeZeta K J s

theorem NumberField.Odlyzko.partialDedekindZeta_eq_normalized_fundamentalConeZeta (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) {s : ℂ} (hs : 1 < s.re) : partialDedekindZeta K C s = (↑(Units.torsionOrder K))⁻¹ * ↑(Ideal.absNorm ↑(inverseClassIdealRepresentative K C)) ^ s * fundamentalConeZeta K (inverseClassIdealRepresentative K C) s

theorem NumberField.Odlyzko.sum_normalized_fundamentalConeZeta (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∑ C : ClassGroup (RingOfIntegers K), (↑(Units.torsionOrder K))⁻¹ * ↑(Ideal.absNorm ↑(inverseClassIdealRepresentative K C)) ^ s * fundamentalConeZeta K (inverseClassIdealRepresentative K C) s = dedekindZeta K s