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.
Normalised LU and LDU factorisations with nonzero pivots are unique
Statement
Let be a field, let , and let .
- Suppose where are unit lower triangular and are upper triangular with nonzero diagonal. Then and .
- Suppose where are unit lower triangular, are diagonal with nonzero diagonal entries, and are unit upper triangular. Then , , and .
Facts & Assumptions
Given: A field , a natural number , a matrix , and two factorisations of of the shapes named in the statement.
A normalised LU factorisation is with unit lower triangular and upper triangular; an LDU factorisation is with unit lower triangular, diagonal, and unit upper triangular (A normalised LU factorisation has a unit lower-triangular L and an upper-triangular U, An LDU factorisation has unit lower-triangular L, diagonal D, and unit upper-triangular U).
Matrix multiplication is the product convention used throughout (Rectangular matrix multiplication and the identity matrix , including zero-sized shapes).
Proof
For claim 1, the first row of equals the first row of both and , because the first rows of and are . Hence the first rows of and agree, in particular . Then the first-column equations are for , so . Subtracting the common first-column outer product leaves two factorizations of the same trailing principal block by unit lower and upper triangular matrices of size with nonzero diagonal. Induction gives equality of the trailing blocks, hence and .
For claim 2, put and . Because are diagonal and are unit upper triangular, are upper triangular and their diagonals are exactly the diagonals of , so they are nonzero. The factorisations are therefore of the kind handled in step 1.1, which gives and . Taking diagonals of yields , and then forces .
Steps 1.1 and 2.1 prove claims 1 and 2. The nonzero-pivot hypothesis is essential: without it, a zero row of the upper factor leaves lower-triangular multipliers undetermined.
Depends on
Used by
Dependency tree · two levels
6 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)