Example: Cholesky factorization

choleskySpec A returns the lower-triangular $L$ with $A=LL^\mathsf{T}$ for a symmetric positive-definite A. Here we factor a 3×3 SPD matrix and check the reconstruction error.

def NN.Examples.Factorization.Cholesky.A : Spec.Tensor Float (Spec.Shape.dim 3 (Spec.Shape.dim 3 Spec.Shape.scalar))

A symmetric positive-definite test matrix.

def NN.Examples.Factorization.Cholesky.L : Spec.Tensor Float (Spec.Shape.dim 3 (Spec.Shape.dim 3 Spec.Shape.scalar))

The Cholesky factor L (lower-triangular).

def NN.Examples.Factorization.Cholesky.reconErr : Float

Reconstruction error $\lVert A-LL^\mathsf{T}\rVert_{\max}$.

Negative control: the positive-pivot hypothesis is necessary

isCholesky_of_pos requires the executable pivots $L_{jj}$ to be positive (0 < choleskyFn A j j), which is exactly the success condition over the reals (SPD is the expected — but here unformalized — sufficient condition for it). The matrix below is symmetric but not positive-definite (eigenvalues 3 and -1), so a pivot is non-positive, the diagonal step takes √(negative), and the reconstruction is NaN — never a small error. This documents that the hypothesis genuinely bites.

def NN.Examples.Factorization.Cholesky.Abad : Spec.Tensor Float (Spec.Shape.dim 2 (Spec.Shape.dim 2 Spec.Shape.scalar))

A symmetric but indefinite matrix (eigenvalues {3, -1}), outside Cholesky's domain.

def NN.Examples.Factorization.Cholesky.Lbad : Spec.Tensor Float (Spec.Shape.dim 2 (Spec.Shape.dim 2 Spec.Shape.scalar))

def NN.Examples.Factorization.Cholesky.reconErrBad : Float