Library Coquelicot.Compactness

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 mathcomp.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 : 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
  | O ⇒ unit
  | S n ⇒ (T × Tn n T)%type
  end.

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
  | O ⇒ fun a b x : Tn O R ⇒ True
  | S n ⇒ fun 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 R → Tn n R → Prop :=
  match n return Tn n R → Tn n R → Prop with
  | O ⇒ fun x t : Tn O R ⇒ True
  | S n ⇒ fun 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 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

Lemma compactness_value :
∀ n a b (delta : Tn n R → posreal),
{ 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 : 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 }.