Comparison of the weighted prime-root sum with ideal von Mangoldt sums

Eventual agreement of prime counts leaves a fixed finite exceptional-prime contribution. Nonnegativity then permits enlarging the ideal-prime sum to all positive integers.

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

The reciprocal sum weighted by the ideal von Mangoldt function.

Equations

• NairTenenbaum.idealMangoldtReciprocalSum K x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (NairTenenbaum.idealVonMangoldt K) n / ↑n

theorem NairTenenbaum.primeRootLogSum_le_idealMangoldt_add (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) (x : ℝ) : primeRootLogSum Q x ≤ idealMangoldtReciprocalSum K x + primeRootLogSum Q ↑N

theorem NairTenenbaum.exists_primeRootLogSum_idealMangoldt_bound (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), primeRootLogSum Q x ≤ idealMangoldtReciprocalSum K x + C