The squarefree-root correction to ideal norm counts

The correction is defined by Dirichlet inversion. Its convolution identity is exact; at primes away from the conductor, the linear Euler coefficient vanishes. Absolute summability and positivity of its total are separate analytic tasks.

noncomputable def NairTenenbaum.squarefreeRootArithmetic (Q : Polynomial ℤ) : ArithmeticFunction ℝ

The squarefree-supported arithmetic function of polynomial root counts.

Equations

• NairTenenbaum.squarefreeRootArithmetic Q = { toFun := fun (n : ℕ) => if Squarefree n then ↑(NairTenenbaum.rootCount Q n) else 0, map_zero' := ⋯ }

theorem NairTenenbaum.squarefreeRootArithmetic_nonneg (Q : Polynomial ℤ) (n : ℕ) : 0 ≤ (squarefreeRootArithmetic Q) n

theorem NairTenenbaum.squarefreeRootArithmetic_le_rootCount (Q : Polynomial ℤ) (n : ℕ) : (squarefreeRootArithmetic Q) n ≤ ↑(rootCount Q n)

theorem NairTenenbaum.squarefreeRootArithmetic_isMultiplicative (Q : Polynomial ℤ) : (squarefreeRootArithmetic Q).IsMultiplicative

theorem NairTenenbaum.squarefreeRootArithmetic_prime (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : (squarefreeRootArithmetic Q) p = ↑(rootCount Q p)

theorem NairTenenbaum.arithmeticFunction_mul_prime (f g : ArithmeticFunction ℝ) {p : ℕ} (hp : Nat.Prime p) : (f * g) p = f 1 * g p + f p * g 1

noncomputable def NairTenenbaum.idealNormInverse (K : Type u_1) [Field K] [NumberField K] : ArithmeticFunction ℝ

The Dirichlet-convolution inverse of the ideal-norm counting function.

Equations

• NairTenenbaum.idealNormInverse K = ArithmeticFunction.dirichletInverse (⇑(NairTenenbaum.idealNormArithmetic K)) (⋯.mpr invertibleOne)

theorem NairTenenbaum.idealNormArithmetic_mul_inverse (K : Type u_1) [Field K] [NumberField K] : idealNormArithmetic K * idealNormInverse K = 1

theorem NairTenenbaum.idealNormInverse_isMultiplicative (K : Type u_1) [Field K] [NumberField K] : (idealNormInverse K).IsMultiplicative

noncomputable def NairTenenbaum.rootIdealCorrection (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) : ArithmeticFunction ℝ

The convolution correction between squarefree root counts and ideal-norm counts.

Equations

• NairTenenbaum.rootIdealCorrection K Q = NairTenenbaum.squarefreeRootArithmetic Q * NairTenenbaum.idealNormInverse K

theorem NairTenenbaum.rootIdealCorrection_isMultiplicative (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) : (rootIdealCorrection K Q).IsMultiplicative

theorem NairTenenbaum.rootIdealCorrection_mul_idealNorm (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) : rootIdealCorrection K Q * idealNormArithmetic K = squarefreeRootArithmetic Q

theorem NairTenenbaum.rootIdealCorrection_prime (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) : (rootIdealCorrection K Q) p = ↑(rootCount Q p) - ↑(idealNormCount K p)