The formal Euler derivative and finite Euler products

noncomputable def NairTenenbaum.powerSeriesEulerDerivative (F : PowerSeries ℝ) : PowerSeries ℝ

The Euler derivative of a power series, multiplying each coefficient by its index.

Equations

• NairTenenbaum.powerSeriesEulerDerivative F = PowerSeries.X * PowerSeries.derivative F

theorem NairTenenbaum.powerSeriesEulerDerivative_coeff (F : PowerSeries ℝ) (k : ℕ) : (PowerSeries.coeff k) (powerSeriesEulerDerivative F) = ↑k * (PowerSeries.coeff k) F

@[simp]

theorem NairTenenbaum.powerSeriesEulerDerivative_one : powerSeriesEulerDerivative 1 = 0

theorem NairTenenbaum.powerSeriesEulerDerivative_mul (F G : PowerSeries ℝ) : powerSeriesEulerDerivative (F * G) = powerSeriesEulerDerivative F * G + F * powerSeriesEulerDerivative G

theorem NairTenenbaum.powerSeriesEulerDerivative_prod_mul_inverse {ι : Type u_1} (S : Finset ι) (F G : ι → PowerSeries ℝ) (hFG : ∀ i ∈ S, F i * G i = 1) : powerSeriesEulerDerivative (∏ i ∈ S, F i) * ∏ i ∈ S, G i = ∑ i ∈ S, powerSeriesEulerDerivative (F i) * G i