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])
```