Library Coq.Reals.Rbasic_fun
Complements for the real numbers
Require Import Rbase.
Require Import R_Ifp.
Require Import Fourier.
Open Local Scope R_scope.
Implicit Type r :
R.
Lemma Rcase_abs :
forall r, {
r < 0} + {
r >= 0}.
Definition Rabs r :
R :=
match Rcase_abs r with
|
left _ => -
r
|
right _ =>
r
end.
Lemma Rabs_R0 :
Rabs 0 = 0.
Lemma Rabs_R1 :
Rabs 1 = 1.
Lemma Rabs_no_R0 :
forall r,
r <> 0 ->
Rabs r <> 0.
Lemma Rabs_left :
forall r,
r < 0 ->
Rabs r = -
r.
Lemma Rabs_right :
forall r,
r >= 0 ->
Rabs r =
r.
Lemma Rabs_left1 :
forall a:R,
a <= 0 ->
Rabs a = -
a.
Lemma Rabs_pos :
forall x:R, 0 <=
Rabs x.
Lemma RRle_abs :
forall x:R,
x <=
Rabs x.
Lemma Rabs_pos_eq :
forall x:R, 0 <=
x ->
Rabs x =
x.
Lemma Rabs_Rabsolu :
forall x:R,
Rabs (
Rabs x) =
Rabs x.
Lemma Rabs_pos_lt :
forall x:R,
x <> 0 -> 0 <
Rabs x.
Lemma Rabs_minus_sym :
forall x y:R,
Rabs (
x -
y) =
Rabs (
y -
x).
Lemma Rabs_mult :
forall x y:R,
Rabs (
x *
y) =
Rabs x *
Rabs y.
Lemma Rabs_Rinv :
forall r,
r <> 0 ->
Rabs (/
r) = /
Rabs r.
Lemma Rabs_Ropp :
forall x:R,
Rabs (-
x) =
Rabs x.
Lemma Rabs_triang :
forall a b:R,
Rabs (
a +
b) <=
Rabs a +
Rabs b.
Lemma Rabs_triang_inv :
forall a b:R,
Rabs a -
Rabs b <=
Rabs (
a -
b).
Lemma Rabs_triang_inv2 :
forall a b:R,
Rabs (
Rabs a -
Rabs b) <=
Rabs (
a -
b).
Lemma Rabs_def1 :
forall x a:R,
x <
a -> -
a <
x ->
Rabs x <
a.
Lemma Rabs_def2 :
forall x a:R,
Rabs x <
a ->
x <
a /\ -
a <
x.
Lemma RmaxAbs :
forall (
p q:R)
r,
p <=
q ->
q <=
r ->
Rabs q <=
Rmax (
Rabs p) (
Rabs r).
Lemma Rabs_Zabs :
forall z:Z,
Rabs (
IZR z) =
IZR (
Zabs z).