Library Coq.Reals.Rbasic_fun
Complements for the real numbers
Definition Rmin (
x y:
R) :
R :=
match Rle_dec x y with
|
left _ =>
x
|
right _ =>
y
end.
Lemma Rmin_case :
forall r1 r2 (
P:
R -> Type),
P r1 -> P r2 -> P (
Rmin r1 r2).
Lemma Rmin_case_strong :
forall r1 r2 (
P:
R -> Type),
(r1 <= r2 -> P r1) -> (r2 <= r1 -> P r2) -> P (
Rmin r1 r2).
Lemma Rmin_Rgt_l :
forall r1 r2 r,
Rmin r1 r2 > r -> r1 > r /\ r2 > r.
Lemma Rmin_Rgt_r :
forall r1 r2 r,
r1 > r /\ r2 > r -> Rmin r1 r2 > r.
Lemma Rmin_Rgt :
forall r1 r2 r,
Rmin r1 r2 > r <-> r1 > r /\ r2 > r.
Lemma Rmin_l :
forall x y:
R,
Rmin x y <= x.
Lemma Rmin_r :
forall x y:
R,
Rmin x y <= y.
Lemma Rmin_left :
forall x y,
x <= y -> Rmin x y = x.
Lemma Rmin_right :
forall x y,
y <= x -> Rmin x y = y.
Lemma Rle_min_compat_r :
forall x y z,
x <= y -> Rmin x z <= Rmin y z.
Lemma Rle_min_compat_l :
forall x y z,
x <= y -> Rmin z x <= Rmin z y.
Lemma Rmin_comm :
forall x y:
R,
Rmin x y = Rmin y x.
Lemma Rmin_stable_in_posreal :
forall x y:
posreal, 0
< Rmin x y.
Lemma Rmin_pos :
forall x y:
R, 0
< x -> 0
< y -> 0
< Rmin x y.
Lemma Rmin_glb :
forall x y z:
R,
z <= x -> z <= y -> z <= Rmin x y.
Lemma Rmin_glb_lt :
forall x y z:
R,
z < x -> z < y -> z < Rmin x y.
Definition Rmax (
x y:
R) :
R :=
match Rle_dec x y with
|
left _ =>
y
|
right _ =>
x
end.
Lemma Rmax_case :
forall r1 r2 (
P:
R -> Type),
P r1 -> P r2 -> P (
Rmax r1 r2).
Lemma Rmax_case_strong :
forall r1 r2 (
P:
R -> Type),
(r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (
Rmax r1 r2).
Lemma Rmax_Rle :
forall r1 r2 r,
r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2.
Lemma Rmax_comm :
forall x y:
R,
Rmax x y = Rmax y x.
Lemma Rmax_l :
forall x y:
R,
x <= Rmax x y.
Lemma Rmax_r :
forall x y:
R,
y <= Rmax x y.
Lemma Rmax_left :
forall x y,
y <= x -> Rmax x y = x.
Lemma Rmax_right :
forall x y,
x <= y -> Rmax x y = y.
Lemma Rle_max_compat_r :
forall x y z,
x <= y -> Rmax x z <= Rmax y z.
Lemma Rle_max_compat_l :
forall x y z,
x <= y -> Rmax z x <= Rmax z y.
Lemma RmaxRmult :
forall (
p q:
R)
r, 0
<= r -> Rmax (
r * p) (
r * q)
= r * Rmax p q.
Lemma Rmax_stable_in_negreal :
forall x y:
negreal,
Rmax x y < 0.
Lemma Rmax_lub :
forall x y z:
R,
x <= z -> y <= z -> Rmax x y <= z.
Lemma Rmax_lub_lt :
forall x y z:
R,
x < z -> y < z -> Rmax x y < z.
Lemma Rmax_Rlt :
forall x y z,
Rmax x y < z <-> x < z /\ y < z.
Lemma Rmax_neg :
forall x y:
R,
x < 0
-> y < 0
-> Rmax x y < 0.
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 Rle_abs :
forall x:
R,
x <= Rabs x.
Definition RRle_abs :=
Rle_abs.
Lemma Rabs_le :
forall a b,
-b <= a <= b -> Rabs a <= b.
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 (
Z.abs z).
Lemma abs_IZR :
forall z,
IZR (
Z.abs z)
= Rabs (
IZR z).
Lemma Ropp_Rmax :
forall x y,
- Rmax x y = Rmin (
-x) (
-y).
Lemma Ropp_Rmin :
forall x y,
- Rmin x y = Rmax (
-x) (
-y).
Lemma Rmax_assoc :
forall a b c,
Rmax a (
Rmax b c)
= Rmax (
Rmax a b)
c.
Lemma Rminmax :
forall a b,
Rmin a b <= Rmax a b.
Lemma Rmin_assoc :
forall x y z,
Rmin x (
Rmin y z)
=
Rmin (
Rmin x y)
z.