equal
deleted
inserted
replaced
34 from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp |
34 from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp |
35 qed |
35 qed |
36 |
36 |
37 abbreviation (in prob_space) "events \<equiv> sets M" |
37 abbreviation (in prob_space) "events \<equiv> sets M" |
38 abbreviation (in prob_space) "prob \<equiv> \<mu>'" |
38 abbreviation (in prob_space) "prob \<equiv> \<mu>'" |
39 abbreviation (in prob_space) "prob_preserving \<equiv> measure_preserving" |
|
40 abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'" |
39 abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'" |
41 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M" |
40 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M" |
42 |
41 |
43 definition (in prob_space) |
42 definition (in prob_space) |
44 "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" |
43 "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" |