mathlib3 documentation

data.polynomial.taylor

Taylor expansions of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

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

The Taylor expansion of a polynomial f at r.

Equations
source
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)
source
@[simp]
theorem polynomial.taylor_X {R : Type u_1} [semiring R] (r : R) :
⇑(polynomial.taylor r) polynomial.X = polynomial.X + ⇑polynomial.C r
source
@[simp]
theorem polynomial.taylor_C {R : Type u_1} [semiring R] (r x : R) :
⇑(polynomial.taylor r) (⇑polynomial.C x) = ⇑polynomial.C x
source
@[simp]
theorem polynomial.taylor_zero' {R : Type u_1} [semiring R] :
polynomial.taylor 0 = linear_map.id
source
theorem polynomial.taylor_zero {R : Type u_1} [semiring R] (f : polynomial R) :
⇑(polynomial.taylor 0) f = f
source
@[simp]
theorem polynomial.taylor_one {R : Type u_1} [semiring R] (r : R) :
⇑(polynomial.taylor r) 1 = ⇑polynomial.C 1
source
@[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
source
theorem polynomial.taylor_coeff {R : Type u_1} [semiring R] (r : R) (f : polynomial R) (n : ℕ) :
(⇑(polynomial.taylor r) f).coeff n = polynomial.eval r (⇑(polynomial.hasse_deriv n) f)

The kth coefficient of polynomial.taylor r f is (polynomial.hasse_deriv k f).eval r.

source
@[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
source
@[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)
source
@[simp]
theorem polynomial.nat_degree_taylor {R : Type u_1} [semiring R] (p : polynomial R) (r : R) :
(⇑(polynomial.taylor r) p).nat_degree = p.nat_degree
source
@[simp]
theorem polynomial.taylor_mul {R : Type u_1} [comm_semiring R] (r : R) (p q : polynomial R) :
⇑(polynomial.taylor r) (p * q) = ⇑(polynomial.taylor r) p * ⇑(polynomial.taylor r) q
source
noncomputable def polynomial.taylor_alg_hom {R : Type u_1} [comm_semiring R] (r : R) :
polynomial R →ₐ[R] polynomial R

polynomial.taylor as a alg_hom for commutative semirings

Equations
source
@[simp]
theorem polynomial.taylor_alg_hom_apply {R : Type u_1} [comm_semiring R] (r : R) (ᾰ : polynomial R) :
⇑(polynomial.taylor_alg_hom r) ᾰ = ⇑(polynomial.taylor r) ᾰ
source
theorem polynomial.taylor_taylor {R : Type u_1} [comm_semiring R] (f : polynomial R) (r s : R) :
⇑(polynomial.taylor r) (⇑(polynomial.taylor s) f) = ⇑(polynomial.taylor (r + s)) f
source
theorem polynomial.taylor_eval {R : Type u_1} [comm_semiring R] (r : R) (f : polynomial R) (s : R) :
polynomial.eval s (⇑(polynomial.taylor r) f) = polynomial.eval (s + r) f
source
theorem polynomial.taylor_eval_sub {R : Type u_1} [comm_ring R] (r : R) (f : polynomial R) (s : R) :
polynomial.eval (s - r) (⇑(polynomial.taylor r) f) = polynomial.eval s f
source
theorem polynomial.taylor_injective {R : Type u_1} [comm_ring R] (r : R) :
function.injective ⇑(polynomial.taylor r)
source
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
source
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.