Commit aa2517ea authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added theorem rounding_up_succ.

parent 16c12aa9
......@@ -194,6 +194,32 @@ admit.
now apply Rlt_le.
Qed.
Theorem rounding_UP_succ :
forall x, (0 < x)%R -> F x ->
forall eps, (0 < eps <= ulp x)%R ->
rounding beta fexp ZrndUP (x + eps) = (x + ulp x)%R.
Proof.
intros x Zx Fx eps (Heps1,[Heps2|Heps2]).
assert (Heps: (0 <= eps < ulp x)%R).
split.
now apply Rlt_le.
exact Heps2.
assert (Hd := rounding_DN_succ x Zx Fx eps Heps).
rewrite ulp_DN_UP.
rewrite Hd.
unfold ulp, canonic_exponent.
now rewrite ln_beta_succ.
intros Fs.
rewrite rounding_generic in Hd.
apply Rgt_not_eq with (2 := Hd).
pattern x at 2 ; rewrite <- Rplus_0_r.
now apply Rplus_lt_compat_l.
exact Fs.
rewrite Heps2.
apply rounding_generic.
now apply generic_format_succ.
Qed.
Theorem ulp_error :
forall Zrnd x,
(Rabs (rounding beta fexp Zrnd x - x) < ulp x)%R.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment