Formal derivatives of univariate power series #

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).

source

theorem PowerSeries.constantCoeff_iterate_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) :

constantCoeff ((⇑derivative)^[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.

source

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

derivative ↑f = ↑(Polynomial.derivative f)

source

@[simp]

theorem PowerSeries.derivative_X {R : Type u_1} [CommSemiring R] :

derivative X = 1

source

theorem PowerSeries.iterate_derivative_zero {R : Type u_1} [CommSemiring R] {k : ℕ} :

(⇑derivative)^[k] 0 = 0

source

theorem PowerSeries.derivative_monomial {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) :

derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)

source

@[simp]

theorem PowerSeries.derivative_monomial_succ {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) :

derivative ((monomial (n + 1)) a) = (monomial n) (a * (↑n + 1))

source

theorem PowerSeries.derivative_C_mul_X {R : Type u_1} [CommSemiring R] (a : R) :

derivative (C a * X) = C a

source

theorem PowerSeries.derivative_C_mul_X_pow {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) :

derivative (C a * X ^ n) = C (a * ↑n) * X ^ (n - 1)

source

theorem PowerSeries.derivative_C_mul_X_sq {R : Type u_1} [CommSemiring R] (a : R) :

derivative (C a * X ^ 2) = C (a * 2) * X

source

theorem PowerSeries.derivative_X_pow {R : Type u_1} [CommSemiring R] (n : ℕ) :

derivative (X ^ n) = C ↑n * X ^ (n - 1)

source

theorem PowerSeries.derivative_X_pow_succ {R : Type u_1} [CommSemiring R] (n : ℕ) :

derivative (X ^ (n + 1)) = C (↑n + 1) * X ^ n

source

theorem PowerSeries.derivative_X_sq {R : Type u_1} [CommSemiring R] :

derivative (X ^ 2) = C 2 * X

source

theorem PowerSeries.derivative_X_add_C {R : Type u_1} [CommSemiring R] (c : R) :

derivative (X + C c) = 1

source

theorem PowerSeries.iterate_derivative_sum {R : Type u_1} [CommSemiring R] {ι : Type u_2} (k : ℕ) (s : Finset ι) (f : ι → PowerSeries R) :

(⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

source

@[simp]

theorem PowerSeries.iterate_derivative_smul {R : Type u_1} [CommSemiring R] {S : Type u_2} [SMul S (PowerSeries R)] [LinearMap.CompatibleSMul (PowerSeries R) (PowerSeries R) S R] (s : S) (f : PowerSeries R) (k : ℕ) :

(⇑derivative)^[k] (s • f) = s • (⇑derivative)^[k] f

source

theorem PowerSeries.trunc_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) :

(trunc n) (derivative f) = Polynomial.derivative ((trunc (n + 1)) f)

source

theorem PowerSeries.trunc_derivative' {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (n : ℕ) :

(trunc (n - 1)) (derivative f) = Polynomial.derivative ((trunc n) f)

source

theorem PowerSeries.derivative_pow {R : Type u_1} [CommSemiring R] (g : PowerSeries R) (n : ℕ) :

derivative (g ^ n) = ↑n * g ^ (n - 1) * derivative g

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

source

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

f = g

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

source

@[simp]

theorem PowerSeries.derivative_inv {R : Type u_1} [CommRing R] (f : (PowerSeries R)ˣ) :

derivative ↑f⁻¹ = -↑f⁻¹ ^ 2 * derivative ↑f

source

@[simp]

theorem PowerSeries.derivative_invOf {R : Type u_1} [CommRing R] (f : PowerSeries R) [Invertible f] :

derivative ⅟f = -⅟f ^ 2 * derivative f

source

@[simp]

theorem PowerSeries.derivative_inv' {R : Type u_1} [Field R] (f : PowerSeries R) :

derivative f⁻¹ = -f⁻¹ ^ 2 * derivative f

source

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

derivative (subst g f) = subst g (derivative f) * derivative g

source

@[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