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 in 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 locale 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 : ℕ} : ArithmeticFunction.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, 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. 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 ↑(Nat.minFac n) 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, 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. 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, 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. 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 : ℕ} : ArithmeticFunction.vonMangoldt n = if IsPrimePow n then Real.log ↑(Nat.minFac n) else 0

@[simp]

theorem ArithmeticFunction.vonMangoldt_apply_one : ArithmeticFunction.vonMangoldt 1 = 0

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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