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 #
arithmetic_function R
consists of functionsf : ℕ → R
such thatf 0 = 0
.- An arithmetic function
f
is_multiplicative
whenx.coprime y → f (x * y) = f x * f y
. - The pointwise operations
pmul
andppow
differ from the multiplication and power instances onarithmetic_function R
, which use Dirichlet multiplication. ζ
is the arithmetic function such thatζ x = 1
for0 < x
.σ k
is the arithmetic function such thatσ k x = ∑ y in divisors x, y ^ k
for0 < x
.pow k
is the arithmetic function such thatpow k x = x ^ k
for0 < x
.id
is the identity arithmetic function onℕ
.ω n
is the number of distinct prime factors ofn
.Ω n
is the number of prime factors ofn
counted with multiplicity.μ
is the Möbius function (spelledmoebius
in code).
Main Results #
- Several forms of Möbius inversion:
sum_eq_iff_sum_mul_moebius_eq
for functions to acomm_ring
sum_eq_iff_sum_smul_moebius_eq
for functions to anadd_comm_group
prod_eq_iff_prod_pow_moebius_eq
for functions to acomm_group
prod_eq_iff_prod_pow_moebius_eq_of_nonzero
for functions to acomm_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
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
- nat.arithmetic_function.has_zero
- nat.arithmetic_function.inhabited
- nat.arithmetic_function.has_coe_to_fun
- nat.arithmetic_function.has_one
- nat.arithmetic_function.nat_coe
- nat.arithmetic_function.int_coe
- nat.arithmetic_function.has_add
- nat.arithmetic_function.add_monoid
- nat.arithmetic_function.add_monoid_with_one
- nat.arithmetic_function.add_comm_monoid
- nat.arithmetic_function.add_group
- nat.arithmetic_function.add_comm_group
- nat.arithmetic_function.has_smul
- nat.arithmetic_function.has_mul
- nat.arithmetic_function.monoid
- nat.arithmetic_function.semiring
- nat.arithmetic_function.comm_semiring
- nat.arithmetic_function.comm_ring
- nat.arithmetic_function.module
Equations
- nat.arithmetic_function.add_monoid = {add := has_add.add nat.arithmetic_function.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (nat.arithmetic_function R)), nsmul_zero' := _, nsmul_succ' := _}
Equations
- nat.arithmetic_function.add_monoid_with_one = {nat_cast := λ (n : ℕ), {to_fun := λ (x : ℕ), ite (x = 1) ↑n 0, map_zero' := _}, add := add_monoid.add nat.arithmetic_function.add_monoid, add_assoc := _, zero := add_monoid.zero nat.arithmetic_function.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul nat.arithmetic_function.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}
Equations
- nat.arithmetic_function.add_comm_monoid = {add := add_monoid.add nat.arithmetic_function.add_monoid, add_assoc := _, zero := add_monoid.zero nat.arithmetic_function.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul nat.arithmetic_function.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- nat.arithmetic_function.add_group = {add := add_monoid.add nat.arithmetic_function.add_monoid, add_assoc := _, zero := add_monoid.zero nat.arithmetic_function.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul nat.arithmetic_function.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (f : nat.arithmetic_function R), {to_fun := λ (n : ℕ), -⇑f n, map_zero' := _}, sub := sub_neg_monoid.sub._default add_monoid.add nat.arithmetic_function.add_group._proof_7 add_monoid.zero nat.arithmetic_function.add_group._proof_8 nat.arithmetic_function.add_group._proof_9 add_monoid.nsmul nat.arithmetic_function.add_group._proof_10 nat.arithmetic_function.add_group._proof_11 (λ (f : nat.arithmetic_function R), {to_fun := λ (n : ℕ), -⇑f n, map_zero' := _}), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add nat.arithmetic_function.add_group._proof_13 add_monoid.zero nat.arithmetic_function.add_group._proof_14 nat.arithmetic_function.add_group._proof_15 add_monoid.nsmul nat.arithmetic_function.add_group._proof_16 nat.arithmetic_function.add_group._proof_17 (λ (f : nat.arithmetic_function R), {to_fun := λ (n : ℕ), -⇑f n, map_zero' := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
Equations
- nat.arithmetic_function.add_comm_group = {add := add_comm_monoid.add nat.arithmetic_function.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero nat.arithmetic_function.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul nat.arithmetic_function.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg nat.arithmetic_function.add_group, sub := add_group.sub nat.arithmetic_function.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul nat.arithmetic_function.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
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
- nat.arithmetic_function.has_smul = {smul := λ (f : nat.arithmetic_function R) (g : nat.arithmetic_function M), {to_fun := λ (n : ℕ), n.divisors_antidiagonal.sum (λ (x : ℕ × ℕ), ⇑f x.fst • ⇑g x.snd), map_zero' := _}}
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
- nat.arithmetic_function.monoid = {mul := has_mul.mul nat.arithmetic_function.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (nat.arithmetic_function R)), npow_zero' := _, npow_succ' := _}
Equations
- nat.arithmetic_function.semiring = {add := has_add.add nat.arithmetic_function.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul nat.arithmetic_function.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul nat.arithmetic_function.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := add_monoid_with_one.one nat.arithmetic_function.add_monoid_with_one, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast nat.arithmetic_function.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow nat.arithmetic_function.monoid, npow_zero' := _, npow_succ' := _}
Equations
- nat.arithmetic_function.comm_semiring = {add := semiring.add nat.arithmetic_function.semiring, add_assoc := _, zero := semiring.zero nat.arithmetic_function.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul nat.arithmetic_function.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul nat.arithmetic_function.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one nat.arithmetic_function.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast nat.arithmetic_function.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow nat.arithmetic_function.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- nat.arithmetic_function.comm_ring = {add := add_comm_group.add nat.arithmetic_function.add_comm_group, add_assoc := _, zero := add_comm_group.zero nat.arithmetic_function.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul nat.arithmetic_function.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg nat.arithmetic_function.add_comm_group, sub := add_comm_group.sub nat.arithmetic_function.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul nat.arithmetic_function.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default comm_semiring.nat_cast add_comm_group.add nat.arithmetic_function.comm_ring._proof_12 add_comm_group.zero nat.arithmetic_function.comm_ring._proof_13 nat.arithmetic_function.comm_ring._proof_14 add_comm_group.nsmul nat.arithmetic_function.comm_ring._proof_15 nat.arithmetic_function.comm_ring._proof_16 comm_semiring.one nat.arithmetic_function.comm_ring._proof_17 nat.arithmetic_function.comm_ring._proof_18 add_comm_group.neg add_comm_group.sub nat.arithmetic_function.comm_ring._proof_19 add_comm_group.zsmul nat.arithmetic_function.comm_ring._proof_20 nat.arithmetic_function.comm_ring._proof_21 nat.arithmetic_function.comm_ring._proof_22 nat.arithmetic_function.comm_ring._proof_23, nat_cast := comm_semiring.nat_cast nat.arithmetic_function.comm_semiring, one := comm_semiring.one nat.arithmetic_function.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semiring.mul nat.arithmetic_function.comm_semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow nat.arithmetic_function.comm_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Equations
- nat.arithmetic_function.module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := nat.arithmetic_function.has_smul smul_with_zero.to_has_smul, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
ζ 0 = 0
, otherwise ζ x = 1
. The Dirichlet Series is the Riemann ζ.
This is the pointwise product of arithmetic_function
s.
This is the pointwise power of arithmetic_function
s.
Multiplicative functions
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
.
pow k n = n ^ k
, except pow 0 0 = 0
.
Equations
σ k n
is the sum of the k
th powers of the divisors of n
Ω n
is the number of prime factors of n
.
ω n
is the number of distinct prime factors of n
.
μ
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
- nat.arithmetic_function.moebius = {to_fun := λ (n : ℕ), ite (squarefree n) ((-1) ^ ⇑nat.arithmetic_function.card_factors n) 0, map_zero' := nat.arithmetic_function.moebius._proof_1}
Equations
A unit in arithmetic_function R
that evaluates to ζ
, with inverse μ
.
Equations
Möbius inversion for functions to an add_comm_group
.
Möbius inversion for functions to a ring
.
Möbius inversion for functions to a comm_group
.
Möbius inversion for functions to a comm_group_with_zero
.