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

• ArithmeticFunction R consists of functions f : ℕ → R such that f 0 = 0.
• An arithmetic function f IsMultiplicative when x.Coprime y → f (x * y) = f x * f y.
• Multiplication and power instances on ArithmeticFunction R, are defined using Dirichlet convolution.

Further examples of arithmetic functions, such as the Möbius function μ, are available in other files in the Mathlib.NumberTheory.ArithmeticFunction directory.

Tags

arithmetic functions, dirichlet convolution, divisors

def ArithmeticFunction (R : Type u_1) [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 ArithmeticFunctions is by Dirichlet convolution.

Equations

• ArithmeticFunction R = ZeroHom ℕ R

@[instance_reducible]

instance ArithmeticFunction.zero (R : Type u_1) [Zero R] : Zero (ArithmeticFunction R)

Equations

• ArithmeticFunction.zero R = { zero := ArithmeticFunction.zero._aux_1 R }

@[instance_reducible]

instance instInhabitedArithmeticFunction (R : Type u_1) [Zero R] : Inhabited (ArithmeticFunction R)

Equations

• instInhabitedArithmeticFunction R = { default := instInhabitedArithmeticFunction._aux_1 R }

@[instance_reducible]

instance ArithmeticFunction.instFunLikeNat {R : Type u_1} [Zero R] : FunLike (ArithmeticFunction R) ℕ R

Equations

• ArithmeticFunction.instFunLikeNat = { coe := ArithmeticFunction.instFunLikeNat._aux_1, coe_injective := ⋯ }

@[simp]

theorem ArithmeticFunction.toFun_eq {R : Type u_1} [Zero R] (f : ArithmeticFunction R) : f.toFun = ⇑f

@[simp]

theorem ArithmeticFunction.coe_mk {R : Type u_1} [Zero R] (f : ℕ → R) (hf : f 0 = 0) : ⇑{ toFun := f, map_zero' := hf } = f

@[simp]

theorem ArithmeticFunction.map_zero {R : Type u_1} [Zero R] {f : ArithmeticFunction R} : f 0 = 0

theorem ArithmeticFunction.coe_inj {R : Type u_1} [Zero R] {f g : ArithmeticFunction R} : ⇑f = ⇑g ↔ f = g

theorem ArithmeticFunction.range_coe {R : Type u_1} [Zero R] : Set.range DFunLike.coe = {f : ℕ → R | f 0 = 0}

@[simp]

theorem ArithmeticFunction.zero_apply {R : Type u_1} [Zero R] {x : ℕ} : 0 x = 0

theorem ArithmeticFunction.ext {R : Type u_1} [Zero R] ⦃f g : ArithmeticFunction R⦄ (h : ∀ (x : ℕ), f x = g x) : f = g

theorem ArithmeticFunction.ext_iff {R : Type u_1} [Zero R] {f g : ArithmeticFunction R} : f = g ↔ ∀ (x : ℕ), f x = g x

@[instance_reducible]

instance ArithmeticFunction.one {R : Type u_1} [Zero R] [One R] : One (ArithmeticFunction R)

Equations

• ArithmeticFunction.one = { one := { toFun := fun (x : ℕ) => if x = 1 then 1 else 0, map_zero' := ⋯ } }

theorem ArithmeticFunction.one_apply {R : Type u_1} [Zero R] [One R] {x : ℕ} : 1 x = if x = 1 then 1 else 0

@[simp]

theorem ArithmeticFunction.one_one {R : Type u_1} [Zero R] [One R] : 1 1 = 1

@[simp]

theorem ArithmeticFunction.one_apply_ne {R : Type u_1} [Zero R] [One R] {x : ℕ} (h : x ≠ 1) : 1 x = 0

def ArithmeticFunction.natToArithmeticFunction {R : Type u_1} [AddMonoidWithOne R] : ArithmeticFunction ℕ → ArithmeticFunction R

Coerce an arithmetic function with values in ℕ to one with values in R. We cannot inline this in natCoe because it gets unfolded too much.

Equations

• ↑f = { toFun := fun (n : ℕ) => ↑(f n), map_zero' := ⋯ }

@[instance_reducible]

instance ArithmeticFunction.natCoe {R : Type u_1} [AddMonoidWithOne R] : Coe (ArithmeticFunction ℕ) (ArithmeticFunction R)

Equations

• ArithmeticFunction.natCoe = { coe := ArithmeticFunction.natToArithmeticFunction }

@[simp]

theorem ArithmeticFunction.natCoe_nat (f : ArithmeticFunction ℕ) : ↑f = f

@[simp]

theorem ArithmeticFunction.natCoe_apply {R : Type u_1} [AddMonoidWithOne R] {f : ArithmeticFunction ℕ} {x : ℕ} : ↑f x = ↑(f x)

def ArithmeticFunction.ofInt {R : Type u_1} [AddGroupWithOne R] : ArithmeticFunction ℤ → ArithmeticFunction R

Coerce an arithmetic function with values in ℤ to one with values in R. We cannot inline this in intCoe because it gets unfolded too much.

Equations

• ↑f = { toFun := fun (n : ℕ) => ↑(f n), map_zero' := ⋯ }

@[instance_reducible]

instance ArithmeticFunction.intCoe {R : Type u_1} [AddGroupWithOne R] : Coe (ArithmeticFunction ℤ) (ArithmeticFunction R)

Equations

• ArithmeticFunction.intCoe = { coe := ArithmeticFunction.ofInt }

@[simp]

theorem ArithmeticFunction.intCoe_int (f : ArithmeticFunction ℤ) : ↑f = f

@[simp]

theorem ArithmeticFunction.intCoe_apply {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction ℤ} {x : ℕ} : ↑f x = ↑(f x)

@[simp]

theorem ArithmeticFunction.coe_coe {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction ℕ} : ↑↑f = ↑f

@[simp]

theorem ArithmeticFunction.natCoe_one {R : Type u_1} [AddMonoidWithOne R] : ↑1 = 1

@[simp]

theorem ArithmeticFunction.intCoe_one {R : Type u_1} [AddGroupWithOne R] : ↑1 = 1

@[instance_reducible]

instance ArithmeticFunction.add {R : Type u_1} [AddMonoid R] : Add (ArithmeticFunction R)

Equations

• ArithmeticFunction.add = { add := fun (f g : ArithmeticFunction R) => { toFun := ⇑f + ⇑g, map_zero' := ⋯ } }

@[simp]

theorem ArithmeticFunction.add_apply {R : Type u_1} [AddMonoid R] {f g : ArithmeticFunction R} {n : ℕ} : (f + g) n = f n + g n

@[instance_reducible]

instance ArithmeticFunction.instAddMonoid {R : Type u_1} [AddMonoid R] : AddMonoid (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] : AddMonoidWithOne (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] : AddCommMonoid (ArithmeticFunction R)

Equations

• ArithmeticFunction.instAddCommMonoid = { toAddMonoid := ArithmeticFunction.instAddMonoid, add_comm := ⋯ }

@[instance_reducible]

instance ArithmeticFunction.instNeg {R : Type u_1} [NegZeroClass R] : Neg (ArithmeticFunction R)

Equations

• ArithmeticFunction.instNeg = { neg := fun (f : ArithmeticFunction R) => { toFun := -⇑f, map_zero' := ⋯ } }

@[simp]

theorem ArithmeticFunction.neg_apply {R : Type u_1} [NegZeroClass R] {f : ArithmeticFunction R} {n : ℕ} : (-f) n = -f n

@[instance_reducible]

instance ArithmeticFunction.instAddGroup {R : Type u_1} [AddGroup R] : AddGroup (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instAddCommGroup {R : Type u_1} [AddCommGroup R] : AddCommGroup (ArithmeticFunction R)

Equations

• ArithmeticFunction.instAddCommGroup = { toAddGroup := ArithmeticFunction.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

instance ArithmeticFunction.instSMul {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] : SMul (ArithmeticFunction R) (ArithmeticFunction 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem ArithmeticFunction.smul_apply {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] {f : ArithmeticFunction R} {g : ArithmeticFunction M} {n : ℕ} : (f • g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 • g x.2

@[instance_reducible]

instance ArithmeticFunction.instMul {R : Type u_1} [Semiring R] : Mul (ArithmeticFunction R)

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

• ArithmeticFunction.instMul = { mul := fun (f g : ArithmeticFunction R) => f • g }

@[simp]

theorem ArithmeticFunction.mul_apply {R : Type u_1} [Semiring R] {f g : ArithmeticFunction R} {n : ℕ} : (f * g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2

theorem ArithmeticFunction.mul_apply_one {R : Type u_1} [Semiring R] {f g : ArithmeticFunction R} : (f * g) 1 = f 1 * g 1

@[simp]

theorem ArithmeticFunction.natCoe_mul {R : Type u_1} [Semiring R] {f g : ArithmeticFunction ℕ} : ↑(f * g) = ↑f * ↑g

@[simp]

theorem ArithmeticFunction.intCoe_mul {R : Type u_1} [Ring R] {f g : ArithmeticFunction ℤ} : ↑(f * g) = ↑f * ↑g

theorem ArithmeticFunction.mul_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : (f * g) • h = f • g • h

theorem ArithmeticFunction.one_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (b : ArithmeticFunction M) : 1 • b = b

@[instance_reducible]

instance ArithmeticFunction.instMonoid {R : Type u_1} [Semiring R] : Monoid (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instSemiring {R : Type u_1} [Semiring R] : Semiring (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instCommSemiring {R : Type u_1} [CommSemiring R] : CommSemiring (ArithmeticFunction R)

Equations

• ArithmeticFunction.instCommSemiring = { toSemiring := ArithmeticFunction.instSemiring, mul_comm := ⋯ }

@[instance_reducible]

instance ArithmeticFunction.instCommRing {R : Type u_1} [CommRing R] : CommRing (ArithmeticFunction R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ArithmeticFunction.instModule {R : Type u_1} {S : Type u_2} [Semiring R] [AddCommMonoid S] [Module R S] : Module R (ArithmeticFunction S)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ArithmeticFunction.smul_map {R : Type u_1} {S : Type u_2} [Semiring R] [AddCommMonoid S] [Module R S] (x : R) (f : ArithmeticFunction S) (n : ℕ) : (x • f) n = x • f n

@[instance_reducible]

instance ArithmeticFunction.instAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] : Algebra R (ArithmeticFunction S)

Equations

• ArithmeticFunction.instAlgebra = Algebra.ofModule ⋯ ⋯

@[simp]

theorem ArithmeticFunction.algebraMap_apply_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (x : R) : ((algebraMap R (ArithmeticFunction S)) x) 1 = (algebraMap R S) x

@[instance_reducible]

instance ArithmeticFunction.instModule_1 {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Module (ArithmeticFunction R) (ArithmeticFunction M)

Equations

• ArithmeticFunction.instModule_1 = { toSMul := ArithmeticFunction.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[irreducible]

def ArithmeticFunction.dirichletInverseFun {R : Type u_1} [Ring R] (f : ℕ → R) (hf : Invertible (f 1)) (n : ℕ) : R

Given an inverse of f 1, construct the Dirichlet inverse of f. We use Invertible to make this definition computable when f is computable.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ArithmeticFunction.dirichletInverseFun_apply_zero {R : Type u_1} [Ring R] (f : ℕ → R) (hf : Invertible (f 1)) : dirichletInverseFun f hf 0 = 0

@[simp]

theorem ArithmeticFunction.dirichletInverseFun_apply_one {R : Type u_1} [Ring R] (f : ℕ → R) (hf : Invertible (f 1)) : dirichletInverseFun f hf 1 = ⅟(f 1)

@[simp]

theorem ArithmeticFunction.dirichletInverseFun_apply_ne {R : Type u_1} [Ring R] (f : ℕ → R) (hf : Invertible (f 1)) {n : ℕ} (hn0 : n ≠ 0) (hn1 : n ≠ 1) : dirichletInverseFun f hf n = -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

def ArithmeticFunction.dirichletInverse {R : Type u_1} [Ring R] (f : ℕ → R) (hf : Invertible (f 1)) : ArithmeticFunction R

Given an inverse of f 1, construct the Dirichlet inverse of f.

Equations

• ArithmeticFunction.dirichletInverse f hf = { toFun := ArithmeticFunction.dirichletInverseFun f hf, map_zero' := ⋯ }

theorem ArithmeticFunction.self_mul_dirichletInverse {R : Type u_1} [Ring R] (f : ArithmeticFunction R) (hf : Invertible (f 1)) : f * dirichletInverse (⇑f) hf = 1

theorem ArithmeticFunction.dirichletInverse_mul_self {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : Invertible (f 1)) : dirichletInverse (⇑f) hf * f = 1

theorem ArithmeticFunction.isUnit_iff_isUnit_apply_one {R : Type u_1} [CommRing R] {f : ArithmeticFunction R} : IsUnit f ↔ IsUnit (f 1)

def ArithmeticFunction.IsMultiplicative {R : Type u_1} [MonoidWithZero R] (f : ArithmeticFunction R) : Prop

Multiplicative functions

Equations

• f.IsMultiplicative = (f 1 = 1 ∧ ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n)

@[simp]

theorem ArithmeticFunction.IsMultiplicative.map_one {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (h : f.IsMultiplicative) : f 1 = 1

@[simp]

theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ} (h : m.gcd n = 1) : f (m * n) = f m * f n

theorem ArithmeticFunction.IsMultiplicative.map_prod {R : Type u_1} {ι : Type u_2} [CommMonoidWithZero R] (g : ι → ℕ) {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (s : Finset ι) (hs : (↑s).Pairwise (Function.onFun Nat.Coprime g)) : f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

theorem ArithmeticFunction.IsMultiplicative.map_prod_of_prime {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (t : Finset ℕ) (ht : ∀ p ∈ t, Nat.Prime p) : f (∏ a ∈ t, a) = ∏ a ∈ t, f a

theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (l : ℕ) (t : Finset ℕ) (ht : t ⊆ l.primeFactors) : f (∏ a ∈ t, a) = ∏ a ∈ t, f a

theorem ArithmeticFunction.IsMultiplicative.prod_primeFactors {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {l : ℕ} (hl : Squarefree l) : ∏ a ∈ l.primeFactors, f a = f l

theorem ArithmeticFunction.IsMultiplicative.map_div_of_coprime {R : Type u_1} [GroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {l d : ℕ} (hdl : d ∣ l) (hl : (l / d).Coprime d) (hd : f d ≠ 0) : f (l / d) = f l / f d

theorem ArithmeticFunction.IsMultiplicative.natCast {R : Type u_1} {f : ArithmeticFunction ℕ} [Semiring R] (h : f.IsMultiplicative) : (↑f).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.intCast {R : Type u_1} {f : ArithmeticFunction ℤ} [Ring R] (h : f.IsMultiplicative) : (↑f).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.mul {R : Type u_1} [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) : (f * g).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.multiplicative_factorization {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : n ≠ 0) : f n = n.factorization.prod fun (p k : ℕ) => f (p ^ k)

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

theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} : f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n

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

theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) (g : ArithmeticFunction R) (hg : g.IsMultiplicative) : f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)

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

theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} : f (x.lcm y) * f (x.gcd y) = f x * f y

theorem ArithmeticFunction.IsMultiplicative.map_gcd {R : Type u_1} [CommGroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} (hf_lcm : f (x.lcm y) ≠ 0) : f (x.gcd y) = f x * f y / f (x.lcm y)

theorem ArithmeticFunction.IsMultiplicative.map_lcm {R : Type u_1} [CommGroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ} (hf_gcd : f (x.gcd y) ≠ 0) : f (x.lcm y) = f x * f y / f (x.gcd y)

theorem ArithmeticFunction.IsMultiplicative.eq_zero_of_squarefree_of_dvd_eq_zero {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ} (hn : Squarefree n) (hmn : m ∣ n) (h_zero : f m = 0) : f n = 0

@[simp]

theorem ArithmeticFunction.isMultiplicative_one {R : Type u_1} [MonoidWithZero R] : IsMultiplicative 1

theorem ArithmeticFunction.isMultiplicative_finsetProd {R : Type u_1} [CommSemiring R] {ι : Type u_2} (f : ι → ArithmeticFunction R) (s : Finset ι) (hf : ∀ i ∈ s, (f i).IsMultiplicative) : (∏ i ∈ s, f i).IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.pow {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {k : ℕ} : (f ^ k).IsMultiplicative