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} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [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 * ‖y‖
• right_inv' (y : F) : f (self.toFun y) = y

instance ContinuousLinearMap.instCoeFunNonlinearRightInverseForall {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) : CoeFun f.NonlinearRightInverse fun (x : f.NonlinearRightInverse) => F → E

@[simp]

theorem ContinuousLinearMap.NonlinearRightInverse.right_inv {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [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} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {f : E →SL[σ] F} (fsymm : f.NonlinearRightInverse) (y : F) : ‖fsymm.toFun y‖ ≤ ↑fsymm.nnnorm * ‖y‖

noncomputable def ContinuousLinearEquiv.toNonlinearRightInverse {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ'] [RingHomInvPair σ' σ] (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).

noncomputable instance instInhabitedNonlinearRightInverseToContinuousLinearMap {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ'] [RingHomInvPair σ' σ] (f : E ≃SL[σ] F) : Inhabited (↑f).NonlinearRightInverse

Proof of the Banach open mapping theorem

theorem ContinuousLinearMap.exists_approx_preimage_norm_le {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] (surj : Function.Surjective ⇑f) : ∃ C ≥ 0, ∀ (y : F), ∃ (x : E), 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} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) : ∃ C > 0, ∀ (y : F), ∃ (x : E), 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} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) : IsOpenMap ⇑f

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

theorem ContinuousLinearMap.isQuotientMap {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) : Topology.IsQuotientMap ⇑f

theorem AffineMap.isOpenMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {P : Type u_6} {Q : Type u_7} [MetricSpace P] [NormedAddTorsor E P] [MetricSpace Q] [NormedAddTorsor F Q] (f : P →ᵃ[𝕜] Q) (hf : Continuous ⇑f) (surj : Function.Surjective ⇑f) : IsOpenMap ⇑f

Applications of the Banach open mapping theorem

theorem ContinuousLinearMap.interior_preimage {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) : interior (⇑f ⁻¹' s) = ⇑f ⁻¹' interior s

theorem ContinuousLinearMap.closure_preimage {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) : closure (⇑f ⁻¹' s) = ⇑f ⁻¹' closure s

theorem ContinuousLinearMap.frontier_preimage {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) : frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s

theorem ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) : ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm

@[irreducible]

noncomputable def ContinuousLinearMap.nonlinearRightInverseOfSurjective {𝕜 : Type u_5} {𝕜' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) : 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.)

theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_def {𝕜 : Type u_5} {𝕜' : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) : f.nonlinearRightInverseOfSurjective hsurj = Classical.choose ⋯

theorem ContinuousLinearMap.nonlinearRightInverseOfSurjective_nnnorm_pos {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (f : E →SL[σ] F) (hsurj : LinearMap.range f = ⊤) : 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm

theorem LinearEquiv.continuous_symm {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (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} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (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.

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (e : E ≃ₛₗ[σ] F) (h : Continuous ⇑e) : ⇑(e.toContinuousLinearEquivOfContinuous h) = ⇑e

@[simp]

theorem LinearEquiv.coeFn_toContinuousLinearEquivOfContinuous_symm {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (e : E ≃ₛₗ[σ] F) (h : Continuous ⇑e) : ⇑(e.toContinuousLinearEquivOfContinuous h).symm = ⇑e.symm

noncomputable def ContinuousLinearMap.equivRange {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) : E ≃SL[σ] ↥(LinearMap.range f)

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

@[simp]

theorem ContinuousLinearMap.coe_linearMap_equivRange {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) : ↑(equivRange hinj hclo) = f.rangeRestrict

@[simp]

theorem ContinuousLinearMap.coe_equivRange {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) : ⇑(equivRange hinj hclo) = ⇑f.rangeRestrict

@[simp]

theorem ContinuousLinearMap.equivRange_symm_toLinearEquiv {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) : (equivRange hinj hclo).symm = (LinearEquiv.ofInjective (↑f) hinj).symm

@[simp]

theorem ContinuousLinearMap.equivRange_symm_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) (x : E) : (equivRange hinj hclo).symm ⟨f x, ⋯⟩ = x

theorem ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →L[𝕜] F) (hf : Function.Injective ⇑f) (hf' : IsClosed (Set.range ⇑f)) : ∃ (K : NNReal), AntilipschitzWith K ⇑f

If f : E →L[𝕜] F is injective with closed range (and E and F are Banach spaces), f is anti-Lipschitz.

theorem ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →L[𝕜] F) (hf : Function.Injective ⇑f) : IsClosed (Set.range ⇑f) ↔ ∃ (K : NNReal), AntilipschitzWith K ⇑f

An injective bounded linear operator between Banach spaces has closed range iff it is anti-Lipschitz.

noncomputable def ContinuousLinearEquiv.ofBijective {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) : 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.

@[simp]

theorem ContinuousLinearEquiv.coeFn_ofBijective {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) : ⇑(ofBijective f hinj hsurj) = ⇑f

theorem ContinuousLinearEquiv.coe_ofBijective {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) : ↑(ofBijective f hinj hsurj) = f

@[simp]

theorem ContinuousLinearEquiv.ofBijective_symm_apply_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) (x : E) : (ofBijective f hinj hsurj).symm (f x) = x

@[simp]

theorem ContinuousLinearEquiv.ofBijective_apply_symm_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : LinearMap.ker f = ⊥) (hsurj : LinearMap.range f = ⊤) (y : F) : f ((ofBijective f hinj hsurj).symm y) = y

theorem ContinuousLinearMap.isUnit_iff_bijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {f : E →L[𝕜] E} : IsUnit f ↔ Function.Bijective ⇑f

noncomputable def ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace ↥G] (hker : LinearMap.ker f = ⊥) : (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.

theorem ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (LinearMap.range f) G) [CompleteSpace ↥G] (hker : LinearMap.ker f = ⊥) : LinearMap.range f = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)

theorem ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) (G : Submodule 𝕜 F) (h : IsCompl (LinearMap.range f) G) (hG : IsClosed ↑G) (hker : LinearMap.ker f = ⊥) : IsClosed ↑(LinearMap.range f)

theorem LinearMap.continuous_of_isClosed_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑g.graph) : E →L[𝕜] F

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

@[simp]

theorem ContinuousLinearMap.coeFn_ofIsClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑g.graph) : ⇑(ofIsClosedGraph hg) = ⇑g

theorem ContinuousLinearMap.coe_ofIsClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑g.graph) : ↑(ofIsClosedGraph hg) = g

def ContinuousLinearMap.ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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.

@[simp]

theorem ContinuousLinearMap.coeFn_ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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) : ⇑(ofSeqClosedGraph hg) = ⇑g

theorem ContinuousLinearMap.coe_ofSeqClosedGraph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 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) : ↑(ofSeqClosedGraph hg) = g

theorem ContinuousLinearMap.closed_range_of_antilipschitz {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] [CompleteSpace E] {f : E →SL[σ] F} {c : NNReal} (hf : AntilipschitzWith c ⇑f) : (LinearMap.range f).topologicalClosure = LinearMap.range f

theorem AntilipschitzWith.completeSpace_range_clm {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] [CompleteSpace E] [CompleteSpace F] {f : E →SL[σ] F} {c : NNReal} (hf : AntilipschitzWith c ⇑f) : CompleteSpace ↥(LinearMap.range f)

theorem ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] [CompleteSpace E] [CompleteSpace F] [RingHomInvPair σ' σ] [RingHomIsometric σ] [RingHomIsometric σ'] (f : E →SL[σ] F) : Function.Bijective ⇑f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ (c : NNReal), AntilipschitzWith c ⇑f