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.21      by (simp add: sigma_finite_measure_count_space_finite)
    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]