LAProof.accuracy_proofs.gemv_acc

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

From mathcomp.algebra_tactics Require Import ring.

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

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

Lemma vec_vec_mul_mixed_error:
  ∀ [n] (A: 'M[ftype t]_(1,n)) (B: 'M[ftype t]_(n,1))
  (Hfin: F.finitemx (F.mulmx A B)),
  ∃ (E : 'M[R]_(1,n)) (eta : 'M[R]_(1,1)),
    map_mx FT2R (F.mulmx A B) = ((map_mx FT2R A + E) ×m (map_mx FT2R B) + eta)%Ri
    ∧ (∀ i j, Rabs (E i j) ≤ g n × Rabs (map_mx FT2R A i j))
    ∧ (∀ i j, Rabs (eta i j) ≤ g1 n n).

Lemma mat_vec_mul_mixed_error:
  ∀ [m n] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,1))
  (Hfin: F.finitemx (F.mulmx A B)),
  ∃ (E : 'M[R]_(m,n)) (eta : 'M[R]_(m,1)),
    map_mx FT2R (F.mulmx A B) = ((map_mx FT2R A + E) ×m (map_mx FT2R B) + eta)%Ri
    ∧ (∀ i j, Rabs (E i j) ≤ g n × Rabs (map_mx FT2R A i j))
    ∧ (∀ i j, Rabs (eta i j) ≤ g1 n n).

Theorem mat_vec_mul_forward_error :
 ∀ [m n] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,1))
  (Hfin: F.finitemx (F.mulmx A B)),
  normv (map_mx FT2R (F.mulmx A B) - (map_mx FT2R A ×m map_mx FT2R B))
    ≤ (g n × normM (map_mx FT2R A) × normv (map_mx FT2R B)) + g1 n n.

End WithNAN.