 170/-! ### Sigma function (sum of divisors) -/
 171
 172/-- The sum-of-divisors function σ_k. -/
 173abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k
 174
 175@[simp] theorem sigma_def (k : ℕ) : sigma k = ArithmeticFunction.sigma k := rfl
 176
 177/-- σ_k(n) = ∑ d ∣ n, d^k. -/
 178theorem sigma_apply {k n : ℕ} : sigma k n = ∑ d ∈ n.divisors, d ^ k := by
 179  simp only [sigma, ArithmeticFunction.sigma_apply]
 180
 181/-- σ_0(n) = number of divisors of n. -/
 182theorem sigma_zero_apply {n : ℕ} : sigma 0 n = n.divisors.card := by
 183  simp only [sigma, ArithmeticFunction.sigma_zero_apply]
 184
 185/-- σ_1(n) = sum of divisors of n. -/
 186theorem sigma_one_apply {n : ℕ} : sigma 1 n = ∑ d ∈ n.divisors, d := by
 187  simp only [sigma, ArithmeticFunction.sigma_one_apply]
 188
 189/-- σ_k is multiplicative. -/
 190theorem sigma_isMultiplicative (k : ℕ) : ArithmeticFunction.IsMultiplicative (sigma k) := by
 191  simp only [sigma]
 192  exact ArithmeticFunction.isMultiplicative_sigma
 193
 194/-- σ_0(p) = 2 for prime p. -/
 195theorem sigma_zero_prime {p : ℕ} (hp : Prime p) : sigma 0 p = 2 := by
 196  have hp' : Nat.Prime p := (prime_iff p).1 hp
 197  simp only [sigma_zero_apply, hp'.divisors]
 198  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 199  rw [Finset.card_insert_of_notMem (by simp [h_ne]), Finset.card_singleton]
 200
 201/-- σ_1(p) = p + 1 for prime p. -/
 202theorem sigma_one_prime {p : ℕ} (hp : Prime p) : sigma 1 p = p + 1 := by
 203  have hp' : Nat.Prime p := (prime_iff p).1 hp

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.