LAProof.accuracy_proofs.vec_op_acc

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).

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).

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).

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).

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).

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.