Arithmetic derivative

DefinitionArithmetic derivative#✓fully proved

For a natural number \(n\), the arithmetic derivative of \(n\) is

\[D(n) = \sum_{p} \nu_p(n) \cdot \frac{n}{p},\]

where the sum runs over the prime factors \(p\) of \(n\) and \(\nu_p(n)\) is the exponent of \(p\) in the prime factorization of \(n\). Since \(0\) and \(1\) have no prime factors, \(D(0) = D(1) = 0\).

def arithmeticDerivative (n : ℕ) : ℕ :=
  ∑ p ∈ n.primeFactors, n.factorization p * (n / p)
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2, equation (2).
Used by 12
Used byArithmetic derivative over a superset of the prime factors · Leibniz rule for the arithmetic derivative · Arithmetic derivative of one · Arithmetic derivative of a prime · Arithmetic derivative of zero · Bounds for the arithmetic derivative · Prime tetrations where the arithmetic derivative and the Collatz map commute · Prime roots give semiprime solutions · Positive solutions of the Collatz arithmetic differential equation are composite · No special semiprime solves the derivative–Collatz equation · Positive solutions of the Collatz arithmetic differential equation are odd · Prime gap bound for semiprime solutions

TheoremArithmetic derivative of zero#✓fully proved

The arithmetic derivative of \(0\) is \(0\): \(D(0) = 0\).

theorem arithmeticDerivative_zero : arithmeticDerivative 0 = 0
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2.
Uses 1 · Used by 1
Statement usesArithmetic derivative
Used byLeibniz rule for the arithmetic derivative

TheoremArithmetic derivative of one#✓fully proved

The arithmetic derivative of \(1\) is \(0\): \(D(1) = 0\).

theorem arithmeticDerivative_one : arithmeticDerivative 1 = 0
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2.
Uses 1
Statement usesArithmetic derivative

TheoremArithmetic derivative of a prime#✓fully proved

For every prime \(p\), the arithmetic derivative of \(p\) is \(1\): \(D(p) = 1\).

theorem arithmeticDerivative_prime {p : ℕ} (hp : p.Prime) : arithmeticDerivative p = 1
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2.
Uses 1
Statement usesArithmetic derivative

TheoremArithmetic derivative over a superset of the prime factors#✓fully proved

Let \(n\) be a natural number and let \(s\) be a finite set of natural numbers containing every prime factor of \(n\). Then the arithmetic derivative of \(n\) is \(D(n) = \sum_{p \in s} \nu_p(n) \cdot (n / p)\), where \(\nu_p(n)\) is the exponent of \(p\) in the prime factorization of \(n\) (zero when \(p\) is not a prime factor of \(n\)) and \(n / p\) is division in the natural numbers, rounded down.

theorem arithmeticDerivative_eq_sum_of_subset {n : ℕ} {s : Finset ℕ}
    (hs : n.primeFactors ⊆ s) :
    arithmeticDerivative n = ∑ p ∈ s, n.factorization p * (n / p)
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2, equation (2).
Uses 1 · Used by 1
Statement usesArithmetic derivative
Used byLeibniz rule for the arithmetic derivative

TheoremLeibniz rule for the arithmetic derivative#✓fully proved

For all natural numbers \(m\) and \(n\), the arithmetic derivative \(D\) satisfies \(D(mn) = D(m)\,n + m\,D(n)\).

theorem arithmeticDerivative_mul (m n : ℕ) :
    arithmeticDerivative (m * n) =
      arithmeticDerivative m * n + m * arithmeticDerivative n
Sources
  • Zachary P. Bradshaw, On a Family of Solutions to Arithmetic Differential Equations Involving the Collatz Map, Journal of Integer Sequences 28 (2025), Article 25.1.8, Section 2, equation (1).
Uses 3
Statement usesArithmetic derivative
Proof usesArithmetic derivative over a superset of the prime factors · Arithmetic derivative of zero
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.