# Derivatives of power function on `ℂ`, `ℝ`, `ℝ≥0`, and `ℝ≥0∞` #

We also prove differentiability and provide derivatives for the power functions `x ^ y`.

source
theorem Complex.hasStrictFDerivAt_cpow {p : ℂ × ℂ} (hp : p.1 ∈ slitPlane) :
HasStrictFDerivAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
source
theorem Complex.hasStrictFDerivAt_cpow' {x y : ℂ} (hp : x ∈ slitPlane) :
HasStrictFDerivAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) ((y * x ^ (y - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (x ^ y * log x) • ContinuousLinearMap.snd ℂ ℂ ℂ) (x, y)
source
theorem Complex.hasStrictDerivAt_const_cpow {x y : ℂ} (h : x ≠ 0 ∨ y ≠ 0) :
HasStrictDerivAt (fun (y : ℂ) => x ^ y) (x ^ y * log x) y
source
theorem Complex.hasFDerivAt_cpow {p : ℂ × ℂ} (hp : p.1 ∈ slitPlane) :
HasFDerivAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
source
theorem HasStrictFDerivAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E} {x : E} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) (h0 : f x ∈ Complex.slitPlane) :
HasStrictFDerivAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
source
theorem HasStrictFDerivAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} {c : ℂ} (hf : HasStrictFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
HasStrictFDerivAt (fun (x : E) => c ^ f x) ((c ^ f x * Complex.log c) • f') x
source
theorem HasFDerivAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (h0 : f x ∈ Complex.slitPlane) :
HasFDerivAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
source
theorem HasFDerivAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} {c : ℂ} (hf : HasFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
HasFDerivAt (fun (x : E) => c ^ f x) ((c ^ f x * Complex.log c) • f') x
source
theorem HasFDerivWithinAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) (h0 : f x ∈ Complex.slitPlane) :
HasFDerivWithinAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
source
theorem HasFDerivWithinAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} {s : Set E} {c : ℂ} (hf : HasFDerivWithinAt f f' s x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
HasFDerivWithinAt (fun (x : E) => c ^ f x) ((c ^ f x * Complex.log c) • f') s x
source
theorem DifferentiableAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {x : E} (hf : DifferentiableAt ℂ f x) (hg : DifferentiableAt ℂ g x) (h0 : f x ∈ Complex.slitPlane) :
DifferentiableAt ℂ (fun (x : E) => f x ^ g x) x
source
theorem DifferentiableAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {c : ℂ} (hf : DifferentiableAt ℂ f x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
DifferentiableAt ℂ (fun (x : E) => c ^ f x) x
source
theorem DifferentiableAt.cpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {c : ℂ} (hf : DifferentiableAt ℂ f x) (h0 : f x ∈ Complex.slitPlane) :
DifferentiableAt ℂ (fun (x : E) => f x ^ c) x
source
theorem DifferentiableWithinAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℂ f s x) (hg : DifferentiableWithinAt ℂ g s x) (h0 : f x ∈ Complex.slitPlane) :
DifferentiableWithinAt ℂ (fun (x : E) => f x ^ g x) s x
source
theorem DifferentiableWithinAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} {c : ℂ} (hf : DifferentiableWithinAt ℂ f s x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
DifferentiableWithinAt ℂ (fun (x : E) => c ^ f x) s x
source
theorem DifferentiableWithinAt.cpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} {c : ℂ} (hf : DifferentiableWithinAt ℂ f s x) (h0 : f x ∈ Complex.slitPlane) :
DifferentiableWithinAt ℂ (fun (x : E) => f x ^ c) s x
source
theorem DifferentiableOn.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} {s : Set E} (hf : DifferentiableOn ℂ f s) (hg : DifferentiableOn ℂ g s) (h0 : Set.MapsTo f s Complex.slitPlane) :
DifferentiableOn ℂ (fun (x : E) => f x ^ g x) s
source
theorem DifferentiableOn.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {c : ℂ} (hf : DifferentiableOn ℂ f s) (h0 : c ≠ 0 ∨ ∀ x ∈ s, f x ≠ 0) :
DifferentiableOn ℂ (fun (x : E) => c ^ f x) s
source
theorem DifferentiableOn.cpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {c : ℂ} (hf : DifferentiableOn ℂ f s) (h0 : ∀ x ∈ s, f x ∈ Complex.slitPlane) :
DifferentiableOn ℂ (fun (x : E) => f x ^ c) s
source
theorem Differentiable.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : E → ℂ} (hf : Differentiable ℂ f) (hg : Differentiable ℂ g) (h0 : ∀ (x : E), f x ∈ Complex.slitPlane) :
Differentiable ℂ fun (x : E) => f x ^ g x
source
theorem Differentiable.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {c : ℂ} (hf : Differentiable ℂ f) (h0 : c ≠ 0 ∨ ∀ (x : E), f x ≠ 0) :
Differentiable ℂ fun (x : E) => c ^ f x
source
theorem differentiable_const_cpow_of_neZero (z : ℂ) [NeZero z] :
Differentiable ℂ fun (s : ℂ) => z ^ s
source
theorem differentiableAt_const_cpow_of_neZero (z : ℂ) [NeZero z] (t : ℂ) :
DifferentiableAt ℂ (fun (s : ℂ) => z ^ s) t
source
theorem HasStrictDerivAt.cpow {f g : ℂ → ℂ} {f' g' x : ℂ} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) (h0 : f x ∈ Complex.slitPlane) :
HasStrictDerivAt (fun (x : ℂ) => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
source
theorem HasStrictDerivAt.const_cpow {f : ℂ → ℂ} {f' x c : ℂ} (hf : HasStrictDerivAt f f' x) (h : c ≠ 0 ∨ f x ≠ 0) :
HasStrictDerivAt (fun (x : ℂ) => c ^ f x) (c ^ f x * Complex.log c * f') x
source
theorem Complex.hasStrictDerivAt_cpow_const {x c : ℂ} (h : x ∈ slitPlane) :
HasStrictDerivAt (fun (z : ℂ) => z ^ c) (c * x ^ (c - 1)) x
source
theorem HasStrictDerivAt.cpow_const {f : ℂ → ℂ} {f' x c : ℂ} (hf : HasStrictDerivAt f f' x) (h0 : f x ∈ Complex.slitPlane) :
HasStrictDerivAt (fun (x : ℂ) => f x ^ c) (c * f x ^ (c - 1) * f') x
source
theorem HasDerivAt.cpow {f g : ℂ → ℂ} {f' g' x : ℂ} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h0 : f x ∈ Complex.slitPlane) :
HasDerivAt (fun (x : ℂ) => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
source
theorem HasDerivAt.const_cpow {f : ℂ → ℂ} {f' x c : ℂ} (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
HasDerivAt (fun (x : ℂ) => c ^ f x) (c ^ f x * Complex.log c * f') x
source
theorem HasDerivAt.cpow_const {f : ℂ → ℂ} {f' x c : ℂ} (hf : HasDerivAt f f' x) (h0 : f x ∈ Complex.slitPlane) :
HasDerivAt (fun (x : ℂ) => f x ^ c) (c * f x ^ (c - 1) * f') x
source
theorem HasDerivWithinAt.cpow {f g : ℂ → ℂ} {s : Set ℂ} {f' g' x : ℂ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) (h0 : f x ∈ Complex.slitPlane) :
HasDerivWithinAt (fun (x : ℂ) => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
source
theorem HasDerivWithinAt.const_cpow {f : ℂ → ℂ} {s : Set ℂ} {f' x c : ℂ} (hf : HasDerivWithinAt f f' s x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
HasDerivWithinAt (fun (x : ℂ) => c ^ f x) (c ^ f x * Complex.log c * f') s x
source
theorem HasDerivWithinAt.cpow_const {f : ℂ → ℂ} {s : Set ℂ} {f' x c : ℂ} (hf : HasDerivWithinAt f f' s x) (h0 : f x ∈ Complex.slitPlane) :
HasDerivWithinAt (fun (x : ℂ) => f x ^ c) (c * f x ^ (c - 1) * f') s x
source
theorem hasDerivAt_ofReal_cpow_const' {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ -1) :
HasDerivAt (fun (y : ℝ) => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Although `fun x => x ^ r` for fixed `r` is not complex-differentiable along the negative real line, it is still real-differentiable, and the derivative is what one would formally expect. See `hasDerivAt_ofReal_cpow_const` for an alternate formulation.

source
theorem hasDerivAt_ofReal_cpow_const {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ 0) :
HasDerivAt (fun (y : ℝ) => ↑y ^ r) (r * ↑x ^ (r - 1)) x

An alternate formulation of `hasDerivAt_ofReal_cpow_const'`.

source
theorem DifferentiableAt.ofReal_cpow_const {c : ℂ} {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (h0 : f x ≠ 0) (h1 : c ≠ 0) :
DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y) ^ c) x

A version of `DifferentiableAt.cpow_const` for a real function.

source
theorem Complex.deriv_cpow_const {x c : ℂ} (hx : x ∈ slitPlane) :
deriv (fun (x : ℂ) => x ^ c) x = c * x ^ (c - 1)
source
theorem Complex.deriv_ofReal_cpow_const {c : ℂ} {x : ℝ} (hx : x ≠ 0) (hc : c ≠ 0) :
deriv (fun (x : ℝ) => ↑x ^ c) x = c * ↑x ^ (c - 1)

A version of `Complex.deriv_cpow_const` for a real variable.

source
theorem deriv_cpow_const {f : ℂ → ℂ} {x c : ℂ} (hf : DifferentiableAt ℂ f x) (hx : f x ∈ Complex.slitPlane) :
deriv (fun (x : ℂ) => f x ^ c) x = c * f x ^ (c - 1) * deriv f x
source
theorem isTheta_deriv_ofReal_cpow_const_atTop {c : ℂ} (hc : c ≠ 0) :
(deriv fun (x : ℝ) => ↑x ^ c) =Θ[Filter.atTop] fun (x : ℝ) => x ^ (c.re - 1)
source
theorem isBigO_deriv_ofReal_cpow_const_atTop (c : ℂ) :
(deriv fun (x : ℝ) => ↑x ^ c) =O[Filter.atTop] fun (x : ℝ) => x ^ (c.re - 1)
source
theorem Real.hasStrictFDerivAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.1) :
HasStrictFDerivAt (fun (x : ℝ × ℝ) => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

`(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `0 < p.fst`.

source
theorem Real.hasStrictFDerivAt_rpow_of_neg (p : ℝ × ℝ) (hp : p.1 < 0) :
HasStrictFDerivAt (fun (x : ℝ × ℝ) => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - exp (log p.1 * p.2) * sin (p.2 * Real.pi) * Real.pi) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

`(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `p.fst < 0`.

source
theorem Real.contDiffAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) {n : WithTop ℕ∞} :
ContDiffAt ℝ n (fun (p : ℝ × ℝ) => p.1 ^ p.2) p

The function `fun (x, y) => x ^ y` is infinitely smooth at `(x, y)` unless `x = 0`.

source
theorem Real.differentiableAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) :
DifferentiableAt ℝ (fun (p : ℝ × ℝ) => p.1 ^ p.2) p
source
theorem HasStrictDerivAt.rpow {x : ℝ} {f g : ℝ → ℝ} {f' g' : ℝ} (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) (h : 0 < f x) :
HasStrictDerivAt (fun (x : ℝ) => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
source
theorem Real.hasStrictDerivAt_rpow_const_of_ne {x : ℝ} (hx : x ≠ 0) (p : ℝ) :
HasStrictDerivAt (fun (x : ℝ) => x ^ p) (p * x ^ (p - 1)) x
source
theorem Real.hasStrictDerivAt_const_rpow {a : ℝ} (ha : 0 < a) (x : ℝ) :
HasStrictDerivAt (fun (x : ℝ) => a ^ x) (a ^ x * log a) x
source
theorem Real.differentiableAt_rpow_const_of_ne (p : ℝ) {x : ℝ} (hx : x ≠ 0) :
DifferentiableAt ℝ (fun (x : ℝ) => x ^ p) x
source
theorem Real.differentiableOn_rpow_const (p : ℝ) :
DifferentiableOn ℝ (fun (x : ℝ) => x ^ p) {0}ᶜ
source
theorem Real.hasStrictDerivAt_const_rpow_of_neg {a x : ℝ} (ha : a < 0) :
HasStrictDerivAt (fun (x : ℝ) => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * Real.pi) * Real.pi) x

This lemma says that `fun x => a ^ x` is strictly differentiable for `a < 0`. Note that these values of `a` are outside of the "official" domain of `a ^ x`, and we may redefine `a ^ x` for negative `a` if some other definition will be more convenient.

source
theorem Real.hasDerivAt_rpow_const {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) :
HasDerivAt (fun (x : ℝ) => x ^ p) (p * x ^ (p - 1)) x
source
theorem Real.differentiable_rpow_const {p : ℝ} (hp : 1 ≤ p) :
Differentiable ℝ fun (x : ℝ) => x ^ p
source
theorem Real.deriv_rpow_const {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) :
deriv (fun (x : ℝ) => x ^ p) x = p * x ^ (p - 1)
source
theorem Real.deriv_rpow_const' {p : ℝ} (h : 1 ≤ p) :
(deriv fun (x : ℝ) => x ^ p) = fun (x : ℝ) => p * x ^ (p - 1)
source
theorem Real.contDiffAt_rpow_const_of_ne {x p : ℝ} {n : WithTop ℕ∞} (h : x ≠ 0) :
ContDiffAt ℝ n (fun (x : ℝ) => x ^ p) x
source
theorem Real.contDiff_rpow_const_of_le {p : ℝ} {n : ℕ} (h : ↑n ≤ p) :
ContDiff ℝ ↑n fun (x : ℝ) => x ^ p
source
theorem Real.contDiffAt_rpow_const_of_le {x p : ℝ} {n : ℕ} (h : ↑n ≤ p) :
ContDiffAt ℝ (↑n) (fun (x : ℝ) => x ^ p) x
source
theorem Real.contDiffAt_rpow_const {x p : ℝ} {n : ℕ} (h : x ≠ 0 ∨ ↑n ≤ p) :
ContDiffAt ℝ (↑n) (fun (x : ℝ) => x ^ p) x
source
theorem Real.hasStrictDerivAt_rpow_const {x p : ℝ} (hx : x ≠ 0 ∨ 1 ≤ p) :
HasStrictDerivAt (fun (x : ℝ) => x ^ p) (p * x ^ (p - 1)) x
source
theorem HasFDerivWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E} {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) (h : 0 < f x) :
HasFDerivWithinAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x
source
theorem HasFDerivAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E} {x : E} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (h : 0 < f x) :
HasFDerivAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
source
theorem HasStrictFDerivAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {f' g' : StrongDual ℝ E} {x : E} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) (h : 0 < f x) :
HasStrictFDerivAt (fun (x : E) => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
source
theorem DifferentiableWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) (h : f x ≠ 0) :
DifferentiableWithinAt ℝ (fun (x : E) => f x ^ g x) s x
source
theorem DifferentiableAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (h : f x ≠ 0) :
DifferentiableAt ℝ (fun (x : E) => f x ^ g x) x
source
theorem DifferentiableOn.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {s : Set E} (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) (h : ∀ x ∈ s, f x ≠ 0) :
DifferentiableOn ℝ (fun (x : E) => f x ^ g x) s
source
theorem Differentiable.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (h : ∀ (x : E), f x ≠ 0) :
Differentiable ℝ fun (x : E) => f x ^ g x
source
theorem HasFDerivWithinAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {s : Set E} {p : ℝ} (hf : HasFDerivWithinAt f f' s x) (h : f x ≠ 0 ∨ 1 ≤ p) :
HasFDerivWithinAt (fun (x : E) => f x ^ p) ((p * f x ^ (p - 1)) • f') s x
source
theorem HasFDerivAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {p : ℝ} (hf : HasFDerivAt f f' x) (h : f x ≠ 0 ∨ 1 ≤ p) :
HasFDerivAt (fun (x : E) => f x ^ p) ((p * f x ^ (p - 1)) • f') x
source
theorem HasStrictFDerivAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {p : ℝ} (hf : HasStrictFDerivAt f f' x) (h : f x ≠ 0 ∨ 1 ≤ p) :
HasStrictFDerivAt (fun (x : E) => f x ^ p) ((p * f x ^ (p - 1)) • f') x
source
theorem DifferentiableWithinAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ} (hf : DifferentiableWithinAt ℝ f s x) (h : f x ≠ 0 ∨ 1 ≤ p) :
DifferentiableWithinAt ℝ (fun (x : E) => f x ^ p) s x
source
@[simp]
theorem DifferentiableAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ} (hf : DifferentiableAt ℝ f x) (h : f x ≠ 0 ∨ 1 ≤ p) :
DifferentiableAt ℝ (fun (x : E) => f x ^ p) x
source
theorem DifferentiableOn.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ} (hf : DifferentiableOn ℝ f s) (h : ∀ x ∈ s, f x ≠ 0 ∨ 1 ≤ p) :
DifferentiableOn ℝ (fun (x : E) => f x ^ p) s
source
theorem Differentiable.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} (hf : Differentiable ℝ f) (h : ∀ (x : E), f x ≠ 0 ∨ 1 ≤ p) :
Differentiable ℝ fun (x : E) => f x ^ p
source
theorem HasFDerivWithinAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {s : Set E} {c : ℝ} (hf : HasFDerivWithinAt f f' s x) (hc : 0 < c) :
HasFDerivWithinAt (fun (x : E) => c ^ f x) ((c ^ f x * Real.log c) • f') s x
source
theorem HasFDerivAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {c : ℝ} (hf : HasFDerivAt f f' x) (hc : 0 < c) :
HasFDerivAt (fun (x : E) => c ^ f x) ((c ^ f x * Real.log c) • f') x
source
theorem HasStrictFDerivAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E} {c : ℝ} (hf : HasStrictFDerivAt f f' x) (hc : 0 < c) :
HasStrictFDerivAt (fun (x : E) => c ^ f x) ((c ^ f x * Real.log c) • f') x
source
theorem ContDiffWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) (h : f x ≠ 0) :
ContDiffWithinAt ℝ n (fun (x : E) => f x ^ g x) s x
source
theorem ContDiffAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (h : f x ≠ 0) :
ContDiffAt ℝ n (fun (x : E) => f x ^ g x) x
source
theorem ContDiffOn.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) (h : ∀ x ∈ s, f x ≠ 0) :
ContDiffOn ℝ n (fun (x : E) => f x ^ g x) s
source
theorem ContDiff.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (h : ∀ (x : E), f x ≠ 0) :
ContDiff ℝ n fun (x : E) => f x ^ g x
source
theorem ContDiffWithinAt.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (h : f x ≠ 0) :
ContDiffWithinAt ℝ n (fun (x : E) => f x ^ p) s x
source
theorem ContDiffAt.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (h : f x ≠ 0) :
ContDiffAt ℝ n (fun (x : E) => f x ^ p) x
source
theorem ContDiffOn.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (h : ∀ x ∈ s, f x ≠ 0) :
ContDiffOn ℝ n (fun (x : E) => f x ^ p) s
source
theorem ContDiff.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (h : ∀ (x : E), f x ≠ 0) :
ContDiff ℝ n fun (x : E) => f x ^ p
source
theorem ContDiffWithinAt.rpow_const_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ} {m : ℕ} (hf : ContDiffWithinAt ℝ (↑m) f s x) (h : ↑m ≤ p) :
ContDiffWithinAt ℝ (↑m) (fun (x : E) => f x ^ p) s x
source
theorem ContDiffAt.rpow_const_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ} {m : ℕ} (hf : ContDiffAt ℝ (↑m) f x) (h : ↑m ≤ p) :
ContDiffAt ℝ (↑m) (fun (x : E) => f x ^ p) x
source
theorem ContDiffOn.rpow_const_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ} {m : ℕ} (hf : ContDiffOn ℝ (↑m) f s) (h : ↑m ≤ p) :
ContDiffOn ℝ (↑m) (fun (x : E) => f x ^ p) s
source
theorem ContDiff.rpow_const_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} {m : ℕ} (hf : ContDiff ℝ (↑m) f) (h : ↑m ≤ p) :
ContDiff ℝ ↑m fun (x : E) => f x ^ p
source
theorem HasDerivWithinAt.rpow {f g : ℝ → ℝ} {f' g' x : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) (h : 0 < f x) :
HasDerivWithinAt (fun (x : ℝ) => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
source
theorem HasDerivAt.rpow {f g : ℝ → ℝ} {f' g' x : ℝ} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h : 0 < f x) :
HasDerivAt (fun (x : ℝ) => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
source
theorem HasDerivWithinAt.rpow_const {f : ℝ → ℝ} {f' x p : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
HasDerivWithinAt (fun (y : ℝ) => f y ^ p) (f' * p * f x ^ (p - 1)) s x
source
theorem HasDerivAt.rpow_const {f : ℝ → ℝ} {f' x p : ℝ} (hf : HasDerivAt f f' x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
HasDerivAt (fun (y : ℝ) => f y ^ p) (f' * p * f x ^ (p - 1)) x
source
theorem derivWithin_rpow_const {f : ℝ → ℝ} {x p : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0 ∨ 1 ≤ p) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => f x ^ p) s x = derivWithin f s x * p * f x ^ (p - 1)
source
@[simp]
theorem deriv_rpow_const {f : ℝ → ℝ} {x p : ℝ} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
deriv (fun (x : ℝ) => f x ^ p) x = deriv f x * p * f x ^ (p - 1)
source
theorem deriv_norm_ofReal_cpow (c : ℂ) {t : ℝ} (ht : 0 < t) :
deriv (fun (x : ℝ) => ‖↑x ^ c‖) t = c.re * t ^ (c.re - 1)
source
theorem isTheta_deriv_rpow_const_atTop {p : ℝ} (hp : p ≠ 0) :
(deriv fun (x : ℝ) => x ^ p) =Θ[Filter.atTop] fun (x : ℝ) => x ^ (p - 1)
source
theorem isBigO_deriv_rpow_const_atTop (p : ℝ) :
(deriv fun (x : ℝ) => x ^ p) =O[Filter.atTop] fun (x : ℝ) => x ^ (p - 1)
source
theorem HasDerivWithinAt.const_rpow {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ} {a : ℝ} (ha : 0 < a) (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ℝ) => a ^ f x) (Real.log a * f' * a ^ f x) s x
source
theorem HasDerivAt.const_rpow {f : ℝ → ℝ} {f' x a : ℝ} (ha : 0 < a) (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => a ^ f x) (Real.log a * f' * a ^ f x) x
source
theorem derivWithin_const_rpow {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} {a : ℝ} (ha : 0 < a) (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => a ^ f x) s x = Real.log a * derivWithin f s x * a ^ f x
source
@[simp]
theorem deriv_const_rpow {f : ℝ → ℝ} {x a : ℝ} (ha : 0 < a) (hf : DifferentiableAt ℝ f x) :
deriv (fun (x : ℝ) => a ^ f x) x = Real.log a * deriv f x * a ^ f x