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

source

theorem has_strict_deriv_at.has_strict_fderiv_at_equiv {𝕜 : Type u} [nontrivially_normed_field 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : has_strict_deriv_at f f' x) (hf' : f' ≠ 0) :

has_strict_fderiv_at f ↑(⇑(continuous_linear_equiv.units_equiv_aut 𝕜) (units.mk0 f' hf')) x

source

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) :

has_fderiv_at f ↑(⇑(continuous_linear_equiv.units_equiv_aut 𝕜) (units.mk0 f' hf')) x

source

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) :

has_strict_deriv_at g f'⁻¹ a

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.

source

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)) :

has_strict_deriv_at ⇑(f.symm) f'⁻¹ 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.

source

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) :

has_deriv_at g f'⁻¹ a

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.

source

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)) :

has_deriv_at ⇑(f.symm) f'⁻¹ 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.

source

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

source

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) :

filter.tendsto f (nhds_within x {x}ᶜ) (nhds_within (f x) {f x}ᶜ)

source

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) :

¬differentiable_within_at 𝕜 g s a

source

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) :

¬differentiable_at 𝕜 g a