add finite entropy
authorhoelzl
Wed Oct 10 12:12:36 2012 +0200 (2012-10-10)
changeset 498032f076e377703
parent 49802 dd8dffaf84b9
child 49804 ace9b5a83e60
add finite entropy
src/HOL/Probability/Information.thy
     1.1 --- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:36 2012 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:36 2012 +0200
     1.3 @@ -339,6 +339,115 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +subsection {* Finite Entropy *}
     1.8 +
     1.9 +definition (in information_space) 
    1.10 +  "finite_entropy S X f \<longleftrightarrow> distributed M S X f \<and> integrable S (\<lambda>x. f x * log b (f x))"
    1.11 +
    1.12 +lemma (in information_space) finite_entropy_simple_function:
    1.13 +  assumes X: "simple_function M X"
    1.14 +  shows "finite_entropy (count_space (X`space M)) X (\<lambda>a. measure M {x \<in> space M. X x = a})"
    1.15 +  unfolding finite_entropy_def
    1.16 +proof
    1.17 +  have [simp]: "finite (X ` space M)"
    1.18 +    using X by (auto simp: simple_function_def)
    1.19 +  then show "integrable (count_space (X ` space M))
    1.20 +     (\<lambda>x. prob {xa \<in> space M. X xa = x} * log b (prob {xa \<in> space M. X xa = x}))"
    1.21 +    by (rule integrable_count_space)
    1.22 +  have d: "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then prob {xa \<in> space M. X xa = x} else 0))"
    1.23 +    by (rule distributed_simple_function_superset[OF X]) (auto intro!: arg_cong[where f=prob])
    1.24 +  show "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (prob {xa \<in> space M. X xa = x}))"
    1.25 +    by (rule distributed_cong_density[THEN iffD1, OF _ _ _ d]) auto
    1.26 +qed
    1.27 +
    1.28 +lemma distributed_transform_AE:
    1.29 +  assumes T: "T \<in> measurable P Q" "absolutely_continuous Q (distr P Q T)"
    1.30 +  assumes g: "distributed M Q Y g"
    1.31 +  shows "AE x in P. 0 \<le> g (T x)"
    1.32 +  using g
    1.33 +  apply (subst AE_distr_iff[symmetric, OF T(1)])
    1.34 +  apply (simp add: distributed_borel_measurable)
    1.35 +  apply (rule absolutely_continuous_AE[OF _ T(2)])
    1.36 +  apply simp
    1.37 +  apply (simp add: distributed_AE)
    1.38 +  done
    1.39 +
    1.40 +lemma ac_fst:
    1.41 +  assumes "sigma_finite_measure T"
    1.42 +  shows "absolutely_continuous S (distr (S \<Otimes>\<^isub>M T) S fst)"
    1.43 +proof -
    1.44 +  interpret sigma_finite_measure T by fact
    1.45 +  { fix A assume "A \<in> sets S" "emeasure S A = 0"
    1.46 +    moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
    1.47 +      by (auto simp: space_pair_measure dest!: sets_into_space)
    1.48 +    ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
    1.49 +      by (simp add: emeasure_pair_measure_Times) }
    1.50 +  then show ?thesis
    1.51 +    unfolding absolutely_continuous_def
    1.52 +    apply (auto simp: null_sets_distr_iff)
    1.53 +    apply (auto simp: null_sets_def intro!: measurable_sets)
    1.54 +    done
    1.55 +qed
    1.56 +
    1.57 +lemma ac_snd:
    1.58 +  assumes "sigma_finite_measure T"
    1.59 +  shows "absolutely_continuous T (distr (S \<Otimes>\<^isub>M T) T snd)"
    1.60 +proof -
    1.61 +  interpret sigma_finite_measure T by fact
    1.62 +  { fix A assume "A \<in> sets T" "emeasure T A = 0"
    1.63 +    moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
    1.64 +      by (auto simp: space_pair_measure dest!: sets_into_space)
    1.65 +    ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
    1.66 +      by (simp add: emeasure_pair_measure_Times) }
    1.67 +  then show ?thesis
    1.68 +    unfolding absolutely_continuous_def
    1.69 +    apply (auto simp: null_sets_distr_iff)
    1.70 +    apply (auto simp: null_sets_def intro!: measurable_sets)
    1.71 +    done
    1.72 +qed
    1.73 +
    1.74 +lemma distributed_integrable:
    1.75 +  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
    1.76 +    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
    1.77 +  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
    1.78 +                    distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
    1.79 +  
    1.80 +lemma distributed_transform_integrable:
    1.81 +  assumes Px: "distributed M N X Px"
    1.82 +  assumes "distributed M P Y Py"
    1.83 +  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
    1.84 +  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
    1.85 +proof -
    1.86 +  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
    1.87 +    by (rule distributed_integrable) fact+
    1.88 +  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
    1.89 +    using Y by simp
    1.90 +  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
    1.91 +    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
    1.92 +  finally show ?thesis .
    1.93 +qed
    1.94 +
    1.95 +lemma integrable_cong_AE_imp: "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
    1.96 +  using integrable_cong_AE by blast
    1.97 +
    1.98 +lemma (in information_space) finite_entropy_integrable:
    1.99 +  "finite_entropy S X Px \<Longrightarrow> integrable S (\<lambda>x. Px x * log b (Px x))"
   1.100 +  unfolding finite_entropy_def by auto
   1.101 +
   1.102 +lemma (in information_space) finite_entropy_distributed:
   1.103 +  "finite_entropy S X Px \<Longrightarrow> distributed M S X Px"
   1.104 +  unfolding finite_entropy_def by auto
   1.105 +
   1.106 +lemma (in information_space) finite_entropy_integrable_transform:
   1.107 +  assumes Fx: "finite_entropy S X Px"
   1.108 +  assumes Fy: "distributed M T Y Py"
   1.109 +    and "X = (\<lambda>x. f (Y x))"
   1.110 +    and "f \<in> measurable T S"
   1.111 +  shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
   1.112 +  using assms unfolding finite_entropy_def
   1.113 +  using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
   1.114 +  by (auto intro: distributed_real_measurable)
   1.115 +
   1.116  subsection {* Mutual Information *}
   1.117  
   1.118  definition (in prob_space)
   1.119 @@ -412,6 +521,120 @@
   1.120  
   1.121  lemma (in information_space)
   1.122    fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   1.123 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   1.124 +  assumes Fx: "finite_entropy S X Px" and Fy: "finite_entropy T Y Py"
   1.125 +  assumes Fxy: "finite_entropy (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   1.126 +  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   1.127 +  shows mutual_information_distr': "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
   1.128 +    and mutual_information_nonneg': "0 \<le> mutual_information b S T X Y"
   1.129 +proof -
   1.130 +  have Px: "distributed M S X Px"
   1.131 +    using Fx by (auto simp: finite_entropy_def)
   1.132 +  have Py: "distributed M T Y Py"
   1.133 +    using Fy by (auto simp: finite_entropy_def)
   1.134 +  have Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   1.135 +    using Fxy by (auto simp: finite_entropy_def)
   1.136 +
   1.137 +  have X: "random_variable S X"
   1.138 +    using Px by (auto simp: distributed_def finite_entropy_def)
   1.139 +  have Y: "random_variable T Y"
   1.140 +    using Py by (auto simp: distributed_def finite_entropy_def)
   1.141 +  interpret S: sigma_finite_measure S by fact
   1.142 +  interpret T: sigma_finite_measure T by fact
   1.143 +  interpret ST: pair_sigma_finite S T ..
   1.144 +  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
   1.145 +  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
   1.146 +  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
   1.147 +  let ?P = "S \<Otimes>\<^isub>M T"
   1.148 +  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
   1.149 +
   1.150 +  { fix A assume "A \<in> sets S"
   1.151 +    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
   1.152 +      by (auto simp: emeasure_distr measurable_Pair measurable_space
   1.153 +               intro!: arg_cong[where f="emeasure M"]) }
   1.154 +  note marginal_eq1 = this
   1.155 +  { fix A assume "A \<in> sets T"
   1.156 +    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
   1.157 +      by (auto simp: emeasure_distr measurable_Pair measurable_space
   1.158 +               intro!: arg_cong[where f="emeasure M"]) }
   1.159 +  note marginal_eq2 = this
   1.160 +
   1.161 +  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
   1.162 +    by auto
   1.163 +
   1.164 +  have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
   1.165 +    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
   1.166 +  proof (subst pair_measure_density)
   1.167 +    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
   1.168 +      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
   1.169 +      using Px Py by (auto simp: distributed_def)
   1.170 +    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
   1.171 +    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   1.172 +  qed (fact | simp)+
   1.173 +  
   1.174 +  have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
   1.175 +    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
   1.176 +
   1.177 +  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
   1.178 +    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
   1.179 +  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
   1.180 +  proof (rule ST.AE_pair_measure)
   1.181 +    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
   1.182 +      using f by auto
   1.183 +    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
   1.184 +      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
   1.185 +  qed
   1.186 +
   1.187 +  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
   1.188 +    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   1.189 +  moreover
   1.190 +  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
   1.191 +    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   1.192 +  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   1.193 +    by eventually_elim auto
   1.194 +
   1.195 +  show "?M = ?R"
   1.196 +    unfolding M f_def
   1.197 +    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
   1.198 +    by (rule ST.KL_density_density)
   1.199 +
   1.200 +  have X: "X = fst \<circ> (\<lambda>x. (X x, Y x))" and Y: "Y = snd \<circ> (\<lambda>x. (X x, Y x))"
   1.201 +    by auto
   1.202 +
   1.203 +  have "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)))"
   1.204 +    using finite_entropy_integrable[OF Fxy]
   1.205 +    using finite_entropy_integrable_transform[OF Fx Pxy, of fst]
   1.206 +    using finite_entropy_integrable_transform[OF Fy Pxy, of snd]
   1.207 +    by simp
   1.208 +  moreover have "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
   1.209 +    unfolding f_def using Px Py Pxy
   1.210 +    by (auto intro: distributed_real_measurable measurable_fst'' measurable_snd''
   1.211 +      intro!: borel_measurable_times borel_measurable_log borel_measurable_divide)
   1.212 +  ultimately have int: "integrable (S \<Otimes>\<^isub>M T) f"
   1.213 +    apply (rule integrable_cong_AE_imp)
   1.214 +    using
   1.215 +      distributed_transform_AE[OF measurable_fst ac_fst, of T, OF T Px]
   1.216 +      distributed_transform_AE[OF measurable_snd ac_snd, of _ _ _ _ S, OF T Py]
   1.217 +      subdensity_real[OF measurable_fst Pxy Px X]
   1.218 +      subdensity_real[OF measurable_snd Pxy Py Y]
   1.219 +      distributed_real_AE[OF Pxy]
   1.220 +    by eventually_elim
   1.221 +       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff mult_nonneg_nonneg)
   1.222 +
   1.223 +  show "0 \<le> ?M" unfolding M
   1.224 +  proof (rule ST.KL_density_density_nonneg
   1.225 +    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
   1.226 +    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
   1.227 +      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
   1.228 +      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
   1.229 +    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
   1.230 +      unfolding distr_eq[symmetric] by unfold_locales
   1.231 +  qed
   1.232 +qed
   1.233 +
   1.234 +
   1.235 +lemma (in information_space)
   1.236 +  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   1.237    assumes "sigma_finite_measure S" "sigma_finite_measure T"
   1.238    assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
   1.239    assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   1.240 @@ -1047,6 +1270,296 @@
   1.241      by simp
   1.242  qed
   1.243  
   1.244 +lemma (in information_space)
   1.245 +  fixes Px :: "_ \<Rightarrow> real"
   1.246 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
   1.247 +  assumes Fx: "finite_entropy S X Px"
   1.248 +  assumes Fz: "finite_entropy P Z Pz"
   1.249 +  assumes Fyz: "finite_entropy (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
   1.250 +  assumes Fxz: "finite_entropy (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
   1.251 +  assumes Fxyz: "finite_entropy (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   1.252 +  shows conditional_mutual_information_generic_eq': "conditional_mutual_information b S T P X Y Z
   1.253 +    = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
   1.254 +    and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
   1.255 +proof -
   1.256 +  note Px = Fx[THEN finite_entropy_distributed]
   1.257 +  note Pz = Fz[THEN finite_entropy_distributed]
   1.258 +  note Pyz = Fyz[THEN finite_entropy_distributed]
   1.259 +  note Pxz = Fxz[THEN finite_entropy_distributed]
   1.260 +  note Pxyz = Fxyz[THEN finite_entropy_distributed]
   1.261 +
   1.262 +  interpret S: sigma_finite_measure S by fact
   1.263 +  interpret T: sigma_finite_measure T by fact
   1.264 +  interpret P: sigma_finite_measure P by fact
   1.265 +  interpret TP: pair_sigma_finite T P ..
   1.266 +  interpret SP: pair_sigma_finite S P ..
   1.267 +  interpret ST: pair_sigma_finite S T ..
   1.268 +  interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
   1.269 +  interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
   1.270 +  interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
   1.271 +  have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
   1.272 +  have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
   1.273 +  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
   1.274 +    using Pyz by (simp add: distributed_measurable)
   1.275 +
   1.276 +  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
   1.277 +    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
   1.278 +
   1.279 +  { fix f g h M
   1.280 +    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
   1.281 +    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
   1.282 +         measurable_comp[OF f Px[THEN distributed_real_measurable]]
   1.283 +         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
   1.284 +    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
   1.285 +      by (simp add: comp_def b_gt_1) }
   1.286 +  note borel_log = this
   1.287 +
   1.288 +  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
   1.289 +    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
   1.290 +  
   1.291 +  from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
   1.292 +    distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
   1.293 +    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
   1.294 +
   1.295 +  have "mutual_information b S P X Z =
   1.296 +    (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
   1.297 +    by (rule mutual_information_distr[OF S P Px Pz Pxz])
   1.298 +  also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   1.299 +    using b_gt_1 Pxz Px Pz
   1.300 +    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
   1.301 +       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
   1.302 +             dest!: distributed_real_measurable)
   1.303 +  finally have mi_eq:
   1.304 +    "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   1.305 +  
   1.306 +  have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
   1.307 +    by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   1.308 +  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   1.309 +    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
   1.310 +  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   1.311 +    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
   1.312 +  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
   1.313 +    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
   1.314 +  moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
   1.315 +    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   1.316 +  moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
   1.317 +    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   1.318 +  moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
   1.319 +    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   1.320 +  moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
   1.321 +    using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
   1.322 +    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
   1.323 +    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
   1.324 +    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
   1.325 +  moreover note ae9 = Pxyz[THEN distributed_real_AE]
   1.326 +  ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
   1.327 +    Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
   1.328 +    Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
   1.329 +    Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   1.330 +  proof eventually_elim
   1.331 +    case (goal1 x)
   1.332 +    show ?case
   1.333 +    proof cases
   1.334 +      assume "Pxyz x \<noteq> 0"
   1.335 +      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
   1.336 +        by auto
   1.337 +      then show ?thesis
   1.338 +        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
   1.339 +    qed simp
   1.340 +  qed
   1.341 +
   1.342 +  have "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)
   1.343 +    (\<lambda>x. Pxyz x * log b (Pxyz x) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pyz (snd x)))"
   1.344 +    using finite_entropy_integrable[OF Fxyz]
   1.345 +    using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
   1.346 +    using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
   1.347 +    by simp
   1.348 +  moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
   1.349 +    using Pxyz Px Pyz
   1.350 +    by (auto intro!: borel_measurable_times measurable_fst'' measurable_snd'' dest!: distributed_real_measurable simp: split_beta')
   1.351 +  ultimately have I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
   1.352 +    apply (rule integrable_cong_AE_imp)
   1.353 +    using ae1 ae4 ae5 ae6 ae9
   1.354 +    by eventually_elim
   1.355 +       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
   1.356 +
   1.357 +  have "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)
   1.358 +    (\<lambda>x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))"
   1.359 +    using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
   1.360 +    using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
   1.361 +    using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
   1.362 +    by (simp add: measurable_Pair measurable_snd'' comp_def)
   1.363 +  moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
   1.364 +    using Pxyz Px Pz
   1.365 +    by (auto intro!: measurable_compose[OF _ distributed_real_measurable[OF Pxz]]
   1.366 +                     measurable_Pair borel_measurable_times measurable_fst'' measurable_snd''
   1.367 +             dest!: distributed_real_measurable simp: split_beta')
   1.368 +  ultimately have I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
   1.369 +    apply (rule integrable_cong_AE_imp)
   1.370 +    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
   1.371 +    by eventually_elim
   1.372 +       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
   1.373 +
   1.374 +  from ae I1 I2 show ?eq
   1.375 +    unfolding conditional_mutual_information_def
   1.376 +    apply (subst mi_eq)
   1.377 +    apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
   1.378 +    apply (subst integral_diff(2)[symmetric])
   1.379 +    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
   1.380 +    done
   1.381 +
   1.382 +  let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
   1.383 +  interpret P: prob_space ?P
   1.384 +    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
   1.385 +    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
   1.386 +
   1.387 +  let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
   1.388 +  interpret Q: prob_space ?Q
   1.389 +    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
   1.390 +    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
   1.391 +
   1.392 +  let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
   1.393 +
   1.394 +  from subdensity_real[of snd, OF _ Pyz Pz]
   1.395 +  have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
   1.396 +  have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
   1.397 +    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   1.398 +
   1.399 +  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.400 +    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
   1.401 +    apply (intro TP.AE_pair_measure)
   1.402 +    apply (auto simp: comp_def measurable_split_conv
   1.403 +                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
   1.404 +                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   1.405 +                        measurable_Pair
   1.406 +                dest: distributed_real_AE distributed_real_measurable)
   1.407 +    done
   1.408 +
   1.409 +  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
   1.410 +           measurable_compose[OF _ measurable_snd]
   1.411 +           measurable_Pair
   1.412 +           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
   1.413 +           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
   1.414 +           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
   1.415 +           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
   1.416 +           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
   1.417 +           STP.borel_measurable_positive_integral_snd
   1.418 +  have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   1.419 +    apply (subst positive_integral_density)
   1.420 +    apply (rule distributed_borel_measurable[OF Pxyz])
   1.421 +    apply (rule distributed_AE[OF Pxyz])
   1.422 +    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   1.423 +    apply (rule positive_integral_mono_AE)
   1.424 +    using ae5 ae6 ae7 ae8
   1.425 +    apply eventually_elim
   1.426 +    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
   1.427 +    done
   1.428 +  also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
   1.429 +    by (subst STP.positive_integral_snd_measurable[symmetric])
   1.430 +       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
   1.431 +  also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
   1.432 +    apply (rule positive_integral_cong_AE)
   1.433 +    using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
   1.434 +    apply eventually_elim
   1.435 +  proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
   1.436 +    fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
   1.437 +      "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
   1.438 +    then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
   1.439 +      apply (subst positive_integral_multc)
   1.440 +      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
   1.441 +                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
   1.442 +                  split: prod.split)
   1.443 +      done
   1.444 +  qed
   1.445 +  also have "\<dots> = 1"
   1.446 +    using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
   1.447 +    by (subst positive_integral_density[symmetric]) (auto intro!: M)
   1.448 +  finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
   1.449 +  also have "\<dots> < \<infinity>" by simp
   1.450 +  finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
   1.451 +
   1.452 +  have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
   1.453 +    apply (subst positive_integral_density)
   1.454 +    apply (rule distributed_borel_measurable[OF Pxyz])
   1.455 +    apply (rule distributed_AE[OF Pxyz])
   1.456 +    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
   1.457 +    apply (simp add: split_beta')
   1.458 +  proof
   1.459 +    let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
   1.460 +    assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
   1.461 +    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
   1.462 +      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
   1.463 +    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
   1.464 +      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   1.465 +      by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
   1.466 +    then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
   1.467 +      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
   1.468 +    with P.emeasure_space_1 show False
   1.469 +      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
   1.470 +  qed
   1.471 +
   1.472 +  have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
   1.473 +    apply (rule positive_integral_0_iff_AE[THEN iffD2])
   1.474 +    apply (auto intro!: M simp: split_beta') []
   1.475 +    apply (subst AE_density)
   1.476 +    apply (auto intro!: M simp: split_beta') []
   1.477 +    using ae5 ae6 ae7 ae8
   1.478 +    apply eventually_elim
   1.479 +    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
   1.480 +    done
   1.481 +
   1.482 +  have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
   1.483 +    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
   1.484 +    using ae
   1.485 +    apply (auto intro!: M simp: split_beta')
   1.486 +    done
   1.487 +
   1.488 +  have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
   1.489 +  proof (intro le_imp_neg_le log_le[OF b_gt_1])
   1.490 +    show "0 < integral\<^isup>L ?P ?f"
   1.491 +      using neg pos fin positive_integral_positive[of ?P ?f]
   1.492 +      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def less_le split_beta')
   1.493 +    show "integral\<^isup>L ?P ?f \<le> 1"
   1.494 +      using neg le1 fin positive_integral_positive[of ?P ?f]
   1.495 +      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def split_beta' one_ereal_def)
   1.496 +  qed
   1.497 +  also have "- log b (integral\<^isup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
   1.498 +  proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
   1.499 +    show "AE x in ?P. ?f x \<in> {0<..}"
   1.500 +      unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
   1.501 +      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   1.502 +      by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
   1.503 +    show "integrable ?P ?f"
   1.504 +      unfolding integrable_def 
   1.505 +      using fin neg by (auto intro!: M simp: split_beta')
   1.506 +    show "integrable ?P (\<lambda>x. - log b (?f x))"
   1.507 +      apply (subst integral_density)
   1.508 +      apply (auto intro!: M) []
   1.509 +      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   1.510 +      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   1.511 +      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
   1.512 +      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   1.513 +      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   1.514 +      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   1.515 +      apply eventually_elim
   1.516 +      apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
   1.517 +      done
   1.518 +  qed (auto simp: b_gt_1 minus_log_convex)
   1.519 +  also have "\<dots> = conditional_mutual_information b S T P X Y Z"
   1.520 +    unfolding `?eq`
   1.521 +    apply (subst integral_density)
   1.522 +    apply (auto intro!: M) []
   1.523 +    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
   1.524 +    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
   1.525 +    apply (intro integral_cong_AE)
   1.526 +    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   1.527 +    apply eventually_elim
   1.528 +    apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
   1.529 +    done
   1.530 +  finally show ?nonneg
   1.531 +    by simp
   1.532 +qed
   1.533 +
   1.534  lemma (in information_space) conditional_mutual_information_eq:
   1.535    assumes Pz: "simple_distributed M Z Pz"
   1.536    assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
   1.537 @@ -1436,6 +1949,25 @@
   1.538    finally show ?thesis by auto
   1.539  qed
   1.540  
   1.541 +lemma (in information_space) 
   1.542 +  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
   1.543 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   1.544 +  assumes Px: "finite_entropy S X Px" and Py: "finite_entropy T Y Py"
   1.545 +  assumes Pxy: "finite_entropy (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   1.546 +  shows "conditional_entropy b S T X Y \<le> entropy b S X"
   1.547 +proof -
   1.548 +
   1.549 +  have "0 \<le> mutual_information b S T X Y" 
   1.550 +    by (rule mutual_information_nonneg') fact+
   1.551 +  also have "\<dots> = entropy b S X - conditional_entropy b S T X Y"
   1.552 +    apply (rule mutual_information_eq_entropy_conditional_entropy')
   1.553 +    using assms
   1.554 +    by (auto intro!: finite_entropy_integrable finite_entropy_distributed
   1.555 +      finite_entropy_integrable_transform[OF Px]
   1.556 +      finite_entropy_integrable_transform[OF Py])
   1.557 +  finally show ?thesis by auto
   1.558 +qed
   1.559 +
   1.560  lemma (in information_space) entropy_chain_rule:
   1.561    assumes X: "simple_function M X" and Y: "simple_function M Y"
   1.562    shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"