analysis.special_functions.pow.deriv

theorem complex.has_strict_fderiv_at_cpow {p : ℂ × ℂ} (hp : 0 < p.fst.re ∨ p.fst.im ≠ 0) :

has_strict_fderiv_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) ((p.snd * p.fst ^ (p.snd - 1)) • continuous_linear_map.fst ℂ ℂ ℂ + (p.fst ^ p.snd * complex.log p.fst) • continuous_linear_map.snd ℂ ℂ ℂ) p

source

theorem complex.has_strict_fderiv_at_cpow' {x y : ℂ} (hp : 0 < x.re ∨ x.im ≠ 0) :

has_strict_fderiv_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) ((y * x ^ (y - 1)) • continuous_linear_map.fst ℂ ℂ ℂ + (x ^ y * complex.log x) • continuous_linear_map.snd ℂ ℂ ℂ) (x, y)

source

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

source

theorem complex.has_fderiv_at_cpow {p : ℂ × ℂ} (hp : 0 < p.fst.re ∨ p.fst.im ≠ 0) :

has_fderiv_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) ((p.snd * p.fst ^ (p.snd - 1)) • continuous_linear_map.fst ℂ ℂ ℂ + (p.fst ^ p.snd * complex.log p.fst) • continuous_linear_map.snd ℂ ℂ ℂ) p

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

theorem real.has_strict_fderiv_at_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.fst) :

has_strict_fderiv_at (λ (x : ℝ × ℝ), x.fst ^ x.snd) ((p.snd * p.fst ^ (p.snd - 1)) • continuous_linear_map.fst ℝ ℝ ℝ + (p.fst ^ p.snd * real.log p.fst) • continuous_linear_map.snd ℝ ℝ ℝ) p

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

source

theorem real.has_strict_fderiv_at_rpow_of_neg (p : ℝ × ℝ) (hp : p.fst < 0) :

has_strict_fderiv_at (λ (x : ℝ × ℝ), x.fst ^ x.snd) ((p.snd * p.fst ^ (p.snd - 1)) • continuous_linear_map.fst ℝ ℝ ℝ + (p.fst ^ p.snd * real.log p.fst - rexp (real.log p.fst * p.snd) * real.sin (p.snd * real.pi) * real.pi) • continuous_linear_map.snd ℝ ℝ ℝ) p

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

source

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.

source

theorem real.differentiable_at_rpow_of_ne (p : ℝ × ℝ) (hp : p.fst ≠ 0) :

differentiable_at ℝ (λ (p : ℝ × ℝ), p.fst ^ p.snd) p

source

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

source

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

source

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

source

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.

source

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

source

theorem real.differentiable_rpow_const {p : ℝ} (hp : 1 ≤ p) :

differentiable ℝ (λ (x : ℝ), x ^ p)

source

theorem real.deriv_rpow_const {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) :

deriv (λ (x : ℝ), x ^ p) x = p * x ^ (p - 1)

source

theorem real.deriv_rpow_const' {p : ℝ} (h : 1 ≤ p) :

deriv (λ (x : ℝ), x ^ p) = λ (x : ℝ), p * x ^ (p - 1)

source

theorem real.cont_diff_at_rpow_const_of_ne {x p : ℝ} {n : ℕ∞} (h : x ≠ 0) :

cont_diff_at ℝ n (λ (x : ℝ), x ^ p) x

source

theorem real.cont_diff_rpow_const_of_le {p : ℝ} {n : ℕ} (h : ↑n ≤ p) :

cont_diff ℝ ↑n (λ (x : ℝ), x ^ p)

source

theorem real.cont_diff_at_rpow_const_of_le {x p : ℝ} {n : ℕ} (h : ↑n ≤ p) :

cont_diff_at ℝ ↑n (λ (x : ℝ), x ^ p) x

source

theorem real.cont_diff_at_rpow_const {x p : ℝ} {n : ℕ} (h : x ≠ 0 ∨ ↑n ≤ p) :

cont_diff_at ℝ ↑n (λ (x : ℝ), x ^ p) x

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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

source

@[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

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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

source

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)

source

@[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)

source

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 +∞.

source

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.

mathlib3 documentation

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

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

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