Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv

Inverse function theorem, 1D case #

In this file 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, inline]
abbrev 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.

Equations
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 isOpenMap_of_hasStrictDerivAt {๐•œ : 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.

    @[deprecated isOpenMap_of_hasStrictDerivAt]
    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) :

    Alias of isOpenMap_of_hasStrictDerivAt.


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