The Möbius function and Möbius inversion

Main Definitions

• μ is the Möbius function (spelled moebius in code; the notation μ is available by opening the namespace ArithmeticFunction.Moebius).

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

Tags

arithmetic functions, dirichlet convolution, divisors

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.