Documentation

Mathlib.Analysis.Calculus.Deriv.Inverse

Inverse function theorem - the easy half #

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 HasStrictDerivAt.hasStrictFDerivAt_equiv {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {x : ๐•œ} (hf : HasStrictDerivAt f f' x) (hf' : f' โ‰  0) :
theorem HasDerivAt.hasFDerivAt_equiv {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {x : ๐•œ} (hf : HasDerivAt f f' x) (hf' : f' โ‰  0) :
HasFDerivAt f (โ†‘((ContinuousLinearEquiv.unitsEquivAut ๐•œ) (Units.mk0 f' hf'))) x
theorem HasStrictDerivAt.of_local_left_inverse {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {g : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {a : ๐•œ} (hg : ContinuousAt g a) (hf : HasStrictDerivAt 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 PartialHomeomorph.hasStrictDerivAt_symm {๐•œ : Type u} [NontriviallyNormedField ๐•œ] (f : PartialHomeomorph ๐•œ ๐•œ) {a : ๐•œ} {f' : ๐•œ} (ha : a โˆˆ f.target) (hf' : f' โ‰  0) (htff' : HasStrictDerivAt (โ†‘f) f' (โ†‘f.symm a)) :
HasStrictDerivAt (โ†‘f.symm) f'โปยน a

If f is a partial 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 HasDerivAt.of_local_left_inverse {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {g : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {a : ๐•œ} (hg : ContinuousAt g a) (hf : HasDerivAt 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 PartialHomeomorph.hasDerivAt_symm {๐•œ : Type u} [NontriviallyNormedField ๐•œ] (f : PartialHomeomorph ๐•œ ๐•œ) {a : ๐•œ} {f' : ๐•œ} (ha : a โˆˆ f.target) (hf' : f' โ‰  0) (htff' : HasDerivAt (โ†‘f) f' (โ†‘f.symm a)) :
HasDerivAt (โ†‘f.symm) f'โปยน a

If f is a partial homeomorphism defined on a neighbourhood of f.symm a, and f has a 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 HasDerivAt.eventually_ne {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : ๐•œ โ†’ F} {f' : F} {x : ๐•œ} (h : HasDerivAt f f' x) (hf' : f' โ‰  0) :
โˆ€แถ  (z : ๐•œ) in nhdsWithin x {x}แถœ, f z โ‰  f x
theorem HasDerivAt.tendsto_punctured_nhds {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : ๐•œ โ†’ F} {f' : F} {x : ๐•œ} (h : HasDerivAt f f' x) (hf' : f' โ‰  0) :
theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {g : ๐•œ โ†’ ๐•œ} {a : ๐•œ} {s : Set ๐•œ} {t : Set ๐•œ} (ha : a โˆˆ s) (hsu : UniqueDiffWithinAt ๐•œ s a) (hf : HasDerivWithinAt f 0 t (g a)) (hst : Set.MapsTo g s t) (hfg : f โˆ˜ g =แถ [nhdsWithin a s] id) :
theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {g : ๐•œ โ†’ ๐•œ} {a : ๐•œ} (hf : HasDerivAt f 0 (g a)) (hfg : f โˆ˜ g =แถ [nhds a] id) :