# HG changeset patch
# User hoelzl
# Date 1282919031 -7200
# Node ID 11314c196e119dda4c87e8478fd042ce9262e1ae
# Parent a2d38b8b693e8b194bccbf2156a8bb93bcaf6f06
factorizable measurable functions
diff -r a2d38b8b693e -r 11314c196e11 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy Fri Aug 27 15:05:07 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy Fri Aug 27 16:23:51 2010 +0200
@@ -562,5 +562,65 @@
unfolding conditional_expectation_def by (rule someI2_ex) blast
qed
+lemma (in sigma_algebra) factorize_measurable_function:
+ fixes Z :: "'a \ pinfreal" and Y :: "'a \ 'c"
+ assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M"
+ shows "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
+ \ (\g\borel_measurable M'. \x\space M. Z x = g (Y x))"
+proof safe
+ interpret M': sigma_algebra M' by fact
+ have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto
+ from M'.sigma_algebra_vimage[OF this]
+ interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" .
+
+ { fix g :: "'c \ pinfreal" assume "g \ borel_measurable M'"
+ with M'.measurable_vimage_algebra[OF Y]
+ have "g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)"
+ by (rule measurable_comp)
+ moreover assume "\x\space M. Z x = g (Y x)"
+ then have "Z \ borel_measurable (M'.vimage_algebra (space M) Y) \
+ g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)"
+ by (auto intro!: measurable_cong)
+ ultimately show "Z \ borel_measurable (M'.vimage_algebra (space M) Y)"
+ by simp }
+
+ assume "Z \ borel_measurable (M'.vimage_algebra (space M) Y)"
+ from va.borel_measurable_implies_simple_function_sequence[OF this]
+ obtain f where f: "\i. va.simple_function (f i)" and "f \ Z" by blast
+
+ have "\i. \g. M'.simple_function g \ (\x\space M. f i x = g (Y x))"
+ proof
+ fix i
+ from f[of i] have "finite (f i`space M)" and B_ex:
+ "\z\(f i)`space M. \B. B \ sets M' \ (f i) -` {z} \ space M = Y -` B \ space M"
+ unfolding va.simple_function_def by auto
+ from B_ex[THEN bchoice] guess B .. note B = this
+
+ let ?g = "\x. \z\f i`space M. z * indicator (B z) x"
+
+ show "\g. M'.simple_function g \ (\x\space M. f i x = g (Y x))"
+ proof (intro exI[of _ ?g] conjI ballI)
+ show "M'.simple_function ?g" using B by auto
+
+ fix x assume "x \ space M"
+ then have "\z. z \ f i`space M \ indicator (B z) (Y x) = (indicator (f i -` {z} \ space M) x::pinfreal)"
+ unfolding indicator_def using B by auto
+ then show "f i x = ?g (Y x)" using `x \ space M` f[of i]
+ by (subst va.simple_function_indicator_representation) auto
+ qed
+ qed
+ from choice[OF this] guess g .. note g = this
+
+ show "\g\borel_measurable M'. \x\space M. Z x = g (Y x)"
+ proof (intro ballI bexI)
+ show "(SUP i. g i) \ borel_measurable M'"
+ using g by (auto intro: M'.borel_measurable_simple_function)
+ fix x assume "x \ space M"
+ have "Z x = (SUP i. f i) x" using `f \ Z` unfolding isoton_def by simp
+ also have "\ = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+ using g `x \ space M` by simp
+ finally show "Z x = (SUP i. g i) (Y x)" .
+ qed
+qed
end