Logarithmic weighting and Dirichlet convolution

Logarithmic weighting is a derivation for Dirichlet convolution. The ideal von Mangoldt function is the logarithmically weighted ideal count convolved with its proved Dirichlet inverse.

noncomputable def NairTenenbaum.arithmeticLogWeight (f : ArithmeticFunction ℝ) : ArithmeticFunction ℝ

The arithmetic weight obtained by multiplying each value by the logarithm of its index.

Equations

• NairTenenbaum.arithmeticLogWeight f = f.pmul ArithmeticFunction.log

@[simp]

theorem NairTenenbaum.arithmeticLogWeight_apply (f : ArithmeticFunction ℝ) (n : ℕ) : (arithmeticLogWeight f) n = f n * Real.log ↑n

noncomputable def NairTenenbaum.arithmeticLogDerivative (f g : ArithmeticFunction ℝ) : ArithmeticFunction ℝ

Logarithmic differentiation of an arithmetic function under Dirichlet convolution.

Equations

• NairTenenbaum.arithmeticLogDerivative f g = NairTenenbaum.arithmeticLogWeight f * g

theorem NairTenenbaum.arithmeticLogDerivative_convolution {f g : ArithmeticFunction ℝ} (hfg : f * g = 1) : f * arithmeticLogDerivative f g = arithmeticLogWeight f

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

The ideal-norm analogue of the von Mangoldt arithmetic function.

Equations

• NairTenenbaum.idealVonMangoldt K = NairTenenbaum.arithmeticLogDerivative (NairTenenbaum.idealNormArithmetic K) (NairTenenbaum.idealNormInverse K)

theorem NairTenenbaum.idealVonMangoldt_convolution (K : Type u_1) [Field K] [NumberField K] : idealNormArithmetic K * idealVonMangoldt K = arithmeticLogWeight (idealNormArithmetic K)

theorem NairTenenbaum.idealVonMangoldt_one (K : Type u_1) [Field K] [NumberField K] : (idealVonMangoldt K) 1 = 0

theorem NairTenenbaum.idealVonMangoldt_prime (K : Type u_1) [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : (idealVonMangoldt K) p = ↑(idealNormCount K p) * Real.log ↑p