# mathlibdocumentation

analysis.normed_space.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 continuous_linear_map.nonlinear_right_inverse {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) :
Type (max u_2 u_3)

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.

@[instance]
def continuous_linear_map.nonlinear_right_inverse.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) :
Equations
@[simp]
theorem continuous_linear_map.nonlinear_right_inverse.right_inv {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E →L[𝕜] F} (fsymm : f.nonlinear_right_inverse) (y : F) :
f (fsymm y) = y
theorem continuous_linear_map.nonlinear_right_inverse.bound {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] {f : E →L[𝕜] F} (fsymm : f.nonlinear_right_inverse) (y : F) :
fsymm y ((fsymm.nnnorm)) * y
def continuous_linear_equiv.to_nonlinear_right_inverse {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃L[𝕜] F) :

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

Equations
@[instance]
def continuous_linear_map.nonlinear_right_inverse.inhabited {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E ≃L[𝕜] F) :
Equations

### Proof of the Banach open mapping theorem #

theorem exists_approx_preimage_norm_le {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (surj : function.surjective f) :
∃ (C : ) (H : 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 exists_preimage_norm_le {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (surj : function.surjective f) :
∃ (C : ) (H : 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 open_mapping {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (surj : function.surjective f) :

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

### Applications of the Banach open mapping theorem #

theorem continuous_linear_map.exists_nonlinear_right_inverse_of_surjective {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hsurj : f.range = ) :
∃ (fsymm : f.nonlinear_right_inverse), 0 < fsymm.nnnorm
def continuous_linear_map.nonlinear_right_inverse_of_surjective {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hsurj : f.range = ) :

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
theorem continuous_linear_map.nonlinear_right_inverse_of_surjective_nnnorm_pos {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hsurj : f.range = ) :
theorem linear_equiv.continuous_symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (e : E ≃ₗ[𝕜] F) (h : continuous e) :

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

def linear_equiv.to_continuous_linear_equiv_of_continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (e : E ≃ₗ[𝕜] F) (h : continuous e) :
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.

Equations
@[simp]
theorem linear_equiv.coe_fn_to_continuous_linear_equiv_of_continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (e : E ≃ₗ[𝕜] F) (h : continuous e) :
@[simp]
theorem linear_equiv.coe_fn_to_continuous_linear_equiv_of_continuous_symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (e : E ≃ₗ[𝕜] F) (h : continuous e) :
= (e.symm)
def continuous_linear_equiv.of_bijective {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) :
E ≃L[𝕜] F

Convert a bijective continuous linear map f : E →L[𝕜] F between two Banach spaces to a continuous linear equivalence.

Equations
@[simp]
theorem continuous_linear_equiv.coe_fn_of_bijective {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) :
hsurj) = f
theorem continuous_linear_equiv.coe_of_bijective {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) :
hsurj) = f
@[simp]
theorem continuous_linear_equiv.of_bijective_symm_apply_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) (x : E) :
hsurj).symm) (f x) = x
@[simp]
theorem continuous_linear_equiv.of_bijective_apply_symm_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) (y : F) :
f ( hsurj).symm) y) = y
def continuous_linear_map.coprod_subtypeL_equiv_of_is_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) {G : F} (h : G) (hker : f.ker = ) :
(E × G) ≃L[𝕜] F

Intermediate definition used to show continuous_linear_map.closed_complemented_range_of_is_compl_of_ker_eq_bot.

This is f.coprod G.subtypeL as an continuous_linear_equiv.

Equations
theorem continuous_linear_map.range_eq_map_coprod_subtypeL_equiv_of_is_compl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) {G : F} (h : G) (hker : f.ker = ) :
theorem continuous_linear_map.closed_complemented_range_of_is_compl_of_ker_eq_bot {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_3} [normed_group F] [ F] (f : E →L[𝕜] F) (G : F) (h : G) (hG : is_closed G) (hker : f.ker = ) :