Skip to content

Unitary convolution

TheoremUnitary divisors of a prime power#✓fully proved

For every prime \(p\) and every natural number \(m\), the unitary divisors of \(p^m\), that is, the divisors \(d\) of \(p^m\) with \(\gcd(d, p^m/d) = 1\), are exactly \(1\) and \(p^m\).

theorem unitaryDivisors_prime_pow {p : ℕ} (hp : p.Prime) (m : ℕ) :
    (p ^ m).unitaryDivisors = {1, p ^ m}
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesUnitary divisors
Used byUnitary convolution at prime powers

TheoremProducts of unitary divisors of coprime numbers#✓fully proved

Let \(m\) and \(n\) be coprime natural numbers. If \(a\) is a unitary divisor of \(m\) and \(b\) is a unitary divisor of \(n\), then \(ab\) is a unitary divisor of \(mn\).

theorem mul_mem_unitaryDivisors_mul {m n a b : ℕ} (hmn : m.Coprime n)
    (ha : a ∈ m.unitaryDivisors) (hb : b ∈ n.unitaryDivisors) :
    a * b ∈ (m * n).unitaryDivisors
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesUnitary divisors
Used byThe unitary convolution of multiplicative functions is multiplicative

TheoremGcd with a coprime factor preserves unitary divisors#✓fully proved

Let \(m\) and \(n\) be coprime natural numbers. If \(d\) is a unitary divisor of \(mn\), then \(\gcd(d, m)\) is a unitary divisor of \(m\).

theorem gcd_mem_unitaryDivisors_of_mem_mul {m n d : ℕ} (hmn : m.Coprime n)
    (hd : d ∈ (m * n).unitaryDivisors) : d.gcd m ∈ m.unitaryDivisors
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesUnitary divisors
Used byThe unitary convolution of multiplicative functions is multiplicative
20 fully proved

c ^ Ω

DefinitionThe arithmetic function \(c^{\Omega}\)#✓fully proved

Let \(R\) be a monoid with zero and let \(c \in R\). This is the arithmetic function \(c^{\Omega}\) with values in \(R\) given by \(c^{\Omega}(0) = 0\) and \(c^{\Omega}(n) = c^{\Omega(n)}\) for \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity. It is completely multiplicative.

def powOmega [MonoidWithZero R] (c : R) : ArithmeticFunction R :=
  ⟨fun n => if n = 0 then 0 else c ^ cardFactors n, by simp⟩
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Used by 5
Used byComplete multiplicativity of \(c^{\Omega}\) · Multiplicativity of \(c^{\Omega}\) · Value of \(c^{\Omega}\) at a positive integer · Value of \(c^{\Omega}\) at \(1\) · Value of \(c^{\Omega}\) at prime powers

TheoremValue of \(c^{\Omega}\) at a positive integer#✓fully proved

Let \(R\) be a monoid with zero, let \(c \in R\), and let \(c^{\Omega}\) be the arithmetic function with values in \(R\) that is \(0\) at \(0\) and \(c^{\Omega(n)}\) at each \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity. For every natural number \(n \ne 0\), its value at \(n\) is \(c^{\Omega(n)}\).

theorem powOmega_apply [MonoidWithZero R] (c : R) {n : ℕ} (hn : n ≠ 0) :
    powOmega c n = c ^ cardFactors n
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Uses 1 · Used by 1
Statement usesThe arithmetic function \(c^{\Omega}\)
Used byComplete multiplicativity of \(c^{\Omega}\)

TheoremValue of \(c^{\Omega}\) at \(1\)#✓fully proved

Let \(R\) be a monoid with zero, let \(c \in R\), and let \(c^{\Omega}\) be the arithmetic function with values in \(R\) that is \(0\) at \(0\) and \(c^{\Omega(n)}\) at each \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity. Its value at \(1\) is \(1\).

@[simp]
theorem powOmega_one [MonoidWithZero R] (c : R) : powOmega c 1 = 1
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Uses 1 · Used by 1
Statement usesThe arithmetic function \(c^{\Omega}\)
Used byMultiplicativity of \(c^{\Omega}\)

TheoremValue of \(c^{\Omega}\) at prime powers#✓fully proved

Let \(R\) be a monoid with zero, let \(c \in R\), and let \(c^{\Omega}\) be the arithmetic function with values in \(R\) that is \(0\) at \(0\) and \(c^{\Omega(n)}\) at each \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity. For every prime \(p\) and every natural number \(m\), its value at \(p^m\) is \(c^m\).

theorem powOmega_prime_pow [MonoidWithZero R] (c : R) {p : ℕ} (hp : p.Prime) (m : ℕ) :
    powOmega c (p ^ m) = c ^ m
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Uses 1
Statement usesThe arithmetic function \(c^{\Omega}\)

TheoremComplete multiplicativity of \(c^{\Omega}\)#✓fully proved

Let \(R\) be a monoid with zero and \(c \in R\). Let \(c^{\Omega}\) be the arithmetic function \(n \mapsto c^{\Omega(n)}\) for \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity. Then \(c^{\Omega}\) is completely multiplicative: for all natural numbers \(m\) and \(n\), its value at \(mn\) is the product of its values at \(m\) and at \(n\).

theorem isCompletelyMultiplicative_powOmega [MonoidWithZero R] (c : R) :
    (powOmega c).IsCompletelyMultiplicative
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Uses 3 · Used by 1
Statement usesCompletely multiplicative arithmetic function · The arithmetic function \(c^{\Omega}\)
Proof usesValue of \(c^{\Omega}\) at a positive integer
Used byMultiplicativity of \(c^{\Omega}\)

TheoremMultiplicativity of \(c^{\Omega}\)#✓fully proved

Let \(R\) be a monoid with zero and \(c \in R\). The arithmetic function \(n \mapsto c^{\Omega(n)}\) for \(n \ge 1\), where \(\Omega(n)\) is the number of prime factors of \(n\) counted with multiplicity, is multiplicative.

theorem isMultiplicative_powOmega [MonoidWithZero R] (c : R) :
    (powOmega c).IsMultiplicative
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 2.
Uses 4
Statement usesThe arithmetic function \(c^{\Omega}\)
Proof usesNormalized completely multiplicative functions are multiplicative · Complete multiplicativity of \(c^{\Omega}\) · Value of \(c^{\Omega}\) at \(1\)

Unitary convolution

DefinitionUnitary convolution#✓fully proved

Let \(R\) be a semiring. The unitary convolution of two arithmetic functions \(f\) and \(g\) with values in \(R\) is the arithmetic function \(f \sqcup g\) given by \((f \sqcup g)(n) = \sum_{d \parallel n} f(d)\, g(n/d)\), where the sum runs over the unitary divisors \(d\) of \(n\): for \(n \ge 1\) these are the divisors \(d\) of \(n\) with \(\gcd(d, n/d) = 1\), and \(0\) has no unitary divisors. In particular \((f \sqcup g)(0) = 0\).

def unitaryConv [Semiring R] (f g : ArithmeticFunction R) : ArithmeticFunction R :=
  ⟨fun n => ∑ d ∈ n.unitaryDivisors, f d * g (n / d), by simp⟩
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 4
Statement usesUnitary divisors
Used byThe unitary convolution of multiplicative functions is multiplicative · Unitary convolution as a sum over unitary divisors · Unitary convolution at \(1\) · Unitary convolution at prime powers

TheoremUnitary convolution as a sum over unitary divisors#✓fully proved

Let \(R\) be a semiring and let \(f\) and \(g\) be arithmetic functions with values in \(R\). For every natural number \(n\), their unitary convolution \(f \sqcup g\) satisfies \((f \sqcup g)(n) = \sum_{d \parallel n} f(d)\, g(n/d)\), where the sum runs over the unitary divisors \(d\) of \(n\): for \(n \ge 1\) these are the divisors \(d\) of \(n\) with \(\gcd(d, n/d) = 1\), and for \(n = 0\) there are none, so the sum is \(0\).

theorem unitaryConv_apply [Semiring R] (f g : ArithmeticFunction R) (n : ℕ) :
    unitaryConv f g n = ∑ d ∈ n.unitaryDivisors, f d * g (n / d)
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 2 · Used by 1
Statement usesUnitary convolution · Unitary divisors
Used byUnitary convolution at prime powers

TheoremUnitary convolution at \(1\)#✓fully proved

Let \(R\) be a semiring and let \(f\) and \(g\) be arithmetic functions with values in \(R\). Their unitary convolution \(f \sqcup g\), defined by \((f \sqcup g)(n) = \sum_{d \parallel n} f(d)\, g(n/d)\) over the unitary divisors \(d\) of \(n\), satisfies \((f \sqcup g)(1) = f(1)\, g(1)\).

@[simp]
theorem unitaryConv_one [Semiring R] (f g : ArithmeticFunction R) :
    unitaryConv f g 1 = f 1 * g 1
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesUnitary convolution
Used byThe unitary convolution of multiplicative functions is multiplicative

TheoremUnitary convolution at prime powers#✓fully proved

Let \(R\) be a semiring and let \(f\) and \(g\) be arithmetic functions with values in \(R\). For every prime \(p\) and every natural number \(m \ge 1\), their unitary convolution \(f \sqcup g\) satisfies \((f \sqcup g)(p^m) = f(1)\, g(p^m) + f(p^m)\, g(1)\).

theorem unitaryConv_prime_pow [Semiring R] (f g : ArithmeticFunction R) {p m : ℕ}
    (hp : p.Prime) (hm : m ≠ 0) :
    unitaryConv f g (p ^ m) = f 1 * g (p ^ m) + f (p ^ m) * g 1
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 4
Statement usesUnitary convolution
Proof usesUnitary convolution as a sum over unitary divisors · Unitary divisors · Unitary divisors of a prime power

TheoremThe unitary convolution of multiplicative functions is multiplicative#✓fully proved

Let \(R\) be a commutative semiring. If \(f\) and \(g\) are multiplicative arithmetic functions with values in \(R\), then their unitary convolution \(f \sqcup g\), given by \((f \sqcup g)(n) = \sum_{d} f(d)\, g(n/d)\) with \(d\) running over the unitary divisors of \(n\), is multiplicative.

theorem isMultiplicative_unitaryConv [CommSemiring R] {f g : ArithmeticFunction R}
    (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
    (unitaryConv f g).IsMultiplicative
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3 ((𝓜, ⊔) is a group).
Uses 5
Statement usesUnitary convolution
Proof usesUnitary convolution at \(1\) · Gcd with a coprime factor preserves unitary divisors · Products of unitary divisors of coprime numbers · Unitary divisors

Multiplicative functions given on prime powers

DefinitionMultiplicative function with prescribed values at prime powers#✓fully proved

Let \(R\) be a commutative monoid with zero and let \(g : \mathbb{N} \to R\). This is the arithmetic function \(f\) with values in \(R\) given by \(f(0) = 0\) and \(f(n) = \prod_{p \mid n} g(v_p(n))\) for \(n \ge 1\), where the product runs over the primes \(p\) dividing \(n\) and \(v_p(n)\) is the exponent of \(p\) in \(n\). It is multiplicative, it takes the value \(g(m)\) at every prime power \(p^m\) with \(m \ge 1\), and its value at \(1\) is the empty product \(1\), so \(g(0)\) never enters.

def multiplicativeOfPrimePowers [CommMonoidWithZero R] (g : ℕ → R) : ArithmeticFunction R :=
  ⟨fun n => if n = 0 then 0 else ∏ p ∈ n.primeFactors, g (n.factorization p), by simp⟩
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3 (a multiplicative function is determined by its values at the prime powers).
Used by 5
Used byA multiplicative function with prescribed prime-power values · Multiplicativity of the function with prescribed prime-power values · Value of the function with prescribed prime-power values · The function with prescribed prime-power values is \(1\) at \(1\) · The function with prescribed prime-power values at a prime power

TheoremValue of the function with prescribed prime-power values#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(g : \mathbb{N} \to R\), and let \(n \ne 0\) be a natural number. The multiplicative function with value \(g(m)\) at every prime power \(p^m\) with \(m \ge 1\) takes the value \(\prod_{q \mid n} g(v_q(n))\) at \(n\), where \(q\) runs over the primes dividing \(n\) and \(v_q(n)\) is the exponent of \(q\) in the factorization of \(n\).

theorem multiplicativeOfPrimePowers_apply [CommMonoidWithZero R] (g : ℕ → R) {n : ℕ}
    (hn : n ≠ 0) :
    multiplicativeOfPrimePowers g n = n.factorization.prod fun _ k => g k
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesMultiplicative function with prescribed values at prime powers
Used byMultiplicativity of the function with prescribed prime-power values

TheoremThe function with prescribed prime-power values is \(1\) at \(1\)#✓fully proved

Let \(R\) be a commutative monoid with zero and \(g : \mathbb{N} \to R\). The multiplicative function with prime-power values \(g\), given by \(n \mapsto \prod_{q \mid n} g(v_q(n))\) for \(n \ge 1\) (with \(q\) running over the primes dividing \(n\) and \(v_q(n)\) the exponent of \(q\) in \(n\)), takes the value \(1\) at \(n = 1\), whatever \(g(0)\) is.

@[simp]
theorem multiplicativeOfPrimePowers_one [CommMonoidWithZero R] (g : ℕ → R) :
    multiplicativeOfPrimePowers g 1 = 1
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 2
Statement usesMultiplicative function with prescribed values at prime powers
Used byA multiplicative function with prescribed prime-power values · Multiplicativity of the function with prescribed prime-power values

TheoremThe function with prescribed prime-power values at a prime power#✓fully proved

Let \(R\) be a commutative monoid with zero and \(g : \mathbb{N} \to R\). For every prime \(p\) and every \(m \ge 1\), the multiplicative function with prime-power values \(g\), given by \(n \mapsto \prod_{q \mid n} g(v_q(n))\) for \(n \ge 1\) (with \(q\) running over the primes dividing \(n\) and \(v_q(n)\) the exponent of \(q\) in \(n\)), takes the value \(g(m)\) at \(p^m\).

theorem multiplicativeOfPrimePowers_prime_pow [CommMonoidWithZero R] (g : ℕ → R) {p m : ℕ}
    (hp : p.Prime) (hm : m ≠ 0) : multiplicativeOfPrimePowers g (p ^ m) = g m
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 1 · Used by 1
Statement usesMultiplicative function with prescribed values at prime powers
Used byA multiplicative function with prescribed prime-power values

TheoremMultiplicativity of the function with prescribed prime-power values#✓fully proved

Let \(R\) be a commutative monoid with zero and \(g : \mathbb{N} \to R\). The arithmetic function \(n \mapsto \prod_{q \mid n} g(v_q(n))\) for \(n \ge 1\), where \(q\) runs over the primes dividing \(n\) and \(v_q(n)\) is the exponent of \(q\) in \(n\), is multiplicative.

theorem isMultiplicative_multiplicativeOfPrimePowers [CommMonoidWithZero R] (g : ℕ → R) :
    (multiplicativeOfPrimePowers g).IsMultiplicative
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3.
Uses 3 · Used by 1
Statement usesMultiplicative function with prescribed values at prime powers
Proof usesValue of the function with prescribed prime-power values · The function with prescribed prime-power values is \(1\) at \(1\)
Used byA multiplicative function with prescribed prime-power values

TheoremA multiplicative function with prescribed prime-power values#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(g : \mathbb{N} \to R\), and let \(f\) be a multiplicative arithmetic function with values in \(R\). If \(f(p^m) = g(m)\) for every prime \(p\) and every \(m \ge 1\), then \(f\) is the multiplicative function with prime-power values \(g\), that is, the arithmetic function \(n \mapsto \prod_{q \mid n} g(v_q(n))\) for \(n \ge 1\), where \(q\) runs over the primes dividing \(n\) and \(v_q(n)\) is the exponent of \(q\) in \(n\).

theorem eq_multiplicativeOfPrimePowers [CommMonoidWithZero R] {f : ArithmeticFunction R}
    (hf : f.IsMultiplicative) (g : ℕ → R)
    (h : ∀ p m : ℕ, p.Prime → m ≠ 0 → f (p ^ m) = g m) :
    f = multiplicativeOfPrimePowers g
Sources
  • Emil Daniel Schwab, Fibonacci Numbers via Dirichlet Convolution and Lucas Numbers via Unitary Convolution, Journal of Integer Sequences 28 (2025), Article 25.1.7, Section 1.3 (a multiplicative function is determined by its values at the prime powers).
Uses 4
Statement usesMultiplicative function with prescribed values at prime powers
Proof usesMultiplicativity of the function with prescribed prime-power values · The function with prescribed prime-power values is \(1\) at \(1\) · The function with prescribed prime-power values at a prime power

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.