# mathlib3documentation

number_theory.arithmetic_function

# Arithmetic Functions and Dirichlet Convolution #

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

This file defines arithmetic functions, which are functions from ℕ to a specified type that map 0 to 0. In the literature, they are often instead defined as functions from ℕ+. These arithmetic functions are endowed with a multiplication, given by Dirichlet convolution, and pointwise addition, to form the Dirichlet ring.

## Main Definitions #

• arithmetic_function R consists of functions f : ℕ → R such that f 0 = 0.
• An arithmetic function f is_multiplicative when x.coprime y → f (x * y) = f x * f y.
• The pointwise operations pmul and ppow differ from the multiplication and power instances on arithmetic_function R, which use Dirichlet multiplication.
• ζ is the arithmetic function such that ζ x = 1 for 0 < x.
• σ k is the arithmetic function such that σ k x = ∑ y in divisors x, y ^ k for 0 < x.
• pow k is the arithmetic function such that pow k x = x ^ k for 0 < x.
• id is the identity arithmetic function on ℕ.
• ω n is the number of distinct prime factors of n.
• Ω n is the number of prime factors of n counted with multiplicity.
• μ is the Möbius function (spelled moebius in code).

## Main Results #

• Several forms of Möbius inversion:
• sum_eq_iff_sum_mul_moebius_eq for functions to a comm_ring
• sum_eq_iff_sum_smul_moebius_eq for functions to an add_comm_group
• prod_eq_iff_prod_pow_moebius_eq for functions to a comm_group
• prod_eq_iff_prod_pow_moebius_eq_of_nonzero for functions to a comm_group_with_zero

## Notation #

The arithmetic functions ζ and σ have Greek letter names, which are localized notation in the namespace arithmetic_function.

## Tags #

arithmetic functions, dirichlet convolution, divisors

@[protected, instance]
@[protected, instance]
def nat.arithmetic_function (R : Type u_1) [has_zero R] :
Type u_1

An arithmetic function is a function from ℕ that maps 0 to 0. In the literature, they are often instead defined as functions from ℕ+. Multiplication on arithmetic_functions is by Dirichlet convolution.

Equations
Instances for nat.arithmetic_function
@[protected, instance]
def nat.arithmetic_function.has_coe_to_fun {R : Type u_1} [has_zero R] :
(λ (_x : , R)
Equations
@[simp]
@[simp]
theorem nat.arithmetic_function.zero_apply {R : Type u_1} [has_zero R] {x : } :
0 x = 0
@[ext]
theorem nat.arithmetic_function.ext {R : Type u_1} [has_zero R] ⦃f g : nat.arithmetic_function R⦄ (h : (x : ), f x = g x) :
f = g
theorem nat.arithmetic_function.ext_iff {R : Type u_1} [has_zero R] {f g : nat.arithmetic_function R} :
f = g (x : ), f x = g x
@[protected, instance]
Equations
theorem nat.arithmetic_function.one_apply {R : Type u_1} [has_zero R] [has_one R] {x : } :
1 x = ite (x = 1) 1 0
@[simp]
theorem nat.arithmetic_function.one_one {R : Type u_1} [has_zero R] [has_one R] :
1 1 = 1
@[simp]
theorem nat.arithmetic_function.one_apply_ne {R : Type u_1} [has_zero R] [has_one R] {x : } (h : x 1) :
1 x = 0
@[protected, instance]
Equations
@[simp]
theorem nat.arithmetic_function.nat_coe_apply {R : Type u_1} {x : } :
f x = (f x)
@[protected, instance]
Equations
@[simp]
theorem nat.arithmetic_function.int_coe_apply {R : Type u_1} {x : } :
f x = (f x)
@[simp]
theorem nat.arithmetic_function.coe_coe {R : Type u_1}  :
@[simp]
theorem nat.arithmetic_function.nat_coe_one {R : Type u_1}  :
1 = 1
@[simp]
theorem nat.arithmetic_function.int_coe_one {R : Type u_1}  :
1 = 1
@[protected, instance]
Equations
@[simp]
theorem nat.arithmetic_function.add_apply {R : Type u_1} [add_monoid R] {f g : nat.arithmetic_function R} {n : } :
(f + g) n = f n + g n
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.arithmetic_function.has_smul {R : Type u_1} {M : Type u_2} [has_zero R] [ M] :

The Dirichlet convolution of two arithmetic functions f and g is another arithmetic function such that (f * g) n is the sum of f x * g y over all (x,y) such that x * y = n.

Equations
@[simp]
theorem nat.arithmetic_function.smul_apply {R : Type u_1} {M : Type u_2} [has_zero R] [ M] {f : nat.arithmetic_function R} {g : nat.arithmetic_function M} {n : } :
(f g) n = n.divisors_antidiagonal.sum (λ (x : × ), f x.fst g x.snd)
@[protected, instance]

The Dirichlet convolution of two arithmetic functions f and g is another arithmetic function such that (f * g) n is the sum of f x * g y over all (x,y) such that x * y = n.

Equations
@[simp]
theorem nat.arithmetic_function.mul_apply {R : Type u_1} [semiring R] {f g : nat.arithmetic_function R} {n : } :
(f * g) n = n.divisors_antidiagonal.sum (λ (x : × ), f x.fst * g x.snd)
theorem nat.arithmetic_function.mul_apply_one {R : Type u_1} [semiring R] {f g : nat.arithmetic_function R} :
(f * g) 1 = f 1 * g 1
@[simp, norm_cast]
@[simp, norm_cast]
theorem nat.arithmetic_function.mul_smul' {R : Type u_1} {M : Type u_2} [semiring R] [ M] (f g : nat.arithmetic_function R) (h : nat.arithmetic_function M) :
(f * g) h = f g h
theorem nat.arithmetic_function.one_smul' {R : Type u_1} {M : Type u_2} [semiring R] [ M] (b : nat.arithmetic_function M) :
1 b = b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def nat.arithmetic_function.module {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations

ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

Equations
@[simp]
theorem nat.arithmetic_function.zeta_apply {x : } :
= ite (x = 0) 0 1
@[simp]
theorem nat.arithmetic_function.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [semiring R] [ M] {f : nat.arithmetic_function M} {x : } :
= x.divisors.sum (λ (i : ), f i)
@[simp]
theorem nat.arithmetic_function.coe_zeta_mul_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {x : } :
= x.divisors.sum (λ (i : ), f i)
@[simp]
theorem nat.arithmetic_function.coe_mul_zeta_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {x : } :
= x.divisors.sum (λ (i : ), f i)

This is the pointwise product of arithmetic_functions.

Equations
@[simp]
theorem nat.arithmetic_function.pmul_apply {R : Type u_1} {f g : nat.arithmetic_function R} {x : } :
(f.pmul g) x = f x * g x

This is the pointwise power of arithmetic_functions.

Equations
@[simp]
theorem nat.arithmetic_function.ppow_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k x : } (kpos : 0 < k) :
(f.ppow k) x = f x ^ k
theorem nat.arithmetic_function.ppow_succ {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k : } :
f.ppow (k + 1) = f.pmul (f.ppow k)
theorem nat.arithmetic_function.ppow_succ' {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k : } {kpos : 0 < k} :
f.ppow (k + 1) = (f.ppow k).pmul f

Multiplicative functions

Equations
@[simp]
theorem nat.arithmetic_function.is_multiplicative.map_prod {R : Type u_1} {ι : Type u_2} (g : ι ) {f : nat.arithmetic_function R} (hf : f.is_multiplicative) (s : finset ι) (hs : s.pairwise ) :
f (s.prod (λ (i : ι), g i)) = s.prod (λ (i : ι), f (g i))

For any multiplicative function f and any n > 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

A recapitulation of the definition of multiplicative that is simpler for proofs

Two multiplicative functions f and g are equal if and only if they agree on prime powers

The identity on ℕ as an arithmetic_function.

Equations
@[simp]

pow k n = n ^ k, except pow 0 0 = 0.

Equations
@[simp]
theorem nat.arithmetic_function.pow_apply {k n : } :
= ite (k = 0 n = 0) 0 (n ^ k)

σ k n is the sum of the kth powers of the divisors of n

Equations
theorem nat.arithmetic_function.sigma_apply {k n : } :
= n.divisors.sum (λ (d : ), d ^ k)

Ω n is the number of prime factors of n.

Equations
@[simp]
theorem nat.arithmetic_function.card_factors_mul {m n : } (m0 : m 0) (n0 : n 0) :

ω n is the number of distinct prime factors of n.

Equations
@[simp]

μ is the Möbius function. If n is squarefree with an even number of distinct prime factors, μ n = 1. If n is squarefree with an odd number of distinct prime factors, μ n = -1. If n is not squarefree, μ n = 0.

Equations
theorem nat.arithmetic_function.moebius_apply_prime_pow {p k : } (hp : nat.prime p) (hk : k 0) :
= ite (k = 1) (-1) 0
@[simp]
@[simp]
@[protected, instance]
Equations

A unit in arithmetic_function R that evaluates to ζ, with inverse μ.

Equations
@[simp]
@[simp]
theorem nat.arithmetic_function.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} {f g : R} :
( (n : ), 0 < n n.divisors.sum (λ (i : ), f i) = g n) (n : ), 0 < n n.divisors_antidiagonal.sum (λ (x : × ), = f n

Möbius inversion for functions to an add_comm_group.

theorem nat.arithmetic_function.sum_eq_iff_sum_mul_moebius_eq {R : Type u_1} [ring R] {f g : R} :
( (n : ), 0 < n n.divisors.sum (λ (i : ), f i) = g n) (n : ), 0 < n n.divisors_antidiagonal.sum (λ (x : × ), * g x.snd) = f n

Möbius inversion for functions to a ring.

theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq {R : Type u_1} [comm_group R] {f g : R} :
( (n : ), 0 < n n.divisors.prod (λ (i : ), f i) = g n) (n : ), 0 < n n.divisors_antidiagonal.prod (λ (x : × ), = f n

Möbius inversion for functions to a comm_group.

theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq_of_nonzero {R : Type u_1} {f g : R} (hf : (n : ), 0 < n f n 0) (hg : (n : ), 0 < n g n 0) :
( (n : ), 0 < n n.divisors.prod (λ (i : ), f i) = g n) (n : ), 0 < n n.divisors_antidiagonal.prod (λ (x : × ), = f n

Möbius inversion for functions to a comm_group_with_zero.