diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4afa6b239..c809887ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -33,6 +33,13 @@ - in `lebesgue_measure.v`: + lemma `measurable_ball` +- in file `normedtype.v`, + + new lemmas `normal_openP`, `uniform_regular`, + `regular_openP`, and `pseudometric_normal`. +- in file `topology.v`, + + new definition `regular_space`. + + new lemma `ent_closure`. + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized @@ -43,8 +50,14 @@ + rewrote `negligible_integral` to replace the positivity condition with an integrability condition, and added `ge0_negligible_integral`. +- removed dependency in `Rstruct.v` on `normedtype.v`: +- added dependency in `normedtype.v` on `Rstruct.v`: + ### Renamed +- in `normedtype.v`: + + `normal_urysohnP` -> `normal_separatorP`. + ### Generalized ### Deprecated diff --git a/theories/Rstruct.v b/theories/Rstruct.v index fe092e087..299ff3eb2 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -695,7 +695,7 @@ End bigmaxr. End ssreal_struct_contd. -Require Import signed topology normedtype. +Require Import signed topology. Section analysis_struct. @@ -764,8 +764,7 @@ Lemma continuity_pt_dnbhs f x : continuity_pt f x <-> forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps). Proof. -rewrite continuity_pt_cvg' (@cvgrPdist_lt _ [normedModType _ of R^o]). -exact. +by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP. Qed. Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : diff --git a/theories/normedtype.v b/theories/normedtype.v index e6ac94fe1..47ced5e7a 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2,7 +2,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality set_interval. +From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule. (******************************************************************************) @@ -1784,6 +1784,89 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. note="use `cvgrPdist_lt` or a variation instead")] Notation cvg_distP := fcvgrPdist_lt. +(* NB: the following section used to be in Rstruct.v *) +Require Rstruct. + +Section analysis_struct. + +Import Rdefinitions. +Import Rstruct. + +Canonical R_pointedType := [pointedType of R for pointed_of_zmodule R_ringType]. +Canonical R_filteredType := + [filteredType R of R for filtered_of_normedZmod R_normedZmodType]. +Canonical R_topologicalType : topologicalType := TopologicalType R + (topologyOfEntourageMixin + (uniformityOfBallMixin + (@nbhs_ball_normE _ R_normedZmodType) + (pseudoMetric_of_normedDomain R_normedZmodType))). +Canonical R_uniformType : uniformType := + UniformType R + (uniformityOfBallMixin (@nbhs_ball_normE _ R_normedZmodType) + (pseudoMetric_of_normedDomain R_normedZmodType)). +Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType := + PseudoMetricType R (pseudoMetric_of_normedDomain R_normedZmodType). + +(* TODO: express using ball?*) +Lemma continuity_pt_nbhs (f : R -> R) x : + Ranalysis1.continuity_pt f x <-> + forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num). +Proof. +split=> [fcont e|fcont _/RltP/posnumP[e]]; last first. + have [_/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 /= distrC. +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 normr0. +apply/RltP/dx_fxe; split; first by split=> //; apply/eqP. +by have /RltP := xyd; rewrite distrC. +Qed. + +Lemma continuity_pt_cvg (f : R -> R) (x : R) : + Ranalysis1.continuity_pt f x <-> {for x, continuous f}. +Proof. +eapply iff_trans; first exact: continuity_pt_nbhs. +apply iff_sym. +have FF : Filter (f @ x). + by typeclasses eauto. + (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*) +case: (@fcvg_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 eps|{H1} H]. +- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num. + exists x0%:num => //= Hx0' /Hx0 /=. + by rewrite /= distrC; apply. +- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0]. + exists x0%:num => //= y /Hx0 /= {}Hx0. + by rewrite /ball /= distrC. +Qed. + +Lemma continuity_ptE (f : R -> R) (x : R) : + Ranalysis1.continuity_pt f x <-> {for x, continuous f}. +Proof. exact: continuity_pt_cvg. Qed. + +Local Open Scope classical_set_scope. + +Lemma continuity_pt_cvg' f x : + Ranalysis1.continuity_pt f x <-> f @ x^' --> f x. +Proof. by rewrite continuity_ptE continuous_withinNx. Qed. + +Lemma continuity_pt_dnbhs f x : + Ranalysis1.continuity_pt f x <-> + forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps). +Proof. +rewrite continuity_pt_cvg' (@cvgrPdist_lt _ [normedModType _ of R^o]). +exact. +Qed. + +Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : + nbhs (f x) P -> Ranalysis1.continuity_pt f x -> \near x, P (f x). +Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. + +End analysis_struct. + Section open_closed_sets. (* TODO: duplicate theory within the subspace topology of Num.real in a numDomainType *) @@ -4006,7 +4089,7 @@ Qed. End urysohn_facts. End topological_urysohn_separator. -Lemma uniform_separatorW {T : uniformType} (A B : set T) : +Lemma uniform_separatorW {T : uniformType} (A B : set T) : (exists2 E, entourage E & A `*` B `&` E = set0) -> uniform_separator A B. Proof. by case=> E entE AB0; exists (Uniform.class T), E; split => // ?. Qed. @@ -4194,7 +4277,6 @@ Qed. End normal_uniform_separators. End Urysohn. - Lemma uniform_separatorP {T : topologicalType} {R : realType} (A B : set T) : uniform_separator A B <-> exists (f : T -> R), [/\ continuous f, range f `<=` `[0, 1], @@ -4215,34 +4297,118 @@ exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split. exact: open_nbhs_nbhs. Qed. -Lemma normal_urysohnP {T : topologicalType} {R : realType} : - normal_space T <-> - forall (A B : set T), closed A -> closed B -> - A `&` B = set0 -> uniform_separator A B. -Proof. -split; first by move=> *; exact: normal_uniform_separator. +Section normalP. +Context {T : topologicalType}. + +Let normal_spaceP : [<-> + (* 0 *) normal_space T; + (* 1 *) forall (A B : set T), closed A -> closed B -> A `&` B = set0 -> + uniform_separator A B; + (* 2 *) forall (A B : set T), closed A -> closed B -> A `&` B = set0 -> + exists U V, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0] ]. +Proof. +pose R := Rstruct.real_realType. +tfae; first by move=> ?; exact: normal_uniform_separator. +- move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R). + case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1]. + exists (f@^-1` `]-1, 1/2[), (f @^-1` `]1/2, 2[); split. + + by apply: open_comp; [|exact: interval_open]. + + by apply: open_comp; [|exact: interval_open]. + + by apply: fa0 => x/= ->; rewrite (@in_itv _ R)/=; apply/andP; split. + + apply: fb1 => x/= ->; rewrite (@in_itv _ R)/= ltr_pdivr_mulr// mul1r. + by rewrite ltr1n. + + rewrite -preimage_setI ?set_itvoo -subset0 => t [] /andP [_ +] /andP [+ _]. + by move=> /lt_trans /[apply]; rewrite ltxx. move=> + A clA B /set_nbhsP [C [oC AC CB]]. have AC0 : A `&` ~` C = set0 by apply/disjoints_subset; rewrite setCK. -move=> /(_ _ _ clA (open_closedC oC) AC0). -move=> /(@uniform_separatorP _ R) [f [cf f01 fa0 fc1]]. -exists (f@^-1` `]-1, 1/2]). - apply (@filterS _ _ _ (f @^-1` (`]-1, 1/2[))). - by apply: preimage_subset; first exact: subset_itvW. - apply/set_nbhsP; exists (f @^-1` `]-1, 1/2[); split => //. - by apply: open_comp => //; exact: interval_open. - by rewrite set_itvoo=> x Ax /=; rewrite (imsub1 fa0)//; apply/andP; split. -have -> : f @^-1` `]-1, 1/2] = f @^-1` `[0, 1/2]. - rewrite eqEsubset set_itvcc set_itvoc; split. - by move=> x /= /andP [_ ->]; rewrite (itvP (f01 _ _)). - by apply: preimage_subset => z /= /andP[z0 ->]; rewrite (lt_le_trans _ z0). -have: closed (f @^-1` `[0, 1/2]) - by apply: closed_comp => //; apply: interval_closed. -rewrite closure_id => <-. -apply: (subset_trans _ CB); apply/subsetCP. -rewrite preimage_setC set_itvcc => x nCx /=; apply/negP. -by rewrite (imsub1 fc1)// ler01/= -ltNge [ltRHS]splitr ltr_addr. +case/(_ _ _ clA (open_closedC oC) AC0) => U [V] [oU oV AU nCV UV0]. +exists (~` closure V). + apply/set_nbhsP; exists U; split => //. + apply/subsetCr; have := open_closedC oU; rewrite closure_id => ->. + by apply/closure_subset/disjoints_subset; rewrite setIC. +apply/(subset_trans _ CB)/subsetCP; apply: (subset_trans nCV). +apply/subsetCr; have := open_closedC oV; rewrite closure_id => ->. +exact/closure_subset/subsetC/subset_closure. +Qed. + +Lemma normal_openP : normal_space T <-> + forall (A B : set T), closed A -> closed B -> A `&` B = set0 -> + exists U V, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0]. +Proof. exact: (normal_spaceP 0%N 2%N). Qed. + +Lemma normal_separatorP : normal_space T <-> + forall (A B : set T), closed A -> closed B -> A `&` B = set0 -> + uniform_separator A B. +Proof. exact: (normal_spaceP 0%N 1%N). Qed. + +End normalP. + +Section pseudometric_normal. + +Lemma uniform_regular {X : uniformType} : @regular_space X. +Proof. +move=> x A; rewrite /= -nbhs_entourageE => -[E entE]. +move/(subset_trans (ent_closure entE)) => ExA. +by exists [set y | split_ent E (x, y)]; first by exists (split_ent E). Qed. +Lemma regular_openP {T : topologicalType} (x : T) : + {for x, @regular_space T} <-> forall A, closed A -> ~ A x -> + exists U V : set T, [/\ open U, open V, U x, A `<=` V & U `&` V = set0]. +Proof. +split. + move=> + A clA nAx => /(_ (~` A)) []. + by apply: open_nbhs_nbhs; split => //; exact: closed_openC. + move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U). + exists (~` closure U) ; split => //; first exact: open_interior. + exact/closed_openC/closed_closure. + apply/disjoints_subset; rewrite setCK. + exact: (subset_trans (@interior_subset _ _) (@subset_closure _ _)). +move=> + A Ax => /(_ (~` interior A)) []; [|exact|]. + exact/open_closedC/open_interior. +move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U. + exact/open_nbhs_nbhs. +apply: (subset_trans (closure_subset UV)). +move/open_closedC/closure_id : oV => <-. +by apply: (subset_trans cAV); rewrite setCK; exact: interior_subset. +Qed. + +Lemma pseudometric_normal {R : realType} {X : pseudoMetricType R} : + normal_space X. +Proof. +apply/normal_openP => A B clA clB AB0. +have eps' (D : set X) : closed D -> forall x, exists eps : {posnum R}, ~ D x -> + ball x eps%:num `&` D = set0. + move=> clD x; have [nDx|?] := pselect (~ D x); last by exists 1%:pos. + have /regular_openP/(_ _ clD) [//|] := @uniform_regular X x. + move=> U [V] [+ oV] Ux /subsetC BV /disjoints_subset UV0. + rewrite openE /interior => /(_ _ Ux); rewrite -nbhs_ballE => -[]. + move => _/posnumP[eps] beU; exists eps => _; apply/disjoints_subset. + exact: (subset_trans beU (subset_trans UV0 _)). +pose epsA x := projT1 (cid (eps' _ clB x)). +pose epsB x := projT1 (cid (eps' _ clA x)). +exists (\bigcup_(x in A) interior (ball x ((epsA x)%:num / 2)%:pos%:num)). +exists (\bigcup_(x in B) interior (ball x ((epsB x)%:num / 2)%:pos%:num)). +split. +- by apply: bigcup_open => ? ?; exact: open_interior. +- by apply: bigcup_open => ? ?; exact: open_interior. +- by move=> x ?; exists x => //; exact: nbhsx_ballx. +- by move=> y ?; exists y => //; exact: nbhsx_ballx. +- apply/eqP/negPn/negP/set0P => -[z [[x Ax /interior_subset Axe]]]. + case=> y By /interior_subset Bye; have nAy : ~ A y. + by move: AB0; rewrite setIC => /disjoints_subset; exact. + have nBx : ~ B x by move/disjoints_subset: AB0; exact. + have [|/ltW] := leP ((epsA x)%:num / 2) ((epsB y)%:num / 2). + move/ball_sym: Axe => /[swap] /le_ball /[apply] /(ball_triangle Bye). + rewrite -splitr => byx; have := projT2 (cid (eps' _ clA y)) nAy. + by rewrite -subset0; apply; split; [exact: byx|]. + move/ball_sym: Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe). + rewrite -splitr => byx; have := projT2 (cid (eps' _ clB x)) nBx. + by rewrite -subset0; apply; split; [exact: byx|]. +Qed. + +End pseudometric_normal. + Section open_closed_sets_ereal. Variable R : realFieldType (* TODO: generalize to numFieldType? *). Local Open Scope ereal_scope. diff --git a/theories/numfun.v b/theories/numfun.v index a3ddd9329..a30a1c415 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -403,27 +403,23 @@ Context {X : topologicalType} {R : realType}. Local Notation "3" := 3%:R : ring_scope. -Hypothesis urysohn_ext : forall A B, - closed A -> closed B -> A `&` B = set0 -> - exists f : X -> R, [/\ continuous f, - f @` A `<=` [set 0], f @` B `<=` [set 1] & range f `<=` `[0, 1]]. +Hypothesis normalX : normal_space X. Lemma urysohn_ext_itv A B x y : closed A -> closed B -> A `&` B = set0 -> x < y -> exists f : X -> R, [/\ continuous f, f @` A `<=` [set x], f @` B `<=` [set y] & range f `<=` `[x, y]]. Proof. -move=> clA clB AB0 xy; have [f [ctsf f0 f1 f01]] := urysohn_ext clA clB AB0. +move=> cA cB A0 xy; move/normal_separatorP : normalX => urysohn_ext. +have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext _ _ cA cB A0. pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=. -- move=> t; apply: continuous_comp; first exact: ctsf. +- move=> t; apply: continuous_comp; first exact: cf. apply: (@continuousD R [normedModType R of R^o]). apply: continuousM; last exact: cvg_cst. by apply: (@continuousB R [normedModType R of R^o]) => //; exact: cvg_cst. by apply: continuousM; [exact: cvg_id|exact: cvg_cst]. -- rewrite -image_comp; apply: (subset_trans (image_subset _ f0)). - by rewrite image_set1 line_path0. -- rewrite -image_comp; apply: (subset_trans (image_subset _ f1)). - by rewrite image_set1 line_path1. +- by rewrite -image_comp => z /= [? /f0 -> <-]; rewrite line_path0. +- by rewrite -image_comp => z /= [? /f1 -> <-]; rewrite line_path1. - rewrite -image_comp; apply: (subset_trans (image_subset _ f01)). by rewrite range_line_path. Qed. @@ -441,18 +437,18 @@ Local Lemma tietze_step' (f : X -> R) (M : R) : (forall x, `|g x| <= 1/3 * M)]. Proof. move: M => _/posnumP[M] ctsf fA1. -have [] := @urysohn_ext_itv (A `&` f @^-1` `]-oo, -(1/3) * M%:num]) +have [] := @urysohn_ext_itv (A `&` f @^-1` `]-oo, -(1/3) * M%:num]) (A `&` f @^-1` `[1/3 * M%:num,+oo[) (-(1/3) * M%:num) (1/3 * M%:num). - by rewrite closed_setSI; exact: closed_comp. - by rewrite closed_setSI; apply: closed_comp => //; exact: interval_closed. - rewrite setIACA -preimage_setI eqEsubset; split => z // [_ []]. rewrite !set_itvE/= => /[swap] /le_trans /[apply]. by rewrite leNgt mulNr gtr_opp// mulr_gt0// divr_gt0. -- by rewrite mulNr gtr_opp// mulr_gt0//. +- by rewrite mulNr gtr_opp// mulr_gt0. move=> g [ctsg gL3 gR3 grng]; exists g; split => //; first last. by move=> x; rewrite ler_norml -mulNr; apply: grng; exists x. move=> x Ax; have := fA1 _ Ax; rewrite 2!ler_norml => /andP[Mfx fxM]. -have [xL|xL] := lerP (f x) (-(1/3) * M%:num). +have [xL|xL] := leP (f x) (-(1/3) * M%:num). have: [set g x | x in A `&` f@^-1` `]-oo, -(1/3) * M%:num]] (g x) by exists x. move/gL3=> ->; rewrite !mulNr opprK; apply/andP; split. by rewrite -ler_subl_addr -opprD -2!mulrDl natr1 divrr ?unitfE// mul1r. @@ -479,9 +475,9 @@ Let tietze_step (f : X -> R) M : & forall x, `|g x| <= 1/3 * M ]}. Proof. apply: cid. -case : (pselect ({within A, continuous f})); last by move => ?; exists point. -case : (pselect (0 < M)); last by move => ?; exists point. -case : (pselect (forall x, A x -> `|f x| <= M)); last by move => ?; exists point. +have [|?] := pselect ({within A, continuous f}); last by exists point. +have [|?] := ltP 0 M; last by exists point. +have [|?] := pselect (forall x, A x -> `|f x| <= M); last by exists point. by move=> bd pm cf; have [g ?] := tietze_step' pm cf bd; exists g. Qed. @@ -523,13 +519,12 @@ have cvgh' : cvg (h_ @ \oo). rewrite (le_lt_trans (ler_norm_sum _ _ _))//. rewrite (le_lt_trans (ler_sum _ (fun i _ => g_bd i t)))// -mulr_sumr. rewrite -(subnKC MN) geometric_partial_tail. - pose L := - (1/3) * M%:num * ((2/3) ^+ m / (1 - (2/3))). + pose L := (1/3) * M%:num * ((2/3) ^+ m / (1 - (2/3))). apply: (@le_lt_trans _ _ L); first by rewrite ler_pmul2l // geometric_le_lim. rewrite /L onem_twothirds. rewrite [_ ^+ _ * _ ^-1]mulrC mulrA -[x in x < _]ger0_norm; last by []. near: m; near_simpl; move: eps epos. - by apply: (cvgr0_norm_lt (fun _ => _ : R^o)); apply: cvg_geometric. + by apply: (cvgr0_norm_lt (fun _ => _ : R^o)); exact: cvg_geometric. have cvgh : {uniform, h_ @ \oo --> lim (h_ @ \oo)}. by move=> ?; rewrite /= uniform_nbhsT; exact: cvgh'. exists (lim (h_ @ \oo)); split. diff --git a/theories/topology.v b/theories/topology.v index 8fd9776a7..13cb683a0 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -118,6 +118,7 @@ Require Import reals signed. (* eventually true. *) (* clopen U == U is both open and closed *) (* normal_space X == X is normal, sometimes called T4 *) +(* regular_space X == X is regular, sometimes called T3 *) (* separate_points_from_closed f == For a closed set U and point x outside *) (* some member of the family f sends *) (* f_i(x) outside (closure (f_i @` U)). *) @@ -4259,6 +4260,15 @@ Arguments entourage_split {M} z {x y A}. #[global] Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core. +Lemma ent_closure {M : uniformType} (x : M) E : entourage E -> + closure (to_set (split_ent E) x) `<=` to_set E x. +Proof. +pose E' := (split_ent E) `&` ((split_ent E)^-1)%classic. +move=> entE z /(_ [set y | E' (z, y)])[]. + by rewrite -nbhs_entourageE; exists E' => //; exact: filterI. +by move=> y [/=] + [_]; exact: entourage_split. +Qed. + Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x : {for x, continuous f} <-> f @ x^' --> f x. Proof. @@ -7794,9 +7804,12 @@ Qed. End gauges. Definition normal_space (T : topologicalType) := - forall (A : set T), closed A -> + forall A : set T, closed A -> set_nbhs A `<=` filter_from (set_nbhs A) closure. +Definition regular_space (T : topologicalType) := + forall a : T, nbhs a `<=` filter_from (nbhs a) closure. + Section ArzelaAscoli. Context {X : topologicalType}. Context {Y : uniformType}.