mathlib3 documentation

number_theory.arithmetic_function

Arithmetic Functions and Dirichlet Convolution #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main Results #

Notation #

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

Tags #

arithmetic functions, dirichlet convolution, divisors

source
@[protected, instance]
def nat.arithmetic_function.inhabited (R : Type u_1) [has_zero R] :
inhabited (nat.arithmetic_function R)
source
@[protected, instance]
def nat.arithmetic_function.has_zero (R : Type u_1) [has_zero R] :
has_zero (nat.arithmetic_function R)
source
def nat.arithmetic_function (R : Type u_1) [has_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 arithmetic_functions is by Dirichlet convolution.

Equations
Instances for nat.arithmetic_function
source
@[protected, instance]
def nat.arithmetic_function.has_coe_to_fun {R : Type u_1} [has_zero R] :
has_coe_to_fun (nat.arithmetic_function R) (λ (_x : nat.arithmetic_function R), ℕ → R)
Equations
source
@[simp]
theorem nat.arithmetic_function.to_fun_eq {R : Type u_1} [has_zero R] (f : nat.arithmetic_function R) :
f.to_fun = ⇑f
source
@[simp]
theorem nat.arithmetic_function.map_zero {R : Type u_1} [has_zero R] {f : nat.arithmetic_function R} :
⇑f 0 = 0
source
theorem nat.arithmetic_function.coe_inj {R : Type u_1} [has_zero R] {f g : nat.arithmetic_function R} :
⇑f = ⇑g ↔ f = g
source
@[simp]
theorem nat.arithmetic_function.zero_apply {R : Type u_1} [has_zero R] {x : ℕ} :
⇑0 x = 0
source
@[ext]
theorem nat.arithmetic_function.ext {R : Type u_1} [has_zero R] ⦃f g : nat.arithmetic_function R⦄ (h : ∀ (x : ℕ), ⇑f x = ⇑g x) :
f = g
source
theorem nat.arithmetic_function.ext_iff {R : Type u_1} [has_zero R] {f g : nat.arithmetic_function R} :
f = g ↔ ∀ (x : ℕ), ⇑f x = ⇑g x
source
@[protected, instance]
def nat.arithmetic_function.has_one {R : Type u_1} [has_zero R] [has_one R] :
has_one (nat.arithmetic_function R)
Equations
source
theorem nat.arithmetic_function.one_apply {R : Type u_1} [has_zero R] [has_one R] {x : ℕ} :
⇑1 x = ite (x = 1) 1 0
source
@[simp]
theorem nat.arithmetic_function.one_one {R : Type u_1} [has_zero R] [has_one R] :
⇑1 1 = 1
source
@[simp]
theorem nat.arithmetic_function.one_apply_ne {R : Type u_1} [has_zero R] [has_one R] {x : ℕ} (h : x ≠ 1) :
⇑1 x = 0
source
@[protected, instance]
def nat.arithmetic_function.nat_coe {R : Type u_1} [add_monoid_with_one R] :
has_coe (nat.arithmetic_function ℕ) (nat.arithmetic_function R)
Equations
source
@[simp]
theorem nat.arithmetic_function.nat_coe_nat (f : nat.arithmetic_function ℕ) :
↑f = f
source
@[simp]
theorem nat.arithmetic_function.nat_coe_apply {R : Type u_1} [add_monoid_with_one R] {f : nat.arithmetic_function ℕ} {x : ℕ} :
⇑↑f x = ↑(⇑f x)
source
@[protected, instance]
def nat.arithmetic_function.int_coe {R : Type u_1} [add_group_with_one R] :
has_coe (nat.arithmetic_function ℤ) (nat.arithmetic_function R)
Equations
source
@[simp]
theorem nat.arithmetic_function.int_coe_int (f : nat.arithmetic_function ℤ) :
↑f = f
source
@[simp]
theorem nat.arithmetic_function.int_coe_apply {R : Type u_1} [add_group_with_one R] {f : nat.arithmetic_function ℤ} {x : ℕ} :
⇑↑f x = ↑(⇑f x)
source
@[simp]
theorem nat.arithmetic_function.coe_coe {R : Type u_1} [add_group_with_one R] {f : nat.arithmetic_function ℕ} :
↑↑f = ↑f
source
@[simp]
theorem nat.arithmetic_function.nat_coe_one {R : Type u_1} [add_monoid_with_one R] :
↑1 = 1
source
@[simp]
theorem nat.arithmetic_function.int_coe_one {R : Type u_1} [add_group_with_one R] :
↑1 = 1
source
@[protected, instance]
def nat.arithmetic_function.has_add {R : Type u_1} [add_monoid R] :
has_add (nat.arithmetic_function R)
Equations
source
@[simp]
theorem nat.arithmetic_function.add_apply {R : Type u_1} [add_monoid R] {f g : nat.arithmetic_function R} {n : ℕ} :
⇑(f + g) n = ⇑f n + ⇑g n
source
@[protected, instance]
def nat.arithmetic_function.add_monoid {R : Type u_1} [add_monoid R] :
add_monoid (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.add_monoid_with_one {R : Type u_1} [add_monoid_with_one R] :
add_monoid_with_one (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.add_comm_monoid {R : Type u_1} [add_comm_monoid R] :
add_comm_monoid (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.add_group {R : Type u_1} [add_group R] :
add_group (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.add_comm_group {R : Type u_1} [add_comm_group R] :
add_comm_group (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.has_smul {R : Type u_1} {M : Type u_2} [has_zero R] [add_comm_monoid M] [has_smul R M] :
has_smul (nat.arithmetic_function R) (nat.arithmetic_function 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
source
@[simp]
theorem nat.arithmetic_function.smul_apply {R : Type u_1} {M : Type u_2} [has_zero R] [add_comm_monoid M] [has_smul R M] {f : nat.arithmetic_function R} {g : nat.arithmetic_function M} {n : ℕ} :
⇑(f • g) n = n.divisors_antidiagonal.sum (λ (x : ℕ × ℕ), ⇑f x.fst • ⇑g x.snd)
source
@[protected, instance]
def nat.arithmetic_function.has_mul {R : Type u_1} [semiring R] :
has_mul (nat.arithmetic_function 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
source
@[simp]
theorem nat.arithmetic_function.mul_apply {R : Type u_1} [semiring R] {f g : nat.arithmetic_function R} {n : ℕ} :
⇑(f * g) n = n.divisors_antidiagonal.sum (λ (x : ℕ × ℕ), ⇑f x.fst * ⇑g x.snd)
source
theorem nat.arithmetic_function.mul_apply_one {R : Type u_1} [semiring R] {f g : nat.arithmetic_function R} :
⇑(f * g) 1 = ⇑f 1 * ⇑g 1
source
@[simp, norm_cast]
theorem nat.arithmetic_function.nat_coe_mul {R : Type u_1} [semiring R] {f g : nat.arithmetic_function ℕ} :
↑(f * g) = ↑f * ↑g
source
@[simp, norm_cast]
theorem nat.arithmetic_function.int_coe_mul {R : Type u_1} [ring R] {f g : nat.arithmetic_function ℤ} :
↑(f * g) = ↑f * ↑g
source
theorem nat.arithmetic_function.mul_smul' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (f g : nat.arithmetic_function R) (h : nat.arithmetic_function M) :
(f * g) • h = f • g • h
source
theorem nat.arithmetic_function.one_smul' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (b : nat.arithmetic_function M) :
1 • b = b
source
@[protected, instance]
def nat.arithmetic_function.monoid {R : Type u_1} [semiring R] :
monoid (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.semiring {R : Type u_1} [semiring R] :
semiring (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.comm_semiring {R : Type u_1} [comm_semiring R] :
comm_semiring (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.comm_ring {R : Type u_1} [comm_ring R] :
comm_ring (nat.arithmetic_function R)
Equations
source
@[protected, instance]
def nat.arithmetic_function.module {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
module (nat.arithmetic_function R) (nat.arithmetic_function M)
Equations
source
def nat.arithmetic_function.zeta  :
nat.arithmetic_function ℕ

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

Equations
source
@[simp]
theorem nat.arithmetic_function.zeta_apply {x : ℕ} :
⇑nat.arithmetic_function.zeta x = ite (x = 0) 0 1
source
theorem nat.arithmetic_function.zeta_apply_ne {x : ℕ} (h : x ≠ 0) :
⇑nat.arithmetic_function.zeta x = 1
source
@[simp]
theorem nat.arithmetic_function.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {f : nat.arithmetic_function M} {x : ℕ} :
⇑(↑nat.arithmetic_function.zeta • f) x = x.divisors.sum (λ (i : ℕ), ⇑f i)
source
@[simp]
theorem nat.arithmetic_function.coe_zeta_mul_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {x : ℕ} :
⇑(↑nat.arithmetic_function.zeta * f) x = x.divisors.sum (λ (i : ℕ), ⇑f i)
source
@[simp]
theorem nat.arithmetic_function.coe_mul_zeta_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {x : ℕ} :
⇑(f * ↑nat.arithmetic_function.zeta) x = x.divisors.sum (λ (i : ℕ), ⇑f i)
source
theorem nat.arithmetic_function.zeta_mul_apply {f : nat.arithmetic_function ℕ} {x : ℕ} :
⇑(nat.arithmetic_function.zeta * f) x = x.divisors.sum (λ (i : ℕ), ⇑f i)
source
theorem nat.arithmetic_function.mul_zeta_apply {f : nat.arithmetic_function ℕ} {x : ℕ} :
⇑(f * nat.arithmetic_function.zeta) x = x.divisors.sum (λ (i : ℕ), ⇑f i)
source
def nat.arithmetic_function.pmul {R : Type u_1} [mul_zero_class R] (f g : nat.arithmetic_function R) :
nat.arithmetic_function R

This is the pointwise product of arithmetic_functions.

Equations
source
@[simp]
theorem nat.arithmetic_function.pmul_apply {R : Type u_1} [mul_zero_class R] {f g : nat.arithmetic_function R} {x : ℕ} :
⇑(f.pmul g) x = ⇑f x * ⇑g x
source
theorem nat.arithmetic_function.pmul_comm {R : Type u_1} [comm_monoid_with_zero R] (f g : nat.arithmetic_function R) :
f.pmul g = g.pmul f
source
@[simp]
theorem nat.arithmetic_function.pmul_zeta {R : Type u_1} [non_assoc_semiring R] (f : nat.arithmetic_function R) :
f.pmul ↑nat.arithmetic_function.zeta = f
source
@[simp]
theorem nat.arithmetic_function.zeta_pmul {R : Type u_1} [non_assoc_semiring R] (f : nat.arithmetic_function R) :
↑nat.arithmetic_function.zeta.pmul f = f
source
def nat.arithmetic_function.ppow {R : Type u_1} [semiring R] (f : nat.arithmetic_function R) (k : ℕ) :
nat.arithmetic_function R

This is the pointwise power of arithmetic_functions.

Equations
source
@[simp]
theorem nat.arithmetic_function.ppow_zero {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} :
f.ppow 0 = ↑nat.arithmetic_function.zeta
source
@[simp]
theorem nat.arithmetic_function.ppow_apply {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k x : ℕ} (kpos : 0 < k) :
⇑(f.ppow k) x = ⇑f x ^ k
source
theorem nat.arithmetic_function.ppow_succ {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k : ℕ} :
f.ppow (k + 1) = f.pmul (f.ppow k)
source
theorem nat.arithmetic_function.ppow_succ' {R : Type u_1} [semiring R] {f : nat.arithmetic_function R} {k : ℕ} {kpos : 0 < k} :
f.ppow (k + 1) = (f.ppow k).pmul f
source
def nat.arithmetic_function.is_multiplicative {R : Type u_1} [monoid_with_zero R] (f : nat.arithmetic_function R) :
Prop

Multiplicative functions

Equations
source
@[simp]
theorem nat.arithmetic_function.is_multiplicative.map_one {R : Type u_1} [monoid_with_zero R] {f : nat.arithmetic_function R} (h : f.is_multiplicative) :
⇑f 1 = 1
source
@[simp]
theorem nat.arithmetic_function.is_multiplicative.map_mul_of_coprime {R : Type u_1} [monoid_with_zero R] {f : nat.arithmetic_function R} (hf : f.is_multiplicative) {m n : ℕ} (h : m.coprime n) :
⇑f (m * n) = ⇑f m * ⇑f n
source
theorem nat.arithmetic_function.is_multiplicative.map_prod {R : Type u_1} {ι : Type u_2} [comm_monoid_with_zero R] (g : ι → ℕ) {f : nat.arithmetic_function R} (hf : f.is_multiplicative) (s : finset ι) (hs : ↑s.pairwise (nat.coprime on g)) :
⇑f (s.prod (λ (i : ι), g i)) = s.prod (λ (i : ι), ⇑f (g i))
source
theorem nat.arithmetic_function.is_multiplicative.nat_cast {R : Type u_1} {f : nat.arithmetic_function ℕ} [semiring R] (h : f.is_multiplicative) :
↑f.is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative.int_cast {R : Type u_1} {f : nat.arithmetic_function ℤ} [ring R] (h : f.is_multiplicative) :
↑f.is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative.mul {R : Type u_1} [comm_semiring R] {f g : nat.arithmetic_function R} (hf : f.is_multiplicative) (hg : g.is_multiplicative) :
(f * g).is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative.pmul {R : Type u_1} [comm_semiring R] {f g : nat.arithmetic_function R} (hf : f.is_multiplicative) (hg : g.is_multiplicative) :
(f.pmul g).is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative.multiplicative_factorization {R : Type u_1} [comm_monoid_with_zero R] (f : nat.arithmetic_function R) (hf : f.is_multiplicative) {n : ℕ} (hn : n ≠ 0) :
⇑f n = n.factorization.prod (λ (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

source
theorem nat.arithmetic_function.is_multiplicative.iff_ne_zero {R : Type u_1} [monoid_with_zero R] {f : nat.arithmetic_function R} :
f.is_multiplicative ↔ ⇑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

source
theorem nat.arithmetic_function.is_multiplicative.eq_iff_eq_on_prime_powers {R : Type u_1} [comm_monoid_with_zero R] (f : nat.arithmetic_function R) (hf : f.is_multiplicative) (g : nat.arithmetic_function R) (hg : g.is_multiplicative) :
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

source
def nat.arithmetic_function.id  :
nat.arithmetic_function ℕ

The identity on ℕ as an arithmetic_function.

Equations
source
@[simp]
theorem nat.arithmetic_function.id_apply {x : ℕ} :
⇑nat.arithmetic_function.id x = x
source
def nat.arithmetic_function.pow (k : ℕ) :
nat.arithmetic_function ℕ

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

Equations
source
@[simp]
theorem nat.arithmetic_function.pow_apply {k n : ℕ} :
⇑(nat.arithmetic_function.pow k) n = ite (k = 0 ∧ n = 0) 0 (n ^ k)
source
theorem nat.arithmetic_function.pow_zero_eq_zeta  :
nat.arithmetic_function.pow 0 = nat.arithmetic_function.zeta
source
def nat.arithmetic_function.sigma (k : ℕ) :
nat.arithmetic_function ℕ

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

Equations
source
theorem nat.arithmetic_function.sigma_apply {k n : ℕ} :
⇑(nat.arithmetic_function.sigma k) n = n.divisors.sum (λ (d : ℕ), d ^ k)
source
theorem nat.arithmetic_function.sigma_one_apply (n : ℕ) :
⇑(nat.arithmetic_function.sigma 1) n = n.divisors.sum (λ (d : ℕ), d)
source
theorem nat.arithmetic_function.sigma_zero_apply (n : ℕ) :
⇑(nat.arithmetic_function.sigma 0) n = n.divisors.card
source
theorem nat.arithmetic_function.sigma_zero_apply_prime_pow {p i : ℕ} (hp : nat.prime p) :
⇑(nat.arithmetic_function.sigma 0) (p ^ i) = i + 1
source
theorem nat.arithmetic_function.zeta_mul_pow_eq_sigma {k : ℕ} :
nat.arithmetic_function.zeta * nat.arithmetic_function.pow k = nat.arithmetic_function.sigma k
source
theorem nat.arithmetic_function.is_multiplicative_one {R : Type u_1} [monoid_with_zero R] :
1.is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative_zeta  :
nat.arithmetic_function.zeta.is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative_id  :
nat.arithmetic_function.id.is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative.ppow {R : Type u_1} [comm_semiring R] {f : nat.arithmetic_function R} (hf : f.is_multiplicative) {k : ℕ} :
(f.ppow k).is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative_pow {k : ℕ} :
(nat.arithmetic_function.pow k).is_multiplicative
source
theorem nat.arithmetic_function.is_multiplicative_sigma {k : ℕ} :
(nat.arithmetic_function.sigma k).is_multiplicative
source
def nat.arithmetic_function.card_factors  :
nat.arithmetic_function ℕ

Ω n is the number of prime factors of n.

Equations
source
theorem nat.arithmetic_function.card_factors_apply {n : ℕ} :
⇑nat.arithmetic_function.card_factors n = n.factors.length
source
@[simp]
theorem nat.arithmetic_function.card_factors_one  :
⇑nat.arithmetic_function.card_factors 1 = 0
source
theorem nat.arithmetic_function.card_factors_eq_one_iff_prime {n : ℕ} :
⇑nat.arithmetic_function.card_factors n = 1 ↔ nat.prime n
source
theorem nat.arithmetic_function.card_factors_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) :
⇑nat.arithmetic_function.card_factors (m * n) = ⇑nat.arithmetic_function.card_factors m + ⇑nat.arithmetic_function.card_factors n
source
theorem nat.arithmetic_function.card_factors_multiset_prod {s : multiset ℕ} (h0 : s.prod ≠ 0) :
⇑nat.arithmetic_function.card_factors s.prod = (multiset.map ⇑nat.arithmetic_function.card_factors s).sum
source
@[simp]
theorem nat.arithmetic_function.card_factors_apply_prime {p : ℕ} (hp : nat.prime p) :
⇑nat.arithmetic_function.card_factors p = 1
source
@[simp]
theorem nat.arithmetic_function.card_factors_apply_prime_pow {p k : ℕ} (hp : nat.prime p) :
⇑nat.arithmetic_function.card_factors (p ^ k) = k
source
def nat.arithmetic_function.card_distinct_factors  :
nat.arithmetic_function ℕ

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

Equations
source
theorem nat.arithmetic_function.card_distinct_factors_zero  :
⇑nat.arithmetic_function.card_distinct_factors 0 = 0
source
@[simp]
theorem nat.arithmetic_function.card_distinct_factors_one  :
⇑nat.arithmetic_function.card_distinct_factors 1 = 0
source
theorem nat.arithmetic_function.card_distinct_factors_apply {n : ℕ} :
⇑nat.arithmetic_function.card_distinct_factors n = n.factors.dedup.length
source
theorem nat.arithmetic_function.card_distinct_factors_eq_card_factors_iff_squarefree {n : ℕ} (h0 : n ≠ 0) :
⇑nat.arithmetic_function.card_distinct_factors n = ⇑nat.arithmetic_function.card_factors n ↔ squarefree n
source
@[simp]
theorem nat.arithmetic_function.card_distinct_factors_apply_prime_pow {p k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) :
⇑nat.arithmetic_function.card_distinct_factors (p ^ k) = 1
source
@[simp]
theorem nat.arithmetic_function.card_distinct_factors_apply_prime {p : ℕ} (hp : nat.prime p) :
⇑nat.arithmetic_function.card_distinct_factors p = 1
source
def nat.arithmetic_function.moebius  :
nat.arithmetic_function ℤ

μ 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
source
@[simp]
theorem nat.arithmetic_function.moebius_apply_of_squarefree {n : ℕ} (h : squarefree n) :
⇑nat.arithmetic_function.moebius n = (-1) ^ ⇑nat.arithmetic_function.card_factors n
source
@[simp]
theorem nat.arithmetic_function.moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬squarefree n) :
⇑nat.arithmetic_function.moebius n = 0
source
theorem nat.arithmetic_function.moebius_apply_one  :
⇑nat.arithmetic_function.moebius 1 = 1
source
theorem nat.arithmetic_function.moebius_ne_zero_iff_squarefree {n : ℕ} :
⇑nat.arithmetic_function.moebius n ≠ 0 ↔ squarefree n
source
theorem nat.arithmetic_function.moebius_ne_zero_iff_eq_or {n : ℕ} :
⇑nat.arithmetic_function.moebius n ≠ 0 ↔ ⇑nat.arithmetic_function.moebius n = 1 ∨ ⇑nat.arithmetic_function.moebius n = -1
source
theorem nat.arithmetic_function.moebius_apply_prime {p : ℕ} (hp : nat.prime p) :
⇑nat.arithmetic_function.moebius p = -1
source
theorem nat.arithmetic_function.moebius_apply_prime_pow {p k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) :
⇑nat.arithmetic_function.moebius (p ^ k) = ite (k = 1) (-1) 0
source
theorem nat.arithmetic_function.moebius_apply_is_prime_pow_not_prime {n : ℕ} (hn : is_prime_pow n) (hn' : ¬nat.prime n) :
⇑nat.arithmetic_function.moebius n = 0
source
theorem nat.arithmetic_function.is_multiplicative_moebius  :
nat.arithmetic_function.moebius.is_multiplicative
source
@[simp]
theorem nat.arithmetic_function.moebius_mul_coe_zeta  :
nat.arithmetic_function.moebius * ↑nat.arithmetic_function.zeta = 1
source
@[simp]
theorem nat.arithmetic_function.coe_zeta_mul_moebius  :
↑nat.arithmetic_function.zeta * nat.arithmetic_function.moebius = 1
source
@[simp]
theorem nat.arithmetic_function.coe_moebius_mul_coe_zeta {R : Type u_1} [ring R] :
↑nat.arithmetic_function.moebius * ↑nat.arithmetic_function.zeta = 1
source
@[simp]
theorem nat.arithmetic_function.coe_zeta_mul_coe_moebius {R : Type u_1} [ring R] :
↑nat.arithmetic_function.zeta * ↑nat.arithmetic_function.moebius = 1
source
@[protected, instance]
def nat.arithmetic_function.zeta.invertible {R : Type u_1} [comm_ring R] :
invertible ↑nat.arithmetic_function.zeta
Equations
source
def nat.arithmetic_function.zeta_unit {R : Type u_1} [comm_ring R] :
(nat.arithmetic_function R)ˣ

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

Equations
source
@[simp]
theorem nat.arithmetic_function.coe_zeta_unit {R : Type u_1} [comm_ring R] :
↑nat.arithmetic_function.zeta_unit = ↑nat.arithmetic_function.zeta
source
@[simp]
theorem nat.arithmetic_function.inv_zeta_unit {R : Type u_1} [comm_ring R] :
↑nat.arithmetic_function.zeta_unit⁻¹ = ↑nat.arithmetic_function.moebius
source
theorem nat.arithmetic_function.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} [add_comm_group R] {f g : ℕ → R} :
(∀ (n : ℕ), 0 < n → n.divisors.sum (λ (i : ℕ), f i) = g n) ↔ ∀ (n : ℕ), 0 < n → n.divisors_antidiagonal.sum (λ (x : ℕ × ℕ), ⇑nat.arithmetic_function.moebius x.fst • g x.snd) = f n

Möbius inversion for functions to an add_comm_group.

source
theorem nat.arithmetic_function.sum_eq_iff_sum_mul_moebius_eq {R : Type u_1} [ring R] {f g : ℕ → R} :
(∀ (n : ℕ), 0 < n → n.divisors.sum (λ (i : ℕ), f i) = g n) ↔ ∀ (n : ℕ), 0 < n → n.divisors_antidiagonal.sum (λ (x : ℕ × ℕ), ↑(⇑nat.arithmetic_function.moebius x.fst) * g x.snd) = f n

Möbius inversion for functions to a ring.

source
theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq {R : Type u_1} [comm_group R] {f g : ℕ → R} :
(∀ (n : ℕ), 0 < n → n.divisors.prod (λ (i : ℕ), f i) = g n) ↔ ∀ (n : ℕ), 0 < n → n.divisors_antidiagonal.prod (λ (x : ℕ × ℕ), g x.snd ^ ⇑nat.arithmetic_function.moebius x.fst) = f n

Möbius inversion for functions to a comm_group.

source
theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq_of_nonzero {R : Type u_1} [comm_group_with_zero R] {f g : ℕ → R} (hf : ∀ (n : ℕ), 0 < n → f n ≠ 0) (hg : ∀ (n : ℕ), 0 < n → g n ≠ 0) :
(∀ (n : ℕ), 0 < n → n.divisors.prod (λ (i : ℕ), f i) = g n) ↔ ∀ (n : ℕ), 0 < n → n.divisors_antidiagonal.prod (λ (x : ℕ × ℕ), g x.snd ^ ⇑nat.arithmetic_function.moebius x.fst) = f n

Möbius inversion for functions to a comm_group_with_zero.