Commit e0c4c9f4 authored by BOLDO Sylvie's avatar BOLDO Sylvie

ulp_le and _ge in FLX and FLT

parent b9707ce8
......@@ -257,6 +257,48 @@ apply Rle_lt_trans with (2:=Hx).
now apply He.
Qed.
Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
intros x Hx.
assert (x <> 0)%R.
intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
rewrite Z, Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0; try assumption.
unfold canonic_exp, FLT_exp.
destruct (ln_beta beta x) as (e,He).
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
rewrite <- bpow_plus.
right; apply f_equal.
apply trans_eq with (e-prec)%Z;[idtac|ring].
simpl; apply Z.max_l.
assert (emin+prec <= e)%Z; try omega.
apply le_bpow with beta.
apply Rle_trans with (1:=Hx).
left; now apply He.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply He.
Qed.
Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
rewrite Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLT_exp.
apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply bpow_ln_beta_gt.
rewrite <- bpow_plus.
apply bpow_le.
apply Z.le_max_l.
Qed.
(** FLT is a nice format: it has a monotone exponent... *)
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
......
......@@ -221,6 +221,33 @@ intros (n,(H1,H2)); contradict H2.
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.
Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLX_0, Rabs_R0.
right; ring.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLX_exp.
replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply bpow_ln_beta_le.
Qed.
Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLX_0, Rabs_R0.
right; ring.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLX_exp.
unfold Zminus; rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
left; now apply bpow_ln_beta_gt.
Qed.
(** FLX is a nice format: it has a monotone exponent... *)
Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
......
......@@ -1951,6 +1951,16 @@ destruct (ln_beta x) as (ex, Ex) ; simpl.
now apply Ex.
Qed.
Theorem bpow_ln_beta_le :
forall x, (x <> 0)%R ->
(bpow (ln_beta x-1) <= Rabs x)%R.
Proof.
intros x Hx.
destruct (ln_beta x) as (ex, Ex) ; simpl.
now apply Ex.
Qed.
Theorem ln_beta_le_Zpower :
forall m e,
m <> Z0 ->
......
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