diff --git a/theories/derive.v b/theories/derive.v index d33d79b2e1..f2bd7bedf1 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1322,11 +1322,11 @@ move=> leab fcont; set imf := [pred t | t \in f @` [set x | x \in `[a, b]]]. have imf_sup : has_sup imf. apply/has_supP; split. by exists (f a); rewrite !inE; apply/asboolP/imageP; rewrite inE/= lexx. - have [M [Mreal imfltM]] : bounded (f @` [set x | x \in `[a, b]] : set R^o). + have [M [Mreal imfltM]] : bounded_set (f @` [set x | x \in `[a, b]] : set R^o). apply/compact_bounded/continuous_compact; last exact: segment_compact. by move=> ?; rewrite inE => /asboolP /fcont. - exists (M + 1); apply/ubP => y; rewrite !inE => /asboolP /imfltM yltM. - apply/ltW; apply: le_lt_trans (yltM _ _); last by rewrite ltr_addl. + exists (M + 1); apply/ubP => y; rewrite !inE => /asboolP /imfltM yleM. + apply: le_trans (yleM _ _); last by rewrite ltr_addl. by rewrite ler_norm. case: (pselect (exists2 c, c \in `[a, b] & f c = sup imf)) => [|imf_ltsup]. move=> [c cab fceqsup]; exists c => // t tab. @@ -1341,23 +1341,17 @@ have invf_continuous : {in `[a, b], continuous (fun t => 1 / (sup imf - f t) : R move=> t tab; apply: (@lim_inv _ [topologicalType of R^o]). by rewrite neq_lt subr_gt0 orbC imf_ltsup. by apply: cvgD; [apply: continuous_cst|apply: cvgN; apply:fcont]. -have [M [Mreal imVfltM]] : bounded ((fun t => 1 / (sup imf - f t)) @` - [set x | x \in `[a, b]] : set R^o). +have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] : + bounded_set ((fun t => 1 / (sup imf - f t)) @` [set x | x \in `[a, b]] : set R^o). apply/compact_bounded/continuous_compact; last exact: segment_compact. by move=> ?; rewrite inE => /asboolP /invf_continuous. -set k := Num.max (M + 1) 1; have kgt0 : 0 < k by rewrite ltxU ltr01 orbC. have : exists2 y, y \in imf & sup imf - k^-1 < y. by apply: sup_adherent => //; rewrite invr_gt0. move=> [y]; rewrite !inE => /asboolP [t tab <-] {y}. -rewrite ltr_subl_addr - ltr_subl_addl. +rewrite ltr_subl_addr -ltr_subl_addl. suff : sup imf - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->. -rewrite -[X in _ < X]invrK ltr_pinv. - rewrite -div1r; apply: le_lt_trans (ler_norm _) _. - by apply: imVfltM; [rewrite ltxU ltr_addl ltr01|apply: imageP]. - by rewrite inE kgt0 unitfE lt0r_neq0. -have invsupft_gt0 : 0 < (sup imf - f t)^-1. - by rewrite invr_gt0 subr_gt0 imf_ltsup. -by rewrite inE invsupft_gt0 unitfE lt0r_neq0. +rewrite -[X in _ < X]invrK ltf_pinv ?qualifE ?invr_gt0 ?subr_gt0 ?imf_ltsup//. +by rewrite -div1r (le_lt_trans (ler_norm _) _) ?imVfltk//; apply: imageP. Qed. Lemma EVT_min (R : realType) (f : R^o -> R^o) (a b : R^o) : diff --git a/theories/normedtype.v b/theories/normedtype.v index b107870e96..baad79357d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -38,7 +38,22 @@ Require Import classical_sets posnum topology prodnormedzmodule. (* `|x| == the norm of x (notation from ssrnum). *) (* ball_norm == balls defined by the norm. *) (* locally_norm == neighborhoods defined by the norm. *) -(* bounded == set of bounded sets. *) +(* *) +(* * Domination notations: *) +(* dominated_by h k f F == `|f| <= k * `|h|, near F *) +(* bounded_on f F == f is bounded near F *) +(* [bounded f x | x in A] == f is bounded on A, ie F := globally A *) +(* [locally [bounded f x | x in A] == f is locally bounded on A *) +(* bounded_set == set of bounded sets. *) +(* := [set A | [bounded x | x in A]] *) +(* bounded_fun == set of bounded functions. *) +(* := [set f | [bounded f x | x in setT]] *) +(* lipshitz_on f F == f is lipshitz near F *) +(* [lipshitz f x | x in A] == f is lipshitz on A *) +(* [locally [lipshitz f x | x in A] == f is locally lipshitz on A *) +(* k.-lipshitz_on f F == f is k.-lipshitz near F *) +(* k.-lipshitz_A f == f is k.-lipshitz on A *) +(* [locally k.-lipshitz_A f] == f is locally k.-lipshitz on A *) (* *) (* * Complete normed modules : *) (* completeNormedModType K == interface type for a complete normed *) @@ -742,11 +757,19 @@ by move=> x; rewrite -ltr_pdivl_mulr //; apply: AM. Qed. Lemma locally_pinfty_gt (c : {posnum R}) : \forall x \near +oo, c%:num < x. -Proof. by exists c%:num; split => // ; rewrite realE posnum_ge0. Qed. +Proof. by exists c%:num; split => // ; rewrite realE posnum_ge0. Qed. Lemma locally_pinfty_ge (c : {posnum R}) : \forall x \near +oo, c%:num <= x. Proof. by exists c%:num; rewrite realE posnum_ge0; split => //; apply: ltW. Qed. +Lemma locally_pinfty_gt_real (c : R) : c \is Num.real -> + \forall x \near +oo, c < x. +Proof. by exists c. Qed. + +Lemma locally_pinfty_ge_real (c : R) : c \is Num.real -> + \forall x \near +oo, c <= x. +Proof. by exists c; split => //; apply: ltW. Qed. + End infty_locally_instances. Hint Extern 0 (is_true (0 < _)) => match goal with @@ -858,7 +881,16 @@ End NormedModule. Export NormedModule.Exports. -Fail Canonical R_NormedModule := [normedModType Rdefinitions.R of Rdefinitions.R^o]. +Lemma R_normZ (R : numDomainType) (l : R) (x : R^o) : + `| l *: x | = `| l | * `| x |. +Proof. by rewrite normrM. Qed. + +Definition numFieldType_NormedModMixin (R : numFieldType) := + NormedModMixin (@R_normZ R). +Canonical numFieldType_normedModType (R : numFieldType) := + NormedModType R R^o (numFieldType_NormedModMixin R). + +Canonical R_NormedModule := [normedModType Rdefinitions.R of Rdefinitions.R^o]. Section NormedModule_numDomainType. Variables (R : numDomainType) (V : normedModType R). @@ -941,6 +973,190 @@ End NormedModule_numDomainType. Hint Resolve normr_ge0 : core. Arguments cvg_norm {_ _ F FF}. +Lemma pinfty_ex_gt {R : numFieldType} (m : R) (A : set R) : m \is Num.real -> + (\forall k \near +oo, A k) -> exists2 M, m < M & A M. +Proof. +by move=> m_real Agt; near (pinfty_locally R) => M; + exists M; near: M => //; exists m. +Grab Existential Variables. all: end_near. Qed. + +Lemma pinfty_ex_gt0 {R : numFieldType} (A : set R) : + (\forall k \near +oo, A k) -> exists2 M, M > 0 & A M. +Proof. by apply: pinfty_ex_gt; rewrite real0. Qed. + +Definition self_sub (K : numDomainType) (V W : normedModType K) + (f : V -> W) (x : V * V) : W := f x.1 - f x.2. +Arguments self_sub {K V W} f x /. + +Definition fun1 {T : Type} {K : numFieldType} : + T -> [normedModType K of K^o] := fun=> 1. +Arguments fun1 {T K} x /. + +Definition dominated_by {T : Type} {K : numDomainType} {V W : normedModType K} + (h : T -> V) (k : K) (f : T -> W) (F : set (set T)) := + F [set x | `|f x| <= k * `|h x|]. + +Definition strictly_dominated_by {T : Type} {K : numDomainType} {V W : normedModType K} + (h : T -> V) (k : K) (f : T -> W) (F : set (set T)) := + F [set x | `|f x| < k * `|h x|]. + +Lemma sub_dominatedl (T : Type) (K : numFieldType) (V W : normedModType K) + (h : T -> V) (k : K) (F G : set (set T)) : F `=>` G -> + (@dominated_by T K V W h k)^~ G `<=` (dominated_by h k)^~ F. +Proof. by move=> FG f; exact: FG. Qed. + +Lemma sub_dominatedr (T : Type) (K : numFieldType) (V : normedModType K) + (h : T -> V) (k : K) (f g : T -> V) (F : set (set T)) (FF : Filter F) : + (\forall x \near F, `|f x| <= `|g x|) -> + dominated_by h k g F -> dominated_by h k f F. +Proof. by move=> le_fg; apply: filterS2 le_fg => x; apply: le_trans. Qed. + +Lemma dominated_by1 {T : Type} {K : numFieldType} {V : normedModType K} : + @dominated_by T K _ V fun1 = fun k f F => F [set x | `|f x| <= k]. +Proof. +rewrite funeq3E => k f F. +by congr F; rewrite funeqE => x; rewrite normr1 mulr1. +Qed. + +Lemma strictly_dominated_by1 {T : Type} {K : numFieldType} {V : normedModType K} : + @strictly_dominated_by T K _ V fun1 = fun k f F => F [set x | `|f x| < k]. +Proof. +rewrite funeq3E => k f F. +by congr F; rewrite funeqE => x; rewrite normr1 mulr1. +Qed. + +Lemma ex_dom_bound {T : Type} {K : numFieldType} {V W : normedModType K} + (h : T -> V) (f : T -> W) (F : set (set T)) {PF : ProperFilter F}: + (\forall M \near +oo, dominated_by h M f F) <-> + exists M, dominated_by h M f F. +Proof. +rewrite /dominated_by; split => [/pinfty_ex_gt0[M M_gt0]|[M]] FM. + by exists M. +have [] := pselect (exists x, (h x != 0) && (`|f x| <= M * `|h x|)); last first. + rewrite -forallN; move=> Nex; exists 0; rewrite real0; split => //. + move=> k k_gt0; apply: filterS FM => x f_le_Mh. + have /negP := Nex x; rewrite negb_and negbK f_le_Mh orbF => /eqP h_eq0. + by rewrite h_eq0 normr0 !mulr0 in f_le_Mh *. +case => x0 /andP[hx0_neq0] /(le_trans (normr_ge0 _)) /ger0_real. +rewrite realrM // ?normr_eq0// => M_real. +exists M; split => // k Mk; apply: filterS FM => x /le_trans->//. +by rewrite ler_wpmul2r// ltW. +Qed. + +Lemma ex_strict_dom_bound {T : Type} {K : numFieldType} {V W : normedModType K} + (h : T -> V) (f : T -> W) (F : set (set T)) {PF : ProperFilter F} : + (\forall x \near F, h x != 0) -> + (\forall M \near +oo, dominated_by h M f F) <-> + exists M, strictly_dominated_by h M f F. +Proof. +move=> hN0; rewrite ex_dom_bound /dominated_by /strictly_dominated_by. +split => -[] M FM; last by exists M; apply: filterS FM => x /ltW. +exists (M + 1); apply: filterS2 hN0 FM => x hN0 /le_lt_trans->//. +by rewrite ltr_pmul2r ?normr_gt0// ltr_addl. +Qed. + +Definition bounded_on {T : Type} {K : numFieldType} {V : normedModType K} + (f : T -> V) (F : set (set T)) := + \forall M \near +oo, F [set x | `|f x| <= M]. + +Lemma boundedE {T : Type} {K : numFieldType} {V : normedModType K} : + @bounded_on T K V = fun f F => \forall M \near +oo, dominated_by fun1 M f F. +Proof. by rewrite dominated_by1. Qed. + +Lemma sub_boundedr (T : Type) (K : numFieldType) (V : normedModType K) + (F G : set (set T)) : F `=>` G -> + (@bounded_on T K V)^~ G `<=` bounded_on^~ F. +Proof. by move=> FG f; rewrite /bounded_on; apply: filterS => M; apply: FG. Qed. + +Lemma sub_boundedl (T : Type) (K : numFieldType) (V : normedModType K) + (f g : T -> V) (F : set (set T)) (FF : Filter F) : + (\forall x \near F, `|f x| <= `|g x|) -> bounded_on g F -> bounded_on f F. +Proof. +move=> le_fg; rewrite /bounded_on; apply: filterS => M. +by apply: filterS2 le_fg => x; apply: le_trans. +Qed. + +Lemma ex_bound {T : Type} {K : numFieldType} {V : normedModType K} + (f : T -> V) (F : set (set T)) {PF : ProperFilter F}: + bounded_on f F <-> exists M, F [set x | `|f x| <= M]. +Proof. by rewrite boundedE ex_dom_bound dominated_by1. Qed. + +Lemma ex_strict_bound {T : Type} {K : numFieldType} {V : normedModType K} + (f : T -> V) (F : set (set T)) {PF : ProperFilter F}: + bounded_on f F <-> exists M, F [set x | `|f x| < M]. +Proof. +rewrite boundedE ex_strict_dom_bound ?strictly_dominated_by1//. +by near=> x; rewrite oner_eq0. +Grab Existential Variables. all: end_near. Qed. + +Lemma ex_strict_bound_gt0 {T : Type} {K : numFieldType} {V : normedModType K} + (f : T -> V) (F : set (set T)) {PF : Filter F}: + bounded_on f F -> exists2 M, M > 0 & F [set x | `|f x| < M]. +Proof. +move=> /pinfty_ex_gt0[M M_gt0 FM]; exists (M + 1); rewrite ?addr_gt0//. +by apply: filterS FM => x /le_lt_trans->//; rewrite ltr_addl. +Qed. + +Notation "[ 'bounded' E | x 'in' A ]" := (bounded_on (fun x => E) (globally A)) + (at level 0, x ident, format "[ 'bounded' E | x 'in' A ]"). +Notation bounded_set := [set A | [bounded x | x in A]]. +Notation bounded_fun := [set f | [bounded f x | x in setT]]. + +Lemma bounded_locally (T : topologicalType) + (R : numFieldType) (V : normedModType R) (A : set T) (f : T -> V) : + [bounded f x | x in A] -> [locally [bounded f x | x in A]]. +Proof. by move=> /sub_boundedr AB x Ax; apply: AB; apply: within_locallyW. Qed. + +Notation "k .-lipshitz_on f" := (dominated_by (self_sub id) k (self_sub f)) + (at level 2, format "k .-lipshitz_on f") : type_scope. + +Definition sub_klipshitz (K : numFieldType) (V W : normedModType K) (k : K) + (f : V -> W) (F G : set (set (V * V))) : + F `=>` G -> k.-lipshitz_on f G -> k.-lipshitz_on f F. +Proof. exact. Qed. + +Definition lipshitz_on (K : numFieldType) (V W : normedModType K) + (f : V -> W) (F : set (set (V * V))) := + \forall M \near +oo, M.-lipshitz_on f F. + +Definition sub_lipshitz (K : numFieldType) (V W : normedModType K) + (f : V -> W) (F G : set (set (V * V))) : + F `=>` G -> lipshitz_on f G -> lipshitz_on f F. +Proof. by move=> FG; rewrite /lipshitz_on; apply: filterS => M; apply: FG. Qed. + +Lemma klipshitzW (K : numFieldType) (V W : normedModType K) (k : K) + (f : V -> W) (F : set (set (V * V))) {PF : ProperFilter F} : + k.-lipshitz_on f F -> lipshitz_on f F. +Proof. by move=> f_lip; apply/ex_dom_bound; exists k. Qed. + +Notation "k .-lipshitz_ A f" := + (k.-lipshitz_on f (globally (A `*` A))) + (at level 2, A at level 0, format "k .-lipshitz_ A f"). +Notation "k .-lipshitz f" := (k.-lipshitz_setT f) + (at level 2, format "k .-lipshitz f") : type_scope. +Notation "[ 'lipshitz' E | x 'in' A ]" := + (lipshitz_on (fun x => E) (globally (A `*` A))) + (at level 0, x ident, format "[ 'lipshitz' E | x 'in' A ]"). +Notation lipshitz f := [lipshitz f x | x in setT]. + +Lemma klipshitz_locally (R : numFieldType) (V W : normedModType R) + (k : R) (f : V -> W) (A : set V) : + k.-lipshitz_A f -> [locally k.-lipshitz_A f]. +Proof. +by move=> bndf x Ax; apply: sub_klipshitz bndf; apply: within_locallyW. +Qed. + +Lemma lipshitz_locally (R : numFieldType) (V W : normedModType R) + (A : set V) (f : V -> W) : + [lipshitz f x | x in A] -> [locally [lipshitz f x | x in A]]. +Proof. +by move=> bndf x Ax; apply: sub_lipshitz bndf; apply: within_locallyW. +Qed. + +Lemma lipshitz_id (R : numFieldType) (V : normedModType R) : 1.-lipshitz (@id V). +Proof. by move=> [/= x y] _; rewrite mul1r. Qed. +Arguments lipshitz_id {R V}. + Section NormedModule_numFieldType. Variables (R : numFieldType) (V : normedModType R). Implicit Types (x y z : V). @@ -1019,25 +1235,21 @@ move=> cv; apply/cvg_normP => _/posnumP[e]; near=> x. by apply: normm_leW => //; near: x; apply: cv. Grab Existential Variables. all: end_near. Qed. -Lemma cvg_bounded_real {F : set (set V)} {FF : Filter F} (y : V) : - F --> y -> - \forall M \near +oo, M \is Num.real /\ \forall y' \near F, `|y'| < M. +Lemma cvgi_map_lim {T} {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) : + F (fun x : T => is_subset1 (f x)) -> + f `@ F --> l -> lim (f `@ F) = l. Proof. -move=> /cvg_norm Fy; exists `|y|; rewrite normr_real; split => // M. -rewrite -subr_gt0 => subM_gt0; split. - rewrite -comparabler0 (@comparabler_trans _ (M - `|y|)) //. - by rewrite -subr_comparable0 opprD addrA subrr add0r opprK comparabler0 - normr_real. - by rewrite comparablerE subr0 realE ltW. -have := Fy _ subM_gt0. -apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|y|)). -rewrite (le_lt_trans _ yy') // (le_trans _ (ler_dist_dist _ _)) // distrC. -by rewrite real_ler_norm // realB. +move=> f_prop f_l; apply: get_unique => // l' f_l'. +exact: cvgi_unique _ f_l' f_l. Qed. Lemma cvg_bounded {F : set (set V)} {FF : Filter F} (y : V) : - F --> y -> \forall M \near +oo, \forall y' \near F, `|y'| < M. -Proof. move/cvg_bounded_real; by apply: filterS => x []. Qed. + F --> y -> bounded_on id F. +Proof. +move=> /cvg_norm Fy; exists `|y|; rewrite normr_real; split => //= M. +rewrite -subr_gt0 => /Fy; apply: filterS => y' yy'; apply: ltW. +by rewrite -(@ltr_add2r _ (- `|y|)) (le_lt_trans (ler_sub_dist _ _))// distrC. +Qed. End NormedModule_numFieldType. Arguments cvg_bounded {_ _ F FF}. @@ -1710,15 +1922,6 @@ Arguments cvg_norm2 {_ _ _ F G FF FG}. Canonical AbsRing_NormedModType (K : absRingType) := NormedModType K K^o (AbsRing_NormedModMixin _).*) -Lemma R_normZ (R : numDomainType) (l : R) (x : R^o) : - `| l *: x | = `| l | * `| x |. -Proof. by rewrite normrM. Qed. - -Definition numFieldType_NormedModMixin (R : numFieldType) := - NormedModMixin (@R_normZ R). -Canonical numFieldType_normedModType (R : numFieldType) := - NormedModType R R^o (numFieldType_NormedModMixin R). - (** Normed vector spaces have some continuous functions *) Section NVS_continuity. @@ -1754,9 +1957,11 @@ rewrite (@distm_lt_split _ _ (k *: z)) // -?(scalerBr, scalerBl) normmZ. by rewrite ler_addl. rewrite -ltr_pdivl_mull // ?(lt_le_trans ltr01) ?ler_addr //; near: z. by apply: cvg_norm; rewrite // mulr_gt0 // ?invr_gt0 ltr_paddl. -have zM : @normr _ V z < M. +have zM : @normr _ V z <= M. by near: z; near: M; apply: cvg_bounded; apply: cvg_refl. rewrite (le_lt_trans (ler_pmul _ _ (lexx _) (_ : _ <= M))) // ?ltW //. +have : M >= 0 := le_trans (normr_ge0 _) zM. +rewrite le_eqVlt => /predU1P[<-|M_gt0]; first by rewrite mulr0. rewrite -ltr_pdivl_mulr ?(le_lt_trans _ zM) //. near: l; apply: (cvg_norm (_ : K^o)) => //. by rewrite divr_gt0 //; near: M; exists 0; rewrite real0. @@ -2101,19 +2306,16 @@ Local Notation "'+oo'" := (@pinfty_locally K). (* TODO: simplify using extremumP when PR merged in mathcomp *) Lemma cvg_seq_bounded {V : normedModType K} (a : nat -> V) : - [cvg a in V] -> {M | forall n, `|a n| <= M}. -Proof. -move=> a_cvg; suff: exists M, M \is Num.real /\ forall n, `|a n| <= M. - by move=> /(@getPex [pointedType of K^o]) [?]; set M := get _; exists M. -near +oo => M. -have [//|Mreal [N _ /(_ _ _) /ltW a_leM]] := !! near (cvg_bounded_real a_cvg) M. -exists (maxr `|M|%:nng (\big[maxr/0%:nng]_(n < N) `|a (val (rev_ord n))|%:nng))%:nngnum. -split => [|/= n]; first by rewrite realE nng_lexU normr_ge0. -rewrite nng_lexU; have [nN|nN] := leqP N n. - by rewrite (@le_trans _ _ M) //=; [exact: a_leM | rewrite real_ler_norm]. -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 /= nng_lexU ?a_le ?lexx ?orbT. + cvg a -> bounded_fun a. +Proof. +move=> /cvg_bounded/ex_bound => -[/= Moo]; rewrite !near_simpl. +rewrite [(\near a, _ <= _)](near_map _ \oo) => -[N _ /(_ _) a_leM]. +have Moo_real : Moo \is Num.real by rewrite ger0_real ?(le_trans _ (a_leM N _)). +rewrite /bounded_on /=; near=> M => n _. +have [nN|nN]/= := leqP N n. + by apply: (le_trans (a_leM _ _)) => //; near: M; apply: locally_pinfty_ge_real. +move: n nN; suff /(_ (Ordinal _)) : forall n : 'I_N, `|a n| <= M by []. +by near: M; apply: filter_forall => i; apply: locally_pinfty_ge_real. Grab Existential Variables. all: end_near. Qed. End cvg_seq_bounded. @@ -2565,14 +2767,8 @@ Qed. (* by apply (Hd (u, v)) => /=; split; apply sub_abs_ball; rewrite absrB. *) (* Qed. *) -Section bounded. -Variable K : numFieldType. -Definition bounded (V : normedModType K) (A : set V) := - \forall M \near +oo, A `<=` [set x | `|x| < M]. -End bounded. - Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) : - compact A -> bounded A. + compact A -> bounded_set A. Proof. rewrite compact_cover => Aco. have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R]. @@ -2586,7 +2782,8 @@ have /Aco [] := covA. move=> D _ DcovA. exists (\big[maxr/0]_(i : D) (fsval i)%:~R). rewrite bigmaxr_real ?real0 //; split => //. -move=> x ltmaxx p /DcovA [n Dn /lt_trans]; apply; apply: le_lt_trans ltmaxx. +move=> x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW]. +apply; apply: le_lt_trans ltmaxx. have {} : n \in enum_fset D by []. rewrite enum_fsetE => /mapP[/= i iD ->]; exact/BigmaxBigminr.ler_bigmaxr. Qed. @@ -2649,16 +2846,16 @@ by have [g []] := clGf _ _ GC f_D; exists (\row_j (g j : T)). Qed. Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R^o]_n.+1) : - bounded A -> closed A -> compact A. + bounded_set A -> closed A -> compact A. Proof. move=> [M [Mreal normAltM]] Acl. have Mnco : compact [set v : 'rV[R^o]_n.+1 | (forall i, (v ord0 i) \in `[(- (M + 1)), (M + 1)])]. apply: (@rV_compact [topologicalType of R^o] _ (fun _ => [set x | x \in `[(- (M + 1)), (M + 1)]])). by move=> _; apply: segment_compact. -apply: subclosed_compact Acl Mnco _ => v /normAltM normvltM i. -suff /ltW : `|v ord0 i : R^o| < M + 1 by rewrite ler_norml. -apply: le_lt_trans (normvltM _ _); last by rewrite ltr_addl. +apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i. +suff : `|v ord0 i : R^o| <= M + 1 by rewrite ler_norml. +apply: le_trans (normvleM _ _); last by rewrite ltr_addl. have /mapP[j Hj ->] : `|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 [in X in _ <= X]/normr /= mx_normrE. diff --git a/theories/topology.v b/theories/topology.v index 052ff05bcb..a3c2f11e72 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -85,6 +85,7 @@ Require Import boolp Rstruct classical_sets posnum. (* (fun x => E). *) (* f `@ F == image of the canonical filter *) (* associated to F by the relation f. *) +(* globally A == filter of the sets containing A. *) (* at_point a == filter of the sets containing a. *) (* within D F == restriction of the filter F to the *) (* domain D. *) @@ -196,6 +197,10 @@ Require Import boolp Rstruct classical_sets posnum. (* cover-based definition of compactness. *) (* connected A <-> the only non empty subset of A which *) (* is both open and closed in A is A. *) +(* [locally P] := forall a, A a -> *) +(* G (within A (locally x)) *) +(* if P is convertible to G (globally A)*) +(* *) (* --> We used these topological notions to prove Tychonoff's Theorem, which *) (* states that any product of compact sets is compact according to the *) (* product topology. *) @@ -605,21 +610,6 @@ split; last by exists P. by move=> [Q [FQ QP]]; apply: (filterS QP). Qed. -Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) - (F : set (set T)) : - Filter F -> (forall i, i \in D -> F (f i)) -> - F (\bigcap_(i in [set i | i \in D]) f i). -Proof. -move=> FF FfD. -suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. -have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. -elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. -apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). - by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. -apply: filterI; first by apply: FfD; rewrite inE eq_refl. -by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. -Qed. - Structure filter_on T := FilterType { filter :> (T -> Prop) -> Prop; _ : Filter filter @@ -913,6 +903,30 @@ move=> FF BN0; apply: Build_ProperFilter=> P [i Di BiP]. by have [x Bix] := BN0 _ Di; exists x; apply: BiP. Qed. +Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T) + (F : set (set T)) : + Filter F -> (forall i, i \in D -> F (f i)) -> + F (\bigcap_(i in [set i | i \in D]) f i). +Proof. +move=> FF FfD. +suff: F [set p | forall i, i \in enum_fset D -> f i p] by []. +have {FfD} : forall i, i \in enum_fset D -> F (f i) by move=> ? /FfD. +elim: (enum_fset D) => [|i s ihs] FfD; first exact: filterS filterT. +apply: (@filterS _ _ _ (f i `&` [set p | forall i, i \in s -> f i p])). + by move=> p [fip fsp] j; rewrite inE => /orP [/eqP->|] //; apply: fsp. +apply: filterI; first by apply: FfD; rewrite inE eq_refl. +by apply: ihs => j sj; apply: FfD; rewrite inE sj orbC. +Qed. + +Lemma filter_forall T (I : finType) (f : I -> set T) (F : set (set T)) : + Filter F -> (forall i : I, \forall x \near F, f i x) -> + \forall x \near F, forall i, f i x. +Proof. +move=> FF fIF; apply: filterS (@filter_bigI T I [fset x in I]%fset f F FF _). + by move=> x fIx i; have := fIx i; rewrite inE/=; apply. +by move=> i; rewrite inE/= => _; apply: (fIF i). +Qed. + (** ** Limits expressed with filters *) Definition fmap {T U : Type} (f : T -> U) (F : set (set T)) := @@ -1027,6 +1041,23 @@ move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G). by apply: filter_app fFG; near=> y => /=; apply: filterS => x /= ->; near: y. Grab Existential Variables. all: by end_near. Qed. +(* globally filter *) + +Definition globally {T : Type} (A : set T) : set (set T) := + [set P : set T | forall x, A x -> P x]. +Arguments globally {T} A _ /. + +Global Instance globally_filter {T : Type} (A : set T) : + Filter (globally A). +Proof. +constructor => //= P Q; last by move=> PQ AP x /AP /PQ. +by move=> AP AQ x Ax; split; [apply: AP|apply: AQ]. +Qed. + +Global Instance globally_properfilter {T : Type} (A : set T) a : + infer (A a) -> ProperFilter (globally A). +Proof. by move=> Aa; apply: Build_ProperFilter' => /(_ a). Qed. + (** ** Specific filters *) Section at_point. @@ -1517,6 +1548,24 @@ Proof. by apply: cvg_fconst; near=> x0. Grab Existential Variables. all: end_near. Qed. Arguments cvg_const {T U F FF} x. +(* Relation between globally and within A (locally x) *) +(* to be combined with lemmas such as boundedP in normedtype *) +Lemma within_locallyW {T : topologicalType} (A : set T) (x : T) : + A x -> within A (locally x) `=>` globally A. +Proof. +move=> Ax P AP; rewrite /within; near=> y; apply: AP. +Grab Existential Variables. all: end_near. Qed. + +(* [locally P] replaces a (globally A) in P by a within A (locally x) *) +(* Can be combined with a notation taking a filter as a its last argument *) +Definition locally_of (T : topologicalType) (A : set T) + (P : set (set T) -> Prop) of phantom Prop (P (globally A)) := + forall x, A x -> P (within A (locally x)). +Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)) + (at level 0, format "[ 'locally' P ]"). +(* e.g. [locally [bounded f x | x in A]] *) +(* see lemmas bounded_locally for example *) + (** ** Topology defined by a filter *) Section TopologyOfFilter. @@ -1897,7 +1946,7 @@ Proof. by move=> F G H A fFA ; exact: H (preimage f A) fFA. Qed. Lemma cvg_within_filter {T U} {f : T -> U} (F : set (set T)) {FF : (Filter F) } (G : set (set U)) : forall (D : set T), (f @ F) --> G -> (f @ within D F) --> G. -Proof. move=> ?; exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed. +Proof. move=> ?; exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed. Lemma cvg_app_within {T} {U : topologicalType} (f : T -> U) (F : set (set T)) (D : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F).