--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 09 14:14:45 2012 +0100
@@ -276,6 +276,10 @@
"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 prod_emb_mono:
+ "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
+ by (auto simp: prod_emb_def)
+
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))}
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri Nov 09 14:14:45 2012 +0100
@@ -102,7 +102,11 @@
show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
using sets[THEN sets_into_space] by (auto simp: space_PiM)
have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
- using M.not_empty by auto
+ proof
+ fix i assume "i \<in> L"
+ interpret prob_space "P {i}" using prob_space by simp
+ from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
+ qed
from bchoice[OF this]
show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
@@ -240,14 +244,12 @@
show ?thesis
proof (intro positive_def[THEN iffD2] conjI ballI)
from generatorE[OF G.empty_sets] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
have "X = {}"
by (rule prod_emb_injective[of J I]) simp_all
then show "\<mu>G {} = 0" by simp
next
fix A assume "A \<in> generator"
from generatorE[OF this] guess J X . note this[simp]
- interpret J: finite_product_sigma_finite M J by default fact
show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
qed
qed
@@ -264,7 +266,6 @@
assume "A \<inter> B = {}"
have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
using J K by auto
- interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
apply (rule prod_emb_injective[of "J \<union> K" I])
apply (insert `A \<inter> B = {}` JK J K)
--- a/src/HOL/Probability/Projective_Family.thy Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Fri Nov 09 14:14:45 2012 +0100
@@ -28,8 +28,6 @@
assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
- assumes proj_finite_measure: "\<And>J. finite J \<Longrightarrow> emeasure (P J) (space (PiM J M)) \<noteq> \<infinity>"
- assumes measure_space: "\<And>i. prob_space (M i)"
begin
lemma emeasure_PiP:
@@ -79,8 +77,7 @@
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
show "Int_stable ?J"
by (rule Int_stable_PiE)
- interpret finite_measure "P J" using proj_finite_measure `finite J`
- by (intro finite_measureI) (simp add: proj_space)
+ interpret prob_space "P J" using prob_space `finite J` by simp
show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
@@ -104,7 +101,4 @@
end
-sublocale projective_family \<subseteq> M: prob_space "M i" for i
- by (rule measure_space)
-
end