author  hoelzl 
Tue, 22 Mar 2011 20:06:10 +0100  
changeset 42067  66c8281349ec 
parent 41981  cdf7693bbe08 
child 42148  d596e7bb251f 
permissions  rwrr 
42067  1 
(* Title: HOL/Probability/Information.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Armin Heller, TU München 

4 
*) 

5 

6 
header {*Information theory*} 

7 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

8 
theory Information 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

9 
imports 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

10 
Probability_Space 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

11 
"~~/src/HOL/Library/Convex" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

12 
begin 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

13 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

14 
lemma (in prob_space) not_zero_less_distribution[simp]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

15 
"(\<not> 0 < distribution X A) \<longleftrightarrow> distribution X A = 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

16 
using distribution_positive[of X A] by arith 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

17 

39097  18 
lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y" 
19 
by (subst log_le_cancel_iff) auto 

20 

21 
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y" 

22 
by (subst log_less_cancel_iff) auto 

23 

24 
lemma setsum_cartesian_product': 

25 
"(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)" 

26 
unfolding setsum_cartesian_product by simp 

27 

36624  28 
section "Convex theory" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

29 

36624  30 
lemma log_setsum: 
31 
assumes "finite s" "s \<noteq> {}" 

32 
assumes "b > 1" 

33 
assumes "(\<Sum> i \<in> s. a i) = 1" 

34 
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" 

35 
assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}" 

36 
shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))" 

37 
proof  

38 
have "convex_on {0 <..} (\<lambda> x.  log b x)" 

39 
by (rule minus_log_convex[OF `b > 1`]) 

40 
hence " log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i *  log b (y i))" 

41 
using convex_on_setsum[of _ _ "\<lambda> x.  log b x"] assms pos_is_convex by fastsimp 

42 
thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le) 

43 
qed 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

44 

36624  45 
lemma log_setsum': 
46 
assumes "finite s" "s \<noteq> {}" 

47 
assumes "b > 1" 

48 
assumes "(\<Sum> i \<in> s. a i) = 1" 

49 
assumes pos: "\<And> i. i \<in> s \<Longrightarrow> 0 \<le> a i" 

50 
"\<And> i. \<lbrakk> i \<in> s ; 0 < a i \<rbrakk> \<Longrightarrow> 0 < y i" 

51 
shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))" 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

52 
proof  
36624  53 
have "\<And>y. (\<Sum> i \<in> s  {i. a i = 0}. a i * y i) = (\<Sum> i \<in> s. a i * y i)" 
54 
using assms by (auto intro!: setsum_mono_zero_cong_left) 

55 
moreover have "log b (\<Sum> i \<in> s  {i. a i = 0}. a i * y i) \<ge> (\<Sum> i \<in> s  {i. a i = 0}. a i * log b (y i))" 

56 
proof (rule log_setsum) 

57 
have "setsum a (s  {i. a i = 0}) = setsum a s" 

58 
using assms(1) by (rule setsum_mono_zero_cong_left) auto 

59 
thus sum_1: "setsum a (s  {i. a i = 0}) = 1" 

60 
"finite (s  {i. a i = 0})" using assms by simp_all 

61 

62 
show "s  {i. a i = 0} \<noteq> {}" 

63 
proof 

64 
assume *: "s  {i. a i = 0} = {}" 

65 
hence "setsum a (s  {i. a i = 0}) = 0" by (simp add: * setsum_empty) 

66 
with sum_1 show False by simp 

38656  67 
qed 
36624  68 

69 
fix i assume "i \<in> s  {i. a i = 0}" 

70 
hence "i \<in> s" "a i \<noteq> 0" by simp_all 

71 
thus "0 \<le> a i" "y i \<in> {0<..}" using pos[of i] by auto 

72 
qed fact+ 

73 
ultimately show ?thesis by simp 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

74 
qed 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

75 

36624  76 
lemma log_setsum_divide: 
77 
assumes "finite S" and "S \<noteq> {}" and "1 < b" 

78 
assumes "(\<Sum>x\<in>S. g x) = 1" 

79 
assumes pos: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0" 

80 
assumes g_pos: "\<And>x. \<lbrakk> x \<in> S ; 0 < g x \<rbrakk> \<Longrightarrow> 0 < f x" 

81 
shows " (\<Sum>x\<in>S. g x * log b (g x / f x)) \<le> log b (\<Sum>x\<in>S. f x)" 

82 
proof  

83 
have log_mono: "\<And>x y. 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log b x \<le> log b y" 

84 
using `1 < b` by (subst log_le_cancel_iff) auto 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

85 

36624  86 
have " (\<Sum>x\<in>S. g x * log b (g x / f x)) = (\<Sum>x\<in>S. g x * log b (f x / g x))" 
87 
proof (unfold setsum_negf[symmetric], rule setsum_cong) 

88 
fix x assume x: "x \<in> S" 

89 
show " (g x * log b (g x / f x)) = g x * log b (f x / g x)" 

90 
proof (cases "g x = 0") 

91 
case False 

92 
with pos[OF x] g_pos[OF x] have "0 < f x" "0 < g x" by simp_all 

93 
thus ?thesis using `1 < b` by (simp add: log_divide field_simps) 

94 
qed simp 

95 
qed rule 

96 
also have "... \<le> log b (\<Sum>x\<in>S. g x * (f x / g x))" 

97 
proof (rule log_setsum') 

98 
fix x assume x: "x \<in> S" "0 < g x" 

99 
with g_pos[OF x] show "0 < f x / g x" by (safe intro!: divide_pos_pos) 

100 
qed fact+ 

101 
also have "... = log b (\<Sum>x\<in>S  {x. g x = 0}. f x)" using `finite S` 

102 
by (auto intro!: setsum_mono_zero_cong_right arg_cong[where f="log b"] 

103 
split: split_if_asm) 

104 
also have "... \<le> log b (\<Sum>x\<in>S. f x)" 

105 
proof (rule log_mono) 

106 
have "0 = (\<Sum>x\<in>S  {x. g x = 0}. 0)" by simp 

107 
also have "... < (\<Sum>x\<in>S  {x. g x = 0}. f x)" (is "_ < ?sum") 

108 
proof (rule setsum_strict_mono) 

109 
show "finite (S  {x. g x = 0})" using `finite S` by simp 

110 
show "S  {x. g x = 0} \<noteq> {}" 

111 
proof 

112 
assume "S  {x. g x = 0} = {}" 

113 
hence "(\<Sum>x\<in>S. g x) = 0" by (subst setsum_0') auto 

114 
with `(\<Sum>x\<in>S. g x) = 1` show False by simp 

115 
qed 

116 
fix x assume "x \<in> S  {x. g x = 0}" 

117 
thus "0 < f x" using g_pos[of x] pos(1)[of x] by auto 

118 
qed 

119 
finally show "0 < ?sum" . 

120 
show "(\<Sum>x\<in>S  {x. g x = 0}. f x) \<le> (\<Sum>x\<in>S. f x)" 

121 
using `finite S` pos by (auto intro!: setsum_mono2) 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

122 
qed 
36624  123 
finally show ?thesis . 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

124 
qed 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

125 

39097  126 
lemma split_pairs: 
40859  127 
"((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and 
128 
"(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto 

38656  129 

130 
section "Information theory" 

131 

40859  132 
locale information_space = prob_space + 
38656  133 
fixes b :: real assumes b_gt_1: "1 < b" 
134 

40859  135 
context information_space 
38656  136 
begin 
137 

40859  138 
text {* Introduce some simplification rules for logarithm of base @{term b}. *} 
139 

140 
lemma log_neg_const: 

141 
assumes "x \<le> 0" 

142 
shows "log b x = log b 0" 

36624  143 
proof  
40859  144 
{ fix u :: real 
145 
have "x \<le> 0" by fact 

146 
also have "0 < exp u" 

147 
using exp_gt_zero . 

148 
finally have "exp u \<noteq> x" 

149 
by auto } 

150 
then show "log b x = log b 0" 

151 
by (simp add: log_def ln_def) 

38656  152 
qed 
153 

40859  154 
lemma log_mult_eq: 
155 
"log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)" 

156 
using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"] 

157 
by (auto simp: zero_less_mult_iff mult_le_0_iff) 

38656  158 

40859  159 
lemma log_inverse_eq: 
160 
"log b (inverse B) = (if 0 < B then  log b B else log b 0)" 

161 
using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

162 

40859  163 
lemma log_divide_eq: 
164 
"log b (A / B) = (if 0 < A * B then log b \<bar>A\<bar>  log b \<bar>B\<bar> else log b 0)" 

165 
unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse 

166 
by (auto simp: zero_less_mult_iff mult_le_0_iff) 

38656  167 

40859  168 
lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq 
38656  169 

170 
end 

171 

39097  172 
subsection "Kullback$$Leibler divergence" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

173 

39097  174 
text {* The Kullback$$Leibler divergence is also known as relative entropy or 
175 
Kullback$$Leibler distance. *} 

176 

177 
definition 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

178 
"KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv M \<nu> x)) \<partial>M\<lparr>measure := \<nu>\<rparr>" 
38656  179 

41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

180 
lemma (in sigma_finite_measure) KL_divergence_vimage: 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

181 
assumes T: "T \<in> measure_preserving M M'" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

182 
and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

183 
and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

184 
and inv': "\<And>x. x \<in> space M' \<Longrightarrow> T (T' x) = x" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

185 
and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

186 
and "1 < b" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

187 
shows "KL_divergence b M' \<nu>' = KL_divergence b M \<nu>" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

188 
proof  
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

189 
interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

190 
have M: "measure_space (M\<lparr> measure := \<nu>\<rparr>)" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

191 
by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

192 
have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

193 
then have saM': "sigma_algebra M'" by simp 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

194 
then interpret M': measure_space M' by (rule measure_space_vimage) fact 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

195 
have ac: "absolutely_continuous \<nu>" unfolding absolutely_continuous_def 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

196 
proof safe 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

197 
fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

198 
then have N': "T' ` N \<inter> space M' \<in> sets M'" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

199 
using T' by (auto simp: measurable_def measure_preserving_def) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

200 
have "T ` (T' ` N \<inter> space M') \<inter> space M = N" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

201 
using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

202 
then have "measure M' (T' ` N \<inter> space M') = 0" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

203 
using measure_preservingD[OF T N'] N_0 by auto 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

204 
with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

205 
unfolding M'.absolutely_continuous_def measurable_def by auto 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

206 
qed 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

207 

563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

208 
have sa: "sigma_algebra (M\<lparr>measure := \<nu>\<rparr>)" by simp default 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

209 
have AE: "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

210 
by (rule RN_deriv_vimage[OF T T' inv \<nu>']) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

211 
show ?thesis 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

212 
unfolding KL_divergence_def 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

213 
proof (subst \<nu>'.integral_vimage[OF sa T']) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

214 
show "(\<lambda>x. log b (real (RN_deriv M \<nu> x))) \<in> borel_measurable (M\<lparr>measure := \<nu>\<rparr>)" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

215 
by (auto intro!: RN_deriv[OF M ac] borel_measurable_log[OF _ `1 < b`]) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

216 
have "(\<integral> x. log b (real (RN_deriv M' \<nu>' x)) \<partial>M'\<lparr>measure := \<nu>'\<rparr>) = 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

217 
(\<integral> x. log b (real (RN_deriv M' \<nu>' (T (T' x)))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "?l = _") 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

218 
using inv' by (auto intro!: \<nu>'.integral_cong) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

219 
also have "\<dots> = (\<integral> x. log b (real (RN_deriv M \<nu> (T' x))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "_ = ?r") 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

220 
using M ac AE 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

221 
by (intro \<nu>'.integral_cong_AE \<nu>'.almost_everywhere_vimage[OF sa T'] absolutely_continuous_AE[OF M]) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

222 
(auto elim!: AE_mp) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

223 
finally show "?l = ?r" . 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

224 
qed 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

225 
qed 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

226 

40859  227 
lemma (in sigma_finite_measure) KL_divergence_cong: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

228 
assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?\<nu>") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

229 
assumes [simp]: "sets N = sets M" "space N = space M" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

230 
"\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

231 
"\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<nu>' A" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

232 
shows "KL_divergence b M \<nu> = KL_divergence b N \<nu>'" 
40859  233 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

234 
interpret \<nu>: measure_space ?\<nu> by fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

235 
have "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv N \<nu>' x)) \<partial>?\<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

236 
by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

237 
also have "\<dots> = KL_divergence b N \<nu>'" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

238 
by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

239 
finally show ?thesis . 
40859  240 
qed 
241 

38656  242 
lemma (in finite_measure_space) KL_divergence_eq_finite: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

243 
assumes v: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)" 
40859  244 
assumes ac: "absolutely_continuous \<nu>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

245 
shows "KL_divergence b M \<nu> = (\<Sum>x\<in>space M. real (\<nu> {x}) * log b (real (\<nu> {x}) / real (\<mu> {x})))" (is "_ = ?sum") 
38656  246 
proof (simp add: KL_divergence_def finite_measure_space.integral_finite_singleton[OF v]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

247 
interpret v: finite_measure_space "M\<lparr>measure := \<nu>\<rparr>" by fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

248 
have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

249 
show "(\<Sum>x \<in> space M. log b (real (RN_deriv M \<nu> x)) * real (\<nu> {x})) = ?sum" 
38656  250 
using RN_deriv_finite_measure[OF ms ac] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

251 
by (auto intro!: setsum_cong simp: field_simps) 
38656  252 
qed 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

253 

38656  254 
lemma (in finite_prob_space) KL_divergence_positive_finite: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

255 
assumes v: "finite_prob_space (M\<lparr>measure := \<nu>\<rparr>)" 
40859  256 
assumes ac: "absolutely_continuous \<nu>" 
38656  257 
and "1 < b" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

258 
shows "0 \<le> KL_divergence b M \<nu>" 
38656  259 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

260 
interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

261 
have ms: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default 
38656  262 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

263 
have " (KL_divergence b M \<nu>) \<le> log b (\<Sum>x\<in>space M. real (\<mu> {x}))" 
40859  264 
proof (subst KL_divergence_eq_finite[OF ms ac], safe intro!: log_setsum_divide not_empty) 
265 
show "finite (space M)" using finite_space by simp 

266 
show "1 < b" by fact 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

267 
show "(\<Sum>x\<in>space M. real (\<nu> {x})) = 1" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

268 
using v.finite_sum_over_space_eq_1 by (simp add: v.\<mu>'_def) 
38656  269 

40859  270 
fix x assume "x \<in> space M" 
271 
then have x: "{x} \<in> sets M" unfolding sets_eq_Pow by auto 

272 
{ assume "0 < real (\<nu> {x})" 

273 
then have "\<nu> {x} \<noteq> 0" by auto 

274 
then have "\<mu> {x} \<noteq> 0" 

275 
using ac[unfolded absolutely_continuous_def, THEN bspec, of "{x}"] x by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

276 
thus "0 < real (\<mu> {x})" using real_measure[OF x] by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

277 
show "0 \<le> real (\<mu> {x})" "0 \<le> real (\<nu> {x})" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

278 
using real_measure[OF x] v.real_measure[of "{x}"] x by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

279 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

280 
thus "0 \<le> KL_divergence b M \<nu>" using finite_sum_over_space_eq_1 by (simp add: \<mu>'_def) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

281 
qed 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

282 

39097  283 
subsection {* Mutual Information *} 
284 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

285 
definition (in prob_space) 
38656  286 
"mutual_information b S T X Y = 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

287 
KL_divergence b (S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

288 
(extreal\<circ>joint_distribution X Y)" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

289 

40859  290 
definition (in prob_space) 
291 
"entropy b s X = mutual_information b s s X X" 

292 

293 
abbreviation (in information_space) 

294 
mutual_information_Pow ("\<I>'(_ ; _')") where 

36624  295 
"\<I>(X ; Y) \<equiv> mutual_information b 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

296 
\<lparr> space = X`space M, sets = Pow (X`space M), measure = extreal\<circ>distribution X \<rparr> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

297 
\<lparr> space = Y`space M, sets = Pow (Y`space M), measure = extreal\<circ>distribution Y \<rparr> X Y" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

298 

40859  299 
lemma (in prob_space) finite_variables_absolutely_continuous: 
300 
assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

301 
shows "measure_space.absolutely_continuous 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

302 
(S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

303 
(extreal\<circ>joint_distribution X Y)" 
40859  304 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

305 
interpret X: finite_prob_space "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

306 
using X by (rule distribution_finite_prob_space) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

307 
interpret Y: finite_prob_space "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

308 
using Y by (rule distribution_finite_prob_space) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

309 
interpret XY: pair_finite_prob_space 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

310 
"S\<lparr>measure := extreal\<circ>distribution X\<rparr>" "T\<lparr> measure := extreal\<circ>distribution Y\<rparr>" by default 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

311 
interpret P: finite_prob_space "XY.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

312 
using assms by (auto intro!: joint_distribution_finite_prob_space) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

313 
note rv = assms[THEN finite_random_variableD] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

314 
show "XY.absolutely_continuous (extreal\<circ>joint_distribution X Y)" 
40859  315 
proof (rule XY.absolutely_continuousI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

316 
show "finite_measure_space (XY.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)" by default 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

317 
fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

318 
then obtain a b where "x = (a, b)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

319 
and "distribution X {a} = 0 \<or> distribution Y {b} = 0" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

320 
by (cases x) (auto simp: space_pair_measure) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

321 
with finite_distribution_order(5,6)[OF X Y] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

322 
show "(extreal \<circ> joint_distribution X Y) {x} = 0" by auto 
40859  323 
qed 
324 
qed 

325 

326 
lemma (in information_space) 

327 
assumes MX: "finite_random_variable MX X" 

328 
assumes MY: "finite_random_variable MY Y" 

329 
shows mutual_information_generic_eq: 

36624  330 
"mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

331 
joint_distribution X Y {(x,y)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

332 
log b (joint_distribution X Y {(x,y)} / 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

333 
(distribution X {x} * distribution Y {y})))" 
40859  334 
(is ?sum) 
36624  335 
and mutual_information_positive_generic: 
40859  336 
"0 \<le> mutual_information b MX MY X Y" (is ?positive) 
36624  337 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

338 
interpret X: finite_prob_space "MX\<lparr>measure := extreal\<circ>distribution X\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

339 
using MX by (rule distribution_finite_prob_space) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

340 
interpret Y: finite_prob_space "MY\<lparr>measure := extreal\<circ>distribution Y\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

341 
using MY by (rule distribution_finite_prob_space) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

342 
interpret XY: pair_finite_prob_space "MX\<lparr>measure := extreal\<circ>distribution X\<rparr>" "MY\<lparr>measure := extreal\<circ>distribution Y\<rparr>" by default 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

343 
interpret P: finite_prob_space "XY.P\<lparr>measure := extreal\<circ>joint_distribution X Y\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

344 
using assms by (auto intro!: joint_distribution_finite_prob_space) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

345 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

346 
have P_ms: "finite_measure_space (XY.P\<lparr>measure := extreal\<circ>joint_distribution X Y\<rparr>)" by default 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

347 
have P_ps: "finite_prob_space (XY.P\<lparr>measure := extreal\<circ>joint_distribution X Y\<rparr>)" by default 
36624  348 

40859  349 
show ?sum 
38656  350 
unfolding Let_def mutual_information_def 
40859  351 
by (subst XY.KL_divergence_eq_finite[OF P_ms finite_variables_absolutely_continuous[OF MX MY]]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

352 
(auto simp add: space_pair_measure setsum_cartesian_product') 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

353 

36624  354 
show ?positive 
40859  355 
using XY.KL_divergence_positive_finite[OF P_ps finite_variables_absolutely_continuous[OF MX MY] b_gt_1] 
356 
unfolding mutual_information_def . 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

357 
qed 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

358 

41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

359 
lemma (in information_space) mutual_information_commute_generic: 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

360 
assumes X: "random_variable S X" and Y: "random_variable T Y" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

361 
assumes ac: "measure_space.absolutely_continuous 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

362 
(S\<lparr>measure := extreal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := extreal\<circ>distribution Y\<rparr>) (extreal\<circ>joint_distribution X Y)" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

363 
shows "mutual_information b S T X Y = mutual_information b T S Y X" 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

364 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

365 
let ?S = "S\<lparr>measure := extreal\<circ>distribution X\<rparr>" and ?T = "T\<lparr>measure := extreal\<circ>distribution Y\<rparr>" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

366 
interpret S: prob_space ?S using X by (rule distribution_prob_space) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

367 
interpret T: prob_space ?T using Y by (rule distribution_prob_space) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

368 
interpret P: pair_prob_space ?S ?T .. 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

369 
interpret Q: pair_prob_space ?T ?S .. 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

370 
show ?thesis 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

371 
unfolding mutual_information_def 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

372 
proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1]) 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

373 
show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

374 
(P.P \<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := extreal\<circ>joint_distribution Y X\<rparr>)" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

375 
using X Y unfolding measurable_def 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

376 
unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

377 
by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>']) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

378 
have "prob_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

379 
using X Y by (auto intro!: distribution_prob_space random_variable_pairI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

380 
then show "measure_space (P.P\<lparr> measure := extreal\<circ>joint_distribution X Y\<rparr>)" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

381 
unfolding prob_space_def by simp 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

382 
qed auto 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

383 
qed 
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

384 

41661  385 
lemma (in information_space) mutual_information_commute: 
386 
assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y" 

387 
shows "mutual_information b S T X Y = mutual_information b T S Y X" 

388 
unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X] 

389 
unfolding joint_distribution_commute_singleton[of X Y] 

390 
by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on]) 

391 

392 
lemma (in information_space) mutual_information_commute_simple: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

393 
assumes X: "simple_function M X" and Y: "simple_function M Y" 
41661  394 
shows "\<I>(X;Y) = \<I>(Y;X)" 
41833
563bea92b2c0
add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents:
41689
diff
changeset

395 
by (intro mutual_information_commute X Y simple_function_imp_finite_random_variable) 
41661  396 

40859  397 
lemma (in information_space) mutual_information_eq: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

398 
assumes "simple_function M X" "simple_function M Y" 
40859  399 
shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

400 
distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} / 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

401 
(distribution X {x} * distribution Y {y})))" 
40859  402 
using assms by (simp add: mutual_information_generic_eq) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

403 

40859  404 
lemma (in information_space) mutual_information_generic_cong: 
39097  405 
assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" 
406 
assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" 

40859  407 
shows "mutual_information b MX MY X Y = mutual_information b MX MY X' Y'" 
408 
unfolding mutual_information_def using X Y 

409 
by (simp cong: distribution_cong) 

39097  410 

40859  411 
lemma (in information_space) mutual_information_cong: 
412 
assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" 

413 
assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x" 

414 
shows "\<I>(X; Y) = \<I>(X'; Y')" 

415 
unfolding mutual_information_def using X Y 

416 
by (simp cong: distribution_cong image_cong) 

417 

418 
lemma (in information_space) mutual_information_positive: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

419 
assumes "simple_function M X" "simple_function M Y" 
40859  420 
shows "0 \<le> \<I>(X;Y)" 
421 
using assms by (simp add: mutual_information_positive_generic) 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

422 

39097  423 
subsection {* Entropy *} 
424 

40859  425 
abbreviation (in information_space) 
426 
entropy_Pow ("\<H>'(_')") where 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

427 
"\<H>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M), measure = extreal\<circ>distribution X \<rparr> X" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

428 

40859  429 
lemma (in information_space) entropy_generic_eq: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

430 
fixes X :: "'a \<Rightarrow> 'c" 
40859  431 
assumes MX: "finite_random_variable MX X" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

432 
shows "entropy b MX X = (\<Sum> x \<in> space MX. distribution X {x} * log b (distribution X {x}))" 
39097  433 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

434 
interpret MX: finite_prob_space "MX\<lparr>measure := extreal\<circ>distribution X\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

435 
using MX by (rule distribution_finite_prob_space) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

436 
let "?X x" = "distribution X {x}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

437 
let "?XX x y" = "joint_distribution X X {(x, y)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

438 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

439 
{ fix x y :: 'c 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

440 
{ assume "x \<noteq> y" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

441 
then have "(\<lambda>x. (X x, X x)) ` {(x,y)} \<inter> space M = {}" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

442 
then have "joint_distribution X X {(x, y)} = 0" by (simp add: distribution_def) } 
39097  443 
then have "?XX x y * log b (?XX x y / (?X x * ?X y)) = 
444 
(if x = y then  ?X y * log b (?X y) else 0)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

445 
by (auto simp: log_simps zero_less_mult_iff) } 
39097  446 
note remove_XX = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

447 

39097  448 
show ?thesis 
449 
unfolding entropy_def mutual_information_generic_eq[OF MX MX] 

450 
unfolding setsum_cartesian_product[symmetric] setsum_negf[symmetric] remove_XX 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

451 
using MX.finite_space by (auto simp: setsum_cases) 
39097  452 
qed 
36624  453 

40859  454 
lemma (in information_space) entropy_eq: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

455 
assumes "simple_function M X" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

456 
shows "\<H>(X) = (\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))" 
40859  457 
using assms by (simp add: entropy_generic_eq) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

458 

40859  459 
lemma (in information_space) entropy_positive: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

460 
"simple_function M X \<Longrightarrow> 0 \<le> \<H>(X)" 
40859  461 
unfolding entropy_def by (simp add: mutual_information_positive) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

462 

40859  463 
lemma (in information_space) entropy_certainty_eq_0: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

464 
assumes X: "simple_function M X" and "x \<in> X ` space M" and "distribution X {x} = 1" 
39097  465 
shows "\<H>(X) = 0" 
466 
proof  

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

467 
let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = extreal\<circ>distribution X\<rparr>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

468 
note simple_function_imp_finite_random_variable[OF `simple_function M X`] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

469 
from distribution_finite_prob_space[OF this, of "\<lparr> measure = extreal\<circ>distribution X \<rparr>"] 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

470 
interpret X: finite_prob_space ?X by simp 
39097  471 
have "distribution X (X ` space M  {x}) = distribution X (X ` space M)  distribution X {x}" 
472 
using X.measure_compl[of "{x}"] assms by auto 

473 
also have "\<dots> = 0" using X.prob_space assms by auto 

474 
finally have X0: "distribution X (X ` space M  {x}) = 0" by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

475 
{ fix y assume *: "y \<in> X ` space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

476 
{ assume asm: "y \<noteq> x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

477 
with * have "{y} \<subseteq> X ` space M  {x}" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

478 
from X.measure_mono[OF this] X0 asm * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

479 
have "distribution X {y} = 0" by (auto intro: antisym) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

480 
then have "distribution X {y} = (if x = y then 1 else 0)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

481 
using assms by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

482 
note fi = this 
39097  483 
have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

484 
show ?thesis unfolding entropy_eq[OF `simple_function M X`] by (auto simp: y fi) 
39097  485 
qed 
486 

40859  487 
lemma (in information_space) entropy_le_card_not_0: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

488 
assumes X: "simple_function M X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

489 
shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))" 
39097  490 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

491 
let "?p x" = "distribution X {x}" 
39097  492 
have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

493 
unfolding entropy_eq[OF X] setsum_negf[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

494 
by (auto intro!: setsum_cong simp: log_simps) 
39097  495 
also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. ?p x * (1 / ?p x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

496 
using not_empty b_gt_1 `simple_function M X` sum_over_space_real_distribution[OF X] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

497 
by (intro log_setsum') (auto simp: simple_function_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

498 
also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?p x \<noteq> 0 then 1 else 0)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

499 
by (intro arg_cong[where f="\<lambda>X. log b X"] setsum_cong) auto 
39097  500 
finally show ?thesis 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

501 
using `simple_function M X` by (auto simp: setsum_cases real_eq_of_nat simple_function_def) 
39097  502 
qed 
503 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

504 
lemma (in prob_space) measure'_translate: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

505 
assumes X: "random_variable S X" and A: "A \<in> sets S" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

506 
shows "finite_measure.\<mu>' (S\<lparr> measure := extreal\<circ>distribution X \<rparr>) A = distribution X A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

507 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

508 
interpret S: prob_space "S\<lparr> measure := extreal\<circ>distribution X \<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

509 
using distribution_prob_space[OF X] . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

510 
from A show "S.\<mu>' A = distribution X A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

511 
unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

512 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

513 

40859  514 
lemma (in information_space) entropy_uniform_max: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

515 
assumes X: "simple_function M X" 
39097  516 
assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}" 
517 
shows "\<H>(X) = log b (real (card (X ` space M)))" 

518 
proof  

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

519 
let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = undefined\<rparr>\<lparr> measure := extreal\<circ>distribution X\<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

520 
note frv = simple_function_imp_finite_random_variable[OF X] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

521 
from distribution_finite_prob_space[OF this, of "\<lparr> measure = extreal\<circ>distribution X \<rparr>"] 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

522 
interpret X: finite_prob_space ?X by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

523 
note rv = finite_random_variableD[OF frv] 
39097  524 
have card_gt0: "0 < card (X ` space M)" unfolding card_gt_0_iff 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

525 
using `simple_function M X` not_empty by (auto simp: simple_function_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

526 
{ fix x assume "x \<in> space ?X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

527 
moreover then have "X.\<mu>' {x} = 1 / card (space ?X)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

528 
proof (rule X.uniform_prob) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

529 
fix x y assume "x \<in> space ?X" "y \<in> space ?X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

530 
with assms(2)[of x y] show "X.\<mu>' {x} = X.\<mu>' {y}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

531 
by (subst (1 2) measure'_translate[OF rv]) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

532 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

533 
ultimately have "distribution X {x} = 1 / card (space ?X)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

534 
by (subst (asm) measure'_translate[OF rv]) auto } 
39097  535 
thus ?thesis 
40859  536 
using not_empty X.finite_space b_gt_1 card_gt0 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

537 
by (simp add: entropy_eq[OF `simple_function M X`] real_eq_of_nat[symmetric] log_simps) 
39097  538 
qed 
539 

40859  540 
lemma (in information_space) entropy_le_card: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

541 
assumes "simple_function M X" 
40859  542 
shows "\<H>(X) \<le> log b (real (card (X ` space M)))" 
39097  543 
proof cases 
544 
assume "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} = {}" 

545 
then have "\<And>x. x\<in>X`space M \<Longrightarrow> distribution X {x} = 0" by auto 

546 
moreover 

547 
have "0 < card (X`space M)" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

548 
using `simple_function M X` not_empty 
40859  549 
by (auto simp: card_gt_0_iff simple_function_def) 
39097  550 
then have "log b 1 \<le> log b (real (card (X`space M)))" 
551 
using b_gt_1 by (intro log_le) auto 

40859  552 
ultimately show ?thesis using assms by (simp add: entropy_eq) 
39097  553 
next 
554 
assume False: "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} \<noteq> {}" 

555 
have "card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}) \<le> card (X ` space M)" 

40859  556 
(is "?A \<le> ?B") using assms not_empty by (auto intro!: card_mono simp: simple_function_def) 
557 
note entropy_le_card_not_0[OF assms] 

39097  558 
also have "log b (real ?A) \<le> log b (real ?B)" 
40859  559 
using b_gt_1 False not_empty `?A \<le> ?B` assms 
560 
by (auto intro!: log_le simp: card_gt_0_iff simp: simple_function_def) 

39097  561 
finally show ?thesis . 
562 
qed 

563 

40859  564 
lemma (in information_space) entropy_commute: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

565 
assumes "simple_function M X" "simple_function M Y" 
40859  566 
shows "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))" 
39097  567 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

568 
have sf: "simple_function M (\<lambda>x. (X x, Y x))" "simple_function M (\<lambda>x. (Y x, X x))" 
40859  569 
using assms by (auto intro: simple_function_Pair) 
39097  570 
have *: "(\<lambda>x. (Y x, X x))`space M = (\<lambda>(a,b). (b,a))`(\<lambda>x. (X x, Y x))`space M" 
571 
by auto 

572 
have inj: "\<And>X. inj_on (\<lambda>(a,b). (b,a)) X" 

573 
by (auto intro!: inj_onI) 

574 
show ?thesis 

40859  575 
unfolding sf[THEN entropy_eq] unfolding * setsum_reindex[OF inj] 
39097  576 
by (simp add: joint_distribution_commute[of Y X] split_beta) 
577 
qed 

578 

40859  579 
lemma (in information_space) entropy_eq_cartesian_product: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

580 
assumes "simple_function M X" "simple_function M Y" 
40859  581 
shows "\<H>(\<lambda>x. (X x, Y x)) = (\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

582 
joint_distribution X Y {(x,y)} * log b (joint_distribution X Y {(x,y)}))" 
39097  583 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

584 
have sf: "simple_function M (\<lambda>x. (X x, Y x))" 
40859  585 
using assms by (auto intro: simple_function_Pair) 
39097  586 
{ fix x assume "x\<notin>(\<lambda>x. (X x, Y x))`space M" 
587 
then have "(\<lambda>x. (X x, Y x)) ` {x} \<inter> space M = {}" by auto 

588 
then have "joint_distribution X Y {x} = 0" 

589 
unfolding distribution_def by auto } 

40859  590 
then show ?thesis using sf assms 
591 
unfolding entropy_eq[OF sf] neg_equal_iff_equal setsum_cartesian_product 

592 
by (auto intro!: setsum_mono_zero_cong_left simp: simple_function_def) 

39097  593 
qed 
594 

595 
subsection {* Conditional Mutual Information *} 

596 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

597 
definition (in prob_space) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

598 
"conditional_mutual_information b MX MY MZ X Y Z \<equiv> 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

599 
mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x))  
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

600 
mutual_information b MX MZ X Z" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

601 

40859  602 
abbreviation (in information_space) 
603 
conditional_mutual_information_Pow ("\<I>'( _ ; _  _ ')") where 

36624  604 
"\<I>(X ; Y  Z) \<equiv> conditional_mutual_information b 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

605 
\<lparr> space = X`space M, sets = Pow (X`space M), measure = extreal\<circ>distribution X \<rparr> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

606 
\<lparr> space = Y`space M, sets = Pow (Y`space M), measure = extreal\<circ>distribution Y \<rparr> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

607 
\<lparr> space = Z`space M, sets = Pow (Z`space M), measure = extreal\<circ>distribution Z \<rparr> 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

608 
X Y Z" 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

609 

40859  610 
lemma (in information_space) conditional_mutual_information_generic_eq: 
611 
assumes MX: "finite_random_variable MX X" 

612 
and MY: "finite_random_variable MY Y" 

613 
and MZ: "finite_random_variable MZ Z" 

614 
shows "conditional_mutual_information b MX MY MZ X Y Z = (\<Sum>(x, y, z) \<in> space MX \<times> space MY \<times> space MZ. 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

615 
distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

616 
log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} / 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

617 
(joint_distribution X Z {(x, z)} * (joint_distribution Y Z {(y,z)} / distribution Z {z}))))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

618 
(is "_ = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z))))") 
40859  619 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

620 
let ?X = "\<lambda>x. distribution X {x}" 
40859  621 
note finite_var = MX MY MZ 
622 
note YZ = finite_random_variable_pairI[OF finite_var(2,3)] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

623 
note XYZ = finite_random_variable_pairI[OF MX YZ] 
40859  624 
note XZ = finite_random_variable_pairI[OF finite_var(1,3)] 
625 
note ZX = finite_random_variable_pairI[OF finite_var(3,1)] 

626 
note YZX = finite_random_variable_pairI[OF finite_var(2) ZX] 

627 
note order1 = 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

628 
finite_distribution_order(5,6)[OF finite_var(1) YZ] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

629 
finite_distribution_order(5,6)[OF finite_var(1,3)] 
40859  630 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

631 
note random_var = finite_var[THEN finite_random_variableD] 
40859  632 
note finite = finite_var(1) YZ finite_var(3) XZ YZX 
633 

634 
have order2: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk> 

635 
\<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0" 

636 
unfolding joint_distribution_commute_singleton[of X] 

637 
unfolding joint_distribution_assoc_singleton[symmetric] 

638 
using finite_distribution_order(6)[OF finite_var(2) ZX] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

639 
by auto 
36624  640 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

641 
have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z)))) = 
40859  642 
(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * (log b (?XYZ x y z / (?X x * ?YZ y z))  log b (?XZ x z / (?X x * ?Z z))))" 
643 
(is "(\<Sum>(x, y, z)\<in>?S. ?L x y z) = (\<Sum>(x, y, z)\<in>?S. ?R x y z)") 

644 
proof (safe intro!: setsum_cong) 

645 
fix x y z assume space: "x \<in> space MX" "y \<in> space MY" "z \<in> space MZ" 

646 
show "?L x y z = ?R x y z" 

647 
proof cases 

648 
assume "?XYZ x y z \<noteq> 0" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

649 
with space have "0 < ?X x" "0 < ?Z z" "0 < ?XZ x z" "0 < ?YZ y z" "0 < ?XYZ x y z" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

650 
using order1 order2 by (auto simp: less_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

651 
with b_gt_1 show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

652 
by (simp add: log_mult log_divide zero_less_mult_iff zero_less_divide_iff) 
40859  653 
qed simp 
654 
qed 

655 
also have "\<dots> = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z)))  

656 
(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z)))" 

657 
by (auto simp add: setsum_subtractf[symmetric] field_simps intro!: setsum_cong) 

658 
also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z))) = 

659 
(\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z)))" 

660 
unfolding setsum_cartesian_product[symmetric] setsum_commute[of _ _ "space MY"] 

661 
setsum_left_distrib[symmetric] 

662 
unfolding joint_distribution_commute_singleton[of X] 

663 
unfolding joint_distribution_assoc_singleton[symmetric] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

664 
using setsum_joint_distribution_singleton[OF finite_var(2) ZX] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

665 
by (intro setsum_cong refl) (simp add: space_pair_measure) 
40859  666 
also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z)))  
667 
(\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z))) = 

668 
conditional_mutual_information b MX MY MZ X Y Z" 

669 
unfolding conditional_mutual_information_def 

670 
unfolding mutual_information_generic_eq[OF finite_var(1,3)] 

671 
unfolding mutual_information_generic_eq[OF finite_var(1) YZ] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

672 
by (simp add: space_sigma space_pair_measure setsum_cartesian_product') 
40859  673 
finally show ?thesis by simp 
674 
qed 

675 

676 
lemma (in information_space) conditional_mutual_information_eq: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

677 
assumes "simple_function M X" "simple_function M Y" "simple_function M Z" 
40859  678 
shows "\<I>(X;YZ) = (\<Sum>(x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

679 
distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

680 
log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} / 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

681 
(joint_distribution X Z {(x, z)} * joint_distribution Y Z {(y,z)} / distribution Z {z})))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

682 
by (subst conditional_mutual_information_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

683 
simp 
40859  684 

685 
lemma (in information_space) conditional_mutual_information_eq_mutual_information: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

686 
assumes X: "simple_function M X" and Y: "simple_function M Y" 
40859  687 
shows "\<I>(X ; Y) = \<I>(X ; Y  (\<lambda>x. ()))" 
36624  688 
proof  
689 
have [simp]: "(\<lambda>x. ()) ` space M = {()}" using not_empty by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

690 
have C: "simple_function M (\<lambda>x. ())" by auto 
36624  691 
show ?thesis 
40859  692 
unfolding conditional_mutual_information_eq[OF X Y C] 
693 
unfolding mutual_information_eq[OF X Y] 

36624  694 
by (simp add: setsum_cartesian_product' distribution_remove_const) 
695 
qed 

696 

40859  697 
lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

698 
unfolding distribution_def using prob_space by auto 
40859  699 

700 
lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

701 
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) 
40859  702 

703 
lemma (in prob_space) setsum_distribution: 

704 
assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1" 

705 
using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

706 
using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp 
40859  707 

708 
lemma (in prob_space) setsum_real_distribution: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

709 
fixes MX :: "('c, 'd) measure_space_scheme" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

710 
assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

711 
using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV, measure = undefined \<rparr>" "\<lambda>x. ()" "{()}"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

712 
using sigma_algebra_Pow[of "UNIV::unit set" "\<lparr> measure = undefined \<rparr>"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

713 
by auto 
40859  714 

715 
lemma (in information_space) conditional_mutual_information_generic_positive: 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

716 
assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z" 
40859  717 
shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z" 
718 
proof (cases "space MX \<times> space MY \<times> space MZ = {}") 

719 
case True show ?thesis 

720 
unfolding conditional_mutual_information_generic_eq[OF assms] True 

721 
by simp 

722 
next 

723 
case False 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

724 
let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

725 
let ?dXZ = "joint_distribution X Z" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

726 
let ?dYZ = "joint_distribution Y Z" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

727 
let ?dX = "distribution X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

728 
let ?dZ = "distribution Z" 
40859  729 
let ?M = "space MX \<times> space MY \<times> space MZ" 
36624  730 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

731 
note YZ = finite_random_variable_pairI[OF Y Z] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

732 
note XZ = finite_random_variable_pairI[OF X Z] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

733 
note ZX = finite_random_variable_pairI[OF Z X] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

734 
note YZ = finite_random_variable_pairI[OF Y Z] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

735 
note XYZ = finite_random_variable_pairI[OF X YZ] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

736 
note finite = Z YZ XZ XYZ 
40859  737 
have order: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk> 
738 
\<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0" 

739 
unfolding joint_distribution_commute_singleton[of X] 

740 
unfolding joint_distribution_assoc_singleton[symmetric] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

741 
using finite_distribution_order(6)[OF Y ZX] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

742 
by auto 
40859  743 

744 
note order = order 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

745 
finite_distribution_order(5,6)[OF X YZ] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

746 
finite_distribution_order(5,6)[OF Y Z] 
40859  747 

748 
have " conditional_mutual_information b MX MY MZ X Y Z =  (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} * 

749 
log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

750 
unfolding conditional_mutual_information_generic_eq[OF assms] neg_equal_iff_equal by auto 
40859  751 
also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

752 
unfolding split_beta' 
36624  753 
proof (rule log_setsum_divide) 
40859  754 
show "?M \<noteq> {}" using False by simp 
36624  755 
show "1 < b" using b_gt_1 . 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

756 

40859  757 
show "finite ?M" using assms 
758 
unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by auto 

759 

760 
show "(\<Sum>x\<in>?M. ?dXYZ {(fst x, fst (snd x), snd (snd x))}) = 1" 

761 
unfolding setsum_cartesian_product' 

762 
unfolding setsum_commute[of _ "space MY"] 

763 
unfolding setsum_commute[of _ "space MZ"] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

764 
by (simp_all add: space_pair_measure 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

765 
setsum_joint_distribution_singleton[OF X YZ] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

766 
setsum_joint_distribution_singleton[OF Y Z] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

767 
setsum_distribution[OF Z]) 
40859  768 

36624  769 
fix x assume "x \<in> ?M" 
38656  770 
let ?x = "(fst x, fst (snd x), snd (snd x))" 
771 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

772 
show "0 \<le> ?dXYZ {?x}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

773 
"0 \<le> ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

774 
by (simp_all add: mult_nonneg_nonneg divide_nonneg_nonneg) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

775 

38656  776 
assume *: "0 < ?dXYZ {?x}" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

777 
with `x \<in> ?M` finite order show "0 < ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

778 
by (cases x) (auto simp add: zero_le_mult_iff zero_le_divide_iff less_le) 
40859  779 
qed 
780 
also have "(\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}) = (\<Sum>z\<in>space MZ. ?dZ {z})" 

36624  781 
apply (simp add: setsum_cartesian_product') 
782 
apply (subst setsum_commute) 

783 
apply (subst (2) setsum_commute) 

40859  784 
by (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

785 
setsum_joint_distribution_singleton[OF X Z] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

786 
setsum_joint_distribution_singleton[OF Y Z] 
36624  787 
intro!: setsum_cong) 
40859  788 
also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

789 
unfolding setsum_real_distribution[OF Z] by simp 
40859  790 
finally show ?thesis by simp 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

791 
qed 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

792 

40859  793 
lemma (in information_space) conditional_mutual_information_positive: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

794 
assumes "simple_function M X" and "simple_function M Y" and "simple_function M Z" 
40859  795 
shows "0 \<le> \<I>(X;YZ)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

796 
by (rule conditional_mutual_information_generic_positive[OF assms[THEN simple_function_imp_finite_random_variable]]) 
40859  797 

39097  798 
subsection {* Conditional Entropy *} 
799 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

800 
definition (in prob_space) 
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

801 
"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

802 

40859  803 
abbreviation (in information_space) 
804 
conditional_entropy_Pow ("\<H>'(_  _')") where 

36624  805 
"\<H>(X  Y) \<equiv> conditional_entropy b 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

806 
\<lparr> space = X`space M, sets = Pow (X`space M), measure = extreal\<circ>distribution X \<rparr> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

807 
\<lparr> space = Y`space M, sets = Pow (Y`space M), measure = extreal\<circ>distribution Y \<rparr> X Y" 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

808 

40859  809 
lemma (in information_space) conditional_entropy_positive: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

810 
"simple_function M X \<Longrightarrow> simple_function M Y \<Longrightarrow> 0 \<le> \<H>(X  Y)" 
40859  811 
unfolding conditional_entropy_def by (auto intro!: conditional_mutual_information_positive) 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

812 

40859  813 
lemma (in information_space) conditional_entropy_generic_eq: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

814 
fixes MX :: "('c, 'd) measure_space_scheme" and MY :: "('e, 'f) measure_space_scheme" 
40859  815 
assumes MX: "finite_random_variable MX X" 
816 
assumes MZ: "finite_random_variable MZ Z" 

39097  817 
shows "conditional_entropy b MX MZ X Z = 
818 
 (\<Sum>(x, z)\<in>space MX \<times> space MZ. 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

819 
joint_distribution X Z {(x, z)} * log b (joint_distribution X Z {(x, z)} / distribution Z {z}))" 
40859  820 
proof  
821 
interpret MX: finite_sigma_algebra MX using MX by simp 

822 
interpret MZ: finite_sigma_algebra MZ using MZ by simp 

823 
let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}" 

824 
let "?XZ x z" = "joint_distribution X Z {(x, z)}" 

825 
let "?Z z" = "distribution Z {z}" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

826 
let "?f x y z" = "log b (?XXZ x y z * ?Z z / (?XZ x z * ?XZ y z))" 
40859  827 
{ fix x z have "?XXZ x x z = ?XZ x z" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

828 
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) } 
40859  829 
note this[simp] 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

830 
{ fix x x' :: 'c and z assume "x' \<noteq> x" 
40859  831 
then have "?XXZ x x' z = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

832 
by (auto simp: distribution_def empty_measure'[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

833 
simp del: empty_measure' intro!: arg_cong[where f=\<mu>']) } 
40859  834 
note this[simp] 
835 
{ fix x x' z assume *: "x \<in> space MX" "z \<in> space MZ" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

836 
then have "(\<Sum>x'\<in>space MX. ?XXZ x x' z * ?f x x' z) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

837 
= (\<Sum>x'\<in>space MX. if x = x' then ?XZ x z * ?f x x z else 0)" 
40859  838 
by (auto intro!: setsum_cong) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

839 
also have "\<dots> = ?XZ x z * ?f x x z" 
40859  840 
using `x \<in> space MX` by (simp add: setsum_cases[OF MX.finite_space]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

841 
also have "\<dots> = ?XZ x z * log b (?Z z / ?XZ x z)" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

842 
also have "\<dots> =  ?XZ x z * log b (?XZ x z / ?Z z)" 
40859  843 
using finite_distribution_order(6)[OF MX MZ] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

844 
by (auto simp: log_simps field_simps zero_less_mult_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

845 
finally have "(\<Sum>x'\<in>space MX. ?XXZ x x' z * ?f x x' z) =  ?XZ x z * log b (?XZ x z / ?Z z)" . } 
40859  846 
note * = this 
847 
show ?thesis 

848 
unfolding conditional_entropy_def 

849 
unfolding conditional_mutual_information_generic_eq[OF MX MX MZ] 

850 
by (auto simp: setsum_cartesian_product' setsum_negf[symmetric] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

851 
setsum_commute[of _ "space MZ"] * 
40859  852 
intro!: setsum_cong) 
39097  853 
qed 
854 

40859  855 
lemma (in information_space) conditional_entropy_eq: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

856 
assumes "simple_function M X" "simple_function M Z" 
40859  857 
shows "\<H>(X  Z) = 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

858 
 (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

859 
joint_distribution X Z {(x, z)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

860 
log b (joint_distribution X Z {(x, z)} / distribution Z {z}))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

861 
by (subst conditional_entropy_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

862 
simp 
39097  863 

40859  864 
lemma (in information_space) conditional_entropy_eq_ce_with_hypothesis: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

865 
assumes X: "simple_function M X" and Y: "simple_function M Y" 
40859  866 
shows "\<H>(X  Y) = 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

867 
(\<Sum>y\<in>Y`space M. distribution Y {y} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

868 
(\<Sum>x\<in>X`space M. joint_distribution X Y {(x,y)} / distribution Y {(y)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

869 
log b (joint_distribution X Y {(x,y)} / distribution Y {(y)})))" 
40859  870 
unfolding conditional_entropy_eq[OF assms] 
871 
using finite_distribution_order(5,6)[OF assms[THEN simple_function_imp_finite_random_variable]] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

872 
by (auto simp: setsum_cartesian_product' setsum_commute[of _ "Y`space M"] setsum_right_distrib 
40859  873 
intro!: setsum_cong) 
39097  874 

40859  875 
lemma (in information_space) conditional_entropy_eq_cartesian_product: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

876 
assumes "simple_function M X" "simple_function M Y" 
40859  877 
shows "\<H>(X  Y) = (\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

878 
joint_distribution X Y {(x,y)} * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

879 
log b (joint_distribution X Y {(x,y)} / distribution Y {y}))" 
40859  880 
unfolding conditional_entropy_eq[OF assms] 
881 
by (auto intro!: setsum_cong simp: setsum_cartesian_product') 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

882 

39097  883 
subsection {* Equalities *} 
884 

40859  885 
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

886 
assumes X: "simple_function M X" and Z: "simple_function M Z" 
40859  887 
shows "\<I>(X ; Z) = \<H>(X)  \<H>(X  Z)" 
888 
proof  

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

889 
let "?XZ x z" = "joint_distribution X Z {(x, z)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

890 
let "?Z z" = "distribution Z {z}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

891 
let "?X x" = "distribution X {x}" 
40859  892 
note fX = X[THEN simple_function_imp_finite_random_variable] 
893 
note fZ = Z[THEN simple_function_imp_finite_random_variable] 

894 
note finite_distribution_order[OF fX fZ, simp] 

895 
{ fix x z assume "x \<in> X`space M" "z \<in> Z`space M" 

896 
have "?XZ x z * log b (?XZ x z / (?X x * ?Z z)) = 

897 
?XZ x z * log b (?XZ x z / ?Z z)  ?XZ x z * log b (?X x)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

898 
by (auto simp: log_simps zero_le_mult_iff field_simps less_le) } 
40859  899 
note * = this 
900 
show ?thesis 

901 
unfolding entropy_eq[OF X] conditional_entropy_eq[OF X Z] mutual_information_eq[OF X Z] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

902 
using setsum_joint_distribution_singleton[OF fZ fX, unfolded joint_distribution_commute_singleton[of Z X]] 
40859  903 
by (simp add: * setsum_cartesian_product' setsum_subtractf setsum_left_distrib[symmetric] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

904 
setsum_distribution) 
40859  905 
qed 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

906 

40859  907 
lemma (in information_space) conditional_entropy_less_eq_entropy: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

908 
assumes X: "simple_function M X" and Z: "simple_function M Z" 
40859  909 
shows "\<H>(X  Z) \<le> \<H>(X)" 
36624  910 
proof  
40859  911 
have "\<I>(X ; Z) = \<H>(X)  \<H>(X  Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] . 
912 
with mutual_information_positive[OF X Z] entropy_positive[OF X] 

36624  913 
show ?thesis by auto 
36080
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 

40859  916 
lemma (in information_space) entropy_chain_rule: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

917 
assumes X: "simple_function M X" and Y: "simple_function M Y" 
40859  918 
shows "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(YX)" 
919 
proof  

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

920 
let "?XY x y" = "joint_distribution X Y {(x, y)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

921 
let "?Y y" = "distribution Y {y}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

922 
let "?X x" = "distribution X {x}" 
40859  923 
note fX = X[THEN simple_function_imp_finite_random_variable] 
924 
note fY = Y[THEN simple_function_imp_finite_random_variable] 

925 
note finite_distribution_order[OF fX fY, simp] 

926 
{ fix x y assume "x \<in> X`space M" "y \<in> Y`space M" 

927 
have "?XY x y * log b (?XY x y / ?X x) = 

928 
?XY x y * log b (?XY x y)  ?XY x y * log b (?X x)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

929 
by (auto simp: log_simps zero_le_mult_iff field_simps less_le) } 
40859  930 
note * = this 
931 
show ?thesis 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

932 
using setsum_joint_distribution_singleton[OF fY fX] 
40859  933 
unfolding entropy_eq[OF X] conditional_entropy_eq_cartesian_product[OF Y X] entropy_eq_cartesian_product[OF X Y] 
934 
unfolding joint_distribution_commute_singleton[of Y X] setsum_commute[of _ "X`space M"] 

935 
by (simp add: * setsum_subtractf setsum_left_distrib[symmetric]) 

936 
qed 

38656  937 

39097  938 
section {* Partitioning *} 
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

939 

36624  940 
definition "subvimage A f g \<longleftrightarrow> (\<forall>x \<in> A. f ` {f x} \<inter> A \<subseteq> g ` {g x} \<inter> A)" 
941 

942 
lemma subvimageI: 

943 
assumes "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y" 

944 
shows "subvimage A f g" 

945 
using assms unfolding subvimage_def by blast 

946 

947 
lemma subvimageE[consumes 1]: 

948 
assumes "subvimage A f g" 

949 
obtains "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y" 

950 
using assms unfolding subvimage_def by blast 

951 

952 
lemma subvimageD: 

953 
"\<lbrakk> subvimage A f g ; x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y" 

954 
using assms unfolding subvimage_def by blast 

955 

956 
lemma subvimage_subset: 

957 
"\<lbrakk> subvimage B f g ; A \<subseteq> B \<rbrakk> \<Longrightarrow> subvimage A f g" 

958 
unfolding subvimage_def by auto 

959 

960 
lemma subvimage_idem[intro]: "subvimage A g g" 

961 
by (safe intro!: subvimageI) 

962 

963 
lemma subvimage_comp_finer[intro]: 

964 
assumes svi: "subvimage A g h" 

965 
shows "subvimage A g (f \<circ> h)" 

966 
proof (rule subvimageI, simp) 

967 
fix x y assume "x \<in> A" "y \<in> A" "g x = g y" 

968 
from svi[THEN subvimageD, OF this] 

969 
show "f (h x) = f (h y)" by simp 

970 
qed 

971 

972 
lemma subvimage_comp_gran: 

973 
assumes svi: "subvimage A g h" 

974 
assumes inj: "inj_on f (g ` A)" 

975 
shows "subvimage A (f \<circ> g) h" 

976 
by (rule subvimageI) (auto intro!: subvimageD[OF svi] simp: inj_on_iff[OF inj]) 

977 

978 
lemma subvimage_comp: 

979 
assumes svi: "subvimage (f ` A) g h" 

980 
shows "subvimage A (g \<circ> f) (h \<circ> f)" 

981 
by (rule subvimageI) (auto intro!: svi[THEN subvimageD]) 

982 

983 
lemma subvimage_trans: 

984 
assumes fg: "subvimage A f g" 

985 
assumes gh: "subvimage A g h" 

986 
shows "subvimage A f h" 

987 
by (rule subvimageI) (auto intro!: fg[THEN subvimageD] gh[THEN subvimageD]) 

988 

989 
lemma subvimage_translator: 

990 
assumes svi: "subvimage A f g" 

991 
shows "\<exists>h. \<forall>x \<in> A. h (f x) = g x" 

992 
proof (safe intro!: exI[of _ "\<lambda>x. (THE z. z \<in> (g ` (f ` {x} \<inter> A)))"]) 

993 
fix x assume "x \<in> A" 

994 
show "(THE x'. x' \<in> (g ` (f ` {f x} \<inter> A))) = g x" 

995 
by (rule theI2[of _ "g x"]) 

996 
(insert `x \<in> A`, auto intro!: svi[THEN subvimageD]) 

997 
qed 

998 

999 
lemma subvimage_translator_image: 

1000 
assumes svi: "subvimage A f g" 

1001 
shows "\<exists>h. h ` f ` A = g ` A" 

1002 
proof  

1003 
from subvimage_translator[OF svi] 

1004 
obtain h where "\<And>x. x \<in> A \<Longrightarrow> h (f x) = g x" by auto 

1005 
thus ?thesis 

1006 
by (auto intro!: exI[of _ h] 

1007 
simp: image_compose[symmetric] comp_def cong: image_cong) 

1008 
qed 

1009 

1010 
lemma subvimage_finite: 

1011 
assumes svi: "subvimage A f g" and fin: "finite (f`A)" 

1012 
shows "finite (g`A)" 

1013 
proof  

1014 
from subvimage_translator_image[OF svi] 

1015 
obtain h where "g`A = h`f`A" by fastsimp 

1016 
with fin show "finite (g`A)" by simp 

1017 
qed 

1018 

1019 
lemma subvimage_disj: 

1020 
assumes svi: "subvimage A f g" 

1021 
shows "f ` {x} \<inter> A \<subseteq> g ` {y} \<inter> A \<or> 

1022 
f ` {x} \<inter> g ` {y} \<inter> A = {}" (is "?sub \<or> ?dist") 

1023 
proof (rule disjCI) 

1024 
assume "\<not> ?dist" 

1025 
then obtain z where "z \<in> A" and "x = f z" and "y = g z" by auto 

1026 
thus "?sub" using svi unfolding subvimage_def by auto 

1027 
qed 

1028 

1029 
lemma setsum_image_split: 

1030 
assumes svi: "subvimage A f g" and fin: "finite (f ` A)" 

1031 
shows "(\<Sum>x\<in>f`A. h x) = (\<Sum>y\<in>g`A. \<Sum>x\<in>f`(g ` {y} \<inter> A). h x)" 

1032 
(is "?lhs = ?rhs") 

1033 
proof  

1034 
have "f ` A = 

1035 
snd ` (SIGMA x : g ` A. f ` (g ` {x} \<inter> A))" 

1036 
(is "_ = snd ` ?SIGMA") 

1037 
unfolding image_split_eq_Sigma[symmetric] 

1038 
by (simp add: image_compose[symmetric] comp_def) 

1039 
moreover 

1040 
have snd_inj: "inj_on snd ?SIGMA" 

1041 
unfolding image_split_eq_Sigma[symmetric] 

1042 
by (auto intro!: inj_onI subvimageD[OF svi]) 

1043 
ultimately 

1044 
have "(\<Sum>x\<in>f`A. h x) = (\<Sum>(x,y)\<in>?SIGMA. h y)" 

1045 
by (auto simp: setsum_reindex intro: setsum_cong) 

1046 
also have "... = ?rhs" 

1047 
using subvimage_finite[OF svi fin] fin 

1048 
apply (subst setsum_Sigma[symmetric]) 

1049 
by (auto intro!: finite_subset[of _ "f`A"]) 

1050 
finally show ?thesis . 

1051 
qed 

1052 

40859  1053 
lemma (in information_space) entropy_partition: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1054 
assumes sf: "simple_function M X" "simple_function M P" 
36624  1055 
assumes svi: "subvimage (space M) X P" 
1056 
shows "\<H>(X) = \<H>(P) + \<H>(XP)" 

1057 
proof  

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1058 
let "?XP x p" = "joint_distribution X P {(x, p)}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1059 
let "?X x" = "distribution X {x}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1060 
let "?P p" = "distribution P {p}" 
40859  1061 
note fX = sf(1)[THEN simple_function_imp_finite_random_variable] 
1062 
note fP = sf(2)[THEN simple_function_imp_finite_random_variable] 

1063 
note finite_distribution_order[OF fX fP, simp] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1064 
have "(\<Sum>x\<in>X ` space M. ?X x * log b (?X x)) = 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1065 
(\<Sum>y\<in>P `space M. \<Sum>x\<in>X ` space M. ?XP x y * log b (?XP x y))" 
36624  1066 
proof (subst setsum_image_split[OF svi], 
40859  1067 
safe intro!: setsum_mono_zero_cong_left imageI) 
1068 
show "finite (X ` space M)" "finite (X ` space M)" "finite (P ` space M)" 

1069 
using sf unfolding simple_function_def by auto 

1070 
next 

36624  1071 
fix p x assume in_space: "p \<in> space M" "x \<in> space M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1072 
assume "?XP (X x) (P p) * log b (?XP (X x) (P p)) \<noteq> 0" 
36624  1073 
hence "(\<lambda>x. (X x, P x)) ` {(X x, P p)} \<inter> space M \<noteq> {}" by (auto simp: distribution_def) 
1074 
with svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`] 

1075 
show "x \<in> P ` {P p}" by auto 

1076 
next 

1077 
fix p x assume in_space: "p \<in> space M" "x \<in> space M" 

1078 
assume "P x = P p" 

1079 
from this[symmetric] svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`] 

1080 
have "X ` {X x} \<inter> space M \<subseteq> P ` {P p} \<inter> space M" 

1081 
by auto 

1082 
hence "(\<lambda>x. (X x, P x)) ` {(X x, P p)} \<inter> space M = X ` {X x} \<inter> space M" 

1083 
by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1084 
thus "?X (X x) * log b (?X (X x)) = ?XP (X x) (P p) * log b (?XP (X x) (P p))" 
36624  1085 
by (auto simp: distribution_def) 
1086 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1087 
moreover have "\<And>x y. ?XP x y * log b (?XP x y / ?P y) = 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1088 
?XP x y * log b (?XP x y)  ?XP x y * log b (?P y)" 
40859  1089 
by (auto simp add: log_simps zero_less_mult_iff field_simps) 
1090 
ultimately show ?thesis 

1091 
unfolding sf[THEN entropy_eq] conditional_entropy_eq[OF sf] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1092 
using setsum_joint_distribution_singleton[OF fX fP] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41833
diff
changeset

1093 
by (simp add: setsum_cartesian_product' setsum_subtractf setsum_distribution 
36624  1094 
setsum_left_distrib[symmetric] setsum_commute[where B="P`space M"]) 
1095 
qed 

1096 

40859  1097 
corollary (in information_space) entropy_data_processing: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1098 
assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)" 
40859  1099 
proof  
1100 
note X 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1101 
moreover have fX: "simple_function M (f \<circ> X)" using X by auto 
40859  1102 
moreover have "subvimage (space M) X (f \<circ> X)" by auto 
1103 
ultimately have "\<H>(X) = \<H>(f\<circ>X) + \<H>(Xf\<circ>X)" by (rule entropy_partition) 

1104 
then show "\<H>(f \<circ> X) \<le> \<H>(X)" 

1105 
by (auto intro: conditional_entropy_positive[OF X fX]) 

1106 
qed 

36624  1107 

40859  1108 
corollary (in information_space) entropy_of_inj: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1109 
assumes X: "simple_function M X" and inj: "inj_on f (X`space M)" 
36624  1110 
shows "\<H>(f \<circ> X) = \<H>(X)" 
1111 
proof (rule antisym) 

40859  1112 
show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] . 
36624  1113 
next 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1114 
have sf: "simple_function M (f \<circ> X)" 
40859  1115 
using X by auto 
36624  1116 
have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))" 
40859  1117 
by (auto intro!: mutual_information_cong simp: entropy_def the_inv_into_f_f[OF inj]) 
36624  1118 
also have "... \<le> \<H>(f \<circ> X)" 
40859  1119 
using entropy_data_processing[OF sf] . 
36624  1120 
finally show "\<H>(X) \<le> \<H>(f \<circ> X)" . 
1121 
qed 

1122 

36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff
changeset

1123 
end 