# HG changeset patch # User hoelzl # Date 1349863947 -7200 # Node ID 6b9b9ebba47d629bf4a99fd5e05242b7cd91143b # Parent e0a4cb91a8a9333a8aab00ac94f263dca3302e4f remove unneeded assumption from conditional_entropy_generic_eq diff -r e0a4cb91a8a9 -r 6b9b9ebba47d src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Wed Oct 10 12:12:27 2012 +0200 +++ b/src/HOL/Probability/Information.thy Wed Oct 10 12:12:27 2012 +0200 @@ -1121,7 +1121,6 @@ lemma (in information_space) fixes Px :: "'b \ real" and Py :: "'c \ real" assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" - assumes Px: "distributed M S X Px" assumes Py: "distributed M T Y Py" assumes Pxy: "distributed M (S \\<^isub>M T) (\x. (X x, Y x)) Pxy" assumes I1: "integrable (S \\<^isub>M T) (\x. Pxy x * log b (Pxy x))" @@ -1149,17 +1148,13 @@ by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong) finally have e_eq: "entropy b T Y = - (\(x,y). Pxy (x,y) * log b (Py y) \(S \\<^isub>M T))" . - have ae1: "AE x in S \\<^isub>M T. Px (fst x) = 0 \ Pxy x = 0" - by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair) - moreover have ae2: "AE x in S \\<^isub>M T. Py (snd x) = 0 \ Pxy x = 0" + have ae2: "AE x in S \\<^isub>M T. Py (snd x) = 0 \ Pxy x = 0" by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair) - moreover have ae3: "AE x in S \\<^isub>M T. 0 \ Px (fst x)" - using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable) moreover have ae4: "AE x in S \\<^isub>M T. 0 \ Py (snd x)" using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable) moreover note ae5 = Pxy[THEN distributed_real_AE] - ultimately have pos: "AE x in S \\<^isub>M T. 0 \ Pxy x \ 0 \ Px (fst x) \ 0 \ Py (snd x) \ - (Pxy x = 0 \ (Pxy x \ 0 \ 0 < Pxy x \ 0 < Px (fst x) \ 0 < Py (snd x)))" + ultimately have pos: "AE x in S \\<^isub>M T. 0 \ Pxy x \ 0 \ Py (snd x) \ + (Pxy x = 0 \ (Pxy x \ 0 \ 0 < Pxy x \ 0 < Py (snd x)))" by eventually_elim auto from pos have ae: "AE x in S \\<^isub>M T. @@ -1180,7 +1175,7 @@ assumes XY: "simple_distributed M (\x. (X x, Y x)) Pxy" shows "\(X | Y) = - (\(x, y)\(\x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))" proof (subst conditional_entropy_generic_eq[OF _ _ - simple_distributed[OF simple_distributedI[OF X refl]] simple_distributed[OF Y] simple_distributed_joint[OF XY]]) + simple_distributed[OF Y] simple_distributed_joint[OF XY]]) have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def) note Y[THEN simple_distributed_finite, simp] show "sigma_finite_measure (count_space (X ` space M))" @@ -1234,7 +1229,7 @@ apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj] log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space) using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE] - apply (auto simp add: not_le[symmetric] AE_count_space) + apply (auto simp add: not_le[symmetric] AE_count_space) done qed