author hoelzl Wed, 10 Oct 2012 12:12:23 +0200 changeset 49784 5e5b2da42a69 parent 49783 38b84d1802ed child 49785 0a8adca22974
remove incseq assumption from measure_eqI_generator_eq
```--- 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 @@

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