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
Mathlib/Analysis/Calculus/Deriv/Basic.lean.
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 : 𝕜) => eval x p) (eval x (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 : 𝕜) => (aeval x) q) ((aeval x) (derivative q)) x
theorem Polynomial.hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => eval x p) (eval x (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 : 𝕜) => (aeval x) q) ((aeval x) (derivative q)) x
theorem Polynomial.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => eval x p) (eval x (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 : 𝕜) => (aeval x) q) ((aeval x) (derivative q)) s x
theorem Polynomial.differentiableAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => 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 : 𝕜) => (aeval x) q) x
theorem Polynomial.differentiableWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => 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 : 𝕜) => (aeval x) q) s x
theorem Polynomial.differentiable {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) :
Differentiable 𝕜 fun (x : 𝕜) => eval x p
theorem Polynomial.differentiable_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) :
Differentiable 𝕜 fun (x : 𝕜) => (aeval x) q
theorem Polynomial.differentiableOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => 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 : 𝕜) => (aeval x) q) s
@[simp]
@[simp]
theorem Polynomial.deriv_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) :
theorem Polynomial.derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) :
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) :
theorem Polynomial.hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) :
HasFDerivAt (fun (x : 𝕜) => eval x p) (ContinuousLinearMap.smulRight 1 (eval x (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 : 𝕜) => (aeval x) q) (ContinuousLinearMap.smulRight 1 ((aeval x) (derivative q))) x
theorem Polynomial.hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜) (x : 𝕜) :
HasFDerivWithinAt (fun (x : 𝕜) => eval x p) (ContinuousLinearMap.smulRight 1 (eval x (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 : 𝕜) => (aeval x) q) (ContinuousLinearMap.smulRight 1 ((aeval x) (derivative q))) s x
@[simp]
@[simp]
theorem Polynomial.fderiv_aeval {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {R : Type u_1} [CommSemiring R] [Algebra R 𝕜] (q : Polynomial R) :
fderiv 𝕜 (fun (x : 𝕜) => (aeval x) q) x = ContinuousLinearMap.smulRight 1 ((aeval x) (derivative q))
theorem Polynomial.fderivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun (x : 𝕜) => eval x p) s x = ContinuousLinearMap.smulRight 1 (eval x (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 : 𝕜) => (aeval x) q) s x = ContinuousLinearMap.smulRight 1 ((aeval x) (derivative q))