--- 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
--- 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"
--- 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
--- 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