diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ec202fc3dd..1d842d6fdb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -60,6 +60,13 @@ + lemma `countable_bijP` + lemma `patchE` +- in file `topology.v`, + + new definitions `countable_uniformity`, `countable_uniformityT`, + `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and + `product_pseudoMetricType`. + + new lemmas `countable_uniformityP`, `countable_sup_ent`, and + `countable_uniformity_metric`. + - in `constructive_ereal.v`: + lemmas `adde_def_doppeD`, `adde_def_doppeB` + lemma `fin_num_sume_distrr` diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index a6de824911..1e123ee155 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -384,8 +384,7 @@ exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic). apply/esym; rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=. rewrite in_itv/= !natr_absz intr_norm intrD. suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. - rewrite [ltRHS]ger0_norm//; last by rewrite addr_ge0// ler0z floor_ge0. - by rewrite (le_lt_trans _ (lt_succ_floor _)) ?ler_norm. + by rewrite ger0_norm ?addr_ge0 ?ler0z ?floor_ge0// lt_succ_floor. by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry. Qed. diff --git a/theories/real_interval.v b/theories/real_interval.v index 8ca4e888b0..257386fd71 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -175,10 +175,10 @@ Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] = Proof. rewrite predeqE => y; split=> /=; last first. by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy. -rewrite in_itv /= andbT => xy; exists (`|floor y|%N.+1) => //=. -rewrite in_itv /= xy /= -natr1. +rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=. +rewrite in_itv /= xy /=. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_spaddr. -by rewrite natr_absz ger0_norm ?lt_succ_floor// floor_ge0 ltW. +by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor. Qed. Lemma itv_o_inftyEbigcup x : diff --git a/theories/topology.v b/theories/topology.v index 784341730c..747168f662 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -285,6 +285,8 @@ Require Import reals signed. (* unif_continuous f <-> f is uniformly continuous. *) (* weak_uniformType == the uniform space for weak topologies *) (* sup_uniformType == the uniform space for sup topologies *) +(* countable_uniformity T == T's entourage has a countable base. This *) +(* is equivalent to `T` being metrizable *) (* *) (* * PseudoMetric spaces : *) (* entourage_ ball == entourages defined using balls *) @@ -365,6 +367,7 @@ Require Import reals signed. (* *) (* We endow several standard types with the types of topological notions: *) (* - products: prod_topologicalType, prod_uniformType, prod_pseudoMetricType *) +(* sup_pseudoMetricType, weak_pseudoMetricType, product_pseudoMetricType *) (* - matrices: matrix_filtered, matrix_topologicalType, matrix_uniformType, *) (* matrix_pseudoMetricType, matrix_completeType, *) (* matrix_completePseudoMetricType *) @@ -2075,7 +2078,7 @@ End TopologyOfBase. (** ** Topology defined by a subbase of open sets *) Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) := - [set \bigcap_(i in [set i | i \in D']) f i | + [set \bigcap_(i in [set` D']) f i | D' in [set A : {fset I} | {subset A <= D}]]. Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) : @@ -3904,6 +3907,27 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. Unshelve. all: by end_near. Qed. +(* This property is primarily useful only for metrizability on uniform spaces *) +Definition countable_uniformity (T : uniformType) := + exists R : set (set (T * T)), [/\ + countable R, + R `<=` entourage & + forall P, entourage P -> exists2 Q, R Q & Q `<=` P]. + +Lemma countable_uniformityP {T : uniformType} : + countable_uniformity T <-> exists2 f : nat -> set (T * T), + (forall A, entourage A -> exists N, f N `<=` A) & + (forall n, entourage (f n)). +Proof. +split=> [[M []]|[f fsubE entf]]. + move=> /pfcard_geP[-> _ /(_ _ entourageT)[]//|/unsquash f eM Msub]. + exists f; last by move=> n; apply: eM; exact: funS. + by move=> ? /Msub [Q + ?] => /(@surj _ _ _ _ f)[n _ fQ]; exists n; rewrite fQ. +exists (range f); split; first exact: card_image_le. + by move=> E [n _] <-; exact: entf. +by move=> E /fsubE [n fnA]; exists (f n) => //; exists n. +Qed. + Section uniform_closeness. Variable (U : uniformType). @@ -4376,6 +4400,47 @@ Definition sup_uniform_mixin:= Definition sup_uniformType := UniformType Tt sup_uniform_mixin. +Lemma countable_sup_ent : + countable [set: Ii] -> (forall n, countable_uniformity (TS n)) -> + countable_uniformity sup_uniformType. +Proof. +move=> Icnt countable_ent; pose f n := cid (countable_ent n). +pose g (n : Ii) : set (set (T * T)) := projT1 (f n). +have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0. + exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|]. + move=> P [w [A _]] <- subP; exists setT => //. + apply: subset_trans subP; apply: sub_bigcap => i _ ? _. + by suff : [set: I] (projT1 i).1 by rewrite I0. +exists (finI_from (\bigcup_n g n) id); split. +- by apply/finI_from_countable/bigcup_countable => //i _; case: (projT2 (f i)). +- move=> E [A AsubGn AE]; exists E => //. + have h (w : set (T * T)) : { p : IEnt | w \in A -> w = (projT1 p).2 }. + apply cid; have [|] := boolP (w \in A); last first. + by exists (exist ent_of _ (IEnt_pointT i0)). + move=> /[dup] /AsubGn /set_mem [n _ gnw] wA. + suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent). + by apply/asboolP; have [_ + _] := projT2 (f n); exact. + exists [fset sval (h w) | w in A]%fset; first by move=> ?; exact: in_setT. + rewrite -AE; rewrite eqEsubset; split => t Ia. + by move=> w Aw; rewrite (svalP (h w) Aw); apply/Ia/imfsetP; exists w. + case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia. + by rewrite (_ : w = x) // (svalP (h x) xA) -M. +- move=> E [w] [ A _ wIA wsubE]. + have ent_Ip (i : IEnt) : @entourage (TS (projT1 i).1) (projT1 i).2. + by apply/asboolP; exact: (projT2 i). + pose h (i : IEnt) : {x : set (T * T) | _} := cid2 (and3_rec + (fun _ _ P => P) (projT2 (f (projT1 i).1)) (projT1 i).2 (ent_Ip i)). + have ehi (i : IEnt) : ent_of ((projT1 i).1, projT1 (h i)). + apply/asboolP => /=; have [] := projT2 (h i). + by have [_ + _ ? ?] := projT2 (f (projT1 i).1); exact. + pose AH := [fset projT1 (h w) | w in A]%fset. + exists (\bigcap_(i in [set` AH]) i). + exists AH => // p /imfsetP [i iA ->]; rewrite inE //. + by exists (projT1 i).1 => //; have [] := projT2 (h i). + apply: subset_trans wsubE; rewrite -wIA => ? It i ?. + by have [?] := projT2 (h i); apply; apply: It; apply/imfsetP; exists i. +Qed. + End sup_uniform. Section product_uniform. @@ -4704,6 +4769,18 @@ by rewrite /unif_continuous -!entourage_ballE filter_fromP. Qed. End entourages. +Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} : + countable_uniformity T. +Proof. +apply/countable_uniformityP. +exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first. + by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos). +move=> E; rewrite -entourage_ballE => -[e e0 subE]. +exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. +rewrite /= -[leRHS]invrK lef_pinv ?posrE ?invr_gt0// -natr1. +by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor. +Qed. + (** ** Specific pseudoMetric spaces *) (** matrices *) @@ -6004,11 +6081,17 @@ End weak_pseudoMetric. - infinite products of metric spaces are metrizable *) Section countable_uniform. -Context {R : realType} {T : uniformType} (f_ : nat -> set (T * T)). +Context {R : realType} {T : uniformType}. -Hypothesis countableBase : forall A, entourage A -> exists N, f_ N `<=` A. +Hypothesis cnt_unif : @countable_uniformity T. -Hypothesis entF : forall n, entourage (f_ n). +Let f_ := projT1 (cid2 (iffLR countable_uniformityP cnt_unif)). + +Local Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A. +Proof. by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed. + +Let entF : forall n, entourage (f_ n). +Proof. by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed. (* Step 1: We build a nicer base `g` for `entourage` with better assumptions than `f` @@ -6021,14 +6104,12 @@ Local Fixpoint g_ (n : nat) : set (T * T) := if n is S n then let W := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1 else [set: T*T]. -Local Lemma entG (n : nat) : entourage (g_ n). +Let entG (n : nat) : entourage (g_ n). Proof. elim: n => /=; first exact: entourageT. by move=> n entg; apply/entourage_invI; exact: filterI. Qed. -#[local] Hint Resolve entG : core. - Local Lemma symG (n : nat) : ((g_ n)^-1)%classic = g_ n. Proof. by case: n => // n; rewrite eqEsubset; split; case=> ? ?; rewrite /= andC. @@ -6302,6 +6383,38 @@ Definition countable_uniform_pseudoMetricType_mixin := PseudoMetric.Mixin End countable_uniform. +Section sup_pseudometric. +Variable (R : realType) (T : pointedType) (Ii : Type). +Variable (Tc : Ii -> PseudoMetric.class_of R T). + +Hypothesis Icnt : countable [set: Ii]. + +Let I : choiceType := classicType_choiceType Ii. +Let TS := fun i => PseudoMetric.Pack (Tc i). + +Definition countable_uniformityT := @countable_sup_ent T Ii Tc Icnt + (fun i => @countable_uniformity_metric _ (TS i)). + +Definition sup_pseudoMetric_mixin := @countable_uniform_pseudoMetricType_mixin R + (sup_uniformType Tc) countable_uniformityT. + +Definition sup_pseudoMetricType := + PseudoMetricType (sup_uniformType Tc) sup_pseudoMetric_mixin. + +End sup_pseudometric. + +Section product_pseudometric. +Variable (R : realType) (Ii : countType) (Tc : Ii -> pseudoMetricType R). + +Hypothesis Icnt : countable [set: Ii]. + +Definition product_pseudoMetricType := + sup_pseudoMetricType (fun i => PseudoMetric.class + (weak_pseudoMetricType (fun f : dep_arrow_pointedType Tc => f i))) + Icnt. + +End product_pseudometric. + Definition subspace {T : Type} (A : set T) := T. Arguments subspace {T} _ : simpl never. @@ -6561,7 +6674,7 @@ Global Instance subspace_proper_filter {T : topologicalType} (continuous (f : subspace A -> _)).*) Notation "{ 'within' A , 'continuous' f }" := (forall x, cvg_to [filter of fmap f (filter_of (Phantom (subspace A) x))] - [filter of f x]). + [filter of f x]) : classical_set_scope. Section SubspaceRelative. Context {T : topologicalType}.