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

• Nat.ArithmeticFunction.vonMangoldt: The von Mangoldt function Λ.

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

Notation

We use the standard notation Λ to represent the von Mangoldt function.

noncomputable def Nat.ArithmeticFunction.log : Nat.ArithmeticFunction ℝ

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

@[simp]

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

noncomputable def Nat.ArithmeticFunction.vonMangoldt : Nat.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, min_fac will give the appropriate prime, as it is the smallest prime factor.

In the ArithmeticFunction locale, we have the notation Λ for this function.

def Nat.ArithmeticFunction.termΛ : Lean.ParserDescr

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

@[simp]

theorem Nat.ArithmeticFunction.vonMangoldt_apply_one : ↑Nat.ArithmeticFunction.vonMangoldt 1 = 0

@[simp]

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

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

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

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

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

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

theorem Nat.ArithmeticFunction.vonMangoldt_sum {n : ℕ} : (Finset.sum (Nat.divisors n) fun i => ↑Nat.ArithmeticFunction.vonMangoldt i) = Real.log ↑n

@[simp]

theorem Nat.ArithmeticFunction.vonMangoldt_mul_zeta : Nat.ArithmeticFunction.vonMangoldt * ↑Nat.ArithmeticFunction.zeta = Nat.ArithmeticFunction.log

@[simp]

theorem Nat.ArithmeticFunction.zeta_mul_vonMangoldt : ↑Nat.ArithmeticFunction.zeta * Nat.ArithmeticFunction.vonMangoldt = Nat.ArithmeticFunction.log

@[simp]

theorem Nat.ArithmeticFunction.log_mul_moebius_eq_vonMangoldt : Nat.ArithmeticFunction.log * ↑Nat.ArithmeticFunction.moebius = Nat.ArithmeticFunction.vonMangoldt

@[simp]

theorem Nat.ArithmeticFunction.moebius_mul_log_eq_vonMangoldt : ↑Nat.ArithmeticFunction.moebius * Nat.ArithmeticFunction.log = Nat.ArithmeticFunction.vonMangoldt

theorem Nat.ArithmeticFunction.sum_moebius_mul_log_eq {n : ℕ} : (Finset.sum (Nat.divisors n) fun d => ↑(↑Nat.ArithmeticFunction.moebius d) * ↑Nat.ArithmeticFunction.log d) = -↑Nat.ArithmeticFunction.vonMangoldt n

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