Topology lemmas

CHANGELOG_UNRELEASED.md

@@ -234,6 +234,30 @@
 - 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`
+- in `lebesgue_stieltjes_measure.v`:
+  + module `MeasurableRocitv`
+  + definition `open_type`
+  + notations `.-open`, `.-open.-measurable`
+  + module `MeasurableRopen`
+    * definition `measurableTypeR`
+    + definition `lebesgue_display`
+    * definition `measurableR`
+    + lemmas `measurable_set1`, `measurable_itv` (also declared as hints)
+    + definition `ocitv_measure`, lemma `ocitv_measure_ext`
+  + module `MeasurableR`
+  + module `RGenOpenSets`
+    * lemma `measurableE`
+
+- in `real_interval.v`:
+  + lemma `set1_bigcap_oo`
+
 ### Changed
 
 - in `realsum.v`:
@@ -354,6 +378,18 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v`
+  + module `RGenOInfty`
+  + module `RGenInftyO`
+  + module `RGenCInfty`
+  + module `RGenOpens`
+
+- moved inside module `MeasurableRocitv` (`lebesgue_stieltjes_measure.v`):
+  + lemmas `measurable_set1`, `measurable_itv`
+
+- in `lebesgue_stieltjes_measure.v`:
+  + lemma `lebesgue_stieltjes_measure_unique` is now about the sigma-algebra generated by open sets
+
 ### Renamed
 
 - in `tvs.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

reals/real_interval.v

@@ -235,6 +235,18 @@ Qed.
 
 End set_ereal.
 
+Lemma set1_bigcap_oo {R : realType} (x : R) :
+  [set x] = \bigcap_(k : nat) `]x - k.+1%:R^-1, x + k.+1%:R^-1[%classic.
+Proof.
+apply/seteqP; split => [_ -> k _|y xy] /=.
+  by rewrite in_itv/= ltrBlDr andbb ltrDl invr_gt0 ltr0n.
+apply/eqP; rewrite eq_sym -subr_eq0 -normr_eq0 eq_le normr_ge0 andbT.
+apply/ler_addgt0Pl => e e0; rewrite addr0.
+have /= := xy (truncn e^-1) I.
+rewrite in_itv/= -ltr_distlC => /ltW/le_trans; apply.
+by rewrite invf_ple ?posrE ?ltr0n ?invr_gt0//; apply/ltW/truncnS_gt.
+Qed.
+
 Lemma set1_bigcap_oc (R : realType) (r : R) :
   [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
 Proof.

theories/borel_hierarchy.v

@@ -47,6 +47,8 @@ Proof. by exists (fun=> S)=> //; rewrite bigcup_const. Qed.
 
 End Gdelta_Fsigma.
 
+Import MeasurableR.
+
 Lemma Gdelta_measurable {R : realType} (S : set R) : Gdelta S -> measurable S.
 Proof.
 move=> [] B oB ->; apply: bigcapT_measurable => i.

theories/ftc.v

@@ -68,6 +68,8 @@ Notation mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
+Import MeasurableR.
+
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
@@ -328,6 +330,8 @@ End FTC.
 #[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `integrable_locally_restrict`")]
 Notation integrable_locally := integrable_locally_restrict (only parsing).
 
+Import MeasurableR.
+
 Definition parameterized_integral {R : realType}
     (mu : {measure set (measurableTypeR R) -> \bar R})
     a x (f : R -> R) : R :=
@@ -524,6 +528,8 @@ rewrite mem_set ?mulr1 /=; first exact: subset_itv_oo_cc.
 exact: cvg_patch.
 Qed.
 
+Import MeasurableR.
+
 Corollary continuous_FTC2 f F a b : (a < b)%R ->
   {within `[a, b], continuous f} ->
   derivable_oo_LRcontinuous F a b ->
@@ -772,6 +778,8 @@ Notation mu := lebesgue_measure.
 Local Open Scope ereal_scope.
 Implicit Types (F G f g : R -> R) (a b : R).
 
+Import MeasurableR.
+
 Lemma integration_by_parts F G f g a b : (a < b)%R ->
     {within `[a, b], continuous f} ->
     derivable_oo_LRcontinuous F a b ->
@@ -824,6 +832,8 @@ Context {R : realType}.
 Notation mu := lebesgue_measure.
 Implicit Types (F G f g : R -> R) (a b : R).
 
+Import MeasurableR.
+
 Lemma Rintegration_by_parts F G f g a b :
     (a < b)%R ->
     {within `[a, b], continuous f} ->
@@ -1030,6 +1040,8 @@ Context {R : realType}.
 Notation mu := lebesgue_measure.
 Implicit Types (F G f : R -> R) (a b : R).
 
+Import MeasurableR.
+
 Lemma integration_by_substitution_decreasing F G a b : (a <= b)%R ->
   {in `[a, b] &, {homo F : x y /~ (x < y)%R}} ->
   {in `]a, b[, continuous F^`()} ->
@@ -1357,7 +1369,7 @@ transitivity (limn (fun n =>
   rewrite -integral_bigsetU_EFin/=.
   - by move=> k; apply: measurableD => //; exact: bigsetU_measurable.
   - exact: iota_uniq.
-  - exact: (@sub_trivIset _ _ _ [set: nat]).
+  - exact: (@sub_trivIset _ _ _ setT).
   - apply/measurable_EFinP.
     apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)%R[)).
       rewrite big_mkord -bigsetU_seqDU.
@@ -1776,11 +1788,12 @@ Qed.
 
 End integration_by_substitution.
 
-
 Section ge0_integration_by_substitution_shift.
 Context {R : realType}.
 Notation mu := (@lebesgue_measure R).
 
+Import MeasurableR.
+
 Lemma ge0_integration_by_substitution_shift_itvy (f : R -> R) (r e : R) :
   {within `[r + e, +oo[, continuous f} ->
   {in `]r + e, +oo[, forall x : R, 0 <= f x} ->
@@ -1828,6 +1841,8 @@ Context {R : realType}.
 Let mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 
+Import MeasurableR.
+
 Lemma integration_by_substitution_onem (G : R -> R) (r : R) :
   (0 <= r <= 1)%R ->
   {within `[0%R, r], continuous G} ->
@@ -1869,6 +1884,8 @@ Context {R : realType}.
 Let mu := @lebesgue_measure R.
 Local Open Scope ereal_scope.
 
+Import MeasurableR.
+
 Lemma ge0_symfun_integralT (f : R -> R) : (forall x, 0 <= f x)%R ->
   continuous f -> f =1 f \o -%R ->
   \int[mu]_x (f x)%:E = 2%:E * \int[mu]_(x in [set x | (0 <= x)%R]) (f x)%:E.
@@ -1877,10 +1894,10 @@ move=> f0 cf evenf.
 have mf : measurable_fun [set: R] f by exact: continuous_measurable_fun.
 have mposnums : measurable [set x : R | 0 <= x]%R by rewrite -set_itvcy.
 rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//=.
-  exact: measurableC.
-  by apply/measurable_EFinP; rewrite setUv.
-  by move=> x _; rewrite lee_fin.
-  exact/disj_setPCl.
+- exact: measurableC.
+- by apply/measurable_EFinP; rewrite setUv.
+- by move=> x _; rewrite lee_fin.
+- exact/disj_setPCl.
 rewrite mule_natl mule2n; congr +%E.
 rewrite -set_itvcy// setCitvr.
 rewrite integral_itvbo_itvbc; first exact/measurable_EFinP/measurable_funTS.

theories/gauss_integral.v

@@ -41,6 +41,8 @@ by apply: (cvg_comp (fun x => x ^+ 2) (fun x => expR (- x)));
   [exact: cvgr_expr2|exact: cvgr_expR].
 Qed.
 
+Import MeasurableR.
+
 Lemma measurable_gauss_fun : measurable_fun setT gauss_fun.
 Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed.
 
@@ -63,6 +65,8 @@ Implicit Type x : R.
 
 Let mu : {measure set _ -> \bar R} := @lebesgue_measure R.
 
+Import MeasurableR.
+
 Definition integral0y_gauss := \int[mu]_(x in `[0%R, +oo[) gauss_fun x.
 
 Let integral0y_gauss_ge0 : 0 <= integral0y_gauss.
@@ -350,6 +354,8 @@ Context {R : realType}.
 Import gauss_integral_proof.
 Let mu := @lebesgue_measure R.
 
+Import MeasurableR.
+
 Lemma integral0y_gauss :
   (\int[mu]_(x in `[0%R, +oo[) (gauss_fun x)%:E)%E = (Num.sqrt pi / 2)%:E.
 Proof.

theories/hoelder.v

@@ -357,11 +357,13 @@ Qed.
 End hoelder_conjugate.
 
 Section hoelder.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}).
 Local Open Scope ereal_scope.
 Implicit Types (p q : R) (f g : T -> R).
 
+Import MeasurableR.
+
 Let measurableT_comp_powR f p :
   measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R.
 Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
@@ -498,6 +500,8 @@ Section hoelder2.
 Context {R : realType}.
 Local Open Scope ring_scope.
 
+Import MeasurableR.
+
 Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
   0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
   0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
@@ -534,6 +538,8 @@ Context {R : realType}.
 Local Open Scope ring_scope.
 Local Open Scope convex_scope.
 
+Import MeasurableR.
+
 Lemma convex_powR p : 1 <= p ->
   convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
@@ -579,8 +585,8 @@ Qed.
 End convex_powR.
 
 Section minkowski.
-Context d (T : measurableType d) (R : realType).
-Variable mu : {measure set T -> \bar R}.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}).
 Implicit Types (f g : T -> R) (p : R).
 
 Let convex_powR_abs_half f g p x : 1 <= p ->
@@ -595,6 +601,8 @@ by apply: (convex_powR p1 (Itv01 _ _)) => //=;
   rewrite ?inE/= ?in_itv/= ?normr_ge0// ?invr_ge0// invf_le1 ?ler1n.
 Qed.
 
+Import MeasurableR.
+
 Let measurableT_comp_powR f p :
   measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R.
 Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
@@ -788,6 +796,8 @@ Definition finite_norm d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
   ('N[ mu ]_p [ EFin \o f ] < +oo)%E.
 
+Import MeasurableR.
+
 HB.mixin Record isLfunction d (T : measurableType d) (R : realType)
     (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R)
   & @MeasurableFun d _ T R f := {

theories/independence.v

@@ -427,19 +427,21 @@ Qed.
 End independent_generators.
 
 Section independent_RVs2.
-Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
-Variable P : probability T R.
+Context {R : realType} {d d'} {T : measurableType d} {T' : measurableType d'}
+ (P : probability T R).
 
 Definition independent_RVs2 (X Y : {mfun T >-> T'}) :=
   independent_RVs P [set: bool] (fun b => if b then Y else X).
 
 End independent_RVs2.
 
 Section independent_RVs2_properties.
-Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
-Variable P : probability T R.
+Context {R : realType} {d d'} {T : measurableType d} {T' : measurableType d'}
+  (P : probability T R).
 Local Open Scope ring_scope.
 
+Import MeasurableR.
+
 Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) :
   independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y).
 Proof.
@@ -517,10 +519,11 @@ HB.instance Definition _ (X Y : {RV P >-> T'}) :=
 End pairRV.
 
 Section independent_RVs2_properties_realType.
-Context {R : realType} d (T : measurableType d).
-Variable P : probability T R.
+Context {R : realType} {d} {T : measurableType d} (P : probability T R).
 Local Open Scope ereal_scope.
 
+Import MeasurableR.
+
 Lemma independent_RVs2_setI_preimage (X Y : {mfun T >-> R}) (A1 A2 : set R) :
   measurable A1 -> measurable A2 ->
   independent_RVs2 P X Y ->
@@ -551,10 +554,11 @@ Qed.
 End independent_RVs2_properties_realType.
 
 Section product_expectation_over_product_measure.
-Context {R : realType} d (T : measurableType d).
-Variable P : probability T R.
+Context {R : realType} {d} {T : measurableType d} (P : probability T R).
 Local Open Scope ereal_scope.
 
+Import MeasurableR.
+
 Lemma independent_Lfun1_expectation_product_measure_lty (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->
   (X : _ -> _) \in Lfun P 1 -> (Y : _ -> _) \in Lfun P 1 ->
@@ -598,11 +602,11 @@ Qed.
 End product_expectation_over_product_measure.
 
 Section expectationM.
-Context {R : realType} d (T : measurableType d).
-Variable P : probability T R.
+Context {R : realType} {d} {T : measurableType d} (P : probability T R).
 Local Open Scope ereal_scope.
 
 Import HBNNSimple.
+Import MeasurableR.
 
 #[local] Lemma expectationM_nnsfun (f g : {nnsfun T >-> R}) :
   (forall y y', y \in range f -> y' \in range g ->
@@ -773,11 +777,11 @@ Qed.
 End expectationM.
 
 Section product_expectation.
-Context {R : realType} d (T : measurableType d).
-Variable P : probability T R.
+Context {R : realType} {d} {T : measurableType d} (P : probability T R).
 Local Open Scope ereal_scope.
 
 Import HBNNSimple.
+Import MeasurableR.
 
 Lemma independent_Lfun1_expectationM_lty (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->