proposition: Theorem relative_error_N_FLT'_ex_separate : forall x, exists x' : R, round beta (FLT_exp emin prec) (Znearest choice) x' = round beta (FLT_exp emin prec) (Znearest choice) x /\ (exists eta, Rabs eta <= /2 * bpow emin /\ x' = x + eta)%R /\ (exists eps, Rabs eps <= u_ro prec / (1 + u_ro prec) /\ round beta (FLT_exp emin prec) (Znearest choice) x' = x' * (1 + eps))%R.
proof: Proof. intro x. set (rx := round _ _ _ x). destruct (relative_error_N_FLT'_ex x) as (d, (e, (Bd, (Be, (Hde0, Hde))))). destruct (Rlt_or_le (Rabs (d * x)) (Rabs e)) as [HdxLte|HeLedx]. { exists rx; split; [|split]. { apply round_generic; [now apply valid_rnd_N|]. now apply generic_format_round; [apply FLT_exp_valid|apply valid_rnd_N]. } { exists e; split; [exact Be|]. unfold rx; rewrite Hde; destruct (Rmult_integral _ _ Hde0) as [Zd|Ze]. { now rewrite Zd, Rplus_0_r, Rmult_1_r. } exfalso; revert HdxLte; rewrite Ze, Rabs_R0; apply Rle_not_lt, Rabs_pos. } exists 0%R; split; [now rewrite Rabs_R0; apply u_rod1pu_ro_pos|]. rewrite Rplus_0_r, Rmult_1_r; apply round_generic; [now apply valid_rnd_N|]. now apply generic_format_round; [apply FLT_exp_valid|apply valid_rnd_N]. } exists x; split; [now simpl|split]. { exists 0%R; split; [rewrite Rabs_R0; apply Rmult_le_pos; [lra|apply bpow_ge_0]|ring]. } exists d; rewrite Hde; destruct (Rmult_integral _ _ Hde0) as [Zd|Ze]. { split; [exact Bd|]. assert (Ze : e = 0%R); [|now rewrite Ze, Rplus_0_r]. apply Rabs_eq_R0, Rle_antisym; [|now apply Rabs_pos]. now revert HeLedx; rewrite Zd, Rmult_0_l, Rabs_R0. } now rewrite Ze, Rplus_0_r. Qed.
imports: Coq(ZArith Reals Psatz) Core