rebase and fix

- fix changelog
- mv defs to appropriate files

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -164,16 +164,9 @@
            `derivable_oy_continuousW`,
            `derivable_Nyo_continuousWoo`,
            `derivable_Nyo_continuousW`
-- in `probability.v`:
-  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
-- file `mathcomp_extra.v`
-  + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
-
-- file `Rstruct.v`
-  + lemma `Pos_to_natE` (from `mathcomp_extra.v`)
-  + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`
 
-- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
+- in `measurable_function.v`:
+  + lemma `preimage_set_system_compS`
 
 - in `numfun.v`:
   + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
@@ -183,9 +176,8 @@
     `funrD_posD`, `funrpos_le`, `funrneg_le`
   + lemmas `funerpos`, `funerneg`
 
-- in `measure.v`:
-  + lemma `preimage_class_comp`
-  + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
+- in `measurable_structure.v`:
+  + definitions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
     notations `.-preimage`, `.-preimage.-measurable`
 
 - in `measurable_realfun.v`:
@@ -323,55 +315,6 @@
   + `le_ereal_inf` -> `ereal_inf_le_tmp`
   + `lb_ereal_inf` -> `le_ereal_inf_tmp`
   + `ereal_sup_ge` -> `le_ereal_sup_tmp`
-- in `kernel.v`:
-  + `isFiniteTransition` -> `isFiniteTransitionKernel`
-- in `lebesgue_integral.v`:
-  + `fubini1a` -> `integrable12ltyP`
-  + `fubini1b` -> `integrable21ltyP`
-  + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin)
-
-- in `mathcomp_extra.v`
-  + `comparable_min_le_min` -> `comparable_le_min2`
-  + `comparable_max_le_max` -> `comparable_le_max2`
-  + `min_le_min` -> `le_min2`
-  + `max_le_max` -> `le_max2`
-  + `real_sqrtC` -> `sqrtC_real`
-- in `measure.v`
-  + `preimage_class` -> `preimage_set_system`
-  + `image_class` -> `image_set_system`
-  + `preimage_classes` -> `g_sigma_preimageU`
-  + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun`
-  + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage`
-  + `sigma_algebra_image_class` -> `sigma_algebra_image`
-  + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
-  + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
-  
-### Renamed
-
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `probability.v`:
-  + `expectationM` -> `expectationZl`
-
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
-
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
-
-- in `probability.v`:
-  + `integral_distribution` -> `ge0_integral_distribution`
-
-- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
 
 ### Generalized
 
@@ -458,45 +401,6 @@
   + lemma `interval_set1` (use `set_itv1` instead)
 - in `ereal.v`:
   + notation `ereal_sup_le` (was deprecated since 1.11.0)
-- file `mathcomp_extra.v`
-  + lemma `Pos_to_natE` (moved to `Rstruct.v`)
-  + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
-    since MathComp 2.1.0)
-- in `sequences.v`:
-  + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
-    `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
-- in `topology_structure.v`:
-  + lemma `closureC`
-
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
-### Removed
-
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
-- in `lebesgue_integral.v`:
-  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
-  + lemma `cst_nnfun_subproof` (turned into a `Let`)
-  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
-
-- in `lebesgue_measurable.v`:
-  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
-  + notation `measurable_power_pos` (deprecated since 0.6.4)
 
 ### Infrastructure
 

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

theories/measure_theory/measurable_structure.v

@@ -90,11 +90,20 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (* ## Other measure-theoretic definitions                                     *)
 (*                                                                            *)
 (* ```                                                                        *)
-(* preimage_set_system D f G == set system of the preimages by f of sets in G *)
-(*    image_set_system D f G == set system of the sets with a preimage by f   *)
-(*                              in G                                          *)
-(* subset_sigma_subadditive mu == alternative predicate defining              *)
-(*                              sigma-subadditivity                           *)
+(*      preimage_set_system D f G == set system of the preimages by f of sets *)
+(*                                   in G                                     *)
+(*     g_sigma_algebra_preimage f == sigma-algebra generated by the           *)
+(*                                   function f                               *)
+(* g_sigma_algebra_preimageType f == the measurableType corresponding to      *)
+(*                                   g_sigma_algebra_preimage f               *)
+(*                                   This is an HB alias.                     *)
+(*      f.-preimage.-measurable A == A is measurable for                      *)
+(*                                   g_sigma_algebra_preimage f               *)
+(*         image_set_system D f G == set system of the sets with a preimage   *)
+(*                                   by f in G                                *)
+(*                                                                            *)
+(*    subset_sigma_subadditive mu == alternative predicate defining           *)
+(*                                   sigma-subadditivity                      *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Product of measurable spaces                                            *)
@@ -1343,6 +1352,58 @@ case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0.
   exact: (mF' i).2.
 Qed.
 
+Definition preimage_display {T T'} : (T -> T') -> measure_display.
+Proof. exact. Qed.
+
+Definition g_sigma_algebra_preimageType d' (T : pointedType)
+  (T' : measurableType d') (f : T -> T') : Type := T.
+
+Definition g_sigma_algebra_preimage d' (T : pointedType)
+    (T' : measurableType d') (f : T -> T') :=
+  preimage_set_system setT f (@measurable _ T').
+
+Section preimage_generated_sigma_algebra.
+Context {d'} (T : pointedType) (T' : measurableType d').
+Variable f : T -> T'.
+
+Let preimage_set0 : g_sigma_algebra_preimage f set0.
+Proof.
+rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
+by exists set0 => //; rewrite preimage_set0 setI0.
+Qed.
+
+Let preimage_setC A :
+  g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A).
+Proof.
+rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}.
+by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
+Qed.
+
+Let preimage_bigcup (F : (set T)^nat) :
+  (forall i, g_sigma_algebra_preimage f (F i)) ->
+  g_sigma_algebra_preimage f (\bigcup_i (F i)).
+Proof.
+move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
+pose g := fun i => sval (cid2 (mF i)).
+pose mg := fun i => svalP (cid2 (mF i)).
+exists (\bigcup_i g i).
+  by apply: bigcup_measurable => k; case: (mg k).
+rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
+by case: (mg k) => _; rewrite setTI.
+Qed.
+
+HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).
+
+HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
+  (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
+  preimage_set0 preimage_setC preimage_bigcup.
+
+End preimage_generated_sigma_algebra.
+
+Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
+Notation "f .-preimage.-measurable" :=
+  (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
+
 Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
     (G : set (set aT)) : set (set rT) :=
   [set B : set rT | G (D `&` f @^-1` B)].

theories/probability.v

@@ -1183,64 +1183,6 @@ Definition mutual_independence (I0 : choiceType) (I : set I0)
 
 End mutual_independence.
 
-(* g_sigma_algebra_preimage f == sigma-algebra generated by the function f      *)
-(* g_sigma_algebra_preimageType f == the measurableType corresponding to       *)
-(*                             g_sigma_algebra_preimage f                      *)
-(*                             This is an HB alias.                           *)
-(* f.-preimage.-measurable A == A is measurable for g_sigma_algebra_preimage f  *)
-
-Definition preimage_display {T T'} : (T -> T') -> measure_display.
-Proof. exact. Qed.
-
-Definition g_sigma_algebra_preimageType d' (T : pointedType)
-  (T' : measurableType d') (f : T -> T') : Type := T.
-
-Definition g_sigma_algebra_preimage d' (T : pointedType)
-    (T' : measurableType d') (f : T -> T') :=
-  preimage_set_system setT f (@measurable _ T').
-
-Section preimage_generated_sigma_algebra.
-Context {d'} (T : pointedType) (T' : measurableType d').
-Variable f : T -> T'.
-
-Let preimage_set0 : g_sigma_algebra_preimage f set0.
-Proof.
-rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
-by exists set0 => //; rewrite preimage_set0 setI0.
-Qed.
-
-Let preimage_setC A :
-  g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A).
-Proof.
-rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}.
-by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
-Qed.
-
-Let preimage_bigcup (F : (set T)^nat) :
-  (forall i, g_sigma_algebra_preimage f (F i)) ->
-  g_sigma_algebra_preimage f (\bigcup_i (F i)).
-Proof.
-move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
-pose g := fun i => sval (cid2 (mF i)).
-pose mg := fun i => svalP (cid2 (mF i)).
-exists (\bigcup_i g i).
-  by apply: bigcup_measurable => k; case: (mg k).
-rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
-by case: (mg k) => _; rewrite setTI.
-Qed.
-
-HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).
-
-HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
-  (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
-  preimage_set0 preimage_setC preimage_bigcup.
-
-End preimage_generated_sigma_algebra.
-
-Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
-Notation "f .-preimage.-measurable" :=
-  (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
-
 Section independent_RVs.
 Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
 Variable P : probability T R.