Documentation

Mathlib.Algebra.Polynomial.Taylor

Taylor expansions of polynomials #

Main declarations #

The Taylor expansion of a polynomial f at r.

Equations
Instances For
    theorem Polynomial.taylor_apply {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) :
    (Polynomial.taylor r) f = f.comp (Polynomial.X + Polynomial.C r)
    @[simp]
    theorem Polynomial.taylor_X {R : Type u_1} [Semiring R] (r : R) :
    (Polynomial.taylor r) Polynomial.X = Polynomial.X + Polynomial.C r
    @[simp]
    theorem Polynomial.taylor_C {R : Type u_1} [Semiring R] (r : R) (x : R) :
    (Polynomial.taylor r) (Polynomial.C x) = Polynomial.C x
    @[simp]
    theorem Polynomial.taylor_zero' {R : Type u_1} [Semiring R] :
    Polynomial.taylor 0 = LinearMap.id
    @[simp]
    theorem Polynomial.taylor_one {R : Type u_1} [Semiring R] (r : R) :
    (Polynomial.taylor r) 1 = Polynomial.C 1
    @[simp]
    theorem Polynomial.taylor_monomial {R : Type u_1} [Semiring R] (r : R) (i : ) (k : R) :
    (Polynomial.taylor r) ((Polynomial.monomial i) k) = Polynomial.C k * (Polynomial.X + Polynomial.C r) ^ i
    theorem Polynomial.taylor_coeff {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) (n : ) :

    The kth coefficient of Polynomial.taylor r f is (Polynomial.hasseDeriv k f).eval r.

    @[simp]
    theorem Polynomial.taylor_coeff_zero {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) :
    ((Polynomial.taylor r) f).coeff 0 = Polynomial.eval r f
    @[simp]
    theorem Polynomial.taylor_coeff_one {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) :
    ((Polynomial.taylor r) f).coeff 1 = Polynomial.eval r (Polynomial.derivative f)
    @[simp]
    theorem Polynomial.natDegree_taylor {R : Type u_1} [Semiring R] (p : Polynomial R) (r : R) :
    ((Polynomial.taylor r) p).natDegree = p.natDegree
    @[simp]
    theorem Polynomial.taylor_mul {R : Type u_2} [CommSemiring R] (r : R) (p : Polynomial R) (q : Polynomial R) :

    Polynomial.taylor as an AlgHom for commutative semirings

    Equations
    Instances For
      theorem Polynomial.taylor_taylor {R : Type u_2} [CommSemiring R] (f : Polynomial R) (r : R) (s : R) :
      theorem Polynomial.taylor_eval {R : Type u_2} [CommSemiring R] (r : R) (f : Polynomial R) (s : R) :
      theorem Polynomial.taylor_eval_sub {R : Type u_2} [CommRing R] (r : R) (f : Polynomial R) (s : R) :
      theorem Polynomial.eq_zero_of_hasseDeriv_eq_zero {R : Type u_2} [CommRing R] (f : Polynomial R) (r : R) (h : ∀ (k : ), Polynomial.eval r ((Polynomial.hasseDeriv k) f) = 0) :
      f = 0
      theorem Polynomial.sum_taylor_eq {R : Type u_2} [CommRing R] (f : Polynomial R) (r : R) :
      (((Polynomial.taylor r) f).sum fun (i : ) (a : R) => Polynomial.C a * (Polynomial.X - Polynomial.C r) ^ i) = f

      Taylor's formula.

      theorem Polynomial.eval_add_of_sq_eq_zero {A : Type u_2} [CommSemiring A] (p : Polynomial A) (x : A) (y : A) (hy : y ^ 2 = 0) :
      Polynomial.eval (x + y) p = Polynomial.eval x p + Polynomial.eval x (Polynomial.derivative p) * y