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}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(hx : x ≠ 0) :
has_strict_deriv_at has_inv.inv (-(x ^ 2)⁻¹) x
theorem
has_deriv_at_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(x_ne_zero : x ≠ 0) :
has_deriv_at (λ (y : 𝕜), y⁻¹) (-(x ^ 2)⁻¹) x
theorem
has_deriv_within_at_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(x_ne_zero : x ≠ 0)
(s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x⁻¹) (-(x ^ 2)⁻¹) s x
theorem
differentiable_at_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜} :
differentiable_at 𝕜 (λ (x : 𝕜), x⁻¹) x ↔ x ≠ 0
theorem
differentiable_within_at_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(x_ne_zero : x ≠ 0) :
differentiable_within_at 𝕜 (λ (x : 𝕜), x⁻¹) s x
theorem
differentiable_on_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜] :
differentiable_on 𝕜 (λ (x : 𝕜), x⁻¹) {x : 𝕜 | x ≠ 0}
@[simp]
theorem
deriv_within_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(x_ne_zero : x ≠ 0)
(hxs : unique_diff_within_at 𝕜 s x) :
theorem
has_fderiv_at_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{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}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(x_ne_zero : x ≠ 0) :
has_fderiv_within_at (λ (x : 𝕜), x⁻¹) (1.smul_right (-(x ^ 2)⁻¹)) s x
theorem
fderiv_within_inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(x_ne_zero : x ≠ 0)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (x : 𝕜), x⁻¹) s x = 1.smul_right (-(x ^ 2)⁻¹)
theorem
has_deriv_within_at.inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(hc : has_deriv_within_at c c' 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}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(hc : has_deriv_at c c' x)
(hx : c x ≠ 0) :
has_deriv_at (λ (y : 𝕜), (c y)⁻¹) (-c' / c x ^ 2) x
theorem
differentiable_within_at.inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{h : E → 𝕜}
{z : E}
{S : set E}
(hf : differentiable_within_at 𝕜 h S z)
(hz : h z ≠ 0) :
differentiable_within_at 𝕜 (λ (x : E), (h x)⁻¹) S z
@[simp]
theorem
differentiable_at.inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{h : E → 𝕜}
{z : E}
(hf : differentiable_at 𝕜 h z)
(hz : h z ≠ 0) :
differentiable_at 𝕜 (λ (x : E), (h x)⁻¹) z
theorem
differentiable_on.inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{h : E → 𝕜}
{S : set E}
(hf : differentiable_on 𝕜 h S)
(hz : ∀ (x : E), x ∈ S → h x ≠ 0) :
differentiable_on 𝕜 (λ (x : E), (h x)⁻¹) S
@[simp]
theorem
differentiable.inv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{h : E → 𝕜}
(hf : differentiable 𝕜 h)
(hz : ∀ (x : E), h x ≠ 0) :
differentiable 𝕜 (λ (x : E), (h x)⁻¹)
theorem
deriv_within_inv'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{c : 𝕜 → 𝕜}
(hc : differentiable_within_at 𝕜 c s x)
(hx : c x ≠ 0)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), (c x)⁻¹) s x = -deriv_within c s x / c x ^ 2
@[simp]
theorem
deriv_inv''
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
(hc : differentiable_at 𝕜 c x)
(hx : c x ≠ 0) :
Derivative of x ↦ c x / d x #
theorem
has_deriv_within_at.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
{c' d' : 𝕜'}
(hc : has_deriv_within_at c c' s x)
(hd : has_deriv_within_at d d' s x)
(hx : d x ≠ 0) :
theorem
has_strict_deriv_at.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
{c' d' : 𝕜'}
(hc : has_strict_deriv_at c c' x)
(hd : has_strict_deriv_at d d' x)
(hx : d x ≠ 0) :
theorem
has_deriv_at.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
{c' d' : 𝕜'}
(hc : has_deriv_at c c' x)
(hd : has_deriv_at d d' x)
(hx : d x ≠ 0) :
theorem
differentiable_within_at.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x)
(hx : d x ≠ 0) :
differentiable_within_at 𝕜 (λ (x : 𝕜), c x / d x) s x
@[simp]
theorem
differentiable_at.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x)
(hx : d x ≠ 0) :
differentiable_at 𝕜 (λ (x : 𝕜), c x / d x) x
theorem
differentiable_on.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable_on 𝕜 c s)
(hd : differentiable_on 𝕜 d s)
(hx : ∀ (x : 𝕜), x ∈ s → d x ≠ 0) :
differentiable_on 𝕜 (λ (x : 𝕜), c x / d x) s
@[simp]
theorem
differentiable.div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable 𝕜 c)
(hd : differentiable 𝕜 d)
(hx : ∀ (x : 𝕜), d x ≠ 0) :
differentiable 𝕜 (λ (x : 𝕜), c x / d x)
theorem
deriv_within_div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x)
(hx : d x ≠ 0)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), c x / d x) s x = (deriv_within c s x * d x - c x * deriv_within d s x) / d x ^ 2
@[simp]
theorem
deriv_div
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c d : 𝕜 → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x)
(hx : d x ≠ 0) :