diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fbd713a931..ef3b44fd86 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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,8 +102,8 @@ + `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` @@ -87,13 +111,13 @@ + `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 diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 701dc9f090..50090397e2 100644 --- a/theories/classical_sets.v +++ b/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). diff --git a/theories/derive.v b/theories/derive.v index 277ebcb2d4..512826bbc2 100644 --- a/theories/derive.v +++ b/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. diff --git a/theories/landau.v b/theories/landau.v index 9e2d47d8c0..90e2251a26 100644 --- a/theories/landau.v +++ b/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. diff --git a/theories/misc/uniform_bigO.v b/theories/misc/uniform_bigO.v index 5da5479d77..eee8016e1d 100644 --- a/theories/misc/uniform_bigO.v +++ b/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. \ No newline at end of file +End UniformBigO. diff --git a/theories/normedtype.v b/theories/normedtype.v index 8497f242c5..aa5f1a6b25 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -239,7 +239,8 @@ Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0. Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K) : filteredType R := Filtered.Pack (Filtered.Class - (@Pointed.class (pointed_of_zmodule R)) (nbhs_ (ball_ (fun x => `|x|)))). + (@Pointed.class (pointed_of_zmodule R)) + (nbhs_ball_ (ball_ (fun x => `|x|)))). Section pseudoMetric_of_normedDomain. Variables (K : numDomainType) (R : normedZmodType K). @@ -255,17 +256,32 @@ move=> /= ? ?; rewrite -(subr0 x) -(subrr y) opprD opprK (addrA x _ y) -addrA. by rewrite (le_lt_trans (ler_norm_add _ _)) // ltr_add. Qed. Definition pseudoMetric_of_normedDomain - : PseudoMetric.mixin_of K (@nbhs_ K R R (ball_ (fun x => `|x|))) + : PseudoMetric.mixin_of K (@entourage_ K R R (ball_ (fun x => `|x|))) := PseudoMetricMixin ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. -End pseudoMetric_of_normedDomain. +Lemma nbhs_ball_normE : + @nbhs_ball_ K R R (ball_ normr) = nbhs_ (entourage_ (ball_ normr)). +Proof. +rewrite /nbhs_ entourage_E predeq2E => x A; split. + move=> [e egt0 sbeA]. + by exists [set xy | ball_ normr xy.1 e xy.2] => //; exists e. +by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE. +Qed. +End pseudoMetric_of_normedDomain. Canonical R_pointedType := [pointedType of Rdefinitions.R for pointed_of_zmodule R_ringType]. (* NB: similar definition in topology.v *) Canonical R_filteredType := [filteredType Rdefinitions.R of Rdefinitions.R for filtered_of_normedZmod R_normedZmodType]. Canonical R_topologicalType : topologicalType := TopologicalType Rdefinitions.R - (topologyOfBallMixin (pseudoMetric_of_normedDomain R_normedZmodType)). + (topologyOfEntourageMixin + (uniformityOfBallMixin + (@nbhs_ball_normE _ R_normedZmodType) + (pseudoMetric_of_normedDomain R_normedZmodType))). +Canonical R_uniformType : uniformType := + UniformType Rdefinitions.R + (uniformityOfBallMixin (@nbhs_ball_normE _ R_normedZmodType) + (pseudoMetric_of_normedDomain R_normedZmodType)). Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType := PseudoMetricType Rdefinitions.R (pseudoMetric_of_normedDomain R_normedZmodType). @@ -277,25 +293,32 @@ Canonical numFieldType_pointedType := Canonical numFieldType_filteredType := [filteredType R of R^o for filtered_of_normedZmod R]. Canonical numFieldType_topologicalType : topologicalType := TopologicalType R^o - (topologyOfBallMixin (pseudoMetric_of_normedDomain [normedZmodType R of R])). + (topologyOfEntourageMixin + (uniformityOfBallMixin + (@nbhs_ball_normE _ [normedZmodType R of R]) + (pseudoMetric_of_normedDomain [normedZmodType R of R]))). +Canonical numFieldType_uniformType : uniformType := UniformType R^o + (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) + (pseudoMetric_of_normedDomain [normedZmodType R of R])). Canonical numFieldType_pseudoMetricType := @PseudoMetric.Pack R R^o (@PseudoMetric.Class R R - (Topological.class numFieldType_topologicalType) (@pseudoMetric_of_normedDomain R R)). + (Uniform.class numFieldType_uniformType) (@pseudoMetric_of_normedDomain R R)). Definition numdFieldType_lalgType : lalgType R := @GRing.regular_lalgType R. End numFieldType_canonical. Lemma nbhsN (R : numFieldType) (x : R^o) : nbhs (- x) = [set [set - y | y in A] | A in nbhs x]. Proof. +rewrite -!(@filter_from_ballE _ [pseudoMetricType R of R^o]). rewrite predeqE => A; split=> [[e egt0 oppxe_A]|[B [e egt0 xe_B] <-]]; last first. exists e => // y xe_y; exists (- y); last by rewrite opprK. apply/xe_B. - by rewrite /ball_ opprK -normrN -mulN1r mulrDr !mulN1r. + by rewrite /ball /= opprK -normrN -mulN1r mulrDr !mulN1r. exists [set - y | y in A]; last first. rewrite predeqE => y; split=> [[z [t At <- <-]]|Ay]; first by rewrite opprK. by exists (- y); [exists y|rewrite opprK]. exists e => // y xe_y; exists (- y); last by rewrite opprK. -by apply/oppxe_A; rewrite /ball_ distrC opprK addrC. +by apply/oppxe_A; rewrite /ball /= distrC opprK addrC. Qed. Lemma openN (R : numFieldType) (A : set R^o) : @@ -319,8 +342,8 @@ Qed. Module PseudoMetricNormedZmodule. Section ClassDef. Variable R : numDomainType. -Record mixin_of (T : normedZmodType R) (nbhs : T -> set (set T)) - (m : PseudoMetric.mixin_of R nbhs) := Mixin { +Record mixin_of (T : normedZmodType R) (ent : set (set (T * T))) + (m : PseudoMetric.mixin_of R ent) := Mixin { _ : PseudoMetric.ball m = ball_ (fun x => `| x |) }. Record class_of (T : Type) := Class { @@ -328,16 +351,20 @@ Record class_of (T : Type) := Class { pointed_mixin : Pointed.point_of T ; nbhs_mixin : Filtered.nbhs_of T T ; topological_mixin : @Topological.mixin_of T nbhs_mixin ; - pseudoMetric_mixin : @PseudoMetric.mixin_of R T nbhs_mixin ; + uniform_mixin : @Uniform.mixin_of T nbhs_mixin ; + pseudoMetric_mixin : + @PseudoMetric.mixin_of R T (Uniform.entourage uniform_mixin) ; mixin : @mixin_of (Num.NormedZmodule.Pack _ base) _ pseudoMetric_mixin }. Local Coercion base : class_of >-> Num.NormedZmodule.class_of. Definition base2 T c := @PseudoMetric.Class _ _ - (@Topological.Class _ - (Filtered.Class - (Pointed.Class (@base T c) (pointed_mixin c)) - (nbhs_mixin c)) - (topological_mixin c)) + (@Uniform.Class _ + (@Topological.Class _ + (Filtered.Class + (Pointed.Class (@base T c) (pointed_mixin c)) + (nbhs_mixin c)) + (topological_mixin c)) + (uniform_mixin c)) (pseudoMetric_mixin c). Local Coercion base2 : class_of >-> PseudoMetric.class_of. (* TODO: base3? *) @@ -358,7 +385,7 @@ Definition pack (b0 : Num.NormedZmodule.class_of R T) lm0 um0 & phant_id (@Num.NormedZmodule.class R (Phant R) bT) b => fun uT (u : PseudoMetric.class_of R T) & phant_id (@PseudoMetric.class R uT) u => fun (m : @mixin_of (Num.NormedZmodule.Pack _ b) _ u) & phant_id m m0 => - @Pack phR T (@Class T b u u u u m). + @Pack phR T (@Class T b u u u u u m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -367,14 +394,17 @@ Definition normedZmodType := @Num.NormedZmodule.Pack R phR cT xclass. Definition pointedType := @Pointed.Pack cT xclass. Definition filteredType := @Filtered.Pack xT cT xclass. Definition topologicalType := @Topological.Pack cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. Definition pseudoMetricType := @PseudoMetric.Pack R cT xclass. Definition pointed_zmodType := @GRing.Zmodule.Pack pointedType xclass. Definition filtered_zmodType := @GRing.Zmodule.Pack filteredType xclass. Definition topological_zmodType := @GRing.Zmodule.Pack topologicalType xclass. +Definition uniform_zmodType := @GRing.Zmodule.Pack uniformType xclass. Definition pseudoMetric_zmodType := @GRing.Zmodule.Pack pseudoMetricType xclass. Definition pointed_normedZmodType := @Num.NormedZmodule.Pack R phR pointedType xclass. Definition filtered_normedZmodType := @Num.NormedZmodule.Pack R phR filteredType xclass. Definition topological_normedZmodType := @Num.NormedZmodule.Pack R phR topologicalType xclass. +Definition uniform_normedZmodType := @Num.NormedZmodule.Pack R phR uniformType xclass. Definition pseudoMetric_normedZmodType := @Num.NormedZmodule.Pack R phR pseudoMetricType xclass. End ClassDef. @@ -400,15 +430,19 @@ Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. Coercion pseudoMetricType : type >-> PseudoMetric.type. Canonical pseudoMetricType. Canonical pointed_zmodType. Canonical filtered_zmodType. Canonical topological_zmodType. +Canonical uniform_zmodType. Canonical pseudoMetric_zmodType. Canonical pointed_normedZmodType. Canonical filtered_normedZmodType. Canonical topological_normedZmodType. +Canonical uniform_normedZmodType. Canonical pseudoMetric_normedZmodType. Notation pseudoMetricNormedZmodType R := (type (Phant R)). Notation PseudoMetricNormedZmodType R T m := @@ -431,7 +465,7 @@ Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}. Local Notation ball_norm := (ball_ (@normr K V)). Lemma ball_normE : ball_norm = ball. -Proof. by case: V => ? [? ? ? ? ? []]. Qed. +Proof. by case: V => ? [? ? ? ? ? ? []]. Qed. End pseudoMetricnormedzmodule_lemmas. @@ -482,19 +516,19 @@ Qed. Lemma nbhsC (x : T) (P : set T) : ~ (forall eps : {posnum R}, ~ (ball x eps%:num `<=` ~` P)) -> nbhs x (~` P). -Proof. by move=> /ex_ball_sig [e] ?; apply/nbhsP; exists e%:num. Qed. +Proof. by move=> /ex_ball_sig [e] ?; apply/nbhs_ballP; exists e%:num. Qed. Lemma nbhsC_ball (x : T) (P : set T) : nbhs x (~` P) -> {d : {posnum R} | ball x d%:num `<=` ~` P}. Proof. -move=> /nbhsP xNP; apply: ex_ball_sig. +move=> /nbhs_ballP xNP; apply: ex_ball_sig. by have [_ /posnumP[e] eP /(_ _ eP)] := xNP. Qed. Lemma nbhs_ex (x : T) (P : T -> Prop) : nbhs x P -> {d : {posnum R} | forall y, ball x d%:num y -> P y}. Proof. -move=> /nbhsP xP. +move=> /nbhs_ballP xP. pose D := [set d : R | d > 0 /\ forall y, ball x d y -> P y]. have [|d_gt0 dP] := @getPex _ D; last by exists (PosNum d_gt0). by move: xP => [e bP]; exists (e : R). @@ -540,17 +574,17 @@ Qed. Lemma coord_continuous {K : numFieldType} m n i j : continuous (fun M : 'M[K^o]_(m.+1, n.+1) => M i j). Proof. -move=> /= M s /= /(nbhsP (M i j)); rewrite nbhs_E => -[e e0 es]. -apply/nbhsP; rewrite nbhs_E; exists e => //= N MN; exact/es/MN. +move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es]. +apply/nbhs_ballP; exists e => //= N MN; exact/es/MN. Qed. Global Instance Proper_nbhs'_numFieldType (R : numFieldType) (x : R^o) : ProperFilter (nbhs' x). Proof. -apply: Build_ProperFilter => A [_/posnumP[e] Ae]. +apply: Build_ProperFilter => A /nbhs_ballP[_/posnumP[e] Ae]. exists (x + e%:num / 2); apply: Ae; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym. -rewrite /= opprD addrA subrr distrC subr0 ger0_norm //. +rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. by rewrite {2}(splitr e%:num) ltr_spaddl. Qed. @@ -658,7 +692,8 @@ Proof. case=> [x| |]. - case: (ereal_nbhs'_filter x%:E) => x0 [//=nxT xI xS]. apply Build_ProperFilter => //=. - by move=> P [r r0 xr]; exists x%:E; apply xr => //=; rewrite subrr normr0. + move=> P /nbhs_ballP[r r0 xr]; exists x%:E; apply xr => //=. + by rewrite /ball /= subrr normr0. apply Build_Filter => //=. by rewrite nbhsE'. move=> P Q. @@ -681,21 +716,21 @@ Lemma ereal_nbhs_singleton (p : {ereal R}) (A : set {ereal R}) : ereal_nbhs p A -> A p. Proof. move: p => -[p | [M [Mreal MA]] | [M [Mreal MA]]] /=; [|exact: MA | exact: MA]. -move/nbhsP; rewrite nbhs_E => -[_/posnumP[e]]; apply; exact/ballxx. +move=> /nbhs_ballP[_/posnumP[e]]; apply; exact/ballxx. Qed. Lemma ereal_nbhs_nbhs (p : {ereal R}) (A : set {ereal R}) : ereal_nbhs p A -> ereal_nbhs p (ereal_nbhs^~ A). Proof. move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=. -- move/nbhsP; rewrite nbhs_E => -[_/posnumP[e]] ballA. - apply/nbhsP; rewrite nbhs_E; exists (e%:num / 2) => //= r per. - apply/nbhsP; rewrite nbhs_E; exists (e%:num / 2) => //= x rex. +- move=> /nbhs_ballP[_/posnumP[e]] ballA. + apply/nbhs_ballP; exists (e%:num / 2) => //= r per. + apply/nbhs_ballP; exists (e%:num / 2) => //= x rex. apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym. - exists (M + 1); split; first by rewrite realD // real1. move=> -[x| _ |] //=. rewrite lte_fin => M'x /=. - apply/nbhsP; rewrite nbhs_E; exists 1 => //= y x1y. + apply/nbhs_ballP; exists 1 => //= y x1y. apply MA; rewrite lte_fin. rewrite addrC -ltr_subr_addl in M'x. rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl. @@ -709,7 +744,7 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=. - exists (M - 1); split; first by rewrite realB // real1. move=> -[x| _ |] //=. rewrite lte_fin => M'x /=. - apply/nbhsP; rewrite nbhs_E; exists 1 => //= y x1y. + apply/nbhs_ballP; exists 1 => //= y x1y. apply MA; rewrite lte_fin. rewrite ltr_subr_addl in M'x. rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl. @@ -921,15 +956,16 @@ Lemma nbhsNe (R : realFieldType) (x : {ereal R}) : nbhs (- x)%E = [set [set (- y)%E | y in A] | A in nbhs x]. Proof. case: x => [r /=| |]. -- rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]]. +- rewrite /nbhs /= /ereal_nbhs -nbhs_ballE. + rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]]. exists (-%E @` S). exists e%:num => // x rex; exists (- x%:E)%E; last by rewrite oppeK. - by apply reS; rewrite /= opprK -normrN opprD opprK. + by apply reS; rewrite /ball /= opprK -normrN opprD opprK. rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss]. by rewrite oppeK. by exists (- s)%E; [exists s | rewrite oppeK]. exists e%:num => // x rex; exists (- x%:E)%E; last by rewrite oppeK. - by apply reS'; rewrite /= opprK -normrN opprD. + by apply reS'; rewrite /ball /= opprK -normrN opprD. - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. exists (-%E @` S). exists (- M); rewrite realN Mreal; split => // x Mx. @@ -1309,7 +1345,7 @@ have e'0 : 0 < e'. rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E). rewrite real_of_er_expand // lt_expand ?inE ?contract_le1// ?ltW//. by rewrite ltr_subl_addl ltr_addr. -apply/nbhsP; exists e' => // r' re'r'; apply reA. +apply/nbhs_ballP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. have [rr'|r'r] := lerP r r'. move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']; first by rewrite subrr normr0. @@ -1340,7 +1376,7 @@ have e'0 : 0 < e'. rewrite /e'. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). by rewrite real_of_er_expand // lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW. -apply/nbhsP; exists e' => // r' r'e'r; apply reA. +apply/nbhs_ballP; exists e' => // r' r'e'r; apply reA. rewrite /ball /= in r'e'r. have [rr'|r'r] := lerP r r'. move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']. @@ -1361,7 +1397,7 @@ Lemma nbhs_fin_out_above_below (r : R) (e : {posnum R}) (A : set {ereal R}) : 1 < contract r%:E + (e)%:num -> nbhs r%:E A. Proof. -move=> reA reN1 re1; suff : A = setT by move=> ->; exists 1. +move=> reA reN1 re1; suff : A = setT by move->; apply: filterT. rewrite predeqE => x; split => // _; apply reA. case: x => [r'| |] //. - have [|r'r] := lerP r r'. @@ -1392,7 +1428,7 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1). move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0. rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0]. move: re1; rewrite r0 contract0 add0r => /eqP e1. - exists 1 => // r' /=; rewrite sub0r normrN => r'1. + apply/nbhs_ballP; exists 1 => // r' /=; rewrite /ball /= sub0r normrN => r'1. by apply reA; rewrite r0 contract0 sub0r normrN e1 contract_lt1. rewrite neq_lt => /orP[re1|re1]. by apply (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r. @@ -1411,9 +1447,9 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1). rewrite [contract +oo]/= ltr0_norm ?subr_lt0; last first. by case/ltr_normlP : (contract_lt1 r). by rewrite opprB reN1 opprB addrA ltr_subl_addl ltr_add. - have : nbhs r%:E (setT `\ -oo%E) by exists 1. - case => _/posnumP[e'] /=; rewrite /ball_ => h. - by exists e'%:num => // y /h; apply: Aoo. + have : nbhs r%:E (setT `\ -oo%E) by apply/nbhs_ballP; exists 1. + move=> /nbhs_ballP[_/posnumP[e']] /=; rewrite /ball /= => h. + by apply/nbhs_ballP; exists e'%:num => // y /h; apply: Aoo. move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. have [/eqP re1|re1] := boolP (contract r%:E + e%:num == 1). by apply (@nbhs_fin_out_above _ e) => //; rewrite re1. @@ -1435,7 +1471,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). rewrite real_of_er_expand//. by rewrite lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW. - apply/nbhsP; exists e' => // r' re'r'; apply reA. + apply/nbhs_ballP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. have [|r'r] := lerP r r'. rewrite le_eqVlt => /orP[/eqP->|rr']. @@ -1480,14 +1516,16 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1]. by apply (@nbhs_fin_out_below _ e) => //; rewrite ltW. Qed. -Lemma ereal_nbhsE : nbhs = nbhs_ ereal_ball. +Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ ereal_ball). Proof. +set diag := fun (e : R) => [set xy | ereal_ball xy.1 e xy.2]. rewrite predeq2E => x A; split. - rewrite {1}/nbhs /= /ereal_nbhs. case: x => [/= r [_/posnumP[e] reA]| [M [/= Mreal MA]]| [M [/= Mreal MA]]]. + pose e' : R := minr (contract r%:E - contract (r%:E - e%:num%:E)) (contract (r%:E + e%:num%:E) - contract r%:E). - exists e'. + exists (diag e'); rewrite /diag. + exists e' => //. rewrite /e' lt_minr; apply/andP; split. by rewrite subr_gt0 lt_contract lte_fin ltr_subl_addr ltr_addl. by rewrite subr_gt0 lt_contract lte_fin ltr_addl. @@ -1495,7 +1533,7 @@ rewrite predeq2E => x A; split. * rewrite /ereal_ball in re'r'. have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). apply reA. - rewrite /ball_ real_ltr_norml // ?num_real //. + rewrite /ball /= real_ltr_norml // ?num_real //. rewrite ger0_norm ?subr_ge0// in re'r'. have H1 : contract (r%:E - e%:num%:E) < contract r'%:E. move: re'r'; rewrite /e' lt_minr => /andP[Hr'1 Hr'2]. @@ -1508,7 +1546,7 @@ rewrite predeq2E => x A; split. by rewrite ltr_oppl oppr0. by rewrite subr_ge0 -lee_fin -le_contract. apply reA. - rewrite /ball_ real_ltr_norml // ?num_real //. + rewrite /ball /= real_ltr_norml // ?num_real //. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. by rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin -lt_contract//. @@ -1544,7 +1582,8 @@ rewrite predeq2E => x A; split. exfalso. move: h; apply/negP; rewrite -leNgt -ler_oppl. by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[]. - + exists (1 - contract M%:E). + + exists (diag (1 - contract M%:E)); rewrite /diag. + exists (1 - contract M%:E) => //. by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. case=> [r| |]. * rewrite /ereal_ball [_ +oo%E]/= => rM1. @@ -1562,7 +1601,8 @@ rewrite predeq2E => x A; split. rewrite -leNgt [in X in _ <= X]ger0_norm // ler_subl_addr. rewrite -/(contract M%:E) addrC -ler_subl_addr opprD addrA subrr sub0r. by move: (contract_le1 M%:E); rewrite ler_norml => /andP[]. - + exists (1 + contract M%:E). + + exists (diag (1 + contract M%:E)); rewrite /diag. + exists (1 + contract M%:E) => //. rewrite -ltr_subl_addl sub0r. by move: (contract_lt1 M); rewrite ltr_norml => /andP[]. case=> [r| |]. @@ -1581,19 +1621,26 @@ rewrite predeq2E => x A; split. rewrite subrr add0r -/(contract M%:E). by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm. * rewrite /ereal_ball /= => _; exact: MA. -- case: x => [r [_/posnumP[e] reA]| [_/posnumP[e] reA] | [_/posnumP[e] reA]] //=. - + rewrite /ereal_ball in reA. - by apply nbhs_fin_inbound with e. - + rewrite /ereal_ball [contract +oo]/= in reA. - have [|] := boolP (e%:num <= 1); first exact: nbhs_oo_up_e1. - by rewrite -ltNge; apply: nbhs_oo_up_1e. - + rewrite /ereal_ball [contract -oo]/= in reA. - have [|] := boolP (e%:num <= 1); first exact: nbhs_oo_down_e1. - by rewrite -ltNge; apply: nbhs_oo_down_1e. +- case: x => [r [E [_/posnumP[e] reA] sEA]| [E [_/posnumP[e] reA] sEA]| [E [_/posnumP[e] reA] sEA]] //=. + + by apply nbhs_fin_inbound with e => ??; apply/sEA/reA. + + have [|] := boolP (e%:num <= 1). + by apply: nbhs_oo_up_e1 => ??; apply/sEA/reA. + by rewrite -ltNge; apply: nbhs_oo_up_1e => ??; apply/sEA/reA. + + have [|] := boolP (e%:num <= 1). + by apply: nbhs_oo_down_e1 => ??; apply/sEA/reA. + by rewrite -ltNge; apply: nbhs_oo_down_1e => ??; apply/sEA/reA. Qed. + Definition ereal_pseudoMetricType_mixin := PseudoMetric.Mixin ereal_ball_center ereal_ball_sym ereal_ball_triangle - ereal_nbhsE. + erefl. + +Definition ereal_uniformType_mixin : @Uniform.mixin_of {ereal R} nbhs := + uniformityOfBallMixin ereal_nbhsE ereal_pseudoMetricType_mixin. + +Canonical ereal_uniformType := + UniformType {ereal R} ereal_uniformType_mixin. + Canonical ereal_pseudoMetricType := PseudoMetricType {ereal R} ereal_pseudoMetricType_mixin. End ereal_PseudoMetric. @@ -1648,11 +1695,13 @@ Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass. Definition pointedType := @Pointed.Pack cT xclass. Definition filteredType := @Filtered.Pack cT cT xclass. Definition topologicalType := @Topological.Pack cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. Definition pseudoMetricType := @PseudoMetric.Pack K cT xclass. Definition pseudoMetricNormedZmodType := @PseudoMetricNormedZmodule.Pack K phK cT xclass. Definition pointed_lmodType := @GRing.Lmodule.Pack K phK pointedType xclass. Definition filtered_lmodType := @GRing.Lmodule.Pack K phK filteredType xclass. Definition topological_lmodType := @GRing.Lmodule.Pack K phK topologicalType xclass. +Definition uniform_lmodType := @GRing.Lmodule.Pack K phK uniformType xclass. Definition pseudoMetric_lmodType := @GRing.Lmodule.Pack K phK pseudoMetricType xclass. Definition normedZmod_lmodType := @GRing.Lmodule.Pack K phK normedZmodType xclass. Definition pseudoMetricNormedZmod_lmodType := @GRing.Lmodule.Pack K phK pseudoMetricNormedZmodType xclass. @@ -1680,6 +1729,8 @@ Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. Coercion pseudoMetricType : type >-> PseudoMetric.type. Canonical pseudoMetricType. Coercion pseudoMetricNormedZmodType : type >-> PseudoMetricNormedZmodule.type. @@ -1687,6 +1738,7 @@ Canonical pseudoMetricNormedZmodType. Canonical pointed_lmodType. Canonical filtered_lmodType. Canonical topological_lmodType. +Canonical uniform_lmodType. Canonical pseudoMetric_lmodType. Canonical normedZmod_lmodType. Canonical pseudoMetricNormedZmod_lmodType. @@ -1720,31 +1772,29 @@ Proof. by case: V x => V0 [a b [c]] //= v; rewrite c. Qed. Local Notation ball_norm := (ball_ (@normr R V)). -Local Notation nbhs_norm := (nbhs_ ball_norm). +Local Notation nbhs_norm := (@nbhs_ball _ V). Lemma nbhs_le_nbhs_norm (x : V) : nbhs x `=>` nbhs_norm x. Proof. -move=> P [_ /posnumP[e] subP]; apply/nbhsP. -by eexists; last (move=> y Py; apply/subP; rewrite ball_normE; apply/Py). +move=> P [_ /posnumP[e] subP]; apply/nbhs_ballP. +by eexists; last (move=> y Py; apply/subP; apply/Py). Qed. Lemma nbhs_norm_le_nbhs x : nbhs_norm x `=>` nbhs x. Proof. -move=> P /nbhsP [_ /posnumP[e] Pxe]. -by exists e%:num => // y; rewrite ball_normE; apply/Pxe. +move=> P /nbhs_ballP [_ /posnumP[e] Pxe]. +by exists e%:num => // y; apply/Pxe. Qed. Lemma nbhs_nbhs_norm : nbhs_norm = nbhs. -Proof. -by rewrite funeqE => x; rewrite /nbhs_norm ball_normE filter_from_ballE. -Qed. +Proof. by rewrite funeqE => x; rewrite -filter_from_ballE. Qed. Lemma nbhs_normP x P : nbhs x P <-> nbhs_norm x P. Proof. by rewrite nbhs_nbhs_norm. Qed. Lemma filter_from_norm_nbhs x : @filter_from R _ [set x : R | 0 < x] (ball_norm x) = nbhs x. -Proof. by rewrite -nbhs_nbhs_norm. Qed. +Proof. by rewrite -nbhs_nbhs_norm ball_normE. Qed. Lemma nbhs_normE (x : V) (P : set V) : nbhs_norm x P = \near x, P x. @@ -1760,7 +1810,7 @@ Proof. exact: nbhs_normE. Qed. Lemma nbhs_norm_ball_norm x (e : {posnum R}) : nbhs_norm x (ball_norm x e%:num). -Proof. by exists e%:num. Qed. +Proof. by rewrite ball_normE; exists e%:num. Qed. Lemma nbhs_ball_norm (x : V) (eps : {posnum R}) : nbhs x (ball_norm x eps%:num). Proof. rewrite -nbhs_nbhs_norm; apply: nbhs_norm_ball_norm. Qed. @@ -1786,7 +1836,7 @@ Lemma cvg_dist {F : set (set V)} {FF : Filter F} (y : V) : Proof. by move=> /cvg_distP. Qed. Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num). -Proof. rewrite nbhs_nbhs_norm; by apply: nbhs_ball. Qed. +Proof. rewrite nbhs_nbhs_norm; by apply: nbhsx_ballx. Qed. End NormedModule_numDomainType. Hint Resolve normr_ge0 : core. @@ -1982,7 +2032,7 @@ Implicit Types (x y z : V). Local Notation ball_norm := (ball_ (@normr R V)). -Local Notation nbhs_norm := (nbhs_ ball_norm). +Local Notation nbhs_norm := (@nbhs_ball _ V). Lemma norm_hausdorff : hausdorff V. Proof. @@ -2085,7 +2135,7 @@ Proof. move=> x y clxy; apply/eqP; rewrite eq_le. apply/(@in_segment_addgt0Pr _ x _ x) => _ /posnumP[e]. rewrite inE -ler_distl; set he := (e%:num / 2)%:pos. -have [z []] := clxy _ _ (nbhs_ball x he) (nbhs_ball y he). +have [z []] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he). move=> zx_he yz_he. rewrite -(subrKA z) (le_trans (ler_norm_add _ _) _)// ltW //. by rewrite (splitr e%:num) (distrC z); apply: ltr_add. @@ -2105,10 +2155,10 @@ Lemma continuous_cvg_dist {R : numFieldType} Proof. move=> cf xl e. move/cvg_dist: (cf l) => /(_ _ (posnum_gt0 e)). -rewrite nearE /= => /nbhsP; rewrite nbhs_E => -[i i0]; apply. +rewrite nearE /= => /nbhs_ballP [i i0]; apply. have /@cvg_dist : Filter [filter of x] by apply: filter_on_Filter. move/(_ _ xl _ i0). -rewrite nearE /= => /nbhsP; rewrite nbhs_E => -[j j0]. +rewrite nearE /= => /nbhs_ballP [j j0]. by move/(_ _ (ballxx _ j0)); rewrite -ball_normE. Qed. @@ -2807,7 +2857,7 @@ Lemma norm_continuous : continuous ((@normr _ V) : V -> K^o). Proof. move=> x; apply/(@cvg_distP _ [normedModType K of K^o]) => _/posnumP[e] /=. rewrite !near_simpl; apply/nbhs_normP; exists e%:num => // y Hy. -exact/(le_lt_trans (ler_dist_dist _ _)). +by rewrite -ball_normE in Hy; apply/(le_lt_trans (ler_dist_dist _ _)). Qed. End NVS_continuity_normedModType. @@ -3071,9 +3121,9 @@ Record class_of (T : Type) := Class { mixin : Complete.axiom (PseudoMetric.Pack base) }. Local Coercion base : class_of >-> NormedModule.class_of. -Definition base2 T (cT : class_of T) : Complete.class_of K T := - @Complete.Class _ _ (@base T cT) (@mixin T cT). -Local Coercion base2 : class_of >-> Complete.class_of. +Definition base2 T (cT : class_of T) : CompletePseudoMetric.class_of K T := + @CompletePseudoMetric.Class _ _ (@base T cT) (@mixin T cT). +Local Coercion base2 : class_of >-> CompletePseudoMetric.class_of. Structure type (phK : phant K) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. @@ -3084,7 +3134,7 @@ Definition class := let: Pack _ c := cT return class_of cT in c. Definition pack := fun bT (b : NormedModule.class_of K T) & phant_id (@NormedModule.class K phK bT) b => - fun mT m & phant_id (@Complete.class K mT) (@Complete.Class K T b m) => + fun mT m & phant_id (@Complete.class mT) (@Complete.Class T b m) => Pack phK (@Class T b m). Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). @@ -3097,23 +3147,41 @@ Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass. Definition pointedType := @Pointed.Pack cT xclass. Definition filteredType := @Filtered.Pack cT cT xclass. Definition topologicalType := @Topological.Pack cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. Definition pseudoMetricType := @PseudoMetric.Pack K cT xclass. Definition pseudoMetricNormedZmodType := @PseudoMetricNormedZmodule.Pack K phK cT xclass. Definition normedModType := @NormedModule.Pack K phK cT xclass. -Definition completeType := @Complete.Pack K cT xclass. +Definition completeType := @Complete.Pack cT xclass. +Definition completePseudoMetricType := @CompletePseudoMetric.Pack K cT xclass. Definition complete_zmodType := @GRing.Zmodule.Pack completeType xclass. Definition complete_lmodType := @GRing.Lmodule.Pack K phK completeType xclass. Definition complete_normedZmodType := @Num.NormedZmodule.Pack K phK completeType xclass. Definition complete_pseudoMetricNormedZmodType := @PseudoMetricNormedZmodule.Pack K phK completeType xclass. Definition complete_normedModType := @NormedModule.Pack K phK completeType xclass. +Definition completePseudoMetric_lmodType : GRing.Lmodule.type phK := + @GRing.Lmodule.Pack K phK (CompletePseudoMetric.sort completePseudoMetricType) + xclass. +Definition completePseudoMetric_zmodType : GRing.Zmodule.type := + @GRing.Zmodule.Pack (CompletePseudoMetric.sort completePseudoMetricType) + xclass. +Definition completePseudoMetric_normedModType : NormedModule.type phK := + @NormedModule.Pack K phK (CompletePseudoMetric.sort completePseudoMetricType) + xclass. +Definition completePseudoMetric_normedZmodType : Num.NormedZmodule.type phK := + @Num.NormedZmodule.Pack K phK + (CompletePseudoMetric.sort completePseudoMetricType) xclass. +Definition completePseudoMetric_pseudoMetricNormedZmodType : + PseudoMetricNormedZmodule.type phK := + @PseudoMetricNormedZmodule.Pack K phK + (CompletePseudoMetric.sort completePseudoMetricType) xclass. End ClassDef. Module Exports. Coercion base : class_of >-> NormedModule.class_of. -Coercion base2 : class_of >-> Complete.class_of. +Coercion base2 : class_of >-> CompletePseudoMetric.class_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Canonical eqType. @@ -3133,17 +3201,26 @@ Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. Coercion pseudoMetricType : type >-> PseudoMetric.type. Canonical pseudoMetricType. Coercion normedModType : type >-> NormedModule.type. Canonical normedModType. Coercion completeType : type >-> Complete.type. Canonical completeType. +Coercion completePseudoMetricType : type >-> CompletePseudoMetric.type. +Canonical completePseudoMetricType. Canonical complete_zmodType. Canonical complete_lmodType. Canonical complete_normedZmodType. Canonical complete_pseudoMetricNormedZmodType. Canonical complete_normedModType. +Canonical completePseudoMetric_lmodType. +Canonical completePseudoMetric_zmodType. +Canonical completePseudoMetric_normedModType. +Canonical completePseudoMetric_normedZmodType. +Canonical completePseudoMetric_pseudoMetricNormedZmodType. Notation completeNormedModType K := (type (Phant K)). Notation "[ 'completeNormedModType' K 'of' T ]" := (@pack _ (Phant K) T _ _ idfun _ _ idfun) (at level 0, format "[ 'completeNormedModType' K 'of' T ]") : form_scope. @@ -3221,9 +3298,9 @@ Arguments cvg_distW {_ _ F FF}. Lemma R_complete (R : realType) (F : set (set R^o)) : ProperFilter F -> cauchy F -> cvg F. Proof. -move=> FF F_cauchy; apply/cvg_ex. +move=> FF /cauchy_ballP F_cauchy; apply/cvg_ex. pose D := \bigcap_(A in F) (down A). -have /cauchyP /(_ 1) [//|x0 x01] := F_cauchy. +have /cauchy_ballP /cauchyP /(_ 1) [//|x0 x01] := F_cauchy. have D_has_sup : has_sup D; first split. - exists (x0 - 1) => A FA. near F => x. @@ -3264,7 +3341,7 @@ Definition at_right (x : R^o) := within (fun u : R => x < u) (nbhs x). Global Instance at_right_proper_filter (x : R^o) : ProperFilter (at_right x). Proof. -apply: Build_ProperFilter' => -[_ /posnumP[d] /(_ (x + d%:num / 2))]. +apply: Build_ProperFilter' => -[_/posnumP[d] /(_ (x + d%:num / 2))]. apply; last (by rewrite ltr_addl); rewrite /=. rewrite opprD !addrA subrr add0r normrN normf_div !ger0_norm //. by rewrite ltr_pdivr_mulr // ltr_pmulr // (_ : 1 = 1%:R) // ltr_nat. @@ -3503,7 +3580,7 @@ move=> x clAx; have abx : x \in `[a, b]. by apply: segment_closed; have /closureI [] := clAx. split=> //; have /sabUf [i Di fx] := abx. have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi]. -have /clAx [y [[aby [D' sD [sayUf _]]] xe_y]] := nbhs_ball x e. +have /clAx [y [[aby [D' sD [sayUf _]]] xe_y]] := nbhsx_ballx x e. exists (i |` D')%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE. split=> [z axz|]; last first. exists i; first by rewrite !inE eq_refl. @@ -3556,7 +3633,7 @@ have supAab : sup A \in `[a, b]. exists (sup A) => //; have lefsupv : f (sup A) <= v. rewrite leNgt; apply/negP => ltvfsup. have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0. - have /fcont /(_ _ (@nbhs_ball _ [normedModType R of R^o] _ (PosNum vltfsup))) [_/posnumP[d] supdfe] + have /fcont /(_ _ (@nbhsx_ballx _ [normedModType R of R^o] _ (PosNum vltfsup))) [_/posnumP[d] supdfe] := supAab. have [t At supd_t] := sup_adherent supA [gt0 of d%:num]. suff /supdfe : @ball _ [normedModType R of R^o] (sup A) d%:num t. @@ -3568,7 +3645,7 @@ exists (sup A) => //; have lefsupv : f (sup A) <= v. apply/eqP; rewrite eq_le; apply/andP; split=> //. rewrite -subr_le0; apply/ler0_addgt0P => _/posnumP[e]. rewrite ler_subl_addr -ler_subl_addl ltW //. -have /fcont /(_ _ (@nbhs_ball _ [normedModType R of R^o] _ e)) [_/posnumP[d] supdfe] := supAab. +have /fcont /(_ _ (@nbhsx_ballx _ [normedModType R of R^o] _ e)) [_/posnumP[d] supdfe] := supAab. have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x. have /supdfe /= : @ball _ [normedModType R of R^o] (sup A) d%:num x. by near: x; rewrite /= nbhs_simpl; exists d%:num => //. @@ -3778,7 +3855,7 @@ have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R]. by rewrite rmorphD /= -floorE floorS_gtr. have /Aco [] := covA. move=> n _; rewrite openE => p; rewrite -subr_gt0 => ltpn. - apply/nbhsP; exists (n%:~R - `|p|) => // q. + apply/nbhs_ballP; exists (n%:~R - `|p|) => // q. rewrite -ball_normE /= ltr_subr_addr distrC; apply: le_lt_trans. by rewrite -{1}(subrK p q) ler_norm_add. move=> D _ DcovA. diff --git a/theories/sequences.v b/theories/sequences.v index c26889bf68..8729c5d987 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -744,7 +744,7 @@ Lemma cauchy_seriesP {R : numFieldType} (V : normedModType R) (u_ : V ^nat) : forall e : R, e > 0 -> \forall n \near (\oo, \oo), `|\sum_(n.1 <= k < n.2) u_ k| < e. Proof. -split=> su_cv _/posnumP[e]; have {}su_cv := su_cv _ e; +rewrite -cauchy_ballP; split=> su_cv _/posnumP[e]; have {}su_cv := su_cv _ e; rewrite -near2_pair -ball_normE !near_simpl/= in su_cv *. apply: filterS su_cv => -[/= m n]; rewrite distrC sub_series. by have [|/ltnW]:= leqP m n => mn//; rewrite (big_geq mn) ?normr0. diff --git a/theories/topology.v b/theories/topology.v index 2ab800eada..5461f1cbff 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -202,49 +202,81 @@ Require Import boolp Rstruct classical_sets posnum. (* --> We used these topological notions to prove Tychonoff's Theorem, which *) (* states that any product of compact sets is compact according to the *) (* product topology. *) +(* * Uniform spaces : *) +(* nbhs_ ent == neighbourhoods defined using entourages *) +(* uniformType == interface type for uniform spaces: a *) +(* type equipped with entourages *) +(* UniformMixin efilter erefl einv esplit nbhse == builds the mixin for a *) +(* uniform space from the properties of *) +(* entourages and the compatibility between *) +(* entourages and nbhs *) +(* UniformType T m == packs the uniform space mixin into a *) +(* uniformType. T must have a canonical *) +(* topologicalType structure *) +(* [uniformType of T for cT] == T-clone of the uniformType structure cT *) +(* [uniformType of T] == clone of a canonical uniformType *) +(* structure on T *) +(* topologyOfEntourageMixin umixin == builds the mixin for a topological *) +(* space from a mixin for a uniform space *) +(* entourage == set of entourages in a uniform space *) +(* split_ent E == when E is an entourage, split_ent E is *) +(* an entourage E' such that E' \o E' is *) +(* included in E when seen as a relation *) +(* unif_continuous f <-> f is uniformly continuous. *) (* *) (* * PseudoMetric spaces : *) -(* nbhs_ ball == neighbourhoods defined using balls *) +(* entourage_ ball == entourages defined using balls *) (* pseudoMetricType == interface type for pseudo metric space *) (* structure: a type equipped with balls. *) (* PseudoMetricMixin brefl bsym btriangle nbhsb == builds the mixin for a *) (* pseudo metric space from the properties *) (* of balls and the compatibility between *) -(* balls and nbhs. *) +(* balls and entourages. *) (* PseudoMetricType T m == packs the pseudo metric space mixin into *) (* a pseudoMetricType. T must have a *) -(* canonical topologicalType structure. *) +(* canonical uniformType structure. *) (* [pseudoMetricType R of T for cT] == T-clone of the pseudoMetricType *) (* structure cT, with R the ball radius. *) (* [pseudoMetricType R of T] == clone of a canonical pseudoMetricType *) (* structure on T, with R the ball radius. *) -(* topologyOfBallMixin umixin == builds the mixin for a topological space *) +(* uniformityOfBallMixin umixin == builds the mixin for a topological space *) (* from a mixin for a pseudoMetric space. *) (* ball x e == ball of center x and radius e. *) +(* nbhs_ball_ ball == nbhs defined using the given balls *) +(* nbhs_ball == nbhs defined using balls in a *) +(* pseudometric space *) (* close x y <-> x and y are arbitrarily close w.r.t. to *) (* balls. *) -(* entourages == set of entourages defined by balls. An *) -(* entourage can be seen as a *) -(* "neighbourhood" of the diagonal set *) -(* D = {(x, x) | x in T}. *) -(* ball_set A e == set A extended with a band of width e *) -(* unif_continuous f <-> f is uniformly continuous. *) (* *) -(* * Complete spaces : *) -(* cauchy_ex F <-> the set of sets F is a cauchy filter *) -(* (epsilon-delta definition). *) +(* * Complete uniform spaces : *) (* cauchy F <-> the set of sets F is a cauchy filter *) -(* (using the near notations). *) -(* completeType == interface type for a complete *) -(* pseudoMetric space structure. *) +(* (entourage definition) *) +(* completeType == interface type for a complete uniform *) +(* space structure. *) (* CompleteType T cvgCauchy == packs the proof that every proper cauchy *) (* filter on T converges into a *) (* completeType structure; T must have a *) -(* canonical pseudoMetricType structure. *) +(* canonical uniformType structure. *) (* [completeType of T for cT] == T-clone of the completeType structure *) (* cT. *) (* [completeType of T] == clone of a canonical completeType *) (* structure on T. *) +(* * Complete pseudometric spaces : *) +(* cauchy_ex F <-> the set of sets F is a cauchy filter *) +(* (epsilon-delta definition). *) +(* cauchy F <-> the set of sets F is a cauchy filter *) +(* (using the near notations). *) +(* completePseudoMetricType == interface type for a complete *) +(* pseudometric space structure. *) +(* CompletePseudoMetricType T cvgCauchy == packs the proof that every proper *) +(* cauchy filter on T converges into a *) +(* completePseudoMetricType structure; T *) +(* must have a canonical pseudoMetricType *) +(* structure. *) +(* [completePseudoMetricType of T for cT] == T-clone of the *) +(* completePseudoMetricType structure cT. *) +(* [completePseudoMetricType of T] == clone of a canonical *) +(* completePseudoMetricType structure on T. *) (******************************************************************************) Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). @@ -2627,28 +2659,480 @@ Definition connected (T : topologicalType) (A : set T) := forall B : set T, B !=set0 -> (exists2 C, open C & B = A `&` C) -> (exists2 C, closed C & B = A `&` C) -> B = A. +(** * Uniform spaces *) + +Local Notation "B \o A" := + ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope. + +Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. + +Local Notation "'to_set' A x" := ([set y | A (x, y)]) + (at level 0, A at level 0) : classical_set_scope. + +Definition nbhs_ {T T'} (ent : set (set (T * T'))) (x : T) := + filter_from ent (fun A => to_set A x). + +Lemma nbhs_E {T T'} (ent : set (set (T * T'))) x : + nbhs_ ent x = filter_from ent (fun A => to_set A x). +Proof. by []. Qed. + +Module Uniform. + +Record mixin_of (M : Type) (nbhs : M -> set (set M)) := Mixin { + entourage : (M * M -> Prop) -> Prop ; + ax1 : Filter entourage ; + ax2 : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A ; + ax3 : forall A, entourage A -> entourage (A^-1)%classic ; + ax4 : forall A, entourage A -> exists2 B, entourage B & B \o B `<=` A ; + ax5 : nbhs = nbhs_ entourage +}. + +Record class_of (M : Type) := Class { + base : Topological.class_of M; + mixin : mixin_of (Filtered.nbhs_op base) +}. + +Section ClassDef. + +Structure type := Pack { sort; _ : class_of sort }. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). +Definition class := let: Pack _ c := cT return class_of cT in c. + +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. +Notation xclass := (class : class_of xT). +Local Coercion base : class_of >-> Topological.class_of. +Local Coercion mixin : class_of >-> mixin_of. + +Definition pack nbhs (m : @mixin_of T nbhs) := + fun bT (b : Topological.class_of T) of phant_id (@Topological.class bT) b => + fun m' of phant_id m (m' : @mixin_of T (Filtered.nbhs_op b)) => + @Pack T (@Class _ b m'). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition pointedType := @Pointed.Pack cT xclass. +Definition filteredType := @Filtered.Pack cT cT xclass. +Definition topologicalType := @Topological.Pack cT xclass. + +End ClassDef. + +Module Exports. + +Coercion sort : type >-> Sortclass. +Coercion base : class_of >-> Topological.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion pointedType : type >-> Pointed.type. +Canonical pointedType. +Coercion filteredType : type >-> Filtered.type. +Canonical filteredType. +Coercion topologicalType : type >-> Topological.type. +Canonical topologicalType. +Notation uniformType := type. +Notation UniformType T m := (@pack T _ m _ _ idfun _ idfun). +Notation UniformMixin := Mixin. +Notation "[ 'uniformType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) + (at level 0, format "[ 'uniformType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'uniformType' 'of' T ]" := (@clone T _ _ id) + (at level 0, format "[ 'uniformType' 'of' T ]") : form_scope. + +End Exports. + +End Uniform. + +Export Uniform.Exports. + +Section UniformTopology. + +Program Definition topologyOfEntourageMixin (T : Type) + (nbhs : T -> set (set T)) (m : Uniform.mixin_of nbhs) : + Topological.mixin_of nbhs := topologyOfFilterMixin _ _ _. +Next Obligation. +rewrite (Uniform.ax5 m) nbhs_E; apply filter_from_proper; last first. + by move=> A entA; exists p; apply: Uniform.ax2 entA _ _. +apply: filter_from_filter. + by exists setT; apply: @filterT (Uniform.ax1 m). +move=> A B entA entB; exists (A `&` B) => //. +exact: (@filterI _ _ (Uniform.ax1 m)). +Qed. +Next Obligation. +move: H; rewrite (Uniform.ax5 m) nbhs_E => - [B entB sBpA]. +by apply: sBpA; apply: Uniform.ax2 entB _ _. +Qed. +Next Obligation. +move: H; rewrite (Uniform.ax5 m) nbhs_E => - [B entB sBpA]. +have /Uniform.ax4 [C entC sC2B] := entB. +exists C => // q Cpq; rewrite nbhs_E; exists C => // r Cqr. +by apply/sBpA/sC2B; exists q. +Qed. + +End UniformTopology. + +Definition entourage {M : uniformType} := Uniform.entourage (Uniform.class M). + +Lemma nbhs_entourageE {M : uniformType} : nbhs_ (@entourage M) = nbhs. +Proof. by case: M=> [?[?[]]]. Qed. + +Lemma filter_from_entourageE {M : uniformType} x : + filter_from (@entourage M) (fun A => to_set A x) = nbhs x. +Proof. by rewrite -nbhs_entourageE. Qed. + +Module Export NbhsEntourage. +Definition nbhs_simpl := + (nbhs_simpl,@filter_from_entourageE,@nbhs_entourageE). +End NbhsEntourage. + +Lemma nbhsP {M : uniformType} (x : M) P : + nbhs x P <-> nbhs_ entourage x P. +Proof. by rewrite nbhs_simpl. Qed. + +Section uniformType1. +Context {M : uniformType}. + +Lemma entourage_refl (A : set (M * M)) x : + entourage A -> A (x, x). +Proof. by move=> entA; apply: Uniform.ax2 entA _ _. Qed. + +Global Instance entourage_filter : ProperFilter (@entourage M). +Proof. +apply Build_ProperFilter; last exact: Uniform.ax1. +by move=> A entA; exists (point, point); apply: entourage_refl. +Qed. + +Lemma entourageT : entourage (@setT (M * M)). +Proof. exact: filterT. Qed. + +Lemma entourage_inv (A : set (M * M)) : entourage A -> entourage (A^-1)%classic. +Proof. exact: Uniform.ax3. Qed. + +Lemma entourage_split_ex (A : set (M * M)) : + entourage A -> exists2 B, entourage B & B \o B `<=` A. +Proof. exact: Uniform.ax4. Qed. + +Definition split_ent (A : set (M * M)) := + get (entourage `&` [set B | B \o B `<=` A]). + +Lemma split_entP (A : set (M * M)) : entourage A -> + entourage (split_ent A) /\ split_ent A \o split_ent A `<=` A. +Proof. by move/entourage_split_ex/exists2P/getPex. Qed. + +Lemma entourage_split_ent (A : set (M * M)) : entourage A -> + entourage (split_ent A). +Proof. by move=> /split_entP []. Qed. + +Lemma subset_split_ent (A : set (M * M)) : entourage A -> + split_ent A \o split_ent A `<=` A. +Proof. by move=> /split_entP []. Qed. + +Lemma entourage_split (z x y : M) A : entourage A -> + split_ent A (x,z) -> split_ent A (z,y) -> A (x,y). +Proof. by move=> /subset_split_ent sA ??; apply: sA; exists z. Qed. + +Lemma nbhs_entourage (x : M) A : entourage A -> nbhs x (to_set A x). +Proof. by move=> ?; apply/nbhsP; exists A. Qed. + +Lemma cvg_entourageP F (FF : Filter F) (p : M) : + F --> p <-> forall A, entourage A -> \forall q \near F, A (p, q). +Proof. by rewrite -filter_fromP !nbhs_simpl. Qed. + +Lemma cvg_entourage {F} {FF : Filter F} (y : M) : + F --> y -> forall A, entourage A -> \forall y' \near F, A (y,y'). +Proof. by move/cvg_entourageP. Qed. + +Lemma cvg_app_entourageP T (f : T -> M) F (FF : Filter F) p : + f @ F --> p <-> forall A, entourage A -> \forall t \near F, A (p, f t). +Proof. exact: cvg_entourageP. Qed. + +End uniformType1. + +Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core. +Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core. +Arguments entourage_split {M} z {x y A}. +Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core. + +Definition unif_continuous (U V : uniformType) (f : U -> V) := + (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage. + +(** product of two uniform spaces *) + +Section prod_Uniform. + +Context {U V : uniformType}. +Implicit Types A : set ((U * V) * (U * V)). + +Definition prod_ent := + [set A : set ((U * V) * (U * V)) | + filter_prod (@entourage U) (@entourage V) + [set ((xy.1.1,xy.2.1),(xy.1.2,xy.2.2)) | xy in A]]. + +Lemma prod_entP (A : set (U * U)) (B : set (V * V)) : + entourage A -> entourage B -> + prod_ent [set xy | A (xy.1.1, xy.2.1) /\ B (xy.1.2, xy.2.2)]. +Proof. +move=> entA entB; exists (A,B) => // xy ABxy. +by exists ((xy.1.1, xy.2.1),(xy.1.2,xy.2.2)); rewrite -!surjective_pairing. +Qed. + +Lemma prod_ent_filter : Filter prod_ent. +Proof. +have prodF := filter_prod_filter (@entourage_filter U) (@entourage_filter V). +split; rewrite /prod_ent; last 1 first. +- by move=> A B sAB; apply: filterS => ? [xy /sAB ??]; exists xy. +- rewrite -setMT; apply: prod_entP filterT filterT. +move=> A B entA entB; apply: filterS (filterI entA entB) => xy []. +move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //. +move/eqP: ztexy; rewrite -zt'exy !xpair_eqE. +by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP->. +Qed. + +Lemma prod_ent_refl A : prod_ent A -> [set xy | xy.1 = xy.2] `<=` A. +Proof. +move=> [B [entB1 entB2] sBA] xy /eqP. +rewrite [_.1]surjective_pairing [xy.2]surjective_pairing xpair_eqE. +move=> /andP [/eqP xy1e /eqP xy2e]. +have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1), (xy.1.2, xy.2.2)). + by rewrite xy1e xy2e; split=> /=; apply: entourage_refl. +move=> [zt Azt /eqP]; rewrite !xpair_eqE. +by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP<-. +Qed. + +Lemma prod_ent_inv A : prod_ent A -> prod_ent (A^-1)%classic. +Proof. +move=> [B [/entourage_inv entB1 /entourage_inv entB2] sBA]. +have:= prod_entP entB1 entB2; rewrite /prod_ent; apply: filterS. +move=> _ [p /(sBA (_,_)) [[x y] ? xyE] <-]; exists (y,x) => //=; move/eqP: xyE. +by rewrite !xpair_eqE => /andP[/andP[/eqP-> /eqP->] /andP[/eqP-> /eqP->]]. +Qed. + +Lemma prod_ent_split A : prod_ent A -> exists2 B, prod_ent B & B \o B `<=` A. +Proof. +move=> [B [entB1 entB2]] sBA; exists [set xy | split_ent B.1 (xy.1.1,xy.2.1) /\ + split_ent B.2 (xy.1.2,xy.2.2)]. + by apply: prod_entP; apply: entourage_split_ent. +move=> xy [uv /= [hB1xyuv1 hB2xyuv1] [hB1xyuv2 hB2xyuv2]]. +have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1),(xy.1.2,xy.2.2)). + by split=> /=; apply: subset_split_ent => //; [exists uv.1|exists uv.2]. +move=> [zt Azt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE. +by rewrite -!surjective_pairing => /eqP<-. +Qed. + +Lemma prod_ent_nbhsE : nbhs = nbhs_ prod_ent. +Proof. +rewrite predeq2E => xy A; split=> [[B []] | [B [C [entC1 entC2] sCB] sBA]]. + rewrite -!nbhs_entourageE => - [C1 entC1 sCB1] [C2 entC2 sCB2] sBA. + exists [set xy | C1 (xy.1.1, xy.2.1) /\ C2 (xy.1.2, xy.2.2)]. + exact: prod_entP. + by move=> uv [/= /sCB1 Buv1 /sCB2 /(conj Buv1) /sBA]. +exists (to_set (C.1) (xy.1), to_set (C.2) (xy.2)). + by rewrite -!nbhs_entourageE; split; [exists C.1|exists C.2]. +move=> uv [/= Cxyuv1 Cxyuv2]; apply: sBA. +have /sCB : (C.1 `*` C.2) ((xy.1,uv.1),(xy.2,uv.2)) by []. +move=> [zt Bzt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE. +by rewrite -!surjective_pairing => /eqP<-. +Qed. + +Definition prod_uniformType_mixin := + Uniform.Mixin prod_ent_filter prod_ent_refl prod_ent_inv prod_ent_split + prod_ent_nbhsE. + +End prod_Uniform. + +Canonical prod_uniformType (U V : uniformType) := + UniformType (U * V) (@prod_uniformType_mixin U V). + +(** matrices *) + +Section matrix_Uniform. + +Variables (m n : nat) (T : uniformType). + +Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)). + +Definition mx_ent := + filter_from + [set P : 'I_m -> 'I_n -> set (T * T) | forall i j, entourage (P i j)] + (fun P => [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | + forall i j, P i j (MN.1 i j, MN.2 i j)]). + +Lemma mx_ent_filter : Filter mx_ent. +Proof. +apply: filter_from_filter => [|A B entA entB]. + by exists (fun _ _ => setT) => _ _; apply: filterT. +exists (fun i j => A i j `&` B i j); first by move=> ??; apply: filterI. +by move=> MN ABMN; split=> i j; have [] := ABMN i j. +Qed. + +Lemma mx_ent_refl A : mx_ent A -> [set MN | MN.1 = MN.2] `<=` A. +Proof. +move=> [B entB sBA] MN MN1e2; apply: sBA => i j. +by rewrite MN1e2; apply: entourage_refl. +Qed. + +Lemma mx_ent_inv A : mx_ent A -> mx_ent (A^-1)%classic. +Proof. +move=> [B entB sBA]; exists (fun i j => ((B i j)^-1)%classic). + by move=> i j; apply: entourage_inv. +by move=> MN BMN; apply: sBA. +Qed. + +Lemma mx_ent_split A : mx_ent A -> exists2 B, mx_ent B & B \o B `<=` A. +Proof. +move=> [B entB sBA]. +have Bsplit : forall i j, exists C, entourage C /\ C \o C `<=` B i j. + by move=> ??; apply/exists2P/entourage_split_ex. +exists [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | + forall i j, get [set C | entourage C /\ C \o C `<=` B i j] + (MN.1 i j, MN.2 i j)]. + by exists (fun i j => get [set C | entourage C /\ C \o C `<=` B i j]). +move=> MN [P CMN1P CPMN2]; apply/sBA => i j. +have /getPex [_] := Bsplit i j; apply; exists (P i j); first exact: CMN1P. +exact: CPMN2. +Qed. + +Lemma mx_ent_nbhsE : nbhs = nbhs_ mx_ent. +Proof. +rewrite predeq2E => M A; split. + move=> [B]; rewrite -nbhs_entourageE => M_B sBA. + set sB := fun i j => [set C | entourage C /\ to_set C (M i j) `<=` B i j]. + have {M_B} M_B : forall i j, sB i j !=set0 by move=> ??; apply/exists2P/M_B. + exists [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | forall i j, + get (sB i j) (MN.1 i j, MN.2 i j)]. + by exists (fun i j => get (sB i j)) => // i j; have /getPex [] := M_B i j. + move=> N CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply. + exact/CMN. +move=> [B [C entC sCB] sBA]; exists (fun i j => to_set (C i j) (M i j)). + by rewrite -nbhs_entourageE => i j; exists (C i j). +by move=> N CMN; apply/sBA/sCB. +Qed. + +Definition matrix_uniformType_mixin := + Uniform.Mixin mx_ent_filter mx_ent_refl mx_ent_inv mx_ent_split + mx_ent_nbhsE. + +Canonical matrix_uniformType := + UniformType 'M[T]_(m, n) matrix_uniformType_mixin. + +End matrix_Uniform. + +Lemma cvg_mx_entourageP (T : uniformType) m n (F : set (set 'M[T]_(m,n))) + (FF : Filter F) (M : 'M[T]_(m,n)) : + F --> M <-> + forall A, entourage A -> \forall N \near F, + forall i j, A (M i j, (N : 'M[T]_(m,n)) i j). +Proof. +split. + by rewrite filter_fromP => FM A ?; apply: (FM (fun i j => to_set A (M i j))). +move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N. +apply: sPA => /=; near: N; set Q := \bigcap_ij P ij.1 ij.2. +apply: filterS (FM Q _); first by move=> N QN i j; apply: (QN _ _ (i, j)). +have -> : Q = + \bigcap_(ij in [set k | k \in [fset x in predT]%fset]) P ij.1 ij.2. + by rewrite predeqE => t; split=> Qt ij _; apply: Qt => //; rewrite !inE. +by apply: filter_bigI => ??; apply: entP. +Grab Existential Variables. all: end_near. Qed. + +(** Functional metric spaces *) + +Section fct_Uniform. + +Variable (T : choiceType) (U : uniformType). + +Definition fct_ent := + filter_from + (@entourage U) + (fun P => [set fg | forall t : T, P (fg.1 t, fg.2 t)]). + +Lemma fct_ent_filter : Filter fct_ent. +Proof. +apply: filter_from_filter; first by exists setT; apply: filterT. +move=> A B entA entB. +exists (A `&` B); first exact: filterI. +by move=> fg ABfg; split=> t; have [] := ABfg t. +Qed. + +Lemma fct_ent_refl A : fct_ent A -> [set fg | fg.1 =fg.2] `<=` A. +Proof. +move=> [B entB sBA] fg feg; apply/sBA => t; rewrite feg. +exact: entourage_refl. +Qed. + +Lemma fct_ent_inv A : fct_ent A -> fct_ent (A^-1)%classic. +Proof. +move=> [B entB sBA]; exists (B^-1)%classic; first exact: entourage_inv. +by move=> fg Bgf; apply/sBA. +Qed. + +Lemma fct_ent_split A : fct_ent A -> exists2 B, fct_ent B & B \o B `<=` A. +Proof. +move=> [B entB sBA]. +(* have Bsplit : exists C, entourage C /\ C \o C `<=` B. *) +(* exact/exists2P/entourage_split_ex. *) +exists [set fg | forall t, split_ent B (fg.1 t, fg.2 t)]. + by exists (split_ent B). +move=> fg [h spBfh spBhg]. +by apply: sBA => t; apply: entourage_split (spBfh t) (spBhg t). +Qed. + +Definition fct_uniformType_mixin := + UniformMixin fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split erefl. + +Definition fct_topologicalTypeMixin := + topologyOfEntourageMixin fct_uniformType_mixin. + +Canonical generic_source_filter := @Filtered.Source _ _ _ (nbhs_ fct_ent). +Canonical fct_topologicalType := + TopologicalType (T -> U) fct_topologicalTypeMixin. +Canonical fct_uniformType := UniformType (T -> U) fct_uniformType_mixin. + +End fct_Uniform. + +Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType) + (F : set (set (T -> U))) (FF : Filter F) (f : T -> U) : + F --> f <-> + forall A, entourage A -> + \forall g \near F, forall t, A (f t, g t). +Proof. +split. + move=> /cvg_entourageP Ff A entA. + by apply: (Ff [set fg | forall t : T, A (fg.1 t, fg.2 t)]); exists A. +move=> Ff; apply/cvg_entourageP => A [P entP sPA]; near=> g. +by apply: sPA => /=; near: g; apply: Ff. +Grab Existential Variables. all: end_near. Qed. + +Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := + exists2 B, entourage B & forall PQ, A PQ -> forall p q, + PQ.1 p -> PQ.2 q -> B (p,q). +Canonical set_filter_source (U : uniformType) := + @Filtered.Source Prop _ U (fun A => nbhs_ (@entourage_set U) A). + (** * PseudoMetric spaces defined using balls *) -Definition nbhs_ {R : numDomainType} {T T'} (ball : T -> R -> set T') (x : T) := - @filter_from R _ [set x | 0 < x] (ball x). +Definition entourage_ {R : numDomainType} {T T'} (ball : T -> R -> set T') := + @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]). -Lemma nbhs_E {R : numDomainType} {T T'} (ball : T -> R -> set T') x : - nbhs_ ball x = @filter_from R _ [set x : R | 0 < x] (ball x). +Lemma entourage_E {R : numDomainType} {T T'} (ball : T -> R -> set T') : + entourage_ ball = + @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]). Proof. by []. Qed. Module PseudoMetric. -Record mixin_of (R : numDomainType) (M : Type) (nbhs : M -> set (set M)) := Mixin { +Record mixin_of (R : numDomainType) (M : Type) (entourage : set (set (M * M))) := Mixin { ball : M -> R -> M -> Prop ; ax1 : forall x (e : R), 0 < e -> ball x e x ; ax2 : forall x y (e : R), ball x e y -> ball y e x ; ax3 : forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z; - ax4 : nbhs = nbhs_ ball + ax4 : entourage = entourage_ ball }. Record class_of (R : numDomainType) (M : Type) := Class { - base : Topological.class_of M; - mixin : mixin_of R (Filtered.nbhs_op base) + base : Uniform.class_of M; + mixin : mixin_of R (Uniform.entourage base) }. Section ClassDef. @@ -2661,12 +3145,12 @@ Definition class := let: Pack _ c := cT return class_of R cT in c. Definition clone c of phant_id class c := @Pack T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of R xT). -Local Coercion base : class_of >-> Topological.class_of. +Local Coercion base : class_of >-> Uniform.class_of. Local Coercion mixin : class_of >-> mixin_of. -Definition pack nbhs' (m : @mixin_of R T nbhs') := - fun bT (b : Topological.class_of T) of phant_id (@Topological.class bT) b => - fun m' of phant_id m (m' : @mixin_of R T (Filtered.nbhs_op b)) => +Definition pack ent (m : @mixin_of R T ent) := + fun bT (b : Uniform.class_of T) of phant_id (@Uniform.class bT) b => + fun m' of phant_id m (m' : @mixin_of R T (Uniform.entourage b)) => @Pack T (@Class R _ b m'). Definition eqType := @Equality.Pack cT xclass. @@ -2674,13 +3158,14 @@ Definition choiceType := @Choice.Pack cT xclass. Definition pointedType := @Pointed.Pack cT xclass. Definition filteredType := @Filtered.Pack cT cT xclass. Definition topologicalType := @Topological.Pack cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. End ClassDef. Module Exports. Coercion sort : type >-> Sortclass. -Coercion base : class_of >-> Topological.class_of. +Coercion base : class_of >-> Uniform.class_of. Coercion mixin : class_of >-> mixin_of. Coercion eqType : type >-> Equality.type. Canonical eqType. @@ -2692,6 +3177,8 @@ Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. Notation pseudoMetricType := type. Notation PseudoMetricType T m := (@pack _ T _ m _ _ idfun _ idfun). Notation PseudoMetricMixin := Mixin. @@ -2706,10 +3193,9 @@ End PseudoMetric. Export PseudoMetric.Exports. -Section PseudoMetricTopology. +Section PseudoMetricUniformity. -Lemma my_ball_le (R : numDomainType) (M : Type) (nbhs' : M -> set (set M)) - (m : PseudoMetric.mixin_of R nbhs') : +Lemma my_ball_le (R : numDomainType) (M : Type) (ent : set (set (M * M))) (m : PseudoMetric.mixin_of R ent) : forall (x : M), {homo PseudoMetric.ball m x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}. Proof. move=> x e1 e2 le12 y xe1_y. @@ -2721,36 +3207,66 @@ exact: PseudoMetric.ax1. Qed. Obligation Tactic := idtac. -Program Definition topologyOfBallMixin (R : numFieldType) (T : Type) - (nbhs' : T -> set (set T)) (m : PseudoMetric.mixin_of R nbhs') : - Topological.mixin_of nbhs' := topologyOfFilterMixin _ _ _. +Program Definition uniformityOfBallMixin (R : numFieldType) (T : Type) + (ent : set (set (T * T))) (nbhs : T -> set (set T)) (nbhsE : nbhs = nbhs_ ent) + (m : PseudoMetric.mixin_of R ent) : Uniform.mixin_of nbhs := + UniformMixin _ _ _ _ nbhsE. Next Obligation. -move=> R T lo m p; -rewrite (PseudoMetric.ax4 m) nbhs_E; apply filter_from_proper; last first. - move=> e egt0; exists p; suff : PseudoMetric.ball m p (PosNum egt0)%:num p by []. - exact: PseudoMetric.ax1. -apply: filter_from_filter => [|_ _ /posnumP[e1] /posnumP[e2]]; first by exists 1. -exists (Num.min e1 e2)%:num; rewrite ?subsetI//. -by split=> //; apply: my_ball_le; rewrite -leEsub le_minl lexx ?orbT. +move=> R T ent nbhs nbhsE m; rewrite (PseudoMetric.ax4 m). +apply: filter_from_filter; first by exists 1. +move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //. +by rewrite subsetI; split=> ?; apply: my_ball_le; + rewrite -leEsub le_minl lexx ?orbT. Qed. Next Obligation. -move=> R T loc m p A; rewrite (PseudoMetric.ax4 m) nbhs_E => - [_/posnumP[e]]; apply. -by have : PseudoMetric.ball m p e%:num p by exact: PseudoMetric.ax1. +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m). +move=> [e egt0 sbeA] xy xey. +apply: sbeA; rewrite xey; exact: PseudoMetric.ax1. Qed. Next Obligation. -move=> R T loc m p A; rewrite (PseudoMetric.ax4 m) nbhs_E => - [_/posnumP[e] pe_A]. -exists (e%:num / 2) => // q phe_q. -rewrite nbhs_E; exists (e%:num / 2) => // r qhe_r. -by apply: pe_A; rewrite [e%:num]splitr; apply: PseudoMetric.ax3 qhe_r. +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m) => - [e egt0 sbeA]. +by exists e => // xy xye; apply: sbeA; apply: PseudoMetric.ax2. +Qed. +Next Obligation. +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m). +move=> [_/posnumP[e] sbeA]. +exists [set xy | PseudoMetric.ball m xy.1 (e%:num / 2) xy.2]. + by exists (e%:num / 2). +move=> xy [z xzhe zyhe]; apply: sbeA. +by rewrite [e%:num]splitr; apply: PseudoMetric.ax3 zyhe. Qed. -End PseudoMetricTopology. +End PseudoMetricUniformity. Definition ball {R : numDomainType} {M : pseudoMetricType R} := PseudoMetric.ball (PseudoMetric.class M). -Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : nbhs_ (@ball R M) = nbhs. +Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} : entourage_ (@ball R M) = entourage. Proof. by case: M=> [?[?[]]]. Qed. +Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} : + @filter_from R _ [set x : R | 0 < x] + (fun e => [set xy | @ball R M xy.1 e xy.2]) = entourage. +Proof. by rewrite -entourage_ballE. Qed. + +Lemma entourage_ball {R : numDomainType} (M : pseudoMetricType R) + (e : {posnum R}) : entourage [set xy : M * M | ball xy.1 e%:num xy.2]. +Proof. by rewrite -entourage_ballE; exists e%:num. Qed. +Hint Resolve entourage_ball. + +Definition nbhs_ball_ {R : numDomainType} {T T'} (ball : T -> R -> set T') + (x : T) := @filter_from R _ [set e | e > 0] (ball x). + +Definition nbhs_ball {R : numDomainType} {M : pseudoMetricType R} := + nbhs_ball_ (@ball R M). + +Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : (@nbhs_ball R M) = nbhs. +Proof. +rewrite predeq2E => x P; rewrite -nbhs_entourageE; split. + by move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2]. +rewrite -entourage_ballE; move=> [A [e egt0 sbeA] sAP]. +by exists e => // ??; apply/sAP/sbeA. +Qed. + Lemma filter_from_ballE {R : numDomainType} {M : pseudoMetricType R} x : @filter_from R _ [set x : R | 0 < x] (@ball R M x) = nbhs x. Proof. by rewrite -nbhs_ballE. Qed. @@ -2759,8 +3275,8 @@ Module Export NbhsBall. Definition nbhs_simpl := (nbhs_simpl,@filter_from_ballE,@nbhs_ballE). End NbhsBall. -Lemma nbhsP {R : numDomainType} {M : pseudoMetricType R} (x : M) P : - nbhs x P <-> nbhs_ ball x P. +Lemma nbhs_ballP {R : numDomainType} {M : pseudoMetricType R} (x : M) P : + nbhs x P <-> nbhs_ball x P. Proof. by rewrite nbhs_simpl. Qed. Lemma ball_center {R : numDomainType} (M : pseudoMetricType R) (x : M) @@ -2781,14 +3297,13 @@ Lemma ball_triangle (y x z : M) (e1 e2 : R) : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. Proof. exact: PseudoMetric.ax3. Qed. -Lemma nbhs_ball (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num). -Proof. by apply/nbhsP; exists eps%:num. Qed. +Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num). +Proof. by apply/nbhs_ballP; exists eps%:num. Qed. Lemma open_nbhs_ball (x : M) (eps : {posnum R}) : open_nbhs x ((ball x eps%:num)^°). Proof. split; first exact: open_interior. -apply: nbhs_singleton; apply: nbhs_interior. -by apply/nbhsP; exists eps%:num. +by apply: nbhs_singleton; apply: nbhs_interior; apply:nbhsx_ballx. Qed. Lemma ball_ler (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2. @@ -2800,22 +3315,15 @@ Qed. Lemma ball_le (x : M) (e1 e2 : R) : (e1 <= e2) -> ball x e1 `<=` ball x e2. Proof. by move=> /ball_ler. Qed. -Definition entourages : set (set (M * M)):= - filter_from [set eps : R | eps > 0] - (fun eps => [set xy | ball xy.1 eps xy.2]). - -Global Instance entourages_filter : ProperFilter entourages. +Global Instance entourage_proper_filter : ProperFilter (@entourage M). Proof. -apply filter_from_proper; last by exists (point,point); apply: ballxx. -apply: filter_from_filter; first by exists 1; rewrite ltr01. -move=> _ _ /posnumP[i] /posnumP[j]; exists (Num.min i j)%:num; rewrite ?subsetI//. -by split=> // ?; apply: ball_ler; rewrite -leEsub le_minl lexx ?orbT. +apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA]. +by exists (point, point); apply: sbeA; apply: ballxx. Qed. -Typeclasses Opaque entourages. Lemma near_ball (y : M) (eps : {posnum R}) : \forall y' \near y, ball y eps%:num y'. -Proof. exact: nbhs_ball. Qed. +Proof. exact: nbhsx_ballx. Qed. Lemma cvg_ballP {F} {FF : Filter F} (y : M) : F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. @@ -2841,8 +3349,8 @@ Lemma cvgi_ballP T {F} {FF : Filter F} (f : T -> M -> Prop) y : f `@ F --> y <-> forall eps : R, 0 < eps -> \forall x \near F, exists z, f x z /\ ball y eps z. Proof. -split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/nbhs_ball. -move=> /nbhsP[_ /posnumP[eps] subP]. +split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/nbhsx_ballx. +move=> /nbhs_ballP[_ /posnumP[eps] subP]. rewrite near_simpl near_mapi; near=> x. have [//|z [fxz yz]] := near (Fy _ (posnum_gt0 eps)) x. by exists z => //; split => //; apply: subP. @@ -2854,12 +3362,8 @@ Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y : forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z]. Proof. by move/cvgi_ballP. Qed. -Definition ball_set (A : set M) e := \bigcup_(p in A) ball p e. -Canonical set_filter_source := - @Filtered.Source Prop _ M (fun A => nbhs_ ball_set A). - End pseudoMetricType_numDomainType. -Hint Resolve nbhs_ball : core. +Hint Resolve nbhsx_ballx : core. Hint Resolve close_refl : core. Arguments close_cvg {T} F1 F2 {FF2} _. @@ -2885,8 +3389,8 @@ rewrite propeqE; split => [cxy eps|cxy]. have [z [zx zy]] := cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos) _ (open_nbhs_ball _ (eps%:num/2)%:pos). by apply: (@ball_splitl z); apply: interior_subset. -move=> B /open_nbhs_nbhs/nbhsP[_/posnumP[e2 e2B]]. -move=> A /open_nbhs_nbhs/nbhsP[_/posnumP[e1 e1A]]. +move=> B /open_nbhs_nbhs/nbhs_ballP[_/posnumP[e2 e2B]]. +move=> A /open_nbhs_nbhs/nbhs_ballP[_/posnumP[e1 e1A]]. by exists y; split; [apply/e1A|apply/e2B/ballxx]. Qed. @@ -2897,8 +3401,8 @@ Qed. Lemma close_cvgxx (x y : M) : close x y -> x --> y. Proof. -rewrite ball_close => cxy P /= /nbhsP /= [_/posnumP [eps] epsP]. -apply/nbhsP; exists (eps%:num / 2) => // z bxz. +rewrite ball_close => cxy P /= /nbhs_ballP /= [_/posnumP [eps] epsP]. +apply/nbhs_ballP; exists (eps%:num / 2) => // z bxz. by apply: epsP; apply: ball_splitr (cxy _) bxz. Qed. @@ -2921,12 +3425,12 @@ Lemma ball_hausdorff : hausdorff T = Proof. rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]]. move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]]. - have /nbhsP[_/posnumP[r] rA] : nbhs a A by apply: open_nbhs_nbhs. - have /nbhsP[_/posnumP[s] rB] : nbhs b B by apply: open_nbhs_nbhs. + have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by apply: open_nbhs_nbhs. + have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by apply: open_nbhs_nbhs. by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0). move=> r s /eqP brs_eq0; exists ((ball a r%:num)^°, (ball b s%:num)^°) => /=. split; by rewrite inE; apply: nbhs_singleton; apply: nbhs_interior; - apply/nbhsP; apply: in_filter_from. + apply/nbhs_ballP; apply: in_filter_from. split; do ?by apply: open_interior. by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset. Qed. @@ -2936,25 +3440,27 @@ Lemma close_cluster (R : numFieldType) (T : pseudoMetricType R) (x y : T) : close x y = cluster (nbhs x) y. Proof. rewrite propeqE; split => xy. -- move=> A B xA; rewrite -nbhs_ballE nbhs_E => -[_/posnumP[e] yeB]. +- move=> A B xA; rewrite -nbhs_ballE => -[_/posnumP[e] yeB]. exists x; split; first exact: nbhs_singleton. by apply/yeB/ball_sym; move: e {yeB}; rewrite -ball_close. - rewrite ball_close => e. have e20 : 0 < e%:num / 2 by apply: divr_gt0. set e2 := PosNum e20. - case: (xy _ _ (nbhs_ball x e2) (nbhs_ball y e2)) => z [xz /ball_sym zy]. + case: (xy _ _ (nbhsx_ballx x e2) (nbhsx_ballx y e2)) => z [xz /ball_sym zy]. by rewrite (splitr e%:num); exact: (ball_triangle xz). Qed. Section entourages. Variable R : numDomainType. -Definition unif_continuous (U V : pseudoMetricType R) (f : U -> V) := - (fun xy => (f xy.1, f xy.2)) @ entourages --> entourages. Lemma unif_continuousP (U V : pseudoMetricType R) (f : U -> V) : unif_continuous f <-> forall e, e > 0 -> exists2 d, d > 0 & forall x, ball x.1 d x.2 -> ball (f x.1) e (f x.2). -Proof. exact: filter_fromP. Qed. +Proof. +have fappF : Filter ((fun xy => (f xy.1, f xy.2)) @ entourage_ ball). + by rewrite entourage_ballE; apply: fmap_filter. +by rewrite /unif_continuous -!entourage_ballE filter_fromP. +Qed. End entourages. (** ** Specific pseudoMetric spaces *) @@ -2992,21 +3498,23 @@ by rewrite inE => /orP [/eqP->|/ihl leminlfi]; Qed. Canonical R_pointedType := PointedType R 0. -Lemma mx_nbhs : nbhs = nbhs_ mx_ball. +Lemma mx_entourage : entourage = entourage_ mx_ball. Proof. -rewrite predeq2E => x A; split; last first. - by move=> [_/posnumP[e] xe_A]; exists (fun i j => ball (x i j) e%:num). -move=> [P]; rewrite -nbhs_ballE => x_P sPA. +rewrite predeqE=> A; split; last first. + move=> [_/posnumP[e] sbeA]. + by exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]). +move=> [P]; rewrite -entourage_ballE => entP sPA. +set diag := fun (e : {posnum R}) => [set xy : T * T | ball xy.1 e%:num xy.2]. exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos - (fun e : {posnum R} => ball (x i j) e%:num `<=` P i j))%:num => //. -move=> y xmin_y; apply: sPA => i j. -have /(xgetPex 1%:pos): exists e : {posnum R}, ball (x i j) (e)%:num `<=` P i j. - by have [_/posnumP[e]] := x_P i j; exists e. -apply; apply: ball_ler (xmin_y i j). + (fun e : {posnum R} => diag e `<=` P i j))%:num => //. +move=> MN MN_min; apply: sPA => i j. +have /(xgetPex 1%:pos): exists e : {posnum R}, diag e `<=` P i j. + by have [_/posnumP[e]] := entP i j; exists e. +apply; apply: ball_ler (MN_min i j). by apply: le_trans (bigminr_ler _ _ i) _; apply: bigminr_ler. Qed. Definition matrix_pseudoMetricType_mixin := - PseudoMetric.Mixin mx_ball_center mx_ball_sym mx_ball_triangle mx_nbhs. + PseudoMetric.Mixin mx_ball_center mx_ball_sym mx_ball_triangle mx_entourage. Canonical matrix_pseudoMetricType := PseudoMetricType 'M[T]_(m, n) matrix_pseudoMetricType_mixin. End matrix_PseudoMetric. @@ -3027,17 +3535,24 @@ Lemma prod_ball_triangle x y z (e1 e2 : R) : Proof. by move=> [bxy1 bxy2] [byz1 byz2]; split; apply: ball_triangle; eassumption. Qed. -Lemma prod_nbhs : nbhs = nbhs_ prod_ball. -Proof. -rewrite predeq2E => -[x y] P; split=> [[[A B] /=[xX yY] XYP] |]; last first. - by move=> [_ /posnumP[eps] epsP]; exists (ball x eps%:num, ball y eps%:num) => /=. -move: xX yY => /nbhsP [_ /posnumP[ex] eX] /nbhsP [_ /posnumP[ey] eY]. -exists (Num.min ex ey)%:num => // -[x' y'] [/= xx' yy']; apply: XYP; split=> /=. - by apply/eX/(ball_ler _ xx'); rewrite -leEsub le_minl lexx. -by apply/eY/(ball_ler _ yy'); rewrite -leEsub le_minl lexx orbT. +Lemma prod_entourage : entourage = entourage_ prod_ball. +Proof. +rewrite predeqE => P; split; last first. + move=> [_/posnumP[e] sbeP]. + exists ([set xy | ball xy.1 e%:num xy.2], + [set xy | ball xy.1 e%:num xy.2]) => //=. + move=> [[a b] [c d]] [bab bcd]; exists ((a, c), (b, d))=> //=. + exact: sbeP. +move=> [[A B]] /=; rewrite -!entourage_ballE. +move=> [[_/posnumP[eA] sbA] [_/posnumP[eB] sbB] sABP]. +exists (Num.min eA eB)%:num => // - [[a b] [c d] [/= bac bbd]]. +suff /sABP [] : (A `*` B) ((a, c), (b, d)) by move=> [[??] [??]] ? [<-<-<-<-]. +split; [apply: sbA|apply: sbB] => /=. + by apply: ball_ler bac; rewrite -leEsub le_minl lexx. +by apply: ball_ler bbd; rewrite -leEsub le_minl lexx orbT. Qed. Definition prod_pseudoMetricType_mixin := - PseudoMetric.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_nbhs. + PseudoMetric.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage. End prod_PseudoMetric. Canonical prod_pseudoMetricType (R : numDomainType) (U V : pseudoMetricType R) := PseudoMetricType (U * V) (@prod_pseudoMetricType_mixin R U V). @@ -3065,73 +3580,41 @@ Proof. by move=> P t; apply: ball_sym. Qed. Lemma fct_ball_triangle (x y z : T -> U) (e1 e2 : R) : fct_ball x e1 y -> fct_ball y e2 z -> fct_ball x (e1 + e2) z. Proof. by move=> xy yz t; apply: (@ball_triangle _ _ (y t)). Qed. +Lemma fct_entourage : entourage = entourage_ fct_ball. +Proof. +rewrite predeqE => A; split; last first. + by move=> [_/posnumP[e] sbeA]; exists [set xy | ball xy.1 e%:num xy.2]. +move=> [P]; rewrite -entourage_ballE => -[_/posnumP[e] sbeP] sPA. +by exists e%:num => // fg fg_e; apply: sPA => t; apply: sbeP; apply: fg_e. +Qed. Definition fct_pseudoMetricType_mixin := - PseudoMetricMixin fct_ball_center fct_ball_sym fct_ball_triangle erefl. -Definition fct_topologicalTypeMixin := - topologyOfBallMixin fct_pseudoMetricType_mixin. -Canonical generic_source_filter := @Filtered.Source _ _ _ (nbhs_ fct_ball). -Canonical fct_topologicalType := - TopologicalType (T -> U) fct_topologicalTypeMixin. + PseudoMetricMixin fct_ball_center fct_ball_sym fct_ball_triangle fct_entourage. Canonical fct_pseudoMetricType := PseudoMetricType (T -> U) fct_pseudoMetricType_mixin. End fct_PseudoMetric. -(** ** Complete pseudoMetric spaces *) -Definition cauchy_ex {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) := - forall eps : R, 0 < eps -> exists x, F (ball x eps). - -Definition cauchy {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) := - forall e, e > 0 -> \forall x & y \near F, ball x e y. - -Lemma cauchy_entouragesP (R : numDomainType) (T : pseudoMetricType R) - (F : set (set T)) (FF : Filter F) : - cauchy F <-> (F, F) --> entourages. -Proof. -split=> cauchyF; last first. - by move=> _/posnumP[eps]; apply: cauchyF; exists eps%:num. -move=> U [_/posnumP[eps] xyepsU]. -by near=> x; apply: xyepsU; near: x; apply: cauchyF. -Grab Existential Variables. all: end_near. Qed. -Arguments cauchy_entouragesP {R T} F {FF}. - -Lemma cvg_cauchy_ex {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) : - cvg F -> cauchy_ex F. -Proof. by move=> Fl _/posnumP[eps]; exists (lim F); apply/Fl/nbhs_ball. Qed. -Arguments cvg_cauchy_ex {R T} F. +(** ** Complete uniform spaces *) -Lemma cauchy_exP (R : numFieldType) (T : pseudoMetricType R) - (F : set (set T)) (FF : Filter F) : - cauchy_ex F -> cauchy F. -Proof. -move=> Fc; apply/cauchy_entouragesP => A [_/posnumP[e] sdeA]. -have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sdeA => /=. -by apply: (@ball_splitr _ _ z); [near: x|near: y]. -Grab Existential Variables. all: end_near. Qed. -Arguments cauchy_exP {R T} F {FF}. +Definition cauchy {T : uniformType} (F : set (set T)) := (F, F) --> entourage. -Lemma cauchyP (R : numFieldType) (T : pseudoMetricType R) - (F : set (set T)) (PF : ProperFilter F) : - cauchy F <-> cauchy_ex F. +Lemma cvg_cauchy {T : uniformType} (F : set (set T)) : Filter F -> + [cvg F in T] -> cauchy F. Proof. -split=> [Fcauchy _/posnumP[e] |/cauchy_exP//]. -by near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F); apply: Fcauchy. -Grab Existential Variables. all: end_near. Qed. -Arguments cauchyP {R T} F {PF}. - -Lemma cvg_cauchy {R : numFieldType} {T : pseudoMetricType R} - (F : set (set T)) {FF : Filter F} : cvg F -> cauchy F. -Proof. by move=> /cvg_cauchy_ex /cauchy_exP. Qed. -Arguments cvg_cauchy {R T} F {FF}. +move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA. +exists (to_set ((B^-1)%classic) (lim F), to_set B (lim F)). + split=> /=; apply: cvF; rewrite /= -nbhs_entourageE; last by exists B. + by exists (B^-1)%classic => //; apply: entourage_inv. +by move=> ab [/= Balima Blimb]; apply: sB2A; exists (lim F). +Qed. Module Complete. -Definition axiom (R : numDomainType) (T : pseudoMetricType R) := +Definition axiom (T : uniformType) := forall (F : set (set T)), ProperFilter F -> cauchy F -> F --> lim F. Section ClassDef. -Variable R : numDomainType. Record class_of (T : Type) := Class { - base : PseudoMetric.class_of R T ; - mixin : axiom (PseudoMetric.Pack base) + base : Uniform.class_of T ; + mixin : axiom (Uniform.Pack base) }. -Local Coercion base : class_of >-> PseudoMetric.class_of. +Local Coercion base : class_of >-> Uniform.class_of. Local Coercion mixin : class_of >-> Complete.axiom. Structure type := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. @@ -3140,18 +3623,18 @@ Definition class := let: Pack _ c := cT return class_of cT in c. Definition clone c of phant_id class c := @Pack T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : axiom (@PseudoMetric.Pack R T b0)) := - fun bT b of phant_id (@PseudoMetric.class R bT) b => +Definition pack b0 (m0 : axiom (@Uniform.Pack T b0)) := + fun bT b of phant_id (@Uniform.class bT) b => fun m of phant_id m m0 => @Pack T (@Class T b m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition pointedType := @Pointed.Pack cT xclass. Definition filteredType := @Filtered.Pack cT cT xclass. Definition topologicalType := @Topological.Pack cT xclass. -Definition pseudoMetricType := @PseudoMetric.Pack R cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> PseudoMetric.class_of. +Coercion base : class_of >-> Uniform.class_of. Coercion mixin : class_of >-> axiom. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. @@ -3164,103 +3647,120 @@ Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Coercion topologicalType : type >-> Topological.type. Canonical topologicalType. -Coercion pseudoMetricType : type >-> PseudoMetric.type. -Canonical pseudoMetricType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. Notation completeType := type. Notation "[ 'completeType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) (at level 0, format "[ 'completeType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'completeType' 'of' T ]" := (@clone T _ _ id) (at level 0, format "[ 'completeType' 'of' T ]") : form_scope. -Notation CompleteType T m := (@pack _ T _ m _ _ idfun _ idfun). +Notation CompleteType T m := (@pack T _ m _ _ idfun _ idfun). End Exports. End Complete. Export Complete.Exports. Section completeType1. -Context {R : numDomainType} {T : completeType R}. -Lemma cauchy_cvg (F : set (set T)) (FF : ProperFilter F) : cauchy F -> cvg F. -Proof. by case: T F FF => [? [?]]. Qed. - -End completeType1. -Arguments cauchy_cvg {R} {T} F {FF}. +Context {T : completeType}. -Section completeType2. -Context {R : numFieldType} {T : completeType R}. +Lemma cauchy_cvg (F : set (set T)) (FF : ProperFilter F) : + cauchy F -> cvg F. +Proof. by case: T F FF => [? [?]]. Qed. Lemma cauchy_cvgP (F : set (set T)) (FF : ProperFilter F) : cauchy F <-> cvg F. Proof. by split=> [/cauchy_cvg|/cvg_cauchy]. Qed. -End completeType2. -Arguments cauchy_cvgP {R} {T} F {FF}. +End completeType1. +Arguments cauchy_cvg {T} F {FF} _. +Arguments cauchy_cvgP {T} F {FF}. Section matrix_Complete. -Variables (R : numFieldType) (T : completeType R) (m n : nat). + +Variables (T : completeType) (m n : nat). Lemma mx_complete (F : set (set 'M[T]_(m, n))) : ProperFilter F -> cauchy F -> cvg F. Proof. move=> FF Fc. -have /(_ _ _) /cauchy_cvg cvF : +have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF : cauchy ((fun M : 'M[T]_(m, n) => M _ _) @ F). - by move=> ?? _ /posnumP[e]; rewrite near_simpl; apply: filterS (Fc _ _). + move=> i j A /= entA; rewrite near_simpl -near2E near_map2. + by apply: Fc; exists (fun _ _ => A). apply/cvg_ex. -exists (\matrix_(i, j) (lim ((fun M : 'M[T]_(m, n) => M i j) @ F) : T)). -apply/cvg_ballP => _ /posnumP[e]; near=> M => i j. -rewrite mxE; near F => M' => /=; apply: (@ball_splitl _ _ (M' i j)). - by near: M'; apply/cvF/nbhs_ball. -by move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: filterS (Fc _ _). +set Mlim := \matrix_(i, j) (lim ((fun M : 'M[T]_(m, n) => M i j) @ F) : T). +exists Mlim; apply/cvg_mx_entourageP => A entA; near=> M => i j; near F => M'. +apply: subset_split_ent => //; exists (M' i j) => /=. + by near: M'; rewrite mxE; apply: cvF. +move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: Fc. +by exists (fun _ _ => (split_ent A)^-1%classic) => ?? //; apply: entourage_inv. Grab Existential Variables. all: end_near. Qed. + Canonical matrix_completeType := CompleteType 'M[T]_(m, n) mx_complete. + End matrix_Complete. Section fun_Complete. -Context {T : choiceType} {R : numFieldType} {U : completeType R}. + +Context {T : choiceType} {U : completeType}. + Lemma fun_complete (F : set (set (T -> U))) {FF : ProperFilter F} : cauchy F -> cvg F. Proof. -move=> Fc; have /(_ _) /cauchy_cvg Ft_cvg : cauchy (@^~_ @ F). - by move=> t e ?; rewrite near_simpl; apply: filterS (Fc _ _). +move=> Fc. +have /(_ _) /cauchy_cvg /cvg_app_entourageP cvF : cauchy (@^~_ @ F). + move=> t A /= entA; rewrite near_simpl -near2E near_map2. + by apply: Fc; exists A. apply/cvg_ex; exists (fun t => lim (@^~t @ F)). -apply/cvg_ballPpos => e; near=> f => t; near F => g => /=. -apply: (@ball_splitl _ _ (g t)); first by near: g; exact/Ft_cvg/nbhs_ball. -by move: (t); near: g; near: f; apply: nearP_dep; apply: filterS (Fc _ _). +apply/cvg_fct_entourageP => A entA; near=> f => t; near F => g. +apply: (entourage_split (g t)) => //; first by near: g; apply: cvF. +move: (t); near: g; near: f; apply: nearP_dep; apply: Fc. +exists ((split_ent A)^-1)%classic=> //=. +by apply: entourage_inv; apply: entourage_split_ent. Grab Existential Variables. all: end_near. Qed. + Canonical fun_completeType := CompleteType (T -> U) fun_complete. + End fun_Complete. (** ** Limit switching *) Section Cvg_switch. Context {T1 T2 : choiceType}. -Lemma cvg_switch_1 {R : numFieldType} {U : pseudoMetricType R} +Lemma cvg_switch_1 {U : uniformType} F1 {FF1 : ProperFilter F1} F2 {FF2 : Filter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) (l : U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> h @ F1 --> l -> g @ F2 --> l. Proof. -move=> fg fh hl; apply/cvg_ballPpos => e. -rewrite near_simpl; near F1 => x1; near=> x2. -apply: (@ball_split _ _ (h x1)); first by near: x1; apply/hl/nbhs_ball. -apply: (@ball_splitl _ _ (f x1 x2)); first by near: x2; apply/fh/nbhs_ball. -by move: (x2); near: x1; apply/(cvg_ball fg). +move=> fg fh hl; apply/cvg_app_entourageP => A entA. +near F1 => x1; near=> x2; apply: (entourage_split (h x1)) => //. + by near: x1; apply/(hl (to_set _ l)) => /=. +apply: (entourage_split (f x1 x2)) => //. + by near: x2; apply/(fh x1 (to_set _ _)) => /=. +move: (x2); near: x1; have /cvg_fct_entourageP /(_ (_^-1%classic)):= fg; apply. +exact: entourage_inv. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_switch_2 {R : numFieldType} {U : completeType R} +Lemma cvg_switch_2 {U : completeType} F1 {FF1 : ProperFilter F1} F2 {FF2 : ProperFilter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x, f x @ F2 --> h x) -> [cvg h @ F1 in U]. Proof. -move=> fg fh; apply: cauchy_cvg => _/posnumP[e]. -rewrite !near_simpl; near=> x1 y1=> /=; near F2 => x2. -apply: (@ball_splitl _ _ (f x1 x2)); first by near: x2; apply/fh/nbhs_ball. -apply: (@ball_split _ _ (f y1 x2)); first by near: x2; apply/fh/nbhs_ball. -apply: (@ball_splitr _ _ (g x2)); move: (x2); [near: y1|near: x1]; -by apply/(cvg_ball fg). +move=> fg fh; apply: cauchy_cvg => A entA. +rewrite !near_simpl -near2_pair near_map2; near=> x1 y1 => /=; near F2 => x2. +apply: (entourage_split (f x1 x2)) => //. + by near: x2; apply/(fh _ (to_set _ _)) => /=. +apply: (entourage_split (f y1 x2)) => //; last first. + near: x2; apply/(fh _ (to_set ((_^-1)%classic) _)). + exact: nbhs_entourage (entourage_inv _). +apply: (entourage_split (g x2)) => //; move: (x2); [near: x1|near: y1]. + have /cvg_fct_entourageP /(_ (_^-1)%classic) := fg; apply. + exact: entourage_inv. +by have /cvg_fct_entourageP := fg; apply. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_switch {R : numFieldType} {U : completeType R} +Lemma cvg_switch {U : completeType} F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> @@ -3271,3 +3771,114 @@ by exists [lim h @ F1 in U]; split=> //; apply: cvg_switch_1 Hfg Hfh hcv. Qed. End Cvg_switch. + +(** ** Complete pseudoMetric spaces *) + +Definition cauchy_ex {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) := + forall eps : R, 0 < eps -> exists x, F (ball x eps). + +Definition cauchy_ball {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) := + forall e, e > 0 -> \forall x & y \near F, ball x e y. + +Lemma cauchy_ballP (R : numDomainType) (T : pseudoMetricType R) + (F : set (set T)) (FF : Filter F) : + cauchy_ball F <-> cauchy F. +Proof. +split=> cauchyF; last first. + by move=> _/posnumP[eps]; apply: cauchyF; rewrite nbhs_simpl. +move=> U; rewrite -entourage_ballE => - [_/posnumP[eps] xyepsU]. +by near=> x; apply: xyepsU; near: x; apply: cauchyF. +Grab Existential Variables. all: end_near. Qed. +Arguments cauchy_ballP {R T} F {FF}. + +Lemma cauchy_exP (R : numFieldType) (T : pseudoMetricType R) + (F : set (set T)) (FF : Filter F) : + cauchy_ex F -> cauchy F. +Proof. +move=> Fc A; rewrite !nbhs_simpl /= -entourage_ballE => -[_/posnumP[e] sdeA]. +have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sdeA => /=. +by apply: (@ball_splitr _ _ z); [near: x|near: y]. +Grab Existential Variables. all: end_near. Qed. +Arguments cauchy_exP {R T} F {FF}. + +Lemma cauchyP (R : numFieldType) (T : pseudoMetricType R) + (F : set (set T)) (PF : ProperFilter F) : + cauchy F <-> cauchy_ex F. +Proof. +split=> [Fcauchy _/posnumP[e] |/cauchy_exP//]. +near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F). +by apply: Fcauchy; rewrite nbhs_simpl. +Grab Existential Variables. all: end_near. Qed. +Arguments cauchyP {R T} F {PF}. + +Module CompletePseudoMetric. +Section ClassDef. +Variable R : numDomainType. +Record class_of (T : Type) := Class { + base : PseudoMetric.class_of R T; + mixin : Complete.axiom (Uniform.Pack base) +}. +Local Coercion base : class_of >-> PseudoMetric.class_of. +Definition base2 T m := Complete.Class (@mixin T m). +Local Coercion base2 : class_of >-> Complete.class_of. + +Structure type := Pack { sort; _ : class_of sort }. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). +Definition class := let: Pack _ c := cT return class_of cT in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. +Notation xclass := (class : class_of xT). +Definition pack := + fun bT b & phant_id (@PseudoMetric.class R bT) (b : PseudoMetric.class_of R T) => + fun mT m & phant_id (Complete.class mT) (@Complete.Class T b m) => + Pack (@Class T b m). +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition pointedType := @Pointed.Pack cT xclass. +Definition filteredType := @Filtered.Pack cT cT xclass. +Definition topologicalType := @Topological.Pack cT xclass. +Definition uniformType := @Uniform.Pack cT xclass. +Definition completeType := @Complete.Pack cT xclass. +Definition pseudoMetricType := @PseudoMetric.Pack R cT xclass. +Definition pseudoMetric_completeType := @Complete.Pack pseudoMetricType xclass. +End ClassDef. +Module Exports. +Coercion base : class_of >-> PseudoMetric.class_of. +Coercion mixin : class_of >-> Complete.axiom. +Coercion base2 : class_of >-> Complete.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion pointedType : type >-> Pointed.type. +Canonical pointedType. +Coercion filteredType : type >-> Filtered.type. +Canonical filteredType. +Coercion topologicalType : type >-> Topological.type. +Canonical topologicalType. +Coercion uniformType : type >-> Uniform.type. +Canonical uniformType. +Coercion completeType : type >-> Complete.type. +Canonical completeType. +Coercion pseudoMetricType : type >-> PseudoMetric.type. +Canonical pseudoMetricType. +Canonical pseudoMetric_completeType. +Notation completePseudoMetricType := type. +Notation "[ 'completePseudoMetricType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) + (at level 0, format "[ 'completePseudoMetricType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'completePseudoMetricType' 'of' T ]" := (@clone T _ _ id) + (at level 0, format "[ 'completePseudoMetricType' 'of' T ]") : form_scope. +Notation CompletePseudoMetricType T m := (@pack _ T _ _ id _ _ id). +End Exports. +End CompletePseudoMetric. +Export CompletePseudoMetric.Exports. + +Canonical matrix_completePseudoMetricType (R : numFieldType) + (T : completePseudoMetricType R) (m n : nat) := + CompletePseudoMetricType 'M[T]_(m, n) mx_complete. + +Canonical fct_completePseudoMetricType (T : choiceType) (R : numFieldType) + (U : completePseudoMetricType R) := + CompletePseudoMetricType (T -> U) fun_complete.