analysis.normed_space.banach

source

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

source

@[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}

source

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

source

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‖

source

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

↑f.nonlinear_right_inverse

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' := _}

source

@[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) :

inhabited ↑f.nonlinear_right_inverse

Equations

continuous_linear_map.nonlinear_right_inverse.inhabited f = {default := f.to_nonlinear_right_inverse}

source

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.

source

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.

source

@[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) :

is_open_map ⇑f

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

source

@[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) :

quotient_map ⇑f

source

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

is_open_map ⇑f

source

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

interior (⇑f ⁻¹' s) = ⇑f ⁻¹' interior s

source

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

closure (⇑f ⁻¹' s) = ⇑f ⁻¹' closure s

source

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

frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s

source

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

source

@[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 = ⊤) :

f.nonlinear_right_inverse

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

f.nonlinear_right_inverse_of_surjective hsurj = classical.some _

source

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

source

@[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.

source

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

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 := _}

source

@[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) :

⇑(e.to_continuous_linear_equiv_of_continuous h) = ⇑e

source

@[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) :

⇑((e.to_continuous_linear_equiv_of_continuous h).symm) = ⇑(e.symm)

source

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

continuous_linear_equiv.of_bijective f hinj hsurj = (linear_equiv.of_bijective ↑f _).to_continuous_linear_equiv_of_continuous _

source

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

source

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

source

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

source

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

source

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 = ⊥) :

(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

f.coprod_subtypeL_equiv_of_is_compl h hker = continuous_linear_equiv.of_bijective (f.coprod G.subtypeL) _ _

source

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

source

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 = ⊥) :

is_closed ↑(linear_map.range f)

source

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

continuous ⇑g

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

source

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

continuous ⇑g

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

source

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

continuous_linear_map.of_is_closed_graph hg = {to_linear_map := g, cont := _}

source

@[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)) :

⇑(continuous_linear_map.of_is_closed_graph hg) = ⇑g

source

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

↑(continuous_linear_map.of_is_closed_graph hg) = g

source

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

continuous_linear_map.of_seq_closed_graph hg = {to_linear_map := g, cont := _}

source

@[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) :

⇑(continuous_linear_map.of_seq_closed_graph hg) = ⇑g

source

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

↑(continuous_linear_map.of_seq_closed_graph hg) = g

mathlib documentation

Banach open mapping theorem #

Proof of the Banach open mapping theorem #

Applications of the Banach open mapping theorem #