Library Coquelicot.Compactness

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

This file describes compactness results: finite covering of opens, finite covering based on a gauge function, specific instances for 1D and 2D spaces.

Require Import Rcomplements.

Open Scope R_scope.

Lemma completeness_any :
   P : RProp,
  ( x y, x yP yP x ) →
   He : ( x, P x),
   Hb : (bound P),
   x, x < proj1_sig (completeness _ Hb He) →
  ¬ ¬ P x.

Lemma false_not_not :
   P Q : Prop, (P¬Q) → (~~P¬Q).

Section Compactness.

Fixpoint Tn n T : Type :=
  match n with
  | Ounit
  | S n ⇒ (T × Tn n T)%type
  end.

Fixpoint bounded_n n : Tn n RTn n RTn n RProp :=
  match n return Tn n RTn n RTn n RProp with
  | Ofun a b x : Tn O RTrue
  | S nfun a b x : Tn (S n) R
    let '(a1,a2) := a in
    let '(b1,b2) := b in
    let '(x1,x2) := x in
    a1 x1 b1 bounded_n n a2 b2 x2
  end.

Fixpoint close_n n d : Tn n RTn n RProp :=
  match n return Tn n RTn n RProp with
  | Ofun x t : Tn O RTrue
  | S nfun x t : Tn (S n) R
    let '(x1,x2) := x in
    let '(t1,t2) := t in
    Rabs (x1 - t1) < d close_n n d x2 t2
  end.

Compactness: there is a finite covering of opens


Lemma compactness_list :
   n a b (delta : Tn n Rposreal),
  ~~ l, x, bounded_n n a b x t, In t l bounded_n n a b t close_n n (delta t) x t.

Compactness: there is a covering based on a gauge function


Lemma compactness_value :
   n a b (delta : Tn n Rposreal),
  { d : posreal | x, bounded_n n a b x~~ t, bounded_n n a b t close_n n (delta t) x t d delta t }.

End Compactness.

Specific instances of compactness for 1D and 2D spaces


Lemma compactness_value_1d :
   a b (delta : Rposreal),
  { d : posreal | x, a x b~~ t, a t b Rabs (x - t) < delta t d delta t }.

Lemma compactness_value_2d :
   a b a' b' (delta : RRposreal),
  { d : posreal | x y, a x ba' y b'
    ~~ u, v, a u b a' v b' Rabs (x - u) < delta u v Rabs (y - v) < delta u v d delta u v }.