src/HOL/Probability/Information.thy
changeset 49788 3c10763f5cb4
parent 49787 d8de705b48d4
child 49790 6b9b9ebba47d
     1.1 --- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:25 2012 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:26 2012 +0200
     1.3 @@ -566,14 +566,13 @@
     1.4    entropy_Pow ("\<H>'(_')") where
     1.5    "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
     1.6  
     1.7 -lemma (in information_space) entropy_distr:
     1.8 +lemma (in information_space)
     1.9    fixes X :: "'a \<Rightarrow> 'b"
    1.10    assumes X: "distributed M MX X f"
    1.11 -  shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"
    1.12 -  unfolding entropy_def KL_divergence_def entropy_density_def comp_def
    1.13 -proof (subst integral_cong_AE)
    1.14 +  shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
    1.15 +proof -
    1.16    note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
    1.17 -  interpret X: prob_space "distr M MX X"
    1.18 +    interpret X: prob_space "distr M MX X"
    1.19      using D(1) by (rule prob_space_distr)
    1.20  
    1.21    have sf: "sigma_finite_measure (distr M MX X)" by default
    1.22 @@ -582,7 +581,8 @@
    1.23      by (intro RN_deriv_unique_sigma_finite)
    1.24         (auto intro: divide_nonneg_nonneg measure_nonneg
    1.25               simp: distributed_distr_eq_density[symmetric, OF X] sf)
    1.26 -  show "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
    1.27 +
    1.28 +  have ae_eq: "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
    1.29      log b (f x)"
    1.30      unfolding distributed_distr_eq_density[OF X]
    1.31      apply (subst AE_density)
    1.32 @@ -591,12 +591,20 @@
    1.33      apply (subst (asm) eq_commute)
    1.34      apply auto
    1.35      done
    1.36 -  show "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
    1.37 +
    1.38 +  have int_eq: "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
    1.39      unfolding distributed_distr_eq_density[OF X]
    1.40      using D
    1.41      by (subst integral_density)
    1.42         (auto simp: borel_measurable_ereal_iff)
    1.43 -qed 
    1.44 +
    1.45 +  show ?eq
    1.46 +    unfolding entropy_def KL_divergence_def entropy_density_def comp_def
    1.47 +    apply (subst integral_cong_AE)
    1.48 +    apply (rule ae_eq)
    1.49 +    apply (rule int_eq)
    1.50 +    done
    1.51 +qed
    1.52  
    1.53  lemma (in prob_space) distributed_imp_emeasure_nonzero:
    1.54    assumes X: "distributed M MX X Px"
    1.55 @@ -896,7 +904,7 @@
    1.56      using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
    1.57  
    1.58    have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
    1.59 -    using Pz distributed_marginal_eq_joint[OF P S Px Pz Pxz]
    1.60 +    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
    1.61      apply (intro TP.AE_pair_measure)
    1.62      apply (auto simp: comp_def measurable_split_conv
    1.63                  intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
    1.64 @@ -1110,7 +1118,7 @@
    1.65    conditional_entropy_Pow ("\<H>'(_ | _')") where
    1.66    "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
    1.67  
    1.68 -lemma (in information_space) conditional_entropy_generic_eq:
    1.69 +lemma (in information_space)
    1.70    fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
    1.71    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
    1.72    assumes Px: "distributed M S X Px"
    1.73 @@ -1118,14 +1126,15 @@
    1.74    assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
    1.75    assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
    1.76    assumes I2: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
    1.77 -  shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
    1.78 +  shows conditional_entropy_generic_eq: "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))" (is ?eq)
    1.79  proof -
    1.80    interpret S: sigma_finite_measure S by fact
    1.81    interpret T: sigma_finite_measure T by fact
    1.82    interpret ST: pair_sigma_finite S T ..
    1.83    have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
    1.84  
    1.85 -  interpret Pxy: prob_space "density (S \<Otimes>\<^isub>M T) Pxy"
    1.86 +  let ?P = "density (S \<Otimes>\<^isub>M T) Pxy"
    1.87 +  interpret Pxy: prob_space ?P
    1.88      unfolding Pxy[THEN distributed_distr_eq_density, symmetric]
    1.89      using Pxy[THEN distributed_measurable] by (rule prob_space_distr)
    1.90  
    1.91 @@ -1140,23 +1149,23 @@
    1.92      by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
    1.93    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.94    
    1.95 -  have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
    1.96 +  have ae1: "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
    1.97      by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
    1.98 -  moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
    1.99 +  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   1.100      by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
   1.101 -  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
   1.102 +  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
   1.103      using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   1.104 -  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
   1.105 +  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
   1.106      using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   1.107 -  moreover note Pxy[THEN distributed_real_AE]
   1.108 +  moreover note ae5 = Pxy[THEN distributed_real_AE]
   1.109    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.110      (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Px (fst x) \<and> 0 < Py (snd x)))"
   1.111      by eventually_elim auto
   1.112  
   1.113 -  from pos have "AE x in S \<Otimes>\<^isub>M T.
   1.114 +  from pos have ae: "AE x in S \<Otimes>\<^isub>M T.
   1.115       Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
   1.116      by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
   1.117 -  with I1 I2 show ?thesis
   1.118 +  with I1 I2 show ?eq
   1.119      unfolding conditional_entropy_def
   1.120      apply (subst e_eq)
   1.121      apply (subst entropy_distr[OF Pxy])