# 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.

Equations
• = { toFun := fun (f : ) => f.comp (Polynomial.X + Polynomial.C r), map_add' := , map_smul' := }
Instances For
theorem Polynomial.taylor_apply {R : Type u_1} [] (r : R) (f : ) :
f = f.comp (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 : ) :
( f).coeff n = Polynomial.eval r ()

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

Polynomial.taylor as an AlgHom for commutative semirings

Equations
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) :
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 () = 0) :
f = 0
theorem Polynomial.sum_taylor_eq {R : Type u_2} [] (f : ) (r : R) :
(( f).sum fun (i : ) (a : R) => Polynomial.C a * (Polynomial.X - Polynomial.C r) ^ i) = f

Taylor's formula.