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