src/HOL/Probability/Information.thy
changeset 36080 0d9affa4e73c
child 36623 d26348b667f2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Apr 07 17:24:44 2010 +0200
     1.3 @@ -0,0 +1,1179 @@
     1.4 +theory Information
     1.5 +imports Probability_Space Product_Measure
     1.6 +begin
     1.7 +
     1.8 +lemma pos_neg_part_abs:
     1.9 +  fixes f :: "'a \<Rightarrow> real"
    1.10 +  shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
    1.11 +unfolding real_abs_def pos_part_def neg_part_def by auto
    1.12 +
    1.13 +lemma pos_part_abs:
    1.14 +  fixes f :: "'a \<Rightarrow> real"
    1.15 +  shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
    1.16 +unfolding pos_part_def real_abs_def by auto
    1.17 +
    1.18 +lemma neg_part_abs:
    1.19 +  fixes f :: "'a \<Rightarrow> real"
    1.20 +  shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
    1.21 +unfolding neg_part_def real_abs_def by auto
    1.22 +
    1.23 +lemma (in measure_space) int_abs:
    1.24 +  assumes "integrable f"
    1.25 +  shows "integrable (\<lambda> x. \<bar>f x\<bar>)"
    1.26 +using assms
    1.27 +proof -
    1.28 +  from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)"
    1.29 +    unfolding integrable_def by auto
    1.30 +  hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)"
    1.31 +    using nnfis_add by auto
    1.32 +  hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp
    1.33 +  thus ?thesis unfolding integrable_def
    1.34 +    using ext[OF pos_part_abs[of f], of "\<lambda> y. y"]
    1.35 +      ext[OF neg_part_abs[of f], of "\<lambda> y. y"]
    1.36 +    using nnfis_0 by auto
    1.37 +qed
    1.38 +
    1.39 +lemma (in measure_space) measure_mono:
    1.40 +  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
    1.41 +  shows "measure M a \<le> measure M b"
    1.42 +proof -
    1.43 +  have "b = a \<union> (b - a)" using assms by auto
    1.44 +  moreover have "{} = a \<inter> (b - a)" by auto
    1.45 +  ultimately have "measure M b = measure M a + measure M (b - a)"
    1.46 +    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
    1.47 +  moreover have "measure M (b - a) \<ge> 0" using positive assms by auto
    1.48 +  ultimately show "measure M a \<le> measure M b" by auto
    1.49 +qed
    1.50 +
    1.51 +lemma (in measure_space) integral_0:
    1.52 +  fixes f :: "'a \<Rightarrow> real"
    1.53 +  assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M"
    1.54 +  shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0"
    1.55 +proof -
    1.56 +  have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto
    1.57 +  moreover
    1.58 +  { fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}"
    1.59 +    hence "\<bar> f y \<bar> > 0" by auto
    1.60 +    hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))"
    1.61 +      using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto
    1.62 +    hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
    1.63 +      by auto }
    1.64 +  moreover
    1.65 +  { fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
    1.66 +    then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto
    1.67 +    hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto
    1.68 +    hence "\<bar>f y\<bar> > 0"
    1.69 +      using real_of_nat_Suc_gt_zero
    1.70 +        positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp
    1.71 +    hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto }
    1.72 +  ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})"
    1.73 +    by blast
    1.74 +  { fix n
    1.75 +    have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using int_abs assms by auto
    1.76 +    have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M)
    1.77 +           \<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)"
    1.78 +      using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto
    1.79 +    hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0"
    1.80 +      using assms unfolding nonneg_def by auto
    1.81 +    have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
    1.82 +      apply (subst Int_commute) unfolding Int_def
    1.83 +      using borel[unfolded borel_measurable_ge_iff] by simp
    1.84 +    hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and>
    1.85 +      {x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M"
    1.86 +      using positive le0 unfolding atLeast_def by fastsimp }
    1.87 +  moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M"
    1.88 +    by auto
    1.89 +  moreover
    1.90 +  { fix n
    1.91 +    have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))"
    1.92 +      using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp
    1.93 +    hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans)
    1.94 +    hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M
    1.95 +         \<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto }
    1.96 +  ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)"
    1.97 +    using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"]
    1.98 +    unfolding o_def by (simp del: of_nat_Suc)
    1.99 +  hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0"
   1.100 +    using LIMSEQ_const[of 0] LIMSEQ_unique by simp
   1.101 +  hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0"
   1.102 +    using assms unfolding nonneg_def by auto
   1.103 +  thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp
   1.104 +qed
   1.105 +
   1.106 +definition
   1.107 +  "KL_divergence b M u v =
   1.108 +    measure_space.integral (M\<lparr>measure := u\<rparr>)
   1.109 +                           (\<lambda>x. log b ((measure_space.RN_deriv (M \<lparr>measure := v\<rparr> ) u) x))"
   1.110 +
   1.111 +lemma (in finite_prob_space) finite_measure_space:
   1.112 +  shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
   1.113 +    (is "finite_measure_space ?S")
   1.114 +proof (rule finite_Pow_additivity_sufficient, simp_all)
   1.115 +  show "finite (X ` space M)" using finite_space by simp
   1.116 +
   1.117 +  show "positive ?S (distribution X)" unfolding distribution_def
   1.118 +    unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto
   1.119 +
   1.120 +  show "additive ?S (distribution X)" unfolding additive_def distribution_def
   1.121 +  proof (simp, safe)
   1.122 +    fix x y
   1.123 +    have x: "(X -` x) \<inter> space M \<in> sets M"
   1.124 +      and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto
   1.125 +    assume "x \<inter> y = {}"
   1.126 +    from additive[unfolded additive_def, rule_format, OF x y] this
   1.127 +    have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) =
   1.128 +      prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)"
   1.129 +      apply (subst Int_Un_distrib2)
   1.130 +      by auto
   1.131 +    thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)"
   1.132 +      by auto
   1.133 +  qed
   1.134 +qed
   1.135 +
   1.136 +lemma (in finite_prob_space) finite_prob_space:
   1.137 +  "finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
   1.138 +  (is "finite_prob_space ?S")
   1.139 +  unfolding finite_prob_space_def prob_space_def prob_space_axioms_def
   1.140 +proof safe
   1.141 +  show "finite_measure_space ?S" by (rule finite_measure_space)
   1.142 +  thus "measure_space ?S" by (simp add: finite_measure_space_def)
   1.143 +
   1.144 +  have "X -` X ` space M \<inter> space M = space M" by auto
   1.145 +  thus "measure ?S (space ?S) = 1"
   1.146 +    by (simp add: distribution_def prob_space)
   1.147 +qed
   1.148 +
   1.149 +lemma (in finite_prob_space) finite_measure_space_image_prod:
   1.150 +  "finite_measure_space \<lparr>space = X ` space M \<times> Y ` space M,
   1.151 +    sets = Pow (X ` space M \<times> Y ` space M), measure_space.measure = distribution (\<lambda>x. (X x, Y x))\<rparr>"
   1.152 +  (is "finite_measure_space ?Z")
   1.153 +proof (rule finite_Pow_additivity_sufficient, simp_all)
   1.154 +  show "finite (X ` space M \<times> Y ` space M)" using finite_space by simp
   1.155 +
   1.156 +  let ?d = "distribution (\<lambda>x. (X x, Y x))"
   1.157 +
   1.158 +  show "positive ?Z ?d"
   1.159 +    using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
   1.160 +
   1.161 +  show "additive ?Z ?d" unfolding additive_def
   1.162 +  proof safe
   1.163 +    fix x y assume "x \<in> sets ?Z" and "y \<in> sets ?Z"
   1.164 +    assume "x \<inter> y = {}"
   1.165 +    thus "?d (x \<union> y) = ?d x + ?d y"
   1.166 +      apply (simp add: distribution_def)
   1.167 +      apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
   1.168 +      by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
   1.169 +  qed
   1.170 +qed
   1.171 +
   1.172 +definition (in prob_space)
   1.173 +  "mutual_information b s1 s2 X Y \<equiv>
   1.174 +    let prod_space =
   1.175 +      prod_measure_space (\<lparr>space = space s1, sets = sets s1, measure = distribution X\<rparr>)
   1.176 +                         (\<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr>)
   1.177 +    in
   1.178 +      KL_divergence b prod_space (joint_distribution X Y) (measure prod_space)"
   1.179 +
   1.180 +abbreviation (in finite_prob_space)
   1.181 +  finite_mutual_information ("\<I>\<^bsub>_\<^esub>'(_ ; _')") where
   1.182 +  "\<I>\<^bsub>b\<^esub>(X ; Y) \<equiv> mutual_information b
   1.183 +    \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
   1.184 +    \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
   1.185 +
   1.186 +abbreviation (in finite_prob_space)
   1.187 +  finite_mutual_information_2 :: "('a \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd) \<Rightarrow> real" ("\<I>'(_ ; _')") where
   1.188 +  "\<I>(X ; Y) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y)"
   1.189 +
   1.190 +lemma (in prob_space) mutual_information_cong:
   1.191 +  assumes [simp]: "space S1 = space S3" "sets S1 = sets S3"
   1.192 +    "space S2 = space S4" "sets S2 = sets S4"
   1.193 +  shows "mutual_information b S1 S2 X Y = mutual_information b S3 S4 X Y"
   1.194 +  unfolding mutual_information_def by simp
   1.195 +
   1.196 +lemma (in prob_space) joint_distribution:
   1.197 +  "joint_distribution X Y = distribution (\<lambda>x. (X x, Y x))"
   1.198 +  unfolding joint_distribution_def_raw distribution_def_raw ..
   1.199 +
   1.200 +lemma (in finite_prob_space) finite_mutual_information_reduce:
   1.201 +  "\<I>\<^bsub>b\<^esub>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
   1.202 +    distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /
   1.203 +                                                   (distribution X {x} * distribution Y {y})))"
   1.204 +  (is "_ = setsum ?log ?prod")
   1.205 +  unfolding Let_def mutual_information_def KL_divergence_def
   1.206 +proof (subst finite_measure_space.integral_finite_singleton, simp_all add: joint_distribution)
   1.207 +  let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure_space.measure = distribution X\<rparr>"
   1.208 +  let ?Y = "\<lparr>space = Y ` space M, sets = Pow (Y ` space M), measure_space.measure = distribution Y\<rparr>"
   1.209 +  let ?P = "prod_measure_space ?X ?Y"
   1.210 +
   1.211 +  interpret X: finite_measure_space "?X" by (rule finite_measure_space)
   1.212 +  moreover interpret Y: finite_measure_space "?Y" by (rule finite_measure_space)
   1.213 +  ultimately have ms_X: "measure_space ?X" and ms_Y: "measure_space ?Y" by unfold_locales
   1.214 +
   1.215 +  interpret P: finite_measure_space "?P" by (rule finite_measure_space_finite_prod_measure) (fact+)
   1.216 +
   1.217 +  let ?P' = "measure_update (\<lambda>_. distribution (\<lambda>x. (X x, Y x))) ?P"
   1.218 +  from finite_measure_space_image_prod[of X Y]
   1.219 +    sigma_prod_sets_finite[OF X.finite_space Y.finite_space]
   1.220 +  show "finite_measure_space ?P'"
   1.221 +    by (simp add: X.sets_eq_Pow Y.sets_eq_Pow joint_distribution finite_measure_space_def prod_measure_space_def)
   1.222 +
   1.223 +  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})
   1.224 +    = setsum ?log ?prod"
   1.225 +  proof (rule setsum_cong)
   1.226 +    show "space ?P = ?prod" unfolding prod_measure_space_def by simp
   1.227 +  next
   1.228 +    fix x assume x: "x \<in> X ` space M \<times> Y ` space M"
   1.229 +    then obtain d e where x_Pair: "x = (d, e)"
   1.230 +      and d: "d \<in> X ` space M"
   1.231 +      and e: "e \<in> Y ` space M" by auto
   1.232 +
   1.233 +    { fix x assume m_0: "measure ?P {x} = 0"
   1.234 +      have "distribution (\<lambda>x. (X x, Y x)) {x} = 0"
   1.235 +      proof (cases x)
   1.236 +        case (Pair a b)
   1.237 +        hence "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = (X -` {a} \<inter> space M) \<inter> (Y -` {b} \<inter> space M)"
   1.238 +          and x_prod: "{x} = {a} \<times> {b}" by auto
   1.239 +
   1.240 +        let ?PROD = "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M"
   1.241 +
   1.242 +        show ?thesis
   1.243 +        proof (cases "{a} \<subseteq> X ` space M \<and> {b} \<subseteq> Y ` space M")
   1.244 +          case False
   1.245 +          hence "?PROD = {}"
   1.246 +            unfolding Pair by auto
   1.247 +          thus ?thesis by (auto simp: distribution_def)
   1.248 +        next
   1.249 +          have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
   1.250 +            using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
   1.251 +
   1.252 +          case True
   1.253 +          with prod_measure_times[OF ms_X ms_Y, simplified, of "{a}" "{b}"]
   1.254 +          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
   1.255 +            by (simp add: prod_measure_space_def distribution_def Pair)
   1.256 +          thus ?thesis
   1.257 +          proof (rule disjE)
   1.258 +            assume ?X_0
   1.259 +            have "prob ?PROD \<le> prob (X -` {a} \<inter> space M)"
   1.260 +              using sets_eq_Pow Pair by (auto intro!: measure_mono)
   1.261 +            thus ?thesis using `?X_0` by (auto simp: distribution_def)
   1.262 +          next
   1.263 +            assume ?Y_0
   1.264 +            have "prob ?PROD \<le> prob (Y -` {b} \<inter> space M)"
   1.265 +              using sets_eq_Pow Pair by (auto intro!: measure_mono)
   1.266 +            thus ?thesis using `?Y_0` by (auto simp: distribution_def)
   1.267 +          qed
   1.268 +        qed
   1.269 +      qed }
   1.270 +    note measure_zero_joint_distribution = this
   1.271 +
   1.272 +    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"
   1.273 +    apply (cases "distribution (\<lambda>x. (X x, Y x)) {x} \<noteq> 0")
   1.274 +    apply (subst P.RN_deriv_finite_singleton)
   1.275 +    proof (simp_all add: x_Pair)
   1.276 +      from `finite_measure_space ?P'` show "measure_space ?P'" by (simp add: finite_measure_space_def)
   1.277 +    next
   1.278 +      fix x assume m_0: "measure ?P {x} = 0" thus "distribution (\<lambda>x. (X x, Y x)) {x} = 0" by fact
   1.279 +    next
   1.280 +      show "(d,e) \<in> space ?P" unfolding prod_measure_space_def using x x_Pair by simp
   1.281 +    next
   1.282 +      assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
   1.283 +      show "measure ?P {(d,e)} \<noteq> 0"
   1.284 +      proof
   1.285 +        assume "measure ?P {(d,e)} = 0"
   1.286 +        from measure_zero_joint_distribution[OF this] jd_0
   1.287 +        show False by simp
   1.288 +      qed
   1.289 +    next
   1.290 +      assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0"
   1.291 +      with prod_measure_times[OF ms_X ms_Y, simplified, of "{d}" "{e}"] d
   1.292 +      show "log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / measure ?P {(d, e)}) =
   1.293 +        log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / (distribution X {d} * distribution Y {e}))"
   1.294 +        by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
   1.295 +    qed
   1.296 +  qed
   1.297 +qed
   1.298 +
   1.299 +lemma (in finite_prob_space) distribution_log_split:
   1.300 +  assumes "1 < b"
   1.301 +  shows
   1.302 +  "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
   1.303 +                                                     (distribution X {X x} * distribution Z {z})) =
   1.304 +   distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} /
   1.305 +                                                     distribution Z {z}) -
   1.306 +   distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution X {X x})"
   1.307 +  (is "?lhs = ?rhs")
   1.308 +proof (cases "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} = 0")
   1.309 +  case True thus ?thesis by simp
   1.310 +next
   1.311 +  case False
   1.312 +
   1.313 +  let ?dZ = "distribution Z"
   1.314 +  let ?dX = "distribution X"
   1.315 +  let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
   1.316 +
   1.317 +  have dist_nneg: "\<And>x X. 0 \<le> distribution X x"
   1.318 +    unfolding distribution_def using sets_eq_Pow by (auto intro: positive)
   1.319 +
   1.320 +  have "?lhs = ?dXZ {(X x, z)} * (log b (?dXZ {(X x, z)} / ?dZ {z}) - log b (?dX {X x}))"
   1.321 +  proof -
   1.322 +    have pos_dXZ: "0 < ?dXZ {(X x, z)}"
   1.323 +      using False dist_nneg[of "\<lambda>x. (X x, Z x)" "{(X x, z)}"] by auto
   1.324 +    moreover
   1.325 +    have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (X -` {X x}) \<inter> space M" by auto
   1.326 +    hence "?dXZ {(X x, z)} \<le> ?dX {X x}"
   1.327 +      unfolding distribution_def
   1.328 +      by (rule measure_mono) (simp_all add: sets_eq_Pow)
   1.329 +    with pos_dXZ have "0 < ?dX {X x}" by (rule less_le_trans)
   1.330 +    moreover
   1.331 +    have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (Z -` {z}) \<inter> space M" by auto
   1.332 +    hence "?dXZ {(X x, z)} \<le> ?dZ {z}"
   1.333 +      unfolding distribution_def
   1.334 +      by (rule measure_mono) (simp_all add: sets_eq_Pow)
   1.335 +    with pos_dXZ have "0 < ?dZ {z}" by (rule less_le_trans)
   1.336 +    moreover have "0 < b" by (rule less_trans[OF _ `1 < b`]) simp
   1.337 +    moreover have "b \<noteq> 1" by (rule ccontr) (insert `1 < b`, simp)
   1.338 +    ultimately show ?thesis
   1.339 +      using pos_dXZ
   1.340 +      apply (subst (2) mult_commute)
   1.341 +      apply (subst divide_divide_eq_left[symmetric])
   1.342 +      apply (subst log_divide)
   1.343 +      by (auto intro: divide_pos_pos)
   1.344 +  qed
   1.345 +  also have "... = ?rhs"
   1.346 +    by (simp add: field_simps)
   1.347 +  finally show ?thesis .
   1.348 +qed
   1.349 +
   1.350 +lemma (in finite_prob_space) finite_mutual_information_reduce_prod:
   1.351 +  "mutual_information b
   1.352 +    \<lparr> space = X ` space M, sets = Pow (X ` space M) \<rparr>
   1.353 +    \<lparr> space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M) \<rparr>
   1.354 +    X (\<lambda>x. (Y x,Z x)) =
   1.355 +    (\<Sum> (x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.
   1.356 +      distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} *
   1.357 +      log b (distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} /
   1.358 +              (distribution X {x} * distribution (\<lambda>x. (Y x,Z x)) {(y,z)})))" (is "_ = setsum ?log ?space")
   1.359 +  unfolding Let_def mutual_information_def KL_divergence_def using finite_space
   1.360 +proof (subst finite_measure_space.integral_finite_singleton,
   1.361 +       simp_all add: prod_measure_space_def sigma_prod_sets_finite joint_distribution)
   1.362 +  let ?sets = "Pow (X ` space M \<times> Y ` space M \<times> Z ` space M)"
   1.363 +    and ?measure = "distribution (\<lambda>x. (X x, Y x, Z x))"
   1.364 +  let ?P = "\<lparr> space = ?space, sets = ?sets, measure = ?measure\<rparr>"
   1.365 +
   1.366 +  show "finite_measure_space ?P"
   1.367 +  proof (rule finite_Pow_additivity_sufficient, simp_all)
   1.368 +    show "finite ?space" using finite_space by auto
   1.369 +
   1.370 +    show "positive ?P ?measure"
   1.371 +      using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive)
   1.372 +
   1.373 +    show "additive ?P ?measure"
   1.374 +    proof (simp add: additive_def distribution_def, safe)
   1.375 +      fix x y assume "x \<subseteq> ?space" and "y \<subseteq> ?space"
   1.376 +      assume "x \<inter> y = {}"
   1.377 +      thus "prob (((\<lambda>x. (X x, Y x, Z x)) -` x \<union> (\<lambda>x. (X x, Y x, Z x)) -` y) \<inter> space M) =
   1.378 +            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)"
   1.379 +        apply (subst measure_additive[unfolded sets_eq_Pow, simplified])
   1.380 +        by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob])
   1.381 +    qed
   1.382 +  qed
   1.383 +
   1.384 +  let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
   1.385 +  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>"
   1.386 +  let ?u = "prod_measure ?X ?YZ"
   1.387 +
   1.388 +  from finite_measure_space[of X] finite_measure_space_image_prod[of Y Z]
   1.389 +  have ms_X: "measure_space ?X" and ms_YZ: "measure_space ?YZ"
   1.390 +    by (simp_all add: finite_measure_space_def)
   1.391 +
   1.392 +  show "(\<Sum>x \<in> ?space. log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
   1.393 +    (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x})
   1.394 +    = setsum ?log ?space"
   1.395 +  proof (rule setsum_cong)
   1.396 +    fix x assume x: "x \<in> ?space"
   1.397 +    then obtain d e f where x_Pair: "x = (d, e, f)"
   1.398 +      and d: "d \<in> X ` space M"
   1.399 +      and e: "e \<in> Y ` space M"
   1.400 +      and f: "f \<in> Z ` space M" by auto
   1.401 +
   1.402 +    { fix x assume m_0: "?u {x} = 0"
   1.403 +
   1.404 +      let ?PROD = "(\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M"
   1.405 +      obtain a b c where Pair: "x = (a, b, c)" by (cases x)
   1.406 +      hence "?PROD = (X -` {a} \<inter> space M) \<inter> ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M)"
   1.407 +        and x_prod: "{x} = {a} \<times> {(b, c)}" by auto
   1.408 +
   1.409 +      have "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0"
   1.410 +      proof (cases "{a} \<subseteq> X ` space M")
   1.411 +        case False
   1.412 +        hence "?PROD = {}"
   1.413 +          unfolding Pair by auto
   1.414 +        thus ?thesis by (auto simp: distribution_def)
   1.415 +      next
   1.416 +        have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0"
   1.417 +          using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0])
   1.418 +
   1.419 +        case True
   1.420 +        with prod_measure_times[OF ms_X ms_YZ, simplified, of "{a}" "{(b,c)}"]
   1.421 +        have "prob (X -` {a} \<inter> space M) = 0 \<or> prob ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M) = 0"
   1.422 +          (is "prob ?X = 0 \<or> prob ?Y = 0") using m_0
   1.423 +          by (simp add: prod_measure_space_def distribution_def Pair)
   1.424 +        thus ?thesis
   1.425 +        proof (rule disjE)
   1.426 +          assume "prob ?X = 0"
   1.427 +          have "prob ?PROD \<le> prob ?X"
   1.428 +            using sets_eq_Pow Pair by (auto intro!: measure_mono)
   1.429 +          thus ?thesis using `prob ?X = 0` by (auto simp: distribution_def)
   1.430 +        next
   1.431 +          assume "prob ?Y = 0"
   1.432 +          have "prob ?PROD \<le> prob ?Y"
   1.433 +            using sets_eq_Pow Pair by (auto intro!: measure_mono)
   1.434 +          thus ?thesis using `prob ?Y = 0` by (auto simp: distribution_def)
   1.435 +        qed
   1.436 +      qed }
   1.437 +    note measure_zero_joint_distribution = this
   1.438 +
   1.439 +    from x_Pair d e f finite_space
   1.440 +    show "log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr>
   1.441 +      (distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x} = ?log x"
   1.442 +    apply (cases "distribution (\<lambda>x. (X x, Y x, Z x)) {x} \<noteq> 0")
   1.443 +    apply (subst finite_measure_space.RN_deriv_finite_singleton)
   1.444 +    proof simp_all
   1.445 +      show "measure_space ?P" using `finite_measure_space ?P` by (simp add: finite_measure_space_def)
   1.446 +
   1.447 +      from finite_measure_space_finite_prod_measure[OF finite_measure_space[of X]
   1.448 +        finite_measure_space_image_prod[of Y Z]] finite_space
   1.449 +      show "finite_measure_space \<lparr>space=?space, sets=?sets, measure=?u\<rparr>"
   1.450 +        by (simp add: prod_measure_space_def sigma_prod_sets_finite)
   1.451 +    next
   1.452 +      fix x assume "?u {x} = 0" thus "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0" by fact
   1.453 +    next
   1.454 +      assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
   1.455 +      show "?u {(d,e,f)} \<noteq> 0"
   1.456 +      proof
   1.457 +        assume "?u {(d, e, f)} = 0"
   1.458 +        from measure_zero_joint_distribution[OF this] jd_0
   1.459 +        show False by simp
   1.460 +      qed
   1.461 +    next
   1.462 +      assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0"
   1.463 +      with prod_measure_times[OF ms_X ms_YZ, simplified, of "{d}" "{(e,f)}"] d
   1.464 +      show "log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / ?u {(d, e, f)}) =
   1.465 +        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)}))"
   1.466 +        by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def)
   1.467 +    qed
   1.468 +  qed simp
   1.469 +qed
   1.470 +
   1.471 +definition (in prob_space)
   1.472 +  "entropy b s X = mutual_information b s s X X"
   1.473 +
   1.474 +abbreviation (in finite_prob_space)
   1.475 +  finite_entropy ("\<H>\<^bsub>_\<^esub>'(_')") where
   1.476 +  "\<H>\<^bsub>b\<^esub>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X"
   1.477 +
   1.478 +abbreviation (in finite_prob_space)
   1.479 +  finite_entropy_2 ("\<H>'(_')") where
   1.480 +  "\<H>(X) \<equiv> \<H>\<^bsub>2\<^esub>(X)"
   1.481 +
   1.482 +lemma (in finite_prob_space) finite_entropy_reduce:
   1.483 +  assumes "1 < b"
   1.484 +  shows "\<H>\<^bsub>b\<^esub>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
   1.485 +proof -
   1.486 +  have fin: "finite (X ` space M)" using finite_space by simp
   1.487 +
   1.488 +  have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
   1.489 +
   1.490 +  { fix x y
   1.491 +    have "(\<lambda>x. (X x, X x)) -` {(x, y)} = (if x = y then X -` {x} else {})" by auto
   1.492 +    hence "distribution (\<lambda>x. (X x, X x))  {(x,y)} = (if x = y then distribution X {x} else 0)"
   1.493 +      unfolding distribution_def by auto }
   1.494 +  moreover
   1.495 +  have "\<And>x. 0 \<le> distribution X x"
   1.496 +    unfolding distribution_def using finite_space sets_eq_Pow by (auto intro: positive)
   1.497 +  hence "\<And>x. distribution X x \<noteq> 0 \<Longrightarrow> 0 < distribution X x" by (auto simp: le_less)
   1.498 +  ultimately
   1.499 +  show ?thesis using `1 < b`
   1.500 +    by (auto intro!: setsum_cong
   1.501 +      simp: log_inverse If_mult_distr setsum_cases[OF fin] inverse_eq_divide[symmetric]
   1.502 +        entropy_def setsum_negf[symmetric] joint_distribution finite_mutual_information_reduce
   1.503 +        setsum_cartesian_product[symmetric])
   1.504 +qed
   1.505 +
   1.506 +lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}"
   1.507 +proof (rule inj_onI, simp)
   1.508 +  fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y"
   1.509 +  show "x = y"
   1.510 +  proof (cases rule: linorder_cases)
   1.511 +    assume "x < y" hence "log b x < log b y"
   1.512 +      using log_less_cancel_iff[OF `1 < b`] pos by simp
   1.513 +    thus ?thesis using * by simp
   1.514 +  next
   1.515 +    assume "y < x" hence "log b y < log b x"
   1.516 +      using log_less_cancel_iff[OF `1 < b`] pos by simp
   1.517 +    thus ?thesis using * by simp
   1.518 +  qed simp
   1.519 +qed
   1.520 +
   1.521 +definition (in prob_space)
   1.522 +  "conditional_mutual_information b s1 s2 s3 X Y Z \<equiv>
   1.523 +    let prod_space =
   1.524 +      prod_measure_space \<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr>
   1.525 +                         \<lparr>space = space s3, sets = sets s3, measure = distribution Z\<rparr>
   1.526 +    in
   1.527 +      mutual_information b s1 prod_space X (\<lambda>x. (Y x, Z x)) -
   1.528 +      mutual_information b s1 s3 X Z"
   1.529 +
   1.530 +abbreviation (in finite_prob_space)
   1.531 +  finite_conditional_mutual_information ("\<I>\<^bsub>_\<^esub>'( _ ; _ | _ ')") where
   1.532 +  "\<I>\<^bsub>b\<^esub>(X ; Y | Z) \<equiv> conditional_mutual_information b
   1.533 +    \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
   1.534 +    \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr>
   1.535 +    \<lparr> space = Z`space M, sets = Pow (Z`space M) \<rparr>
   1.536 +    X Y Z"
   1.537 +
   1.538 +abbreviation (in finite_prob_space)
   1.539 +  finite_conditional_mutual_information_2 ("\<I>'( _ ; _ | _ ')") where
   1.540 +  "\<I>(X ; Y | Z) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y | Z)"
   1.541 +
   1.542 +lemma image_pair_eq_Sigma:
   1.543 +  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
   1.544 +proof (safe intro!: imageI vimageI, simp_all)
   1.545 +  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
   1.546 +  show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" unfolding eq[symmetric]
   1.547 +    using * by auto
   1.548 +qed
   1.549 +
   1.550 +lemma inj_on_swap: "inj_on (\<lambda>(x,y). (y,x)) A" by (auto intro!: inj_onI)
   1.551 +
   1.552 +lemma (in finite_prob_space) finite_conditional_mutual_information_reduce:
   1.553 +  assumes "1 < b"
   1.554 +  shows "\<I>\<^bsub>b\<^esub>(X ; Y | Z) =
   1.555 +	- (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
   1.556 +             distribution (\<lambda>x. (X x, Z x)) {(x,z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(x,z)} / distribution Z {z}))
   1.557 +	+ (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
   1.558 +             distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *
   1.559 +             log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}/
   1.560 +             distribution (\<lambda>x. (Y x, Z x)) {(y, z)}))" (is "_ = ?rhs")
   1.561 +unfolding conditional_mutual_information_def Let_def using finite_space
   1.562 +apply (simp add: prod_measure_space_def sigma_prod_sets_finite)
   1.563 +apply (subst mutual_information_cong[of _ "\<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>"
   1.564 +  _ "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M)\<rparr>"], simp_all)
   1.565 +apply (subst finite_mutual_information_reduce_prod, simp_all)
   1.566 +apply (subst finite_mutual_information_reduce, simp_all)
   1.567 +proof -
   1.568 +  let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))"
   1.569 +  let ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
   1.570 +  let ?dYZ = "distribution (\<lambda>x. (Y x, Z x))"
   1.571 +  let ?dX = "distribution X"
   1.572 +  let ?dY = "distribution Y"
   1.573 +  let ?dZ = "distribution Z"
   1.574 +
   1.575 +  have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto
   1.576 +  { fix x y
   1.577 +    have "(\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M =
   1.578 +      (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
   1.579 +    hence "?dXYZ {(X x, y)} = (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then ?dXYZ {(X x, y)} else 0)"
   1.580 +      unfolding distribution_def by auto }
   1.581 +  note split_measure = this
   1.582 +
   1.583 +  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
   1.584 +
   1.585 +  have cong: "\<And>A B C D. \<lbrakk> A = C ; B = D \<rbrakk> \<Longrightarrow> A + B = C + D" by auto
   1.586 +
   1.587 +  { fix A f have "setsum f A = setsum (\<lambda>(x, y). f (y, x)) ((\<lambda>(x, y). (y, x)) ` A)"
   1.588 +    using setsum_reindex[OF inj_on_swap, of "\<lambda>(x, y). f (y, x)" A] by (simp add: split_twice) }
   1.589 +  note setsum_reindex_swap = this
   1.590 +
   1.591 +  { fix A B f assume *: "finite A" "\<forall>x\<in>A. finite (B x)"
   1.592 +    have "(\<Sum>x\<in>Sigma A B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) (B x))"
   1.593 +      unfolding setsum_Sigma[OF *] by simp }
   1.594 +  note setsum_Sigma = this
   1.595 +
   1.596 +  { fix x
   1.597 +    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)})"
   1.598 +      apply (subst setsum_reindex_swap)
   1.599 +      apply (simp add: image_image distribution_def)
   1.600 +      unfolding image_pair_eq_Sigma
   1.601 +      apply (subst setsum_Sigma)
   1.602 +      using finite_space apply simp_all
   1.603 +      apply (rule setsum_cong[OF refl])
   1.604 +      apply (subst measure_finitely_additive'')
   1.605 +      by (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) }
   1.606 +
   1.607 +  thus "(\<Sum>(x, y, z)\<in>X ` space M \<times> Y ` space M \<times> Z ` space M.
   1.608 +      ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / (?dX {x} * ?dYZ {(y, z)}))) -
   1.609 +    (\<Sum>(x, y)\<in>X ` space M \<times> Z ` space M.
   1.610 +      ?dXZ {(x, y)} * log b (?dXZ {(x, y)} / (?dX {x} * ?dZ {y}))) =
   1.611 +  - (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M).
   1.612 +      ?dXZ {(x,z)} * log b (?dXZ {(x,z)} / ?dZ {z})) +
   1.613 +    (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M).
   1.614 +      ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / ?dYZ {(y, z)}))"
   1.615 +    using finite_space
   1.616 +    apply (auto simp: setsum_cartesian_product[symmetric] setsum_negf[symmetric]
   1.617 +                      setsum_addf[symmetric] diff_minus
   1.618 +      intro!: setsum_cong[OF refl])
   1.619 +    apply (subst split_measure)
   1.620 +    apply (simp add: If_mult_distr setsum_cases sets distribution_log_split[OF assms, of X])
   1.621 +    apply (subst add_commute)
   1.622 +    by (simp add: setsum_subtractf setsum_negf field_simps setsum_right_distrib[symmetric] sets_eq_Pow)
   1.623 +qed
   1.624 +
   1.625 +definition (in prob_space)
   1.626 +  "conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y"
   1.627 +
   1.628 +abbreviation (in finite_prob_space)
   1.629 +  finite_conditional_entropy ("\<H>\<^bsub>_\<^esub>'(_ | _')") where
   1.630 +  "\<H>\<^bsub>b\<^esub>(X | Y) \<equiv> conditional_entropy b
   1.631 +    \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr>
   1.632 +    \<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y"
   1.633 +
   1.634 +abbreviation (in finite_prob_space)
   1.635 +  finite_conditional_entropy_2 ("\<H>'(_ | _')") where
   1.636 +  "\<H>(X | Y) \<equiv> \<H>\<^bsub>2\<^esub>(X | Y)"
   1.637 +
   1.638 +lemma (in finite_prob_space) finite_conditional_entropy_reduce:
   1.639 +  assumes "1 < b"
   1.640 +  shows "\<H>\<^bsub>b\<^esub>(X | Z) =
   1.641 +     - (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
   1.642 +         joint_distribution X Z {(x, z)} *
   1.643 +         log b (joint_distribution X Z {(x, z)} / distribution Z {z}))"
   1.644 +proof -
   1.645 +  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
   1.646 +  show ?thesis
   1.647 +    unfolding finite_conditional_mutual_information_reduce[OF assms]
   1.648 +      conditional_entropy_def joint_distribution_def distribution_def *
   1.649 +    by (auto intro!: setsum_0')
   1.650 +qed
   1.651 +
   1.652 +lemma (in finite_prob_space) finite_mutual_information_eq_entropy_conditional_entropy:
   1.653 +  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 = _")
   1.654 +  unfolding finite_mutual_information_reduce
   1.655 +    finite_entropy_reduce[OF assms]
   1.656 +    finite_conditional_entropy_reduce[OF assms]
   1.657 +    joint_distribution diff_minus_eq_add
   1.658 +  using finite_space
   1.659 +  apply (auto simp add: setsum_addf[symmetric] setsum_subtractf
   1.660 +      setsum_Sigma[symmetric] distribution_log_split[OF assms] setsum_negf[symmetric]
   1.661 +    intro!: setsum_cong[OF refl])
   1.662 +  apply (simp add: setsum_negf setsum_left_distrib[symmetric])
   1.663 +proof (rule disjI2)
   1.664 +  let ?dX = "distribution X"
   1.665 +  and ?dXZ = "distribution (\<lambda>x. (X x, Z x))"
   1.666 +
   1.667 +  fix x assume "x \<in> space M"
   1.668 +  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
   1.669 +  thus "(\<Sum>z\<in>Z ` space M. distribution (\<lambda>x. (X x, Z x)) {(X x, z)}) = distribution X {X x}"
   1.670 +    unfolding distribution_def
   1.671 +    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"])
   1.672 +    using finite_space sets_eq_Pow by auto
   1.673 +qed
   1.674 +
   1.675 +(* -------------Entropy of a RV with a certain event is zero---------------- *)
   1.676 +
   1.677 +lemma (in finite_prob_space) finite_entropy_certainty_eq_0:
   1.678 +  assumes "x \<in> X ` space M" and "distribution X {x} = 1" and "b > 1"
   1.679 +  shows "\<H>\<^bsub>b\<^esub>(X) = 0"
   1.680 +proof -
   1.681 +  interpret X: finite_prob_space "\<lparr> space = X ` space M,
   1.682 +    sets = Pow (X ` space M),
   1.683 +    measure = distribution X\<rparr>" by (rule finite_prob_space)
   1.684 +
   1.685 +  have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"
   1.686 +    using X.measure_compl[of "{x}"] assms by auto
   1.687 +  also have "\<dots> = 0" using X.prob_space assms by auto
   1.688 +  finally have X0: "distribution X (X ` space M - {x}) = 0" by auto
   1.689 +
   1.690 +  { fix y assume asm: "y \<noteq> x" "y \<in> X ` space M"
   1.691 +    hence "{y} \<subseteq> X ` space M - {x}" by auto
   1.692 +    from X.measure_mono[OF this] X0 X.positive[of "{y}"] asm
   1.693 +    have "distribution X {y} = 0" by auto }
   1.694 +
   1.695 +  hence fi: "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = (if x = y then 1 else 0)"
   1.696 +    using assms by auto
   1.697 +
   1.698 +  have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp
   1.699 +
   1.700 +  show ?thesis
   1.701 +    unfolding finite_entropy_reduce[OF `b > 1`] by (auto simp: y fi)
   1.702 +qed
   1.703 +(* --------------- upper bound on entropy for a rv ------------------------- *)
   1.704 +
   1.705 +definition convex_set :: "real set \<Rightarrow> bool"
   1.706 +where
   1.707 +  "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)"
   1.708 +
   1.709 +lemma pos_is_convex:
   1.710 +  shows "convex_set {0 <..}"
   1.711 +unfolding convex_set_def
   1.712 +proof safe
   1.713 +  fix x y \<mu> :: real
   1.714 +  assume asms: "\<mu> \<ge> 0" "\<mu> \<le> 1" "x > 0" "y > 0"
   1.715 +  { assume "\<mu> = 0"
   1.716 +    hence "\<mu> * x + (1 - \<mu>) * y = y" by simp
   1.717 +    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
   1.718 +  moreover
   1.719 +  { assume "\<mu> = 1"
   1.720 +    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp }
   1.721 +  moreover
   1.722 +  { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
   1.723 +    hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
   1.724 +    hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms
   1.725 +      apply (subst add_nonneg_pos[of "\<mu> * x" "(1 - \<mu>) * y"])
   1.726 +      using real_mult_order by auto fastsimp }
   1.727 +  ultimately show "\<mu> * x + (1 - \<mu>) * y > 0" using assms by blast
   1.728 +qed
   1.729 +
   1.730 +definition convex_fun :: "(real \<Rightarrow> real) \<Rightarrow> real set \<Rightarrow> bool"
   1.731 +where
   1.732 +  "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 
   1.733 +                   \<longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y))"
   1.734 +
   1.735 +lemma pos_convex_function:
   1.736 +  fixes f :: "real \<Rightarrow> real"
   1.737 +  assumes "convex_set C"
   1.738 +  assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
   1.739 +  shows "convex_fun f C"
   1.740 +unfolding convex_fun_def
   1.741 +using assms
   1.742 +proof safe
   1.743 +  fix x y \<mu> :: real
   1.744 +  let ?x = "\<mu> * x + (1 - \<mu>) * y"
   1.745 +  assume asm: "convex_set C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
   1.746 +  hence "1 - \<mu> \<ge> 0" by auto
   1.747 +  hence xpos: "?x \<in> C" using asm unfolding convex_set_def by auto
   1.748 +  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) 
   1.749 +            \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
   1.750 +    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
   1.751 +      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
   1.752 +  hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
   1.753 +    by (auto simp add:field_simps)
   1.754 +  thus "\<mu> * f x + (1 - \<mu>) * f y \<ge> f ?x" by simp
   1.755 +qed
   1.756 +
   1.757 +lemma atMostAtLeast_subset_convex:
   1.758 +  assumes "convex_set C"
   1.759 +  assumes "x \<in> C" "y \<in> C" "x < y"
   1.760 +  shows "{x .. y} \<subseteq> C"
   1.761 +proof safe
   1.762 +  fix z assume zasm: "z \<in> {x .. y}"
   1.763 +  { assume asm: "x < z" "z < y"
   1.764 +    let "?\<mu>" = "(y - z) / (y - x)"
   1.765 +    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps)
   1.766 +    hence comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C" 
   1.767 +      using assms[unfolded convex_set_def] by blast
   1.768 +    have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
   1.769 +      by (auto simp add:field_simps)
   1.770 +    also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
   1.771 +      using assms unfolding add_divide_distrib by (auto simp:field_simps)
   1.772 +    also have "\<dots> = z" 
   1.773 +      using assms by (auto simp:field_simps)
   1.774 +    finally have "z \<in> C"
   1.775 +      using comb by auto } note less = this
   1.776 +  show "z \<in> C" using zasm less assms
   1.777 +    unfolding atLeastAtMost_iff le_less by auto
   1.778 +qed
   1.779 +
   1.780 +lemma f''_imp_f':
   1.781 +  fixes f :: "real \<Rightarrow> real"
   1.782 +  assumes "convex_set C"
   1.783 +  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
   1.784 +  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
   1.785 +  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   1.786 +  assumes "x \<in> C" "y \<in> C"
   1.787 +  shows "f' x * (y - x) \<le> f y - f x"
   1.788 +using assms
   1.789 +proof -
   1.790 +  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x"
   1.791 +    hence ge: "y - x > 0" "y - x \<ge> 0" by auto
   1.792 +    from asm have le: "x - y < 0" "x - y \<le> 0" by auto
   1.793 +    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
   1.794 +      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `y \<in> C` `x < y`],
   1.795 +        THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
   1.796 +      by auto
   1.797 +    hence "z1 \<in> C" using atMostAtLeast_subset_convex
   1.798 +      `convex_set C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
   1.799 +    from z1 have z1': "f x - f y = (x - y) * f' z1"
   1.800 +      by (simp add:field_simps)
   1.801 +    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
   1.802 +      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1`],
   1.803 +        THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
   1.804 +      by auto
   1.805 +    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
   1.806 +      using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y`],
   1.807 +        THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
   1.808 +      by auto
   1.809 +    have "f' y - (f x - f y) / (x - y) = f' y - f' z1" 
   1.810 +      using asm z1' by auto
   1.811 +    also have "\<dots> = (y - z1) * f'' z3" using z3 by auto
   1.812 +    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
   1.813 +    have A': "y - z1 \<ge> 0" using z1 by auto
   1.814 +    have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
   1.815 +      `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
   1.816 +    hence B': "f'' z3 \<ge> 0" using assms by auto
   1.817 +    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
   1.818 +    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
   1.819 +    from mult_right_mono_neg[OF this le(2)]
   1.820 +    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
   1.821 +      unfolding diff_def using real_add_mult_distrib by auto
   1.822 +    hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
   1.823 +    hence res: "f' y * (x - y) \<le> f x - f y" by auto
   1.824 +    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
   1.825 +      using asm z1 by auto
   1.826 +    also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto
   1.827 +    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
   1.828 +    have A: "z1 - x \<ge> 0" using z1 by auto
   1.829 +    have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
   1.830 +      `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
   1.831 +    hence B: "f'' z2 \<ge> 0" using assms by auto
   1.832 +    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
   1.833 +    from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
   1.834 +    from mult_right_mono[OF this ge(2)]
   1.835 +    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)" 
   1.836 +      unfolding diff_def using real_add_mult_distrib by auto
   1.837 +    hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
   1.838 +    hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
   1.839 +      using res by auto } note less_imp = this
   1.840 +  { fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y"
   1.841 +    hence"f y - f x \<ge> f' x * (y - x)"
   1.842 +    unfolding neq_iff apply safe
   1.843 +    using less_imp by auto } note neq_imp = this
   1.844 +  moreover
   1.845 +  { fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y"
   1.846 +    hence "f y - f x \<ge> f' x * (y - x)" by auto }
   1.847 +  ultimately show ?thesis using assms by blast
   1.848 +qed
   1.849 +
   1.850 +lemma f''_ge0_imp_convex:
   1.851 +  fixes f :: "real \<Rightarrow> real"
   1.852 +  assumes conv: "convex_set C"
   1.853 +  assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
   1.854 +  assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
   1.855 +  assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
   1.856 +  shows "convex_fun f C"
   1.857 +using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
   1.858 +
   1.859 +lemma minus_log_convex:
   1.860 +  fixes b :: real
   1.861 +  assumes "b > 1"
   1.862 +  shows "convex_fun (\<lambda> x. - log b x) {0 <..}"
   1.863 +proof -
   1.864 +  have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
   1.865 +  hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
   1.866 +    using DERIV_minus by auto
   1.867 +  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
   1.868 +    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
   1.869 +  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
   1.870 +  have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
   1.871 +    by auto
   1.872 +  hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
   1.873 +    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
   1.874 +  have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
   1.875 +    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
   1.876 +  from f''_ge0_imp_convex[OF pos_is_convex, 
   1.877 +    unfolded greaterThan_iff, OF f' f''0 f''_ge0]
   1.878 +  show ?thesis by auto
   1.879 +qed
   1.880 +
   1.881 +lemma setsum_nonneg_0:
   1.882 +  fixes f :: "'a \<Rightarrow> real"
   1.883 +  assumes "finite s"
   1.884 +  assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   1.885 +  assumes "(\<Sum> i \<in> s. f i) = 0"
   1.886 +  assumes "i \<in> s"
   1.887 +  shows "f i = 0"
   1.888 +proof -
   1.889 +  { assume asm: "f i > 0"
   1.890 +    from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
   1.891 +    from setsum_nonneg[of "s - {i}" f, OF this]
   1.892 +    have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
   1.893 +    hence "(\<Sum> j \<in> s - {i}. f j) + f i > 0" using asm by auto
   1.894 +    from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
   1.895 +    have "(\<Sum> j \<in> s. f j) > 0" by auto
   1.896 +    hence "False" using assms by auto }
   1.897 +  thus ?thesis using assms by fastsimp
   1.898 +qed
   1.899 +
   1.900 +lemma setsum_nonneg_leq_1:
   1.901 +  fixes f :: "'a \<Rightarrow> real"
   1.902 +  assumes "finite s"
   1.903 +  assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   1.904 +  assumes "(\<Sum> i \<in> s. f i) = 1"
   1.905 +  assumes "i \<in> s"
   1.906 +  shows "f i \<le> 1"
   1.907 +proof -
   1.908 +  { assume asm: "f i > 1"
   1.909 +    from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto
   1.910 +    from setsum_nonneg[of "s - {i}" f, OF this]
   1.911 +    have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp
   1.912 +    hence "(\<Sum> j \<in> s - {i}. f j) + f i > 1" using asm by auto
   1.913 +    from this setsum.remove[of s i f, OF `finite s` `i \<in> s`]
   1.914 +    have "(\<Sum> j \<in> s. f j) > 1" by auto
   1.915 +    hence "False" using assms by auto }
   1.916 +  thus ?thesis using assms by fastsimp
   1.917 +qed
   1.918 +
   1.919 +lemma convex_set_setsum:
   1.920 +  assumes "finite s" "s \<noteq> {}"
   1.921 +  assumes "convex_set C"
   1.922 +  assumes "(\<Sum> i \<in> s. a i) = 1"
   1.923 +  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
   1.924 +  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
   1.925 +  shows "(\<Sum> j \<in> s. a j * y j) \<in> C"
   1.926 +using assms
   1.927 +proof (induct s arbitrary:a rule:finite_ne_induct)
   1.928 +  case (singleton i) note asms = this
   1.929 +  hence "a i = 1" by auto
   1.930 +  thus ?case using asms by auto
   1.931 +next
   1.932 +  case (insert i s) note asms = this
   1.933 +  { assume "a i = 1"
   1.934 +    hence "(\<Sum> j \<in> s. a j) = 0"
   1.935 +      using asms by auto
   1.936 +    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 
   1.937 +      using setsum_nonneg_0 asms by fastsimp
   1.938 +    hence ?case using asms by auto }
   1.939 +  moreover
   1.940 +  { assume asm: "a i \<noteq> 1"
   1.941 +    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
   1.942 +    have fis: "finite (insert i s)" using asms by auto
   1.943 +    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
   1.944 +    hence "a i < 1" using asm by auto
   1.945 +    hence i0: "1 - a i > 0" by auto
   1.946 +    let "?a j" = "a j / (1 - a i)"
   1.947 +    { fix j assume "j \<in> s"
   1.948 +      hence "?a j \<ge> 0" 
   1.949 +        using i0 asms divide_nonneg_pos 
   1.950 +        by fastsimp } note a_nonneg = this
   1.951 +    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
   1.952 +    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
   1.953 +    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
   1.954 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
   1.955 +    from this asms
   1.956 +    have "(\<Sum>j\<in>s. ?a j * y j) \<in> C" using a_nonneg by fastsimp
   1.957 +    hence "a i * y i + (1 - a i) * (\<Sum> j \<in> s. ?a j * y j) \<in> C"
   1.958 +      using asms[unfolded convex_set_def, rule_format] yai ai1 by auto
   1.959 +    hence "a i * y i + (\<Sum> j \<in> s. (1 - a i) * (?a j * y j)) \<in> C"
   1.960 +      using mult_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j * y j" s] by auto
   1.961 +    hence "a i * y i + (\<Sum> j \<in> s. a j * y j) \<in> C" using i0 by auto
   1.962 +    hence ?case using setsum.insert asms by auto }
   1.963 +  ultimately show ?case by auto
   1.964 +qed
   1.965 +
   1.966 +lemma convex_fun_setsum:
   1.967 +  fixes a :: "'a \<Rightarrow> real"
   1.968 +  assumes "finite s" "s \<noteq> {}"
   1.969 +  assumes "convex_fun f C"
   1.970 +  assumes "(\<Sum> i \<in> s. a i) = 1"
   1.971 +  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
   1.972 +  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C"
   1.973 +  shows "f (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
   1.974 +using assms
   1.975 +proof (induct s arbitrary:a rule:finite_ne_induct)
   1.976 +  case (singleton i)
   1.977 +  hence ai: "a i = 1" by auto
   1.978 +  thus ?case by auto
   1.979 +next
   1.980 +  case (insert i s) note asms = this
   1.981 +  hence "convex_fun f C" by simp
   1.982 +  from this[unfolded convex_fun_def, rule_format]
   1.983 +  have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk>
   1.984 +  \<Longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
   1.985 +    by simp
   1.986 +  { assume "a i = 1"
   1.987 +    hence "(\<Sum> j \<in> s. a j) = 0"
   1.988 +      using asms by auto
   1.989 +    hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 
   1.990 +      using setsum_nonneg_0 asms by fastsimp
   1.991 +    hence ?case using asms by auto }
   1.992 +  moreover
   1.993 +  { assume asm: "a i \<noteq> 1"
   1.994 +    from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto
   1.995 +    have fis: "finite (insert i s)" using asms by auto
   1.996 +    hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp
   1.997 +    hence "a i < 1" using asm by auto
   1.998 +    hence i0: "1 - a i > 0" by auto
   1.999 +    let "?a j" = "a j / (1 - a i)"
  1.1000 +    { fix j assume "j \<in> s"
  1.1001 +      hence "?a j \<ge> 0" 
  1.1002 +        using i0 asms divide_nonneg_pos 
  1.1003 +        by fastsimp } note a_nonneg = this
  1.1004 +    have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
  1.1005 +    hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
  1.1006 +    hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
  1.1007 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
  1.1008 +    have "convex_set C" using asms unfolding convex_fun_def by auto
  1.1009 +    hence asum: "(\<Sum> j \<in> s. ?a j * y j) \<in> C"
  1.1010 +      using asms convex_set_setsum[OF `finite s` `s \<noteq> {}` 
  1.1011 +        `convex_set C` a1 a_nonneg] by auto
  1.1012 +    have asum_le: "f (\<Sum> j \<in> s. ?a j * y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))"
  1.1013 +      using a_nonneg a1 asms by blast
  1.1014 +    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)"
  1.1015 +      using setsum.insert[of s i "\<lambda> j. a j * y j", OF `finite s` `i \<notin> s`] asms 
  1.1016 +      by (auto simp only:add_commute)
  1.1017 +    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j) / (1 - a i) + a i * y i)"
  1.1018 +      using i0 by auto
  1.1019 +    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j / (1 - a i)) + a i * y i)"
  1.1020 +      unfolding divide.setsum[of "\<lambda> j. a j * y j" s "1 - a i", symmetric] by auto
  1.1021 +    also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. ?a j * y j) + a i * y i)" by auto
  1.1022 +    also have "\<dots> \<le> (1 - a i) * f ((\<Sum> j \<in> s. ?a j * y j)) + a i * f (y i)"
  1.1023 +      using conv[of "y i" "(\<Sum> j \<in> s. ?a j * y j)" "a i", OF yai(1) asum yai(2) ai1]
  1.1024 +      by (auto simp only:add_commute)
  1.1025 +    also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
  1.1026 +      using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", 
  1.1027 +        OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
  1.1028 +    also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
  1.1029 +      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
  1.1030 +    also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
  1.1031 +    also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
  1.1032 +    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))"
  1.1033 +      by simp }
  1.1034 +  ultimately show ?case by auto
  1.1035 +qed
  1.1036 +
  1.1037 +lemma log_setsum:
  1.1038 +  assumes "finite s" "s \<noteq> {}"
  1.1039 +  assumes "b > 1"
  1.1040 +  assumes "(\<Sum> i \<in> s. a i) = 1"
  1.1041 +  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
  1.1042 +  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
  1.1043 +  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
  1.1044 +proof -
  1.1045 +  have "convex_fun (\<lambda> x. - log b x) {0 <..}"
  1.1046 +    by (rule minus_log_convex[OF `b > 1`])
  1.1047 +  hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
  1.1048 +    using convex_fun_setsum assms by blast
  1.1049 +  thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
  1.1050 +qed
  1.1051 +
  1.1052 +lemma (in finite_prob_space) finite_entropy_le_card:
  1.1053 +  assumes "1 < b"
  1.1054 +  shows "\<H>\<^bsub>b\<^esub>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
  1.1055 +proof -
  1.1056 +  interpret X: finite_prob_space "\<lparr>space = X ` space M,
  1.1057 +                                    sets = Pow (X ` space M),
  1.1058 +                                 measure = distribution X\<rparr>"
  1.1059 +    using finite_prob_space by auto
  1.1060 +  have triv: "\<And> x. (if distribution X {x} \<noteq> 0 then distribution X {x} else 0) = distribution X {x}"
  1.1061 +    by auto
  1.1062 +  hence sum1: "(\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x}) = 1"
  1.1063 +    using X.measure_finitely_additive''[of "X ` space M" "\<lambda> x. {x}", simplified]
  1.1064 +      sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
  1.1065 +    unfolding disjoint_family_on_def  X.prob_space[symmetric]
  1.1066 +    using finite_imageI[OF finite_space, of X] by (auto simp add:triv setsum_restrict_set)
  1.1067 +  have pos: "\<And> x. x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0} \<Longrightarrow> inverse (distribution X {x}) > 0"
  1.1068 +    using X.positive sets_eq_Pow unfolding inverse_positive_iff_positive less_le by auto
  1.1069 +  { assume asm: "X ` space M \<inter> {y. distribution X {y} \<noteq> 0} = {}" 
  1.1070 +    { fix x assume "x \<in> X ` space M"
  1.1071 +      hence "distribution X {x} = 0" using asm by blast }
  1.1072 +    hence A: "(\<Sum> x \<in> X ` space M. distribution X {x}) = 0" by auto
  1.1073 +    have B: "(\<Sum> x \<in> X ` space M. distribution X {x})
  1.1074 +      \<ge> (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x})"
  1.1075 +      using finite_imageI[OF finite_space, of X]
  1.1076 +      by (subst setsum_mono2) auto
  1.1077 +    from A B have "False" using sum1 by auto } note not_empty = this
  1.1078 +  { fix x assume asm: "x \<in> X ` space M"
  1.1079 +    have "- distribution X {x} * log b (distribution X {x})
  1.1080 +       = - (if distribution X {x} \<noteq> 0 
  1.1081 +            then distribution X {x} * log b (distribution X {x})
  1.1082 +            else 0)"
  1.1083 +      by auto
  1.1084 +    also have "\<dots> = (if distribution X {x} \<noteq> 0 
  1.1085 +          then distribution X {x} * - log b (distribution X {x})
  1.1086 +          else 0)"
  1.1087 +      by auto
  1.1088 +    also have "\<dots> = (if distribution X {x} \<noteq> 0
  1.1089 +                    then distribution X {x} * log b (inverse (distribution X {x}))
  1.1090 +                    else 0)"
  1.1091 +      using log_inverse `1 < b` X.positive[of "{x}"] asm by auto
  1.1092 +    finally have "- distribution X {x} * log b (distribution X {x})
  1.1093 +                 = (if distribution X {x} \<noteq> 0 
  1.1094 +                    then distribution X {x} * log b (inverse (distribution X {x}))
  1.1095 +                    else 0)"
  1.1096 +      by auto } note log_inv = this
  1.1097 +  have "- (\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))
  1.1098 +       = (\<Sum> x \<in> X ` space M. (if distribution X {x} \<noteq> 0 
  1.1099 +          then distribution X {x} * log b (inverse (distribution X {x}))
  1.1100 +          else 0))"
  1.1101 +    unfolding setsum_negf[symmetric] using log_inv by auto
  1.1102 +  also have "\<dots> = (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
  1.1103 +                          distribution X {x} * log b (inverse (distribution X {x})))"
  1.1104 +    unfolding setsum_restrict_set[OF finite_imageI[OF finite_space, of X]] by auto
  1.1105 +  also have "\<dots> \<le> log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}.
  1.1106 +                          distribution X {x} * (inverse (distribution X {x})))"
  1.1107 +    apply (subst log_setsum[OF _ _ `b > 1` sum1, 
  1.1108 +     unfolded greaterThan_iff, OF _ _ _]) using pos sets_eq_Pow
  1.1109 +      X.finite_space assms X.positive not_empty by auto
  1.1110 +  also have "\<dots> = log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. 1)"
  1.1111 +    by auto
  1.1112 +  also have "\<dots> \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))"
  1.1113 +    by auto
  1.1114 +  finally have "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
  1.1115 +               \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" by simp
  1.1116 +  thus ?thesis unfolding finite_entropy_reduce[OF assms] real_eq_of_nat by auto
  1.1117 +qed
  1.1118 +
  1.1119 +(* --------------- entropy is maximal for a uniform rv --------------------- *)
  1.1120 +
  1.1121 +lemma (in finite_prob_space) uniform_prob:
  1.1122 +  assumes "x \<in> space M"
  1.1123 +  assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}"
  1.1124 +  shows "prob {x} = 1 / real (card (space M))"
  1.1125 +proof -
  1.1126 +  have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}"
  1.1127 +    using assms(2)[OF _ `x \<in> space M`] by blast
  1.1128 +  have "1 = prob (space M)"
  1.1129 +    using prob_space by auto
  1.1130 +  also have "\<dots> = (\<Sum> x \<in> space M. prob {x})"
  1.1131 +    using measure_finitely_additive''[of "space M" "\<lambda> x. {x}", simplified]
  1.1132 +      sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format]
  1.1133 +      finite_space unfolding disjoint_family_on_def  prob_space[symmetric]
  1.1134 +    by (auto simp add:setsum_restrict_set)
  1.1135 +  also have "\<dots> = (\<Sum> y \<in> space M. prob {x})"
  1.1136 +    using prob_x by auto
  1.1137 +  also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
  1.1138 +  finally have one: "1 = real (card (space M)) * prob {x}"
  1.1139 +    using real_eq_of_nat by auto
  1.1140 +  hence two: "real (card (space M)) \<noteq> 0" by fastsimp 
  1.1141 +  from one have three: "prob {x} \<noteq> 0" by fastsimp
  1.1142 +  thus ?thesis using one two three divide_cancel_right
  1.1143 +    by (auto simp:field_simps)
  1.1144 +qed
  1.1145 +
  1.1146 +lemma (in finite_prob_space) finite_entropy_uniform_max:
  1.1147 +  assumes "b > 1"
  1.1148 +  assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
  1.1149 +  shows "\<H>\<^bsub>b\<^esub>(X) = log b (real (card (X ` space M)))"
  1.1150 +proof -
  1.1151 +  interpret X: finite_prob_space "\<lparr>space = X ` space M,
  1.1152 +                                    sets = Pow (X ` space M),
  1.1153 +                                 measure = distribution X\<rparr>"
  1.1154 +    using finite_prob_space by auto
  1.1155 +  { fix x assume xasm: "x \<in> X ` space M"
  1.1156 +    hence card_gt0: "real (card (X ` space M)) > 0"
  1.1157 +      using card_gt_0_iff X.finite_space by auto
  1.1158 +    from xasm have "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = distribution X {x}"
  1.1159 +      using assms by blast
  1.1160 +    hence "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x}))
  1.1161 +         = - (\<Sum> y \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"
  1.1162 +      by auto
  1.1163 +    also have "\<dots> = - real_of_nat (card (X ` space M)) * distribution X {x} * log b (distribution X {x})"
  1.1164 +      by auto
  1.1165 +    also have "\<dots> = - real (card (X ` space M)) * (1 / real (card (X ` space M))) * log b (1 / real (card (X ` space M)))"
  1.1166 +      unfolding real_eq_of_nat[symmetric]
  1.1167 +      by (auto simp: X.uniform_prob[simplified, OF xasm assms(2)])
  1.1168 +    also have "\<dots> = log b (real (card (X ` space M)))"
  1.1169 +      unfolding inverse_eq_divide[symmetric]
  1.1170 +      using card_gt0 log_inverse `b > 1` 
  1.1171 +      by (auto simp add:field_simps card_gt0)
  1.1172 +    finally have ?thesis
  1.1173 +      unfolding finite_entropy_reduce[OF `b > 1`] by auto }
  1.1174 +  moreover
  1.1175 +  { assume "X ` space M = {}"
  1.1176 +    hence "distribution X (X ` space M) = 0"
  1.1177 +      using X.empty_measure by simp
  1.1178 +    hence "False" using X.prob_space by auto }
  1.1179 +  ultimately show ?thesis by auto
  1.1180 +qed
  1.1181 +
  1.1182 +end