src/HOL/Probability/Borel.thy

 header {*Borel spaces*}
 
 theory Borel
   imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
 begin
+
+lemma LIMSEQ_max:
+  "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0"
+  by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D)
 
 section "Generic Borel spaces"
 
 definition "borel_space = sigma (UNIV::'a::topological_space set) open"
 abbreviation "borel_measurable M \<equiv> measurable M borel_space"

       by (metis borel_space.top borel_space_def_raw mem_def space_sigma)
     ultimately show ?case
       by (auto simp: vimage_Diff borel_space.Diff)
   qed (auto simp add: vimage_UN)
 qed
+
+lemma (in sigma_algebra) borel_measurable_restricted:
+  fixes f :: "'a \<Rightarrow> 'x\<Colon>{topological_space, semiring_1}" assumes "A \<in> sets M"
+  shows "f \<in> borel_measurable (restricted_space A) \<longleftrightarrow>
+    (\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
+    (is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M")
+proof -
+  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
+  have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R"
+    by (auto intro!: measurable_cong)
+  show ?thesis unfolding *
+    unfolding in_borel_measurable_borel_space
+  proof (simp, safe)
+    fix S :: "'x set" assume "S \<in> sets borel_space"
+      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
+    then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
+    then have f: "?f -` S \<inter> A \<in> sets M"
+      using `A \<in> sets M` sets_into_space by fastsimp
+    show "?f -` S \<inter> space M \<in> sets M"
+    proof cases
+      assume "0 \<in> S"
+      then have "?f -` S \<inter> space M = ?f -` S \<inter> A \<union> (space M - A)"
+        using `A \<in> sets M` sets_into_space by auto
+      then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff)
+    next
+      assume "0 \<notin> S"
+      then have "?f -` S \<inter> space M = ?f -` S \<inter> A"
+        using `A \<in> sets M` sets_into_space
+        by (auto simp: indicator_def split: split_if_asm)
+      then show ?thesis using f by auto
+    qed
+  next
+    fix S :: "'x set" assume "S \<in> sets borel_space"
+      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> space M \<in> sets M"
+    then have f: "?f -` S \<inter> space M \<in> sets M" by auto
+    then show "?f -` S \<inter> A \<in> op \<inter> A ` sets M"
+      using `A \<in> sets M` sets_into_space
+      apply (simp add: image_iff)
+      apply (rule bexI[OF _ f])
+      by auto
+  qed
+qed
+
+lemma (in sigma_algebra) borel_measurable_subalgebra:
+  assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
+  shows "f \<in> borel_measurable M"
+  using assms unfolding measurable_def by auto
 
 section "Borel spaces on euclidean spaces"
 
 lemma lessThan_borel[simp, intro]:
   fixes a :: "'a\<Colon>ordered_euclidean_space"

     by (simp add: pinfreal_less_minus_iff)
   then show "{x \<in> space M. a < f x - g x} \<in> sets M"
     using assms by auto
 qed
 
+lemma (in sigma_algebra) borel_measurable_psuminf:
+  assumes "\<And>i. f i \<in> borel_measurable M"
+  shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
+  using assms unfolding psuminf_def
+  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
+
+section "LIMSEQ is borel measurable"
+
+lemma (in sigma_algebra) borel_measurable_LIMSEQ:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+  assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
+  and u: "\<And>i. u i \<in> borel_measurable M"
+  shows "u' \<in> borel_measurable M"
+proof -
+  let "?pu x i" = "max (u i x) 0"
+  let "?nu x i" = "max (- u i x) 0"
+
+  { fix x assume x: "x \<in> space M"
+    have "(?pu x) ----> max (u' x) 0"
+      "(?nu x) ----> max (- u' x) 0"
+      using u'[OF x] by (auto intro!: LIMSEQ_max LIMSEQ_minus)
+    from LIMSEQ_imp_lim_INF[OF _ this(1)] LIMSEQ_imp_lim_INF[OF _ this(2)]
+    have "(SUP n. INF m. Real (u (n + m) x)) = Real (u' x)"
+      "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)"
+      by (simp_all add: Real_max'[symmetric]) }
+  note eq = this
+
+  have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
+    by auto
+
+  have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
+       "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
+    using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
+  with eq[THEN measurable_cong, of M "\<lambda>x. x" borel_space]
+  have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
+       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
+    unfolding SUPR_fun_expand INFI_fun_expand by auto
+  note this[THEN borel_measurable_real]
+  from borel_measurable_diff[OF this]
+  show ?thesis unfolding * .
+qed
+
 end