TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

An invertible leading block yields block LU through its Schur complement

Statement

Let

$A = (\begin{array}{cc} A_{11} & A_{12} \\ A_{21} & A_{22} \end{array})$

be a square block matrix over a field, with $A_{11}$ square and invertible, and let $S : = A_{22} - A_{21} A_{11}^{- 1} A_{12}$ .

One has the exact block factorisation $A = (\begin{array}{cc} I & 0 \\ A_{21} A_{11}^{- 1} & I \end{array}) (\begin{array}{cc} A_{11} & A_{12} \\ 0 & S \end{array}) .$
If $S = \tilde{L} \tilde{U}$ is any normalised LU factorisation, then $A = (\begin{array}{cc} I & 0 \\ A_{21} A_{11}^{- 1} & \tilde{L} \end{array}) (\begin{array}{cc} A_{11} & A_{12} \\ 0 & \tilde{U} \end{array})$ is a block LU factorisation across the same partition.

Facts & Assumptions

Given: The displayed block matrix $A$ , an invertible leading block $A_{11}$ , and the Schur complement $S = A_{22} - A_{21} A_{11}^{- 1} A_{12}$ .

[L1]

Block LU factorisation and Schur complement are defined as in Block LU factorisation and the associated Schur complement.

[L2]

Triangular solves with nonzero diagonal are correct and unique (Forward and backward substitution are correct, unique, and quadratic in scalar operations).

[L3]

An invertible matrix has a two-sided inverse (Invertible matrices and the general linear group ${GL}_{n} (F)$ ).

[L4]

Matrix multiplication is associative and uses the product convention of Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

Proof

technique · explicit block multiplication

1.1

By [L3], $A_{11}^{- 1}$ exists, and by [L4] the block product $(\begin{array}{cc} I & 0 \\ A_{21} A_{11}^{- 1} & I \end{array}) (\begin{array}{cc} A_{11} & A_{12} \\ 0 & S \end{array})$ has upper-left block $A_{11}$ , upper-right block $A_{12}$ , lower-left block $A_{21} A_{11}^{- 1} A_{11} = A_{21}$ , and lower-right block $A_{21} A_{11}^{- 1} A_{12} + S = A_{22}$ . Hence it equals $A$ .

L1L3L4algebra

2.1

If $S = \tilde{L} \tilde{U}$ , substitute this into step 1.1 and absorb the factorisation of $S$ into the lower-right block. The resulting left factor is block lower triangular and the right factor is block upper triangular, so this is a block LU factorisation in the sense of [L1].

step 1.1L1algebra

2.2

The off-diagonal block $A_{21} A_{11}^{- 1}$ is exactly the block of multipliers obtained by solving $X A_{11} = A_{21}$ . If $A_{11}$ itself has a triangular factorisation, [L2] computes these multipliers by triangular solves.

L2step 1.1

3.1

Steps 1.1 and 2.1 prove claims 1 and 2, and step 2.2 identifies the solve interpretation of the multiplier block.

step 1.1step 2.1step 2.2∎

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

David Bindel, CS 4220: Numerical Analysis, Blocked LU and Cholesky (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Section 2.6 (standard reference, not scraped)