src/HOL/Probability/Probability_Space.thy
changeset 39091 11314c196e11
parent 39090 a2d38b8b693e
child 39092 98de40859858
equal deleted inserted replaced
39090:a2d38b8b693e 39091:11314c196e11
   560 
   560 
   561   from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
   561   from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
   562     unfolding conditional_expectation_def by (rule someI2_ex) blast
   562     unfolding conditional_expectation_def by (rule someI2_ex) blast
   563 qed
   563 qed
   564 
   564 
       
   565 lemma (in sigma_algebra) factorize_measurable_function:
       
   566   fixes Z :: "'a \<Rightarrow> pinfreal" and Y :: "'a \<Rightarrow> 'c"
       
   567   assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
       
   568   shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
       
   569     \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))"
       
   570 proof safe
       
   571   interpret M': sigma_algebra M' by fact
       
   572   have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto
       
   573   from M'.sigma_algebra_vimage[OF this]
       
   574   interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" .
       
   575 
       
   576   { fix g :: "'c \<Rightarrow> pinfreal" assume "g \<in> borel_measurable M'"
       
   577     with M'.measurable_vimage_algebra[OF Y]
       
   578     have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
       
   579       by (rule measurable_comp)
       
   580     moreover assume "\<forall>x\<in>space M. Z x = g (Y x)"
       
   581     then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow>
       
   582        g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
       
   583        by (auto intro!: measurable_cong)
       
   584     ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
       
   585       by simp }
       
   586 
       
   587   assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
       
   588   from va.borel_measurable_implies_simple_function_sequence[OF this]
       
   589   obtain f where f: "\<And>i. va.simple_function (f i)" and "f \<up> Z" by blast
       
   590 
       
   591   have "\<forall>i. \<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
       
   592   proof
       
   593     fix i
       
   594     from f[of i] have "finite (f i`space M)" and B_ex:
       
   595       "\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) -` {z} \<inter> space M = Y -` B \<inter> space M"
       
   596       unfolding va.simple_function_def by auto
       
   597     from B_ex[THEN bchoice] guess B .. note B = this
       
   598 
       
   599     let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x"
       
   600 
       
   601     show "\<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))"
       
   602     proof (intro exI[of _ ?g] conjI ballI)
       
   603       show "M'.simple_function ?g" using B by auto
       
   604 
       
   605       fix x assume "x \<in> space M"
       
   606       then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::pinfreal)"
       
   607         unfolding indicator_def using B by auto
       
   608       then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i]
       
   609         by (subst va.simple_function_indicator_representation) auto
       
   610     qed
       
   611   qed
       
   612   from choice[OF this] guess g .. note g = this
       
   613 
       
   614   show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
       
   615   proof (intro ballI bexI)
       
   616     show "(SUP i. g i) \<in> borel_measurable M'"
       
   617       using g by (auto intro: M'.borel_measurable_simple_function)
       
   618     fix x assume "x \<in> space M"
       
   619     have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
       
   620     also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
       
   621       using g `x \<in> space M` by simp
       
   622     finally show "Z x = (SUP i. g i) (Y x)" .
       
   623   qed
       
   624 qed
   565 
   625 
   566 end
   626 end