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

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

theorem Complex.hasStrictFDerivAt_cpow {p : ℂ × ℂ} (hp : p.1 ∈ Complex.slitPlane) : HasStrictFDerivAt (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 Complex.hasStrictFDerivAt_cpow' {x y : ℂ} (hp : x ∈ Complex.slitPlane) : HasStrictFDerivAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) ((y * x ^ (y - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (x ^ y * Complex.log x) • ContinuousLinearMap.snd ℂ ℂ ℂ) (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 g : E → ℂ} {f' 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 g : E → ℂ} {f' 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 g : E → ℂ} {f' 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 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 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 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 ∨ ∀ x ∈ s, f x ≠ 0) : DifferentiableOn ℂ (fun (x : E) => c ^ f x) s

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

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 differentiable_const_cpow_of_neZero (z : ℂ) [NeZero z] : Differentiable ℂ fun (s : ℂ) => z ^ s

theorem differentiableAt_const_cpow_of_neZero (z : ℂ) [NeZero z] (t : ℂ) : DifferentiableAt ℂ (fun (s : ℂ) => z ^ s) t

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.differentiableOn_rpow_const (p : ℝ) : DifferentiableOn ℝ (fun (x : ℝ) => x ^ p) {0}ᶜ

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 g : E → ℝ} {f' 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 g : E → ℝ} {f' 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 g : E → ℝ} {f' 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 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 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 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

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

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 : ∀ x ∈ s, 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 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 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 g : E → ℝ} {s : Set E} {n : ℕ∞} (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

theorem ContDiff.rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f 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 : ∀ x ∈ s, 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.