TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.principalIdealNormCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : ℕ

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

Equations

• NumberField.Odlyzko.principalIdealNormCount K J n = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n }

noncomputable def NumberField.Odlyzko.fundamentalConeNormCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : ℕ

A fundamental cone norm count used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fundamentalConeNormCount K J n = Nat.card { a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) // NumberField.mixedEmbedding.norm ↑a = ↑n }

noncomputable def NumberField.Odlyzko.idealSetIntNorm (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : ℕ

An ideal set int norm used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealSetIntNorm K J a = NumberField.mixedEmbedding.fundamentalCone.intNorm ↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J) a)

noncomputable def NumberField.Odlyzko.idealSetIntNormFiberEquiv (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : { a : ↑(mixedEmbedding.fundamentalCone.idealSet K J) // idealSetIntNorm K J a = n } ≃ { a : ↑(mixedEmbedding.fundamentalCone.idealSet K J) // mixedEmbedding.norm ↑a = ↑n }

An ideal set int norm fiber equiv used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealSetIntNormFiberEquiv K J n = Equiv.subtypeEquivRight ⋯

theorem NumberField.Odlyzko.fundamentalConeNormCount_eq_natCard_idealSetIntNorm (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : fundamentalConeNormCount K J n = Nat.card { a : ↑(mixedEmbedding.fundamentalCone.idealSet K J) // idealSetIntNorm K J a = n }

theorem NumberField.Odlyzko.idealSetIntNorm_ne_zero (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) : idealSetIntNorm K J a ≠ 0

theorem NumberField.Odlyzko.fundamentalConeNormCount_eq_torsion_mul (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : fundamentalConeNormCount K J n = principalIdealNormCount K J n * Units.torsionOrder K

theorem NumberField.Odlyzko.principalIdealNormCount_le_idealNormCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (n : ℕ) : principalIdealNormCount K J n ≤ idealNormCount K n

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

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

Equations

• NumberField.Odlyzko.principalIdealZeta K J s = LSeries (fun (n : ℕ) => ↑(NumberField.Odlyzko.principalIdealNormCount K J n)) s

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

A fundamental cone zeta used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.fundamentalConeZeta K J s = LSeries (fun (n : ℕ) => ↑(NumberField.Odlyzko.fundamentalConeNormCount K J n)) s

theorem NumberField.Odlyzko.lSeriesSummable_principalIdealNormCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(principalIdealNormCount K J n)) s

theorem NumberField.Odlyzko.lSeriesSummable_fundamentalConeNormCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(fundamentalConeNormCount K J n)) s

theorem NumberField.Odlyzko.summable_idealSet_inverseNormPower (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : Summable fun (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) => ↑(idealSetIntNorm K J a) ^ (-s)

theorem NumberField.Odlyzko.hasSum_idealSet_inverseNormPower (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (a : ↑(mixedEmbedding.fundamentalCone.idealSet K J)) => ↑(idealSetIntNorm K J a) ^ (-s)) (fundamentalConeZeta K J s)

theorem NumberField.Odlyzko.fundamentalConeZeta_eq_torsion_mul_principalIdealZeta (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) (s : ℂ) : fundamentalConeZeta K J s = ↑(Units.torsionOrder K) * principalIdealZeta K J s