The von Mangoldt Function

In this file we define the von Mangoldt function: the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p.

Main Results

The main definition for this file is

• ArithmeticFunction.vonMangoldt: The von Mangoldt function Λ.

We then prove the classical summation property of the von Mangoldt function in ArithmeticFunction.vonMangoldt_sum, that ∑ i ∈ n.divisors, Λ i = Real.log n, and use this to deduce alternative expressions for the von Mangoldt function via Möbius inversion, see ArithmeticFunction.sum_moebius_mul_log_eq.

Notation

We use the standard notation Λ to represent the von Mangoldt function. It is accessible in the locales ArithmeticFunction (like the notations for other arithmetic functions) and also in the scope ArithmeticFunction.vonMangoldt.

noncomputable def ArithmeticFunction.log : ArithmeticFunction ℝ

log as an arithmetic function ℕ → ℝ. Note this is in the ArithmeticFunction namespace to indicate that it is bundled as an ArithmeticFunction rather than being the usual real logarithm.

Equations

• ArithmeticFunction.log = { toFun := fun (n : ℕ) => Real.log ↑n, map_zero' := ArithmeticFunction.log._proof_1 }

@[simp]

theorem ArithmeticFunction.log_apply {n : ℕ} : log n = Real.log ↑n

noncomputable def ArithmeticFunction.vonMangoldt : ArithmeticFunction ℝ

The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, Nat.minFac will give the appropriate prime, as it is the smallest prime factor.

In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

Equations

• ArithmeticFunction.vonMangoldt = { toFun := fun (n : ℕ) => if IsPrimePow n then Real.log ↑n.minFac else 0, map_zero' := ArithmeticFunction.vonMangoldt._proof_1 }

def ArithmeticFunction.termΛ : Lean.ParserDescr

The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, Nat.minFac will give the appropriate prime, as it is the smallest prime factor.

In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

Equations

• ArithmeticFunction.termΛ = Lean.ParserDescr.node `ArithmeticFunction.termΛ 1024 (Lean.ParserDescr.symbol "Λ")

def ArithmeticFunction.vonMangoldt.termΛ : Lean.ParserDescr

The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, Nat.minFac will give the appropriate prime, as it is the smallest prime factor.

In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

Equations

• ArithmeticFunction.vonMangoldt.termΛ = Lean.ParserDescr.node `ArithmeticFunction.vonMangoldt.termΛ 1024 (Lean.ParserDescr.symbol "Λ")

theorem ArithmeticFunction.vonMangoldt_apply {n : ℕ} : vonMangoldt n = if IsPrimePow n then Real.log ↑n.minFac else 0

@[simp]

theorem ArithmeticFunction.vonMangoldt_apply_one : vonMangoldt 1 = 0

@[simp]

theorem ArithmeticFunction.vonMangoldt_nonneg {n : ℕ} : 0 ≤ vonMangoldt n

theorem ArithmeticFunction.vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : vonMangoldt (n ^ k) = vonMangoldt n

theorem ArithmeticFunction.vonMangoldt_apply_prime {p : ℕ} (hp : Nat.Prime p) : vonMangoldt p = Real.log ↑p

theorem ArithmeticFunction.vonMangoldt_ne_zero_iff {n : ℕ} : vonMangoldt n ≠ 0 ↔ IsPrimePow n

theorem ArithmeticFunction.vonMangoldt_pos_iff {n : ℕ} : 0 < vonMangoldt n ↔ IsPrimePow n

theorem ArithmeticFunction.vonMangoldt_eq_zero_iff {n : ℕ} : vonMangoldt n = 0 ↔ ¬IsPrimePow n

theorem ArithmeticFunction.vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, vonMangoldt i = Real.log ↑n

@[simp]

theorem ArithmeticFunction.vonMangoldt_mul_zeta : vonMangoldt * ↑zeta = log

@[simp]

theorem ArithmeticFunction.zeta_mul_vonMangoldt : ↑zeta * vonMangoldt = log

@[simp]

theorem ArithmeticFunction.log_mul_moebius_eq_vonMangoldt : log * ↑moebius = vonMangoldt

@[simp]

theorem ArithmeticFunction.moebius_mul_log_eq_vonMangoldt : ↑moebius * log = vonMangoldt

theorem ArithmeticFunction.sum_moebius_mul_log_eq {n : ℕ} : ∑ d ∈ n.divisors, ↑(moebius d) * log d = -vonMangoldt n

theorem ArithmeticFunction.vonMangoldt_le_log {n : ℕ} : vonMangoldt n ≤ Real.log ↑n