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

All notation is localized in the namespace ArithmeticFunction.

The arithmetic functions ζ, σ, ω, Ω and μ have Greek letter names.

The arithmetic function $$n \mapsto \prod_{p \mid n} f(p)$$ is given custom notation ∏ᵖ p ∣ n, f p when applied to n.

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 ArithmeticFunction.zero (R : Type u_1) [Zero R] : Zero (ArithmeticFunction R)

Equations

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

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

Equations

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

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

Equations

• ArithmeticFunction.instFunLikeArithmeticFunctionNat = inferInstanceAs (FunLike (ZeroHom ℕ R) ℕ R)

@[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 : ArithmeticFunction R} {g : ArithmeticFunction R} : ⇑f = ⇑g ↔ f = g

@[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 : ArithmeticFunction R⦄ ⦃g : ArithmeticFunction R⦄ (h : ∀ (x : ℕ), f x = g x) : f = g

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

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

Equations

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

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' := (_ : ↑(f 0) = 0) }

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' := (_ : ↑(f 0) = 0) }

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 ArithmeticFunction.add {R : Type u_1} [AddMonoid R] : Add (ArithmeticFunction R)

Equations

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

@[simp]

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

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 ArithmeticFunction.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] : AddMonoidWithOne (ArithmeticFunction R)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance ArithmeticFunction.instSMulArithmeticFunctionArithmeticFunctionToZeroToAddMonoid {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 = Finset.sum (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => f x.1 • g x.2

instance ArithmeticFunction.instMulArithmeticFunctionToZeroToMonoidWithZero {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.instMulArithmeticFunctionToZeroToMonoidWithZero = { mul := fun (x x_1 : ArithmeticFunction R) => x • x_1 }

@[simp]

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

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

@[simp]

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

@[simp]

theorem ArithmeticFunction.intCoe_mul {R : Type u_1} [Ring R] {f : ArithmeticFunction ℤ} {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 : ArithmeticFunction R) (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 ArithmeticFunction.instMonoid {R : Type u_1} [Semiring R] : Monoid (ArithmeticFunction R)

Equations

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

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 ArithmeticFunction.instCommSemiringArithmeticFunctionToZeroToCommMonoidWithZero {R : Type u_1} [CommSemiring R] : CommSemiring (ArithmeticFunction R)

Equations

• ArithmeticFunction.instCommSemiringArithmeticFunctionToZeroToCommMonoidWithZero = let src := ArithmeticFunction.instSemiring; CommSemiring.mk (_ : ∀ (f g : ArithmeticFunction R), f * g = g * f)

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

Equations

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

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

Equations

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

def ArithmeticFunction.zeta : ArithmeticFunction ℕ

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

Equations

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

def ArithmeticFunction.termζ : Lean.ParserDescr

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

Equations

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

@[simp]

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

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

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

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

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

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

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

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

This is the pointwise product of ArithmeticFunctions.

Equations

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

This is the pointwise power of ArithmeticFunctions.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

This is the pointwise division of ArithmeticFunctions.

Equations

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

@[simp]

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

@[simp]

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

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

def ArithmeticFunction.prodPrimeFactors {R : Type u_1} [CommMonoidWithZero R] (f : ℕ → R) : ArithmeticFunction R

The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function

Equations

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

def ArithmeticFunction.bigproddvd : Lean.ParserDescr

∏ᵖ p ∣ n, f p is custom notation for prodPrimeFactors f n

Equations

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

@[simp]

theorem ArithmeticFunction.prodPrimeFactors_apply {R : Type u_1} [CommMonoidWithZero R] {f : ℕ → R} {n : ℕ} (hn : n ≠ 0) : (ArithmeticFunction.prodPrimeFactors fun (p : ℕ) => f p) n = Finset.prod n.primeFactors fun (p : ℕ) => f p

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

Multiplicative functions

Equations

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

@[simp]

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

@[simp]

theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : ArithmeticFunction.IsMultiplicative f) {m : ℕ} {n : ℕ} (h : Nat.Coprime m n) : 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 : 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 ArithmeticFunction.IsMultiplicative.map_prod_of_prime {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : ArithmeticFunction.IsMultiplicative f) (t : Finset ℕ) (ht : ∀ p ∈ t, Nat.Prime p) : f (Finset.prod t fun (a : ℕ) => a) = Finset.prod t fun (a : ℕ) => f a

theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : ArithmeticFunction.IsMultiplicative f) (l : ℕ) (t : Finset ℕ) (ht : t ⊆ l.primeFactors) : f (Finset.prod t fun (a : ℕ) => a) = Finset.prod t fun (a : ℕ) => f a

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

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

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

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

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

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

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors {R : Type u_1} [CommMonoidWithZero R] (f : ℕ → R) : ArithmeticFunction.IsMultiplicative (ArithmeticFunction.prodPrimeFactors f)

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} (hf : ArithmeticFunction.IsMultiplicative f) (hg : ArithmeticFunction.IsMultiplicative g) {n : ℕ} (hn : Squarefree n) : (ArithmeticFunction.prodPrimeFactors fun (p : ℕ) => (f + g) p) n = (f * g) n

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

def ArithmeticFunction.id : ArithmeticFunction ℕ

The identity on ℕ as an ArithmeticFunction.

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

• 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 ArithmeticFunction.termσ : Lean.ParserDescr

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

Equations

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

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

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

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

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

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

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

theorem ArithmeticFunction.isMultiplicative_zeta : ArithmeticFunction.IsMultiplicative ArithmeticFunction.zeta

theorem ArithmeticFunction.isMultiplicative_id : ArithmeticFunction.IsMultiplicative ArithmeticFunction.id

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

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

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

def ArithmeticFunction.cardFactors : ArithmeticFunction ℕ

Ω n is the number of prime factors of n.

Equations

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

def ArithmeticFunction.termΩ : Lean.ParserDescr

Ω n is the number of prime factors of n.

Equations

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

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

@[simp]

theorem ArithmeticFunction.cardFactors_zero : ArithmeticFunction.cardFactors 0 = 0

@[simp]

theorem ArithmeticFunction.cardFactors_one : ArithmeticFunction.cardFactors 1 = 0

@[simp]

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

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

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

@[simp]

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

@[simp]

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

def ArithmeticFunction.cardDistinctFactors : ArithmeticFunction ℕ

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

Equations

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

def ArithmeticFunction.termω : Lean.ParserDescr

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

Equations

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

theorem ArithmeticFunction.cardDistinctFactors_zero : ArithmeticFunction.cardDistinctFactors 0 = 0

@[simp]

theorem ArithmeticFunction.cardDistinctFactors_one : ArithmeticFunction.cardDistinctFactors 1 = 0

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

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

@[simp]

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

@[simp]

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

def ArithmeticFunction.moebius : 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

• ArithmeticFunction.moebius = { toFun := fun (n : ℕ) => if Squarefree n then (-1) ^ ArithmeticFunction.cardFactors n else 0, map_zero' := ArithmeticFunction.moebius.proof_1 }

def 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

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

@[simp]

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

@[simp]

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

theorem ArithmeticFunction.moebius_apply_one : ArithmeticFunction.moebius 1 = 1

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

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

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

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

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

theorem ArithmeticFunction.isMultiplicative_moebius : ArithmeticFunction.IsMultiplicative ArithmeticFunction.moebius

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : ArithmeticFunction.IsMultiplicative f) {n : ℕ} (hn : Squarefree n) : (Finset.prod n.primeFactors fun (p : ℕ) => 1 + f p) = Finset.sum (Nat.divisors n) fun (d : ℕ) => f d

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : ArithmeticFunction.IsMultiplicative f) {n : ℕ} (hn : Squarefree n) : (Finset.prod n.primeFactors fun (p : ℕ) => 1 - f p) = Finset.sum (Nat.divisors n) fun (d : ℕ) => ↑(ArithmeticFunction.moebius d) * f d

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

def ArithmeticFunction.zetaUnit {R : Type u_1} [CommRing R] : (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 ArithmeticFunction.coe_zetaUnit {R : Type u_1} [CommRing R] : ↑ArithmeticFunction.zetaUnit = ↑ArithmeticFunction.zeta

@[simp]

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

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

Möbius inversion for functions to an AddCommGroup.

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

Möbius inversion for functions to a Ring.

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

Möbius inversion for functions to a CommGroup.

theorem 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 > 0, (Finset.prod (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n > 0, (Finset.prod (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => g x.2 ^ ArithmeticFunction.moebius x.1) = f n

Möbius inversion for functions to a CommGroupWithZero.

theorem 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 > 0, n ∈ s → (Finset.sum (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n > 0, n ∈ s → (Finset.sum (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => ArithmeticFunction.moebius x.1 • g x.2) = f n

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

theorem 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 ∈ s, (Finset.sum (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n ∈ s, (Finset.sum (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => ArithmeticFunction.moebius x.1 • g x.2) = f n

theorem 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 > 0, n ∈ s → (Finset.sum (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n > 0, n ∈ s → (Finset.sum (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => ↑(ArithmeticFunction.moebius x.1) * g x.2) = f n

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

theorem 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 > 0, n ∈ s → (Finset.prod (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n > 0, n ∈ s → (Finset.prod (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => g x.2 ^ ArithmeticFunction.moebius x.1) = f n

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

theorem 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 > 0, f n ≠ 0) (hg : ∀ n > 0, g n ≠ 0) : (∀ n > 0, n ∈ s → (Finset.prod (Nat.divisors n) fun (i : ℕ) => f i) = g n) ↔ ∀ n > 0, n ∈ s → (Finset.prod (Nat.divisorsAntidiagonal n) fun (x : ℕ × ℕ) => g x.2 ^ ArithmeticFunction.moebius x.1) = f n

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