Taylor expansions of polynomials #
Main declarations #
Polynomial.taylor
: the Taylor expansion of the polynomialf
atr
Polynomial.taylor_coeff
: thek
th coefficient oftaylor 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
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' := ⋯ }
Instances For
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]
(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 k
th 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
Instances For
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.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
Taylor's formula.
theorem
Polynomial.eval_add_of_sq_eq_zero
{A : Type u_2}
[CommSemiring A]
(p : Polynomial A)
(x : A)
(y : A)
(hy : y ^ 2 = 0)
:
Polynomial.eval (x + y) p = Polynomial.eval x p + Polynomial.eval x (Polynomial.derivative p) * y