src/HOL/Probability/Information.thy
author hoelzl
Wed Oct 10 12:12:36 2012 +0200 (2012-10-10)
changeset 49803 2f076e377703
parent 49802 dd8dffaf84b9
child 49825 bb5db3d1d6dd
permissions -rw-r--r--
add finite entropy
     1 (*  Title:      HOL/Probability/Information.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Armin Heller, TU München
     4 *)
     5 
     6 header {*Information theory*}
     7 
     8 theory Information
     9 imports
    10   Independent_Family
    11   Radon_Nikodym
    12   "~~/src/HOL/Library/Convex"
    13 begin
    14 
    15 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
    16   by (subst log_le_cancel_iff) auto
    17 
    18 lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
    19   by (subst log_less_cancel_iff) auto
    20 
    21 lemma setsum_cartesian_product':
    22   "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
    23   unfolding setsum_cartesian_product by simp
    24 
    25 lemma split_pairs:
    26   "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
    27   "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
    28 
    29 section "Information theory"
    30 
    31 locale information_space = prob_space +
    32   fixes b :: real assumes b_gt_1: "1 < b"
    33 
    34 context information_space
    35 begin
    36 
    37 text {* Introduce some simplification rules for logarithm of base @{term b}. *}
    38 
    39 lemma log_neg_const:
    40   assumes "x \<le> 0"
    41   shows "log b x = log b 0"
    42 proof -
    43   { fix u :: real
    44     have "x \<le> 0" by fact
    45     also have "0 < exp u"
    46       using exp_gt_zero .
    47     finally have "exp u \<noteq> x"
    48       by auto }
    49   then show "log b x = log b 0"
    50     by (simp add: log_def ln_def)
    51 qed
    52 
    53 lemma log_mult_eq:
    54   "log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)"
    55   using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
    56   by (auto simp: zero_less_mult_iff mult_le_0_iff)
    57 
    58 lemma log_inverse_eq:
    59   "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
    60   using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp
    61 
    62 lemma log_divide_eq:
    63   "log b (A / B) = (if 0 < A * B then log b \<bar>A\<bar> - log b \<bar>B\<bar> else log b 0)"
    64   unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
    65   by (auto simp: zero_less_mult_iff mult_le_0_iff)
    66 
    67 lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
    68 
    69 end
    70 
    71 subsection "Kullback$-$Leibler divergence"
    72 
    73 text {* The Kullback$-$Leibler divergence is also known as relative entropy or
    74 Kullback$-$Leibler distance. *}
    75 
    76 definition
    77   "entropy_density b M N = log b \<circ> real \<circ> RN_deriv M N"
    78 
    79 definition
    80   "KL_divergence b M N = integral\<^isup>L N (entropy_density b M N)"
    81 
    82 lemma (in information_space) measurable_entropy_density:
    83   assumes ac: "absolutely_continuous M N" "sets N = events"
    84   shows "entropy_density b M N \<in> borel_measurable M"
    85 proof -
    86   from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
    87     unfolding entropy_density_def
    88     by (intro measurable_comp) auto
    89 qed
    90 
    91 lemma (in sigma_finite_measure) KL_density:
    92   fixes f :: "'a \<Rightarrow> real"
    93   assumes "1 < b"
    94   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
    95   shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)"
    96   unfolding KL_divergence_def
    97 proof (subst integral_density)
    98   show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
    99     using f
   100     by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
   101   have "density M (RN_deriv M (density M f)) = density M f"
   102     using f by (intro density_RN_deriv_density) auto
   103   then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
   104     using f
   105     by (intro density_unique)
   106        (auto intro!: borel_measurable_log borel_measurable_RN_deriv_density simp: RN_deriv_density_nonneg)
   107   show "(\<integral>x. f x * entropy_density b M (density M (\<lambda>x. ereal (f x))) x \<partial>M) = (\<integral>x. f x * log b (f x) \<partial>M)"
   108     apply (intro integral_cong_AE)
   109     using eq
   110     apply eventually_elim
   111     apply (auto simp: entropy_density_def)
   112     done
   113 qed fact+
   114 
   115 lemma (in sigma_finite_measure) KL_density_density:
   116   fixes f g :: "'a \<Rightarrow> real"
   117   assumes "1 < b"
   118   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   119   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   120   assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
   121   shows "KL_divergence b (density M f) (density M g) = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
   122 proof -
   123   interpret Mf: sigma_finite_measure "density M f"
   124     using f by (subst sigma_finite_iff_density_finite) auto
   125   have "KL_divergence b (density M f) (density M g) =
   126     KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
   127     using f g ac by (subst density_density_divide) simp_all
   128   also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
   129     using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
   130   also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
   131     using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
   132   finally show ?thesis .
   133 qed
   134 
   135 lemma (in information_space) KL_gt_0:
   136   fixes D :: "'a \<Rightarrow> real"
   137   assumes "prob_space (density M D)"
   138   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   139   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   140   assumes A: "density M D \<noteq> M"
   141   shows "0 < KL_divergence b M (density M D)"
   142 proof -
   143   interpret N: prob_space "density M D" by fact
   144 
   145   obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"
   146     using measure_eqI[of "density M D" M] `density M D \<noteq> M` by auto
   147 
   148   let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
   149   have [simp, intro]: "?D_set \<in> sets M"
   150     using D by auto
   151 
   152   have D_neg: "(\<integral>\<^isup>+ x. ereal (- D x) \<partial>M) = 0"
   153     using D by (subst positive_integral_0_iff_AE) auto
   154 
   155   have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
   156     using D by (simp add: emeasure_density cong: positive_integral_cong)
   157   then have D_pos: "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = 1"
   158     using N.emeasure_space_1 by simp
   159 
   160   have "integrable M D" "integral\<^isup>L M D = 1"
   161     using D D_pos D_neg unfolding integrable_def lebesgue_integral_def by simp_all
   162 
   163   have "0 \<le> 1 - measure M ?D_set"
   164     using prob_le_1 by (auto simp: field_simps)
   165   also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
   166     using `integrable M D` `integral\<^isup>L M D = 1`
   167     by (simp add: emeasure_eq_measure)
   168   also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"
   169   proof (rule integral_less_AE)
   170     show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
   171       using `integrable M D`
   172       by (intro integral_diff integral_indicator) auto
   173   next
   174     from integral_cmult(1)[OF int, of "ln b"]
   175     show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 
   176       by (simp add: ac_simps)
   177   next
   178     show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
   179     proof
   180       assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
   181       then have disj: "AE x in M. D x = 1 \<or> D x = 0"
   182         using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
   183 
   184       have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
   185         using D(1) by auto
   186       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"
   187         using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
   188       finally have "AE x in M. D x = 1"
   189         using D D_pos by (intro AE_I_eq_1) auto
   190       then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. ereal (D x) * indicator A x\<partial>M)"
   191         by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
   192       also have "\<dots> = density M D A"
   193         using `A \<in> sets M` D by (simp add: emeasure_density)
   194       finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
   195     qed
   196     show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
   197       using D(1) by (auto intro: sets_Collect_conj)
   198 
   199     show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
   200       D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
   201       using D(2)
   202     proof (eventually_elim, safe)
   203       fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"
   204         and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"
   205 
   206       have "D t - 1 = D t - indicator ?D_set t"
   207         using Dt by simp
   208       also note eq
   209       also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"
   210         using b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
   211         by (simp add: log_def ln_div less_le)
   212       finally have "ln (1 / D t) = 1 / D t - 1"
   213         using `D t \<noteq> 0` by (auto simp: field_simps)
   214       from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
   215       show False by auto
   216     qed
   217 
   218     show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
   219       using D(2) AE_space
   220     proof eventually_elim
   221       fix t assume "t \<in> space M" "0 \<le> D t"
   222       show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
   223       proof cases
   224         assume asm: "D t \<noteq> 0"
   225         then have "0 < D t" using `0 \<le> D t` by auto
   226         then have "0 < 1 / D t" by auto
   227         have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
   228           using asm `t \<in> space M` by (simp add: field_simps)
   229         also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
   230           using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
   231         also have "\<dots> = D t * (ln b * log b (D t))"
   232           using `0 < D t` b_gt_1
   233           by (simp_all add: log_def ln_div)
   234         finally show ?thesis by simp
   235       qed simp
   236     qed
   237   qed
   238   also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"
   239     by (simp add: ac_simps)
   240   also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"
   241     using int by (rule integral_cmult)
   242   finally show ?thesis
   243     using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)
   244 qed
   245 
   246 lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"
   247 proof -
   248   have "AE x in M. 1 = RN_deriv M M x"
   249   proof (rule RN_deriv_unique)
   250     show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto
   251     show "density M (\<lambda>x. 1) = M"
   252       apply (auto intro!: measure_eqI emeasure_density)
   253       apply (subst emeasure_density)
   254       apply auto
   255       done
   256   qed
   257   then have "AE x in M. log b (real (RN_deriv M M x)) = 0"
   258     by (elim AE_mp) simp
   259   from integral_cong_AE[OF this]
   260   have "integral\<^isup>L M (entropy_density b M M) = 0"
   261     by (simp add: entropy_density_def comp_def)
   262   then show "KL_divergence b M M = 0"
   263     unfolding KL_divergence_def
   264     by auto
   265 qed
   266 
   267 lemma (in information_space) KL_eq_0_iff_eq:
   268   fixes D :: "'a \<Rightarrow> real"
   269   assumes "prob_space (density M D)"
   270   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   271   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   272   shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"
   273   using KL_same_eq_0[of b] KL_gt_0[OF assms]
   274   by (auto simp: less_le)
   275 
   276 lemma (in information_space) KL_eq_0_iff_eq_ac:
   277   fixes D :: "'a \<Rightarrow> real"
   278   assumes "prob_space N"
   279   assumes ac: "absolutely_continuous M N" "sets N = sets M"
   280   assumes int: "integrable N (entropy_density b M N)"
   281   shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"
   282 proof -
   283   interpret N: prob_space N by fact
   284   have "finite_measure N" by unfold_locales
   285   from real_RN_deriv[OF this ac] guess D . note D = this
   286   
   287   have "N = density M (RN_deriv M N)"
   288     using ac by (rule density_RN_deriv[symmetric])
   289   also have "\<dots> = density M D"
   290     using borel_measurable_RN_deriv[OF ac] D by (auto intro!: density_cong)
   291   finally have N: "N = density M D" .
   292 
   293   from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density
   294   have "integrable N (\<lambda>x. log b (D x))"
   295     by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])
   296        (auto simp: N entropy_density_def)
   297   with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"
   298     by (subst integral_density(2)[symmetric]) (auto simp: N[symmetric] comp_def)
   299   with `prob_space N` D show ?thesis
   300     unfolding N
   301     by (intro KL_eq_0_iff_eq) auto
   302 qed
   303 
   304 lemma (in information_space) KL_nonneg:
   305   assumes "prob_space (density M D)"
   306   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   307   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   308   shows "0 \<le> KL_divergence b M (density M D)"
   309   using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)
   310 
   311 lemma (in sigma_finite_measure) KL_density_density_nonneg:
   312   fixes f g :: "'a \<Rightarrow> real"
   313   assumes "1 < b"
   314   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"
   315   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"
   316   assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
   317   assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"
   318   shows "0 \<le> KL_divergence b (density M f) (density M g)"
   319 proof -
   320   interpret Mf: prob_space "density M f" by fact
   321   interpret Mf: information_space "density M f" b by default fact
   322   have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
   323     using f g ac by (subst density_density_divide) simp_all
   324 
   325   have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
   326   proof (rule Mf.KL_nonneg)
   327     show "prob_space ?DD" unfolding eq by fact
   328     from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
   329       by auto
   330     show "AE x in density M f. 0 \<le> g x / f x"
   331       using f g by (auto simp: AE_density divide_nonneg_nonneg)
   332     show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
   333       using `1 < b` f g ac
   334       by (subst integral_density)
   335          (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)
   336   qed
   337   also have "\<dots> = KL_divergence b (density M f) (density M g)"
   338     using f g ac by (subst density_density_divide) simp_all
   339   finally show ?thesis .
   340 qed
   341 
   342 subsection {* Finite Entropy *}
   343 
   344 definition (in information_space) 
   345   "finite_entropy S X f \<longleftrightarrow> distributed M S X f \<and> integrable S (\<lambda>x. f x * log b (f x))"
   346 
   347 lemma (in information_space) finite_entropy_simple_function:
   348   assumes X: "simple_function M X"
   349   shows "finite_entropy (count_space (X`space M)) X (\<lambda>a. measure M {x \<in> space M. X x = a})"
   350   unfolding finite_entropy_def
   351 proof
   352   have [simp]: "finite (X ` space M)"
   353     using X by (auto simp: simple_function_def)
   354   then show "integrable (count_space (X ` space M))
   355      (\<lambda>x. prob {xa \<in> space M. X xa = x} * log b (prob {xa \<in> space M. X xa = x}))"
   356     by (rule integrable_count_space)
   357   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))"
   358     by (rule distributed_simple_function_superset[OF X]) (auto intro!: arg_cong[where f=prob])
   359   show "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (prob {xa \<in> space M. X xa = x}))"
   360     by (rule distributed_cong_density[THEN iffD1, OF _ _ _ d]) auto
   361 qed
   362 
   363 lemma distributed_transform_AE:
   364   assumes T: "T \<in> measurable P Q" "absolutely_continuous Q (distr P Q T)"
   365   assumes g: "distributed M Q Y g"
   366   shows "AE x in P. 0 \<le> g (T x)"
   367   using g
   368   apply (subst AE_distr_iff[symmetric, OF T(1)])
   369   apply (simp add: distributed_borel_measurable)
   370   apply (rule absolutely_continuous_AE[OF _ T(2)])
   371   apply simp
   372   apply (simp add: distributed_AE)
   373   done
   374 
   375 lemma ac_fst:
   376   assumes "sigma_finite_measure T"
   377   shows "absolutely_continuous S (distr (S \<Otimes>\<^isub>M T) S fst)"
   378 proof -
   379   interpret sigma_finite_measure T by fact
   380   { fix A assume "A \<in> sets S" "emeasure S A = 0"
   381     moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
   382       by (auto simp: space_pair_measure dest!: sets_into_space)
   383     ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
   384       by (simp add: emeasure_pair_measure_Times) }
   385   then show ?thesis
   386     unfolding absolutely_continuous_def
   387     apply (auto simp: null_sets_distr_iff)
   388     apply (auto simp: null_sets_def intro!: measurable_sets)
   389     done
   390 qed
   391 
   392 lemma ac_snd:
   393   assumes "sigma_finite_measure T"
   394   shows "absolutely_continuous T (distr (S \<Otimes>\<^isub>M T) T snd)"
   395 proof -
   396   interpret sigma_finite_measure T by fact
   397   { fix A assume "A \<in> sets T" "emeasure T A = 0"
   398     moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
   399       by (auto simp: space_pair_measure dest!: sets_into_space)
   400     ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
   401       by (simp add: emeasure_pair_measure_Times) }
   402   then show ?thesis
   403     unfolding absolutely_continuous_def
   404     apply (auto simp: null_sets_distr_iff)
   405     apply (auto simp: null_sets_def intro!: measurable_sets)
   406     done
   407 qed
   408 
   409 lemma distributed_integrable:
   410   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
   411     integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
   412   by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
   413                     distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
   414   
   415 lemma distributed_transform_integrable:
   416   assumes Px: "distributed M N X Px"
   417   assumes "distributed M P Y Py"
   418   assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
   419   shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
   420 proof -
   421   have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
   422     by (rule distributed_integrable) fact+
   423   also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
   424     using Y by simp
   425   also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
   426     using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
   427   finally show ?thesis .
   428 qed
   429 
   430 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"
   431   using integrable_cong_AE by blast
   432 
   433 lemma (in information_space) finite_entropy_integrable:
   434   "finite_entropy S X Px \<Longrightarrow> integrable S (\<lambda>x. Px x * log b (Px x))"
   435   unfolding finite_entropy_def by auto
   436 
   437 lemma (in information_space) finite_entropy_distributed:
   438   "finite_entropy S X Px \<Longrightarrow> distributed M S X Px"
   439   unfolding finite_entropy_def by auto
   440 
   441 lemma (in information_space) finite_entropy_integrable_transform:
   442   assumes Fx: "finite_entropy S X Px"
   443   assumes Fy: "distributed M T Y Py"
   444     and "X = (\<lambda>x. f (Y x))"
   445     and "f \<in> measurable T S"
   446   shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
   447   using assms unfolding finite_entropy_def
   448   using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
   449   by (auto intro: distributed_real_measurable)
   450 
   451 subsection {* Mutual Information *}
   452 
   453 definition (in prob_space)
   454   "mutual_information b S T X Y =
   455     KL_divergence b (distr M S X \<Otimes>\<^isub>M distr M T Y) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
   456 
   457 lemma (in information_space) mutual_information_indep_vars:
   458   fixes S T X Y
   459   defines "P \<equiv> distr M S X \<Otimes>\<^isub>M distr M T Y"
   460   defines "Q \<equiv> distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   461   shows "indep_var S X T Y \<longleftrightarrow>
   462     (random_variable S X \<and> random_variable T Y \<and>
   463       absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>
   464       mutual_information b S T X Y = 0)"
   465   unfolding indep_var_distribution_eq
   466 proof safe
   467   assume rv: "random_variable S X" "random_variable T Y"
   468 
   469   interpret X: prob_space "distr M S X"
   470     by (rule prob_space_distr) fact
   471   interpret Y: prob_space "distr M T Y"
   472     by (rule prob_space_distr) fact
   473   interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
   474   interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
   475 
   476   interpret Q: prob_space Q unfolding Q_def
   477     by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
   478 
   479   { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   480     then have [simp]: "Q = P"  unfolding Q_def P_def by simp
   481 
   482     show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)
   483     then have ed: "entropy_density b P Q \<in> borel_measurable P"
   484       by (rule P.measurable_entropy_density) simp
   485 
   486     have "AE x in P. 1 = RN_deriv P Q x"
   487     proof (rule P.RN_deriv_unique)
   488       show "density P (\<lambda>x. 1) = Q"
   489         unfolding `Q = P` by (intro measure_eqI) (auto simp: emeasure_density)
   490     qed auto
   491     then have ae_0: "AE x in P. entropy_density b P Q x = 0"
   492       by eventually_elim (auto simp: entropy_density_def)
   493     then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0)"
   494       using ed unfolding `Q = P` by (intro integrable_cong_AE) auto
   495     then show "integrable Q (entropy_density b P Q)" by simp
   496 
   497     show "mutual_information b S T X Y = 0"
   498       unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] `Q = P`
   499       using ae_0 by (simp cong: integral_cong_AE) }
   500 
   501   { assume ac: "absolutely_continuous P Q"
   502     assume int: "integrable Q (entropy_density b P Q)"
   503     assume I_eq_0: "mutual_information b S T X Y = 0"
   504 
   505     have eq: "Q = P"
   506     proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])
   507       show "prob_space Q" by unfold_locales
   508       show "absolutely_continuous P Q" by fact
   509       show "integrable Q (entropy_density b P Q)" by fact
   510       show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)
   511       show "KL_divergence b P Q = 0"
   512         using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)
   513     qed
   514     then show "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   515       unfolding P_def Q_def .. }
   516 qed
   517 
   518 abbreviation (in information_space)
   519   mutual_information_Pow ("\<I>'(_ ; _')") where
   520   "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) X Y"
   521 
   522 lemma (in information_space)
   523   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   524   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
   525   assumes Fx: "finite_entropy S X Px" and Fy: "finite_entropy T Y Py"
   526   assumes Fxy: "finite_entropy (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   527   defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   528   shows mutual_information_distr': "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
   529     and mutual_information_nonneg': "0 \<le> mutual_information b S T X Y"
   530 proof -
   531   have Px: "distributed M S X Px"
   532     using Fx by (auto simp: finite_entropy_def)
   533   have Py: "distributed M T Y Py"
   534     using Fy by (auto simp: finite_entropy_def)
   535   have Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   536     using Fxy by (auto simp: finite_entropy_def)
   537 
   538   have X: "random_variable S X"
   539     using Px by (auto simp: distributed_def finite_entropy_def)
   540   have Y: "random_variable T Y"
   541     using Py by (auto simp: distributed_def finite_entropy_def)
   542   interpret S: sigma_finite_measure S by fact
   543   interpret T: sigma_finite_measure T by fact
   544   interpret ST: pair_sigma_finite S T ..
   545   interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
   546   interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
   547   interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
   548   let ?P = "S \<Otimes>\<^isub>M T"
   549   let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
   550 
   551   { fix A assume "A \<in> sets S"
   552     with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
   553       by (auto simp: emeasure_distr measurable_Pair measurable_space
   554                intro!: arg_cong[where f="emeasure M"]) }
   555   note marginal_eq1 = this
   556   { fix A assume "A \<in> sets T"
   557     with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
   558       by (auto simp: emeasure_distr measurable_Pair measurable_space
   559                intro!: arg_cong[where f="emeasure M"]) }
   560   note marginal_eq2 = this
   561 
   562   have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
   563     by auto
   564 
   565   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)))"
   566     unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
   567   proof (subst pair_measure_density)
   568     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
   569       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
   570       using Px Py by (auto simp: distributed_def)
   571     show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
   572     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   573   qed (fact | simp)+
   574   
   575   have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
   576     unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
   577 
   578   from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
   579     by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
   580   have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
   581   proof (rule ST.AE_pair_measure)
   582     show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
   583       using f by auto
   584     show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
   585       using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
   586   qed
   587 
   588   have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
   589     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   590   moreover
   591   have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
   592     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   593   ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   594     by eventually_elim auto
   595 
   596   show "?M = ?R"
   597     unfolding M f_def
   598     using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
   599     by (rule ST.KL_density_density)
   600 
   601   have X: "X = fst \<circ> (\<lambda>x. (X x, Y x))" and Y: "Y = snd \<circ> (\<lambda>x. (X x, Y x))"
   602     by auto
   603 
   604   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)))"
   605     using finite_entropy_integrable[OF Fxy]
   606     using finite_entropy_integrable_transform[OF Fx Pxy, of fst]
   607     using finite_entropy_integrable_transform[OF Fy Pxy, of snd]
   608     by simp
   609   moreover have "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
   610     unfolding f_def using Px Py Pxy
   611     by (auto intro: distributed_real_measurable measurable_fst'' measurable_snd''
   612       intro!: borel_measurable_times borel_measurable_log borel_measurable_divide)
   613   ultimately have int: "integrable (S \<Otimes>\<^isub>M T) f"
   614     apply (rule integrable_cong_AE_imp)
   615     using
   616       distributed_transform_AE[OF measurable_fst ac_fst, of T, OF T Px]
   617       distributed_transform_AE[OF measurable_snd ac_snd, of _ _ _ _ S, OF T Py]
   618       subdensity_real[OF measurable_fst Pxy Px X]
   619       subdensity_real[OF measurable_snd Pxy Py Y]
   620       distributed_real_AE[OF Pxy]
   621     by eventually_elim
   622        (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff mult_nonneg_nonneg)
   623 
   624   show "0 \<le> ?M" unfolding M
   625   proof (rule ST.KL_density_density_nonneg
   626     [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
   627     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
   628       unfolding distributed_distr_eq_density[OF Pxy, symmetric]
   629       using distributed_measurable[OF Pxy] by (rule prob_space_distr)
   630     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
   631       unfolding distr_eq[symmetric] by unfold_locales
   632   qed
   633 qed
   634 
   635 
   636 lemma (in information_space)
   637   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   638   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   639   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
   640   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   641   defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   642   shows mutual_information_distr: "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
   643     and mutual_information_nonneg: "integrable (S \<Otimes>\<^isub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"
   644 proof -
   645   have X: "random_variable S X"
   646     using Px by (auto simp: distributed_def)
   647   have Y: "random_variable T Y"
   648     using Py by (auto simp: distributed_def)
   649   interpret S: sigma_finite_measure S by fact
   650   interpret T: sigma_finite_measure T by fact
   651   interpret ST: pair_sigma_finite S T ..
   652   interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
   653   interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
   654   interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
   655   let ?P = "S \<Otimes>\<^isub>M T"
   656   let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
   657 
   658   { fix A assume "A \<in> sets S"
   659     with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
   660       by (auto simp: emeasure_distr measurable_Pair measurable_space
   661                intro!: arg_cong[where f="emeasure M"]) }
   662   note marginal_eq1 = this
   663   { fix A assume "A \<in> sets T"
   664     with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
   665       by (auto simp: emeasure_distr measurable_Pair measurable_space
   666                intro!: arg_cong[where f="emeasure M"]) }
   667   note marginal_eq2 = this
   668 
   669   have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
   670     by auto
   671 
   672   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)))"
   673     unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
   674   proof (subst pair_measure_density)
   675     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
   676       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
   677       using Px Py by (auto simp: distributed_def)
   678     show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
   679     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   680   qed (fact | simp)+
   681   
   682   have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
   683     unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
   684 
   685   from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
   686     by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
   687   have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
   688   proof (rule ST.AE_pair_measure)
   689     show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
   690       using f by auto
   691     show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
   692       using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
   693   qed
   694 
   695   have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
   696     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   697   moreover
   698   have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
   699     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   700   ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   701     by eventually_elim auto
   702 
   703   show "?M = ?R"
   704     unfolding M f_def
   705     using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
   706     by (rule ST.KL_density_density)
   707 
   708   assume int: "integrable (S \<Otimes>\<^isub>M T) f"
   709   show "0 \<le> ?M" unfolding M
   710   proof (rule ST.KL_density_density_nonneg
   711     [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
   712     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
   713       unfolding distributed_distr_eq_density[OF Pxy, symmetric]
   714       using distributed_measurable[OF Pxy] by (rule prob_space_distr)
   715     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
   716       unfolding distr_eq[symmetric] by unfold_locales
   717   qed
   718 qed
   719 
   720 lemma (in information_space)
   721   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   722   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   723   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
   724   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   725   assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"
   726   shows mutual_information_eq_0: "mutual_information b S T X Y = 0"
   727 proof -
   728   interpret S: sigma_finite_measure S by fact
   729   interpret T: sigma_finite_measure T by fact
   730   interpret ST: pair_sigma_finite S T ..
   731 
   732   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
   733     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   734   moreover
   735   have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   736     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   737   moreover 
   738   have "AE x in S \<Otimes>\<^isub>M T. Pxy x = Px (fst x) * Py (snd x)"
   739     using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]
   740     by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')
   741   ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"
   742     by eventually_elim simp
   743   then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
   744     by (rule integral_cong_AE)
   745   then show ?thesis
   746     by (subst mutual_information_distr[OF assms(1-5)]) simp
   747 qed
   748 
   749 lemma (in information_space) mutual_information_simple_distributed:
   750   assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"
   751   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
   752   shows "\<I>(X ; Y) = (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x))`space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
   753 proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
   754   note fin = simple_distributed_joint_finite[OF XY, simp]
   755   show "sigma_finite_measure (count_space (X ` space M))"
   756     by (simp add: sigma_finite_measure_count_space_finite)
   757   show "sigma_finite_measure (count_space (Y ` space M))"
   758     by (simp add: sigma_finite_measure_count_space_finite)
   759   let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
   760   let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"
   761   have "\<And>x. ?f x = (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) else 0)"
   762     by auto
   763   with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M))) =
   764     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
   765     by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'
   766              intro!: setsum_cong)
   767 qed
   768 
   769 lemma (in information_space)
   770   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   771   assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"
   772   assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
   773   assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"
   774   shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"
   775 proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
   776   have "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) =
   777     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
   778     by (intro setsum_cong) (auto simp: ae)
   779   then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
   780     Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
   781 qed
   782 
   783 subsection {* Entropy *}
   784 
   785 definition (in prob_space) entropy :: "real \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real" where
   786   "entropy b S X = - KL_divergence b S (distr M S X)"
   787 
   788 abbreviation (in information_space)
   789   entropy_Pow ("\<H>'(_')") where
   790   "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
   791 
   792 lemma (in prob_space) distributed_RN_deriv:
   793   assumes X: "distributed M S X Px"
   794   shows "AE x in S. RN_deriv S (density S Px) x = Px x"
   795 proof -
   796   note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
   797   interpret X: prob_space "distr M S X"
   798     using D(1) by (rule prob_space_distr)
   799 
   800   have sf: "sigma_finite_measure (distr M S X)" by default
   801   show ?thesis
   802     using D
   803     apply (subst eq_commute)
   804     apply (intro RN_deriv_unique_sigma_finite)
   805     apply (auto intro: divide_nonneg_nonneg measure_nonneg
   806              simp: distributed_distr_eq_density[symmetric, OF X] sf)
   807     done
   808 qed
   809 
   810 lemma (in information_space)
   811   fixes X :: "'a \<Rightarrow> 'b"
   812   assumes X: "distributed M MX X f"
   813   shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
   814 proof -
   815   note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
   816   note ae = distributed_RN_deriv[OF X]
   817 
   818   have ae_eq: "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
   819     log b (f x)"
   820     unfolding distributed_distr_eq_density[OF X]
   821     apply (subst AE_density)
   822     using D apply simp
   823     using ae apply eventually_elim
   824     apply auto
   825     done
   826 
   827   have int_eq: "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
   828     unfolding distributed_distr_eq_density[OF X]
   829     using D
   830     by (subst integral_density)
   831        (auto simp: borel_measurable_ereal_iff)
   832 
   833   show ?eq
   834     unfolding entropy_def KL_divergence_def entropy_density_def comp_def
   835     apply (subst integral_cong_AE)
   836     apply (rule ae_eq)
   837     apply (rule int_eq)
   838     done
   839 qed
   840 
   841 lemma (in prob_space) distributed_imp_emeasure_nonzero:
   842   assumes X: "distributed M MX X Px"
   843   shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0"
   844 proof
   845   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   846   interpret X: prob_space "distr M MX X"
   847     using distributed_measurable[OF X] by (rule prob_space_distr)
   848 
   849   assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0"
   850   with Px have "AE x in MX. Px x = 0"
   851     by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ereal_iff)
   852   moreover
   853   from X.emeasure_space_1 have "(\<integral>\<^isup>+x. Px x \<partial>MX) = 1"
   854     unfolding distributed_distr_eq_density[OF X] using Px
   855     by (subst (asm) emeasure_density)
   856        (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
   857   ultimately show False
   858     by (simp add: positive_integral_cong_AE)
   859 qed
   860 
   861 lemma (in information_space) entropy_le:
   862   fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
   863   assumes X: "distributed M MX X Px"
   864   and fin: "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> \<infinity>"
   865   and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
   866   shows "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
   867 proof -
   868   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   869   interpret X: prob_space "distr M MX X"
   870     using distributed_measurable[OF X] by (rule prob_space_distr)
   871 
   872   have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
   873     - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
   874     using Px fin
   875     by (subst integral_indicator) (auto simp: measure_def borel_measurable_ereal_iff)
   876   also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
   877     unfolding distributed_distr_eq_density[OF X] using Px
   878     apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
   879     by (subst integral_density) (auto simp: borel_measurable_ereal_iff intro!: integral_cong)
   880   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   881   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
   882     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
   883       unfolding distributed_distr_eq_density[OF X]
   884       using Px by (auto simp: AE_density)
   885     have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
   886       by (auto simp: one_ereal_def)
   887     have "(\<integral>\<^isup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^isup>+ x. 0 \<partial>MX)"
   888       by (intro positive_integral_cong) (auto split: split_max)
   889     then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
   890       unfolding distributed_distr_eq_density[OF X] using Px
   891       by (auto simp: positive_integral_density integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
   892               cong: positive_integral_cong)
   893     have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
   894       integrable MX (\<lambda>x. - Px x * log b (Px x))"
   895       using Px
   896       by (intro integrable_cong_AE)
   897          (auto simp: borel_measurable_ereal_iff log_divide_eq
   898                   intro!: measurable_If)
   899     then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
   900       unfolding distributed_distr_eq_density[OF X]
   901       using Px int
   902       by (subst integral_density) (auto simp: borel_measurable_ereal_iff)
   903   qed (auto simp: minus_log_convex[OF b_gt_1])
   904   also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
   905     unfolding distributed_distr_eq_density[OF X] using Px
   906     by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
   907   also have "\<dots> = - entropy b MX X"
   908     unfolding distributed_distr_eq_density[OF X] using Px
   909     by (subst entropy_distr[OF X]) (auto simp: borel_measurable_ereal_iff integral_density)
   910   finally show ?thesis
   911     by simp
   912 qed
   913 
   914 lemma (in information_space) entropy_le_space:
   915   fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
   916   assumes X: "distributed M MX X Px"
   917   and fin: "finite_measure MX"
   918   and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
   919   shows "entropy b MX X \<le> log b (measure MX (space MX))"
   920 proof -
   921   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   922   interpret finite_measure MX by fact
   923   have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
   924     using int X by (intro entropy_le) auto
   925   also have "\<dots> \<le> log b (measure MX (space MX))"
   926     using Px distributed_imp_emeasure_nonzero[OF X]
   927     by (intro log_le)
   928        (auto intro!: borel_measurable_ereal_iff finite_measure_mono b_gt_1
   929                      less_le[THEN iffD2] measure_nonneg simp: emeasure_eq_measure)
   930   finally show ?thesis .
   931 qed
   932 
   933 lemma (in prob_space) uniform_distributed_params:
   934   assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
   935   shows "A \<in> sets MX" "measure MX A \<noteq> 0"
   936 proof -
   937   interpret X: prob_space "distr M MX X"
   938     using distributed_measurable[OF X] by (rule prob_space_distr)
   939 
   940   show "measure MX A \<noteq> 0"
   941   proof
   942     assume "measure MX A = 0"
   943     with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
   944     show False
   945       by (simp add: emeasure_density zero_ereal_def[symmetric])
   946   qed
   947   with measure_notin_sets[of A MX] show "A \<in> sets MX"
   948     by blast
   949 qed
   950 
   951 lemma (in information_space) entropy_uniform:
   952   assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
   953   shows "entropy b MX X = log b (measure MX A)"
   954 proof (subst entropy_distr[OF X])
   955   have [simp]: "emeasure MX A \<noteq> \<infinity>"
   956     using uniform_distributed_params[OF X] by (auto simp add: measure_def)
   957   have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   958     (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
   959     using measure_nonneg[of MX A] uniform_distributed_params[OF X]
   960     by (auto intro!: integral_cong split: split_indicator simp: log_divide_eq)
   961   show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   962     log b (measure MX A)"
   963     unfolding eq using uniform_distributed_params[OF X]
   964     by (subst lebesgue_integral_cmult) (auto simp: measure_def)
   965 qed
   966 
   967 lemma (in information_space) entropy_simple_distributed:
   968   "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
   969   by (subst entropy_distr[OF simple_distributed])
   970      (auto simp add: lebesgue_integral_count_space_finite)
   971 
   972 lemma (in information_space) entropy_le_card_not_0:
   973   assumes X: "simple_distributed M X f"
   974   shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"
   975 proof -
   976   let ?X = "count_space (X`space M)"
   977   have "\<H>(X) \<le> log b (measure ?X {x \<in> space ?X. f x \<noteq> 0})"
   978     by (rule entropy_le[OF simple_distributed[OF X]])
   979        (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space)
   980   also have "measure ?X {x \<in> space ?X. f x \<noteq> 0} = card (X ` space M \<inter> {x. f x \<noteq> 0})"
   981     by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def Int_def)
   982   finally show ?thesis .
   983 qed
   984 
   985 lemma (in information_space) entropy_le_card:
   986   assumes X: "simple_distributed M X f"
   987   shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
   988 proof -
   989   let ?X = "count_space (X`space M)"
   990   have "\<H>(X) \<le> log b (measure ?X (space ?X))"
   991     by (rule entropy_le_space[OF simple_distributed[OF X]])
   992        (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space finite_measure_count_space)
   993   also have "measure ?X (space ?X) = card (X ` space M)"
   994     by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def)
   995   finally show ?thesis .
   996 qed
   997 
   998 subsection {* Conditional Mutual Information *}
   999 
  1000 definition (in prob_space)
  1001   "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
  1002     mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x)) -
  1003     mutual_information b MX MZ X Z"
  1004 
  1005 abbreviation (in information_space)
  1006   conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
  1007   "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
  1008     (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
  1009 
  1010 lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
  1011   "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
  1012   using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
  1013 
  1014 lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
  1015   assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
  1016 proof -
  1017   interpret Q: pair_sigma_finite M2 M1 by default
  1018   from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
  1019 qed
  1020 
  1021 lemma (in information_space)
  1022   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
  1023   assumes Px: "distributed M S X Px"
  1024   assumes Pz: "distributed M P Z Pz"
  1025   assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
  1026   assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
  1027   assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
  1028   assumes 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))))"
  1029   assumes 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)))"
  1030   shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
  1031     = (\<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")
  1032     and conditional_mutual_information_generic_nonneg: "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
  1033 proof -
  1034   interpret S: sigma_finite_measure S by fact
  1035   interpret T: sigma_finite_measure T by fact
  1036   interpret P: sigma_finite_measure P by fact
  1037   interpret TP: pair_sigma_finite T P ..
  1038   interpret SP: pair_sigma_finite S P ..
  1039   interpret ST: pair_sigma_finite S T ..
  1040   interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
  1041   interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
  1042   interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
  1043   have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
  1044   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
  1045   have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
  1046     using Pyz by (simp add: distributed_measurable)
  1047 
  1048   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"
  1049     using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
  1050 
  1051   { fix f g h M
  1052     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)"
  1053     from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
  1054          measurable_comp[OF f Px[THEN distributed_real_measurable]]
  1055          measurable_comp[OF g Pz[THEN distributed_real_measurable]]
  1056     have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
  1057       by (simp add: comp_def b_gt_1) }
  1058   note borel_log = this
  1059 
  1060   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)"
  1061     by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
  1062   
  1063   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
  1064     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))"
  1065     by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
  1066 
  1067   have "mutual_information b S P X Z =
  1068     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
  1069     by (rule mutual_information_distr[OF S P Px Pz Pxz])
  1070   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))"
  1071     using b_gt_1 Pxz Px Pz
  1072     by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
  1073        (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
  1074              dest!: distributed_real_measurable)
  1075   finally have mi_eq:
  1076     "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))" .
  1077   
  1078   have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
  1079     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
  1080   moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1081     by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
  1082   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"
  1083     by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
  1084   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
  1085     by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
  1086   moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
  1087     using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
  1088   moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
  1089     using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1090   moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
  1091     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)
  1092   moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
  1093     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
  1094     using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
  1095     using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
  1096     by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
  1097   moreover note Pxyz[THEN distributed_real_AE]
  1098   ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
  1099     Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
  1100     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
  1101     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
  1102   proof eventually_elim
  1103     case (goal1 x)
  1104     show ?case
  1105     proof cases
  1106       assume "Pxyz x \<noteq> 0"
  1107       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"
  1108         by auto
  1109       then show ?thesis
  1110         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
  1111     qed simp
  1112   qed
  1113   with I1 I2 show ?eq
  1114     unfolding conditional_mutual_information_def
  1115     apply (subst mi_eq)
  1116     apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
  1117     apply (subst integral_diff(2)[symmetric])
  1118     apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
  1119     done
  1120 
  1121   let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
  1122   interpret P: prob_space ?P
  1123     unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
  1124     using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
  1125 
  1126   let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
  1127   interpret Q: prob_space ?Q
  1128     unfolding distributed_distr_eq_density[OF Pyz, symmetric]
  1129     using distributed_measurable[OF Pyz] by (rule prob_space_distr)
  1130 
  1131   let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
  1132 
  1133   from subdensity_real[of snd, OF _ Pyz Pz]
  1134   have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
  1135   have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
  1136     using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1137 
  1138   have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
  1139     using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
  1140     apply (intro TP.AE_pair_measure)
  1141     apply (auto simp: comp_def measurable_split_conv
  1142                 intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
  1143                         SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
  1144                         measurable_Pair
  1145                 dest: distributed_real_AE distributed_real_measurable)
  1146     done
  1147 
  1148   note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
  1149            measurable_compose[OF _ measurable_snd]
  1150            measurable_Pair
  1151            measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
  1152            measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
  1153            measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
  1154            measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
  1155            measurable_compose[OF _ Px[THEN distributed_real_measurable]]
  1156            STP.borel_measurable_positive_integral_snd
  1157   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))"
  1158     apply (subst positive_integral_density)
  1159     apply (rule distributed_borel_measurable[OF Pxyz])
  1160     apply (rule distributed_AE[OF Pxyz])
  1161     apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
  1162     apply (rule positive_integral_mono_AE)
  1163     using ae5 ae6 ae7 ae8
  1164     apply eventually_elim
  1165     apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
  1166     done
  1167   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)"
  1168     by (subst STP.positive_integral_snd_measurable[symmetric])
  1169        (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
  1170   also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
  1171     apply (rule positive_integral_cong_AE)
  1172     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
  1173     apply eventually_elim
  1174   proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
  1175     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"
  1176       "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
  1177     then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
  1178       apply (subst positive_integral_multc)
  1179       apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
  1180                           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
  1181                   split: prod.split)
  1182       done
  1183   qed
  1184   also have "\<dots> = 1"
  1185     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
  1186     by (subst positive_integral_density[symmetric]) (auto intro!: M)
  1187   finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
  1188   also have "\<dots> < \<infinity>" by simp
  1189   finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
  1190 
  1191   have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
  1192     apply (subst positive_integral_density)
  1193     apply (rule distributed_borel_measurable[OF Pxyz])
  1194     apply (rule distributed_AE[OF Pxyz])
  1195     apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
  1196     apply (simp add: split_beta')
  1197   proof
  1198     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)))"
  1199     assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
  1200     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
  1201       by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
  1202     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
  1203       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1204       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
  1205     then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
  1206       by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
  1207     with P.emeasure_space_1 show False
  1208       by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
  1209   qed
  1210 
  1211   have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
  1212     apply (rule positive_integral_0_iff_AE[THEN iffD2])
  1213     apply (auto intro!: M simp: split_beta') []
  1214     apply (subst AE_density)
  1215     apply (auto intro!: M simp: split_beta') []
  1216     using ae5 ae6 ae7 ae8
  1217     apply eventually_elim
  1218     apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
  1219     done
  1220 
  1221   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))))"
  1222     apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
  1223     using ae
  1224     apply (auto intro!: M simp: split_beta')
  1225     done
  1226 
  1227   have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
  1228   proof (intro le_imp_neg_le log_le[OF b_gt_1])
  1229     show "0 < integral\<^isup>L ?P ?f"
  1230       using neg pos fin positive_integral_positive[of ?P ?f]
  1231       by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def less_le split_beta')
  1232     show "integral\<^isup>L ?P ?f \<le> 1"
  1233       using neg le1 fin positive_integral_positive[of ?P ?f]
  1234       by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def split_beta' one_ereal_def)
  1235   qed
  1236   also have "- log b (integral\<^isup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
  1237   proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
  1238     show "AE x in ?P. ?f x \<in> {0<..}"
  1239       unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
  1240       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1241       by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
  1242     show "integrable ?P ?f"
  1243       unfolding integrable_def 
  1244       using fin neg by (auto intro!: M simp: split_beta')
  1245     show "integrable ?P (\<lambda>x. - log b (?f x))"
  1246       apply (subst integral_density)
  1247       apply (auto intro!: M) []
  1248       apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
  1249       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1250       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
  1251       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1252       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1253       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1254       apply eventually_elim
  1255       apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
  1256       done
  1257   qed (auto simp: b_gt_1 minus_log_convex)
  1258   also have "\<dots> = conditional_mutual_information b S T P X Y Z"
  1259     unfolding `?eq`
  1260     apply (subst integral_density)
  1261     apply (auto intro!: M) []
  1262     apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
  1263     apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1264     apply (intro integral_cong_AE)
  1265     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1266     apply eventually_elim
  1267     apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
  1268     done
  1269   finally show ?nonneg
  1270     by simp
  1271 qed
  1272 
  1273 lemma (in information_space)
  1274   fixes Px :: "_ \<Rightarrow> real"
  1275   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
  1276   assumes Fx: "finite_entropy S X Px"
  1277   assumes Fz: "finite_entropy P Z Pz"
  1278   assumes Fyz: "finite_entropy (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
  1279   assumes Fxz: "finite_entropy (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
  1280   assumes Fxyz: "finite_entropy (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
  1281   shows conditional_mutual_information_generic_eq': "conditional_mutual_information b S T P X Y Z
  1282     = (\<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")
  1283     and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
  1284 proof -
  1285   note Px = Fx[THEN finite_entropy_distributed]
  1286   note Pz = Fz[THEN finite_entropy_distributed]
  1287   note Pyz = Fyz[THEN finite_entropy_distributed]
  1288   note Pxz = Fxz[THEN finite_entropy_distributed]
  1289   note Pxyz = Fxyz[THEN finite_entropy_distributed]
  1290 
  1291   interpret S: sigma_finite_measure S by fact
  1292   interpret T: sigma_finite_measure T by fact
  1293   interpret P: sigma_finite_measure P by fact
  1294   interpret TP: pair_sigma_finite T P ..
  1295   interpret SP: pair_sigma_finite S P ..
  1296   interpret ST: pair_sigma_finite S T ..
  1297   interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
  1298   interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
  1299   interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
  1300   have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
  1301   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
  1302   have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
  1303     using Pyz by (simp add: distributed_measurable)
  1304 
  1305   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"
  1306     using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
  1307 
  1308   { fix f g h M
  1309     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)"
  1310     from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
  1311          measurable_comp[OF f Px[THEN distributed_real_measurable]]
  1312          measurable_comp[OF g Pz[THEN distributed_real_measurable]]
  1313     have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
  1314       by (simp add: comp_def b_gt_1) }
  1315   note borel_log = this
  1316 
  1317   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)"
  1318     by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
  1319   
  1320   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
  1321     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))"
  1322     by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
  1323 
  1324   have "mutual_information b S P X Z =
  1325     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
  1326     by (rule mutual_information_distr[OF S P Px Pz Pxz])
  1327   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))"
  1328     using b_gt_1 Pxz Px Pz
  1329     by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
  1330        (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
  1331              dest!: distributed_real_measurable)
  1332   finally have mi_eq:
  1333     "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))" .
  1334   
  1335   have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
  1336     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
  1337   moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1338     by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
  1339   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"
  1340     by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
  1341   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
  1342     by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
  1343   moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
  1344     using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
  1345   moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
  1346     using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1347   moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
  1348     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)
  1349   moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
  1350     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
  1351     using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
  1352     using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
  1353     by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
  1354   moreover note ae9 = Pxyz[THEN distributed_real_AE]
  1355   ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
  1356     Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
  1357     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
  1358     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
  1359   proof eventually_elim
  1360     case (goal1 x)
  1361     show ?case
  1362     proof cases
  1363       assume "Pxyz x \<noteq> 0"
  1364       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"
  1365         by auto
  1366       then show ?thesis
  1367         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
  1368     qed simp
  1369   qed
  1370 
  1371   have "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)
  1372     (\<lambda>x. Pxyz x * log b (Pxyz x) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pyz (snd x)))"
  1373     using finite_entropy_integrable[OF Fxyz]
  1374     using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
  1375     using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
  1376     by simp
  1377   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)"
  1378     using Pxyz Px Pyz
  1379     by (auto intro!: borel_measurable_times measurable_fst'' measurable_snd'' dest!: distributed_real_measurable simp: split_beta')
  1380   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))))"
  1381     apply (rule integrable_cong_AE_imp)
  1382     using ae1 ae4 ae5 ae6 ae9
  1383     by eventually_elim
  1384        (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
  1385 
  1386   have "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)
  1387     (\<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))))"
  1388     using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
  1389     using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
  1390     using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
  1391     by (simp add: measurable_Pair measurable_snd'' comp_def)
  1392   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)"
  1393     using Pxyz Px Pz
  1394     by (auto intro!: measurable_compose[OF _ distributed_real_measurable[OF Pxz]]
  1395                      measurable_Pair borel_measurable_times measurable_fst'' measurable_snd''
  1396              dest!: distributed_real_measurable simp: split_beta')
  1397   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)))"
  1398     apply (rule integrable_cong_AE_imp)
  1399     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
  1400     by eventually_elim
  1401        (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
  1402 
  1403   from ae I1 I2 show ?eq
  1404     unfolding conditional_mutual_information_def
  1405     apply (subst mi_eq)
  1406     apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
  1407     apply (subst integral_diff(2)[symmetric])
  1408     apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
  1409     done
  1410 
  1411   let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
  1412   interpret P: prob_space ?P
  1413     unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
  1414     using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
  1415 
  1416   let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
  1417   interpret Q: prob_space ?Q
  1418     unfolding distributed_distr_eq_density[OF Pyz, symmetric]
  1419     using distributed_measurable[OF Pyz] by (rule prob_space_distr)
  1420 
  1421   let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
  1422 
  1423   from subdensity_real[of snd, OF _ Pyz Pz]
  1424   have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
  1425   have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
  1426     using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1427 
  1428   have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
  1429     using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
  1430     apply (intro TP.AE_pair_measure)
  1431     apply (auto simp: comp_def measurable_split_conv
  1432                 intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
  1433                         SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
  1434                         measurable_Pair
  1435                 dest: distributed_real_AE distributed_real_measurable)
  1436     done
  1437 
  1438   note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
  1439            measurable_compose[OF _ measurable_snd]
  1440            measurable_Pair
  1441            measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
  1442            measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
  1443            measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
  1444            measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
  1445            measurable_compose[OF _ Px[THEN distributed_real_measurable]]
  1446            STP.borel_measurable_positive_integral_snd
  1447   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))"
  1448     apply (subst positive_integral_density)
  1449     apply (rule distributed_borel_measurable[OF Pxyz])
  1450     apply (rule distributed_AE[OF Pxyz])
  1451     apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
  1452     apply (rule positive_integral_mono_AE)
  1453     using ae5 ae6 ae7 ae8
  1454     apply eventually_elim
  1455     apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
  1456     done
  1457   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)"
  1458     by (subst STP.positive_integral_snd_measurable[symmetric])
  1459        (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
  1460   also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
  1461     apply (rule positive_integral_cong_AE)
  1462     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
  1463     apply eventually_elim
  1464   proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
  1465     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"
  1466       "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
  1467     then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
  1468       apply (subst positive_integral_multc)
  1469       apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
  1470                           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
  1471                   split: prod.split)
  1472       done
  1473   qed
  1474   also have "\<dots> = 1"
  1475     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
  1476     by (subst positive_integral_density[symmetric]) (auto intro!: M)
  1477   finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
  1478   also have "\<dots> < \<infinity>" by simp
  1479   finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
  1480 
  1481   have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
  1482     apply (subst positive_integral_density)
  1483     apply (rule distributed_borel_measurable[OF Pxyz])
  1484     apply (rule distributed_AE[OF Pxyz])
  1485     apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
  1486     apply (simp add: split_beta')
  1487   proof
  1488     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)))"
  1489     assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
  1490     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
  1491       by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
  1492     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
  1493       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1494       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
  1495     then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
  1496       by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
  1497     with P.emeasure_space_1 show False
  1498       by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
  1499   qed
  1500 
  1501   have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
  1502     apply (rule positive_integral_0_iff_AE[THEN iffD2])
  1503     apply (auto intro!: M simp: split_beta') []
  1504     apply (subst AE_density)
  1505     apply (auto intro!: M simp: split_beta') []
  1506     using ae5 ae6 ae7 ae8
  1507     apply eventually_elim
  1508     apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
  1509     done
  1510 
  1511   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))))"
  1512     apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
  1513     using ae
  1514     apply (auto intro!: M simp: split_beta')
  1515     done
  1516 
  1517   have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
  1518   proof (intro le_imp_neg_le log_le[OF b_gt_1])
  1519     show "0 < integral\<^isup>L ?P ?f"
  1520       using neg pos fin positive_integral_positive[of ?P ?f]
  1521       by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def less_le split_beta')
  1522     show "integral\<^isup>L ?P ?f \<le> 1"
  1523       using neg le1 fin positive_integral_positive[of ?P ?f]
  1524       by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def split_beta' one_ereal_def)
  1525   qed
  1526   also have "- log b (integral\<^isup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
  1527   proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
  1528     show "AE x in ?P. ?f x \<in> {0<..}"
  1529       unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
  1530       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1531       by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
  1532     show "integrable ?P ?f"
  1533       unfolding integrable_def 
  1534       using fin neg by (auto intro!: M simp: split_beta')
  1535     show "integrable ?P (\<lambda>x. - log b (?f x))"
  1536       apply (subst integral_density)
  1537       apply (auto intro!: M) []
  1538       apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
  1539       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1540       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
  1541       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1542       apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1543       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1544       apply eventually_elim
  1545       apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
  1546       done
  1547   qed (auto simp: b_gt_1 minus_log_convex)
  1548   also have "\<dots> = conditional_mutual_information b S T P X Y Z"
  1549     unfolding `?eq`
  1550     apply (subst integral_density)
  1551     apply (auto intro!: M) []
  1552     apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
  1553     apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
  1554     apply (intro integral_cong_AE)
  1555     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
  1556     apply eventually_elim
  1557     apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
  1558     done
  1559   finally show ?nonneg
  1560     by simp
  1561 qed
  1562 
  1563 lemma (in information_space) conditional_mutual_information_eq:
  1564   assumes Pz: "simple_distributed M Z Pz"
  1565   assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
  1566   assumes Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"
  1567   assumes Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"
  1568   shows "\<I>(X ; Y | Z) =
  1569    (\<Sum>(x, y, z)\<in>(\<lambda>x. (X x, Y x, Z x))`space M. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
  1570 proof (subst conditional_mutual_information_generic_eq[OF _ _ _ _
  1571     simple_distributed[OF Pz] simple_distributed_joint[OF Pyz] simple_distributed_joint[OF Pxz]
  1572     simple_distributed_joint2[OF Pxyz]])
  1573   note simple_distributed_joint2_finite[OF Pxyz, simp]
  1574   show "sigma_finite_measure (count_space (X ` space M))"
  1575     by (simp add: sigma_finite_measure_count_space_finite)
  1576   show "sigma_finite_measure (count_space (Y ` space M))"
  1577     by (simp add: sigma_finite_measure_count_space_finite)
  1578   show "sigma_finite_measure (count_space (Z ` space M))"
  1579     by (simp add: sigma_finite_measure_count_space_finite)
  1580   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =
  1581       count_space (X`space M \<times> Y`space M \<times> Z`space M)"
  1582     (is "?P = ?C")
  1583     by (simp add: pair_measure_count_space)
  1584 
  1585   let ?Px = "\<lambda>x. measure M (X -` {x} \<inter> space M)"
  1586   have "(\<lambda>x. (X x, Z x)) \<in> measurable M (count_space (X ` space M) \<Otimes>\<^isub>M count_space (Z ` space M))"
  1587     using simple_distributed_joint[OF Pxz] by (rule distributed_measurable)
  1588   from measurable_comp[OF this measurable_fst]
  1589   have "random_variable (count_space (X ` space M)) X"
  1590     by (simp add: comp_def)
  1591   then have "simple_function M X"    
  1592     unfolding simple_function_def by auto
  1593   then have "simple_distributed M X ?Px"
  1594     by (rule simple_distributedI) auto
  1595   then show "distributed M (count_space (X ` space M)) X ?Px"
  1596     by (rule simple_distributed)
  1597 
  1598   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then Pxyz x else 0)"
  1599   let ?g = "(\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x)) ` space M then Pyz x else 0)"
  1600   let ?h = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x)) ` space M then Pxz x else 0)"
  1601   show
  1602       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?f (x, y, z) / (?Px x * ?g (y, z))))"
  1603       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?h (x, z) / (?Px x * Pz z)))"
  1604     by (auto intro!: integrable_count_space simp: pair_measure_count_space)
  1605   let ?i = "\<lambda>x y z. ?f (x, y, z) * log b (?f (x, y, z) / (?h (x, z) * (?g (y, z) / Pz z)))"
  1606   let ?j = "\<lambda>x y z. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z)))"
  1607   have "(\<lambda>(x, y, z). ?i x y z) = (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then ?j (fst x) (fst (snd x)) (snd (snd x)) else 0)"
  1608     by (auto intro!: ext)
  1609   then show "(\<integral> (x, y, z). ?i x y z \<partial>?P) = (\<Sum>(x, y, z)\<in>(\<lambda>x. (X x, Y x, Z x)) ` space M. ?j x y z)"
  1610     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta')
  1611 qed
  1612 
  1613 lemma (in information_space) conditional_mutual_information_nonneg:
  1614   assumes X: "simple_function M X" and Y: "simple_function M Y" and Z: "simple_function M Z"
  1615   shows "0 \<le> \<I>(X ; Y | Z)"
  1616 proof -
  1617   have [simp]: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =
  1618       count_space (X`space M \<times> Y`space M \<times> Z`space M)"
  1619     by (simp add: pair_measure_count_space X Y Z simple_functionD)
  1620   note sf = sigma_finite_measure_count_space_finite[OF simple_functionD(1)]
  1621   note sd = simple_distributedI[OF _ refl]
  1622   note sp = simple_function_Pair
  1623   show ?thesis
  1624    apply (rule conditional_mutual_information_generic_nonneg[OF sf[OF X] sf[OF Y] sf[OF Z]])
  1625    apply (rule simple_distributed[OF sd[OF X]])
  1626    apply (rule simple_distributed[OF sd[OF Z]])
  1627    apply (rule simple_distributed_joint[OF sd[OF sp[OF Y Z]]])
  1628    apply (rule simple_distributed_joint[OF sd[OF sp[OF X Z]]])
  1629    apply (rule simple_distributed_joint2[OF sd[OF sp[OF X sp[OF Y Z]]]])
  1630    apply (auto intro!: integrable_count_space simp: X Y Z simple_functionD)
  1631    done
  1632 qed
  1633 
  1634 subsection {* Conditional Entropy *}
  1635 
  1636 definition (in prob_space)
  1637   "conditional_entropy b S T X Y = - (\<integral>(x, y). log b (real (RN_deriv (S \<Otimes>\<^isub>M T) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (x, y)) / 
  1638     real (RN_deriv T (distr M T Y) y)) \<partial>distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
  1639 
  1640 abbreviation (in information_space)
  1641   conditional_entropy_Pow ("\<H>'(_ | _')") where
  1642   "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
  1643 
  1644 lemma (in information_space) conditional_entropy_generic_eq:
  1645   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
  1646   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1647   assumes Py: "distributed M T Y Py"
  1648   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1649   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))"
  1650 proof -
  1651   interpret S: sigma_finite_measure S by fact
  1652   interpret T: sigma_finite_measure T by fact
  1653   interpret ST: pair_sigma_finite S T ..
  1654 
  1655   have "AE x in density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x)). Pxy x = real (RN_deriv (S \<Otimes>\<^isub>M T) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) x)"
  1656     unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
  1657     unfolding distributed_distr_eq_density[OF Pxy]
  1658     using distributed_RN_deriv[OF Pxy]
  1659     by auto
  1660   moreover
  1661   have "AE x in density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x)). Py (snd x) = real (RN_deriv T (distr M T Y) (snd x))"
  1662     unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
  1663     unfolding distributed_distr_eq_density[OF Py]
  1664     apply (rule ST.AE_pair_measure)
  1665     apply (auto intro!: sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
  1666                         distributed_real_measurable[OF Pxy] distributed_real_AE[OF Py]
  1667                         borel_measurable_real_of_ereal measurable_compose[OF _ borel_measurable_RN_deriv_density])
  1668     using distributed_RN_deriv[OF Py]
  1669     apply auto
  1670     done    
  1671   ultimately
  1672   have "conditional_entropy b S T X Y = - (\<integral>x. Pxy x * log b (Pxy x / Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1673     unfolding conditional_entropy_def neg_equal_iff_equal
  1674     apply (subst integral_density(1)[symmetric])
  1675     apply (auto simp: distributed_real_measurable[OF Pxy] distributed_real_AE[OF Pxy]
  1676                       measurable_compose[OF _ distributed_real_measurable[OF Py]]
  1677                       distributed_distr_eq_density[OF Pxy]
  1678                 intro!: integral_cong_AE)
  1679     done
  1680   then show ?thesis by (simp add: split_beta')
  1681 qed
  1682 
  1683 lemma (in information_space) conditional_entropy_eq_entropy:
  1684   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
  1685   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1686   assumes Py: "distributed M T Y Py"
  1687   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1688   assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
  1689   assumes I2: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
  1690   shows "conditional_entropy b S T X Y = entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) - entropy b T Y"
  1691 proof -
  1692   interpret S: sigma_finite_measure S by fact
  1693   interpret T: sigma_finite_measure T by fact
  1694   interpret ST: pair_sigma_finite S T ..
  1695 
  1696   have "entropy b T Y = - (\<integral>y. Py y * log b (Py y) \<partial>T)"
  1697     by (rule entropy_distr[OF Py])
  1698   also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))"
  1699     using b_gt_1 Py[THEN distributed_real_measurable]
  1700     by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
  1701   finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
  1702 
  1703   have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1704     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
  1705   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
  1706     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1707   moreover note ae5 = Pxy[THEN distributed_real_AE]
  1708   ultimately have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Py (snd x) \<and>
  1709     (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Py (snd x)))"
  1710     by eventually_elim auto
  1711   then have ae: "AE x in S \<Otimes>\<^isub>M T.
  1712      Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
  1713     by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
  1714   have "conditional_entropy b S T X Y = 
  1715     - (\<integral>x. Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1716     unfolding conditional_entropy_generic_eq[OF S T Py Pxy] neg_equal_iff_equal
  1717     apply (intro integral_cong_AE)
  1718     using ae
  1719     apply eventually_elim
  1720     apply auto
  1721     done
  1722   also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) - - (\<integral>x.  Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1723     by (simp add: integral_diff[OF I1 I2])
  1724   finally show ?thesis 
  1725     unfolding conditional_entropy_generic_eq[OF S T Py Pxy] entropy_distr[OF Pxy] e_eq
  1726     by (simp add: split_beta')
  1727 qed
  1728 
  1729 lemma (in information_space) conditional_entropy_eq_entropy_simple:
  1730   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1731   shows "\<H>(X | Y) = entropy b (count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x)) - \<H>(Y)"
  1732 proof -
  1733   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
  1734     (is "?P = ?C") using X Y by (simp add: simple_functionD pair_measure_count_space)
  1735   show ?thesis
  1736     by (rule conditional_entropy_eq_entropy sigma_finite_measure_count_space_finite
  1737                  simple_functionD  X Y simple_distributed simple_distributedI[OF _ refl]
  1738                  simple_distributed_joint simple_function_Pair integrable_count_space)+
  1739        (auto simp: `?P = ?C` intro!: integrable_count_space simple_functionD  X Y)
  1740 qed
  1741 
  1742 lemma (in information_space) conditional_entropy_eq:
  1743   assumes Y: "simple_distributed M Y Py"
  1744   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
  1745     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))"
  1746 proof (subst conditional_entropy_generic_eq[OF _ _
  1747   simple_distributed[OF Y] simple_distributed_joint[OF XY]])
  1748   have "finite ((\<lambda>x. (X x, Y x))`space M)"
  1749     using XY unfolding simple_distributed_def by auto
  1750   from finite_imageI[OF this, of fst]
  1751   have [simp]: "finite (X`space M)"
  1752     by (simp add: image_compose[symmetric] comp_def)
  1753   note Y[THEN simple_distributed_finite, simp]
  1754   show "sigma_finite_measure (count_space (X ` space M))"
  1755     by (simp add: sigma_finite_measure_count_space_finite)
  1756   show "sigma_finite_measure (count_space (Y ` space M))"
  1757     by (simp add: sigma_finite_measure_count_space_finite)
  1758   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
  1759   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
  1760     (is "?P = ?C")
  1761     using Y by (simp add: simple_distributed_finite pair_measure_count_space)
  1762   have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
  1763     (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / Py (snd x)) else 0)"
  1764     by auto
  1765   from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
  1766     - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
  1767     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
  1768 qed
  1769 
  1770 lemma (in information_space) conditional_mutual_information_eq_conditional_entropy:
  1771   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1772   shows "\<I>(X ; X | Y) = \<H>(X | Y)"
  1773 proof -
  1774   def Py \<equiv> "\<lambda>x. if x \<in> Y`space M then measure M (Y -` {x} \<inter> space M) else 0"
  1775   def Pxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M) else 0"
  1776   def Pxxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, X x, Y x))`space M then measure M ((\<lambda>x. (X x, X x, Y x)) -` {x} \<inter> space M) else 0"
  1777   let ?M = "X`space M \<times> X`space M \<times> Y`space M"
  1778 
  1779   note XY = simple_function_Pair[OF X Y]
  1780   note XXY = simple_function_Pair[OF X XY]
  1781   have Py: "simple_distributed M Y Py"
  1782     using Y by (rule simple_distributedI) (auto simp: Py_def)
  1783   have Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
  1784     using XY by (rule simple_distributedI) (auto simp: Pxy_def)
  1785   have Pxxy: "simple_distributed M (\<lambda>x. (X x, X x, Y x)) Pxxy"
  1786     using XXY by (rule simple_distributedI) (auto simp: Pxxy_def)
  1787   have eq: "(\<lambda>x. (X x, X x, Y x)) ` space M = (\<lambda>(x, y). (x, x, y)) ` (\<lambda>x. (X x, Y x)) ` space M"
  1788     by auto
  1789   have inj: "\<And>A. inj_on (\<lambda>(x, y). (x, x, y)) A"
  1790     by (auto simp: inj_on_def)
  1791   have Pxxy_eq: "\<And>x y. Pxxy (x, x, y) = Pxy (x, y)"
  1792     by (auto simp: Pxxy_def Pxy_def intro!: arg_cong[where f=prob])
  1793   have "AE x in count_space ((\<lambda>x. (X x, Y x))`space M). Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1794     by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
  1795   then show ?thesis
  1796     apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
  1797     apply (subst conditional_entropy_eq[OF Py Pxy])
  1798     apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
  1799                 log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
  1800     using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
  1801   apply (auto simp add: not_le[symmetric] AE_count_space)
  1802     done
  1803 qed
  1804 
  1805 lemma (in information_space) conditional_entropy_nonneg:
  1806   assumes X: "simple_function M X" and Y: "simple_function M Y" shows "0 \<le> \<H>(X | Y)"
  1807   using conditional_mutual_information_eq_conditional_entropy[OF X Y] conditional_mutual_information_nonneg[OF X X Y]
  1808   by simp
  1809 
  1810 subsection {* Equalities *}
  1811 
  1812 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy_distr:
  1813   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
  1814   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1815   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
  1816   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1817   assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
  1818   assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
  1819   assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
  1820   shows  "mutual_information b S T X Y = entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
  1821 proof -
  1822   have X: "entropy b S X = - (\<integral>x. Pxy x * log b (Px (fst x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1823     using b_gt_1 Px[THEN distributed_real_measurable]
  1824     apply (subst entropy_distr[OF Px])
  1825     apply (subst distributed_transform_integral[OF Pxy Px, where T=fst])
  1826     apply (auto intro!: integral_cong)
  1827     done
  1828 
  1829   have Y: "entropy b T Y = - (\<integral>x. Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1830     using b_gt_1 Py[THEN distributed_real_measurable]
  1831     apply (subst entropy_distr[OF Py])
  1832     apply (subst distributed_transform_integral[OF Pxy Py, where T=snd])
  1833     apply (auto intro!: integral_cong)
  1834     done
  1835 
  1836   interpret S: sigma_finite_measure S by fact
  1837   interpret T: sigma_finite_measure T by fact
  1838   interpret ST: pair_sigma_finite S T ..
  1839   have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
  1840 
  1841   have XY: "entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^isub>M T))"
  1842     by (subst entropy_distr[OF Pxy]) (auto intro!: integral_cong)
  1843   
  1844   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
  1845     by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
  1846   moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1847     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
  1848   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
  1849     using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
  1850   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
  1851     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1852   moreover note Pxy[THEN distributed_real_AE]
  1853   ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) = 
  1854     Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
  1855     (is "AE x in _. ?f x = ?g x")
  1856   proof eventually_elim
  1857     case (goal1 x)
  1858     show ?case
  1859     proof cases
  1860       assume "Pxy x \<noteq> 0"
  1861       with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
  1862         by auto
  1863       then show ?thesis
  1864         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
  1865     qed simp
  1866   qed
  1867 
  1868   have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?f"
  1869     unfolding X Y XY
  1870     apply (subst integral_diff)
  1871     apply (intro integral_diff Ixy Ix Iy)+
  1872     apply (subst integral_diff)
  1873     apply (intro integral_diff Ixy Ix Iy)+
  1874     apply (simp add: field_simps)
  1875     done
  1876   also have "\<dots> = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?g"
  1877     using `AE x in _. ?f x = ?g x` by (rule integral_cong_AE)
  1878   also have "\<dots> = mutual_information b S T X Y"
  1879     by (rule mutual_information_distr[OF S T Px Py Pxy, symmetric])
  1880   finally show ?thesis ..
  1881 qed
  1882 
  1883 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy':
  1884   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
  1885   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1886   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
  1887   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1888   assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
  1889   assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
  1890   assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
  1891   shows  "mutual_information b S T X Y = entropy b S X - conditional_entropy b S T X Y"
  1892   using
  1893     mutual_information_eq_entropy_conditional_entropy_distr[OF S T Px Py Pxy Ix Iy Ixy]
  1894     conditional_entropy_eq_entropy[OF S T Py Pxy Ixy Iy]
  1895   by simp
  1896 
  1897 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
  1898   assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
  1899   shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"
  1900 proof -
  1901   have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
  1902     using sf_X by (rule simple_distributedI) auto
  1903   have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
  1904     using sf_Y by (rule simple_distributedI) auto
  1905   have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
  1906     using sf_X sf_Y by (rule simple_function_Pair)
  1907   then have XY: "simple_distributed M (\<lambda>x. (X x, Y x)) (\<lambda>x. measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M))"
  1908     by (rule simple_distributedI) auto
  1909   from simple_distributed_joint_finite[OF this, simp]
  1910   have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
  1911     by (simp add: pair_measure_count_space)
  1912 
  1913   have "\<I>(X ; Y) = \<H>(X) + \<H>(Y) - entropy b (count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x))"
  1914     using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]
  1915     by (rule mutual_information_eq_entropy_conditional_entropy_distr) (auto simp: eq integrable_count_space)
  1916   then show ?thesis
  1917     unfolding conditional_entropy_eq_entropy_simple[OF sf_X sf_Y] by simp
  1918 qed
  1919 
  1920 lemma (in information_space) mutual_information_nonneg_simple:
  1921   assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
  1922   shows  "0 \<le> \<I>(X ; Y)"
  1923 proof -
  1924   have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
  1925     using sf_X by (rule simple_distributedI) auto
  1926   have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
  1927     using sf_Y by (rule simple_distributedI) auto
  1928 
  1929   have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
  1930     using sf_X sf_Y by (rule simple_function_Pair)
  1931   then have XY: "simple_distributed M (\<lambda>x. (X x, Y x)) (\<lambda>x. measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M))"
  1932     by (rule simple_distributedI) auto
  1933 
  1934   from simple_distributed_joint_finite[OF this, simp]
  1935   have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
  1936     by (simp add: pair_measure_count_space)
  1937 
  1938   show ?thesis
  1939     by (rule mutual_information_nonneg[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
  1940        (simp_all add: eq integrable_count_space sigma_finite_measure_count_space_finite)
  1941 qed
  1942 
  1943 lemma (in information_space) conditional_entropy_less_eq_entropy:
  1944   assumes X: "simple_function M X" and Z: "simple_function M Z"
  1945   shows "\<H>(X | Z) \<le> \<H>(X)"
  1946 proof -
  1947   have "0 \<le> \<I>(X ; Z)" using X Z by (rule mutual_information_nonneg_simple)
  1948   also have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
  1949   finally show ?thesis by auto
  1950 qed
  1951 
  1952 lemma (in information_space) 
  1953   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
  1954   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1955   assumes Px: "finite_entropy S X Px" and Py: "finite_entropy T Y Py"
  1956   assumes Pxy: "finite_entropy (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1957   shows "conditional_entropy b S T X Y \<le> entropy b S X"
  1958 proof -
  1959 
  1960   have "0 \<le> mutual_information b S T X Y" 
  1961     by (rule mutual_information_nonneg') fact+
  1962   also have "\<dots> = entropy b S X - conditional_entropy b S T X Y"
  1963     apply (rule mutual_information_eq_entropy_conditional_entropy')
  1964     using assms
  1965     by (auto intro!: finite_entropy_integrable finite_entropy_distributed
  1966       finite_entropy_integrable_transform[OF Px]
  1967       finite_entropy_integrable_transform[OF Py])
  1968   finally show ?thesis by auto
  1969 qed
  1970 
  1971 lemma (in information_space) entropy_chain_rule:
  1972   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1973   shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
  1974 proof -
  1975   note XY = simple_distributedI[OF simple_function_Pair[OF X Y] refl]
  1976   note YX = simple_distributedI[OF simple_function_Pair[OF Y X] refl]
  1977   note simple_distributed_joint_finite[OF this, simp]
  1978   let ?f = "\<lambda>x. prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
  1979   let ?g = "\<lambda>x. prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M)"
  1980   let ?h = "\<lambda>x. if x \<in> (\<lambda>x. (Y x, X x)) ` space M then prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M) else 0"
  1981   have "\<H>(\<lambda>x. (X x, Y x)) = - (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` space M. ?f x * log b (?f x))"
  1982     using XY by (rule entropy_simple_distributed)
  1983   also have "\<dots> = - (\<Sum>x\<in>(\<lambda>(x, y). (y, x)) ` (\<lambda>x. (X x, Y x)) ` space M. ?g x * log b (?g x))"
  1984     by (subst (2) setsum_reindex) (auto simp: inj_on_def intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
  1985   also have "\<dots> = - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` space M. ?h x * log b (?h x))"
  1986     by (auto intro!: setsum_cong)
  1987   also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
  1988     by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
  1989        (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
  1990              cong del: setsum_cong  intro!: setsum_mono_zero_left)
  1991   finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
  1992   then show ?thesis
  1993     unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
  1994 qed
  1995 
  1996 lemma (in information_space) entropy_partition:
  1997   assumes X: "simple_function M X"
  1998   shows "\<H>(X) = \<H>(f \<circ> X) + \<H>(X|f \<circ> X)"
  1999 proof -
  2000   note fX = simple_function_compose[OF X, of f]  
  2001   have eq: "(\<lambda>x. ((f \<circ> X) x, X x)) ` space M = (\<lambda>x. (f x, x)) ` X ` space M" by auto
  2002   have inj: "\<And>A. inj_on (\<lambda>x. (f x, x)) A"
  2003     by (auto simp: inj_on_def)
  2004   show ?thesis
  2005     apply (subst entropy_chain_rule[symmetric, OF fX X])
  2006     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]])
  2007     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
  2008     unfolding eq
  2009     apply (subst setsum_reindex[OF inj])
  2010     apply (auto intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
  2011     done
  2012 qed
  2013 
  2014 corollary (in information_space) entropy_data_processing:
  2015   assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
  2016 proof -
  2017   note fX = simple_function_compose[OF X, of f]
  2018   from X have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
  2019   then show "\<H>(f \<circ> X) \<le> \<H>(X)"
  2020     by (auto intro: conditional_entropy_nonneg[OF X fX])
  2021 qed
  2022 
  2023 corollary (in information_space) entropy_of_inj:
  2024   assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
  2025   shows "\<H>(f \<circ> X) = \<H>(X)"
  2026 proof (rule antisym)
  2027   show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
  2028 next
  2029   have sf: "simple_function M (f \<circ> X)"
  2030     using X by auto
  2031   have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
  2032     unfolding o_assoc
  2033     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
  2034     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\<lambda>x. prob (X -` {x} \<inter> space M)"])
  2035     apply (auto intro!: setsum_cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
  2036     done
  2037   also have "... \<le> \<H>(f \<circ> X)"
  2038     using entropy_data_processing[OF sf] .
  2039   finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
  2040 qed
  2041 
  2042 end