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

src/HOL/Probability/Information.thy

changeset 45710 | 10192f961619 |

parent 44890 | 22f665a2e91c |

child 45712 | 852597248663 |

1.1 --- a/src/HOL/Probability/Information.thy Thu Dec 01 13:34:16 2011 +0100 1.2 +++ b/src/HOL/Probability/Information.thy Thu Dec 01 14:03:57 2011 +0100 1.3 @@ -1020,13 +1020,6 @@ 1.4 using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"] 1.5 using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp 1.6 1.7 -lemma (in prob_space) setsum_real_distribution: 1.8 - fixes MX :: "('c, 'd) measure_space_scheme" 1.9 - assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1" 1.10 - using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV, measure = undefined \<rparr>" "\<lambda>x. ()" "{()}"] 1.11 - using sigma_algebra_Pow[of "UNIV::unit set" "\<lparr> measure = undefined \<rparr>"] 1.12 - by auto 1.13 - 1.14 lemma (in information_space) conditional_mutual_information_generic_positive: 1.15 assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z" 1.16 shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z" 1.17 @@ -1101,7 +1094,7 @@ 1.18 setsum_joint_distribution_singleton[OF Y Z] 1.19 intro!: setsum_cong) 1.20 also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0" 1.21 - unfolding setsum_real_distribution[OF Z] by simp 1.22 + unfolding setsum_distribution[OF Z] by simp 1.23 finally show ?thesis by simp 1.24 qed 1.25