proposition: Theorem Axpy_aux1_aux3 : Fsubnormal radix b t -> Fcanonic radix b u -> (0 < u)%R -> (Z.succ (- dExp b) <= Fexp (FPred b radix precision u))%Z -> (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) <= / 4 * Fulp b radix precision (FPred b radix precision u))%R.
proof: Proof. intros H1 H2 H3 H4. apply Rle_trans with (/ 2 * Fulp b radix precision t)%R. apply Rmult_le_reg_l with 2%R; auto with real arith; rewrite <- Rmult_assoc; rewrite Rinv_r; auto with arith real. ring_simplify (1 * Fulp b radix precision t)%R; unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith. apply Rmult_le_reg_l with 4%R; auto with real arith; repeat rewrite <- Rmult_assoc. change 4%R with (2 * 2)%R. rewrite (Rmult_assoc 2 2 (/ 2)); repeat rewrite Rinv_r; auto with real arith. ring_simplify; unfold Fulp in |- *. replace (Fnormalize radix b precision t) with t; [ elim H1; intros H9 H10; elim H10; intros H11 H12; rewrite H11 | idtac ]. 2: apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. 2: right; auto. 2: apply FnormalizeCanonic; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with zarith. replace (Fnormalize radix b precision (FPred b radix precision u)) with (FPred b radix precision u). 2: apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. 2: apply FPredCanonic; auto with zarith. 2: apply FnormalizeCanonic; auto with zarith. 2: apply FBoundedPred; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with zarith. replace (2 * powerRZ radix (- dExp b))%R with (powerRZ radix (Z.succ (- dExp b))); [ apply Rle_powerRZ | unfold Z.succ in |- * ]; auto with zarith real. rewrite powerRZ_add; auto with real zarith; simpl in |- *; unfold radix. ring. Qed.
imports: Reals ZArith List PeanoNat Psatz