Contents
Given a matrix its Cholesky
factorization is given by where is LowerTriangular. Matrix is called the Cholesky
factor of matrix .
Cholesky Factorization Theorem: Let be a SymmetricPositiveDefinite
matrix. Then there exists a LowerTriangular
matrix such that . If the diagonal of is taken to be positive, the
factorization is unique. 
The Cholesky
factorization is commonly used when solving a square SystemOfLinearEquations
where SymmetricPositiveDefinite
matrix and are given and is to be computed. If , then
·
means
·
or
·
so that can be computed by first solving the LowerTriangularSystem of equations (often referred to as ForwardSubstitution) and then solving the
UpperTriangularSystem (often referred to as BackwardSubstitution).
denotes the operation that overwrites the Lowertriangular part of with the LowerTriangular
matrix .
The PME for this operation is given by
·
Details of how to derive the PME
for this operation.
The dependencies in the above PME allow for
three different loopinvariants to be identified:
Invariant 1 

Invariant 2 

