Evaluating divisor-sum series

The integral divisor-sum series converges at a parameter of norm less than one in a complete non-archimedean normed ring with ‖1‖ = 1. Its value is the sum of its evaluated coefficients. In a commutative target ring, evalIntSeries_divisorSumSeries identifies evaluation of the formal series divisorSumSeries k under evalIntSeries with its analytic value divisorSumAt k q.

theorem TauCeti.summable_divisorSumSeries {K : Type u_1} [NormedRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (k : ℕ) {q : K} (hq : ‖q‖ < 1) : Summable fun (n : ℕ) => ↑↑((ArithmeticFunction.sigma k) n) * q ^ n

The divisor-sum series s_k(q) = ∑ σ_k(n) q^n converges for ‖q‖ < 1.

noncomputable def TauCeti.divisorSumAt {K : Type u_1} [NormedRing K] (k : ℕ) (q : K) : K

Evaluation of the integral divisor-sum series in a complete non-archimedean normed ring. Its convergence for ‖q‖ < 1 is summable_divisorSumSeries.

Equations

• TauCeti.divisorSumAt k q = ∑' (n : ℕ), ↑↑((ArithmeticFunction.sigma k) n) * q ^ n

theorem TauCeti.divisorSumAt_def {K : Type u_1} [NormedRing K] (k : ℕ) (q : K) : divisorSumAt k q = ∑' (n : ℕ), ↑↑((ArithmeticFunction.sigma k) n) * q ^ n

The value of a divisor-sum series is its defining sum.

@[simp]

theorem TauCeti.evalIntSeries_divisorSumSeries {K : Type u_2} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (k : ℕ) (q : K) (hq : ‖q‖ < 1) : (evalIntSeries q hq) (divisorSumSeries k) = divisorSumAt k q

Evaluating the integral divisor-sum series gives its convergent analytic value.