src/HOL/Probability/Information.thy
 author hoelzl Mon May 03 14:35:10 2010 +0200 (2010-05-03) changeset 36623 d26348b667f2 parent 36080 0d9affa4e73c child 36624 25153c08655e permissions -rw-r--r--
Moved Convex theory to library.
```     1 theory Information
```
```     2 imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex"
```
```     3 begin
```
```     4
```
```     5 lemma pos_neg_part_abs:
```
```     6   fixes f :: "'a \<Rightarrow> real"
```
```     7   shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
```
```     8 unfolding real_abs_def pos_part_def neg_part_def by auto
```
```     9
```
```    10 lemma pos_part_abs:
```
```    11   fixes f :: "'a \<Rightarrow> real"
```
```    12   shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
```
```    13 unfolding pos_part_def real_abs_def by auto
```
```    14
```
```    15 lemma neg_part_abs:
```
```    16   fixes f :: "'a \<Rightarrow> real"
```
```    17   shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
```
```    18 unfolding neg_part_def real_abs_def by auto
```
```    19
```
```    20 lemma (in measure_space) int_abs:
```
```    21   assumes "integrable f"
```
```    22   shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
```
```    23 using assms
```
```    24 proof -
```
```    25   from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"
```
```    26     unfolding integrable_def by auto
```
```    27   hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"
```
```    28     using nnfis_add by auto
```
```    29   hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp
```
```    30   thus ?thesis unfolding integrable_def
```
```    31     using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]
```
```    32       ext[OF neg_part_abs[of f], of "\<lambda> y. y"]
```
```    33     using nnfis_0 by auto
```
```    34 qed
```
```    35
```
```    36 lemma (in measure_space) measure_mono:
```
```    37   assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
```
```    38   shows "measure M a \<le> measure M b"
```
```    39 proof -
```
```    40   have "b = a \<union> (b - a)" using assms by auto
```
```    41   moreover have "{} = a \<inter> (b - a)" by auto
```
```    42   ultimately have "measure M b = measure M a + measure M (b - a)"
```
```    43     using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
```
```    44   moreover have "measure M (b - a) \<ge> 0" using positive assms by auto
```
```    45   ultimately show "measure M a \<le> measure M b" by auto
```
```    46 qed
```
```    47
```
```    48 lemma (in measure_space) integral_0:
```
```    49   fixes f :: "'a \<Rightarrow> real"
```
```    50   assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"
```
```    51   shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"
```
```    52 proof -
```
```    53   have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto
```
```    54   moreover
```
```    55   { fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"
```
```    56     hence "\<bar> f y \<bar> > 0" by auto
```
```    57     hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"
```
```    58       using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto
```
```    59     hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
```
```    60       by auto }
```
```    61   moreover
```
```    62   { fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
```
```    63     then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto
```
```    64     hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto
```
```    65     hence "\<bar>f y\<bar> > 0"
```
```    66       using real_of_nat_Suc_gt_zero
```
```    67         positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp
```
```    68     hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }
```
```    69   ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
```
```    70     by blast
```
```    71   { fix n
```
```    72     have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using int_abs assms by auto
```
```    73     have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M)
```
```    74            \<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"
```
```    75       using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto
```
```    76     hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"
```
```    77       using assms unfolding nonneg_def by auto
```
```    78     have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
```
```    79       apply (subst Int_commute) unfolding Int_def
```
```    80       using borel[unfolded borel_measurable_ge_iff] by simp
```
```    81     hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>
```
```    82       {x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
```
```    83       using positive le0 unfolding atLeast_def by fastsimp }
```
```    84   moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"
```
```    85     by auto
```
```    86   moreover
```
```    87   { fix n
```
```    88     have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"
```
```    89       using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp
```
```    90     hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)
```
```    91     hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M
```
```    92          \<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }
```
```    93   ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"
```
```    94     using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]
```
```    95     unfolding o_def by (simp del: of_nat_Suc)
```
```    96   hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"
```
```    97     using LIMSEQ_const[of 0] LIMSEQ_unique by simp
```
```    98   hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"
```
```    99     using assms unfolding nonneg_def by auto
```
```   100   thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp
```
```   101 qed
```
```   102
```
```   103 definition
```
```   104   "KL_divergence b M u v =
```
```   105     measure_space.integral (M\<lparr>measure := u\<rparr>)
```
```   106                            (\<lambda>x. log b ((measure_space.RN_deriv (M \<lparr>measure := v\<rparr> ) u) x))"
```
```   107
```
```   108 lemma (in finite_prob_space) finite_measure_space:
```
```   109   shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
```
```   110     (is "finite_measure_space ?S")
```
```   111 proof (rule finite_Pow_additivity_sufficient, simp_all)
```
```   112   show "finite (X ` space M)" using finite_space by simp
```
```   113
```
```   114   show "positive ?S (distribution X)" unfolding distribution_def
```
```   115     unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto
```
```   116
```
```   117   show "additive ?S (distribution X)" unfolding additive_def distribution_def
```
```   118   proof (simp, safe)
```
```   119     fix x y
```
```   120     have x: "(X -` x) \<inter> space M \<in> sets M"
```
```   121       and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
```
```   122     assume "x \<inter> y = {}"
```
```   123     from additive[unfolded additive_def, rule_format, OF x y] this
```
```   124     have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) =
```
```   125       prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)"
```
```   126       apply (subst Int_Un_distrib2)
```
```   127       by auto
```
```   128     thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)"
```
```   129       by auto
```
```   130   qed
```
```   131 qed
```
```   132
```
```   133 lemma (in finite_prob_space) finite_prob_space:
```
```   134   "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
```
```   135   (is "finite_prob_space ?S")
```
```   136   unfolding finite_prob_space_def prob_space_def prob_space_axioms_def
```
```   137 proof safe
```
```   138   show "finite_measure_space ?S" by (rule finite_measure_space)
```
```   139   thus "measure_space ?S" by (simp add: finite_measure_space_def)
```
```   140
```
```   141   have "X -` X ` space M \<inter> space M = space M" by auto
```
```   142   thus "measure ?S (space ?S) = 1"
```
```   143     by (simp add: distribution_def prob_space)
```
```   144 qed
```
```   145
```
```   146 lemma (in finite_prob_space) finite_measure_space_image_prod:
```
```   147   "finite_measure_space \<lparr>space = X ` space M \<times> Y ` space M,
```
```   148     sets = Pow (X ` space M \<times> Y ` space M), measure_space.measure = distribution (\<lambda>x. (X x, Y x))\<rparr>"
```
```   149   (is "finite_measure_space ?Z")
```
```   150 proof (rule finite_Pow_additivity_sufficient, simp_all)
```
```   151   show "finite (X ` space M \<times> Y ` space M)" using finite_space by simp
```
```   152
```
```   153   let ?d = "distribution (\<lambda>x. (X x, Y x))"
```
```   154
```
```   155   show "positive ?Z ?d"
```
```   156     using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
```
```   157
```
```   158   show "additive ?Z ?d" unfolding additive_def
```
```   159   proof safe
```
```   160     fix x y assume "x \<in> sets ?Z" and "y \<in> sets ?Z"
```
```   161     assume "x \<inter> y = {}"
```
```   162     thus "?d (x \<union> y) = ?d x + ?d y"
```
```   163       apply (simp add: distribution_def)
```
```   164       apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
```
```   165       by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
```
```   166   qed
```
```   167 qed
```
```   168
```
```   169 definition (in prob_space)
```
```   170   "mutual_information b s1 s2 X Y \<equiv>
```
```   171     let prod_space =
```
```   172       prod_measure_space (\<lparr>space = space s1, sets = sets s1, measure = distribution X\<rparr>)
```
```   173                          (\<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr>)
```
```   174     in
```
```   175       KL_divergence b prod_space (joint_distribution X Y) (measure prod_space)"
```
```   176
```
```   177 abbreviation (in finite_prob_space)
```
```   178   finite_mutual_information ("\<I>\<^bsub>_\<^esub>'(_ ; _')") where
```
```   179   "\<I>\<^bsub>b\<^esub>(X ; Y) \<equiv> mutual_information b
```
```   180     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
```
```   181     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
```
```   182
```
```   183 abbreviation (in finite_prob_space)
```
```   184   finite_mutual_information_2 :: "('a \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd) \<Rightarrow> real" ("\<I>'(_ ; _')") where
```
```   185   "\<I>(X ; Y) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y)"
```
```   186
```
```   187 lemma (in prob_space) mutual_information_cong:
```
```   188   assumes [simp]: "space S1 = space S3" "sets S1 = sets S3"
```
```   189     "space S2 = space S4" "sets S2 = sets S4"
```
```   190   shows "mutual_information b S1 S2 X Y = mutual_information b S3 S4 X Y"
```
```   191   unfolding mutual_information_def by simp
```
```   192
```
```   193 lemma (in prob_space) joint_distribution:
```
```   194   "joint_distribution X Y = distribution (\<lambda>x. (X x, Y x))"
```
```   195   unfolding joint_distribution_def_raw distribution_def_raw ..
```
```   196
```
```   197 lemma (in finite_prob_space) finite_mutual_information_reduce:
```
```   198   "\<I>\<^bsub>b\<^esub>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
```
```   199     distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /
```
```   200                                                    (distribution X {x} * distribution Y {y})))"
```
```   201   (is "_ = setsum ?log ?prod")
```
```   202   unfolding Let_def mutual_information_def KL_divergence_def
```
```   203 proof (subst finite_measure_space.integral_finite_singleton, simp_all add: joint_distribution)
```
```   204   let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure_space.measure = distribution X\<rparr>"
```
```   205   let ?Y = "\<lparr>space = Y ` space M, sets = Pow (Y ` space M), measure_space.measure = distribution Y\<rparr>"
```
```   206   let ?P = "prod_measure_space ?X ?Y"
```
```   207
```
```   208   interpret X: finite_measure_space "?X" by (rule finite_measure_space)
```
```   209   moreover interpret Y: finite_measure_space "?Y" by (rule finite_measure_space)
```
```   210   ultimately have ms_X: "measure_space ?X" and ms_Y: "measure_space ?Y" by unfold_locales
```
```   211
```
```   212   interpret P: finite_measure_space "?P" by (rule finite_measure_space_finite_prod_measure) (fact+)
```
```   213
```
```   214   let ?P' = "measure_update (\<lambda>_. distribution (\<lambda>x. (X x, Y x))) ?P"
```
```   215   from finite_measure_space_image_prod[of X Y]
```
```   216     sigma_prod_sets_finite[OF X.finite_space Y.finite_space]
```
```   217   show "finite_measure_space ?P'"
```
```   218     by (simp add: X.sets_eq_Pow Y.sets_eq_Pow joint_distribution finite_measure_space_def prod_measure_space_def)
```
```   219
```
```   220   show "(\<Sum>x \<in> space ?P. log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x})
```
```   221     = setsum ?log ?prod"
```
```   222   proof (rule setsum_cong)
```
```   223     show "space ?P = ?prod" unfolding prod_measure_space_def by simp
```
```   224   next
```
```   225     fix x assume x: "x \<in> X ` space M \<times> Y ` space M"
```
```   226     then obtain d e where x_Pair: "x = (d, e)"
```
```   227       and d: "d \<in> X ` space M"
```
```   228       and e: "e \<in> Y ` space M" by auto
```
```   229
```
```   230     { fix x assume m_0: "measure ?P {x} = 0"
```
```   231       have "distribution (\<lambda>x. (X x, Y x)) {x} = 0"
```
```   232       proof (cases x)
```
```   233         case (Pair a b)
```
```   234         hence "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = (X -` {a} \<inter> space M) \<inter> (Y -` {b} \<inter> space M)"
```
```   235           and x_prod: "{x} = {a} \<times> {b}" by auto
```
```   236
```
```   237         let ?PROD = "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M"
```
```   238
```
```   239         show ?thesis
```
```   240         proof (cases "{a} \<subseteq> X ` space M \<and> {b} \<subseteq> Y ` space M")
```
```   241           case False
```
```   242           hence "?PROD = {}"
```
```   243             unfolding Pair by auto
```
```   244           thus ?thesis by (auto simp: distribution_def)
```
```   245         next
```
```   246           have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
```
```   247             using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
```
```   248
```
```   249           case True
```
```   250           with prod_measure_times[OF ms_X ms_Y, simplified, of "{a}" "{b}"]
```
```   251           have "prob (X -` {a} \<inter> space M) = 0 \<or> prob (Y -` {b} \<inter> space M) = 0" (is "?X_0 \<or> ?Y_0") using m_0
```
```   252             by (simp add: prod_measure_space_def distribution_def Pair)
```
```   253           thus ?thesis
```
```   254           proof (rule disjE)
```
```   255             assume ?X_0
```
```   256             have "prob ?PROD \<le> prob (X -` {a} \<inter> space M)"
```
```   257               using sets_eq_Pow Pair by (auto intro!: measure_mono)
```
```   258             thus ?thesis using `?X_0` by (auto simp: distribution_def)
```
```   259           next
```
```   260             assume ?Y_0
```
```   261             have "prob ?PROD \<le> prob (Y -` {b} \<inter> space M)"
```
```   262               using sets_eq_Pow Pair by (auto intro!: measure_mono)
```
```   263             thus ?thesis using `?Y_0` by (auto simp: distribution_def)
```
```   264           qed
```
```   265         qed
```
```   266       qed }
```
```   267     note measure_zero_joint_distribution = this
```
```   268
```
```   269     show "log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x} = ?log x"
```
```   270     apply (cases "distribution (\<lambda>x. (X x, Y x)) {x} \<noteq> 0")
```
```   271     apply (subst P.RN_deriv_finite_singleton)
```
```   272     proof (simp_all add: x_Pair)
```
```   273       from `finite_measure_space ?P'` show "measure_space ?P'" by (simp add: finite_measure_space_def)
```
```   274     next
```
```   275       fix x assume m_0: "measure ?P {x} = 0" thus "distribution (\<lambda>x. (X x, Y x)) {x} = 0" by fact
```
```   276     next
```
```   277       show "(d,e) \<in> space ?P" unfolding prod_measure_space_def using x x_Pair by simp
```
```   278     next
```
```   279       assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
```
```   280       show "measure ?P {(d,e)} \<noteq> 0"
```
```   281       proof
```
```   282         assume "measure ?P {(d,e)} = 0"
```
```   283         from measure_zero_joint_distribution[OF this] jd_0
```
```   284         show False by simp
```
```   285       qed
```
```   286     next
```
```   287       assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
```
```   288       with prod_measure_times[OF ms_X ms_Y, simplified, of "{d}" "{e}"] d
```
```   289       show "log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / measure ?P {(d, e)}) =
```
```   290         log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / (distribution X {d} * distribution Y {e}))"
```
```   291         by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
```
```   292     qed
```
```   293   qed
```
```   294 qed
```
```   295
```
```   296 lemma (in finite_prob_space) distribution_log_split:
```
```   297   assumes "1 < b"
```
```   298   shows
```
```   299   "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
```
```   300                                                      (distribution X {X x} * distribution Z {z})) =
```
```   301    distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
```
```   302                                                      distribution Z {z}) -
```
```   303    distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution X {X x})"
```
```   304   (is "?lhs = ?rhs")
```
```   305 proof (cases "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} = 0")
```
```   306   case True thus ?thesis by simp
```
```   307 next
```
```   308   case False
```
```   309
```
```   310   let ?dZ = "distribution Z"
```
```   311   let ?dX = "distribution X"
```
```   312   let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
```
```   313
```
```   314   have dist_nneg: "\<And>x X. 0 \<le> distribution X x"
```
```   315     unfolding distribution_def using sets_eq_Pow by (auto intro: positive)
```
```   316
```
```   317   have "?lhs = ?dXZ {(X x, z)} * (log b (?dXZ {(X x, z)} / ?dZ {z}) - log b (?dX {X x}))"
```
```   318   proof -
```
```   319     have pos_dXZ: "0 < ?dXZ {(X x, z)}"
```
```   320       using False dist_nneg[of "\<lambda>x. (X x, Z x)" "{(X x, z)}"] by auto
```
```   321     moreover
```
```   322     have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (X -` {X x}) \<inter> space M" by auto
```
```   323     hence "?dXZ {(X x, z)} \<le> ?dX {X x}"
```
```   324       unfolding distribution_def
```
```   325       by (rule measure_mono) (simp_all add: sets_eq_Pow)
```
```   326     with pos_dXZ have "0 < ?dX {X x}" by (rule less_le_trans)
```
```   327     moreover
```
```   328     have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (Z -` {z}) \<inter> space M" by auto
```
```   329     hence "?dXZ {(X x, z)} \<le> ?dZ {z}"
```
```   330       unfolding distribution_def
```
```   331       by (rule measure_mono) (simp_all add: sets_eq_Pow)
```
```   332     with pos_dXZ have "0 < ?dZ {z}" by (rule less_le_trans)
```
```   333     moreover have "0 < b" by (rule less_trans[OF _ `1 < b`]) simp
```
```   334     moreover have "b \<noteq> 1" by (rule ccontr) (insert `1 < b`, simp)
```
```   335     ultimately show ?thesis
```
```   336       using pos_dXZ
```
```   337       apply (subst (2) mult_commute)
```
```   338       apply (subst divide_divide_eq_left[symmetric])
```
```   339       apply (subst log_divide)
```
```   340       by (auto intro: divide_pos_pos)
```
```   341   qed
```
```   342   also have "... = ?rhs"
```
```   343     by (simp add: field_simps)
```
```   344   finally show ?thesis .
```
```   345 qed
```
```   346
```
```   347 lemma (in finite_prob_space) finite_mutual_information_reduce_prod:
```
```   348   "mutual_information b
```
```   349     \<lparr> space = X ` space M, sets = Pow (X ` space M) \<rparr>
```
```   350     \<lparr> space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M) \<rparr>
```
```   351     X (\<lambda>x. (Y x,Z x)) =
```
```   352     (\<Sum> (x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.
```
```   353       distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} *
```
```   354       log b (distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} /
```
```   355               (distribution X {x} * distribution (\<lambda>x. (Y x,Z x)) {(y,z)})))" (is "_ = setsum ?log ?space")
```
```   356   unfolding Let_def mutual_information_def KL_divergence_def using finite_space
```
```   357 proof (subst finite_measure_space.integral_finite_singleton,
```
```   358        simp_all add: prod_measure_space_def sigma_prod_sets_finite joint_distribution)
```
```   359   let ?sets = "Pow (X ` space M \<times> Y ` space M \<times> Z ` space M)"
```
```   360     and ?measure = "distribution (\<lambda>x. (X x, Y x, Z x))"
```
```   361   let ?P = "\<lparr> space = ?space, sets = ?sets, measure = ?measure\<rparr>"
```
```   362
```
```   363   show "finite_measure_space ?P"
```
```   364   proof (rule finite_Pow_additivity_sufficient, simp_all)
```
```   365     show "finite ?space" using finite_space by auto
```
```   366
```
```   367     show "positive ?P ?measure"
```
```   368       using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
```
```   369
```
```   370     show "additive ?P ?measure"
```
```   371     proof (simp add: additive_def distribution_def, safe)
```
```   372       fix x y assume "x \<subseteq> ?space" and "y \<subseteq> ?space"
```
```   373       assume "x \<inter> y = {}"
```
```   374       thus "prob (((\<lambda>x. (X x, Y x, Z x)) -` x \<union> (\<lambda>x. (X x, Y x, Z x)) -` y) \<inter> space M) =
```
```   375             prob ((\<lambda>x. (X x, Y x, Z x)) -` x \<inter> space M) + prob ((\<lambda>x. (X x, Y x, Z x)) -` y \<inter> space M)"
```
```   376         apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
```
```   377         by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
```
```   378     qed
```
```   379   qed
```
```   380
```
```   381   let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
```
```   382   and ?YZ = "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M), measure = distribution (\<lambda>x. (Y x, Z x))\<rparr>"
```
```   383   let ?u = "prod_measure ?X ?YZ"
```
```   384
```
```   385   from finite_measure_space[of X] finite_measure_space_image_prod[of Y Z]
```
```   386   have ms_X: "measure_space ?X" and ms_YZ: "measure_space ?YZ"
```
```   387     by (simp_all add: finite_measure_space_def)
```
```   388
```
```   389   show "(\<Sum>x \<in> ?space. log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
```
```   390     (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x})
```
```   391     = setsum ?log ?space"
```
```   392   proof (rule setsum_cong)
```
```   393     fix x assume x: "x \<in> ?space"
```
```   394     then obtain d e f where x_Pair: "x = (d, e, f)"
```
```   395       and d: "d \<in> X ` space M"
```
```   396       and e: "e \<in> Y ` space M"
```
```   397       and f: "f \<in> Z ` space M" by auto
```
```   398
```
```   399     { fix x assume m_0: "?u {x} = 0"
```
```   400
```
```   401       let ?PROD = "(\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M"
```
```   402       obtain a b c where Pair: "x = (a, b, c)" by (cases x)
```
```   403       hence "?PROD = (X -` {a} \<inter> space M) \<inter> ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M)"
```
```   404         and x_prod: "{x} = {a} \<times> {(b, c)}" by auto
```
```   405
```
```   406       have "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0"
```
```   407       proof (cases "{a} \<subseteq> X ` space M")
```
```   408         case False
```
```   409         hence "?PROD = {}"
```
```   410           unfolding Pair by auto
```
```   411         thus ?thesis by (auto simp: distribution_def)
```
```   412       next
```
```   413         have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
```
```   414           using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
```
```   415
```
```   416         case True
```
```   417         with prod_measure_times[OF ms_X ms_YZ, simplified, of "{a}" "{(b,c)}"]
```
```   418         have "prob (X -` {a} \<inter> space M) = 0 \<or> prob ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M) = 0"
```
```   419           (is "prob ?X = 0 \<or> prob ?Y = 0") using m_0
```
```   420           by (simp add: prod_measure_space_def distribution_def Pair)
```
```   421         thus ?thesis
```
```   422         proof (rule disjE)
```
```   423           assume "prob ?X = 0"
```
```   424           have "prob ?PROD \<le> prob ?X"
```
```   425             using sets_eq_Pow Pair by (auto intro!: measure_mono)
```
```   426           thus ?thesis using `prob ?X = 0` by (auto simp: distribution_def)
```
```   427         next
```
```   428           assume "prob ?Y = 0"
```
```   429           have "prob ?PROD \<le> prob ?Y"
```
```   430             using sets_eq_Pow Pair by (auto intro!: measure_mono)
```
```   431           thus ?thesis using `prob ?Y = 0` by (auto simp: distribution_def)
```
```   432         qed
```
```   433       qed }
```
```   434     note measure_zero_joint_distribution = this
```
```   435
```
```   436     from x_Pair d e f finite_space
```
```   437     show "log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
```
```   438       (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x} = ?log x"
```
```   439     apply (cases "distribution (\<lambda>x. (X x, Y x, Z x)) {x} \<noteq> 0")
```
```   440     apply (subst finite_measure_space.RN_deriv_finite_singleton)
```
```   441     proof simp_all
```
```   442       show "measure_space ?P" using `finite_measure_space ?P` by (simp add: finite_measure_space_def)
```
```   443
```
```   444       from finite_measure_space_finite_prod_measure[OF finite_measure_space[of X]
```
```   445         finite_measure_space_image_prod[of Y Z]] finite_space
```
```   446       show "finite_measure_space \<lparr>space=?space, sets=?sets, measure=?u\<rparr>"
```
```   447         by (simp add: prod_measure_space_def sigma_prod_sets_finite)
```
```   448     next
```
```   449       fix x assume "?u {x} = 0" thus "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0" by fact
```
```   450     next
```
```   451       assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
```
```   452       show "?u {(d,e,f)} \<noteq> 0"
```
```   453       proof
```
```   454         assume "?u {(d, e, f)} = 0"
```
```   455         from measure_zero_joint_distribution[OF this] jd_0
```
```   456         show False by simp
```
```   457       qed
```
```   458     next
```
```   459       assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
```
```   460       with prod_measure_times[OF ms_X ms_YZ, simplified, of "{d}" "{(e,f)}"] d
```
```   461       show "log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / ?u {(d, e, f)}) =
```
```   462         log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / (distribution X {d} * distribution (\<lambda>x. (Y x, Z x)) {(e,f)}))"
```
```   463         by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
```
```   464     qed
```
```   465   qed simp
```
```   466 qed
```
```   467
```
```   468 definition (in prob_space)
```
```   469   "entropy b s X = mutual_information b s s X X"
```
```   470
```
```   471 abbreviation (in finite_prob_space)
```
```   472   finite_entropy ("\<H>\<^bsub>_\<^esub>'(_')") where
```
```   473   "\<H>\<^bsub>b\<^esub>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
```
```   474
```
```   475 abbreviation (in finite_prob_space)
```
```   476   finite_entropy_2 ("\<H>'(_')") where
```
```   477   "\<H>(X) \<equiv> \<H>\<^bsub>2\<^esub>(X)"
```
```   478
```
```   479 lemma (in finite_prob_space) finite_entropy_reduce:
```
```   480   assumes "1 < b"
```
```   481   shows "\<H>\<^bsub>b\<^esub>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
```
```   482 proof -
```
```   483   have fin: "finite (X ` space M)" using finite_space by simp
```
```   484
```
```   485   have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
```
```   486
```
```   487   { fix x y
```
```   488     have "(\<lambda>x. (X x, X x)) -` {(x, y)} = (if x = y then X -` {x} else {})" by auto
```
```   489     hence "distribution (\<lambda>x. (X x, X x))  {(x,y)} = (if x = y then distribution X {x} else 0)"
```
```   490       unfolding distribution_def by auto }
```
```   491   moreover
```
```   492   have "\<And>x. 0 \<le> distribution X x"
```
```   493     unfolding distribution_def using finite_space sets_eq_Pow by (auto intro: positive)
```
```   494   hence "\<And>x. distribution X x \<noteq> 0 \<Longrightarrow> 0 < distribution X x" by (auto simp: le_less)
```
```   495   ultimately
```
```   496   show ?thesis using `1 < b`
```
```   497     by (auto intro!: setsum_cong
```
```   498       simp: log_inverse If_mult_distr setsum_cases[OF fin] inverse_eq_divide[symmetric]
```
```   499         entropy_def setsum_negf[symmetric] joint_distribution finite_mutual_information_reduce
```
```   500         setsum_cartesian_product[symmetric])
```
```   501 qed
```
```   502
```
```   503 lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
```
```   504 proof (rule inj_onI, simp)
```
```   505   fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
```
```   506   show "x = y"
```
```   507   proof (cases rule: linorder_cases)
```
```   508     assume "x < y" hence "log b x < log b y"
```
```   509       using log_less_cancel_iff[OF `1 < b`] pos by simp
```
```   510     thus ?thesis using * by simp
```
```   511   next
```
```   512     assume "y < x" hence "log b y < log b x"
```
```   513       using log_less_cancel_iff[OF `1 < b`] pos by simp
```
```   514     thus ?thesis using * by simp
```
```   515   qed simp
```
```   516 qed
```
```   517
```
```   518 definition (in prob_space)
```
```   519   "conditional_mutual_information b s1 s2 s3 X Y Z \<equiv>
```
```   520     let prod_space =
```
```   521       prod_measure_space \<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr>
```
```   522                          \<lparr>space = space s3, sets = sets s3, measure = distribution Z\<rparr>
```
```   523     in
```
```   524       mutual_information b s1 prod_space X (\<lambda>x. (Y x, Z x)) -
```
```   525       mutual_information b s1 s3 X Z"
```
```   526
```
```   527 abbreviation (in finite_prob_space)
```
```   528   finite_conditional_mutual_information ("\<I>\<^bsub>_\<^esub>'( _ ; _ | _ ')") where
```
```   529   "\<I>\<^bsub>b\<^esub>(X ; Y | Z) \<equiv> conditional_mutual_information b
```
```   530     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
```
```   531     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr>
```
```   532     \<lparr> space = Z`space M, sets = Pow (Z`space M) \<rparr>
```
```   533     X Y Z"
```
```   534
```
```   535 abbreviation (in finite_prob_space)
```
```   536   finite_conditional_mutual_information_2 ("\<I>'( _ ; _ | _ ')") where
```
```   537   "\<I>(X ; Y | Z) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y | Z)"
```
```   538
```
```   539 lemma image_pair_eq_Sigma:
```
```   540   "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
```
```   541 proof (safe intro!: imageI vimageI, simp_all)
```
```   542   fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
```
```   543   show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" unfolding eq[symmetric]
```
```   544     using * by auto
```
```   545 qed
```
```   546
```
```   547 lemma inj_on_swap: "inj_on (\<lambda>(x,y). (y,x)) A" by (auto intro!: inj_onI)
```
```   548
```
```   549 lemma (in finite_prob_space) finite_conditional_mutual_information_reduce:
```
```   550   assumes "1 < b"
```
```   551   shows "\<I>\<^bsub>b\<^esub>(X ; Y | Z) =
```
```   552 	- (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
```
```   553              distribution (\<lambda>x. (X x, Z x)) {(x,z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(x,z)} / distribution Z {z}))
```
```   554 	+ (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
```
```   555              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
```
```   556              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}/
```
```   557              distribution (\<lambda>x. (Y x, Z x)) {(y, z)}))" (is "_ = ?rhs")
```
```   558 unfolding conditional_mutual_information_def Let_def using finite_space
```
```   559 apply (simp add: prod_measure_space_def sigma_prod_sets_finite)
```
```   560 apply (subst mutual_information_cong[of _ "\<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
```
```   561   _ "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M)\<rparr>"], simp_all)
```
```   562 apply (subst finite_mutual_information_reduce_prod, simp_all)
```
```   563 apply (subst finite_mutual_information_reduce, simp_all)
```
```   564 proof -
```
```   565   let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))"
```
```   566   let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
```
```   567   let ?dYZ = "distribution (\<lambda>x. (Y x, Z x))"
```
```   568   let ?dX = "distribution X"
```
```   569   let ?dY = "distribution Y"
```
```   570   let ?dZ = "distribution Z"
```
```   571
```
```   572   have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
```
```   573   { fix x y
```
```   574     have "(\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M =
```
```   575       (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then (\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M else {})" by auto
```
```   576     hence "?dXYZ {(X x, y)} = (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then ?dXYZ {(X x, y)} else 0)"
```
```   577       unfolding distribution_def by auto }
```
```   578   note split_measure = this
```
```   579
```
```   580   have sets: "Y ` space M \<times> Z ` space M \<inter> (\<lambda>x. (Y x, Z x)) ` space M = (\<lambda>x. (Y x, Z x)) ` space M" by auto
```
```   581
```
```   582   have cong: "\<And>A B C D. \<lbrakk> A = C ; B = D \<rbrakk> \<Longrightarrow> A + B = C + D" by auto
```
```   583
```
```   584   { fix A f have "setsum f A = setsum (\<lambda>(x, y). f (y, x)) ((\<lambda>(x, y). (y, x)) ` A)"
```
```   585     using setsum_reindex[OF inj_on_swap, of "\<lambda>(x, y). f (y, x)" A] by (simp add: split_twice) }
```
```   586   note setsum_reindex_swap = this
```
```   587
```
```   588   { fix A B f assume *: "finite A" "\<forall>x\<in>A. finite (B x)"
```
```   589     have "(\<Sum>x\<in>Sigma A B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) (B x))"
```
```   590       unfolding setsum_Sigma[OF *] by simp }
```
```   591   note setsum_Sigma = this
```
```   592
```
```   593   { fix x
```
```   594     have "(\<Sum>z\<in>Z ` space M. ?dXZ {(X x, z)}) = (\<Sum>yz\<in>(\<lambda>x. (Y x, Z x)) ` space M. ?dXYZ {(X x, yz)})"
```
```   595       apply (subst setsum_reindex_swap)
```
```   596       apply (simp add: image_image distribution_def)
```
```   597       unfolding image_pair_eq_Sigma
```
```   598       apply (subst setsum_Sigma)
```
```   599       using finite_space apply simp_all
```
```   600       apply (rule setsum_cong[OF refl])
```
```   601       apply (subst measure_finitely_additive'')
```
```   602       by (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) }
```
```   603
```
```   604   thus "(\<Sum>(x, y, z)\<in>X ` space M \<times> Y ` space M \<times> Z ` space M.
```
```   605       ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / (?dX {x} * ?dYZ {(y, z)}))) -
```
```   606     (\<Sum>(x, y)\<in>X ` space M \<times> Z ` space M.
```
```   607       ?dXZ {(x, y)} * log b (?dXZ {(x, y)} / (?dX {x} * ?dZ {y}))) =
```
```   608   - (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
```
```   609       ?dXZ {(x,z)} * log b (?dXZ {(x,z)} / ?dZ {z})) +
```
```   610     (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
```
```   611       ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / ?dYZ {(y, z)}))"
```
```   612     using finite_space
```
```   613     apply (auto simp: setsum_cartesian_product[symmetric] setsum_negf[symmetric]
```
```   614                       setsum_addf[symmetric] diff_minus
```
```   615       intro!: setsum_cong[OF refl])
```
```   616     apply (subst split_measure)
```
```   617     apply (simp add: If_mult_distr setsum_cases sets distribution_log_split[OF assms, of X])
```
```   618     apply (subst add_commute)
```
```   619     by (simp add: setsum_subtractf setsum_negf field_simps setsum_right_distrib[symmetric] sets_eq_Pow)
```
```   620 qed
```
```   621
```
```   622 definition (in prob_space)
```
```   623   "conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y"
```
```   624
```
```   625 abbreviation (in finite_prob_space)
```
```   626   finite_conditional_entropy ("\<H>\<^bsub>_\<^esub>'(_ | _')") where
```
```   627   "\<H>\<^bsub>b\<^esub>(X | Y) \<equiv> conditional_entropy b
```
```   628     \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
```
```   629     \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
```
```   630
```
```   631 abbreviation (in finite_prob_space)
```
```   632   finite_conditional_entropy_2 ("\<H>'(_ | _')") where
```
```   633   "\<H>(X | Y) \<equiv> \<H>\<^bsub>2\<^esub>(X | Y)"
```
```   634
```
```   635 lemma (in finite_prob_space) finite_conditional_entropy_reduce:
```
```   636   assumes "1 < b"
```
```   637   shows "\<H>\<^bsub>b\<^esub>(X | Z) =
```
```   638      - (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
```
```   639          joint_distribution X Z {(x, z)} *
```
```   640          log b (joint_distribution X Z {(x, z)} / distribution Z {z}))"
```
```   641 proof -
```
```   642   have *: "\<And>x y z. (\<lambda>x. (X x, X x, Z x)) -` {(x, y, z)} = (if x = y then (\<lambda>x. (X x, Z x)) -` {(x, z)} else {})" by auto
```
```   643   show ?thesis
```
```   644     unfolding finite_conditional_mutual_information_reduce[OF assms]
```
```   645       conditional_entropy_def joint_distribution_def distribution_def *
```
```   646     by (auto intro!: setsum_0')
```
```   647 qed
```
```   648
```
```   649 lemma (in finite_prob_space) finite_mutual_information_eq_entropy_conditional_entropy:
```
```   650   assumes "1 < b" shows "\<I>\<^bsub>b\<^esub>(X ; Z) = \<H>\<^bsub>b\<^esub>(X) - \<H>\<^bsub>b\<^esub>(X | Z)" (is "mutual_information b ?X ?Z X Z = _")
```
```   651   unfolding finite_mutual_information_reduce
```
```   652     finite_entropy_reduce[OF assms]
```
```   653     finite_conditional_entropy_reduce[OF assms]
```
```   654     joint_distribution diff_minus_eq_add
```
```   655   using finite_space
```
```   656   apply (auto simp add: setsum_addf[symmetric] setsum_subtractf
```
```   657       setsum_Sigma[symmetric] distribution_log_split[OF assms] setsum_negf[symmetric]
```
```   658     intro!: setsum_cong[OF refl])
```
```   659   apply (simp add: setsum_negf setsum_left_distrib[symmetric])
```
```   660 proof (rule disjI2)
```
```   661   let ?dX = "distribution X"
```
```   662   and ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
```
```   663
```
```   664   fix x assume "x \<in> space M"
```
```   665   have "\<And>z. (\<lambda>x. (X x, Z x)) -` {(X x, z)} \<inter> space M = (X -` {X x} \<inter> space M) \<inter> (Z -` {z} \<inter> space M)" by auto
```
```   666   thus "(\<Sum>z\<in>Z ` space M. distribution (\<lambda>x. (X x, Z x)) {(X x, z)}) = distribution X {X x}"
```
```   667     unfolding distribution_def
```
```   668     apply (subst prob_real_sum_image_fn[where e="X -` {X x} \<inter> space M" and s = "Z`space M" and f="\<lambda>z. Z -` {z} \<inter> space M"])
```
```   669     using finite_space sets_eq_Pow by auto
```
```   670 qed
```
```   671
```
```   672 (* -------------Entropy of a RV with a certain event is zero---------------- *)
```
```   673
```
```   674 lemma (in finite_prob_space) finite_entropy_certainty_eq_0:
```
```   675   assumes "x \<in> X ` space M" and "distribution X {x} = 1" and "b > 1"
```
```   676   shows "\<H>\<^bsub>b\<^esub>(X) = 0"
```
```   677 proof -
```
```   678   interpret X: finite_prob_space "\<lparr> space = X ` space M,
```
```   679     sets = Pow (X ` space M),
```
```   680     measure = distribution X\<rparr>" by (rule finite_prob_space)
```
```   681
```
```   682   have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"
```
```   683     using X.measure_compl[of "{x}"] assms by auto
```
```   684   also have "\<dots> = 0" using X.prob_space assms by auto
```
```   685   finally have X0: "distribution X (X ` space M - {x}) = 0" by auto
```
```   686
```
```   687   { fix y assume asm: "y \<noteq> x" "y \<in> X ` space M"
```
```   688     hence "{y} \<subseteq> X ` space M - {x}" by auto
```
```   689     from X.measure_mono[OF this] X0 X.positive[of "{y}"] asm
```
```   690     have "distribution X {y} = 0" by auto }
```
```   691
```
```   692   hence fi: "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = (if x = y then 1 else 0)"
```
```   693     using assms by auto
```
```   694
```
```   695   have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp
```
```   696
```
```   697   show ?thesis
```
```   698     unfolding finite_entropy_reduce[OF `b > 1`] by (auto simp: y fi)
```
```   699 qed
```
```   700 (* --------------- upper bound on entropy for a rv ------------------------- *)
```
```   701
```
```   702 lemma log_setsum:
```
```   703   assumes "finite s" "s \<noteq> {}"
```
```   704   assumes "b > 1"
```
```   705   assumes "(\<Sum> i \<in> s. a i) = 1"
```
```   706   assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
```
```   707   assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
```
```   708   shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
```
```   709 proof -
```
```   710   have "convex_on {0 <..} (\<lambda> x. - log b x)"
```
```   711     by (rule minus_log_convex[OF `b > 1`])
```
```   712   hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
```
```   713     using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastsimp
```
```   714   thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
```
```   715 qed
```
```   716
```
```   717 lemma (in finite_prob_space) finite_entropy_le_card:
```
```   718   assumes "1 < b"
```
```   719   shows "\<H>\<^bsub>b\<^esub>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
```
```   720 proof -
```
```   721   interpret X: finite_prob_space "\<lparr>space = X ` space M,
```
```   722                                     sets = Pow (X ` space M),
```
```   723                                  measure = distribution X\<rparr>"
```
```   724     using finite_prob_space by auto
```
```   725   have triv: "\<And> x. (if distribution X {x} \<noteq> 0 then distribution X {x} else 0) = distribution X {x}"
```
```   726     by auto
```
```   727   hence sum1: "(\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x}) = 1"
```
```   728     using X.measure_finitely_additive''[of "X ` space M" "\<lambda> x. {x}", simplified]
```
```   729       sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
```
```   730     unfolding disjoint_family_on_def  X.prob_space[symmetric]
```
```   731     using finite_imageI[OF finite_space, of X] by (auto simp add:triv setsum_restrict_set)
```
```   732   have pos: "\<And> x. x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0} \<Longrightarrow> inverse (distribution X {x}) > 0"
```
```   733     using X.positive sets_eq_Pow unfolding inverse_positive_iff_positive less_le by auto
```
```   734   { assume asm: "X ` space M \<inter> {y. distribution X {y} \<noteq> 0} = {}"
```
```   735     { fix x assume "x \<in> X ` space M"
```
```   736       hence "distribution X {x} = 0" using asm by blast }
```
```   737     hence A: "(\<Sum> x \<in> X ` space M. distribution X {x}) = 0" by auto
```
```   738     have B: "(\<Sum> x \<in> X ` space M. distribution X {x})
```
```   739       \<ge> (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x})"
```
```   740       using finite_imageI[OF finite_space, of X]
```
```   741       by (subst setsum_mono2) auto
```
```   742     from A B have "False" using sum1 by auto } note not_empty = this
```
```   743   { fix x assume asm: "x \<in> X ` space M"
```
```   744     have "- distribution X {x} * log b (distribution X {x})
```
```   745        = - (if distribution X {x} \<noteq> 0
```
```   746             then distribution X {x} * log b (distribution X {x})
```
```   747             else 0)"
```
```   748       by auto
```
```   749     also have "\<dots> = (if distribution X {x} \<noteq> 0
```
```   750           then distribution X {x} * - log b (distribution X {x})
```
```   751           else 0)"
```
```   752       by auto
```
```   753     also have "\<dots> = (if distribution X {x} \<noteq> 0
```
```   754                     then distribution X {x} * log b (inverse (distribution X {x}))
```
```   755                     else 0)"
```
```   756       using log_inverse `1 < b` X.positive[of "{x}"] asm by auto
```
```   757     finally have "- distribution X {x} * log b (distribution X {x})
```
```   758                  = (if distribution X {x} \<noteq> 0
```
```   759                     then distribution X {x} * log b (inverse (distribution X {x}))
```
```   760                     else 0)"
```
```   761       by auto } note log_inv = this
```
```   762   have "- (\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))
```
```   763        = (\<Sum> x \<in> X ` space M. (if distribution X {x} \<noteq> 0
```
```   764           then distribution X {x} * log b (inverse (distribution X {x}))
```
```   765           else 0))"
```
```   766     unfolding setsum_negf[symmetric] using log_inv by auto
```
```   767   also have "\<dots> = (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
```
```   768                           distribution X {x} * log b (inverse (distribution X {x})))"
```
```   769     unfolding setsum_restrict_set[OF finite_imageI[OF finite_space, of X]] by auto
```
```   770   also have "\<dots> \<le> log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
```
```   771                           distribution X {x} * (inverse (distribution X {x})))"
```
```   772     apply (subst log_setsum[OF _ _ `b > 1` sum1,
```
```   773      unfolded greaterThan_iff, OF _ _ _]) using pos sets_eq_Pow
```
```   774       X.finite_space assms X.positive not_empty by auto
```
```   775   also have "\<dots> = log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. 1)"
```
```   776     by auto
```
```   777   also have "\<dots> \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))"
```
```   778     by auto
```
```   779   finally have "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
```
```   780                \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" by simp
```
```   781   thus ?thesis unfolding finite_entropy_reduce[OF assms] real_eq_of_nat by auto
```
```   782 qed
```
```   783
```
```   784 (* --------------- entropy is maximal for a uniform rv --------------------- *)
```
```   785
```
```   786 lemma (in finite_prob_space) uniform_prob:
```
```   787   assumes "x \<in> space M"
```
```   788   assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}"
```
```   789   shows "prob {x} = 1 / real (card (space M))"
```
```   790 proof -
```
```   791   have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}"
```
```   792     using assms(2)[OF _ `x \<in> space M`] by blast
```
```   793   have "1 = prob (space M)"
```
```   794     using prob_space by auto
```
```   795   also have "\<dots> = (\<Sum> x \<in> space M. prob {x})"
```
```   796     using measure_finitely_additive''[of "space M" "\<lambda> x. {x}", simplified]
```
```   797       sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
```
```   798       finite_space unfolding disjoint_family_on_def  prob_space[symmetric]
```
```   799     by (auto simp add:setsum_restrict_set)
```
```   800   also have "\<dots> = (\<Sum> y \<in> space M. prob {x})"
```
```   801     using prob_x by auto
```
```   802   also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
```
```   803   finally have one: "1 = real (card (space M)) * prob {x}"
```
```   804     using real_eq_of_nat by auto
```
```   805   hence two: "real (card (space M)) \<noteq> 0" by fastsimp
```
```   806   from one have three: "prob {x} \<noteq> 0" by fastsimp
```
```   807   thus ?thesis using one two three divide_cancel_right
```
```   808     by (auto simp:field_simps)
```
```   809 qed
```
```   810
```
```   811 lemma (in finite_prob_space) finite_entropy_uniform_max:
```
```   812   assumes "b > 1"
```
```   813   assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
```
```   814   shows "\<H>\<^bsub>b\<^esub>(X) = log b (real (card (X ` space M)))"
```
```   815 proof -
```
```   816   interpret X: finite_prob_space "\<lparr>space = X ` space M,
```
```   817                                     sets = Pow (X ` space M),
```
```   818                                  measure = distribution X\<rparr>"
```
```   819     using finite_prob_space by auto
```
```   820   { fix x assume xasm: "x \<in> X ` space M"
```
```   821     hence card_gt0: "real (card (X ` space M)) > 0"
```
```   822       using card_gt_0_iff X.finite_space by auto
```
```   823     from xasm have "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = distribution X {x}"
```
```   824       using assms by blast
```
```   825     hence "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
```
```   826          = - (\<Sum> y \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
```
```   827       by auto
```
```   828     also have "\<dots> = - real_of_nat (card (X ` space M)) * distribution X {x} * log b (distribution X {x})"
```
```   829       by auto
```
```   830     also have "\<dots> = - real (card (X ` space M)) * (1 / real (card (X ` space M))) * log b (1 / real (card (X ` space M)))"
```
```   831       unfolding real_eq_of_nat[symmetric]
```
```   832       by (auto simp: X.uniform_prob[simplified, OF xasm assms(2)])
```
```   833     also have "\<dots> = log b (real (card (X ` space M)))"
```
```   834       unfolding inverse_eq_divide[symmetric]
```
```   835       using card_gt0 log_inverse `b > 1`
```
```   836       by (auto simp add:field_simps card_gt0)
```
```   837     finally have ?thesis
```
```   838       unfolding finite_entropy_reduce[OF `b > 1`] by auto }
```
```   839   moreover
```
```   840   { assume "X ` space M = {}"
```
```   841     hence "distribution X (X ` space M) = 0"
```
```   842       using X.empty_measure by simp
```
```   843     hence "False" using X.prob_space by auto }
```
```   844   ultimately show ?thesis by auto
```
```   845 qed
```
```   846
```
```   847 end
```