# Documentation

Mathlib.NumberTheory.VonMangoldt

# 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 :

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.

Instances For
Instances For
theorem Nat.ArithmeticFunction.vonMangoldt_apply {n : } :
= if then Real.log ↑() else 0
@[simp]