mv defs to appropriate files

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -74,11 +74,10 @@
 - in `probability.v`:
   + lemmas `eq_bernoulli`, `eq_bernoulliV2`
 
-
 - file `mathcomp_extra.v`
   + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
 
-- in `measure.v`:
+- in `measurable_function.v`:
   + lemma `preimage_set_system_compS`
 
 - in `numfun.v`:

theories/measure_theory/measurable_structure.v

@@ -92,11 +92,20 @@ From mathcomp Require Import sequences esum numfun.
 (* ## 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

@@ -1179,64 +1179,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.