Non-linear maps close to affine maps #
In this file 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.toPartialHomeomorph to
be a PartialHomeomorph with toFun = f, source = s, and target = f '' s.
between s and f '' s. More precisely, we define ApproximatesLinearOn.toPartialHomeomorph to
be a PartialHomeomorph 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.toPartialHomeomorph will imply that the locally inverse function
and ApproximatesLinearOn.toPartialHomeomorph 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
to prove a lower estimate on the size of the domain of the inverse function;
to reuse parts of the proofs in the case if a function is not strictly differentiable. E.g., for a function
f : E × F → Gwith estimates onf x y₁ - f x y₂but not onf x₁ y - f x₂ y.
Notations #
We introduce some local notation to make formulas shorter:
- by
Nwe denote‖f'⁻¹‖; - by
gwe denote the auxiliary contracting mapx ↦ x + f'.symm (y - f x)used to prove that{x | f x = y}is nonempty.
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
First we prove some properties of a function that ApproximatesLinearOn a (not necessarily
invertible) continuous linear map.
Alias of the reverse direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.
Alias of the forward direction of ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith.
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.
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.
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'⁻¹‖.
A map approximating a linear equivalence on a set defines a partial equivalence on this set.
Should not be used outside of this file, because it is superseded by toPartialHomeomorph below.
This is a first step towards the inverse function.
Equations
- hf.toPartialEquiv hc = Set.InjOn.toPartialEquiv f s ⋯
Instances For
The inverse function is continuous on f '' s.
Use properties of PartialHomeomorph instead.
The inverse function is approximated linearly on f '' s by f'.symm.
Given a function f that approximates a linear equivalence on an open set s,
returns a partial homeomorphism with toFun = f and source = s.
Equations
- ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs = { toPartialEquiv := hf.toPartialEquiv hc, open_source := hs, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
Instances For
A function f that approximates a linear equivalence on the whole space is a homeomorphism.
Equations
- ApproximatesLinearOn.toHomeomorph f hf hc = (ApproximatesLinearOn.toPartialHomeomorph f Set.univ hf hc ⋯).toHomeomorphOfSourceEqUnivTargetEqUniv ⋯ ⋯