The Arithmetic Function `σ`

Stream: mathlib4

[Alex Kontorovich]

As we're (slowly) working through Iwaniec-Kowalski (see here for Ch. 1), we realized that the σ function (sum of divisor powers) is currently defined as an ArithmeticFunction where the powers k (and hence codomain) are the naturals. There's a lot of API already developed in that setting. But for things like Fourier coefficients of nonholomorphic Eisenstein series (e.g.), we'll want to allow k to be a complex number, and hence σ to take complex values. In the short term, we made our own definition:

noncomputable def sigmaC {R : Type*} [Semiring R] [HPow R R R] (s : R) : ArithmeticFunction R where
  toFun := fun n ↦ ∑ d ∈ n.divisors, (d : R) ^ s
  map_zero' := by simp

which can handle complex or natural exponents. But before we get too far, it'd be great to get community input on whether it'd be better to refactor the existing σ function? @Michael Stoll @David Loeffler

[Michael Stoll]

My gut feeling is that we should keep the version with natural exponents as converting between pow and cpow is a bit of a hassle.
But it would certainly be OK to use the more general one version to refactor proofs of API lemmas for the natural exponent version (if this gives simpler proofs, which I'm not necessarily convinced of).