Liouville's divisor-function identity

TheoremLiouville's divisor-function identity for all natural numbers#✓fully proved

For every natural number \(n\), writing \(\tau(d)\) for the number of positive divisors of \(d\),

\[\left(\sum_{d \mid n} \tau(d)\right)^2 = \sum_{d \mid n} \tau(d)^3,\]

where both sums run over the positive divisors \(d\) of \(n\). By convention the divisor set of \(0\) is empty here, so for \(n = 0\) both sides are \(0\).

theorem liouville_divisor_function_identity_general (n : ℕ) :
    (∑ d ∈ n.divisors, d.divisors.card) ^ 2 =
      ∑ d ∈ n.divisors, (d.divisors.card) ^ 3

Used by 1

Used byLiouville's divisor-function identity

TheoremLiouville's divisor-function identity#✓fully proved

For every positive integer \(n\), writing \(\tau(d)\) for the number of positive divisors of \(d\),

\[\left(\sum_{d \mid n} \tau(d)\right)^2 = \sum_{d \mid n} \tau(d)^3,\]

where both sums run over the positive divisors \(d\) of \(n\).

theorem liouville_divisor_function_identity
    (n : ℕ) (hn : 0 < n) :
    (∑ d ∈ n.divisors, d.divisors.card) ^ 2 =
      ∑ d ∈ n.divisors, (d.divisors.card) ^ 3

Sources

• Seon-Hong Kim and Kenneth B. Stolarsky, “Translations and Extensions of the Nicomachean Identity,” Journal of Integer Sequences 27 (2024), lines 317–322, https://cs.uwaterloo.ca/journals/JIS/VOL27/Kim/kim8.tex. Here d.divisors.card is the source's divisor-count function. It follows from liouville_divisor_function_identity_general; the hypothesis hn is unused and keeps the source's shape (at n = 0 both sides are 0, since Nat.divisors 0 = ∅).

Uses 1

Proof usesLiouville's divisor-function identity for all natural numbers

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.