Derivative identities for power series

For a power series v over a commutative semiring and e, n : ℕ with e ≠ 0,

e • coeff (e * (n + 1)) (v ^ (n + 1)) = coeff (e * (n + 1) - 1) (v ^ n * v'),

and for all e, n : ℕ (including e = 0),

e • coeff (e * (n + 1)) (v ^ (n + 1)) = coeff (e * (n + 1)) (X * (v ^ n * v')).

Over a ring in which n + 1 is not a zero divisor this is the coefficient of X ^ (e * (n + 1) - 1) in (v ^ (n + 1))' = (n + 1) v ^ n v', divided by n + 1. The identity holds over every commutative semiring because both sides are polynomials with natural-number coefficients in the coefficients of v; the proof specializes the generic power series with coefficients the variables of MvPolynomial ℕ ℕ.

In positive characteristic p the division by n + 1 is unavailable when p ∣ n + 1, and this identity is what replaces it. Applied to the inverse of a unit u ∈ R⟦X⟧ˣ over a commutative ring, since (u⁻¹)' = -(u⁻¹)² u', it yields the universal coefficient identity

(e : R) * coeff (e * k) (u ^ (-k)) + coeff (e * k - 1) (u ^ (-k - 1) * u') = 0

for e, k ≥ 1, which governs the behaviour of residues under a substitution X ↦ φ of order e.

Substitution by a series satisfying a' = w(a) intertwines the weighted derivative w d/dX to the ordinary derivative. The iterated chain rule then reads the constant coefficient of an iterated weighted derivative as a factorial-scaled coefficient after substitution.

Main results

• PowerSeries.derivative_subst_of_derivative_eq_subst: the weighted chain rule for a substitution satisfying a' = w(a).
• PowerSeries.iterate_derivative_subst, PowerSeries.constantCoeff_iterate_of_derivative_subst: iteration and coefficient extraction for an operator intertwined with the derivative by substitution.
• PowerSeries.derivative_map: the derivative commutes with change of coefficients.
• PowerSeries.iterate_derivative_coe: iterated derivatives of a polynomial are computed as polynomials.
• PowerSeries.coeff_iterate_derivative_eq_descFactorial: the M-th coefficient of f⁽ⁱ⁾ is (M + i) (M + i - 1) ⋯ (M + 1) times the (M + i)-th coefficient of f.
• PowerSeries.coeff_X_pow_mul_iterate_derivative: Xⁱ f⁽ⁱ⁾ has M-th coefficient M (M - 1) ⋯ (M - i + 1) times that of f.
• PowerSeries.derivative_algebraMap_polynomial, PowerSeries.derivative_polynomial_smul: the derivative of the image of a polynomial, and the Leibniz rule for the action of R[X] on A⟦X⟧.
• PowerSeries.polynomial_map_algebraMap_smul: the actions of R[X] and S[X] on A⟦X⟧ agree along a scalar tower R → S → A.
• PowerSeries.polynomial_C_smul, PowerSeries.polynomial_X_smul, PowerSeries.polynomial_X_pow_smul, PowerSeries.polynomial_monomial_smul: under the action of R[X] on A⟦X⟧, constants act as scalars, Xʲ as multiplication by Xʲ, and a Xʲ as a times multiplication by Xʲ.
• PowerSeries.smul_derivative_mem: a submodule over R[X] stable under p • d⁄dX contains (p * r ^ 2) • x' whenever it contains r • x.
• PowerSeries.coeff_eq_zero_of_derivative_eq_zero: in prime characteristic p, a series with zero derivative is supported on degrees divisible by p.
• PowerSeries.nsmul_coeff_mul_succ_pow_succ_eq_coeff_X_mul_pow_mul_derivative, PowerSeries.nsmul_coeff_mul_succ_pow_succ_eq_coeff_pow_mul_derivative: e • coeff (e * (n + 1)) (v ^ (n + 1)) = coeff (e * (n + 1) - 1) (v ^ n * v') for e ≠ 0, and its X *-shifted form for all e.
• PowerSeries.coeff_succ_pow_succ_eq_coeff_pow_mul_derivative: the e = 1 case coeff (n + 1) (v ^ (n + 1)) = coeff n (v ^ n * v').
• PowerSeries.mul_coeff_val_zpow_neg_add_coeff_val_zpow_neg_sub_one_mul_derivative_eq_zero: for a unit u : R⟦X⟧ˣ over a commutative ring and e, k ≥ 1, (e : R) * coeff (e * k) (u ^ (-k)) + coeff (e * k - 1) (u ^ (-k - 1) * u') = 0.

@[simp]

theorem PowerSeries.derivative_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : PowerSeries R) (f : R →+* S) : derivative ((map f) φ) = (map f) (derivative φ)

The derivative of power series commutes with change of coefficients.

theorem PowerSeries.iterate_derivative_coe {R : Type u_1} [CommSemiring R] (p : Polynomial R) (m : ℕ) : (⇑derivative)^[m] ↑p = ↑((⇑Polynomial.derivative)^[m] p)

Iterated derivatives of a polynomial, viewed as a power series, are computed as polynomials.

theorem PowerSeries.coeff_iterate_derivative_eq_descFactorial {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (i M : ℕ) : (coeff M) ((⇑derivative)^[i] f) = ↑((M + i).descFactorial i) * (coeff (M + i)) f

The M-th coefficient of the i-th derivative is the falling factorial (M + i) (M + i - 1) ⋯ (M + 1) times the (M + i)-th coefficient.

theorem PowerSeries.coeff_X_pow_mul_iterate_derivative {R : Type u_1} [CommSemiring R] (f : PowerSeries R) (i M : ℕ) : (coeff M) (X ^ i * (⇑derivative)^[i] f) = ↑(M.descFactorial i) * (coeff M) f

Multiplying the i-th derivative by Xⁱ multiplies the M-th coefficient by the falling factorial M (M - 1) ⋯ (M - i + 1).

theorem PowerSeries.nsmul_coeff_mul_succ_pow_succ_eq_coeff_X_mul_pow_mul_derivative {R : Type u_1} [CommSemiring R] (v : PowerSeries R) (e n : ℕ) : e • (coeff (e * (n + 1))) (v ^ (n + 1)) = (coeff (e * (n + 1))) (X * (v ^ n * derivative v))

For a power series v over any commutative semiring and e, n : ℕ, e times the coefficient of X ^ (e * (n + 1)) in v ^ (n + 1) is the coefficient of X ^ (e * (n + 1)) in X * (v ^ n * v').

theorem PowerSeries.nsmul_coeff_mul_succ_pow_succ_eq_coeff_pow_mul_derivative {R : Type u_1} [CommSemiring R] (v : PowerSeries R) {e : ℕ} (he : e ≠ 0) (n : ℕ) : e • (coeff (e * (n + 1))) (v ^ (n + 1)) = (coeff (e * (n + 1) - 1)) (v ^ n * derivative v)

For e ≠ 0, e times the coefficient of X ^ (e * (n + 1)) in v ^ (n + 1) is the coefficient of X ^ (e * (n + 1) - 1) in v ^ n * v', over any commutative semiring.

theorem PowerSeries.coeff_succ_pow_succ_eq_coeff_pow_mul_derivative {R : Type u_1} [CommSemiring R] (v : PowerSeries R) (n : ℕ) : (coeff (n + 1)) (v ^ (n + 1)) = (coeff n) (v ^ n * derivative v)

The coefficient of X ^ (n + 1) in v ^ (n + 1) is the coefficient of X ^ n in v ^ n * v', over any commutative semiring.

theorem PowerSeries.iterate_derivative_subst {R : Type u_1} [CommRing R] {a : PowerSeries R} {D : PowerSeries R → PowerSeries R} (hD : ∀ (f : PowerSeries R), derivative (subst a f) = subst a (D f)) (f : PowerSeries R) (n : ℕ) : (⇑derivative)^[n] (subst a f) = subst a (D^[n] f)

An operator intertwined with the derivative by substitution satisfies the iterated chain rule.

theorem PowerSeries.constantCoeff_iterate_of_derivative_subst {R : Type u_1} [CommRing R] {a : PowerSeries R} {D : PowerSeries R → PowerSeries R} (ha : constantCoeff a = 0) (hD : ∀ (f : PowerSeries R), derivative (subst a f) = subst a (D f)) (f : PowerSeries R) (n : ℕ) : constantCoeff (D^[n] f) = ↑n.factorial * (coeff n) (subst a f)

If substitution by a series with zero constant coefficient intertwines an operator with the ordinary derivative, the constant coefficient of its n-th iterate is n ! times the n-th coefficient after substitution.

theorem PowerSeries.derivative_subst_of_derivative_eq_subst {R : Type u_1} [CommRing R] {a w : PowerSeries R} (ha : HasSubst a) (ha' : derivative a = subst a w) (f : PowerSeries R) : derivative (subst a f) = subst a (w * derivative f)

If a' = w(a), substitution by a intertwines the weighted derivative w d/dX with the ordinary derivative.

theorem PowerSeries.nsmul_coeff_val_inv_pow_succ_add_coeff_X_mul_val_inv_pow_add_two_mul_derivative_eq_zero {R : Type u_1} [CommRing R] (u : (PowerSeries R)ˣ) (e n : ℕ) : e • (coeff (e * (n + 1))) (↑u⁻¹ ^ (n + 1)) + (coeff (e * (n + 1))) (X * (↑u⁻¹ ^ (n + 2) * derivative ↑u)) = 0

Universal coefficient identity for a unit u : R⟦X⟧ˣ over a commutative ring, in shifted form for all e, n : ℕ: e • coeff (e * (n + 1)) (u⁻¹ ^ (n + 1)) + coeff (e * (n + 1)) (X * (u⁻¹ ^ (n + 2) * u')) = 0.

theorem PowerSeries.mul_coeff_val_zpow_neg_add_coeff_val_zpow_neg_sub_one_mul_derivative_eq_zero {R : Type u_1} [CommRing R] (u : (PowerSeries R)ˣ) {e k : ℕ} (he : e ≠ 0) (hk : k ≠ 0) : ↑e * (coeff (e * k)) ↑(u ^ (-↑k)) + (coeff (e * k - 1)) (↑(u ^ (-↑k - 1)) * derivative ↑u) = 0

Universal coefficient identity for negative powers of a unit power series. For a commutative ring R, a unit u : R⟦X⟧ˣ, and e, k ≥ 1, (e : R) * coeff (e * k) (u ^ (-k)) + coeff (e * k - 1) (u ^ (-k - 1) * u') = 0.

@[simp]

theorem PowerSeries.derivative_algebraMap_polynomial {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (p : Polynomial R) : derivative ((algebraMap (Polynomial R) (PowerSeries A)) p) = (algebraMap (Polynomial R) (PowerSeries A)) (Polynomial.derivative p)

The image of a polynomial under PowerSeries.algebraPolynomial is differentiated as a polynomial.

theorem PowerSeries.iterate_derivative_algebraMap_polynomial {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (p : Polynomial R) (m : ℕ) : (⇑derivative)^[m] ((algebraMap (Polynomial R) (PowerSeries A)) p) = (algebraMap (Polynomial R) (PowerSeries A)) ((⇑Polynomial.derivative)^[m] p)

Iterated derivatives of the image of a polynomial under PowerSeries.algebraPolynomial.

theorem PowerSeries.derivative_polynomial_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (p : Polynomial R) (f : PowerSeries A) : derivative (p • f) = Polynomial.derivative p • f + p • derivative f

The Leibniz rule for the action of R[X] on A⟦X⟧ given by PowerSeries.algebraPolynomial.

@[simp]

theorem PowerSeries.polynomial_C_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (a : R) (f : PowerSeries A) : Polynomial.C a • f = a • f

A constant polynomial acts on A⟦X⟧ through PowerSeries.algebraPolynomial as the corresponding scalar.

@[simp]

theorem PowerSeries.polynomial_X_pow_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (j : ℕ) (f : PowerSeries A) : Polynomial.X ^ j • f = X ^ j * f

The polynomial Xʲ acts on A⟦X⟧ through PowerSeries.algebraPolynomial as multiplication by the power series Xʲ.

@[simp]

theorem PowerSeries.polynomial_X_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : PowerSeries A) : Polynomial.X • f = X * f

The polynomial X acts on A⟦X⟧ through PowerSeries.algebraPolynomial as multiplication by the power series X.

@[simp]

theorem PowerSeries.polynomial_monomial_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (j : ℕ) (a : R) (f : PowerSeries A) : (Polynomial.monomial j) a • f = a • (X ^ j * f)

The monomial a Xʲ acts on A⟦X⟧ through PowerSeries.algebraPolynomial as the scalar a times multiplication by the power series Xʲ.

theorem PowerSeries.polynomial_map_algebraMap_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {S : Type u_3} [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] (q : Polynomial R) (f : PowerSeries A) : Polynomial.map (algebraMap R S) q • f = q • f

Along a scalar tower R → S → A, a polynomial over R acts on A⟦X⟧ as its image in S[X] does.

instance PowerSeries.instIsTorsionFreePolynomial_tauCeti {k : Type u_3} {K : Type u_4} [Field k] [CommRing K] [Algebra k K] : Module.IsTorsionFree (Polynomial k) (PowerSeries K)

Nonzero polynomials over the base field act injectively on power series over any commutative algebra.

theorem PowerSeries.smul_derivative_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Submodule (Polynomial R) (PowerSeries A)} {p : Polynomial R} (hS : ∀ y ∈ S, p • derivative y ∈ S) {r : Polynomial R} {x : PowerSeries A} (hx : r • x ∈ S) : (p * r ^ 2) • derivative x ∈ S

If a submodule S over R[X] is stable under p • d⁄dX and contains r • x, then it contains (p * r ^ 2) • x'. This is the induction step showing that nonzero multiples of all derivatives of a series lie in a fixed submodule.

theorem PowerSeries.coeff_eq_zero_of_derivative_eq_zero {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {f : PowerSeries R} (hf : derivative f = 0) {n : ℕ} (hn : ¬p ∣ n) : (coeff n) f = 0

In prime characteristic, a series with zero derivative has no coefficients outside the multiples of the characteristic.