src/HOL/Probability/Sigma_Algebra.thy

   qed auto
 qed
 
 subsubsection {* Restricted Space Sigma Algebra *}
 
-definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
-
-lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
-  unfolding restrict_space_def by (subst space_measure_of) auto
-
-lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
-  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
-  unfolding restrict_space_def
-  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
+definition restrict_space where
+  "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)"
+
+lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
+  using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
+
+lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
+  by (simp add: space_restrict_space sets.sets_into_space)
+
+lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
+proof -
+  have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
+    (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
+    using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
+    by (simp add: sets.sigma_sets_eq)
+  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
+    using sets.sets_into_space by (intro image_cong) auto
+  ultimately show ?thesis
+    using sets.sets_into_space[of _ M] unfolding restrict_space_def
+    by (subst sets_measure_of) fastforce+
+qed
 
 lemma sets_restrict_space_iff:
-  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
-  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
+  "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
+proof (subst sets_restrict_space, safe)
+  fix A assume "\<Omega> \<inter> space M \<in> sets M" and A: "A \<in> sets M"
+  then have "(\<Omega> \<inter> space M) \<inter> A \<in> sets M"
+    by rule
+  also have "(\<Omega> \<inter> space M) \<inter> A = \<Omega> \<inter> A"
+    using sets.sets_into_space[OF A] by auto
+  finally show "\<Omega> \<inter> A \<in> sets M"
+    by auto
+qed auto
 
 lemma measurable_restrict_space1:
-  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
+  shows "f \<in> measurable (restrict_space M \<Omega>) N"
   unfolding measurable_def
 proof (intro CollectI conjI ballI)
   show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
     using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
 
   fix A assume "A \<in> sets N"
-  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
+  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> (\<Omega> \<inter> space M)"
     using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
   also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
     unfolding sets_restrict_space_iff[OF \<Omega>]
     using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast
   finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" .
 qed
 
 lemma measurable_restrict_space2:
-  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)"
+  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
+    f \<in> measurable M (restrict_space N \<Omega>)"
   by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
 
 end
+