diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b44ac9e97..dccb4cf71 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 32f6dc978..3f7c75e0e 100644 --- a/theories/measure_theory/measurable_function.v +++ b/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 *) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 33bd1d264..06f7b4ec9 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/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 "'<>'" (format "'<>'"). Reserved Notation "'<>'" (format "'<>'"). Reserved Notation "'<>'" (format "'<>'"). @@ -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)]. diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index c4a725288..7d29e1a26 100644 --- a/theories/measure_theory/probability_measure.v +++ 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).