# Documentation

Mathlib.Data.Polynomial.Taylor

# Taylor expansions of polynomials #

## Main declarations #

• Polynomial.taylor: the Taylor expansion of the polynomial f at r
• Polynomial.taylor_coeff: the kth coefficient of taylor r f is (Polynomial.hasseDeriv k f).eval r
• Polynomial.eq_zero_of_hasseDeriv_eq_zero: the identity principle: a polynomial is 0 iff all its Hasse derivatives are zero
def Polynomial.taylor {R : Type u_1} [] (r : R) :

The Taylor expansion of a polynomial f at r.

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

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} [] (r : R) (f : ) :
Polynomial.coeff (↑() f) 0 =
@[simp]
theorem Polynomial.taylor_coeff_one {R : Type u_1} [] (r : R) (f : ) :
Polynomial.coeff (↑() f) 1 = Polynomial.eval r (Polynomial.derivative f)
@[simp]
theorem Polynomial.natDegree_taylor {R : Type u_1} [] (p : ) (r : R) :
@[simp]
theorem Polynomial.taylor_mul {R : Type u_2} [] (r : R) (p : ) (q : ) :
↑() (p * q) = ↑() p * ↑() q
@[simp]
theorem Polynomial.taylorAlgHom_apply {R : Type u_2} [] (r : R) (a : ) :
↑() a = ↑() a
def Polynomial.taylorAlgHom {R : Type u_2} [] (r : R) :

Polynomial.taylor as an AlgHom for commutative semirings

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

Taylor's formula.