Formal derivatives of univariate power series

This file defines PowerSeries.derivative, the formal derivative of a univariate power series, as a Derivation R R⟦X⟧ R⟦X⟧.

See also MvPowerSeries.pderiv for the multivariate setting.

Main definitions

• PowerSeries.derivative: the formal derivative, as a derivation.

Main results

• PowerSeries.coeff_derivative: coefficient formula coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1).
• PowerSeries.derivative_coe: compatibility with Polynomial.derivative.
• PowerSeries.trunc_derivative: truncation commutes with differentiation.
• PowerSeries.derivative.ext: a power series is determined by its constant term and derivative.
• PowerSeries.derivative_pow: power rule.
• PowerSeries.derivative_inv, PowerSeries.derivative_inv': derivative of an inverse.
• PowerSeries.derivative_subst: chain rule for power series substitution.

noncomputable def PowerSeries.derivative (R : Type u_1) [CommSemiring R] : Derivation R (PowerSeries R) (PowerSeries R)

The formal derivative of a formal power series

Equations

• PowerSeries.derivative R = MvPowerSeries.pderiv R ()

def PowerSeries.«termD⁄dX» : Lean.ParserDescr

Abbreviation of PowerSeries.derivative, the formal derivative on R⟦X⟧

Equations

• PowerSeries.«termD⁄dX» = Lean.ParserDescr.node `PowerSeries.«termD⁄dX» 1024 (Lean.ParserDescr.symbol "d⁄dX")

@[simp]

theorem PowerSeries.derivative_C {R : Type u_1} [CommSemiring R] {r : R} : (derivative R) (C r) = 0

theorem PowerSeries.derivative_one {R : Type u_1} [CommSemiring R] : (derivative R) 1 = 0

theorem PowerSeries.coeff_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : (coeff n) ((derivative R) f) = (coeff (n + 1)) f * (↑n + 1)

theorem PowerSeries.coeff_iterate_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n k : ℕ) : (coeff k) ((⇑(derivative R))^[n] f) = ↑((k + 1).ascFactorial n) * (coeff (k + n)) f

The k-th coefficient of the n-th formal derivative: differentiating n times multiplies the (k + n)-th coefficient by the ascending factorial (k + 1)(k + 2) ⋯ (k + n).

theorem PowerSeries.constantCoeff_iterate_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : constantCoeff ((⇑(derivative R))^[n] f) = ↑n.factorial * (coeff n) f

Specialisation of coeff_iterate_derivative at k = 0: the constant term of the n-th formal derivative recovers n ! times the n-th coefficient, constantCoeff (Dⁿ f) = n ! * coeff n f.

theorem PowerSeries.derivative_coe {R : Type u_1} [CommSemiring R] (f : Polynomial R) : (derivative R) ↑f = ↑(Polynomial.derivative f)

@[simp]

theorem PowerSeries.derivative_X {R : Type u_1} [CommSemiring R] : (derivative R) X = 1

theorem PowerSeries.trunc_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : (trunc n) ((derivative R) f) = Polynomial.derivative ((trunc (n + 1)) f)

theorem PowerSeries.trunc_derivative' {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : (trunc (n - 1)) ((derivative R) f) = Polynomial.derivative ((trunc n) f)

theorem PowerSeries.derivative_pow {R : Type u_1} [CommSemiring R] (g : PowerSeries R) (n : ℕ) : (derivative R) (g ^ n) = ↑n * g ^ (n - 1) * (derivative R) g

The derivative of g^n equals n * g^(n-1) * g'.

theorem PowerSeries.derivative.ext {R : Type u_1} [CommRing R] [IsAddTorsionFree R] {f g : PowerSeries R} (hD : (derivative R) f = (derivative R) g) (hc : constantCoeff f = constantCoeff g) : f = g

If f and g have the same constant term and derivative, then they are equal.

@[simp]

theorem PowerSeries.derivative_inv {R : Type u_1} [CommRing R] (f : (PowerSeries R)ˣ) : (derivative R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (derivative R) ↑f

@[simp]

theorem PowerSeries.derivative_invOf {R : Type u_1} [CommRing R] (f : PowerSeries R) [Invertible f] : (derivative R) ⅟f = -⅟f ^ 2 * (derivative R) f

@[simp]

theorem PowerSeries.derivative_inv' {R : Type u_1} [Field R] (f : PowerSeries R) : (derivative R) f⁻¹ = -f⁻¹ ^ 2 * (derivative R) f

theorem PowerSeries.derivative_subst {R : Type u_1} [CommRing R] {f g : PowerSeries R} (hg : HasSubst g) : (derivative R) (subst g f) = subst g ((derivative R) f) * (derivative R) g

@[deprecated PowerSeries.derivative (since := "2026-06-26")]

noncomputable def PowerSeries.derivativeFun {R : Type u_1} [CommSemiring R] (f : PowerSeries R) : PowerSeries R

The formal derivative of a power series in one variable. This is defined here as a function, but will be packaged as a derivation derivative on R⟦X⟧.

Equations

• f.derivativeFun = (↑(PowerSeries.derivative R)).toFun f

@[deprecated "Use Derivation.map_add" (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_add {R : Type u_1} [CommSemiring R] (f g : PowerSeries R) : (f + g).derivativeFun = f.derivativeFun + g.derivativeFun

@[deprecated "Use Derivation.leibniz" (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_mul {R : Type u_1} [CommSemiring R] (f g : PowerSeries R) : (f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun

@[deprecated "Use Derivation.map_one_eq_zero" (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_one {R : Type u_1} [CommSemiring R] : derivativeFun 1 = 0

@[deprecated "Use Derivation.map_smul" (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_smul {R : Type u_1} [CommSemiring R] (r : R) (f : PowerSeries R) : (r • f).derivativeFun = r • f.derivativeFun

@[deprecated PowerSeries.derivative_C (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_C {R : Type u_1} [CommSemiring R] {r : R} : (derivative R) (C r) = 0

Alias of PowerSeries.derivative_C.

@[deprecated PowerSeries.coeff_derivative (since := "2026-06-26")]

theorem PowerSeries.coeff_derivativeFun {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : (coeff n) ((derivative R) f) = (coeff (n + 1)) f * (↑n + 1)

Alias of PowerSeries.coeff_derivative.

@[deprecated PowerSeries.derivative_coe (since := "2026-06-26")]

theorem PowerSeries.derivativeFun_coe {R : Type u_1} [CommSemiring R] (f : Polynomial R) : (derivative R) ↑f = ↑(Polynomial.derivative f)

Alias of PowerSeries.derivative_coe.

@[deprecated PowerSeries.trunc_derivative (since := "2026-06-26")]

theorem PowerSeries.trunc_derivativeFun {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) : (trunc n) ((derivative R) f) = Polynomial.derivative ((trunc (n + 1)) f)

Alias of PowerSeries.trunc_derivative.