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
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 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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 => 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 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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 => 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 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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 => 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 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
DifferentiableAt ℂ (fun x => 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 => 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 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
DifferentiableWithinAt ℂ (fun x => 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 => c ^ f x) s x
theorem
HasStrictDerivAt.cpow
{f : ℂ → ℂ}
{g : ℂ → ℂ}
{f' : ℂ}
{g' : ℂ}
{x : ℂ}
(hf : HasStrictDerivAt f f' x)
(hg : HasStrictDerivAt g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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
HasDerivAt.cpow
{f : ℂ → ℂ}
{g : ℂ → ℂ}
{f' : ℂ}
{g' : ℂ}
{x : ℂ}
(hf : HasDerivAt f f' x)
(hg : HasDerivAt g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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
HasDerivWithinAt.cpow
{f : ℂ → ℂ}
{g : ℂ → ℂ}
{s : Set ℂ}
{f' : ℂ}
{g' : ℂ}
{x : ℂ}
(hf : HasDerivWithinAt f f' s x)
(hg : HasDerivWithinAt g g' s x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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
(x, y) ↦ x ^ y
is strictly differentiable at p : ℝ × ℝ
such that 0 < p.fst
.
(x, y) ↦ x ^ y
is strictly differentiable at p : ℝ × ℝ
such that p.fst < 0
.
theorem
Real.contDiffAt_rpow_of_ne
(p : ℝ × ℝ)
(hp : p.fst ≠ 0)
{n : ℕ∞}
:
ContDiffAt ℝ n (fun p => p.fst ^ p.snd) 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.fst ≠ 0)
:
DifferentiableAt ℝ (fun p => p.fst ^ p.snd) p
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
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.contDiffAt_rpow_const_of_ne
{x : ℝ}
{p : ℝ}
{n : ℕ∞}
(h : x ≠ 0)
:
ContDiffAt ℝ n (fun x => x ^ p) x
theorem
Real.contDiffAt_rpow_const_of_le
{x : ℝ}
{p : ℝ}
{n : ℕ}
(h : ↑n ≤ p)
:
ContDiffAt ℝ (↑n) (fun x => x ^ p) 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)
:
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)
:
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)
:
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 => 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 => 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 : ∀ (x : E), x ∈ s → f x ≠ 0)
:
DifferentiableOn ℝ (fun x => 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 => 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)
:
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)
:
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)
:
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 => 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 => 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 : E), x ∈ s → f x ≠ 0 ∨ 1 ≤ p)
:
DifferentiableOn ℝ (fun x => 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 => 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)
:
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)
:
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)
:
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 => 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 => 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 : ∀ (x : E), x ∈ s → f x ≠ 0)
:
ContDiffOn ℝ n (fun x => f x ^ g x) s
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 => 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 => 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 : E), x ∈ s → f x ≠ 0)
:
ContDiffOn ℝ n (fun x => 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)
:
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 => 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 => 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 => 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)
:
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)
The function (1 + t/x) ^ x
tends to exp t
at +∞
.
The function (1 + t/x) ^ x
tends to exp t
at +∞
for naturals x
.