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
@[simp]
theorem
derivWithin_inv
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
(x_ne_zero : x ≠ 0)
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
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)
:
HasStrictFDerivAt (fun (x : 𝕜) => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) x
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
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)
:
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)
:
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)
:
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)
:
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 : ∀ x ∈ s, 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)
: