author | hoelzl |
Wed, 07 Apr 2010 17:24:44 +0200 | |
changeset 36080 | 0d9affa4e73c |
child 36623 | d26348b667f2 |
permissions | -rw-r--r-- |
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1 |
theory Information |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
2 |
imports Probability_Space Product_Measure |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
3 |
begin |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
4 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
5 |
lemma pos_neg_part_abs: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
6 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
7 |
shows "pos_part f x + neg_part f x = \<bar>f x\<bar>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
8 |
unfolding real_abs_def pos_part_def neg_part_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
9 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
10 |
lemma pos_part_abs: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
11 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
12 |
shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
13 |
unfolding pos_part_def real_abs_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
14 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
15 |
lemma neg_part_abs: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
16 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
17 |
shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
18 |
unfolding neg_part_def real_abs_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
19 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
20 |
lemma (in measure_space) int_abs: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
21 |
assumes "integrable f" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
22 |
shows "integrable (\<lambda> x. \<bar>f x\<bar>)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
23 |
using assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
24 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
25 |
from assms obtain p q where pq: "p \<in> nnfis (pos_part f)" "q \<in> nnfis (neg_part f)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
26 |
unfolding integrable_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
27 |
hence "p + q \<in> nnfis (\<lambda> x. pos_part f x + neg_part f x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
28 |
using nnfis_add by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
29 |
hence "p + q \<in> nnfis (\<lambda> x. \<bar>f x\<bar>)" using pos_neg_part_abs[of f] by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
30 |
thus ?thesis unfolding integrable_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
31 |
using ext[OF pos_part_abs[of f], of "\<lambda> y. y"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
32 |
ext[OF neg_part_abs[of f], of "\<lambda> y. y"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
33 |
using nnfis_0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
34 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
35 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
36 |
lemma (in measure_space) measure_mono: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
37 |
assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
38 |
shows "measure M a \<le> measure M b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
39 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
40 |
have "b = a \<union> (b - a)" using assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
41 |
moreover have "{} = a \<inter> (b - a)" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
42 |
ultimately have "measure M b = measure M a + measure M (b - a)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
43 |
using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
44 |
moreover have "measure M (b - a) \<ge> 0" using positive assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
45 |
ultimately show "measure M a \<le> measure M b" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
46 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
47 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
48 |
lemma (in measure_space) integral_0: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
49 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
50 |
assumes "integrable f" "integral f = 0" "nonneg f" and borel: "f \<in> borel_measurable M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
51 |
shows "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
52 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
53 |
have "{x. f x \<noteq> 0} = {x. \<bar>f x\<bar> > 0}" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
54 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
55 |
{ fix y assume "y \<in> {x. \<bar> f x \<bar> > 0}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
56 |
hence "\<bar> f y \<bar> > 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
57 |
hence "\<exists> n. \<bar>f y\<bar> \<ge> inverse (real (Suc n))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
58 |
using ex_inverse_of_nat_Suc_less[of "\<bar>f y\<bar>"] less_imp_le unfolding real_of_nat_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
59 |
hence "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
60 |
by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
61 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
62 |
{ fix y assume "y \<in> (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
63 |
then obtain n where n: "y \<in> {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
64 |
hence "\<bar>f y\<bar> \<ge> inverse (real (Suc n))" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
65 |
hence "\<bar>f y\<bar> > 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
66 |
using real_of_nat_Suc_gt_zero |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
67 |
positive_imp_inverse_positive[of "real_of_nat (Suc n)"] by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
68 |
hence "y \<in> {x. \<bar>f x\<bar> > 0}" by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
69 |
ultimately have fneq0_UN: "{x. f x \<noteq> 0} = (\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
70 |
by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
71 |
{ fix n |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
72 |
have int_one: "integrable (\<lambda> x. \<bar>f x\<bar> ^ 1)" using int_abs assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
73 |
have "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
74 |
\<le> integral (\<lambda> x. \<bar>f x\<bar> ^ 1) / (inverse (real (Suc n)) ^ 1)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
75 |
using markov_ineq[OF `integrable f` _ int_one] real_of_nat_Suc_gt_zero by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
76 |
hence le0: "measure M (f -` {inverse (real (Suc n))..} \<inter> space M) \<le> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
77 |
using assms unfolding nonneg_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
78 |
have "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
79 |
apply (subst Int_commute) unfolding Int_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
80 |
using borel[unfolded borel_measurable_ge_iff] by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
81 |
hence m0: "measure M ({x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0 \<and> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
82 |
{x. f x \<ge> inverse (real (Suc n))} \<inter> space M \<in> sets M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
83 |
using positive le0 unfolding atLeast_def by fastsimp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
84 |
moreover hence "range (\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) \<subseteq> sets M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
85 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
86 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
87 |
{ fix n |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
88 |
have "inverse (real (Suc n)) \<ge> inverse (real (Suc (Suc n)))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
89 |
using less_imp_inverse_less real_of_nat_Suc_gt_zero[of n] by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
90 |
hence "\<And> x. f x \<ge> inverse (real (Suc n)) \<Longrightarrow> f x \<ge> inverse (real (Suc (Suc n)))" by (rule order_trans) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
91 |
hence "{x. f x \<ge> inverse (real (Suc n))} \<inter> space M |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
92 |
\<subseteq> {x. f x \<ge> inverse (real (Suc (Suc n)))} \<inter> space M" by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
93 |
ultimately have "(\<lambda> x. 0) ----> measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
94 |
using monotone_convergence[of "\<lambda> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
95 |
unfolding o_def by (simp del: of_nat_Suc) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
96 |
hence "measure M (\<Union> n. {x. f x \<ge> inverse (real (Suc n))} \<inter> space M) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
97 |
using LIMSEQ_const[of 0] LIMSEQ_unique by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
98 |
hence "measure M ((\<Union> n. {x. \<bar>f x\<bar> \<ge> inverse (real (Suc n))}) \<inter> space M) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
99 |
using assms unfolding nonneg_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
100 |
thus "measure M ({x. f x \<noteq> 0} \<inter> space M) = 0" using fneq0_UN by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
101 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
102 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
103 |
definition |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
104 |
"KL_divergence b M u v = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
105 |
measure_space.integral (M\<lparr>measure := u\<rparr>) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
106 |
(\<lambda>x. log b ((measure_space.RN_deriv (M \<lparr>measure := v\<rparr> ) u) x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
107 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
108 |
lemma (in finite_prob_space) finite_measure_space: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
109 |
shows "finite_measure_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
110 |
(is "finite_measure_space ?S") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
111 |
proof (rule finite_Pow_additivity_sufficient, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
112 |
show "finite (X ` space M)" using finite_space by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
113 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
114 |
show "positive ?S (distribution X)" unfolding distribution_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
115 |
unfolding positive_def using positive'[unfolded positive_def] sets_eq_Pow by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
116 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
117 |
show "additive ?S (distribution X)" unfolding additive_def distribution_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
118 |
proof (simp, safe) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
119 |
fix x y |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
120 |
have x: "(X -` x) \<inter> space M \<in> sets M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
121 |
and y: "(X -` y) \<inter> space M \<in> sets M" using sets_eq_Pow by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
122 |
assume "x \<inter> y = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
123 |
from additive[unfolded additive_def, rule_format, OF x y] this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
124 |
have "prob (((X -` x) \<union> (X -` y)) \<inter> space M) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
125 |
prob ((X -` x) \<inter> space M) + prob ((X -` y) \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
126 |
apply (subst Int_Un_distrib2) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
127 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
128 |
thus "prob ((X -` x \<union> X -` y) \<inter> space M) = prob (X -` x \<inter> space M) + prob (X -` y \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
129 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
130 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
131 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
132 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
133 |
lemma (in finite_prob_space) finite_prob_space: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
134 |
"finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
135 |
(is "finite_prob_space ?S") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
136 |
unfolding finite_prob_space_def prob_space_def prob_space_axioms_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
137 |
proof safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
138 |
show "finite_measure_space ?S" by (rule finite_measure_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
139 |
thus "measure_space ?S" by (simp add: finite_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
140 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
141 |
have "X -` X ` space M \<inter> space M = space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
142 |
thus "measure ?S (space ?S) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
143 |
by (simp add: distribution_def prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
144 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
145 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
146 |
lemma (in finite_prob_space) finite_measure_space_image_prod: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
147 |
"finite_measure_space \<lparr>space = X ` space M \<times> Y ` space M, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
148 |
sets = Pow (X ` space M \<times> Y ` space M), measure_space.measure = distribution (\<lambda>x. (X x, Y x))\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
149 |
(is "finite_measure_space ?Z") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
150 |
proof (rule finite_Pow_additivity_sufficient, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
151 |
show "finite (X ` space M \<times> Y ` space M)" using finite_space by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
152 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
153 |
let ?d = "distribution (\<lambda>x. (X x, Y x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
154 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
155 |
show "positive ?Z ?d" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
156 |
using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
157 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
158 |
show "additive ?Z ?d" unfolding additive_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
159 |
proof safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
160 |
fix x y assume "x \<in> sets ?Z" and "y \<in> sets ?Z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
161 |
assume "x \<inter> y = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
162 |
thus "?d (x \<union> y) = ?d x + ?d y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
163 |
apply (simp add: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
164 |
apply (subst measure_additive[unfolded sets_eq_Pow, simplified]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
165 |
by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
166 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
167 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
168 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
169 |
definition (in prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
170 |
"mutual_information b s1 s2 X Y \<equiv> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
171 |
let prod_space = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
172 |
prod_measure_space (\<lparr>space = space s1, sets = sets s1, measure = distribution X\<rparr>) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
173 |
(\<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr>) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
174 |
in |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
175 |
KL_divergence b prod_space (joint_distribution X Y) (measure prod_space)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
176 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
177 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
178 |
finite_mutual_information ("\<I>\<^bsub>_\<^esub>'(_ ; _')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
179 |
"\<I>\<^bsub>b\<^esub>(X ; Y) \<equiv> mutual_information b |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
180 |
\<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
181 |
\<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
182 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
183 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
184 |
finite_mutual_information_2 :: "('a \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd) \<Rightarrow> real" ("\<I>'(_ ; _')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
185 |
"\<I>(X ; Y) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
186 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
187 |
lemma (in prob_space) mutual_information_cong: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
188 |
assumes [simp]: "space S1 = space S3" "sets S1 = sets S3" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
189 |
"space S2 = space S4" "sets S2 = sets S4" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
190 |
shows "mutual_information b S1 S2 X Y = mutual_information b S3 S4 X Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
191 |
unfolding mutual_information_def by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
192 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
193 |
lemma (in prob_space) joint_distribution: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
194 |
"joint_distribution X Y = distribution (\<lambda>x. (X x, Y x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
195 |
unfolding joint_distribution_def_raw distribution_def_raw .. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
196 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
197 |
lemma (in finite_prob_space) finite_mutual_information_reduce: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
198 |
"\<I>\<^bsub>b\<^esub>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
199 |
distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} / |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
200 |
(distribution X {x} * distribution Y {y})))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
201 |
(is "_ = setsum ?log ?prod") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
202 |
unfolding Let_def mutual_information_def KL_divergence_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
203 |
proof (subst finite_measure_space.integral_finite_singleton, simp_all add: joint_distribution) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
204 |
let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure_space.measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
205 |
let ?Y = "\<lparr>space = Y ` space M, sets = Pow (Y ` space M), measure_space.measure = distribution Y\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
206 |
let ?P = "prod_measure_space ?X ?Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
207 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
208 |
interpret X: finite_measure_space "?X" by (rule finite_measure_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
209 |
moreover interpret Y: finite_measure_space "?Y" by (rule finite_measure_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
210 |
ultimately have ms_X: "measure_space ?X" and ms_Y: "measure_space ?Y" by unfold_locales |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
211 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
212 |
interpret P: finite_measure_space "?P" by (rule finite_measure_space_finite_prod_measure) (fact+) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
213 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
214 |
let ?P' = "measure_update (\<lambda>_. distribution (\<lambda>x. (X x, Y x))) ?P" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
215 |
from finite_measure_space_image_prod[of X Y] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
216 |
sigma_prod_sets_finite[OF X.finite_space Y.finite_space] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
217 |
show "finite_measure_space ?P'" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
218 |
by (simp add: X.sets_eq_Pow Y.sets_eq_Pow joint_distribution finite_measure_space_def prod_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
219 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
220 |
show "(\<Sum>x \<in> space ?P. log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
221 |
= setsum ?log ?prod" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
222 |
proof (rule setsum_cong) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
223 |
show "space ?P = ?prod" unfolding prod_measure_space_def by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
224 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
225 |
fix x assume x: "x \<in> X ` space M \<times> Y ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
226 |
then obtain d e where x_Pair: "x = (d, e)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
227 |
and d: "d \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
228 |
and e: "e \<in> Y ` space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
229 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
230 |
{ fix x assume m_0: "measure ?P {x} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
231 |
have "distribution (\<lambda>x. (X x, Y x)) {x} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
232 |
proof (cases x) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
233 |
case (Pair a b) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
234 |
hence "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = (X -` {a} \<inter> space M) \<inter> (Y -` {b} \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
235 |
and x_prod: "{x} = {a} \<times> {b}" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
236 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
237 |
let ?PROD = "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
238 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
239 |
show ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
240 |
proof (cases "{a} \<subseteq> X ` space M \<and> {b} \<subseteq> Y ` space M") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
241 |
case False |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
242 |
hence "?PROD = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
243 |
unfolding Pair by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
244 |
thus ?thesis by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
245 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
246 |
have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
247 |
using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
248 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
249 |
case True |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
250 |
with prod_measure_times[OF ms_X ms_Y, simplified, of "{a}" "{b}"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
251 |
have "prob (X -` {a} \<inter> space M) = 0 \<or> prob (Y -` {b} \<inter> space M) = 0" (is "?X_0 \<or> ?Y_0") using m_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
252 |
by (simp add: prod_measure_space_def distribution_def Pair) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
253 |
thus ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
254 |
proof (rule disjE) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
255 |
assume ?X_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
256 |
have "prob ?PROD \<le> prob (X -` {a} \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
257 |
using sets_eq_Pow Pair by (auto intro!: measure_mono) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
258 |
thus ?thesis using `?X_0` by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
259 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
260 |
assume ?Y_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
261 |
have "prob ?PROD \<le> prob (Y -` {b} \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
262 |
using sets_eq_Pow Pair by (auto intro!: measure_mono) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
263 |
thus ?thesis using `?Y_0` by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
264 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
265 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
266 |
qed } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
267 |
note measure_zero_joint_distribution = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
268 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
269 |
show "log b (measure_space.RN_deriv ?P (distribution (\<lambda>x. (X x, Y x))) x) * distribution (\<lambda>x. (X x, Y x)) {x} = ?log x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
270 |
apply (cases "distribution (\<lambda>x. (X x, Y x)) {x} \<noteq> 0") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
271 |
apply (subst P.RN_deriv_finite_singleton) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
272 |
proof (simp_all add: x_Pair) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
273 |
from `finite_measure_space ?P'` show "measure_space ?P'" by (simp add: finite_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
274 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
275 |
fix x assume m_0: "measure ?P {x} = 0" thus "distribution (\<lambda>x. (X x, Y x)) {x} = 0" by fact |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
276 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
277 |
show "(d,e) \<in> space ?P" unfolding prod_measure_space_def using x x_Pair by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
278 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
279 |
assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
280 |
show "measure ?P {(d,e)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
281 |
proof |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
282 |
assume "measure ?P {(d,e)} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
283 |
from measure_zero_joint_distribution[OF this] jd_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
284 |
show False by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
285 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
286 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
287 |
assume jd_0: "distribution (\<lambda>x. (X x, Y x)) {(d, e)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
288 |
with prod_measure_times[OF ms_X ms_Y, simplified, of "{d}" "{e}"] d |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
289 |
show "log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / measure ?P {(d, e)}) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
290 |
log b (distribution (\<lambda>x. (X x, Y x)) {(d, e)} / (distribution X {d} * distribution Y {e}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
291 |
by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
292 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
293 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
294 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
295 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
296 |
lemma (in finite_prob_space) distribution_log_split: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
297 |
assumes "1 < b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
298 |
shows |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
299 |
"distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} / |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
300 |
(distribution X {X x} * distribution Z {z})) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
301 |
distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(X x, z)} / |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
302 |
distribution Z {z}) - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
303 |
distribution (\<lambda>x. (X x, Z x)) {(X x, z)} * log b (distribution X {X x})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
304 |
(is "?lhs = ?rhs") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
305 |
proof (cases "distribution (\<lambda>x. (X x, Z x)) {(X x, z)} = 0") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
306 |
case True thus ?thesis by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
307 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
308 |
case False |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
309 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
310 |
let ?dZ = "distribution Z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
311 |
let ?dX = "distribution X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
312 |
let ?dXZ = "distribution (\<lambda>x. (X x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
313 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
314 |
have dist_nneg: "\<And>x X. 0 \<le> distribution X x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
315 |
unfolding distribution_def using sets_eq_Pow by (auto intro: positive) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
316 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
317 |
have "?lhs = ?dXZ {(X x, z)} * (log b (?dXZ {(X x, z)} / ?dZ {z}) - log b (?dX {X x}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
318 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
319 |
have pos_dXZ: "0 < ?dXZ {(X x, z)}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
320 |
using False dist_nneg[of "\<lambda>x. (X x, Z x)" "{(X x, z)}"] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
321 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
322 |
have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (X -` {X x}) \<inter> space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
323 |
hence "?dXZ {(X x, z)} \<le> ?dX {X x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
324 |
unfolding distribution_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
325 |
by (rule measure_mono) (simp_all add: sets_eq_Pow) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
326 |
with pos_dXZ have "0 < ?dX {X x}" by (rule less_le_trans) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
327 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
328 |
have "((\<lambda>x. (X x, Z x)) -` {(X x, z)}) \<inter> space M \<subseteq> (Z -` {z}) \<inter> space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
329 |
hence "?dXZ {(X x, z)} \<le> ?dZ {z}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
330 |
unfolding distribution_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
331 |
by (rule measure_mono) (simp_all add: sets_eq_Pow) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
332 |
with pos_dXZ have "0 < ?dZ {z}" by (rule less_le_trans) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
333 |
moreover have "0 < b" by (rule less_trans[OF _ `1 < b`]) simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
334 |
moreover have "b \<noteq> 1" by (rule ccontr) (insert `1 < b`, simp) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
335 |
ultimately show ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
336 |
using pos_dXZ |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
337 |
apply (subst (2) mult_commute) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
338 |
apply (subst divide_divide_eq_left[symmetric]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
339 |
apply (subst log_divide) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
340 |
by (auto intro: divide_pos_pos) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
341 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
342 |
also have "... = ?rhs" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
343 |
by (simp add: field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
344 |
finally show ?thesis . |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
345 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
346 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
347 |
lemma (in finite_prob_space) finite_mutual_information_reduce_prod: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
348 |
"mutual_information b |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
349 |
\<lparr> space = X ` space M, sets = Pow (X ` space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
350 |
\<lparr> space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
351 |
X (\<lambda>x. (Y x,Z x)) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
352 |
(\<Sum> (x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
353 |
distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} * |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
354 |
log b (distribution (\<lambda>x. (X x, Y x,Z x)) {(x, y, z)} / |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
355 |
(distribution X {x} * distribution (\<lambda>x. (Y x,Z x)) {(y,z)})))" (is "_ = setsum ?log ?space") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
356 |
unfolding Let_def mutual_information_def KL_divergence_def using finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
357 |
proof (subst finite_measure_space.integral_finite_singleton, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
358 |
simp_all add: prod_measure_space_def sigma_prod_sets_finite joint_distribution) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
359 |
let ?sets = "Pow (X ` space M \<times> Y ` space M \<times> Z ` space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
360 |
and ?measure = "distribution (\<lambda>x. (X x, Y x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
361 |
let ?P = "\<lparr> space = ?space, sets = ?sets, measure = ?measure\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
362 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
363 |
show "finite_measure_space ?P" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
364 |
proof (rule finite_Pow_additivity_sufficient, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
365 |
show "finite ?space" using finite_space by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
366 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
367 |
show "positive ?P ?measure" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
368 |
using sets_eq_Pow by (auto simp: positive_def distribution_def intro!: positive) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
369 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
370 |
show "additive ?P ?measure" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
371 |
proof (simp add: additive_def distribution_def, safe) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
372 |
fix x y assume "x \<subseteq> ?space" and "y \<subseteq> ?space" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
373 |
assume "x \<inter> y = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
374 |
thus "prob (((\<lambda>x. (X x, Y x, Z x)) -` x \<union> (\<lambda>x. (X x, Y x, Z x)) -` y) \<inter> space M) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
375 |
prob ((\<lambda>x. (X x, Y x, Z x)) -` x \<inter> space M) + prob ((\<lambda>x. (X x, Y x, Z x)) -` y \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
376 |
apply (subst measure_additive[unfolded sets_eq_Pow, simplified]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
377 |
by (auto simp: Un_Int_distrib Un_Int_distrib2 intro!: arg_cong[where f=prob]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
378 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
379 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
380 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
381 |
let ?X = "\<lparr>space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
382 |
and ?YZ = "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M), measure = distribution (\<lambda>x. (Y x, Z x))\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
383 |
let ?u = "prod_measure ?X ?YZ" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
384 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
385 |
from finite_measure_space[of X] finite_measure_space_image_prod[of Y Z] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
386 |
have ms_X: "measure_space ?X" and ms_YZ: "measure_space ?YZ" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
387 |
by (simp_all add: finite_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
388 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
389 |
show "(\<Sum>x \<in> ?space. log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
390 |
(distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
391 |
= setsum ?log ?space" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
392 |
proof (rule setsum_cong) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
393 |
fix x assume x: "x \<in> ?space" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
394 |
then obtain d e f where x_Pair: "x = (d, e, f)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
395 |
and d: "d \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
396 |
and e: "e \<in> Y ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
397 |
and f: "f \<in> Z ` space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
398 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
399 |
{ fix x assume m_0: "?u {x} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
400 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
401 |
let ?PROD = "(\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
402 |
obtain a b c where Pair: "x = (a, b, c)" by (cases x) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
403 |
hence "?PROD = (X -` {a} \<inter> space M) \<inter> ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
404 |
and x_prod: "{x} = {a} \<times> {(b, c)}" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
405 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
406 |
have "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
407 |
proof (cases "{a} \<subseteq> X ` space M") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
408 |
case False |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
409 |
hence "?PROD = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
410 |
unfolding Pair by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
411 |
thus ?thesis by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
412 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
413 |
have [intro]: "prob ?PROD \<le> 0 \<Longrightarrow> prob ?PROD = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
414 |
using sets_eq_Pow by (auto intro!: positive real_le_antisym[of _ 0]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
415 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
416 |
case True |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
417 |
with prod_measure_times[OF ms_X ms_YZ, simplified, of "{a}" "{(b,c)}"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
418 |
have "prob (X -` {a} \<inter> space M) = 0 \<or> prob ((\<lambda>x. (Y x, Z x)) -` {(b, c)} \<inter> space M) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
419 |
(is "prob ?X = 0 \<or> prob ?Y = 0") using m_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
420 |
by (simp add: prod_measure_space_def distribution_def Pair) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
421 |
thus ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
422 |
proof (rule disjE) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
423 |
assume "prob ?X = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
424 |
have "prob ?PROD \<le> prob ?X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
425 |
using sets_eq_Pow Pair by (auto intro!: measure_mono) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
426 |
thus ?thesis using `prob ?X = 0` by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
427 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
428 |
assume "prob ?Y = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
429 |
have "prob ?PROD \<le> prob ?Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
430 |
using sets_eq_Pow Pair by (auto intro!: measure_mono) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
431 |
thus ?thesis using `prob ?Y = 0` by (auto simp: distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
432 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
433 |
qed } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
434 |
note measure_zero_joint_distribution = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
435 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
436 |
from x_Pair d e f finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
437 |
show "log b (measure_space.RN_deriv \<lparr>space=?space, sets=?sets, measure=?u\<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
438 |
(distribution (\<lambda>x. (X x, Y x, Z x))) x) * distribution (\<lambda>x. (X x, Y x, Z x)) {x} = ?log x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
439 |
apply (cases "distribution (\<lambda>x. (X x, Y x, Z x)) {x} \<noteq> 0") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
440 |
apply (subst finite_measure_space.RN_deriv_finite_singleton) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
441 |
proof simp_all |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
442 |
show "measure_space ?P" using `finite_measure_space ?P` by (simp add: finite_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
443 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
444 |
from finite_measure_space_finite_prod_measure[OF finite_measure_space[of X] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
445 |
finite_measure_space_image_prod[of Y Z]] finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
446 |
show "finite_measure_space \<lparr>space=?space, sets=?sets, measure=?u\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
447 |
by (simp add: prod_measure_space_def sigma_prod_sets_finite) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
448 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
449 |
fix x assume "?u {x} = 0" thus "distribution (\<lambda>x. (X x, Y x, Z x)) {x} = 0" by fact |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
450 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
451 |
assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
452 |
show "?u {(d,e,f)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
453 |
proof |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
454 |
assume "?u {(d, e, f)} = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
455 |
from measure_zero_joint_distribution[OF this] jd_0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
456 |
show False by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
457 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
458 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
459 |
assume jd_0: "distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
460 |
with prod_measure_times[OF ms_X ms_YZ, simplified, of "{d}" "{(e,f)}"] d |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
461 |
show "log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / ?u {(d, e, f)}) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
462 |
log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(d, e, f)} / (distribution X {d} * distribution (\<lambda>x. (Y x, Z x)) {(e,f)}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
463 |
by (auto intro!: arg_cong[where f="log b"] simp: prod_measure_space_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
464 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
465 |
qed simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
466 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
467 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
468 |
definition (in prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
469 |
"entropy b s X = mutual_information b s s X X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
470 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
471 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
472 |
finite_entropy ("\<H>\<^bsub>_\<^esub>'(_')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
473 |
"\<H>\<^bsub>b\<^esub>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
474 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
475 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
476 |
finite_entropy_2 ("\<H>'(_')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
477 |
"\<H>(X) \<equiv> \<H>\<^bsub>2\<^esub>(X)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
478 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
479 |
lemma (in finite_prob_space) finite_entropy_reduce: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
480 |
assumes "1 < b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
481 |
shows "\<H>\<^bsub>b\<^esub>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
482 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
483 |
have fin: "finite (X ` space M)" using finite_space by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
484 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
485 |
have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
486 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
487 |
{ fix x y |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
488 |
have "(\<lambda>x. (X x, X x)) -` {(x, y)} = (if x = y then X -` {x} else {})" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
489 |
hence "distribution (\<lambda>x. (X x, X x)) {(x,y)} = (if x = y then distribution X {x} else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
490 |
unfolding distribution_def by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
491 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
492 |
have "\<And>x. 0 \<le> distribution X x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
493 |
unfolding distribution_def using finite_space sets_eq_Pow by (auto intro: positive) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
494 |
hence "\<And>x. distribution X x \<noteq> 0 \<Longrightarrow> 0 < distribution X x" by (auto simp: le_less) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
495 |
ultimately |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
496 |
show ?thesis using `1 < b` |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
497 |
by (auto intro!: setsum_cong |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
498 |
simp: log_inverse If_mult_distr setsum_cases[OF fin] inverse_eq_divide[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
499 |
entropy_def setsum_negf[symmetric] joint_distribution finite_mutual_information_reduce |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
500 |
setsum_cartesian_product[symmetric]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
501 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
502 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
503 |
lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
504 |
proof (rule inj_onI, simp) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
505 |
fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
506 |
show "x = y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
507 |
proof (cases rule: linorder_cases) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
508 |
assume "x < y" hence "log b x < log b y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
509 |
using log_less_cancel_iff[OF `1 < b`] pos by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
510 |
thus ?thesis using * by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
511 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
512 |
assume "y < x" hence "log b y < log b x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
513 |
using log_less_cancel_iff[OF `1 < b`] pos by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
514 |
thus ?thesis using * by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
515 |
qed simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
516 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
517 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
518 |
definition (in prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
519 |
"conditional_mutual_information b s1 s2 s3 X Y Z \<equiv> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
520 |
let prod_space = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
521 |
prod_measure_space \<lparr>space = space s2, sets = sets s2, measure = distribution Y\<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
522 |
\<lparr>space = space s3, sets = sets s3, measure = distribution Z\<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
523 |
in |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
524 |
mutual_information b s1 prod_space X (\<lambda>x. (Y x, Z x)) - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
525 |
mutual_information b s1 s3 X Z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
526 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
527 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
528 |
finite_conditional_mutual_information ("\<I>\<^bsub>_\<^esub>'( _ ; _ | _ ')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
529 |
"\<I>\<^bsub>b\<^esub>(X ; Y | Z) \<equiv> conditional_mutual_information b |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
530 |
\<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
531 |
\<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
532 |
\<lparr> space = Z`space M, sets = Pow (Z`space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
533 |
X Y Z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
534 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
535 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
536 |
finite_conditional_mutual_information_2 ("\<I>'( _ ; _ | _ ')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
537 |
"\<I>(X ; Y | Z) \<equiv> \<I>\<^bsub>2\<^esub>(X ; Y | Z)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
538 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
539 |
lemma image_pair_eq_Sigma: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
540 |
"(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
541 |
proof (safe intro!: imageI vimageI, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
542 |
fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
543 |
show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" unfolding eq[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
544 |
using * by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
545 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
546 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
547 |
lemma inj_on_swap: "inj_on (\<lambda>(x,y). (y,x)) A" by (auto intro!: inj_onI) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
548 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
549 |
lemma (in finite_prob_space) finite_conditional_mutual_information_reduce: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
550 |
assumes "1 < b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
551 |
shows "\<I>\<^bsub>b\<^esub>(X ; Y | Z) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
552 |
- (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M). |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
553 |
distribution (\<lambda>x. (X x, Z x)) {(x,z)} * log b (distribution (\<lambda>x. (X x, Z x)) {(x,z)} / distribution Z {z})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
554 |
+ (\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M). |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
555 |
distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} * |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
556 |
log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}/ |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
557 |
distribution (\<lambda>x. (Y x, Z x)) {(y, z)}))" (is "_ = ?rhs") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
558 |
unfolding conditional_mutual_information_def Let_def using finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
559 |
apply (simp add: prod_measure_space_def sigma_prod_sets_finite) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
560 |
apply (subst mutual_information_cong[of _ "\<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
561 |
_ "\<lparr>space = Y ` space M \<times> Z ` space M, sets = Pow (Y ` space M \<times> Z ` space M)\<rparr>"], simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
562 |
apply (subst finite_mutual_information_reduce_prod, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
563 |
apply (subst finite_mutual_information_reduce, simp_all) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
564 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
565 |
let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
566 |
let ?dXZ = "distribution (\<lambda>x. (X x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
567 |
let ?dYZ = "distribution (\<lambda>x. (Y x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
568 |
let ?dX = "distribution X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
569 |
let ?dY = "distribution Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
570 |
let ?dZ = "distribution Z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
571 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
572 |
have If_mult_distr: "\<And>A B C D. If A B C * D = If A (B * D) (C * D)" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
573 |
{ fix x y |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
574 |
have "(\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
575 |
(if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then (\<lambda>x. (X x, Y x, Z x)) -` {(X x, y)} \<inter> space M else {})" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
576 |
hence "?dXYZ {(X x, y)} = (if y \<in> (\<lambda>x. (Y x, Z x)) ` space M then ?dXYZ {(X x, y)} else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
577 |
unfolding distribution_def by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
578 |
note split_measure = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
579 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
580 |
have sets: "Y ` space M \<times> Z ` space M \<inter> (\<lambda>x. (Y x, Z x)) ` space M = (\<lambda>x. (Y x, Z x)) ` space M" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
581 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
582 |
have cong: "\<And>A B C D. \<lbrakk> A = C ; B = D \<rbrakk> \<Longrightarrow> A + B = C + D" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
583 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
584 |
{ fix A f have "setsum f A = setsum (\<lambda>(x, y). f (y, x)) ((\<lambda>(x, y). (y, x)) ` A)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
585 |
using setsum_reindex[OF inj_on_swap, of "\<lambda>(x, y). f (y, x)" A] by (simp add: split_twice) } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
586 |
note setsum_reindex_swap = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
587 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
588 |
{ fix A B f assume *: "finite A" "\<forall>x\<in>A. finite (B x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
589 |
have "(\<Sum>x\<in>Sigma A B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) (B x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
590 |
unfolding setsum_Sigma[OF *] by simp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
591 |
note setsum_Sigma = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
592 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
593 |
{ fix x |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
594 |
have "(\<Sum>z\<in>Z ` space M. ?dXZ {(X x, z)}) = (\<Sum>yz\<in>(\<lambda>x. (Y x, Z x)) ` space M. ?dXYZ {(X x, yz)})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
595 |
apply (subst setsum_reindex_swap) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
596 |
apply (simp add: image_image distribution_def) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
597 |
unfolding image_pair_eq_Sigma |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
598 |
apply (subst setsum_Sigma) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
599 |
using finite_space apply simp_all |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
600 |
apply (rule setsum_cong[OF refl]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
601 |
apply (subst measure_finitely_additive'') |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
602 |
by (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
603 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
604 |
thus "(\<Sum>(x, y, z)\<in>X ` space M \<times> Y ` space M \<times> Z ` space M. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
605 |
?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / (?dX {x} * ?dYZ {(y, z)}))) - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
606 |
(\<Sum>(x, y)\<in>X ` space M \<times> Z ` space M. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
607 |
?dXZ {(x, y)} * log b (?dXZ {(x, y)} / (?dX {x} * ?dZ {y}))) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
608 |
- (\<Sum> (x, z) \<in> (X ` space M \<times> Z ` space M). |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
609 |
?dXZ {(x,z)} * log b (?dXZ {(x,z)} / ?dZ {z})) + |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
610 |
(\<Sum> (x, y, z) \<in> (X ` space M \<times> (\<lambda>x. (Y x, Z x)) ` space M). |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
611 |
?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / ?dYZ {(y, z)}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
612 |
using finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
613 |
apply (auto simp: setsum_cartesian_product[symmetric] setsum_negf[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
614 |
setsum_addf[symmetric] diff_minus |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
615 |
intro!: setsum_cong[OF refl]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
616 |
apply (subst split_measure) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
617 |
apply (simp add: If_mult_distr setsum_cases sets distribution_log_split[OF assms, of X]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
618 |
apply (subst add_commute) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
619 |
by (simp add: setsum_subtractf setsum_negf field_simps setsum_right_distrib[symmetric] sets_eq_Pow) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
620 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
621 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
622 |
definition (in prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
623 |
"conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
624 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
625 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
626 |
finite_conditional_entropy ("\<H>\<^bsub>_\<^esub>'(_ | _')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
627 |
"\<H>\<^bsub>b\<^esub>(X | Y) \<equiv> conditional_entropy b |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
628 |
\<lparr> space = X`space M, sets = Pow (X`space M) \<rparr> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
629 |
\<lparr> space = Y`space M, sets = Pow (Y`space M) \<rparr> X Y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
630 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
631 |
abbreviation (in finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
632 |
finite_conditional_entropy_2 ("\<H>'(_ | _')") where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
633 |
"\<H>(X | Y) \<equiv> \<H>\<^bsub>2\<^esub>(X | Y)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
634 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
635 |
lemma (in finite_prob_space) finite_conditional_entropy_reduce: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
636 |
assumes "1 < b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
637 |
shows "\<H>\<^bsub>b\<^esub>(X | Z) = |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
638 |
- (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
639 |
joint_distribution X Z {(x, z)} * |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
640 |
log b (joint_distribution X Z {(x, z)} / distribution Z {z}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
641 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
642 |
have *: "\<And>x y z. (\<lambda>x. (X x, X x, Z x)) -` {(x, y, z)} = (if x = y then (\<lambda>x. (X x, Z x)) -` {(x, z)} else {})" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
643 |
show ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
644 |
unfolding finite_conditional_mutual_information_reduce[OF assms] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
645 |
conditional_entropy_def joint_distribution_def distribution_def * |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
646 |
by (auto intro!: setsum_0') |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
647 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
648 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
649 |
lemma (in finite_prob_space) finite_mutual_information_eq_entropy_conditional_entropy: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
650 |
assumes "1 < b" shows "\<I>\<^bsub>b\<^esub>(X ; Z) = \<H>\<^bsub>b\<^esub>(X) - \<H>\<^bsub>b\<^esub>(X | Z)" (is "mutual_information b ?X ?Z X Z = _") |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
651 |
unfolding finite_mutual_information_reduce |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
652 |
finite_entropy_reduce[OF assms] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
653 |
finite_conditional_entropy_reduce[OF assms] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
654 |
joint_distribution diff_minus_eq_add |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
655 |
using finite_space |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
656 |
apply (auto simp add: setsum_addf[symmetric] setsum_subtractf |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
657 |
setsum_Sigma[symmetric] distribution_log_split[OF assms] setsum_negf[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
658 |
intro!: setsum_cong[OF refl]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
659 |
apply (simp add: setsum_negf setsum_left_distrib[symmetric]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
660 |
proof (rule disjI2) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
661 |
let ?dX = "distribution X" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
662 |
and ?dXZ = "distribution (\<lambda>x. (X x, Z x))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
663 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
664 |
fix x assume "x \<in> space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
665 |
have "\<And>z. (\<lambda>x. (X x, Z x)) -` {(X x, z)} \<inter> space M = (X -` {X x} \<inter> space M) \<inter> (Z -` {z} \<inter> space M)" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
666 |
thus "(\<Sum>z\<in>Z ` space M. distribution (\<lambda>x. (X x, Z x)) {(X x, z)}) = distribution X {X x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
667 |
unfolding distribution_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
668 |
apply (subst prob_real_sum_image_fn[where e="X -` {X x} \<inter> space M" and s = "Z`space M" and f="\<lambda>z. Z -` {z} \<inter> space M"]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
669 |
using finite_space sets_eq_Pow by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
670 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
671 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
672 |
(* -------------Entropy of a RV with a certain event is zero---------------- *) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
673 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
674 |
lemma (in finite_prob_space) finite_entropy_certainty_eq_0: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
675 |
assumes "x \<in> X ` space M" and "distribution X {x} = 1" and "b > 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
676 |
shows "\<H>\<^bsub>b\<^esub>(X) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
677 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
678 |
interpret X: finite_prob_space "\<lparr> space = X ` space M, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
679 |
sets = Pow (X ` space M), |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
680 |
measure = distribution X\<rparr>" by (rule finite_prob_space) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
681 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
682 |
have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
683 |
using X.measure_compl[of "{x}"] assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
684 |
also have "\<dots> = 0" using X.prob_space assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
685 |
finally have X0: "distribution X (X ` space M - {x}) = 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
686 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
687 |
{ fix y assume asm: "y \<noteq> x" "y \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
688 |
hence "{y} \<subseteq> X ` space M - {x}" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
689 |
from X.measure_mono[OF this] X0 X.positive[of "{y}"] asm |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
690 |
have "distribution X {y} = 0" by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
691 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
692 |
hence fi: "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = (if x = y then 1 else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
693 |
using assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
694 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
695 |
have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
696 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
697 |
show ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
698 |
unfolding finite_entropy_reduce[OF `b > 1`] by (auto simp: y fi) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
699 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
700 |
(* --------------- upper bound on entropy for a rv ------------------------- *) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
701 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
702 |
definition convex_set :: "real set \<Rightarrow> bool" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
703 |
where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
704 |
"convex_set C \<equiv> (\<forall> x y \<mu>. x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> \<mu> * x + (1 - \<mu>) * y \<in> C)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
705 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
706 |
lemma pos_is_convex: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
707 |
shows "convex_set {0 <..}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
708 |
unfolding convex_set_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
709 |
proof safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
710 |
fix x y \<mu> :: real |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
711 |
assume asms: "\<mu> \<ge> 0" "\<mu> \<le> 1" "x > 0" "y > 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
712 |
{ assume "\<mu> = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
713 |
hence "\<mu> * x + (1 - \<mu>) * y = y" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
714 |
hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
715 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
716 |
{ assume "\<mu> = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
717 |
hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms by simp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
718 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
719 |
{ assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
720 |
hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
721 |
hence "\<mu> * x + (1 - \<mu>) * y > 0" using asms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
722 |
apply (subst add_nonneg_pos[of "\<mu> * x" "(1 - \<mu>) * y"]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
723 |
using real_mult_order by auto fastsimp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
724 |
ultimately show "\<mu> * x + (1 - \<mu>) * y > 0" using assms by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
725 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
726 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
727 |
definition convex_fun :: "(real \<Rightarrow> real) \<Rightarrow> real set \<Rightarrow> bool" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
728 |
where |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
729 |
"convex_fun f C \<equiv> (\<forall> x y \<mu>. convex_set C \<and> (x \<in> C \<and> y \<in> C \<and> 0 \<le> \<mu> \<and> \<mu> \<le> 1 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
730 |
\<longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
731 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
732 |
lemma pos_convex_function: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
733 |
fixes f :: "real \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
734 |
assumes "convex_set C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
735 |
assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y - x) \<le> f y - f x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
736 |
shows "convex_fun f C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
737 |
unfolding convex_fun_def |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
738 |
using assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
739 |
proof safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
740 |
fix x y \<mu> :: real |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
741 |
let ?x = "\<mu> * x + (1 - \<mu>) * y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
742 |
assume asm: "convex_set C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
743 |
hence "1 - \<mu> \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
744 |
hence xpos: "?x \<in> C" using asm unfolding convex_set_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
745 |
have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
746 |
\<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
747 |
using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
748 |
mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
749 |
hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
750 |
by (auto simp add:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
751 |
thus "\<mu> * f x + (1 - \<mu>) * f y \<ge> f ?x" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
752 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
753 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
754 |
lemma atMostAtLeast_subset_convex: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
755 |
assumes "convex_set C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
756 |
assumes "x \<in> C" "y \<in> C" "x < y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
757 |
shows "{x .. y} \<subseteq> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
758 |
proof safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
759 |
fix z assume zasm: "z \<in> {x .. y}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
760 |
{ assume asm: "x < z" "z < y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
761 |
let "?\<mu>" = "(y - z) / (y - x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
762 |
have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
763 |
hence comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
764 |
using assms[unfolded convex_set_def] by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
765 |
have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
766 |
by (auto simp add:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
767 |
also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
768 |
using assms unfolding add_divide_distrib by (auto simp:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
769 |
also have "\<dots> = z" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
770 |
using assms by (auto simp:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
771 |
finally have "z \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
772 |
using comb by auto } note less = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
773 |
show "z \<in> C" using zasm less assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
774 |
unfolding atLeastAtMost_iff le_less by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
775 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
776 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
777 |
lemma f''_imp_f': |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
778 |
fixes f :: "real \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
779 |
assumes "convex_set C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
780 |
assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
781 |
assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
782 |
assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
783 |
assumes "x \<in> C" "y \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
784 |
shows "f' x * (y - x) \<le> f y - f x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
785 |
using assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
786 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
787 |
{ fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
788 |
hence ge: "y - x > 0" "y - x \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
789 |
from asm have le: "x - y < 0" "x - y \<le> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
790 |
then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
791 |
using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `y \<in> C` `x < y`], |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
792 |
THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
793 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
794 |
hence "z1 \<in> C" using atMostAtLeast_subset_convex |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
795 |
`convex_set C` `x \<in> C` `y \<in> C` `x < y` by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
796 |
from z1 have z1': "f x - f y = (x - y) * f' z1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
797 |
by (simp add:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
798 |
obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
799 |
using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `x \<in> C` `z1 \<in> C` `x < z1`], |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
800 |
THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
801 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
802 |
obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
803 |
using subsetD[OF atMostAtLeast_subset_convex[OF `convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y`], |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
804 |
THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
805 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
806 |
have "f' y - (f x - f y) / (x - y) = f' y - f' z1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
807 |
using asm z1' by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
808 |
also have "\<dots> = (y - z1) * f'' z3" using z3 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
809 |
finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
810 |
have A': "y - z1 \<ge> 0" using z1 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
811 |
have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
812 |
`convex_set C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
813 |
hence B': "f'' z3 \<ge> 0" using assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
814 |
from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
815 |
from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
816 |
from mult_right_mono_neg[OF this le(2)] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
817 |
have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
818 |
unfolding diff_def using real_add_mult_distrib by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
819 |
hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
820 |
hence res: "f' y * (x - y) \<le> f x - f y" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
821 |
have "(f y - f x) / (y - x) - f' x = f' z1 - f' x" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
822 |
using asm z1 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
823 |
also have "\<dots> = (z1 - x) * f'' z2" using z2 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
824 |
finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
825 |
have A: "z1 - x \<ge> 0" using z1 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
826 |
have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
827 |
`convex_set C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
828 |
hence B: "f'' z2 \<ge> 0" using assms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
829 |
from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
830 |
from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
831 |
from mult_right_mono[OF this ge(2)] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
832 |
have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
833 |
unfolding diff_def using real_add_mult_distrib by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
834 |
hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
835 |
hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
836 |
using res by auto } note less_imp = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
837 |
{ fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
838 |
hence"f y - f x \<ge> f' x * (y - x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
839 |
unfolding neq_iff apply safe |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
840 |
using less_imp by auto } note neq_imp = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
841 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
842 |
{ fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
843 |
hence "f y - f x \<ge> f' x * (y - x)" by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
844 |
ultimately show ?thesis using assms by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
845 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
846 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
847 |
lemma f''_ge0_imp_convex: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
848 |
fixes f :: "real \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
849 |
assumes conv: "convex_set C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
850 |
assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
851 |
assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
852 |
assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
853 |
shows "convex_fun f C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
854 |
using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
855 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
856 |
lemma minus_log_convex: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
857 |
fixes b :: real |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
858 |
assumes "b > 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
859 |
shows "convex_fun (\<lambda> x. - log b x) {0 <..}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
860 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
861 |
have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
862 |
hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
863 |
using DERIV_minus by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
864 |
have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
865 |
using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
866 |
from this[THEN DERIV_cmult, of _ "- 1 / ln b"] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
867 |
have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
868 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
869 |
hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
870 |
unfolding inverse_eq_divide by (auto simp add:real_mult_assoc) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
871 |
have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
872 |
using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
873 |
from f''_ge0_imp_convex[OF pos_is_convex, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
874 |
unfolded greaterThan_iff, OF f' f''0 f''_ge0] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
875 |
show ?thesis by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
876 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
877 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
878 |
lemma setsum_nonneg_0: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
879 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
880 |
assumes "finite s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
881 |
assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
882 |
assumes "(\<Sum> i \<in> s. f i) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
883 |
assumes "i \<in> s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
884 |
shows "f i = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
885 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
886 |
{ assume asm: "f i > 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
887 |
from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
888 |
from setsum_nonneg[of "s - {i}" f, OF this] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
889 |
have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
890 |
hence "(\<Sum> j \<in> s - {i}. f j) + f i > 0" using asm by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
891 |
from this setsum.remove[of s i f, OF `finite s` `i \<in> s`] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
892 |
have "(\<Sum> j \<in> s. f j) > 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
893 |
hence "False" using assms by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
894 |
thus ?thesis using assms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
895 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
896 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
897 |
lemma setsum_nonneg_leq_1: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
898 |
fixes f :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
899 |
assumes "finite s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
900 |
assumes "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
901 |
assumes "(\<Sum> i \<in> s. f i) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
902 |
assumes "i \<in> s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
903 |
shows "f i \<le> 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
904 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
905 |
{ assume asm: "f i > 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
906 |
from assms have "\<forall> j \<in> s - {i}. f j \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
907 |
from setsum_nonneg[of "s - {i}" f, OF this] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
908 |
have "(\<Sum> j \<in> s - {i}. f j) \<ge> 0" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
909 |
hence "(\<Sum> j \<in> s - {i}. f j) + f i > 1" using asm by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
910 |
from this setsum.remove[of s i f, OF `finite s` `i \<in> s`] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
911 |
have "(\<Sum> j \<in> s. f j) > 1" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
912 |
hence "False" using assms by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
913 |
thus ?thesis using assms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
914 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
915 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
916 |
lemma convex_set_setsum: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
917 |
assumes "finite s" "s \<noteq> {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
918 |
assumes "convex_set C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
919 |
assumes "(\<Sum> i \<in> s. a i) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
920 |
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
921 |
assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
922 |
shows "(\<Sum> j \<in> s. a j * y j) \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
923 |
using assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
924 |
proof (induct s arbitrary:a rule:finite_ne_induct) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
925 |
case (singleton i) note asms = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
926 |
hence "a i = 1" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
927 |
thus ?case using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
928 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
929 |
case (insert i s) note asms = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
930 |
{ assume "a i = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
931 |
hence "(\<Sum> j \<in> s. a j) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
932 |
using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
933 |
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
934 |
using setsum_nonneg_0 asms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
935 |
hence ?case using asms by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
936 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
937 |
{ assume asm: "a i \<noteq> 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
938 |
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
939 |
have fis: "finite (insert i s)" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
940 |
hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
941 |
hence "a i < 1" using asm by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
942 |
hence i0: "1 - a i > 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
943 |
let "?a j" = "a j / (1 - a i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
944 |
{ fix j assume "j \<in> s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
945 |
hence "?a j \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
946 |
using i0 asms divide_nonneg_pos |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
947 |
by fastsimp } note a_nonneg = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
948 |
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
949 |
hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
950 |
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
951 |
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
952 |
from this asms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
953 |
have "(\<Sum>j\<in>s. ?a j * y j) \<in> C" using a_nonneg by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
954 |
hence "a i * y i + (1 - a i) * (\<Sum> j \<in> s. ?a j * y j) \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
955 |
using asms[unfolded convex_set_def, rule_format] yai ai1 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
956 |
hence "a i * y i + (\<Sum> j \<in> s. (1 - a i) * (?a j * y j)) \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
957 |
using mult_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j * y j" s] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
958 |
hence "a i * y i + (\<Sum> j \<in> s. a j * y j) \<in> C" using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
959 |
hence ?case using setsum.insert asms by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
960 |
ultimately show ?case by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
961 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
962 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
963 |
lemma convex_fun_setsum: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
964 |
fixes a :: "'a \<Rightarrow> real" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
965 |
assumes "finite s" "s \<noteq> {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
966 |
assumes "convex_fun f C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
967 |
assumes "(\<Sum> i \<in> s. a i) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
968 |
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
969 |
assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
970 |
shows "f (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * f (y i))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
971 |
using assms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
972 |
proof (induct s arbitrary:a rule:finite_ne_induct) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
973 |
case (singleton i) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
974 |
hence ai: "a i = 1" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
975 |
thus ?case by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
976 |
next |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
977 |
case (insert i s) note asms = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
978 |
hence "convex_fun f C" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
979 |
from this[unfolded convex_fun_def, rule_format] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
980 |
have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk> |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
981 |
\<Longrightarrow> f (\<mu> * x + (1 - \<mu>) * y) \<le> \<mu> * f x + (1 - \<mu>) * f y" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
982 |
by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
983 |
{ assume "a i = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
984 |
hence "(\<Sum> j \<in> s. a j) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
985 |
using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
986 |
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
987 |
using setsum_nonneg_0 asms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
988 |
hence ?case using asms by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
989 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
990 |
{ assume asm: "a i \<noteq> 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
991 |
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
992 |
have fis: "finite (insert i s)" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
993 |
hence ai1: "a i \<le> 1" using setsum_nonneg_leq_1[of "insert i s" a] asms by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
994 |
hence "a i < 1" using asm by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
995 |
hence i0: "1 - a i > 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
996 |
let "?a j" = "a j / (1 - a i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
997 |
{ fix j assume "j \<in> s" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
998 |
hence "?a j \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
999 |
using i0 asms divide_nonneg_pos |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1000 |
by fastsimp } note a_nonneg = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1001 |
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1002 |
hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1003 |
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1004 |
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1005 |
have "convex_set C" using asms unfolding convex_fun_def by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1006 |
hence asum: "(\<Sum> j \<in> s. ?a j * y j) \<in> C" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1007 |
using asms convex_set_setsum[OF `finite s` `s \<noteq> {}` |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1008 |
`convex_set C` a1 a_nonneg] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1009 |
have asum_le: "f (\<Sum> j \<in> s. ?a j * y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1010 |
using a_nonneg a1 asms by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1011 |
have "f (\<Sum> j \<in> insert i s. a j * y j) = f ((\<Sum> j \<in> s. a j * y j) + a i * y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1012 |
using setsum.insert[of s i "\<lambda> j. a j * y j", OF `finite s` `i \<notin> s`] asms |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1013 |
by (auto simp only:add_commute) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1014 |
also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j) / (1 - a i) + a i * y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1015 |
using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1016 |
also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. a j * y j / (1 - a i)) + a i * y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1017 |
unfolding divide.setsum[of "\<lambda> j. a j * y j" s "1 - a i", symmetric] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1018 |
also have "\<dots> = f ((1 - a i) * (\<Sum> j \<in> s. ?a j * y j) + a i * y i)" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1019 |
also have "\<dots> \<le> (1 - a i) * f ((\<Sum> j \<in> s. ?a j * y j)) + a i * f (y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1020 |
using conv[of "y i" "(\<Sum> j \<in> s. ?a j * y j)" "a i", OF yai(1) asum yai(2) ai1] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1021 |
by (auto simp only:add_commute) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1022 |
also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1023 |
using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1024 |
OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1025 |
also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1026 |
unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1027 |
also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1028 |
also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1029 |
finally have "f (\<Sum> j \<in> insert i s. a j * y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1030 |
by simp } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1031 |
ultimately show ?case by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1032 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1033 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1034 |
lemma log_setsum: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1035 |
assumes "finite s" "s \<noteq> {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1036 |
assumes "b > 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1037 |
assumes "(\<Sum> i \<in> s. a i) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1038 |
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1039 |
assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1040 |
shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1041 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1042 |
have "convex_fun (\<lambda> x. - log b x) {0 <..}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1043 |
by (rule minus_log_convex[OF `b > 1`]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1044 |
hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1045 |
using convex_fun_setsum assms by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1046 |
thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1047 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1048 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1049 |
lemma (in finite_prob_space) finite_entropy_le_card: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1050 |
assumes "1 < b" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1051 |
shows "\<H>\<^bsub>b\<^esub>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1052 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1053 |
interpret X: finite_prob_space "\<lparr>space = X ` space M, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1054 |
sets = Pow (X ` space M), |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1055 |
measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1056 |
using finite_prob_space by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1057 |
have triv: "\<And> x. (if distribution X {x} \<noteq> 0 then distribution X {x} else 0) = distribution X {x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1058 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1059 |
hence sum1: "(\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x}) = 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1060 |
using X.measure_finitely_additive''[of "X ` space M" "\<lambda> x. {x}", simplified] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1061 |
sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1062 |
unfolding disjoint_family_on_def X.prob_space[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1063 |
using finite_imageI[OF finite_space, of X] by (auto simp add:triv setsum_restrict_set) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1064 |
have pos: "\<And> x. x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0} \<Longrightarrow> inverse (distribution X {x}) > 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1065 |
using X.positive sets_eq_Pow unfolding inverse_positive_iff_positive less_le by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1066 |
{ assume asm: "X ` space M \<inter> {y. distribution X {y} \<noteq> 0} = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1067 |
{ fix x assume "x \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1068 |
hence "distribution X {x} = 0" using asm by blast } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1069 |
hence A: "(\<Sum> x \<in> X ` space M. distribution X {x}) = 0" by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1070 |
have B: "(\<Sum> x \<in> X ` space M. distribution X {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1071 |
\<ge> (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. distribution X {x})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1072 |
using finite_imageI[OF finite_space, of X] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1073 |
by (subst setsum_mono2) auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1074 |
from A B have "False" using sum1 by auto } note not_empty = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1075 |
{ fix x assume asm: "x \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1076 |
have "- distribution X {x} * log b (distribution X {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1077 |
= - (if distribution X {x} \<noteq> 0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1078 |
then distribution X {x} * log b (distribution X {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1079 |
else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1080 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1081 |
also have "\<dots> = (if distribution X {x} \<noteq> 0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1082 |
then distribution X {x} * - log b (distribution X {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1083 |
else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1084 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1085 |
also have "\<dots> = (if distribution X {x} \<noteq> 0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1086 |
then distribution X {x} * log b (inverse (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1087 |
else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1088 |
using log_inverse `1 < b` X.positive[of "{x}"] asm by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1089 |
finally have "- distribution X {x} * log b (distribution X {x}) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1090 |
= (if distribution X {x} \<noteq> 0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1091 |
then distribution X {x} * log b (inverse (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1092 |
else 0)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1093 |
by auto } note log_inv = this |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1094 |
have "- (\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1095 |
= (\<Sum> x \<in> X ` space M. (if distribution X {x} \<noteq> 0 |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1096 |
then distribution X {x} * log b (inverse (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1097 |
else 0))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1098 |
unfolding setsum_negf[symmetric] using log_inv by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1099 |
also have "\<dots> = (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1100 |
distribution X {x} * log b (inverse (distribution X {x})))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1101 |
unfolding setsum_restrict_set[OF finite_imageI[OF finite_space, of X]] by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1102 |
also have "\<dots> \<le> log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1103 |
distribution X {x} * (inverse (distribution X {x})))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1104 |
apply (subst log_setsum[OF _ _ `b > 1` sum1, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1105 |
unfolded greaterThan_iff, OF _ _ _]) using pos sets_eq_Pow |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1106 |
X.finite_space assms X.positive not_empty by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1107 |
also have "\<dots> = log b (\<Sum> x \<in> X ` space M \<inter> {y. distribution X {y} \<noteq> 0}. 1)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1108 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1109 |
also have "\<dots> \<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1110 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1111 |
finally have "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1112 |
\<le> log b (real_of_nat (card (X ` space M \<inter> {y. distribution X {y} \<noteq> 0})))" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1113 |
thus ?thesis unfolding finite_entropy_reduce[OF assms] real_eq_of_nat by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1114 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1115 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1116 |
(* --------------- entropy is maximal for a uniform rv --------------------- *) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1117 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1118 |
lemma (in finite_prob_space) uniform_prob: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1119 |
assumes "x \<in> space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1120 |
assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1121 |
shows "prob {x} = 1 / real (card (space M))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1122 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1123 |
have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1124 |
using assms(2)[OF _ `x \<in> space M`] by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1125 |
have "1 = prob (space M)" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1126 |
using prob_space by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1127 |
also have "\<dots> = (\<Sum> x \<in> space M. prob {x})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1128 |
using measure_finitely_additive''[of "space M" "\<lambda> x. {x}", simplified] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1129 |
sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1130 |
finite_space unfolding disjoint_family_on_def prob_space[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1131 |
by (auto simp add:setsum_restrict_set) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1132 |
also have "\<dots> = (\<Sum> y \<in> space M. prob {x})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1133 |
using prob_x by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1134 |
also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1135 |
finally have one: "1 = real (card (space M)) * prob {x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1136 |
using real_eq_of_nat by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1137 |
hence two: "real (card (space M)) \<noteq> 0" by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1138 |
from one have three: "prob {x} \<noteq> 0" by fastsimp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1139 |
thus ?thesis using one two three divide_cancel_right |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1140 |
by (auto simp:field_simps) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1141 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1142 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1143 |
lemma (in finite_prob_space) finite_entropy_uniform_max: |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1144 |
assumes "b > 1" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1145 |
assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1146 |
shows "\<H>\<^bsub>b\<^esub>(X) = log b (real (card (X ` space M)))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1147 |
proof - |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1148 |
interpret X: finite_prob_space "\<lparr>space = X ` space M, |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1149 |
sets = Pow (X ` space M), |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1150 |
measure = distribution X\<rparr>" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1151 |
using finite_prob_space by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1152 |
{ fix x assume xasm: "x \<in> X ` space M" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1153 |
hence card_gt0: "real (card (X ` space M)) > 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1154 |
using card_gt_0_iff X.finite_space by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1155 |
from xasm have "\<And> y. y \<in> X ` space M \<Longrightarrow> distribution X {y} = distribution X {x}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1156 |
using assms by blast |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1157 |
hence "- (\<Sum>x\<in>X ` space M. distribution X {x} * log b (distribution X {x})) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1158 |
= - (\<Sum> y \<in> X ` space M. distribution X {x} * log b (distribution X {x}))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1159 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1160 |
also have "\<dots> = - real_of_nat (card (X ` space M)) * distribution X {x} * log b (distribution X {x})" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1161 |
by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1162 |
also have "\<dots> = - real (card (X ` space M)) * (1 / real (card (X ` space M))) * log b (1 / real (card (X ` space M)))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1163 |
unfolding real_eq_of_nat[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1164 |
by (auto simp: X.uniform_prob[simplified, OF xasm assms(2)]) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1165 |
also have "\<dots> = log b (real (card (X ` space M)))" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1166 |
unfolding inverse_eq_divide[symmetric] |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1167 |
using card_gt0 log_inverse `b > 1` |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1168 |
by (auto simp add:field_simps card_gt0) |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1169 |
finally have ?thesis |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1170 |
unfolding finite_entropy_reduce[OF `b > 1`] by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1171 |
moreover |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1172 |
{ assume "X ` space M = {}" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1173 |
hence "distribution X (X ` space M) = 0" |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1174 |
using X.empty_measure by simp |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1175 |
hence "False" using X.prob_space by auto } |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1176 |
ultimately show ?thesis by auto |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1177 |
qed |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1178 |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset
|
1179 |
end |