src/HOL/Probability/Information.thy
author hoelzl
Wed Dec 07 15:10:29 2011 +0100 (2011-12-07)
changeset 45777 c36637603821
parent 45712 852597248663
child 46731 5302e932d1e5
permissions -rw-r--r--
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
     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 \<nu> = log b \<circ> real \<circ> RN_deriv M \<nu>"
   176 
   177 definition
   178   "KL_divergence b M \<nu> = integral\<^isup>L (M\<lparr>measure := \<nu>\<rparr>) (entropy_density b M \<nu>)"
   179 
   180 lemma (in information_space) measurable_entropy_density:
   181   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
   182   assumes ac: "absolutely_continuous \<nu>"
   183   shows "entropy_density b M \<nu> \<in> borel_measurable M"
   184 proof -
   185   interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
   186   have "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by fact
   187   from RN_deriv[OF this ac] b_gt_1 show ?thesis
   188     unfolding entropy_density_def
   189     by (intro measurable_comp) auto
   190 qed
   191 
   192 lemma (in information_space) KL_gt_0:
   193   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
   194   assumes ac: "absolutely_continuous \<nu>"
   195   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
   196   assumes A: "A \<in> sets M" "\<nu> A \<noteq> \<mu> A"
   197   shows "0 < KL_divergence b M \<nu>"
   198 proof -
   199   interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
   200   have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
   201   have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
   202   note RN = RN_deriv[OF ms ac]
   203 
   204   from real_RN_deriv[OF fms ac] guess D . note D = this
   205   with absolutely_continuous_AE[OF ms] ac
   206   have D\<nu>: "AE x in M\<lparr>measure := \<nu>\<rparr>. RN_deriv M \<nu> x = ereal (D x)"
   207     by auto
   208 
   209   def f \<equiv> "\<lambda>x. if D x = 0 then 1 else 1 / D x"
   210   with D have f_borel: "f \<in> borel_measurable M"
   211     by (auto intro!: measurable_If)
   212 
   213   have "KL_divergence b M \<nu> = 1 / ln b * (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
   214     unfolding KL_divergence_def using int b_gt_1
   215     by (simp add: integral_cmult)
   216 
   217   { fix A assume "A \<in> sets M"
   218     with RN D have "\<nu>.\<mu> A = (\<integral>\<^isup>+ x. ereal (D x) * indicator A x \<partial>M)"
   219       by (auto intro!: positive_integral_cong_AE) }
   220   note D_density = this
   221 
   222   have ln_entropy: "(\<lambda>x. ln b * entropy_density b M \<nu> x) \<in> borel_measurable M"
   223     using measurable_entropy_density[OF ps ac] by auto
   224 
   225   have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x)"
   226     using int by auto
   227   moreover have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x) \<longleftrightarrow>
   228       integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
   229     using D D_density ln_entropy
   230     by (intro integral_translated_density) auto
   231   ultimately have M_int: "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
   232     by simp
   233 
   234   have D_neg: "(\<integral>\<^isup>+ x. ereal (- D x) \<partial>M) = 0"
   235     using D by (subst positive_integral_0_iff_AE) auto
   236 
   237   have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = \<nu> (space M)"
   238     using RN D by (auto intro!: positive_integral_cong_AE)
   239   then have D_pos: "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = 1"
   240     using \<nu>.measure_space_1 by simp
   241 
   242   have "integrable M D"
   243     using D_pos D_neg D by (auto simp: integrable_def)
   244 
   245   have "integral\<^isup>L M D = 1"
   246     using D_pos D_neg by (auto simp: lebesgue_integral_def)
   247 
   248   let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
   249   have [simp, intro]: "?D_set \<in> sets M"
   250     using D by (auto intro: sets_Collect)
   251 
   252   have "0 \<le> 1 - \<mu>' ?D_set"
   253     using prob_le_1 by (auto simp: field_simps)
   254   also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
   255     using `integrable M D` `integral\<^isup>L M D = 1`
   256     by (simp add: \<mu>'_def)
   257   also have "\<dots> < (\<integral> x. D x * (ln b * entropy_density b M \<nu> x) \<partial>M)"
   258   proof (rule integral_less_AE)
   259     show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
   260       using `integrable M D`
   261       by (intro integral_diff integral_indicator) auto
   262   next
   263     show "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"
   264       by fact
   265   next
   266     show "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
   267     proof
   268       assume eq_0: "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
   269       then have disj: "AE x. D x = 1 \<or> D x = 0"
   270         using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
   271 
   272       have "\<mu> {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
   273         using D(1) by auto
   274       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) * indicator {x\<in>space M. D x \<noteq> 0} x \<partial>M)"
   275         using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
   276       also have "\<dots> = \<nu> {x\<in>space M. D x \<noteq> 0}"
   277         using D(1) D_density by auto
   278       also have "\<dots> = \<nu> (space M)"
   279         using D_density D(1) by (auto intro!: positive_integral_cong simp: indicator_def)
   280       finally have "AE x. D x = 1"
   281         using D(1) \<nu>.measure_space_1 by (intro AE_I_eq_1) auto
   282       then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. ereal (D x) * indicator A x\<partial>M)"
   283         by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
   284       also have "\<dots> = \<nu> A"
   285         using `A \<in> sets M` D_density by simp
   286       finally show False using `A \<in> sets M` `\<nu> A \<noteq> \<mu> A` by simp
   287     qed
   288     show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
   289       using D(1) by (auto intro: sets_Collect)
   290 
   291     show "AE t. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
   292       D t - indicator ?D_set t \<noteq> D t * (ln b * entropy_density b M \<nu> t)"
   293       using D(2)
   294     proof (elim AE_mp, safe intro!: AE_I2)
   295       fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0"
   296         and RN: "RN_deriv M \<nu> t = ereal (D t)"
   297         and eq: "D t - indicator ?D_set t = D t * (ln b * entropy_density b M \<nu> t)"
   298 
   299       have "D t - 1 = D t - indicator ?D_set t"
   300         using Dt by simp
   301       also note eq
   302       also have "D t * (ln b * entropy_density b M \<nu> t) = - D t * ln (1 / D t)"
   303         using RN b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
   304         by (simp add: entropy_density_def log_def ln_div less_le)
   305       finally have "ln (1 / D t) = 1 / D t - 1"
   306         using `D t \<noteq> 0` by (auto simp: field_simps)
   307       from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
   308       show False by auto
   309     qed
   310 
   311     show "AE t. D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"
   312       using D(2)
   313     proof (elim AE_mp, intro AE_I2 impI)
   314       fix t assume "t \<in> space M" and RN: "RN_deriv M \<nu> t = ereal (D t)"
   315       show "D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"
   316       proof cases
   317         assume asm: "D t \<noteq> 0"
   318         then have "0 < D t" using `0 \<le> D t` by auto
   319         then have "0 < 1 / D t" by auto
   320         have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
   321           using asm `t \<in> space M` by (simp add: field_simps)
   322         also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
   323           using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
   324         also have "\<dots> = D t * (ln b * entropy_density b M \<nu> t)"
   325           using `0 < D t` RN b_gt_1
   326           by (simp_all add: log_def ln_div entropy_density_def)
   327         finally show ?thesis by simp
   328       qed simp
   329     qed
   330   qed
   331   also have "\<dots> = (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
   332     using D D_density ln_entropy
   333     by (intro integral_translated_density[symmetric]) auto
   334   also have "\<dots> = ln b * (\<integral> x. entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"
   335     using int by (rule \<nu>.integral_cmult)
   336   finally show "0 < KL_divergence b M \<nu>"
   337     using b_gt_1 by (auto simp: KL_divergence_def zero_less_mult_iff)
   338 qed
   339 
   340 lemma (in sigma_finite_measure) KL_eq_0:
   341   assumes eq: "\<forall>A\<in>sets M. \<nu> A = measure M A"
   342   shows "KL_divergence b M \<nu> = 0"
   343 proof -
   344   have "AE x. 1 = RN_deriv M \<nu> x"
   345   proof (rule RN_deriv_unique)
   346     show "measure_space (M\<lparr>measure := \<nu>\<rparr>)"
   347       using eq by (intro measure_space_cong) auto
   348     show "absolutely_continuous \<nu>"
   349       unfolding absolutely_continuous_def using eq by auto
   350     show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x. 0 \<le> (1 :: ereal)" by auto
   351     fix A assume "A \<in> sets M"
   352     with eq show "\<nu> A = \<integral>\<^isup>+ x. 1 * indicator A x \<partial>M" by simp
   353   qed
   354   then have "AE x. log b (real (RN_deriv M \<nu> x)) = 0"
   355     by (elim AE_mp) simp
   356   from integral_cong_AE[OF this]
   357   have "integral\<^isup>L M (entropy_density b M \<nu>) = 0"
   358     by (simp add: entropy_density_def comp_def)
   359   with eq show "KL_divergence b M \<nu> = 0"
   360     unfolding KL_divergence_def
   361     by (subst integral_cong_measure) auto
   362 qed
   363 
   364 lemma (in information_space) KL_eq_0_imp:
   365   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
   366   assumes ac: "absolutely_continuous \<nu>"
   367   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
   368   assumes KL: "KL_divergence b M \<nu> = 0"
   369   shows "\<forall>A\<in>sets M. \<nu> A = \<mu> A"
   370   by (metis less_imp_neq KL_gt_0 assms)
   371 
   372 lemma (in information_space) KL_ge_0:
   373   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"
   374   assumes ac: "absolutely_continuous \<nu>"
   375   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"
   376   shows "0 \<le> KL_divergence b M \<nu>"
   377   using KL_eq_0 KL_gt_0[OF ps ac int]
   378   by (cases "\<forall>A\<in>sets M. \<nu> A = measure M A") (auto simp: le_less)
   379 
   380 
   381 lemma (in sigma_finite_measure) KL_divergence_vimage:
   382   assumes T: "T \<in> measure_preserving M M'"
   383     and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)"
   384     and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x"
   385     and inv': "\<And>x. x \<in> space M' \<Longrightarrow> T (T' x) = x"
   386   and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'"
   387   and "1 < b"
   388   shows "KL_divergence b M' \<nu>' = KL_divergence b M \<nu>"
   389 proof -
   390   interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact
   391   have M: "measure_space (M\<lparr> measure := \<nu>\<rparr>)"
   392     by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default
   393   have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default
   394   then have saM': "sigma_algebra M'" by simp
   395   then interpret M': measure_space M' by (rule measure_space_vimage) fact
   396   have ac: "absolutely_continuous \<nu>" unfolding absolutely_continuous_def
   397   proof safe
   398     fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0"
   399     then have N': "T' -` N \<inter> space M' \<in> sets M'"
   400       using T' by (auto simp: measurable_def measure_preserving_def)
   401     have "T -` (T' -` N \<inter> space M') \<inter> space M = N"
   402       using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def)
   403     then have "measure M' (T' -` N \<inter> space M') = 0"
   404       using measure_preservingD[OF T N'] N_0 by auto
   405     with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N
   406       unfolding M'.absolutely_continuous_def measurable_def by auto
   407   qed
   408 
   409   have sa: "sigma_algebra (M\<lparr>measure := \<nu>\<rparr>)" by simp default
   410   have AE: "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"
   411     by (rule RN_deriv_vimage[OF T T' inv \<nu>'])
   412   show ?thesis
   413     unfolding KL_divergence_def entropy_density_def comp_def
   414   proof (subst \<nu>'.integral_vimage[OF sa T'])
   415     show "(\<lambda>x. log b (real (RN_deriv M \<nu> x))) \<in> borel_measurable (M\<lparr>measure := \<nu>\<rparr>)"
   416       by (auto intro!: RN_deriv[OF M ac] borel_measurable_log[OF _ `1 < b`])
   417     have "(\<integral> x. log b (real (RN_deriv M' \<nu>' x)) \<partial>M'\<lparr>measure := \<nu>'\<rparr>) =
   418       (\<integral> x. log b (real (RN_deriv M' \<nu>' (T (T' x)))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "?l = _")
   419       using inv' by (auto intro!: \<nu>'.integral_cong)
   420     also have "\<dots> = (\<integral> x. log b (real (RN_deriv M \<nu> (T' x))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "_ = ?r")
   421       using M ac AE
   422       by (intro \<nu>'.integral_cong_AE \<nu>'.almost_everywhere_vimage[OF sa T'] absolutely_continuous_AE[OF M])
   423          (auto elim!: AE_mp)
   424     finally show "?l = ?r" .
   425   qed
   426 qed
   427 
   428 lemma (in sigma_finite_measure) KL_divergence_cong:
   429   assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?\<nu>")
   430   assumes [simp]: "sets N = sets M" "space N = space M"
   431     "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A"
   432     "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<nu>' A"
   433   shows "KL_divergence b M \<nu> = KL_divergence b N \<nu>'"
   434 proof -
   435   interpret \<nu>: measure_space ?\<nu> by fact
   436   have "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv N \<nu>' x)) \<partial>?\<nu>"
   437     by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def entropy_density_def)
   438   also have "\<dots> = KL_divergence b N \<nu>'"
   439     by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def entropy_density_def comp_def)
   440   finally show ?thesis .
   441 qed
   442 
   443 lemma (in finite_measure_space) KL_divergence_eq_finite:
   444   assumes v: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)"
   445   assumes ac: "absolutely_continuous \<nu>"
   446   shows "KL_divergence b M \<nu> = (\<Sum>x\<in>space M. real (\<nu> {x}) * log b (real (\<nu> {x}) / real (\<mu> {x})))" (is "_ = ?sum")
   447 proof (simp add: KL_divergence_def finite_measure_space.integral_finite_singleton[OF v] entropy_density_def)
   448   interpret v: finite_measure_space "M\<lparr>measure := \<nu>\<rparr>" by fact
   449   have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
   450   show "(\<Sum>x \<in> space M. log b (real (RN_deriv M \<nu> x)) * real (\<nu> {x})) = ?sum"
   451     using RN_deriv_finite_measure[OF ms ac]
   452     by (auto intro!: setsum_cong simp: field_simps)
   453 qed
   454 
   455 lemma (in finite_prob_space) KL_divergence_positive_finite:
   456   assumes v: "finite_prob_space (M\<lparr>measure := \<nu>\<rparr>)"
   457   assumes ac: "absolutely_continuous \<nu>"
   458   and "1 < b"
   459   shows "0 \<le> KL_divergence b M \<nu>"
   460 proof -
   461   interpret information_space M by default fact
   462   interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
   463   have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
   464   from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis .
   465 qed
   466 
   467 subsection {* Mutual Information *}
   468 
   469 definition (in prob_space)
   470   "mutual_information b S T X Y =
   471     KL_divergence b (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>)
   472       (ereal\<circ>joint_distribution X Y)"
   473 
   474 lemma (in information_space)
   475   fixes S T X Y
   476   defines "P \<equiv> S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   477   shows "indep_var S X T Y \<longleftrightarrow>
   478     (random_variable S X \<and> random_variable T Y \<and>
   479       measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y) \<and>
   480       integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)
   481         (entropy_density b P (ereal\<circ>joint_distribution X Y)) \<and>
   482      mutual_information b S T X Y = 0)"
   483 proof safe
   484   assume indep: "indep_var S X T Y"
   485   then have "random_variable S X" "random_variable T Y"
   486     by (blast dest: indep_var_rv1 indep_var_rv2)+
   487   then show "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"
   488     by blast+
   489 
   490   interpret X: prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"
   491     by (rule distribution_prob_space) fact
   492   interpret Y: prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   493     by (rule distribution_prob_space) fact
   494   interpret XY: pair_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default
   495   interpret XY: information_space XY.P b by default (rule b_gt_1)
   496 
   497   let ?J = "XY.P\<lparr> measure := (ereal\<circ>joint_distribution X Y) \<rparr>"
   498   { fix A assume "A \<in> sets XY.P"
   499     then have "ereal (joint_distribution X Y A) = XY.\<mu> A"
   500       using indep_var_distributionD[OF indep]
   501       by (simp add: XY.P.finite_measure_eq) }
   502   note j_eq = this
   503 
   504   interpret J: prob_space ?J
   505     using j_eq by (intro XY.prob_space_cong) auto
   506 
   507   have ac: "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
   508     by (simp add: XY.absolutely_continuous_def j_eq)
   509   then show "measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y)"
   510     unfolding P_def .
   511 
   512   have ed: "entropy_density b XY.P (ereal\<circ>joint_distribution X Y) \<in> borel_measurable XY.P"
   513     by (rule XY.measurable_entropy_density) (default | fact)+
   514 
   515   have "AE x in XY.P. 1 = RN_deriv XY.P (ereal\<circ>joint_distribution X Y) x"
   516   proof (rule XY.RN_deriv_unique[OF _ ac])
   517     show "measure_space ?J" by default
   518     fix A assume "A \<in> sets XY.P"
   519     then show "(ereal\<circ>joint_distribution X Y) A = (\<integral>\<^isup>+ x. 1 * indicator A x \<partial>XY.P)"
   520       by (simp add: j_eq)
   521   qed (insert XY.measurable_const[of 1 borel], auto)
   522   then have ae_XY: "AE x in XY.P. entropy_density b XY.P (ereal\<circ>joint_distribution X Y) x = 0"
   523     by (elim XY.AE_mp) (simp add: entropy_density_def)
   524   have ae_J: "AE x in ?J. entropy_density b XY.P (ereal\<circ>joint_distribution X Y) x = 0"
   525   proof (rule XY.absolutely_continuous_AE)
   526     show "measure_space ?J" by default
   527     show "XY.absolutely_continuous (measure ?J)"
   528       using ac by simp
   529   qed (insert ae_XY, simp_all)
   530   then show "integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)
   531         (entropy_density b P (ereal\<circ>joint_distribution X Y))"
   532     unfolding P_def
   533     using ed XY.measurable_const[of 0 borel]
   534     by (subst J.integrable_cong_AE) auto
   535 
   536   show "mutual_information b S T X Y = 0"
   537     unfolding mutual_information_def KL_divergence_def P_def
   538     by (subst J.integral_cong_AE[OF ae_J]) simp
   539 next
   540   assume "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"
   541   then have rvs: "random_variable S X" "random_variable T Y" by blast+
   542 
   543   interpret X: prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"
   544     by (rule distribution_prob_space) fact
   545   interpret Y: prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   546     by (rule distribution_prob_space) fact
   547   interpret XY: pair_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default
   548   interpret XY: information_space XY.P b by default (rule b_gt_1)
   549 
   550   let ?J = "XY.P\<lparr> measure := (ereal\<circ>joint_distribution X Y) \<rparr>"
   551   interpret J: prob_space ?J
   552     using rvs by (intro joint_distribution_prob_space) auto
   553 
   554   assume ac: "measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y)"
   555   assume int: "integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)
   556         (entropy_density b P (ereal\<circ>joint_distribution X Y))"
   557   assume I_eq_0: "mutual_information b S T X Y = 0"
   558 
   559   have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A"
   560   proof (rule XY.KL_eq_0_imp)
   561     show "prob_space ?J" by unfold_locales
   562     show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
   563       using ac by (simp add: P_def)
   564     show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))"
   565       using int by (simp add: P_def)
   566     show "KL_divergence b XY.P (ereal\<circ>joint_distribution X Y) = 0"
   567       using I_eq_0 unfolding mutual_information_def by (simp add: P_def)
   568   qed
   569 
   570   { fix S X assume "sigma_algebra S"
   571     interpret S: sigma_algebra S by fact
   572     have "Int_stable \<lparr>space = space M, sets = {X -` A \<inter> space M |A. A \<in> sets S}\<rparr>"
   573     proof (safe intro!: Int_stableI)
   574       fix A B assume "A \<in> sets S" "B \<in> sets S"
   575       then show "\<exists>C. (X -` A \<inter> space M) \<inter> (X -` B \<inter> space M) = (X -` C \<inter> space M) \<and> C \<in> sets S"
   576         by (intro exI[of _ "A \<inter> B"]) auto
   577     qed }
   578   note Int_stable = this
   579 
   580   show "indep_var S X T Y" unfolding indep_var_eq
   581   proof (intro conjI indep_set_sigma_sets Int_stable)
   582     show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}"
   583     proof (safe intro!: indep_setI)
   584       { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M"
   585         using `X \<in> measurable M S` by (auto intro: measurable_sets) }
   586       { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M"
   587         using `Y \<in> measurable M T` by (auto intro: measurable_sets) }
   588     next
   589       fix A B assume ab: "A \<in> sets S" "B \<in> sets T"
   590       have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) =
   591         ereal (joint_distribution X Y (A \<times> B))"
   592         unfolding distribution_def
   593         by (intro arg_cong[where f="\<lambda>C. ereal (prob C)"]) auto
   594       also have "\<dots> = XY.\<mu> (A \<times> B)"
   595         using ab eq by (auto simp: XY.finite_measure_eq)
   596       also have "\<dots> = ereal (distribution X A) * ereal (distribution Y B)"
   597         using ab by (simp add: XY.pair_measure_times)
   598       finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
   599         prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
   600         unfolding distribution_def by simp
   601     qed
   602   qed fact+
   603 qed
   604 
   605 lemma (in information_space) mutual_information_commute_generic:
   606   assumes X: "random_variable S X" and Y: "random_variable T Y"
   607   assumes ac: "measure_space.absolutely_continuous
   608     (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>) (ereal\<circ>joint_distribution X Y)"
   609   shows "mutual_information b S T X Y = mutual_information b T S Y X"
   610 proof -
   611   let ?S = "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" and ?T = "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   612   interpret S: prob_space ?S using X by (rule distribution_prob_space)
   613   interpret T: prob_space ?T using Y by (rule distribution_prob_space)
   614   interpret P: pair_prob_space ?S ?T ..
   615   interpret Q: pair_prob_space ?T ?S ..
   616   show ?thesis
   617     unfolding mutual_information_def
   618   proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1])
   619     show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving
   620       (P.P \<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := ereal\<circ>joint_distribution Y X\<rparr>)"
   621       using X Y unfolding measurable_def
   622       unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable
   623       by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>'])
   624     have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
   625       using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
   626     then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
   627       unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp
   628   qed auto
   629 qed
   630 
   631 definition (in prob_space)
   632   "entropy b s X = mutual_information b s s X X"
   633 
   634 abbreviation (in information_space)
   635   mutual_information_Pow ("\<I>'(_ ; _')") where
   636   "\<I>(X ; Y) \<equiv> mutual_information b
   637     \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr>
   638     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = ereal\<circ>distribution Y \<rparr> X Y"
   639 
   640 lemma (in prob_space) finite_variables_absolutely_continuous:
   641   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   642   shows "measure_space.absolutely_continuous
   643     (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>)
   644     (ereal\<circ>joint_distribution X Y)"
   645 proof -
   646   interpret X: finite_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"
   647     using X by (rule distribution_finite_prob_space)
   648   interpret Y: finite_prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   649     using Y by (rule distribution_finite_prob_space)
   650   interpret XY: pair_finite_prob_space
   651     "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr> measure := ereal\<circ>distribution Y\<rparr>" by default
   652   interpret P: finite_prob_space "XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>"
   653     using assms by (auto intro!: joint_distribution_finite_prob_space)
   654   note rv = assms[THEN finite_random_variableD]
   655   show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
   656   proof (rule XY.absolutely_continuousI)
   657     show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
   658     fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"
   659     then obtain a b where "x = (a, b)"
   660       and "distribution X {a} = 0 \<or> distribution Y {b} = 0"
   661       by (cases x) (auto simp: space_pair_measure)
   662     with finite_distribution_order(5,6)[OF X Y]
   663     show "(ereal \<circ> joint_distribution X Y) {x} = 0" by auto
   664   qed
   665 qed
   666 
   667 lemma (in information_space)
   668   assumes MX: "finite_random_variable MX X"
   669   assumes MY: "finite_random_variable MY Y"
   670   shows mutual_information_generic_eq:
   671     "mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY.
   672       joint_distribution X Y {(x,y)} *
   673       log b (joint_distribution X Y {(x,y)} /
   674       (distribution X {x} * distribution Y {y})))"
   675     (is ?sum)
   676   and mutual_information_positive_generic:
   677      "0 \<le> mutual_information b MX MY X Y" (is ?positive)
   678 proof -
   679   interpret X: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"
   680     using MX by (rule distribution_finite_prob_space)
   681   interpret Y: finite_prob_space "MY\<lparr>measure := ereal\<circ>distribution Y\<rparr>"
   682     using MY by (rule distribution_finite_prob_space)
   683   interpret XY: pair_finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>" "MY\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default
   684   interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>"
   685     using assms by (auto intro!: joint_distribution_finite_prob_space)
   686 
   687   have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
   688   have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
   689 
   690   show ?sum
   691     unfolding Let_def mutual_information_def
   692     by (subst XY.KL_divergence_eq_finite[OF P_ms finite_variables_absolutely_continuous[OF MX MY]])
   693        (auto simp add: space_pair_measure setsum_cartesian_product')
   694 
   695   show ?positive
   696     using XY.KL_divergence_positive_finite[OF P_ps finite_variables_absolutely_continuous[OF MX MY] b_gt_1]
   697     unfolding mutual_information_def .
   698 qed
   699 
   700 lemma (in information_space) mutual_information_commute:
   701   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
   702   shows "mutual_information b S T X Y = mutual_information b T S Y X"
   703   unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]
   704   unfolding joint_distribution_commute_singleton[of X Y]
   705   by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])
   706 
   707 lemma (in information_space) mutual_information_commute_simple:
   708   assumes X: "simple_function M X" and Y: "simple_function M Y"
   709   shows "\<I>(X;Y) = \<I>(Y;X)"
   710   by (intro mutual_information_commute X Y simple_function_imp_finite_random_variable)
   711 
   712 lemma (in information_space) mutual_information_eq:
   713   assumes "simple_function M X" "simple_function M Y"
   714   shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
   715     distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /
   716                                                    (distribution X {x} * distribution Y {y})))"
   717   using assms by (simp add: mutual_information_generic_eq)
   718 
   719 lemma (in information_space) mutual_information_generic_cong:
   720   assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
   721   assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
   722   shows "mutual_information b MX MY X Y = mutual_information b MX MY X' Y'"
   723   unfolding mutual_information_def using X Y
   724   by (simp cong: distribution_cong)
   725 
   726 lemma (in information_space) mutual_information_cong:
   727   assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
   728   assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
   729   shows "\<I>(X; Y) = \<I>(X'; Y')"
   730   unfolding mutual_information_def using X Y
   731   by (simp cong: distribution_cong image_cong)
   732 
   733 lemma (in information_space) mutual_information_positive:
   734   assumes "simple_function M X" "simple_function M Y"
   735   shows "0 \<le> \<I>(X;Y)"
   736   using assms by (simp add: mutual_information_positive_generic)
   737 
   738 subsection {* Entropy *}
   739 
   740 abbreviation (in information_space)
   741   entropy_Pow ("\<H>'(_')") where
   742   "\<H>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr> X"
   743 
   744 lemma (in information_space) entropy_generic_eq:
   745   fixes X :: "'a \<Rightarrow> 'c"
   746   assumes MX: "finite_random_variable MX X"
   747   shows "entropy b MX X = -(\<Sum> x \<in> space MX. distribution X {x} * log b (distribution X {x}))"
   748 proof -
   749   interpret MX: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"
   750     using MX by (rule distribution_finite_prob_space)
   751   let "?X x" = "distribution X {x}"
   752   let "?XX x y" = "joint_distribution X X {(x, y)}"
   753 
   754   { fix x y :: 'c
   755     { assume "x \<noteq> y"
   756       then have "(\<lambda>x. (X x, X x)) -` {(x,y)} \<inter> space M = {}" by auto
   757       then have "joint_distribution X X {(x, y)} = 0" by (simp add: distribution_def) }
   758     then have "?XX x y * log b (?XX x y / (?X x * ?X y)) =
   759         (if x = y then - ?X y * log b (?X y) else 0)"
   760       by (auto simp: log_simps zero_less_mult_iff) }
   761   note remove_XX = this
   762 
   763   show ?thesis
   764     unfolding entropy_def mutual_information_generic_eq[OF MX MX]
   765     unfolding setsum_cartesian_product[symmetric] setsum_negf[symmetric] remove_XX
   766     using MX.finite_space by (auto simp: setsum_cases)
   767 qed
   768 
   769 lemma (in information_space) entropy_eq:
   770   assumes "simple_function M X"
   771   shows "\<H>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
   772   using assms by (simp add: entropy_generic_eq)
   773 
   774 lemma (in information_space) entropy_positive:
   775   "simple_function M X \<Longrightarrow> 0 \<le> \<H>(X)"
   776   unfolding entropy_def by (simp add: mutual_information_positive)
   777 
   778 lemma (in information_space) entropy_certainty_eq_0:
   779   assumes X: "simple_function M X" and "x \<in> X ` space M" and "distribution X {x} = 1"
   780   shows "\<H>(X) = 0"
   781 proof -
   782   let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = ereal\<circ>distribution X\<rparr>"
   783   note simple_function_imp_finite_random_variable[OF `simple_function M X`]
   784   from distribution_finite_prob_space[OF this, of "\<lparr> measure = ereal\<circ>distribution X \<rparr>"]
   785   interpret X: finite_prob_space ?X by simp
   786   have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"
   787     using X.measure_compl[of "{x}"] assms by auto
   788   also have "\<dots> = 0" using X.prob_space assms by auto
   789   finally have X0: "distribution X (X ` space M - {x}) = 0" by auto
   790   { fix y assume *: "y \<in> X ` space M"
   791     { assume asm: "y \<noteq> x"
   792       with * have "{y} \<subseteq> X ` space M - {x}" by auto
   793       from X.measure_mono[OF this] X0 asm *
   794       have "distribution X {y} = 0"  by (auto intro: antisym) }
   795     then have "distribution X {y} = (if x = y then 1 else 0)"
   796       using assms by auto }
   797   note fi = this
   798   have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp
   799   show ?thesis unfolding entropy_eq[OF `simple_function M X`] by (auto simp: y fi)
   800 qed
   801 
   802 lemma (in information_space) entropy_le_card_not_0:
   803   assumes X: "simple_function M X"
   804   shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))"
   805 proof -
   806   let "?p x" = "distribution X {x}"
   807   have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"
   808     unfolding entropy_eq[OF X] setsum_negf[symmetric]
   809     by (auto intro!: setsum_cong simp: log_simps)
   810   also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. ?p x * (1 / ?p x))"
   811     using not_empty b_gt_1 `simple_function M X` sum_over_space_real_distribution[OF X]
   812     by (intro log_setsum') (auto simp: simple_function_def)
   813   also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?p x \<noteq> 0 then 1 else 0)"
   814     by (intro arg_cong[where f="\<lambda>X. log b X"] setsum_cong) auto
   815   finally show ?thesis
   816     using `simple_function M X` by (auto simp: setsum_cases real_eq_of_nat simple_function_def)
   817 qed
   818 
   819 lemma (in prob_space) measure'_translate:
   820   assumes X: "random_variable S X" and A: "A \<in> sets S"
   821   shows "finite_measure.\<mu>' (S\<lparr> measure := ereal\<circ>distribution X \<rparr>) A = distribution X A"
   822 proof -
   823   interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
   824     using distribution_prob_space[OF X] .
   825   from A show "S.\<mu>' A = distribution X A"
   826     unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
   827 qed
   828 
   829 lemma (in information_space) entropy_uniform_max:
   830   assumes X: "simple_function M X"
   831   assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
   832   shows "\<H>(X) = log b (real (card (X ` space M)))"
   833 proof -
   834   let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = undefined\<rparr>\<lparr> measure := ereal\<circ>distribution X\<rparr>"
   835   note frv = simple_function_imp_finite_random_variable[OF X]
   836   from distribution_finite_prob_space[OF this, of "\<lparr> measure = ereal\<circ>distribution X \<rparr>"]
   837   interpret X: finite_prob_space ?X by simp
   838   note rv = finite_random_variableD[OF frv]
   839   have card_gt0: "0 < card (X ` space M)" unfolding card_gt_0_iff
   840     using `simple_function M X` not_empty by (auto simp: simple_function_def)
   841   { fix x assume "x \<in> space ?X"
   842     moreover then have "X.\<mu>' {x} = 1 / card (space ?X)"
   843     proof (rule X.uniform_prob)
   844       fix x y assume "x \<in> space ?X" "y \<in> space ?X"
   845       with assms(2)[of x y] show "X.\<mu>' {x} = X.\<mu>' {y}"
   846         by (subst (1 2) measure'_translate[OF rv]) auto
   847     qed
   848     ultimately have "distribution X {x} = 1 / card (space ?X)"
   849       by (subst (asm) measure'_translate[OF rv]) auto }
   850   thus ?thesis
   851     using not_empty X.finite_space b_gt_1 card_gt0
   852     by (simp add: entropy_eq[OF `simple_function M X`] real_eq_of_nat[symmetric] log_simps)
   853 qed
   854 
   855 lemma (in information_space) entropy_le_card:
   856   assumes "simple_function M X"
   857   shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
   858 proof cases
   859   assume "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} = {}"
   860   then have "\<And>x. x\<in>X`space M \<Longrightarrow> distribution X {x} = 0" by auto
   861   moreover
   862   have "0 < card (X`space M)"
   863     using `simple_function M X` not_empty
   864     by (auto simp: card_gt_0_iff simple_function_def)
   865   then have "log b 1 \<le> log b (real (card (X`space M)))"
   866     using b_gt_1 by (intro log_le) auto
   867   ultimately show ?thesis using assms by (simp add: entropy_eq)
   868 next
   869   assume False: "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} \<noteq> {}"
   870   have "card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}) \<le> card (X ` space M)"
   871     (is "?A \<le> ?B") using assms not_empty by (auto intro!: card_mono simp: simple_function_def)
   872   note entropy_le_card_not_0[OF assms]
   873   also have "log b (real ?A) \<le> log b (real ?B)"
   874     using b_gt_1 False not_empty `?A \<le> ?B` assms
   875     by (auto intro!: log_le simp: card_gt_0_iff simp: simple_function_def)
   876   finally show ?thesis .
   877 qed
   878 
   879 lemma (in information_space) entropy_commute:
   880   assumes "simple_function M X" "simple_function M Y"
   881   shows "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))"
   882 proof -
   883   have sf: "simple_function M (\<lambda>x. (X x, Y x))" "simple_function M (\<lambda>x. (Y x, X x))"
   884     using assms by (auto intro: simple_function_Pair)
   885   have *: "(\<lambda>x. (Y x, X x))`space M = (\<lambda>(a,b). (b,a))`(\<lambda>x. (X x, Y x))`space M"
   886     by auto
   887   have inj: "\<And>X. inj_on (\<lambda>(a,b). (b,a)) X"
   888     by (auto intro!: inj_onI)
   889   show ?thesis
   890     unfolding sf[THEN entropy_eq] unfolding * setsum_reindex[OF inj]
   891     by (simp add: joint_distribution_commute[of Y X] split_beta)
   892 qed
   893 
   894 lemma (in information_space) entropy_eq_cartesian_product:
   895   assumes "simple_function M X" "simple_function M Y"
   896   shows "\<H>(\<lambda>x. (X x, Y x)) = -(\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M.
   897     joint_distribution X Y {(x,y)} * log b (joint_distribution X Y {(x,y)}))"
   898 proof -
   899   have sf: "simple_function M (\<lambda>x. (X x, Y x))"
   900     using assms by (auto intro: simple_function_Pair)
   901   { fix x assume "x\<notin>(\<lambda>x. (X x, Y x))`space M"
   902     then have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = {}" by auto
   903     then have "joint_distribution X Y {x} = 0"
   904       unfolding distribution_def by auto }
   905   then show ?thesis using sf assms
   906     unfolding entropy_eq[OF sf] neg_equal_iff_equal setsum_cartesian_product
   907     by (auto intro!: setsum_mono_zero_cong_left simp: simple_function_def)
   908 qed
   909 
   910 subsection {* Conditional Mutual Information *}
   911 
   912 definition (in prob_space)
   913   "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
   914     mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x)) -
   915     mutual_information b MX MZ X Z"
   916 
   917 abbreviation (in information_space)
   918   conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
   919   "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
   920     \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr>
   921     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = ereal\<circ>distribution Y \<rparr>
   922     \<lparr> space = Z`space M, sets = Pow (Z`space M), measure = ereal\<circ>distribution Z \<rparr>
   923     X Y Z"
   924 
   925 lemma (in information_space) conditional_mutual_information_generic_eq:
   926   assumes MX: "finite_random_variable MX X"
   927     and MY: "finite_random_variable MY Y"
   928     and MZ: "finite_random_variable MZ Z"
   929   shows "conditional_mutual_information b MX MY MZ X Y Z = (\<Sum>(x, y, z) \<in> space MX \<times> space MY \<times> space MZ.
   930              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
   931              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} /
   932     (joint_distribution X Z {(x, z)} * (joint_distribution Y Z {(y,z)} / distribution Z {z}))))"
   933   (is "_ = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z))))")
   934 proof -
   935   let ?X = "\<lambda>x. distribution X {x}"
   936   note finite_var = MX MY MZ
   937   note YZ = finite_random_variable_pairI[OF finite_var(2,3)]
   938   note XYZ = finite_random_variable_pairI[OF MX YZ]
   939   note XZ = finite_random_variable_pairI[OF finite_var(1,3)]
   940   note ZX = finite_random_variable_pairI[OF finite_var(3,1)]
   941   note YZX = finite_random_variable_pairI[OF finite_var(2) ZX]
   942   note order1 =
   943     finite_distribution_order(5,6)[OF finite_var(1) YZ]
   944     finite_distribution_order(5,6)[OF finite_var(1,3)]
   945 
   946   note random_var = finite_var[THEN finite_random_variableD]
   947   note finite = finite_var(1) YZ finite_var(3) XZ YZX
   948 
   949   have order2: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>
   950           \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"
   951     unfolding joint_distribution_commute_singleton[of X]
   952     unfolding joint_distribution_assoc_singleton[symmetric]
   953     using finite_distribution_order(6)[OF finite_var(2) ZX]
   954     by auto
   955 
   956   have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z)))) =
   957     (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * (log b (?XYZ x y z / (?X x * ?YZ y z)) - log b (?XZ x z / (?X x * ?Z z))))"
   958     (is "(\<Sum>(x, y, z)\<in>?S. ?L x y z) = (\<Sum>(x, y, z)\<in>?S. ?R x y z)")
   959   proof (safe intro!: setsum_cong)
   960     fix x y z assume space: "x \<in> space MX" "y \<in> space MY" "z \<in> space MZ"
   961     show "?L x y z = ?R x y z"
   962     proof cases
   963       assume "?XYZ x y z \<noteq> 0"
   964       with space have "0 < ?X x" "0 < ?Z z" "0 < ?XZ x z" "0 < ?YZ y z" "0 < ?XYZ x y z"
   965         using order1 order2 by (auto simp: less_le)
   966       with b_gt_1 show ?thesis
   967         by (simp add: log_mult log_divide zero_less_mult_iff zero_less_divide_iff)
   968     qed simp
   969   qed
   970   also have "\<dots> = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -
   971                   (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z)))"
   972     by (auto simp add: setsum_subtractf[symmetric] field_simps intro!: setsum_cong)
   973   also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z))) =
   974              (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z)))"
   975     unfolding setsum_cartesian_product[symmetric] setsum_commute[of _ _ "space MY"]
   976               setsum_left_distrib[symmetric]
   977     unfolding joint_distribution_commute_singleton[of X]
   978     unfolding joint_distribution_assoc_singleton[symmetric]
   979     using setsum_joint_distribution_singleton[OF finite_var(2) ZX]
   980     by (intro setsum_cong refl) (simp add: space_pair_measure)
   981   also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -
   982              (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z))) =
   983              conditional_mutual_information b MX MY MZ X Y Z"
   984     unfolding conditional_mutual_information_def
   985     unfolding mutual_information_generic_eq[OF finite_var(1,3)]
   986     unfolding mutual_information_generic_eq[OF finite_var(1) YZ]
   987     by (simp add: space_sigma space_pair_measure setsum_cartesian_product')
   988   finally show ?thesis by simp
   989 qed
   990 
   991 lemma (in information_space) conditional_mutual_information_eq:
   992   assumes "simple_function M X" "simple_function M Y" "simple_function M Z"
   993   shows "\<I>(X;Y|Z) = (\<Sum>(x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.
   994              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
   995              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} /
   996     (joint_distribution X Z {(x, z)} * joint_distribution Y Z {(y,z)} / distribution Z {z})))"
   997   by (subst conditional_mutual_information_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]])
   998      simp
   999 
  1000 lemma (in information_space) conditional_mutual_information_eq_mutual_information:
  1001   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1002   shows "\<I>(X ; Y) = \<I>(X ; Y | (\<lambda>x. ()))"
  1003 proof -
  1004   have [simp]: "(\<lambda>x. ()) ` space M = {()}" using not_empty by auto
  1005   have C: "simple_function M (\<lambda>x. ())" by auto
  1006   show ?thesis
  1007     unfolding conditional_mutual_information_eq[OF X Y C]
  1008     unfolding mutual_information_eq[OF X Y]
  1009     by (simp add: setsum_cartesian_product' distribution_remove_const)
  1010 qed
  1011 
  1012 lemma (in information_space) conditional_mutual_information_generic_positive:
  1013   assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
  1014   shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
  1015 proof (cases "space MX \<times> space MY \<times> space MZ = {}")
  1016   case True show ?thesis
  1017     unfolding conditional_mutual_information_generic_eq[OF assms] True
  1018     by simp
  1019 next
  1020   case False
  1021   let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))"
  1022   let ?dXZ = "joint_distribution X Z"
  1023   let ?dYZ = "joint_distribution Y Z"
  1024   let ?dX = "distribution X"
  1025   let ?dZ = "distribution Z"
  1026   let ?M = "space MX \<times> space MY \<times> space MZ"
  1027 
  1028   note YZ = finite_random_variable_pairI[OF Y Z]
  1029   note XZ = finite_random_variable_pairI[OF X Z]
  1030   note ZX = finite_random_variable_pairI[OF Z X]
  1031   note YZ = finite_random_variable_pairI[OF Y Z]
  1032   note XYZ = finite_random_variable_pairI[OF X YZ]
  1033   note finite = Z YZ XZ XYZ
  1034   have order: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>
  1035           \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"
  1036     unfolding joint_distribution_commute_singleton[of X]
  1037     unfolding joint_distribution_assoc_singleton[symmetric]
  1038     using finite_distribution_order(6)[OF Y ZX]
  1039     by auto
  1040 
  1041   note order = order
  1042     finite_distribution_order(5,6)[OF X YZ]
  1043     finite_distribution_order(5,6)[OF Y Z]
  1044 
  1045   have "- conditional_mutual_information b MX MY MZ X Y Z = - (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
  1046     log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))"
  1047     unfolding conditional_mutual_information_generic_eq[OF assms] neg_equal_iff_equal by auto
  1048   also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})"
  1049     unfolding split_beta'
  1050   proof (rule log_setsum_divide)
  1051     show "?M \<noteq> {}" using False by simp
  1052     show "1 < b" using b_gt_1 .
  1053 
  1054     show "finite ?M" using assms
  1055       unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by auto
  1056 
  1057     show "(\<Sum>x\<in>?M. ?dXYZ {(fst x, fst (snd x), snd (snd x))}) = 1"
  1058       unfolding setsum_cartesian_product'
  1059       unfolding setsum_commute[of _ "space MY"]
  1060       unfolding setsum_commute[of _ "space MZ"]
  1061       by (simp_all add: space_pair_measure
  1062                         setsum_joint_distribution_singleton[OF X YZ]
  1063                         setsum_joint_distribution_singleton[OF Y Z]
  1064                         setsum_distribution[OF Z])
  1065 
  1066     fix x assume "x \<in> ?M"
  1067     let ?x = "(fst x, fst (snd x), snd (snd x))"
  1068 
  1069     show "0 \<le> ?dXYZ {?x}"
  1070       "0 \<le> ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
  1071      by (simp_all add: mult_nonneg_nonneg divide_nonneg_nonneg)
  1072 
  1073     assume *: "0 < ?dXYZ {?x}"
  1074     with `x \<in> ?M` finite order show "0 < ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
  1075       by (cases x) (auto simp add: zero_le_mult_iff zero_le_divide_iff less_le)
  1076   qed
  1077   also have "(\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}) = (\<Sum>z\<in>space MZ. ?dZ {z})"
  1078     apply (simp add: setsum_cartesian_product')
  1079     apply (subst setsum_commute)
  1080     apply (subst (2) setsum_commute)
  1081     by (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric]
  1082                    setsum_joint_distribution_singleton[OF X Z]
  1083                    setsum_joint_distribution_singleton[OF Y Z]
  1084           intro!: setsum_cong)
  1085   also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0"
  1086     unfolding setsum_distribution[OF Z] by simp
  1087   finally show ?thesis by simp
  1088 qed
  1089 
  1090 lemma (in information_space) conditional_mutual_information_positive:
  1091   assumes "simple_function M X" and "simple_function M Y" and "simple_function M Z"
  1092   shows "0 \<le> \<I>(X;Y|Z)"
  1093   by (rule conditional_mutual_information_generic_positive[OF assms[THEN simple_function_imp_finite_random_variable]])
  1094 
  1095 subsection {* Conditional Entropy *}
  1096 
  1097 definition (in prob_space)
  1098   "conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y"
  1099 
  1100 abbreviation (in information_space)
  1101   conditional_entropy_Pow ("\<H>'(_ | _')") where
  1102   "\<H>(X | Y) \<equiv> conditional_entropy b
  1103     \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr>
  1104     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = ereal\<circ>distribution Y \<rparr> X Y"
  1105 
  1106 lemma (in information_space) conditional_entropy_positive:
  1107   "simple_function M X \<Longrightarrow> simple_function M Y \<Longrightarrow> 0 \<le> \<H>(X | Y)"
  1108   unfolding conditional_entropy_def by (auto intro!: conditional_mutual_information_positive)
  1109 
  1110 lemma (in information_space) conditional_entropy_generic_eq:
  1111   fixes MX :: "('c, 'd) measure_space_scheme" and MY :: "('e, 'f) measure_space_scheme"
  1112   assumes MX: "finite_random_variable MX X"
  1113   assumes MZ: "finite_random_variable MZ Z"
  1114   shows "conditional_entropy b MX MZ X Z =
  1115      - (\<Sum>(x, z)\<in>space MX \<times> space MZ.
  1116          joint_distribution X Z {(x, z)} * log b (joint_distribution X Z {(x, z)} / distribution Z {z}))"
  1117 proof -
  1118   interpret MX: finite_sigma_algebra MX using MX by simp
  1119   interpret MZ: finite_sigma_algebra MZ using MZ by simp
  1120   let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
  1121   let "?XZ x z" = "joint_distribution X Z {(x, z)}"
  1122   let "?Z z" = "distribution Z {z}"
  1123   let "?f x y z" = "log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))"
  1124   { fix x z have "?XXZ x x z = ?XZ x z"
  1125       unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) }
  1126   note this[simp]
  1127   { fix x x' :: 'c and z assume "x' \<noteq> x"
  1128     then have "?XXZ x x' z = 0"
  1129       by (auto simp: distribution_def empty_measure'[symmetric]
  1130                simp del: empty_measure' intro!: arg_cong[where f=\<mu>']) }
  1131   note this[simp]
  1132   { fix x x' z assume *: "x \<in> space MX" "z \<in> space MZ"
  1133     then have "(\<Sum>x'\<in>space MX. ?XXZ x x' z * ?f x x' z)
  1134       = (\<Sum>x'\<in>space MX. if x = x' then ?XZ x z * ?f x x z else 0)"
  1135       by (auto intro!: setsum_cong)
  1136     also have "\<dots> = ?XZ x z * ?f x x z"
  1137       using `x \<in> space MX` by (simp add: setsum_cases[OF MX.finite_space])
  1138     also have "\<dots> = ?XZ x z * log b (?Z z / ?XZ x z)" by auto
  1139     also have "\<dots> = - ?XZ x z * log b (?XZ x z / ?Z z)"
  1140       using finite_distribution_order(6)[OF MX MZ]
  1141       by (auto simp: log_simps field_simps zero_less_mult_iff)
  1142     finally have "(\<Sum>x'\<in>space MX. ?XXZ x x' z * ?f x x' z) = - ?XZ x z * log b (?XZ x z / ?Z z)" . }
  1143   note * = this
  1144   show ?thesis
  1145     unfolding conditional_entropy_def
  1146     unfolding conditional_mutual_information_generic_eq[OF MX MX MZ]
  1147     by (auto simp: setsum_cartesian_product' setsum_negf[symmetric]
  1148                    setsum_commute[of _ "space MZ"] *
  1149              intro!: setsum_cong)
  1150 qed
  1151 
  1152 lemma (in information_space) conditional_entropy_eq:
  1153   assumes "simple_function M X" "simple_function M Z"
  1154   shows "\<H>(X | Z) =
  1155      - (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
  1156          joint_distribution X Z {(x, z)} *
  1157          log b (joint_distribution X Z {(x, z)} / distribution Z {z}))"
  1158   by (subst conditional_entropy_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]])
  1159      simp
  1160 
  1161 lemma (in information_space) conditional_entropy_eq_ce_with_hypothesis:
  1162   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1163   shows "\<H>(X | Y) =
  1164     -(\<Sum>y\<in>Y`space M. distribution Y {y} *
  1165       (\<Sum>x\<in>X`space M. joint_distribution X Y {(x,y)} / distribution Y {(y)} *
  1166               log b (joint_distribution X Y {(x,y)} / distribution Y {(y)})))"
  1167   unfolding conditional_entropy_eq[OF assms]
  1168   using finite_distribution_order(5,6)[OF assms[THEN simple_function_imp_finite_random_variable]]
  1169   by (auto simp: setsum_cartesian_product'  setsum_commute[of _ "Y`space M"] setsum_right_distrib
  1170            intro!: setsum_cong)
  1171 
  1172 lemma (in information_space) conditional_entropy_eq_cartesian_product:
  1173   assumes "simple_function M X" "simple_function M Y"
  1174   shows "\<H>(X | Y) = -(\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M.
  1175     joint_distribution X Y {(x,y)} *
  1176     log b (joint_distribution X Y {(x,y)} / distribution Y {y}))"
  1177   unfolding conditional_entropy_eq[OF assms]
  1178   by (auto intro!: setsum_cong simp: setsum_cartesian_product')
  1179 
  1180 subsection {* Equalities *}
  1181 
  1182 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
  1183   assumes X: "simple_function M X" and Z: "simple_function M Z"
  1184   shows  "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
  1185 proof -
  1186   let "?XZ x z" = "joint_distribution X Z {(x, z)}"
  1187   let "?Z z" = "distribution Z {z}"
  1188   let "?X x" = "distribution X {x}"
  1189   note fX = X[THEN simple_function_imp_finite_random_variable]
  1190   note fZ = Z[THEN simple_function_imp_finite_random_variable]
  1191   note finite_distribution_order[OF fX fZ, simp]
  1192   { fix x z assume "x \<in> X`space M" "z \<in> Z`space M"
  1193     have "?XZ x z * log b (?XZ x z / (?X x * ?Z z)) =
  1194           ?XZ x z * log b (?XZ x z / ?Z z) - ?XZ x z * log b (?X x)"
  1195       by (auto simp: log_simps zero_le_mult_iff field_simps less_le) }
  1196   note * = this
  1197   show ?thesis
  1198     unfolding entropy_eq[OF X] conditional_entropy_eq[OF X Z] mutual_information_eq[OF X Z]
  1199     using setsum_joint_distribution_singleton[OF fZ fX, unfolded joint_distribution_commute_singleton[of Z X]]
  1200     by (simp add: * setsum_cartesian_product' setsum_subtractf setsum_left_distrib[symmetric]
  1201                      setsum_distribution)
  1202 qed
  1203 
  1204 lemma (in information_space) conditional_entropy_less_eq_entropy:
  1205   assumes X: "simple_function M X" and Z: "simple_function M Z"
  1206   shows "\<H>(X | Z) \<le> \<H>(X)"
  1207 proof -
  1208   have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
  1209   with mutual_information_positive[OF X Z] entropy_positive[OF X]
  1210   show ?thesis by auto
  1211 qed
  1212 
  1213 lemma (in information_space) entropy_chain_rule:
  1214   assumes X: "simple_function M X" and Y: "simple_function M Y"
  1215   shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
  1216 proof -
  1217   let "?XY x y" = "joint_distribution X Y {(x, y)}"
  1218   let "?Y y" = "distribution Y {y}"
  1219   let "?X x" = "distribution X {x}"
  1220   note fX = X[THEN simple_function_imp_finite_random_variable]
  1221   note fY = Y[THEN simple_function_imp_finite_random_variable]
  1222   note finite_distribution_order[OF fX fY, simp]
  1223   { fix x y assume "x \<in> X`space M" "y \<in> Y`space M"
  1224     have "?XY x y * log b (?XY x y / ?X x) =
  1225           ?XY x y * log b (?XY x y) - ?XY x y * log b (?X x)"
  1226       by (auto simp: log_simps zero_le_mult_iff field_simps less_le) }
  1227   note * = this
  1228   show ?thesis
  1229     using setsum_joint_distribution_singleton[OF fY fX]
  1230     unfolding entropy_eq[OF X] conditional_entropy_eq_cartesian_product[OF Y X] entropy_eq_cartesian_product[OF X Y]
  1231     unfolding joint_distribution_commute_singleton[of Y X] setsum_commute[of _ "X`space M"]
  1232     by (simp add: * setsum_subtractf setsum_left_distrib[symmetric])
  1233 qed
  1234 
  1235 section {* Partitioning *}
  1236 
  1237 definition "subvimage A f g \<longleftrightarrow> (\<forall>x \<in> A. f -` {f x} \<inter> A \<subseteq> g -` {g x} \<inter> A)"
  1238 
  1239 lemma subvimageI:
  1240   assumes "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
  1241   shows "subvimage A f g"
  1242   using assms unfolding subvimage_def by blast
  1243 
  1244 lemma subvimageE[consumes 1]:
  1245   assumes "subvimage A f g"
  1246   obtains "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
  1247   using assms unfolding subvimage_def by blast
  1248 
  1249 lemma subvimageD:
  1250   "\<lbrakk> subvimage A f g ; x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
  1251   using assms unfolding subvimage_def by blast
  1252 
  1253 lemma subvimage_subset:
  1254   "\<lbrakk> subvimage B f g ; A \<subseteq> B \<rbrakk> \<Longrightarrow> subvimage A f g"
  1255   unfolding subvimage_def by auto
  1256 
  1257 lemma subvimage_idem[intro]: "subvimage A g g"
  1258   by (safe intro!: subvimageI)
  1259 
  1260 lemma subvimage_comp_finer[intro]:
  1261   assumes svi: "subvimage A g h"
  1262   shows "subvimage A g (f \<circ> h)"
  1263 proof (rule subvimageI, simp)
  1264   fix x y assume "x \<in> A" "y \<in> A" "g x = g y"
  1265   from svi[THEN subvimageD, OF this]
  1266   show "f (h x) = f (h y)" by simp
  1267 qed
  1268 
  1269 lemma subvimage_comp_gran:
  1270   assumes svi: "subvimage A g h"
  1271   assumes inj: "inj_on f (g ` A)"
  1272   shows "subvimage A (f \<circ> g) h"
  1273   by (rule subvimageI) (auto intro!: subvimageD[OF svi] simp: inj_on_iff[OF inj])
  1274 
  1275 lemma subvimage_comp:
  1276   assumes svi: "subvimage (f ` A) g h"
  1277   shows "subvimage A (g \<circ> f) (h \<circ> f)"
  1278   by (rule subvimageI) (auto intro!: svi[THEN subvimageD])
  1279 
  1280 lemma subvimage_trans:
  1281   assumes fg: "subvimage A f g"
  1282   assumes gh: "subvimage A g h"
  1283   shows "subvimage A f h"
  1284   by (rule subvimageI) (auto intro!: fg[THEN subvimageD] gh[THEN subvimageD])
  1285 
  1286 lemma subvimage_translator:
  1287   assumes svi: "subvimage A f g"
  1288   shows "\<exists>h. \<forall>x \<in> A. h (f x)  = g x"
  1289 proof (safe intro!: exI[of _ "\<lambda>x. (THE z. z \<in> (g ` (f -` {x} \<inter> A)))"])
  1290   fix x assume "x \<in> A"
  1291   show "(THE x'. x' \<in> (g ` (f -` {f x} \<inter> A))) = g x"
  1292     by (rule theI2[of _ "g x"])
  1293       (insert `x \<in> A`, auto intro!: svi[THEN subvimageD])
  1294 qed
  1295 
  1296 lemma subvimage_translator_image:
  1297   assumes svi: "subvimage A f g"
  1298   shows "\<exists>h. h ` f ` A = g ` A"
  1299 proof -
  1300   from subvimage_translator[OF svi]
  1301   obtain h where "\<And>x. x \<in> A \<Longrightarrow> h (f x) = g x" by auto
  1302   thus ?thesis
  1303     by (auto intro!: exI[of _ h]
  1304       simp: image_compose[symmetric] comp_def cong: image_cong)
  1305 qed
  1306 
  1307 lemma subvimage_finite:
  1308   assumes svi: "subvimage A f g" and fin: "finite (f`A)"
  1309   shows "finite (g`A)"
  1310 proof -
  1311   from subvimage_translator_image[OF svi]
  1312   obtain h where "g`A = h`f`A" by fastforce
  1313   with fin show "finite (g`A)" by simp
  1314 qed
  1315 
  1316 lemma subvimage_disj:
  1317   assumes svi: "subvimage A f g"
  1318   shows "f -` {x} \<inter> A \<subseteq> g -` {y} \<inter> A \<or>
  1319       f -` {x} \<inter> g -` {y} \<inter> A = {}" (is "?sub \<or> ?dist")
  1320 proof (rule disjCI)
  1321   assume "\<not> ?dist"
  1322   then obtain z where "z \<in> A" and "x = f z" and "y = g z" by auto
  1323   thus "?sub" using svi unfolding subvimage_def by auto
  1324 qed
  1325 
  1326 lemma setsum_image_split:
  1327   assumes svi: "subvimage A f g" and fin: "finite (f ` A)"
  1328   shows "(\<Sum>x\<in>f`A. h x) = (\<Sum>y\<in>g`A. \<Sum>x\<in>f`(g -` {y} \<inter> A). h x)"
  1329     (is "?lhs = ?rhs")
  1330 proof -
  1331   have "f ` A =
  1332       snd ` (SIGMA x : g ` A. f ` (g -` {x} \<inter> A))"
  1333       (is "_ = snd ` ?SIGMA")
  1334     unfolding image_split_eq_Sigma[symmetric]
  1335     by (simp add: image_compose[symmetric] comp_def)
  1336   moreover
  1337   have snd_inj: "inj_on snd ?SIGMA"
  1338     unfolding image_split_eq_Sigma[symmetric]
  1339     by (auto intro!: inj_onI subvimageD[OF svi])
  1340   ultimately
  1341   have "(\<Sum>x\<in>f`A. h x) = (\<Sum>(x,y)\<in>?SIGMA. h y)"
  1342     by (auto simp: setsum_reindex intro: setsum_cong)
  1343   also have "... = ?rhs"
  1344     using subvimage_finite[OF svi fin] fin
  1345     apply (subst setsum_Sigma[symmetric])
  1346     by (auto intro!: finite_subset[of _ "f`A"])
  1347   finally show ?thesis .
  1348 qed
  1349 
  1350 lemma (in information_space) entropy_partition:
  1351   assumes sf: "simple_function M X" "simple_function M P"
  1352   assumes svi: "subvimage (space M) X P"
  1353   shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
  1354 proof -
  1355   let "?XP x p" = "joint_distribution X P {(x, p)}"
  1356   let "?X x" = "distribution X {x}"
  1357   let "?P p" = "distribution P {p}"
  1358   note fX = sf(1)[THEN simple_function_imp_finite_random_variable]
  1359   note fP = sf(2)[THEN simple_function_imp_finite_random_variable]
  1360   note finite_distribution_order[OF fX fP, simp]
  1361   have "(\<Sum>x\<in>X ` space M. ?X x * log b (?X x)) =
  1362     (\<Sum>y\<in>P `space M. \<Sum>x\<in>X ` space M. ?XP x y * log b (?XP x y))"
  1363   proof (subst setsum_image_split[OF svi],
  1364       safe intro!: setsum_mono_zero_cong_left imageI)
  1365     show "finite (X ` space M)" "finite (X ` space M)" "finite (P ` space M)"
  1366       using sf unfolding simple_function_def by auto
  1367   next
  1368     fix p x assume in_space: "p \<in> space M" "x \<in> space M"
  1369     assume "?XP (X x) (P p) * log b (?XP (X x) (P p)) \<noteq> 0"
  1370     hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M \<noteq> {}" by (auto simp: distribution_def)
  1371     with svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
  1372     show "x \<in> P -` {P p}" by auto
  1373   next
  1374     fix p x assume in_space: "p \<in> space M" "x \<in> space M"
  1375     assume "P x = P p"
  1376     from this[symmetric] svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
  1377     have "X -` {X x} \<inter> space M \<subseteq> P -` {P p} \<inter> space M"
  1378       by auto
  1379     hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M = X -` {X x} \<inter> space M"
  1380       by auto
  1381     thus "?X (X x) * log b (?X (X x)) = ?XP (X x) (P p) * log b (?XP (X x) (P p))"
  1382       by (auto simp: distribution_def)
  1383   qed
  1384   moreover have "\<And>x y. ?XP x y * log b (?XP x y / ?P y) =
  1385       ?XP x y * log b (?XP x y) - ?XP x y * log b (?P y)"
  1386     by (auto simp add: log_simps zero_less_mult_iff field_simps)
  1387   ultimately show ?thesis
  1388     unfolding sf[THEN entropy_eq] conditional_entropy_eq[OF sf]
  1389     using setsum_joint_distribution_singleton[OF fX fP]
  1390     by (simp add: setsum_cartesian_product' setsum_subtractf setsum_distribution
  1391       setsum_left_distrib[symmetric] setsum_commute[where B="P`space M"])
  1392 qed
  1393 
  1394 corollary (in information_space) entropy_data_processing:
  1395   assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
  1396 proof -
  1397   note X
  1398   moreover have fX: "simple_function M (f \<circ> X)" using X by auto
  1399   moreover have "subvimage (space M) X (f \<circ> X)" by auto
  1400   ultimately have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
  1401   then show "\<H>(f \<circ> X) \<le> \<H>(X)"
  1402     by (auto intro: conditional_entropy_positive[OF X fX])
  1403 qed
  1404 
  1405 corollary (in information_space) entropy_of_inj:
  1406   assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
  1407   shows "\<H>(f \<circ> X) = \<H>(X)"
  1408 proof (rule antisym)
  1409   show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
  1410 next
  1411   have sf: "simple_function M (f \<circ> X)"
  1412     using X by auto
  1413   have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
  1414     by (auto intro!: mutual_information_cong simp: entropy_def the_inv_into_f_f[OF inj])
  1415   also have "... \<le> \<H>(f \<circ> X)"
  1416     using entropy_data_processing[OF sf] .
  1417   finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
  1418 qed
  1419 
  1420 end