The quantitative ideal-counting estimate

Summing the power-saving counts over the finite class group gives a linear main term. The established qualitative mean identifies its coefficient with the positive Dedekind zeta residue.

noncomputable def NairTenenbaum.nonzeroIdealNormCount (K : Type u_1) [Field K] [NumberField K] (x : ℝ) : ℕ

The count of nonzero integral ideals below a real norm cutoff.

Equations

• NairTenenbaum.nonzeroIdealNormCount K x = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x }

theorem NairTenenbaum.nonzeroIdealNormCount_eq_sum_classes (K : Type u_1) [Field K] [NumberField K] {x : ℝ} (hx : 0 ≤ x) : nonzeroIdealNormCount K x = ∑ A : ClassGroup (NumberField.RingOfIntegers K), idealClassNormCount K A x

theorem NairTenenbaum.exists_nonzeroIdealNormCount_power_error (K : Type u_1) [Field K] [NumberField K] : ∃ (V : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |↑(nonzeroIdealNormCount K x) - V * x| ≤ C * x ^ numberFieldCountingExponent K

theorem NairTenenbaum.sum_idealNormCount_eq_nonzero_count (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ∑ k ∈ Finset.Icc 1 n, idealNormCount K k = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // Ideal.absNorm ↑I ≤ n }

theorem NairTenenbaum.arithmeticSummatory_idealNormArithmetic_eq (K : Type u_1) [Field K] [NumberField K] {x : ℝ} (hx : 0 ≤ x) : arithmeticSummatory (⇑(idealNormArithmetic K)) x = ↑(nonzeroIdealNormCount K x)

theorem NairTenenbaum.exists_idealNormArithmetic_power_error (K : Type u_1) [Field K] [NumberField K] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |arithmeticSummatory (⇑(idealNormArithmetic K)) x - NumberField.dedekindZeta_residue K * x| ≤ C * x ^ numberFieldCountingExponent K