Derivatives of power function on ℂ
, ℝ
, ℝ≥0
, and ℝ≥0∞
#
We also prove differentiability and provide derivatives for the power functions x ^ y
.
theorem
complex.has_strict_deriv_at_const_cpow
{x y : ℂ}
(h : x ≠ 0 ∨ y ≠ 0) :
has_strict_deriv_at (λ (y : ℂ), x ^ y) (x ^ y * complex.log x) y
theorem
has_strict_fderiv_at.cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f g : E → ℂ}
{f' g' : E →L[ℂ] ℂ}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(hg : has_strict_fderiv_at g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_strict_fderiv_at.const_cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{c : ℂ}
(hf : has_strict_fderiv_at f f' x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
has_strict_fderiv_at (λ (x : E), c ^ f x) ((c ^ f x * complex.log c) • f') x
theorem
has_fderiv_at.cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f g : E → ℂ}
{f' g' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x)
(hg : has_fderiv_at g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_fderiv_at.const_cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{c : ℂ}
(hf : has_fderiv_at f f' x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
has_fderiv_at (λ (x : E), c ^ f x) ((c ^ f x * complex.log c) • f') x
theorem
has_fderiv_within_at.cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f g : E → ℂ}
{f' g' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(hg : has_fderiv_within_at g g' s x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_fderiv_within_at.const_cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
{c : ℂ}
(hf : has_fderiv_within_at f f' s x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
has_fderiv_within_at (λ (x : E), c ^ f x) ((c ^ f x * complex.log c) • f') s x
theorem
differentiable_at.cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f g : E → ℂ}
{x : E}
(hf : differentiable_at ℂ f x)
(hg : differentiable_at ℂ g x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable_at ℂ (λ (x : E), f x ^ g x) x
theorem
differentiable_at.const_cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{c : ℂ}
(hf : differentiable_at ℂ f x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
differentiable_at ℂ (λ (x : E), c ^ f x) x
theorem
differentiable_within_at.cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f g : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x)
(hg : differentiable_within_at ℂ g s x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable_within_at ℂ (λ (x : E), f x ^ g x) s x
theorem
differentiable_within_at.const_cpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{c : ℂ}
(hf : differentiable_within_at ℂ f s x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
differentiable_within_at ℂ (λ (x : E), c ^ f x) s x
theorem
has_strict_deriv_at.cpow
{f g : ℂ → ℂ}
{f' g' x : ℂ}
(hf : has_strict_deriv_at f f' x)
(hg : has_strict_deriv_at g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_strict_deriv_at.const_cpow
{f : ℂ → ℂ}
{f' x c : ℂ}
(hf : has_strict_deriv_at f f' x)
(h : c ≠ 0 ∨ f x ≠ 0) :
has_strict_deriv_at (λ (x : ℂ), c ^ f x) (c ^ f x * complex.log c * f') x
theorem
has_deriv_at.cpow
{f g : ℂ → ℂ}
{f' g' x : ℂ}
(hf : has_deriv_at f f' x)
(hg : has_deriv_at g g' x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_deriv_at.const_cpow
{f : ℂ → ℂ}
{f' x c : ℂ}
(hf : has_deriv_at f f' x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
has_deriv_at (λ (x : ℂ), c ^ f x) (c ^ f x * complex.log c * f') x
theorem
has_deriv_within_at.cpow
{f g : ℂ → ℂ}
{s : set ℂ}
{f' g' x : ℂ}
(hf : has_deriv_within_at f f' s x)
(hg : has_deriv_within_at g g' s x)
(h0 : 0 < (f x).re ∨ (f x).im ≠ 0) :
theorem
has_deriv_within_at.const_cpow
{f : ℂ → ℂ}
{s : set ℂ}
{f' x c : ℂ}
(hf : has_deriv_within_at f f' s x)
(h0 : c ≠ 0 ∨ f x ≠ 0) :
has_deriv_within_at (λ (x : ℂ), c ^ f x) (c ^ f x * complex.log c * f') s x
This lemma says that λ 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.cont_diff_at_rpow_const_of_ne
{x p : ℝ}
{n : ℕ∞}
(h : x ≠ 0) :
cont_diff_at ℝ n (λ (x : ℝ), x ^ p) x
theorem
has_fderiv_within_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{f' g' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x)
(hg : has_fderiv_within_at g g' s x)
(h : 0 < f x) :
theorem
has_fderiv_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{f' g' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x)
(hg : has_fderiv_at g g' x)
(h : 0 < f x) :
theorem
has_strict_fderiv_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{f' g' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x)
(hg : has_strict_fderiv_at g g' x)
(h : 0 < f x) :
theorem
differentiable_within_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hg : differentiable_within_at ℝ g s x)
(h : f x ≠ 0) :
differentiable_within_at ℝ (λ (x : E), f x ^ g x) s x
theorem
differentiable_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{x : E}
(hf : differentiable_at ℝ f x)
(hg : differentiable_at ℝ g x)
(h : f x ≠ 0) :
differentiable_at ℝ (λ (x : E), f x ^ g x) x
theorem
differentiable_on.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{s : set E}
(hf : differentiable_on ℝ f s)
(hg : differentiable_on ℝ g s)
(h : ∀ (x : E), x ∈ s → f x ≠ 0) :
differentiable_on ℝ (λ (x : E), f x ^ g x) s
theorem
differentiable.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
(hf : differentiable ℝ f)
(hg : differentiable ℝ g)
(h : ∀ (x : E), f x ≠ 0) :
differentiable ℝ (λ (x : E), f x ^ g x)
theorem
has_fderiv_within_at.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
{p : ℝ}
(hf : has_fderiv_within_at f f' s x)
(h : f x ≠ 0 ∨ 1 ≤ p) :
theorem
has_fderiv_at.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{p : ℝ}
(hf : has_fderiv_at f f' x)
(h : f x ≠ 0 ∨ 1 ≤ p) :
theorem
has_strict_fderiv_at.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{p : ℝ}
(hf : has_strict_fderiv_at f f' x)
(h : f x ≠ 0 ∨ 1 ≤ p) :
theorem
differentiable_within_at.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{p : ℝ}
(hf : differentiable_within_at ℝ f s x)
(h : f x ≠ 0 ∨ 1 ≤ p) :
differentiable_within_at ℝ (λ (x : E), f x ^ p) s x
@[simp]
theorem
differentiable_at.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{p : ℝ}
(hf : differentiable_at ℝ f x)
(h : f x ≠ 0 ∨ 1 ≤ p) :
differentiable_at ℝ (λ (x : E), f x ^ p) x
theorem
differentiable_on.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{p : ℝ}
(hf : differentiable_on ℝ f s)
(h : ∀ (x : E), x ∈ s → f x ≠ 0 ∨ 1 ≤ p) :
differentiable_on ℝ (λ (x : E), f x ^ p) s
theorem
differentiable.rpow_const
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{p : ℝ}
(hf : differentiable ℝ f)
(h : ∀ (x : E), f x ≠ 0 ∨ 1 ≤ p) :
differentiable ℝ (λ (x : E), f x ^ p)
theorem
has_fderiv_within_at.const_rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
{c : ℝ}
(hf : has_fderiv_within_at f f' s x)
(hc : 0 < c) :
theorem
has_fderiv_at.const_rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{c : ℝ}
(hf : has_fderiv_at f f' x)
(hc : 0 < c) :
theorem
has_strict_fderiv_at.const_rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{c : ℝ}
(hf : has_strict_fderiv_at f f' x)
(hc : 0 < c) :
theorem
cont_diff_within_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{x : E}
{s : set E}
{n : ℕ∞}
(hf : cont_diff_within_at ℝ n f s x)
(hg : cont_diff_within_at ℝ n g s x)
(h : f x ≠ 0) :
cont_diff_within_at ℝ n (λ (x : E), f x ^ g x) s x
theorem
cont_diff_at.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{x : E}
{n : ℕ∞}
(hf : cont_diff_at ℝ n f x)
(hg : cont_diff_at ℝ n g x)
(h : f x ≠ 0) :
cont_diff_at ℝ n (λ (x : E), f x ^ g x) x
theorem
cont_diff_on.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{s : set E}
{n : ℕ∞}
(hf : cont_diff_on ℝ n f s)
(hg : cont_diff_on ℝ n g s)
(h : ∀ (x : E), x ∈ s → f x ≠ 0) :
cont_diff_on ℝ n (λ (x : E), f x ^ g x) s
theorem
cont_diff.rpow
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f g : E → ℝ}
{n : ℕ∞}
(hf : cont_diff ℝ n f)
(hg : cont_diff ℝ n g)
(h : ∀ (x : E), f x ≠ 0) :
theorem
cont_diff_within_at.rpow_const_of_ne
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{p : ℝ}
{n : ℕ∞}
(hf : cont_diff_within_at ℝ n f s x)
(h : f x ≠ 0) :
cont_diff_within_at ℝ n (λ (x : E), f x ^ p) s x
theorem
cont_diff_at.rpow_const_of_ne
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{p : ℝ}
{n : ℕ∞}
(hf : cont_diff_at ℝ n f x)
(h : f x ≠ 0) :
cont_diff_at ℝ n (λ (x : E), f x ^ p) x
theorem
cont_diff_on.rpow_const_of_ne
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{p : ℝ}
{n : ℕ∞}
(hf : cont_diff_on ℝ n f s)
(h : ∀ (x : E), x ∈ s → f x ≠ 0) :
cont_diff_on ℝ n (λ (x : E), f x ^ p) s
theorem
cont_diff.rpow_const_of_ne
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{p : ℝ}
{n : ℕ∞}
(hf : cont_diff ℝ n f)
(h : ∀ (x : E), f x ≠ 0) :
theorem
cont_diff_within_at.rpow_const_of_le
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{p : ℝ}
{m : ℕ}
(hf : cont_diff_within_at ℝ ↑m f s x)
(h : ↑m ≤ p) :
cont_diff_within_at ℝ ↑m (λ (x : E), f x ^ p) s x
theorem
cont_diff_at.rpow_const_of_le
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{p : ℝ}
{m : ℕ}
(hf : cont_diff_at ℝ ↑m f x)
(h : ↑m ≤ p) :
cont_diff_at ℝ ↑m (λ (x : E), f x ^ p) x
theorem
cont_diff_on.rpow_const_of_le
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{p : ℝ}
{m : ℕ}
(hf : cont_diff_on ℝ ↑m f s)
(h : ↑m ≤ p) :
cont_diff_on ℝ ↑m (λ (x : E), f x ^ p) s
theorem
has_deriv_at.rpow
{f g : ℝ → ℝ}
{f' g' x : ℝ}
(hf : has_deriv_at f f' x)
(hg : has_deriv_at g g' x)
(h : 0 < f x) :
theorem
deriv_within_rpow_const
{f : ℝ → ℝ}
{x p : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hx : f x ≠ 0 ∨ 1 ≤ p)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), f x ^ p) s x = deriv_within f s x * p * f x ^ (p - 1)
theorem
tendsto_one_plus_div_rpow_exp
(t : ℝ) :
filter.tendsto (λ (x : ℝ), (1 + t / x) ^ x) filter.at_top (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 (λ (x : ℕ), (1 + t / ↑x) ^ x) filter.at_top (nhds (real.exp t))
The function (1 + t/x) ^ x
tends to exp t
at +∞
for naturals x
.