Merge pull request #242 from math-comp/uniform_spaces

Insert a structure of uniform space

Author: CohenCyril

CHANGELOG_UNRELEASED.md

@@ -7,9 +7,24 @@
 - in `boolp.v`, new lemma `andC`
 - in `topology.v`:
   + new lemma `open_nbhsE`
+  + `uniformType` a structure for uniform spaces based on entourages
+    (`entourage`)
+  + `uniformType` structure on products, matrices, function spaces
+  + definitions `nbhs_`, `topologyOfEntourageMixin`, `split_ent`, `nbhsP`,
+    `entourage_set`, `entourage_`, `uniformityOfBallMixin`, `nbhs_ball`
+  + lemmas `nbhs_E`, `nbhs_entourageE`, `filter_from_entourageE`,
+    `entourage_refl`, `entourage_filter`, `entourageT`, `entourage_inv`,
+    `entourage_split_ex`, `split_entP`, `entourage_split_ent`,
+    `subset_split_ent`, `entourage_split`, `nbhs_entourage`, `cvg_entourageP`,
+    `cvg_entourage`, `cvg_app_entourageP`, `cvg_mx_entourageP`,
+    `cvg_fct_entourageP`, `entourage_E`, `entourage_ballE`,
+    `entourage_from_ballE`, `entourage_ball`, `entourage_proper_filter`
+  + `completePseudoMetricType` structure
+  + `completePseudoMetricType` structure on matrices and function spaces
 - in `classical_sets.v`:
   + lemmas `setICr`, `setUidPl`, `subsets_disjoint`, `disjoints_subset`, `setDidPl`,
-    `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`
+    `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`,
+    `setMT`
 - in `ereal.v`:
   + notation `\+` (`ereal_scope`) for function addition
   + notations `>` and `>=` for comparison of extended real numbers
@@ -19,7 +34,9 @@
   + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`,
     `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`,
     `lee_subl_addr`, `lte_spaddr`
-- in `normedtype.v`, lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`.
+- in `normedtype.v`:
+  + lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`.
+  + `uniformType` structure for `ereal`
 - in `sequences.v`:
   + definitions `arithmetic`, `geometric`, `geometric_invn`
   + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`,
@@ -33,6 +50,13 @@
 - moved from `normedtype.v` to `boolp.v` and renamed:
   + `forallN` -> `forallNE`
   + `existsN` -> `existsNE`
+- `topology.v`:
+  + `unif_continuous` uses `entourage`
+  + `pseudoMetricType` inherits from `uniformType`
+  + `generic_source_filter` and `set_filter_source` use entourages
+  + `cauchy` is based on entourages and its former version is renamed
+    `cauchy_ball`
+  + `completeType` inherits from `uniformType` and not from `pseudoMetricType`
 
 ### Renamed
 
@@ -78,22 +102,22 @@
   + `Canonical locally'_filter_on` -> `Canonical nbhs'_filter_on`
   + `locally_locally'` -> `nbhs_nbhs'`
   + `Global Instance within_locally_proper` -> `Global Instance within_nbhs_proper`
-  + `locallyP` -> `nbhsP`
-  + `locally_ball` -> `nbhs_ball`
+  + `locallyP` -> `nbhs_ballP`
+  + `locally_ball` -> `nbhsx_ballx`
   + `neigh_ball` -> `open_nbhs_ball`
   + `mx_locally` -> `mx_nbhs`
   + `prod_locally` -> `prod_nbhs`
   + `Filtered.locally_op` -> `Filtered.nbhs_op`
   + `locally_of` -> `nbhs_of`
   + `open_of_locally` -> `open_of_nhbs`
   + `locally_of_open` -> `nbhs_of_open`
-  + `locally_` -> `nbhs_`
-  + lemma `locally_E` -> `nbhs_E`
+  + `locally_` -> `nbhs_ball`
   + lemma `locally_ballE` -> `nbhs_ballE`
   + `locallyW` -> `nearW`
   + `nearW` -> `near_skip_subproof`
   + `locally_infty_gt` -> `nbhs_infty_gt`
   + `locally_infty_ge` -> `nbhs_infty_ge`
+  + `cauchy_entouragesP` -> `cauchy_ballP`
 - in `normedtype.v`:
   + `locallyN` -> `nbhsN`
   + `locallyC` -> `nbhsC`
@@ -169,6 +193,10 @@
 
 ### Removed
 
+- in `topology.v`:
+  + definitions `entourages`, `topologyOfBallMixin`, `ball_set`
+  + lemmas `locally_E`, `entourages_filter`, `cvg_cauchy_ex`
+
 ### Infrastructure
 
 ### Misc

theories/classical_sets.v

@@ -539,6 +539,9 @@ rewrite predeqE => t; split => [capU|cupU i _].
 by rewrite -(setCK (U i)) => CU; apply cupU; exists i.
 Qed.
 
+Lemma setMT {A B} : (@setT A) `*` (@setT B) = setT.
+Proof. by rewrite predeqE. Qed.
+
 Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := Logic.all (is_subset1 \o f).
 Definition is_total {A B} (f : A -> B -> Prop) := Logic.all (nonempty \o f).

theories/derive.v

@@ -170,7 +170,8 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
 rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first.
   apply/eqOP; near=> k; rewrite /cst [`|1 : R^o|]normr1 mulr1.
   near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
-  by exists k; [near: k; exists 0; rewrite real0|move=> ? /=; rewrite sub0r normrN].
+  exists k; first by near: k; exists 0; rewrite real0.
+  by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
 rewrite addfo; first by move=> /eqolim; rewrite cvg_shift add0r.
 by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
 Grab Existential Variables. all: end_near. Qed.
@@ -303,15 +304,15 @@ pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
 rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
   rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
   rewrite /ball_ /= => eX.
-  apply/nbhsP; rewrite nbhs_E.
+  apply/nbhs_ballP.
   by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE // subrr normr0.
 rewrite /g2.
 have [/eqP ->|v0] := boolP (v == 0).
   rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst.
   by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
 apply/cvg_distP => e e0.
-rewrite nearE /=; apply/nbhsP; rewrite nbhs_E.
-have /(littleoP [littleo of k]) /nbhsP[i i0 Hi] : 0 < e / (2 * `|v|).
+rewrite nearE /=; apply/nbhs_ballP.
+have /(littleoP [littleo of k]) /nbhs_ballP[i i0 Hi] : 0 < e / (2 * `|v|).
   by rewrite divr_gt0 // pmulr_rgt0 // normr_gt0.
 exists (i / `|v|); first by rewrite divr_gt0 // normr_gt0.
 move=> /= j; rewrite /ball /= /ball_ add0r normrN.
@@ -447,13 +448,13 @@ Proof.
 apply/eqoP => _ /posnumP[e].
 have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : U) id of f]].
 have := littleoP [littleo of [o_ (0 : V') id of g]].
-move=>  /(_ (e%:num / k%:num)) /(_ _) /nbhsP [//|_ /posnumP[d] hd].
+move=>  /(_ (e%:num / k%:num)) /(_ _) /nbhs_ballP [//|_ /posnumP[d] hd].
 apply: filter_app; near=> x => leOxkx; apply: le_trans (hd _ _) _; last first.
   rewrite -ler_pdivl_mull //; apply: le_trans leOxkx _.
   by rewrite invf_div mulrA -[_ / _ * _]mulrA mulVf // mulr1.
 rewrite -ball_normE /= distrC subr0 (le_lt_trans leOxkx) //.
 rewrite -ltr_pdivl_mull //; near: x; rewrite /= !nbhs_simpl.
-apply/nbhsP; exists (k%:num ^-1 * d%:num)=> // x.
+apply/nbhs_ballP; exists (k%:num ^-1 * d%:num)=> // x.
 by rewrite -ball_normE /= distrC subr0.
 Grab Existential Variables. all: end_near. Qed.
 
@@ -469,14 +470,14 @@ Lemma compOo_eqo  (U V' W' : normedModType R) (f : U -> V')
 Proof.
 apply/eqoP => _ /posnumP[e].
 have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : V') id of g]].
-move=> /nbhsP [_ /posnumP[d] hd].
+move=> /nbhs_ballP [_ /posnumP[d] hd].
 have ekgt0 : e%:num / k%:num > 0 by [].
 have /(_ _ ekgt0) := littleoP [littleo of [o_ (0 : U) id of f]].
 apply: filter_app; near=> x => leoxekx; apply: le_trans (hd _ _) _; last first.
   by rewrite -ler_pdivl_mull // mulrA [_^-1 * _]mulrC.
 rewrite -ball_normE /= distrC subr0; apply: le_lt_trans leoxekx _.
 rewrite -ltr_pdivl_mull //; near: x; rewrite /= nbhs_simpl.
-apply/nbhsP; exists ((e%:num / k%:num) ^-1 * d%:num)=> // x.
+apply/nbhs_ballP; exists ((e%:num / k%:num) ^-1 * d%:num)=> // x.
 by rewrite -ball_normE /= distrC subr0.
 Grab Existential Variables. all: end_near. Qed.
 
@@ -493,7 +494,7 @@ rewrite funeqE => x; apply/eqP; case: (ler0P `|x|) => [|xn0].
   by rewrite normr_le0 => /eqP ->; rewrite linear0.
 rewrite -normr_le0 -(mul0r `|x|) -ler_pdivr_mulr //.
 apply/ler0_addgt0P => _ /posnumP[e]; rewrite ler_pdivr_mulr //.
-have /oid /nbhsP [_ /posnumP[d] dfe] := posnum_gt0 e.
+have /oid /nbhs_ballP [_ /posnumP[d] dfe] := posnum_gt0 e.
 set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1.
 rewrite -{1}(@scalerKV _ _ k _ x) // linearZZ normmZ.
 rewrite -ler_pdivl_mull; last by rewrite gtr0_norm.
@@ -675,8 +676,8 @@ Qed.
 Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) :
   continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|.
 Proof.
-move=> /(_ 0); rewrite linear0 => /(_ _ (nbhs_ball 0 1%:pos)).
-move=> /nbhsP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
+move=> /(_ 0); rewrite linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
 case: (lerP `|x| 0) => [|xn0].
   by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
 set k := 2 / e%:num * (PosNum xn0)%:num.
@@ -744,8 +745,8 @@ Lemma bilinear_schwarz (U V' W' : normedModType R)
   (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) ->
   exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|.
 Proof.
-move=> /(_ 0); rewrite linear0r => /(_ _ (nbhs_ball 0 1%:pos)).
-move=> /nbhsP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
+move=> /(_ 0); rewrite linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)).
+move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
 case: (lerP `|u| 0) => [|un0].
   by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r.
 case: (lerP `|v| 0) => [|vn0].
@@ -780,7 +781,7 @@ rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_le_maxr /= lexx orbT.
 rewrite -ler_pdivl_mull //.
 suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_le_maxr /= lexx.
 near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
-by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite distrC subr0 => /ltW.
+by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite -ball_normE /= distrC subr0 => /ltW.
 Grab Existential Variables. all: end_near. Qed.
 
 Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
@@ -791,8 +792,8 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
 Proof.
 move=> fc; split=> [q|].
   by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
-    move=> A /(fc (_.1, _.2)) /= /nbhsP [_ /posnumP[e] fpqe_A];
-    apply/nbhsP; exists e%:num => // r [??]; exact: (fpqe_A (_.1, _.2)).
+    move=> A /(fc (_.1, _.2)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A];
+    apply/nbhs_ballP; exists e%:num => // r [??]; exact: (fpqe_A (_.1, _.2)).
 apply/eqaddoE; rewrite funeqE => q /=.
 rewrite linearDl !linearDr addrA addrC.
 rewrite -[f q.1 _ + _ + _]addrA [f q.1 _ + _]addrC addrA [f q.1 _ + _]addrC.
@@ -933,7 +934,7 @@ rewrite mulrA mulf_div mulr1.
 have hDx_neq0 : h + x != 0.
   near: h; rewrite !nbhs_simpl; apply/nbhs_normP.
   exists `|x|; first by rewrite normr_gt0.
-  move=> h /=; rewrite distrC subr0 -subr_gt0 => lthx.
+  move=> h /=; rewrite -ball_normE /= distrC subr0 -subr_gt0 => lthx.
   rewrite -(normr_gt0 (h + x : R^o)) addrC -[h]opprK.
   apply: lt_le_trans (ler_dist_dist _ _).
   by rewrite ger0_norm normrN //; apply: ltW.
@@ -1357,7 +1358,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_right_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /nbhsP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
 by exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
 Qed.
 
@@ -1367,7 +1368,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_left_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /nbhsP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
 exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _].
 by apply: xe_A => //; rewrite eq_sym.
 Qed.

theories/landau.v

@@ -1118,11 +1118,11 @@ Lemma near_shift {K : numDomainType} {R : normedModType K}
    (\near x, P x) = (\forall z \near y, (P \o shift (x - y)) z).
 Proof.
 rewrite propeqE; split=> /= /nbhs_normP [_/posnumP[e] ye];
-apply/nbhs_normP; exists e%:num => // t /= et.
-  apply: ye; rewrite /= !opprD addrA addrACA subrr add0r.
+apply/nbhs_normP; exists e%:num => // t; rewrite -ball_normE /= => et.
+  apply: ye; rewrite -ball_normE /= !opprD addrA addrACA subrr add0r.
   by rewrite opprK addrC.
 have /= := ye (t - (x - y)); rewrite addrNK; apply.
-by rewrite opprB addrCA opprD addrA subrr add0r opprB.
+by rewrite -ball_normE /= opprB addrCA opprD addrA subrr add0r opprB.
 Qed.
 
 Lemma cvg_shift {T : Type} {K : numDomainType} {R : normedModType K}
@@ -1157,7 +1157,7 @@ suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.
   near +oo => k; near=> y.
   rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivl_mull; last by near: k; exists 0; rewrite real0.
   near: y; apply/nbhs_normP.
-  eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
+  eexists; last by move=> ?; rewrite -ball_normE /= sub0r normrN; apply.
   by rewrite mulr_gt0 // invr_gt0; near: k; exists 0; rewrite real0.
 have /nbhs_normP [_/posnumP[d]] := Of1.
 rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
@@ -1169,7 +1169,7 @@ rewrite -[X in _ <= X]mulr1 -ler_pdivr_mull ?pmulr_rgt0 //; last by near: k; exi
 rewrite -(ler_pmul2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
 rewrite -normm_s.
 have <- : GRing.Scale.op s_law =2 s by rewrite GRing.Scale.opE.
-rewrite -linearZ fk //= distrC subr0 normmZ ger0_norm //.
+rewrite -linearZ fk //= -ball_normE /= distrC subr0 normmZ ger0_norm //.
 rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivr_mulr //; last by near: k; exists 0; rewrite real0.
 rewrite mulrC -ltr_pdivr_mulr //; near: k; apply: nbhs_pinfty_gt.
 Grab Existential Variables. all: end_near. Qed.

theories/misc/uniform_bigO.v

@@ -1,14 +1,16 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
-From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum.
+From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 Require Import boolp reals Rstruct Rbar.
 Require Import classical_sets posnum topology normedtype landau.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Import GRing.Theory Num.Def Num.Theory.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+
+Local Open Scope ring_scope.
 
 Section UniformBigO.
 
@@ -36,22 +38,25 @@ Definition OuP (f : A -> R * R -> R) (g : R * R -> R) :=
 
 (* first we replace sig with ex and the l^2 norm with the l^oo norm *)
 
+Let normedR2 := [normedModType _ of (R^o * R^o)].
+
 Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
   exists2 alp, 0 < alp & exists2 C, 0 < C &
-    forall X, forall dX : R^o * R^o, `|[dX]| < alp -> P dX ->
-    `|[f X dX]| <= C * `|[g dX]|.
+    forall X, forall dX : normedR2,
+    `|dX| < alp -> P dX -> `|f X dX| <= C * `|g dX|.
 
-Lemma ler_norm2 (x : R^o * R^o) :
-  `|[x]| <= sqrt (Rsqr (fst x) + Rsqr (snd x)) <= Num.sqrt 2 * `|[x]|.
+Lemma ler_norm2 (x : normedR2) :
+  `|x| <= sqrt (Rsqr (fst x) + Rsqr (snd x)) <= Num.sqrt 2 * `|x|.
 Proof.
 rewrite RsqrtE; last by rewrite addr_ge0 //; apply/RleP/Rle_0_sqr.
 rewrite !Rsqr_pow2 !RpowE; apply/andP; split.
-  by rewrite ler_maxl; apply/andP; split;
-    rewrite -[`|[_]|]sqrtr_sqr ler_wsqrtr // (ler_addl, ler_addr) sqr_ge0.
+  by rewrite le_maxl; apply/andP; split;
+    rewrite -[`|_|]sqrtr_sqr ler_wsqrtr // (ler_addl, ler_addr) sqr_ge0.
 wlog lex12 : x / (`|x.1| <= `|x.2|).
-  move=> ler_norm; case: (lerP `|x.1| `|x.2|) => [/ler_norm|/ltrW lex21] //.
-  by rewrite addrC [`|[_]|]maxrC (ler_norm (x.2, x.1)).
-rewrite [`|[_]|]maxr_r // [`|[_]|]absRE -[X in X * _]ger0_norm // -normrM.
+  move=> ler_norm; case: (lerP `|x.1| `|x.2|) => [/ler_norm|] //.
+  rewrite lt_leAnge => /andP [lex21 _].
+  by rewrite addrC [`|_|]maxC (ler_norm (x.2, x.1)).
+rewrite [`|_|]max_r // -[X in X * _]ger0_norm // -normrM.
 rewrite -sqrtr_sqr ler_wsqrtr // exprMn sqr_sqrtr // mulr_natl mulr2n ler_add2r.
 rewrite -[_ ^+ 2]ger0_norm ?sqr_ge0 // -[X in _ <=X]ger0_norm ?sqr_ge0 //.
 by rewrite !normrX ler_expn2r // nnegrE normr_ge0.
@@ -61,7 +66,7 @@ Lemma OuP_to_ex f g : OuP f g -> OuPex f g.
 Proof.
 move=> [_ [_ [/posnumP[a] [/posnumP[C] fOg]]]].
 exists (a%:num / Num.sqrt 2) => //; exists C%:num => // x dx ltdxa Pdx.
-apply: fOg; move: ltdxa; rewrite ltr_pdivl_mulr //; apply: ler_lt_trans.
+apply: fOg; move: ltdxa; rewrite ltr_pdivl_mulr //; apply: le_lt_trans.
 by rewrite mulrC; have /andP[] := ler_norm2 dx.
 Qed.
 
@@ -70,7 +75,7 @@ Proof.
 move=> /exists2P /getPex; set Q := fun a => _ /\ _ => - [lt0getQ].
 move=> /exists2P /getPex; set R := fun C => _ /\ _ => - [lt0getR fOg].
 apply: existT (get Q) _; apply: exist (get R) _; split=> //; split => //.
-move=> x dx ltdxgetQ; apply: fOg; apply: ler_lt_trans ltdxgetQ.
+move=> x dx ltdxgetQ; apply: fOg; apply: le_lt_trans ltdxgetQ.
 by have /andP [] := ler_norm2 dx.
 Qed.
 
@@ -83,26 +88,27 @@ Definition OuO (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
 Lemma OuP_to_O f g : OuP f g -> OuO f g.
 Proof.
 move=> /OuP_to_ex [_/posnumP[a] [_/posnumP[C] fOg]].
-apply/eqOP; near=> k; near=> x; apply: ler_trans (fOg _ _ _ _) _; last 2 first.
+apply/eqOP; near=> k; near=> x; apply: le_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.
+- rewrite ler_pmul => //; near: k; exists C%:num; split.
+    exact: posnum_real.
+  by move=> ?; rewrite lt_leAnge => /andP[].
 - 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.
+    by split=> //=; rewrite /within; near=> x =>_; near: x; apply: nbhsx_ballx.
+  move=> x [_ [/=]]; rewrite -ball_normE /= distrC subr0 distrC subr0.
+  by move=> ??; rewrite lt_maxl; apply/andP.
 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=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]].
+have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_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.
+exists (maxr 1 (k + 1)); first by rewrite lt_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.
+move: dxe; rewrite lt_maxl !lt_minr => /andP[/andP [dxe11 _] /andP [_ dxe22]].
+by apply/sRQ => //; split; [apply/Re1|apply/Re2]; rewrite /= distrC subr0.
 Qed.
 
-End UniformBigO.
+End UniformBigO.