Documentation

Mathlib.Analysis.Normed.Module.Complemented

Complemented subspaces of normed vector spaces #

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

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
Instances For
    @[simp]
    def Submodule.prodEquivOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (p q : Subspace 𝕜 E) (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed 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
    Instances For
      def Submodule.linearProjOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (p q : Subspace 𝕜 E) (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
      E →L[𝕜] p

      Projection to a closed submodule along a closed complement.

      Equations
      Instances For
        @[simp]
        theorem Submodule.coe_prodEquivOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
        @[simp]
        theorem Submodule.coe_prodEquivOfClosedCompl_symm {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
        @[simp]
        theorem Submodule.coe_continuous_linearProjOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
        @[simp]
        theorem Submodule.coe_continuous_linearProjOfClosedCompl' {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
        theorem Submodule.ClosedComplemented.of_isCompl_isClosed {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :