The two blocks of a self-adjoint involution

Let Z be a self-adjoint unitary — equivalently Z⋆ = Z and Z² = 1 — and let U be an orthogonally complemented subspace. Read Z as a 2 × 2 matrix against U ⊕ Uᗮ:

Z = [[D₀, G⋆], [G, -D₁]].

This module records what Z² = 1 says about the four blocks, in the representation-free form

• D := U.diagonalPart Z — the block-diagonal part diag (D₀, -D₁);
• S := U.offDiagonalPart Z — the block-off-diagonal part, carrying G.

Then D and S are self-adjoint, D + S = Z, and

D² + S² = 1, D S + S D = 0.

Blockwise these are exactly D₀² + G⋆G = 1, D₁² + G G⋆ = 1 and D₁ G = G D₀, so the single pair of operator identities encodes the whole double-angle geometry of the reflected pair. For the Davis--Kahan reading D₀ = cos 2Θ₀, D₁ = cos 2Θ₁, |G| = sin 2Θ₀, and D² + S² = 1 is cos² 2Θ + sin² 2Θ = 1.

The kinship to ForTauCeti/Analysis/InnerProductSpace/DoubleAngle/Gram.lean is deliberate: there the same doubled-angle geometry appears as G⋆G = 4 M (1 - M) for M the principal-sine Gram operator of a rectangular cross block, here as G⋆G = 1 - D₀² for the cross block of a reflection. Both say that the Gram operator of a doubled-angle cross block is a scalar functional expression in the single-angle Gram operator.

Main results

• TauCeti.isSelfAdjoint_diagonalPart, TauCeti.isSelfAdjoint_offDiagonalPart.
• TauCeti.diagonalPart_sq_add_offDiagonalPart_sq: D² + S² = 1.
• TauCeti.diagonalPart_mul_offDiagonalPart_add_offDiagonalPart_mul_diagonalPart: D S + S D = 0.
• TauCeti.norm_sq_diagonalPart_add_norm_sq_offDiagonalPart_of_mem: the vector form ‖D x‖² + ‖S x‖² = ‖x‖² on U and on Uᗮ, proved from unitarity of Z alone.
• TauCeti.diagonalPart_mem_of_mem, TauCeti.offDiagonalPart_mem_orthogonal_of_mem and their mirrors: D is even and S is odd for the splitting U ⊕ Uᗮ.

References

• C. Davis and W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1--46, Section 7 and the Appendix to Section 6: the reflection Z = 2Q - 1 through a reducing subspace, and the block system its commutation with the operator produces.

theorem TauCeti.starProjection_orthogonal_eq_zero_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [Uᗮ.HasOrthogonalProjection] {x : E} (hx : x ∈ U) : Uᗮ.starProjection x = 0

The complementary projection kills a vector of U.

theorem TauCeti.diagonalPart_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ U) : (U.diagonalPart Z) x = U.starProjection (Z x)

On U the diagonal part of Z is the U-component of Z x.

theorem TauCeti.diagonalPart_apply_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ Uᗮ) : (U.diagonalPart Z) x = Uᗮ.starProjection (Z x)

On Uᗮ the diagonal part of Z is the Uᗮ-component of Z x.

theorem TauCeti.offDiagonalPart_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ U) : (U.offDiagonalPart Z) x = Uᗮ.starProjection (Z x)

On U the off-diagonal part of Z is the Uᗮ-component of Z x.

theorem TauCeti.offDiagonalPart_apply_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ Uᗮ) : (U.offDiagonalPart Z) x = U.starProjection (Z x)

On Uᗮ the off-diagonal part of Z is the U-component of Z x.

theorem TauCeti.diagonalPart_mem_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ U) : (U.diagonalPart Z) x ∈ U

The diagonal part preserves U.

theorem TauCeti.diagonalPart_mem_orthogonal_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ Uᗮ) : (U.diagonalPart Z) x ∈ Uᗮ

The diagonal part preserves Uᗮ.

theorem TauCeti.offDiagonalPart_mem_orthogonal_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ U) : (U.offDiagonalPart Z) x ∈ Uᗮ

The off-diagonal part carries U into Uᗮ.

theorem TauCeti.offDiagonalPart_mem_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) {x : E} (hx : x ∈ Uᗮ) : (U.offDiagonalPart Z) x ∈ U

The off-diagonal part carries Uᗮ into U.

theorem TauCeti.diagonalPart_add_offDiagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (Z : E →L[𝕜] E) : U.diagonalPart Z + U.offDiagonalPart Z = Z

The two parts recompose the operator.

theorem TauCeti.diagonalPart_sq_add_offDiagonalPart_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {Z : E →L[𝕜] E} (hZ : Z * Z = 1) : U.diagonalPart Z * U.diagonalPart Z + U.offDiagonalPart Z * U.offDiagonalPart Z = 1

The double-angle Pythagorean identity, in operator form. If Z² = 1 then D² + S² = 1 for the two blocks of Z relative to U. Blockwise this is the pair D₀² + G⋆G = 1, D₁² + G G⋆ = 1.

theorem TauCeti.diagonalPart_mul_offDiagonalPart_add_offDiagonalPart_mul_diagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {Z : E →L[𝕜] E} (hZ : Z * Z = 1) : U.diagonalPart Z * U.offDiagonalPart Z + U.offDiagonalPart Z * U.diagonalPart Z = 0

The blocks of an involution anticommute. If Z² = 1 then D S + S D = 0; blockwise this is the intertwining relation D₁ G = G D₀, which is the double-angle content of the reflected pair.

theorem TauCeti.norm_sq_diagonalPart_add_norm_sq_offDiagonalPart_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] {Z : E →L[𝕜] E} (hZ : ∀ (v : E), ‖Z v‖ = ‖v‖) {x : E} (hx : x ∈ U) : ‖(U.diagonalPart Z) x‖ ^ 2 + ‖(U.offDiagonalPart Z) x‖ ^ 2 = ‖x‖ ^ 2

The vector double-angle Pythagoras identity on U. If Z preserves norms then ‖D x‖² + ‖S x‖² = ‖x‖² for x ∈ U: the two blocks of Z x are orthogonal. Blockwise this is D₀² + G⋆G = 1 tested at x.

theorem TauCeti.norm_sq_diagonalPart_add_norm_sq_offDiagonalPart_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] {Z : E →L[𝕜] E} (hZ : ∀ (v : E), ‖Z v‖ = ‖v‖) {x : E} (hx : x ∈ Uᗮ) : ‖(U.diagonalPart Z) x‖ ^ 2 + ‖(U.offDiagonalPart Z) x‖ ^ 2 = ‖x‖ ^ 2

The mirror of norm_sq_diagonalPart_add_norm_sq_offDiagonalPart_of_mem on Uᗮ: blockwise D₁² + G G⋆ = 1.

theorem TauCeti.isSelfAdjoint_diagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] [CompleteSpace E] {Z : E →L[𝕜] E} (hZ : IsSelfAdjoint Z) : IsSelfAdjoint (U.diagonalPart Z)

The diagonal part of a self-adjoint operator is self-adjoint.

theorem TauCeti.isSelfAdjoint_offDiagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] [CompleteSpace E] {Z : E →L[𝕜] E} (hZ : IsSelfAdjoint Z) : IsSelfAdjoint (U.offDiagonalPart Z)

The off-diagonal part of a self-adjoint operator is self-adjoint.