proposition: Theorem relative_error_N_FLT'_ex : forall x, exists eps eta : R, (Rabs eps <= u_ro prec / (1 + u_ro prec))%R /\ (Rabs eta <= /2 * bpow emin)%R /\ (eps * eta = 0)%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps) + eta)%R.
proof: Proof. intro x. set (rx := round _ _ _ x). assert (Pb := u_rod1pu_ro_pos prec). destruct (Rle_or_lt (bpow (emin + prec - 1)) (Rabs x)) as [MX|Mx]. { destruct (relative_error_N_FLX'_ex prec Hp choice x) as (d, (Bd, Hd)). exists d, 0%R; split; [exact Bd|]; split. { rewrite Rabs_R0; apply Rmult_le_pos; [lra|apply bpow_ge_0]. } rewrite Rplus_0_r, Rmult_0_r; split; [reflexivity|]. now rewrite <- Hd; apply round_FLT_FLX. } assert (H : (Rabs (rx - x) <= /2 * bpow emin)%R). { refine (Rle_trans _ _ _ (error_le_half_ulp _ _ _ _) _); [now apply FLT_exp_valid|]. rewrite ulp_FLT_small; [now right|now simpl|]. apply (Rlt_le_trans _ _ _ Mx), bpow_le; lia. } exists 0%R, (rx - x)%R; split; [now rewrite Rabs_R0|]; split; [exact H|]. now rewrite Rmult_0_l, Rplus_0_r, Rmult_1_r; split; [|ring]. Qed.
imports: Coq(ZArith Reals Psatz) Core