LAProof.accuracy_proofs.sum_acc

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

Require Import Permutation.

Section WithNan .
Context {NAN: FPCore.Nans} {t: type}.
Notation g := (@g t).

Notation D := (@default_rel t).

Notation neg_zero := (@common.neg_zero t).

Theorem bSUM :
  ∀ (x: list (ftype t)) (Hfin: Binary.is_finite (sumF x)),
    ∃ (x': list R),
    size x' = size x ∧
    FT2R (sumF x) = sumR x' ∧
    (∀ n, (n < size x')%nat → ∃ delta,
        nth 0 x' n = FT2R (nth neg_zero x n) × (1 + delta) ∧ Rabs delta ≤ g (size x' - 1)).

Theorem Fsum_backward_error :
  ∀ [n] (x: 'I_n → ftype t) (Hfin: Binary.is_finite (mv_mathcomp.F.sum x)),
    ∃ (x': 'I_n → R),
    FT2R (mv_mathcomp.F.sum x) = \sum_i x' i ∧
    (∀ i: 'I_n, ∃ delta,
        x' i = FT2R (x i) × (1 + delta) ∧ Rabs delta ≤ g (n-1)).

Theorem fSUM :
    ∀ (x: list (ftype t)) (Hfin: Binary.is_finite (sumF x)),
    Rabs ((sumR (map FT2R x)) - FT2R (sumF x)) ≤ g (size x) × (sumR (map Rabs (map FT2R x))).

Lemma Fsum_forward_error:
    ∀ [n] (x: 'I_n → ftype t) (Hfin: Binary.is_finite (mv_mathcomp.F.sum x)),
    Rabs (\sum_i (FT2R (x i)) - FT2R (mv_mathcomp.F.sum x)) ≤ g n × (\sum_i (Rabs (FT2R (x i)))).

Lemma sum_forward_error_permute' :
   ∀ (x x0: list (ftype t))
    (Hfin: Binary.is_finite (sumF x))
    (Hfin0: Binary.is_finite (sumF x0))
    (Hper: Permutation x x0),
    Rabs ((sumR (map FT2R x0)) - FT2R (sumF x0)) ≤ g (size x) × (sumR (map Rabs (map FT2R x0))).

Theorem sum_forward_error_permute :
   ∀ (x x0: list (ftype t))
    (Hfin: Binary.is_finite (sumF x))
    (Hfin0: Binary.is_finite (sumF x0))
    (Hper: Permutation x x0),
    Rabs ((sumR (map FT2R x)) - FT2R (sumF x0)) ≤ g (size x) × (sumR (map Rabs (map FT2R x))).

End WithNan.