src/HOL/Probability/Information.thy
 author hoelzl Wed Apr 07 17:24:44 2010 +0200 (2010-04-07) changeset 36080 0d9affa4e73c child 36623 d26348b667f2 permissions -rw-r--r--
Added Information theory and Example: dining cryptographers
```     1 theory Information
```
```     2 imports Probability_Space Product_Measure
```
```     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 definition convex_set :: "real set \<Rightarrow> bool"
```
```   703 where
```
```   704   "convex_set C \<equiv> (\<forall> x y \<mu>. x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> \<mu> * x + (1 - \<mu>) * y \<in> C)"
```
```   705
```
```   706 lemma pos_is_convex:
```
```   707   shows "convex_set {0 <..}"
```
```   708 unfolding convex_set_def
```
```   709 proof safe
```
```   710   fix x y \<mu> :: real
```
```   711   assume asms: "\<mu> \<ge> 0" "\<mu> \<le> 1" "x > 0" "y > 0"
```
```   712   { assume "\<mu> = 0"
```
```   713     hence "\<mu> * x + (1 - \<mu>) * y = y" by simp
```
```   714     hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
```
```   715   moreover
```
```   716   { assume "\<mu> = 1"
```
```   717     hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
```
```   718   moreover
```
```   719   { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
```
```   720     hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
```
```   721     hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms
```
```   722       apply (subst add_nonneg_pos[of "\<mu> * x" "(1 - \<mu>) * y"])
```
```   723       using real_mult_order by auto fastsimp }
```
```   724   ultimately show "\<mu> * x + (1 - \<mu>) * y > 0" using assms by blast
```
```   725 qed
```
```   726
```
```   727 definition convex_fun :: "(real \<Rightarrow> real) \<Rightarrow> real set \<Rightarrow> bool"
```
```   728 where
```
```   729   "convex_fun f C \<equiv> (\<forall> x y \<mu>. convex_set C \<and> (x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1
```
```   730                    \<longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y))"
```
```   731
```
```   732 lemma pos_convex_function:
```
```   733   fixes f :: "real \<Rightarrow> real"
```
```   734   assumes "convex_set C"
```
```   735   assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
```
```   736   shows "convex_fun f C"
```
```   737 unfolding convex_fun_def
```
```   738 using assms
```
```   739 proof safe
```
```   740   fix x y \<mu> :: real
```
```   741   let ?x = "\<mu> * x + (1 - \<mu>) * y"
```
```   742   assume asm: "convex_set C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
```
```   743   hence "1 - \<mu> \<ge> 0" by auto
```
```   744   hence xpos: "?x \<in> C" using asm unfolding convex_set_def by auto
```
```   745   have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
```
```   746             \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
```
```   747     using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
```
```   748       mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
```
```   749   hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
```
```   750     by (auto simp add:field_simps)
```
```   751   thus "\<mu> * f x + (1 - \<mu>) * f y \<ge> f ?x" by simp
```
```   752 qed
```
```   753
```
```   754 lemma atMostAtLeast_subset_convex:
```
```   755   assumes "convex_set C"
```
```   756   assumes "x \<in> C" "y \<in> C" "x < y"
```
```   757   shows "{x .. y} \<subseteq> C"
```
```   758 proof safe
```
```   759   fix z assume zasm: "z \<in> {x .. y}"
```
```   760   { assume asm: "x < z" "z < y"
```
```   761     let "?\<mu>" = "(y - z) / (y - x)"
```
```   762     have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps)
```
```   763     hence comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
```
```   764       using assms[unfolded convex_set_def] by blast
```
```   765     have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
```
```   766       by (auto simp add:field_simps)
```
```   767     also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
```
```   768       using assms unfolding add_divide_distrib by (auto simp:field_simps)
```
```   769     also have "\<dots> = z"
```
```   770       using assms by (auto simp:field_simps)
```
```   771     finally have "z \<in> C"
```
```   772       using comb by auto } note less = this
```
```   773   show "z \<in> C" using zasm less assms
```
```   774     unfolding atLeastAtMost_iff le_less by auto
```
```   775 qed
```
```   776
```
```   777 lemma f''_imp_f':
```
```   778   fixes f :: "real \<Rightarrow> real"
```
```   779   assumes "convex_set C"
```
```   780   assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
```
```   781   assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
```
```   782   assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
```
```   783   assumes "x \<in> C" "y \<in> C"
```
```   784   shows "f' x * (y - x) \<le> f y - f x"
```
```   785 using assms
```
```   786 proof -
```
```   787   { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x"
```
```   788     hence ge: "y - x > 0" "y - x \<ge> 0" by auto
```
```   789     from asm have le: "x - y < 0" "x - y \<le> 0" by auto
```
```   790     then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
```
```   791       using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `y \<in> C` `x < y`],
```
```   792         THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
```
```   793       by auto
```
```   794     hence "z1 \<in> C" using atMostAtLeast_subset_convex
```
```   795       `convex_set C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
```
```   796     from z1 have z1': "f x - f y = (x - y) * f' z1"
```
```   797       by (simp add:field_simps)
```
```   798     obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
```
```   799       using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1`],
```
```   800         THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
```
```   801       by auto
```
```   802     obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
```
```   803       using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y`],
```
```   804         THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
```
```   805       by auto
```
```   806     have "f' y - (f x - f y) / (x - y) = f' y - f' z1"
```
```   807       using asm z1' by auto
```
```   808     also have "\<dots> = (y - z1) * f'' z3" using z3 by auto
```
```   809     finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
```
```   810     have A': "y - z1 \<ge> 0" using z1 by auto
```
```   811     have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
```
```   812       `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
```
```   813     hence B': "f'' z3 \<ge> 0" using assms by auto
```
```   814     from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
```
```   815     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
```
```   816     from mult_right_mono_neg[OF this le(2)]
```
```   817     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
```
```   818       unfolding diff_def using real_add_mult_distrib by auto
```
```   819     hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
```
```   820     hence res: "f' y * (x - y) \<le> f x - f y" by auto
```
```   821     have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
```
```   822       using asm z1 by auto
```
```   823     also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto
```
```   824     finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
```
```   825     have A: "z1 - x \<ge> 0" using z1 by auto
```
```   826     have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
```
```   827       `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
```
```   828     hence B: "f'' z2 \<ge> 0" using assms by auto
```
```   829     from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
```
```   830     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
```
```   831     from mult_right_mono[OF this ge(2)]
```
```   832     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
```
```   833       unfolding diff_def using real_add_mult_distrib by auto
```
```   834     hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
```
```   835     hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
```
```   836       using res by auto } note less_imp = this
```
```   837   { fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y"
```
```   838     hence"f y - f x \<ge> f' x * (y - x)"
```
```   839     unfolding neq_iff apply safe
```
```   840     using less_imp by auto } note neq_imp = this
```
```   841   moreover
```
```   842   { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y"
```
```   843     hence "f y - f x \<ge> f' x * (y - x)" by auto }
```
```   844   ultimately show ?thesis using assms by blast
```
```   845 qed
```
```   846
```
```   847 lemma f''_ge0_imp_convex:
```
```   848   fixes f :: "real \<Rightarrow> real"
```
```   849   assumes conv: "convex_set C"
```
```   850   assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
```
```   851   assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
```
```   852   assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
```
```   853   shows "convex_fun f C"
```
```   854 using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
```
```   855
```
```   856 lemma minus_log_convex:
```
```   857   fixes b :: real
```
```   858   assumes "b > 1"
```
```   859   shows "convex_fun (\<lambda> x. - log b x) {0 <..}"
```
```   860 proof -
```
```   861   have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
```
```   862   hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
```
```   863     using DERIV_minus by auto
```
```   864   have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
```
```   865     using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
```
```   866   from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
```
```   867   have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
```
```   868     by auto
```
```   869   hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
```
```   870     unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
```
```   871   have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
```
```   872     using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
```
```   873   from f''_ge0_imp_convex[OF pos_is_convex,
```
```   874     unfolded greaterThan_iff, OF f' f''0 f''_ge0]
```
```   875   show ?thesis by auto
```
```   876 qed
```
```   877
```
```   878 lemma setsum_nonneg_0:
```
```   879   fixes f :: "'a \<Rightarrow> real"
```
```   880   assumes "finite s"
```
```   881   assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
```
```   882   assumes "(\<Sum> i \<in> s. f i) = 0"
```
```   883   assumes "i \<in> s"
```
```   884   shows "f i = 0"
```
```   885 proof -
```
```   886   { assume asm: "f i > 0"
```
```   887     from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
```
```   888     from setsum_nonneg[of "s - {i}" f, OF this]
```
```   889     have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
```
```   890     hence "(\<Sum> j \<in> s - {i}. f j) + f i > 0" using asm by auto
```
```   891     from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
```
```   892     have "(\<Sum> j \<in> s. f j) > 0" by auto
```
```   893     hence "False" using assms by auto }
```
```   894   thus ?thesis using assms by fastsimp
```
```   895 qed
```
```   896
```
```   897 lemma setsum_nonneg_leq_1:
```
```   898   fixes f :: "'a \<Rightarrow> real"
```
```   899   assumes "finite s"
```
```   900   assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
```
```   901   assumes "(\<Sum> i \<in> s. f i) = 1"
```
```   902   assumes "i \<in> s"
```
```   903   shows "f i \<le> 1"
```
```   904 proof -
```
```   905   { assume asm: "f i > 1"
```
```   906     from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
```
```   907     from setsum_nonneg[of "s - {i}" f, OF this]
```
```   908     have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
```
```   909     hence "(\<Sum> j \<in> s - {i}. f j) + f i > 1" using asm by auto
```
```   910     from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
```
```   911     have "(\<Sum> j \<in> s. f j) > 1" by auto
```
```   912     hence "False" using assms by auto }
```
```   913   thus ?thesis using assms by fastsimp
```
```   914 qed
```
```   915
```
```   916 lemma convex_set_setsum:
```
```   917   assumes "finite s" "s \<noteq> {}"
```
```   918   assumes "convex_set C"
```
```   919   assumes "(\<Sum> i \<in> s. a i) = 1"
```
```   920   assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
```
```   921   assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
```
```   922   shows "(\<Sum> j \<in> s. a j * y j) \<in> C"
```
```   923 using assms
```
```   924 proof (induct s arbitrary:a rule:finite_ne_induct)
```
```   925   case (singleton i) note asms = this
```
```   926   hence "a i = 1" by auto
```
```   927   thus ?case using asms by auto
```
```   928 next
```
```   929   case (insert i s) note asms = this
```
```   930   { assume "a i = 1"
```
```   931     hence "(\<Sum> j \<in> s. a j) = 0"
```
```   932       using asms by auto
```
```   933     hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
```
```   934       using setsum_nonneg_0 asms by fastsimp
```
```   935     hence ?case using asms by auto }
```
```   936   moreover
```
```   937   { assume asm: "a i \<noteq> 1"
```
```   938     from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
```
```   939     have fis: "finite (insert i s)" using asms by auto
```
```   940     hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
```
```   941     hence "a i < 1" using asm by auto
```
```   942     hence i0: "1 - a i > 0" by auto
```
```   943     let "?a j" = "a j / (1 - a i)"
```
```   944     { fix j assume "j \<in> s"
```
```   945       hence "?a j \<ge> 0"
```
```   946         using i0 asms divide_nonneg_pos
```
```   947         by fastsimp } note a_nonneg = this
```
```   948     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
```
```   949     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
```
```   950     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
```
```   951     hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
```
```   952     from this asms
```
```   953     have "(\<Sum>j\<in>s. ?a j * y j) \<in> C" using a_nonneg by fastsimp
```
```   954     hence "a i * y i + (1 - a i) * (\<Sum> j \<in> s. ?a j * y j) \<in> C"
```
```   955       using asms[unfolded convex_set_def, rule_format] yai ai1 by auto
```
```   956     hence "a i * y i + (\<Sum> j \<in> s. (1 - a i) * (?a j * y j)) \<in> C"
```
```   957       using mult_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j * y j" s] by auto
```
```   958     hence "a i * y i + (\<Sum> j \<in> s. a j * y j) \<in> C" using i0 by auto
```
```   959     hence ?case using setsum.insert asms by auto }
```
```   960   ultimately show ?case by auto
```
```   961 qed
```
```   962
```
```   963 lemma convex_fun_setsum:
```
```   964   fixes a :: "'a \<Rightarrow> real"
```
```   965   assumes "finite s" "s \<noteq> {}"
```
```   966   assumes "convex_fun f C"
```
```   967   assumes "(\<Sum> i \<in> s. a i) = 1"
```
```   968   assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
```
```   969   assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
```
```   970   shows "f (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
```
```   971 using assms
```
```   972 proof (induct s arbitrary:a rule:finite_ne_induct)
```
```   973   case (singleton i)
```
```   974   hence ai: "a i = 1" by auto
```
```   975   thus ?case by auto
```
```   976 next
```
```   977   case (insert i s) note asms = this
```
```   978   hence "convex_fun f C" by simp
```
```   979   from this[unfolded convex_fun_def, rule_format]
```
```   980   have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk>
```
```   981   \<Longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
```
```   982     by simp
```
```   983   { assume "a i = 1"
```
```   984     hence "(\<Sum> j \<in> s. a j) = 0"
```
```   985       using asms by auto
```
```   986     hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
```
```   987       using setsum_nonneg_0 asms by fastsimp
```
```   988     hence ?case using asms by auto }
```
```   989   moreover
```
```   990   { assume asm: "a i \<noteq> 1"
```
```   991     from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
```
```   992     have fis: "finite (insert i s)" using asms by auto
```
```   993     hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
```
```   994     hence "a i < 1" using asm by auto
```
```   995     hence i0: "1 - a i > 0" by auto
```
```   996     let "?a j" = "a j / (1 - a i)"
```
```   997     { fix j assume "j \<in> s"
```
```   998       hence "?a j \<ge> 0"
```
```   999         using i0 asms divide_nonneg_pos
```
```  1000         by fastsimp } note a_nonneg = this
```
```  1001     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
```
```  1002     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
```
```  1003     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
```
```  1004     hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
```
```  1005     have "convex_set C" using asms unfolding convex_fun_def by auto
```
```  1006     hence asum: "(\<Sum> j \<in> s. ?a j * y j) \<in> C"
```
```  1007       using asms convex_set_setsum[OF `finite s` `s \<noteq> {}`
```
```  1008         `convex_set C` a1 a_nonneg] by auto
```
```  1009     have asum_le: "f (\<Sum> j \<in> s. ?a j * y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))"
```
```  1010       using a_nonneg a1 asms by blast
```
```  1011     have "f (\<Sum> j \<in> insert i s. a j * y j) = f ((\<Sum> j \<in> s. a j * y j) + a i * y i)"
```
```  1012       using setsum.insert[of s i "\<lambda> j. a j * y j", OF `finite s` `i \<notin> s`] asms
```
```  1013       by (auto simp only:add_commute)
```
```  1014     also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j) / (1 - a i) + a i * y i)"
```
```  1015       using i0 by auto
```
```  1016     also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j / (1 - a i)) + a i * y i)"
```
```  1017       unfolding divide.setsum[of "\<lambda> j. a j * y j" s "1 - a i", symmetric] by auto
```
```  1018     also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. ?a j * y j) + a i * y i)" by auto
```
```  1019     also have "\<dots> \<le> (1 - a i) * f ((\<Sum> j \<in> s. ?a j * y j)) + a i * f (y i)"
```
```  1020       using conv[of "y i" "(\<Sum> j \<in> s. ?a j * y j)" "a i", OF yai(1) asum yai(2) ai1]
```
```  1021       by (auto simp only:add_commute)
```
```  1022     also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
```
```  1023       using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
```
```  1024         OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
```
```  1025     also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
```
```  1026       unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
```
```  1027     also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
```
```  1028     also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
```
```  1029     finally have "f (\<Sum> j \<in> insert i s. a j * y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"
```
```  1030       by simp }
```
```  1031   ultimately show ?case by auto
```
```  1032 qed
```
```  1033
```
```  1034 lemma log_setsum:
```
```  1035   assumes "finite s" "s \<noteq> {}"
```
```  1036   assumes "b > 1"
```
```  1037   assumes "(\<Sum> i \<in> s. a i) = 1"
```
```  1038   assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
```
```  1039   assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
```
```  1040   shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
```
```  1041 proof -
```
```  1042   have "convex_fun (\<lambda> x. - log b x) {0 <..}"
```
```  1043     by (rule minus_log_convex[OF `b > 1`])
```
```  1044   hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
```
```  1045     using convex_fun_setsum assms by blast
```
```  1046   thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
```
```  1047 qed
```
```  1048
```
```  1049 lemma (in finite_prob_space) finite_entropy_le_card:
```
```  1050   assumes "1 < b"
```
```  1051   shows "\<H>\<^bsub>b\<^esub>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
```
```  1052 proof -
```
```  1053   interpret X: finite_prob_space "\<lparr>space = X ` space M,
```
```  1054                                     sets = Pow (X ` space M),
```
```  1055                                  measure = distribution X\<rparr>"
```
```  1056     using finite_prob_space by auto
```
```  1057   have triv: "\<And> x. (if distribution X {x} \<noteq> 0 then distribution X {x} else 0) = distribution X {x}"
```
```  1058     by auto
```
```  1059   hence sum1: "(\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x}) = 1"
```
```  1060     using X.measure_finitely_additive''[of "X ` space M" "\<lambda> x. {x}", simplified]
```
```  1061       sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
```
```  1062     unfolding disjoint_family_on_def  X.prob_space[symmetric]
```
```  1063     using finite_imageI[OF finite_space, of X] by (auto simp add:triv setsum_restrict_set)
```
```  1064   have pos: "\<And> x. x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0} \<Longrightarrow> inverse (distribution X {x}) > 0"
```
```  1065     using X.positive sets_eq_Pow unfolding inverse_positive_iff_positive less_le by auto
```
```  1066   { assume asm: "X ` space M \<inter> {y. distribution X {y} \<noteq> 0} = {}"
```
```  1067     { fix x assume "x \<in> X ` space M"
```
```  1068       hence "distribution X {x} = 0" using asm by blast }
```
```  1069     hence A: "(\<Sum> x \<in> X ` space M. distribution X {x}) = 0" by auto
```
```  1070     have B: "(\<Sum> x \<in> X ` space M. distribution X {x})
```
```  1071       \<ge> (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x})"
```
```  1072       using finite_imageI[OF finite_space, of X]
```
```  1073       by (subst setsum_mono2) auto
```
```  1074     from A B have "False" using sum1 by auto } note not_empty = this
```
```  1075   { fix x assume asm: "x \<in> X ` space M"
```
```  1076     have "- distribution X {x} * log b (distribution X {x})
```
```  1077        = - (if distribution X {x} \<noteq> 0
```
```  1078             then distribution X {x} * log b (distribution X {x})
```
```  1079             else 0)"
```
```  1080       by auto
```
```  1081     also have "\<dots> = (if distribution X {x} \<noteq> 0
```
```  1082           then distribution X {x} * - log b (distribution X {x})
```
```  1083           else 0)"
```
```  1084       by auto
```
```  1085     also have "\<dots> = (if distribution X {x} \<noteq> 0
```
```  1086                     then distribution X {x} * log b (inverse (distribution X {x}))
```
```  1087                     else 0)"
```
```  1088       using log_inverse `1 < b` X.positive[of "{x}"] asm by auto
```
```  1089     finally have "- distribution X {x} * log b (distribution X {x})
```
```  1090                  = (if distribution X {x} \<noteq> 0
```
```  1091                     then distribution X {x} * log b (inverse (distribution X {x}))
```
```  1092                     else 0)"
```
```  1093       by auto } note log_inv = this
```
```  1094   have "- (\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))
```
```  1095        = (\<Sum> x \<in> X ` space M. (if distribution X {x} \<noteq> 0
```
```  1096           then distribution X {x} * log b (inverse (distribution X {x}))
```
```  1097           else 0))"
```
```  1098     unfolding setsum_negf[symmetric] using log_inv by auto
```
```  1099   also have "\<dots> = (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
```
```  1100                           distribution X {x} * log b (inverse (distribution X {x})))"
```
```  1101     unfolding setsum_restrict_set[OF finite_imageI[OF finite_space, of X]] by auto
```
```  1102   also have "\<dots> \<le> log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
```
```  1103                           distribution X {x} * (inverse (distribution X {x})))"
```
```  1104     apply (subst log_setsum[OF _ _ `b > 1` sum1,
```
```  1105      unfolded greaterThan_iff, OF _ _ _]) using pos sets_eq_Pow
```
```  1106       X.finite_space assms X.positive not_empty by auto
```
```  1107   also have "\<dots> = log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. 1)"
```
```  1108     by auto
```
```  1109   also have "\<dots> \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))"
```
```  1110     by auto
```
```  1111   finally have "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
```
```  1112                \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" by simp
```
```  1113   thus ?thesis unfolding finite_entropy_reduce[OF assms] real_eq_of_nat by auto
```
```  1114 qed
```
```  1115
```
```  1116 (* --------------- entropy is maximal for a uniform rv --------------------- *)
```
```  1117
```
```  1118 lemma (in finite_prob_space) uniform_prob:
```
```  1119   assumes "x \<in> space M"
```
```  1120   assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}"
```
```  1121   shows "prob {x} = 1 / real (card (space M))"
```
```  1122 proof -
```
```  1123   have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}"
```
```  1124     using assms(2)[OF _ `x \<in> space M`] by blast
```
```  1125   have "1 = prob (space M)"
```
```  1126     using prob_space by auto
```
```  1127   also have "\<dots> = (\<Sum> x \<in> space M. prob {x})"
```
```  1128     using measure_finitely_additive''[of "space M" "\<lambda> x. {x}", simplified]
```
```  1129       sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
```
```  1130       finite_space unfolding disjoint_family_on_def  prob_space[symmetric]
```
```  1131     by (auto simp add:setsum_restrict_set)
```
```  1132   also have "\<dots> = (\<Sum> y \<in> space M. prob {x})"
```
```  1133     using prob_x by auto
```
```  1134   also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
```
```  1135   finally have one: "1 = real (card (space M)) * prob {x}"
```
```  1136     using real_eq_of_nat by auto
```
```  1137   hence two: "real (card (space M)) \<noteq> 0" by fastsimp
```
```  1138   from one have three: "prob {x} \<noteq> 0" by fastsimp
```
```  1139   thus ?thesis using one two three divide_cancel_right
```
```  1140     by (auto simp:field_simps)
```
```  1141 qed
```
```  1142
```
```  1143 lemma (in finite_prob_space) finite_entropy_uniform_max:
```
```  1144   assumes "b > 1"
```
```  1145   assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
```
```  1146   shows "\<H>\<^bsub>b\<^esub>(X) = log b (real (card (X ` space M)))"
```
```  1147 proof -
```
```  1148   interpret X: finite_prob_space "\<lparr>space = X ` space M,
```
```  1149                                     sets = Pow (X ` space M),
```
```  1150                                  measure = distribution X\<rparr>"
```
```  1151     using finite_prob_space by auto
```
```  1152   { fix x assume xasm: "x \<in> X ` space M"
```
```  1153     hence card_gt0: "real (card (X ` space M)) > 0"
```
```  1154       using card_gt_0_iff X.finite_space by auto
```
```  1155     from xasm have "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = distribution X {x}"
```
```  1156       using assms by blast
```
```  1157     hence "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
```
```  1158          = - (\<Sum> y \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
```
```  1159       by auto
```
```  1160     also have "\<dots> = - real_of_nat (card (X ` space M)) * distribution X {x} * log b (distribution X {x})"
```
```  1161       by auto
```
```  1162     also have "\<dots> = - real (card (X ` space M)) * (1 / real (card (X ` space M))) * log b (1 / real (card (X ` space M)))"
```
```  1163       unfolding real_eq_of_nat[symmetric]
```
```  1164       by (auto simp: X.uniform_prob[simplified, OF xasm assms(2)])
```
```  1165     also have "\<dots> = log b (real (card (X ` space M)))"
```
```  1166       unfolding inverse_eq_divide[symmetric]
```
```  1167       using card_gt0 log_inverse `b > 1`
```
```  1168       by (auto simp add:field_simps card_gt0)
```
```  1169     finally have ?thesis
```
```  1170       unfolding finite_entropy_reduce[OF `b > 1`] by auto }
```
```  1171   moreover
```
```  1172   { assume "X ` space M = {}"
```
```  1173     hence "distribution X (X ` space M) = 0"
```
```  1174       using X.empty_measure by simp
```
```  1175     hence "False" using X.prob_space by auto }
```
```  1176   ultimately show ?thesis by auto
```
```  1177 qed
```
```  1178
```
```  1179 end
```