# 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} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) :
Type (max u_3 u_4)

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.

• toFun : F β E
• nnnorm : NNReal
• bound' : β (y : F), βself.toFun yβ β€ βself.nnnorm *
• right_inv' : β (y : F), f (self.toFun y) = y
Instances For
theorem ContinuousLinearMap.NonlinearRightInverse.bound' {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] {f : E βSL[Ο] F} (self : f.NonlinearRightInverse) (y : F) :
βself.toFun yβ β€ βself.nnnorm *
theorem ContinuousLinearMap.NonlinearRightInverse.right_inv' {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] {f : E βSL[Ο] F} (self : f.NonlinearRightInverse) (y : F) :
f (self.toFun y) = y
instance ContinuousLinearMap.instCoeFunNonlinearRightInverseForall {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) :
CoeFun f.NonlinearRightInverse fun (x : f.NonlinearRightInverse) => F β E
Equations
• f.instCoeFunNonlinearRightInverseForall = { coe := fun (fsymm : f.NonlinearRightInverse) => fsymm.toFun }
@[simp]
theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] {f : E βSL[Ο] F} (fsymm : f.NonlinearRightInverse) (y : F) :
f (fsymm.toFun y) = y
theorem ContinuousLinearMap.NonlinearRightInverse.bound {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] {f : E βSL[Ο] F} (fsymm : f.NonlinearRightInverse) (y : F) :
βfsymm.toFun yβ β€ βfsymm.nnnorm *
noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) :
(βf).NonlinearRightInverse

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

Equations
• f.toNonlinearRightInverse = { toFun := f.invFun, nnnorm := ββf.symmββ, bound' := β―, right_inv' := β― }
Instances For
noncomputable instance instInhabitedNonlinearRightInverseToContinuousLinearMap {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) :
Inhabited (βf).NonlinearRightInverse
Equations
• = { default := f.toNonlinearRightInverse }

### Proof of the Banach open mapping theorem #

theorem ContinuousLinearMap.exists_approx_preimage_norm_le {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] (surj : ) :
β C β₯ 0, β (y : F), β (x : E), dist (f x) y β€ 1 / 2 * β§ β€ C *

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} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (surj : ) :
β C > 0, β (y : F), β (x : E), f x = y β§ β€ C *

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} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (surj : ) :
IsOpenMap βf

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

theorem ContinuousLinearMap.quotientMap {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (surj : ) :
QuotientMap βf
theorem AffineMap.isOpenMap {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {P : Type u_6} {Q : Type u_7} [] [] [] [] (f : P βα΅[π] Q) (hf : Continuous βf) (surj : ) :
IsOpenMap βf

### Applications of the Banach open mapping theorem #

theorem ContinuousLinearMap.interior_preimage {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (hsurj : ) (s : Set F) :
interior (βf β»ΒΉ' s) = βf β»ΒΉ'
theorem ContinuousLinearMap.closure_preimage {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (hsurj : ) (s : Set F) :
closure (βf β»ΒΉ' s) = βf β»ΒΉ'
theorem ContinuousLinearMap.frontier_preimage {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] (f : E βSL[Ο] F) [] [] (hsurj : ) (s : Set F) :
frontier (βf β»ΒΉ' s) = βf β»ΒΉ'
theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hsurj : ) :
β (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_def {π : Type u_5} {π' : Type u_6} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_7} [NormedSpace π E] {F : Type u_8} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hsurj : ) :
f.nonlinearRightInverseOfSurjective hsurj =
@[irreducible]
noncomputable def ContinuousLinearMap.nonlinearRightInverseOfSurjective {π : Type u_5} {π' : Type u_6} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_7} [NormedSpace π E] {F : Type u_8} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hsurj : ) :
f.NonlinearRightInverse

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

Equations
Instances For
theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hsurj : ) :
0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
theorem LinearEquiv.continuous_symm {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (e : E βββ[Ο] F) (h : Continuous βe) :
Continuous βe.symm

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

def LinearEquiv.toContinuousLinearEquivOfContinuous {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (e : E βββ[Ο] F) (h : Continuous βe) :
E βSL[Ο] 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.

Equations
• e.toContinuousLinearEquivOfContinuous h = { toLinearEquiv := e, continuous_toFun := h, continuous_invFun := β― }
Instances For
@[simp]
theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (e : E βββ[Ο] F) (h : Continuous βe) :
β(e.toContinuousLinearEquivOfContinuous h) = βe
@[simp]
theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (e : E βββ[Ο] F) (h : Continuous βe) :
β(e.toContinuousLinearEquivOfContinuous h).symm = βe.symm
noncomputable def ContinuousLinearMap.equivRange {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hclo : IsClosed (Set.range βf)) :
E βSL[Ο] β₯

An injective continuous linear map with a closed range defines a continuous linear equivalence between its domain and its range.

Equations
• f.equivRange hinj hclo = let_fun this := β―; (LinearEquiv.ofInjective (βf) hinj).toContinuousLinearEquivOfContinuous β―
Instances For
@[simp]
theorem ContinuousLinearMap.coe_linearMap_equivRange {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hclo : IsClosed (Set.range βf)) :
β(f.equivRange hinj hclo) = f.rangeRestrict
@[simp]
theorem ContinuousLinearMap.coe_equivRange {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hclo : IsClosed (Set.range βf)) :
β(f.equivRange hinj hclo) = βf.rangeRestrict
noncomputable def ContinuousLinearEquiv.ofBijective {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hsurj : ) :
E βSL[Ο] F

Convert a bijective continuous linear map f : E βSL[Ο] F from a Banach space to a normed space to a continuous linear equivalence.

Equations
Instances For
@[simp]
theorem ContinuousLinearEquiv.coeFn_ofBijective {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hsurj : ) :
β(ContinuousLinearEquiv.ofBijective f hinj hsurj) = βf
theorem ContinuousLinearEquiv.coe_ofBijective {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hsurj : ) :
β(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f
@[simp]
theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hsurj : ) (x : E) :
(ContinuousLinearEquiv.ofBijective f hinj hsurj).symm (f x) = x
@[simp]
theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) (hinj : ) (hsurj : ) (y : F) :
f ((ContinuousLinearEquiv.ofBijective f hinj hsurj).symm y) = y
theorem ContinuousLinearMap.isUnit_iff_bijective {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {f : E βL[π] E} :
noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] (f : E βL[π] F) {G : Submodule π F} (h : ) [CompleteSpace β₯G] (hker : ) :
(E Γ β₯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.

Equations
Instances For
theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] (f : E βL[π] F) {G : Submodule π F} (h : ) [CompleteSpace β₯G] (hker : ) :
= Submodule.map (ββ(f.coprodSubtypeLEquivOfIsCompl h hker)) (β€.prod β₯)
theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] (f : E βL[π] F) (G : Submodule π F) (h : ) (hG : IsClosed βG) (hker : ) :
IsClosed β
theorem LinearMap.continuous_of_isClosed_graph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] (g : E ββ[π] F) (hg : IsClosed βg.graph) :
Continuous βg

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_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] (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) :
Continuous βg

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_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {g : E ββ[π] F} (hg : IsClosed βg.graph) :
E βL[π] F

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

Equations
• = { toLinearMap := g, cont := β― }
Instances For
@[simp]
theorem ContinuousLinearMap.coeFn_ofIsClosedGraph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {g : E ββ[π] F} (hg : IsClosed βg.graph) :
= βg
theorem ContinuousLinearMap.coe_ofIsClosedGraph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {g : E ββ[π] F} (hg : IsClosed βg.graph) :
= g
def ContinuousLinearMap.ofSeqClosedGraph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {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.

Equations
• = { toLinearMap := g, cont := β― }
Instances For
@[simp]
theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {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) :
= βg
theorem ContinuousLinearMap.coe_ofSeqClosedGraph {π : Type u_1} [] {E : Type u_3} [NormedSpace π E] [] {F : Type u_5} [NormedSpace π F] [] {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.closed_range_of_antilipschitz {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] {f : E βSL[Ο] F} {c : NNReal} (hf : AntilipschitzWith c βf) :
.topologicalClosure =
theorem ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] [RingHomInvPair Ο' Ο] [] [] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] (f : E βSL[Ο] F) :
β .topologicalClosure = β€ β§ β (c : NNReal), AntilipschitzWith c βf
theorem AntilipschitzWith.completeSpace_range_clm {π : Type u_1} {π' : Type u_2} [] [] {Ο : π β+* π'} {Ο' : π' β+* π} [RingHomInvPair Ο Ο'] {E : Type u_3} [NormedSpace π E] {F : Type u_4} [NormedSpace π' F] [] [] {f : E βSL[Ο] F} {c : NNReal} (hf : AntilipschitzWith c βf) :