The ideal-norm series is bounded by the root Euler exponential

noncomputable def NairTenenbaum.idealsOfNorm {K : Type u_1} [Field K] [NumberField K] (n : ℕ) : Finset (Ideal (NumberField.RingOfIntegers K))

The finite set of integral ideals with a specified absolute norm.

Equations

• NairTenenbaum.idealsOfNorm n = ⋯.toFinset

@[simp]

theorem NairTenenbaum.mem_idealsOfNorm {K : Type u_1} [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) (n : ℕ) : I ∈ idealsOfNorm n ↔ Ideal.absNorm I = n

theorem NairTenenbaum.card_idealsOfNorm {K : Type u_1} [Field K] [NumberField K] (n : ℕ) : (idealsOfNorm n).card = idealNormCount K n

theorem NairTenenbaum.idealNormCount_sum_eq {K : Type u_1} [Field K] [NumberField K] (T : Finset ℕ) (w : ℕ → ℝ) : ∑ n ∈ T, ↑(idealNormCount K n) * w n = ∑ I ∈ T.biUnion idealsOfNorm, w (Ideal.absNorm I)

noncomputable def NairTenenbaum.idealRootEulerError {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) : ℝ

The local error in comparing root and ideal Euler factors.

Equations

• NairTenenbaum.idealRootEulerError θ = ↑(Module.finrank ℚ K) * (↑(RingOfIntegers.exponent θ).primeFactors.card + 3 * ∑' (n : ℕ), ↑n ^ (-2))

theorem NairTenenbaum.finite_idealNorm_sum_le_root_exp {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (hD : RingOfIntegers.exponent θ ≠ 0) (T : Finset (Ideal (NumberField.RingOfIntegers K))) (hT : ∀ I ∈ T, I ≠ ⊥) {σ : ℝ} (hσ : 1 ≤ σ) (hs : Summable fun (p : Nat.Primes) => ↑(rootCount (minpoly ℤ θ) ↑p) * ↑↑p ^ (-σ)) : ∑ I ∈ T, ↑(Ideal.absNorm I) ^ (-σ) ≤ Real.exp (rootPrimePowerSum (minpoly ℤ θ) σ + idealRootEulerError θ)

theorem NairTenenbaum.idealNormDirichlet_le_root_exp {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (hD : RingOfIntegers.exponent θ ≠ 0) {σ : ℝ} (hσ : 1 < σ) (hs : Summable fun (p : Nat.Primes) => ↑(rootCount (minpoly ℤ θ) ↑p) * ↑↑p ^ (-σ)) : idealNormDirichlet K σ ≤ Real.exp (rootPrimePowerSum (minpoly ℤ θ) σ + idealRootEulerError θ)