mathlib documentation

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.

theorem exists_approx_preimage_norm_le {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (f : E →L[𝕜] F) [complete_space F] :
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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (f : E →L[𝕜] F) [complete_space F] [complete_space E] :
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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] (f : E →L[𝕜] F) [complete_space F] [complete_space E] :

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

theorem linear_equiv.continuous_symm {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (e : E ≃ₗ[𝕜] F) :

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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (e : E ≃ₗ[𝕜] F) :
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
def continuous_linear_equiv.of_bijective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (f : E →L[𝕜] F) :
f.ker = 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) :

@[simp]
theorem continuous_linear_equiv.of_bijective_symm_apply_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) (x : E) :

@[simp]
theorem continuous_linear_equiv.of_bijective_apply_symm_apply {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] (f : E →L[𝕜] F) (hinj : f.ker = ) (hsurj : f.range = ) (y : F) :