Documentation

Mathlib.NumberTheory.ArithmeticFunction.Misc

Miscellaneous arithmetic Functions #

This file defines some simple examples of arithmetic functions (functions ℕ → R vanishing at 0, considered as a ring under Dirichlet convolution). Note that the Von Mangoldt and Möbius functions are in separate files.

Main Definitions #

σ 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.

Notation #

The arithmetic functions σ, ω and Ω have Greek letter names. This notation is scoped to the separate locales ArithmeticFunction.sigma for σ, ArithmeticFunction.omega for ω and ArithmeticFunction.Omega for Ω, to allow for selective access.

Tags #

arithmetic functions, dirichlet convolution, divisors

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

Instances For

def ArithmeticFunction.bigproddvd :

Lean.ParserDescr

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

Equations

Instances For

@[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

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

def ArithmeticFunction.id :

ArithmeticFunction ℕ

The identity on ℕ as an ArithmeticFunction.

Equations

Instances For

@[simp]

theorem ArithmeticFunction.id_apply {x : ℕ} :

id x = x

theorem ArithmeticFunction.isMultiplicative_id :

id.IsMultiplicative

def ArithmeticFunction.pow (k : ℕ) :

ArithmeticFunction ℕ

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

Equations

Instances For

@[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 :

theorem ArithmeticFunction.pow_one_eq_id :

theorem ArithmeticFunction.isMultiplicative_pow {k : ℕ} :

(pow k).IsMultiplicative

def ArithmeticFunction.sigma (k : ℕ) :

ArithmeticFunction ℕ

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

Equations

Instances For

def ArithmeticFunction.sigma.termσ :

Lean.ParserDescr

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

Equations

Instances For

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_sigma {k : ℕ} :

(sigma k).IsMultiplicative

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

Instances For

def ArithmeticFunction.Omega.termΩ :

Lean.ParserDescr

Ω n is the number of prime factors of n.

Equations

Instances For

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

Instances For

def ArithmeticFunction.omega.termω :

Lean.ParserDescr

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

Equations

Instances For

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

theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff {n : ℕ} :

cardDistinctFactors n = 1 ↔ IsPrimePow 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

theorem ArithmeticFunction.cardDistinctFactors_mul {m n : ℕ} (h : m.Coprime n) :

cardDistinctFactors (m * n) = cardDistinctFactors m + cardDistinctFactors n

theorem ArithmeticFunction.cardDistinctFactors_prod {ι : Type u_2} {s : Finset ι} {f : ι → ℕ} (h : (↑s).Pairwise (Function.onFun Nat.Coprime f)) :

cardDistinctFactors (∏ i ∈ s, f i) = ∑ i ∈ s, cardDistinctFactors (f i)

theorem ArithmeticFunction.sum_Ioc_zeta (N : ℕ) :

∑ n ∈ Finset.Ioc 0 N, zeta n = N

theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter {R : Type u_2} [Semiring R] (f g : ArithmeticFunction R) (N : ℕ) :

∑ n ∈ Finset.Ioc 0 N, (f * g) n = ∑ x ∈ Finset.Ioc 0 N ×ˢ Finset.Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_sum {R : Type u_2} [Semiring R] (f g : ArithmeticFunction R) (N : ℕ) :

∑ n ∈ Finset.Ioc 0 N, (f * g) n = ∑ n ∈ Finset.Ioc 0 N, f n * ∑ m ∈ Finset.Ioc 0 (N / n), g m

theorem ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum {R : Type u_2} [Semiring R] (f : ArithmeticFunction R) (N : ℕ) :

∑ n ∈ Finset.Ioc 0 N, (f * ↑zeta) n = ∑ n ∈ Finset.Ioc 0 N, f n * ↑(N / n)

theorem ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div (N : ℕ) :

∑ n ∈ Finset.Ioc 0 N, (sigma 0) n = ∑ n ∈ Finset.Ioc 0 N, N / n

An O(N) formula for the sum of the number of divisors function.

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 :

Extension for ArithmeticFunction.sigma.

Equations

Instances For