src/HOL/Probability/Information.thy
author hoelzl
Wed Oct 10 12:12:25 2012 +0200 (2012-10-10)
changeset 49786 f33d5f009627
parent 49785 0a8adca22974
child 49787 d8de705b48d4
permissions -rw-r--r--
continuous version of entropy_le
     1 (*  Title:      HOL/Probability/Information.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Armin Heller, TU München
     4 *)
     5 
     6 header {*Information theory*}
     7 
     8 theory Information
     9 imports
    10   Independent_Family
    11   Radon_Nikodym
    12   "~~/src/HOL/Library/Convex"
    13 begin
    14 
    15 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
    16   by (subst log_le_cancel_iff) auto
    17 
    18 lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
    19   by (subst log_less_cancel_iff) auto
    20 
    21 lemma setsum_cartesian_product':
    22   "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
    23   unfolding setsum_cartesian_product by simp
    24 
    25 section "Convex theory"
    26 
    27 lemma log_setsum:
    28   assumes "finite s" "s \<noteq> {}"
    29   assumes "b > 1"
    30   assumes "(\<Sum> i \<in> s. a i) = 1"
    31   assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
    32   assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
    33   shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
    34 proof -
    35   have "convex_on {0 <..} (\<lambda> x. - log b x)"
    36     by (rule minus_log_convex[OF `b > 1`])
    37   hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
    38     using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastforce
    39   thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
    40 qed
    41 
    42 lemma log_setsum':
    43   assumes "finite s" "s \<noteq> {}"
    44   assumes "b > 1"
    45   assumes "(\<Sum> i \<in> s. a i) = 1"
    46   assumes pos: "\<And> i. i \<in> s \<Longrightarrow> 0 \<le> a i"
    47           "\<And> i. \<lbrakk> i \<in> s ; 0 < a i \<rbrakk> \<Longrightarrow> 0 < y i"
    48   shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
    49 proof -
    50   have "\<And>y. (\<Sum> i \<in> s - {i. a i = 0}. a i * y i) = (\<Sum> i \<in> s. a i * y i)"
    51     using assms by (auto intro!: setsum_mono_zero_cong_left)
    52   moreover have "log b (\<Sum> i \<in> s - {i. a i = 0}. a i * y i) \<ge> (\<Sum> i \<in> s - {i. a i = 0}. a i * log b (y i))"
    53   proof (rule log_setsum)
    54     have "setsum a (s - {i. a i = 0}) = setsum a s"
    55       using assms(1) by (rule setsum_mono_zero_cong_left) auto
    56     thus sum_1: "setsum a (s - {i. a i = 0}) = 1"
    57       "finite (s - {i. a i = 0})" using assms by simp_all
    58 
    59     show "s - {i. a i = 0} \<noteq> {}"
    60     proof
    61       assume *: "s - {i. a i = 0} = {}"
    62       hence "setsum a (s - {i. a i = 0}) = 0" by (simp add: * setsum_empty)
    63       with sum_1 show False by simp
    64     qed
    65 
    66     fix i assume "i \<in> s - {i. a i = 0}"
    67     hence "i \<in> s" "a i \<noteq> 0" by simp_all
    68     thus "0 \<le> a i" "y i \<in> {0<..}" using pos[of i] by auto
    69   qed fact+
    70   ultimately show ?thesis by simp
    71 qed
    72 
    73 lemma log_setsum_divide:
    74   assumes "finite S" and "S \<noteq> {}" and "1 < b"
    75   assumes "(\<Sum>x\<in>S. g x) = 1"
    76   assumes pos: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
    77   assumes g_pos: "\<And>x. \<lbrakk> x \<in> S ; 0 < g x \<rbrakk> \<Longrightarrow> 0 < f x"
    78   shows "- (\<Sum>x\<in>S. g x * log b (g x / f x)) \<le> log b (\<Sum>x\<in>S. f x)"
    79 proof -
    80   have log_mono: "\<And>x y. 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log b x \<le> log b y"
    81     using `1 < b` by (subst log_le_cancel_iff) auto
    82 
    83   have "- (\<Sum>x\<in>S. g x * log b (g x / f x)) = (\<Sum>x\<in>S. g x * log b (f x / g x))"
    84   proof (unfold setsum_negf[symmetric], rule setsum_cong)
    85     fix x assume x: "x \<in> S"
    86     show "- (g x * log b (g x / f x)) = g x * log b (f x / g x)"
    87     proof (cases "g x = 0")
    88       case False
    89       with pos[OF x] g_pos[OF x] have "0 < f x" "0 < g x" by simp_all
    90       thus ?thesis using `1 < b` by (simp add: log_divide field_simps)
    91     qed simp
    92   qed rule
    93   also have "... \<le> log b (\<Sum>x\<in>S. g x * (f x / g x))"
    94   proof (rule log_setsum')
    95     fix x assume x: "x \<in> S" "0 < g x"
    96     with g_pos[OF x] show "0 < f x / g x" by (safe intro!: divide_pos_pos)
    97   qed fact+
    98   also have "... = log b (\<Sum>x\<in>S - {x. g x = 0}. f x)" using `finite S`
    99     by (auto intro!: setsum_mono_zero_cong_right arg_cong[where f="log b"]
   100         split: split_if_asm)
   101   also have "... \<le> log b (\<Sum>x\<in>S. f x)"
   102   proof (rule log_mono)
   103     have "0 = (\<Sum>x\<in>S - {x. g x = 0}. 0)" by simp
   104     also have "... < (\<Sum>x\<in>S - {x. g x = 0}. f x)" (is "_ < ?sum")
   105     proof (rule setsum_strict_mono)
   106       show "finite (S - {x. g x = 0})" using `finite S` by simp
   107       show "S - {x. g x = 0} \<noteq> {}"
   108       proof
   109         assume "S - {x. g x = 0} = {}"
   110         hence "(\<Sum>x\<in>S. g x) = 0" by (subst setsum_0') auto
   111         with `(\<Sum>x\<in>S. g x) = 1` show False by simp
   112       qed
   113       fix x assume "x \<in> S - {x. g x = 0}"
   114       thus "0 < f x" using g_pos[of x] pos(1)[of x] by auto
   115     qed
   116     finally show "0 < ?sum" .
   117     show "(\<Sum>x\<in>S - {x. g x = 0}. f x) \<le> (\<Sum>x\<in>S. f x)"
   118       using `finite S` pos by (auto intro!: setsum_mono2)
   119   qed
   120   finally show ?thesis .
   121 qed
   122 
   123 lemma split_pairs:
   124   "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
   125   "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
   126 
   127 section "Information theory"
   128 
   129 locale information_space = prob_space +
   130   fixes b :: real assumes b_gt_1: "1 < b"
   131 
   132 context information_space
   133 begin
   134 
   135 text {* Introduce some simplification rules for logarithm of base @{term b}. *}
   136 
   137 lemma log_neg_const:
   138   assumes "x \<le> 0"
   139   shows "log b x = log b 0"
   140 proof -
   141   { fix u :: real
   142     have "x \<le> 0" by fact
   143     also have "0 < exp u"
   144       using exp_gt_zero .
   145     finally have "exp u \<noteq> x"
   146       by auto }
   147   then show "log b x = log b 0"
   148     by (simp add: log_def ln_def)
   149 qed
   150 
   151 lemma log_mult_eq:
   152   "log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)"
   153   using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
   154   by (auto simp: zero_less_mult_iff mult_le_0_iff)
   155 
   156 lemma log_inverse_eq:
   157   "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
   158   using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp
   159 
   160 lemma log_divide_eq:
   161   "log b (A / B) = (if 0 < A * B then log b \<bar>A\<bar> - log b \<bar>B\<bar> else log b 0)"
   162   unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
   163   by (auto simp: zero_less_mult_iff mult_le_0_iff)
   164 
   165 lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
   166 
   167 end
   168 
   169 subsection "Kullback$-$Leibler divergence"
   170 
   171 text {* The Kullback$-$Leibler divergence is also known as relative entropy or
   172 Kullback$-$Leibler distance. *}
   173 
   174 definition
   175   "entropy_density b M N = log b \<circ> real \<circ> RN_deriv M N"
   176 
   177 definition
   178   "KL_divergence b M N = integral\<^isup>L N (entropy_density b M N)"
   179 
   180 lemma (in information_space) measurable_entropy_density:
   181   assumes ac: "absolutely_continuous M N" "sets N = events"
   182   shows "entropy_density b M N \<in> borel_measurable M"
   183 proof -
   184   from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
   185     unfolding entropy_density_def
   186     by (intro measurable_comp) auto
   187 qed
   188 
   189 lemma (in sigma_finite_measure) KL_density:
   190   fixes f :: "'a \<Rightarrow> real"
   191   assumes "1 < b"
   192   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   193   shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)"
   194   unfolding KL_divergence_def
   195 proof (subst integral_density)
   196   show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
   197     using f
   198     by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
   199   have "density M (RN_deriv M (density M f)) = density M f"
   200     using f by (intro density_RN_deriv_density) auto
   201   then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
   202     using f
   203     by (intro density_unique)
   204        (auto intro!: borel_measurable_log borel_measurable_RN_deriv_density simp: RN_deriv_density_nonneg)
   205   show "(\<integral>x. f x * entropy_density b M (density M (\<lambda>x. ereal (f x))) x \<partial>M) = (\<integral>x. f x * log b (f x) \<partial>M)"
   206     apply (intro integral_cong_AE)
   207     using eq
   208     apply eventually_elim
   209     apply (auto simp: entropy_density_def)
   210     done
   211 qed fact+
   212 
   213 lemma (in sigma_finite_measure) KL_density_density:
   214   fixes f g :: "'a \<Rightarrow> real"
   215   assumes "1 < b"
   216   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   217   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   218   assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
   219   shows "KL_divergence b (density M f) (density M g) = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
   220 proof -
   221   interpret Mf: sigma_finite_measure "density M f"
   222     using f by (subst sigma_finite_iff_density_finite) auto
   223   have "KL_divergence b (density M f) (density M g) =
   224     KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
   225     using f g ac by (subst density_density_divide) simp_all
   226   also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
   227     using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
   228   also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
   229     using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
   230   finally show ?thesis .
   231 qed
   232 
   233 lemma (in information_space) KL_gt_0:
   234   fixes D :: "'a \<Rightarrow> real"
   235   assumes "prob_space (density M D)"
   236   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   237   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   238   assumes A: "density M D \<noteq> M"
   239   shows "0 < KL_divergence b M (density M D)"
   240 proof -
   241   interpret N: prob_space "density M D" by fact
   242 
   243   obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"
   244     using measure_eqI[of "density M D" M] `density M D \<noteq> M` by auto
   245 
   246   let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
   247   have [simp, intro]: "?D_set \<in> sets M"
   248     using D by auto
   249 
   250   have D_neg: "(\<integral>\<^isup>+ x. ereal (- D x) \<partial>M) = 0"
   251     using D by (subst positive_integral_0_iff_AE) auto
   252 
   253   have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
   254     using D by (simp add: emeasure_density cong: positive_integral_cong)
   255   then have D_pos: "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = 1"
   256     using N.emeasure_space_1 by simp
   257 
   258   have "integrable M D" "integral\<^isup>L M D = 1"
   259     using D D_pos D_neg unfolding integrable_def lebesgue_integral_def by simp_all
   260 
   261   have "0 \<le> 1 - measure M ?D_set"
   262     using prob_le_1 by (auto simp: field_simps)
   263   also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
   264     using `integrable M D` `integral\<^isup>L M D = 1`
   265     by (simp add: emeasure_eq_measure)
   266   also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"
   267   proof (rule integral_less_AE)
   268     show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
   269       using `integrable M D`
   270       by (intro integral_diff integral_indicator) auto
   271   next
   272     from integral_cmult(1)[OF int, of "ln b"]
   273     show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 
   274       by (simp add: ac_simps)
   275   next
   276     show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
   277     proof
   278       assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
   279       then have disj: "AE x in M. D x = 1 \<or> D x = 0"
   280         using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
   281 
   282       have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
   283         using D(1) by auto
   284       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"
   285         using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
   286       finally have "AE x in M. D x = 1"
   287         using D D_pos by (intro AE_I_eq_1) auto
   288       then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. ereal (D x) * indicator A x\<partial>M)"
   289         by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
   290       also have "\<dots> = density M D A"
   291         using `A \<in> sets M` D by (simp add: emeasure_density)
   292       finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
   293     qed
   294     show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
   295       using D(1) by (auto intro: sets_Collect_conj)
   296 
   297     show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
   298       D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
   299       using D(2)
   300     proof (eventually_elim, safe)
   301       fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"
   302         and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"
   303 
   304       have "D t - 1 = D t - indicator ?D_set t"
   305         using Dt by simp
   306       also note eq
   307       also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"
   308         using b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
   309         by (simp add: log_def ln_div less_le)
   310       finally have "ln (1 / D t) = 1 / D t - 1"
   311         using `D t \<noteq> 0` by (auto simp: field_simps)
   312       from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
   313       show False by auto
   314     qed
   315 
   316     show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
   317       using D(2) AE_space
   318     proof eventually_elim
   319       fix t assume "t \<in> space M" "0 \<le> D t"
   320       show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
   321       proof cases
   322         assume asm: "D t \<noteq> 0"
   323         then have "0 < D t" using `0 \<le> D t` by auto
   324         then have "0 < 1 / D t" by auto
   325         have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
   326           using asm `t \<in> space M` by (simp add: field_simps)
   327         also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
   328           using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
   329         also have "\<dots> = D t * (ln b * log b (D t))"
   330           using `0 < D t` b_gt_1
   331           by (simp_all add: log_def ln_div)
   332         finally show ?thesis by simp
   333       qed simp
   334     qed
   335   qed
   336   also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"
   337     by (simp add: ac_simps)
   338   also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"
   339     using int by (rule integral_cmult)
   340   finally show ?thesis
   341     using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)
   342 qed
   343 
   344 lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"
   345 proof -
   346   have "AE x in M. 1 = RN_deriv M M x"
   347   proof (rule RN_deriv_unique)
   348     show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto
   349     show "density M (\<lambda>x. 1) = M"
   350       apply (auto intro!: measure_eqI emeasure_density)
   351       apply (subst emeasure_density)
   352       apply auto
   353       done
   354   qed
   355   then have "AE x in M. log b (real (RN_deriv M M x)) = 0"
   356     by (elim AE_mp) simp
   357   from integral_cong_AE[OF this]
   358   have "integral\<^isup>L M (entropy_density b M M) = 0"
   359     by (simp add: entropy_density_def comp_def)
   360   then show "KL_divergence b M M = 0"
   361     unfolding KL_divergence_def
   362     by auto
   363 qed
   364 
   365 lemma (in information_space) KL_eq_0_iff_eq:
   366   fixes D :: "'a \<Rightarrow> real"
   367   assumes "prob_space (density M D)"
   368   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   369   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   370   shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"
   371   using KL_same_eq_0[of b] KL_gt_0[OF assms]
   372   by (auto simp: less_le)
   373 
   374 lemma (in information_space) KL_eq_0_iff_eq_ac:
   375   fixes D :: "'a \<Rightarrow> real"
   376   assumes "prob_space N"
   377   assumes ac: "absolutely_continuous M N" "sets N = sets M"
   378   assumes int: "integrable N (entropy_density b M N)"
   379   shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"
   380 proof -
   381   interpret N: prob_space N by fact
   382   have "finite_measure N" by unfold_locales
   383   from real_RN_deriv[OF this ac] guess D . note D = this
   384   
   385   have "N = density M (RN_deriv M N)"
   386     using ac by (rule density_RN_deriv[symmetric])
   387   also have "\<dots> = density M D"
   388     using borel_measurable_RN_deriv[OF ac] D by (auto intro!: density_cong)
   389   finally have N: "N = density M D" .
   390 
   391   from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density
   392   have "integrable N (\<lambda>x. log b (D x))"
   393     by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])
   394        (auto simp: N entropy_density_def)
   395   with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"
   396     by (subst integral_density(2)[symmetric]) (auto simp: N[symmetric] comp_def)
   397   with `prob_space N` D show ?thesis
   398     unfolding N
   399     by (intro KL_eq_0_iff_eq) auto
   400 qed
   401 
   402 lemma (in information_space) KL_nonneg:
   403   assumes "prob_space (density M D)"
   404   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
   405   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
   406   shows "0 \<le> KL_divergence b M (density M D)"
   407   using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)
   408 
   409 lemma (in sigma_finite_measure) KL_density_density_nonneg:
   410   fixes f g :: "'a \<Rightarrow> real"
   411   assumes "1 < b"
   412   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"
   413   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"
   414   assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
   415   assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"
   416   shows "0 \<le> KL_divergence b (density M f) (density M g)"
   417 proof -
   418   interpret Mf: prob_space "density M f" by fact
   419   interpret Mf: information_space "density M f" b by default fact
   420   have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
   421     using f g ac by (subst density_density_divide) simp_all
   422 
   423   have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
   424   proof (rule Mf.KL_nonneg)
   425     show "prob_space ?DD" unfolding eq by fact
   426     from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
   427       by auto
   428     show "AE x in density M f. 0 \<le> g x / f x"
   429       using f g by (auto simp: AE_density divide_nonneg_nonneg)
   430     show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
   431       using `1 < b` f g ac
   432       by (subst integral_density)
   433          (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)
   434   qed
   435   also have "\<dots> = KL_divergence b (density M f) (density M g)"
   436     using f g ac by (subst density_density_divide) simp_all
   437   finally show ?thesis .
   438 qed
   439 
   440 subsection {* Mutual Information *}
   441 
   442 definition (in prob_space)
   443   "mutual_information b S T X Y =
   444     KL_divergence b (distr M S X \<Otimes>\<^isub>M distr M T Y) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
   445 
   446 lemma (in information_space) mutual_information_indep_vars:
   447   fixes S T X Y
   448   defines "P \<equiv> distr M S X \<Otimes>\<^isub>M distr M T Y"
   449   defines "Q \<equiv> distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   450   shows "indep_var S X T Y \<longleftrightarrow>
   451     (random_variable S X \<and> random_variable T Y \<and>
   452       absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>
   453       mutual_information b S T X Y = 0)"
   454   unfolding indep_var_distribution_eq
   455 proof safe
   456   assume rv: "random_variable S X" "random_variable T Y"
   457 
   458   interpret X: prob_space "distr M S X"
   459     by (rule prob_space_distr) fact
   460   interpret Y: prob_space "distr M T Y"
   461     by (rule prob_space_distr) fact
   462   interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
   463   interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
   464 
   465   interpret Q: prob_space Q unfolding Q_def
   466     by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
   467 
   468   { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   469     then have [simp]: "Q = P"  unfolding Q_def P_def by simp
   470 
   471     show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)
   472     then have ed: "entropy_density b P Q \<in> borel_measurable P"
   473       by (rule P.measurable_entropy_density) simp
   474 
   475     have "AE x in P. 1 = RN_deriv P Q x"
   476     proof (rule P.RN_deriv_unique)
   477       show "density P (\<lambda>x. 1) = Q"
   478         unfolding `Q = P` by (intro measure_eqI) (auto simp: emeasure_density)
   479     qed auto
   480     then have ae_0: "AE x in P. entropy_density b P Q x = 0"
   481       by eventually_elim (auto simp: entropy_density_def)
   482     then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0)"
   483       using ed unfolding `Q = P` by (intro integrable_cong_AE) auto
   484     then show "integrable Q (entropy_density b P Q)" by simp
   485 
   486     show "mutual_information b S T X Y = 0"
   487       unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] `Q = P`
   488       using ae_0 by (simp cong: integral_cong_AE) }
   489 
   490   { assume ac: "absolutely_continuous P Q"
   491     assume int: "integrable Q (entropy_density b P Q)"
   492     assume I_eq_0: "mutual_information b S T X Y = 0"
   493 
   494     have eq: "Q = P"
   495     proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])
   496       show "prob_space Q" by unfold_locales
   497       show "absolutely_continuous P Q" by fact
   498       show "integrable Q (entropy_density b P Q)" by fact
   499       show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)
   500       show "KL_divergence b P Q = 0"
   501         using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)
   502     qed
   503     then show "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   504       unfolding P_def Q_def .. }
   505 qed
   506 
   507 abbreviation (in information_space)
   508   mutual_information_Pow ("\<I>'(_ ; _')") where
   509   "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) X Y"
   510 
   511 lemma (in information_space)
   512   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   513   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   514   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
   515   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   516   defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
   517   shows mutual_information_distr: "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
   518     and mutual_information_nonneg: "integrable (S \<Otimes>\<^isub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"
   519 proof -
   520   have X: "random_variable S X"
   521     using Px by (auto simp: distributed_def)
   522   have Y: "random_variable T Y"
   523     using Py by (auto simp: distributed_def)
   524   interpret S: sigma_finite_measure S by fact
   525   interpret T: sigma_finite_measure T by fact
   526   interpret ST: pair_sigma_finite S T ..
   527   interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
   528   interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
   529   interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
   530   let ?P = "S \<Otimes>\<^isub>M T"
   531   let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
   532 
   533   { fix A assume "A \<in> sets S"
   534     with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
   535       by (auto simp: emeasure_distr measurable_Pair measurable_space
   536                intro!: arg_cong[where f="emeasure M"]) }
   537   note marginal_eq1 = this
   538   { fix A assume "A \<in> sets T"
   539     with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
   540       by (auto simp: emeasure_distr measurable_Pair measurable_space
   541                intro!: arg_cong[where f="emeasure M"]) }
   542   note marginal_eq2 = this
   543 
   544   have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
   545     by auto
   546 
   547   have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
   548     unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
   549   proof (subst pair_measure_density)
   550     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
   551       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
   552       using Px Py by (auto simp: distributed_def)
   553     show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
   554     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   555   qed (fact | simp)+
   556   
   557   have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
   558     unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
   559 
   560   from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
   561     by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
   562   have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
   563   proof (rule ST.AE_pair_measure)
   564     show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
   565       using f by auto
   566     show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
   567       using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
   568   qed
   569 
   570   have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
   571     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   572   moreover
   573   have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
   574     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   575   ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   576     by eventually_elim auto
   577 
   578   show "?M = ?R"
   579     unfolding M f_def
   580     using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
   581     by (rule ST.KL_density_density)
   582 
   583   assume int: "integrable (S \<Otimes>\<^isub>M T) f"
   584   show "0 \<le> ?M" unfolding M
   585   proof (rule ST.KL_density_density_nonneg
   586     [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
   587     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
   588       unfolding distributed_distr_eq_density[OF Pxy, symmetric]
   589       using distributed_measurable[OF Pxy] by (rule prob_space_distr)
   590     show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
   591       unfolding distr_eq[symmetric] by unfold_locales
   592   qed
   593 qed
   594 
   595 lemma (in information_space)
   596   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   597   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   598   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
   599   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   600   assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"
   601   shows mutual_information_eq_0: "mutual_information b S T X Y = 0"
   602 proof -
   603   interpret S: sigma_finite_measure S by fact
   604   interpret T: sigma_finite_measure T by fact
   605   interpret ST: pair_sigma_finite S T ..
   606 
   607   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
   608     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
   609   moreover
   610   have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
   611     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
   612   moreover 
   613   have "AE x in S \<Otimes>\<^isub>M T. Pxy x = Px (fst x) * Py (snd x)"
   614     using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]
   615     by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')
   616   ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"
   617     by eventually_elim simp
   618   then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
   619     by (rule integral_cong_AE)
   620   then show ?thesis
   621     by (subst mutual_information_distr[OF assms(1-5)]) simp
   622 qed
   623 
   624 lemma (in information_space) mutual_information_simple_distributed:
   625   assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"
   626   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
   627   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)))"
   628 proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
   629   note fin = simple_distributed_joint_finite[OF XY, simp]
   630   show "sigma_finite_measure (count_space (X ` space M))"
   631     by (simp add: sigma_finite_measure_count_space_finite)
   632   show "sigma_finite_measure (count_space (Y ` space M))"
   633     by (simp add: sigma_finite_measure_count_space_finite)
   634   let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
   635   let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"
   636   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)"
   637     by auto
   638   with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M))) =
   639     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
   640     by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'
   641              intro!: setsum_cong)
   642 qed
   643 
   644 lemma (in information_space)
   645   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   646   assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"
   647   assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
   648   assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"
   649   shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"
   650 proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
   651   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))) =
   652     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
   653     by (intro setsum_cong) (auto simp: ae)
   654   then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
   655     Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
   656 qed
   657 
   658 subsection {* Entropy *}
   659 
   660 definition (in prob_space) entropy :: "real \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real" where
   661   "entropy b S X = - KL_divergence b S (distr M S X)"
   662 
   663 abbreviation (in information_space)
   664   entropy_Pow ("\<H>'(_')") where
   665   "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
   666 
   667 lemma (in information_space) entropy_distr:
   668   fixes X :: "'a \<Rightarrow> 'b"
   669   assumes X: "distributed M MX X f"
   670   shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"
   671   unfolding entropy_def KL_divergence_def entropy_density_def comp_def
   672 proof (subst integral_cong_AE)
   673   note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
   674   interpret X: prob_space "distr M MX X"
   675     using D(1) by (rule prob_space_distr)
   676 
   677   have sf: "sigma_finite_measure (distr M MX X)" by default
   678   have ae: "AE x in MX. f x = RN_deriv MX (density MX f) x"
   679     using D
   680     by (intro RN_deriv_unique_sigma_finite)
   681        (auto intro: divide_nonneg_nonneg measure_nonneg
   682              simp: distributed_distr_eq_density[symmetric, OF X] sf)
   683   show "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
   684     log b (f x)"
   685     unfolding distributed_distr_eq_density[OF X]
   686     apply (subst AE_density)
   687     using D apply simp
   688     using ae apply eventually_elim
   689     apply (subst (asm) eq_commute)
   690     apply auto
   691     done
   692   show "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
   693     unfolding distributed_distr_eq_density[OF X]
   694     using D
   695     by (subst integral_density)
   696        (auto simp: borel_measurable_ereal_iff)
   697 qed 
   698 
   699 lemma (in prob_space) distributed_imp_emeasure_nonzero:
   700   assumes X: "distributed M MX X Px"
   701   shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0"
   702 proof
   703   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   704   interpret X: prob_space "distr M MX X"
   705     using distributed_measurable[OF X] by (rule prob_space_distr)
   706 
   707   assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0"
   708   with Px have "AE x in MX. Px x = 0"
   709     by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ereal_iff)
   710   moreover
   711   from X.emeasure_space_1 have "(\<integral>\<^isup>+x. Px x \<partial>MX) = 1"
   712     unfolding distributed_distr_eq_density[OF X] using Px
   713     by (subst (asm) emeasure_density)
   714        (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
   715   ultimately show False
   716     by (simp add: positive_integral_cong_AE)
   717 qed
   718 
   719 lemma (in information_space) entropy_le:
   720   fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
   721   assumes X: "distributed M MX X Px"
   722   and fin: "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> \<infinity>"
   723   and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
   724   shows "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
   725 proof -
   726   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   727   interpret X: prob_space "distr M MX X"
   728     using distributed_measurable[OF X] by (rule prob_space_distr)
   729 
   730   have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
   731     - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
   732     using Px fin
   733     by (subst integral_indicator) (auto simp: measure_def borel_measurable_ereal_iff)
   734   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)"
   735     unfolding distributed_distr_eq_density[OF X] using Px
   736     apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
   737     by (subst integral_density) (auto simp: borel_measurable_ereal_iff intro!: integral_cong)
   738   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   739   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
   740     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
   741       unfolding distributed_distr_eq_density[OF X]
   742       using Px by (auto simp: AE_density)
   743     have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
   744       by (auto simp: one_ereal_def)
   745     have "(\<integral>\<^isup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^isup>+ x. 0 \<partial>MX)"
   746       by (intro positive_integral_cong) (auto split: split_max)
   747     then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
   748       unfolding distributed_distr_eq_density[OF X] using Px
   749       by (auto simp: positive_integral_density integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
   750               cong: positive_integral_cong)
   751     have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
   752       integrable MX (\<lambda>x. - Px x * log b (Px x))"
   753       using Px
   754       by (intro integrable_cong_AE)
   755          (auto simp: borel_measurable_ereal_iff log_divide_eq
   756                   intro!: measurable_If)
   757     then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
   758       unfolding distributed_distr_eq_density[OF X]
   759       using Px int
   760       by (subst integral_density) (auto simp: borel_measurable_ereal_iff)
   761   qed (auto simp: minus_log_convex[OF b_gt_1])
   762   also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
   763     unfolding distributed_distr_eq_density[OF X] using Px
   764     by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
   765   also have "\<dots> = - entropy b MX X"
   766     unfolding distributed_distr_eq_density[OF X] using Px
   767     by (subst entropy_distr[OF X]) (auto simp: borel_measurable_ereal_iff integral_density)
   768   finally show ?thesis
   769     by simp
   770 qed
   771 
   772 lemma (in information_space) entropy_le_space:
   773   fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
   774   assumes X: "distributed M MX X Px"
   775   and fin: "finite_measure MX"
   776   and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
   777   shows "entropy b MX X \<le> log b (measure MX (space MX))"
   778 proof -
   779   note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
   780   interpret finite_measure MX by fact
   781   have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
   782     using int X by (intro entropy_le) auto
   783   also have "\<dots> \<le> log b (measure MX (space MX))"
   784     using Px distributed_imp_emeasure_nonzero[OF X]
   785     by (intro log_le)
   786        (auto intro!: borel_measurable_ereal_iff finite_measure_mono b_gt_1
   787                      less_le[THEN iffD2] measure_nonneg simp: emeasure_eq_measure)
   788   finally show ?thesis .
   789 qed
   790 
   791 lemma (in prob_space) uniform_distributed_params:
   792   assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
   793   shows "A \<in> sets MX" "measure MX A \<noteq> 0"
   794 proof -
   795   interpret X: prob_space "distr M MX X"
   796     using distributed_measurable[OF X] by (rule prob_space_distr)
   797 
   798   show "measure MX A \<noteq> 0"
   799   proof
   800     assume "measure MX A = 0"
   801     with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
   802     show False
   803       by (simp add: emeasure_density zero_ereal_def[symmetric])
   804   qed
   805   with measure_notin_sets[of A MX] show "A \<in> sets MX"
   806     by blast
   807 qed
   808 
   809 lemma (in information_space) entropy_uniform:
   810   assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
   811   shows "entropy b MX X = log b (measure MX A)"
   812 proof (subst entropy_distr[OF X])
   813   have [simp]: "emeasure MX A \<noteq> \<infinity>"
   814     using uniform_distributed_params[OF X] by (auto simp add: measure_def)
   815   have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   816     (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
   817     using measure_nonneg[of MX A] uniform_distributed_params[OF X]
   818     by (auto intro!: integral_cong split: split_indicator simp: log_divide_eq)
   819   show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   820     log b (measure MX A)"
   821     unfolding eq using uniform_distributed_params[OF X]
   822     by (subst lebesgue_integral_cmult) (auto simp: measure_def)
   823 qed
   824 
   825 lemma (in information_space) entropy_simple_distributed:
   826   "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
   827   by (subst entropy_distr[OF simple_distributed])
   828      (auto simp add: lebesgue_integral_count_space_finite)
   829 
   830 lemma (in information_space) entropy_le_card_not_0:
   831   assumes X: "simple_distributed M X f"
   832   shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"
   833 proof -
   834   have "\<H>(X) = (\<Sum>x\<in>X`space M. f x * log b (1 / f x))"
   835     unfolding entropy_simple_distributed[OF X] setsum_negf[symmetric]
   836     using X by (auto dest: simple_distributed_nonneg intro!: setsum_cong simp: log_simps less_le)
   837   also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. f x * (1 / f x))"
   838     using not_empty b_gt_1 `simple_distributed M X f`
   839     by (intro log_setsum') (auto simp: simple_distributed_nonneg simple_distributed_setsum_space)
   840   also have "\<dots> = log b (\<Sum>x\<in>X`space M. if f x \<noteq> 0 then 1 else 0)"
   841     by (intro arg_cong[where f="\<lambda>X. log b X"] setsum_cong) auto
   842   finally show ?thesis
   843     using `simple_distributed M X f` by (auto simp: setsum_cases real_eq_of_nat)
   844 qed
   845 
   846 lemma (in information_space) entropy_le_card:
   847   assumes "simple_distributed M X f"
   848   shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
   849 proof cases
   850   assume "X ` space M \<inter> {x. f x \<noteq> 0} = {}"
   851   then have "\<And>x. x\<in>X`space M \<Longrightarrow> f x = 0" by auto
   852   moreover
   853   have "0 < card (X`space M)"
   854     using `simple_distributed M X f` not_empty by (auto simp: card_gt_0_iff)
   855   then have "log b 1 \<le> log b (real (card (X`space M)))"
   856     using b_gt_1 by (intro log_le) auto
   857   ultimately show ?thesis using assms by (simp add: entropy_simple_distributed)
   858 next
   859   assume False: "X ` space M \<inter> {x. f x \<noteq> 0} \<noteq> {}"
   860   have "card (X ` space M \<inter> {x. f x \<noteq> 0}) \<le> card (X ` space M)"
   861     (is "?A \<le> ?B") using assms not_empty
   862     by (auto intro!: card_mono simp: simple_function_def simple_distributed_def)
   863   note entropy_le_card_not_0[OF assms]
   864   also have "log b (real ?A) \<le> log b (real ?B)"
   865     using b_gt_1 False not_empty `?A \<le> ?B` assms
   866     by (auto intro!: log_le simp: card_gt_0_iff simp: simple_distributed_def)
   867   finally show ?thesis .
   868 qed
   869 
   870 subsection {* Conditional Mutual Information *}
   871 
   872 definition (in prob_space)
   873   "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
   874     mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x)) -
   875     mutual_information b MX MZ X Z"
   876 
   877 abbreviation (in information_space)
   878   conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
   879   "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
   880     (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
   881 
   882 lemma (in information_space) conditional_mutual_information_generic_eq:
   883   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
   884   assumes Px: "distributed M S X Px"
   885   assumes Pz: "distributed M P Z Pz"
   886   assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
   887   assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
   888   assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   889   assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
   890   assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
   891   shows "conditional_mutual_information b S T P X Y Z
   892     = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   893 proof -
   894   interpret S: sigma_finite_measure S by fact
   895   interpret T: sigma_finite_measure T by fact
   896   interpret P: sigma_finite_measure P by fact
   897   interpret TP: pair_sigma_finite T P ..
   898   interpret SP: pair_sigma_finite S P ..
   899   interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
   900   interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
   901   have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
   902   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
   903   have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
   904     using Pyz by (simp add: distributed_measurable)
   905 
   906   have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
   907     using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
   908 
   909   { fix f g h M
   910     assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
   911     from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
   912          measurable_comp[OF f Px[THEN distributed_real_measurable]]
   913          measurable_comp[OF g Pz[THEN distributed_real_measurable]]
   914     have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
   915       by (simp add: comp_def b_gt_1) }
   916   note borel_log = this
   917 
   918   have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
   919     by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
   920   
   921   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
   922     distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
   923     by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
   924 
   925   have "mutual_information b S P X Z =
   926     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
   927     by (rule mutual_information_distr[OF S P Px Pz Pxz])
   928   also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
   929     using b_gt_1 Pxz Px Pz
   930     by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
   931        (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
   932              dest!: distributed_real_measurable)
   933   finally have mi_eq:
   934     "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   935   
   936   have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
   937     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   938   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   939     by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
   940   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
   941     by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
   942   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
   943     by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
   944   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
   945     using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
   946   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
   947     using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
   948   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
   949     using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   950   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
   951     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
   952     using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
   953     using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
   954     by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
   955   moreover note Pxyz[THEN distributed_real_AE]
   956   ultimately have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
   957     Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
   958     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
   959     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
   960   proof eventually_elim
   961     case (goal1 x)
   962     show ?case
   963     proof cases
   964       assume "Pxyz x \<noteq> 0"
   965       with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
   966         by auto
   967       then show ?thesis
   968         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
   969     qed simp
   970   qed
   971   with I1 I2 show ?thesis
   972     unfolding conditional_mutual_information_def
   973     apply (subst mi_eq)
   974     apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
   975     apply (subst integral_diff(2)[symmetric])
   976     apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
   977     done
   978 qed
   979 
   980 lemma (in information_space) conditional_mutual_information_eq:
   981   assumes Pz: "simple_distributed M Z Pz"
   982   assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
   983   assumes Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"
   984   assumes Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   985   shows "\<I>(X ; Y | Z) =
   986    (\<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))))"
   987 proof (subst conditional_mutual_information_generic_eq[OF _ _ _ _
   988     simple_distributed[OF Pz] simple_distributed_joint[OF Pyz] simple_distributed_joint[OF Pxz]
   989     simple_distributed_joint2[OF Pxyz]])
   990   note simple_distributed_joint2_finite[OF Pxyz, simp]
   991   show "sigma_finite_measure (count_space (X ` space M))"
   992     by (simp add: sigma_finite_measure_count_space_finite)
   993   show "sigma_finite_measure (count_space (Y ` space M))"
   994     by (simp add: sigma_finite_measure_count_space_finite)
   995   show "sigma_finite_measure (count_space (Z ` space M))"
   996     by (simp add: sigma_finite_measure_count_space_finite)
   997   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =
   998       count_space (X`space M \<times> Y`space M \<times> Z`space M)"
   999     (is "?P = ?C")
  1000     by (simp add: pair_measure_count_space)
  1001 
  1002   let ?Px = "\<lambda>x. measure M (X -` {x} \<inter> space M)"
  1003   have "(\<lambda>x. (X x, Z x)) \<in> measurable M (count_space (X ` space M) \<Otimes>\<^isub>M count_space (Z ` space M))"
  1004     using simple_distributed_joint[OF Pxz] by (rule distributed_measurable)
  1005   from measurable_comp[OF this measurable_fst]
  1006   have "random_variable (count_space (X ` space M)) X"
  1007     by (simp add: comp_def)
  1008   then have "simple_function M X"    
  1009     unfolding simple_function_def by auto
  1010   then have "simple_distributed M X ?Px"
  1011     by (rule simple_distributedI) auto
  1012   then show "distributed M (count_space (X ` space M)) X ?Px"
  1013     by (rule simple_distributed)
  1014 
  1015   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then Pxyz x else 0)"
  1016   let ?g = "(\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x)) ` space M then Pyz x else 0)"
  1017   let ?h = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x)) ` space M then Pxz x else 0)"
  1018   show
  1019       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?f (x, y, z) / (?Px x * ?g (y, z))))"
  1020       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?h (x, z) / (?Px x * Pz z)))"
  1021     by (auto intro!: integrable_count_space simp: pair_measure_count_space)
  1022   let ?i = "\<lambda>x y z. ?f (x, y, z) * log b (?f (x, y, z) / (?h (x, z) * (?g (y, z) / Pz z)))"
  1023   let ?j = "\<lambda>x y z. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z)))"
  1024   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)"
  1025     by (auto intro!: ext)
  1026   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)"
  1027     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta')
  1028 qed
  1029 
  1030 lemma (in information_space) conditional_mutual_information_nonneg:
  1031   assumes X: "simple_function M X" and Y: "simple_function M Y" and Z: "simple_function M Z"
  1032   shows "0 \<le> \<I>(X ; Y | Z)"
  1033 proof -
  1034   def Pz \<equiv> "\<lambda>x. if x \<in> Z`space M then measure M (Z -` {x} \<inter> space M) else 0"
  1035   def Pxz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x))`space M then measure M ((\<lambda>x. (X x, Z x)) -` {x} \<inter> space M) else 0"
  1036   def Pyz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x))`space M then measure M ((\<lambda>x. (Y x, Z x)) -` {x} \<inter> space M) else 0"
  1037   def Pxyz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then measure M ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M) else 0"
  1038   let ?M = "X`space M \<times> Y`space M \<times> Z`space M"
  1039 
  1040   note XZ = simple_function_Pair[OF X Z]
  1041   note YZ = simple_function_Pair[OF Y Z]
  1042   note XYZ = simple_function_Pair[OF X simple_function_Pair[OF Y Z]]
  1043   have Pz: "simple_distributed M Z Pz"
  1044     using Z by (rule simple_distributedI) (auto simp: Pz_def)
  1045   have Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"
  1046     using XZ by (rule simple_distributedI) (auto simp: Pxz_def)
  1047   have Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
  1048     using YZ by (rule simple_distributedI) (auto simp: Pyz_def)
  1049   have Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"
  1050     using XYZ by (rule simple_distributedI) (auto simp: Pxyz_def)
  1051 
  1052   { fix z assume z: "z \<in> Z ` space M" then have "(\<Sum>x\<in>X ` space M. Pxz (x, z)) = Pz z"
  1053       using distributed_marginal_eq_joint_simple[OF X Pz Pxz z]
  1054       by (auto intro!: setsum_cong simp: Pxz_def) }
  1055   note marginal1 = this
  1056 
  1057   { fix z assume z: "z \<in> Z ` space M" then have "(\<Sum>y\<in>Y ` space M. Pyz (y, z)) = Pz z"
  1058       using distributed_marginal_eq_joint_simple[OF Y Pz Pyz z]
  1059       by (auto intro!: setsum_cong simp: Pyz_def) }
  1060   note marginal2 = this
  1061 
  1062   have "- \<I>(X ; Y | Z) = - (\<Sum>(x, y, z) \<in> ?M. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
  1063     unfolding conditional_mutual_information_eq[OF Pz Pyz Pxz Pxyz]
  1064     using X Y Z by (auto intro!: setsum_mono_zero_left simp: Pxyz_def simple_functionD)
  1065   also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. Pxz (x, z) * (Pyz (y,z) / Pz z))"
  1066     unfolding split_beta'
  1067   proof (rule log_setsum_divide)
  1068     show "?M \<noteq> {}" using not_empty by simp
  1069     show "1 < b" using b_gt_1 .
  1070 
  1071     show "finite ?M" using X Y Z by (auto simp: simple_functionD)
  1072 
  1073     then show "(\<Sum>x\<in>?M. Pxyz (fst x, fst (snd x), snd (snd x))) = 1"
  1074       apply (subst Pxyz[THEN simple_distributed_setsum_space, symmetric])
  1075       apply simp
  1076       apply (intro setsum_mono_zero_right)
  1077       apply (auto simp: Pxyz_def)
  1078       done
  1079     let ?N = "(\<lambda>x. (X x, Y x, Z x)) ` space M"
  1080     fix x assume x: "x \<in> ?M"
  1081     let ?Q = "Pxyz (fst x, fst (snd x), snd (snd x))"
  1082     let ?P = "Pxz (fst x, snd (snd x)) * (Pyz (fst (snd x), snd (snd x)) / Pz (snd (snd x)))"
  1083     from x show "0 \<le> ?Q" "0 \<le> ?P"
  1084       using Pxyz[THEN simple_distributed, THEN distributed_real_AE]
  1085       using Pxz[THEN simple_distributed, THEN distributed_real_AE]
  1086       using Pyz[THEN simple_distributed, THEN distributed_real_AE]
  1087       using Pz[THEN simple_distributed, THEN distributed_real_AE]
  1088       by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg simp: AE_count_space Pxyz_def Pxz_def Pyz_def Pz_def)
  1089     moreover assume "0 < ?Q"
  1090     moreover have "AE x in count_space ?N. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1091       by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz[THEN simple_distributed] Pz[THEN simple_distributed]]) (auto intro: measurable_snd')
  1092     then have "\<And>x. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1093       by (auto simp: Pz_def Pxyz_def AE_count_space)
  1094     moreover have "AE x in count_space ?N. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1095       by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz[THEN simple_distributed] Pxz[THEN simple_distributed]]) (auto intro: measurable_Pair measurable_snd')
  1096     then have "\<And>x. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
  1097       by (auto simp: Pz_def Pxyz_def AE_count_space)
  1098     moreover have "AE x in count_space ?N. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
  1099       by (intro subdensity_real[of snd, OF _ Pxyz[THEN simple_distributed] Pyz[THEN simple_distributed]]) (auto intro: measurable_Pair)
  1100     then have "\<And>x. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
  1101       by (auto simp: Pz_def Pxyz_def AE_count_space)
  1102     ultimately show "0 < ?P" using x by (auto intro!: divide_pos_pos mult_pos_pos simp: less_le)
  1103   qed
  1104   also have "(\<Sum>(x, y, z) \<in> ?M. Pxz (x, z) * (Pyz (y,z) / Pz z)) = (\<Sum>z\<in>Z`space M. Pz z)"
  1105     apply (simp add: setsum_cartesian_product')
  1106     apply (subst setsum_commute)
  1107     apply (subst (2) setsum_commute)
  1108     apply (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric] marginal1 marginal2
  1109           intro!: setsum_cong)
  1110     done
  1111   also have "log b (\<Sum>z\<in>Z`space M. Pz z) = 0"
  1112     using Pz[THEN simple_distributed_setsum_space] by simp
  1113   finally show ?thesis by simp
  1114 qed
  1115 
  1116 subsection {* Conditional Entropy *}
  1117 
  1118 definition (in prob_space)
  1119   "conditional_entropy b S T X Y = entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) - entropy b T Y"
  1120 
  1121 abbreviation (in information_space)
  1122   conditional_entropy_Pow ("\<H>'(_ | _')") where
  1123   "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
  1124 
  1125 lemma (in information_space) conditional_entropy_generic_eq:
  1126   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
  1127   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1128   assumes Px: "distributed M S X Px"
  1129   assumes Py: "distributed M T Y Py"
  1130   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1131   assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
  1132   assumes I2: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
  1133   shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
  1134 proof -
  1135   interpret S: sigma_finite_measure S by fact
  1136   interpret T: sigma_finite_measure T by fact
  1137   interpret ST: pair_sigma_finite S T ..
  1138   have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
  1139 
  1140   interpret Pxy: prob_space "density (S \<Otimes>\<^isub>M T) Pxy"
  1141     unfolding Pxy[THEN distributed_distr_eq_density, symmetric]
  1142     using Pxy[THEN distributed_measurable] by (rule prob_space_distr)
  1143 
  1144   from Py Pxy have distr_eq: "distr M T Y =
  1145     distr (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) T snd"
  1146     by (subst distr_distr[OF measurable_snd]) (auto dest: distributed_measurable simp: comp_def)
  1147 
  1148   have "entropy b T Y = - (\<integral>y. Py y * log b (Py y) \<partial>T)"
  1149     by (rule entropy_distr[OF Py])
  1150   also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))"
  1151     using b_gt_1 Py[THEN distributed_real_measurable]
  1152     by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
  1153   finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
  1154   
  1155   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
  1156     by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
  1157   moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1158     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
  1159   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
  1160     using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
  1161   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
  1162     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1163   moreover note Pxy[THEN distributed_real_AE]
  1164   ultimately have pos: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Px (fst x) \<and> 0 \<le> Py (snd x) \<and>
  1165     (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Px (fst x) \<and> 0 < Py (snd x)))"
  1166     by eventually_elim auto
  1167 
  1168   from pos have "AE x in S \<Otimes>\<^isub>M T.
  1169      Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
  1170     by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
  1171   with I1 I2 show ?thesis
  1172     unfolding conditional_entropy_def
  1173     apply (subst e_eq)
  1174     apply (subst entropy_distr[OF Pxy])
  1175     unfolding minus_diff_minus
  1176     apply (subst integral_diff(2)[symmetric])
  1177     apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
  1178     done
  1179 qed
  1180 
  1181 lemma (in information_space) conditional_entropy_eq:
  1182   assumes Y: "simple_distributed M Y Py" and X: "simple_function M X"
  1183   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
  1184     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))"
  1185 proof (subst conditional_entropy_generic_eq[OF _ _
  1186   simple_distributed[OF simple_distributedI[OF X refl]] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
  1187   have [simp]: "finite (X`space M)" using X by (simp add: simple_function_def)
  1188   note Y[THEN simple_distributed_finite, simp]
  1189   show "sigma_finite_measure (count_space (X ` space M))"
  1190     by (simp add: sigma_finite_measure_count_space_finite)
  1191   show "sigma_finite_measure (count_space (Y ` space M))"
  1192     by (simp add: sigma_finite_measure_count_space_finite)
  1193   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
  1194   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
  1195     (is "?P = ?C")
  1196     using X Y by (simp add: simple_distributed_finite pair_measure_count_space)
  1197   with X Y show
  1198       "integrable ?P (\<lambda>x. ?f x * log b (?f x))"
  1199       "integrable ?P (\<lambda>x. ?f x * log b (Py (snd x)))"
  1200     by (auto intro!: integrable_count_space simp: simple_distributed_finite)
  1201   have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
  1202     (\<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)"
  1203     by auto
  1204   from X Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
  1205     - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
  1206     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
  1207 qed
  1208 
  1209 lemma (in information_space) conditional_mutual_information_eq_conditional_entropy:
  1210   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1211   shows "\<I>(X ; X | Y) = \<H>(X | Y)"
  1212 proof -
  1213   def Py \<equiv> "\<lambda>x. if x \<in> Y`space M then measure M (Y -` {x} \<inter> space M) else 0"
  1214   def Pxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M) else 0"
  1215   def Pxxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, X x, Y x))`space M then measure M ((\<lambda>x. (X x, X x, Y x)) -` {x} \<inter> space M) else 0"
  1216   let ?M = "X`space M \<times> X`space M \<times> Y`space M"
  1217 
  1218   note XY = simple_function_Pair[OF X Y]
  1219   note XXY = simple_function_Pair[OF X XY]
  1220   have Py: "simple_distributed M Y Py"
  1221     using Y by (rule simple_distributedI) (auto simp: Py_def)
  1222   have Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
  1223     using XY by (rule simple_distributedI) (auto simp: Pxy_def)
  1224   have Pxxy: "simple_distributed M (\<lambda>x. (X x, X x, Y x)) Pxxy"
  1225     using XXY by (rule simple_distributedI) (auto simp: Pxxy_def)
  1226   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"
  1227     by auto
  1228   have inj: "\<And>A. inj_on (\<lambda>(x, y). (x, x, y)) A"
  1229     by (auto simp: inj_on_def)
  1230   have Pxxy_eq: "\<And>x y. Pxxy (x, x, y) = Pxy (x, y)"
  1231     by (auto simp: Pxxy_def Pxy_def intro!: arg_cong[where f=prob])
  1232   have "AE x in count_space ((\<lambda>x. (X x, Y x))`space M). Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1233     by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
  1234   then show ?thesis
  1235     apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
  1236     apply (subst conditional_entropy_eq[OF Py X Pxy])
  1237     apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
  1238                 log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
  1239     using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
  1240     apply (auto simp add: not_le[symmetric] AE_count_space)
  1241     done
  1242 qed
  1243 
  1244 lemma (in information_space) conditional_entropy_nonneg:
  1245   assumes X: "simple_function M X" and Y: "simple_function M Y" shows "0 \<le> \<H>(X | Y)"
  1246   using conditional_mutual_information_eq_conditional_entropy[OF X Y] conditional_mutual_information_nonneg[OF X X Y]
  1247   by simp
  1248 
  1249 subsection {* Equalities *}
  1250 
  1251 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy_distr:
  1252   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
  1253   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  1254   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
  1255   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
  1256   assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
  1257   assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
  1258   assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
  1259   shows  "mutual_information b S T X Y = entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
  1260 proof -
  1261   have X: "entropy b S X = - (\<integral>x. Pxy x * log b (Px (fst x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1262     using b_gt_1 Px[THEN distributed_real_measurable]
  1263     apply (subst entropy_distr[OF Px])
  1264     apply (subst distributed_transform_integral[OF Pxy Px, where T=fst])
  1265     apply (auto intro!: integral_cong)
  1266     done
  1267 
  1268   have Y: "entropy b T Y = - (\<integral>x. Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
  1269     using b_gt_1 Py[THEN distributed_real_measurable]
  1270     apply (subst entropy_distr[OF Py])
  1271     apply (subst distributed_transform_integral[OF Pxy Py, where T=snd])
  1272     apply (auto intro!: integral_cong)
  1273     done
  1274 
  1275   interpret S: sigma_finite_measure S by fact
  1276   interpret T: sigma_finite_measure T by fact
  1277   interpret ST: pair_sigma_finite S T ..
  1278   have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
  1279 
  1280   have XY: "entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^isub>M T))"
  1281     by (subst entropy_distr[OF Pxy]) (auto intro!: integral_cong)
  1282   
  1283   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
  1284     by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
  1285   moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
  1286     by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
  1287   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
  1288     using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
  1289   moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
  1290     using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
  1291   moreover note Pxy[THEN distributed_real_AE]
  1292   ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) = 
  1293     Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
  1294     (is "AE x in _. ?f x = ?g x")
  1295   proof eventually_elim
  1296     case (goal1 x)
  1297     show ?case
  1298     proof cases
  1299       assume "Pxy x \<noteq> 0"
  1300       with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
  1301         by auto
  1302       then show ?thesis
  1303         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
  1304     qed simp
  1305   qed
  1306 
  1307   have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?f"
  1308     unfolding X Y XY
  1309     apply (subst integral_diff)
  1310     apply (intro integral_diff Ixy Ix Iy)+
  1311     apply (subst integral_diff)
  1312     apply (intro integral_diff Ixy Ix Iy)+
  1313     apply (simp add: field_simps)
  1314     done
  1315   also have "\<dots> = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?g"
  1316     using `AE x in _. ?f x = ?g x` by (rule integral_cong_AE)
  1317   also have "\<dots> = mutual_information b S T X Y"
  1318     by (rule mutual_information_distr[OF S T Px Py Pxy, symmetric])
  1319   finally show ?thesis ..
  1320 qed
  1321 
  1322 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
  1323   assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
  1324   shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"
  1325 proof -
  1326   have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
  1327     using sf_X by (rule simple_distributedI) auto
  1328   have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
  1329     using sf_Y by (rule simple_distributedI) auto
  1330   have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
  1331     using sf_X sf_Y by (rule simple_function_Pair)
  1332   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))"
  1333     by (rule simple_distributedI) auto
  1334   from simple_distributed_joint_finite[OF this, simp]
  1335   have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
  1336     by (simp add: pair_measure_count_space)
  1337 
  1338   have "\<I>(X ; Y) = \<H>(X) + \<H>(Y) - entropy b (count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x))"
  1339     using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]
  1340     by (rule mutual_information_eq_entropy_conditional_entropy_distr) (auto simp: eq integrable_count_space)
  1341   then show ?thesis
  1342     unfolding conditional_entropy_def by simp
  1343 qed
  1344 
  1345 lemma (in information_space) mutual_information_nonneg_simple:
  1346   assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
  1347   shows  "0 \<le> \<I>(X ; Y)"
  1348 proof -
  1349   have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
  1350     using sf_X by (rule simple_distributedI) auto
  1351   have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
  1352     using sf_Y by (rule simple_distributedI) auto
  1353 
  1354   have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
  1355     using sf_X sf_Y by (rule simple_function_Pair)
  1356   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))"
  1357     by (rule simple_distributedI) auto
  1358 
  1359   from simple_distributed_joint_finite[OF this, simp]
  1360   have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
  1361     by (simp add: pair_measure_count_space)
  1362 
  1363   show ?thesis
  1364     by (rule mutual_information_nonneg[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
  1365        (simp_all add: eq integrable_count_space sigma_finite_measure_count_space_finite)
  1366 qed
  1367 
  1368 lemma (in information_space) conditional_entropy_less_eq_entropy:
  1369   assumes X: "simple_function M X" and Z: "simple_function M Z"
  1370   shows "\<H>(X | Z) \<le> \<H>(X)"
  1371 proof -
  1372   have "0 \<le> \<I>(X ; Z)" using X Z by (rule mutual_information_nonneg_simple)
  1373   also have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
  1374   finally show ?thesis by auto
  1375 qed
  1376 
  1377 lemma (in information_space) entropy_chain_rule:
  1378   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1379   shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
  1380 proof -
  1381   note XY = simple_distributedI[OF simple_function_Pair[OF X Y] refl]
  1382   note YX = simple_distributedI[OF simple_function_Pair[OF Y X] refl]
  1383   note simple_distributed_joint_finite[OF this, simp]
  1384   let ?f = "\<lambda>x. prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
  1385   let ?g = "\<lambda>x. prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M)"
  1386   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"
  1387   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))"
  1388     using XY by (rule entropy_simple_distributed)
  1389   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))"
  1390     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)"])
  1391   also have "\<dots> = - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` space M. ?h x * log b (?h x))"
  1392     by (auto intro!: setsum_cong)
  1393   also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
  1394     by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
  1395        (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
  1396              cong del: setsum_cong  intro!: setsum_mono_zero_left)
  1397   finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
  1398   then show ?thesis
  1399     unfolding conditional_entropy_def by simp
  1400 qed
  1401 
  1402 lemma (in information_space) entropy_partition:
  1403   assumes X: "simple_function M X"
  1404   shows "\<H>(X) = \<H>(f \<circ> X) + \<H>(X|f \<circ> X)"
  1405 proof -
  1406   note fX = simple_function_compose[OF X, of f]  
  1407   have eq: "(\<lambda>x. ((f \<circ> X) x, X x)) ` space M = (\<lambda>x. (f x, x)) ` X ` space M" by auto
  1408   have inj: "\<And>A. inj_on (\<lambda>x. (f x, x)) A"
  1409     by (auto simp: inj_on_def)
  1410   show ?thesis
  1411     apply (subst entropy_chain_rule[symmetric, OF fX X])
  1412     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]])
  1413     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
  1414     unfolding eq
  1415     apply (subst setsum_reindex[OF inj])
  1416     apply (auto intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
  1417     done
  1418 qed
  1419 
  1420 corollary (in information_space) entropy_data_processing:
  1421   assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
  1422 proof -
  1423   note fX = simple_function_compose[OF X, of f]
  1424   from X have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
  1425   then show "\<H>(f \<circ> X) \<le> \<H>(X)"
  1426     by (auto intro: conditional_entropy_nonneg[OF X fX])
  1427 qed
  1428 
  1429 corollary (in information_space) entropy_of_inj:
  1430   assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
  1431   shows "\<H>(f \<circ> X) = \<H>(X)"
  1432 proof (rule antisym)
  1433   show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
  1434 next
  1435   have sf: "simple_function M (f \<circ> X)"
  1436     using X by auto
  1437   have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
  1438     unfolding o_assoc
  1439     apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
  1440     apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\<lambda>x. prob (X -` {x} \<inter> space M)"])
  1441     apply (auto intro!: setsum_cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
  1442     done
  1443   also have "... \<le> \<H>(f \<circ> X)"
  1444     using entropy_data_processing[OF sf] .
  1445   finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
  1446 qed
  1447 
  1448 end