Topology lemmas

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`:

_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

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 -> <<s D, B>> = <<s D, open>>.
+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 : 
+<<s (@open T)>> = <<s closed>>.
+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) : 
+  <<s G>> = 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) : <<s ocitv>> [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) : <<s ocitv>> 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) : <<s open>> `]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 : <<s open>> = <<s ocitv>>.
+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.

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}

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).

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.