--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:27 2012 +0200
@@ -33,15 +33,18 @@
{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
(\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
+lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
+ using space_closed[of A] space_closed[of B] by auto
+
lemma space_pair_measure:
"space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
- unfolding pair_measure_def using space_closed[of A] space_closed[of B]
- by (intro space_measure_of) auto
+ unfolding pair_measure_def using pair_measure_closed[of A B]
+ by (rule space_measure_of)
lemma sets_pair_measure:
"sets (A \<Otimes>\<^isub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
- unfolding pair_measure_def using space_closed[of A] space_closed[of B]
- by (intro sets_measure_of) auto
+ unfolding pair_measure_def using pair_measure_closed[of A B]
+ by (rule sets_measure_of)
lemma sets_pair_measure_cong[cong]:
"sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
@@ -162,40 +165,24 @@
assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
(is "?s Q \<in> _")
-proof -
- let ?\<Omega> = "space N \<times> space M" and ?D = "{A\<in>sets (N \<Otimes>\<^isub>M M). ?s A \<in> borel_measurable N}"
- note space_pair_measure[simp]
- interpret dynkin_system ?\<Omega> ?D
- proof (intro dynkin_systemI)
- fix A assume "A \<in> ?D" then show "A \<subseteq> ?\<Omega>"
- using sets_into_space[of A "N \<Otimes>\<^isub>M M"] by simp
- next
- from top show "?\<Omega> \<in> ?D"
- by (auto simp add: if_distrib intro!: measurable_If)
- next
- fix A assume "A \<in> ?D"
- with sets_into_space have "\<And>x. emeasure M (Pair x -` (?\<Omega> - A)) =
- (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
- by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
- with `A \<in> ?D` top show "?\<Omega> - A \<in> ?D"
- by (auto intro!: measurable_If)
- next
- fix F :: "nat \<Rightarrow> ('b\<times>'a) set" assume "disjoint_family F" "range F \<subseteq> ?D"
- moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
- by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
- ultimately show "(\<Union>i. F i) \<in> ?D"
- by (auto simp: vimage_UN intro!: borel_measurable_psuminf)
- qed
- let ?G = "{a \<times> b | a b. a \<in> sets N \<and> b \<in> sets M}"
- have "sigma_sets ?\<Omega> ?G = ?D"
- proof (rule dynkin_lemma)
- show "?G \<subseteq> ?D"
- by (auto simp: if_distrib Int_def[symmetric] intro!: measurable_If)
- qed (auto simp: sets_pair_measure Int_stable_pair_measure_generator)
- with `Q \<in> sets (N \<Otimes>\<^isub>M M)` have "Q \<in> ?D"
- by (simp add: sets_pair_measure[symmetric])
- then show "?s Q \<in> borel_measurable N" by simp
-qed
+ using Int_stable_pair_measure_generator pair_measure_closed assms
+ unfolding sets_pair_measure
+proof (induct rule: sigma_sets_induct_disjoint)
+ case (compl A)
+ with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
+ (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
+ unfolding sets_pair_measure[symmetric]
+ by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
+ with compl top show ?case
+ by (auto intro!: measurable_If simp: space_pair_measure)
+next
+ case (union F)
+ moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
+ unfolding sets_pair_measure[symmetric]
+ by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
+ ultimately show ?case
+ by (auto simp: vimage_UN)
+qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
lemma (in sigma_finite_measure) measurable_emeasure_Pair:
assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
--- a/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:27 2012 +0200
@@ -633,48 +633,45 @@
proof -
let ?\<mu> = "emeasure M" and ?\<nu> = "emeasure N"
interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
- { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
+ have "space M = \<Omega>"
+ using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
+
+ { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
- let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
- interpret D: dynkin_system \<Omega> ?D
- proof (rule dynkin_systemI, simp_all)
- fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
- then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
+ assume "D \<in> sets M"
+ with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
+ unfolding M
+ proof (induct rule: sigma_sets_induct_disjoint)
+ case (basic A)
+ then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def)
+ then show ?case using eq by auto
next
- have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
- then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
- using `F \<in> E` eq by (auto intro: sigma_sets_top)
+ case empty then show ?case by simp
next
- fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
+ case (compl A)
then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
- using `F \<in> E` S.sets_into_space by auto
+ using `F \<in> E` S.sets_into_space by (auto simp: M)
have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
- also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
+ also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp
also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
by (auto intro!: emeasure_Diff[symmetric] simp: M N)
- finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
- using * by auto
+ finally show ?case
+ using `space M = \<Omega>` by auto
next
- fix A :: "nat \<Rightarrow> 'a set"
- assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
+ case (union A)
then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
- with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))"
+ with A show ?case
by auto
- qed
- have *: "sigma_sets \<Omega> E = ?D"
- using `F \<in> E` `Int_stable E`
- by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
- have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
- unfolding M by (subst (asm) *) auto }
+ qed }
note * = this
show "M = N"
proof (rule measure_eqI)
@@ -684,9 +681,7 @@
using A(1) by (auto simp: subset_eq M)
fix F assume "F \<in> sets M"
let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
- have "space M = \<Omega>"
- using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
- then have F_eq: "F = (\<Union>i. ?D i)"
+ from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
have [simp, intro]: "\<And>i. ?D i \<in> sets M"
using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 10 12:12:26 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 10 12:12:27 2012 +0200
@@ -2041,4 +2041,25 @@
using assms by (auto simp: dynkin_def)
qed
+lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+ assumes "Int_stable G"
+ and closed: "G \<subseteq> Pow \<Omega>"
+ and A: "A \<in> sigma_sets \<Omega> G"
+ assumes basic: "\<And>A. A \<in> G \<Longrightarrow> P A"
+ and empty: "P {}"
+ and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
+ and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
+ shows "P A"
+proof -
+ let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
+ interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
+ using closed by (rule sigma_algebra_sigma_sets)
+ from compl[OF _ empty] closed have space: "P \<Omega>" by simp
+ interpret dynkin_system \<Omega> ?D
+ by default (auto dest: sets_into_space intro!: space compl union)
+ have "sigma_sets \<Omega> G = ?D"
+ by (rule dynkin_lemma) (auto simp: basic `Int_stable G`)
+ with A show ?thesis by auto
+qed
+
end