Derivatives of polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
@[protected]
theorem
polynomial.has_strict_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(p : polynomial 𝕜)
(x : 𝕜) :
has_strict_deriv_at (λ (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.
@[protected]
theorem
polynomial.has_strict_deriv_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(x : 𝕜) :
has_strict_deriv_at (λ (x : 𝕜), ⇑(polynomial.aeval x) q) (⇑(polynomial.aeval x) (⇑polynomial.derivative q)) x
@[protected]
theorem
polynomial.has_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(p : polynomial 𝕜)
(x : 𝕜) :
has_deriv_at (λ (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.
@[protected]
theorem
polynomial.has_deriv_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(x : 𝕜) :
has_deriv_at (λ (x : 𝕜), ⇑(polynomial.aeval x) q) (⇑(polynomial.aeval x) (⇑polynomial.derivative q)) x
@[protected]
theorem
polynomial.has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(p : polynomial 𝕜)
(x : 𝕜)
(s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), polynomial.eval x p) (polynomial.eval x (⇑polynomial.derivative p)) s x
@[protected]
theorem
polynomial.has_deriv_within_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(x : 𝕜)
(s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), ⇑(polynomial.aeval x) q) (⇑(polynomial.aeval x) (⇑polynomial.derivative q)) s x
@[protected]
theorem
polynomial.differentiable_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(p : polynomial 𝕜) :
differentiable_at 𝕜 (λ (x : 𝕜), polynomial.eval x p) x
@[protected]
theorem
polynomial.differentiable_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
differentiable_at 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q) x
@[protected]
theorem
polynomial.differentiable_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(p : polynomial 𝕜) :
differentiable_within_at 𝕜 (λ (x : 𝕜), polynomial.eval x p) s x
@[protected]
theorem
polynomial.differentiable_within_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
differentiable_within_at 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q) s x
@[protected]
theorem
polynomial.differentiable
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(p : polynomial 𝕜) :
differentiable 𝕜 (λ (x : 𝕜), polynomial.eval x p)
@[protected]
theorem
polynomial.differentiable_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
differentiable 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q)
@[protected]
theorem
polynomial.differentiable_on
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
(p : polynomial 𝕜) :
differentiable_on 𝕜 (λ (x : 𝕜), polynomial.eval x p) s
@[protected]
theorem
polynomial.differentiable_on_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
differentiable_on 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q) s
@[protected, simp]
theorem
polynomial.deriv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(p : polynomial 𝕜) :
deriv (λ (x : 𝕜), polynomial.eval x p) x = polynomial.eval x (⇑polynomial.derivative p)
@[protected, simp]
theorem
polynomial.deriv_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
deriv (λ (x : 𝕜), ⇑(polynomial.aeval x) q) x = ⇑(polynomial.aeval x) (⇑polynomial.derivative q)
@[protected]
theorem
polynomial.deriv_within
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(p : polynomial 𝕜)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), polynomial.eval x p) s x = polynomial.eval x (⇑polynomial.derivative p)
@[protected]
theorem
polynomial.deriv_within_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), ⇑(polynomial.aeval x) q) s x = ⇑(polynomial.aeval x) (⇑polynomial.derivative q)
@[protected]
theorem
polynomial.has_fderiv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(p : polynomial 𝕜)
(x : 𝕜) :
has_fderiv_at (λ (x : 𝕜), polynomial.eval x p) (1.smul_right (polynomial.eval x (⇑polynomial.derivative p))) x
@[protected]
theorem
polynomial.has_fderiv_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(x : 𝕜) :
has_fderiv_at (λ (x : 𝕜), ⇑(polynomial.aeval x) q) (1.smul_right (⇑(polynomial.aeval x) (⇑polynomial.derivative q))) x
@[protected]
theorem
polynomial.has_fderiv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
(p : polynomial 𝕜)
(x : 𝕜) :
has_fderiv_within_at (λ (x : 𝕜), polynomial.eval x p) (1.smul_right (polynomial.eval x (⇑polynomial.derivative p))) s x
@[protected]
theorem
polynomial.has_fderiv_within_at_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(x : 𝕜) :
has_fderiv_within_at (λ (x : 𝕜), ⇑(polynomial.aeval x) q) (1.smul_right (⇑(polynomial.aeval x) (⇑polynomial.derivative q))) s x
@[protected, simp]
theorem
polynomial.fderiv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(p : polynomial 𝕜) :
fderiv 𝕜 (λ (x : 𝕜), polynomial.eval x p) x = 1.smul_right (polynomial.eval x (⇑polynomial.derivative p))
@[protected, simp]
theorem
polynomial.fderiv_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R) :
fderiv 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q) x = 1.smul_right (⇑(polynomial.aeval x) (⇑polynomial.derivative q))
@[protected]
theorem
polynomial.fderiv_within
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(p : polynomial 𝕜)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : 𝕜), polynomial.eval x p) s x = 1.smul_right (polynomial.eval x (⇑polynomial.derivative p))
@[protected]
theorem
polynomial.fderiv_within_aeval
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{R : Type u_1}
[comm_semiring R]
[algebra R 𝕜]
(q : polynomial R)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : 𝕜), ⇑(polynomial.aeval x) q) s x = 1.smul_right (⇑(polynomial.aeval x) (⇑polynomial.derivative q))