src/HOL/Probability/Information.thy
 changeset 49792 43f49922811d parent 49791 e0854abfb3fc child 49802 dd8dffaf84b9
```     1.1 --- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:28 2012 +0200
1.2 +++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:29 2012 +0200
1.3 @@ -1227,12 +1227,16 @@
1.4  qed
1.5
1.6  lemma (in information_space) conditional_entropy_eq:
1.7 -  assumes Y: "simple_distributed M Y Py" and X: "simple_function M X"
1.8 +  assumes Y: "simple_distributed M Y Py"
1.9    assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
1.10      shows "\<H>(X | Y) = - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
1.11  proof (subst conditional_entropy_generic_eq[OF _ _
1.12    simple_distributed[OF Y] simple_distributed_joint[OF XY]])
1.13 -  have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def)
1.14 +  have "finite ((\<lambda>x. (X x, Y x))`space M)"
1.15 +    using XY unfolding simple_distributed_def by auto
1.16 +  from finite_imageI[OF this, of fst]
1.17 +  have [simp]: "finite (X`space M)"
1.18 +    by (simp add: image_compose[symmetric] comp_def)
1.19    note Y[THEN simple_distributed_finite, simp]
1.20    show "sigma_finite_measure (count_space (X ` space M))"
1.22 @@ -1241,11 +1245,11 @@
1.23    let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
1.24    have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
1.25      (is "?P = ?C")
1.26 -    using X Y by (simp add: simple_distributed_finite pair_measure_count_space)
1.27 +    using Y by (simp add: simple_distributed_finite pair_measure_count_space)
1.28    have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
1.29      (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / Py (snd x)) else 0)"
1.30      by auto
1.31 -  from X Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
1.32 +  from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
1.33      - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
1.34      by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
1.35  qed
1.36 @@ -1277,7 +1281,7 @@
1.37      by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
1.38    then show ?thesis
1.39      apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
1.40 -    apply (subst conditional_entropy_eq[OF Py X Pxy])
1.41 +    apply (subst conditional_entropy_eq[OF Py Pxy])
1.42      apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
1.43                  log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
1.44      using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
```