mathlib3 documentation

analysis.calculus.deriv.polynomial

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 #

Keywords #

derivative, polynomial

Derivative of a polynomial #

@[protected]

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

@[protected]
@[protected]
theorem polynomial.has_deriv_at {𝕜 : Type u} [nontrivially_normed_field 𝕜] (p : polynomial 𝕜) (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 : 𝕜) :
@[protected]
theorem polynomial.has_deriv_within_at {𝕜 : Type u} [nontrivially_normed_field 𝕜] (p : polynomial 𝕜) (x : 𝕜) (s : set 𝕜) :
@[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 𝕜) :
@[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 𝕜) :
@[protected, simp]
theorem polynomial.deriv_aeval {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {R : Type u_1} [comm_semiring R] [algebra R 𝕜] (q : polynomial R) :
@[protected]
theorem polynomial.deriv_within {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} (p : polynomial 𝕜) (hxs : unique_diff_within_at 𝕜 s x) :
@[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) :
@[protected]
theorem polynomial.has_fderiv_at {𝕜 : Type u} [nontrivially_normed_field 𝕜] (p : polynomial 𝕜) (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 : 𝕜) :
@[protected]
theorem polynomial.has_fderiv_within_at {𝕜 : Type u} [nontrivially_normed_field 𝕜] {s : set 𝕜} (p : polynomial 𝕜) (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 : 𝕜) :
@[protected, simp]
theorem polynomial.fderiv {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} (p : polynomial 𝕜) :
@[protected, simp]
theorem polynomial.fderiv_aeval {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {R : Type u_1} [comm_semiring R] [algebra R 𝕜] (q : polynomial R) :
@[protected]
theorem polynomial.fderiv_within {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} (p : polynomial 𝕜) (hxs : unique_diff_within_at 𝕜 s x) :
@[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) :