hasDerivAt_zpow
theorem hasDerivAt_zpow :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜),
x ≠ 0 ∨ 0 ≤ m → HasDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
The theorem `hasDerivAt_zpow` states that for any nontrivially normed field `𝕜` and any integer `m` and any element `x` of `𝕜`, if `x` is not equal to 0 or `m` is nonnegative, then the function `f(x) = x^m` has a derivative at `x`, and that derivative is `m * x^(m - 1)`. In mathematical notation, this says that if `x ≠ 0` or `m ≥ 0`, then `f'(x) = m * x^(m - 1)`.
More concisely: For any nontrivially normed field and any nonzero element x and nonnegative integer m, the function f(x) = x^m has derivative f'(x) = m * x^(m-1).
|
differentiableAt_zpow
theorem differentiableAt_zpow :
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {m : ℤ},
DifferentiableAt 𝕜 (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
This theorem states that for any nontrivially normed field `𝕜` and any point `x` from `𝕜` and integer `m`, the function `x ↦ x^m` is differentiable at `x` if and only if `x` is nonzero or `m` is nonnegative. In other words, in the context of a given field `𝕜`, the function which maps `x` to `x` raised to the power of `m` is differentiable at a point `x` exactly when `x` is not zero or `m` is zero or positive.
More concisely: The function `x ↦ x^m` is differentiable at `x` in a nontrivially normed field if and only if `x` is nonzero or `m` is nonnegative.
|