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.

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
@[protected, instance]
def continuous_linear_map.nonlinear_right_inverse.has_coe_to_fun {π•œ : 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) :
Equations
@[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) :
noncomputable def continuous_linear_equiv.to_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) :

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

Equations
@[protected, instance]
noncomputable def continuous_linear_map.nonlinear_right_inverse.inhabited {π•œ : 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) :
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]
theorem continuous_linear_map.is_open_map {π•œ : 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) :

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

@[protected]
theorem continuous_linear_map.quotient_map {π•œ : 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) :
theorem affine_map.is_open_map {π•œ : 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] {P : Type u_4} {Q : Type u_5} [metric_space P] [normed_add_torsor E P] [metric_space Q] [normed_add_torsor F Q] (f : P →ᡃ[π•œ] Q) (hf : continuous ⇑f) (surj : function.surjective ⇑f) :

Applications of the Banach open mapping theorem #

theorem continuous_linear_map.interior_preimage {π•œ : 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] (hsurj : function.surjective ⇑f) (s : set F) :
theorem continuous_linear_map.closure_preimage {π•œ : 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] (hsurj : function.surjective ⇑f) (s : set F) :
theorem continuous_linear_map.frontier_preimage {π•œ : 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] (hsurj : function.surjective ⇑f) (s : set F) :
theorem continuous_linear_map.exists_nonlinear_right_inverse_of_surjective {π•œ : 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) (hsurj : f.range = ⊀) :
βˆƒ (fsymm : f.nonlinear_right_inverse), 0 < fsymm.nnnorm
@[irreducible]
noncomputable def continuous_linear_map.nonlinear_right_inverse_of_surjective {π•œ : 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) (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} [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) (hsurj : f.range = ⊀) :
@[continuity]
theorem linear_equiv.continuous_symm {π•œ : 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] (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} [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] (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
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 : f.ker = βŠ₯) (hsurj : f.range = ⊀) :
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
@[simp]
theorem continuous_linear_equiv.coe_fn_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 : f.ker = βŠ₯) (hsurj : f.range = ⊀) :
theorem continuous_linear_equiv.coe_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 : f.ker = βŠ₯) (hsurj : f.range = ⊀) :
@[simp]
theorem continuous_linear_equiv.of_bijective_symm_apply_apply {π•œ : 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 : f.ker = βŠ₯) (hsurj : f.range = ⊀) (x : E) :
@[simp]
theorem continuous_linear_equiv.of_bijective_apply_symm_apply {π•œ : 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 : f.ker = βŠ₯) (hsurj : f.range = ⊀) (y : F) :
noncomputable def continuous_linear_map.coprod_subtypeL_equiv_of_is_compl {π•œ : 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) {G : submodule π•œ F} (h : is_compl f.range G) [complete_space β†₯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.closed_complemented_range_of_is_compl_of_ker_eq_bot {π•œ : 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) (G : submodule π•œ F) (h : is_compl f.range G) (hG : is_closed ↑G) (hker : f.ker = βŠ₯) :
theorem linear_map.continuous_of_is_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 : is_closed ↑(g.graph)) :

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

theorem linear_map.continuous_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) :

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 continuous_linear_map.of_is_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 : is_closed ↑(g.graph)) :
E β†’L[π•œ] F

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

Equations
@[simp]
theorem continuous_linear_map.coe_of_is_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 : is_closed ↑(g.graph)) :
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
@[simp]
theorem continuous_linear_map.coe_fn_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) :
theorem continuous_linear_map.coe_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) :