src/HOL/Probability/Independent_Family.thy
changeset 50123 69b35a75caf3
parent 50104 de19856feb54
child 50244 de72bbe42190
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 16:14:18 2012 +0100
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 12:29:02 2012 +0100
     1.3 @@ -867,7 +867,7 @@
     1.4        then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
     1.5          by (simp add: emeasure_distr X)
     1.6        also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
     1.7 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
     1.8 +        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
     1.9        also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
    1.10          using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J]
    1.11          by (auto simp: emeasure_eq_measure setprod_ereal)
    1.12 @@ -898,7 +898,7 @@
    1.13          Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
    1.14        let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)"
    1.15        from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
    1.16 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
    1.17 +        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
    1.18        then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
    1.19          by simp
    1.20        also have "\<dots> = emeasure ?D ?E"