diff --git a/classical_sets.v b/classical_sets.v index 369ec8e826..c0f3f0ed94 100644 --- a/classical_sets.v +++ b/classical_sets.v @@ -350,6 +350,9 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa]. by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di. Qed. +Lemma setMT A B : (@setT A) `*` (@setT B) = setT. +Proof. by rewrite predeqE. Qed. + Definition is_prop {A} (X : set A) := forall x y, X x -> X y -> x = y. Definition is_fun {A B} (f : A -> B -> Prop) := all (is_prop \o f). Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f). diff --git a/derive.v b/derive.v index 76b6701c08..03de1591ec 100644 --- a/derive.v +++ b/derive.v @@ -138,7 +138,7 @@ Proof. by move=> ?; apply: DiffDef. Qed. Section jacobian. -Definition jacobian n m (R : absRingType) (f : 'rV[R]_n.+1 -> 'rV[R]_m.+1) p := +Definition jacobian n m (R : absRingType) (f : 'rV[R]_n -> 'rV[R]_m) p := lin1_mx ('d f p). End jacobian. @@ -280,24 +280,22 @@ apply: flim_map_lim. pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v. pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ). rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: lim_add. - rewrite -(scale1r (_ _ v)); apply: lim_scalel => /= X [e e0]. - rewrite /AbsRing_ball /ball_ /= => eX. - apply/locallyP; rewrite locally_E. - by exists e => //= x _ x0; apply eX; rewrite mulVr // subrr absr0. + rewrite -(scale1r (_ _ v)); apply: lim_scalel. + apply/(@app_flim_locally _ _ [normedModType R of R^o]) => _/posnumP[e]. + by apply/locally_normP; exists e%:num => // x _ x0; rewrite mulVf. rewrite /g2. have [/eqP ->|v0] := boolP (v == 0). rewrite (_ : (fun _ => _) = cst 0); first exact: cst_continuous. by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0. -apply/flim_normP => e e0. -rewrite nearE /=; apply/locallyP; rewrite locally_E. -have /(littleoP [littleo of k]) /locallyP[i i0 Hi] : 0 < e / (2 * `|[v]|). +apply/flim_normP => e e0; rewrite /locally' -filter_from_norm_locally. +have /(littleoP [littleo of k]) /locally_normP [i i0 Hi] : 0 < e / (2 * `|[v]|). by rewrite divr_gt0 // pmulr_rgt0 // normm_gt0. exists (i / `|[v]|); first by rewrite divr_gt0 // normm_gt0. -move=> /= j; rewrite /ball /= /AbsRing_ball /ball_ add0r absrN. +move=> /= j; rewrite /ball add0r normmN. rewrite ltr_pdivl_mulr ?normm_gt0 // => jvi j0. rewrite add0r normmN normmZ -ltr_pdivl_mull ?normr_gt0 ?invr_neq0 //. -have /Hi/ler_lt_trans -> // : ball 0 i (j *: v). - by rewrite -ball_normE /ball_ add0r normmN (ler_lt_trans _ jvi) // normmZ. +have /Hi/ler_lt_trans -> // : ball norm 0 i (j *: v). + by rewrite /ball add0r normmN (ler_lt_trans _ jvi) // normmZ. rewrite -(mulrC e) -mulrA -ltr_pdivl_mull // mulrA mulVr ?unitfE ?gtr_eqF //. rewrite absRE normrV ?unitfE // div1r invrK ltr_pdivr_mull; last first. by rewrite pmulr_rgt0 // normm_gt0. @@ -314,7 +312,7 @@ Hint Extern 0 (derivable _ _ _) => solve[apply: ex_derive] : core. Section DifferentialR2. Implicit Type (V : normedModType R). -Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) : +Lemma derivemxE m n (f : 'rV[R]_m -> 'rV[R]_n) (a v : 'rV[R]_m) : differentiable f a -> 'D_ v f a = v *m jacobian f a. Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed. @@ -365,14 +363,13 @@ rewrite funeqE => x; apply/eqP; case: (ler0P `|[x]|) => [|xn0]. by rewrite normm_le0 => /eqP ->; rewrite linear0. rewrite -normm_le0 -(mul0r `|[x]|) -ler_pdivr_mulr //. apply/ler0_addgt0P => _ /posnumP[e]; rewrite ler_pdivr_mulr //. -have /oid /locallyP [_ /posnumP[d] dfe] := posnum_gt0 e. +have /oid /locally_normP [_/posnumP[d] dfe] := [gt0 of e%:num]. set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1. rewrite -{1}(@scalerKV _ _ k _ x) // linearZZ normmZ. -rewrite -ler_pdivl_mull; last by rewrite absRE gtr0_norm. -rewrite mulrCA (@ler_trans _ (e%:num * `|[k^-1 *: x]|)) //; last first. - by rewrite ler_pmul // normmZ absRE normfV. -apply dfe. -rewrite -ball_normE /ball_ sub0r normmN normmZ. +rewrite -ler_pdivl_mull ?absRE ?gtr0_norm // mulrCA. +rewrite (@ler_trans _ (e%:num * `|[k^-1 *: x]|)) //; last first. + by rewrite ler_pmul // normmZ absRE normfV gtr0_norm. +apply dfe; rewrite /ball sub0r normmN normmZ. rewrite invrK -ltr_pdivl_mulr // absRE ger0_norm // ltr_pdivr_mulr //. by rewrite -mulrA mulVf ?lt0r_neq0 // mulr1 [X in _ < X]splitr ltr_addl. Qed. @@ -597,10 +594,10 @@ apply: DiffDef; first exact/linear_differentiable/scaler_continuous. by rewrite diff_lin //; apply: scaler_continuous. Qed. -Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j : - differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R^o) M. +Lemma differentiable_coord m n (M : 'M[R]_(m, n)) i j : + differentiable (fun N : 'M[R]_(m, n) => N i j : R^o) M. Proof. -have @f : {linear 'M[R]_(m.+1, n.+1) -> R^o}. +have @f : {linear 'M[R]_(m, n) -> R^o}. by exists (fun N : 'M[R]_(_, _) => N i j); eexists; move=> ? ?; rewrite !mxE. rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous. Qed. @@ -609,17 +606,17 @@ 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 => /(_ _ (locally_ball 0 1%:pos)). -move=> /locallyP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. +move=> /locally_normP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. case: (lerP `|[x]| 0) => [|xn0]. by rewrite normm_le0 => /eqP->; rewrite linear0 !normm0 mulr0. set k := 2 / e%:num * (PosNum xn0)%:num. have kn0 : k != 0 by []. have abskgt0 : `|k| > 0 by rewrite normr_gt0. rewrite -[x in X in X <= _](scalerKV kn0) linearZZ normmZ -ler_pdivl_mull //. -suff /he : ball 0 e%:num (k^-1 *: x). - rewrite -ball_normE /= normmB subr0 => /ltrW /ler_trans; apply. +suff /he : ball norm 0 e%:num (k^-1 *: x). + rewrite /ball /= normmB subr0 => /ltrW /ler_trans; apply. by rewrite absRE ger0_norm // mulVf. -rewrite -ball_normE /= normmB subr0 normmZ. +rewrite /ball normmB subr0 normmZ. rewrite absRE normfV ger0_norm // invrM ?unitfE // mulrAC mulVf //. by rewrite invf_div mul1r [X in _ < X]splitr; apply: ltr_spaddr. Qed. @@ -640,17 +637,14 @@ Lemma compoO_eqo (K : absRingType) (U V' W' : normedModType K) (f : U -> V') (g : V' -> W') : [o_ (0 : V') id of g] \o [O_ (0 : U) id of f] =o_ (0 : U) id. 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)) /(_ _) /locallyP [//|_ /posnumP[d] hd]. -apply: filter_app; near=> x => leOxkx; apply: ler_trans (hd _ _) _; last first. - rewrite -ler_pdivl_mull //; apply: ler_trans leOxkx _. - by rewrite invf_div mulrA -[_ / _ * _]mulrA mulVf // mulr1. -rewrite -ball_normE /= normmB subr0 (ler_lt_trans leOxkx) //. -rewrite -ltr_pdivl_mull //; near: x; rewrite /= !locally_simpl. -apply/locallyP; exists (k%:num ^-1 * d%:num)=> // x. -by rewrite -ball_normE /= normmB subr0. +apply/eqoP => _ /posnumP[e]; have [go] := littleo; have [fO k fOid] := bigO. +move=> /(_ (e%:num / k%:num) _) /locally_normP [//|_/posnumP[d] hd]. +apply: filter_app fOid; near=> x => leOxkx; apply: ler_trans (hd _ _) _. + rewrite /= normmB subr0 (ler_lt_trans leOxkx) // -ltr_pdivl_mull //; near: x. + apply/locally_normP; exists (k%:num ^-1 * d%:num) => // x. + by rewrite /= normmB subr0. +rewrite -ler_pdivl_mull //; apply: ler_trans leOxkx _. +by rewrite invf_div mulrA -[_ / _ * _]mulrA mulVf // mulr1. Grab Existential Variables. all: end_near. Qed. Lemma compoO_eqox (K : absRingType) (U V' W' : normedModType K) (f : U -> V') @@ -663,17 +657,13 @@ Lemma compOo_eqo (K : absRingType) (U V' W' : normedModType K) (f : U -> V') (g : V' -> W') : [O_ (0 : V') id of g] \o [o_ (0 : U) id of f] =o_ (0 : U) id. Proof. -apply/eqoP => _ /posnumP[e]. -have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : V') id of g]]. -move=> /locallyP [_ /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: ler_trans (hd _ _) _; last first. +apply/eqoP => _/posnumP[e]; have [gO k /locally_normP[_/posnumP[d] hd]] := bigO. +have [fo /(_ _ [gt0 of e%:num / k%:num])] := littleo; apply: filter_app. +near=> x => leoxekx; apply: ler_trans (hd _ _) _; last first. by rewrite -ler_pdivl_mull // mulrA [_^-1 * _]mulrC. -rewrite -ball_normE /= normmB subr0; apply: ler_lt_trans leoxekx _. -rewrite -ltr_pdivl_mull //; near: x; rewrite /= locally_simpl. -apply/locallyP; exists ((e%:num / k%:num) ^-1 * d%:num)=> // x. -by rewrite -ball_normE /= normmB subr0. +rewrite /ball normmB subr0; apply: ler_lt_trans leoxekx _. +rewrite -ltr_pdivl_mull //; near: x; apply/locally_normP. +by exists ((e%:num / k%:num) ^-1 * d%:num)=> // x; rewrite /ball normmB subr0. Grab Existential Variables. all: end_near. Qed. Lemma compOo_eqox (K : absRingType) (U V' W' : normedModType K) (f : U -> V') @@ -718,26 +708,27 @@ 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 => /(_ _ (locally_ball 0 1%:pos)). -move=> /locallyP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v. +move=> /(_ (0, 0)); rewrite linear0r => /(_ _ (locally_ball 0 1%:pos)). +move=> [[A B] [/locally_normP /= [_/posnumP[eA] sA]]]. +move=> /locally_normP [_/posnumP[eB] sB] sAB. +set e := minr eA%:num eB%:num; exists ((2 / e) ^+2) => // u v. case: (lerP `|[u]| 0) => [|un0]. by rewrite normm_le0 => /eqP->; rewrite linear0l !normm0 mulr0 mul0r. case: (lerP `|[v]| 0) => [|vn0]. by rewrite normm_le0 => /eqP->; rewrite linear0r !normm0 mulr0. rewrite -[`|[u]|]/((PosNum un0)%:num) -[`|[v]|]/((PosNum vn0)%:num). -set ku := 2 / e%:num * (PosNum un0)%:num. -set kv := 2 / e%:num * (PosNum vn0)%:num. -rewrite -[X in f X](@scalerKV _ _ ku) // linearZl_LR normmZ. -rewrite absRE gtr0_norm // -ler_pdivl_mull //. -rewrite -[X in f _ X](@scalerKV _ _ kv) // linearZr_LR normmZ. -rewrite absRE gtr0_norm // -ler_pdivl_mull //. -suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v). - rewrite -ball_normE /= normmB subr0 => /ltrW /ler_trans; apply. - rewrite ler_pdivl_mull // mulr1 ler_pdivl_mull //. - by rewrite mulrA [ku * _]mulrAC expr2. -rewrite -ball_normE /= normmB subr0. +set ku := 2 / e * (PosNum un0)%:num. +set kv := 2 / e * (PosNum vn0)%:num. +rewrite -[X in f X](@scalerKV _ _ ku) // linearZl_LR normmZ absRE gtr0_norm //. +rewrite -ler_pdivl_mull // -[X in f _ X](@scalerKV _ _ kv) // linearZr_LR. +rewrite normmZ absRE gtr0_norm // -ler_pdivl_mull //. +suff : ball norm 0 e (ku^-1 *: u, kv^-1 *: v). + rewrite /ball ltr_maxl !ltr_minr => /andP [/andP[/sA uA _] /andP[_ /sB vB]]. + have /sAB /= := conj uA vB; rewrite normmB subr0 => /ltrW /ler_trans; apply. + by rewrite ler_pdivl_mull// mulr1 ler_pdivl_mull// mulrA [ku * _]mulrAC expr2. +rewrite /ball normmB subr0. have -> : (ku^-1 *: u, kv^-1 *: v) = - (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v). + (e / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v). rewrite invrM ?unitfE // [kv ^-1]invrM ?unitfE //. rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA. by rewrite invf_div. @@ -753,8 +744,8 @@ apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (ler_trans (fschwarz _ _))//. rewrite ler_pmul ?pmulr_rge0 //; last by rewrite ler_maxr orbC lerr. rewrite -ler_pdivl_mull //. suff : `|[x]| <= k%:num ^-1 * e%:num by apply: ler_trans; rewrite ler_maxr lerr. -near: x; rewrite !near_simpl; apply/locally_le_locally_norm. -by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite normmB subr0 => /ltrW. +near: x; apply/locally_normP; exists (k%:num ^-1 * e%:num) => //. +by move=> ? /=; rewrite normmB subr0 => /ltrW. Grab Existential Variables. all: end_near. Qed. Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : @@ -764,9 +755,13 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id. 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)) /= /locallyP [_ /posnumP[e] fpqe_A]; - apply/locallyP; exists e%:num => // r [??]; apply: (fpqe_A (_.1, _.2)). + apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2)); + move=> A /(fc (_.1, _.2)) [PQ [/locally_normP [_/posnumP[eP] sP]]]; + move=> /locally_normP [_/posnumP[eQ] sQ] sPQ /=; apply/locally_normP. + exists eQ%:num => // xy; rewrite /= ltr_maxl => /andP [_ /sQ Qy]. + by apply: (sPQ (_,_)); split=> //=; apply/sP. + exists eP%:num => // xy; rewrite /= ltr_maxl => /andP [/sP Px _]. + by apply: (sPQ (_,_)); split=> //=; apply/sQ. apply/eqaddoE; rewrite funeqE => q /=. rewrite linearDl !linearDr addrA addrC. rewrite -[f q.1 _ + _ + _]addrA [f q.1 _ + _]addrC addrA [f q.1 _ + _]addrC. @@ -897,33 +892,33 @@ rewrite -[X in X + _]mulr1 -[X in 1 / _ * X](@mulfVK _ (x ^+ 2)); last first. by rewrite sqrf_eq0. rewrite mulrA mulf_div mulr1. have hDx_neq0 : h + x != 0. - near: h; rewrite !locally_simpl; apply/locally_normP. - exists `|x|; first by rewrite normr_gt0. + near: h; apply/locally_normP; exists `|x|; first by rewrite normr_gt0. move=> h /=; rewrite normmB subr0 -subr_gt0 => lthx. rewrite -(normm_gt0 (h + x : R^o)) addrC -[h]opprK. apply: ltr_le_trans (ler_distm_dist _ _). by rewrite absRE ger0_norm normmN //; apply: ltrW. rewrite addrC -[X in X * _]mulr1 -{2}[1](@mulfVK _ (h + x)) //. rewrite mulrA expr_div_n expr1n mulf_div mulr1 [_ ^+ 2 * _]mulrC -mulrA. -rewrite -mulrDr mulrBr [1 / _ * _]mulrC [`|[ _ ]|]absRE normrM. +rewrite -mulrDr mulrBr [1 / _ * _]mulrC [`|[_]|]normrM. rewrite mulrDl mulrDl opprD addrACA addrA [x * _]mulrC expr2. do 2 ?[rewrite -addrA [- _ + _]addrC subrr addr0]. rewrite div1r normfV [X in _ / X]normrM invfM [X in _ * X]mulrC. rewrite mulrA mulrAC ler_pdivr_mulr ?normr_gt0 ?mulf_neq0 //. rewrite mulrAC ler_pdivr_mulr ?normr_gt0 //. have : `|h * h| <= `|x / 2| * (e%:num * `|x * x| * `|[h : R^o]|). - rewrite !mulrA; near: h; exists (`|x / 2| * e%:num * `|x * x|). + rewrite !mulrA; near: h; apply/locally_normP. + exists (`|x / 2| * e%:num * `|x * x|). by rewrite !pmulr_rgt0 // normr_gt0 mulf_neq0. - by move=> h /ltrW; rewrite absrB subr0 [`|h * _|]normrM => /ler_pmul; apply. + by move=> h /ltrW; rewrite normmB subr0 [`|h * _|]normrM => /ler_pmul; apply. move=> /ler_trans-> //; rewrite [X in X <= _]mulrC ler_pmul ?mulr_ge0 //. -near: h; exists (`|x| / 2); first by rewrite divr_gt0 ?normr_gt0. -move=> h; rewrite /AbsRing_ball /= absrB subr0 => lthhx; rewrite addrC -[h]opprK. -apply: ler_trans (@ler_distm_dist _ [normedModType R of R^o] _ _). -rewrite absRE normmN [X in _ <= X]ger0_norm; last first. - rewrite subr_ge0; apply: ltrW; apply: ltr_le_trans lthhx _. - by rewrite [`|[_]|]splitr ler_addl; apply: divr_ge0. -rewrite ler_subr_addr -ler_subr_addl (splitr `|[x : R^o]|). -by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltrW. +near: h; apply/locally_normP; exists (`|x| / 2). + by rewrite divr_gt0 ?normr_gt0. +move=> h; rewrite /ball normmB subr0 => lthhx; rewrite addrC -[h]opprK. +apply: ler_trans (ler_dist_dist _ _); rewrite normrN [X in _ <= X]ger0_norm. + rewrite ler_subr_addr -ler_subr_addl (splitr `|x|). + by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltrW. +rewrite subr_ge0; apply: ltrW; apply: ltr_le_trans lthhx _. +by rewrite {2}[`|_|%R]splitr ler_addl; apply: divr_ge0. Grab Existential Variables. all: end_near. Qed. Lemma diff_Rinv (x : R^o) : x != 0 -> @@ -1248,8 +1243,9 @@ move=> fxn0 df. have /derivable1P/derivable1_diffP/differentiable_continuous := df. move=> /continuous_withinNx; rewrite scale0r add0r => fc. have fn0 : locally' (0 : R^o) [set h | f (h *: v + x) != 0]. - apply: (fc [set x | x != 0]); exists `|[f x]|; first by rewrite normm_gt0. - move=> y; rewrite /AbsRing_ball /= => yltfx. + apply: (fc [set x | x != 0]); rewrite /= -filter_from_norm_locally. + exists `|[f x]|; first by rewrite normm_gt0. + move=> y; rewrite /ball => yltfx. by apply/eqP => y0; move: yltfx; rewrite y0 subr0 ltrr. have : (fun h => - ((1 / f x) * (1 / f (h *: v + x))) *: (h^-1 *: (f (h *: v + x) - f x))) @ locally' (0 : R^o) --> @@ -1257,10 +1253,11 @@ have : (fun h => - ((1 / f x) * (1 / f (h *: v + x))) *: apply: flim_comp2 (@lim_mult _ _ _) => //=. apply: (@lim_opp _ [normedModType R of R^o]); rewrite expr2. by apply: lim_scaler; apply: lim_inv. -apply: flim_trans => A [_/posnumP[e] /= Ae]. -move: fn0; apply: filter_app; near=> h => /=. -move=> fhvxn0; have he : AbsRing_ball 0 e%:num h by near: h; exists e%:num. -have hn0 : h != 0 by near: h; exists e%:num. +apply: flim_trans; rewrite [in X in _ --> X]/locally' -filter_from_norm_locally. +move=> A [_/posnumP[e] Ae]; move: fn0; apply: filter_app; near=> h => /= fhvxn0. +have he : ball norm 0 e%:num (h : R^o). + by near: h; apply/locally_normP; exists e%:num. +have hn0 : h != 0 by near: h; apply/locally_normP; exists e%:num. suff <- : - ((1 / f x) * (1 / f (h *: v + x))) *: (h^-1 *: (f (h *: v + x) - f x)) = h^-1 *: (1 / f (h *: v + x) - 1 / f x) by exact: Ae. @@ -1339,25 +1336,24 @@ have /(EVT_max leab) [c clr fcmax] : {in `[a, b], continuous (- f)}. by exists c => // ? /fcmax; rewrite ler_opp2. Qed. -Lemma cvg_at_rightE (V : normedModType R) (f : R -> V) x : +Lemma cvg_at_rightE (V : normedModType R) (f : R^o -> V) x : cvg (f @ locally' x) -> lim (f @ locally' x) = lim (f @ at_right x). Proof. -move=> cvfx; apply/Logic.eq_sym. -(* should be inferred *) -have atrF := at_right_proper_filter x. -apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A]. -by exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _]; apply: xe_A. +move=> cvfx; apply/esym. (* should be inferred *) +have atrF := at_right_proper_filter x; apply: flim_map_lim => A /cvfx. +rewrite /locally' /at_right -filter_from_norm_locally. +move=> [_/posnumP[e] xe_A]; exists e%:num => // y xe_y. +by rewrite ltr_def => /andP[xney _]; apply: xe_A. Qed. -Lemma cvg_at_leftE (V : normedModType R) (f : R -> V) x : +Lemma cvg_at_leftE (V : normedModType R) (f : R^o -> V) x : cvg (f @ locally' x) -> lim (f @ locally' x) = lim (f @ at_left x). Proof. -move=> cvfx; apply/Logic.eq_sym. -(* should be inferred *) -have atrF := at_left_proper_filter x. -apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A]. -exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _]. -by apply: xe_A => //; rewrite eq_sym. +move=> cvfx; apply/esym. (* should be inferred *) +have atrF := at_left_proper_filter x; apply: flim_map_lim => A /cvfx. +rewrite /locally' /at_left -filter_from_norm_locally. +move=> [_ /posnumP[e] xe_A]; exists e%:num => // y xe_y. +by rewrite ltr_def => /andP [xney _]; apply: xe_A => //; rewrite eq_sym. Qed. Lemma le0r_flim_map (T : topologicalType) (F : set (set T)) @@ -1367,7 +1363,7 @@ Proof. move=> fge0 fcv; case: (lerP 0 (lim (f @ F))) => // limlt0; near F => x. have := near fge0 x; rewrite lerNgt => /(_ _) /negbTE<- //; near: x. have normlimgt0 : `|[lim (f @ F)]| > 0 by rewrite normm_gt0 ltr0_neq0. -have /fcv := locally_ball_norm (lim (f @ F)) (PosNum normlimgt0). +have /fcv := locally_ball (lim (f @ F)) (PosNum normlimgt0). rewrite /= !near_simpl; apply: filterS => x. rewrite /= normmB [ `|[_]| ]absRE => /(ler_lt_trans (ler_norm _)). rewrite ltr_subl_addr => /ltr_le_trans; apply. @@ -1411,10 +1407,12 @@ apply/eqP; rewrite eqr_le; apply/andP; split. move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //. exact/lt0r_neq0. near=> h; apply: mulr_ge0_le0. - by rewrite invr_ge0; apply: ltrW; near: h; exists 1. + rewrite invr_ge0; apply: ltrW; near: h. + by apply/(@locally_normP _ [normedModType R of R^o]); exists 1. rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h. + apply/(@locally_normP _ [normedModType R of R^o]). exists (b - c); first by rewrite subr_gt0 (itvP cab). - move=> h; rewrite /AbsRing_ball /= absrB subr0 absRE. + move=> h; rewrite /ball normmB subr0. move=> /(ler_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE => ->. by move=> /ltr_spsaddl -> //; rewrite (itvP cab). rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl. @@ -1424,10 +1422,12 @@ apply: le0r_flim_map; last first. move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //. exact/ltr0_neq0. near=> h; apply: mulr_le0. - by rewrite invr_le0; apply: ltrW; near: h; exists 1. + rewrite invr_le0; apply: ltrW; near: h. + by apply/(@locally_normP _ [normedModType R of R^o]); exists 1. rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h. +apply/(@locally_normP _ [normedModType R of R^o]). exists (c - a); first by rewrite subr_gt0 (itvP cab). -move=> h; rewrite /AbsRing_ball /= absrB subr0 absRE. +move=> h; rewrite /ball normmB subr0. move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE => -> _. by move=> /ltr_snsaddl -> //; rewrite (itvP cab). Grab Existential Variables. all: end_near. Qed. diff --git a/misc/uniform_bigO.v b/misc/uniform_bigO.v index 5da5479d77..f3e43a3000 100644 --- a/misc/uniform_bigO.v +++ b/misc/uniform_bigO.v @@ -86,23 +86,21 @@ move=> /OuP_to_ex [_/posnumP[a] [_/posnumP[C] fOg]]. apply/eqOP; near=> k; near=> x; apply: ler_trans (fOg _ _ _ _) _; last 2 first. - by near: x; exists (setT, P); [split=> //=; apply: withinT|move=> ? []]. - by rewrite ler_pmul => //; near: k; exists C%:num => ? /ltrW. -- near: x; exists (setT, ball (0 : R^o * R^o) a%:num). - by split=> //=; rewrite /within; near=> x =>_; near: x; apply: locally_ball. - move=> x [_ [/=]]; rewrite -ball_normE /= normmB subr0 normmB subr0. - by move=> ??; rewrite ltr_maxl; apply/andP. +- near: x; exists (setT, ball norm (0 : R^o * R^o) a%:num); last first. + by move=> x [_ /=]; rewrite normmB subr0. + split=> //=; rewrite /within; near=> x =>_; near: x. + exact: (@locally_ball _ [normedModType R of R^o * R^o]). Grab Existential Variables. all: end_near. Qed. Lemma OuO_to_P f g : OuO f g -> OuP f g. Proof. move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k hk]. have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite ltr_maxr ltr_addl orbC ltr01. -move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg. -exists (minr e1%:num e2%:num) => //. -exists (maxr 1 (k + 1)); first by rewrite ltr_maxr ltr01. +rewrite /= -(@filter_from_norm_locally _ [normedModType R of R^o * R^o]). +move=> -[_/posnumP[e] seQ] fOg; exists e%:num => //; exists (maxr 1 (k + 1)). + by rewrite ltr_maxr ltr01. move=> x dx dxe Pdx; apply: (fOg (x, dx)); split=> //=. -move: dxe; rewrite ltr_maxl !ltr_minr => /andP[/andP [dxe11 _] /andP [_ dxe22]]. -by apply/sRQ => //; split; [apply/Re1|apply/Re2]; - rewrite /AbsRing_ball /= absrB subr0. +by apply: seQ => //; rewrite /ball normmB subr0. Qed. End UniformBigO. \ No newline at end of file diff --git a/normedtype.v b/normedtype.v index a4517fcfcd..5ded220a3d 100644 --- a/normedtype.v +++ b/normedtype.v @@ -21,22 +21,21 @@ Require Import classical_sets posnum topology. (* [absRingType of T] == clone of a canonical absRingType *) (* structure on T. *) (* `|x| == the absolute value of x. *) -(* ball_ N == balls defined by the norm/absolute value *) +(* ball N == balls defined by the norm/absolute value *) (* N. *) -(* locally_dist == neighbourhoods defined by a "distance" *) -(* function *) +(* entourage_ N == entourages defined by the norm/absolute *) +(* value N. *) (* *) (* * Normed modules : *) (* normedModType K == interface type for a normed module *) (* structure over the ring with absolute *) (* value K. *) -(* NormedModMixin normD normZ balln normeq0 == builds the mixin for a *) -(* normed module from the algebraic *) -(* properties of the norm and the *) -(* compatibility between the norm and *) -(* balls; the carrier type must have a *) -(* lmodType K structure for K an *) -(* absRingType. *) +(* NormedModMixin normD normZ entn normeq0 == builds the mixin for a normed *) +(* module from the algebraic properties of *) +(* the norm and the compatibility between *) +(* the norm and entourages; the carrier *) +(* type must have a lmodType K structure *) +(* for K an absRingType. *) (* NormedModType K T m == packs the mixin m to build a *) (* normedModType K; T must have canonical *) (* lmodType K and uniformType structures. *) @@ -45,8 +44,6 @@ Require Import classical_sets posnum topology. (* [normedModType K of T] == clone of a canonical normedModType K *) (* structure on T. *) (* `|[x]| == the norm of x. *) -(* ball_norm == balls defined by the norm. *) -(* locally_norm == neighbourhoods defined by the norm. *) (* bounded == set of bounded sets. *) (* *) (* * Complete normed modules : *) @@ -221,86 +218,68 @@ End AbsRing1. Hint Resolve absr_ge0 : core. Hint Resolve absr1_gt0 : core. -Definition ball_ (V : zmodType) (norm : V -> R) (x : V) +Definition ball (V : zmodType) (norm : V -> R) (x : V) (e : R) := [set y | norm (x - y) < e]. -Arguments ball_ {V} norm x e%R y /. +Arguments ball {V} norm x e%R y /. -Section AbsRing_UniformSpace. +Definition entourage_ (V : zmodType) (norm : V -> R) := + filter_from [set e : R | e > 0] (fun e => [set xy | norm (xy.1 - xy.2) < e]). -Context {K : absRingType}. - -Definition AbsRing_ball := ball_ (@abs K). - -Lemma AbsRing_ball_center (x : K) (e : R) : 0 < e -> AbsRing_ball x e x. -Proof. by rewrite /AbsRing_ball /= subrr absr0. Qed. - -Lemma AbsRing_ball_sym (x y : K) (e : R) : - AbsRing_ball x e y -> AbsRing_ball y e x. -Proof. by rewrite /AbsRing_ball /= absrB. Qed. +Section NormedUniformity. -(* :TODO: to math-comp *) -Lemma subr_trans (M : zmodType) (z x y : M) : x - y = (x - z) + (z - y). -Proof. by rewrite addrA addrNK. Qed. +Variable (V : zmodType) (norm : V -> R). +Hypothesis (norm0 : norm 0 = 0). +Hypothesis (normB : forall x y, norm (x - y) = norm (y - x)). +Hypothesis (ler_dist_add : forall z x y, + norm (x - y) <= norm (x - z) + norm (z - y)). -Lemma AbsRing_ball_triangle (x y z : K) (e1 e2 : R) : - AbsRing_ball x e1 y -> AbsRing_ball y e2 z -> AbsRing_ball x (e1 + e2) z. -Proof. -rewrite /AbsRing_ball /= => xy yz. -by rewrite (subr_trans y) (ler_lt_trans (ler_abs_add _ _)) ?ltr_add. +Program Definition uniformityOfNormMixin := + @Uniform.Mixin V (locally_ (entourage_ norm)) (entourage_ norm) _ _ _ _ _. +Next Obligation. +apply: filter_from_filter; first by exists 1. +move=> _ _ /posnumP[e1] /posnumP[e2]; exists (minr e1%:num e2%:num) => // xy. +by rewrite ltr_minr => /andP. +Qed. +Next Obligation. +by case: H => _/posnumP[e] sA xy xey; apply: sA; rewrite xey subrr norm0. +Qed. +Next Obligation. +case: H => _/posnumP[e] sA; exists e%:num => // xy; rewrite normB => xey. +exact: sA. +Qed. +Next Obligation. +case: H => _/posnumP[e] sA; exists [set xy | norm (xy.1 - xy.2) < e%:num / 2]. + by exists (e%:num / 2). +move=> xz [y /= xy yz]; apply: sA; apply: ler_lt_trans (ler_dist_add y _ _) _. +by rewrite [e%:num]splitr ltr_add. Qed. -Definition AbsRingUniformMixin := - UniformMixin AbsRing_ball_center AbsRing_ball_sym AbsRing_ball_triangle erefl. - -End AbsRing_UniformSpace. +End NormedUniformity. (* :TODO: DANGEROUS ! Must change this to include uniform type et al inside absring *) Coercion absRing_pointedType (K : absRingType) := PointedType K 0. Canonical absRing_pointedType. Coercion absRing_filteredType (K : absRingType) := - FilteredType K K (locally_ AbsRing_ball). + FilteredType K K (locally_ (entourage_ abs)). Canonical absRing_filteredType. -Coercion absRing_topologicalType (K : absRingType) := - TopologicalType K (topologyOfBallMixin AbsRingUniformMixin). -Canonical absRing_topologicalType. -Coercion absRing_UniformType (K : absRingType) := UniformType K AbsRingUniformMixin. -Canonical absRing_UniformType. -Lemma ball_absE (K : absRingType) : ball = ball_ (@abs K). -Proof. by []. Qed. +(* :TODO: to math-comp *) +Lemma subr_trans (M : zmodType) (z x y : M) : x - y = (x - z) + (z - y). +Proof. by rewrite addrA addrNK. Qed. -Lemma locallyN (R : absRingType) (x : R) : - locally (- x) = [set [set - y | y in A] | A in locally x]. -Proof. -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 /AbsRing_ball /ball_ opprK -absrN -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 /AbsRing_ball /ball_ absrB opprK addrC. -Qed. +Lemma ler_dist_abs_add (K : absRingType) (z x y : K) : + `|x - y| <= `|x - z|%real + `|z - y|%real. +Proof. by rewrite (subr_trans z) ler_abs_add. Qed. -Lemma openN (R : absRingType) (A : set R) : - open A -> open [set - x | x in A]. -Proof. -move=> Aop; rewrite openE => _ [x /Aop x_A <-]. -by rewrite /interior locallyN; exists A. -Qed. +Definition AbsRingUniformMixin (K : absRingType) := + uniformityOfNormMixin absr0 absrB (@ler_dist_abs_add K). -Lemma closedN (R : absRingType) (A : set R) : - closed A -> closed [set - x | x in A]. -Proof. -move=> Acl x clNAx. -suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK. -move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0. - by apply: clNAx; rewrite -[x]opprK locallyN; exists B. -move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). -by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. -Qed. +Coercion absRing_topologicalType (K : absRingType) := + TopologicalType K (topologyOfEntourageMixin (AbsRingUniformMixin K)). +Canonical absRing_topologicalType. +Coercion absRing_UniformType (K : absRingType) := + UniformType K (AbsRingUniformMixin K). +Canonical absRing_UniformType. (** real numbers *) @@ -318,200 +297,18 @@ Canonical Ro_filteredType := [filteredType R^o of R^o for R_absRingType]. Canonical Ro_topologicalType := [topologicalType of R^o for R_absRingType]. Canonical Ro_uniformType := [uniformType of R^o for R_absRingType]. -(** locally *) - -Section Locally. -Context {T : uniformType}. - -Lemma forallN {U} (P : set U) : (forall x, ~ P x) = ~ exists x, P x. -Proof. (*boolP*) -rewrite propeqE; split; first by move=> fP [x /fP]. -by move=> nexP x Px; apply: nexP; exists x. -Qed. - -Lemma eqNNP (P : Prop) : (~ ~ P) = P. (*boolP*) -Proof. by rewrite propeqE; split=> [/contrapT|?]. Qed. - -Lemma existsN {U} (P : set U) : (exists x, ~ P x) = ~ forall x, P x. (*boolP*) -Proof. -rewrite propeqE; split=> [[x Px] Nall|Nall]; first exact: Px. -by apply: contrapT; rewrite -forallN => allP; apply: Nall => x; apply: contrapT. -Qed. - -Lemma ex_ball_sig (x : T) (P : set T) : - ~ (forall eps : posreal, ~ (ball x eps%:num `<=` ~` P)) -> - {d : posreal | ball x d%:num `<=` ~` P}. -Proof. -rewrite forallN eqNNP => exNP. -pose D := [set d : R | d > 0 /\ ball x d `<=` ~` P]. -have [|d_gt0] := @getPex _ D; last by exists (PosNum d_gt0). -by move: exNP => [e eP]; exists e%:num. -Qed. - -Lemma locallyC (x : T) (P : set T) : - ~ (forall eps : posreal, ~ (ball x eps%:num `<=` ~` P)) -> - locally x (~` P). -Proof. by move=> /ex_ball_sig [e] ?; apply/locallyP; exists e%:num. Qed. - -Lemma locallyC_ball (x : T) (P : set T) : - locally x (~` P) -> {d : posreal | ball x d%:num `<=` ~` P}. -Proof. -move=> /locallyP xNP; apply: ex_ball_sig. -by have [_ /posnumP[e] eP /(_ _ eP)] := xNP. -Qed. - -Lemma locally_ex (x : T) (P : T -> Prop) : locally x P -> - {d : posreal | forall y, ball x d%:num y -> P y}. -Proof. -move=> /locallyP 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). -Qed. - -End Locally. - -Lemma ler_addgt0Pr (R : realFieldType) (x y : R) : - reflect (forall e, e > 0 -> x <= y + e) (x <= y). -Proof. -apply/(iffP idP)=> [lexy _/posnumP[e] | lexye]; first by rewrite ler_paddr. -case: (lerP x y) => // ltyx. -have /midf_lt [_] := ltyx; rewrite ltrNge -eqbF_neg => /eqP<-. -suff -> : (y + x) / 2 = y + (x - y) / 2. - by apply/lexye/divr_gt0 => //; rewrite subr_gt0. -by rewrite !mulrDl addrC -mulN1r -mulrA mulN1r [RHS]addrC {3}(splitr y) - [RHS]GRing.subrKA. -Qed. - -Lemma ler_addgt0Pl (R : realFieldType) (x y : R) : - reflect (forall e, e > 0 -> x <= e + y) (x <= y). -Proof. -by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. -Qed. - -Lemma in_segment_addgt0Pr (R : realFieldType) (x y z : R) : - reflect (forall e, e > 0 -> y \in `[(x - e), (z + e)]) (y \in `[x, z]). -Proof. -apply/(iffP idP)=> [xyz _/posnumP[e] | xyz_e]. - rewrite inE; apply/andP; split; last by rewrite ler_paddr // (itvP xyz). - by rewrite ler_subl_addr ler_paddr // (itvP xyz). -rewrite inE; apply/andP. -by split; apply/ler_addgt0Pr => ? /xyz_e /andP []; rewrite ler_subl_addr. -Qed. - -Lemma in_segment_addgt0Pl (R : realFieldType) (x y z : R) : - reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). -Proof. -apply/(equivP (in_segment_addgt0Pr x y z)). -by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. -Qed. - -Lemma absRE (x : R) : `|x|%real = `|x|%R. -Proof. by []. Qed. - -Lemma Rhausdorff : hausdorff [topologicalType of R]. -Proof. -move=> x y clxy. -apply/eqP; rewrite eqr_le; apply/in_segment_addgt0Pr => _ /posnumP[e]. -rewrite inE -ler_distl -absRE; set he := (e%:num / 2)%:pos. -have [z []] := clxy _ _ (locally_ball x he) (locally_ball y he). -rewrite ball_absE /ball_ absrB => zx_he yz_he. -rewrite (subr_trans z) (ler_trans (ler_abs_add _ _) _)// ltrW//. -by rewrite (splitr e%:num); apply: ltr_add. -Qed. - -Lemma coord_continuous {K : absRingType} m n i j : - continuous (fun M : 'M[K]_(m.+1, n.+1) => M i j). -Proof. -move=> /= M s /= /locallyP; rewrite locally_E => -[e e0 es]. -apply/locallyP; rewrite locally_E; exists e => //= N MN; exact/es/MN. -Qed. - -(** * Some Topology on [Rbar] *) - -(* NB: already defined in R_scope in Rbar.v *) - -Notation "'+oo'" := p_infty : real_scope. -Notation "'-oo'" := m_infty : real_scope. -Definition Rbar_locally' (a : Rbar) (P : R -> Prop) := - match a with - | Finite a => locally' a P - | +oo => exists M : R, forall x, M < x -> P x - | -oo => exists M : R, forall x, x < M -> P x - end. -Definition Rbar_locally (a : Rbar) (P : R -> Prop) := - match a with - | Finite a => locally a P - | +oo => exists M : R, forall x, M < x -> P x - | -oo => exists M : R, forall x, x < M -> P x - end. - -Canonical Rbar_choiceType := ChoiceType Rbar gen_choiceMixin. -Canonical Rbar_pointed := PointedType Rbar (+oo). -Canonical Rbar_filter := FilteredType R Rbar (Rbar_locally). - -Global Instance Rlocally'_proper (x : R) : ProperFilter (locally' x). -Proof. -apply: Build_ProperFilter => A [_/posnumP[e] Ae]. -exists (x + e%:num / 2); apply: Ae; last first. - by rewrite eq_sym addrC -subr_eq subrr eq_sym. -rewrite /AbsRing_ball /= opprD addrA subrr absrB subr0 absRE ger0_norm //. -by rewrite {2}(splitr e%:num) ltr_spaddl. -Qed. - -Global Instance Rbar_locally'_filter : forall x, ProperFilter (Rbar_locally' x). -Proof. -case=> [x||]; first exact: Rlocally'_proper. - apply Build_ProperFilter. - by move=> P [M gtMP]; exists (M + 1); apply: gtMP; rewrite ltr_addl. - split=> /= [|P Q [MP gtMP] [MQ gtMQ] |P Q sPQ [M gtMP]]; first by exists 0. - by exists (maxr MP MQ) => ?; rewrite ltr_maxl => /andP [/gtMP ? /gtMQ]. - by exists M => ? /gtMP /sPQ. -apply Build_ProperFilter. - by move=> P [M ltMP]; exists (M - 1); apply: ltMP; rewrite gtr_addl oppr_lt0. -split=> /= [|P Q [MP ltMP] [MQ ltMQ] |P Q sPQ [M ltMP]]; first by exists 0. - by exists (minr MP MQ) => ?; rewrite ltr_minr => /andP [/ltMP ? /ltMQ]. -by exists M => ? /ltMP /sPQ. -Qed. -Typeclasses Opaque Rbar_locally'. - - -Global Instance Rbar_locally_filter : forall x, ProperFilter (Rbar_locally x). -Proof. -case=> [x||]. -by apply/locally_filter. -exact: (Rbar_locally'_filter +oo). -exact: (Rbar_locally'_filter -oo). -Qed. -Typeclasses Opaque Rbar_locally. - -Lemma near_pinfty_div2 (A : set R) : - (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)). -Proof. -by move=> [M AM]; exists (M * 2) => x; rewrite -ltr_pdivl_mulr //; apply: AM. -Qed. - -Lemma locally_pinfty_gt c : \forall x \near +oo, c < x. -Proof. by exists c. Qed. - -Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x. -Proof. by exists c; apply: ltrW. Qed. - -Hint Extern 0 (is_true (0 < _)) => match goal with - H : ?x \is_near (locally +oo) |- _ => - solve[near: x; exists 0 => _/posnumP[x] //] end : core. - (** ** Modules with a norm *) Reserved Notation "`|[ x ]|" (at level 0, x at level 99, format "`|[ x ]|"). Module NormedModule. -Record mixin_of (K : absRingType) (V : lmodType K) loc (m : @Uniform.mixin_of V loc) := Mixin { +Record mixin_of (K : absRingType) (V : lmodType K) loc + (m : @Uniform.mixin_of V loc) := Mixin { norm : V -> R ; ax1 : forall (x y : V), norm (x + y) <= norm x + norm y ; - ax2 : forall (l : K) (x : V), norm (l *: x) = abs l * norm x; - ax3 : Uniform.ball m = ball_ norm; + ax2 : forall (l : K) (x : V), norm (l *: x) = `|l|%real * norm x; + ax3 : Uniform.entourage m = entourage_ norm; ax4 : forall x : V, norm x = 0 -> x = 0 }. @@ -610,6 +407,17 @@ Definition norm {K : absRingType} {V : normedModType K} : V -> R := NormedModule.norm (NormedModule.class _). Notation "`|[ x ]|" := (norm x) : ring_scope. +(** Rings with absolute values are normed modules *) + +Lemma entourage_absE (K : absRingType) : entourage = entourage_ (@abs K). +Proof. by []. Qed. + +Definition AbsRing_NormedModMixin (K : absRingType) := + @NormedModule.Mixin K _ _ _ (abs : K^o -> R) ler_abs_add absrM + (entourage_absE K) absr0_eq0. +Canonical AbsRing_NormedModType (K : absRingType) := + NormedModType K K^o (AbsRing_NormedModMixin _). + Section NormedModule1. Context {K : absRingType} {V : normedModType K}. Implicit Types (l : K) (x y : V) (eps : posreal). @@ -620,11 +428,11 @@ Proof. exact: NormedModule.ax1. Qed. Lemma normmZ l x : `|[l *: x]| = `|l|%real * `|[x]|. Proof. exact: NormedModule.ax2. Qed. -Notation ball_norm := (ball_ (@norm K V)). +Notation entourage_norm := (entourage_ (@norm K V)). -Notation locally_norm := (locally_ ball_norm). +Notation locally_norm := (locally_ entourage_norm). -Lemma ball_normE : ball_norm = ball. +Lemma entourage_normE : entourage_norm = entourage. Proof. by rewrite -NormedModule.ax3. Qed. Lemma normm0_eq0 x : `|[x]| = 0 -> x = 0. @@ -646,308 +454,840 @@ apply/eqP; rewrite eqr_le; apply/andP; split. by rewrite -{1}(scale0r 0) normmZ absr0 mul0r. by rewrite -(ler_add2r `|[0 : V]|) add0r -{1}[0 : V]add0r ler_normm_add. Qed. -Hint Resolve normm0 : core. - -Lemma normm_eq0 x : (`|[x]| == 0) = (x == 0). -Proof. by apply/eqP/eqP=> [/normm0_eq0|->//]. Qed. +Hint Resolve normm0. + +Lemma normm_eq0 x : (`|[x]| == 0) = (x == 0). +Proof. by apply/eqP/eqP=> [/normm0_eq0|->//]. Qed. + +Lemma normm_ge0 x : 0 <= `|[x]|. +Proof. +rewrite -(@pmulr_rge0 _ 2) // mulr2n mulrDl !mul1r. +by rewrite -{2}normmN (ler_trans _ (ler_normm_add _ _)) // subrr normm0. +Qed. + +Lemma normm_gt0 x : (0 < `|[x]|) = (x != 0). +Proof. by rewrite ltr_def normm_eq0 normm_ge0 andbT. Qed. + +Lemma normm_lt0 x : (`|[x]| < 0) = false. +Proof. by rewrite ltrNge normm_ge0. Qed. + +Lemma normm_le0 x : (`|[x]| <= 0) = (x == 0). +Proof. by rewrite lerNgt normm_gt0 negbK. Qed. + +Lemma absRE (x : R) : `|x|%real = `|x|%R. +Proof. by []. Qed. + +Lemma ler_distm_dist x y : `| `|[x]| - `|[y]| | <= `|[x - y]|. +Proof. +wlog gt_xy : x y / `|[x]| >= `|[y]| => [hw|]. + by have [/hw//|/ltrW/hw] := lerP `|[y]| `|[x]|; rewrite absRE distrC normmB. +rewrite absRE ger0_norm ?subr_ge0 // ler_subl_addr. +by rewrite -{1}[x](addrNK y) ler_normm_add. +Qed. + +Lemma entourage_ball (e : posreal) : + entourage [set xy : V * V | `|[xy.1 - xy.2]| < e%:num]. +Proof. by rewrite -entourage_normE; apply: in_filter_from. Qed. +Hint Resolve entourage_ball. + +Lemma distm_lt_split z x y (e : R) : + `|[x - z]| < (e / 2)%R -> `|[z - y]| < (e / 2)%R -> `|[x - y]| < e. +Proof. +move=> xz zy; rewrite -(subrK z x) -addrA (ler_lt_trans (ler_normm_add _ _)) //. +by rewrite [e]splitr ltr_add. +Qed. + +Lemma distm_lt_splitr z x y (e : R) : + `|[z - x]| < (e / 2)%R -> `|[z - y]| < (e / 2)%R -> `|[x - y]| < e. +Proof. by rewrite normmB; apply: distm_lt_split. Qed. + +Lemma distm_lt_splitl z x y (e : R) : + `|[x - z]| < (e / 2)%R -> `|[y - z]| < (e / 2)%R -> `|[x - y]| < e. +Proof. by rewrite (normmB y); apply: distm_lt_split. Qed. + +Lemma normm_leW x (e : R) : e > 0 -> `|[x]| <= (e / 2)%R -> `|[x]| < e. +Proof. +move=> /posnumP[{e}e] /ler_lt_trans ->//. +by rewrite [X in _ < X]splitr ltr_spaddl. +Qed. + +Lemma normm_lt_split x y (e : R) : + `|[x]| < (e / 2)%R -> `|[y]| < (e / 2)%R -> `|[x + y]| < e. +Proof. +by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. +Qed. + +Lemma closeE x y : close x y = (x = y). +Proof. +rewrite propeqE; split => [cl_xy|->//]; have [//|neq_xy] := eqVneq x y. +have dxy_gt0 : `|[x - y]| > 0 by rewrite normm_gt0 subr_eq0. +have dxy_ge0 := ltrW dxy_gt0. +have /cl_xy /= := (entourage_ball ((PosNum dxy_gt0)%:num / 2)%:pos). +rewrite -subr_lt0 ler_gtF // -[X in X - _]mulr1 -mulrBr mulr_ge0 //. +by rewrite subr_ge0 -(@ler_pmul2r _ 2) // mulVf // mul1r ler1n. +Qed. +Lemma eq_close x y : close x y -> x = y. by rewrite closeE. Qed. + +Lemma locally_le_locally_norm x : flim (locally x) (locally_norm x). +Proof. +move=> P [A entA sAB]; apply/locallyP; exists A => //. +by rewrite -entourage_normE. +Qed. + +Lemma locally_norm_le_locally x : flim (locally_norm x) (locally x). +Proof. +by move=> P /locallyP [A entA sAP]; exists A => //; rewrite entourage_normE. +Qed. + +(* NB: this lemmas was not here before *) +Lemma locally_locally_norm : locally_norm = locally. +Proof. +by rewrite funeqE => x; rewrite /locally_norm entourage_normE + filter_from_entourageE. +Qed. + +Lemma filter_from_norm_locally x : + @filter_from R _ [set x : R | 0 < x] (ball norm x) = locally x. +Proof. +rewrite predeqE => A; split=> [[_/posnumP[e] sxeA] |]. + by rewrite -locally_entourageE; exists [set xy | `|[xy.1 - xy.2]| < e%:num]. +rewrite -locally_locally_norm => - [B [_/posnumP[e] seB] sBA]. +by exists e%:num => // y xye; apply/sBA/seB. +Qed. + +Lemma locally_normP x P : + locally x P <-> @filter_from R _ [set x : R | 0 < x] (ball norm x) P. +Proof. by rewrite filter_from_norm_locally. Qed. + +Lemma locally_normE (x : V) (P : set V) : + locally_norm x P = \near x, P x. +Proof. by rewrite locally_locally_norm near_simpl. Qed. + +Lemma filter_from_normE (x : V) (P : set V) : + @filter_from R _ [set x : R | 0 < x] (ball norm x) P = \near x, P x. +Proof. by rewrite filter_from_norm_locally. Qed. + +Lemma near_locally_norm (x : V) (P : set V) : + (\forall x \near locally_norm x, P x) = \near x, P x. +Proof. exact: locally_normE. Qed. + +Lemma locally_norm_ball x (e : posreal) : + locally_norm x (ball norm x e%:num). +Proof. +by rewrite locally_locally_norm -filter_from_norm_locally; exists e%:num. +Qed. + +Lemma locally_ball (x : V) (e : posreal) : locally x (ball norm x e%:num). +Proof. rewrite -locally_locally_norm; apply: locally_norm_ball. Qed. + +Lemma ball_triangle (x y z : V) (e1 e2 : R) : + ball norm x e1 y -> ball norm y e2 z -> ball norm x (e1 + e2) z. +Proof. +rewrite /ball => H1 H2; rewrite (subr_trans y). +by rewrite (ler_lt_trans (ler_normm_add _ _)) ?ltr_add. +Qed. + +Lemma ball_center (x : V) (e : posreal) : ball norm x e%:num x. +Proof. by rewrite /ball subrr normm0. Qed. + +Lemma ball_dec x y (e : R) : {ball norm x e y} + {~ ball norm x e y}. +Proof. exact: pselect. Qed. + +Lemma ball_sym x y (e : R) : ball norm x e y -> ball norm y e x. +Proof. by rewrite /ball -opprB normmN. Qed. + +Lemma ball_norm_le x (e1 e2 : R) : + e1 <= e2 -> ball norm x e1 `<=` ball norm x e2. +Proof. by move=> e1e2 y /ltr_le_trans; apply. Qed. + +Lemma norm_close x y : + close x y = (forall e : posreal, ball norm x e%:num y). +Proof. +rewrite propeqE; split; first by move=> xy e; have /xy := entourage_ball e. +by move=> xy A; rewrite -entourage_normE => - [_/posnumP[e]]; apply; apply: xy. +Qed. + +Lemma ball_norm_eq x y : (forall eps : posreal, ball norm x eps%:num y) -> x = y. +Proof. by rewrite -norm_close closeE. Qed. + +Lemma flim_unique {F} {FF : ProperFilter F} : + is_prop [set x : V | F --> x]. +Proof. by move=> Fx Fy; rewrite -closeE; apply: flim_close. Qed. + +Lemma locally_flim_unique (x y : V) : x --> y -> x = y. +Proof. by rewrite -closeE; apply: flim_close. Qed. + +Lemma lim_id (x : V) : lim x = x. +Proof. by symmetry; apply: locally_flim_unique; apply/cvg_ex; exists x. Qed. + +Lemma flim_lim {F} {FF : ProperFilter F} (l : V) : + F --> l -> lim F = l. +Proof. by move=> Fl; have Fcv := cvgP Fl; apply: flim_unique. Qed. + +Lemma flim_map_lim {T : Type} {F} {FF : ProperFilter F} (f : T -> V) (l : V) : + f @ F --> l -> lim (f @ F) = l. +Proof. exact: flim_lim. Qed. + +End NormedModule1. + +Hint Resolve normm_ge0. +Hint Resolve entourage_ball. +Hint Resolve ball_center. + +Module Export LocallyNorm. +Definition locally_simpl := (locally_simpl,@locally_locally_norm,@filter_from_norm_locally). +End LocallyNorm. + +Module Export NearNorm. +Definition near_simpl := (@near_simpl, @locally_normE, + @filter_from_normE, @near_locally_norm). +Ltac near_simpl := rewrite ?near_simpl. +End NearNorm. + +Lemma locallyN (R : absRingType) (x : R) : + locally (- x) = [set [set - y | y in A] | A in locally x]. +Proof. +rewrite predeqE -!(@filter_from_norm_locally _ [normedModType R of R^o]) => A. +split=> [[e egt0 oppxe_A] | [B [e egt0 xe_B] <-]]; last first. + exists e => // y xe_y; exists (- y); last by rewrite opprK. + by apply/xe_B; rewrite /ball opprK -normmN -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 normmB opprK addrC. +Qed. + +Lemma openN (R : absRingType) (A : set R) : + open A -> open [set - x | x in A]. +Proof. +move=> Aop; rewrite openE => _ [x /Aop x_A <-]. +by rewrite /interior locallyN; exists A. +Qed. + +Lemma closedN (R : absRingType) (A : set R) : + closed A -> closed [set - x | x in A]. +Proof. +move=> Acl x clNAx. +suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK. +move=> B oppx_B; have : [set - x | x in A] `&` [set - x | x in B] !=set0. + by apply: clNAx; rewrite -[x]opprK locallyN; exists B. +move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). +by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. +Qed. + +Section NormedModule2. + +Context {T : Type} {K : absRingType} {V : normedModType K}. + +Lemma flimi_unique {F} {FF : ProperFilter F} (f : T -> set V) : + {near F, is_fun f} -> is_prop [set x : V | f `@ F --> x]. +Proof. by move=> ffun fx fy; rewrite -closeE; apply: flimi_close. Qed. + +Lemma flim_normP {F : set (set V)} {FF : Filter F} (y : V) : + F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, `|[y - y']| < eps. +Proof. by rewrite -filter_fromP /= !locally_simpl. Qed. + +Lemma flim_normW {F : set (set V)} {FF : Filter F} (y : V) : + (forall eps : R, 0 < eps -> \forall y' \near F, `|[y - y']| <= eps) -> + F --> y. +Proof. +move=> cv; apply/flim_normP => _/posnumP[e]; near=> x. +by apply: normm_leW => //; near: x; apply: cv. +Grab Existential Variables. all: end_near. Qed. + +Lemma flim_norm {F : set (set V)} {FF : Filter F} (y : V) : + F --> y -> forall eps, eps > 0 -> \forall y' \near F, `|[y - y']| < eps. +Proof. by move=> /flim_normP. Qed. + +Lemma flimi_map_lim {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) : + F (fun x : T => is_prop (f x)) -> + f `@ F --> l -> lim (f `@ F) = l. +Proof. +move=> f_prop f_l; apply: get_unique => // l' f_l'. +exact: flimi_unique _ f_l' f_l. +Qed. + +End NormedModule2. +Arguments flim_norm {_ _ F FF}. + +Lemma continuous_flim_norm {K : absRingType} (V W : normedModType K) (f : V -> W) x l : + continuous f -> x --> l -> forall e : posreal, `|[f l - f x]| < e. +Proof. +move=> cf xl e. +have /flim_norm /(_ _ [gt0 of e%:num]) /locally_normP [_/posnumP[d]] := (cf l). +apply; have /flim_norm /(_ _ [gt0 of d%:num]) := xl. +by move=> /locally_normP [_/posnumP[d']]; apply. +Qed. + +Section Locally. + +Context {K : absRingType} {V : normedModType K}. + +Lemma forallN {U} (P : set U) : (forall x, ~ P x) = ~ exists x, P x. +Proof. (*boolP*) +rewrite propeqE; split; first by move=> fP [x /fP]. +by move=> nexP x Px; apply: nexP; exists x. +Qed. + +Lemma eqNNP (P : Prop) : (~ ~ P) = P. (*boolP*) +Proof. by rewrite propeqE; split=> [/contrapT|?]. Qed. + +Lemma existsN {U} (P : set U) : (exists x, ~ P x) = ~ forall x, P x. (*boolP*) +Proof. +rewrite propeqE; split=> [[x Px] Nall|Nall]; first exact: Px. +by apply: contrapT; rewrite -forallN => allP; apply: Nall => x; apply: contrapT. +Qed. + +Lemma ex_ball_sig (x : V) (P : set V) : + ~ (forall eps : posreal, ~ (ball norm x eps%:num `<=` ~` P)) -> + {d : posreal | ball norm x d%:num `<=` ~` P}. +Proof. +rewrite forallN eqNNP => exNP. +pose D := [set d : R | d > 0 /\ ball norm x d `<=` ~` P]. +have [|d_gt0] := @getPex _ D; last by exists (PosNum d_gt0). +by move: exNP => [e eP]; exists e%:num. +Qed. + +Lemma locallyC (x : V) (P : set V) : + ~ (forall eps : posreal, ~ (ball norm x eps%:num `<=` ~` P)) -> + locally x (~` P). +Proof. by move=> /ex_ball_sig [e] ?; apply/locally_normP; exists e%:num. Qed. + +Lemma locallyC_ball (x : V) (P : set V) : + locally x (~` P) -> {d : posreal | ball norm x d%:num `<=` ~` P}. +Proof. +move=> /locally_normP xNP; apply: ex_ball_sig. +by have [_ /posnumP[e] eP /(_ _ eP)] := xNP. +Qed. + +Lemma locally_ex (x : V) (P : V -> Prop) : locally x P -> + {d : posreal | forall y, ball norm x d%:num y -> P y}. +Proof. +move=> /locally_normP xP. +pose D := [set d : R | d > 0 /\ forall y, ball norm x d y -> P y]. +have [|d_gt0 dP] := @getPex _ D; last by exists (PosNum d_gt0). +by move: xP => [e bP]; exists e. +Qed. + +End Locally. + +Lemma unif_contP (K K' : absRingType) (V : normedModType K) + (V' : normedModType K') (f : V -> V') : + unif_cont f <-> + forall e, e > 0 -> exists2 d, d > 0 & + forall x, ball norm x.1 d x.2 -> ball norm (f x.1) e (f x.2). +Proof. +have fappF : Filter ((fun xy => (f xy.1, f xy.2)) @ entourage_ norm). + by rewrite entourage_normE; apply: filtermap_filter. +by rewrite /unif_cont -!entourage_normE filter_fromP. +Qed. + +Section Locally_fct. + +Context {T : Type} {K : absRingType} {V : normedModType K}. + +Lemma near_ball (y : V) (eps : posreal) : + \forall y' \near y, ball norm y eps%:num y'. +Proof. exact: locally_ball. Qed. + +Lemma flim_ballP {F} {FF : Filter F} (y : V) : + F --> y <-> forall eps, 0 < eps -> \forall y' \near F, ball norm y eps y'. +Proof. exact: flim_normP. Qed. +Definition flim_locally := @flim_ballP. + +Lemma flim_ballPpos {F} {FF : Filter F} (y : V) : + F --> y <-> + forall eps : posreal, \forall y' \near F, ball norm y eps%:num y'. +Proof. +by split => [/flim_ballP|] pos; [case|apply/flim_ballP=> _/posnumP[eps] //]. +Qed. + +Lemma flim_ball {F} {FF : Filter F} (y : V) : + F --> y -> forall eps, 0 < eps -> \forall y' \near F, ball norm y eps y'. +Proof. by move/flim_ballP. Qed. + +Lemma app_flim_locally {F} {FF : Filter F} (f : T -> V) y : + f @ F --> y <-> + forall eps, 0 < eps -> \forall x \near F, ball norm y eps (f x). +Proof. exact: flim_ballP. Qed. + +Lemma flimi_ballP {F} {FF : Filter F} (f : T -> V -> Prop) y : + f `@ F --> y <-> + forall eps, 0 < eps -> + \forall x \near F, exists z, f x z /\ ball norm y eps z. +Proof. +split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/locally_ball. +move=> /locally_normP[_ /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. +Unshelve. all: end_near. Qed. +Definition flimi_locally := @flimi_ballP. + +Lemma flimi_ball {F} {FF : Filter F} (f : T -> V -> Prop) y : + f `@ F --> y -> + forall eps, 0 < eps -> F [set x | exists z, f x z /\ ball norm y eps z]. +Proof. by move/flimi_ballP. Qed. + +End Locally_fct. + +Lemma ler_addgt0Pr (R : realFieldType) (x y : R) : + reflect (forall e, e > 0 -> x <= y + e) (x <= y). +Proof. +apply/(iffP idP)=> [lexy _/posnumP[e] | lexye]; first by rewrite ler_paddr. +case: (lerP x y) => // ltyx. +have /midf_lt [_] := ltyx; rewrite ltrNge -eqbF_neg => /eqP<-. +suff -> : (y + x) / 2 = y + (x - y) / 2. + by apply/lexye/divr_gt0 => //; rewrite subr_gt0. +by rewrite !mulrDl addrC -mulN1r -mulrA mulN1r [RHS]addrC {3}(splitr y) + [RHS]GRing.subrKA. +Qed. + +Lemma ler_addgt0Pl (R : realFieldType) (x y : R) : + reflect (forall e, e > 0 -> x <= e + y) (x <= y). +Proof. +by apply/(equivP (ler_addgt0Pr x y)); split=> lexy e /lexy; rewrite addrC. +Qed. + +Lemma in_segment_addgt0Pr (R : realFieldType) (x y z : R) : + reflect (forall e, e > 0 -> y \in `[(x - e), (z + e)]) (y \in `[x, z]). +Proof. +apply/(iffP idP)=> [xyz _/posnumP[e] | xyz_e]. + rewrite inE; apply/andP; split; last by rewrite ler_paddr // (itvP xyz). + by rewrite ler_subl_addr ler_paddr // (itvP xyz). +rewrite inE; apply/andP. +by split; apply/ler_addgt0Pr => ? /xyz_e /andP []; rewrite ler_subl_addr. +Qed. + +Lemma in_segment_addgt0Pl (R : realFieldType) (x y z : R) : + reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]). +Proof. +apply/(equivP (in_segment_addgt0Pr x y z)). +by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC. +Qed. + +Lemma Rhausdorff : hausdorff [topologicalType of R]. +Proof. +move=> x y clxy. +apply/eqP; rewrite eqr_le; apply/in_segment_addgt0Pr => _ /posnumP[e]. +rewrite inE -ler_distl; set he := (e%:num / 2)%:pos. +have [z []] := clxy _ _ (locally_ball (x : R^o) he) (locally_ball (y : R^o) he). +rewrite /ball normmB => zx yz; apply: ler_trans (ler_dist_add z _ _) _. +by rewrite ltrW // [e%:num]splitr ltr_add. +Qed. + +Lemma normedModType_hausdorff (K : absRingType) (V : normedModType K) : + hausdorff V. +Proof. +move=> p q clp_q; apply/subr0_eq/normm0_eq0/Rhausdorff => A B pq_A. +rewrite -(@normm0 _ V) -(subrr p) => pp_B. +suff loc_preim r C : + locally `|[p - r]| C -> locally r ((fun r => `|[p - r]|) @^-1` C). + have [r []] := clp_q _ _ (loc_preim _ _ pp_B) (loc_preim _ _ pq_A). + by exists `|[p - r]|. +move=> /(@locally_normP _ [normedModType R of R^o]) [_/posnumP[e] sC]. +apply/locally_normP; exists e%:num=> // s re_s; apply/sC. +apply: ler_lt_trans (ler_distm_dist _ _) _. +by rewrite opprB addrC -subr_trans normmB. +Qed. + +(** * Some Topology on [Rbar] *) + +(* NB: already defined in R_scope in Rbar.v *) + +Notation "'+oo'" := p_infty : real_scope. +Notation "'-oo'" := m_infty : real_scope. +Definition Rbar_locally' (a : Rbar) (P : R -> Prop) := + match a with + | Finite a => locally' a P + | +oo => exists M : R, forall x, M < x -> P x + | -oo => exists M : R, forall x, x < M -> P x + end. +Definition Rbar_locally (a : Rbar) (P : R -> Prop) := + match a with + | Finite a => locally a P + | +oo => exists M : R, forall x, M < x -> P x + | -oo => exists M : R, forall x, x < M -> P x + end. + +Canonical Rbar_choiceType := ChoiceType Rbar gen_choiceMixin. +Canonical Rbar_pointed := PointedType Rbar (+oo). +Canonical Rbar_filter := FilteredType R Rbar (Rbar_locally). + +Global Instance Rlocally'_proper (x : R^o) : ProperFilter (locally' x). +Proof. +apply: Build_ProperFilter => A; rewrite /locally' -filter_from_norm_locally. +move=> [_/posnumP[e] sA]; exists (x + e%:num / 2); apply: sA; last first. + by rewrite eq_sym addrC -subr_eq subrr eq_sym. +rewrite /= opprD addrA subrr sub0r normmN [ `|[_]| ]ger0_norm //. +by rewrite {2}(splitr e%:num) ltr_spaddl. +Qed. + +Global Instance Rbar_locally'_filter : forall x, ProperFilter (Rbar_locally' x). +Proof. +case=> [x||]; first exact: Rlocally'_proper. + apply Build_ProperFilter. + by move=> P [M gtMP]; exists (M + 1); apply: gtMP; rewrite ltr_addl. + split=> /= [|P Q [MP gtMP] [MQ gtMQ] |P Q sPQ [M gtMP]]; first by exists 0. + by exists (maxr MP MQ) => ?; rewrite ltr_maxl => /andP [/gtMP ? /gtMQ]. + by exists M => ? /gtMP /sPQ. +apply Build_ProperFilter. + by move=> P [M ltMP]; exists (M - 1); apply: ltMP; rewrite gtr_addl oppr_lt0. +split=> /= [|P Q [MP ltMP] [MQ ltMQ] |P Q sPQ [M ltMP]]; first by exists 0. + by exists (minr MP MQ) => ?; rewrite ltr_minr => /andP [/ltMP ? /ltMQ]. +by exists M => ? /ltMP /sPQ. +Qed. +Typeclasses Opaque Rbar_locally'. + +Global Instance Rbar_locally_filter : forall x, ProperFilter (Rbar_locally x). +Proof. +case=> [x||]. +by apply/locally_filter. +exact: (Rbar_locally'_filter +oo). +exact: (Rbar_locally'_filter -oo). +Qed. +Typeclasses Opaque Rbar_locally. -Lemma normm_ge0 x : 0 <= `|[x]|. +Lemma near_pinfty_div2 (A : set R) : + (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)). Proof. -rewrite -(@pmulr_rge0 _ 2) // mulr2n mulrDl !mul1r. -by rewrite -{2}normmN (ler_trans _ (ler_normm_add _ _)) // subrr normm0. +by move=> [M AM]; exists (M * 2) => x; rewrite -ltr_pdivl_mulr //; apply: AM. Qed. -Lemma normm_gt0 x : (0 < `|[x]|) = (x != 0). -Proof. by rewrite ltr_def normm_eq0 normm_ge0 andbT. Qed. +Lemma locally_pinfty_gt c : \forall x \near +oo, c < x. +Proof. by exists c. Qed. -Lemma normm_lt0 x : (`|[x]| < 0) = false. -Proof. by rewrite ltrNge normm_ge0. Qed. +Lemma locally_pinfty_ge c : \forall x \near +oo, c <= x. +Proof. by exists c; apply: ltrW. Qed. -Lemma normm_le0 x : (`|[x]| <= 0) = (x == 0). -Proof. by rewrite lerNgt normm_gt0 negbK. Qed. +Hint Extern 0 (is_true (0 < _)) => match goal with + H : ?x \is_near (locally +oo) |- _ => + solve[near: x; exists 0 => _/posnumP[x] //] end : core. -Lemma ler_distm_dist x y : `| `|[x]| - `|[y]| | <= `|[x - y]|. +Lemma flim_bounded (K : absRingType) (V : normedModType K) {F : set (set V)} + {FF : Filter F} (y : V) : + F --> y -> \forall M \near +oo, \forall y' \near F, `|[y']|%real < M. Proof. -wlog gt_xy : x y / `|[x]| >= `|[y]| => [hw|]. - by have [/hw//|/ltrW/hw] := lerP `|[y]| `|[x]|; rewrite absRE distrC normmB. -rewrite absRE ger0_norm ?subr_ge0 // ler_subl_addr. -by rewrite -{1}[x](addrNK y) ler_normm_add. +move=> /flim_norm Fy; exists `|[y]| => M. +rewrite -subr_gt0 => subM_gt0; have := Fy _ subM_gt0. +apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|[y]|)). +rewrite (ler_lt_trans _ yy') //. +by rewrite (ler_trans _ (ler_distm_dist _ _)) // absRE distrC ler_norm. Qed. +Arguments flim_bounded {_ _ F FF}. -Lemma distm_lt_split z x y (e : R) : - `|[x - z]| < (e / 2)%R -> `|[z - y]| < (e / 2)%R -> `|[x - y]| < e. -Proof. by have := @ball_split _ z x y e; rewrite -ball_normE. Qed. - -Lemma distm_lt_splitr z x y (e : R) : - `|[z - x]| < (e / 2)%R -> `|[z - y]| < (e / 2)%R -> `|[x - y]| < e. -Proof. by have := @ball_splitr _ z x y e; rewrite -ball_normE. Qed. +Section Bigmaxr. -Lemma distm_lt_splitl z x y (e : R) : - `|[x - z]| < (e / 2)%R -> `|[y - z]| < (e / 2)%R -> `|[x - y]| < e. -Proof. by have := @ball_splitl _ z x y e; rewrite -ball_normE. Qed. +Variable (R : realDomainType). -Lemma normm_leW x (e : R) : e > 0 -> `|[x]| <= (e / 2)%R -> `|[x]| < e. +Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> R) x : + \big[maxr/x]_(i <- r | P i) F i = + \big[maxr/x]_(i <- r) (if P i then F i else x). Proof. -move=> /posnumP[{e}e] /ler_lt_trans ->//. -by rewrite [X in _ < X]splitr ltr_spaddl. +rewrite unlock; elim: r x => //= i r ihr x. +case P; rewrite ihr // maxr_r //; elim: r {ihr} => //= j r ihr. +by rewrite ler_maxr ihr orbT. Qed. -Lemma normm_lt_split x y (e : R) : - `|[x]| < (e / 2)%R -> `|[y]| < (e / 2)%R -> `|[x + y]| < e. +Lemma bigminr_maxr I r (P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. Proof. -by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. +by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. Qed. -Lemma closeE x y : close x y = (x = y). +Lemma bigminr_mkcond I r (P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = + \big[minr/x]_(i <- r) (if P i then F i else x). Proof. -rewrite propeqE; split => [cl_xy|->//]; have [//|neq_xy] := eqVneq x y. -have dxy_gt0 : `|[x - y]| > 0 by rewrite normm_gt0 subr_eq0. -have dxy_ge0 := ltrW dxy_gt0. -have := cl_xy ((PosNum dxy_gt0)%:num / 2)%:pos. -rewrite -ball_normE /= -subr_lt0 ler_gtF //. -rewrite -[X in X - _]mulr1 -mulrBr mulr_ge0 //. -by rewrite subr_ge0 -(@ler_pmul2r _ 2) // mulVf // mul1r ler1n. +rewrite !bigminr_maxr bigmaxr_mkcond; congr (- _). +by apply: eq_bigr => i _; case P. Qed. -Lemma eq_close x y : close x y -> x = y. by rewrite closeE. Qed. -Lemma locally_le_locally_norm x : flim (locally x) (locally_norm x). +Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> R) x : + \big[maxr/x]_(i <- r | P i) (maxr (F1 i) (F2 i)) = + maxr (\big[maxr/x]_(i <- r | P i) F1 i) (\big[maxr/x]_(i <- r | P i) F2 i). Proof. -move=> P [_ /posnumP[e] subP]; apply/locallyP. -by eexists; last (move=> y Py; apply/subP; rewrite ball_normE; apply/Py). +by elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?maxrr // maxrCA -!maxrA maxrCA. Qed. -Lemma locally_norm_le_locally x : flim (locally_norm x) (locally x). +Lemma bigminr_split I r (P : pred I) (F1 F2 : I -> R) x : + \big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) = + minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i). Proof. -move=> P /locallyP [_ /posnumP[e] Pxe]. -by exists e%:num => // y; rewrite ball_normE; apply/Pxe. +rewrite !bigminr_maxr -oppr_max -bigmaxr_split; congr (- _). +by apply: eq_bigr => i _; rewrite oppr_min. Qed. -(* NB: this lemmas was not here before *) -Lemma locally_locally_norm : locally_norm = locally. +Lemma filter_andb I r (a P : pred I) : + [seq i <- r | P i && a i] = [seq i <- [seq j <- r | P j] | a i]. +Proof. by elim: r => //= i r ->; case P. Qed. + +Lemma bigmaxr_idl I r (P : pred I) (F : I -> R) x : + \big[maxr/x]_(i <- r | P i) F i = maxr x (\big[maxr/x]_(i <- r | P i) F i). Proof. -by rewrite funeqE => x; rewrite /locally_norm ball_normE filter_from_ballE. +rewrite -big_filter; elim: [seq i <- r | P i] => [|i l ihl]. + by rewrite big_nil maxrr. +by rewrite big_cons maxrCA -ihl. Qed. -Lemma locally_normP x P : locally x P <-> locally_norm x P. -Proof. by rewrite locally_locally_norm. Qed. - -Lemma filter_from_norm_locally x : - @filter_from R _ [set x : R | 0 < x] (ball_norm x) = locally x. -Proof. by rewrite -locally_locally_norm. Qed. - -Lemma locally_normE (x : V) (P : set V) : - locally_norm x P = \near x, P x. -Proof. by rewrite locally_locally_norm near_simpl. Qed. - -Lemma filter_from_normE (x : V) (P : set V) : - @filter_from R _ [set x : R | 0 < x] (ball_norm x) P = \near x, P x. -Proof. by rewrite filter_from_norm_locally. Qed. +Lemma bigminr_idl I r (P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i). +Proof. by rewrite !bigminr_maxr {1}bigmaxr_idl oppr_max opprK. Qed. -Lemma near_locally_norm (x : V) (P : set V) : - (\forall x \near locally_norm x, P x) = \near x, P x. -Proof. exact: locally_normE. Qed. - -Lemma locally_norm_ball_norm x (e : posreal) : - locally_norm x (ball_norm x e%:num). -Proof. by exists e%:num. Qed. - -Lemma locally_norm_ball x (eps : posreal) : locally_norm x (ball x eps%:num). -Proof. rewrite locally_locally_norm; by apply: locally_ball. Qed. - -Lemma locally_ball_norm (x : V) (eps : posreal) : locally x (ball_norm x eps%:num). -Proof. rewrite -locally_locally_norm; apply: locally_norm_ball_norm. Qed. - -Lemma ball_norm_triangle (x y z : V) (e1 e2 : R) : - ball_norm x e1 y -> ball_norm y e2 z -> ball_norm x (e1 + e2) z. +Lemma bigmaxrID I r (a P : pred I) (F : I -> R) x : + \big[maxr/x]_(i <- r | P i) F i = + maxr (\big[maxr/x]_(i <- r | P i && a i) F i) + (\big[maxr/x]_(i <- r | P i && ~~ a i) F i). Proof. -rewrite /ball_norm => H1 H2; rewrite (subr_trans y). -by rewrite (ler_lt_trans (ler_normm_add _ _)) ?ltr_add. +rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter. +rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split. +have eqmax : forall i, P i -> + maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x. + by move=> i _; case: (a i) => //=; rewrite maxrC. +rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P). +elim: [seq j <- r | P j] => [|j l ihl]; first by rewrite !big_nil. +by rewrite !big_cons -maxrA -bigmaxr_idl ihl. Qed. -Lemma ball_norm_center (x : V) (e : posreal) : ball_norm x e%:num x. -Proof. by rewrite /ball_norm subrr normm0. Qed. +Lemma bigminrID I r (a P : pred I) (F : I -> R) x : + \big[minr/x]_(i <- r | P i) F i = + minr (\big[minr/x]_(i <- r | P i && a i) F i) + (\big[minr/x]_(i <- r | P i && ~~ a i) F i). +Proof. by rewrite !bigminr_maxr -oppr_max -bigmaxrID. Qed. -Lemma ball_norm_dec x y (e : R) : {ball_norm x e y} + {~ ball_norm x e y}. -Proof. exact: pselect. Qed. - -Lemma ball_norm_sym x y (e : R) : ball_norm x e y -> ball_norm y e x. -Proof. by rewrite /ball_norm -opprB normmN. Qed. - -Lemma ball_norm_le x (e1 e2 : R) : - e1 <= e2 -> ball_norm x e1 `<=` ball_norm x e2. -Proof. by move=> e1e2 y /ltr_le_trans; apply. Qed. - -Lemma norm_close x y : close x y = (forall eps : posreal, ball_norm x eps%:num y). -Proof. by rewrite propeqE ball_normE. Qed. +Lemma bigmaxr_seq1 I (i : I) (F : I -> R) x : + \big[maxr/x]_(j <- [:: i]) F j = maxr (F i) x. +Proof. by rewrite unlock /=. Qed. -Lemma ball_norm_eq x y : (forall eps : posreal, ball_norm x eps%:num y) -> x = y. -Proof. by rewrite -norm_close closeE. Qed. +Lemma bigminr_seq1 I (i : I) (F : I -> R) x : + \big[minr/x]_(j <- [:: i]) F j = minr (F i) x. +Proof. by rewrite unlock /=. Qed. -Lemma flim_unique {F} {FF : ProperFilter F} : - is_prop [set x : V | F --> x]. -Proof. by move=> Fx Fy; rewrite -closeE; apply: flim_close. Qed. +Lemma bigmaxr_pred1_eq (I : finType) (i : I) (F : I -> R) x : + \big[maxr/x]_(j | j == i) F j = maxr (F i) x. +Proof. by rewrite -big_filter filter_index_enum enum1 bigmaxr_seq1. Qed. -Lemma locally_flim_unique (x y : V) : x --> y -> x = y. -Proof. by rewrite -closeE; apply: flim_close. Qed. +Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I -> R) x : + \big[minr/x]_(j | j == i) F j = minr (F i) x. +Proof. by rewrite bigminr_maxr bigmaxr_pred1_eq oppr_max !opprK. Qed. -Lemma lim_id (x : V) : lim x = x. -Proof. by symmetry; apply: locally_flim_unique; apply/cvg_ex; exists x. Qed. +Lemma bigmaxr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : + P =1 pred1 i -> \big[maxr/x]_(j | P j) F j = maxr (F i) x. +Proof. by move/(eq_bigl _ _)->; apply: bigmaxr_pred1_eq. Qed. -Lemma flim_lim {F} {FF : ProperFilter F} (l : V) : - F --> l -> lim F = l. -Proof. by move=> Fl; have Fcv := cvgP Fl; apply: flim_unique. Qed. +Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : + P =1 pred1 i -> \big[minr/x]_(j | P j) F j = minr (F i) x. +Proof. by move/(eq_bigl _ _)->; apply: bigminr_pred1_eq. Qed. -Lemma flim_map_lim {T : Type} {F} {FF : ProperFilter F} (f : T -> V) (l : V) : - f @ F --> l -> lim (f @ F) = l. -Proof. exact: flim_lim. Qed. +Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> R) x : + P j -> \big[maxr/x]_(i | P i) F i + = maxr (F j) (\big[maxr/x]_(i | P i && (i != j)) F i). +Proof. +move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxrA. +by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->. +Qed. -Lemma normedModType_hausdorff : hausdorff V. +Lemma bigminrD1 (I : finType) j (P : pred I) (F : I -> R) x : + P j -> \big[minr/x]_(i | P i) F i + = minr (F j) (\big[minr/x]_(i | P i && (i != j)) F i). Proof. -move=> p q clp_q; apply/subr0_eq/normm0_eq0/Rhausdorff => A B pq_A. -rewrite -normm0 -(subrr p) => pp_B. -suff loc_preim r C : - locally `|[p - r]| C -> locally r ((fun r => `|[p - r]|) @^-1` C). - have [r []] := clp_q _ _ (loc_preim _ _ pp_B) (loc_preim _ _ pq_A). - by exists `|[p - r]|. -move=> [e egt0 pre_C]; apply: locally_le_locally_norm; exists e => // s re_s. -apply: pre_C; apply: ler_lt_trans (ler_distm_dist _ _) _. -by rewrite opprB addrC -subr_trans normmB. +by move=> Pj; rewrite !bigminr_maxr (bigmaxrD1 _ _ Pj) oppr_max opprK. Qed. -End NormedModule1. +Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> R) x i0 : + P i0 -> F i0 <= \big[maxr/x]_(i | P i) F i. +Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) ler_maxr lerr. Qed. -Module Export LocallyNorm. -Definition locally_simpl := (locally_simpl,@locally_locally_norm,@filter_from_norm_locally). -End LocallyNorm. +Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I -> R) x i0 : + P i0 -> \big[minr/x]_(i | P i) F i <= F i0. +Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) ler_minl lerr. Qed. -Module Export NearNorm. -Definition near_simpl := (@near_simpl, @locally_normE, - @filter_from_normE, @near_locally_norm). -Ltac near_simpl := rewrite ?near_simpl. -End NearNorm. +Lemma ler_bigmaxr (I : finType) (F : I -> R) (i0 : I) x : + F i0 <= \big[maxr/x]_i F i. +Proof. exact: ler_bigmaxr_cond. Qed. -Section NormedModule2. +Lemma bigminr_ler (I : finType) (F : I -> R) (i0 : I) x : + \big[minr/x]_i F i <= F i0. +Proof. exact: bigminr_ler_cond. Qed. -Context {T : Type} {K : absRingType} {V : normedModType K}. +Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (x <= m /\ forall i, P i -> F i <= m) + (\big[maxr/x]_(i | P i) F i <= m). +Proof. +apply: (iffP idP) => [|[lexm leFm]]; last first. + by elim/big_ind: _ => // ??; rewrite ler_maxl =>->. +rewrite bigmaxr_idl ler_maxl => /andP[-> leFm]; split=> // i Pi. +by apply: ler_trans leFm; apply: ler_bigmaxr_cond. +Qed. -Lemma flimi_unique {F} {FF : ProperFilter F} (f : T -> set V) : - {near F, is_fun f} -> is_prop [set x : V | f `@ F --> x]. -Proof. by move=> ffun fx fy; rewrite -closeE; apply: flimi_close. Qed. +Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (m <= x /\ forall i, P i -> m <= F i) + (m <= \big[minr/x]_(i | P i) F i). +Proof. +rewrite bigminr_maxr ler_oppr; apply: (iffP idP). + by move=> /bigmaxr_lerP [? lemF]; split=> [|??]; rewrite -ler_opp2 ?lemF. +by move=> [? lemF]; apply/bigmaxr_lerP; split=> [|??]; rewrite ler_opp2 ?lemF. +Qed. -Lemma flim_normP {F : set (set V)} {FF : Filter F} (y : V) : - F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, `|[y - y']| < eps. -Proof. by rewrite -filter_fromP /= !locally_simpl. Qed. +Lemma bigmaxr_sup (I : finType) i0 (P : pred I) m (F : I -> R) x : + P i0 -> m <= F i0 -> m <= \big[maxr/x]_(i | P i) F i. +Proof. by move=> Pi0 ?; apply: ler_trans (ler_bigmaxr_cond _ _ Pi0). Qed. -Lemma flim_normW {F : set (set V)} {FF : Filter F} (y : V) : - (forall eps : R, 0 < eps -> \forall y' \near F, `|[y - y']| <= eps) -> - F --> y. +Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I -> R) x : + P i0 -> F i0 <= m -> \big[minr/x]_(i | P i) F i <= m. +Proof. by move=> Pi0 ?; apply: ler_trans (bigminr_ler_cond _ _ Pi0) _. Qed. + +Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (x < m /\ forall i, P i -> F i < m) + (\big[maxr/x]_(i | P i) F i < m). Proof. -move=> cv; apply/flim_normP => _/posnumP[e]; near=> x. -by apply: normm_leW => //; near: x; apply: cv. -Grab Existential Variables. all: end_near. Qed. +apply: (iffP idP) => [|[ltxm ltFm]]; last first. + by elim/big_ind: _ => // ??; rewrite ltr_maxl =>->. +rewrite bigmaxr_idl ltr_maxl => /andP[-> ltFm]; split=> // i Pi. +by apply: ler_lt_trans ltFm; apply: ler_bigmaxr_cond. +Qed. -Lemma flim_norm {F : set (set V)} {FF : Filter F} (y : V) : - F --> y -> forall eps, eps > 0 -> \forall y' \near F, `|[y - y']| < eps. -Proof. by move=> /flim_normP. Qed. +Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (m < x /\ forall i, P i -> m < F i) + (m < \big[minr/x]_(i | P i) F i). +Proof. +rewrite bigminr_maxr ltr_oppr; apply: (iffP idP). + by move=> /bigmaxr_ltrP [? ltmF]; split=> [|??]; rewrite -ltr_opp2 ?ltmF. +by move=> [? ltmF]; apply/bigmaxr_ltrP; split=> [|??]; rewrite ltr_opp2 ?ltmF. +Qed. -Lemma flim_bounded {F : set (set V)} {FF : Filter F} (y : V) : - F --> y -> \forall M \near +oo, \forall y' \near F, `|[y']|%real < M. +Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (m <= x \/ exists2 i, P i & m <= F i) + (m <= \big[maxr/x]_(i | P i) F i). Proof. -move=> /flim_norm Fy; exists `|[y]| => M. -rewrite -subr_gt0 => subM_gt0; have := Fy _ subM_gt0. -apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|[y]|)). -rewrite (ler_lt_trans _ yy') //. -by rewrite (ler_trans _ (ler_distm_dist _ _)) // absRE distrC ler_norm. +apply: (iffP idP) => [|[lemx|[i Pi lemFi]]]; last 2 first. +- by rewrite bigmaxr_idl ler_maxr lemx. +- by rewrite (bigmaxrD1 _ _ Pi) ler_maxr lemFi. +rewrite lerNgt => /bigmaxr_ltrP /asboolPn. +rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. + by rewrite -lerNgt; left. +by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -lerNgt; right; exists i. Qed. -Lemma flimi_map_lim {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) : - F (fun x : T => is_prop (f x)) -> - f `@ F --> l -> lim (f `@ F) = l. +Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (x <= m \/ exists2 i, P i & F i <= m) + (\big[minr/x]_(i | P i) F i <= m). Proof. -move=> f_prop f_l; apply: get_unique => // l' f_l'. -exact: flimi_unique _ f_l' f_l. +rewrite bigminr_maxr ler_oppl; apply: (iffP idP). + by move=> /bigmaxr_gerP [?|[i ??]]; [left|right; exists i => //]; + rewrite -ler_opp2. +by move=> [?|[i ??]]; apply/bigmaxr_gerP; [left|right; exists i => //]; + rewrite ler_opp2. Qed. -End NormedModule2. -Hint Resolve normm_ge0 : core. -Arguments flim_norm {_ _ F FF}. -Arguments flim_bounded {_ _ F FF}. +Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (m < x \/ exists2 i, P i & m < F i) + (m < \big[maxr/x]_(i | P i) F i). +Proof. +apply: (iffP idP) => [|[ltmx|[i Pi ltmFi]]]; last 2 first. +- by rewrite bigmaxr_idl ltr_maxr ltmx. +- by rewrite (bigmaxrD1 _ _ Pi) ltr_maxr ltmFi. +rewrite ltrNge => /bigmaxr_lerP /asboolPn. +rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. + by rewrite -ltrNge; left. +by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -ltrNge; right; exists i. +Qed. -Lemma continuous_flim_norm {K : absRingType} (V W : normedModType K) (f : V -> W) x l : - continuous f -> x --> l -> forall e : posreal, `|[f l - f x]| < e. +Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : + reflect (x < m \/ exists2 i, P i & F i < m) + (\big[minr/x]_(i | P i) F i < m). Proof. -move=> cf xl e. -move/flim_norm: (cf l) => /(_ _ (posnum_gt0 e)). -rewrite nearE /= => /locallyP; rewrite locally_E => -[i i0]; apply. -have /@flim_norm : Filter [filter of x] by apply: filter_on_Filter. -move/(_ _ xl _ i0). -rewrite nearE /= => /locallyP; rewrite locally_E => -[j j0]. -move/(_ _ (ballxx _ j0)); by rewrite -ball_normE. +rewrite bigminr_maxr ltr_oppl; apply: (iffP idP). + by move=> /bigmaxr_gtrP [?|[i ??]]; [left|right; exists i => //]; + rewrite -ltr_opp2. +by move=> [?|[i ??]]; apply/bigmaxr_gtrP; [left|right; exists i => //]; + rewrite ltr_opp2. Qed. +End Bigmaxr. + +Arguments bigmaxr_mkcond {R I r}. +Arguments bigmaxrID {R I r}. +Arguments bigmaxr_pred1 {R I} i {P F}. +Arguments bigmaxrD1 {R I} j {P F}. +Arguments ler_bigmaxr_cond {R I P F}. +Arguments ler_bigmaxr {R I F}. +Arguments bigmaxr_sup {R I} i0 {P m F}. +Arguments bigminr_mkcond {R I r}. +Arguments bigminrID {R I r}. +Arguments bigminr_pred1 {R I} i {P F}. +Arguments bigminrD1 {R I} j {P F}. +Arguments bigminr_ler_cond {R I P F}. +Arguments bigminr_ler {R I F}. +Arguments bigminr_inf {R I} i0 {P m F}. + (** ** Matrices *) Section matrix_normedMod. Variables (K : absRingType) (m n : nat). -(* take m.+1, n.+1 because ball_normE is not provable for m = 0 or n = 0 *) -Definition mx_norm (x : 'M[K]_(m.+1, n.+1)) := - bigmaxr 0 [seq `|x ij.1 ij.2| | ij : 'I_m.+1 * 'I_n.+1]. +Definition mx_norm (x : 'M[K]_(m, n)) := \big[maxr/0]_ij `|x ij.1 ij.2|. Program Definition matrix_NormedModMixin := @NormedModMixin _ _ - (@locally _ [filteredType 'M[K]_(m.+1, n.+1) of 'M[K]_(m.+1, n.+1)]) + (@locally _ [filteredType 'M[K]_(m, n) of 'M[K]_(m, n)]) (Uniform.mixin (Uniform.class _)) mx_norm _ _ _ _. Next Obligation. -apply/bigmaxr_lerP=> [|i]; rewrite size_map -cardT mxvec_cast // => ltimn. -rewrite (nth_map (ord0, ord0)); last by rewrite -cardT mxvec_cast. -rewrite mxE; apply: ler_trans (ler_abs_add _ _) _. -do 2 ?[rewrite -(nth_map _ 0 (fun p => `|_ p.1 p.2|)) -?cardT ?mxvec_cast //]. -by apply: ler_add; apply: bigmaxr_ler; rewrite size_map -cardT mxvec_cast. +apply/bigmaxr_lerP; split. + by apply: addr_ge0; apply/bigmaxr_gerP; left. +move=> ij _; rewrite mxE; apply: ler_trans (ler_abs_add _ _) _. +apply: ler_add; apply: ler_bigmaxr. Qed. Next Obligation. -apply/bigmaxrP; split=> [|i]. - have : (0 < size [seq `|x ij.1 ij.2|%real | ij : 'I_m.+1 * 'I_n.+1])%N. - by rewrite size_map -cardT mxvec_cast. - move=> /bigmaxr_mem - /(_ 0) /mapP [ij ijP normx]; rewrite [mx_norm _]normx. - by apply/mapP; exists ij => //; rewrite mxE absrM. -rewrite size_map -cardT mxvec_cast // => ltimn. -rewrite (nth_map (ord0, ord0)); last by rewrite -cardT mxvec_cast. -rewrite mxE absrM ler_pmul // -(nth_map _ 0 (fun p => `|x p.1 p.2|)). - by apply: bigmaxr_ler; rewrite size_map -cardT mxvec_cast. -by rewrite -cardT mxvec_cast. +apply/eqP; rewrite eqr_le; apply/andP; split. + apply/bigmaxr_lerP; split. + by apply: mulr_ge0 => //; apply/bigmaxr_gerP; left. + by move=> ij _; rewrite mxE absrM ler_wpmul2l //; apply: ler_bigmaxr. +case: (ler0P `|l|%real) => l0. + have : `|l| == 0 by rewrite eqr_le l0 absr_ge0. + rewrite absr_eq0 => /eqP->; rewrite scale0r absr0 mul0r; apply/bigmaxr_gerP. + by left. +rewrite -ler_pdivl_mull //; apply/bigmaxr_lerP; split. + by apply: mulr_ge0; rewrite ?invr_ge0 //; apply/bigmaxr_gerP; left. +by move=> ij _; rewrite ler_pdivl_mull // -absrM (bigmaxr_sup ij) // mxE. Qed. Next Obligation. -rewrite predeq3E => x e y; split. - move=> xe_y; apply/bigmaxr_ltrP; rewrite size_map -cardT mxvec_cast //. - move=> i iltmn; rewrite (nth_map (ord0, ord0)). - by rewrite !mxE; apply: xe_y. - by rewrite -cardT mxvec_cast. -move=> /bigmaxr_ltrP; rewrite size_map -cardT mxvec_cast => xe_y i j. -have := xe_y _ (index (i, j) (enum [finType of 'I_m.+1 * 'I_n.+1])). -have memij : (i, j) \in enum [finType of 'I_m.+1 * 'I_n.+1]. - by rewrite mem_enum. -rewrite (nth_map (ord0, ord0)); last by rewrite index_mem. -by rewrite !mxE !nth_index //=; apply=> //; rewrite -mxvec_cast cardT index_mem. +rewrite predeqE => A; split; last first. + move=> [_/posnumP[e] sA]; exists (fun _ _ => [set p | `|p.1 - p.2| < e%:num]). + by move=> _ _; exists e%:num. + move=> [x y] /= xy; apply: sA => /=. + by apply/bigmaxr_ltrP; split=> // ij _; rewrite !mxE. +move=> [P entP sPA]; set sP := fun i j => [set e | 0 < e /\ + [set pq | `|pq.1 - pq.2| < e] `<=` P i j]. +have {entP} entP : forall i j, sP i j !=set0. + by move=> i j; have [e] := entP i j; exists e. +exists (\big[minr/1]_ij get (sP ij.1 ij.2)). + by apply/bigminr_gtrP; split=> // ij _; have /getPex [] := entP ij.1 ij.2. +move=> [x y] /= /bigminr_gtrP [_ xy]; apply: sPA => i j /=. +have /getPex [_] := entP i j; apply => /=. +by have /bigmaxr_ltrP [_ /(_ (i,j))] := xy (i,j) erefl; rewrite !mxE; apply. Qed. Next Obligation. +have /eqP := H; rewrite eqr_le => /andP [/bigmaxr_lerP [_ x0] _]. apply/matrixP => i j; rewrite mxE; apply/eqP. -rewrite -absr_eq0 eqr_le; apply/andP; split; last exact: absr_ge0. -have /(bigmaxr_ler 0) : - (index (i, j) (enum [finType of 'I_m.+1 * 'I_n.+1]) < - size [seq (`|x ij.1 ij.2|)%real | ij : 'I_m.+1 * 'I_n.+1])%N. - by rewrite size_map index_mem mem_enum. -rewrite -{3}H; apply: ler_trans. -rewrite (nth_map (ord0, ord0)); last by rewrite index_mem mem_enum. -by rewrite nth_index // mem_enum. +by rewrite -absr_eq0 eqr_le absr_ge0 (x0 (i,j)). Qed. Canonical matrix_normedModType := - NormedModType K 'M[K]_(m.+1, n.+1) matrix_NormedModMixin. + NormedModType K 'M[K]_(m, n) matrix_NormedModMixin. End matrix_normedMod. +Lemma coord_continuous {K : absRingType} m n i j : + continuous (fun M : 'M[K]_(m, n) => M i j). +Proof. +move=> M A /= /(@locally_normP _ [normedModType K of K^o]) [_/posnumP[e] sA]. +apply/locally_normP; exists e%:num => // N MN; apply/sA. +by have /bigmaxr_ltrP [_ MeN] := MN; have:= (MeN (i,j)); rewrite !mxE; apply. +Qed. + (** ** Pairs *) Section prod_NormedModule. @@ -956,9 +1296,9 @@ Context {K : absRingType} {U V : normedModType K}. Definition prod_norm (x : U * V) := maxr `|[x.1]| `|[x.2]|. -Lemma prod_norm_triangle : forall x y : U * V, prod_norm (x + y) <= prod_norm x + prod_norm y. +Lemma prod_norm_triangle x y : prod_norm (x + y) <= prod_norm x + prod_norm y. Proof. -by move=> [xu xv] [yu yv]; rewrite ler_maxl /=; apply/andP; split; +by rewrite ler_maxl /=; apply/andP; split; apply: ler_trans (ler_normm_add _ _) _; apply: ler_add; rewrite ler_maxr lerr // orbC. Qed. @@ -967,10 +1307,25 @@ Lemma prod_norm_scal (l : K) (x : U * V) : prod_norm (l *: x) = abs l * prod_norm x. Proof. by rewrite /prod_norm !normmZ maxr_pmulr. Qed. -Lemma ball_prod_normE : ball = ball_ prod_norm. -Proof. -rewrite funeq2E => - [xu xv] e; rewrite predeqE => - [yu yv]. -by rewrite /ball /= /prod_ball -!ball_normE /ball_ ltr_maxl; split=> /andP. +Lemma entourage_prod_normE : entourage = entourage_ prod_norm. +Proof. +rewrite predeqE => A; split; last first. + move=> [_/posnumP[e] sA]; exists ([set u | `|[u.1 - u.2]| < e%:num], + [set v | `|[v.1 - v.2]| < e%:num]) => //=. + move=> /= uv [uv1e uv2e]; exists ((uv.1.1, uv.2.1), (uv.1.2, uv.2.2)). + by apply: sA; rewrite ltr_maxl uv1e uv2e. + by rewrite /= -!surjective_pairing. +move=> [PQ []]; rewrite -!entourage_normE. +move=> [_/posnumP[eP] sP] [_/posnumP[eQ] sQ] sPQA. +exists (minr eP%:num eQ%:num) => // xy. +rewrite ltr_maxl !ltr_minr => /andP [/andP [xy1P xy1Q] /andP [xy2P xy2Q]]. +have PQxy1 : PQ.1 (xy.1.1, xy.2.1) by apply: sP. +have /(conj PQxy1) : PQ.2 (xy.1.2, xy.2.2) by apply: sQ. +move=> /(sPQA ((xy.1.1, xy.2.1), (xy.1.2, xy.2.2))) [uv Auv]. +move=> /eqP /andP [/andP [/= /eqP uvxy11 /eqP uvxy21] /andP + [/= /eqP uvxy12 /eqP uvxy22]]. +rewrite [xy]surjective_pairing [_.2]surjective_pairing [_.1]surjective_pairing. +by rewrite -uvxy11 -uvxy12 -uvxy21 -uvxy22 -!surjective_pairing. Qed. Lemma prod_norm_eq0 (x : U * V) : prod_norm x = 0 -> x = 0. @@ -986,7 +1341,7 @@ End prod_NormedModule. Definition prod_NormedModule_mixin (K : absRingType) (U V : normedModType K) := @NormedModMixin K _ _ _ (@prod_norm K U V) prod_norm_triangle - prod_norm_scal ball_prod_normE prod_norm_eq0. + prod_norm_scal entourage_prod_normE prod_norm_eq0. Canonical prod_NormedModule (K : absRingType) (U V : normedModType K) := NormedModType K (U * V) (@prod_NormedModule_mixin K U V). @@ -1021,17 +1376,20 @@ Lemma flim_norm2 {F : set (set U)} {G : set (set V)} \forall y' \near F & z' \near G, `|[(y, z) - (y', z')]| < eps. Proof. by rewrite flim_normP. Qed. +Lemma flim_ball2P {F : set (set U)} {G : set (set V)} + {FF : Filter F} {FG : Filter G} (y : U) (z : V): + (F, G) --> (y, z) <-> + forall eps, eps > 0 -> \forall y' \near F & z' \near G, + ball norm y eps y' /\ ball norm z eps z'. +Proof. +by rewrite flim_norm2P; split=> FGyz e /FGyz; + apply: filter_app; apply: filterE => x; rewrite ltr_maxl; + [move=> /andP[] | move=> [-> ->]]. +Qed. + End NormedModule3. Arguments flim_norm2 {_ _ _ F G FF FG}. -(** Rings with absolute values are normed modules *) - -Definition AbsRing_NormedModMixin (K : absRingType) := - @NormedModule.Mixin K _ _ _ (abs : K^o -> R) ler_abs_add absrM (ball_absE K) - absr0_eq0. -Canonical AbsRing_NormedModType (K : absRingType) := - NormedModType K K^o (AbsRing_NormedModMixin _). - (** Normed vector spaces have some continuous functions *) Section NVS_continuity. @@ -1134,10 +1492,83 @@ Lemma continuousM (f g : T -> K) x : {for x, continuous (fun x => f x * g x)}. Proof. by move=> fc gc; apply: flim_comp2 fc gc _; apply: lim_mult. Qed. +(** Continuity of norm *) + +Lemma continuous_norm : continuous (@norm _ V). +Proof. +move=> x A /= /(@locally_normP _ [normedModType R of R^o]) [_/posnumP[e] sA]. +apply/locally_normP; exists e%:num => // ??; apply/sA. +exact: ler_lt_trans (ler_distm_dist _ _) _. +Qed. + +(* :TODO: yet, not used anywhere?! *) +Lemma flim_norm0 {U} {F : set (set U)} {FF : Filter F} (f : U -> V) : + (fun x => `|[f x]|) @ F --> (0 : R) + -> f @ F --> (0 : V). +Proof. +move=> /(@flim_norm _ [normedModType R of R^o]) fx0. +apply/flim_normP => e egt0. +rewrite near_simpl; have := fx0 _ egt0; rewrite near_simpl. +by apply: filterS => x; rewrite !sub0r !normmN [ `|[_]| ]ger0_norm. +Qed. + +(* TODO: simplify using extremumP when PR merged in mathcomp *) +Lemma cvg_seq_bounded (a : nat -> V) : + [cvg a in V] -> {M : R | forall n, norm (a n) <= M}. +Proof. +move=> a_cvg; suff: exists M, forall n, norm (a n) <= M. + by move=> /getPex; set M := get _; exists M. +near +oo => M. +have [//|N _ /(_ _ _) /ltrW a_leM] := !! near (flim_bounded _ a_cvg) M. +exists (maxr M (\big[maxr/M]_(n < N) `|[a (val (rev_ord n))]|)) => /= n. +rewrite ler_maxr; have [nN|nN] := leqP N n; first by rewrite a_leM. +apply/orP; right => {a_leM}; elim: N n nN=> //= N IHN n. +rewrite leq_eqVlt => /orP[/eqP[->] |/IHN a_le]; +by rewrite big_ord_recl subn1 /= ler_maxr ?a_le ?lerr ?orbT. +Grab Existential Variables. all: end_near. Qed. + End limit_composition. (** ** Complete Normed Modules *) +Section Cauchy. + +Context {K : absRingType} {V : normedModType K}. + +Definition cauchy_ball (F : set (set V)) := + forall e, e > 0 -> \forall x & y \near F, ball norm x e y. + +Lemma cauchy_cauchy_ball (F : set (set V)) : cauchy F -> cauchy_ball F. +Proof. by move=> Fc _/posnumP[e]; apply: Fc (entourage_ball e). Qed. + +Lemma cauchy_ballP (F : set (set V)) : Filter F -> cauchy_ball F <-> cauchy F. +Proof. +move=> FF; split=> [Fc A|/cauchy_cauchy_ball] //. +by rewrite -entourage_normE => -[_/posnumP[e] sA]; apply: filterS sA (Fc _ _). +Qed. + +Definition cauchy_ex (F : set (set V)) := + forall eps, 0 < eps -> exists x, F (ball norm x eps). + +Lemma cvg_cauchy_ex (F : set (set V)) : [cvg F in V] -> cauchy_ex F. +Proof. by move=> Fl _/posnumP[e]; exists (lim F); apply/Fl/locally_ball. Qed. + +Lemma cauchy_exP (F : set (set V)) : Filter F -> cauchy_ex F -> cauchy F. +Proof. +move=> FF Fc A; rewrite -entourage_normE => -[_/posnumP[e] sA]. +have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sA => /=. +by apply: (@distm_lt_splitr _ _ z); [near: x|near: y]. +Grab Existential Variables. all: end_near. Qed. + +Lemma cauchyP (F : set (set V)) : ProperFilter F -> cauchy F <-> cauchy_ex F. +Proof. +move=> FF; split=> [Fcauchy _/posnumP[e] |/cauchy_exP//]. +near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F); apply: Fcauchy. +exact: entourage_ball. +Grab Existential Variables. all: end_near. Qed. + +End Cauchy. + Module CompleteNormedModule. Section ClassDef. @@ -1224,68 +1655,6 @@ Export CompleteNormedModule.Exports. (** * The topology on real numbers *) -(* TODO: Remove R_complete_lim and use lim instead *) -(* Definition R_lim (F : (R -> Prop) -> Prop) : R := *) -(* sup (fun x : R => `[]). *) - -(* move: (Lub_Rbar_correct (fun x : R => F (ball (x + 1) 1))). *) -(* move Hl : (Lub_Rbar _) => l{Hl}; move: l => [x| |] [Hx1 Hx2]. *) -(* - case: (HF (Num.min 2 eps%:num / 2)%:pos) => z Hz. *) -(* have H1 : z - Num.min 2 eps%:num / 2 + 1 <= x + 1. *) -(* rewrite ler_add //; apply/RleP/Hx1. *) -(* apply: filterS Hz. *) -(* rewrite /ball /= => u; rewrite /AbsRing_ball absrB ltr_distl. *) -(* rewrite absrB ltr_distl. *) -(* case/andP => {Hx1 Hx2 FF HF x F} Bu1 Bu2. *) -(* have H : Num.min 2 eps%:num <= 2 by rewrite ler_minl lerr. *) -(* rewrite addrK -addrA Bu1 /= (ltr_le_trans Bu2) //. *) -(* rewrite -addrA ler_add // -addrA addrC ler_subr_addl. *) -(* by rewrite ler_add // ler_pdivr_mulr // ?mul1r. *) -(* have H2 : x + 1 <= z + Num.min 2 eps%:num / 2 + 1. *) -(* rewrite ler_add //; apply/RleP/(Hx2 (Finite _)) => v Hv. *) -(* apply: Rbar_not_lt_le => /RltP Hlt. *) -(* apply: filter_not_empty. *) -(* apply: filterS (filterI Hz Hv). *) -(* rewrite /ball /= => w []; rewrite /AbsRing_ball //. *) -(* rewrite absrB ltr_distl => /andP[_ Hw1]. *) -(* rewrite absrB ltr_distl addrK => /andP[Hw2 _]. *) -(* by move: (ltr_trans (ltr_trans Hw1 Hlt) Hw2); rewrite ltrr. *) -(* apply: filterS Hz. *) -(* rewrite /ball /= => u; rewrite /AbsRing_ball absrB absRE 2!ltr_distl. *) -(* case/andP => {Hx1 Hx2 F FF HF} H H0. *) -(* have H3 : Num.min 2 eps%:num <= eps by rewrite ler_minl lerr orbT. *) -(* apply/andP; split. *) -(* - move: H1; rewrite -ler_subr_addr addrK ler_subl_addr => H1. *) -(* rewrite ltr_subl_addr // (ltr_le_trans H0) //. *) -(* rewrite -ler_subr_addr (ler_trans H1) //. *) -(* rewrite -ler_subr_addl -!addrA (addrC x) !addrA subrK. *) -(* rewrite ler_subr_addr -mulrDl ler_pdivr_mulr //. *) -(* by rewrite -mulr2n -mulr_natl mulrC ler_pmul. *) -(* - move: H2; rewrite -ler_subr_addr addrK. *) -(* move/ler_lt_trans; apply. *) -(* move: H; rewrite // ltr_subl_addr => H. *) -(* rewrite -ltr_subr_addr (ltr_le_trans H) //. *) -(* rewrite addrC -ler_subr_addr -!addrA (addrC u) !addrA subrK. *) -(* rewrite -ler_subl_addr opprK -mulrDl ler_pdivr_mulr // -mulr2n -mulr_natl. *) -(* by rewrite mulrC ler_pmul. *) -(* - case (HF 1%:pos) => y Fy. *) -(* case: (Hx2 (y + 1)) => x Fx. *) -(* apply: Rbar_not_lt_le => Hlt. *) -(* apply: filter_not_empty. *) -(* apply: filterS (filterI Fy Fx) => z [Hz1 Hz2]. *) -(* apply: Rbar_le_not_lt Hlt; apply/RleP. *) -(* rewrite -(ler_add2r (-(y - 1))) opprB !addrA -![in X in _ <= X]addrA. *) -(* rewrite (addrC y) ![in X in _ <= X]addrA subrK. *) -(* suff : `|x + 1 - y|%R <= 1 + 1 by rewrite ler_norml => /andP[]. *) -(* rewrite ltrW // (@subr_trans _ z). *) -(* by rewrite (ler_lt_trans (ler_norm_add _ _)) // ltr_add // distrC. *) -(* - case: (HF 1%:pos) => y Fy. *) -(* case: (Hx1 (y - 1)); by rewrite addrAC addrK. *) -(* Qed. *) -(* Admitted. *) - -Arguments flim_normW {_ _ F FF}. - (* :TODO: add to mathcomp *) Lemma ltr_distW (R : realDomainType) (x y e : R): (`|x - y|%R < e) -> y - e < x. @@ -1298,32 +1667,34 @@ Proof. by rewrite ler_distl => /andP[]. Qed. Lemma R_complete (F : set (set R)) : ProperFilter F -> cauchy F -> cvg F. Proof. -move=> FF F_cauchy; apply/cvg_ex. +move=> FF Fc; apply/cvg_ex. pose D := \bigcap_(A in F) (down (mem A)). -have /cauchyP /(_ 1) [//|x0 x01] := F_cauchy. +have /Fc := @entourage_ball _ [normedModType R of R^o] 1%:pos. +rewrite near_simpl -near2_pair => /nearP_dep /filter_ex /= [x0 x01]. have D_has_sup : has_sup (mem D); first split. - exists (x0 - 1); rewrite in_setE => A FA. apply/existsbP; near F => x; first exists x. by rewrite ler_distW 1?distrC 1?ltrW ?andbT ?in_setE //; near: x. - exists (x0 + 1); apply/forallbP => x; apply/implyP; rewrite in_setE. move=> /(_ _ x01) /existsbP [y /andP[]]; rewrite in_setE. - rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltrW]. - by move=> /(ler_trans _) yx01 _ /yx01. -exists (sup (mem D)). -apply: (flim_normW (_ : R^o)) => /= _ /posnumP[eps]; near=> x. + by rewrite ltr_distl ltr_subl_addr=> /andP[/ltrW] /(ler_trans _) yx01 _ /yx01. +exists (sup (mem D)); apply: (@flim_normW _ [normedModType R of R^o]). +move=> _/posnumP[eps]; near=> x. rewrite ler_distl sup_upper_bound //=. apply: sup_le_ub => //; first by case: D_has_sup. apply/forallbP => y; apply/implyP; rewrite in_setE. - move=> /(_ (ball_ norm x eps%:num) _) /existsbP []. - by near: x; apply: nearP_dep; apply: F_cauchy. - move=> z /andP[]; rewrite in_setE /ball_ ltr_distl ltr_subl_addr. + move=> /(_ (ball norm x eps%:num) _) /existsbP []. + near: x; apply: nearP_dep; apply: Fc. + exact: (@entourage_ball _ [normedModType R of R^o]). + move=> z /andP[]; rewrite in_setE /ball ltr_distl ltr_subl_addr. by move=> /andP [/ltrW /(ler_trans _) le_xeps _ /le_xeps]. rewrite in_setE /D /= => A FA; near F => y. apply/existsbP; exists y; apply/andP; split. by rewrite in_setE; near: y. rewrite ler_subl_addl -ler_subl_addr ltrW //. suff: `|x - y| < eps%:num by rewrite ltr_norml => /andP[_]. -by near: y; near: x; apply: nearP_dep; apply: F_cauchy. +near: y; near: x; apply: nearP_dep; apply: Fc. +exact: (@entourage_ball _ [normedModType R of R^o]). Grab Existential Variables. all: end_near. Qed. Canonical R_completeType := CompleteType R R_complete. @@ -1336,70 +1707,37 @@ Definition at_right x := within (fun u : R => x < u) (locally x). Global Instance at_right_proper_filter (x : R) : ProperFilter (at_right x). Proof. -apply: Build_ProperFilter' => -[_ /posnumP[d] /(_ (x + d%:num / 2))]. -apply; last (by rewrite ltr_addl); rewrite /AbsRing_ball /=. -rewrite opprD !addrA subrr add0r absrN absRE normf_div !ger0_norm //. +apply: Build_ProperFilter'. +rewrite /at_right -(@filter_from_norm_locally _ [normedModType R of R^o]). +move=> [_/posnumP[e] /(_ (x + e%:num / 2))]; apply; last by rewrite ltr_addl. +rewrite /= opprD addrA subrr add0r [ `|[_]|]normrN normf_div !ger0_norm //. by rewrite ltr_pdivr_mulr // ltr_pmulr // (_ : 1 = 1%:R) // ltr_nat. Qed. Global Instance at_left_proper_filter (x : R) : ProperFilter (at_left x). Proof. -apply: Build_ProperFilter' => -[_ /posnumP[d] /(_ (x - d%:num / 2))]. -apply; last (by rewrite ltr_subl_addl ltr_addr); rewrite /AbsRing_ball /=. -rewrite opprD !addrA subrr add0r opprK absRE normf_div !ger0_norm //. +apply: Build_ProperFilter' => -[A [_/posnumP[d] sA]] /(_ (x - d%:num / 2)). +apply; last by rewrite ltr_subl_addl ltr_addr. +apply: sA; rewrite opprD !addrA subrr add0r opprK absRE normf_div !ger0_norm //. by rewrite ltr_pdivr_mulr // ltr_pmulr // (_ : 1 = 1%:R) // ltr_nat. Qed. Typeclasses Opaque at_left at_right. -(** Continuity of norm *) - -Lemma continuous_norm {K : absRingType} {V : normedModType K} : - continuous (@norm _ V). -Proof. -move=> x; apply/(@flim_normP _ [normedModType R of R^o]) => _/posnumP[e] /=. -rewrite !near_simpl; apply/locally_normP; exists e%:num => // y Hy. -exact/(ler_lt_trans (ler_distm_dist _ _)). -Qed. - -(* :TODO: yet, not used anywhere?! *) -Lemma flim_norm0 {U} {K : absRingType} {V : normedModType K} - {F : set (set U)} {FF : Filter F} (f : U -> V) : - (fun x => `|[f x]|) @ F --> (0 : R) - -> f @ F --> (0 : V). -Proof. -move=> /(flim_norm (_ : R^o)) fx0; apply/flim_normP => _/posnumP[e]. -rewrite near_simpl; have := fx0 _ [gt0 of e%:num]; rewrite near_simpl. -by apply: filterS => x; rewrite !sub0r !normmN [ `|[_]| ]ger0_norm. -Qed. - -(* TODO: simplify using extremumP when PR merged in mathcomp *) -Lemma cvg_seq_bounded {K : absRingType} {V : normedModType K} (a : nat -> V) : - [cvg a in V] -> {M : R | forall n, norm (a n) <= M}. -Proof. -move=> a_cvg; suff: exists M, forall n, norm (a n) <= M. - by move=> /getPex; set M := get _; exists M. -near +oo => M. -have [//|N _ /(_ _ _) /ltrW a_leM] := !! near (flim_bounded _ a_cvg) M. -exists (maxr M (\big[maxr/M]_(n < N) `|[a (val (rev_ord n))]|)) => /= n. -rewrite ler_maxr; have [nN|nN] := leqP N n; first by rewrite a_leM. -apply/orP; right => {a_leM}; elim: N n nN=> //= N IHN n. -rewrite leq_eqVlt => /orP[/eqP[->] |/IHN a_le]; -by rewrite big_ord_recl subn1 /= ler_maxr ?a_le ?lerr ?orbT. -Grab Existential Variables. all: end_near. Qed. - (** Some open sets of [R] *) Lemma open_lt (y : R) : open (< y). Proof. -move=> x /=; rewrite -subr_gt0 => yDx_gt0; exists (y - x) => // z. -by rewrite /AbsRing_ball /= absrB ltr_distl addrCA subrr addr0 => /andP[]. +rewrite openE => x /= ltxy; apply/(@locally_normP _ [normedModType R of R^o]). +exists (y - x); first by rewrite subr_gt0. +by move=> ?; rewrite /= normmB ltr_distl addrCA subrr addr0 => /andP[]. Qed. Hint Resolve open_lt : core. Lemma open_gt (y : R) : open (> y). Proof. -move=> x /=; rewrite -subr_gt0 => xDy_gt0; exists (x - y) => // z. -by rewrite /AbsRing_ball /= absrB ltr_distl opprB addrCA subrr addr0 => /andP[]. +rewrite openE => x /= gtxy; apply/(@locally_normP _ [normedModType R of R^o]). +exists (x - y); first by rewrite subr_gt0. +by move=> ?; rewrite /= normmB ltr_distl opprB addrCA subrr addr0 => /andP[]. Qed. Hint Resolve open_gt : core. @@ -1483,18 +1821,20 @@ have Az : A z. rewrite AeabB; split. suff : {subset `[y, x] <= `[a, b]} by apply. by apply/subitvP; rewrite /= (itvP abx); have /sAab/itvP-> := Ay. - apply: Bcl => D [_ /posnumP[e] ze_D]. + apply: Bcl => D /(@locally_normP _ [normedModType R of R^o]) + [_ /posnumP[e] ze_D]. have [t] := sup_adherent Altxsup [gt0 of e%:num]. rewrite in_setE => - [At lttx] ltzet. exists t; split; first by move: At; rewrite AeabB => - []. - apply/ze_D; rewrite /AbsRing_ball /= absRE ltr_distl. + apply/ze_D; rewrite /ball /= ltr_distl. apply/andP; split; last by rewrite -ltr_subl_addr. rewrite ltr_subl_addr; apply: ltr_spaddr => //. by apply/sup_upper_bound => //; rewrite in_setE. have ltzx : 0 < x - z. have : z <= x by rewrite (itvP yxz). by rewrite subr_gt0 ler_eqVlt => /orP [/eqP zex|] //; move: nAx; rewrite -zex. -have := Az; rewrite AeabC => - [_ /Cop [_ /posnumP[e] ze_C]]. +have := Az; rewrite AeabC => - [_ /Cop /(@locally_normP _ + [normedModType R of R^o]) [_ /posnumP[e] ze_C]]. suff [t Altxt] : exists2 t, Altx t & z < t. by rewrite ltrNge => /negP; apply; apply/sup_upper_bound. exists (z + (minr (e%:num / 2) ((PosNum ltzx)%:num / 2))); last first. @@ -1503,7 +1843,7 @@ rewrite in_setE; split; last first. rewrite -[(< _) _]ltr_subr_addl ltr_minl; apply/orP; right. by rewrite ltr_pdivr_mulr // mulrDr mulr1 ltr_addl. rewrite AeabC; split; last first. - apply: ze_C; rewrite /AbsRing_ball /ball_ absRE ltr_distl. + apply: ze_C; rewrite /ball ltr_distl. apply/andP; split; last by rewrite -addrA ltr_addl. rewrite -addrA gtr_addl subr_lt0 ltr_minl; apply/orP; left. by rewrite [X in _ < X]splitr ltr_addl. @@ -1542,33 +1882,37 @@ apply: segment_connected. by rewrite eqr_le !(itvP aex). - exists B => //; rewrite openE => x [D' sD [saxUf [i Di fx]]]. have : open (f i) by have /sD := Di; rewrite in_setE => /fop. - rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y. + rewrite openE => /(_ _ fx); rewrite !/(_^°) -!(@filter_from_norm_locally _ + [normedModType R of R^o]). + move=> [e egt0 xe_fi]; exists e => // y xe_y. exists D' => //; split; last by exists i => //; apply/xe_fi. move=> z ayz; case: (lerP z x) => [lezx|ltxz]. by apply/saxUf; rewrite inE (itvP ayz) lezx. - exists i=> //; apply/xe_fi; rewrite /AbsRing_ball/ball_ absrB absRE ger0_norm. + exists i=> //; apply/xe_fi; rewrite /ball normmB [ `|[_]|]ger0_norm. have lezy : z <= y by rewrite (itvP ayz). rewrite ltr_subl_addl; apply: ler_lt_trans lezy _; rewrite -ltr_subl_addr. - by have := xe_y; rewrite /AbsRing_ball/ball_ absRE => /ltr_distW. + by have := xe_y; rewrite /ball => /ltr_distW. by rewrite subr_ge0; apply/ltrW. exists A; last by rewrite predeqE => x; split=> [[] | []]. 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]] := locally_ball x e. +have /fop := Di; rewrite openE => /(_ _ fx). +rewrite /(_^°) -(@filter_from_norm_locally _ [normedModType R of R^o]). +move=> [_ /posnumP[e] xe_fi]. +have /clAx [y [[aby [D' sD [sayUf _]]] xe_y]] := locally_ball (x : R^o) e. exists (i |` D')%fset; first by move=> j /fset1UP[->|/sD] //; rewrite in_setE. split=> [z axz|]; last first. exists i; first by rewrite !inE eq_refl. - exact/xe_fi/(@ball_center [uniformType of R]). + exact/xe_fi/ball_center. case: (lerP z y) => [lezy|ltyz]. have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite inE (itvP axz) lezy. by exists j => //; rewrite inE orbC Dj. exists i; first by rewrite !inE eq_refl. -apply/xe_fi; rewrite /AbsRing_ball/ball_ absRE ger0_norm; last first. +apply/xe_fi; rewrite /ball [ `|[_]|]ger0_norm; last first. by rewrite subr_ge0 (itvP axz). rewrite ltr_subl_addl -ltr_subl_addr; apply: ltr_trans ltyz. -by apply: ltr_distW; rewrite -absRE absrB. +by apply: ltr_distW; rewrite distrC. Qed. Lemma ler0_addgt0P (R : realFieldType) (x : R) : @@ -1610,30 +1954,35 @@ have supAab : sup A \in `[a, b]. exists (sup A) => //; have lefsupv : f (sup A) <= v. rewrite lerNgt; apply/negP => ltvfsup. have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0. - have /fcont /(_ _ (locally_ball _ (PosNum vltfsup))) [_/posnumP[d] supdfe] - := supAab. + have /fcont /(_ _ (@locally_ball _ [normedModType R of R^o] _ + (PosNum vltfsup))) := supAab. + rewrite locally_simpl => /= /(@locally_normP _ [normedModType R of R^o]) + [_/posnumP[d] supdfe]. have [t At supd_t] := sup_adherent supA [gt0 of d%:num]. - suff /supdfe : ball (sup A) d%:num t. - rewrite ball_absE /= absRE ltr_norml => /andP [_]. + suff /supdfe : ball norm (sup A : R^o) d%:num t. + rewrite ltr_norml => /andP [_]. by rewrite ltr_add2l ltr_oppr opprK ltrNge; have /andP [_ ->] := At. - rewrite ball_absE /= absRE ger0_norm. + rewrite /ball [ `|[_]|]ger0_norm. by rewrite ltr_subl_addr -ltr_subl_addl. by rewrite subr_ge0 sup_upper_bound. apply/eqP; rewrite eqr_le; apply/andP; split=> //. rewrite -subr_le0; apply/ler0_addgt0P => _/posnumP[e]. rewrite ler_subl_addr -ler_subl_addl ltrW //. -have /fcont /(_ _ (locally_ball _ e)) [_/posnumP[d] supdfe] := supAab. +have /fcont /(_ _ (@locally_ball _ [normedModType R of R^o] _ e)) := supAab. +rewrite locally_simpl /= => /(@locally_normP _ [normedModType R of R^o]). +move=> [_/posnumP[d] supdfe]. have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x. -have /supdfe /= : ball (sup A) d%:num x. - by near: x; rewrite /= locally_simpl; exists d%:num => //. -rewrite ball_absE /= absRE => /ltr_distW; apply: ler_lt_trans. +have /supdfe /= : ball norm (sup A : R^o) d%:num x. + by near: x; apply/(@locally_normP _ [normedModType R of R^o]); exists d%:num. +move/ltr_distW; apply: ler_lt_trans. rewrite ler_add2r ltrW //; suff : forall t, t \in `](sup A), b] -> v < f t. - apply; rewrite inE; apply/andP; split; first by near: x; exists 1. - near: x; exists (b - sup A). + apply; rewrite inE; apply/andP; split. + by near: x; apply/(@locally_normP _ [normedModType R of R^o]); exists 1. + near:x; apply/(@locally_normP _ [normedModType R of R^o]); exists (b - sup A). rewrite subr_gt0 ltr_def (itvP supAab) andbT; apply/negP => /eqP besup. by move: lefsupv; rewrite lerNgt -besup ltvfb. - move=> t lttb ltsupt; move: lttb; rewrite /AbsRing_ball /= absrB absRE. - by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltrW. + move=> t lttb ltsupt; move: lttb; rewrite /ball normmB. + by rewrite [ `|[_]|]gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltrW. move=> t /andP [ltsupt letb]; rewrite ltrNge; apply/negP => leftv. move: ltsupt; rewrite ltrNge => /negP; apply; apply: sup_upper_bound => //. by rewrite inE letb leftv. @@ -1647,8 +1996,8 @@ Lemma locally_interval (P : R -> Prop) (x : R) (a b : Rbar) : locally x P. Proof. move => Hax Hxb Hp; case: (Rbar_lt_locally _ _ _ Hax Hxb) => d Hd. -exists d%:num => //= y; rewrite /AbsRing_ball /= absrB. -by move=> /Hd /andP[??]; apply: Hp. +apply/(@locally_normP _ [normedModType R of R^o]); exists d%:num => //= y. +by rewrite /ball normmB => /Hd /andP[??]; apply: Hp. Qed. (** * Topology on [R]² *) @@ -1811,8 +2160,8 @@ 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/locallyP; exists (n%:~R - `|[p]|) => // q. - rewrite -ball_normE /= ltr_subr_addr normmB; apply: ler_lt_trans. + apply/locally_normP; exists (n%:~R - `|[p]|) => // q. + rewrite /ball ltr_subr_addr normmB; apply: ler_lt_trans. by rewrite -{1}(subrK p q) ler_normm_add. move=> D _ DcovA. exists (bigmaxr 0 [seq n%:~R | n <- enum_fset D]). @@ -1822,23 +2171,23 @@ rewrite -(nth_index 0 Dn) -(nth_map _ 0) //; apply: bigmaxr_ler. by rewrite size_map. Qed. -Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 -> set T) : +Lemma rV_compact (T : topologicalType) n (A : 'I_n -> set T) : (forall i, compact (A i)) -> - compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)]. + compact [ set v : 'rV[T]_n | forall i, A i (v ord0 i)]. Proof. move=> Aico. have : @compact (product_topologicalType _) [set f | forall i, A i (f i)]. by apply: tychonoff. move=> Aco F FF FA. -set G := [set [set f : 'I_n.+1 -> T | B (\row_j f j)] | B in F]. -have row_simpl (v : 'rV[T]_n.+1) : \row_j (v ord0 j) = v. +set G := [set [set f : 'I_n -> T | B (\row_j f j)] | B in F]. +have row_simpl (v : 'rV[T]_n) : \row_j (v ord0 j) = v. by apply/rowP => ?; rewrite mxE. -have row_simpl' (f : 'I_n.+1 -> T) : (\row_j f j) ord0 = f. +have row_simpl' (f : 'I_n -> T) : (\row_j f j) ord0 = f. by rewrite funeqE=> ?; rewrite mxE. have [f [Af clGf]] : [set f | forall i, A i (f i)] `&` @cluster (product_topologicalType _) G !=set0. suff GF : ProperFilter G. - apply: Aco; exists [set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)] => //. + apply: Aco; exists [set v : 'rV[T]_n | forall i, A i (v ord0 i)] => //. by rewrite predeqE => f; split => Af i; [have := Af i|]; rewrite row_simpl'. apply Build_ProperFilter. move=> _ [C FC <-]; have /filter_ex [v Cv] := FC. @@ -1846,7 +2195,7 @@ have [f [Af clGf]] : [set f | forall i, A i (f i)] `&` split. - by exists setT => //; apply: filterT. - by move=> _ _ [C FC <-] [D FD <-]; exists (C `&` D) => //; apply: filterI. - move=> C D sCD [E FE EeqC]; exists [set v : 'rV[T]_n.+1 | D (v ord0)]. + move=> C D sCD [E FE EeqC]; exists [set v : 'rV[T]_n | D (v ord0)]. by apply: filterS FE => v Ev; apply/sCD; rewrite -EeqC row_simpl. by rewrite predeqE => ?; rewrite row_simpl'. exists (\row_j f j); split; first by move=> i; rewrite mxE; apply: Af. @@ -1861,12 +2210,10 @@ move=> C D FC f_D; have {f_D} f_D : move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'. by have /getPex [_ /(_ _ (Pg j))] := exPj j. split; last by move=> j; have /getPex [[]] := exPj j. - exists [set [set g | forall j, get (Pj j) (g j)] | k in 'I_n.+1]; - last first. - rewrite predeqE => g; split; first by move=> [_ [_ _ <-]]. - move=> Pg; exists [set g | forall j, get (Pj j) (g j)] => //. - by exists ord0. - move=> _ [_ _ <-]; set s := [seq (@^~ j) @^-1` (get (Pj j)) | j : 'I_n.+1]. + exists [set [set g | forall j, get (Pj j) (g j)]]; last first. + rewrite predeqE => g; split=> [[? ->] | Pg] //. + by exists [set g | forall j, get (Pj j) (g j)]. + move=> _ ->; set s := [seq (@^~ j) @^-1` (get (Pj j)) | j : 'I_n]. exists [fset x in s]%fset. move=> B'; rewrite in_fset => /mapP [j _ ->]; rewrite inE. apply/asboolP; exists j => //; exists (get (Pj j)) => //. @@ -1879,21 +2226,17 @@ have GC : G [set g | C (\row_j g j)] by exists C. by have [g []] := clGf _ _ GC f_D; exists (\row_j (g j : T)). Qed. -Lemma bounded_closed_compact n (A : set 'rV[R]_n.+1) : +Lemma bounded_closed_compact n (A : set 'rV[R]_n) : bounded A -> closed A -> compact A. Proof. move=> [M normAltM] Acl. have Mnco : compact - [set v : 'rV[R]_n.+1 | (forall i, (v ord0 i) \in `[(- (M + 1)), (M + 1)])]. + [set v : 'rV[R]_n | (forall i, (v ord0 i) \in `[(- (M + 1)), (M + 1)])]. apply: (@rV_compact _ _ (fun _ => [set x | x \in `[(- (M + 1)), (M + 1)]])). by move=> _; apply: segment_compact. apply: subclosed_compact Acl Mnco _ => v /normAltM normvltM i. -suff /ltrW : `|[v ord0 i : R^o]| < M + 1 by rewrite [ `|[_]| ]absRE ler_norml. -apply: ler_lt_trans (normvltM _ _); last by rewrite ltr_addl. -have vinseq : `|v ord0 i| \in [seq `|v ij.1 ij.2| | ij : 'I_1 * 'I_n.+1]. - by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum. -rewrite -[X in X <= _](nth_index 0 vinseq); apply: bigmaxr_ler. -by rewrite index_mem. +suff /ltrW : `|[v ord0 i : R^o]| < M + 1 by rewrite ler_norml. +by apply: ler_lt_trans (ler_bigmaxr (_,_) _) (normvltM _ _); rewrite ltr_addl. Qed. (** Open sets in [Rbar] *) @@ -1931,13 +2274,14 @@ Qed. Lemma Rbar_locally'_le x : Rbar_locally' x --> Rbar_locally x. Proof. -move: x => [x P [_/posnumP[e] HP] |x P|x P] //=. -by exists e%:num => // ???; apply: HP. +by move: x => [||] x P //=; rewrite locally_simpl /locally /= locallyE' => -[]. Qed. Lemma Rbar_locally'_le_finite (x : R) : Rbar_locally' x --> locally x. Proof. -by move=> P [_/posnumP[e] HP] //=; exists e%:num => // ???; apply: HP. +move=> P; rewrite locally_simpl => /(@locally_normP _ [normedModType R of R^o]). +move=> [_/posnumP[e] sP] /=; apply/(@locally_normP _ [normedModType R of R^o]). +by exists e%:num => // ? /sP. Qed. (** * Some limits on real functions *) @@ -1951,7 +2295,8 @@ Definition Rbar_loc_seq (x : Rbar) (n : nat) := match x with Lemma flim_Rbar_loc_seq x : Rbar_loc_seq x --> Rbar_locally' x. Proof. move=> P; rewrite /Rbar_loc_seq. -case: x => /= [x [_/posnumP[delta] Hp] |[delta Hp] |[delta Hp]]; last 2 first. +case: x => /= [x /(@locally_normP _ [normedModType R of R^o]) + [_/posnumP[delta] Hp] |[delta Hp] |[delta Hp]]; last 2 first. have /ZnatP [N Nfloor] : ifloor (maxr delta 0) \is a Znat. by rewrite Znat_def ifloor_ge0 ler_maxr lerr orbC. exists N.+1 => // n ltNn; apply: Hp. @@ -1970,8 +2315,8 @@ exists N => // n leNn; have gt0Sn : 0 < INR n + 1. by apply: ltr_spaddr => //; apply/RleP/pos_INR. apply: Hp; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym; apply/invr_neq0/lt0r_neq0. -rewrite /AbsRing_ball /= opprD addrA subrr absrB subr0. -rewrite absRE gtr0_norm; last by rewrite invr_gt0. +rewrite /ball opprD addrA subrr normmB subr0. +rewrite [ `|[_]|]gtr0_norm; last by rewrite invr_gt0. rewrite -[X in X < _]mulr1 ltr_pdivr_mull // -ltr_pdivr_mulr // div1r. apply: ltr_le_trans (floorS_gtr _) _; rewrite floorE Nfloor ler_add //. by rewrite INRE ler_nat. @@ -1982,55 +2327,38 @@ Lemma continuity_pt_locally f x : continuity_pt f x <-> forall eps : posreal, locally x (fun u => `|f u - f x| < eps). Proof. split=> [fcont e|fcont _/RltP/posnumP[e]]; last first. - have [_/posnumP[d] xd_fxe] := fcont e. + have /(@locally_normP _ [normedModType R of R^o]) [_/posnumP[d] xd_fxe] := + fcont e. exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num]. - by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /AbsRing_ball /= absrB. + by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /ball normmB. +apply/(@locally_normP _ [normedModType R of R^o]). have /RltP egt0 := [gt0 of e%:num]. have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0. exists d%:num => // y xyd; case: (eqVneq x y) => [->|xney]. by rewrite subrr absr0. apply/RltP/dx_fxe; split; first by split=> //; apply/eqP. -by have /RltP := xyd; rewrite absrB. +by have /RltP := xyd; rewrite normmB. Qed. Lemma continuity_pt_flim (f : R -> R) (x : R) : continuity_pt f x <-> {for x, continuous f}. Proof. -eapply iff_trans; first exact: continuity_pt_locally. -apply iff_sym. +apply: iff_trans (continuity_pt_locally _ _) _; apply: iff_sym. have FF : Filter (f @ x). (* (* BUG: this should work *) *) (* by typeclasses eauto. *) by apply filtermap_filter; apply: @filter_filter' (locally_filter _). -case: (@flim_ballP _ (f @ x) FF (f x)) => {FF}H1 H2. -(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *) -split => [{H2} - /H1 {H1} H1 eps|{H1} H]. -- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num. - exists x0%:num => // Hx0' /Hx0 /=. - by rewrite ball_absE /= absrB; apply. -- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0]. - exists x0%:num => // y /Hx0 /= {Hx0}Hx0. - by rewrite ball_absE /= absrB. -Qed. +apply: iff_trans (flim_normP (f x : R^o)) _; split=> [fx e|fx _/posnumP[e]]. + have /fx := [gt0 of e%:num]. + by apply: (@filter_app _ (locally x)); near=> y; rewrite /= normmB. +have := fx e; rewrite !near_simpl; apply: filter_app. +by near=> y; rewrite normmB. +Unshelve. all: end_near. Qed. Lemma continuity_ptE (f : R -> R) (x : R) : continuity_pt f x <-> {for x, continuous f}. Proof. exact: continuity_pt_flim. Qed. -Lemma continuous_withinNx {U V : uniformType} - (f : U -> V) x : - {for x, continuous f} <-> f @ locally' x --> f x. -Proof. -split=> - cfx P /= fxP. - rewrite /locally' !near_simpl near_withinE. - by rewrite /locally'; apply: flim_within; apply/cfx. - (* :BUG: ssr apply: does not work, - because the type of the filter is not inferred *) -rewrite !locally_nearE !near_map !near_locally in fxP *; have /= := cfx P fxP. -rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. -by have [->|] := eqVneq y x; [by apply: locally_singleton|near: y]. -Grab Existential Variables. all: end_near. Qed. - Lemma continuity_pt_flim' f x : continuity_pt f x <-> f @ locally' x --> f x. Proof. by rewrite continuity_ptE continuous_withinNx. Qed. diff --git a/topology.v b/topology.v index f66dd3a114..cbf2bf058d 100644 --- a/topology.v +++ b/topology.v @@ -1,8 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -Require Import Reals. From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice. -From mathcomp Require Import seq fintype bigop ssralg ssrnum finmap matrix. -Require Import boolp Rstruct classical_sets posnum. +From mathcomp Require Import seq fintype ssralg finmap matrix. +Require Import boolp classical_sets posnum. (******************************************************************************) (* This file develops tools for the manipulation of filters and basic *) @@ -195,38 +194,37 @@ Require Import boolp Rstruct classical_sets posnum. (* product topology. *) (* *) (* * Uniform spaces : *) -(* locally_ ball == neighbourhoods defined using balls *) +(* locally_ ent == neighbourhoods defined using entourages. *) (* uniformType == interface type for uniform space *) -(* structure. We use here a pseudo-metric *) +(* structure. We use here the entourage *) (* definition of uniform space: a type *) -(* equipped with balls. *) -(* UniformMixin brefl bsym btriangle locb == builds the mixin for a *) -(* uniform space from the properties of *) -(* balls and the compatibility between *) -(* balls and locally. *) +(* equipped with a set of entourages, also *) +(* called uniformity. An entourage can be *) +(* seen as a "neighbourhood" of the *) +(* diagonal set {(x, x) | x in T}. *) +(* UniformMixin entF ent_refl ent_inv ent_split loc_ent == builds the mixin *) +(* for a uniform space from the properties *) +(* of entourages and the compatibility *) +(* between entourages and locally. *) (* 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. *) -(* topologyOfBallMixin umixin == builds the mixin for a topological space *) -(* from a mixin for a uniform space. *) -(* ball x e == ball of center x and radius e. *) -(* 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 *) +(* topologyOfEntourageMixin umixin == builds the mixin for a topological *) +(* space from a mixin for a uniform space. *) +(* entourage == set of entourages. *) +(* split_ent A == "half entourage": entourage B such that, *) +(* when seen as a relation, B \o B `<=` A. *) +(* close x y <-> x and y are arbitrarily close, i.e. the *) +(* pair (x,y) is in any entourage. *) (* unif_cont f <-> f is uniformly continuous. *) +(* entourage_set == set of entourages on the parts of a *) +(* uniform space. *) (* *) (* * Complete 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). *) (* completeType == interface type for a complete uniform *) (* space structure. *) (* CompleteType T cvgCauchy == packs the proof that every proper cauchy *) @@ -275,7 +273,6 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing.Theory Num.Def Num.Theory. Local Open Scope classical_set_scope. Module Filtered. @@ -2271,23 +2268,32 @@ 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 defined using balls *) +(** * Uniform spaces defined using entourages *) -Definition locally_ {T T'} (ball : T -> R -> set T') (x : T) := - @filter_from R _ [set x | 0 < x] (ball x). +Local Notation "B \o A" := + ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope. -Lemma locally_E {T T'} (ball : T -> R -> set T') x : - locally_ ball x = @filter_from R _ [set x : R | 0 < x] (ball x). +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 locally_ {T T'} (ent : set (set (T * T'))) (x : T) := + filter_from ent (fun A => to_set A x). + +Lemma locally_E {T T'} (ent : set (set (T * T'))) x : + locally_ ent x = filter_from ent (fun A => to_set A x). Proof. by []. Qed. Module Uniform. Record mixin_of (M : Type) (locally : M -> set (set 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 : locally = locally_ ball + 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 ; + ax4 : forall A, entourage A -> exists2 B, entourage B & B \o B `<=` A ; + ax5 : locally = locally_ entourage }. Record class_of (M : Type) := Class { @@ -2352,183 +2358,154 @@ Export Uniform.Exports. Section UniformTopology. -Lemma my_ball_le (M : Type) (loc : M -> set (set M)) - (m : Uniform.mixin_of loc) : - forall (x : M) (e1 e2 : R), e1 <= e2 -> - forall (y : M), Uniform.ball m x e1 y -> Uniform.ball m x e2 y. -Proof. -move=> x e1 e2 le12 y xe1_y. -move: le12; rewrite ler_eqVlt => /orP [/eqP <- //|]. -rewrite -subr_gt0 => lt12. -rewrite -[e2](subrK e1); apply: Uniform.ax3 xe1_y. -suff : Uniform.ball m x (PosNum lt12)%:num x by []. -exact: Uniform.ax1. -Qed. - -Program Definition topologyOfBallMixin (T : Type) +Program Definition topologyOfEntourageMixin (T : Type) (loc : T -> set (set T)) (m : Uniform.mixin_of loc) : Topological.mixin_of loc := topologyOfFilterMixin _ _ _. Next Obligation. -rewrite (Uniform.ax4 m) locally_E; apply filter_from_proper; last first. - move=> e egt0; exists p; suff : Uniform.ball m p (PosNum egt0)%:num p by []. - exact: Uniform.ax1. -apply: filter_from_filter; first by exists 1%:pos%:num. -move=> e1 e2 e1gt0 e2gt0; exists (Num.min e1 e2). - by have := min_pos_gt0 (PosNum e1gt0) (PosNum e2gt0). -by move=> q pmin_q; split; apply: my_ball_le pmin_q; - rewrite ler_minl lerr // orbC. +rewrite (Uniform.ax5 m) locally_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.ax4 m) locally_E => - [e egt0]; apply. -by have : Uniform.ball m p (PosNum egt0)%:num p by exact: Uniform.ax1. +move: H; rewrite (Uniform.ax5 m) locally_E => - [B entB sBpA]. +by apply: sBpA; apply: Uniform.ax2 entB _ _. Qed. Next Obligation. -move: H; rewrite (Uniform.ax4 m) locally_E => - [e egt0 pe_A]. -exists ((PosNum egt0)%:num / 2) => // q phe_q. -rewrite locally_E; exists ((PosNum egt0)%:num / 2) => // r qhe_r. -by apply: pe_A; rewrite [e]splitr; apply: Uniform.ax3 qhe_r. +move: H; rewrite (Uniform.ax5 m) locally_E => - [B entB sBpA]. +have /Uniform.ax4 [C entC sC2B] := entB. +exists C => // q Cpq; rewrite locally_E; exists C => // r Cqr. +by apply/sBpA/sC2B; exists q. Qed. End UniformTopology. -Definition ball {M : uniformType} := Uniform.ball (Uniform.class M). +Definition entourage {M : uniformType} := Uniform.entourage (Uniform.class M). -Lemma locally_ballE {M : uniformType} : locally_ (@ball M) = locally. +Lemma locally_entourageE {M : uniformType} : locally_ (@entourage M) = locally. Proof. by case: M=> [?[?[]]]. Qed. -Lemma filter_from_ballE {M : uniformType} x : - @filter_from R _ [set x : R | 0 < x] (@ball M x) = locally x. -Proof. by rewrite -locally_ballE. Qed. +Lemma filter_from_entourageE {M : uniformType} x : + filter_from (@entourage M) (fun A => to_set A x) = locally x. +Proof. by rewrite -locally_entourageE. Qed. -Module Export LocallyBall. -Definition locally_simpl := (locally_simpl,@filter_from_ballE,@locally_ballE). -End LocallyBall. +Module Export LocallyEntourage. +Definition locally_simpl := + (locally_simpl,@filter_from_entourageE,@locally_entourageE). +End LocallyEntourage. Lemma locallyP {M : uniformType} (x : M) P : - locally x P <-> locally_ ball x P. + locally x P <-> locally_ entourage x P. Proof. by rewrite locally_simpl. Qed. Section uniformType1. Context {M : uniformType}. -Lemma ball_center (x : M) (e : posreal) : ball x e%:num x. -Proof. exact: Uniform.ax1. Qed. -Hint Resolve ball_center : core. +Lemma entourage_refl (A : set (M * M)) x : + entourage A -> A (x, x). +Proof. by move=> entA; apply: Uniform.ax2 entA _ _. Qed. -Lemma ballxx (x : M) (e : R) : (0 < e)%R -> ball x e x. -Proof. by move=> e_gt0; apply: ball_center (PosNum e_gt0). 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 ball_sym (x y : M) (e : R) : ball x e y -> ball y e x. -Proof. exact: Uniform.ax2. Qed. +Lemma entourageT : entourage (@setT (M * M)). +Proof. exact: filterT. Qed. -Lemma ball_triangle (y x z : M) (e1 e2 : R) : - ball x e1 y -> ball y e2 z -> ball x (e1 + e2)%R z. +Lemma entourage_inv (A : set (M * M)) : entourage A -> entourage A^-1. Proof. exact: Uniform.ax3. Qed. -Lemma ball_split (z x y : M) (e : R) : - ball x (e / 2)%R z -> ball z (e / 2)%R y -> ball x e y. -Proof. by move=> /ball_triangle h /h; rewrite -splitr. Qed. +Lemma entourage_split_ex (A : set (M * M)) : + entourage A -> exists2 B, entourage B & B \o B `<=` A. +Proof. exact: Uniform.ax4. Qed. -Lemma ball_splitr (z x y : M) (e : R) : - ball z (e / 2)%R x -> ball z (e / 2)%R y -> ball x e y. -Proof. by move=> /ball_sym /ball_split; apply. Qed. +Definition split_ent (A : set (M * M)) := + get (entourage `&` [set B | B \o B `<=` A]). -Lemma ball_splitl (z x y : M) (e : R) : - ball x (e / 2) z -> ball y (e / 2) z -> ball x e y. -Proof. by move=> bxz /ball_sym /(ball_split bxz). Qed. +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 ball_ler (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2. -Proof. -move=> le12 y; case: ltrgtP le12 => [//|lte12 _|->//]. -by rewrite -[e2](subrK e1); apply/ball_triangle/ballxx; rewrite subr_gt0. -Qed. +Lemma entourage_split_ent (A : set (M * M)) : entourage A -> + entourage (split_ent A). +Proof. by move=> /split_entP []. Qed. +Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core. +Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core. -Lemma ball_le (x : M) (e1 e2 : R) : (e1 <= e2)%coqR -> ball x e1 `<=` ball x e2. -Proof. by move=> /RleP/ball_ler. 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 locally_ball (x : M) (eps : posreal) : locally x (ball x eps%:num). -Proof. by apply/locallyP; exists eps%:num. Qed. -Hint Resolve locally_ball : core. +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. +Arguments entourage_split z {x y A}. -Definition close (x y : M) : Prop := forall eps : posreal, ball x eps%:num y. +Definition close (x y : M) : Prop := forall A, entourage A -> A (x,y). -Lemma close_refl (x : M) : close x x. Proof. by []. Qed. +Lemma close_refl (x : M) : close x x. Proof. by move=> ? /entourage_refl. Qed. Lemma close_sym (x y : M) : close x y -> close y x. -Proof. by move=> ??; apply: ball_sym. Qed. +Proof. by move=> cxy ? /entourage_inv /cxy. Qed. Lemma close_trans (x y z : M) : close x y -> close y z -> close x z. -Proof. by move=> cxy cyz eps; apply: ball_split (cxy _) (cyz _). Qed. - -Lemma close_limxx (x y : M) : close x y -> x --> y. Proof. -move=> cxy P /= /locallyP /= [_/posnumP [eps] epsP]. -apply/locallyP; exists (eps%:num / 2) => // z bxz. -by apply: epsP; apply: ball_splitr (cxy _) bxz. +by move=> cxy cyz A entA; apply: (entourage_split y) => //; + [apply: cxy|apply: cyz]. 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. +Lemma close_limxx (x y : M) : close x y -> x --> y. 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 (minr i j) => // [[/= x y]] bxy. -by eexists => /=; apply: ball_ler bxy; rewrite ler_minl lerr ?orbT. +move=> cxy A /= /locallyP [B entB sBA]. +apply/locallyP; exists (split_ent B) => // z hByz; apply/sBA. +by apply: subset_split_ent => //; exists x => //=; apply: (close_sym cxy). Qed. -Typeclasses Opaque entourages. + +Lemma locally_entourage (x : M) A : entourage A -> locally x (to_set A x). +Proof. by move=> ?; apply/locallyP; exists A. Qed. +Hint Resolve locally_entourage. Lemma flim_close {F} {FF : ProperFilter F} (x y : M) : F --> x -> F --> y -> close x y. Proof. -move=> Fx Fy e; near F => z; apply: (@ball_splitl z); near: z; -by [apply/Fx/locally_ball|apply/Fy/locally_ball]. +move=> Fx Fy A entA; apply: subset_split_ent => //. +near F => z; exists z => /=; near: z; first exact/Fx/locally_entourage. +by apply/Fy; apply: locally_entourage (entourage_inv _). Grab Existential Variables. all: end_near. Qed. Lemma flimx_close (x y : M) : x --> y -> close x y. Proof. exact: flim_close. Qed. -Lemma near_ball (y : M) (eps : posreal) : - \forall y' \near y, ball y eps%:num y'. -Proof. exact: locally_ball. Qed. - -Lemma flim_ballP {F} {FF : Filter F} (y : M) : - F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. -Proof. by rewrite -filter_fromP !locally_simpl /=. Qed. -Definition flim_locally := @flim_ballP. - -Lemma flim_ballPpos {F} {FF : Filter F} (y : M) : - F --> y <-> forall eps : {posnum R}, \forall y' \near F, ball y eps%:num y'. -Proof. -by split => [/flim_ballP|] pos; [case|apply/flim_ballP=> _/posnumP[eps] //]. -Qed. +Lemma flim_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 !locally_simpl. Qed. -Lemma flim_ball {F} {FF : Filter F} (y : M) : - F --> y -> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. -Proof. by move/flim_ballP. Qed. +Lemma flim_entourage {F} {FF : Filter F} (y : M) : + F --> y -> forall A, entourage A -> \forall y' \near F, A (y,y'). +Proof. by move/flim_entourageP. Qed. -Lemma app_flim_locally T {F} {FF : Filter F} (f : T -> M) y : - f @ F --> y <-> forall eps : R, 0 < eps -> \forall x \near F, ball y eps (f x). -Proof. exact: flim_ballP. Qed. +Lemma app_flim_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: flim_entourageP. Qed. -Lemma flimi_ballP T {F} {FF : Filter F} (f : T -> M -> Prop) y : +Lemma flimi_entourageP 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. + forall A, entourage A -> \forall x \near F, exists z, f x z /\ A (y,z). Proof. -split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/locally_ball. -move=> /locallyP[_ /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. +split=> [Fy A entA|Fy A] /=; first exact/Fy/locally_entourage. +move=> /locallyP [B entB sBA]; rewrite near_simpl near_mapi; near=> x. +by have [//|z [fxz Byz]]:= near (Fy _ entB) x; exists z; split=> //; apply: sBA. Unshelve. all: end_near. Qed. -Definition flimi_locally := @flimi_ballP. +Definition flimi_locally := @flimi_entourageP. -Lemma flimi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y : +Lemma flimi_entourage T {F} {FF : Filter F} (f : T -> M -> Prop) y : f `@ F --> y -> - forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z]. -Proof. by move/flimi_ballP. Qed. + forall A, entourage A -> F [set x | exists z, f x z /\ A (y,z)]. +Proof. by move/flimi_entourageP. Qed. Lemma flimi_close T {F} {FF: ProperFilter F} (f : T -> set M) (l l' : M) : {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'. @@ -2536,15 +2513,15 @@ Proof. move=> f_prop fFl fFl'. suff f_totalfun: infer {near F, is_totalfun f} by exact: flim_close fFl fFl'. apply: filter_app f_prop; near=> x; split=> //=. -by have [//|y [fxy _]] := near (flimi_ball fFl [gt0 of 1]) x; exists y. +by have [//|y []] := near (flimi_entourage fFl entourageT) x; exists y. Grab Existential Variables. all: end_near. Qed. Definition flimi_locally_close := @flimi_close. Lemma flim_const {T} {F : set (set T)} {FF : Filter F} (a : M) : a @[_ --> F] --> a. Proof. -move=> P /locallyP[_ /posnumP[eps] subP]; rewrite !near_simpl /=. -by apply: filterE=> ?; apply/subP. +move=> A /locallyP [B entB sBA]; rewrite !near_simpl /=. +by apply: filterE => _; apply/sBA; apply: entourage_refl. Qed. Lemma close_lim (F1 F2 : set (set M)) {FF2 : ProperFilter F2} : @@ -2553,7 +2530,7 @@ Proof. move=> F12 F21; have [/(flim_trans F21) F2l|dvgF1] := pselect (cvg F1). by apply: (@flim_close F2) => //; apply: cvgP F2l. have [/(flim_trans F12)/cvgP//|dvgF2] := pselect (cvg F2). -by rewrite dvgP // dvgP //. +by rewrite dvgP // dvgP //; apply: close_refl. Qed. Lemma flim_closeP (F : set (set M)) (l : M) : ProperFilter F -> @@ -2564,149 +2541,221 @@ move=> FF; split=> [Fl|[cvF]Cl]. by apply: flim_trans (close_limxx Cl). 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 => locally_ ball_set A). - End uniformType1. -Hint Resolve ball_center : core. -Hint Resolve close_refl : core. -Hint Resolve locally_ball : core. +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 (locally _ (to_set _ _)) => exact: locally_entourage : core. +Hint Resolve close_refl. Arguments flim_const {M T F FF} a. Arguments close_lim {M} F1 F2 {FF2} _. -Section entourages. +Lemma continuous_withinNx {U V : uniformType} + (f : U -> V) x : + {for x, continuous f} <-> f @ locally' x --> f x. +Proof. +split=> - cfx P /= fxP. + rewrite /locally' !near_simpl near_withinE. + by rewrite /locally'; apply: flim_within; apply/cfx. + (* :BUG: ssr apply: does not work, + because the type of the filter is not inferred *) +rewrite !locally_nearE !near_map !near_locally in fxP *; have /= := cfx P fxP. +rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. +by have [->|] := eqVneq y x; [by apply: locally_singleton|near: y]. +Grab Existential Variables. all: end_near. Qed. Definition unif_cont (U V : uniformType) (f : U -> V) := - (fun xy => (f xy.1, f xy.2)) @ entourages --> entourages. - -Lemma unif_contP (U V : uniformType) (f : U -> V) : - unif_cont 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. - -End entourages. + (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage. -(** ** Specific uniform spaces *) - -(** matrices *) - -Section matrix_Uniform. - -Variables (m n : nat) (T : uniformType). - -Implicit Types x y : 'M[T]_(m, n). +(** product of two uniform spaces *) -Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j). +Section prod_Uniform. -Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x. -Proof. by move=> ???; apply: ballxx. Qed. +Context {U V : uniformType}. +Implicit Types A : set ((U * V) * (U * V)). -Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x. -Proof. by move=> xe_y ??; apply/ball_sym/xe_y. Qed. +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 mx_ball_triangle x y z (e1 e2 : R) : - mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z. +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. -by move=> xe1_y ye2_z ??; apply: ball_triangle; [apply: xe1_y| apply: ye2_z]. +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 ltr_bigminr (I : finType) (R : realDomainType) (f : I -> R) (x0 x : R) : - x < x0 -> (forall i, x < f i) -> x < \big[minr/x0]_i f i. +Lemma prod_ent_filter : Filter prod_ent. Proof. -move=> ltx0 ltxf; elim/big_ind: _ => // y z ltxy ltxz. -by rewrite ltr_minr ltxy ltxz. +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 bigminr_ler (I : finType) (R : realDomainType) (f : I -> R) (x0 : R) i : - \big[minr/x0]_j f j <= f i. +Lemma prod_ent_refl A : prod_ent A -> [set xy | xy.1 = xy.2] `<=` A. Proof. -have := mem_index_enum i; rewrite unlock; elim: (index_enum I) => //= j l ihl. -by rewrite inE => /orP [/eqP->|/ihl leminlfi]; - rewrite ler_minl ?lerr // leminlfi orbC. +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. -Canonical R_pointedType := PointedType R 0. +Lemma prod_ent_inv A : prod_ent A -> prod_ent A^-1. +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 mx_locally : locally = locally_ mx_ball. +Lemma prod_ent_split A : prod_ent A -> exists2 B, prod_ent B & B \o B `<=` A. Proof. -rewrite predeq2E => x A; split; last first. - by move=> [e egt0 xe_A]; exists (fun i j => ball (x i j) (PosNum egt0)%:num). -move=> [P]; rewrite -locally_ballE => x_P sPA. -exists (\big[minr/1]_i \big[minr/1]_j - get (fun e : R => 0 < e /\ ball (x i j) e `<=` P i j)). - apply: ltr_bigminr => // i; apply: ltr_bigminr => // j. - by have /exists2P/getPex [] := x_P i j. -move=> y xmin_y; apply: sPA => i j; have /exists2P/getPex [_] := x_P i j; apply. -apply: ball_ler (xmin_y i j). -by apply: ler_trans (bigminr_ler _ _ i) _; apply: bigminr_ler. +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. -Definition matrix_uniformType_mixin := - Uniform.Mixin mx_ball_center mx_ball_sym mx_ball_triangle mx_locally. +Lemma prod_ent_locallyE : locally = locally_ prod_ent. +Proof. +rewrite predeq2E => xy A; split=> [[B []] | [B [C [entC1 entC2] sCB] sBA]]. + rewrite -!locally_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 -!locally_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. -Canonical matrix_uniformType := - UniformType 'M[T]_(m, n) matrix_uniformType_mixin. +Definition prod_uniformType_mixin := + Uniform.Mixin prod_ent_filter prod_ent_refl prod_ent_inv prod_ent_split + prod_ent_locallyE. -End matrix_Uniform. +End prod_Uniform. -(** product of two uniform spaces *) +Canonical prod_uniformType (U V : uniformType) := + UniformType (U * V) (@prod_uniformType_mixin U V). -Section prod_Uniform. +Lemma flim_entourage2P (U V : uniformType) {F : set (set U)} {G : set (set V)} + {FF : Filter F} {FG : Filter G} (y : U) (z : V): + (F, G) --> (y, z) <-> + forall A, entourage A -> + \forall y' \near F & z' \near G, A ((y,z),(y',z')). +Proof. +split=> [/flim_entourageP FGyz A /FGyz|FGyz]. + by rewrite near_simpl -near2_pair. +by apply/flim_entourageP => A /FGyz; rewrite (near2_pair _ _ (to_set A (y,z))). +Qed. -Context {U V : uniformType}. -Implicit Types (x y : U * V). +(** matrices *) -Definition prod_point : U * V := (point, point). +Section matrix_Uniform. -Definition prod_ball x (eps : R) y := - ball (fst x) eps (fst y) /\ ball (snd x) eps (snd y). +Variables (m n : nat) (T : uniformType). -Lemma prod_ball_center x (eps : R) : 0 < eps -> prod_ball x eps x. -Proof. by move=> /posnumP[e]; split. Qed. +Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)). -Lemma prod_ball_sym x y (eps : R) : prod_ball x eps y -> prod_ball y eps x. -Proof. by move=> [bxy1 bxy2]; split; apply: ball_sym. Qed. +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 prod_ball_triangle x y z (e1 e2 : R) : - prod_ball x e1 y -> prod_ball y e2 z -> prod_ball x (e1 + e2) z. +Lemma mx_ent_filter : Filter mx_ent. Proof. -by move=> [bxy1 bxy2] [byz1 byz2]; split; eapply ball_triangle; eassumption. +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 prod_locally : locally = locally_ prod_ball. +Lemma mx_ent_refl A : mx_ent A -> [set MN | MN.1 = MN.2] `<=` A. 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 => /locallyP [_ /posnumP[ex] eX] /locallyP [_ /posnumP[ey] eY]. -exists (minr ex%:num ey%:num) => // -[x' y'] [/= xx' yy']. -apply: XYP; split=> /=. - by apply/eX/(ball_ler _ xx'); rewrite ler_minl lerr. -by apply/eY/(ball_ler _ yy'); rewrite ler_minl lerr orbT. +move=> [B entB sBA] MN MN1e2; apply: sBA => i j. +by rewrite MN1e2; apply: entourage_refl. Qed. -Definition prod_uniformType_mixin := - Uniform.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_locally. +Lemma mx_ent_inv A : mx_ent A -> mx_ent A^-1. +Proof. +move=> [B entB sBA]; exists (fun i j => (B i j)^-1). + by move=> i j; apply: entourage_inv. +by move=> MN BMN; apply: sBA. +Qed. -End prod_Uniform. +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. -Canonical prod_uniformType (U V : uniformType) := - UniformType (U * V) (@prod_uniformType_mixin U V). +Lemma mx_ent_locallyE : locally = locally_ mx_ent. +Proof. +rewrite predeq2E => M A; split. + move=> [B]; rewrite -locally_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 -locally_entourageE => i j; exists (C i j). +by move=> N CMN; apply/sBA/sCB. +Qed. -Section Locally_fct2. +Definition matrix_uniformType_mixin := + Uniform.Mixin mx_ent_filter mx_ent_refl mx_ent_inv mx_ent_split + mx_ent_locallyE. -Context {T : Type} {U V : uniformType}. +Canonical matrix_uniformType := + UniformType 'M[T]_(m, n) matrix_uniformType_mixin. -Lemma flim_ball2P {F : set (set U)} {G : set (set V)} - {FF : Filter F} {FG : Filter G} (y : U) (z : V): - (F, G) --> (y, z) <-> - forall eps : R, eps > 0 -> \forall y' \near F & z' \near G, - ball y eps y' /\ ball z eps z'. -Proof. exact: flim_ballP. Qed. +End matrix_Uniform. -End Locally_fct2. +Lemma flim_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/flim_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 *) @@ -2714,73 +2763,91 @@ Section fct_Uniform. Variable (T : choiceType) (U : uniformType). -Definition fct_ball (x : T -> U) (eps : R) (y : T -> U) := - forall t : T, ball (x t) eps (y t). +Definition fct_ent := + filter_from + [set P : T -> set (U * U) | forall t, entourage (P t)] + (fun P => [set fg | forall t, P t (fg.1 t, fg.2 t)]). + +Lemma fct_ent_filter : Filter fct_ent. +Proof. +apply: filter_from_filter; first by exists (fun=> setT) => _; apply: filterT. +move=> A B entA entB. +exists (fun t => A t `&` B t); first by move=> ?; apply: filterI. +by move=> fg ABfg; split=> t; have [] := ABfg t. +Qed. -Lemma fct_ball_center (x : T -> U) (e : R) : 0 < e -> fct_ball x e x. -Proof. by move=> /posnumP[{e}e] 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_ball_sym (x y : T -> U) (e : R) : fct_ball x e y -> fct_ball y e x. -Proof. by move=> P t; apply: ball_sym. Qed. +Lemma fct_ent_inv A : fct_ent A -> fct_ent A^-1. +Proof. +move=> [B entB sBA]; exists (fun t => (B t)^-1). + by move=> ?; apply: entourage_inv. +by move=> fg Bgf; apply/sBA. +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_ent_split A : fct_ent A -> exists2 B, fct_ent B & B \o B `<=` A. +Proof. +move=> [B entB sBA]. +have Bsplit t : exists C, entourage C /\ C \o C `<=` B t. + exact/exists2P/entourage_split_ex. +exists [set fg | forall t, + get [set C | entourage C /\ C \o C `<=` B t] (fg.1 t, fg.2 t)]. + by exists (fun t => get [set C | entourage C /\ C \o C `<=` B t]). +move=> fg [h Cfh Chg]; apply/sBA => t; have /getPex [_] := Bsplit t; apply. +by exists (h t); [apply: Cfh|apply: Chg]. +Qed. Definition fct_uniformType_mixin := - UniformMixin fct_ball_center fct_ball_sym fct_ball_triangle erefl. + UniformMixin fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split erefl. Definition fct_topologicalTypeMixin := - topologyOfBallMixin fct_uniformType_mixin. + topologyOfEntourageMixin fct_uniformType_mixin. -Canonical generic_source_filter := @Filtered.Source _ _ _ (locally_ fct_ball). +Canonical generic_source_filter := @Filtered.Source _ _ _ (locally_ fct_ent). Canonical fct_topologicalType := TopologicalType (T -> U) fct_topologicalTypeMixin. Canonical fct_uniformType := UniformType (T -> U) fct_uniformType_mixin. End fct_Uniform. -(** ** Complete uniform spaces *) - -(* :TODO: Use cauchy2 alternative to define cauchy? *) -(* Or not: is the fact that cauchy F -/> ProperFilter F a problem? *) -Definition cauchy_ex {T : uniformType} (F : set (set T)) := - forall eps : R, 0 < eps -> exists x, F (ball x eps). - -Definition cauchy {T : uniformType} (F : set (set T)) := - forall e, e > 0 -> \forall x & y \near F, ball x e y. - -Lemma cauchy_entouragesP (T : uniformType) (F : set (set T)) : - Filter F -> cauchy F <-> (F, F) --> entourages. +(* TODO: is it possible to remove A's dependency in t? *) +Lemma flim_fct_entourageP (T : choiceType) (U : uniformType) + (F : set (set (T -> U))) (FF : Filter F) (f : T -> U) : + F --> f <-> + forall A, (forall t, entourage (A t)) -> + \forall g \near F, forall t, A t (f t, g t). Proof. -move=> FF; 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. +split. + move=> /flim_entourageP Ff A entA. + apply: (Ff [set fg | forall t : T, A t (fg.1 t, fg.2 t)]). + by exists (fun t => A t). +move=> Ff; apply/flim_entourageP => A [P entP sPA]; near=> g. +by apply: sPA => /=; near: g; apply: Ff. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_cauchy_ex {T : uniformType} (F : set (set T)) : - [cvg F in T] -> cauchy_ex F. -Proof. by move=> Fl _/posnumP[eps]; exists (lim F); apply/Fl/locally_ball. 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 => locally_ (@entourage_set U) A). -Lemma cauchy_exP (T : uniformType) (F : set (set T)) : Filter F -> - cauchy_ex F -> cauchy F. -Proof. -move=> FF 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. +(** ** Complete uniform spaces *) -Lemma cauchyP (T : uniformType) (F : set (set T)) : ProperFilter F -> - cauchy F <-> cauchy_ex F. -Proof. -move=> FF; 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. +Definition cauchy {T : uniformType} (F : set (set T)) := (F, F) --> entourage. Lemma cvg_cauchy {T : uniformType} (F : set (set T)) : Filter F -> [cvg F in T] -> cauchy F. -Proof. by move=> FF /cvg_cauchy_ex /cauchy_exP. Qed. +Proof. +move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA. +exists (to_set (B^-1) (lim F), to_set B (lim F)). + split=> /=; apply: cvF; rewrite /= -locally_entourageE; last by exists B. + by exists B^-1 => //; apply: entourage_inv. +by move=> ab [/= Balima Blimb]; apply: sB2A; exists (lim F). +Qed. Module Complete. @@ -2869,15 +2936,17 @@ Lemma mx_complete (F : set (set 'M[T]_(m, n))) : ProperFilter F -> cauchy F -> cvg F. Proof. move=> FF Fc. -have /(_ _ _) /complete_cauchy cvF : +have /(_ _ _) /complete_cauchy /app_flim_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/flim_ballP => _ /posnumP[e]; near=> M => i j. -rewrite mxE; near F => M' => /=; apply: (@ball_splitl _ (M' i j)). - by near: M'; apply/cvF/locally_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/flim_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) => ?? //; apply: entourage_inv. Grab Existential Variables. all: end_near. Qed. Canonical matrix_completeType := CompleteType 'M[T]_(m, n) mx_complete. @@ -2891,12 +2960,15 @@ Context {T : choiceType} {U : completeType}. Lemma fun_complete (F : set (set (T -> U))) {FF : ProperFilter F} : cauchy F -> cvg F. Proof. -move=> Fc; have /(_ _) /complete_cauchy Ft_cvg : cauchy (@^~_ @ F). - by move=> t e ?; rewrite near_simpl; apply: filterS (Fc _ _). +move=> Fc. +have /(_ _) /complete_cauchy /app_flim_entourageP cvF : cauchy (@^~_ @ F). + move=> t A /= entA; rewrite near_simpl -near2E near_map2. + by apply: Fc; exists (fun=> A). apply/cvg_ex; exists (fun t => lim (@^~t @ F)). -apply/flim_ballPpos => e; near=> f => t; near F => g => /=. -apply: (@ball_splitl _ (g t)); first by near: g; exact/Ft_cvg/locally_ball. -by move: (t); near: g; near: f; apply: nearP_dep; apply: filterS (Fc _ _). +apply/flim_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. +by exists (fun t => (split_ent (A t))^-1) => ? //; apply: entourage_inv. Grab Existential Variables. all: end_near. Qed. Canonical fun_completeType := CompleteType (T -> U) fun_complete. @@ -2915,11 +2987,13 @@ Lemma flim_switch_1 {U : uniformType} f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> h @ F1 --> l -> g @ F2 --> l. Proof. -move=> fg fh hl; apply/flim_ballPpos => e. -rewrite near_simpl; near F1 => x1; near=> x2. -apply: (@ball_split _ (h x1)); first by near: x1; apply/hl/locally_ball. -apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/locally_ball. -by move: (x2); near: x1; apply/(flim_ball fg). +move=> fg fh hl; apply/app_flim_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 /flim_fct_entourageP /(_ (fun=> _^-1)):= fg; apply. +by move=> _; apply: entourage_inv. Grab Existential Variables. all: end_near. Qed. Lemma flim_switch_2 {U : completeType} @@ -2928,12 +3002,17 @@ Lemma flim_switch_2 {U : completeType} f @ F1 --> g -> (forall x, f x @ F2 --> h x) -> [cvg h @ F1 in U]. Proof. -move=> fg fh; apply: complete_cauchy => _/posnumP[e]. -rewrite !near_simpl; near=> x1 y1=> /=; near F2 => x2. -apply: (@ball_splitl _ (f x1 x2)); first by near: x2; apply/fh/locally_ball. -apply: (@ball_split _ (f y1 x2)); first by near: x2; apply/fh/locally_ball. -apply: (@ball_splitr _ (g x2)); move: (x2); [near: y1|near: x1]; -by apply/(flim_ball fg). +move=> fg fh; apply: complete_cauchy => 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) _)). + exact: locally_entourage (entourage_inv _). +apply: (entourage_split (g x2)) => //; move: (x2); [near: x1|near: y1]. + have /flim_fct_entourageP /(_ (fun=> _^-1)) := fg; apply=> _. + exact: entourage_inv. +by have /flim_fct_entourageP /(_ (fun=> _)) := fg; apply. Grab Existential Variables. all: end_near. Qed. (* Alternative version *)