Matrix Multiplication Forward and Mixed Error Analysis

This module establishes rigorous rounding error bounds for floating-point matrix operations, including matrix multiplication, scalar-matrix multiplication, matrix addition, and the general matrix multiply-accumulate (GEMM) operation.

Error Factors

Throughout, the accumulated relative error factor is \(g(n) = (1 + \mathbf{u})^n - 1\) and the mixed absolute error factor is \(g_1(n_1, n_2) = n_1 \cdot \eta \cdot (1 + g(n_2))\), where \(\mathbf{u}\) is the unit roundoff and \(\eta\) is the underflow threshold for the given type. Both are defined in common.

Error Bound Taxonomy

The theorems in this file fall into three categories: Pure forward error bounds characterize the absolute difference between the computed result and the exact result in terms of the input data. No reference is made to a nearby exact problem. Mixed forward-backward error bounds express the computed result as the exact result of a slightly perturbed input (backward component), where the perturbation is bounded in terms of the original input data (forward component). The perturbation appears as an additive error matrix satisfying entry-wise bounds. Pure backward error bounds express the computed result as the exact result of a perturbed input problem, with no forward error term.

Key Results

• MMC_error _(mixed)_: Shows that the floating-point matrix product \(\mathtt{fl}(AB)\) equals the exact product of slightly perturbed columns plus a small entry-wise absolute error. The column perturbation is bounded column-wise by \(g(n)\) relative to the input, and the absolute residual by \(g_1(n,n)\) per entry.
• scaleM_error _(mixed)_: Shows that floating-point scalar-matrix multiplication equals exact scaling of a slightly perturbed matrix plus a small entry-wise absolute error. The relative perturbation is bounded by \(\mathbf{u}\) and the absolute residual by \(\eta\).
• sMMC_error _(mixed)_: Composes MMC_error and scaleM_error to give a structured decomposition of \(\mathtt{fl}(x \cdot (AB))\) with backward perturbations from both the matrix product and the scaling step, together with forward absolute errors from each.
• mat_sum_error _(pure backward)_: Shows that floating-point matrix addition equals the exact sum of two slightly perturbed matrices, with each entry perturbed by a relative factor bounded by \(\mathbf{u}\). No forward error term appears.
• mat_axpby_error _(mixed)_: Bounds \(\mathtt{fl}(xA + yB)\) by combining mixed errors from each scaling step with a backward error from the floating-point addition, yielding relative perturbations of the inputs and small absolute forward errors.
• GEMM_error _(mixed)_: Master theorem for \(\mathtt{fl}(s_1(AB) + s_2 Y)\). Decomposes the full GEMM result into backward perturbation components and forward absolute errors from matrix multiplication, scalar scaling, and matrix addition.

We work in an abstract floating-point context NAN (specifying NaN behavior) and over an abstract floating-point type t .

Matrix Multiplication Error

MMC_error establishes that the floating-point matrix product equals the exact product plus a column-wise backward perturbation and a small entry-wise absolute offset. The relative column perturbation is bounded by \(g(n)\) and the absolute residual by \(g_1(n,n)\) per entry, where \(n\) is the inner dimension.

Apply the induction hypothesis to the right submatrix of B.

Apply the matrix-vector mixed error lemma to the left submatrix.

Scalar-Matrix Multiplication Error

scaleM_error establishes that floating-point scalar-matrix multiplication \(\mathtt{fl}(x \cdot A)\) equals exact scaling of a slightly perturbed matrix plus a small entry-wise absolute offset. The relative perturbation is bounded entry-wise by the unit roundoff \(\mathbf{u}\) and the absolute residual by the underflow threshold \(\eta\).

Scaled Matrix Product Error

sMMC_error composes MMC_error and scaleM_error to give a structured decomposition of \(\mathtt{fl}(x \cdot (AB))\). The result carries backward perturbations from the matrix product (bounded by \(g(n)\) column-wise) and from the scaling step (bounded by \(\mathbf{u}\) entry-wise), together with forward absolute errors from each, bounded by \(g_1(n,n)\) and \(\eta\) respectively.

Decompose the outer scaling error for x * (A*B).

Decompose the matrix-multiplication error for A*B, propagating finiteness from F.scalemx x (F.mulmx A B).

Matrix Addition Error

mat_sum_error establishes that floating-point matrix addition \(\mathtt{fl}(A + B)\) equals the exact sum of two slightly perturbed matrices. Each entry of both perturbation matrices is bounded in relative terms by the unit roundoff \(\mathbf{u}\). This is a pure backward result: no forward error term appears.

Scaled Matrix Sum Error

mat_axpby_error bounds the floating-point operation \(\mathtt{fl}(xA + yB)\) by combining the mixed errors from each scaling step with a backward error from the floating-point addition. The result decomposes into relative perturbations of \(A\) and \(B\) bounded by \(\mathbf{u}\) and irreducible absolute forward errors from each scaling, bounded by \(\eta\).

Decompose the outer addition as a pure backward error.

Decompose the mixed error for the scaling x * A.

Decompose the mixed error for the scaling y * B.

General GEMM Error

GEMM_error is the master error theorem for the floating-point GEMM operation \(\mathtt{fl}(s_1(AB) + s_2 Y)\). It decomposes the result into backward perturbation components and forward absolute errors arising from matrix multiplication (bounded by \(g(n)\) and \(g_1(n,n)\)), scalar scaling (bounded by \(\mathbf{u}\) and \(\eta\)), and matrix addition (backward, bounded by \(\mathbf{u}\)). The proof composes mat_axpby_error and MMC_error.

Decompose the axpby structure for s1*(A*B) + s2*Y, obtaining backward addition errors ab5, y3 and forward scaling errors ab4, y2, together with backward scaling perturbations ab3, y1.

Decompose the matrix-multiplication error for A*B, propagating finiteness from the s1*(A*B) factor of Hfin.