diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a..1e7cac042 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,14 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in `topology_structure.v` : + + definitions `separable`, `separable_set` + + lemmas `basisP`, `separableE`, `second_countable_separable`, + `bigcupT_separable`, `bigcup_separable` + +- new file `measurable_topology.v` + + lemmas `salgebra_countable_basis`, `salgebra_open_closedE` + ### Changed - in `realsum.v`: diff --git a/_CoqProject b/_CoqProject index f0b745c7f..98873fe72 100644 --- a/_CoqProject +++ b/_CoqProject @@ -99,6 +99,7 @@ theories/derive.v theories/numfun.v theories/measure_theory/measurable_structure.v +theories/measure_theory/measurable_topology.v theories/measure_theory/measure_function.v theories/measure_theory/counting_measure.v theories/measure_theory/dirac_measure.v diff --git a/theories/measure_theory/measurable_topology.v b/theories/measure_theory/measurable_topology.v new file mode 100644 index 000000000..56546867e --- /dev/null +++ b/theories/measure_theory/measurable_topology.v @@ -0,0 +1,56 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect_compat algebra finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import boolp classical_sets functions cardinality reals. +From mathcomp Require Import measurable_structure topology_structure metric_structure. + +(**md**************************************************************************) +(* # Measure theory applied to topological spaces via the Borel sigma-algebra.*) +(* *) +(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) +(* *) +(* *) +(* ## Mathematical structures *) +(* ```Soon : default display open.-sigma for topological types *) +(* ``` *) +(******************************************************************************) + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import ProperNotations. +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section measurable_topology. +Context {T : topologicalType}. + +Lemma salgebra_countable_basis {B : set_system T} (D : set T) : +countable B -> basis B -> <> = <>. +Proof. +rewrite eqEsubset => /countable_bijP [A /card_esym/pcard_eqP/bijPex/= + [g [fg _ ag]]] /basisP [BO bB]; split. exact: sigma_algebra_sub. +apply: sigma_algebra_subl=> U /bB ->. +have sgU : set_surj (A `&` [set n | g n `<=` U]) (B `&` [set W | W `<=` U]) g. +by rewrite surjE in ag; rewrite surjE=> W [/ag [n An <-]/= gnU]; exists n. +rewrite (reindex_bigcup _ _ _ _ _ sgU). move=> n /= [a u]; split=>//. exact: fg. +rewrite bigcup_mkcond; apply: sigma_algebra_bigcup=> i. case: ifP=>//[|_]. + rewrite in_setE=> [[Ai _]]. apply: sub_sigma_algebra. exact: fg. +exact: sigma_algebra0. +Qed. + +Lemma salgebra_open_closedE : +<> = <>. +Proof. +rewrite eqEsubset; split; apply: sigma_algebra_subl. + move=> U oU; rewrite -(setCK U); apply: (sigma_algebraC (sub_sigma_algebra _)); + exact: open_closedC. +move=> F cF; rewrite -(setCK F); apply: (sigma_algebraC (sub_sigma_algebra _)); +exact: closed_openC. +Qed. + +End measurable_topology. \ No newline at end of file diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 76783da1e..7c05bcc23 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -253,6 +253,9 @@ HB.instance Definition _ (K : numFieldType) m n := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n) (@mx_normZ K m n). +HB.instance Definition _ (K : numFieldType) m n := + isNormedModule.Build _ 'M[K]_(m, n). + End matrix_NormedModule. Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat} diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1252178b3..92255cf69 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -92,11 +92,33 @@ HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -#[short(type="normedModType")] -HB.structure Definition NormedModule (K : numDomainType) := +HB.structure Definition NormedModule0 (K : numDomainType) := {T of PseudoMetricNormedZmod K T & ConvexTvs K T & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. +#[short(type="normedModType")] +HB.structure Definition NormedModule (K : numDomainType) := + {T of NormedModule0 K T & Metric K T}. + +HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. + +HB.builders Context K T & isNormedModule K T. + +Let mdist (x y : T) : K := `|x - y|. + +Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed. + +Let mdist_positivity x y : mdist x y = 0 -> x = y. +Proof. by move=> /normr0_eq0/subr0_eq. Qed. + +Let ballEmdist x d : ball x d = [set y | mdist x y < d]. +Proof. by rewrite -ball_normE. Qed. + +HB.instance Definition _ := + @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist. + +HB.end. + #[short(type="subNormedModType")] HB.structure Definition SubNormedModule (R : numDomainType) (V : normedModType R) (S : pred V) := @@ -1723,7 +1745,7 @@ Qed. Section prod_NormedModule. Context {K : numFieldType} {U V : normedModType K}. -Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. +Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := @@ -1732,6 +1754,9 @@ HB.instance Definition _ := End prod_NormedModule. +HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) := + isNormedModule.Build _ (U * V')%type. + Section prod_NormedModule_lemmas. Context {T : Type} {K : numDomainType} {U V : normedModType K}. @@ -2659,6 +2684,9 @@ HB.instance Definition _ (V : vectType R) := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) (@Norm.normZ _ _ (@max_norm V)). +HB.instance Definition _ (V : vectType R) := + isNormedModule.Build _ (max_space V). + (* NB: Get Trocq to prove the continuity part automatically. *) Lemma sup_closed_ball_compact (V : vectType R) : compact (closed_ball (0 : max_space V) 1). diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index a6170e44b..6388976e2 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -45,6 +45,8 @@ From mathcomp Require Export filter. (* isolated A == the set of isolated points of A *) (* dense S == the set (S : set T) is dense in T, with T of *) (* type topologicalType *) +(* separable T == T has a countable dense subset *) +(* separable_set A == A : set T has a countable dense subset *) (* continuousType == type of continuous functions *) (* The HB structures is Continuous. *) (* mkcts f_cts == object of type continuousType corresponding to *) @@ -122,11 +124,6 @@ Context {T : topologicalType}. Definition open_nbhs (p : T) (A : set T) := open A /\ A p. -Definition basis (B : set_system T) := - B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. - -Definition second_countable := exists2 B, countable B & basis B. - Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). Proof. by apply: nbhs_pfilter_subproof; case: T p => ? []. Qed. Typeclasses Opaque nbhs. @@ -998,6 +995,88 @@ apply/not_implyP; split; first exact: openT. by rewrite setTI => -[]. Qed. +Section basis. +Context {T : topologicalType}. + +Definition basis (B : set (set T)) := + B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. + +(* Maybe rename separable_space*) +Definition separable := exists D : set T, + countable D /\ dense D. + +Definition separable_set (A : set T) := +exists D, + [/\ countable D, D `<=` A & forall O, A`&`O !=set0 -> open O -> O`&`D !=set0]. + +Definition second_countable := exists2 B, countable B & basis B. + +Lemma basisP {B : set_system T} : basis B <-> B `<=`open +/\ (forall U: set T, open U -> U = \bigcup_(V in [set W | B W /\ W `<=`U]) V). +Proof. +split=> [[oB bB]|[Bo dec]]. split=> //U oU. + rewrite eqEsubset /bigcup; split=>[x Ux/=|x [A/= [BA AU] /AU //]]. + have:= bB x. rewrite/cvg_to {2}/nbhs/filter_from/= => /(_ U)/=. + have nT: \near x, U x by apply: (open_in_nearW oU)=>[y|]; rewrite in_setE. + rewrite nbhs_nearE !exists2E/= => /(_ nT). + by under eq_exists=>x0 do rewrite -andA {1}(andC (x0 x) _) andA. +split=>// x. rewrite/cvg_to/=nbhsE/open_nbhs => P /= + [U [/(dec U)->] [A [BA AU] Ax] UP]. exists A=>// t At; apply: UP. by exists A. +Qed. + +(* Could be renamed to separableTE*) +Lemma separableE : separable = separable_set [set:T]. +Proof. +apply: eq_exists=>A. rewrite [X in [/\ _, _ & X]] (_:_ = dense A)//. + by under eq_forall do rewrite setTI. +by rewrite propeqE; split=>[[cA dA]|[cA _ dA]]. +Qed. + +Lemma second_countable_separable : + second_countable -> separable. +Proof. +move=> [B] /(sub_countable (card_le_setD B [set set0])). +rewrite/countable=> /pfcard_geP. case=> [|[f] /basisP [oB bB]]. + rewrite setD_eq0=> /subset_set1. case=> -> /basisP [oB bB]; + have:= (bB [set:T]) openT. rewrite [X in \bigcup_(_ in X) _] (_:_ = set0). + by apply: eq_set=>x/=; rewrite andB. rewrite bigcup0=>//. + move=> T0; exists set0; split=>// O [x /(subsetT O)]. by rewrite T0. + rewrite [X in \bigcup_(_ in X) _] (_:_ = [set set0]). + apply: eq_set=>x/=; rewrite [X in _/\ X] (_:_ = True). + by apply: propT; exact: subsetT. by rewrite andB.1.2. rewrite bigcup_set1. + move=> T0; exists set0; split=>// O [x /(subsetT O)]. by rewrite T0. +have:= image_eq f. rewrite eqEsubset=> [[rfbs bsrf]]. +have: forall n, exists x:T, B (f n) /\ f n x. + move:rfbs=>/[swap] n. rewrite/subset/= => /(_ (f n)). + have:exists2 x, True & f x = f n by exists n. + move=> /[swap] /[apply] [[bfn /eqP /set0P [x fnx]]]. by exists x. +move=> /choice [g gP]. exists (range g). +split=> [|U /[swap] /(bB U) -> /bigcup_nonempty [A/= [BA AU] /set0P /eqP An0]]. + apply: card_image_le. have: (B `\ set0) A by[]. move=> /bsrf [n _ fnA]. +exists (g n). split=>/=. by exists A=>//; rewrite -fnA; +have [_] := gP n. by exists n. +Qed. + +Lemma bigcupT_separable [A : (set T)^nat] : (forall n, separable_set (A n)) -> +separable_set (\bigcup_n A n). +Proof. +move=>/choice [D_ /all_and3 [cDx DAx dDx]]. exists (\bigcup_n D_ n); split. + exact: bigcup_countable. exact: subset_bigcup. move=> O [x [[n _ Anx] Ox] oO]. +have /(dDx n O) /(_ oO) [y [Oy Dny]] : A n `&` O !=set0 by exists x. +by exists y; split=>//; exists n. +Qed. + +Lemma bigcup_separable [A : (set T)^nat] [P : set nat] : +(forall n, P n -> separable_set (A n)) +-> separable_set (\bigcup_(i in P) A i). +Proof. +rewrite bigcup_mkcond => nsPA. apply: bigcupT_separable=>n. +case: ifPn=>[|_]. rewrite in_setE. apply: (nsPA n). +by exists set0; split=>// O [x [F]]. +Qed. + +End basis. + Section ClopenSets. Implicit Type T : topologicalType.