mathlib3 documentation

analysis.normed_space.complemented

Complemented subspaces of normed vector spaces #

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

A submodule p of a topological module E over R is called complemented if there exists a continuous linear projection f : E →ₗ[R] p, ∀ x : p, f x = x. We prove that for a closed subspace of a normed space this condition is equivalent to existence of a closed subspace q such that p ⊓ q = ⊥, p ⊔ q = ⊤. We also prove that a subspace of finite codimension is always a complemented subspace.

Tags #

complemented subspace, normed vector space

noncomputable def continuous_linear_map.equiv_prod_of_surjective_of_is_compl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] [normed_add_comm_group G] [normed_space 𝕜 G] [complete_space E] [complete_space (F × G)] (f : E →L[𝕜] F) (g : E →L[𝕜] G) (hf : linear_map.range f = ) (hg : linear_map.range g = ) (hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :
E ≃L[𝕜] F × G

If f : E →L[R] F and g : E →L[R] G are two surjective linear maps and their kernels are complement of each other, then x ↦ (f x, g x) defines a linear equivalence E ≃L[R] F × G.

Equations
noncomputable def subspace.prod_equiv_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] (p q : subspace 𝕜 E) (h : is_compl p q) (hp : is_closed p) (hq : is_closed q) :
(p × q) ≃L[𝕜] E

If q is a closed complement of a closed subspace p, then p × q is continuously isomorphic to E.

Equations
noncomputable def subspace.linear_proj_of_closed_compl {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space E] (p q : subspace 𝕜 E) (h : is_compl p q) (hp : is_closed p) (hq : is_closed q) :
E →L[𝕜] p

Projection to a closed submodule along a closed complement.

Equations