Diagonal and off-diagonal blocks of an operator

Let U be a submodule of an inner product space E admitting an orthogonal projection P_U. Relative to the orthogonal decomposition E = U ⊕ Uᗮ, a bounded operator A on E is a 2 × 2 block operator. Its diagonal part U.diagBlock A = P_U A P_U + P_{Uᗮ} A P_{Uᗮ} keeps the U → U and Uᗮ → Uᗮ blocks, and its off-diagonal part U.offDiagBlock A = P_U A P_{Uᗮ} + P_{Uᗮ} A P_U keeps the Uᗮ → U and U → Uᗮ blocks.

Both parts are expressed through the reflection R_U = 2 P_U - 1 across U: conjugating by R_U fixes the diagonal blocks and negates the off-diagonal ones, so the two parts are the average and the half-difference of A and R_U A R_U. Since R_U is an isometry, these formulas turn operator-norm estimates for A into estimates for its blocks.

The reduced extension A.reducedExtension U κ applies A on U and extends it by scalar multiplication by κ on Uᗮ. Its quadratic form splits orthogonally when U is invariant.

Main definitions

• ContinuousLinearMap.reducedExtension A U κ: the reduced extension from U with scalar κ on Uᗮ.
• Submodule.diagBlock U A: the block-diagonal part of A relative to U ⊕ Uᗮ.
• Submodule.offDiagBlock U A: the off-diagonal part of A relative to U ⊕ Uᗮ.

Main results

• Submodule.diagBlock_add_offDiagBlock: the two parts sum to A.
• Submodule.diagBlock_diagBlock, Submodule.offDiagBlock_offDiagBlock, Submodule.diagBlock_offDiagBlock, Submodule.offDiagBlock_diagBlock: taking either part is idempotent, and each part annihilates the other.
• Submodule.two_smul_diagBlock: 2 • U.diagBlock A = A + R_U A R_U.
• Submodule.two_smul_offDiagBlock: 2 • U.offDiagBlock A = A - R_U A R_U.
• Submodule.commute_reflection_iff: R_U commutes with A exactly when P_U does.
• Submodule.offDiagBlock_eq_zero_iff, Submodule.diagBlock_eq_self_iff: A is block diagonal exactly when P_U commutes with A.
• ContinuousLinearMap.reducedExtension_def, ContinuousLinearMap.eq_reducedExtension_iff: its operator equation and characterization by its actions on the two blocks.
• ContinuousLinearMap.re_inner_reducedExtension_self: its orthogonal form splitting.
• ContinuousLinearMap.le_re_inner_reducedExtension_self, ContinuousLinearMap.re_inner_reducedExtension_self_le: a local lower (upper) bound r extends to the whole space when r ≤ κ (respectively κ ≤ r).

References

• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970).

Acknowledgements

The block-diagonal extension lemmas belong to the sin Θ lineage adapted from the Spectra Formalization Project (Adam Bornemann; Apache-2.0) at upstream revision 8dbaaf6728d1342ae16acf79fd7eef7c59b37e63. The reduced-extension specialization is also present in the maintained AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0), at ForTauCeti/Analysis/InnerProductSpace/ReducedExtension.lean.

noncomputable def ContinuousLinearMap.reducedExtension {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) : E →L[𝕜] E

Extend A from the selected block U by the scalar κ on Uᗮ. It agrees with A on U and acts as scalar multiplication by κ on Uᗮ.

theorem ContinuousLinearMap.reducedExtension_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) : A.reducedExtension U κ = A ∘SL U.starProjection + ↑κ • Uᗮ.starProjection

The reduced extension applies A after projection onto U, plus κ times the projection onto Uᗮ.

theorem ContinuousLinearMap.reducedExtension_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) (x : E) : (A.reducedExtension U κ) x = A (U.starProjection x) + ↑κ • Uᗮ.starProjection x

The reduced extension acts blockwise on an arbitrary vector.

@[simp]

theorem ContinuousLinearMap.reducedExtension_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) {x : E} (hx : x ∈ U) : (A.reducedExtension U κ) x = A x

On the selected subspace, the reduced extension agrees with the original operator.

@[simp]

theorem ContinuousLinearMap.reducedExtension_apply_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) {x : E} (hx : x ∈ Uᗮ) : (A.reducedExtension U κ) x = ↑κ • x

On the orthogonal block, the reduced extension acts by the scalar κ.

theorem ContinuousLinearMap.eq_reducedExtension_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (B A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (κ : ℝ) : B = A.reducedExtension U κ ↔ (∀ x ∈ U, B x = A x) ∧ ∀ x ∈ Uᗮ, B x = ↑κ • x

A continuous linear map is the reduced extension of A precisely when it agrees with A on U and acts as multiplication by κ on Uᗮ.

theorem ContinuousLinearMap.re_inner_reducedExtension_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : ∀ x ∈ U, A x ∈ U) (κ : ℝ) (x : E) : RCLike.re (inner 𝕜 ((A.reducedExtension U κ) x) x) = RCLike.re (inner 𝕜 (A (U.starProjection x)) (U.starProjection x)) + κ * ‖Uᗮ.starProjection x‖ ^ 2

For an invariant block U, the form of A P_U + κ P_{Uᗮ} splits orthogonally into the form of A on U and the scalar form on Uᗮ.

theorem ContinuousLinearMap.le_re_inner_reducedExtension_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : ∀ x ∈ U, A x ∈ U) {r κ : ℝ} (hκ : r ≤ κ) (hA : ∀ x ∈ U, r * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (x : E) : r * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 ((A.reducedExtension U κ) x) x)

A local lower bound r extends to the reduced extension whenever the complementary-block scalar satisfies r ≤ κ.

theorem ContinuousLinearMap.re_inner_reducedExtension_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (B : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : ∀ x ∈ U, B x ∈ U) {r κ : ℝ} (hκ : κ ≤ r) (hB : ∀ x ∈ U, RCLike.re (inner 𝕜 (B x) x) ≤ r * ‖x‖ ^ 2) (x : E) : RCLike.re (inner 𝕜 ((B.reducedExtension U κ) x) x) ≤ r * ‖x‖ ^ 2

A local upper bound r extends to the reduced extension whenever the complementary-block scalar satisfies κ ≤ r.

noncomputable def Submodule.diagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : E →L[𝕜] E

The block-diagonal part P_U A P_U + P_{Uᗮ} A P_{Uᗮ} of an operator A relative to the orthogonal decomposition E = U ⊕ Uᗮ.

noncomputable def Submodule.offDiagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : E →L[𝕜] E

The off-diagonal part P_U A P_{Uᗮ} + P_{Uᗮ} A P_U of an operator A relative to the orthogonal decomposition E = U ⊕ Uᗮ.

theorem Submodule.diagBlock_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagBlock A = U.starProjection ∘SL A ∘SL U.starProjection + Uᗮ.starProjection ∘SL A ∘SL Uᗮ.starProjection

theorem Submodule.offDiagBlock_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.offDiagBlock A = U.starProjection ∘SL A ∘SL Uᗮ.starProjection + Uᗮ.starProjection ∘SL A ∘SL U.starProjection

@[simp]

theorem Submodule.diagBlock_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A B : E →L[𝕜] E) : U.diagBlock (A + B) = U.diagBlock A + U.diagBlock B

Taking the diagonal part is additive.

@[simp]

theorem Submodule.diagBlock_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (c : 𝕜) (A : E →L[𝕜] E) : U.diagBlock (c • A) = c • U.diagBlock A

Taking the diagonal part commutes with scalar multiplication.

@[simp]

theorem Submodule.offDiagBlock_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A B : E →L[𝕜] E) : U.offDiagBlock (A + B) = U.offDiagBlock A + U.offDiagBlock B

Taking the off-diagonal part is additive.

@[simp]

theorem Submodule.offDiagBlock_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (c : 𝕜) (A : E →L[𝕜] E) : U.offDiagBlock (c • A) = c • U.offDiagBlock A

Taking the off-diagonal part commutes with scalar multiplication.

@[simp]

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

@[simp]

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

@[simp]

theorem Submodule.diagBlock_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagBlock (-A) = -U.diagBlock A

Taking the diagonal part commutes with negation.

@[simp]

theorem Submodule.offDiagBlock_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.offDiagBlock (-A) = -U.offDiagBlock A

Taking the off-diagonal part commutes with negation.

@[simp]

theorem Submodule.diagBlock_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A B : E →L[𝕜] E) : U.diagBlock (A - B) = U.diagBlock A - U.diagBlock B

Taking the diagonal part commutes with subtraction.

@[simp]

theorem Submodule.offDiagBlock_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A B : E →L[𝕜] E) : U.offDiagBlock (A - B) = U.offDiagBlock A - U.offDiagBlock B

Taking the off-diagonal part commutes with subtraction.

@[simp]

theorem Submodule.diagBlock_add_offDiagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagBlock A + U.offDiagBlock A = A

Every operator is the sum of its diagonal and off-diagonal parts.

theorem Submodule.two_smul_diagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : 2 • U.diagBlock A = A + ↑↑U.reflection ∘SL A ∘SL ↑↑U.reflection

The diagonal part of A is the average of A and its conjugate R_U A R_U by the reflection across U.

theorem Submodule.two_smul_offDiagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : 2 • U.offDiagBlock A = A - ↑↑U.reflection ∘SL A ∘SL ↑↑U.reflection

The off-diagonal part of A is half the difference of A and its conjugate R_U A R_U by the reflection across U.

theorem Submodule.commute_reflection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : Commute (↑↑U.reflection) A ↔ Commute U.starProjection A

The reflection across U commutes with an operator exactly when the orthogonal projection onto U does, that is, exactly when U reduces the operator.

theorem LinearMap.IsSymmetric.commute_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} (hA : (↑A).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) : Commute (↑↑U.reflection) A

Reflection across an invariant subspace commutes with a symmetric operator.

@[simp]

theorem Submodule.offDiagBlock_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : U.offDiagBlock A = 0 ↔ Commute U.starProjection A

The off-diagonal part of A vanishes exactly when A commutes with the orthogonal projection onto U, that is, when A is block diagonal relative to U ⊕ Uᗮ.

@[simp]

theorem Submodule.diagBlock_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : U.diagBlock A = A ↔ Commute U.starProjection A

An operator equals its diagonal part exactly when it commutes with the orthogonal projection onto U.

theorem Submodule.commute_starProjection_diagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : Commute U.starProjection (U.diagBlock A)

The diagonal part of any operator commutes with the orthogonal projection onto U.

@[simp]

theorem Submodule.diagBlock_diagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagBlock (U.diagBlock A) = U.diagBlock A

The diagonal part of the diagonal part of A is the diagonal part of A.

@[simp]

theorem Submodule.offDiagBlock_diagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.offDiagBlock (U.diagBlock A) = 0

The off-diagonal part of the diagonal part of A vanishes.

@[simp]

theorem Submodule.diagBlock_offDiagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagBlock (U.offDiagBlock A) = 0

The diagonal part of the off-diagonal part of A vanishes.

@[simp]

theorem Submodule.offDiagBlock_offDiagBlock {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.offDiagBlock (U.offDiagBlock A) = U.offDiagBlock A

The off-diagonal part of the off-diagonal part of A is the off-diagonal part of A.

@[simp]

theorem Submodule.diagBlock_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : Uᗮ.diagBlock A = U.diagBlock A

The diagonal part of A relative to Uᗮ ⊕ Uᗮᗮ is its diagonal part relative to U ⊕ Uᗮ.

@[simp]

theorem Submodule.offDiagBlock_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : Uᗮ.offDiagBlock A = U.offDiagBlock A

The off-diagonal part of A relative to Uᗮ ⊕ Uᗮᗮ is its off-diagonal part relative to U ⊕ Uᗮ.

theorem Submodule.lift_crossBlocks_eq_starProjection_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [FiniteDimensional 𝕜 E] (V : Submodule 𝕜 E) [V.HasOrthogonalProjection] : ↑↑↑(V.orthogonalDecomposition.trans (LinearIsometryEquiv.withLpProdComm 2 𝕜 ↥V ↥Vᗮ)).symm ∘ₗ LinearMap.withLpMap 2 ((↑Vᗮ.orthogonalProjectionOnto ∘ₗ U.subtype).prodMap (-LinearMap.adjoint (↑Uᗮ.orthogonalProjectionOnto ∘ₗ V.subtype))) ∘ₗ ↑↑↑U.orthogonalDecomposition = ↑U.starProjection - ↑V.starProjection

The two-block lift of the cross-projections P_{Vᗮ} |_U and -(P_{Uᗮ} |_V)ᴴ through the orthogonal decompositions is the difference of the projections P_U - P_V.

theorem Submodule.lift_residualBlocks_eq_comp_sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [FiniteDimensional 𝕜 E] {A B : E →L[𝕜] E} (hAB : (↑(A - B)).IsSymmetric) (V : Submodule 𝕜 E) [V.HasOrthogonalProjection] : ↑↑↑(V.orthogonalDecomposition.trans (LinearIsometryEquiv.withLpProdComm 2 𝕜 ↥V ↥Vᗮ)).symm ∘ₗ LinearMap.withLpMap 2 ((↑Vᗮ.orthogonalProjectionOnto ∘ₗ ↑(B - A) ∘ₗ U.subtype).prodMap (LinearMap.adjoint (↑Uᗮ.orthogonalProjectionOnto ∘ₗ ↑(A - B) ∘ₗ V.subtype))) ∘ₗ ↑↑↑U.orthogonalDecomposition = ↑(B - A) ∘ₗ ↑U.starProjection - ↑V.starProjection ∘ₗ ↑(B - A)

The two-block lift of the residual blocks P_{Vᗮ} (B - A) |_U and (P_{Uᗮ} (A - B) |_V)ᴴ through the orthogonal decompositions is the checkerboard residual (B - A) P_U - P_V (B - A).