Common-gap stability of orthogonal projectors

Abstract

Coercive Sylvester estimates and the common-gap Davis–Kahan projector bound over arbitrary complete real or complex Hilbert spaces.

The scalar k has an RCLike structure, including the real and complex fields. ContinuousLinearMap(k,E,F) denotes bounded continuous k-linear maps from E to F; LinearMap(k,E,F) denotes algebraic k-linear maps. Every norm of a continuous linear map is its operator norm; vector norms are the given Hilbert norms. Inner products use the displayed scalar k, and re takes their real part. All displayed variables and typeclass assumptions are quantified.

For a projectable submodule U, P(U) denotes U.starProjection, the orthogonal projector regarded as a bounded endomorphism of the ambient space. Orthogonal(U) is U’s orthogonal complement. Comp denotes continuous-linear-map composition and agrees with multiplication of endomorphisms; the numeral one denotes the identity endomorphism. Real scalars in k-linear expressions use the canonical RCLike real embedding.

The full projector theorem allows arbitrary dimension, including zero-dimensional and infinite-dimensional ambient spaces, and zero, whole, or coincident subspaces. It assumes no equal-rank, finite-rank, simple-eigenvalue, operator-positivity, nonzero-subspace, or small-perturbation condition. The four quadratic-form bounds use the same real c and positive gap g. These are conditional form estimates; no spectral-measure or spectral-support conversion is asserted.

Theorem 1.1 (norm_le_of_abs_re_inner_map_self_le).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)]\forall (C:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (q:\mathbb{R}),((\mathrm{IsSymmetric}(C))\wedge (0\le q)\wedge (\forall (x:E),\left|\mathrm{re}(⟨C(x),x{⟩}_k)\right|\le (q)\cdot ({\Vert x\Vert }^2)))\Rightarrow \Vert C\Vert \le q$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.norm_le_of_abs_re_inner_map_self_le (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

TauCeti.ContinuousLinearMap.norm_le_of_abs_re_inner_map_self_le bounds a symmetric operator by its real quadratic form. Completeness is absent. The private correction-operator estimate norm_opNorm_smul_one_sub_le uses it in the Sylvester absorption argument.

Theorem 1.2 (le_div_of_comp_add_comp_eq_rectangular).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (w:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),\forall (F:{\mathrm{Type}}_w),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{NormedAddCommGroup}(F)][\mathrm{InnerProductSpace}(k,F)]\forall (A:\mathrm{ContinuousLinearMap}(k,F,F)),\forall (B:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (X:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (Y:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (N:(\mathrm{ContinuousLinearMap}(k,E,F))\to \mathbb{R}),\forall (d:\mathbb{R}),(((\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (h:\mathrm{ContinuousLinearMap}(k,E,F)),N(f+h)\le N(f)+N(h))\wedge (\forall (a:k),\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),N((a)\cdot (f))=(\Vert a\Vert )\cdot (N(f)))\wedge (\forall (C:\mathrm{ContinuousLinearMap}(k,F,F)),\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),N((C)\circ (f))\le (\Vert C\Vert )\cdot (N(f)))\wedge (\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (C:\mathrm{ContinuousLinearMap}(k,E,E)),N((f)\circ (C))\le (N(f))\cdot (\Vert C\Vert )))\wedge (\mathrm{IsSymmetric}(A))\wedge (\mathrm{IsSymmetric}(B))\wedge (0<d)\wedge (\forall (x:F),(d)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨A(x),x{⟩}_k))\wedge (\forall (x:E),(d)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨B(x),x{⟩}_k))\wedge ((A)\circ (X)+(X)\circ (B)=Y))\Rightarrow N(X)\le \frac{N(Y)}{(2)\cdot (d)}$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.le_div_of_comp_add_comp_eq_rectangular (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

TauCeti.ContinuousLinearMap.le_div_of_comp_add_comp_eq_rectangular bounds an arbitrary rectangular solution of A composed with X plus X composed with B equals Y. The real-valued functional N is subadditive, exactly homogeneous in the scalar norm, and bounded under left and right multiplication by the operator norm. No definiteness, completeness, equal carrier, or nonzero-solution assumption is imposed. The zero solution is treated separately. Correction operators yield absorption by twice the positive coercivity delta.

Theorem 1.3 (le_div_of_comp_sub_comp_eq_rectangular).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (w:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),\forall (F:{\mathrm{Type}}_w),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{NormedAddCommGroup}(F)][\mathrm{InnerProductSpace}(k,F)]\forall (A:\mathrm{ContinuousLinearMap}(k,F,F)),\forall (B:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (X:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (Y:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (N:(\mathrm{ContinuousLinearMap}(k,E,F))\to \mathbb{R}),\forall (c:\mathbb{R}),\forall (g:\mathbb{R}),(((\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (h:\mathrm{ContinuousLinearMap}(k,E,F)),N(f+h)\le N(f)+N(h))\wedge (\forall (a:k),\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),N((a)\cdot (f))=(\Vert a\Vert )\cdot (N(f)))\wedge (\forall (C:\mathrm{ContinuousLinearMap}(k,F,F)),\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),N((C)\circ (f))\le (\Vert C\Vert )\cdot (N(f)))\wedge (\forall (f:\mathrm{ContinuousLinearMap}(k,E,F)),\forall (C:\mathrm{ContinuousLinearMap}(k,E,E)),N((f)\circ (C))\le (N(f))\cdot (\Vert C\Vert )))\wedge (\mathrm{IsSymmetric}(A))\wedge (\mathrm{IsSymmetric}(B))\wedge (0<g)\wedge (\forall (x:F),(c+g)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨A(x),x{⟩}_k))\wedge (\forall (x:E),\mathrm{re}(⟨B(x),x{⟩}_k)\le (c)\cdot ({\Vert x\Vert }^2))\wedge ((A)\circ (X)-(X)\circ (B)=Y))\Rightarrow N(X)\le \frac{N(Y)}{g}$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.le_div_of_comp_sub_comp_eq_rectangular (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

TauCeti.ContinuousLinearMap.le_div_of_comp_sub_comp_eq_rectangular applies the preceding estimate after shifting at the midpoint c plus g divided by two. The upper bound for B is c and the lower bound for A is c plus g. All four assumptions on the rectangular functional N remain explicit.

Theorem 1.4 (opNorm_le_div_of_comp_sub_comp_eq).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (w:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),\forall (F:{\mathrm{Type}}_w),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{NormedAddCommGroup}(F)][\mathrm{InnerProductSpace}(k,F)]\forall (A:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (B:\mathrm{ContinuousLinearMap}(k,F,F)),\forall (X:\mathrm{ContinuousLinearMap}(k,F,E)),\forall (Y:\mathrm{ContinuousLinearMap}(k,F,E)),\forall (c:\mathbb{R}),\forall (g:\mathbb{R}),((\mathrm{IsSymmetric}(A))\wedge (\mathrm{IsSymmetric}(B))\wedge (0<g)\wedge (\forall (x:E),(c+g)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨A(x),x{⟩}_k))\wedge (\forall (x:F),\mathrm{re}(⟨B(x),x{⟩}_k)\le (c)\cdot ({\Vert x\Vert }^2))\wedge ((A)\circ (X)-(X)\circ (B)=Y))\Rightarrow \Vert X\Vert \le \frac{\Vert Y\Vert }{g}$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.opNorm_le_div_of_comp_sub_comp_eq (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

TauCeti.ContinuousLinearMap.opNorm_le_div_of_comp_sub_comp_eq specializes the separated rectangular estimate to the operator norm. The source and target are independently quantified normed inner-product spaces over the same k, without completeness assumptions.

Theorem 1.5 (re_inner_reducedExtension_self).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)]\forall (R:\mathrm{LinearMap}(k,E,E)),\forall (W:\mathrm{Submodule}(k,E)),[\mathrm{HasOrthogonalProjection}(W)]\forall (q:\mathbb{R}),\forall (x:E),(\forall (x:E),(x\in W)\Rightarrow R(x)\in W)\Rightarrow \mathrm{re}(⟨R(P(W)(x))+(\mathrm{ofReal}(q))\cdot (x-P(W)(x)),x{⟩}_k)=\mathrm{re}(⟨R(P(W)(x)),P(W)(x){⟩}_k)+(q)\cdot ({\Vert x-P(W)(x)\Vert }^2)$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.re_inner_reducedExtension_self (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

TauCeti.re_inner_reducedExtension_self splits the real quadratic form of a linear map on a projectable invariant subspace and a scalar action on its orthogonal complement. The map R is algebraic, need not be bounded or symmetric, and needs invariance only on W. The private bounded-map version re_inner_bounded_reducedExtension_self applies this identity to the reduced extensions in Submodule.sinTheta_directed_coercive.

Theorem 1.6 (norm_add_eq_max_of_block).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{CompleteSpace}(E)]\forall (P:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (A:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (B:\mathrm{ContinuousLinearMap}(k,E,E)),((\mathrm{IsSelfAdjoint}(P))\wedge (\mathrm{IsIdempotentElem}(P))\wedge (\forall (x:E),\Vert P(x)\Vert \le \Vert x\Vert )\wedge (\forall (x:E),\Vert (1-P)(x)\Vert \le \Vert x\Vert )\wedge ((A)\circ (P)=A)\wedge ((P)\circ (A)=A)\wedge ((B)\circ (P)=0)\wedge ((P)\circ (B)=0))\Rightarrow \Vert A+B\Vert =\max (\Vert A\Vert ,\Vert B\Vert )$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.norm_add_eq_max_of_block (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

ContinuousLinearMap.norm_add_eq_max_of_block gives the exact maximum of the norms of two complementary supported blocks. Its hypotheses include self-adjointness, idempotence, contraction of P and one minus P, and all four left/right support equations. The Pythagorean split controls the upper bound and the support equations recover both lower bounds.

Theorem 1.7 (norm_starProjection_sub_eq_max).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{CompleteSpace}(E)]\forall (U:\mathrm{Submodule}(k,E)),\forall (V:\mathrm{Submodule}(k,E)),[\mathrm{HasOrthogonalProjection}(U)][\mathrm{HasOrthogonalProjection}(V)]\Vert P(U)-P(V)\Vert =\max (\Vert (1-P(V))\circ (P(U))\Vert ,\Vert (1-P(U))\circ (P(V))\Vert )$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.norm_starProjection_sub_eq_max (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

Submodule.norm_starProjection_sub_eq_max expresses the symmetric projector distance as the maximum of its two directed cross-projection norms. It uses ContinuousLinearMap.norm_add_eq_max_of_block and the C-star norm identities. It requires no rank or nonzero-subspace restriction.

Theorem 1.8 (sinTheta_directed_coercive).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (E:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(E)][\mathrm{InnerProductSpace}(k,E)][\mathrm{CompleteSpace}(E)]\forall (A:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (B:\mathrm{ContinuousLinearMap}(k,E,E)),\forall (U:\mathrm{Submodule}(k,E)),\forall (V:\mathrm{Submodule}(k,E)),[\mathrm{HasOrthogonalProjection}(U)][\mathrm{HasOrthogonalProjection}(V)]\forall (c:\mathbb{R}),\forall (g:\mathbb{R}),((\mathrm{IsSymmetric}(A))\wedge (\mathrm{IsSymmetric}(B))\wedge ((\forall (x:E),(x\in U)\Rightarrow A(x)\in U)\wedge (\forall (x:E),(x\in \mathrm{Orthogonal}(U))\Rightarrow A(x)\in \mathrm{Orthogonal}(U)))\wedge ((\forall (x:E),(x\in V)\Rightarrow B(x)\in V)\wedge (\forall (x:E),(x\in \mathrm{Orthogonal}(V))\Rightarrow B(x)\in \mathrm{Orthogonal}(V)))\wedge (0<g)\wedge (\forall (x:E),(x\in U)\Rightarrow (c+g)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨A(x),x{⟩}_k))\wedge (\forall (x:E),(x\in V)\Rightarrow \mathrm{re}(⟨B(x),x{⟩}_k)\le (c)\cdot ({\Vert x\Vert }^2)))\Rightarrow \Vert (P(V))\circ (P(U))\Vert \le \frac{\Vert B-A\Vert }{g}$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.sinTheta_directed_coercive (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

Submodule.sinTheta_directed_coercive forms reduced extensions on U and V. The two operators preserve their respective subspaces and orthogonal complements. Projection commutation gives a Sylvester equation for the cross projection, and perturbation compression bounds its forcing term by the norm of B minus A. Only the lower form bound on U and the upper form bound on V are required here.

Theorem 1.9 (opNorm_starProjection_sub_le_of_coercive).

$$\forall (u:\mathrm{UniverseLevel}()),\forall (v:\mathrm{UniverseLevel}()),\forall (k:{\mathrm{Type}}_u),\forall (H:{\mathrm{Type}}_v),[\mathrm{RCLike}(k)][\mathrm{NormedAddCommGroup}(H)][\mathrm{InnerProductSpace}(k,H)][\mathrm{CompleteSpace}(H)]\forall (A:\mathrm{ContinuousLinearMap}(k,H,H)),\forall (B:\mathrm{ContinuousLinearMap}(k,H,H)),\forall (U:\mathrm{Submodule}(k,H)),\forall (W:\mathrm{Submodule}(k,H)),[\mathrm{HasOrthogonalProjection}(U)][\mathrm{HasOrthogonalProjection}(W)]\forall (c:\mathbb{R}),\forall (g:\mathbb{R}),((\mathrm{IsSymmetric}(A))\wedge (\mathrm{IsSymmetric}(B))\wedge ((\forall (x:H),(x\in U)\Rightarrow A(x)\in U)\wedge (\forall (x:H),(x\in \mathrm{Orthogonal}(U))\Rightarrow A(x)\in \mathrm{Orthogonal}(U)))\wedge ((\forall (x:H),(x\in W)\Rightarrow B(x)\in W)\wedge (\forall (x:H),(x\in \mathrm{Orthogonal}(W))\Rightarrow B(x)\in \mathrm{Orthogonal}(W)))\wedge (0<g)\wedge (\forall (x:H),(x\in U)\Rightarrow (c+g)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨A(x),x{⟩}_k))\wedge (\forall (x:H),(x\in \mathrm{Orthogonal}(U))\Rightarrow \mathrm{re}(⟨A(x),x{⟩}_k)\le (c)\cdot ({\Vert x\Vert }^2))\wedge (\forall (x:H),(x\in W)\Rightarrow (c+g)\cdot ({\Vert x\Vert }^2)\le \mathrm{re}(⟨B(x),x{⟩}_k))\wedge (\forall (x:H),(x\in \mathrm{Orthogonal}(W))\Rightarrow \mathrm{re}(⟨B(x),x{⟩}_k)\le (c)\cdot ({\Vert x\Vert }^2)))\Rightarrow \Vert P(U)-P(W)\Vert \le \frac{\Vert B-A\Vert }{g}$$

Proof. Machine-checked in Lean as D5/S3/HilbertOperators/DavisKahanProjector.opNorm_starProjection_sub_le_of_coercive (✓ std3). ∎

Citation. Jon Crall, GPT 5.6 High, Claude Fable 5, and Claude Opus 5 (2026). Coercive Sylvester estimates and common-gap Davis–Kahan projector bounds. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8/LeanPool/DavisKahan/ForTauCeti/Analysis/InnerProductSpace/BoundedOperator/Projector.lean.

Commentary.

Submodule.opNorm_starProjection_sub_le_of_coercive is the common-gap projector theorem. Apply Submodule.sinTheta_directed_coercive to U and the orthogonal complement of W, then to W and the orthogonal complement of U, and combine the two estimates with Submodule.norm_starProjection_sub_eq_max. The constant is one, with denominator g.

References

• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.le_div_of_comp_add_comp_eq_rectangular
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.le_div_of_comp_sub_comp_eq_rectangular
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.norm_add_eq_max_of_block
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.norm_le_of_abs_re_inner_map_self_le
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.norm_starProjection_sub_eq_max
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.opNorm_le_div_of_comp_sub_comp_eq
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.opNorm_starProjection_sub_le_of_coercive
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.re_inner_reducedExtension_self
• Truth anchor: D5/S3/HilbertOperators/DavisKahanProjector.sinTheta_directed_coercive