Divisor-sum power series

This file defines the generating series s_k(q) = ∑_{n ≥ 1} σ_k(n) qⁿ of the divisor-sum function σ k.

Main definitions

• TauCeti.divisorSumSeries k: the power series with n-th coefficient σ k n.

noncomputable def TauCeti.divisorSumSeries (k : ℕ) : PowerSeries ℤ

The divisor-sum series s_k(q) = ∑_{n ≥ 1} σ_k(n) qⁿ in ℤ⟦q⟧, the power series expansion of the Lambert series ∑_{n ≥ 1} nᵏ qⁿ / (1 - qⁿ). Its constant coefficient is σ_k(0) = 0.

Equations

• TauCeti.divisorSumSeries k = PowerSeries.mk fun (n : ℕ) => ↑((ArithmeticFunction.sigma k) n)

@[simp]

theorem TauCeti.coeff_divisorSumSeries (k n : ℕ) : (PowerSeries.coeff n) (divisorSumSeries k) = ↑((ArithmeticFunction.sigma k) n)

@[simp]

theorem TauCeti.constantCoeff_divisorSumSeries (k : ℕ) : PowerSeries.constantCoeff (divisorSumSeries k) = 0