sigma-algebra generated by a function

CHANGELOG_UNRELEASED.md

@@ -70,6 +70,14 @@
 - in `derive.v`:
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
+- in `measurable_structure.v`:
+  + definitions `preimage_display`, `g_sigma_algebra_preimageType`,
+    `g_sigma_algebra_preimage`
+  +  notations `.-preimage`, `.-preimage.-measurable`
+
+- in `measurable_function.v`:
+  + lemma `preimage_set_system_compS`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.

theories/measure_theory/measurable_function.v

@@ -334,6 +334,17 @@ HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g)
 
 End mfun_measurableType.
 
+Lemma preimage_set_system_compS (aT : Type)
+    d (rT : measurableType d) d' (T : sigmaRingType d')
+    (g : rT -> T) (f : aT -> rT) (D : set aT) :
+  measurable_fun setT g ->
+  preimage_set_system D (g \o f) measurable `<=`
+    preimage_set_system D f measurable.
+Proof.
+move=> mg A; rewrite /preimage_set_system => -[B GB]; exists (g @^-1` B) => //.
+by rewrite -[X in measurable X]setTI; exact: mg.
+Qed.
+
 Section measurability.
 
 (* f is measurable on the sigma-algebra generated by itself *)

theories/measure_theory/measurable_structure.v

@@ -89,11 +89,19 @@ 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                                            *)
@@ -128,6 +136,8 @@ Reserved Notation "'d<<' D '>>'".
 Reserved Notation "mu .-measurable" (format "mu .-measurable").
 Reserved Notation "G .-sigma" (format "G .-sigma").
 Reserved Notation "G .-sigma.-measurable" (format "G .-sigma.-measurable").
+Reserved Notation "f .-preimage" (format "f .-preimage").
+Reserved Notation "f .-preimage.-measurable" (format "f .-preimage.-measurable").
 Reserved Notation "'<<l' D , G '>>'" (format "'<<l'  D ,  G  '>>'").
 Reserved Notation "'<<l' G '>>'" (format "'<<l'  G  '>>'").
 Reserved Notation "'<<d' G '>>'" (format "'<<d'  G '>>'").
@@ -1339,6 +1349,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/measure_theory/probability_measure.v

@@ -189,7 +189,6 @@ apply/funext => x; rewrite /mnormalize/= probability_setT.
 by rewrite onee_eq0/= invr1 mule1.
 Qed.
 
-
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
   isPointed.Build (probability T R) (dirac point).