Replace balls with entourages and separate normed spaces

Author: damien rouhling

AUTHORS.md

@@ -7,9 +7,9 @@
 - Pierre-Yves Strub, École polytechnique
 
 # Acknowledgments
-- `hierarchy.v` is a reimplementation of file `Hierarchy.v` from the
-  library Coquelicot by Sylvie Boldo, Catherine Lelay, and Guillaume
-  Melquiond (http://coquelicot.saclay.inria.fr/)
+- `topology.v` and `normedtype.v` contain a reimplementation of file
+  `Hierarchy.v` from the library Coquelicot by Sylvie Boldo, Catherine Lelay,
+  and Guillaume Melquiond (http://coquelicot.saclay.inria.fr/)
 - our proof of Zorn's Lemma in `set.v` is a reimplementation of the one by
   Daniel Schepler (https://github.com/coq-contribs/zorns-lemma); we also took
   inspiration from his work on topology

FILES.md

@@ -5,7 +5,7 @@
 - `posnum.v`
 - `classical_set.v`
 - `topology.v`
-- `hierarchy.v`
+- `normedtype.v`
 - `landau.v`
 - `derive.v`
 - `README.md`

_CoqProject

@@ -9,7 +9,7 @@ classical_sets.v
 Rstruct.v
 Rbar.v
 topology.v
-hierarchy.v
+normedtype.v
 forms.v
 derive.v
 summability.v

classical_sets.v

@@ -334,6 +334,9 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
 by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
 Qed.
 
+Lemma setMT A B : (@setT A) `*` (@setT B) = setT.
+Proof. by rewrite predeqE. Qed.
+
 Definition is_prop {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := all (is_prop \o f).
 Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).

derive.v

@@ -3,7 +3,7 @@ Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum.
 Require Import boolp reals Rstruct Rbar.
-Require Import classical_sets posnum topology hierarchy.
+Require Import classical_sets posnum topology normedtype.
 
 (******************************************************************************)
 (*              BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O                  *)

landau.v

@@ -3,7 +3,7 @@ Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum.
 Require Import boolp reals Rstruct Rbar.
-Require Import classical_sets posnum topology hierarchy landau.
+Require Import classical_sets posnum topology normedtype landau.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -86,23 +86,21 @@ move=> /OuP_to_ex [_/posnumP[a] [_/posnumP[C] fOg]].
 apply/eqOP; near=> k; near=> x; apply: ler_trans (fOg _ _ _ _) _; last 2 first.
 - by near: x; exists (setT, P); [split=> //=; apply: withinT|move=> ? []].
 - by rewrite ler_pmul => //; near: k; exists C%:num => ? /ltrW.
-- near: x; exists (setT, ball (0 : R^o * R^o) a%:num).
-    by split=> //=; rewrite /within; near=> x =>_; near: x; apply: locally_ball.
-  move=> x [_ [/=]]; rewrite -ball_normE /= normmB subr0 normmB subr0.
-  by move=> ??; rewrite ltr_maxl; apply/andP.
+- near: x; exists (setT, ball norm (0 : R^o * R^o) a%:num); last first.
+    by move=> x [_ /=]; rewrite normmB subr0.
+  split=> //=; rewrite /within; near=> x =>_; near: x.
+  exact: (@locally_ball _ [normedModType R of R^o * R^o]).
 Grab Existential Variables. all: end_near. Qed.
 
 Lemma OuO_to_P f g : OuO f g -> OuP f g.
 Proof.
 move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k hk].
 have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite ltr_maxr ltr_addl orbC ltr01.
-move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg.
-exists (minr e1%:num e2%:num) => //.
-exists (maxr 1 (k + 1)); first by rewrite ltr_maxr ltr01.
+rewrite /= -(@filter_from_norm_locally _ [normedModType R of R^o * R^o]).
+move=> -[_/posnumP[e] seQ] fOg; exists e%:num => //; exists (maxr 1 (k + 1)).
+  by rewrite ltr_maxr ltr01.
 move=> x dx dxe Pdx; apply: (fOg (x, dx)); split=> //=.
-move: dxe; rewrite ltr_maxl !ltr_minr => /andP[/andP [dxe11 _] /andP [_ dxe22]].
-by apply/sRQ => //; split; [apply/Re1|apply/Re2];
-  rewrite /AbsRing_ball /= absrB subr0.
+by apply: seQ => //; rewrite /ball normmB subr0.
 Qed.
 
 End UniformBigO.