Every local root correction is a polynomial with positive value at 1/p

theorem NairTenenbaum.squarefreeRootArithmetic_series (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (squarefreeRootArithmetic Q) p = ↑(1 + Polynomial.C ↑(rootCount Q p) * Polynomial.X)

noncomputable def NairTenenbaum.rootIdealLocalPolynomial (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) (p : ℕ) : Polynomial ℝ

The finite local correction polynomial relating root counts and ideal norms.

Equations

• NairTenenbaum.rootIdealLocalPolynomial K Q p = (1 + Polynomial.C ↑(NairTenenbaum.rootCount Q p) * Polynomial.X) * NairTenenbaum.idealLocalEulerPolynomial K p

theorem NairTenenbaum.rootIdealCorrection_series_eq_polynomial (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (rootIdealCorrection K Q) p = ↑(rootIdealLocalPolynomial K Q p)

theorem NairTenenbaum.rootIdealCorrection_prime_pow_eq_coeff (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : (rootIdealCorrection K Q) (p ^ k) = (rootIdealLocalPolynomial K Q p).coeff k

theorem NairTenenbaum.idealLocalEulerPolynomial_eval_pos (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : 0 < Polynomial.eval (1 / ↑p) (idealLocalEulerPolynomial K p)

theorem NairTenenbaum.rootIdealLocalPolynomial_eval_pos (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : 0 < Polynomial.eval (1 / ↑p) (rootIdealLocalPolynomial K Q p)

theorem NairTenenbaum.rootIdealCorrection_local_abs_summable (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : Summable fun (k : ℕ) => |(rootIdealCorrection K Q) (p ^ k)| / ↑p ^ k

theorem NairTenenbaum.rootIdealCorrection_local_sum_eq_eval (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : ∑' (k : ℕ), (rootIdealCorrection K Q) (p ^ k) / ↑p ^ k = Polynomial.eval (1 / ↑p) (rootIdealLocalPolynomial K Q p)

theorem NairTenenbaum.rootIdealCorrection_local_sum_pos (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : 0 < ∑' (k : ℕ), (rootIdealCorrection K Q) (p ^ k) / ↑p ^ k