# 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.

# Rmin

Definition Rmin (x y:R) : R :=
match Rle_dec x y with
| left _ => x
| right _ => y
end.

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_comm : forall a b:R, Rmin a b = Rmin b a.

Lemma Rmin_stable_in_posreal : forall x y:posreal, 0 < Rmin x y.

# Rmax

Definition Rmax (x y:R) : R :=
match Rle_dec x y with
| left _ => y
| right _ => x
end.

Lemma Rmax_Rle : forall r1 r2 r, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2.

Lemma RmaxLess1 : forall r1 r2, r1 <= Rmax r1 r2.

Lemma RmaxLess2 : forall r1 r2, r2 <= Rmax r1 r2.

Lemma Rmax_comm : forall p q:R, Rmax p q = Rmax q p.

Notation RmaxSym := Rmax_comm (only parsing).

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.

# Rabsolu

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).