1.1 --- a/src/HOL/Probability/Borel.thy Thu Aug 26 15:20:41 2010 +0200
1.2 +++ b/src/HOL/Probability/Borel.thy Thu Aug 26 18:41:54 2010 +0200
1.3 @@ -81,7 +81,7 @@
1.4 "(\<lambda>x. c) \<in> borel_measurable M"
1.5 by (auto intro!: measurable_const)
1.6
1.7 -lemma (in sigma_algebra) borel_measurable_indicator:
1.8 +lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
1.9 assumes A: "A \<in> sets M"
1.10 shows "indicator A \<in> borel_measurable M"
1.11 unfolding indicator_def_raw using A
2.1 --- a/src/HOL/Probability/Probability_Space.thy Thu Aug 26 15:20:41 2010 +0200
2.2 +++ b/src/HOL/Probability/Probability_Space.thy Thu Aug 26 18:41:54 2010 +0200
2.3 @@ -1,5 +1,5 @@
2.4 theory Probability_Space
2.5 -imports Lebesgue_Integration
2.6 +imports Lebesgue_Integration Radon_Nikodym
2.7 begin
2.8
2.9 lemma (in measure_space) measure_inter_full_set:
2.10 @@ -463,4 +463,101 @@
2.11 by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
2.12 qed
2.13
2.14 +lemma (in prob_space) prob_space_subalgebra:
2.15 + assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
2.16 + shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
2.17 +
2.18 +lemma (in measure_space) measure_space_subalgebra:
2.19 + assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
2.20 + shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
2.21 +
2.22 +lemma pinfreal_0_less_mult_iff[simp]:
2.23 + fixes x y :: pinfreal shows "0 < x * y \<longleftrightarrow> 0 < x \<and> 0 < y"
2.24 + by (cases x, cases y) (auto simp: zero_less_mult_iff)
2.25 +
2.26 +lemma (in sigma_algebra) simple_function_subalgebra:
2.27 + assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f"
2.28 + and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)"
2.29 + shows "simple_function f"
2.30 + using assms
2.31 + unfolding simple_function_def
2.32 + unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)]
2.33 + by auto
2.34 +
2.35 +lemma (in measure_space) simple_integral_subalgebra[simp]:
2.36 + assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>"
2.37 + shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral"
2.38 + unfolding simple_integral_def_raw
2.39 + unfolding measure_space.simple_integral_def_raw[OF assms] by simp
2.40 +
2.41 +lemma (in sigma_algebra) borel_measurable_subalgebra:
2.42 + assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
2.43 + shows "f \<in> borel_measurable M"
2.44 + using assms unfolding measurable_def by auto
2.45 +
2.46 +lemma (in measure_space) positive_integral_subalgebra[simp]:
2.47 + assumes borel: "f \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
2.48 + and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets := N\<rparr>)"
2.49 + shows "measure_space.positive_integral (M\<lparr>sets := N\<rparr>) \<mu> f = positive_integral f"
2.50 +proof -
2.51 + note msN = measure_space_subalgebra[OF N_subalgebra]
2.52 + then interpret N: measure_space "M\<lparr>sets:=N\<rparr>" \<mu> .
2.53 +
2.54 + from N.borel_measurable_implies_simple_function_sequence[OF borel]
2.55 + obtain fs where Nsf: "\<And>i. N.simple_function (fs i)" and "fs \<up> f" by blast
2.56 + then have sf: "\<And>i. simple_function (fs i)"
2.57 + using simple_function_subalgebra[OF _ N_subalgebra] by blast
2.58 +
2.59 + from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
2.60 + show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
2.61 +qed
2.62 +(*
2.63 +lemma (in prob_space)
2.64 + fixes X :: "'a \<Rightarrow> pinfreal"
2.65 + assumes borel: "X \<in> borel_measurable M"
2.66 + and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
2.67 + shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
2.68 + positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
2.69 +proof -
2.70 + interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
2.71 + using prob_space_subalgebra[OF N_subalgebra] .
2.72 +
2.73 + let "?f A" = "\<lambda>x. X x * indicator A x"
2.74 + let "?Q A" = "positive_integral (?f A)"
2.75 +
2.76 + from measure_space_density[OF borel]
2.77 + have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
2.78 + by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
2.79 + then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
2.80 +
2.81 + have "P.absolutely_continuous ?Q"
2.82 + unfolding P.absolutely_continuous_def
2.83 + proof (safe, simp)
2.84 + fix A assume "A \<in> N" "\<mu> A = 0"
2.85 + moreover then have f_borel: "?f A \<in> borel_measurable M"
2.86 + using borel N_subalgebra by (auto intro: borel_measurable_indicator)
2.87 + moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
2.88 + by (auto simp: indicator_def)
2.89 + moreover have "\<mu> \<dots> \<le> \<mu> A"
2.90 + using `A \<in> N` N_subalgebra f_borel
2.91 + by (auto intro!: measure_mono Int[of _ A] measurable_sets)
2.92 + ultimately show "?Q A = 0"
2.93 + by (simp add: positive_integral_0_iff)
2.94 + qed
2.95 + from P.Radon_Nikodym[OF Q this]
2.96 + obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
2.97 + "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
2.98 + by blast
2.99 + show ?thesis
2.100 + proof (intro bexI[OF _ Y(1)] ballI)
2.101 + fix A assume "A \<in> N"
2.102 + have "positive_integral (\<lambda>x. Y x * indicator A x) = P.positive_integral (\<lambda>x. Y x * indicator A x)"
2.103 + unfolding P.positive_integral_def positive_integral_def
2.104 + unfolding P.simple_integral_def_raw simple_integral_def_raw
2.105 + apply simp
2.106 + show "positive_integral (\<lambda>x. Y x * indicator A x) = ?Q A"
2.107 + qed
2.108 +qed
2.109 +*)
2.110 +
2.111 end