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.
• The pointwise operations pmul and ppow differ from the multiplication and power instances on ArithmeticFunction 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 CommRing
• sum_eq_iff_sum_smul_moebius_eq for functions to an AddCommGroup
• prod_eq_iff_prod_pow_moebius_eq for functions to a CommGroup
• prod_eq_iff_prod_pow_moebius_eq_of_nonzero for functions to a CommGroupWithZero
• And variants that apply when the equalities only hold on a set S : Set ℕ such that m ∣ n → n ∈ S → m ∈ S:
• sum_eq_iff_sum_mul_moebius_eq_on for functions to a CommRing
• sum_eq_iff_sum_smul_moebius_eq_on for functions to an AddCommGroup
• prod_eq_iff_prod_pow_moebius_eq_on for functions to a CommGroup
• prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero for functions to a CommGroupWithZero

Notation

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

Tags

arithmetic functions, dirichlet convolution, divisors

def Nat.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

• Nat.ArithmeticFunction R = ZeroHom ℕ R

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

Equations

• Nat.ArithmeticFunction.zero R = inferInstanceAs (Zero (ZeroHom ℕ R))

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

Equations

• Nat.instInhabitedArithmeticFunction R = inferInstanceAs (Inhabited (ZeroHom ℕ R))

instance Nat.ArithmeticFunction.instFunLikeArithmeticFunctionNat {R : Type u_1} [Zero R] : FunLike (Nat.ArithmeticFunction R) ℕ fun x => R

Equations

• Nat.ArithmeticFunction.instFunLikeArithmeticFunctionNat = inferInstanceAs (FunLike (ZeroHom ℕ R) ℕ fun x => R)

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

Equations

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

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

@[simp]

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

@[simp]

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

def Nat.ArithmeticFunction.natToArithmeticFunction {R : Type u_1} [AddMonoidWithOne R] : Nat.ArithmeticFunction ℕ → Nat.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' := (_ : ↑(↑f 0) = 0) }

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

Equations

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

@[simp]

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

@[simp]

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

def Nat.ArithmeticFunction.ofInt {R : Type u_1} [AddGroupWithOne R] : Nat.ArithmeticFunction ℤ → Nat.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' := (_ : ↑(↑f 0) = 0) }

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Nat.ArithmeticFunction.add = { add := fun f g => { toFun := fun n => ↑f n + ↑g n, map_zero' := (_ : ↑f 0 + ↑g 0 = 0) } }

@[simp]

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

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

Equations

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

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

Equations

• Nat.ArithmeticFunction.instAddMonoidWithOne = let src := Nat.ArithmeticFunction.instAddMonoid; let src_1 := Nat.ArithmeticFunction.one; AddMonoidWithOne.mk

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

Equations

• Nat.ArithmeticFunction.instAddCommMonoid = let src := Nat.ArithmeticFunction.instAddMonoid; AddCommMonoid.mk (_ : ∀ (x x_1 : Nat.ArithmeticFunction R), x + x_1 = x_1 + x)

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

Equations

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

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

Equations

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

instance Nat.ArithmeticFunction.instSMulArithmeticFunctionArithmeticFunctionToZeroToAddMonoid {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] : SMul (Nat.ArithmeticFunction R) (Nat.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 Nat.ArithmeticFunction.smul_apply {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] {f : Nat.ArithmeticFunction R} {g : Nat.ArithmeticFunction M} {n : ℕ} : ↑(f • g) n = Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑f x.fst • ↑g x.snd

instance Nat.ArithmeticFunction.instMulArithmeticFunctionToZeroToMonoidWithZero {R : Type u_1} [Semiring R] : Mul (Nat.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

• Nat.ArithmeticFunction.instMulArithmeticFunctionToZeroToMonoidWithZero = { mul := fun x x_1 => x • x_1 }

@[simp]

theorem Nat.ArithmeticFunction.mul_apply {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {g : Nat.ArithmeticFunction R} {n : ℕ} : ↑(f * g) n = Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑f x.fst * ↑g x.snd

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• Nat.ArithmeticFunction.instMonoid = Monoid.mk (_ : ∀ (b : Nat.ArithmeticFunction R), 1 • b = b) (_ : ∀ (f : Nat.ArithmeticFunction R), f * 1 = f) npowRec

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Nat.ArithmeticFunction.zeta : Nat.ArithmeticFunction ℕ

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

Equations

• Nat.ArithmeticFunction.zeta = { toFun := fun x => if x = 0 then 0 else 1, map_zero' := Nat.ArithmeticFunction.zeta.proof_1 }

def Nat.ArithmeticFunction.termζ : Lean.ParserDescr

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

Equations

• Nat.ArithmeticFunction.termζ = Lean.ParserDescr.node `Nat.ArithmeticFunction.termζ 1024 (Lean.ParserDescr.symbol "ζ")

@[simp]

theorem Nat.ArithmeticFunction.zeta_apply {x : ℕ} : ↑Nat.ArithmeticFunction.zeta x = if x = 0 then 0 else 1

theorem Nat.ArithmeticFunction.zeta_apply_ne {x : ℕ} (h : x ≠ 0) : ↑Nat.ArithmeticFunction.zeta x = 1

theorem Nat.ArithmeticFunction.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : Nat.ArithmeticFunction M} {x : ℕ} : ↑(↑Nat.ArithmeticFunction.zeta • f) x = Finset.sum (Nat.divisors x) fun i => ↑f i

theorem Nat.ArithmeticFunction.coe_zeta_mul_apply {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {x : ℕ} : ↑(↑Nat.ArithmeticFunction.zeta * f) x = Finset.sum (Nat.divisors x) fun i => ↑f i

theorem Nat.ArithmeticFunction.coe_mul_zeta_apply {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {x : ℕ} : ↑(f * ↑Nat.ArithmeticFunction.zeta) x = Finset.sum (Nat.divisors x) fun i => ↑f i

theorem Nat.ArithmeticFunction.zeta_mul_apply {f : Nat.ArithmeticFunction ℕ} {x : ℕ} : ↑(Nat.ArithmeticFunction.zeta * f) x = Finset.sum (Nat.divisors x) fun i => ↑f i

theorem Nat.ArithmeticFunction.mul_zeta_apply {f : Nat.ArithmeticFunction ℕ} {x : ℕ} : ↑(f * Nat.ArithmeticFunction.zeta) x = Finset.sum (Nat.divisors x) fun i => ↑f i

def Nat.ArithmeticFunction.pmul {R : Type u_1} [MulZeroClass R] (f : Nat.ArithmeticFunction R) (g : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction R

This is the pointwise product of ArithmeticFunctions.

Equations

• Nat.ArithmeticFunction.pmul f g = { toFun := fun x => ↑f x * ↑g x, map_zero' := (_ : ↑f 0 * ↑g 0 = 0) }

@[simp]

theorem Nat.ArithmeticFunction.pmul_apply {R : Type u_1} [MulZeroClass R] {f : Nat.ArithmeticFunction R} {g : Nat.ArithmeticFunction R} {x : ℕ} : ↑(Nat.ArithmeticFunction.pmul f g) x = ↑f x * ↑g x

theorem Nat.ArithmeticFunction.pmul_comm {R : Type u_1} [CommMonoidWithZero R] (f : Nat.ArithmeticFunction R) (g : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction.pmul f g = Nat.ArithmeticFunction.pmul g f

@[simp]

theorem Nat.ArithmeticFunction.pmul_zeta {R : Type u_1} [NonAssocSemiring R] (f : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction.pmul f ↑Nat.ArithmeticFunction.zeta = f

@[simp]

theorem Nat.ArithmeticFunction.zeta_pmul {R : Type u_1} [NonAssocSemiring R] (f : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction.pmul (↑Nat.ArithmeticFunction.zeta) f = f

def Nat.ArithmeticFunction.ppow {R : Type u_1} [Semiring R] (f : Nat.ArithmeticFunction R) (k : ℕ) : Nat.ArithmeticFunction R

This is the pointwise power of ArithmeticFunctions.

Equations

• Nat.ArithmeticFunction.ppow f k = if h0 : k = 0 then ↑Nat.ArithmeticFunction.zeta else { toFun := fun x => ↑f x ^ k, map_zero' := (_ : (fun x => ↑f x ^ k) 0 = 0) }

@[simp]

theorem Nat.ArithmeticFunction.ppow_zero {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} : Nat.ArithmeticFunction.ppow f 0 = ↑Nat.ArithmeticFunction.zeta

@[simp]

theorem Nat.ArithmeticFunction.ppow_apply {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {k : ℕ} {x : ℕ} (kpos : 0 < k) : ↑(Nat.ArithmeticFunction.ppow f k) x = ↑f x ^ k

theorem Nat.ArithmeticFunction.ppow_succ {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {k : ℕ} : Nat.ArithmeticFunction.ppow f (k + 1) = Nat.ArithmeticFunction.pmul f (Nat.ArithmeticFunction.ppow f k)

theorem Nat.ArithmeticFunction.ppow_succ' {R : Type u_1} [Semiring R] {f : Nat.ArithmeticFunction R} {k : ℕ} {kpos : 0 < k} : Nat.ArithmeticFunction.ppow f (k + 1) = Nat.ArithmeticFunction.pmul (Nat.ArithmeticFunction.ppow f k) f

def Nat.ArithmeticFunction.pdiv {R : Type u_1} [GroupWithZero R] (f : Nat.ArithmeticFunction R) (g : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction R

This is the pointwise division of ArithmeticFunctions.

Equations

• Nat.ArithmeticFunction.pdiv f g = { toFun := fun n => ↑f n / ↑g n, map_zero' := (_ : ↑f 0 / ↑g 0 = 0) }

@[simp]

theorem Nat.ArithmeticFunction.pdiv_apply {R : Type u_1} [GroupWithZero R] (f : Nat.ArithmeticFunction R) (g : Nat.ArithmeticFunction R) (n : ℕ) : ↑(Nat.ArithmeticFunction.pdiv f g) n = ↑f n / ↑g n

@[simp]

theorem Nat.ArithmeticFunction.pdiv_zeta {R : Type u_1} [DivisionSemiring R] (f : Nat.ArithmeticFunction R) : Nat.ArithmeticFunction.pdiv f ↑Nat.ArithmeticFunction.zeta = f

This result only holds for DivisionSemirings instead of GroupWithZeros because zeta takes values in ℕ, and hence the coersion requires an AddMonoidWithOne. TODO: Generalise zeta

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

Multiplicative functions

Equations

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

@[simp]

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

@[simp]

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

theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod {R : Type u_1} {ι : Type u_2} [CommMonoidWithZero R] (g : ι → ℕ) {f : Nat.ArithmeticFunction R} (hf : Nat.ArithmeticFunction.IsMultiplicative f) (s : Finset ι) (hs : Set.Pairwise (↑s) (Nat.Coprime on g)) : ↑f (Finset.prod s fun i => g i) = Finset.prod s fun i => ↑f (g i)

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

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

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

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

theorem Nat.ArithmeticFunction.IsMultiplicative.pdiv {R : Type u_1} [CommGroupWithZero R] {f : Nat.ArithmeticFunction R} {g : Nat.ArithmeticFunction R} (hf : Nat.ArithmeticFunction.IsMultiplicative f) (hg : Nat.ArithmeticFunction.IsMultiplicative g) : Nat.ArithmeticFunction.IsMultiplicative (Nat.ArithmeticFunction.pdiv f g)

theorem Nat.ArithmeticFunction.IsMultiplicative.multiplicative_factorization {R : Type u_1} [CommMonoidWithZero R] (f : Nat.ArithmeticFunction R) (hf : Nat.ArithmeticFunction.IsMultiplicative f) {n : ℕ} (hn : n ≠ 0) : ↑f n = Finsupp.prod (Nat.factorization n) 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 Nat.ArithmeticFunction.IsMultiplicative.iff_ne_zero {R : Type u_1} [MonoidWithZero R] {f : Nat.ArithmeticFunction R} : Nat.ArithmeticFunction.IsMultiplicative f ↔ ↑f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → Nat.Coprime m n → ↑f (m * n) = ↑f m * ↑f n

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

theorem Nat.ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers {R : Type u_1} [CommMonoidWithZero R] (f : Nat.ArithmeticFunction R) (hf : Nat.ArithmeticFunction.IsMultiplicative f) (g : Nat.ArithmeticFunction R) (hg : Nat.ArithmeticFunction.IsMultiplicative g) : 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

def Nat.ArithmeticFunction.id : Nat.ArithmeticFunction ℕ

The identity on ℕ as an ArithmeticFunction.

Equations

• Nat.ArithmeticFunction.id = { toFun := id, map_zero' := Nat.ArithmeticFunction.id.proof_1 }

@[simp]

theorem Nat.ArithmeticFunction.id_apply {x : ℕ} : ↑Nat.ArithmeticFunction.id x = x

def Nat.ArithmeticFunction.pow (k : ℕ) : Nat.ArithmeticFunction ℕ

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

Equations

• Nat.ArithmeticFunction.pow k = Nat.ArithmeticFunction.ppow Nat.ArithmeticFunction.id k

@[simp]

theorem Nat.ArithmeticFunction.pow_apply {k : ℕ} {n : ℕ} : ↑(Nat.ArithmeticFunction.pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

theorem Nat.ArithmeticFunction.pow_zero_eq_zeta : Nat.ArithmeticFunction.pow 0 = Nat.ArithmeticFunction.zeta

def Nat.ArithmeticFunction.sigma (k : ℕ) : Nat.ArithmeticFunction ℕ

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

Equations

• Nat.ArithmeticFunction.sigma k = { toFun := fun n => Finset.sum (Nat.divisors n) fun d => d ^ k, map_zero' := (_ : (Finset.sum (Nat.divisors 0) fun d => d ^ k) = 0) }

def Nat.ArithmeticFunction.termσ : Lean.ParserDescr

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

Equations

• Nat.ArithmeticFunction.termσ = Lean.ParserDescr.node `Nat.ArithmeticFunction.termσ 1024 (Lean.ParserDescr.symbol "σ")

theorem Nat.ArithmeticFunction.sigma_apply {k : ℕ} {n : ℕ} : ↑(Nat.ArithmeticFunction.sigma k) n = Finset.sum (Nat.divisors n) fun d => d ^ k

theorem Nat.ArithmeticFunction.sigma_one_apply (n : ℕ) : ↑(Nat.ArithmeticFunction.sigma 1) n = Finset.sum (Nat.divisors n) fun d => d

theorem Nat.ArithmeticFunction.sigma_zero_apply (n : ℕ) : ↑(Nat.ArithmeticFunction.sigma 0) n = Finset.card (Nat.divisors n)

theorem Nat.ArithmeticFunction.sigma_zero_apply_prime_pow {p : ℕ} {i : ℕ} (hp : Nat.Prime p) : ↑(Nat.ArithmeticFunction.sigma 0) (p ^ i) = i + 1

theorem Nat.ArithmeticFunction.zeta_mul_pow_eq_sigma {k : ℕ} : Nat.ArithmeticFunction.zeta * Nat.ArithmeticFunction.pow k = Nat.ArithmeticFunction.sigma k

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

theorem Nat.ArithmeticFunction.isMultiplicative_zeta : Nat.ArithmeticFunction.IsMultiplicative Nat.ArithmeticFunction.zeta

theorem Nat.ArithmeticFunction.isMultiplicative_id : Nat.ArithmeticFunction.IsMultiplicative Nat.ArithmeticFunction.id

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

theorem Nat.ArithmeticFunction.isMultiplicative_pow {k : ℕ} : Nat.ArithmeticFunction.IsMultiplicative (Nat.ArithmeticFunction.pow k)

theorem Nat.ArithmeticFunction.isMultiplicative_sigma {k : ℕ} : Nat.ArithmeticFunction.IsMultiplicative (Nat.ArithmeticFunction.sigma k)

def Nat.ArithmeticFunction.cardFactors : Nat.ArithmeticFunction ℕ

Ω n is the number of prime factors of n.

Equations

• Nat.ArithmeticFunction.cardFactors = { toFun := fun n => List.length (Nat.factors n), map_zero' := Nat.ArithmeticFunction.cardFactors.proof_1 }

def Nat.ArithmeticFunction.termΩ : Lean.ParserDescr

Ω n is the number of prime factors of n.

Equations

• Nat.ArithmeticFunction.termΩ = Lean.ParserDescr.node `Nat.ArithmeticFunction.termΩ 1024 (Lean.ParserDescr.symbol "Ω")

theorem Nat.ArithmeticFunction.cardFactors_apply {n : ℕ} : ↑Nat.ArithmeticFunction.cardFactors n = List.length (Nat.factors n)

@[simp]

theorem Nat.ArithmeticFunction.cardFactors_one : ↑Nat.ArithmeticFunction.cardFactors 1 = 0

theorem Nat.ArithmeticFunction.cardFactors_eq_one_iff_prime {n : ℕ} : ↑Nat.ArithmeticFunction.cardFactors n = 1 ↔ Nat.Prime n

theorem Nat.ArithmeticFunction.cardFactors_mul {m : ℕ} {n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) : ↑Nat.ArithmeticFunction.cardFactors (m * n) = ↑Nat.ArithmeticFunction.cardFactors m + ↑Nat.ArithmeticFunction.cardFactors n

theorem Nat.ArithmeticFunction.cardFactors_multiset_prod {s : Multiset ℕ} (h0 : Multiset.prod s ≠ 0) : ↑Nat.ArithmeticFunction.cardFactors (Multiset.prod s) = Multiset.sum (Multiset.map (↑Nat.ArithmeticFunction.cardFactors) s)

@[simp]

theorem Nat.ArithmeticFunction.cardFactors_apply_prime {p : ℕ} (hp : Nat.Prime p) : ↑Nat.ArithmeticFunction.cardFactors p = 1

@[simp]

theorem Nat.ArithmeticFunction.cardFactors_apply_prime_pow {p : ℕ} {k : ℕ} (hp : Nat.Prime p) : ↑Nat.ArithmeticFunction.cardFactors (p ^ k) = k

def Nat.ArithmeticFunction.cardDistinctFactors : Nat.ArithmeticFunction ℕ

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

Equations

• Nat.ArithmeticFunction.cardDistinctFactors = { toFun := fun n => List.length (List.dedup (Nat.factors n)), map_zero' := Nat.ArithmeticFunction.cardDistinctFactors.proof_1 }

def Nat.ArithmeticFunction.termω : Lean.ParserDescr

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

Equations

• Nat.ArithmeticFunction.termω = Lean.ParserDescr.node `Nat.ArithmeticFunction.termω 1024 (Lean.ParserDescr.symbol "ω")

theorem Nat.ArithmeticFunction.cardDistinctFactors_zero : ↑Nat.ArithmeticFunction.cardDistinctFactors 0 = 0

@[simp]

theorem Nat.ArithmeticFunction.cardDistinctFactors_one : ↑Nat.ArithmeticFunction.cardDistinctFactors 1 = 0

theorem Nat.ArithmeticFunction.cardDistinctFactors_apply {n : ℕ} : ↑Nat.ArithmeticFunction.cardDistinctFactors n = List.length (List.dedup (Nat.factors n))

theorem Nat.ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree {n : ℕ} (h0 : n ≠ 0) : ↑Nat.ArithmeticFunction.cardDistinctFactors n = ↑Nat.ArithmeticFunction.cardFactors n ↔ Squarefree n

@[simp]

theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime_pow {p : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : ↑Nat.ArithmeticFunction.cardDistinctFactors (p ^ k) = 1

@[simp]

theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime {p : ℕ} (hp : Nat.Prime p) : ↑Nat.ArithmeticFunction.cardDistinctFactors p = 1

def Nat.ArithmeticFunction.moebius : Nat.ArithmeticFunction ℤ

μ 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.ArithmeticFunction.moebius = { toFun := fun n => if Squarefree n then (-1) ^ ↑Nat.ArithmeticFunction.cardFactors n else 0, map_zero' := Nat.ArithmeticFunction.moebius.proof_1 }

def Nat.ArithmeticFunction.termμ : Lean.ParserDescr

μ 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.ArithmeticFunction.termμ = Lean.ParserDescr.node `Nat.ArithmeticFunction.termμ 1024 (Lean.ParserDescr.symbol "μ")

@[simp]

theorem Nat.ArithmeticFunction.moebius_apply_of_squarefree {n : ℕ} (h : Squarefree n) : ↑Nat.ArithmeticFunction.moebius n = (-1) ^ ↑Nat.ArithmeticFunction.cardFactors n

@[simp]

theorem Nat.ArithmeticFunction.moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) : ↑Nat.ArithmeticFunction.moebius n = 0

theorem Nat.ArithmeticFunction.moebius_apply_one : ↑Nat.ArithmeticFunction.moebius 1 = 1

theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_squarefree {n : ℕ} : ↑Nat.ArithmeticFunction.moebius n ≠ 0 ↔ Squarefree n

theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_eq_or {n : ℕ} : ↑Nat.ArithmeticFunction.moebius n ≠ 0 ↔ ↑Nat.ArithmeticFunction.moebius n = 1 ∨ ↑Nat.ArithmeticFunction.moebius n = -1

theorem Nat.ArithmeticFunction.moebius_apply_prime {p : ℕ} (hp : Nat.Prime p) : ↑Nat.ArithmeticFunction.moebius p = -1

theorem Nat.ArithmeticFunction.moebius_apply_prime_pow {p : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : ↑Nat.ArithmeticFunction.moebius (p ^ k) = if k = 1 then -1 else 0

theorem Nat.ArithmeticFunction.moebius_apply_isPrimePow_not_prime {n : ℕ} (hn : IsPrimePow n) (hn' : ¬Nat.Prime n) : ↑Nat.ArithmeticFunction.moebius n = 0

theorem Nat.ArithmeticFunction.isMultiplicative_moebius : Nat.ArithmeticFunction.IsMultiplicative Nat.ArithmeticFunction.moebius

@[simp]

theorem Nat.ArithmeticFunction.moebius_mul_coe_zeta : Nat.ArithmeticFunction.moebius * ↑Nat.ArithmeticFunction.zeta = 1

@[simp]

theorem Nat.ArithmeticFunction.coe_zeta_mul_moebius : ↑Nat.ArithmeticFunction.zeta * Nat.ArithmeticFunction.moebius = 1

@[simp]

theorem Nat.ArithmeticFunction.coe_moebius_mul_coe_zeta {R : Type u_1} [Ring R] : ↑Nat.ArithmeticFunction.moebius * ↑Nat.ArithmeticFunction.zeta = 1

@[simp]

theorem Nat.ArithmeticFunction.coe_zeta_mul_coe_moebius {R : Type u_1} [Ring R] : ↑Nat.ArithmeticFunction.zeta * ↑Nat.ArithmeticFunction.moebius = 1

instance Nat.ArithmeticFunction.instInvertibleArithmeticFunctionToZeroToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingInstMulArithmeticFunctionToZeroToMonoidWithZeroToSemiringToCommSemiringOneToOneNatToArithmeticFunctionZeta {R : Type u_1} [CommRing R] : Invertible ↑Nat.ArithmeticFunction.zeta

Equations

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

def Nat.ArithmeticFunction.zetaUnit {R : Type u_1} [CommRing R] : (Nat.ArithmeticFunction R)ˣ

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

Equations

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

@[simp]

theorem Nat.ArithmeticFunction.coe_zetaUnit {R : Type u_1} [CommRing R] : ↑Nat.ArithmeticFunction.zetaUnit = ↑Nat.ArithmeticFunction.zeta

@[simp]

theorem Nat.ArithmeticFunction.inv_zetaUnit {R : Type u_1} [CommRing R] : ↑Nat.ArithmeticFunction.zetaUnit⁻¹ = ↑Nat.ArithmeticFunction.moebius

theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} [AddCommGroup R] {f : ℕ → R} {g : ℕ → R} : (∀ (n : ℕ), n > 0 → (Finset.sum (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → (Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑Nat.ArithmeticFunction.moebius x.fst • g x.snd) = f n

Möbius inversion for functions to an AddCommGroup.

theorem Nat.ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq {R : Type u_1} [Ring R] {f : ℕ → R} {g : ℕ → R} : (∀ (n : ℕ), n > 0 → (Finset.sum (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → (Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑(↑Nat.ArithmeticFunction.moebius x.fst) * g x.snd) = f n

Möbius inversion for functions to a Ring.

theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq {R : Type u_1} [CommGroup R] {f : ℕ → R} {g : ℕ → R} : (∀ (n : ℕ), n > 0 → (Finset.prod (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → (Finset.prod (Nat.divisorsAntidiagonal n) fun x => g x.snd ^ ↑Nat.ArithmeticFunction.moebius x.fst) = f n

Möbius inversion for functions to a CommGroup.

theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero {R : Type u_1} [CommGroupWithZero R] {f : ℕ → R} {g : ℕ → R} (hf : ∀ (n : ℕ), 0 < n → f n ≠ 0) (hg : ∀ (n : ℕ), 0 < n → g n ≠ 0) : (∀ (n : ℕ), n > 0 → (Finset.prod (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → (Finset.prod (Nat.divisorsAntidiagonal n) fun x => g x.snd ^ ↑Nat.ArithmeticFunction.moebius x.fst) = f n

Möbius inversion for functions to a CommGroupWithZero.

theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on {R : Type u_1} [AddCommGroup R] {f : ℕ → R} {g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ (n : ℕ), n > 0 → n ∈ s → (Finset.sum (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → (Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑Nat.ArithmeticFunction.moebius x.fst • g x.snd) = f n

Möbius inversion for functions to an AddCommGroup, where the equalities only hold on a well-behaved set.

theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on' {R : Type u_1} [AddCommGroup R] {f : ℕ → R} {g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) (hs₀ : ¬0 ∈ s) : (∀ (n : ℕ), n ∈ s → (Finset.sum (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n ∈ s → (Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑Nat.ArithmeticFunction.moebius x.fst • g x.snd) = f n

theorem Nat.ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on {R : Type u_1} [Ring R] {f : ℕ → R} {g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ (n : ℕ), n > 0 → n ∈ s → (Finset.sum (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → (Finset.sum (Nat.divisorsAntidiagonal n) fun x => ↑(↑Nat.ArithmeticFunction.moebius x.fst) * g x.snd) = f n

Möbius inversion for functions to a Ring, where the equalities only hold on a well-behaved set.

theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on {R : Type u_1} [CommGroup R] {f : ℕ → R} {g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ (n : ℕ), n > 0 → n ∈ s → (Finset.prod (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → (Finset.prod (Nat.divisorsAntidiagonal n) fun x => g x.snd ^ ↑Nat.ArithmeticFunction.moebius x.fst) = f n

Möbius inversion for functions to a CommGroup, where the equalities only hold on a well-behaved set.

theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero {R : Type u_1} [CommGroupWithZero R] (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) {f : ℕ → R} {g : ℕ → R} (hf : ∀ (n : ℕ), n > 0 → f n ≠ 0) (hg : ∀ (n : ℕ), n > 0 → g n ≠ 0) : (∀ (n : ℕ), n > 0 → n ∈ s → (Finset.prod (Nat.divisors n) fun i => f i) = g n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → (Finset.prod (Nat.divisorsAntidiagonal n) fun x => g x.snd ^ ↑Nat.ArithmeticFunction.moebius x.fst) = f n

Möbius inversion for functions to a CommGroupWithZero, where the equalities only hold on a well-behaved set.