equal
deleted
inserted
replaced
5 |
5 |
6 header {*Information theory*} |
6 header {*Information theory*} |
7 |
7 |
8 theory Information |
8 theory Information |
9 imports |
9 imports |
10 Probability_Space |
10 Probability_Measure |
11 "~~/src/HOL/Library/Convex" |
11 "~~/src/HOL/Library/Convex" |
12 begin |
12 begin |
13 |
13 |
14 lemma (in prob_space) not_zero_less_distribution[simp]: |
14 lemma (in prob_space) not_zero_less_distribution[simp]: |
15 "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0" |
15 "(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0" |