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..eace6f066 --- /dev/null +++ b/theories/measure_theory/measurable_topology.v @@ -0,0 +1,142 @@ +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 all_reals. +From mathcomp Require Import measurable_structure topology. +From mathcomp Require Import normed_module real_interval. + +(**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.Def Num.Theory. +Import numFieldTopology.Exports. + +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. + +Section measurable_real. +Context {R : realType}. +Definition ocitv := [set `]ab.1,ab.2]%classic | ab in [set:R*R]]. + +Lemma is_ocitv a b : ocitv `]a, b]%classic. +Proof. by exists (a, b). Qed. +Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core. + +Lemma salgebra_measurable {T : choiceType} (G : set_system T) : + <> = G.-sigma.-measurable. +Proof. by rewrite/measurable. Qed. + +Lemma ocitv_measurable_set1 (r : R) : + measurable [set r : g_sigma_algebraType ocitv]. +Proof. +rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. +exact: sub_sigma_algebra. +Qed. +#[local] Hint Resolve ocitv_measurable_set1 : core. + +Lemma ocitv_measurable_itv (i : interval R) : <> [set` i]. +Proof. +rewrite salgebra_measurable. +have moc (a b : R) : measurable (`]a, b] : set (g_sigma_algebraType ocitv)). + by apply: sub_sigma_algebra. +have mopoo (x : R) : measurable (`]x, +oo[ : set (g_sigma_algebraType ocitv)). + by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. +have mnooc (x : R) : measurable (`]-oo, x] : set (g_sigma_algebraType ocitv)). + by rewrite -setCitvr; exact/measurableC. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. + by rewrite setDitv1r. +have moo (a b : R) : measurable (`]a, b[ : set (g_sigma_algebraType ocitv)). + rewrite ooE; exact: measurableD. +have mcc (a b : R) : measurable (`[a, b] : set (g_sigma_algebraType ocitv)). + case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU_1itvob//; apply/measurableU. +have mco (a b : R) : measurable (`[a, b[ : set (g_sigma_algebraType ocitv)). + case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU_1itvob//; apply/measurableU. +have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. + by rewrite setDitv1r. +case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. +- by rewrite -setU_1itvob//; exact/measurableU. +- by rewrite oooE; exact/measurableD. +- by rewrite set_itvNyy. +Qed. +#[local] Hint Resolve ocitv_measurable_itv : core. + + +Lemma open_octiv_measurable (U : set R) (oU : open U) : <> U. +Proof. +rewrite (open_disjoint_itv_bigcup oU); apply: sigma_algebra_bigcup => k. +have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. +exact : ocitv_measurable_itv. +Qed. + +Lemma octiv_open_measurable (a b : R) : <> `]a,b]%classic. +Proof. +rewrite [(`]a,b]%classic)] (_:_ = \bigcap_k `]a,b+(k.+1%:R)^-1[%classic). + rewrite eqEsubset set_itvoc. split=> [x /= /andP[ax xb] i _|x cupx/=]. + rewrite set_itvoo/=. apply/andP; split=>[//|]. apply: (le_lt_trans xb). + rewrite -[X in X<_]addr0; apply: ler_ltD=>//. by rewrite invr_gt0. + apply/andP; split. have :=cupx 1%N I. by rewrite set_itvoo => /=/andP[ax]. + apply/ler_gtP=> z bz. have := cupx (truncn (z-b)^-1) I. + rewrite set_itvoo/= =>/andP[_ xbz]. have := (addrNK b z); rewrite addrC => <-. + apply: (ltW (lt_trans xbz (lt_le_trans (ler_ltD (le_refl b) _) (le_refl _)))). + rewrite invf_plt ?posrE // ?subr_gt0//. exact: truncnS_gt. +rewrite -[X in _ X]setCK setC_bigcap; apply: sigma_algebraC. +apply: sigma_algebra_bigcup=>i; apply: sigma_algebraC; exact: sub_sigma_algebra. +Qed. + +Lemma salgebra_ocitv_openE : <> = <>. +Proof. +rewrite eqEsubset; split; apply: sigma_algebra_subl => /= E. + by move=>/open_octiv_measurable. +move=> [[a b] _ /= <-]; exact: octiv_open_measurable. +Qed. + +Lemma measurable_ocitv_openE : + (@open R).-sigma.-measurable = ocitv.-sigma.-measurable. +Proof. exact: salgebra_ocitv_openE. Qed. + +End measurable_real. \ 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.