Documentation

Mathlib.Analysis.Calculus.Inverse

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 HasStrictDerivAt.toLocalHomeomorph that repacks a function f with a hf : HasStrictFDerivAt f f' a, f' : E โ‰ƒL[๐•œ] F, into a LocalHomeomorph. The toFun of this LocalHomeomorph is defeq to f, so one can apply theorems about LocalHomeomorph to hf.toLocalHomeomorph f, and get statements about f.

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

In the one-dimensional case we reformulate these theorems in terms of HasStrictDerivAt and f'โปยน.

We also reformulate the theorems in terms of ContDiff, to give that C^k (respectively, smooth) inputs give C^k (smooth) inverses. These versions require that continuous differentiability implies strict differentiability; this is false over a general field, true over โ„ or โ„‚ and implemented here assuming IsROrC ๐•‚.

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.

Notations #

In the section about ApproximatesLinearOn we introduce some local notation to make formulas shorter:

Tags #

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

Non-linear maps close to affine maps #

In this section we study a map f such that โ€–f x - f y - f' (x - y)โ€– โ‰ค c * โ€–x - yโ€– on an open set s, where f' : E โ†’L[๐•œ] F is a continuous linear map and c is suitably small. Maps of this type behave like f a + f' (x - a) near each a โˆˆ s.

When f' is onto, we show that f is locally onto.

When f' is a continuous linear equiv, we show that f is a homeomorphism between s and f '' s. More precisely, we define ApproximatesLinearOn.toLocalHomeomorph to be a LocalHomeomorph with toFun = f, source = s, and target = f '' s.

Maps of this type naturally appear in the proof of the inverse function theorem (see next section), and ApproximatesLinearOn.toLocalHomeomorph will imply that the locally inverse function exists.

We define this auxiliary notion to split the proof of the inverse function theorem into small lemmas. This approach makes it possible

def ApproximatesLinearOn {๐•œ : 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) (s : Set E) (c : NNReal) :

We say that f approximates a continuous linear map f' on s with constant c, if โ€–f x - f y - f' (x - y)โ€– โ‰ค c * โ€–x - yโ€– whenever x, y โˆˆ s.

This predicate is defined to facilitate the splitting of the inverse function theorem into small lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined on a specific set.

Instances For
    @[simp]
    theorem approximatesLinearOn_empty {๐•œ : 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) (c : NNReal) :

    First we prove some properties of a function that ApproximatesLinearOn a (not necessarily invertible) continuous linear map.

    theorem ApproximatesLinearOn.mono_num {๐•œ : 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} {s : Set E} {c : NNReal} {c' : NNReal} (hc : c โ‰ค c') (hf : ApproximatesLinearOn f f' s c) :
    theorem ApproximatesLinearOn.mono_set {๐•œ : 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} {s : Set E} {t : Set E} {c : NNReal} (hst : s โŠ† t) (hf : ApproximatesLinearOn f f' t c) :
    theorem ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith {๐•œ : 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} {s : Set E} {c : NNReal} :
    ApproximatesLinearOn f f' s c โ†” LipschitzOnWith c (f - โ†‘f') s
    theorem ApproximatesLinearOn.lipschitzOnWith {๐•œ : 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} {s : Set E} {c : NNReal} :
    ApproximatesLinearOn f f' s c โ†’ LipschitzOnWith c (f - โ†‘f') s

    Alias of the forward direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.

    theorem LipschitzOnWith.approximatesLinearOn {๐•œ : 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} {s : Set E} {c : NNReal} :
    LipschitzOnWith c (f - โ†‘f') s โ†’ ApproximatesLinearOn f f' s c

    Alias of the reverse direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.

    theorem ApproximatesLinearOn.lipschitz_sub {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    LipschitzWith c fun x => f โ†‘x - โ†‘f' โ†‘x
    theorem ApproximatesLinearOn.lipschitz {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    theorem ApproximatesLinearOn.continuous {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
    theorem ApproximatesLinearOn.continuousOn {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :

    We prove that a function which is linearly approximated by a continuous linear map with a nonlinear right inverse is locally onto. This will apply to the case where the approximating map is a linear equivalence, for the local inverse theorem, but also whenever the approximating map is onto, by Banach's open mapping theorem.

    theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse {๐•œ : 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} {s : Set E} {c : NNReal} {f' : E โ†’L[๐•œ] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : ContinuousLinearMap.NonlinearRightInverse f') {ฮต : โ„} {b : E} (ฮต0 : 0 โ‰ค ฮต) (hฮต : Metric.closedBall b ฮต โŠ† s) :
    Set.SurjOn f (Metric.closedBall b ฮต) (Metric.closedBall (f b) (((โ†‘f'symm.nnnorm)โปยน - โ†‘c) * ฮต))

    If a function is linearly approximated by a continuous linear map with a (possibly nonlinear) right inverse, then it is locally onto: a ball of an explicit radius is included in the image of the map.

    theorem ApproximatesLinearOn.open_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} {s : Set E} {c : NNReal} {f' : E โ†’L[๐•œ] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : ContinuousLinearMap.NonlinearRightInverse f') (hs : IsOpen s) (hc : Subsingleton F โˆจ c < f'symm.nnnormโปยน) :
    IsOpen (f '' s)
    theorem ApproximatesLinearOn.image_mem_nhds {๐•œ : 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} {s : Set E} {c : NNReal} {f' : E โ†’L[๐•œ] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : ContinuousLinearMap.NonlinearRightInverse f') {x : E} (hs : s โˆˆ nhds x) (hc : Subsingleton F โˆจ c < f'symm.nnnormโปยน) :
    f '' s โˆˆ nhds (f x)
    theorem ApproximatesLinearOn.map_nhds_eq {๐•œ : 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} {s : Set E} {c : NNReal} {f' : E โ†’L[๐•œ] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : ContinuousLinearMap.NonlinearRightInverse f') {x : E} (hs : s โˆˆ nhds x) (hc : Subsingleton F โˆจ c < f'symm.nnnormโปยน) :
    Filter.map f (nhds x) = nhds (f x)

    From now on we assume that f approximates an invertible continuous linear map f : E โ‰ƒL[๐•œ] F.

    We also assume that either E = {0}, or c < โ€–f'โปยนโ€–โปยน. We use N as an abbreviation for โ€–f'โปยนโ€–.

    theorem ApproximatesLinearOn.injective {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :
    theorem ApproximatesLinearOn.injOn {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :
    theorem ApproximatesLinearOn.surjective {๐•œ : 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} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (โ†‘f') Set.univ c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :
    def ApproximatesLinearOn.toLocalEquiv {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :

    A map approximating a linear equivalence on a set defines a local equivalence on this set. Should not be used outside of this file, because it is superseded by toLocalHomeomorph below.

    This is a first step towards the inverse function.

    Instances For
      theorem ApproximatesLinearOn.inverse_continuousOn {๐•œ : 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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :

      The inverse function is continuous on f '' s. Use properties of LocalHomeomorph instead.

      The inverse function is approximated linearly on f '' s by f'.symm.

      def ApproximatesLinearOn.toLocalHomeomorph {๐•œ : 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} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) (hs : IsOpen s) :

      Given a function f that approximates a linear equivalence on an open set s, returns a local homeomorph with toFun = f and source = s.

      Instances For
        @[simp]
        theorem ApproximatesLinearOn.toLocalHomeomorph_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} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) (hs : IsOpen s) :
        @[simp]
        theorem ApproximatesLinearOn.toLocalHomeomorph_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} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) (hs : IsOpen s) :
        (ApproximatesLinearOn.toLocalHomeomorph f s hf hc hs).toLocalEquiv.source = s
        @[simp]
        theorem ApproximatesLinearOn.toLocalHomeomorph_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} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) (hs : IsOpen s) :
        (ApproximatesLinearOn.toLocalHomeomorph f s hf hc hs).toLocalEquiv.target = f '' s
        def ApproximatesLinearOn.toHomeomorph {๐•œ : 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} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') Set.univ c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) :

        A function f that approximates a linear equivalence on the whole space is a homeomorphism.

        Instances For

          In a real vector space, a function f that approximates a linear equivalence on a subset s can be extended to a homeomorphism of the whole space.

          theorem ApproximatesLinearOn.closedBall_subset_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} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (โ†‘f') s c) (hc : Subsingleton E โˆจ c < โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน) (hs : IsOpen s) {b : E} (ฮต0 : 0 โ‰ค ฮต) (hฮต : Metric.closedBall b ฮต โŠ† s) :
          Metric.closedBall (f b) ((โ†‘โ€–โ†‘(ContinuousLinearEquiv.symm f')โ€–โ‚Šโปยน - โ†‘c) * ฮต) โŠ† (ApproximatesLinearOn.toLocalHomeomorph f s hf hc hs).toLocalEquiv.target

          Inverse function theorem #

          Now we prove the 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.toLocalHomeomorph 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, 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) :
          def HasStrictFDerivAt.toLocalHomeomorph {๐•œ : 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 LocalHomeomorph 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 LocalHomeomorph has derivative f'.symm.

          Instances For
            @[simp]
            theorem HasStrictFDerivAt.toLocalHomeomorph_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_toLocalHomeomorph_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) :
            a โˆˆ (HasStrictFDerivAt.toLocalHomeomorph f hf).toLocalEquiv.source
            theorem HasStrictFDerivAt.image_mem_toLocalHomeomorph_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) :
            f a โˆˆ (HasStrictFDerivAt.toLocalHomeomorph f hf).toLocalEquiv.target
            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.

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

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

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

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

              Inverse function theorem, 1D case #

              In this case we prove a version of the inverse function theorem for maps f : ๐•œ โ†’ ๐•œ. We use ContinuousLinearEquiv.unitsEquivAut to translate HasStrictDerivAt f f' a and f' โ‰  0 into HasStrictFDerivAt f (_ : ๐•œ โ‰ƒL[๐•œ] ๐•œ) a.

              @[reducible]
              def HasStrictDerivAt.localInverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] (f : ๐•œ โ†’ ๐•œ) (f' : ๐•œ) (a : ๐•œ) (hf : HasStrictDerivAt f f' a) (hf' : f' โ‰  0) :
              ๐•œ โ†’ ๐•œ

              A function that is inverse to f near a.

              Instances For
                theorem HasStrictDerivAt.map_nhds_eq {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {a : ๐•œ} (hf : HasStrictDerivAt f f' a) (hf' : f' โ‰  0) :
                Filter.map f (nhds a) = nhds (f a)
                theorem HasStrictDerivAt.to_localInverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {a : ๐•œ} (hf : HasStrictDerivAt f f' a) (hf' : f' โ‰  0) :
                theorem HasStrictDerivAt.to_local_left_inverse {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ} {a : ๐•œ} (hf : HasStrictDerivAt f f' a) (hf' : f' โ‰  0) {g : ๐•œ โ†’ ๐•œ} (hg : โˆ€แถ  (x : ๐•œ) in nhds a, g (f x) = x) :
                theorem open_map_of_strict_deriv {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] [CompleteSpace ๐•œ] {f : ๐•œ โ†’ ๐•œ} {f' : ๐•œ โ†’ ๐•œ} (hf : โˆ€ (x : ๐•œ), HasStrictDerivAt f (f' x) x) (h0 : โˆ€ (x : ๐•œ), f' x โ‰  0) :

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

                Inverse function theorem, smooth case #

                def ContDiffAt.toLocalHomeomorph {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] (f : E' โ†’ F') {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :

                Given a ContDiff function over ๐•‚ (which is โ„ or โ„‚) with an invertible derivative at a, returns a LocalHomeomorph with to_fun = f and a โˆˆ source.

                Instances For
                  @[simp]
                  theorem ContDiffAt.toLocalHomeomorph_coe {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                  โ†‘(ContDiffAt.toLocalHomeomorph f hf hf' hn) = f
                  theorem ContDiffAt.mem_toLocalHomeomorph_source {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                  a โˆˆ (ContDiffAt.toLocalHomeomorph f hf hf' hn).toLocalEquiv.source
                  theorem ContDiffAt.image_mem_toLocalHomeomorph_target {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                  f a โˆˆ (ContDiffAt.toLocalHomeomorph f hf hf' hn).toLocalEquiv.target
                  def ContDiffAt.localInverse {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                  F' โ†’ E'

                  Given a ContDiff function over ๐•‚ (which is โ„ or โ„‚) with an invertible derivative at a, returns a function that is locally inverse to f.

                  Instances For
                    theorem ContDiffAt.localInverse_apply_image {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                    ContDiffAt.localInverse hf hf' hn (f a) = a
                    theorem ContDiffAt.to_localInverse {๐•‚ : Type u_6} [IsROrC ๐•‚] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ๐•‚ E'] {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ๐•‚ F'] [CompleteSpace E'] {f : E' โ†’ F'} {f' : E' โ‰ƒL[๐•‚] F'} {a : E'} {n : โ„•โˆž} (hf : ContDiffAt ๐•‚ n f a) (hf' : HasFDerivAt f (โ†‘f') a) (hn : 1 โ‰ค n) :
                    ContDiffAt ๐•‚ n (ContDiffAt.localInverse hf hf' hn) (f a)

                    Given a ContDiff function over ๐•‚ (which is โ„ or โ„‚) with an invertible derivative at a, the inverse function (produced by ContDiff.toLocalHomeomorph) is also ContDiff.