The polynomial inverse of the local ideal-counting series

noncomputable def NairTenenbaum.arithmeticPrimeSeries (f : ArithmeticFunction ℝ) (p : ℕ) : PowerSeries ℝ

The power series obtained by restricting an arithmetic function to powers of a prime.

Equations

• NairTenenbaum.arithmeticPrimeSeries f p = PowerSeries.mk fun (k : ℕ) => f (p ^ k)

@[simp]

theorem NairTenenbaum.arithmeticPrimeSeries_coeff (f : ArithmeticFunction ℝ) (p k : ℕ) : (PowerSeries.coeff k) (arithmeticPrimeSeries f p) = f (p ^ k)

theorem NairTenenbaum.arithmeticPrimeSeries_mul (f g : ArithmeticFunction ℝ) {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (f * g) p = arithmeticPrimeSeries f p * arithmeticPrimeSeries g p

@[simp]

theorem NairTenenbaum.arithmeticPrimeSeries_one {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries 1 p = 1

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

The finite polynomial inverse of the local ideal-norm Euler factor.

Equations

• NairTenenbaum.idealLocalEulerPolynomial K p = NairTenenbaum.weightedEulerPolynomial fun (P : ↥(NairTenenbaum.primeIdealSupport K p)) => (↑P).inertiaDeg ℤ

theorem NairTenenbaum.idealNormArithmetic_series_mul_euler (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (idealNormArithmetic K) p * ↑(idealLocalEulerPolynomial K p) = 1

theorem NairTenenbaum.idealNormInverse_series_eq_euler (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : arithmeticPrimeSeries (idealNormInverse K) p = ↑(idealLocalEulerPolynomial K p)