mathlib3 documentation

analysis.special_functions.pow.deriv

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
has_strict_fderiv_at (λ (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 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) :
has_fderiv_at (λ (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 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) :
has_fderiv_within_at (λ (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 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) :
has_strict_deriv_at (λ (x : ), f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * complex.log (f x) * g') x
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 complex.has_strict_deriv_at_cpow_const {x c : } (h : 0 < x.re x.im 0) :
has_strict_deriv_at (λ (z : ), z ^ c) (c * x ^ (c - 1)) x
theorem has_strict_deriv_at.cpow_const {f : } {f' x c : } (hf : has_strict_deriv_at f f' x) (h0 : 0 < (f x).re (f x).im 0) :
has_strict_deriv_at (λ (x : ), f x ^ c) (c * f x ^ (c - 1) * 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) :
has_deriv_at (λ (x : ), f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * complex.log (f x) * g') x
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_at.cpow_const {f : } {f' x c : } (hf : has_deriv_at f f' x) (h0 : 0 < (f x).re (f x).im 0) :
has_deriv_at (λ (x : ), f x ^ c) (c * f x ^ (c - 1) * 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) :
has_deriv_within_at (λ (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 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
theorem has_deriv_within_at.cpow_const {f : } {s : set } {f' x c : } (hf : has_deriv_within_at f f' s x) (h0 : 0 < (f x).re (f x).im 0) :
has_deriv_within_at (λ (x : ), f x ^ c) (c * f x ^ (c - 1) * f') s x
theorem has_deriv_at_of_real_cpow {x : } (hx : x 0) {r : } (hr : r -1) :
has_deriv_at (λ (y : ), y ^ (r + 1) / (r + 1)) (x ^ r) x

Although λ 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.

(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.cont_diff_at_rpow_of_ne (p : × ) (hp : p.fst 0) {n : ℕ∞} :
cont_diff_at n (λ (p : × ), p.fst ^ p.snd) p

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

theorem real.differentiable_at_rpow_of_ne (p : × ) (hp : p.fst 0) :
differentiable_at (λ (p : × ), p.fst ^ p.snd) p
theorem has_strict_deriv_at.rpow {x : } {f g : } {f' g' : } (hf : has_strict_deriv_at f f' x) (hg : has_strict_deriv_at g g' x) (h : 0 < f x) :
has_strict_deriv_at (λ (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.has_strict_deriv_at_rpow_const_of_ne {x : } (hx : x 0) (p : ) :
has_strict_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x
theorem real.has_strict_deriv_at_const_rpow {a : } (ha : 0 < a) (x : ) :
has_strict_deriv_at (λ (x : ), a ^ x) (a ^ x * real.log a) x
theorem real.has_strict_deriv_at_const_rpow_of_neg {a x : } (ha : a < 0) :
has_strict_deriv_at (λ (x : ), a ^ x) (a ^ x * real.log a - rexp (real.log a * x) * real.sin (x * real.pi) * real.pi) 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.has_deriv_at_rpow_const {x p : } (h : x 0 1 p) :
has_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x
theorem real.differentiable_rpow_const {p : } (hp : 1 p) :
differentiable (λ (x : ), x ^ p)
theorem real.deriv_rpow_const {x p : } (h : x 0 1 p) :
deriv (λ (x : ), x ^ p) x = p * x ^ (p - 1)
theorem real.deriv_rpow_const' {p : } (h : 1 p) :
deriv (λ (x : ), x ^ p) = λ (x : ), p * x ^ (p - 1)
theorem real.cont_diff_at_rpow_const_of_ne {x p : } {n : ℕ∞} (h : x 0) :
cont_diff_at n (λ (x : ), x ^ p) x
theorem real.cont_diff_rpow_const_of_le {p : } {n : } (h : n p) :
cont_diff n (λ (x : ), x ^ p)
theorem real.cont_diff_at_rpow_const_of_le {x p : } {n : } (h : n p) :
cont_diff_at n (λ (x : ), x ^ p) x
theorem real.cont_diff_at_rpow_const {x p : } {n : } (h : x 0 n p) :
cont_diff_at n (λ (x : ), x ^ p) x
theorem real.has_strict_deriv_at_rpow_const {x p : } (hx : x 0 1 p) :
has_strict_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) 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) :
has_fderiv_within_at (λ (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 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) :
has_fderiv_at (λ (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 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) :
has_strict_fderiv_at (λ (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 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) :
has_fderiv_within_at (λ (x : E), f x ^ p) ((p * f x ^ (p - 1)) f') s x
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) :
has_fderiv_at (λ (x : E), f x ^ p) ((p * f x ^ (p - 1)) f') x
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) :
has_strict_fderiv_at (λ (x : E), f x ^ p) ((p * f x ^ (p - 1)) f') x
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) :
has_fderiv_within_at (λ (x : E), c ^ f x) ((c ^ f x * real.log c) f') s x
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) :
has_fderiv_at (λ (x : E), c ^ f x) ((c ^ f x * real.log c) f') x
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) :
has_strict_fderiv_at (λ (x : E), c ^ f x) ((c ^ f x * real.log c) f') x
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) :
cont_diff n (λ (x : E), f x ^ g x)
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) :
cont_diff n (λ (x : E), f x ^ p)
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 cont_diff.rpow_const_of_le {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {p : } {m : } (hf : cont_diff m f) (h : m p) :
cont_diff m (λ (x : E), f x ^ p)
theorem has_deriv_within_at.rpow {f g : } {f' g' x : } {s : set } (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) (h : 0 < f x) :
has_deriv_within_at (λ (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 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) :
has_deriv_at (λ (x : ), f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * real.log (f x)) x
theorem has_deriv_within_at.rpow_const {f : } {f' x p : } {s : set } (hf : has_deriv_within_at f f' s x) (hx : f x 0 1 p) :
has_deriv_within_at (λ (y : ), f y ^ p) (f' * p * f x ^ (p - 1)) s x
theorem has_deriv_at.rpow_const {f : } {f' x p : } (hf : has_deriv_at f f' x) (hx : f x 0 1 p) :
has_deriv_at (λ (y : ), f y ^ p) (f' * p * f x ^ (p - 1)) 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)
@[simp]
theorem deriv_rpow_const {f : } {x p : } (hf : differentiable_at f x) (hx : f x 0 1 p) :
deriv (λ (x : ), f x ^ p) x = deriv f 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 (rexp 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 (rexp t))

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