remove unneeded assumption from conditional_entropy_generic_eq
authorhoelzl
Wed Oct 10 12:12:27 2012 +0200 (2012-10-10)
changeset 497906b9b9ebba47d
parent 49789 e0a4cb91a8a9
child 49791 e0854abfb3fc
remove unneeded assumption from conditional_entropy_generic_eq
src/HOL/Probability/Information.thy
     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