Library Coquelicot.Lub

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 mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Markov.

This file gives properties of (least) upper and (greatest) lower bounds, especially in Rbar.
  • There are links between our bounds on Rbar and those of the
standard library on R: for example Lemma Rbar_ub_R_ub between our Rbar_is_upper_bound and the standard library is_upper_bound.
  • From Markov's principle, we deduce the construction of a lub (and
of a glb) in Rbar from any non-empty set of reals: see Lemma ex_lub_Rbar_ne.

Open Scope R_scope.

Bounds for sets in R

Upper and Lower bounds


Definition is_ub_Rbar (E : R → Prop) (l : Rbar) :=
  ∀ (x : R), E x → Rbar_le x l.
Definition is_lb_Rbar (E : R → Prop) (l : Rbar) :=
  ∀ (x : R), E x → Rbar_le l x.

Lemma is_ub_Rbar_opp (E : R → Prop) (l : Rbar) :
  is_lb_Rbar E l ↔ is_ub_Rbar (fun x ⇒ E (- x)) (Rbar_opp l).
Lemma is_lb_Rbar_opp (E : R → Prop) (l : Rbar) :
  is_ub_Rbar E l ↔ is_lb_Rbar (fun x ⇒ E (- x)) (Rbar_opp l).

Decidability

Lemma is_ub_Rbar_dec (E : R → Prop) :
  {l : R | is_ub_Rbar E l} + {(∀ l : R, ¬is_ub_Rbar E l)}.

Lemma is_lb_Rbar_dec (E : R → Prop) :
  {l : R | is_lb_Rbar E l} + {(∀ l : R, ¬is_lb_Rbar E l)}.

Order

Lemma is_ub_Rbar_subset (E1 E2 : R → Prop) (l : Rbar) :
  (∀ x : R, E2 x → E1 x) → is_ub_Rbar E1 l → is_ub_Rbar E2 l.
Lemma is_lb_Rbar_subset (E1 E2 : R → Prop) (l : Rbar) :
  (∀ x : R, E2 x → E1 x) → is_lb_Rbar E1 l → is_lb_Rbar E2 l.

Least upper bound and Greatest Lower Bound


Definition is_lub_Rbar (E : R → Prop) (l : Rbar) :=
  is_ub_Rbar E l ∧ (∀ b, is_ub_Rbar E b → Rbar_le l b).
Definition is_glb_Rbar (E : R → Prop) (l : Rbar) :=
  is_lb_Rbar E l ∧ (∀ b, is_lb_Rbar E b → Rbar_le b l).

Lemma is_lub_Rbar_opp (E : R → Prop) (l : Rbar) :
  is_glb_Rbar E l ↔ is_lub_Rbar (fun x ⇒ E (- x)) (Rbar_opp l).
Lemma is_glb_Rbar_opp (E : R → Prop) (l : Rbar) :
  is_lub_Rbar E l ↔ is_glb_Rbar (fun x ⇒ E (- x)) (Rbar_opp l).

Existence

Lemma ex_lub_Rbar (E : R → Prop) : {l : Rbar | is_lub_Rbar E l}.
Lemma ex_glb_Rbar (E : R → Prop) : {l : Rbar | is_glb_Rbar E l}.

Functions

Definition Lub_Rbar (E : R → Prop) := proj1_sig (ex_lub_Rbar E).
Definition Glb_Rbar (E : R → Prop) := proj1_sig (ex_glb_Rbar E).

Lemma is_lub_Rbar_unique (E : R → Prop) (l : Rbar) :
  is_lub_Rbar E l → Lub_Rbar E = l.
Lemma is_glb_Rbar_unique (E : R → Prop) (l : Rbar) :
  is_glb_Rbar E l → Glb_Rbar E = l.

Lemma Lub_Rbar_correct (E : R → Prop) :
  is_lub_Rbar E (Lub_Rbar E).
Lemma Glb_Rbar_correct (E : R → Prop) :
  is_glb_Rbar E (Glb_Rbar E).

Order

Lemma is_lub_Rbar_subset (E1 E2 : R → Prop) (l1 l2 : Rbar) :
  (∀ x : R, E2 x → E1 x) → is_lub_Rbar E1 l1 → is_lub_Rbar E2 l2
    → Rbar_le l2 l1.
Lemma is_glb_Rbar_subset (E1 E2 : R → Prop) (l1 l2 : Rbar) :
  (∀ x : R, E2 x → E1 x) → is_glb_Rbar E1 l1 → is_glb_Rbar E2 l2
    → Rbar_le l1 l2.

Lemma is_lub_Rbar_eqset (E1 E2 : R → Prop) (l : Rbar) :
  (∀ x : R, E2 x ↔ E1 x) → is_lub_Rbar E1 l → is_lub_Rbar E2 l.
Lemma is_glb_Rbar_eqset (E1 E2 : R → Prop) (l : Rbar) :
  (∀ x : R, E2 x ↔ E1 x) → is_glb_Rbar E1 l → is_glb_Rbar E2 l.

Lemma Lub_Rbar_eqset (E1 E2 : R → Prop) :
  (∀ x, E1 x ↔ E2 x) → Lub_Rbar E1 = Lub_Rbar E2.
Lemma Glb_Rbar_eqset (E1 E2 : R → Prop) :
  (∀ x, E1 x ↔ E2 x) → Glb_Rbar E1 = Glb_Rbar E2.

Bounds for sets in Rbar

Upper and Lower bounds


Definition Rbar_is_upper_bound (E : Rbar → Prop) (l : Rbar) :=
  ∀ x, E x → Rbar_le x l.

Definition Rbar_is_lower_bound (E : Rbar → Prop) (l : Rbar) :=
  ∀ x, E x → Rbar_le l x.

Lemma Rbar_ub_lb (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_upper_bound (fun x ⇒ E (Rbar_opp x)) (Rbar_opp l)
    ↔ Rbar_is_lower_bound E l.
Lemma Rbar_lb_ub (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_lower_bound (fun x ⇒ E (Rbar_opp x)) (Rbar_opp l)
    ↔ Rbar_is_upper_bound E l.

Lemma is_ub_Rbar_correct (E : R → Prop) (l : Rbar) :
  is_ub_Rbar E l ↔ Rbar_is_upper_bound (fun x ⇒ is_finite x ∧ E x) l.
Lemma is_lb_Rbar_correct (E : R → Prop) (l : Rbar) :
  is_lb_Rbar E l ↔ Rbar_is_lower_bound (fun x ⇒ is_finite x ∧ E x) l.

Basic properties

Lemma Rbar_ub_p_infty (E : Rbar → Prop) :
  Rbar_is_upper_bound E p_infty.
Lemma Rbar_lb_m_infty (E : Rbar → Prop) :
  Rbar_is_lower_bound E m_infty.

Lemma Rbar_ub_Finite (E : Rbar → Prop) (l : R) :
  Rbar_is_upper_bound E l →
    is_upper_bound (fun (x : R) ⇒ E x) l.
Lemma Rbar_lb_Finite (E : Rbar → Prop) (l : R) :
  Rbar_is_lower_bound E (Finite l) →
    is_upper_bound (fun x ⇒ E (Finite (- x))) (- l).

Lemma Rbar_ub_m_infty (E : Rbar → Prop) :
  Rbar_is_upper_bound E m_infty → ∀ x, E x → x = m_infty.
Lemma Rbar_lb_p_infty (E : Rbar → Prop) :
  Rbar_is_lower_bound E p_infty → (∀ x, E x → x = p_infty).

Lemma Rbar_lb_le_ub (E : Rbar → Prop) (l1 l2 : Rbar) : (∃ x, E x) →
  Rbar_is_lower_bound E l1 → Rbar_is_upper_bound E l2 → Rbar_le l1 l2.
Lemma Rbar_lb_eq_ub (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_lower_bound E l → Rbar_is_upper_bound E l → ∀ x, E x → x = l.

Decidability

Lemma Rbar_ub_dec (E : Rbar → Prop) (Hp : ¬ E p_infty) :
  {M : R | Rbar_is_upper_bound E M}
    + {(∀ (M : R), ¬Rbar_is_upper_bound E M)}.
Lemma Rbar_lb_dec (E : Rbar → Prop) (Hm : ¬ E m_infty) :
  {M : R | Rbar_is_lower_bound E (Finite M)}
    + {(∀ M, ¬Rbar_is_lower_bound E (Finite M))}.

Order

Lemma Rbar_is_ub_subset (E1 E2 : Rbar → Prop) (l : Rbar) :
  (∀ x, E1 x → E2 x) → (Rbar_is_upper_bound E2 l) → (Rbar_is_upper_bound E1 l).
Lemma Rbar_is_lb_subset (E1 E2 : Rbar → Prop) (l : Rbar) :
  (∀ x, E1 x → E2 x) → (Rbar_is_lower_bound E2 l) → (Rbar_is_lower_bound E1 l).

Least upper bound and Greatest Lower Bound


Definition Rbar_is_lub (E : Rbar → Prop) (l : Rbar) :=
  Rbar_is_upper_bound E l ∧
    (∀ b : Rbar, Rbar_is_upper_bound E b → Rbar_le l b).
Definition Rbar_is_glb (E : Rbar → Prop) (l : Rbar) :=
  Rbar_is_lower_bound E l ∧
    (∀ b : Rbar, Rbar_is_lower_bound E b → Rbar_le b l).

Lemma Rbar_lub_glb (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_lub (fun x ⇒ E (Rbar_opp x)) (Rbar_opp l)
    ↔ Rbar_is_glb E l.
Lemma Rbar_glb_lub (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_glb (fun x ⇒ E (Rbar_opp x)) (Rbar_opp l)
    ↔ Rbar_is_lub E l.

Lemma is_lub_Rbar_correct (E : R → Prop) (l : Rbar) :
  is_lub_Rbar E l ↔ Rbar_is_lub (fun x ⇒ is_finite x ∧ E x) l.
Lemma is_glb_Rbar_correct (E : R → Prop) (l : Rbar) :
  is_glb_Rbar E l ↔ Rbar_is_glb (fun x ⇒ is_finite x ∧ E x) l.

Lemma Rbar_ex_lub (E : Rbar → Prop) :
  {l : Rbar | Rbar_is_lub E l}.

Lemma Rbar_ex_glb (E : Rbar → Prop) :
  {l : Rbar | Rbar_is_glb E l}.

Functions

Definition Rbar_lub (E : Rbar → Prop)
  := proj1_sig (Rbar_ex_lub E).
Definition Rbar_glb (E : Rbar → Prop)
  := proj1_sig (Rbar_ex_glb E).

Lemma Rbar_opp_glb_lub (E : Rbar → Prop) :
  Rbar_glb (fun x ⇒ E (Rbar_opp x)) = Rbar_opp (Rbar_lub E).
Lemma Rbar_opp_lub_glb (E : Rbar → Prop) :
  Rbar_lub (fun x ⇒ E (Rbar_opp x)) = Rbar_opp (Rbar_glb E).

Lemma Rbar_is_lub_unique (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_lub E l → Rbar_lub E = l.
Lemma Rbar_is_glb_unique (E : Rbar → Prop) (l : Rbar) :
  Rbar_is_glb E l → Rbar_glb E = l.

Order

Lemma Rbar_glb_le_lub (E : Rbar → Prop) :
  (∃ x, E x) → Rbar_le (Rbar_glb E) (Rbar_lub E).

Lemma Rbar_is_lub_subset (E1 E2 : Rbar → Prop) (l1 l2 : Rbar) :
  (∀ x, E1 x → E2 x) → (Rbar_is_lub E1 l1) → (Rbar_is_lub E2 l2)
  → Rbar_le l1 l2.
Lemma Rbar_is_glb_subset (E1 E2 : Rbar → Prop) (l1 l2 : Rbar) :
  (∀ x, E2 x → E1 x) → (Rbar_is_glb E1 l1) → (Rbar_is_glb E2 l2)
  → Rbar_le l1 l2.

Lemma Rbar_is_lub_eq (E1 E2 : Rbar → Prop) (l1 l2 : Rbar) :
  (∀ x, E1 x ↔ E2 x) → (Rbar_is_lub E1 l1) → (Rbar_is_lub E2 l2)
  → l1 = l2.
Lemma Rbar_is_glb_eq (E1 E2 : Rbar → Prop) (l1 l2 : Rbar) :
  (∀ x, E1 x ↔ E2 x) → (Rbar_is_glb E1 l1) → (Rbar_is_glb E2 l2)
  → l1 = l2.

Lemma Rbar_is_lub_ext (E1 E2 : Rbar → Prop) (l : Rbar) :
  (∀ x, E1 x ↔ E2 x) → (Rbar_is_lub E1 l) → (Rbar_is_lub E2 l).
Lemma Rbar_is_glb_ext (E1 E2 : Rbar → Prop) (l : Rbar) :
  (∀ x, E1 x ↔ E2 x) → (Rbar_is_glb E1 l) → (Rbar_is_glb E2 l).

Lemma Rbar_lub_subset (E1 E2 : Rbar → Prop) :
  (∀ x, E1 x → E2 x) → Rbar_le (Rbar_lub E1) (Rbar_lub E2).
Lemma Rbar_glb_subset (E1 E2 : Rbar → Prop) :
  (∀ x, E2 x → E1 x) → Rbar_le (Rbar_glb E1) (Rbar_glb E2).

Lemma Rbar_lub_rw (E1 E2 : Rbar → Prop) :
  (∀ x, E1 x ↔ E2 x) → Rbar_lub E1 = Rbar_lub E2.
Lemma Rbar_glb_rw (E1 E2 : Rbar → Prop) :
  (∀ x, E1 x ↔ E2 x) → Rbar_glb E1 = Rbar_glb E2.

Emptiness is decidable


Definition Empty (E : R → Prop) :=
  Lub_Rbar (fun x ⇒ x = 0 ∨ E x) = Glb_Rbar (fun x ⇒ x = 0 ∨ E x)
  ∧ Lub_Rbar (fun x ⇒ x = 1 ∨ E x) = Glb_Rbar (fun x ⇒ x = 1 ∨ E x).

Lemma Empty_correct_1 (E : R → Prop) :
  Empty E → ∀ x, ¬ E x.

Lemma Empty_correct_2 (E : R → Prop) :
  (∀ x, ¬ E x) → Empty E.

Lemma Empty_dec (E : R → Prop) :
  {¬Empty E}+{Empty E}.
Lemma not_Empty_dec (E : R → Prop) : (Decidable.decidable (∃ x, E x)) →
  {(∃ x, E x)} + {(∀ x, ¬ E x)}.

Lemma uniqueness_dec P : (∃ ! x : R, P x) → {x : R | P x}.