LAProof.accuracy_proofs.dot_acc

This file contains three main theorems for the accuracy of the non-fma dot product : dotprod_mixed_error, dotprod_forward_error, and sparse_dotprod_forward_error.

From LAProof.accuracy_proofs Require Import preamble common
                                            dotprod_model sum_model
                                            float_acc_lems dot_acc_lemmas.

Require Import Reals.
Open Scope R.

Section MixedError.
Context {NAN: FPCore.Nans} {t : type}.

Notation g := (@g t).
Notation g1 := (@g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).
Notation neg_zero := (@common.neg_zero t).

Variables (v1 v2: list (ftype t)).
Hypothesis Hlen: size v1 = size v2.
Hypothesis Hfin: Binary.is_finite (dotprodF v1 v2) = true.

Lemma dotprod_mixed_error:
  ∃ (u : list R) (eta : R ),
    size u = size v2 ∧
    FT2R (dotprodF v1 v2) = dotprodR u (map FT2R v2) + eta ∧
    (∀ n, (n < size v2)%nat → ∃ delta ,
      nth 0 u n = FT2R (nth neg_zero v1 n) × (1 + delta ) ∧ Rabs delta ≤ g (size v2)) ∧
    Rabs eta ≤ g1 (size v2) (size v2).

End MixedError.

Section ForwardError.
Context {NAN: FPCore.Nans} {t : type}.

Variables v1 v2 : list (ftype t).
Notation v1R := (map FT2R v1).
Notation v2R := (map FT2R v2).
Notation v1R' := (map Rabs v1R).
Notation v2R' := (map Rabs v2R).
Notation n := (size v2).

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

Hypothesis Hlen: size v1 = size v2.
Hypothesis Hfin: Binary.is_finite (dotprodF v1 v2) = true.

Lemma dotprod_forward_error:
  Rabs (FT2R (dotprodF v1 v2) - dotprodR v1R v2R )
        ≤ g n × dotprodR v1R' v2R' + g1 n (n - 1).

Notation nnzR := (common.nnzR v1R).

Lemma sparse_dotprod_forward_error:
  Rabs (FT2R (dotprodF v1 v2) - dotprodR v1R v2R ) ≤
       g nnzR × dotprodR v1R' v2R' + g1 nnzR (nnzR - 1).

End ForwardError.