Local ideal von Mangoldt coefficients

theorem NairTenenbaum.arithmeticPrimeSeries_logWeight (f : ArithmeticFunction ℝ) {p : ℕ} (_hp : Nat.Prime p) : arithmeticPrimeSeries (arithmeticLogWeight f) p = PowerSeries.C (Real.log ↑p) * powerSeriesEulerDerivative (arithmeticPrimeSeries f p)

theorem NairTenenbaum.idealLocalEulerPolynomial_coe (K : Type u_1) [Field K] [NumberField K] {p : ℕ} : ↑(idealLocalEulerPolynomial K p) = ∏ P : ↥(primeIdealSupport K p), (1 - PowerSeries.X ^ (↑P).inertiaDeg ℤ)

theorem NairTenenbaum.idealNormArithmetic_series_eq_geometric_product (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (idealNormArithmetic K) p = ∏ P : ↥(primeIdealSupport K p), weightedGeometricSeries ((↑P).inertiaDeg ℤ) ⋯

theorem NairTenenbaum.idealVonMangoldt_series (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (idealVonMangoldt K) p = PowerSeries.C (Real.log ↑p) * ∑ P : ↥(primeIdealSupport K p), ↑((↑P).inertiaDeg ℤ) * (weightedGeometricSeries ((↑P).inertiaDeg ℤ) ⋯ - 1)

theorem NairTenenbaum.idealVonMangoldt_prime_pow (K : Type u_1) [Field K] [NumberField K] {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : (idealVonMangoldt K) (p ^ k) = Real.log ↑p * ∑ P : ↥(primeIdealSupport K p), if (↑P).inertiaDeg ℤ ∣ k then ↑((↑P).inertiaDeg ℤ) else 0

theorem NairTenenbaum.idealVonMangoldt_prime_pow_nonneg (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : 0 ≤ (idealVonMangoldt K) (p ^ k)

theorem NairTenenbaum.idealVonMangoldt_prime_pow_le (K : Type u_1) [Field K] [NumberField K] {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : (idealVonMangoldt K) (p ^ k) ≤ ↑(Module.finrank ℚ K) * Real.log ↑p