Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

Inverse function theorem #

In this file we prove the inverse function theorem. It says that if a map f : E โ†’ F has an invertible strict derivative f' at a, then it is locally invertible, and the inverse function has derivative f' โปยน.

We define HasStrictFDerivAt.toPartialHomeomorph that repacks a function f with a hf : HasStrictFDerivAt f f' a, f' : E โ‰ƒL[๐•œ] F, into a PartialHomeomorph. The toFun of this PartialHomeomorph is defeq to f, so one can apply theorems about PartialHomeomorph to hf.toPartialHomeomorph f, and get statements about f.

Then we define HasStrictFDerivAt.localInverse to be the invFun of this PartialHomeomorph, and prove two versions of the inverse function theorem:

Some related theorems, providing the derivative and higher regularity assuming that we already know the inverse function, are formulated in the Analysis/Calculus/FDeriv and Analysis/Calculus/Deriv folders, and in ContDiff.lean.

Tags #

derivative, strictly differentiable, continuously differentiable, smooth, inverse function

Inverse function theorem #

Let f : E โ†’ F be a map defined on a complete vector space E. Assume that f has an invertible derivative f' : E โ‰ƒL[๐•œ] F at a : E in the strict sense. Then f approximates f' in the sense of ApproximatesLinearOn on an open neighborhood of a, and we can apply ApproximatesLinearOn.toPartialHomeomorph to construct the inverse function.

theorem HasStrictFDerivAt.approximates_deriv_on_nhds {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {f' : E โ†’L[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f f' a) {c : NNReal} (hc : Subsingleton E โˆจ 0 < c) :
โˆƒ s โˆˆ nhds a, ApproximatesLinearOn f f' s c

If f has derivative f' at a in the strict sense and c > 0, then f approximates f' with constant c on some neighborhood of a.

theorem HasStrictFDerivAt.map_nhds_eq_of_surj {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] [CompleteSpace F] {f : E โ†’ F} {f' : E โ†’L[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f f' a) (h : LinearMap.range f' = โŠค) :
Filter.map f (nhds a) = nhds (f a)
theorem HasStrictFDerivAt.approximates_deriv_on_open_nhds {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
โˆƒ (s : Set E), a โˆˆ s โˆง IsOpen s โˆง ApproximatesLinearOn f (โ†‘f') s (โ€–โ†‘f'.symmโ€–โ‚Šโปยน / 2)
def HasStrictFDerivAt.toPartialHomeomorph {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] (f : E โ†’ F) {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :

Given a function with an invertible strict derivative at a, returns a PartialHomeomorph with to_fun = f and a โˆˆ source. This is a part of the inverse function theorem. The other part HasStrictFDerivAt.to_localInverse states that the inverse function of this PartialHomeomorph has derivative f'.symm.

Equations
Instances For
    @[simp]
    theorem HasStrictFDerivAt.toPartialHomeomorph_coe {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
    theorem HasStrictFDerivAt.mem_toPartialHomeomorph_source {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
    theorem HasStrictFDerivAt.image_mem_toPartialHomeomorph_target {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
    theorem HasStrictFDerivAt.map_nhds_eq_of_equiv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
    Filter.map f (nhds a) = nhds (f a)
    def HasStrictFDerivAt.localInverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] (f : E โ†’ F) (f' : E โ‰ƒL[๐•œ] F) (a : E) (hf : HasStrictFDerivAt f (โ†‘f') a) :
    F โ†’ E

    Given a function f with an invertible derivative, returns a function that is locally inverse to f.

    Equations
    Instances For
      theorem HasStrictFDerivAt.localInverse_def {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      theorem HasStrictFDerivAt.eventually_left_inverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      โˆ€แถ  (x : E) in nhds a, HasStrictFDerivAt.localInverse f f' a hf (f x) = x
      @[simp]
      theorem HasStrictFDerivAt.localInverse_apply_image {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      theorem HasStrictFDerivAt.eventually_right_inverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      โˆ€แถ  (y : F) in nhds (f a), f (HasStrictFDerivAt.localInverse f f' a hf y) = y
      theorem HasStrictFDerivAt.localInverse_continuousAt {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      theorem HasStrictFDerivAt.localInverse_tendsto {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      theorem HasStrictFDerivAt.localInverse_unique {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) {g : F โ†’ E} (hg : โˆ€แถ  (x : E) in nhds a, g (f x) = x) :
      โˆ€แถ  (y : F) in nhds (f a), g y = HasStrictFDerivAt.localInverse f f' a hf y
      theorem HasStrictFDerivAt.to_localInverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) :
      HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (โ†‘f'.symm) (f a)

      If f has an invertible derivative f' at a in the sense of strict differentiability (hf), then the inverse function hf.localInverse f has derivative f'.symm at f a.

      theorem HasStrictFDerivAt.to_local_left_inverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ‰ƒL[๐•œ] F} {a : E} (hf : HasStrictFDerivAt f (โ†‘f') a) {g : F โ†’ E} (hg : โˆ€แถ  (x : E) in nhds a, g (f x) = x) :
      HasStrictFDerivAt g (โ†‘f'.symm) (f a)

      If f : E โ†’ F has an invertible derivative f' at a in the sense of strict differentiability and g (f x) = x in a neighborhood of a, then g has derivative f'.symm at f a.

      For a version assuming f (g y) = y and continuity of g at f a but not [CompleteSpace E] see of_local_left_inverse.

      theorem isOpenMap_of_hasStrictFDerivAt_equiv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ†’ E โ‰ƒL[๐•œ] F} (hf : โˆ€ (x : E), HasStrictFDerivAt f (โ†‘(f' x)) x) :

      If a function has an invertible strict derivative at all points, then it is an open map.

      @[deprecated isOpenMap_of_hasStrictFDerivAt_equiv]
      theorem open_map_of_strict_fderiv_equiv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace E] {f : E โ†’ F} {f' : E โ†’ E โ‰ƒL[๐•œ] F} (hf : โˆ€ (x : E), HasStrictFDerivAt f (โ†‘(f' x)) x) :

      Alias of isOpenMap_of_hasStrictFDerivAt_equiv.


      If a function has an invertible strict derivative at all points, then it is an open map.