Matrix-Vector Multiplication Error Bounds

This file establishes mixed and forward error bounds for floating-point matrix-vector multiplication, building on the dot product and summation accuracy results.

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.

Main Results

• vec_vec_mul_mixed_error: Shows that the floating-point row-times-column dot product can be expressed as an exact product of a componentwise-perturbed row vector with the exact column vector, plus a small absolute residual.
• mat_vec_mul_mixed_error: Shows that the floating-point matrix-vector product can be expressed as an exact product of a componentwise-perturbed matrix with the exact input vector, plus a small absolute residual. Proved by applying vec_vec_mul_mixed_error row by row.
• mat_vec_mul_forward_error: Bounds the absolute forward error of the floating-point matrix-vector product in the vector max-norm by \(g(n) \cdot \|A\| \cdot \|B\| + g_1(n,n)\), where \(\|A\|\) is the matrix infinity norm and \(\|B\|\) is the vector max-norm.

Dependencies

This file relies on:

• preamble, common: basic setup and shared definitions
• dotprod_model, sum_model: relational models of dot product and summation
• dot_acc, float_acc_lems: accuracy lemmas
• mv_mathcomp: floating-point matrix/vector operations and norm definitions

Row-Vector Times Column-Vector: Mixed Error Bound

vec_vec_mul_mixed_error shows that the floating-point row-times-column dot product can be expressed as an exact product of a componentwise-perturbed row vector with the exact column vector, plus a small absolute residual.

General Matrix-Vector Product: Mixed Error Bound

mat_vec_mul_mixed_error shows that the floating-point matrix-vector product can be expressed as an exact product of a componentwise-perturbed matrix with the exact input vector, plus a small absolute residual. Proved by applying vec_vec_mul_mixed_error row by row.

Matrix-Vector Product: Forward Error Bound

mat_vec_mul_forward_error bounds the absolute forward error of the floating-point matrix-vector product in the vector max-norm by \(g(n) \cdot \|A\|_M \cdot \|B\| + g_1(n,n)\), where normM is the matrix infinity norm and normv is the vector max-norm.