author hoelzl Wed Oct 10 12:12:27 2012 +0200 (2012-10-10) changeset 49790 6b9b9ebba47d parent 49789 e0a4cb91a8a9 child 49791 e0854abfb3fc
remove unneeded assumption from conditional_entropy_generic_eq
```     1.1 --- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:27 2012 +0200
1.2 +++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:27 2012 +0200
1.3 @@ -1121,7 +1121,6 @@
1.4  lemma (in information_space)
1.5    fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
1.6    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
1.7 -  assumes Px: "distributed M S X Px"
1.8    assumes Py: "distributed M T Y Py"
1.9    assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
1.10    assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
1.11 @@ -1149,17 +1148,13 @@
1.12      by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
1.13    finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
1.14
1.15 -  have ae1: "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
1.16 -    by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
1.17 -  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
1.18 +  have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
1.19      by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
1.20 -  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
1.21 -    using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
1.22    moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
1.23      using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
1.24    moreover note ae5 = Pxy[THEN distributed_real_AE]
1.25 -  ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Px (fst x) \<and> 0 \<le> Py (snd x) \<and>
1.26 -    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Px (fst x) \<and> 0 < Py (snd x)))"
1.27 +  ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Py (snd x) \<and>
1.28 +    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Py (snd x)))"
1.29      by eventually_elim auto
1.30
1.31    from pos have ae: "AE x in S \<Otimes>\<^isub>M T.
1.32 @@ -1180,7 +1175,7 @@
1.33    assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
1.34      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.35  proof (subst conditional_entropy_generic_eq[OF _ _
1.36 -  simple_distributed[OF simple_distributedI[OF X refl]] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
1.37 +  simple_distributed[OF Y] simple_distributed_joint[OF XY]])
1.38    have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def)
1.39    note Y[THEN simple_distributed_finite, simp]
1.40    show "sigma_finite_measure (count_space (X ` space M))"
1.41 @@ -1234,7 +1229,7 @@
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]
1.45 -    apply (auto simp add: not_le[symmetric] AE_count_space)
1.46 +  apply (auto simp add: not_le[symmetric] AE_count_space)
1.47      done
1.48  qed
1.49
```