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