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

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

• 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) : (taylor r) f = f.comp (X + C r)

@[simp]

theorem Polynomial.taylor_X {R : Type u_1} [Semiring R] (r : R) : (taylor r) X = X + C r

@[simp]

theorem Polynomial.taylor_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) : (taylor r) (X ^ n) = (X + C r) ^ n

@[simp]

theorem Polynomial.taylor_C {R : Type u_1} [Semiring R] (r x : R) : (taylor r) (C x) = C x

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

@[simp]

theorem Polynomial.taylor_zero' {R : Type u_1} [Semiring R] : taylor 0 = LinearMap.id

@[simp]

theorem Polynomial.taylor_one {R : Type u_1} [Semiring R] (r : R) : (taylor r) 1 = C 1

@[simp]

theorem Polynomial.taylor_monomial {R : Type u_1} [Semiring R] (r : R) (i : ℕ) (k : R) : (taylor r) ((monomial i) k) = C k * (X + C r) ^ i

theorem Polynomial.taylor_coeff {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) (n : ℕ) : ((taylor r) f).coeff n = eval r ((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) : ((taylor r) f).coeff 0 = eval r f

@[simp]

theorem Polynomial.taylor_coeff_one {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((taylor r) f).coeff 1 = eval r (derivative f)

@[simp]

theorem Polynomial.coeff_taylor_natDegree {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((taylor r) f).coeff f.natDegree = f.leadingCoeff

@[simp]

theorem Polynomial.natDegree_taylor {R : Type u_1} [Semiring R] (p : Polynomial R) (r : R) : ((taylor r) p).natDegree = p.natDegree

@[simp]

theorem Polynomial.leadingCoeff_taylor {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((taylor r) f).leadingCoeff = f.leadingCoeff

@[simp]

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

@[simp]

theorem Polynomial.degree_taylor {R : Type u_1} [Semiring R] (p : Polynomial R) (r : R) : ((taylor r) p).degree = p.degree

theorem Polynomial.eq_zero_of_hasseDeriv_eq_zero {R : Type u_1} [Semiring R] (f : Polynomial R) (r : R) (h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0) : f = 0

@[simp]

theorem Polynomial.map_taylor {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (p : Polynomial R) (r : R) (f : R →+* S) : map f ((taylor r) p) = (taylor (f r)) (map f p)

theorem Polynomial.taylor_injective {R : Type u_1} [Ring R] (r : R) : Function.Injective ⇑(taylor r)

@[simp]

theorem Polynomial.taylor_inj {R : Type u_1} [Ring R] {r : R} {p q : Polynomial R} : (taylor r) p = (taylor r) q ↔ p = q

@[simp]

theorem Polynomial.taylor_mul {R : Type u_1} [CommSemiring R] (r : R) (p q : Polynomial R) : (taylor r) (p * q) = (taylor r) p * (taylor r) q

noncomputable def Polynomial.taylorAlgHom {R : Type u_1} [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) ⋯ ⋯

@[simp]

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

@[simp]

theorem Polynomial.taylor_pow {R : Type u_1} [CommSemiring R] (r : R) (f : Polynomial R) (n : ℕ) : (taylor r) (f ^ n) = (taylor r) f ^ n

@[simp]

theorem Polynomial.coe_taylorAlgHom {R : Type u_1} [CommSemiring R] (r : R) : ↑(taylorAlgHom r) = taylor r

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

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

theorem Polynomial.exists_mul_sq_add_linear_part_eq_eval_add {R : Type u_1} [CommSemiring R] (p : Polynomial R) (x y : R) : ∃ (c : R), c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p

theorem Polynomial.eval_add_of_sq_eq_zero {R : Type u_1} [CommSemiring R] (p : Polynomial R) (x y : R) (hy : y ^ 2 = 0) : eval (x + y) p = eval x p + eval x (derivative p) * y

theorem Polynomial.aeval_add_of_sq_eq_zero {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommRing S] [Algebra R S] (p : Polynomial R) (x y : S) (hy : y ^ 2 = 0) : (aeval (x + y)) p = (aeval x) p + (aeval x) (derivative p) * y

noncomputable def Polynomial.taylorEquiv {R : Type u_1} [CommRing R] (r : R) : Polynomial R ≃ₐ[R] Polynomial R

Polynomial.taylor as an AlgEquiv for commutative rings.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.toAlgHom_taylorEquiv {R : Type u_1} [CommRing R] (r : R) : ↑(taylorEquiv r) = taylorAlgHom r

@[simp]

theorem Polynomial.coe_taylorEquiv {R : Type u_1} [CommRing R] (r : R) : ↑↑(taylorEquiv r) = taylor r

@[simp]

theorem Polynomial.taylorEquiv_symm {R : Type u_1} [CommRing R] (r : R) : (taylorEquiv r).symm = taylorEquiv (-r)

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

theorem Polynomial.sum_taylor_eq {R : Type u_1} [CommRing R] (f : Polynomial R) (r : R) : (((taylor r) f).sum fun (i : ℕ) (a : R) => C a * (X - C r) ^ i) = f

Taylor's formula.