src/HOL/Probability/Borel_Space.thy

      by (auto simp: fun_eq_iff pextreal_noteq_omega_Ex)
   show ?thesis using assms unfolding *
     by (auto intro!: measurable_If)
 qed
 
-lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
-  fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-proof -
-  have *: "(\<lambda>x. f x * g x) =
-     (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
-      Real (real (f x) * real (g x)))"
-     by (auto simp: fun_eq_iff pextreal_noteq_omega_Ex)
-  show ?thesis using assms unfolding *
-    by (auto intro!: measurable_If)
-qed
-
 lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
 proof cases
   assume "finite S"
   thus ?thesis using assms
     by induct auto
 qed (simp add: borel_measurable_const)
+
+lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
+  fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+proof -
+  have *: "(\<lambda>x. f x * g x) =
+     (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
+      Real (real (f x) * real (g x)))"
+     by (auto simp: fun_eq_iff pextreal_noteq_omega_Ex)
+  show ?thesis using assms unfolding *
+    by (auto intro!: measurable_If)
+qed
+
+lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms by induct auto
+qed simp
 
 lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
   fixes f g :: "'a \<Rightarrow> pextreal"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"