# 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 locale ArithmeticFunction.vonMangoldt.

noncomputable def ArithmeticFunction.log :

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
Instances For
@[simp]
theorem ArithmeticFunction.log_apply {n : } :
ArithmeticFunction.log n = Real.log n
noncomputable def ArithmeticFunction.vonMangoldt :

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
Instances For

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
Instances For

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
Instances For
theorem ArithmeticFunction.vonMangoldt_apply {n : } :
ArithmeticFunction.vonMangoldt n = if then Real.log n.minFac 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 : ) :
ArithmeticFunction.vonMangoldt p = Real.log p
theorem ArithmeticFunction.vonMangoldt_ne_zero_iff {n : } :
ArithmeticFunction.vonMangoldt n 0
theorem ArithmeticFunction.vonMangoldt_pos_iff {n : } :
0 < ArithmeticFunction.vonMangoldt n
theorem ArithmeticFunction.vonMangoldt_eq_zero_iff {n : } :
ArithmeticFunction.vonMangoldt n = 0
theorem ArithmeticFunction.vonMangoldt_sum {n : } :
in.divisors, ArithmeticFunction.vonMangoldt i = Real.log n
theorem ArithmeticFunction.sum_moebius_mul_log_eq {n : } :
dn.divisors, (ArithmeticFunction.moebius d) * ArithmeticFunction.log d = -ArithmeticFunction.vonMangoldt n
theorem ArithmeticFunction.vonMangoldt_le_log {n : } :
ArithmeticFunction.vonMangoldt n Real.log n