Orthogonal Projections onto Complementary Subspaces

Abstract

Complementary orthogonal projections satisfy the six canonical operator identities.

Theorem 1.1 (Closed-subspace projections obey the complement identities).

$$\forall k,E:\mathrm{Type},[\mathrm{RCLike}(k)],[\mathrm{NormedAddCommGroup}(E)],[{\mathrm{InnerProductSpace}}_k(E)],[\mathrm{CompleteSpace}(E)],M:{\mathrm{ClosedSubmodule}}_k(E),P_{M^{\perp }}=I-P_M\wedge P_M\circ P_M=P_M\wedge P_{M^{\perp }}\circ P_{M^{\perp }}=P_{M^{\perp }}\wedge P_M\circ P_{M^{\perp }}=0\wedge P_{M^{\perp }}\circ P_M=0\wedge P_M+P_{M^{\perp }}=I.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/OrthogonalProjectionComplement.orthogonal_complement_projection_identities (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let M be a closed subspace of a complete real or complex inner-product space, and let P with subscript M denote its orthogonal projection. The projection onto the orthogonal complement is the identity minus P with subscript M.

Both projections are idempotent. Their compositions vanish in both orders, and their sum is the identity operator. These are all six equalities in the named statement, retained as one conjunction.

Loogle and the pinned Mathlib tree supplied the exact complementary, idempotence, orthogonality, and sum declarations used by the Lean proof. The LeanSearch endpoint attempted for corroboration returned HTTP 404.

References

• Truth anchor: D5/S3/Quantum/Algebra/OrthogonalProjectionComplement.orthogonal_complement_projection_identities