Divisor-power sums

DefinitionDivisor-power sum with complex exponent#✓fully proved

For a complex number \(s\), \(\sigma_s\) is the complex-valued arithmetic function with \(\sigma_s(n) = \sum_{d \mid n} d^s\) for every natural number \(n \ge 1\), where \(d^s\) is the complex power, and \(\sigma_s(0) = 0\).

noncomputable def sigmaR (s : ℂ) : ArithmeticFunction ℂ where
  toFun := fun n => ∑ d ∈ n.divisors, (d : ℂ) ^ s
  map_zero' := by simp

Used by 4

Used byDivisor-sum formula for the complex-exponent divisor sum · The complex-exponent divisor sum at one · Natural exponents give the classical divisor function · The complex-exponent divisor sum at exponent zero counts divisors

TheoremDivisor-sum formula for the complex-exponent divisor sum#✓fully proved

For every natural number \(n\) and complex number \(s\), the divisor-power sum \(\sigma_s\) with complex exponent \(s\) satisfies \(\sigma_s(n) = \sum_{d \mid n} d^s\), the sum running over the positive divisors \(d\) of \(n\); for \(n = 0\) the sum is empty, so \(\sigma_s(0) = 0\).

theorem sigmaR_apply {n : ℕ} {s : ℂ} :
    sigmaR s n = ∑ d ∈ n.divisors, (d : ℂ) ^ s

Uses 1 · Used by 3

Statement usesDivisor-power sum with complex exponent

Used byThe complex-exponent divisor sum at one · Natural exponents give the classical divisor function · The complex-exponent divisor sum at exponent zero counts divisors

TheoremThe complex-exponent divisor sum at one#✓fully proved

For every complex number \(s\), the divisor-power sum \(\sigma_s(n) = \sum_{d \mid n} d^s\) with complex exponent \(s\) satisfies \(\sigma_s(1) = 1\).

@[simp]
theorem sigmaR_apply_one (s : ℂ) : sigmaR s 1 = 1

Uses 2

Statement usesDivisor-power sum with complex exponent

Proof usesDivisor-sum formula for the complex-exponent divisor sum

TheoremThe complex-exponent divisor sum at exponent zero counts divisors#✓fully proved

Let \(\sigma_s(n) = \sum_{d \mid n} d^s\) be the divisor-power sum with complex exponent \(s\). For every natural number \(n\), \(\sigma_0(n)\) equals the number of positive divisors of \(n\), with the convention that \(0\) has no divisors, so that \(\sigma_0(0) = 0\).

@[simp]
theorem sigmaR_zero_apply (n : ℕ) :
    sigmaR 0 n = (n.divisors.card : ℂ)

Uses 2

Statement usesDivisor-power sum with complex exponent

Proof usesDivisor-sum formula for the complex-exponent divisor sum

TheoremNatural exponents give the classical divisor function#✓fully proved

For all natural numbers \(k\) and \(n\), the value at \(n\) of the complex-exponent divisor sum \(\sum_{d \mid n} d^s\) with \(s = k\) equals the natural number \(\sigma_k(n) = \sum_{d \mid n} d^k\), viewed as a complex number.

@[simp]
theorem sigmaR_natCast_apply (k n : ℕ) :
    sigmaR (k : ℂ) n = (sigma k n : ℂ)

Uses 2

Statement usesDivisor-power sum with complex exponent

Proof usesDivisor-sum formula for the complex-exponent divisor sum

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.