src/HOL/Probability/Infinite_Product_Measure.thy
changeset 50244 de72bbe42190
parent 50123 69b35a75caf3
child 50252 4aa34bd43228
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4    next
     1.5      fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
     1.6      then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
     1.7 -      by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
     1.8 +      by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
     1.9      have "emb I J (Pi\<^isub>E J X) \<in> generator"
    1.10        using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
    1.11      then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
    1.12 @@ -393,7 +393,7 @@
    1.13  
    1.14  lemma (in finite_product_prob_space) finite_measure_PiM_emb:
    1.15    "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
    1.16 -  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
    1.17 +  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
    1.18    by auto
    1.19  
    1.20  lemma (in product_prob_space) PiM_component:
    1.21 @@ -465,7 +465,7 @@
    1.22    then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
    1.23      (if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
    1.24                else space (\<Pi>\<^isub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
    1.25 -    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets_into_space)
    1.26 +    by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
    1.27    show "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
    1.28      unfolding * by (auto simp: A intro!: sets_Collect_single)
    1.29  qed
    1.30 @@ -507,7 +507,7 @@
    1.31    shows "Pi UNIV E \<in> sets S"
    1.32  proof -
    1.33    have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
    1.34 -    using E E[THEN sets_into_space]
    1.35 +    using E E[THEN sets.sets_into_space]
    1.36      by (auto simp: prod_emb_def Pi_iff extensional_def) blast
    1.37    with E show ?thesis by auto
    1.38  qed
    1.39 @@ -520,7 +520,7 @@
    1.40    have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
    1.41      using E by (simp add: measure_PiM_emb)
    1.42    moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
    1.43 -    using E E[THEN sets_into_space]
    1.44 +    using E E[THEN sets.sets_into_space]
    1.45      by (auto simp: prod_emb_def extensional_def Pi_iff) blast
    1.46    moreover have "range ?E \<subseteq> sets S"
    1.47      using E by auto
    1.48 @@ -544,7 +544,7 @@
    1.49    fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
    1.50    let ?X = "prod_emb ?I ?M J (\<Pi>\<^isub>E j\<in>J. E j)"
    1.51    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    1.52 -    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    1.53 +    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    1.54    with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
    1.55      (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
    1.56      (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    1.57 @@ -576,7 +576,7 @@
    1.58    fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
    1.59    let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
    1.60    have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
    1.61 -    using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    1.62 +    using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    1.63    with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
    1.64      (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    1.65     by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib