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.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) x

theorem hasStrictFDerivAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (x_ne_zero : x ≠ 0) : HasStrictFDerivAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) x

theorem hasFDerivWithinAt_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (x_ne_zero : x ≠ 0) : HasFDerivWithinAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) s x

theorem fderiv_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} : fderiv 𝕜 (fun (x : 𝕜) => x⁻¹) x = ContinuousLinearMap.toSpanSingleton 𝕜 (-(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.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)

theorem HasDerivWithinAt.inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) : HasDerivWithinAt c⁻¹ (-c' / c x ^ 2) s x

theorem HasDerivWithinAt.fun_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (hx : c x ≠ 0) : HasDerivWithinAt (fun (i : 𝕜) => (c i)⁻¹) (-c' / c x ^ 2) s x

Eta-expanded form of HasDerivWithinAt.inv

theorem HasDerivAt.inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'} (hc : HasDerivAt c c' x) (hx : c x ≠ 0) : HasDerivAt c⁻¹ (-c' / c x ^ 2) x

theorem HasDerivAt.fun_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'} (hc : HasDerivAt c c' x) (hx : c x ≠ 0) : HasDerivAt (fun (i : 𝕜) => (c i)⁻¹) (-c' / c x ^ 2) x

Eta-expanded form of HasDerivAt.inv

theorem derivWithin_fun_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0) : derivWithin (fun (x : 𝕜) => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

theorem derivWithin_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0) : derivWithin c⁻¹ s x = -derivWithin c s x / c x ^ 2

@[simp]

theorem deriv_fun_inv'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (hx : c x ≠ 0) : deriv (fun (x : 𝕜) => (c x)⁻¹) x = -deriv c x / c x ^ 2

@[simp]

theorem deriv_inv'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (hx : c x ≠ 0) : deriv c⁻¹ x = -deriv c x / c x ^ 2

Derivative of x ↦ c x / d x

theorem HasDerivWithinAt.fun_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 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 (c / d) ((c' * d x - c x * d') / d x ^ 2) s x

theorem HasStrictDerivAt.fun_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 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 (c / d) ((c' * d x - c x * d') / d x ^ 2) x

theorem HasDerivAt.fun_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 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 (c / d) ((c' * d x - c x * d') / d x ^ 2) x

theorem DifferentiableWithinAt.fun_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

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 𝕜 (c / d) 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 𝕜 (c / d) x

@[simp]

theorem DifferentiableAt.fun_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 (i : 𝕜) => c i / d i) x

Eta-expanded form of DifferentiableAt.div

theorem DifferentiableOn.div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) (hx : ∀ x ∈ s, d x ≠ 0) : DifferentiableOn 𝕜 (c / d) s

theorem DifferentiableOn.fun_div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) (hx : ∀ x ∈ s, d x ≠ 0) : DifferentiableOn 𝕜 (fun (i : 𝕜) => c i / d i) s

Eta-expanded form of DifferentiableOn.div

@[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 𝕜 (c / d)

@[simp]

theorem Differentiable.fun_div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) (hx : ∀ (x : 𝕜), d x ≠ 0) : Differentiable 𝕜 fun (i : 𝕜) => c i / d i

Eta-expanded form of Differentiable.div

theorem derivWithin_fun_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) : derivWithin (fun (x : 𝕜) => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

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) : derivWithin (c / d) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

@[simp]

theorem deriv_fun_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

@[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 (c / d) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2

theorem deriv_const_div {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {d : 𝕜 → 𝕜'} (c : 𝕜') (hd : DifferentiableAt 𝕜 d x) (hx : d x ≠ 0) : deriv (fun (x : 𝕜) => c / d x) x = -c * deriv d x / d x ^ 2

@[simp]

theorem deriv_const_div_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜) : deriv (fun (x : 𝕜) => c / x) x = -c / x ^ 2