# HG changeset patch
# User hoelzl
# Date 1295017002 -3600
# Node ID 9c869baf1c661b125da41ff0e223dd9aa42e6612
# Parent  c3b977fee8a326de7f262c3de4d52f613aa6cae6
tuned formalization of subalgebra

diff -r c3b977fee8a3 -r 9c869baf1c66 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri Jan 14 14:21:48 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Jan 14 15:56:42 2011 +0100
@@ -170,7 +170,7 @@
 qed
 
 lemma (in sigma_algebra) borel_measurable_subalgebra:
-  assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
+  assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N"
   shows "f \<in> borel_measurable M"
   using assms unfolding measurable_def by auto
 
diff -r c3b977fee8a3 -r 9c869baf1c66 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 14:21:48 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 15:56:42 2011 +0100
@@ -463,12 +463,12 @@
 qed
 
 lemma (in sigma_algebra) simple_function_subalgebra:
-  assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)"
+  assumes "sigma_algebra.simple_function N f"
+  and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M" "sigma_algebra N"
   shows "simple_function f"
   using assms
   unfolding simple_function_def
-  unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)]
+  unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)]
   by auto
 
 lemma (in sigma_algebra) simple_function_vimage:
@@ -809,11 +809,11 @@
     unfolding pextreal_mult_cancel_left by auto
 qed
 
-lemma (in measure_space) simple_integral_subalgebra[simp]:
-  assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>"
-  shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral"
+lemma (in measure_space) simple_integral_subalgebra:
+  assumes N: "measure_space N \<mu>" and [simp]: "space N = space M"
+  shows "measure_space.simple_integral N \<mu> = simple_integral"
   unfolding simple_integral_def_raw
-  unfolding measure_space.simple_integral_def_raw[OF assms] by simp
+  unfolding measure_space.simple_integral_def_raw[OF N] by simp
 
 lemma (in measure_space) simple_integral_vimage:
   fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
@@ -1543,19 +1543,18 @@
   qed
 qed
 
-lemma (in measure_space) positive_integral_subalgebra[simp]:
-  assumes borel: "f \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets := N\<rparr>)"
-  shows "measure_space.positive_integral (M\<lparr>sets := N\<rparr>) \<mu> f = positive_integral f"
+lemma (in measure_space) positive_integral_subalgebra:
+  assumes borel: "f \<in> borel_measurable N"
+  and N: "sets N \<subseteq> sets M" "space N = space M" and sa: "sigma_algebra N"
+  shows "measure_space.positive_integral N \<mu> f = positive_integral f"
 proof -
-  note msN = measure_space_subalgebra[OF N_subalgebra]
-  then interpret N: measure_space "M\<lparr>sets:=N\<rparr>" \<mu> .
+  interpret N: measure_space N \<mu> using measure_space_subalgebra[OF sa N] .
   from N.borel_measurable_implies_simple_function_sequence[OF borel]
   obtain fs where Nsf: "\<And>i. N.simple_function (fs i)" and "fs \<up> f" by blast
   then have sf: "\<And>i. simple_function (fs i)"
-    using simple_function_subalgebra[OF _ N_subalgebra] by blast
+    using simple_function_subalgebra[OF _ N sa] by blast
   from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
-  show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
+  show ?thesis unfolding isoton_def simple_integral_def N.simple_integral_def `space N = space M` by simp
 qed
 
 section "Lebesgue Integral"
@@ -1847,6 +1846,22 @@
     using positive_integral_linear[OF f, of 1] by simp
 qed
 
+lemma (in measure_space) integral_subalgebra:
+  assumes borel: "f \<in> borel_measurable N"
+  and N: "sets N \<subseteq> sets M" "space N = space M" and sa: "sigma_algebra N"
+  shows "measure_space.integrable N \<mu> f \<longleftrightarrow> integrable f" (is ?P)
+    and "measure_space.integral N \<mu> f = integral f" (is ?I)
+proof -
+  interpret N: measure_space N \<mu> using measure_space_subalgebra[OF sa N] .
+  have "(\<lambda>x. Real (f x)) \<in> borel_measurable N" "(\<lambda>x. Real (- f x)) \<in> borel_measurable N"
+    using borel by auto
+  note * = this[THEN positive_integral_subalgebra[OF _ N sa]]
+  have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N"
+    using assms unfolding measurable_def by auto
+  then show ?P ?I unfolding integrable_def N.integrable_def integral_def N.integral_def
+    unfolding * by auto
+qed
+
 lemma (in measure_space) integrable_bound:
   assumes "integrable f"
   and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
diff -r c3b977fee8a3 -r 9c869baf1c66 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Jan 14 14:21:48 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Jan 14 15:56:42 2011 +0100
@@ -919,16 +919,15 @@
 qed
 
 lemma (in measure_space) measure_space_subalgebra:
-  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>"
+  assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
+  shows "measure_space N \<mu>"
 proof -
-  interpret N: sigma_algebra "M\<lparr> sets := N \<rparr>" by fact
+  interpret N: sigma_algebra N by fact
   show ?thesis
   proof
-    show "countably_additive (M\<lparr>sets := N\<rparr>) \<mu>"
-      using `N \<subseteq> sets M`
-      by (auto simp add: countably_additive_def
-               intro!: measure_countably_additive)
+    from `sets N \<subseteq> sets M` have "\<And>A. range A \<subseteq> sets N \<Longrightarrow> range A \<subseteq> sets M" by blast
+    then show "countably_additive N \<mu>"
+      by (auto intro!: measure_countably_additive simp: countably_additive_def)
   qed simp
 qed
 
diff -r c3b977fee8a3 -r 9c869baf1c66 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 14:21:48 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 15:56:42 2011 +0100
@@ -851,13 +851,13 @@
 qed
 
 lemma (in prob_space) prob_space_subalgebra:
-  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>"
+  assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
+  shows "prob_space N \<mu>"
 proof -
-  interpret N: measure_space "M\<lparr> sets := N \<rparr>" \<mu>
+  interpret N: measure_space N \<mu>
     using measure_space_subalgebra[OF assms] .
   show ?thesis
-    proof qed (simp add: measure_space_1)
+    proof qed (simp add: `space N = space M` measure_space_1)
 qed
 
 lemma (in prob_space) prob_space_of_restricted_space:
@@ -955,46 +955,46 @@
 lemma (in prob_space) conditional_expectation_exists:
   fixes X :: "'a \<Rightarrow> pextreal"
   assumes borel: "X \<in> borel_measurable M"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
+  and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
+  shows "\<exists>Y\<in>borel_measurable N. \<forall>C\<in>sets N.
       (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)"
 proof -
-  interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
-    using prob_space_subalgebra[OF N_subalgebra] .
+  interpret P: prob_space N \<mu>
+    using prob_space_subalgebra[OF N] .
 
   let "?f A" = "\<lambda>x. X x * indicator A x"
   let "?Q A" = "positive_integral (?f A)"
 
   from measure_space_density[OF borel]
-  have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
-    by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
-  then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
+  have Q: "measure_space N ?Q"
+    by (rule measure_space.measure_space_subalgebra[OF _ N])
+  then interpret Q: measure_space N ?Q .
 
   have "P.absolutely_continuous ?Q"
     unfolding P.absolutely_continuous_def
-  proof (safe, simp)
-    fix A assume "A \<in> N" "\<mu> A = 0"
+  proof safe
+    fix A assume "A \<in> sets N" "\<mu> A = 0"
     moreover then have f_borel: "?f A \<in> borel_measurable M"
-      using borel N_subalgebra by (auto intro: borel_measurable_indicator)
+      using borel N by (auto intro: borel_measurable_indicator)
     moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
       by (auto simp: indicator_def)
     moreover have "\<mu> \<dots> \<le> \<mu> A"
-      using `A \<in> N` N_subalgebra f_borel
+      using `A \<in> sets N` N f_borel
       by (auto intro!: measure_mono Int[of _ A] measurable_sets)
     ultimately show "?Q A = 0"
       by (simp add: positive_integral_0_iff)
   qed
   from P.Radon_Nikodym[OF Q this]
-  obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
-    "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
+  obtain Y where Y: "Y \<in> borel_measurable N"
+    "\<And>A. A \<in> sets N \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
     by blast
-  with N_subalgebra show ?thesis
-    by (auto intro!: bexI[OF _ Y(1)])
+  with N(2) show ?thesis
+    by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ N(2,3,1)])
 qed
 
 definition (in prob_space)
-  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
-    \<and> (\<forall>C\<in>N. (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)))"
+  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N
+    \<and> (\<forall>C\<in>sets N. (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)))"
 
 abbreviation (in prob_space)
   "conditional_prob N A \<equiv> conditional_expectation N (indicator A)"
@@ -1002,19 +1002,19 @@
 lemma (in prob_space)
   fixes X :: "'a \<Rightarrow> pextreal"
   assumes borel: "X \<in> borel_measurable M"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
   shows borel_measurable_conditional_expectation:
-    "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
-  and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
+    "conditional_expectation N X \<in> borel_measurable N"
+  and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow>
       (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x) =
       (\<integral>\<^isup>+x. X x * indicator C x)"
-   (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
+   (is "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C")
 proof -
   note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
-  then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+  then show "conditional_expectation N X \<in> borel_measurable N"
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 
-  from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
+  from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C"
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 qed