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 ∈ 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. This notation is scpoed to the separate locales ArithmeticFunction.zeta for ζ, ArithmeticFunction.sigma for σ, ArithmeticFunction.omega for ω, ArithmeticFunction.Omega for Ω, and ArithmeticFunction.Moebius for μ, to allow for selective access.

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.instFunLikeNat {R : Type u_1} [Zero R] : FunLike (ArithmeticFunction R) ℕ R

Equations

• ArithmeticFunction.instFunLikeNat = 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 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 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 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 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 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' := ⋯ } }

@[simp]

theorem ArithmeticFunction.add_apply {R : Type u_1} [AddMonoid R] {f 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

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

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

Equations

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

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

Equations

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

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

Equations

• ArithmeticFunction.instAddCommGroup = { toAddGroup := have this := inferInstance; this, add_comm := ⋯ }

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 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 (x1 x2 : ArithmeticFunction R) => x1 • x2 }

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

Equations

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

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 ArithmeticFunction.instModule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Module (ArithmeticFunction R) (ArithmeticFunction M)

Equations

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

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.zeta.termζ : Lean.ParserDescr

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

Equations

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

@[simp]

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

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

theorem ArithmeticFunction.zeta_eq_zero {x : ℕ} : zeta x = 0 ↔ x = 0

theorem ArithmeticFunction.zeta_pos {x : ℕ} : 0 < zeta x ↔ 0 < x

theorem ArithmeticFunction.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [MulAction R M] {f : ArithmeticFunction M} {x : ℕ} : (↑zeta • f) x = ∑ i ∈ x.divisors, f i

@[simp]

theorem ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [MulAction R M] {f : ArithmeticFunction M} {x : ℕ} : (∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then 0 • f x.2 else f x.2) = ∑ i ∈ x.divisors, f i

@[simp]-normal form of coe_zeta_smul_apply.

theorem ArithmeticFunction.coe_zeta_mul_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (↑zeta * f) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.coe_mul_zeta_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (f * ↑zeta) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.coe_zeta_mul_comm {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} : ↑zeta * f = f * ↑zeta

theorem ArithmeticFunction.zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (zeta * f) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.mul_zeta_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (f * zeta) x = ∑ i ∈ x.divisors, f i

theorem ArithmeticFunction.zeta_mul_comm {f : ArithmeticFunction ℕ} : zeta * f = f * zeta

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

This is the pointwise product of ArithmeticFunctions.

Equations

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

@[simp]

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

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

theorem ArithmeticFunction.pmul_assoc {R : Type u_1} [SemigroupWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R) : (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

@[simp]

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

@[simp]

theorem ArithmeticFunction.zeta_pmul {R : Type u_1} [NonAssocSemiring R] (f : ArithmeticFunction R) : (↑zeta).pmul 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

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

@[simp]

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

@[simp]

theorem ArithmeticFunction.ppow_one {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} : f.ppow 1 = f

@[simp]

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

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

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

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

This is the pointwise division of ArithmeticFunctions.

Equations

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

@[simp]

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

@[simp]

theorem ArithmeticFunction.pdiv_zeta {R : Type u_1} [DivisionSemiring R] (f : ArithmeticFunction R) : f.pdiv ↑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

• ArithmeticFunction.prodPrimeFactors f = { toFun := fun (d : ℕ) => if d = 0 then 0 else ∏ p ∈ d.primeFactors, f p, map_zero' := ⋯ }

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) : (prodPrimeFactors fun (p : ℕ) => f p) n = ∏ p ∈ n.primeFactors, f p

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

theorem ArithmeticFunction.IsMultiplicative.pdiv {R : Type u_1} [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) : (f.pdiv 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.prodPrimeFactors {R : Type u_1} [CommMonoidWithZero R] (f : ℕ → R) : (ArithmeticFunction.prodPrimeFactors f).IsMultiplicative

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

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 : ℕ} : id x = x

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

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

Equations

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

@[simp]

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

theorem ArithmeticFunction.pow_zero_eq_zeta : pow 0 = zeta

theorem ArithmeticFunction.pow_one_eq_id : pow 1 = id

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 : ℕ) => ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ }

def ArithmeticFunction.sigma.termσ : Lean.ParserDescr

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

Equations

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

theorem ArithmeticFunction.sigma_apply {k n : ℕ} : (sigma k) n = ∑ d ∈ n.divisors, d ^ k

@[simp]

theorem ArithmeticFunction.sigma_eq_zero {k n : ℕ} : (sigma k) n = 0 ↔ n = 0

@[simp]

theorem ArithmeticFunction.sigma_pos_iff {k n : ℕ} : 0 < (sigma k) n ↔ 0 < n

theorem ArithmeticFunction.sigma_apply_prime_pow {k p i : ℕ} (hp : Nat.Prime p) : (sigma k) (p ^ i) = ∑ j ∈ Finset.range (i + 1), p ^ (j * k)

theorem ArithmeticFunction.sigma_one_apply (n : ℕ) : (sigma 1) n = ∑ d ∈ n.divisors, d

theorem ArithmeticFunction.sigma_one_apply_prime_pow {p i : ℕ} (hp : Nat.Prime p) : (sigma 1) (p ^ i) = ∑ k ∈ Finset.range (i + 1), p ^ k

theorem ArithmeticFunction.sigma_eq_sum_div (k n : ℕ) : (sigma k) n = ∑ d ∈ n.divisors, (n / d) ^ k

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

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

@[simp]

theorem ArithmeticFunction.sigma_one (k : ℕ) : (sigma k) 1 = 1

theorem ArithmeticFunction.sigma_pos (k n : ℕ) (hn0 : n ≠ 0) : 0 < (sigma k) n

theorem ArithmeticFunction.sigma_mono (k k' n : ℕ) (hk : k ≤ k') : (sigma k) n ≤ (sigma k') n

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

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

theorem ArithmeticFunction.isMultiplicative_zeta : zeta.IsMultiplicative

theorem ArithmeticFunction.isMultiplicative_id : id.IsMultiplicative

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

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

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

theorem Nat.card_divisors {n : ℕ} (hn : n ≠ 0) : n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

@[simp]

theorem Nat.divisors_card_eq_one_iff (n : ℕ) : n.divisors.card = 1 ↔ n = 1

@[simp]

theorem ArithmeticFunction.sigma_eq_one_iff (k n : ℕ) : (sigma k) n = 1 ↔ n = 1

theorem ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul {k n : ℕ} (hn : n ≠ 0) : (sigma k) n = ∏ p ∈ n.primeFactors, ∑ i ∈ Finset.range (n.factorization p + 1), p ^ (i * k)

theorem Nat.sum_divisors {n : ℕ} (hn : n ≠ 0) : ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ Finset.range (n.factorization p + 1), p ^ k

def ArithmeticFunction.cardFactors : ArithmeticFunction ℕ

Ω n is the number of prime factors of n.

Equations

• ArithmeticFunction.cardFactors = { toFun := fun (n : ℕ) => n.primeFactorsList.length, map_zero' := ArithmeticFunction.cardFactors._proof_1 }

def ArithmeticFunction.Omega.termΩ : Lean.ParserDescr

Ω n is the number of prime factors of n.

Equations

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

theorem ArithmeticFunction.cardFactors_apply {n : ℕ} : cardFactors n = n.primeFactorsList.length

theorem ArithmeticFunction.cardFactors_zero : cardFactors 0 = 0

@[simp]

theorem ArithmeticFunction.cardFactors_one : cardFactors 1 = 0

@[simp]

theorem ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one {n : ℕ} : cardFactors n = 0 ↔ n = 0 ∨ n = 1

@[simp]

theorem ArithmeticFunction.cardFactors_pos_iff_one_lt {n : ℕ} : 0 < cardFactors n ↔ 1 < n

@[simp]

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

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

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

@[simp]

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

theorem ArithmeticFunction.cardFactors_pow {m k : ℕ} : cardFactors (m ^ k) = k * cardFactors m

@[simp]

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

theorem ArithmeticFunction.cardFactors_eq_sum_factorization {n : ℕ} : cardFactors n = n.factorization.sum fun (x k : ℕ) => k

def ArithmeticFunction.cardDistinctFactors : ArithmeticFunction ℕ

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

Equations

• ArithmeticFunction.cardDistinctFactors = { toFun := fun (n : ℕ) => n.primeFactorsList.dedup.length, map_zero' := ArithmeticFunction.cardDistinctFactors._proof_1 }

def ArithmeticFunction.omega.termω : Lean.ParserDescr

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

Equations

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

theorem ArithmeticFunction.cardDistinctFactors_zero : cardDistinctFactors 0 = 0

@[simp]

theorem ArithmeticFunction.cardDistinctFactors_one : cardDistinctFactors 1 = 0

theorem ArithmeticFunction.cardDistinctFactors_apply {n : ℕ} : cardDistinctFactors n = n.primeFactorsList.dedup.length

@[simp]

theorem ArithmeticFunction.cardDistinctFactors_eq_zero {n : ℕ} : cardDistinctFactors n = 0 ↔ n ≤ 1

@[simp]

theorem ArithmeticFunction.cardDistinctFactors_pos {n : ℕ} : 0 < cardDistinctFactors n ↔ 1 < n

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

@[simp]

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

@[simp]

theorem ArithmeticFunction.cardDistinctFactors_apply_prime {p : ℕ} (hp : Nat.Prime p) : 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.Moebius.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.Moebius.termμ = Lean.ParserDescr.node `ArithmeticFunction.Moebius.termμ 1024 (Lean.ParserDescr.symbol "μ")

@[simp]

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

@[simp]

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

theorem ArithmeticFunction.moebius_apply_one : moebius 1 = 1

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

theorem ArithmeticFunction.moebius_eq_or (n : ℕ) : moebius n = 0 ∨ moebius n = 1 ∨ moebius n = -1

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

theorem ArithmeticFunction.moebius_sq_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) : moebius l ^ 2 = 1

theorem ArithmeticFunction.abs_moebius_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) : |moebius l| = 1

theorem ArithmeticFunction.moebius_sq {n : ℕ} : moebius n ^ 2 = if Squarefree n then 1 else 0

theorem ArithmeticFunction.abs_moebius {n : ℕ} : |moebius n| = if Squarefree n then 1 else 0

theorem ArithmeticFunction.abs_moebius_le_one {n : ℕ} : |moebius n| ≤ 1

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

theorem ArithmeticFunction.moebius_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : 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) : moebius n = 0

theorem ArithmeticFunction.isMultiplicative_moebius : moebius.IsMultiplicative

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) : ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d

theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) : ∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, ↑(moebius d) * f d

@[simp]

theorem ArithmeticFunction.moebius_mul_coe_zeta : moebius * ↑zeta = 1

@[simp]

theorem ArithmeticFunction.coe_zeta_mul_moebius : ↑zeta * moebius = 1

@[simp]

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

@[simp]

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

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

Equations

• ArithmeticFunction.instInvertibleNatToArithmeticFunctionZeta = { invOf := ↑ArithmeticFunction.moebius, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

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

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

Equations

• ArithmeticFunction.zetaUnit = { val := ↑ArithmeticFunction.zeta, inv := ↑ArithmeticFunction.moebius, val_inv := ⋯, inv_val := ⋯ }

@[simp]

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

@[simp]

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

theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} [AddCommGroup R] {f g : ℕ → R} : (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, 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} [NonAssocRing R] {f g : ℕ → R} : (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(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 g : ℕ → R} : (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ 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 g : ℕ → R} (hf : ∀ (n : ℕ), 0 < n → f n ≠ 0) (hg : ∀ (n : ℕ), 0 < n → g n ≠ 0) : (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ 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 g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, 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 g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) (hs₀ : 0 ∉ s) : (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, moebius x.1 • g x.2 = f n

theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on {R : Type u_1} [NonAssocRing R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(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 g : ℕ → R} (s : Set ℕ) (hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) : (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ 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 g : ℕ → R} (hf : ∀ n > 0, f n ≠ 0) (hg : ∀ n > 0, g n ≠ 0) : (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ moebius x.1 = f n

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

theorem Nat.Coprime.card_divisors_mul {m n : ℕ} (hmn : m.Coprime n) : (m * n).divisors.card = m.divisors.card * n.divisors.card

theorem Nat.Coprime.sum_divisors_mul {m n : ℕ} (hmn : m.Coprime n) : ∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d

def Mathlib.Meta.Positivity.evalArithmeticFunctionSigma : PositivityExt

Extension for ArithmeticFunction.sigma.

Equations

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

def Mathlib.Meta.Positivity.evalArithmeticFunctionZeta : PositivityExt

Extension for ArithmeticFunction.zeta.

Equations

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