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