proposition: Theorem ErrFmaApprox_2_aux: (Rabs (z+w-(a*x+b)) <= (3*radix/2+/2)*powerRZ radix (2-2*p)*Rabs z)%R.
proof: Proof. replace (z+w-(a*x+b))%R with ((t-(uh-z))+-(t+v-w)+-(pl+ul-v))%R; [idtac|rewrite ulDef; rewrite plDef; ring]. pattern (FtoRradix t) at 1; replace (FtoRradix t) with (uh-z)%R. 2: elim tBounded with bo radix p a x b ph pl uh z; auto with zarith. 2: fold FtoRradix; intros t' T; elim T; intros; clear T. 2: rewrite <- H0; unfold FtoRradix. 2: apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. 2: fold FtoRradix; rewrite H0; auto. replace (uh - z - (uh - z) + - (t + v - w) + - (pl + ul - v))%R with (-((t + v - w)+(pl + ul - v)))%R;[rewrite Rabs_Ropp|ring]. apply Rle_trans with (Rabs (t+v-w)+Rabs (pl+ul-v))%R;[apply Rabs_triang|idtac]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (2*Rabs (t + v - w) + 2*Rabs (pl + ul - v))%R;[right; simpl; ring|idtac]. apply Rle_trans with ((Fulp bo radix p w)+(Fulp bo radix p v))%R. apply Rplus_le_compat; unfold FtoRradix; apply ClosestUlp; auto with zarith. apply Rle_trans with (Rabs w*powerRZ radix (Z.succ (-p))+Rabs v*powerRZ radix (Z.succ (-p)))%R. apply Rplus_le_compat; unfold FtoRradix; apply FulpLe2; auto with zarith. elim wDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. elim vDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. apply Rle_trans with (powerRZ radix (Z.succ (-p))*(Rabs w+Rabs v))%R;[right; ring|idtac]. generalize wLe; generalize vLe; intros. apply Rle_trans with (powerRZ radix (Z.succ (-p))*(powerRZ radix (Fexp z) * (2 * radix + 1) + powerRZ radix (Fexp z) *radix))%R; [apply Rmult_le_compat_l; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with ((3*radix+1)*(powerRZ radix (Z.succ (- p))*(powerRZ radix (Fexp z))))%R; [right; ring|idtac]. apply Rle_trans with ((3 * radix + 1) * (powerRZ radix (2- 2*p) *Rabs z))%R; [idtac|right; field; auto with real]. apply Rmult_le_compat_l; auto with real zarith. apply Rle_trans with (0+1)%R; auto with real. assert (0 < 3*radix)%R; auto with real. apply Rmult_lt_0_compat; try apply IZR_lt; auto with real zarith. replace (2-2*p)%Z with (Z.succ (-p)+Z.succ (-p))%Z;[idtac|unfold Z.succ; ring]. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (Fulp bo radix p z). unfold Fulp;rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. unfold FtoRradix; rewrite Rmult_comm; apply FulpLe2; auto with zarith. elim zDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz