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

• 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

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

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

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

• 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

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

• 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_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 ArithmeticFunction.sigma_le_pow_succ (k n : ℕ) : (sigma k) n ≤ n ^ (k + 1)

A crude upper bound: σ_k(n) ≤ n ^ (k + 1).

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

• 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

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 : PositivityExt

Extension for ArithmeticFunction.sigma.

Equations

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