Library Coquelicot.Rbar

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Reals.
Require Import Ssreflect.ssreflect.
Require Import Rcomplements.

This file contains the definition and properties of the set R ∪ {+ ∞} ∪ {- ∞} denoted by Rbar. We have defined:

Open Scope R_scope.

Definitions


Inductive Rbar :=
  | Finite : RRbar
  | p_infty : Rbar
  | m_infty : Rbar.
Definition real (x : Rbar) :=
  match x with
    | Finite xx
    | _ ⇒ 0
  end.
Coercion Finite : R >-> Rbar.
Coercion real : Rbar >-> R.

Definition is_finite (x : Rbar) := Finite (real x) = x.
Lemma is_finite_correct (x : Rbar) :
  is_finite x y : R, x = Finite y.

Order


Definition Rbar_lt (x y : Rbar) : Prop :=
  match x,y with
    | p_infty, _ | _, m_inftyFalse
    | m_infty, _ | _, p_inftyTrue
    | Finite x, Finite yRlt x y
  end.

Definition Rbar_le (x y : Rbar) : Prop :=
  match x,y with
    | m_infty, _ | _, p_inftyTrue
    | p_infty, _ | _, m_inftyFalse
    | Finite x, Finite yRle x y
  end.

Operations

Additive operators


Definition Rbar_opp (x : Rbar) :=
  match x with
    | Finite xFinite (-x)
    | p_inftym_infty
    | m_inftyp_infty
  end.

Definition Rbar_plus' (x y : Rbar) :=
  match x,y with
    | p_infty, m_infty | m_infty, p_inftyNone
    | p_infty, _ | _, p_inftySome p_infty
    | m_infty, _ | _, m_inftySome m_infty
    | Finite x', Finite y'Some (Finite (x' + y'))
  end.
Definition Rbar_plus (x y : Rbar) :=
  match Rbar_plus' x y with Some zz | NoneFinite 0 end.
Definition is_Rbar_plus (x y z : Rbar) : Prop :=
  Rbar_plus' x y = Some z.
Definition ex_Rbar_plus (x y : Rbar) : Prop :=
  match Rbar_plus' x y with Some _True | NoneFalse end.

Lemma is_Rbar_plus_unique (x y z : Rbar) :
  is_Rbar_plus x y zRbar_plus x y = z.
Lemma Rbar_plus_correct (x y : Rbar) :
  ex_Rbar_plus x yis_Rbar_plus x y (Rbar_plus x y).

Definition Rbar_minus (x y : Rbar) := Rbar_plus x (Rbar_opp y).
Definition is_Rbar_minus (x y z : Rbar) : Prop :=
  is_Rbar_plus x (Rbar_opp y) z.
Definition ex_Rbar_minus (x y : Rbar) : Prop :=
  ex_Rbar_plus x (Rbar_opp y).

Multiplicative operators


Definition Rbar_inv (x : Rbar) : Rbar :=
  match x with
    | Finite xFinite (/x)
    | _Finite 0
  end.

Definition Rbar_mult' (x y : Rbar) :=
  match x with
    | Finite xmatch y with
      | Finite ySome (Finite (x × y))
      | p_inftymatch (Rle_dec 0 x) with
        | left Hmatch Rle_lt_or_eq_dec _ _ H with left _Some p_infty | right _None end
        | right _Some m_infty
      end
      | m_inftymatch (Rle_dec 0 x) with
        | left Hmatch Rle_lt_or_eq_dec _ _ H with left _Some m_infty | right _None end
        | right _Some p_infty
      end
    end
    | p_inftymatch y with
      | Finite ymatch (Rle_dec 0 y) with
        | left Hmatch Rle_lt_or_eq_dec _ _ H with left _Some p_infty | right _None end
        | right _Some m_infty
      end
      | p_inftySome p_infty
      | m_inftySome m_infty
    end
    | m_inftymatch y with
      | Finite ymatch (Rle_dec 0 y) with
        | left Hmatch Rle_lt_or_eq_dec _ _ H with left _Some m_infty | right _None end
        | right _Some p_infty
      end
      | p_inftySome m_infty
      | m_inftySome p_infty
    end
  end.
Definition Rbar_mult (x y : Rbar) :=
  match Rbar_mult' x y with Some zz | NoneFinite 0 end.

Definition is_Rbar_mult (x y z : Rbar) : Prop :=
  Rbar_mult' x y = Some z.
Definition ex_Rbar_mult (x y : Rbar) : Prop :=
  match x with
    | Finite xmatch y with
      | Finite yTrue
      | p_inftyx 0
      | m_inftyx 0
    end
    | p_inftymatch y with
      | Finite yy 0
      | p_inftyTrue
      | m_inftyTrue
    end
    | m_inftymatch y with
      | Finite yy 0
      | p_inftyTrue
      | m_inftyTrue
    end
  end.

Definition Rbar_mult_pos (x : Rbar) (y : posreal) :=
  match x with
    | Finite xFinite (x×y)
    | _x
  end.

Lemma is_Rbar_mult_unique (x y z : Rbar) :
  is_Rbar_mult x y zRbar_mult x y = z.
Lemma Rbar_mult_correct (x y : Rbar) :
  ex_Rbar_mult x yis_Rbar_mult x y (Rbar_mult x y).
Lemma Rbar_mult_correct' (x y z : Rbar) :
  is_Rbar_mult x y zex_Rbar_mult x y.

Definition Rbar_div (x y : Rbar) : Rbar :=
  Rbar_mult x (Rbar_inv y).
Definition is_Rbar_div (x y z : Rbar) : Prop :=
  is_Rbar_mult x (Rbar_inv y) z.
Definition ex_Rbar_div (x y : Rbar) : Prop :=
  ex_Rbar_mult x (Rbar_inv y).
Definition Rbar_div_pos (x : Rbar) (y : posreal) :=
  match x with
    | Finite xFinite (x/y)
    | _x
  end.

Compatibility with real numbers

For equality and order. The compatibility of addition and multiplication is proved in Rbar_seq

Lemma Rbar_finite_eq (x y : R) :
  Finite x = Finite y x = y.
Lemma Rbar_finite_neq (x y : R) :
  Finite x Finite y x y.

Properties of order

Relations between inequalities


Lemma Rbar_lt_not_eq (x y : Rbar) :
  Rbar_lt x yxy.

Lemma Rbar_not_le_lt (x y : Rbar) :
  ¬ Rbar_le x yRbar_lt y x.

Lemma Rbar_lt_not_le (x y : Rbar) :
  Rbar_lt y x¬ Rbar_le x y.

Lemma Rbar_not_lt_le (x y : Rbar) :
  ¬ Rbar_lt x yRbar_le y x.

Lemma Rbar_le_not_lt (x y : Rbar) :
  Rbar_le y x¬ Rbar_lt x y.

Lemma Rbar_le_refl :
   x : Rbar, Rbar_le x x.

Lemma Rbar_lt_le :
   x y : Rbar,
  Rbar_lt x yRbar_le x y.

Decidability


Lemma Rbar_total_order (x y : Rbar) :
  {Rbar_lt x y} + {x = y} + {Rbar_lt y x}.

Lemma Rbar_eq_dec (x y : Rbar) :
  {x = y} + {x y}.

Lemma Rbar_lt_dec (x y : Rbar) :
  {Rbar_lt x y} + {¬Rbar_lt x y}.

Lemma Rbar_lt_le_dec (x y : Rbar) :
  {Rbar_lt x y} + {Rbar_le y x}.

Lemma Rbar_le_dec (x y : Rbar) :
  {Rbar_le x y} + {¬Rbar_le x y}.

Lemma Rbar_le_lt_dec (x y : Rbar) :
  {Rbar_le x y} + {Rbar_lt y x}.

Lemma Rbar_le_lt_or_eq_dec (x y : Rbar) :
  Rbar_le x y{ Rbar_lt x y } + { x = y }.

Transitivity


Lemma Rbar_lt_trans (x y z : Rbar) :
  Rbar_lt x yRbar_lt y zRbar_lt x z.

Lemma Rbar_lt_le_trans (x y z : Rbar) :
  Rbar_lt x yRbar_le y zRbar_lt x z.

Lemma Rbar_le_lt_trans (x y z : Rbar) :
  Rbar_le x yRbar_lt y zRbar_lt x z.

Lemma Rbar_le_trans (x y z : Rbar) :
  Rbar_le x yRbar_le y zRbar_le x z.

Lemma Rbar_le_antisym (x y : Rbar) :
  Rbar_le x yRbar_le y xx = y.

Properties of operations

Additive operators

Rbar_opp

Rbar_plus


Lemma Rbar_plus'_comm :
   x y, Rbar_plus' x y = Rbar_plus' y x.

Lemma ex_Rbar_plus_comm :
   x y,
  ex_Rbar_plus x yex_Rbar_plus y x.

Lemma ex_Rbar_plus_opp (x y : Rbar) :
  ex_Rbar_plus x yex_Rbar_plus (Rbar_opp x) (Rbar_opp y).

Lemma Rbar_plus_0_r (x : Rbar) : Rbar_plus x (Finite 0) = x.
Lemma Rbar_plus_0_l (x : Rbar) : Rbar_plus (Finite 0) x = x.

Lemma Rbar_plus_comm (x y : Rbar) : Rbar_plus x y = Rbar_plus y x.

Lemma Rbar_plus_lt_compat (a b c d : Rbar) :
  Rbar_lt a bRbar_lt c dRbar_lt (Rbar_plus a c) (Rbar_plus b d).

Lemma Rbar_plus_le_compat (a b c d : Rbar) :
  Rbar_le a bRbar_le c dRbar_le (Rbar_plus a c) (Rbar_plus b d).

Lemma Rbar_plus_opp (x y : Rbar) :
  Rbar_plus (Rbar_opp x) (Rbar_opp y) = Rbar_opp (Rbar_plus x y).

Rbar_minus


Lemma Rbar_minus_eq_0 (x : Rbar) : Rbar_minus x x = 0.
Lemma Rbar_opp_minus (x y : Rbar) :
  Rbar_opp (Rbar_minus x y) = Rbar_minus y x.

Multiplicative

Rbar_inv


Lemma Rbar_inv_opp (x : Rbar) :
  x 0 → Rbar_inv (Rbar_opp x) = Rbar_opp (Rbar_inv x).

Rbar_mult


Lemma Rbar_mult'_comm (x y : Rbar) :
  Rbar_mult' x y = Rbar_mult' y x.

Lemma Rbar_mult'_opp_r (x y : Rbar) :
  Rbar_mult' x (Rbar_opp y) = match Rbar_mult' x y with Some zSome (Rbar_opp z) | NoneNone end.

Lemma Rbar_mult_comm (x y : Rbar) :
  Rbar_mult x y = Rbar_mult y x.
Lemma Rbar_mult_opp_r (x y : Rbar) :
  Rbar_mult x (Rbar_opp y) = (Rbar_opp (Rbar_mult x y)).
Lemma Rbar_mult_opp_l (x y : Rbar) :
  Rbar_mult (Rbar_opp x) y = Rbar_opp (Rbar_mult x y).
Lemma Rbar_mult_opp (x y : Rbar) :
  Rbar_mult (Rbar_opp x) (Rbar_opp y) = Rbar_mult x y.
Lemma Rbar_mult_0_l (x : Rbar) : Rbar_mult 0 x = 0.
Lemma Rbar_mult_0_r (x : Rbar) : Rbar_mult x 0 = 0.

Lemma Rbar_mult_eq_0 (y x : Rbar) :
  Rbar_mult x y = 0 → x = 0 y = 0.

Lemma ex_Rbar_mult_sym (x y : Rbar) :
  ex_Rbar_mult x yex_Rbar_mult y x.
Lemma ex_Rbar_mult_opp_l (x y : Rbar) :
  ex_Rbar_mult x yex_Rbar_mult (Rbar_opp x) y.
Lemma ex_Rbar_mult_opp_r (x y : Rbar) :
  ex_Rbar_mult x yex_Rbar_mult x (Rbar_opp y).

Lemma is_Rbar_mult_sym (x y z : Rbar) :
  is_Rbar_mult x y zis_Rbar_mult y x z.
Lemma is_Rbar_mult_opp_l (x y z : Rbar) :
  is_Rbar_mult x y zis_Rbar_mult (Rbar_opp x) y (Rbar_opp z).
Lemma is_Rbar_mult_opp_r (x y z : Rbar) :
  is_Rbar_mult x y zis_Rbar_mult x (Rbar_opp y) (Rbar_opp z).

Lemma is_Rbar_mult_p_infty_pos (x : Rbar) :
  Rbar_lt 0 xis_Rbar_mult p_infty x p_infty.
Lemma is_Rbar_mult_p_infty_neg (x : Rbar) :
  Rbar_lt x 0 → is_Rbar_mult p_infty x m_infty.
Lemma is_Rbar_mult_m_infty_pos (x : Rbar) :
  Rbar_lt 0 xis_Rbar_mult m_infty x m_infty.
Lemma is_Rbar_mult_m_infty_neg (x : Rbar) :
  Rbar_lt x 0 → is_Rbar_mult m_infty x p_infty.

Rbar_div

Lemma is_Rbar_div_p_infty (x : R) :
  is_Rbar_div x p_infty 0.
Lemma is_Rbar_div_m_infty (x : R) :
  is_Rbar_div x m_infty 0.

Rbar_mult_pos
Rbar_div_pos

Rbar_min


Definition Rbar_min (x y : Rbar) : Rbar :=
  match x, y with
  | z, p_infty | p_infty, zz
  | _ , m_infty | m_infty, _m_infty
  | Finite x, Finite yRmin x y
  end.

Lemma Rbar_lt_locally (a b : Rbar) (x : R) :
  Rbar_lt a xRbar_lt x b
   delta : posreal,
     y, Rabs (y - x) < deltaRbar_lt a y Rbar_lt y b.

Lemma Rbar_min_comm (x y : Rbar) : Rbar_min x y = Rbar_min y x.

Lemma Rbar_min_r (x y : Rbar) : Rbar_le (Rbar_min x y) y.

Lemma Rbar_min_l (x y : Rbar) : Rbar_le (Rbar_min x y) x.

Lemma Rbar_min_case (x y : Rbar) (P : RbarType) :
  P xP yP (Rbar_min x y).
Lemma Rbar_min_case_strong (r1 r2 : Rbar) (P : RbarType) :
  (Rbar_le r1 r2P r1) → (Rbar_le r2 r1P r2)
    → P (Rbar_min r1 r2).

Rbar_abs


Definition Rbar_abs (x : Rbar) :=
  match x with
    | Finite xFinite (Rabs x)
    | _p_infty
  end.

Lemma Rbar_abs_lt_between (x y : Rbar) :
  Rbar_lt (Rbar_abs x) y (Rbar_lt (Rbar_opp y) x Rbar_lt x y).

Lemma Rbar_abs_opp (x : Rbar) :
  Rbar_abs (Rbar_opp x) = Rbar_abs x.

Lemma Rbar_abs_pos (x : Rbar) :
  Rbar_le 0 xRbar_abs x = x.
Lemma Rbar_abs_neg (x : Rbar) :
  Rbar_le x 0 → Rbar_abs x = Rbar_opp x.