Documentation

Mathlib.Analysis.Calculus.Deriv.Inv

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} [NontriviallyNormedField 𝕜] {x : 𝕜} (hx : x 0) :
HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
theorem hasDerivAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (x_ne_zero : x 0) :
HasDerivAt (fun (y : 𝕜) => y⁻¹) (-(x ^ 2)⁻¹) x
theorem hasDerivWithinAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (x_ne_zero : x 0) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => x⁻¹) (-(x ^ 2)⁻¹) s x
theorem differentiableAt_inv_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => x⁻¹) x x 0
theorem deriv_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} :
deriv (fun (x : 𝕜) => x⁻¹) x = -(x ^ 2)⁻¹
@[simp]
theorem deriv_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] :
(deriv fun (x : 𝕜) => x⁻¹) = fun (x : 𝕜) => -(x ^ 2)⁻¹
theorem derivWithin_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (x : 𝕜) => x⁻¹) s x = -(x ^ 2)⁻¹
theorem hasFDerivAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (x_ne_zero : x 0) :
HasFDerivAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) x
theorem hasStrictFDerivAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (x_ne_zero : x 0) :
theorem hasFDerivWithinAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) :
HasFDerivWithinAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) s x
theorem fderiv_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} :
fderiv 𝕜 (fun (x : 𝕜) => x⁻¹) x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
theorem fderivWithin_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun (x : 𝕜) => x⁻¹) s x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
theorem HasDerivWithinAt.inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {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} [NontriviallyNormedField 𝕜] {x : 𝕜} {c : 𝕜𝕜} {c' : 𝕜} (hc : HasDerivAt c c' x) (hx : c x 0) :
HasDerivAt (fun (y : 𝕜) => (c y)⁻¹) (-c' / c x ^ 2) x
theorem derivWithin_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {c : 𝕜𝕜} (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (x : 𝕜) => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2
@[simp]
theorem deriv_inv'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {c : 𝕜𝕜} (hc : DifferentiableAt 𝕜 c x) (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} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {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} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {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} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {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} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hx : d x 0) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => c x / d x) s x
@[simp]
theorem DifferentiableAt.div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) (hx : d x 0) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => c x / d x) x
theorem DifferentiableOn.div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) (hx : xs, d x 0) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => c x / d x) s
@[simp]
theorem Differentiable.div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) (hx : ∀ (x : 𝕜), d x 0) :
Differentiable 𝕜 fun (x : 𝕜) => c x / d x
theorem derivWithin_div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hx : d x 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
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} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {d : 𝕜𝕜'} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) (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