Commit 97b1ddd9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Gave a proper name and place to theorem toto.

parent 416d16fe
......@@ -55,39 +55,6 @@ Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) :=
forall x : R, Rnd_ZR_pt F x (rnd x).
Theorem toto :
forall (F : R -> Prop) (rnd: R-> R),
Rnd_ZR F rnd ->
forall x : R, (Rabs (rnd x) <= Rabs x)%R.
Proof.
intros F rnd H x.
assert (F 0%R).
replace 0%R with (rnd 0%R).
eapply H.
apply Rle_refl.
destruct (H 0%R) as (H1, H2).
apply Rle_antisym.
apply H1.
apply Rle_refl.
apply H2.
apply Rle_refl.
(* . *)
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
now apply (proj1 (H x)).
apply Rle_ge.
now apply (proj1 (H x)).
(* negative *)
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
apply (proj2 (H x)).
auto with real.
apply (proj2 (H x)) ; auto with real.
Qed.
(* property of being a rounding to nearest *)
Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
F f /\
......
......@@ -325,6 +325,39 @@ apply Hd.
apply Hu.
Qed.
Theorem Rnd_ZR_abs :
forall (F : R -> Prop) (rnd: R-> R),
Rnd_ZR F rnd ->
forall x : R, (Rabs (rnd x) <= Rabs x)%R.
Proof.
intros F rnd H x.
assert (F 0%R).
replace 0%R with (rnd 0%R).
eapply H.
apply Rle_refl.
destruct (H 0%R) as (H1, H2).
apply Rle_antisym.
apply H1.
apply Rle_refl.
apply H2.
apply Rle_refl.
(* . *)
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
now apply (proj1 (H x)).
apply Rle_ge.
now apply (proj1 (H x)).
(* negative *)
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
apply (proj2 (H x)).
auto with real.
apply (proj2 (H x)) ; auto with real.
Qed.
Theorem Rnd_N_pt_DN_or_UP :
forall F : R -> Prop,
forall x f : 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