Definitions

In this file we define an operation derivative (formal differentiation) on the ring of formal power series in one variable (over an arbitrary commutative semiring).

Under suitable assumptions, we prove that two power series are equal if their derivatives are equal and their constant terms are equal. This will give us a simple tool for proving power series identities. For example, one can easily prove the power series identity $\exp ( \log (1+X)) = 1+X$ by differentiating twice.

Main Definition

• PowerSeries.derivative R : Derivation R R⟦X⟧ R⟦X⟧ the formal derivative operation. This is abbreviated d⁄dX R.

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.mk fun (n : ℕ) => (PowerSeries.coeff R (n + 1)) f * (↑n + 1)

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

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

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

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

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

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

Leibniz rule for formal power series.

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

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

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 = { toFun := PowerSeries.derivativeFun, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

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) : (PowerSeries.derivative R) ((PowerSeries.C R) r) = 0

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

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

@[simp]

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

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

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

theorem PowerSeries.derivative.ext {R : Type u_1} [CommRing R] [NoZeroSMulDivisors ℕ R] {f g : PowerSeries R} (hD : (PowerSeries.derivative R) f = (PowerSeries.derivative R) g) (hc : (PowerSeries.constantCoeff R) f = (PowerSeries.constantCoeff R) 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)ˣ) : (PowerSeries.derivative R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (PowerSeries.derivative R) ↑f

@[simp]

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

@[simp]

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