Derivatives of Formal Power Series #

This file formalizes the theory of derivatives of formal power series (FPS) from AlgebraicCombinatorics/tex/FPS/Derivatives.tex.

Main Results #

The derivative of a formal power series f = ∑ fₙ xⁿ is defined as f' = ∑ n · fₙ · x^(n-1).

Mathlib already provides PowerSeries.derivative as a derivation on R⟦X⟧. We document the correspondence with the textbook theorems and provide any additional results.

Derivative Rules (Theorem thm.fps.deriv.rules) #

(a) (f + g)' = f' + g' — derivative_add
(b) Summable families: (∑ fᵢ)' = ∑ fᵢ' — derivative_sum, derivative_summableFPSSum
(c) (c · f)' = c · f' — derivative_smul, derivative_C_mul
(d) (f · g)' = f' · g + f · g' — derivative_mul (Leibniz rule)
(e) (f / g)' = (f' · g - f · g') / g² — derivative_div (quotient rule)
(f) (g^n)' = n · g^(n-1) · g' — derivative_pow' (power rule)
(g) (f ∘ g)' = (f' ∘ g) · g' — derivative_comp (chain rule)
(h) If f' = g', then f - g is constant — derivative_eq_imp_diff_const

References #

Mathlib: Mathlib.RingTheory.PowerSeries.Derivative
Source: AlgebraicCombinatorics/tex/FPS/Derivatives.tex

Definition of Derivative #

The derivative of a formal power series is already defined in Mathlib as PowerSeries.derivative : Derivation R R⟦X⟧ R⟦X⟧.

For f = ∑ fₙ xⁿ, we have f' = ∑ (n+1) · f_{n+1} · xⁿ, or equivalently, the n-th coefficient of f' is (n+1) · f_{n+1}.

This matches Definition def.fps.deriv from the source.

Definition def.fps.deriv #

For f = ∑ fₙ xⁿ, the textbook defines f' := ∑_{n>0} n · fₙ · x^{n-1}.

Reindexing with m = n-1 (so n = m+1), this becomes: f' = ∑_{m≥0} (m+1) · f_{m+1} · x^m

This is exactly PowerSeries.derivativeFun from Mathlib, which defines: derivativeFun f := mk (fun n => coeff (n + 1) f * (n + 1))

The derivative is then packaged as a Derivation R R⟦X⟧ R⟦X⟧.

source

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

(PowerSeries.coeff n) ((PowerSeries.derivative R) f) = (PowerSeries.coeff (n + 1)) f * (↑n + 1)

Definition def.fps.deriv: The n-th coefficient of the derivative of f equals (n+1) times the (n+1)-th coefficient of f.

This is PowerSeries.coeff_derivative in Mathlib.

source

theorem AlgebraicCombinatorics.FPS.derivative_eq_mk {R : Type u_1} [CommSemiring R] (f : PowerSeries R) :

(PowerSeries.derivative R) f = PowerSeries.mk fun (n : ℕ) => (↑n + 1) * (PowerSeries.coeff (n + 1)) f

Definition def.fps.deriv: The derivative expressed in terms of mk.

For f = ∑ fₙ xⁿ, the textbook defines f' := ∑_{n>0} n · fₙ · x^{n-1}. Reindexing gives f' = mk (fun m => (m+1) * f_{m+1}).

source

theorem AlgebraicCombinatorics.FPS.derivative_eq_derivativeFun {R : Type u_1} [CommSemiring R] (f : PowerSeries R) :

(PowerSeries.derivative R) f = f.derivativeFun

The derivative operation is exactly derivativeFun from Mathlib.

source

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

(PowerSeries.coeff n) ((PowerSeries.derivative R) f) = (↑n + 1) * (PowerSeries.coeff (n + 1)) f

Alternative characterization: the coefficient of xⁿ in f' is (n+1) · f_{n+1}. This is the "shift and multiply" form of the derivative.

source

@[simp]

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

(PowerSeries.derivative R) (PowerSeries.X ^ (n + 1)) = (↑n + 1) • PowerSeries.X ^ n

The derivative of X^(n+1) is (n+1) * X^n. This is a convenient form for induction.

source

theorem AlgebraicCombinatorics.FPS.derivative_X_pow_of_pos {R : Type u_1} [CommSemiring R] {n : ℕ} (hn : 0 < n) :

(PowerSeries.derivative R) (PowerSeries.X ^ n) = ↑n • PowerSeries.X ^ (n - 1)

Derivative of X^n for n > 0.

Theorem thm.fps.deriv.rules: Derivative Rules #

We document the correspondence between the textbook theorems and Mathlib.

Part (a): Additivity #

(f + g)' = f' + g'

This is automatic since derivative is a Derivation, hence an additive map.

source

theorem AlgebraicCombinatorics.FPS.derivative_add {R : Type u_1} [CommSemiring R] (f g : PowerSeries R) :

(PowerSeries.derivative R) (f + g) = (PowerSeries.derivative R) f + (PowerSeries.derivative R) g

Theorem thm.fps.deriv.rules (a): Derivative is additive.

source

@[simp]

theorem AlgebraicCombinatorics.FPS.derivative_neg {R : Type u_2} [CommRing R] (f : PowerSeries R) :

(PowerSeries.derivative R) (-f) = -(PowerSeries.derivative R) f

Derivative of negation: (-f)' = -f'.

source

@[simp]

theorem AlgebraicCombinatorics.FPS.derivative_sub {R : Type u_2} [CommRing R] (f g : PowerSeries R) :

(PowerSeries.derivative R) (f - g) = (PowerSeries.derivative R) f - (PowerSeries.derivative R) g

Derivative of subtraction: (f - g)' = f' - g'.

Part (b): Summable Families #

If (fᵢ)_{i ∈ I} is a summable family of FPSs, then (∑ fᵢ)' = ∑ fᵢ'.

We first state it for finite sums (which follows from additivity), then for infinite summable families (where summability means that for each coefficient index, only finitely many family members have nonzero coefficient).

source

theorem AlgebraicCombinatorics.FPS.derivative_sum {R : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → PowerSeries R) :

(PowerSeries.derivative R) (∑ i ∈ s, f i) = ∑ i ∈ s, (PowerSeries.derivative R) (f i)

Theorem thm.fps.deriv.rules (b) (finite version): Derivative commutes with finite sums.

source

theorem AlgebraicCombinatorics.FPS.summableFPS_derivative {R' : Type u_2} [CommRing R'] {ι : Type u_3} (f : ι → PowerSeries R') (hf : SummableFPS f) :

SummableFPS fun (i : ι) => (PowerSeries.derivative R') (f i)

If (fᵢ) is a summable family, then (fᵢ') is also summable.

source

theorem AlgebraicCombinatorics.FPS.derivative_summableFPSSum {R' : Type u_2} [CommRing R'] {ι : Type u_3} (f : ι → PowerSeries R') (hf : SummableFPS f) :

(PowerSeries.derivative R') (summableFPSSum f hf) = summableFPSSum (fun (i : ι) => (PowerSeries.derivative R') (f i)) ⋯

Theorem thm.fps.deriv.rules (b) (infinite version): Derivative commutes with infinite summable sums.

If (fᵢ){i ∈ I} is a summable family of FPSs, then (fᵢ'){i ∈ I} is summable and (∑ fᵢ)' = ∑ fᵢ'.

Part (c): Scalar Multiplication #

(c · f)' = c · f'

This is automatic since derivative is an R-linear map.

source

theorem AlgebraicCombinatorics.FPS.derivative_smul {R : Type u_1} [CommSemiring R] (c : R) (f : PowerSeries R) :

(PowerSeries.derivative R) (c • f) = c • (PowerSeries.derivative R) f

Theorem thm.fps.deriv.rules (c): Derivative commutes with scalar multiplication.

source

theorem AlgebraicCombinatorics.FPS.derivative_C_mul {R : Type u_1} [CommSemiring R] (c : R) (f : PowerSeries R) :

(PowerSeries.derivative R) (PowerSeries.C c * f) = PowerSeries.C c * (PowerSeries.derivative R) f

Variant with C c * f instead of c • f.

Part (d): Leibniz Rule (Product Rule) #

(f · g)' = f' · g + f · g'

This is the defining property of a derivation.

source

theorem AlgebraicCombinatorics.FPS.derivative_mul {R : Type u_1} [CommSemiring R] (f g : PowerSeries R) :

(PowerSeries.derivative R) (f * g) = (PowerSeries.derivative R) f * g + f * (PowerSeries.derivative R) g

Theorem thm.fps.deriv.rules (d): Leibniz rule for power series.

Part (e): Quotient Rule #

(f / g)' = (f' · g - f · g') / g² for invertible g.

In Mathlib, this is expressed using PowerSeries.derivative_inv' for fields, or PowerSeries.derivative_inv for units.

source

theorem AlgebraicCombinatorics.FPS.derivative_div {K : Type u_3} [Field K] (f g : PowerSeries K) (hg : PowerSeries.constantCoeff g ≠ 0) :

(PowerSeries.derivative K) (f * g⁻¹) = ((PowerSeries.derivative K) f * g - f * (PowerSeries.derivative K) g) * g⁻¹ ^ 2

Theorem thm.fps.deriv.rules (e): Quotient rule for power series.

Note: In Mathlib, this is stated as (f⁻¹)' = -f⁻¹² · f'. The full quotient rule follows from combining this with Leibniz.

Part (f): Power Rule #

(g^n)' = n · g^(n-1) · g'

This is PowerSeries.derivative_pow in Mathlib.

source

theorem AlgebraicCombinatorics.FPS.derivative_pow' {A : Type u_4} [CommRing A] (g : PowerSeries A) (n : ℕ) :

(PowerSeries.derivative A) (g ^ n) = ↑n * g ^ (n - 1) * (PowerSeries.derivative A) g

Theorem thm.fps.deriv.rules (f): Power rule for power series.

Part (g): Chain Rule #

(f ∘ g)' = (f' ∘ g) · g' when composition is defined.

In Mathlib, composition is PowerSeries.subst, and this is PowerSeries.derivative_subst. The condition for substitution is that g has nilpotent constant term (which includes the case when [x⁰]g = 0).

source

theorem AlgebraicCombinatorics.FPS.derivative_comp {A : Type u_4} [CommRing A] (f g : PowerSeries A) (hg : PowerSeries.HasSubst g) :

(PowerSeries.derivative A) (PowerSeries.subst g f) = PowerSeries.subst g ((PowerSeries.derivative A) f) * (PowerSeries.derivative A) g

Theorem thm.fps.deriv.rules (g): Chain rule for power series.

This holds when g has nilpotent constant coefficient (in particular when [x⁰]g = 0).

Part (h): Uniqueness of Antiderivatives #

If f' = g' and K is a ℚ-algebra, then f - g is constant.

In Mathlib, this is PowerSeries.derivative.ext (with the converse direction: if derivatives and constant terms match, then the series are equal).

source

theorem AlgebraicCombinatorics.FPS.derivative_eq_imp_diff_const {R : Type u_5} [CommRing R] [IsAddTorsionFree R] {f g : PowerSeries R} (h : (PowerSeries.derivative R) f = (PowerSeries.derivative R) g) (n : ℕ) :

n ≠ 0 → (PowerSeries.coeff n) (f - g) = 0

Theorem thm.fps.deriv.rules (h): Two power series with equal derivatives differ by a constant.

Note: Mathlib states this as: if f' = g' and f₀ = g₀, then f = g. We state the equivalent: if f' = g', then f - g has zero derivative, hence is constant (all higher coefficients are zero).

source

theorem AlgebraicCombinatorics.FPS.eq_of_derivative_eq_of_constantCoeff_eq {R : Type u_5} [CommRing R] [IsAddTorsionFree R] {f g : PowerSeries R} (hD : (PowerSeries.derivative R) f = (PowerSeries.derivative R) g) (hc : PowerSeries.constantCoeff f = PowerSeries.constantCoeff g) :

f = g

Equivalent formulation: if two power series have equal derivatives and equal constant terms, they are equal. This is PowerSeries.derivative.ext in Mathlib.