Documentation

TauCeti.Analysis.InnerProductSpace.Projection.SinTheta

The dimension-free Davis–Kahan sin Θ theorem #

Let A and B be bounded operators on an inner product space E, let U be invariant under A and W invariant under B, with B symmetric. If the quadratic form of A on U lies above that of B on W with a margin g,

(c + g) ‖u‖² ≤ re ⟪A u, u⟫ for u ∈ U and re ⟪B w, w⟫ ≤ c ‖w‖² for w ∈ W,

then g ‖P_W P_U‖ ≤ ‖B - A‖. Taking W = Vᗮ for a B-invariant subspace V bounds the directed gap ‖P_{Vᗮ} P_U‖, the operator norm of the directed sine from U towards V: for g > 0, the A-invariant subspace U sticks out of the B-invariant subspace V by at most ‖B - A‖ / g, as long as the part of A on U stays separated by g from the part of B on Vᗮ. With the separation hypotheses in both orientations, the sharp gap identity Submodule.projectionGap_eq_max turns the two directed bounds into the bound g ‖P_U - P_V‖ ≤ ‖B - A‖ on the gap between U and V.

No completeness, finite dimension, or spectral theorem is used; the hypotheses are quadratic-form bounds, which on invariant subspaces of symmetric operators on finite-dimensional spaces are equivalent to spectral containment (LinearMap.IsSymmetric.pointSpectrumIn_Iic_iff, LinearMap.IsSymmetric.pointSpectrumIn_Ici_iff). The theorem is a consequence of the separated Sylvester bound ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_re_inner_le_of_le_re_inner.

Main results #

References #

Acknowledgements #

Material in the Sylvester and sin Θ lineage was adapted from the Spectra Formalization Project (Adam Bornemann; Apache-2.0) at upstream revision 8dbaaf6728d1342ae16acf79fd7eef7c59b37e63.

theorem Submodule.mul_norm_starProjection_comp_starProjection_le_norm_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U W : Submodule 𝕜 E) [U.HasOrthogonalProjection] [W.HasOrthogonalProjection] (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hW : ∀ x ∈ W, B x ∈ W) {c g : ℝ} (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBW : ∀ x ∈ W, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :

The dimension-free directed Davis–Kahan sin Θ theorem. Let U be invariant under A and W invariant under the symmetric operator B. If the quadratic form of A on U is at least c + g and that of B on W is at most c, then g ‖P_W P_U‖ ≤ ‖B - A‖. For g > 0 this bounds ‖P_W P_U‖ by ‖B - A‖ / g. Neither completeness nor finite dimension is assumed.

theorem Submodule.norm_starProjection_comp_starProjection_le_norm_sub_div {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U W : Submodule 𝕜 E) [U.HasOrthogonalProjection] [W.HasOrthogonalProjection] (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hW : ∀ x ∈ W, B x ∈ W) {c g : ℝ} (hg : 0 < g) (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBW : ∀ x ∈ W, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :

The directed Davis–Kahan sin Θ theorem in division form: for g > 0, under the hypotheses of mul_norm_starProjection_comp_starProjection_le_norm_sub, ‖P_W P_U‖ ≤ ‖B - A‖ / g.

theorem Submodule.mul_directedProjectionGap_le_norm_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c g : ℝ} (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :

The directed Davis–Kahan sin Θ theorem for the directed gap. Let U be invariant under A and V invariant under the symmetric operator B. If the quadratic form of A on U is at least c + g and that of B on Vᗮ is at most c, then the directed gap ‖P_{Vᗮ} P_U‖ from U to V satisfies g ‖P_{Vᗮ} P_U‖ ≤ ‖B - A‖.

theorem Submodule.directedProjectionGap_le_norm_sub_div {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c g : ℝ} (hg : 0 < g) (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :

The directed Davis–Kahan sin Θ theorem for the directed gap in division form: for g > 0, under the hypotheses of mul_directedProjectionGap_le_norm_sub, the directed gap from U to V is at most ‖B - A‖ / g.

theorem Submodule.mul_projectionGap_le_norm_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c c' g : ℝ} (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) (hBV' : ∀ x ∈ V, (c' + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B x) x)) (hAU' : ∀ x ∈ Uᗮ, RCLike.re (inner 𝕜 (A x) x) ≤ c' * ‖x‖ ^ 2) :

The dimension-free Davis–Kahan sin Θ theorem for the gap. Let U be invariant under the symmetric operator A and V invariant under the symmetric operator B. Suppose that the quadratic form of A on U is at least c + g while that of B on Vᗮ is at most c, and that the quadratic form of B on V is at least c' + g while that of A on Uᗮ is at most c'. Then the gap between U and V satisfies g ‖P_U - P_V‖ ≤ ‖B - A‖.

theorem Submodule.projectionGap_le_norm_sub_div {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c c' g : ℝ} (hg : 0 < g) (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) (hBV' : ∀ x ∈ V, (c' + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B x) x)) (hAU' : ∀ x ∈ Uᗮ, RCLike.re (inner 𝕜 (A x) x) ≤ c' * ‖x‖ ^ 2) :

The Davis–Kahan sin Θ theorem for the gap in division form: for g > 0, under the hypotheses of mul_projectionGap_le_norm_sub, ‖P_U - P_V‖ ≤ ‖B - A‖ / g.