Banach open mapping theorem #
This file contains the Banach open mapping theorem, i.e., the fact that a bijective bounded linear map between Banach spaces has a bounded inverse.
- to_fun : F → E
- nnnorm : ℝ≥0
- bound' : ∀ (y : F), ∥self.to_fun y∥ ≤ (↑(self.nnnorm)) * ∥y∥
- right_inv' : ∀ (y : F), ⇑f (self.to_fun y) = y
A (possibly nonlinear) right inverse to a continuous linear map, which doesn't have to be
linear itself but which satisfies a bound
∥inverse x∥ ≤ C * ∥x∥. A surjective continuous linear
map doesn't always have a continuous linear right inverse, but it always has a nonlinear inverse
in this sense, by Banach's open mapping theorem.
Given a continuous linear equivalence, the inverse is in particular an instance of
nonlinear_right_inverse (which turns out to be linear).
Proof of the Banach open mapping theorem #
First step of the proof of the Banach open mapping theorem (using completeness of
by Baire's theorem, there exists a ball in
E whose image closure has nonempty interior.
Rescaling everything, it follows that any
y ∈ F is arbitrarily well approached by
images of elements of norm at most
C * ∥y∥.
For further use, we will only need such an element whose image
is within distance
y, to apply an iterative process.
The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then any point has a preimage with controlled norm.
The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.
Applications of the Banach open mapping theorem #
A surjective continuous linear map between Banach spaces admits a (possibly nonlinear)
controlled right inverse. In general, it is not possible to ensure that such a right inverse
is linear (take for instance the map from
F is a closed subspace of
without a closed complement. Then it doesn't have a continuous linear right inverse.)
If a bounded linear map is a bijection, then its inverse is also a bounded linear map.
Associating to a linear equivalence between Banach spaces a continuous linear equivalence when the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the inverse map is also continuous.
Convert a bijective continuous linear map
f : E →L[𝕜] F from a Banach space to a normed space
to a continuous linear equivalence.
Intermediate definition used to show
f.coprod G.subtypeL as an