--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 08 20:02:41 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Nov 06 11:03:28 2012 +0100
@@ -43,6 +43,15 @@
"extensional I \<inter> extensional I' = extensional (I \<inter> I')"
unfolding extensional_def by auto
+lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
+ by (auto simp: extensional_def)
+
+lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
+ unfolding restrict_def extensional_def by auto
+
+lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
+ unfolding restrict_def by (simp add: fun_eq_iff)
+
definition
"merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
@@ -253,6 +262,20 @@
lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
by (auto simp: prod_emb_def Pi_iff)
+lemma prod_emb_trans[simp]:
+ "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
+ by (auto simp add: Int_absorb1 prod_emb_def)
+
+lemma prod_emb_Pi:
+ assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
+ shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
+ using assms space_closed
+ by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
+
+lemma prod_emb_id:
+ "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
+ by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
+
definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
"PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
{(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
@@ -309,6 +332,17 @@
\<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
by (auto simp: prod_algebra_def Pi_iff)
+lemma prod_algebraI_finite:
+ "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
+ using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
+
+lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
+proof (safe intro!: Int_stableI)
+ fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
+ then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
+ by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
+qed
+
lemma prod_algebraE:
assumes A: "A \<in> prod_algebra I M"
obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
@@ -546,6 +580,14 @@
using A X by (auto intro!: measurable_sets)
qed (insert X, auto dest: measurable_space)
+lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
+ by (intro measurable_restrict measurable_component_singleton) auto
+
+lemma measurable_prod_emb[intro, simp]:
+ "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
+ unfolding prod_emb_def space_PiM[symmetric]
+ by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
+
lemma sets_in_Pi_aux:
"finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
{x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 08 20:02:41 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Nov 06 11:03:28 2012 +0100
@@ -8,15 +8,6 @@
imports Probability_Measure Caratheodory
begin
-lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
- by (auto simp: extensional_def)
-
-lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
- unfolding restrict_def extensional_def by auto
-
-lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
- unfolding restrict_def by (simp add: fun_eq_iff)
-
lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
unfolding merge_def by auto
@@ -44,39 +35,6 @@
qed
qed
-lemma prod_algebraI_finite:
- "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
- using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
-
-lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
-proof (safe intro!: Int_stableI)
- fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
- then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
- by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
-qed
-
-lemma prod_emb_trans[simp]:
- "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
- by (auto simp add: Int_absorb1 prod_emb_def)
-
-lemma prod_emb_Pi:
- assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
- shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
- using assms space_closed
- by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
-
-lemma prod_emb_id:
- "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
- by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
-
-lemma measurable_prod_emb[intro, simp]:
- "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
- unfolding prod_emb_def space_PiM[symmetric]
- by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
-
-lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
- by (intro measurable_restrict measurable_component_singleton) auto
-
lemma (in product_prob_space) distr_restrict:
assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")