# Documentation

Mathlib.Analysis.NormedSpace.Banach

# 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.

structure ContinuousLinearMap.NonlinearRightInverse {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) :
Type (max u_2 u_3)
• toFun : FE
• nnnorm : NNReal
• bound' : ∀ (y : F), s.nnnorm * y
• right_inv' : ∀ (y : F),

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.

Instances For
instance ContinuousLinearMap.instCoeFunNonlinearRightInverseForAll {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) :
CoeFun () fun x => FE
@[simp]
theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : E →L[𝕜] F} (fsymm : ) (y : F) :
f () = y
theorem ContinuousLinearMap.NonlinearRightInverse.bound {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {f : E →L[𝕜] F} (fsymm : ) (y : F) :
fsymm.nnnorm * y
noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E ≃L[𝕜] F) :

Given a continuous linear equivalence, the inverse is in particular an instance of ContinuousLinearMap.NonlinearRightInverse (which turns out to be linear).

Instances For

### Proof of the Banach open mapping theorem #

theorem ContinuousLinearMap.exists_approx_preimage_norm_le {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] (surj : ) :
C, C 0 ∀ (y : F), x, dist (f x) y 1 / 2 * y x C * y

First step of the proof of the Banach open mapping theorem (using completeness of F): 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‖/2 of y, to apply an iterative process.

theorem ContinuousLinearMap.exists_preimage_norm_le {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (surj : ) :
C, C > 0 ∀ (y : F), x, f x = y x C * y

The Banach open mapping theorem: if a bounded linear map between Banach spaces is onto, then any point has a preimage with controlled norm.

theorem ContinuousLinearMap.isOpenMap {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (surj : ) :

The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.

theorem ContinuousLinearMap.quotientMap {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (surj : ) :
theorem AffineMap.isOpenMap {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {P : Type u_4} {Q : Type u_5} [] [] [] [] (f : P →ᵃ[𝕜] Q) (hf : ) (surj : ) :

### Applications of the Banach open mapping theorem #

theorem ContinuousLinearMap.interior_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (hsurj : ) (s : Set F) :
interior (f ⁻¹' s) = f ⁻¹'
theorem ContinuousLinearMap.closure_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (hsurj : ) (s : Set F) :
closure (f ⁻¹' s) = f ⁻¹'
theorem ContinuousLinearMap.frontier_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] (f : E →L[𝕜] F) [] [] (hsurj : ) (s : Set F) :
frontier (f ⁻¹' s) = f ⁻¹'
theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hsurj : ) :
fsymm, 0 < fsymm.nnnorm
theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_def {𝕜 : Type u_4} {E : Type u_5} [] {F : Type u_6} [] [] [] (f : E →L[𝕜] F) (hsurj : ) :
= Classical.choose (_ : fsymm, 0 < fsymm.nnnorm)
@[irreducible]
noncomputable def ContinuousLinearMap.nonlinearRightInverseOfSurjective {𝕜 : Type u_4} {E : Type u_5} [] {F : Type u_6} [] [] [] (f : E →L[𝕜] F) (hsurj : ) :

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 E to E/F where F is a closed subspace of E without a closed complement. Then it doesn't have a continuous linear right inverse.)

Instances For
theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hsurj : ) :
0 < ().nnnorm
theorem LinearEquiv.continuous_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (e : E ≃ₗ[𝕜] F) (h : ) :

If a bounded linear map is a bijection, then its inverse is also a bounded linear map.

def LinearEquiv.toContinuousLinearEquivOfContinuous {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (e : E ≃ₗ[𝕜] F) (h : ) :
E ≃L[𝕜] F

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.

Instances For
@[simp]
theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (e : E ≃ₗ[𝕜] F) (h : ) :
@[simp]
theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (e : E ≃ₗ[𝕜] F) (h : ) :
noncomputable def ContinuousLinearEquiv.ofBijective {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hinj : ) (hsurj : ) :
E ≃L[𝕜] F

Convert a bijective continuous linear map f : E →L[𝕜] F from a Banach space to a normed space to a continuous linear equivalence.

Instances For
@[simp]
theorem ContinuousLinearEquiv.coeFn_ofBijective {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hinj : ) (hsurj : ) :
↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f
theorem ContinuousLinearEquiv.coe_ofBijective {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hinj : ) (hsurj : ) :
@[simp]
theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hinj : ) (hsurj : ) (x : E) :
@[simp]
theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (hinj : ) (hsurj : ) (y : F) :
noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) {G : } (h : ) [CompleteSpace { x // x G }] (hker : ) :
(E × { x // x G }) ≃L[𝕜] F

Intermediate definition used to show ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot.

This is f.coprod G.subtypeL as a ContinuousLinearEquiv.

Instances For
theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) {G : } (h : ) [CompleteSpace { x // x G }] (hker : ) :
theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (f : E →L[𝕜] F) (G : ) (h : ) (hG : IsClosed G) (hker : ) :
theorem LinearMap.continuous_of_isClosed_graph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (g : E →ₗ[𝕜] F) (hg : ) :

The closed graph theorem : a linear map between two Banach spaces whose graph is closed is continuous.

theorem LinearMap.continuous_of_seq_closed_graph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] (g : E →ₗ[𝕜] F) (hg : ∀ (u : E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x)Filter.Tendsto (g u) Filter.atTop (nhds y)y = g x) :

A useful form of the closed graph theorem : let f be a linear map between two Banach spaces. To show that f is continuous, it suffices to show that for any convergent sequence uₙ ⟶ x, if f(uₙ) ⟶ y then y = f(x).

def ContinuousLinearMap.ofIsClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ) :
E →L[𝕜] F

Upgrade a LinearMap to a ContinuousLinearMap using the closed graph theorem.

Instances For
@[simp]
theorem ContinuousLinearMap.coeFn_ofIsClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ) :
theorem ContinuousLinearMap.coe_ofIsClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ) :
def ContinuousLinearMap.ofSeqClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ∀ (u : E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x)Filter.Tendsto (g u) Filter.atTop (nhds y)y = g x) :
E →L[𝕜] F

Upgrade a LinearMap to a ContinuousLinearMap using a variation on the closed graph theorem.

Instances For
@[simp]
theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ∀ (u : E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x)Filter.Tendsto (g u) Filter.atTop (nhds y)y = g x) :
theorem ContinuousLinearMap.coe_ofSeqClosedGraph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] [] [] {g : E →ₗ[𝕜] F} (hg : ∀ (u : E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (nhds x)Filter.Tendsto (g u) Filter.atTop (nhds y)y = g x) :