Global bounds for the ideal von Mangoldt function

The local residue-degree formula and prime-power support compare the ideal von Mangoldt function pointwise with the ordinary one. Chebyshev's estimate then gives a linear bound for its summatory function.

theorem NairTenenbaum.idealVonMangoldt_eq_zero_of_not_primePower (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : ¬IsPrimePow n) : (idealVonMangoldt K) n = 0

theorem NairTenenbaum.idealVonMangoldt_nonneg (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : 0 ≤ (idealVonMangoldt K) n

theorem NairTenenbaum.idealVonMangoldt_le_degree_mul (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : (idealVonMangoldt K) n ≤ ↑(Module.finrank ℚ K) * ArithmeticFunction.vonMangoldt n

theorem NairTenenbaum.idealVonMangoldt_summatory_le_psi (K : Type u_1) [Field K] [NumberField K] (x : ℝ) : arithmeticSummatory (⇑(idealVonMangoldt K)) x ≤ ↑(Module.finrank ℚ K) * Chebyshev.psi x

theorem NairTenenbaum.idealVonMangoldt_summatory_le (K : Type u_1) [Field K] [NumberField K] {x : ℝ} (hx : 0 ≤ x) : arithmeticSummatory (⇑(idealVonMangoldt K)) x ≤ ↑(Module.finrank ℚ K) * (Real.log 4 + 4) * x