Library Coqtail.Topology.Metrics


Topological space


Require Import Reals.
Require Import Ensembles.
Require Import Topology.
Require Import Fourier.

Metric Space


Class Metric_Space
  (X : Type)
  (d : XXR)
:= {
  metric_pos : x y, (0 d x y)%R;
  metric_sym : x y, d x y = d y x;
  metric_refl : x y, (d x y = 0 x = y)%R;
  metric_tri : x y z, (d x y d x z + d z y)%R
}.

Open sets


Section Open_sets.
  Variable X : Type.
  Variable d : XXR.

  Open Scope R_scope.

  Definition metric_open W: Prop :=
     x, In _ W x eps:R, 0 < eps
     y, d x y < epsIn _ W y.

End Open_sets.

Balls


Section Balls.
  Variable X : Type.
  Variable d : XXR.
  Variable E : Metric_Space X d.

  Inductive open_ball c r (rpos : (0 < r)%R) : Ensemble X :=
    open_ball_intro : x, (d x c < r)%RIn _ (open_ball c r rpos) x.

  Inductive closed_ball c r (rpos : (0 < r)%R) : Ensemble X :=
    closed_ball_intro : x, (d x c r)%RIn _ (closed_ball c r rpos) x.

  Lemma open_ball_is_open : c r rpos, metric_open X d (open_ball c r rpos).
  Proof.
  intros c r rpos x Hx.
  destruct Hx as [x Hxc].
   (r - d x c)%R; split.
   apply Rlt_Rminus; auto.

   intros y Hxy.
   constructor.
   eapply Rle_lt_trans.
    apply (metric_tri _ _ x).

    rewrite (metric_sym y x); fourier.
  Qed.
End Balls.

A metric space defines a topology


Section Metric_topology.
  Variable X : Type.
  Variable d : XXR.

  Fact metric_open_empty_set : metric_open X d (Empty_set _).
  intros x H.
  inversion H.
  Qed.

  Fact metric_open_full_set : metric_open X d (Full_set _).
  intros x _.
   1%R.
  split. intuition.
  intros y _.
  constructor.
  Qed.

  Fact metric_intersection_stable : A B : Ensemble _,
    metric_open X d Ametric_open X d B
    metric_open X d (Intersection _ A B).
  intros A B OA OB.
  intros x [y yA yB].
  elim (OA y). intros epsa [epsapos opena].
  elim (OB y). intros epsb [epsbpos openb].
   (Rmin epsa epsb).
  split.
    apply Rmin_Rgt_r.
    split; assumption.
  intros x' inx'.
  apply Rmin_Rgt_l in inx' as [ax' bx'].
  apply Intersection_intro;
    [apply opena | apply openb];
    apply Rgt_lt; assumption.
  assumption.
  assumption.
  Qed.

  Fact metric_union_stable : I : Type, Ai : IEnsemble _,
   ( i : I, metric_open X d (Ai i)) → metric_open X d (Infinite_Union _ I Ai).
  intros I Ai openAi.
  intros x xinU.
  induction xinU.
  elim H. intros i inxAi.
  elim (openAi i x).
  intros eps [epspos B].
   eps.
  split.
    exact epspos.
    intros y yinB.
  . i.
  apply (B _ yinB).
  assumption.
  Qed.

  Instance metric_space_topological : Topological_Space _ (Full_set _) (metric_open X d) := {
    open_empty_set := metric_open_empty_set;
    open_full_set := metric_open_full_set;
    intersection_stable := metric_intersection_stable;
    union_stable := metric_union_stable
  }.
End Metric_topology.

A metric space is separated


Lemma metric_space_is_separated : X d (MX : Metric_Space X d),
  separated_space X (Full_set X) (metric_open X d).
Proof.
intros X d MX x y _ _ H.
apply (proj1 (metric_refl _ _)).
destruct (Rtotal_order (d x y) 0%R) as [|[|]]; auto.
 apply RIneq.Rle_not_lt in H0.
  contradiction.
  apply metric_pos.
 pose (d x y / 2)%R as r.
 assert (rpos : 0 < r).
  unfold r; fourier.
 pose (fun copen_ball X d c r rpos) as ball.
 assert (centerinball : x, ball x x).
  constructor.
  rewrite (proj2 (metric_refl _ _)); auto.
 destruct (H (ball x) (ball y)
  (open_ball_is_open _ _ _ _ _ _)
  (open_ball_is_open _ _ _ _ _ _)
  (centerinball _)
  (centerinball _)) as [z []].
 destruct H1 as [z H1].
 destruct H2 as [z H2].
 unfold r in ×.
 assert (d x y < d x y).
  apply Rle_lt_trans with (d z x + d z y).
   rewrite metric_sym with z x; apply metric_tri.

   replace (d x y) with (d x y / 2 + d x y / 2) by field.
   apply Rplus_lt_compat; auto.
 apply Rlt_irrefl in H3.
 contradiction.
Qed.