mathlib3 documentation

number_theory.von_mangoldt

The von Mangoldt Function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We then prove the classical summation property of the von Mangoldt function in nat.arithmetic_function.von_mangoldt_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.arithmetic_function.sum_moebius_mul_log_eq.

Notation #

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

source
noncomputable def nat.arithmetic_function.log  :
nat.arithmetic_function ℝ

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

Equations
source
@[simp]
theorem nat.arithmetic_function.log_apply {n : ℕ} :
⇑nat.arithmetic_function.log n = real.log ↑n
source
noncomputable def nat.arithmetic_function.von_mangoldt  :
nat.arithmetic_function ℝ

The von_mangoldt 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 arithmetic_function locale, we have the notation Λ for this function.

Equations
source
theorem nat.arithmetic_function.von_mangoldt_apply {n : ℕ} :
⇑nat.arithmetic_function.von_mangoldt n = ite (is_prime_pow n) (real.log ↑(n.min_fac)) 0
source
@[simp]
theorem nat.arithmetic_function.von_mangoldt_apply_one  :
⇑nat.arithmetic_function.von_mangoldt 1 = 0
source
@[simp]
theorem nat.arithmetic_function.von_mangoldt_nonneg {n : ℕ} :
0 ≤ ⇑nat.arithmetic_function.von_mangoldt n
source
theorem nat.arithmetic_function.von_mangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) :
⇑nat.arithmetic_function.von_mangoldt (n ^ k) = ⇑nat.arithmetic_function.von_mangoldt n
source
theorem nat.arithmetic_function.von_mangoldt_apply_prime {p : ℕ} (hp : nat.prime p) :
⇑nat.arithmetic_function.von_mangoldt p = real.log ↑p
source
theorem nat.arithmetic_function.von_mangoldt_ne_zero_iff {n : ℕ} :
⇑nat.arithmetic_function.von_mangoldt n ≠ 0 ↔ is_prime_pow n
source
theorem nat.arithmetic_function.von_mangoldt_pos_iff {n : ℕ} :
0 < ⇑nat.arithmetic_function.von_mangoldt n ↔ is_prime_pow n
source
theorem nat.arithmetic_function.von_mangoldt_eq_zero_iff {n : ℕ} :
⇑nat.arithmetic_function.von_mangoldt n = 0 ↔ ¬is_prime_pow n
source
theorem nat.arithmetic_function.von_mangoldt_sum {n : ℕ} :
n.divisors.sum (λ (i : ℕ), ⇑nat.arithmetic_function.von_mangoldt i) = real.log ↑n
source
@[simp]
theorem nat.arithmetic_function.von_mangoldt_mul_zeta  :
nat.arithmetic_function.von_mangoldt * ↑nat.arithmetic_function.zeta = nat.arithmetic_function.log
source
@[simp]
theorem nat.arithmetic_function.zeta_mul_von_mangoldt  :
↑nat.arithmetic_function.zeta * nat.arithmetic_function.von_mangoldt = nat.arithmetic_function.log
source
@[simp]
theorem nat.arithmetic_function.log_mul_moebius_eq_von_mangoldt  :
nat.arithmetic_function.log * ↑nat.arithmetic_function.moebius = nat.arithmetic_function.von_mangoldt
source
@[simp]
theorem nat.arithmetic_function.moebius_mul_log_eq_von_mangoldt  :
↑nat.arithmetic_function.moebius * nat.arithmetic_function.log = nat.arithmetic_function.von_mangoldt
source
theorem nat.arithmetic_function.sum_moebius_mul_log_eq {n : ℕ} :
n.divisors.sum (λ (d : ℕ), ↑(⇑nat.arithmetic_function.moebius d) * ⇑nat.arithmetic_function.log d) = -⇑nat.arithmetic_function.von_mangoldt n
source
theorem nat.arithmetic_function.von_mangoldt_le_log {n : ℕ} :
⇑nat.arithmetic_function.von_mangoldt n ≤ real.log ↑n