summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Independent_Family.thy

changeset 49776 | 199d1d5bb17e |

parent 49772 | 75660d89c339 |

child 49781 | 59b219ca3513 |

1.1 --- a/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:17 2012 +0200 1.2 +++ b/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:18 2012 +0200 1.3 @@ -1035,7 +1035,7 @@ 1.4 fix X assume "X \<in> ?E" 1.5 then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto 1.6 then have "emeasure ?P X = emeasure M1 A * emeasure M2 B" 1.7 - by (simp add: emeasure_pair_measure_Times) 1.8 + by (simp add: M2.emeasure_pair_measure_Times) 1.9 also have "\<dots> = emeasure M (A \<times> B)" 1.10 using A B emeasure by auto 1.11 finally show "emeasure ?P X = emeasure M X" 1.12 @@ -1143,7 +1143,7 @@ 1.13 also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)" 1.14 unfolding `?S \<Otimes>\<^isub>M ?T = ?J` .. 1.15 also have "\<dots> = emeasure ?S A * emeasure ?T B" 1.16 - using ab by (simp add: XY.emeasure_pair_measure_Times) 1.17 + using ab by (simp add: Y.emeasure_pair_measure_Times) 1.18 finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) = 1.19 prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)" 1.20 using rvs ab by (simp add: emeasure_eq_measure emeasure_distr)