The reflection block system for an unbounded operator

Let A be a partial linear map reduced by U, let B be a bounded operator that is odd for the splitting U ⊕ Uᗮ (it exchanges the two summands), and let Z be a bounded operator that commutes with A + B on D(A) and preserves D(A). Writing

• C := U.diagonalPart Z (the even block of Z),
• S := U.offDiagonalPart Z (the odd block of Z),

this module proves the two facts the unbounded double-angle theory rests on.

Domain control

C and S preserve D(A). In blocks, with Z = [[D₀, G⋆], [G, -D₁]], this is exactly

D₀ D(A₀) ⊆ D(A₀), G D(A₀) ⊆ D(A₁), G⋆ D(A₁) ⊆ D(A₀), D₁ D(A₁) ⊆ D(A₁),

the compatibility that is awkward to obtain when the four blocks are handled separately. It follows from Z D(A) ⊆ D(A) together with the reducing projections preserving D(A); nothing about the spectrum of A is used.

The Sylvester equation

On the whole of D(A),

A (S x) - S (A x) = C (B x) - B (C x).

This is the domain-correct, branch-free form of Davis--Kahan equation (7.6). Blockwise, on D(A₀), it reads

A₁ G - G A₀ = -D₁ B - B D₀,

an honest operator identity: every term is defined, by the domain inclusions above. No global |A|, no indefinite closed form, and no sign selection: the sign of cos 2θ is inside C x, and only C appears.

Main results

• TauCeti.mem_domain_diagonalPart, TauCeti.mem_domain_offDiagonalPart.
• TauCeti.sylvester_offDiagonalPart_of_mem and TauCeti.sylvester_offDiagonalPart_of_mem_orthogonal: the two block forms.
• TauCeti.sylvester_offDiagonalPart: the ambient identity on all of D(A).

References

• C. Davis and W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1--46: equation (7.6) and the Appendix to Section 6, where the unbounded extension is stated to be analogous but is not written out.

def TauCeti.IsOddFor {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (U : Submodule 𝕜 H) (B : H →L[𝕜] H) : Prop

B exchanges the two summands. This is the Davis--Kahan hypothesis H₀ = H₁ = 0: the perturbation is fully off-diagonal.

Equations

• TauCeti.IsOddFor U B = ((∀ x ∈ U, B x ∈ Uᗮ) ∧ ∀ x ∈ Uᗮ, B x ∈ U)

theorem TauCeti.mem_domain_diagonalPart {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {A : H →ₗ.[𝕜] H} {U : Submodule 𝕜 H} [U.HasOrthogonalProjection] {Z : H →L[𝕜] H} (hred : LinearPMap.ReducesSubspace A U) (hZ : LinearPMap.MapsDomainTo A A Z) (x : ↥A.domain) : (U.diagonalPart Z) ↑x ∈ A.domain

The even block preserves the domain.

theorem TauCeti.mem_domain_offDiagonalPart {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {A : H →ₗ.[𝕜] H} {U : Submodule 𝕜 H} [U.HasOrthogonalProjection] {Z : H →L[𝕜] H} (hred : LinearPMap.ReducesSubspace A U) (hZ : LinearPMap.MapsDomainTo A A Z) (x : ↥A.domain) : (U.offDiagonalPart Z) ↑x ∈ A.domain

The odd block preserves the domain.

theorem TauCeti.sylvester_offDiagonalPart_of_mem {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {A : H →ₗ.[𝕜] H} {U : Submodule 𝕜 H} [U.HasOrthogonalProjection] {B Z : H →L[𝕜] H} (hred : LinearPMap.ReducesSubspace A U) (hB : IsOddFor U B) (hZdom : LinearPMap.MapsDomainTo A A Z) (hZcomm : ∀ (x : ↥A.domain), ↑A ⟨Z ↑x, ⋯⟩ + B (Z ↑x) = Z (↑A x) + Z (B ↑x)) (x : ↥A.domain) (hx : ↑x ∈ U) : ↑A ⟨(U.offDiagonalPart Z) ↑x, ⋯⟩ + B ((U.diagonalPart Z) ↑x) = (U.offDiagonalPart Z) (↑A x) + (U.diagonalPart Z) (B ↑x)

Equation (7.6) for an unbounded operator, on D(A₀).

For x in the domain and in U,

A (S x) - S (A x) = C (B x) - B (C x),

which in blocks is A₁ G x - G A₀ x = -D₁ B x - B D₀ x. Every term is defined: S x ∈ D(A) ∩ Uᗮ and C x ∈ D(A) ∩ U by mem_domain_offDiagonalPart and mem_domain_diagonalPart.

theorem TauCeti.sylvester_offDiagonalPart_of_mem_orthogonal {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {A : H →ₗ.[𝕜] H} {U : Submodule 𝕜 H} [U.HasOrthogonalProjection] {B Z : H →L[𝕜] H} (hred : LinearPMap.ReducesSubspace A U) (hB : IsOddFor U B) (hZdom : LinearPMap.MapsDomainTo A A Z) (hZcomm : ∀ (x : ↥A.domain), ↑A ⟨Z ↑x, ⋯⟩ + B (Z ↑x) = Z (↑A x) + Z (B ↑x)) (x : ↥A.domain) (hx : ↑x ∈ Uᗮ) : ↑A ⟨(U.offDiagonalPart Z) ↑x, ⋯⟩ + B ((U.diagonalPart Z) ↑x) = (U.offDiagonalPart Z) (↑A x) + (U.diagonalPart Z) (B ↑x)

Equation (7.6) for an unbounded operator, on D(A₁). The mirror of sylvester_offDiagonalPart_of_mem, with the same conclusion.

theorem TauCeti.sylvester_offDiagonalPart {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {A : H →ₗ.[𝕜] H} {U : Submodule 𝕜 H} [U.HasOrthogonalProjection] {B Z : H →L[𝕜] H} (hred : LinearPMap.ReducesSubspace A U) (hB : IsOddFor U B) (hZdom : LinearPMap.MapsDomainTo A A Z) (hZcomm : ∀ (x : ↥A.domain), ↑A ⟨Z ↑x, ⋯⟩ + B (Z ↑x) = Z (↑A x) + Z (B ↑x)) (x : ↥A.domain) : ↑A ⟨(U.offDiagonalPart Z) ↑x, ⋯⟩ + B ((U.diagonalPart Z) ↑x) = (U.offDiagonalPart Z) (↑A x) + (U.diagonalPart Z) (B ↑x)

Equation (7.6) for an unbounded operator, on all of D(A).

A (S x) - S (A x) = C (B x) - B (C x), with every term defined by the domain inclusions. Branch-free: no sign of cos 2θ is selected anywhere, because the sign is absorbed into C x.