mathlib3 documentation

analysis.calculus.deriv.inverse

Inverse function theorem - the easy half #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that g' (f x) = (f' x)⁻¹ provided that f is strictly differentiable at x, f' x ≠ 0, and g is a local left inverse of f that is continuous at f x. This is the easy half of the inverse function theorem: the harder half states that g exists.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

Keywords #

derivative, inverse function

theorem has_deriv_at.has_fderiv_at_equiv {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f : 𝕜 𝕜} {f' x : 𝕜} (hf : has_deriv_at f f' x) (hf' : f' 0) :
theorem has_strict_deriv_at.of_local_left_inverse {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f g : 𝕜 𝕜} {f' a : 𝕜} (hg : continuous_at g a) (hf : has_strict_deriv_at f f' (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem local_homeomorph.has_strict_deriv_at_symm {𝕜 : Type u} [nontrivially_normed_field 𝕜] (f : local_homeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a f.to_local_equiv.target) (hf' : f' 0) (htff' : has_strict_deriv_at f f' ((f.symm) a)) :

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a in the strict sense, then f.symm has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem has_deriv_at.of_local_left_inverse {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f g : 𝕜 𝕜} {f' a : 𝕜} (hg : continuous_at g a) (hf : has_deriv_at f f' (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a, then g has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem local_homeomorph.has_deriv_at_symm {𝕜 : Type u} [nontrivially_normed_field 𝕜] (f : local_homeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a f.to_local_equiv.target) (hf' : f' 0) (htff' : has_deriv_at f f' ((f.symm) a)) :

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has an nonzero derivative f' at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem has_deriv_at.eventually_ne {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : has_deriv_at f f' x) (hf' : f' 0) :
∀ᶠ (z : 𝕜) in nhds_within x {x}, f z f x
theorem has_deriv_at.tendsto_punctured_nhds {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f : 𝕜 F} {f' : F} {x : 𝕜} (h : has_deriv_at f f' x) (hf' : f' 0) :
theorem not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f g : 𝕜 𝕜} {a : 𝕜} {s t : set 𝕜} (ha : a s) (hsu : unique_diff_within_at 𝕜 s a) (hf : has_deriv_within_at f 0 t (g a)) (hst : set.maps_to g s t) (hfg : f g =ᶠ[nhds_within a s] id) :
theorem not_differentiable_at_of_local_left_inverse_has_deriv_at_zero {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f g : 𝕜 𝕜} {a : 𝕜} (hf : has_deriv_at f 0 (g a)) (hfg : f g =ᶠ[nhds a] id) :