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

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 hasStrictDerivAt_inv {𝕜 : Type u} {x : 𝕜} (hx : x 0) :
HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
theorem hasDerivAt_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) :
HasDerivAt (fun (y : 𝕜) => y⁻¹) (-(x ^ 2)⁻¹) x
theorem hasDerivWithinAt_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => x⁻¹) (-(x ^ 2)⁻¹) s x
theorem differentiableAt_inv {𝕜 : Type u} {x : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => x⁻¹) x x 0
theorem differentiableWithinAt_inv {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => x⁻¹) s x
theorem differentiableOn_inv {𝕜 : Type u} :
DifferentiableOn 𝕜 (fun (x : 𝕜) => x⁻¹) {x : 𝕜 | x 0}
theorem deriv_inv {𝕜 : Type u} {x : 𝕜} :
deriv (fun (x : 𝕜) => x⁻¹) x = -(x ^ 2)⁻¹
@[simp]
theorem deriv_inv' {𝕜 : Type u} :
(deriv fun (x : 𝕜) => x⁻¹) = fun (x : 𝕜) => -(x ^ 2)⁻¹
theorem derivWithin_inv {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) (hxs : ) :
derivWithin (fun (x : 𝕜) => x⁻¹) s x = -(x ^ 2)⁻¹
theorem hasFDerivAt_inv {𝕜 : Type u} {x : 𝕜} (x_ne_zero : x 0) :
HasFDerivAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) x
theorem hasFDerivWithinAt_inv {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) :
HasFDerivWithinAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) s x
theorem fderiv_inv {𝕜 : Type u} {x : 𝕜} :
fderiv 𝕜 (fun (x : 𝕜) => x⁻¹) x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
theorem fderivWithin_inv {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) (hxs : ) :
fderivWithin 𝕜 (fun (x : 𝕜) => x⁻¹) s x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
theorem HasDerivWithinAt.inv {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {c : 𝕜𝕜} {c' : 𝕜} (hc : HasDerivWithinAt c c' s x) (hx : c x 0) :
HasDerivWithinAt (fun (y : 𝕜) => (c y)⁻¹) (-c' / c x ^ 2) s x
theorem HasDerivAt.inv {𝕜 : Type u} {x : 𝕜} {c : 𝕜𝕜} {c' : 𝕜} (hc : HasDerivAt c c' x) (hx : c x 0) :
HasDerivAt (fun (y : 𝕜) => (c y)⁻¹) (-c' / c x ^ 2) x
theorem DifferentiableWithinAt.inv {𝕜 : Type u} {E : Type w} [] {h : E𝕜} {z : E} {S : Set E} (hf : ) (hz : h z 0) :
DifferentiableWithinAt 𝕜 (fun (x : E) => (h x)⁻¹) S z
@[simp]
theorem DifferentiableAt.inv {𝕜 : Type u} {E : Type w} [] {h : E𝕜} {z : E} (hf : ) (hz : h z 0) :
DifferentiableAt 𝕜 (fun (x : E) => (h x)⁻¹) z
theorem DifferentiableOn.inv {𝕜 : Type u} {E : Type w} [] {h : E𝕜} {S : Set E} (hf : ) (hz : xS, h x 0) :
DifferentiableOn 𝕜 (fun (x : E) => (h x)⁻¹) S
@[simp]
theorem Differentiable.inv {𝕜 : Type u} {E : Type w} [] {h : E𝕜} (hf : ) (hz : ∀ (x : E), h x 0) :
Differentiable 𝕜 fun (x : E) => (h x)⁻¹
theorem derivWithin_inv' {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {c : 𝕜𝕜} (hc : ) (hx : c x 0) (hxs : ) :
derivWithin (fun (x : 𝕜) => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2
@[simp]
theorem deriv_inv'' {𝕜 : Type u} {x : 𝕜} {c : 𝕜𝕜} (hc : ) (hx : c x 0) :
deriv (fun (x : 𝕜) => (c x)⁻¹) x = -deriv c x / c x ^ 2

### Derivative of x ↦ c x / d x#

theorem HasDerivWithinAt.div {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} {c' : 𝕜'} {d' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) (hx : d x 0) :
HasDerivWithinAt (fun (y : 𝕜) => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
theorem HasStrictDerivAt.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} {c' : 𝕜'} {d' : 𝕜'} (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) (hx : d x 0) :
HasStrictDerivAt (fun (y : 𝕜) => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
theorem HasDerivAt.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} {c' : 𝕜'} {d' : 𝕜'} (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) (hx : d x 0) :
HasDerivAt (fun (y : 𝕜) => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
theorem DifferentiableWithinAt.div {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : d x 0) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => c x / d x) s x
@[simp]
theorem DifferentiableAt.div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : d x 0) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => c x / d x) x
theorem DifferentiableOn.div {𝕜 : Type u} {s : Set 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : xs, d x 0) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => c x / d x) s
@[simp]
theorem Differentiable.div {𝕜 : Type u} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : ∀ (x : 𝕜), d x 0) :
Differentiable 𝕜 fun (x : 𝕜) => c x / d x
theorem derivWithin_div {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : d x 0) (hxs : ) :
derivWithin (fun (x : 𝕜) => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2
@[simp]
theorem deriv_div {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : ) (hd : ) (hx : d x 0) :
deriv (fun (x : 𝕜) => c x / d x) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2