Documentation

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

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

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

theorem Complex.hasStrictDerivAt_const_cpow {x : } {y : } (h : x 0 y 0) :
HasStrictDerivAt (fun (y : ) => x ^ y) (x ^ y * Complex.log x) y
theorem Complex.hasFDerivAt_cpow {p : × } (hp : p.1 Complex.slitPlane) :
HasFDerivAt (fun (x : × ) => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) ContinuousLinearMap.fst + (p.1 ^ p.2 * Complex.log p.1) ContinuousLinearMap.snd ) p
theorem HasStrictFDerivAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem HasStrictFDerivAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasFDerivAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem HasFDerivAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasFDerivWithinAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem HasFDerivWithinAt.const_cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem DifferentiableAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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
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
theorem DifferentiableWithinAt.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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
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
theorem DifferentiableOn.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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
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 xs, f x 0) :
DifferentiableOn (fun (x : E) => c ^ f x) s
theorem Differentiable.cpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} (hf : Differentiable f) (hg : Differentiable g) (h0 : ∀ (x : E), f x Complex.slitPlane) :
Differentiable fun (x : E) => f x ^ g x
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
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
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
theorem Complex.hasStrictDerivAt_cpow_const {x : } {c : } (h : x Complex.slitPlane) :
HasStrictDerivAt (fun (z : ) => z ^ c) (c * x ^ (c - 1)) x
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
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
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
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
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
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
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
theorem hasDerivAt_ofReal_cpow {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.

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 * Real.log p.1) ContinuousLinearMap.snd ) p

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

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 * Real.log p.1 - Real.exp (Real.log p.1 * p.2) * Real.sin (p.2 * Real.pi) * Real.pi) ContinuousLinearMap.snd ) p

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

theorem Real.contDiffAt_rpow_of_ne (p : × ) (hp : p.1 0) {n : ℕ∞} :
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.

theorem Real.differentiableAt_rpow_of_ne (p : × ) (hp : p.1 0) :
DifferentiableAt (fun (p : × ) => p.1 ^ p.2) p
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
theorem Real.hasStrictDerivAt_rpow_const_of_ne {x : } (hx : x 0) (p : ) :
HasStrictDerivAt (fun (x : ) => x ^ p) (p * x ^ (p - 1)) x
theorem Real.hasStrictDerivAt_const_rpow {a : } (ha : 0 < a) (x : ) :
HasStrictDerivAt (fun (x : ) => a ^ x) (a ^ x * Real.log a) x
theorem Real.differentiableAt_rpow_const_of_ne (p : ) {x : } (hx : x 0) :
DifferentiableAt (fun (x : ) => x ^ p) x
theorem Real.hasStrictDerivAt_const_rpow_of_neg {a : } {x : } (ha : a < 0) :
HasStrictDerivAt (fun (x : ) => a ^ x) (a ^ x * Real.log a - Real.exp (Real.log a * x) * Real.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.

theorem Real.hasDerivAt_rpow_const {x : } {p : } (h : x 0 1 p) :
HasDerivAt (fun (x : ) => x ^ p) (p * x ^ (p - 1)) x
theorem Real.differentiable_rpow_const {p : } (hp : 1 p) :
Differentiable fun (x : ) => x ^ p
theorem Real.deriv_rpow_const {x : } {p : } (h : x 0 1 p) :
deriv (fun (x : ) => x ^ p) x = p * x ^ (p - 1)
theorem Real.deriv_rpow_const' {p : } (h : 1 p) :
(deriv fun (x : ) => x ^ p) = fun (x : ) => p * x ^ (p - 1)
theorem Real.contDiffAt_rpow_const_of_ne {x : } {p : } {n : ℕ∞} (h : x 0) :
ContDiffAt n (fun (x : ) => x ^ p) x
theorem Real.contDiff_rpow_const_of_le {p : } {n : } (h : n p) :
ContDiff n fun (x : ) => x ^ p
theorem Real.contDiffAt_rpow_const_of_le {x : } {p : } {n : } (h : n p) :
ContDiffAt (↑n) (fun (x : ) => x ^ p) x
theorem Real.contDiffAt_rpow_const {x : } {p : } {n : } (h : x 0 n p) :
ContDiffAt (↑n) (fun (x : ) => x ^ p) x
theorem Real.hasStrictDerivAt_rpow_const {x : } {p : } (hx : x 0 1 p) :
HasStrictDerivAt (fun (x : ) => x ^ p) (p * x ^ (p - 1)) x
theorem HasFDerivWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem HasFDerivAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem HasStrictFDerivAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {f' : E →L[] } {g' : E →L[] } {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
theorem DifferentiableWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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
theorem DifferentiableAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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
theorem DifferentiableOn.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {s : Set E} (hf : DifferentiableOn f s) (hg : DifferentiableOn g s) (h : xs, f x 0) :
DifferentiableOn (fun (x : E) => f x ^ g x) s
theorem Differentiable.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} (hf : Differentiable f) (hg : Differentiable g) (h : ∀ (x : E), f x 0) :
Differentiable fun (x : E) => f x ^ g x
theorem HasFDerivWithinAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasFDerivAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasStrictFDerivAt.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
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
@[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
theorem DifferentiableOn.rpow_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {p : } (hf : DifferentiableOn f s) (h : xs, f x 0 1 p) :
DifferentiableOn (fun (x : E) => f x ^ p) s
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
theorem HasFDerivWithinAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasFDerivAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem HasStrictFDerivAt.const_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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
theorem ContDiffWithinAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {x : E} {s : Set E} {n : ℕ∞} (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
theorem ContDiffAt.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) (hg : ContDiffAt n g x) (h : f x 0) :
ContDiffAt n (fun (x : E) => f x ^ g x) x
theorem ContDiffOn.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) (hg : ContDiffOn n g s) (h : xs, f x 0) :
ContDiffOn n (fun (x : E) => f x ^ g x) s
theorem ContDiff.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {g : E} {n : ℕ∞} (hf : ContDiff n f) (hg : ContDiff n g) (h : ∀ (x : E), f x 0) :
ContDiff n fun (x : E) => f x ^ g x
theorem ContDiffWithinAt.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {p : } {n : ℕ∞} (hf : ContDiffWithinAt n f s x) (h : f x 0) :
ContDiffWithinAt n (fun (x : E) => f x ^ p) s x
theorem ContDiffAt.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {p : } {n : ℕ∞} (hf : ContDiffAt n f x) (h : f x 0) :
ContDiffAt n (fun (x : E) => f x ^ p) x
theorem ContDiffOn.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {p : } {n : ℕ∞} (hf : ContDiffOn n f s) (h : xs, f x 0) :
ContDiffOn n (fun (x : E) => f x ^ p) s
theorem ContDiff.rpow_const_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {p : } {n : ℕ∞} (hf : ContDiff n f) (h : ∀ (x : E), f x 0) :
ContDiff n fun (x : E) => f x ^ p
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
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
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
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
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
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
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
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
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)
@[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)
theorem isTheta_deriv_rpow_const_atTop {p : } (hp : p 0) :
(deriv fun (x : ) => x ^ p) =Θ[Filter.atTop] fun (x : ) => x ^ (p - 1)
theorem isBigO_deriv_rpow_const_atTop (p : ) :
(deriv fun (x : ) => x ^ p) =O[Filter.atTop] fun (x : ) => x ^ (p - 1)
theorem tendsto_one_plus_div_rpow_exp (t : ) :
Filter.Tendsto (fun (x : ) => (1 + t / x) ^ x) Filter.atTop (nhds (Real.exp t))

The function (1 + t/x) ^ x tends to exp t at +∞.

theorem tendsto_one_plus_div_pow_exp (t : ) :
Filter.Tendsto (fun (x : ) => (1 + t / x) ^ x) Filter.atTop (nhds (Real.exp t))

The function (1 + t/x) ^ x tends to exp t at +∞ for naturals x.