Jordan's totient function

DefinitionJordan's totient function#✓fully proved

For a natural number \(k\), Jordan's totient function \(J_k\) is the arithmetic function with natural-number values given by \(J_k(0) = 0\) and, for \(n \ne 0\),

\[J_k(n) = \prod_{p \mid n} p^{k(v_p(n) - 1)} (p^k - 1),\]

where the product runs over the prime divisors \(p\) of \(n\) and \(v_p(n)\) is the exponent of \(p\) in the prime factorization of \(n\).

For \(k \ge 1\) and \(n \ge 1\) this equals \(n^k \prod_{p \mid n} (1 - p^{-k})\), the form in which the function is usually defined.

public def jordanTotient (k : ℕ) : ArithmeticFunction ℕ where
  toFun n :=
    if n = 0 then 0
    else ∏ p ∈ n.primeFactors, p ^ (k * (n.factorization p - 1)) *
      (p ^ k - 1)
  map_zero' := ite_eq_left rfl

Sources

• Yuan He, On the mean values of products of Dirichlet L-functions at positive integers, arXiv:2310.18048v3, equation (1.7).

Used by 10

Used byJordan's totient function is multiplicative · Jordan's totient at one · Prime-factorization formula for Jordan's totient · Euler product for Jordan's totient · Möbius sum for Jordan's totient · Cleared-denominator Euler product for Jordan's totient · Jordan's totient of order one is Euler's totient · Jordan's totient at primes · Jordan's totient at prime powers · Jordan's totient at zero

TheoremJordan's totient at zero#✓fully proved

For every natural number \(k\), the Jordan totient function satisfies \(J_k(0) = 0\); this is the convention extending \(J_k\) to \(0\).

public theorem jordanTotient_zero (k : ℕ) :
    jordanTotient k 0 = 0

Uses 1 · Used by 1

Statement usesJordan's totient function

Used byJordan's totient of order one is Euler's totient

TheoremJordan's totient at one#✓fully proved

For every natural number \(k\), the Jordan totient function satisfies \(J_k(1) = 1\).

public theorem jordanTotient_apply_one (k : ℕ) :
    jordanTotient k 1 = 1

Uses 1 · Used by 1

Statement usesJordan's totient function

Used byJordan's totient function is multiplicative

TheoremPrime-factorization formula for Jordan's totient#✓fully proved

For all natural numbers \(k\) and \(n \neq 0\), the Jordan totient function satisfies

\[J_k(n) = \prod_{p \mid n} p^{k(v_p(n) - 1)} (p^k - 1),\]

where the product runs over the distinct primes \(p\) dividing \(n\) and \(v_p(n)\) is the exponent of \(p\) in the prime factorization of \(n\).

public theorem jordanTotient_eq_prod_factorization {k n : ℕ}
    (hn : n ≠ 0) :
    jordanTotient k n = ∏ p ∈ n.primeFactors,
      p ^ (k * (n.factorization p - 1)) * (p ^ k - 1)

Sources

• Yuan He, arXiv:2310.18048v3, equation (1.7), in integral form.

Uses 1 · Used by 4

Statement usesJordan's totient function

Used byJordan's totient function is multiplicative · Cleared-denominator Euler product for Jordan's totient · Jordan's totient of order one is Euler's totient · Jordan's totient at prime powers

TheoremJordan's totient at prime powers#✓fully proved

For every natural number \(k\), every prime \(p\) and every integer \(e \ge 1\), the Jordan totient function satisfies \(J_k(p^e) = p^{k(e-1)}(p^k - 1)\).

public theorem jordanTotient_prime_pow {k p e : ℕ} (hp : p.Prime)
    (he : 0 < e) :
    jordanTotient k (p ^ e) =
      p ^ (k * (e - 1)) * (p ^ k - 1)

Uses 2 · Used by 2

Statement usesJordan's totient function

Proof usesPrime-factorization formula for Jordan's totient

Used byMöbius sum for Jordan's totient · Jordan's totient at primes

TheoremJordan's totient at primes#✓fully proved

For every natural number \(k\) and every prime \(p\), the Jordan totient function satisfies \(J_k(p) = p^k - 1\).

public theorem jordanTotient_prime {k p : ℕ} (hp : p.Prime) :
    jordanTotient k p = p ^ k - 1

Uses 2

Statement usesJordan's totient function

Proof usesJordan's totient at prime powers

TheoremJordan's totient function is multiplicative#✓fully proved

For every natural number \(k\), the Jordan totient function \(J_k\) is multiplicative: \(J_k(1) = 1\), and \(J_k(mn) = J_k(m) J_k(n)\) for all coprime natural numbers \(m\) and \(n\).

public theorem isMultiplicative_jordanTotient (k : ℕ) :
    IsMultiplicative (jordanTotient k)

Uses 3 · Used by 1

Statement usesJordan's totient function

Proof usesJordan's totient at one · Prime-factorization formula for Jordan's totient

Used byMöbius sum for Jordan's totient

TheoremJordan's totient of order one is Euler's totient#✓fully proved

For every natural number \(n\), \(J_1(n) = \varphi(n)\), where \(J_1\) is the Jordan totient function \(J_k\) with \(k = 1\) and \(\varphi\) is Euler's totient function; at \(n = 0\) both sides are \(0\).

public theorem jordanTotient_one_apply (n : ℕ) :
    jordanTotient 1 n = n.totient

Sources

• Yuan He, arXiv:2310.18048v3, equation (1.7).

Uses 3

Statement usesJordan's totient function

Proof usesPrime-factorization formula for Jordan's totient · Jordan's totient at zero

TheoremMöbius sum for Jordan's totient#✓fully proved

For all natural numbers \(k\) and \(n \neq 0\), the Jordan totient function satisfies, as an identity of integers,

\[J_k(n) = \sum_{d \mid n} \mu(n/d)\, d^k,\]

where \(d\) runs over the positive divisors of \(n\) and \(\mu\) is the Möbius function.

public theorem jordanTotient_eq_sum_moebius {k n : ℕ} (hn : n ≠ 0) :
    ((jordanTotient k n : ℕ) : ℤ) =
      ∑ d ∈ n.divisors, moebius (n / d) * (d : ℤ) ^ k

Sources

• Yuan He, arXiv:2310.18048v3, equation (2.7), stated there for positive k; here k = 0 is also allowed.

Uses 3

Statement usesJordan's totient function

Proof usesJordan's totient function is multiplicative · Jordan's totient at prime powers

TheoremCleared-denominator Euler product for Jordan's totient#✓fully proved

For all natural numbers \(k\) and \(n \neq 0\), the Jordan totient function satisfies

\[J_k(n) \prod_{p \mid n} p^k = n^k \prod_{p \mid n} (p^k - 1),\]

where both products run over the distinct primes \(p\) dividing \(n\).

public theorem jordanTotient_mul_prod_primeFactors_pow {k n : ℕ}
    (hn : n ≠ 0) :
    jordanTotient k n * ∏ p ∈ n.primeFactors, p ^ k =
      n ^ k * ∏ p ∈ n.primeFactors, (p ^ k - 1)

Sources

• Yuan He, arXiv:2310.18048v3, equation (1.7), with denominators cleared.

Uses 2 · Used by 1

Statement usesJordan's totient function

Proof usesPrime-factorization formula for Jordan's totient

Used byEuler product for Jordan's totient

TheoremEuler product for Jordan's totient#✓fully proved

For all natural numbers \(k\) and \(n \neq 0\), the Jordan totient function satisfies, as an identity of rational numbers,

\[J_k(n) = n^k \prod_{p \mid n} \left(1 - \frac{1}{p^k}\right),\]

where the product runs over the distinct primes \(p\) dividing \(n\).

public theorem jordanTotient_eq_rational_prod {k n : ℕ} (hn : n ≠ 0) :
    ((jordanTotient k n : ℕ) : ℚ) =
      (n : ℚ) ^ k *
        ∏ p ∈ n.primeFactors, (1 - 1 / (p : ℚ) ^ k)

Sources

• Yuan He, arXiv:2310.18048v3, equation (1.7), stated there for positive k; here k = 0 is also allowed.

Uses 2

Statement usesJordan's totient function

Proof usesCleared-denominator Euler product for Jordan's totient

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.