src/HOL/Probability/Infinite_Product_Measure.thy
changeset 50123 69b35a75caf3
parent 50099 a58bb401af80
child 50244 de72bbe42190
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
     1.3 @@ -234,11 +234,9 @@
     1.4                using w'(1) J(3)[of "Suc k"]
     1.5                by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
     1.6              show ?thesis
     1.7 -              apply (rule exI[of _ ?w])
     1.8                using w' J_mono[of k "Suc k"] wk unfolding *
     1.9 -              apply (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM)
    1.10 -              apply (force simp: extensional_def)
    1.11 -              done
    1.12 +              by (intro exI[of _ ?w])
    1.13 +                 (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
    1.14            qed
    1.15            then have "?P k (w k) (w (Suc k))"
    1.16              unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
    1.17 @@ -295,8 +293,8 @@
    1.18          using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
    1.19  
    1.20        { fix n
    1.21 -        have "restrict w' (J n) = w n" using w(1)
    1.22 -          by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def space_PiM)
    1.23 +        have "restrict w' (J n) = w n" using w(1)[of n]
    1.24 +          by (auto simp add: fun_eq_iff space_PiM)
    1.25          with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
    1.26          then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
    1.27        then have "w' \<in> (\<Inter>i. A i)" by auto
    1.28 @@ -391,7 +389,7 @@
    1.29  lemma sets_Collect_single':
    1.30    "i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
    1.31    using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
    1.32 -  by (simp add: space_PiM Pi_iff cong: conj_cong)
    1.33 +  by (simp add: space_PiM PiE_iff cong: conj_cong)
    1.34  
    1.35  lemma (in finite_product_prob_space) finite_measure_PiM_emb:
    1.36    "(\<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.37 @@ -462,7 +460,7 @@
    1.38    "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
    1.39  proof (rule measurable_PiM_single)
    1.40    show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
    1.41 -    by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
    1.42 +    by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
    1.43    fix j :: nat and A assume A: "A \<in> sets M"
    1.44    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.45      (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.46 @@ -550,7 +548,7 @@
    1.47    with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
    1.48      (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
    1.49      (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    1.50 -   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib Pi_iff
    1.51 +   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
    1.52                 split: split_comb_seq split_comb_seq_asm)
    1.53    then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^isub>M S) (?E \<times> ?F)"
    1.54      by (subst emeasure_distr[OF measurable_comb_seq])
    1.55 @@ -581,7 +579,7 @@
    1.56      using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    1.57    with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
    1.58      (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    1.59 -   by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
    1.60 +   by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
    1.61        split: nat.split nat.split_asm)
    1.62    then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
    1.63      by (subst emeasure_distr)