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.
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.
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.