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.toOpenPartialHomeomorph that repacks a function f
with a hf : HasStrictFDerivAt f f' a, f' : E โL[๐] F, into an OpenPartialHomeomorph.
The toFun of this OpenPartialHomeomorph is defeq to f, so one can apply theorems
about OpenPartialHomeomorph to hf.toOpenPartialHomeomorph f, and get statements about f.
Then we define HasStrictFDerivAt.localInverse to be the invFun of this OpenPartialHomeomorph,
and prove two versions of the inverse function theorem:
HasStrictFDerivAt.to_localInverse: iffhas an invertible derivativef'atain the strict sense (hf), thenhf.localInverse f f' ahas derivativef'.symmatf ain the strict sense;HasStrictFDerivAt.to_local_left_inverse: iffhas an invertible derivativef'atain the strict sense andgis locally left inverse tofneara, thenghas derivativef'.symmatf ain the strict sense.
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.toOpenPartialHomeomorph to construct the inverse
function.
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.
Given a function with an invertible strict derivative at a, returns an OpenPartialHomeomorph
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 OpenPartialHomeomorph has derivative f'.symm.
Equations
- HasStrictFDerivAt.toOpenPartialHomeomorph f hf = ApproximatesLinearOn.toOpenPartialHomeomorph f (Classical.choose โฏ) โฏ โฏ โฏ
Instances For
Alias of HasStrictFDerivAt.toOpenPartialHomeomorph.
Given a function with an invertible strict derivative at a, returns an OpenPartialHomeomorph
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 OpenPartialHomeomorph has derivative f'.symm.
Instances For
Alias of HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source.
Alias of HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target.
Given a function f with an invertible derivative, returns a function that is locally inverse
to f.
Equations
- HasStrictFDerivAt.localInverse f f' a hf = โ(HasStrictFDerivAt.toOpenPartialHomeomorph f hf).symm
Instances For
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.
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.
If a function has an invertible strict derivative at all points, then it is an open map.