Polynomial.hasDerivAt_aeval
theorem Polynomial.hasDerivAt_aeval :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
(q : Polynomial R) (x : 𝕜),
HasDerivAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x
The theorem `Polynomial.hasDerivAt_aeval` states that for any nontrivially normed field `𝕜`, any commutative semiring `R`, any `R`-algebra structure on `𝕜`, any polynomial `q` over `R`, and any element `x` of `𝕜`, the function that maps `x` to the evaluation of `q` at `x` has a derivative at `x`. The derivative at `x` is the evaluation of the derivative of `q` at `x`. In mathematical terms, if we denote the function `f(x) = (Polynomial.aeval x) q`, this theorem is saying that `f` has a derivative at `x`, and this derivative is `(Polynomial.aeval x) (Polynomial.derivative q)`.
More concisely: For any nontrivially normed field `𝕜`, commutative semiring `R`, `R`-algebra structure on `𝕜`, polynomial `q` over `R`, and element `x` of `𝕜`, the function `f(x) = (Polynomial.aeval x) q` has derivative `(Polynomial.aeval x) (Polynomial.derivative q)` at `x`.
|
Polynomial.differentiableAt
theorem Polynomial.differentiableAt :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜),
DifferentiableAt 𝕜 (fun x => Polynomial.eval x p) x
The theorem `Polynomial.differentiableAt` states that for any field `𝕜` equipped with a norm (specifically a field that is nontrivially normed), any polynomial `p` with coefficients in `𝕜`, and any point `x` in `𝕜`, the function that maps `x` to the evaluation of the polynomial `p` at `x` is differentiable at `x`. In other words, for any polynomial and any point, there exists a derivative of the polynomial at that point.
More concisely: For any field equipped with a norm and any polynomial with coefficients in that field, the polynomial evaluation function is differentiable.
|
Polynomial.hasDerivAt
theorem Polynomial.hasDerivAt :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
HasDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
This theorem states that for every non-trivially normed field `𝕜` and a polynomial `p` defined over `𝕜`, and for every element `x` of `𝕜`, the derivative of the polynomial `p` at the point `x` (in the sense of analysis) is given by the evaluation of the derivative of `p` at `x`. In mathematical terms, if we denote the polynomial evaluation function at `x` as `(fun x => Polynomial.eval x p)`, then its derivative at any point `x` is `(Polynomial.eval x (Polynomial.derivative p))`, where `Polynomial.derivative p` represents the formal derivative of the polynomial `p`.
More concisely: For any non-trivially normed field `𝕜` and polynomial `p` over `𝕜`, the derivative of `p` at an element `x` in `𝕜` is equal to the evaluation of the derivative of `p` at `x`.
|
Polynomial.hasStrictDerivAt
theorem Polynomial.hasStrictDerivAt :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
HasStrictDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
This theorem states that for any nontrivial normed field `𝕜` and any polynomial `p` over `𝕜`, the strict derivative of the polynomial at a point `x` in `𝕜` exists and is given by evaluating the formal derivative of the polynomial at `x`. In other words, the derivative of a polynomial function at a point in the classical analysis sense corresponds to the concept of the derivative in the algebraic sense, where the derivative of a polynomial is obtained by taking the derivative of each term separately.
More concisely: For any nontrivial normed field `𝕜` and polynomial `p` over `𝕜`, the strict derivative of `p` at a point `x` in `𝕜` equals the evaluation of the formal derivative of `p` at `x`.
|