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)
- to_fun : F → E
- nnnorm : nnreal
- bound' : ∀ (y : F), ‖self.to_fun y‖ ≤ ↑(self.nnnorm) * ‖y‖
- right_inv' : ∀ (y : F), ⇑f (self.to_fun y) = y
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
- continuous_linear_map.nonlinear_right_inverse.has_sizeof_inst
- continuous_linear_map.nonlinear_right_inverse.has_coe_to_fun
- continuous_linear_map.nonlinear_right_inverse.inhabited
@[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) :
has_coe_to_fun f.nonlinear_right_inverse (λ (_x : f.nonlinear_right_inverse), F → E)
Equations
- continuous_linear_map.nonlinear_right_inverse.has_coe_to_fun f = {coe := λ (fsymm : f.nonlinear_right_inverse), fsymm.to_fun}
@[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) :
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
- f.to_nonlinear_right_inverse = {to_fun := f.to_linear_equiv.inv_fun, nnnorm := ‖↑(f.symm)‖₊, bound' := _, right_inv' := _}
@[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) :
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) :
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) :
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 : linear_map.range f = ⊤) :
∃ (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 : linear_map.range f = ⊤) :
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 : linear_map.range f = ⊤) :
0 < (f.nonlinear_right_inverse_of_surjective hsurj).nnnorm
@[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) :
continuous ⇑(e.symm)
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) :
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
- e.to_continuous_linear_equiv_of_continuous h = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := h, continuous_inv_fun := _}
@[simp]
theorem
linear_equiv.coe_fn_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) :
@[simp]
theorem
linear_equiv.coe_fn_to_continuous_linear_equiv_of_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) :
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 = ⊤) :
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 : linear_map.ker f = ⊥)
(hsurj : linear_map.range f = ⊤) :
⇑(continuous_linear_equiv.of_bijective f hinj hsurj) = ⇑f
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 : linear_map.ker f = ⊥)
(hsurj : linear_map.range f = ⊤) :
↑(continuous_linear_equiv.of_bijective f hinj hsurj) = f
@[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 : linear_map.ker f = ⊥)
(hsurj : linear_map.range f = ⊤)
(x : E) :
⇑((continuous_linear_equiv.of_bijective f hinj hsurj).symm) (⇑f x) = x
@[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 : linear_map.ker f = ⊥)
(hsurj : linear_map.range f = ⊤)
(y : F) :
⇑f (⇑((continuous_linear_equiv.of_bijective f hinj hsurj).symm) y) = y
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 (linear_map.range f) G)
[complete_space ↥G]
(hker : linear_map.ker 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
- f.coprod_subtypeL_equiv_of_is_compl h hker = continuous_linear_equiv.of_bijective (f.coprod G.subtypeL) _ _
theorem
continuous_linear_map.range_eq_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 (linear_map.range f) G)
[complete_space ↥G]
(hker : linear_map.ker f = ⊥) :
linear_map.range f = submodule.map ↑(f.coprod_subtypeL_equiv_of_is_compl h hker) (⊤.prod ⊥)
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 (linear_map.range f) G)
(hG : is_closed ↑G)
(hker : linear_map.ker f = ⊥) :
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)) :
Upgrade a linear_map to a continuous_linear_map using the closed graph theorem.
Equations
- continuous_linear_map.of_is_closed_graph hg = {to_linear_map := g, cont := _}
@[simp]
theorem
continuous_linear_map.coe_fn_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)) :
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) :
Upgrade a linear_map to a continuous_linear_map using a variation on the
closed graph theorem.
Equations
- continuous_linear_map.of_seq_closed_graph hg = {to_linear_map := g, cont := _}
@[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) :