--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
@@ -385,7 +385,7 @@
then show "sets ?D = sigma_sets (space ?P) ?E"
by simp
next
- show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+ show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
using F by (auto simp: space_pair_measure)
next
fix X assume "X \<in> ?E"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
@@ -751,7 +751,6 @@
show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
using fin by (auto simp: prod_algebra_eq_finite)
- show "incseq ?F" by fact
show "(\<Union>i. \<Pi>\<^isub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i))"
using F(3) by (simp add: space_PiM)
next
--- a/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:23 2012 +0200
@@ -23,13 +23,6 @@
qed auto
definition (in prob_space)
- "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
- (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
-
-definition (in prob_space)
- "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
-
-definition (in prob_space)
"indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
@@ -37,6 +30,24 @@
"indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
definition (in prob_space)
+ indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
+
+lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
+ by auto
+
+lemma (in prob_space) indep_events_def:
+ "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
+ (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
+ unfolding indep_events_def_alt indep_sets_def
+ apply (simp add: Ball_def Pi_iff image_subset_iff_funcset)
+ apply (intro conj_cong refl arg_cong[where f=All] ext imp_cong)
+ apply auto
+ done
+
+definition (in prob_space)
+ "indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV"
+
+definition (in prob_space)
"indep_vars M' X I \<longleftrightarrow>
(\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
@@ -48,11 +59,6 @@
"I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
-lemma (in prob_space) indep_sets_singleton_iff_indep_events:
- "indep_sets (\<lambda>i. {F i}) I \<longleftrightarrow> indep_events F I"
- unfolding indep_sets_def indep_events_def
- by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff)
-
lemma (in prob_space) indep_events_finite_index_events:
"indep_events F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_events F J)"
by (auto simp: indep_events_def)
@@ -660,7 +666,7 @@
show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
proof (rule indep_sets_sigma)
show "indep_sets (\<lambda>i. {F i}) UNIV"
- unfolding indep_sets_singleton_iff_indep_events by fact
+ unfolding indep_events_def_alt[symmetric] by fact
fix i show "Int_stable {F i}"
unfolding Int_stable_def by simp
qed
@@ -892,7 +898,7 @@
show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')"
by (simp add: sets_PiM space_PiM cong: prod_algebra_cong)
let ?A = "\<lambda>i. \<Pi>\<^isub>E i\<in>I. space (M' i)"
- show "range ?A \<subseteq> prod_algebra I M'" "incseq ?A" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')"
+ show "range ?A \<subseteq> prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')"
by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong)
{ fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
next
@@ -1042,7 +1048,7 @@
then show "sets M = sigma_sets (space ?P) ?E"
using sets[symmetric] by simp
next
- show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+ show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
using F by (auto simp: space_pair_measure)
next
fix X assume "X \<in> ?E"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200
@@ -87,7 +87,7 @@
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
show "Int_stable ?J"
by (rule Int_stable_PiE)
- show "range ?F \<subseteq> ?J" "incseq ?F" "(\<Union>i. ?F i) = ?\<Omega>"
+ show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
using `finite J` by (auto intro!: prod_algebraI_finite)
{ fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200
@@ -569,7 +569,6 @@
by (simp_all add: borel_eq_atLeastAtMost sets_eq)
show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
- show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
{ fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto
--- a/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:23 2012 +0200
@@ -628,7 +628,7 @@
and eq: "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
and M: "sets M = sigma_sets \<Omega> E"
and N: "sets N = sigma_sets \<Omega> E"
- and A: "range A \<subseteq> E" "incseq A" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
+ and A: "range A \<subseteq> E" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
shows "M = N"
proof -
let ?\<mu> = "emeasure M" and ?\<nu> = "emeasure N"
@@ -673,25 +673,38 @@
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> sigma_sets \<Omega> E \<Longrightarrow> ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)"
- by (subst (asm) *) auto }
+ have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
+ unfolding M by (subst (asm) *) auto }
note * = this
show "M = N"
proof (rule measure_eqI)
show "sets M = sets N"
using M N by simp
+ have [simp, intro]: "\<And>i. A i \<in> sets M"
+ using A(1) by (auto simp: subset_eq M)
fix F assume "F \<in> sets M"
- then have "F \<in> sigma_sets \<Omega> E"
- using M by simp
- let ?A = "\<lambda>i. A i \<inter> F"
- have "range ?A \<subseteq> sigma_sets \<Omega> E" "incseq ?A"
- using A(1,2) `F \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
- moreover
- { fix i have "?\<mu> (?A i) = ?\<nu> (?A i)"
- using *[of "A i" F] `F \<in> sigma_sets \<Omega> E` A finite by auto }
- ultimately show "?\<mu> F = ?\<nu> F"
- using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `F \<in> sigma_sets \<Omega> E`
- by (auto simp: M N SUP_emeasure_incseq)
+ 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)"
+ 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`
+ by (auto simp: subset_eq)
+ have "disjoint_family ?D"
+ by (auto simp: disjoint_family_disjointed)
+ moreover
+ { fix i
+ have "A i \<inter> ?D i = ?D i"
+ by (auto simp: disjointed_def)
+ then have "emeasure M (?D i) = emeasure N (?D i)"
+ using *[of "A i" "?D i", OF _ A(3)] A(1) by auto }
+ ultimately show "emeasure M F = emeasure N F"
+ using N M
+ apply (subst (1 2) F_eq)
+ apply (subst (1 2) suminf_emeasure[symmetric])
+ apply auto
+ done
qed
qed