proposition: Theorem Axpy_aux2 : Fcanonic radix b u -> Fsubnormal radix b t -> (0 < u)%R -> FtoRradix u = (t + y)%R -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) < / 4 * Fulp b radix precision (FPred b radix precision u))%R -> MinOrMax radix b (a1 * x1 + y1) u.
proof: Proof. intros H1 H2 H3 H4 H5. apply MinOrMax1 with precision; auto with zarith; fold FtoRradix in |- *. replace (a1 * x1 + y1 - FtoRradix u)%R with (y1 - y + (a1 * x1 - a * x) + (a * x - t + (t + y - u)))%R; [ idtac | ring ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t + (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rabs_triang | idtac ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t + (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rplus_le_compat_r; apply Rabs_triang | idtac ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x) + (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rplus_le_compat_l; apply Rabs_triang | idtac ]. apply Rlt_le_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rplus_lt_compat_r; auto | idtac ]. apply Rle_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + (/ 2 * powerRZ radix (- dExp b) + 0))%R. apply Rplus_le_compat; auto with real. apply Rplus_le_compat. apply Rle_trans with (/ 2 * Fulp b radix precision t)%R; [ apply Rmult_le_reg_l with 2%R | apply Rmult_le_compat_l ]; auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith. ring_simplify (1 * Fulp b radix precision t)%R; unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith. unfold Fulp in |- *; replace (Fnormalize radix b precision t) with t. elim H2; intros H6 H7; elim H7; intros H8 H9; rewrite H8; auto with zarith real. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. right; auto. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. rewrite H4; right. ring_simplify (FtoRradix t + FtoRradix y - (FtoRradix t + FtoRradix y))%R; apply Rabs_R0. replace (/ 2 * powerRZ radix (- dExp b) + 0)%R with (/ 2 * powerRZ radix (- dExp b))%R; [ idtac | ring ]. apply Rle_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + / 2 * Fulp b radix precision (FPred b radix precision u))%R; [ apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real arith | idtac ]. unfold Fulp in |- *; apply Rle_powerRZ; auto with zarith real. cut (Fbounded b (Fnormalize radix b precision (FPred b radix precision u))); [ intros H6; elim H6; auto | idtac ]. apply FnormalizeBounded; auto with zarith arith. apply FBoundedPred; auto with zarith arith. apply Rle_trans with ((/ 4 + / 2) * Fulp b radix precision (FPred b radix precision u))%R; [ right; ring | idtac ]. apply Rle_trans with (1 * Fulp b radix precision (FPred b radix precision u))%R; [ apply Rmult_le_compat_r; auto with real zarith | right; ring ]. unfold Fulp in |- *; auto with real zarith. now apply powerRZ_le, IZR_lt. lra. Qed.
imports: Reals ZArith List PeanoNat Psatz