mathlib3 documentation

analysis.normed_space.banach

Banach open mapping theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 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.

Instances for continuous_linear_map.nonlinear_right_inverse
@[simp]
theorem continuous_linear_map.nonlinear_right_inverse.right_inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E →L[𝕜] F} (fsymm : f.nonlinear_right_inverse) (y : F) :
fsymm y (fsymm.nnnorm) * y

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

Equations

Proof of the Banach open mapping theorem #

theorem continuous_linear_map.exists_approx_preimage_norm_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E →L[𝕜] F) [complete_space F] (surj : function.surjective f) :
(C : ) (H : C 0), (y : F), (x : E), has_dist.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 continuous_linear_map.exists_preimage_norm_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E →L[𝕜] F) [complete_space F] [complete_space E] (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.

@[protected]

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

Applications of the Banach open mapping theorem #

@[irreducible]

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
@[continuity]

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

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

Equations

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

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

Upgrade a linear_map to a continuous_linear_map using the closed graph theorem.

Equations
def continuous_linear_map.of_seq_closed_graph {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space F] [complete_space E] {g : E →ₗ[𝕜] F} (hg : (u : E) (x : E) (y : F), filter.tendsto u filter.at_top (nhds x) filter.tendsto (g u) filter.at_top (nhds y) y = g x) :
E →L[𝕜] F

Upgrade a linear_map to a continuous_linear_map using a variation on the closed graph theorem.

Equations