The gap between two subspaces

For submodules U and V of an inner product space admitting orthogonal projections P_U and P_V, the gap between U and V is the operator norm ‖P_U - P_V‖, and the directed gap from U to V is ‖P_{Vᗮ} P_U‖, which measures how far vectors of U of norm at most one can stick out of V. The gap is symmetric, bounded by 1, and vanishes exactly when U = V; it is the quantity in which perturbation bounds for spectral subspaces are stated.

The main result is the sharp identity ‖P_U - P_V‖ = max ‖P_{Vᗮ} P_U‖ ‖P_{Uᗮ} P_V‖, with no completeness or dimension hypothesis. It reduces gap estimates to estimates of the two directed gaps, and identifies the gap as a measure of how far each subspace sticks out of the other. When U and V are finite-dimensional of the same dimension, the two directed gaps coincide, so the gap is the single directed gap ‖P_{Vᗮ} P_U‖: the largest principal sine from U to V. This holds in an arbitrary ambient inner product space, and fails without the dimension hypothesis, for instance for a line inside a plane.

Main definitions

• Submodule.projectionGap U V: the gap ‖P_U - P_V‖.
• Submodule.directedProjectionGap U V: the directed gap ‖P_{Vᗮ} P_U‖.

Main results

• Submodule.projectionGap_comm: the gap is symmetric.
• Submodule.directedProjectionGap_le_projectionGap: each directed gap is at most the gap.
• Submodule.projectionGap_eq_max: the gap is the larger of the two directed gaps.
• Submodule.directedProjectionGap_le_iff: the directed gap from U to V is the least s ≥ 0 with ‖P_{Vᗮ} u‖ ≤ s ‖u‖ for every u ∈ U.
• Submodule.disjoint_orthogonal_of_directedProjectionGap_lt_one: if the directed gap from U to V is less than 1, then U ⊓ Vᗮ = ⊥.
• Submodule.directedProjectionGap_le_directedProjectionGap_of_finrank_le: for a finite-dimensional subspace and a subspace of at least its dimension, the directed gap from the former is at most the directed gap from the latter.
• Submodule.directedProjectionGap_comm_of_finrank_eq and Submodule.projectionGap_eq_directedProjectionGap_of_finrank_eq: for finite-dimensional subspaces of equal dimension the two directed gaps agree, and the gap equals either of them.
• Submodule.directedProjectionGap_eq_zero_iff: the directed gap from U to V vanishes exactly when U ≤ V; consequently Submodule.projectionGap_eq_zero_iff.

References

• T. Kato, Perturbation Theory for Linear Operators, Springer (1995), §I.6.8.
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970).
• G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press (1990), §I.5.

noncomputable def Submodule.projectionGap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ℝ

The gap ‖P_U - P_V‖ between two subspaces with orthogonal projections.

noncomputable def Submodule.directedProjectionGap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ℝ

The directed gap ‖P_{Vᗮ} P_U‖ from U to V: the supremum of the norm of the component orthogonal to V of a vector of U with norm at most one.

theorem Submodule.projectionGap_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.projectionGap V = ‖U.starProjection - V.starProjection‖

theorem Submodule.directedProjectionGap_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.directedProjectionGap V = ‖Vᗮ.starProjection ∘SL U.starProjection‖

theorem Submodule.projectionGap_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : 0 ≤ U.projectionGap V

theorem Submodule.directedProjectionGap_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : 0 ≤ U.directedProjectionGap V

theorem Submodule.projectionGap_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.projectionGap V = V.projectionGap U

The gap is symmetric.

@[simp]

theorem Submodule.projectionGap_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.projectionGap U = 0

@[simp]

theorem Submodule.projectionGap_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : Uᗮ.projectionGap Vᗮ = U.projectionGap V

Passing to orthogonal complements preserves the gap.

@[simp]

theorem Submodule.directedProjectionGap_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : Vᗮ.directedProjectionGap Uᗮ = U.directedProjectionGap V

Passing to orthogonal complements reverses the directed gap.

theorem Submodule.directedProjectionGap_le_projectionGap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.directedProjectionGap V ≤ U.projectionGap V

The directed gap from U to V is at most the gap.

theorem Submodule.directedProjectionGap_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.directedProjectionGap V ≤ 1

The directed gap from U to V is at most 1.

theorem Submodule.projectionGap_eq_max {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.projectionGap V = max (U.directedProjectionGap V) (V.directedProjectionGap U)

The sharp projection-gap identity: the gap between two subspaces is the larger of the two directed gaps, ‖P_U - P_V‖ = max ‖P_{Vᗮ} P_U‖ ‖P_{Uᗮ} P_V‖.

theorem Submodule.projectionGap_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.projectionGap V ≤ 1

The gap between two subspaces is at most 1.

@[simp]

theorem Submodule.directedProjectionGap_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.directedProjectionGap V = 0 ↔ U ≤ V

The directed gap from U to V vanishes exactly when U is contained in V.

@[simp]

theorem Submodule.directedProjectionGap_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.directedProjectionGap U = 0

@[simp]

theorem Submodule.projectionGap_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.projectionGap V = 0 ↔ U = V

The gap between U and V vanishes exactly when U = V.

theorem Submodule.directedProjectionGap_le_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] {s : ℝ} (hs : 0 ≤ s) : U.directedProjectionGap V ≤ s ↔ ∀ u ∈ U, ‖Vᗮ.starProjection u‖ ≤ s * ‖u‖

For s ≥ 0, the directed gap from U to V is at most s exactly when every vector of U has its component orthogonal to V bounded by s times its norm.

theorem Submodule.disjoint_orthogonal_of_directedProjectionGap_lt_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U.directedProjectionGap V < 1) : Disjoint U Vᗮ

If the directed gap ‖P_{Vᗮ} P_U‖ from U to V is less than 1, then no nonzero vector of U is orthogonal to V.

theorem Submodule.directedProjectionGap_le_directedProjectionGap_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥V] (h : Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 ↥U) : V.directedProjectionGap U ≤ U.directedProjectionGap V

For a finite-dimensional subspace V and a subspace U with dim V ≤ dim U, the directed gap from V to U is at most the directed gap from U to V: ‖P_{Uᗮ} P_V‖ ≤ ‖P_{Vᗮ} P_U‖.

theorem Submodule.directedProjectionGap_comm_of_finrank_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥U] [FiniteDimensional 𝕜 ↥V] (h : Module.finrank 𝕜 ↥U = Module.finrank 𝕜 ↥V) : U.directedProjectionGap V = V.directedProjectionGap U

For finite-dimensional subspaces of equal dimension, the directed gap from U to V equals the directed gap from V to U: ‖P_{Vᗮ} P_U‖ = ‖P_{Uᗮ} P_V‖. The ambient space is arbitrary. Without the dimension hypothesis this fails: for a line U inside a plane V the first gap is 0 and the second is 1.

theorem Submodule.projectionGap_eq_directedProjectionGap_of_finrank_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥U] [FiniteDimensional 𝕜 ↥V] (h : Module.finrank 𝕜 ↥U = Module.finrank 𝕜 ↥V) : U.projectionGap V = U.directedProjectionGap V

The equal-rank sine identity: for finite-dimensional subspaces of equal dimension, the gap is the directed gap, ‖P_U - P_V‖ = ‖P_{Vᗮ} P_U‖.