LAProof.accuracy_proofs.vecnorm_acc

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

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

Definition two_normF (x: list (ftype t)) : R := sqrt (FT2R (dotprodF x x)).
Definition two_normR (x: list R) : R := sqrt (dotprodR x x).

Variable (x : list (ftype t)).
Notation xR := (map FT2R x).
Notation n:= (size x).
Hypothesis Hfin: Binary.is_finite (dotprodF x x) = true.

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

Lemma bfVNRM2:
  ∃ (x' : list R) (eta : R),
   two_normF x = sqrt (dotprodR x' xR + eta) ∧
    (∀ m, (m < n)%nat → ∃ delta,
      nth 0 x' m = FT2R (nth neg_zero x m) × (1 + delta) ∧ Rabs delta ≤ g n) ∧
    Rabs eta ≤ g1 n n.

End TwoNorm.

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

Definition one_normF (x: list (ftype t)) : R := FT2R (sumF x).
Definition one_normR (x: list R) : R := fold_right Rplus 0 x.

Variables (x : list (ftype t)).
Hypothesis Hfin: Binary.is_finite (sumF x) = true.

Notation xR := (map FT2R x).
Notation n:= (size x).
Notation g := (@g t).
Notation neg_zero := (@common.neg_zero t).

Lemma bfVNRM1:
    ∃ (x': list R),
    one_normF x = one_normR x' ∧
    (∀ m, (m < n)%nat → ∃ delta,
        nth 0 x' m = FT2R (nth neg_zero x m) × (1 + delta) ∧ Rabs delta ≤ g (n - 1)).

End OneNorm.