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} [Semiring R] (r : R) : Polynomial R →ₗ[R] Polynomial R

The Taylor expansion of a polynomial f at r.

Equations

• Polynomial.taylor r = { toFun := fun (f : Polynomial R) => f.comp (Polynomial.X + Polynomial.C r), map_add' := ⋯, map_smul' := ⋯ }

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

theorem Polynomial.taylor_zero {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.taylor 0) f = f

@[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 : ℕ) : ((Polynomial.taylor r) f).coeff n = Polynomial.eval r ((Polynomial.hasseDeriv n) 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} [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 r) (p * q) = (Polynomial.taylor r) p * (Polynomial.taylor r) q

@[simp]

theorem Polynomial.taylorAlgHom_apply {R : Type u_2} [CommSemiring R] (r : R) (a : Polynomial R) : (Polynomial.taylorAlgHom r) a = (Polynomial.taylor r) a

def Polynomial.taylorAlgHom {R : Type u_2} [CommSemiring R] (r : R) : Polynomial R →ₐ[R] Polynomial R

Polynomial.taylor as an AlgHom for commutative semirings

Equations

• Polynomial.taylorAlgHom r = AlgHom.ofLinearMap (Polynomial.taylor r) ⋯ ⋯

theorem Polynomial.taylor_taylor {R : Type u_2} [CommSemiring R] (f : Polynomial R) (r : R) (s : R) : (Polynomial.taylor r) ((Polynomial.taylor s) f) = (Polynomial.taylor (r + s)) f

theorem Polynomial.taylor_eval {R : Type u_2} [CommSemiring R] (r : R) (f : Polynomial R) (s : R) : Polynomial.eval s ((Polynomial.taylor r) f) = Polynomial.eval (s + r) f

theorem Polynomial.taylor_eval_sub {R : Type u_2} [CommRing R] (r : R) (f : Polynomial R) (s : R) : Polynomial.eval (s - r) ((Polynomial.taylor r) f) = Polynomial.eval s f

theorem Polynomial.taylor_injective {R : Type u_2} [CommRing R] (r : R) : Function.Injective ⇑(Polynomial.taylor 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.