Documentation

Mathlib.RingTheory.PowerSeries.Derivative

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 #

noncomputable def PowerSeries.derivativeFun {R : Type u_1} [CommSemiring R] (f : 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
Instances For
    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 : PowerSeries R) (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 : PowerSeries R) (g : PowerSeries R) :
    (f * g).derivativeFun = f g.derivativeFun + g f.derivativeFun

    Leibniz rule for formal power series.

    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] :

    The formal derivative of a formal power series

    Equations
    • PowerSeries.derivative R = { toFun := PowerSeries.derivativeFun, map_add' := , map_smul' := , map_one_eq_zero' := , leibniz' := }
    Instances For

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

      Equations
      Instances For
        @[simp]
        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)

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