Schur Complement Associativity

Abstract

Sequential and one-shot Schur elimination give the same retained operator.

Theorem 1.1 (Sequential elimination equals one-shot elimination).

$$\forall H0\in \mathrm{Type}\left(\right),H1\in \mathrm{Type}\left(\right),H2\in \mathrm{Type}\left(\right),A00\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H0,H0\right),A01\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H1,H0\right),A02\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H2,H0\right),A10\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H0,H1\right),A11\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H1,H1\right),A12\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H2,H1\right),A20\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H0,H2\right),A21\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H1,H2\right),A22\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H2,H2\right),A22Inv\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H2,H2\right),reducedA11Inv\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},H1,H1\right),lowerInv\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{Prod}\left(H1,H2\right),\mathrm{Prod}\left(H1,H2\right)\right),\left(\mathrm{NormedAddCommGroup}\left(H0\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathbb{C},H0\right)\wedge \left(\mathrm{CompleteSpace}\left(H0\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(H1\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathbb{C},H1\right)\wedge \left(\mathrm{CompleteSpace}\left(H1\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(H2\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathbb{C},H2\right)\wedge \left(\mathrm{CompleteSpace}\left(H2\right)\wedge \left(\mathrm{comp}\left(A22Inv,A22\right)=\mathrm{id}\left(\mathbb{C},H2\right)\wedge \left(\mathrm{comp}\left(reducedA11Inv,A11-\mathrm{comp}\left(A12,\mathrm{comp}\left(A22Inv,A21\right)\right)\right)=\mathrm{id}\left(\mathbb{C},H1\right)\wedge \mathrm{comp}\left(\mathrm{prod}\left(\mathrm{coprod}\left(A11,A12\right),\mathrm{coprod}\left(A21,A22\right)\right),lowerInv\right)=\mathrm{id}\left(\mathbb{C},\mathrm{Prod}\left(H1,H2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow A00-\mathrm{comp}\left(A02,\mathrm{comp}\left(A22Inv,A20\right)\right)-\mathrm{comp}\left(A01-\mathrm{comp}\left(A02,\mathrm{comp}\left(A22Inv,A21\right)\right),\mathrm{comp}\left(reducedA11Inv,A10-\mathrm{comp}\left(A12,\mathrm{comp}\left(A22Inv,A20\right)\right)\right)\right)=A00-\mathrm{comp}\left(\mathrm{coprod}\left(A01,A02\right),\mathrm{comp}\left(lowerInv,\mathrm{prod}\left(A10,A20\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/SchurComplementAssociativity.schur_complement_associativity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let H0, H1, and H2 be complete complex inner-product spaces. Nine bounded maps are the blocks of an operator on their three-fold product.

Suppose the H2 block, the H1 block obtained after eliminating H2, and the combined lower block have the displayed inverse witnesses. Then sequentially eliminating H2 and H1 gives the same retained H0 operator as eliminating H1 times H2 in one step.

The proof applies the combined lower inverse to the retained column, solves its two block equations successively, and substitutes those solutions into the retained row.

References

• Truth anchor: D5/S3/Weil/ZetaLinear/SchurComplementAssociativity.schur_complement_associativity