Relative error of the roundings
Require Import Fcore.
Section Fprop_relative.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Section Fprop_relative_generic.
Variable fexp :
Z ->
Z.
Context {
prop_exp :
Valid_exp fexp }.
Section relative_error_conversion.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Lemma relative_error_lt_conversion :
forall x b, (0 <
b)%
R ->
(
x <> 0 ->
Rabs (
round beta fexp rnd x -
x) <
b *
Rabs x)%
R ->
exists eps,
(
Rabs eps <
b)%
R /\
round beta fexp rnd x = (
x * (1 +
eps))%
R.
Proof with
Lemma relative_error_le_conversion :
forall x b, (0 <=
b)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <=
b *
Rabs x)%
R ->
exists eps,
(
Rabs eps <=
b)%
R /\
round beta fexp rnd x = (
x * (1 +
eps))%
R.
Proof with
End relative_error_conversion.
Variable emin p :
Z.
Hypothesis Hmin :
forall k, (
emin <
k)%
Z -> (
p <=
k -
fexp k)%
Z.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Theorem relative_error :
forall x,
(
bpow emin <=
Rabs x)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
bpow (-
p + 1) *
Rabs x)%
R.
Proof with
1+ε property in any rounding
Theorem relative_error_ex :
forall x,
(
bpow emin <=
Rabs x)%
R ->
exists eps,
(
Rabs eps <
bpow (-
p + 1))%
R /\
round beta fexp rnd x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_F2R_emin :
forall m,
let x :=
F2R (
Float beta m emin)
in
(
x <> 0)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
bpow (-
p + 1) *
Rabs x)%
R.
Proof.
Theorem relative_error_F2R_emin_ex :
forall m,
let x :=
F2R (
Float beta m emin)
in
exists eps,
(
Rabs eps <
bpow (-
p + 1))%
R /\
round beta fexp rnd x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_round :
(0 <
p)%
Z ->
forall x,
(
bpow emin <=
Rabs x)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
bpow (-
p + 1) *
Rabs (
round beta fexp rnd x))%
R.
Proof with
Theorem relative_error_round_F2R_emin :
(0 <
p)%
Z ->
forall m,
let x :=
F2R (
Float beta m emin)
in
(
x <> 0)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
bpow (-
p + 1) *
Rabs (
round beta fexp rnd x))%
R.
Proof.
Variable choice :
Z ->
bool.
Theorem relative_error_N :
forall x,
(
bpow emin <=
Rabs x)%
R ->
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
bpow (-
p + 1) *
Rabs x)%
R.
Proof.
1+ε property in rounding to nearest
Theorem relative_error_N_ex :
forall x,
(
bpow emin <=
Rabs x)%
R ->
exists eps,
(
Rabs eps <= /2 *
bpow (-
p + 1))%
R /\
round beta fexp (
Znearest choice)
x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_N_F2R_emin :
forall m,
let x :=
F2R (
Float beta m emin)
in
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
bpow (-
p + 1) *
Rabs x)%
R.
Proof with
Theorem relative_error_N_F2R_emin_ex :
forall m,
let x :=
F2R (
Float beta m emin)
in
exists eps,
(
Rabs eps <= /2 *
bpow (-
p + 1))%
R /\
round beta fexp (
Znearest choice)
x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_N_round :
(0 <
p)%
Z ->
forall x,
(
bpow emin <=
Rabs x)%
R ->
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
bpow (-
p + 1) *
Rabs (
round beta fexp (
Znearest choice)
x))%
R.
Proof with
Theorem relative_error_N_round_F2R_emin :
(0 <
p)%
Z ->
forall m,
let x :=
F2R (
Float beta m emin)
in
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
bpow (-
p + 1) *
Rabs (
round beta fexp (
Znearest choice)
x))%
R.
Proof with
End Fprop_relative_generic.
Section Fprop_relative_FLT.
Variable emin prec :
Z.
Variable Hp :
Zlt 0
prec.
Lemma relative_error_FLT_aux :
forall k, (
emin +
prec - 1 <
k)%
Z -> (
prec <=
k -
FLT_exp emin prec k)%
Z.
Proof.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Theorem relative_error_FLT :
forall x,
(
bpow (
emin +
prec - 1) <=
Rabs x)%
R ->
(
Rabs (
round beta (
FLT_exp emin prec)
rnd x -
x) <
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
Theorem relative_error_FLT_F2R_emin :
forall m,
let x :=
F2R (
Float beta m emin)
in
(
x <> 0)%
R ->
(
Rabs (
round beta (
FLT_exp emin prec)
rnd x -
x) <
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
Theorem relative_error_FLT_F2R_emin_ex :
forall m,
let x :=
F2R (
Float beta m emin)
in
exists eps,
(
Rabs eps <
bpow (-
prec + 1))%
R /\
round beta (
FLT_exp emin prec)
rnd x = (
x * (1 +
eps))%
R.
Proof with
1+ε property in any rounding in FLT
Theorem relative_error_FLT_ex :
forall x,
(
bpow (
emin +
prec - 1) <=
Rabs x)%
R ->
exists eps,
(
Rabs eps <
bpow (-
prec + 1))%
R /\
round beta (
FLT_exp emin prec)
rnd x = (
x * (1 +
eps))%
R.
Proof with
Variable choice :
Z ->
bool.
Theorem relative_error_N_FLT :
forall x,
(
bpow (
emin +
prec - 1) <=
Rabs x)%
R ->
(
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
1+ε property in rounding to nearest in FLT
Theorem relative_error_N_FLT_ex :
forall x,
(
bpow (
emin +
prec - 1) <=
Rabs x)%
R ->
exists eps,
(
Rabs eps <= /2 *
bpow (-
prec + 1))%
R /\
round beta (
FLT_exp emin prec) (
Znearest choice)
x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_N_FLT_round :
forall x,
(
bpow (
emin +
prec - 1) <=
Rabs x)%
R ->
(
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x))%
R.
Proof with
Theorem relative_error_N_FLT_F2R_emin :
forall m,
let x :=
F2R (
Float beta m emin)
in
(
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
Theorem relative_error_N_FLT_F2R_emin_ex :
forall m,
let x :=
F2R (
Float beta m emin)
in
exists eps,
(
Rabs eps <= /2 *
bpow (-
prec + 1))%
R /\
round beta (
FLT_exp emin prec) (
Znearest choice)
x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_N_FLT_round_F2R_emin :
forall m,
let x :=
F2R (
Float beta m emin)
in
(
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs (
round beta (
FLT_exp emin prec) (
Znearest choice)
x))%
R.
Proof with
Lemma error_N_FLT_aux :
forall x,
(0 <
x)%
R ->
exists eps,
exists eta,
(
Rabs eps <= /2 *
bpow (-
prec + 1))%
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.
End Fprop_relative_FLT.
Lemma error_N_FLT :
forall (
emin prec :
Z), (0 <
prec)%
Z ->
forall (
choice :
Z ->
bool),
forall (
x :
R),
exists eps eta :
R,
(
Rabs eps <= /2 *
bpow (-
prec + 1))%
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.
intros emin prec Pprec choice x.
destruct (
Rtotal_order x 0)
as [
Nx|[
Zx|
Px]].
{
assert (
Pmx : (0 < -
x)%
R).
{
now rewrite <-
Ropp_0;
apply Ropp_lt_contravar. }
destruct (
error_N_FLT_aux emin prec Pprec
(
fun t :
Z =>
negb (
choice (- (
t + 1))%
Z))
(-
x)%
R Pmx)
as (
d,(
e,(
Hd,(
He,(
Hde,
Hr))))).
exists d;
exists (-
e)%
R;
split; [
exact Hd|
split; [|
split]].
{
now rewrite Rabs_Ropp. }
{
now rewrite Ropp_mult_distr_r_reverse, <-
Ropp_0;
apply f_equal. }
rewrite <- (
Ropp_involutive x),
round_N_opp.
now rewrite Ropp_mult_distr_l_reverse, <-
Ropp_plus_distr;
apply f_equal. }
{
assert (
Ph2 : (0 <= / 2)%
R).
{
apply (
Rmult_le_reg_l 2
_ _ Rlt_0_2).
rewrite Rmult_0_r,
Rinv_r; [
exact Rle_0_1|].
apply Rgt_not_eq,
Rlt_gt,
Rlt_0_2. }
exists R0;
exists R0;
rewrite Zx;
split; [|
split; [|
split]].
{
now rewrite Rabs_R0;
apply Rmult_le_pos; [|
apply bpow_ge_0]. }
{
now rewrite Rabs_R0;
apply Rmult_le_pos; [|
apply bpow_ge_0]. }
{
now rewrite Rmult_0_l. }
now rewrite Rmult_0_l,
Rplus_0_l,
round_0; [|
apply valid_rnd_N]. }
now apply error_N_FLT_aux.
Qed.
Section Fprop_relative_FLX.
Variable prec :
Z.
Variable Hp :
Zlt 0
prec.
Lemma relative_error_FLX_aux :
forall k, (
prec <=
k -
FLX_exp prec k)%
Z.
Proof.
intros k.
unfold FLX_exp.
omega.
Qed.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Theorem relative_error_FLX :
forall x,
(
x <> 0)%
R ->
(
Rabs (
round beta (
FLX_exp prec)
rnd x -
x) <
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
1+ε property in any rounding in FLX
Theorem relative_error_FLX_ex :
forall x,
exists eps,
(
Rabs eps <
bpow (-
prec + 1))%
R /\
round beta (
FLX_exp prec)
rnd x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_FLX_round :
forall x,
(
x <> 0)%
R ->
(
Rabs (
round beta (
FLX_exp prec)
rnd x -
x) <
bpow (-
prec + 1) *
Rabs (
round beta (
FLX_exp prec)
rnd x))%
R.
Proof with
Variable choice :
Z ->
bool.
Theorem relative_error_N_FLX :
forall x,
(
Rabs (
round beta (
FLX_exp prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs x)%
R.
Proof with
1+ε property in rounding to nearest in FLX
Theorem relative_error_N_FLX_ex :
forall x,
exists eps,
(
Rabs eps <= /2 *
bpow (-
prec + 1))%
R /\
round beta (
FLX_exp prec) (
Znearest choice)
x = (
x * (1 +
eps))%
R.
Proof with
Theorem relative_error_N_FLX_round :
forall x,
(
Rabs (
round beta (
FLX_exp prec) (
Znearest choice)
x -
x) <= /2 *
bpow (-
prec + 1) *
Rabs (
round beta (
FLX_exp prec) (
Znearest choice)
x))%
R.
Proof with
End Fprop_relative_FLX.
End Fprop_relative.