# Derivatives of polynomials #

In this file we prove that derivatives of polynomials in the analysis sense agree with their derivatives in the algebraic sense.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

## TODO #

• Generalize some (most?) results to an algebra over the base field.

## Keywords #

derivative, polynomial

### Derivative of a polynomial #

theorem Polynomial.hasStrictDerivAt {𝕜 : Type u} (p : ) (x : 𝕜) :
HasStrictDerivAt (fun (x : 𝕜) => ) (Polynomial.eval x (Polynomial.derivative p)) x

The derivative (in the analysis sense) of a polynomial p is given by p.derivative.

theorem Polynomial.hasStrictDerivAt_aeval {𝕜 : Type u} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (x : 𝕜) :
HasStrictDerivAt (fun (x : 𝕜) => () q) (() (Polynomial.derivative q)) x
theorem Polynomial.hasDerivAt {𝕜 : Type u} (p : ) (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => ) (Polynomial.eval x (Polynomial.derivative p)) x

The derivative (in the analysis sense) of a polynomial p is given by p.derivative.

theorem Polynomial.hasDerivAt_aeval {𝕜 : Type u} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => () q) (() (Polynomial.derivative q)) x
theorem Polynomial.hasDerivWithinAt {𝕜 : Type u} (p : ) (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => ) (Polynomial.eval x (Polynomial.derivative p)) s x
theorem Polynomial.hasDerivWithinAt_aeval {𝕜 : Type u} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => () q) (() (Polynomial.derivative q)) s x
theorem Polynomial.differentiableAt {𝕜 : Type u} {x : 𝕜} (p : ) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => ) x
theorem Polynomial.differentiableAt_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => () q) x
theorem Polynomial.differentiableWithinAt {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (p : ) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => ) s x
theorem Polynomial.differentiableWithinAt_aeval {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => () q) s x
theorem Polynomial.differentiable {𝕜 : Type u} (p : ) :
Differentiable 𝕜 fun (x : 𝕜) =>
theorem Polynomial.differentiable_aeval {𝕜 : Type u} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
Differentiable 𝕜 fun (x : 𝕜) => () q
theorem Polynomial.differentiableOn {𝕜 : Type u} {s : Set 𝕜} (p : ) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => ) s
theorem Polynomial.differentiableOn_aeval {𝕜 : Type u} {s : Set 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => () q) s
@[simp]
theorem Polynomial.deriv {𝕜 : Type u} {x : 𝕜} (p : ) :
deriv (fun (x : 𝕜) => ) x = Polynomial.eval x (Polynomial.derivative p)
@[simp]
theorem Polynomial.deriv_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
deriv (fun (x : 𝕜) => () q) x = () (Polynomial.derivative q)
theorem Polynomial.derivWithin {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (p : ) (hxs : ) :
derivWithin (fun (x : 𝕜) => ) s x = Polynomial.eval x (Polynomial.derivative p)
theorem Polynomial.derivWithin_aeval {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (hxs : ) :
derivWithin (fun (x : 𝕜) => () q) s x = () (Polynomial.derivative q)
theorem Polynomial.hasFDerivAt {𝕜 : Type u} (p : ) (x : 𝕜) :
HasFDerivAt (fun (x : 𝕜) => ) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) x
theorem Polynomial.hasFDerivAt_aeval {𝕜 : Type u} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (x : 𝕜) :
HasFDerivAt (fun (x : 𝕜) => () q) (ContinuousLinearMap.smulRight 1 (() (Polynomial.derivative q))) x
theorem Polynomial.hasFDerivWithinAt {𝕜 : Type u} {s : Set 𝕜} (p : ) (x : 𝕜) :
HasFDerivWithinAt (fun (x : 𝕜) => ) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) s x
theorem Polynomial.hasFDerivWithinAt_aeval {𝕜 : Type u} {s : Set 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (x : 𝕜) :
HasFDerivWithinAt (fun (x : 𝕜) => () q) (ContinuousLinearMap.smulRight 1 (() (Polynomial.derivative q))) s x
@[simp]
theorem Polynomial.fderiv {𝕜 : Type u} {x : 𝕜} (p : ) :
fderiv 𝕜 (fun (x : 𝕜) => ) x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
@[simp]
theorem Polynomial.fderiv_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) :
fderiv 𝕜 (fun (x : 𝕜) => () q) x = ContinuousLinearMap.smulRight 1 (() (Polynomial.derivative q))
theorem Polynomial.fderivWithin {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (p : ) (hxs : ) :
fderivWithin 𝕜 (fun (x : 𝕜) => ) s x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
theorem Polynomial.fderivWithin_aeval {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [] [Algebra R 𝕜] (q : ) (hxs : ) :
fderivWithin 𝕜 (fun (x : 𝕜) => () q) s x = ContinuousLinearMap.smulRight 1 (() (Polynomial.derivative q))