Library Coquelicot.Compactness

This file is part of the Coquelicot formalization of real analysis in Coq:
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.

From Coq Require Import Reals List ssreflect.

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 : R Prop,
  ( x y, x y P y P 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

Fixpoint bounded_n n : Tn n R Tn n R Tn n R Prop :=
  match n return Tn n R Tn n R Tn n R Prop 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

Fixpoint close_n n d : Tn n R Tn n R Prop :=
  match n return Tn n R Tn n R Prop 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

Compactness: there is a finite covering of opens

Lemma compactness_list :
   n a b (delta : Tn n R posreal),
  ~~ 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

Specific instances of compactness for 1D and 2D spaces

Lemma compactness_value_1d :
   a b (delta : R posreal),
  { 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 : R R posreal),
  { d : posreal | x y, a x b a' 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 }.