src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41023 9118eb4eb8dc
child 41689 3e39b0e730d6
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (* Author: Johannes Hoelzl, TU Muenchen *)
     2 
     3 header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *}
     4 
     5 theory Koepf_Duermuth_Countermeasure
     6   imports Information "~~/src/HOL/Library/Permutation"
     7 begin
     8 
     9 lemma
    10   fixes p u :: "'a \<Rightarrow> real"
    11   assumes "1 < b"
    12   assumes sum: "(\<Sum>i\<in>S. p i) = (\<Sum>i\<in>S. u i)"
    13   and pos: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> p i" "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> u i"
    14   and cont: "\<And>i. i \<in> S \<Longrightarrow> 0 < p i \<Longrightarrow> 0 < u i"
    15   shows "(\<Sum>i\<in>S. p i * log b (u i)) \<le> (\<Sum>i\<in>S. p i * log b (p i))"
    16 proof -
    17   have "(\<Sum>i\<in>S. p i * ln (u i) - p i * ln (p i)) \<le> (\<Sum>i\<in>S. u i - p i)"
    18   proof (intro setsum_mono)
    19     fix i assume [intro, simp]: "i \<in> S"
    20     show "p i * ln (u i) - p i * ln (p i) \<le> u i - p i"
    21     proof cases
    22       assume "p i = 0" with pos[of i] show ?thesis by simp
    23     next
    24       assume "p i \<noteq> 0"
    25       then have "0 < p i" "0 < u i" using pos[of i] cont[of i] by auto
    26       then have *: "0 < u i / p i" by (blast intro: divide_pos_pos cont)
    27       from `0 < p i` `0 < u i`
    28       have "p i * ln (u i) - p i * ln (p i) = p i * ln (u i / p i)"
    29         by (simp add: ln_div field_simps)
    30       also have "\<dots> \<le> p i * (u i / p i - 1)"
    31         using exp_ge_add_one_self[of "ln (u i / p i)"] pos[of i] exp_ln[OF *]
    32         by (auto intro!: mult_left_mono)
    33       also have "\<dots> = u i - p i"
    34         using `p i \<noteq> 0` by (simp add: field_simps)
    35       finally show ?thesis by simp
    36     qed
    37   qed
    38   also have "\<dots> = 0" using sum by (simp add: setsum_subtractf)
    39   finally show ?thesis using `1 < b` unfolding log_def setsum_subtractf
    40     by (auto intro!: divide_right_mono
    41              simp: times_divide_eq_right setsum_divide_distrib[symmetric])
    42 qed
    43 
    44 definition (in prob_space)
    45   "ordered_variable_partition X = (SOME f. bij_betw f {0..<card (X`space M)} (X`space M) \<and>
    46     (\<forall>i<card (X`space M). \<forall>j<card (X`space M). i \<le> j \<longrightarrow> distribution X {f i} \<le> distribution X {f j}))"
    47 
    48 lemma ex_ordered_bij_betw_nat_finite:
    49   fixes order :: "nat \<Rightarrow> 'a\<Colon>linorder"
    50   assumes "finite S"
    51   shows "\<exists>f. bij_betw f {0..<card S} S \<and> (\<forall>i<card S. \<forall>j<card S. i \<le> j \<longrightarrow> order (f i) \<le> order (f j))"
    52 proof -
    53   from ex_bij_betw_nat_finite [OF `finite S`] guess f .. note f = this
    54   let ?xs = "sort_key order (map f [0 ..< card S])"
    55 
    56   have "?xs <~~> map f [0 ..< card S]"
    57     unfolding multiset_of_eq_perm[symmetric] by (rule multiset_of_sort)
    58   from permutation_Ex_bij [OF this]
    59   obtain g where g: "bij_betw g {0..<card S} {0..<card S}" and
    60     map: "\<And>i. i<card S \<Longrightarrow> ?xs ! i = map f [0 ..< card S] ! g i"
    61     by (auto simp: atLeast0LessThan)
    62 
    63   { fix i assume "i < card S"
    64     then have "g i < card S" using g by (auto simp: bij_betw_def)
    65     with map [OF `i < card S`] have "f (g i) = ?xs ! i" by simp }
    66   note this[simp]
    67 
    68   show ?thesis
    69   proof (intro exI allI conjI impI)
    70     show "bij_betw (f\<circ>g) {0..<card S} S"
    71       using g f by (rule bij_betw_trans)
    72     fix i j assume [simp]: "i < card S" "j < card S" "i \<le> j"
    73     from sorted_nth_mono[of "map order ?xs" i j]
    74     show "order ((f\<circ>g) i) \<le> order ((f\<circ>g) j)" by simp
    75   qed
    76 qed
    77 
    78 lemma (in prob_space)
    79   assumes "finite (X`space M)"
    80   shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
    81   and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
    82     distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
    83 proof -
    84   
    85 qed
    86 
    87 definition (in prob_space)
    88   "order_distribution X i = real (distribution X {ordered_variable_partition X i})"
    89 
    90 definition (in prob_space)
    91   "guessing_entropy b X = (\<Sum>i<card(X`space M). real i * log b (order_distribution X i))"
    92 
    93 abbreviation (in finite_information_space)
    94   finite_guessing_entropy ("\<G>'(_')") where
    95   "\<G>(X) \<equiv> guessing_entropy b X"
    96 
    97 
    98 
    99 lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
   100   by auto
   101 
   102 definition extensional :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
   103   "extensional d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
   104 
   105 lemma extensional_empty[simp]: "extensional d {} = {\<lambda>x. d}"
   106   unfolding extensional_def by (simp add: expand_set_eq expand_fun_eq)
   107 
   108 lemma funset_eq_UN_fun_upd_I:
   109   assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
   110   and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
   111   and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
   112   shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
   113 proof safe
   114   fix f assume f: "f \<in> F (insert a A)"
   115   show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
   116   proof (rule UN_I[of "f(a := d)"])
   117     show "f(a := d) \<in> F A" using *[OF f] .
   118     show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
   119     proof (rule image_eqI[of _ _ "f a"])
   120       show "f a \<in> G (f(a := d))" using **[OF f] .
   121     qed simp
   122   qed
   123 next
   124   fix f x assume "f \<in> F A" "x \<in> G f"
   125   from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
   126 qed
   127 
   128 lemma extensional_insert[simp]:
   129   assumes "a \<notin> A"
   130   shows "extensional d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
   131   apply (rule funset_eq_UN_fun_upd_I)
   132   using assms
   133   by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
   134 
   135 lemma finite_extensional_funcset[simp, intro]:
   136   assumes "finite A" "finite B"
   137   shows "finite (extensional d A \<inter> (A \<rightarrow> B))"
   138   using assms by induct auto
   139 
   140 lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
   141   by (auto simp: expand_fun_eq)
   142 
   143 lemma card_funcset:
   144   assumes "finite A" "finite B"
   145   shows "card (extensional d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
   146 using `finite A` proof induct
   147   case (insert a A) thus ?case unfolding extensional_insert[OF `a \<notin> A`]
   148   proof (subst card_UN_disjoint, safe, simp_all)
   149     show "finite (extensional d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
   150       using `finite B` `finite A` by simp_all
   151   next
   152     fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
   153       ext: "f \<in> extensional d A" "g \<in> extensional d A"
   154     have "f a = d" "g a = d"
   155       using ext `a \<notin> A` by (auto simp add: extensional_def)
   156     with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
   157       by (auto simp: fun_upd_idem fun_upd_eq_iff)
   158   next
   159     { fix f assume "f \<in> extensional d A \<inter> (A \<rightarrow> B)"
   160       have "card (fun_upd f a ` B) = card B"
   161       proof (auto intro!: card_image inj_onI)
   162         fix b b' assume "f(a := b) = f(a := b')"
   163         from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
   164       qed }
   165     then show "(\<Sum>i\<in>extensional d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
   166       using insert by simp
   167   qed
   168 qed simp
   169 
   170 lemma set_of_list_extend:
   171   "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} =
   172     (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)"
   173   by (auto simp: length_Suc_conv)
   174 
   175 lemma
   176   assumes "finite A"
   177   shows finite_lists:
   178     "finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}" (is "finite (?lists n)")
   179   and card_list_length:
   180     "card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n"
   181 proof -
   182   from `finite A`
   183   have "(card {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} = (card A)^n) \<and>
   184          finite {xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)}"
   185   proof (induct n)
   186     case (Suc n)
   187     moreover note set_of_list_extend[of n A]
   188     moreover have "inj_on (\<lambda>(xs, n). n#xs) (?lists n \<times> A)"
   189       by (auto intro!: inj_onI)
   190     ultimately show ?case using assms by (auto simp: card_image)
   191   qed (simp cong: conj_cong)
   192   then show "finite (?lists n)" "card (?lists n) = card A ^ n"
   193     by auto
   194 qed
   195 
   196 locale finite_information =
   197   fixes \<Omega> :: "'a set"
   198     and p :: "'a \<Rightarrow> real"
   199     and b :: real
   200   assumes finite_space[simp, intro]: "finite \<Omega>"
   201   and p_sums_1[simp]: "(\<Sum>\<omega>\<in>\<Omega>. p \<omega>) = 1"
   202   and positive_p[simp, intro]: "\<And>x. 0 \<le> p x"
   203   and b_gt_1[simp, intro]: "1 < b"
   204 
   205 lemma (in finite_information) positive_p_sum[simp]: "0 \<le> setsum p X"
   206    by (auto intro!: setsum_nonneg)
   207 
   208 sublocale finite_information \<subseteq> finite_information_space "\<lparr> space = \<Omega>, sets = Pow \<Omega> \<rparr>" "\<lambda>S. Real (setsum p S)" b
   209 proof -
   210   show "finite_information_space \<lparr> space = \<Omega>, sets = Pow \<Omega> \<rparr> (\<lambda>S. Real (setsum p S)) b"
   211     unfolding finite_information_space_def finite_information_space_axioms_def
   212     unfolding finite_prob_space_def prob_space_def prob_space_axioms_def
   213     unfolding finite_measure_space_def finite_measure_space_axioms_def
   214     by (force intro!: sigma_algebra.finite_additivity_sufficient
   215               simp: additive_def sigma_algebra_Pow positive_def Real_eq_Real
   216                     setsum.union_disjoint finite_subset)
   217 qed
   218 
   219 lemma (in prob_space) prob_space_subalgebra:
   220   assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
   221   shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
   222 
   223 lemma (in measure_space) measure_space_subalgebra:
   224   assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
   225   shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>" sorry
   226 
   227 locale koepf_duermuth = K: finite_information keys K b + M: finite_information messages M b
   228     for b :: real
   229     and keys :: "'key set" and K :: "'key \<Rightarrow> real"
   230     and messages :: "'message set" and M :: "'message \<Rightarrow> real" +
   231   fixes observe :: "'key \<Rightarrow> 'message \<Rightarrow> 'observation"
   232     and n :: nat
   233 begin
   234 
   235 definition msgs :: "('key \<times> 'message list) set" where
   236   "msgs = keys \<times> {ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
   237 
   238 definition P :: "('key \<times> 'message list) \<Rightarrow> real" where
   239   "P = (\<lambda>(k, ms). K k * (\<Prod>i<length ms. M (ms ! i)))"
   240 
   241 end
   242 
   243 sublocale koepf_duermuth \<subseteq> finite_information msgs P b
   244 proof default
   245   show "finite msgs" unfolding msgs_def
   246     using finite_lists[OF M.finite_space, of n]
   247     by auto
   248 
   249   have [simp]: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A" by (force intro!: inj_onI)
   250 
   251   note setsum_right_distrib[symmetric, simp]
   252   note setsum_left_distrib[symmetric, simp]
   253   note setsum_cartesian_product'[simp]
   254 
   255   have "(\<Sum>ms | length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages). \<Prod>x<length ms. M (ms ! x)) = 1"
   256   proof (induct n)
   257     case 0 then show ?case by (simp cong: conj_cong)
   258   next
   259     case (Suc n)
   260     then show ?case
   261       by (simp add: comp_def set_of_list_extend
   262                     lessThan_eq_Suc_image setsum_reindex setprod_reindex)
   263   qed
   264   then show "setsum P msgs = 1"
   265     unfolding msgs_def P_def by simp
   266 
   267   fix x
   268   have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: setprod_nonneg)
   269   then show "0 \<le> P x"
   270     unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
   271 qed auto
   272 
   273 lemma SIGMA_image_vimage:
   274   "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
   275   by (auto simp: image_iff)
   276 
   277 lemma zero_le_eq_True: "0 \<le> (x::pextreal) \<longleftrightarrow> True" by simp
   278 
   279 lemma Real_setprod:
   280   assumes"\<And>i. i\<in>X \<Longrightarrow> 0 \<le> f i"
   281   shows "(\<Prod>i\<in>X. Real (f i)) = Real (\<Prod>i\<in>X. f i)"
   282 proof cases
   283   assume "finite X"
   284   from this assms show ?thesis by induct (auto simp: mult_le_0_iff)
   285 qed simp
   286 
   287 lemma inj_Cons[simp]: "\<And>X. inj_on (\<lambda>(xs, x). x#xs) X" by (auto intro!: inj_onI)
   288 
   289 lemma setprod_setsum_distrib_lists:
   290   fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
   291   shows "(\<Sum>ms\<in>{ms. length ms = n \<and> set ms \<subseteq> S \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
   292          (\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
   293 proof (induct n arbitrary: P)
   294   case 0 then show ?case by (simp cong: conj_cong)
   295 next
   296   case (Suc n)
   297   have *: "{ms. length ms = Suc n \<and> set ms \<subseteq> S \<and> (\<forall>i<Suc n. P i (ms ! i))} =
   298     (\<lambda>(xs, x). x#xs) ` ({ms. length ms = n \<and> set ms \<subseteq> S \<and> (\<forall>i<n. P (Suc i) (ms ! i))} \<times> {m\<in>S. P 0 m})"
   299     apply (auto simp: image_iff length_Suc_conv)
   300     apply force+
   301     apply (case_tac i)
   302     by force+
   303   show ?case unfolding *
   304     using Suc[of "\<lambda>i. P (Suc i)"]
   305     by (simp add: setsum_reindex split_conv setsum_cartesian_product'
   306       lessThan_eq_Suc_image setprod_reindex setsum_left_distrib[symmetric] setsum_right_distrib[symmetric])
   307 qed
   308 
   309 context koepf_duermuth
   310 begin
   311 
   312 definition observations :: "'observation set" where
   313   "observations = (\<Union>f\<in>observe ` keys. f ` messages)"
   314 
   315 lemma finite_observations[simp, intro]: "finite observations"
   316   unfolding observations_def by auto
   317 
   318 definition OB :: "'key \<times> 'message list \<Rightarrow> 'observation list" where
   319   "OB = (\<lambda>(k, ms). map (observe k) ms)"
   320 
   321 definition t :: "'observation list \<Rightarrow> 'observation \<Rightarrow> nat" where
   322   "t seq obs = length (filter (op = obs) seq)"
   323 
   324 lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
   325 proof -
   326   have "(t\<circ>OB)`msgs \<subseteq> extensional 0 observations \<inter> (observations \<rightarrow> {.. n})"
   327     unfolding observations_def extensional_def OB_def msgs_def
   328     by (auto simp add: t_def comp_def image_iff)
   329   with finite_extensional_funcset
   330   have "card ((t\<circ>OB)`msgs) \<le> card (extensional 0 observations \<inter> (observations \<rightarrow> {.. n}))"
   331     by (rule card_mono) auto
   332   also have "\<dots> = (n + 1) ^ card observations"
   333     by (subst card_funcset) auto
   334   finally show ?thesis .
   335 qed
   336 
   337 abbreviation
   338  "p A \<equiv> setsum P A"
   339 
   340 abbreviation probability ("\<P>'(_') _") where
   341  "\<P>(X) x \<equiv> real (distribution X x)"
   342 
   343 abbreviation joint_probability ("\<P>'(_, _') _") where
   344  "\<P>(X, Y) x \<equiv> real (joint_distribution X Y x)"
   345 
   346 abbreviation conditional_probability ("\<P>'(_|_') _") where
   347  "\<P>(X|Y) x \<equiv> \<P>(X, Y) x / \<P>(Y) (snd`x)"
   348 
   349 notation
   350   finite_entropy ("\<H>'( _ ')")
   351 
   352 notation
   353   finite_conditional_entropy ("\<H>'( _ | _ ')")
   354 
   355 notation
   356   finite_mutual_information ("\<I>'( _ ; _ ')")
   357 
   358 lemma t_eq_imp_bij_func:
   359   assumes "t xs = t ys"
   360   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
   361 proof -
   362   have "count (multiset_of xs) = count (multiset_of ys)"
   363     using assms by (simp add: expand_fun_eq count_multiset_of t_def)
   364   then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject .
   365   then show ?thesis by (rule permutation_Ex_func)
   366 qed
   367 
   368 lemma \<P>_k: assumes "k \<in> keys" shows "\<P>(fst) {k} = K k"
   369 proof -
   370   from assms have *:
   371       "fst -` {k} \<inter> msgs = {k}\<times>{ms. length ms = n \<and> (\<forall>M\<in>set ms. M \<in> messages)}"
   372     unfolding msgs_def by auto
   373   show "\<P>(fst) {k} = K k" unfolding distribution_def
   374     apply (simp add: *) unfolding P_def
   375     apply (simp add: setsum_cartesian_product')
   376     using setprod_setsum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"]
   377     by (simp add: setsum_right_distrib[symmetric] subset_eq setprod_1)
   378 qed
   379 
   380 lemma fst_image_msgs[simp]: "fst`msgs = keys"
   381 proof -
   382   from M.not_empty obtain m where "m \<in> messages" by auto
   383   then have *: "{m. length m = n \<and> (\<forall>x\<in>set m. x\<in>messages)} \<noteq> {}"
   384     by (auto intro!: exI[of _ "replicate n m"])
   385   then show ?thesis
   386     unfolding msgs_def fst_image_times if_not_P[OF *] by simp
   387 qed
   388 
   389 lemma ce_OB_eq_ce_t: "\<H>(fst | OB) = \<H>(fst | t\<circ>OB)"
   390 proof -
   391   txt {* Lemma 2 *}
   392 
   393   { fix k obs obs'
   394     assume "k \<in> keys" "K k \<noteq> 0" and obs': "obs' \<in> OB ` msgs" and obs: "obs \<in> OB ` msgs"
   395     assume "t obs = t obs'"
   396     from t_eq_imp_bij_func[OF this]
   397     obtain t_f where "bij_betw t_f {..<n} {..<n}" and
   398       obs_t_f: "\<And>i. i<n \<Longrightarrow> obs!i = obs' ! t_f i"
   399       using obs obs' unfolding OB_def msgs_def by auto
   400     then have t_f: "inj_on t_f {..<n}" "{..<n} = t_f`{..<n}" unfolding bij_betw_def by auto
   401 
   402     { fix obs assume "obs \<in> OB`msgs"
   403       then have **: "\<And>ms. length ms = n \<Longrightarrow> OB (k, ms) = obs \<longleftrightarrow> (\<forall>i<n. observe k (ms!i) = obs ! i)"
   404         unfolding OB_def msgs_def by (simp add: image_iff list_eq_iff_nth_eq)
   405 
   406       have "\<P>(OB, fst) {(obs, k)} / K k =
   407           p ({k}\<times>{ms. (k,ms) \<in> msgs \<and> OB (k,ms) = obs}) / K k"
   408         unfolding distribution_def by (auto intro!: arg_cong[where f=p])
   409       also have "\<dots> =
   410           (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
   411         unfolding P_def using `K k \<noteq> 0` `k \<in> keys`
   412         apply (simp add: setsum_cartesian_product' setsum_divide_distrib msgs_def ** cong: conj_cong)
   413         apply (subst setprod_setsum_distrib_lists[OF M.finite_space, unfolded subset_eq]) ..
   414       finally have "\<P>(OB, fst) {(obs, k)} / K k =
   415             (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
   416     note * = this
   417 
   418     have "\<P>(OB, fst) {(obs, k)} / K k = \<P>(OB, fst) {(obs', k)} / K k"
   419       unfolding *[OF obs] *[OF obs']
   420       using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod_reindex)
   421     then have "\<P>(OB, fst) {(obs, k)} = \<P>(OB, fst) {(obs', k)}"
   422       using `K k \<noteq> 0` by auto }
   423   note t_eq_imp = this
   424 
   425   let "?S obs" = "t -`{t obs} \<inter> OB`msgs"
   426   { fix k obs assume "k \<in> keys" "K k \<noteq> 0" and obs: "obs \<in> OB`msgs"
   427     have *: "((\<lambda>x. (t (OB x), fst x)) -` {(t obs, k)} \<inter> msgs) =
   428       (\<Union>obs'\<in>?S obs. ((\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs))" by auto
   429     have df: "disjoint_family_on (\<lambda>obs'. (\<lambda>x. (OB x, fst x)) -` {(obs', k)} \<inter> msgs) (?S obs)"
   430       unfolding disjoint_family_on_def by auto
   431     have "\<P>(t\<circ>OB, fst) {(t obs, k)} = (\<Sum>obs'\<in>?S obs. \<P>(OB, fst) {(obs', k)})"
   432       unfolding distribution_def comp_def
   433       using real_finite_measure_finite_Union[OF _ df]
   434       by (force simp add: * intro!: setsum_nonneg)
   435     also have "(\<Sum>obs'\<in>?S obs. \<P>(OB, fst) {(obs', k)}) = real (card (?S obs)) * \<P>(OB, fst) {(obs, k)}"
   436       by (simp add: t_eq_imp[OF `k \<in> keys` `K k \<noteq> 0` obs] real_eq_of_nat)
   437     finally have "\<P>(t\<circ>OB, fst) {(t obs, k)} = real (card (?S obs)) * \<P>(OB, fst) {(obs, k)}" .}
   438   note P_t_eq_P_OB = this
   439 
   440   { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
   441     have "\<P>(t\<circ>OB | fst) {(t obs, k)} =
   442       real (card (t -` {t obs} \<inter> OB ` msgs)) * \<P>(OB | fst) {(obs, k)}"
   443       using \<P>_k[OF `k \<in> keys`] P_t_eq_P_OB[OF `k \<in> keys` _ obs] by auto }
   444   note CP_t_K = this
   445 
   446   { fix k obs assume "k \<in> keys" and obs: "obs \<in> OB`msgs"
   447     then have "t -`{t obs} \<inter> OB`msgs \<noteq> {}" (is "?S \<noteq> {}") by auto
   448     then have "real (card ?S) \<noteq> 0" by auto
   449 
   450     have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / \<P>(t\<circ>OB) {t obs}"
   451       using real_distribution_order'[of fst k "t\<circ>OB" "t obs"]
   452       by (subst joint_distribution_commute) auto
   453     also have "\<P>(t\<circ>OB) {t obs} = (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'})"
   454       using setsum_real_distribution(2)[of "t\<circ>OB" fst "t obs", symmetric]
   455       using real_distribution_order'[of fst _ "t\<circ>OB" "t obs"] by (auto intro!: setsum_cong)
   456     also have "\<P>(t\<circ>OB | fst) {(t obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(t\<circ>OB|fst) {(t obs, k')} * \<P>(fst) {k'}) =
   457       \<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / (\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'})"
   458       using CP_t_K[OF `k\<in>keys` obs] CP_t_K[OF _ obs] `real (card ?S) \<noteq> 0`
   459       by (simp only: setsum_right_distrib[symmetric] ac_simps
   460           mult_divide_mult_cancel_left[OF `real (card ?S) \<noteq> 0`]
   461         cong: setsum_cong)
   462     also have "(\<Sum>k'\<in>keys. \<P>(OB|fst) {(obs, k')} * \<P>(fst) {k'}) = \<P>(OB) {obs}"
   463       using setsum_real_distribution(2)[of OB fst obs, symmetric]
   464       using real_distribution_order'[of fst _ OB obs] by (auto intro!: setsum_cong)
   465     also have "\<P>(OB | fst) {(obs, k)} * \<P>(fst) {k} / \<P>(OB) {obs} = \<P>(fst | OB) {(k, obs)}"
   466       using real_distribution_order'[of fst k OB obs]
   467       by (subst joint_distribution_commute) auto
   468     finally have "\<P>(fst | t\<circ>OB) {(k, t obs)} = \<P>(fst | OB) {(k, obs)}" . }
   469   note CP_T_eq_CP_O = this
   470 
   471   let "?H obs" = "(\<Sum>k\<in>keys. \<P>(fst|OB) {(k, obs)} * log b (\<P>(fst|OB) {(k, obs)})) :: real"
   472   let "?Ht obs" = "(\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, obs)} * log b (\<P>(fst|t\<circ>OB) {(k, obs)})) :: real"
   473 
   474   note [[simproc del: finite_information_space.mult_log]]
   475 
   476   { fix obs assume obs: "obs \<in> OB`msgs"
   477     have "?H obs = (\<Sum>k\<in>keys. \<P>(fst|t\<circ>OB) {(k, t obs)} * log b (\<P>(fst|t\<circ>OB) {(k, t obs)}))"
   478       using CP_T_eq_CP_O[OF _ obs]
   479       by simp
   480     then have "?H obs = ?Ht (t obs)" . }
   481   note * = this
   482 
   483   have **: "\<And>x f A. (\<Sum>y\<in>t-`{x}\<inter>A. f y (t y)) = (\<Sum>y\<in>t-`{x}\<inter>A. f y x)" by auto
   484 
   485   { fix x
   486     have *: "(\<lambda>x. t (OB x)) -` {t (OB x)} \<inter> msgs =
   487       (\<Union>obs\<in>?S (OB x). OB -` {obs} \<inter> msgs)" by auto
   488     have df: "disjoint_family_on (\<lambda>obs. OB -` {obs} \<inter> msgs) (?S (OB x))"
   489       unfolding disjoint_family_on_def by auto
   490     have "\<P>(t\<circ>OB) {t (OB x)} = (\<Sum>obs\<in>?S (OB x). \<P>(OB) {obs})"
   491       unfolding distribution_def comp_def
   492       using real_finite_measure_finite_Union[OF _ df]
   493       by (force simp add: * intro!: setsum_nonneg) }
   494   note P_t_sum_P_O = this
   495 
   496   txt {* Lemma 3 *}
   497   have "\<H>(fst | OB) = -(\<Sum>obs\<in>OB`msgs. \<P>(OB) {obs} * ?Ht (t obs))"
   498     unfolding conditional_entropy_eq_ce_with_hypothesis using * by simp
   499   also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
   500     apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
   501     apply (subst setsum_reindex)
   502     apply (fastsimp intro!: inj_onI)
   503     apply simp
   504     apply (subst setsum_Sigma[symmetric, unfolded split_def])
   505     using finite_space apply fastsimp
   506     using finite_space apply fastsimp
   507     apply (safe intro!: setsum_cong)
   508     using P_t_sum_P_O
   509     by (simp add: setsum_divide_distrib[symmetric] field_simps **
   510                   setsum_right_distrib[symmetric] setsum_left_distrib[symmetric])
   511   also have "\<dots> = \<H>(fst | t\<circ>OB)"
   512     unfolding conditional_entropy_eq_ce_with_hypothesis
   513     by (simp add: comp_def image_image[symmetric])
   514   finally show ?thesis .
   515 qed
   516 
   517 theorem "\<I>(fst ; OB) \<le> real (card observations) * log b (real n + 1)"
   518 proof -
   519   have "\<I>(fst ; OB) = \<H>(fst) - \<H>(fst | OB)"
   520     using mutual_information_eq_entropy_conditional_entropy .
   521   also have "\<dots> = \<H>(fst) - \<H>(fst | t\<circ>OB)"
   522     unfolding ce_OB_eq_ce_t ..
   523   also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
   524     unfolding entropy_chain_rule[symmetric] sign_simps
   525     by (subst entropy_commute) simp
   526   also have "\<dots> \<le> \<H>(t\<circ>OB)"
   527     using conditional_entropy_positive[of "t\<circ>OB" fst] by simp
   528   also have "\<dots> \<le> log b (real (card ((t\<circ>OB)`msgs)))"
   529     using entropy_le_card[of "t\<circ>OB"] by simp
   530   also have "\<dots> \<le> log b (real (n + 1)^card observations)"
   531     using card_T_bound not_empty
   532     by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power)
   533   also have "\<dots> = real (card observations) * log b (real n + 1)"
   534     by (simp add: log_nat_power real_of_nat_Suc)
   535   finally show ?thesis  .
   536 qed
   537 
   538 end
   539 
   540 end