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

src/HOL/Probability/Information.thy

changeset 50002 | ce0d316b5b44 |

parent 49999 | dfb63b9b8908 |

child 50003 | 8c213922ed49 |

1.1 --- a/src/HOL/Probability/Information.thy Fri Nov 02 14:00:39 2012 +0100 1.2 +++ b/src/HOL/Probability/Information.thy Fri Nov 02 14:23:40 2012 +0100 1.3 @@ -446,7 +446,7 @@ 1.4 shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))" 1.5 using assms unfolding finite_entropy_def 1.6 using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"] 1.7 - by (auto intro: distributed_real_measurable) 1.8 + by (auto dest!: distributed_real_measurable) 1.9 1.10 subsection {* Mutual Information *} 1.11 1.12 @@ -1578,7 +1578,7 @@ 1.13 have "random_variable (count_space (X ` space M)) X" 1.14 by (simp add: comp_def) 1.15 then have "simple_function M X" 1.16 - unfolding simple_function_def by auto 1.17 + unfolding simple_function_def by (auto simp: measurable_count_space_eq2) 1.18 then have "simple_distributed M X ?Px" 1.19 by (rule simple_distributedI) auto 1.20 then show "distributed M (count_space (X ` space M)) X ?Px"