LAProof.accuracy_proofs.vec_op_acc

Mixed Error Bounds for Floating-Point Matrix-Vector Operations

This file establishes mixed error bounds for scalar-matrix multiplication, entry-wise matrix addition, and general matrix-vector multiply-accumulate (GEMV), computed in floating-point arithmetic. Each result decomposes the floating-point output into its exact real counterpart plus structured entry-wise error terms.

Main Results

Fscalemx_mixed_error: Shows that the floating-point scalar-matrix product can be expressed as an exact scaled sum where each matrix entry carries a relative error bounded by the unit roundoff and an absolute error bounded by the underflow threshold.
Faddmx_mixed_error: Shows that the floating-point entry-wise matrix sum can be expressed as an exact sum of two componentwise-perturbed matrices, where each perturbation is relative and bounded by the unit roundoff.
Smat_sumF_mixed_error: Shows that the floating-point scaled matrix sum can be expressed as a sum of two perturbed scaled matrices, by composing Fscalemx_mixed_error and Faddmx_mixed_error.
Smat_vec_mul_mixed_error: Shows that the floating-point scaled matrix-vector product can be expressed as an exact scaled result with a forward error on the inner matrix-vector multiply and a mixed error from the outer scalar multiplication.
gemv_error: Shows that the floating-point GEMV operation \(s_1 A x + s_2 y\) can be expressed as an exact result plus structured error matrices, combining the bounds from all preceding lemmas.

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
gemv_acc: forward error bound for floating-point matrix-vector multiplication

From LAProof.accuracy_proofs Require Import preamble common
dotprod_model sum_model dot_acc float_acc_lems mv_mathcomp gemv_acc.

Section WithNans.

Context {NAN : FPCore.Nans} {t : FPStdLib.type}.

Notation g := (@common.g t).
Notation g1 := (@common.g1 t).

Scalar-Matrix Multiplication: Mixed Error Bound

Fscalemx_mixed_error shows that the floating-point scalar-matrix product equals an exact scaled sum of perturbed matrix entries plus an absolute residual, with each entry carrying a relative perturbation bounded by the unit roundoff and an absolute error bounded by the underflow threshold.

Lemma Fscalemx_mixed_error :
  ∀ [m n] (a : ftype t) (v : 'M[ftype t]_(m, n))
    (Hfin : F.finitemx (F.scalemx a v)),
  let vr := map_mx FT2R v in
  ∃ (e eta : 'M[R]_(m, n)),
    map_mx FT2R (F.scalemx a v) = (scalemx (FT2R a) (vr + e) + eta)%Ri
    ∧ (∀ i j, ∃ d ,
          e i j = vr i j × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, Rabs (eta i j) ≤ @default_abs t ).

Entry-wise Matrix Addition: Mixed Error Bound

Faddmx_mixed_error shows that the floating-point entry-wise matrix sum can be expressed as an exact sum of two componentwise-perturbed matrices, where each perturbation is a relative error bounded by the unit roundoff.

Lemma Faddmx_mixed_error :
  ∀ [m n] (A B : 'M[ftype t]_(m, n))
    (Hfin : F.finitemx (F.addmx A B)),
  let Ar := map_mx FT2R A in
  let Br := map_mx FT2R B in
  ∃ (e1 e2 : 'M[R]_(m, n)),
    map_mx FT2R (F.addmx A B) = ((Ar + e1) + (Br + e2))%Ri
    ∧ (∀ i j, ∃ d , e1 i j = Ar i j × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d , e2 i j = Br i j × d ∧ Rabs d ≤ @default_rel t ).

Scaled Matrix Sum: Mixed Error Bound

Smat_sumF_mixed_error shows that the floating-point scaled matrix sum can be expressed as a sum of two perturbed scaled matrices, by composing Fscalemx_mixed_error and Faddmx_mixed_error. Each scaling step contributes a relative and an absolute error; the outer addition contributes an additional relative error per summand.

Lemma Smat_sumF_mixed_error :
  ∀ [m n] (u v : 'M[ftype t]_(m, n)) (a b : ftype t)
    (Hfin : F.finitemx (F.addmx (F.scalemx a u) (F.scalemx b v))),
  let vr := map_mx FT2R v in
  let ur := map_mx FT2R u in
  ∃ (e1 e2 e3 e4 e5 e6 : 'M[R]_(m, n)),
    map_mx FT2R (F.addmx (F.scalemx a u) (F.scalemx b v)) =
      ((scalemx (FT2R a) (ur + e1) + e2 + e3) +
       (scalemx (FT2R b) (vr + e4) + e5 + e6))%Ri
    ∧ (∀ i j, ∃ d ,
          e1 i j = ur i j × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d ,
          e4 i j = vr i j × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d ,
          e3 i j = (scalemx (FT2R a) (ur + e1) + e2) i j × d
          ∧ Rabs d ≤ @default_rel t)%Ri
    ∧ (∀ i j, ∃ d ,
          e6 i j = (scalemx (FT2R b) (vr + e4) + e5) i j × d
          ∧ Rabs d ≤ @default_rel t)%Ri
    ∧ (∀ i j, Rabs (e5 i j) ≤ @default_abs t )
    ∧ (∀ i j, Rabs (e2 i j) ≤ @default_abs t ).

Scaled Matrix-Vector Product: Mixed Error Bound

Smat_vec_mul_mixed_error shows that the floating-point scaled matrix-vector product can be expressed as an exact scaled result with a forward error on the inner matrix-vector multiply (bounded in terms of \(g(n)\)) and a mixed error from the outer scalar multiplication.

Lemma Smat_vec_mul_mixed_error :
  ∀ [m n] (b : ftype t) (A : 'M[ftype t]_(m, n)) (B : 'M[ftype t]_(n, 1))
    (Hfin : F.finitemx (F.scalemx b (F.mulmx A B))),
  ∃ (E : 'M[R]_(m, n)) (e eta1 eta2 : 'M[R]_(m, 1)),
    map_mx FT2R (F.scalemx b (F.mulmx A B)) =
      (scalemx (FT2R b)
         ((map_mx FT2R A + E) ×m map_mx FT2R B + eta1 + e) + eta2)%Ri
    ∧ (∀ i j, Rabs (E i j) ≤ g n × Rabs (map_mx FT2R A i j))
    ∧ (∀ i j, Rabs (eta2 i j) ≤ @default_abs t )
    ∧ (∀ i j, ∃ d ,
          e i j = FT2R (F.mulmx A B i j) × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, Rabs (eta1 i j) ≤ g1 n n ).

General Matrix-Vector Multiply-Accumulate (GEMV): Mixed Error Bound

gemv_error is the central result of this file. It shows that the floating-point GEMV operation \(s_1 A x + s_2 y\) can be expressed as an exact result plus structured error matrices, combining the bounds from Smat_sumF_mixed_error and mat_vec_mul_mixed_error.

Lemma gemv_error :
  ∀ [m n] (A : 'M[ftype t]_(m, n)) (x : 'cV[ftype t]_n)
               (y : 'cV[ftype t]_m) (s1 s2 : ftype t)
    (Hfin : F.finitemx
              (F.addmx (F.scalemx s1 (F.mulmx A x)) (F.scalemx s2 y))),
  ∃ e1 e2 e3 e4 e5 e6 e7 e8 ,
    map_mx FT2R (F.addmx (F.scalemx s1 (F.mulmx A x)) (F.scalemx s2 y)) =
      ((scalemx (FT2R s1)
          ((((map_mx FT2R A + e1) ×m map_mx FT2R x) + e2) + e3) + e4) + e5) +
      ((scalemx (FT2R s2) (map_mx FT2R y + e6) + e7) + e8)
    ∧ (∀ i j, Rabs (e1 i j) ≤ g n × Rabs (map_mx FT2R A i j))
    ∧ (∀ i j, Rabs (e2 i j) ≤ g1 n n )
    ∧ (∀ i j, ∃ d ,
          e3 i j =
            (((map_mx FT2R A + e1) ×m map_mx FT2R x) + e2)%Ri i j × d
          ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d ,
          e6 i j = map_mx FT2R y i j × d ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d ,
          e5 i j =
            (scalemx (FT2R s1)
              ((((map_mx FT2R A + e1) ×m map_mx FT2R x) + e2) + e3) + e4) i j × d
          ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, ∃ d ,
          e8 i j =
            (scalemx (FT2R s2) (map_mx FT2R y + e6) + e7) i j × d
          ∧ Rabs d ≤ @default_rel t )
    ∧ (∀ i j, Rabs (e7 i j) ≤ @default_abs t )
    ∧ (∀ i j, Rabs (e4 i j) ≤ @default_abs t ).

End WithNans.