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

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

Keywords

derivative, polynomial

Derivative of a polynomial

theorem Polynomial.hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) : HasStrictDerivAt (fun (x : 𝕜) => Polynomial.eval x p) (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} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (x : 𝕜) : HasStrictDerivAt (fun (x : 𝕜) => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x

theorem Polynomial.hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) : HasDerivAt (fun (x : 𝕜) => Polynomial.eval x p) (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} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (x : 𝕜) : HasDerivAt (fun (x : 𝕜) => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x

theorem Polynomial.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) (s : Set 𝕜) : HasDerivWithinAt (fun (x : 𝕜) => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) s x

theorem Polynomial.hasDerivWithinAt_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (x : 𝕜) (s : Set 𝕜) : HasDerivWithinAt (fun (x : 𝕜) => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) s x

theorem Polynomial.differentiableAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜) : DifferentiableAt 𝕜 (fun (x : 𝕜) => Polynomial.eval x p) x

theorem Polynomial.differentiableAt_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : DifferentiableAt 𝕜 (fun (x : 𝕜) => (Polynomial.aeval x) q) x

theorem Polynomial.differentiableWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) : DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => Polynomial.eval x p) s x

theorem Polynomial.differentiableWithinAt_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => (Polynomial.aeval x) q) s x

theorem Polynomial.differentiable {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) : Differentiable 𝕜 fun (x : 𝕜) => Polynomial.eval x p

theorem Polynomial.differentiable_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : Differentiable 𝕜 fun (x : 𝕜) => (Polynomial.aeval x) q

theorem Polynomial.differentiableOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜) : DifferentiableOn 𝕜 (fun (x : 𝕜) => Polynomial.eval x p) s

theorem Polynomial.differentiableOn_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : DifferentiableOn 𝕜 (fun (x : 𝕜) => (Polynomial.aeval x) q) s

@[simp]

theorem Polynomial.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜) : deriv (fun (x : 𝕜) => Polynomial.eval x p) x = Polynomial.eval x (Polynomial.derivative p)

@[simp]

theorem Polynomial.deriv_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : deriv (fun (x : 𝕜) => (Polynomial.aeval x) q) x = (Polynomial.aeval x) (Polynomial.derivative q)

theorem Polynomial.derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (fun (x : 𝕜) => Polynomial.eval x p) s x = Polynomial.eval x (Polynomial.derivative p)

theorem Polynomial.derivWithin_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin (fun (x : 𝕜) => (Polynomial.aeval x) q) s x = (Polynomial.aeval x) (Polynomial.derivative q)

theorem Polynomial.hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) : HasFDerivAt (fun (x : 𝕜) => Polynomial.eval x p) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) x

theorem Polynomial.hasFDerivAt_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (x : 𝕜) : HasFDerivAt (fun (x : 𝕜) => (Polynomial.aeval x) q) (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) x

theorem Polynomial.hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜) (x : 𝕜) : HasFDerivWithinAt (fun (x : 𝕜) => Polynomial.eval x p) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) s x

theorem Polynomial.hasFDerivWithinAt_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (x : 𝕜) : HasFDerivWithinAt (fun (x : 𝕜) => (Polynomial.aeval x) q) (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) s x

@[simp]

theorem Polynomial.fderiv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜) : fderiv 𝕜 (fun (x : 𝕜) => Polynomial.eval x p) x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))

@[simp]

theorem Polynomial.fderiv_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) : fderiv 𝕜 (fun (x : 𝕜) => (Polynomial.aeval x) q) x = ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))

theorem Polynomial.fderivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (x : 𝕜) => Polynomial.eval x p) s x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))

theorem Polynomial.fderivWithin_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (x : 𝕜) => (Polynomial.aeval x) q) s x = ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))