Library Stdlib.Reals.Rbasic_fun
Complements for the real numbers
Require Import Rdefinitions Raxioms RIneq.
Require Import R_Ifp.
Local Open Scope R_scope.
Implicit Type r : R.
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.
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.
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_inv r : Rabs (/ r) = / Rabs r.
Lemma Rabs_Rinv_depr : forall r, r <> 0 -> Rabs (/ r) = / Rabs r.
#[deprecated(since="8.16",note="Use Rabs_inv.")]
Notation Rabs_Rinv := Rabs_Rinv_depr.
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.
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_inv r : Rabs (/ r) = / Rabs r.
Lemma Rabs_Rinv_depr : forall r, r <> 0 -> Rabs (/ r) = / Rabs r.
#[deprecated(since="8.16",note="Use Rabs_inv.")]
Notation Rabs_Rinv := Rabs_Rinv_depr.
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.