mathlib documentation

data.polynomial.taylor

Taylor expansions of polynomials #

Main declarations #

noncomputable def polynomial.taylor {R : Type u_1} [semiring R] (r : R) :

The Taylor expansion of a polynomial f at r.

Equations
theorem polynomial.taylor_apply {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
@[simp]
theorem polynomial.taylor_C {R : Type u_1} [semiring R] (r x : R) :
@[simp]
theorem polynomial.taylor_zero {R : Type u_1} [semiring R] (f : polynomial R) :
@[simp]
theorem polynomial.taylor_one {R : Type u_1} [semiring R] (r : R) :
@[simp]
theorem polynomial.taylor_monomial {R : Type u_1} [semiring R] (r : R) (i : ) (k : R) :
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.hasse_deriv k f).eval r.

@[simp]
theorem polynomial.taylor_coeff_zero {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
@[simp]
@[simp]
theorem polynomial.nat_degree_taylor {R : Type u_1} [semiring R] (p : polynomial R) (r : R) :
@[simp]
theorem polynomial.taylor_mul {R : Type u_1} [comm_semiring R] (r : R) (p q : polynomial R) :
theorem polynomial.taylor_taylor {R : Type u_1} [comm_semiring R] (f : polynomial R) (r s : R) :
theorem polynomial.taylor_eval {R : Type u_1} [comm_semiring R] (r : R) (f : polynomial R) (s : R) :
theorem polynomial.taylor_eval_sub {R : Type u_1} [comm_ring R] (r : R) (f : polynomial R) (s : R) :
theorem polynomial.eq_zero_of_hasse_deriv_eq_zero {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) (h : ∀ (k : ), polynomial.eval r ((polynomial.hasse_deriv k) f) = 0) :
f = 0
theorem polynomial.sum_taylor_eq {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) :
((polynomial.taylor r) f).sum (λ (i : ) (a : R), (polynomial.C a) * (polynomial.X - polynomial.C r) ^ i) = f

Taylor's formula.