TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.extendByZero {α : Type u_1} {β : Type u_2} {E : Type u_3} [AddCommMonoid E] (e : α → β) (f : α → E) (b : β) : E

An extend by zero used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.extendByZero e f b = Function.extend e f 0 b

theorem NumberField.Odlyzko.extendByZero_apply {α : Type u_1} {β : Type u_2} {E : Type u_3} [AddCommMonoid E] (e : α → β) (he : Function.Injective e) (f : α → E) (a : α) : extendByZero e f (e a) = f a

theorem NumberField.Odlyzko.extendByZero_eq_zero_of_not_mem_range {α : Type u_1} {β : Type u_2} {E : Type u_3} [AddCommMonoid E] (e : α → β) (f : α → E) {b : β} (hb : b ∉ Set.range e) : extendByZero e f b = 0

theorem NumberField.Odlyzko.hasSum_extendByZero {α : Type u_1} {β : Type u_2} {E : Type u_3} [AddCommMonoid E] [TopologicalSpace E] (e : α → β) (he : Function.Injective e) {f : α → E} {a : E} (hf : HasSum f a) : HasSum (extendByZero e f) a

theorem NumberField.Odlyzko.summable_extendByZero {α : Type u_1} {β : Type u_2} {E : Type u_3} [AddCommMonoid E] [TopologicalSpace E] (e : α → β) (he : Function.Injective e) {f : α → E} (hf : Summable f) : Summable (extendByZero e f)

theorem NumberField.Odlyzko.absNorm_idealOfPrimeFactors (K : Type u_1) [Field K] [NumberField K] (m : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : Ideal.absNorm ↑(idealOfPrimeFactors K m) = (Multiset.map (primeIdealNorm K) m).prod

theorem NumberField.Odlyzko.inverseNormPower_idealOfPrimeFactors (K : Type u_1) [Field K] [NumberField K] (m : Multiset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℂ) : ↑(Ideal.absNorm ↑(idealOfPrimeFactors K m)) ^ (-s) = (Multiset.map (fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => inverseNormPower (primeIdealNorm K P) s) m).prod

theorem NumberField.Odlyzko.inverseNormPower_nonzeroIdealEquivPrimeFactors (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) (s : ℂ) : ↑(Ideal.absNorm ↑I) ^ (-s) = (Multiset.map (fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => inverseNormPower (primeIdealNorm K P) s) ((nonzeroIdealEquivPrimeFactors K) I)).prod

noncomputable def NumberField.Odlyzko.primeValueHom {M : Type u_1} [CommMonoidWithZero M] (a : ℕ → M) : ℕ →*₀ M

A prime value hom used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.primeValueHom a = { toFun := fun (n : ℕ) => if n = 0 then 0 else n.factorization.prod fun (p e : ℕ) => a p ^ e, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NumberField.Odlyzko.primeValueHom_one {M : Type u_1} [CommMonoidWithZero M] (a : ℕ → M) : (primeValueHom a) 1 = 1

@[simp]

theorem NumberField.Odlyzko.primeValueHom_apply_of_prime {M : Type u_1} [CommMonoidWithZero M] (a : ℕ → M) {p : ℕ} (hp : Nat.Prime p) : (primeValueHom a) p = a p

@[simp]

theorem NumberField.Odlyzko.primeValueHom_apply_prime_subtype {M : Type u_1} [CommMonoidWithZero M] (a : ℕ → M) (p : Nat.Primes) : (primeValueHom a) ↑p = a ↑p

theorem NumberField.Odlyzko.primeValueHom_multiset_prod_of_prime {M : Type u_1} [CommMonoidWithZero M] (a : ℕ → M) {m : Multiset ℕ} (hm : ∀ p ∈ m, Nat.Prime p) : (primeValueHom a) m.prod = (Multiset.map a m).prod

instance NumberField.Odlyzko.countableIdealRingOfIntegers (K : Type u_1) [Field K] [NumberField K] : Countable (Ideal (RingOfIntegers K))

instance NumberField.Odlyzko.countableHeightOneSpectrum (K : Type u_1) [Field K] [NumberField K] : Countable (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

@[instance_reducible]

noncomputable instance NumberField.Odlyzko.encodableHeightOneSpectrum (K : Type u_1) [Field K] [NumberField K] : Encodable (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

Equations

• NumberField.Odlyzko.encodableHeightOneSpectrum K = Encodable.ofCountable (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

noncomputable def NumberField.Odlyzko.primeIdealCode (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : ℕ

A prime ideal code used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.primeIdealCode K P = Nat.nth Nat.Prime (Encodable.encode P)

theorem NumberField.Odlyzko.prime_primeIdealCode (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : Nat.Prime (primeIdealCode K P)

theorem NumberField.Odlyzko.primeIdealCode_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective (primeIdealCode K)

noncomputable def NumberField.Odlyzko.primeIdealCodeEmbedding (K : Type u_1) [Field K] [NumberField K] : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) ↪ Nat.Primes

A prime ideal code embedding used in the Odlyzko-bound argument.

Equations

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

noncomputable def NumberField.Odlyzko.idealPrimeCode (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) : ℕ

An ideal prime code used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.idealPrimeCode K I = (Multiset.map (NumberField.Odlyzko.primeIdealCode K) (NumberField.Odlyzko.idealPrimeFactors K I)).prod

theorem NumberField.Odlyzko.prime_mem_idealPrimeCode_factors (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) (p : ℕ) : p ∈ Multiset.map (primeIdealCode K) (idealPrimeFactors K I) → Nat.Prime p

theorem NumberField.Odlyzko.normalizedFactors_idealPrimeCode (K : Type u_1) [Field K] [NumberField K] (I : NonzeroIdeal K) : UniqueFactorizationMonoid.normalizedFactors (idealPrimeCode K I) = Multiset.map (primeIdealCode K) (idealPrimeFactors K I)

theorem NumberField.Odlyzko.idealPrimeCode_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective (idealPrimeCode K)

noncomputable def NumberField.Odlyzko.primeIdealAtCode (K : Type u_1) [Field K] [NumberField K] (p : ℕ) : Option (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

A prime ideal at code used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.primeIdealAtCode_eq_some_iff (K : Type u_1) [Field K] [NumberField K] {p : ℕ} {P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} : primeIdealAtCode K p = some P ↔ primeIdealCode K P = p

@[simp]

theorem NumberField.Odlyzko.primeIdealAtCode_primeIdealCode (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : primeIdealAtCode K (primeIdealCode K P) = some P

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

An encoded prime ideal weight used in the Odlyzko-bound argument.

Equations

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

@[simp]

theorem NumberField.Odlyzko.encodedPrimeIdealWeight_primeIdealCode (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : encodedPrimeIdealWeight K s (primeIdealCode K P) = inverseNormPower (primeIdealNorm K P) s

theorem NumberField.Odlyzko.encodedPrimeIdealWeight_ne_zero_iff (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (p : ℕ) : encodedPrimeIdealWeight K s p ≠ 0 ↔ ∃ (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), primeIdealCode K P = p

noncomputable def NumberField.Odlyzko.encodedIdealSummand (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℕ →*₀ ℂ

An encoded ideal summand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.encodedIdealSummand K s = NumberField.Odlyzko.primeValueHom (NumberField.Odlyzko.encodedPrimeIdealWeight K s)

theorem NumberField.Odlyzko.encodedIdealSummand_idealPrimeCode (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (I : NonzeroIdeal K) : (encodedIdealSummand K s) (idealPrimeCode K I) = ↑(Ideal.absNorm ↑I) ^ (-s)

theorem NumberField.Odlyzko.exists_idealPrimeCode_eq_of_primeFactors (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : n ≠ 0) (hcodes : ∀ p ∈ ↑n.primeFactorsList, ∃ (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), primeIdealCode K P = p) : ∃ (I : NonzeroIdeal K), idealPrimeCode K I = n

theorem NumberField.Odlyzko.exists_idealPrimeCode_eq_of_encodedIdealSummand_ne_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) {n : ℕ} (hn : (encodedIdealSummand K s) n ≠ 0) : ∃ (I : NonzeroIdeal K), idealPrimeCode K I = n

theorem NumberField.Odlyzko.encodedIdealSummand_ne_zero_iff (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (n : ℕ) : (encodedIdealSummand K s) n ≠ 0 ↔ ∃ (I : NonzeroIdeal K), idealPrimeCode K I = n

theorem NumberField.Odlyzko.summable_nonzeroIdeal_norm_inverseNormPower (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable fun (I : NonzeroIdeal K) => ‖↑(Ideal.absNorm ↑I) ^ (-s)‖

theorem NumberField.Odlyzko.norm_encodedIdealSummand_eq_extendByZero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : (fun (n : ℕ) => ‖(encodedIdealSummand K s) n‖) = extendByZero (idealPrimeCode K) fun (I : NonzeroIdeal K) => ‖↑(Ideal.absNorm ↑I) ^ (-s)‖

theorem NumberField.Odlyzko.summable_norm_encodedIdealSummand (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : Summable fun (n : ℕ) => ‖(encodedIdealSummand K s) n‖

theorem NumberField.Odlyzko.encodedIdealSummand_eq_extendByZero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ⇑(encodedIdealSummand K s) = extendByZero (idealPrimeCode K) fun (I : NonzeroIdeal K) => ↑(Ideal.absNorm ↑I) ^ (-s)

theorem NumberField.Odlyzko.hasSum_encodedIdealSummand (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasSum (⇑(encodedIdealSummand K s)) (dedekindZeta K s)

noncomputable def NumberField.Odlyzko.encodedIdealFactor (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (p : Nat.Primes) : ℂ

An encoded ideal factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.encodedIdealFactor K s p = (1 - (NumberField.Odlyzko.encodedIdealSummand K s) ↑p)⁻¹

theorem NumberField.Odlyzko.encodedIdealFactor_primeIdealCode (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : encodedIdealFactor K s ((primeIdealCodeEmbedding K) P) = primeIdealFactor K P s

theorem NumberField.Odlyzko.encodedIdealFactor_eq_one_of_not_mem_range (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (p : Nat.Primes) (hp : p ∉ Set.range ⇑(primeIdealCodeEmbedding K)) : encodedIdealFactor K s p = 1

theorem NumberField.Odlyzko.dedekindZeta_primeIdeal_eulerProduct_hasProd (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : HasProd (fun (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => primeIdealFactor K P s) (dedekindZeta K s)

theorem NumberField.Odlyzko.dedekindZeta_primeIdeal_eulerProduct_tprod (K : Type u_1) [Field K] [NumberField K] {s : ℂ} (hs : 1 < s.re) : ∏' (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), primeIdealFactor K P s = dedekindZeta K s