mathlib3documentation

analysis.calculus.deriv.inv

Derivatives of x ↦ x⁻¹ and f x / g x#

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

In this file we prove (x⁻¹)' = -1 / x ^ 2, ((f x)⁻¹)' = -f' x / (f x) ^ 2, and (f x / g x)' = (f' x * g x - f x * g' x) / (g x) ^ 2 for different notions of derivative.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

Keywords #

derivative

Derivative of x ↦ x⁻¹#

theorem has_strict_deriv_at_inv {𝕜 : Type u} {x : 𝕜} (hx : x 0) :
(-(x ^ 2)⁻¹) x
theorem has_deriv_at_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) :
has_deriv_at (λ (y : 𝕜), y⁻¹) (-(x ^ 2)⁻¹) x
theorem has_deriv_within_at_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x⁻¹) (-(x ^ 2)⁻¹) s x
theorem differentiable_at_inv {𝕜 : Type u} {x : 𝕜} :
(λ (x : 𝕜), x⁻¹) x x 0
theorem differentiable_within_at_inv {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (x_ne_zero : x 0) :
(λ (x : 𝕜), x⁻¹) s x
theorem differentiable_on_inv {𝕜 : Type u}  :
(λ (x : 𝕜), x⁻¹) {x : 𝕜 | x 0}
theorem deriv_inv {𝕜 : Type u} {x : 𝕜} :
deriv (λ (x : 𝕜), x⁻¹) x = -(x ^ 2)⁻¹
@[simp]
theorem deriv_inv' {𝕜 : Type u}  :
deriv (λ (x : 𝕜), x⁻¹) = λ (x : 𝕜), -(x ^ 2)⁻¹
theorem deriv_within_inv {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (x_ne_zero : x 0) (hxs : x) :
deriv_within (λ (x : 𝕜), x⁻¹) s x = -(x ^ 2)⁻¹
theorem has_fderiv_at_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) :
has_fderiv_at (λ (x : 𝕜), x⁻¹) (1.smul_right (-(x ^ 2)⁻¹)) x
theorem has_fderiv_within_at_inv {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (x_ne_zero : x 0) :
has_fderiv_within_at (λ (x : 𝕜), x⁻¹) (1.smul_right (-(x ^ 2)⁻¹)) s x
theorem fderiv_inv {𝕜 : Type u} {x : 𝕜} :
(λ (x : 𝕜), x⁻¹) x = 1.smul_right (-(x ^ 2)⁻¹)
theorem fderiv_within_inv {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (x_ne_zero : x 0) (hxs : x) :
(λ (x : 𝕜), x⁻¹) s x = 1.smul_right (-(x ^ 2)⁻¹)
theorem has_deriv_within_at.inv {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (hc : s x) (hx : c x 0) :
has_deriv_within_at (λ (y : 𝕜), (c y)⁻¹) (-c' / c x ^ 2) s x
theorem has_deriv_at.inv {𝕜 : Type u} {x : 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (hc : c' x) (hx : c x 0) :
has_deriv_at (λ (y : 𝕜), (c y)⁻¹) (-c' / c x ^ 2) x
theorem differentiable_within_at.inv {𝕜 : Type u} {E : Type w} [ E] {h : E 𝕜} {z : E} {S : set E} (hf : z) (hz : h z 0) :
(λ (x : E), (h x)⁻¹) S z
@[simp]
theorem differentiable_at.inv {𝕜 : Type u} {E : Type w} [ E] {h : E 𝕜} {z : E} (hf : z) (hz : h z 0) :
(λ (x : E), (h x)⁻¹) z
theorem differentiable_on.inv {𝕜 : Type u} {E : Type w} [ E] {h : E 𝕜} {S : set E} (hf : S) (hz : (x : E), x S h x 0) :
(λ (x : E), (h x)⁻¹) S
@[simp]
theorem differentiable.inv {𝕜 : Type u} {E : Type w} [ E] {h : E 𝕜} (hf : h) (hz : (x : E), h x 0) :
(λ (x : E), (h x)⁻¹)
theorem deriv_within_inv' {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} (hc : x) (hx : c x 0) (hxs : x) :
deriv_within (λ (x : 𝕜), (c x)⁻¹) s x = - s x / c x ^ 2
@[simp]
theorem deriv_inv'' {𝕜 : Type u} {x : 𝕜} {c : 𝕜 𝕜} (hc : x) (hx : c x 0) :
deriv (λ (x : 𝕜), (c x)⁻¹) x = - x / c x ^ 2

Derivative of x ↦ c x / d x#

theorem has_deriv_within_at.div {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} {c' d' : 𝕜'} (hc : s x) (hd : s x) (hx : d x 0) :
has_deriv_within_at (λ (y : 𝕜), c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
theorem has_strict_deriv_at.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} {c' d' : 𝕜'} (hc : x) (hd : x) (hx : d x 0) :
has_strict_deriv_at (λ (y : 𝕜), c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
theorem has_deriv_at.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} {c' d' : 𝕜'} (hc : c' x) (hd : d' x) (hx : d x 0) :
has_deriv_at (λ (y : 𝕜), c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
theorem differentiable_within_at.div {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : x) (hd : x) (hx : d x 0) :
(λ (x : 𝕜), c x / d x) s x
@[simp]
theorem differentiable_at.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : x) (hd : x) (hx : d x 0) :
(λ (x : 𝕜), c x / d x) x
theorem differentiable_on.div {𝕜 : Type u} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : s) (hd : s) (hx : (x : 𝕜), x s d x 0) :
(λ (x : 𝕜), c x / d x) s
@[simp]
theorem differentiable.div {𝕜 : Type u} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : c) (hd : d) (hx : (x : 𝕜), d x 0) :
(λ (x : 𝕜), c x / d x)
theorem deriv_within_div {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : x) (hd : x) (hx : d x 0) (hxs : x) :
deriv_within (λ (x : 𝕜), c x / d x) s x = s x * d x - c x * s x) / d x ^ 2
@[simp]
theorem deriv_div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c d : 𝕜 𝕜'} (hc : x) (hd : x) (hx : d x 0) :
deriv (λ (x : 𝕜), c x / d x) x = (deriv c x * d x - c x * x) / d x ^ 2