Formal logarithmic derivatives of the factors 1/(1-X^f)

noncomputable def NairTenenbaum.weightedGeometricSeries (f : ℕ) (hf : f ≠ 0) : PowerSeries ℝ

A geometric series with coefficients weighted by their index.

Equations

• NairTenenbaum.weightedGeometricSeries f hf = (PowerSeries.expand f hf) (PowerSeries.mk 1)

theorem NairTenenbaum.weightedGeometricSeries_coeff (f : ℕ) (hf : f ≠ 0) (k : ℕ) : (PowerSeries.coeff k) (weightedGeometricSeries f hf) = if f ∣ k then 1 else 0

theorem NairTenenbaum.weightedGeometricSeries_mul_one_sub (f : ℕ) (hf : f ≠ 0) : weightedGeometricSeries f hf * (1 - PowerSeries.X ^ f) = 1

theorem NairTenenbaum.weightedGeometricSeries_eulerDerivative (f : ℕ) (hf : f ≠ 0) : powerSeriesEulerDerivative (weightedGeometricSeries f hf) * (1 - PowerSeries.X ^ f) = ↑f * (weightedGeometricSeries f hf - 1)