mathlib documentation

number_theory.arithmetic_function

Arithmetic Functions and Dirichlet Convolution

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

Notation

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

Tags

arithmetic functions, dirichlet convolution, divisors

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
@[simp]

@[simp]
theorem nat.arithmetic_function.map_zero {R : Type u_1} [has_zero R] {f : nat.arithmetic_function R} :
f 0 = 0

theorem nat.arithmetic_function.coe_inj {R : Type u_1} [has_zero R] {f g : nat.arithmetic_function R} :
f = g f = g

@[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

@[instance]

Equations
@[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

@[simp]
theorem nat.arithmetic_function.nat_coe_apply {R : Type u_1} [has_zero R] [has_one R] [has_add R] {f : nat.arithmetic_function } {x : } :
f x = (f x)

@[simp]
theorem nat.arithmetic_function.int_coe_apply {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] {f : nat.arithmetic_function } {x : } :
f x = (f x)

@[simp]

@[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

@[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 = ∑ (x : × ) in n.divisors_antidiagonal, (f x.fst) * g x.snd

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

Equations
@[simp]

@[simp]

This is the pointwise product of arithmetic_functions.

Equations
@[simp]
theorem nat.arithmetic_function.pmul_apply {R : Type u_1} [mul_zero_class R] {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_mul_of_coprime {R : Type u_1} [monoid_with_zero R] {f : nat.arithmetic_function R} (hf : f.is_multiplicative) {m n : } (h : m.coprime n) :
f (m * n) = (f m) * f n

The identity on as an arithmetic_function.

Equations
@[simp]
theorem nat.arithmetic_function.pow_apply {k n : } :
(nat.arithmetic_function.pow 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
@[simp]

Ω n is the number of prime factors of n.

Equations

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

Equations

μ 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

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

Equations
theorem nat.arithmetic_function.sum_eq_iff_sum_moebius_eq {R : Type u_1} [comm_ring R] {f g : → R} (hf : f 0 = 0) (hg : g 0 = 0) :
(∀ (n : ), ∑ (i : ) in n.divisors, f i = g n) ∀ (n : ), ∑ (x : × ) in n.divisors_antidiagonal, ((nat.arithmetic_function.moebius x.fst)) * g x.snd = f n

One version of Möbius inversion.