author  hoelzl 
Mon, 23 Apr 2012 12:14:35 +0200  
changeset 47694  05663f75964c 
parent 46905  6b1c0a80a57a 
child 49776  199d1d5bb17e 
permissions  rwrr 
42148  1 
(* Title: HOL/Probability/Probability_Measure.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
Author: Armin Heller, TU München 

4 
*) 

5 

42148  6 
header {*Probability measure*} 
42067  7 

42148  8 
theory Probability_Measure 
47694  9 
imports Lebesgue_Measure Radon_Nikodym 
35582  10 
begin 
11 

47694  12 
lemma funset_eq_UN_fun_upd_I: 
13 
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A" 

14 
and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))" 

15 
and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)" 

16 
shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))" 

17 
proof safe 

18 
fix f assume f: "f \<in> F (insert a A)" 

19 
show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)" 

20 
proof (rule UN_I[of "f(a := d)"]) 

21 
show "f(a := d) \<in> F A" using *[OF f] . 

22 
show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))" 

23 
proof (rule image_eqI[of _ _ "f a"]) 

24 
show "f a \<in> G (f(a := d))" using **[OF f] . 

25 
qed simp 

26 
qed 

27 
next 

28 
fix f x assume "f \<in> F A" "x \<in> G f" 

29 
from ***[OF this] show "f(a := x) \<in> F (insert a A)" . 

30 
qed 

31 

32 
lemma extensional_funcset_insert_eq[simp]: 

33 
assumes "a \<notin> A" 

34 
shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)" 

35 
apply (rule funset_eq_UN_fun_upd_I) 

36 
using assms 

37 
by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def) 

38 

39 
lemma finite_extensional_funcset[simp, intro]: 

40 
assumes "finite A" "finite B" 

41 
shows "finite (extensional A \<inter> (A \<rightarrow> B))" 

42 
using assms by induct auto 

43 

44 
lemma finite_PiE[simp, intro]: 

45 
assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)" 

46 
shows "finite (Pi\<^isub>E A B)" 

47 
proof  

48 
have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto 

49 
show ?thesis 

50 
using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto 

51 
qed 

52 

53 

54 
lemma countably_additiveI[case_names countably]: 

55 
assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" 

56 
shows "countably_additive M \<mu>" 

57 
using assms unfolding countably_additive_def by auto 

58 

59 
lemma convex_le_Inf_differential: 

60 
fixes f :: "real \<Rightarrow> real" 

61 
assumes "convex_on I f" 

62 
assumes "x \<in> interior I" "y \<in> I" 

63 
shows "f y \<ge> f x + Inf ((\<lambda>t. (f x  f t) / (x  t)) ` ({x<..} \<inter> I)) * (y  x)" 

64 
(is "_ \<ge> _ + Inf (?F x) * (y  x)") 

65 
proof  

66 
show ?thesis 

67 
proof (cases rule: linorder_cases) 

68 
assume "x < y" 

69 
moreover 

70 
have "open (interior I)" by auto 

71 
from openE[OF this `x \<in> interior I`] guess e . note e = this 

72 
moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)" 

73 
ultimately have "x < t" "t < y" "t \<in> ball x e" 

74 
by (auto simp: dist_real_def field_simps split: split_min) 

75 
with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto 

76 

77 
have "open (interior I)" by auto 

78 
from openE[OF this `x \<in> interior I`] guess e . 

79 
moreover def K \<equiv> "x  e / 2" 

80 
with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def) 

81 
ultimately have "K \<in> I" "K < x" "x \<in> I" 

82 
using interior_subset[of I] `x \<in> interior I` by auto 

83 

84 
have "Inf (?F x) \<le> (f x  f y) / (x  y)" 

85 
proof (rule Inf_lower2) 

86 
show "(f x  f t) / (x  t) \<in> ?F x" 

87 
using `t \<in> I` `x < t` by auto 

88 
show "(f x  f t) / (x  t) \<le> (f x  f y) / (x  y)" 

89 
using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff) 

90 
next 

91 
fix y assume "y \<in> ?F x" 

92 
with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]] 

93 
show "(f K  f x) / (K  x) \<le> y" by auto 

94 
qed 

95 
then show ?thesis 

96 
using `x < y` by (simp add: field_simps) 

97 
next 

98 
assume "y < x" 

99 
moreover 

100 
have "open (interior I)" by auto 

101 
from openE[OF this `x \<in> interior I`] guess e . note e = this 

102 
moreover def t \<equiv> "x + e / 2" 

103 
ultimately have "x < t" "t \<in> ball x e" 

104 
by (auto simp: dist_real_def field_simps) 

105 
with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto 

106 

107 
have "(f x  f y) / (x  y) \<le> Inf (?F x)" 

108 
proof (rule Inf_greatest) 

109 
have "(f x  f y) / (x  y) = (f y  f x) / (y  x)" 

110 
using `y < x` by (auto simp: field_simps) 

111 
also 

112 
fix z assume "z \<in> ?F x" 

113 
with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]] 

114 
have "(f y  f x) / (y  x) \<le> z" by auto 

115 
finally show "(f x  f y) / (x  y) \<le> z" . 

116 
next 

117 
have "open (interior I)" by auto 

118 
from openE[OF this `x \<in> interior I`] guess e . note e = this 

119 
then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def) 

120 
with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto 

121 
then show "?F x \<noteq> {}" by blast 

122 
qed 

123 
then show ?thesis 

124 
using `y < x` by (simp add: field_simps) 

125 
qed simp 

126 
qed 

127 

128 
lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N" 

129 
by (rule measure_eqI) (auto simp: emeasure_distr) 

130 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

131 
locale prob_space = finite_measure + 
47694  132 
assumes emeasure_space_1: "emeasure M (space M) = 1" 
38656  133 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

134 
lemma prob_spaceI[Pure.intro!]: 
47694  135 
assumes *: "emeasure M (space M) = 1" 
45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

136 
shows "prob_space M" 
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

137 
proof  
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

138 
interpret finite_measure M 
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

139 
proof 
47694  140 
show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 
45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

141 
qed 
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

142 
show "prob_space M" by default fact 
38656  143 
qed 
144 

40859  145 
abbreviation (in prob_space) "events \<equiv> sets M" 
47694  146 
abbreviation (in prob_space) "prob \<equiv> measure M" 
147 
abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M 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

148 
abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M" 
35582  149 

47694  150 
lemma (in prob_space) prob_space_distr: 
151 
assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)" 

152 
proof (rule prob_spaceI) 

153 
have "f ` space M' \<inter> space M = space M" using f by (auto dest: measurable_space) 

154 
with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1" 

155 
by (auto simp: emeasure_distr emeasure_space_1) 

43339  156 
qed 
157 

40859  158 
lemma (in prob_space) prob_space: "prob (space M) = 1" 
47694  159 
using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

160 

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

161 
lemma (in prob_space) prob_le_1[simp, intro]: "prob A \<le> 1" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

162 
using bounded_measure[of A] by (simp add: prob_space) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

163 

47694  164 
lemma (in prob_space) not_empty: "space M \<noteq> {}" 
165 
using prob_space by auto 

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

166 

47694  167 
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1" 
168 
using emeasure_space[of M X] by (simp add: emeasure_space_1) 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42902
diff
changeset

169 

43339  170 
lemma (in prob_space) AE_I_eq_1: 
47694  171 
assumes "emeasure M {x\<in>space M. P x} = 1" "{x\<in>space M. P x} \<in> sets M" 
172 
shows "AE x in M. P x" 

43339  173 
proof (rule AE_I) 
47694  174 
show "emeasure M (space M  {x \<in> space M. P x}) = 0" 
175 
using assms emeasure_space_1 by (simp add: emeasure_compl) 

43339  176 
qed (insert assms, auto) 
177 

40859  178 
lemma (in prob_space) prob_compl: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

179 
assumes A: "A \<in> events" 
38656  180 
shows "prob (space M  A) = 1  prob A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

181 
using finite_measure_compl[OF A] by (simp add: prob_space) 
35582  182 

47694  183 
lemma (in prob_space) AE_in_set_eq_1: 
184 
assumes "A \<in> events" shows "(AE x in M. x \<in> A) \<longleftrightarrow> prob A = 1" 

185 
proof 

186 
assume ae: "AE x in M. x \<in> A" 

187 
have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M  A" 

188 
using `A \<in> events`[THEN sets_into_space] by auto 

189 
with AE_E2[OF ae] `A \<in> events` have "1  emeasure M A = 0" 

190 
by (simp add: emeasure_compl emeasure_space_1) 

191 
then show "prob A = 1" 

192 
using `A \<in> events` by (simp add: emeasure_eq_measure one_ereal_def) 

193 
next 

194 
assume prob: "prob A = 1" 

195 
show "AE x in M. x \<in> A" 

196 
proof (rule AE_I) 

197 
show "{x \<in> space M. x \<notin> A} \<subseteq> space M  A" by auto 

198 
show "emeasure M (space M  A) = 0" 

199 
using `A \<in> events` prob 

200 
by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def) 

201 
show "space M  A \<in> events" 

202 
using `A \<in> events` by auto 

203 
qed 

204 
qed 

205 

206 
lemma (in prob_space) AE_False: "(AE x in M. False) \<longleftrightarrow> False" 

207 
proof 

208 
assume "AE x in M. False" 

209 
then have "AE x in M. x \<in> {}" by simp 

210 
then show False 

211 
by (subst (asm) AE_in_set_eq_1) auto 

212 
qed simp 

213 

214 
lemma (in prob_space) AE_prob_1: 

215 
assumes "prob A = 1" shows "AE x in M. x \<in> A" 

216 
proof  

217 
from `prob A = 1` have "A \<in> events" 

218 
by (metis measure_notin_sets zero_neq_one) 

219 
with AE_in_set_eq_1 assms show ?thesis by simp 

220 
qed 

221 

40859  222 
lemma (in prob_space) prob_space_increasing: "increasing M prob" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

223 
by (auto intro!: finite_measure_mono simp: increasing_def) 
35582  224 

40859  225 
lemma (in prob_space) prob_zero_union: 
35582  226 
assumes "s \<in> events" "t \<in> events" "prob t = 0" 
227 
shows "prob (s \<union> t) = prob s" 

38656  228 
using assms 
35582  229 
proof  
230 
have "prob (s \<union> t) \<le> prob s" 

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

231 
using finite_measure_subadditive[of s t] assms by auto 
35582  232 
moreover have "prob (s \<union> t) \<ge> prob s" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

233 
using assms by (blast intro: finite_measure_mono) 
35582  234 
ultimately show ?thesis by simp 
235 
qed 

236 

40859  237 
lemma (in prob_space) prob_eq_compl: 
35582  238 
assumes "s \<in> events" "t \<in> events" 
239 
assumes "prob (space M  s) = prob (space M  t)" 

240 
shows "prob s = prob t" 

38656  241 
using assms prob_compl by auto 
35582  242 

40859  243 
lemma (in prob_space) prob_one_inter: 
35582  244 
assumes events:"s \<in> events" "t \<in> events" 
245 
assumes "prob t = 1" 

246 
shows "prob (s \<inter> t) = prob s" 

247 
proof  

38656  248 
have "prob ((space M  s) \<union> (space M  t)) = prob (space M  s)" 
249 
using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union) 

250 
also have "(space M  s) \<union> (space M  t) = space M  (s \<inter> t)" 

251 
by blast 

252 
finally show "prob (s \<inter> t) = prob s" 

253 
using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s]) 

35582  254 
qed 
255 

40859  256 
lemma (in prob_space) prob_eq_bigunion_image: 
35582  257 
assumes "range f \<subseteq> events" "range g \<subseteq> events" 
258 
assumes "disjoint_family f" "disjoint_family g" 

259 
assumes "\<And> n :: nat. prob (f n) = prob (g n)" 

260 
shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))" 

261 
using assms 

262 
proof  

38656  263 
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

264 
by (rule finite_measure_UNION[OF assms(1,3)]) 
38656  265 
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

266 
by (rule finite_measure_UNION[OF assms(2,4)]) 
38656  267 
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp 
35582  268 
qed 
269 

40859  270 
lemma (in prob_space) prob_countably_zero: 
35582  271 
assumes "range c \<subseteq> events" 
272 
assumes "\<And> i. prob (c i) = 0" 

38656  273 
shows "prob (\<Union> i :: nat. c i) = 0" 
274 
proof (rule antisym) 

275 
show "prob (\<Union> i :: nat. c i) \<le> 0" 

47694  276 
using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2)) 
277 
qed (simp add: measure_nonneg) 

35582  278 

40859  279 
lemma (in prob_space) prob_equiprobable_finite_unions: 
38656  280 
assumes "s \<in> events" 
281 
assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" 

35582  282 
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" 
38656  283 
shows "prob s = real (card s) * prob {SOME x. x \<in> s}" 
35582  284 
proof (cases "s = {}") 
38656  285 
case False hence "\<exists> x. x \<in> s" by blast 
35582  286 
from someI_ex[OF this] assms 
287 
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast 

288 
have "prob s = (\<Sum> x \<in> s. prob {x})" 

47694  289 
using finite_measure_eq_setsum_singleton[OF s_finite] by simp 
35582  290 
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto 
38656  291 
also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}" 
292 
using setsum_constant assms by (simp add: real_eq_of_nat) 

35582  293 
finally show ?thesis by simp 
38656  294 
qed simp 
35582  295 

40859  296 
lemma (in prob_space) prob_real_sum_image_fn: 
35582  297 
assumes "e \<in> events" 
298 
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" 

299 
assumes "finite s" 

38656  300 
assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" 
301 
assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)" 

35582  302 
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" 
303 
proof  

38656  304 
have e: "e = (\<Union> i \<in> s. e \<inter> f i)" 
305 
using `e \<in> events` sets_into_space upper by blast 

306 
hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp 

307 
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" 

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

308 
proof (rule finite_measure_finite_Union) 
38656  309 
show "finite s" by fact 
47694  310 
show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto 
38656  311 
show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" 
312 
using disjoint by (auto simp: disjoint_family_on_def) 

313 
qed 

314 
finally show ?thesis . 

35582  315 
qed 
316 

43339  317 
lemma (in prob_space) expectation_less: 
318 
assumes [simp]: "integrable M X" 

319 
assumes gt: "\<forall>x\<in>space M. X x < b" 

320 
shows "expectation X < b" 

321 
proof  

322 
have "expectation X < expectation (\<lambda>x. b)" 

47694  323 
using gt emeasure_space_1 
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset

324 
by (intro integral_less_AE_space) auto 
43339  325 
then show ?thesis using prob_space by simp 
326 
qed 

327 

328 
lemma (in prob_space) expectation_greater: 

329 
assumes [simp]: "integrable M X" 

330 
assumes gt: "\<forall>x\<in>space M. a < X x" 

331 
shows "a < expectation X" 

332 
proof  

333 
have "expectation (\<lambda>x. a) < expectation X" 

47694  334 
using gt emeasure_space_1 
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
43339
diff
changeset

335 
by (intro integral_less_AE_space) auto 
43339  336 
then show ?thesis using prob_space by simp 
337 
qed 

338 

339 
lemma (in prob_space) jensens_inequality: 

340 
fixes a b :: real 

341 
assumes X: "integrable M X" "X ` space M \<subseteq> I" 

342 
assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" 

343 
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" 

344 
shows "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" 

345 
proof  

46731  346 
let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x  q t) / (x  t)) ` ({x<..} \<inter> I))" 
43339  347 
from not_empty X(2) have "I \<noteq> {}" by auto 
348 

349 
from I have "open I" by auto 

350 

351 
note I 

352 
moreover 

353 
{ assume "I \<subseteq> {a <..}" 

354 
with X have "a < expectation X" 

355 
by (intro expectation_greater) auto } 

356 
moreover 

357 
{ assume "I \<subseteq> {..< b}" 

358 
with X have "expectation X < b" 

359 
by (intro expectation_less) auto } 

360 
ultimately have "expectation X \<in> I" 

361 
by (elim disjE) (auto simp: subset_eq) 

362 
moreover 

363 
{ fix y assume y: "y \<in> I" 

364 
with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y  x)) ` I) = q y" 

365 
by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } 

366 
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X  x)) ` I)" 

367 
by simp 

368 
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" 

369 
proof (rule Sup_least) 

370 
show "(\<lambda>x. q x + ?F x * (expectation X  x)) ` I \<noteq> {}" 

371 
using `I \<noteq> {}` by auto 

372 
next 

373 
fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X  x)) ` I" 

374 
then guess x .. note x = this 

375 
have "q x + ?F x * (expectation X  x) = expectation (\<lambda>w. q x + ?F x * (X w  x))" 

47694  376 
using prob_space by (simp add: X) 
43339  377 
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))" 
378 
using `x \<in> I` `open I` X(2) 

379 
by (intro integral_mono integral_add integral_cmult integral_diff 

380 
lebesgue_integral_const X q convex_le_Inf_differential) 

381 
(auto simp: interior_open) 

382 
finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto 

383 
qed 

384 
finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" . 

385 
qed 

386 

40859  387 
lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0: 
35582  388 
assumes "{x} \<in> events" 
38656  389 
assumes "prob {x} = 1" 
35582  390 
assumes "{y} \<in> events" 
391 
assumes "y \<noteq> x" 

392 
shows "prob {y} = 0" 

393 
using prob_one_inter[of "{y}" "{x}"] assms by auto 

394 

40859  395 
lemma (in prob_space) joint_distribution_Times_le_fst: 
47694  396 
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 
397 
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MX X) A" 

398 
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) 

40859  399 

400 
lemma (in prob_space) joint_distribution_Times_le_snd: 

47694  401 
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 
402 
\<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^isub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B" 

403 
by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets) 

40859  404 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

405 
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 
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

406 

47694  407 
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^isub>M M2" 
45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

408 
proof 
47694  409 
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1" 
410 
by (simp add: emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure) 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

411 
qed 
40859  412 

47694  413 
locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" + 
45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

414 
fixes I :: "'i set" 
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

415 
assumes prob_space: "\<And>i. prob_space (M i)" 
42988  416 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

417 
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i 
42988  418 
by (rule prob_space) 
419 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

420 
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I 
42988  421 

422 
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i" 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

423 
proof 
47694  424 
show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1" 
425 
by (simp add: measure_times M.emeasure_space_1 setprod_1 space_PiM) 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

426 
qed 
42988  427 

428 
lemma (in finite_product_prob_space) prob_times: 

429 
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)" 

430 
shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" 

431 
proof  

47694  432 
have "ereal (measure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)) = emeasure (\<Pi>\<^isub>M i\<in>I. M i) (\<Pi>\<^isub>E i\<in>I. X i)" 
433 
using X by (simp add: emeasure_eq_measure) 

434 
also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))" 

42988  435 
using measure_times X by simp 
47694  436 
also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))" 
437 
using X by (simp add: M.emeasure_eq_measure setprod_ereal) 

42859
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset

438 
finally show ?thesis by simp 
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset

439 
qed 
d9dfc733f25c
add product of probability spaces with finite cardinality
hoelzl
parents:
42858
diff
changeset

440 

47694  441 
section {* Distributions *} 
42892  442 

47694  443 
definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
444 
f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N" 

36624  445 

47694  446 
lemma 
447 
shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f" 

448 
and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N" 

449 
and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N" 

450 
and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)" 

451 
by (simp_all add: distributed_def) 

39097  452 

47694  453 
lemma 
454 
shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N" 

455 
and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)" 

456 
by (simp_all add: distributed_def borel_measurable_ereal_iff) 

35977  457 

47694  458 
lemma distributed_count_space: 
459 
assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A" 

460 
shows "P a = emeasure M (X ` {a} \<inter> space M)" 

39097  461 
proof  
47694  462 
have "emeasure M (X ` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}" 
463 
using X a A by (simp add: distributed_measurable emeasure_distr) 

464 
also have "\<dots> = emeasure (density (count_space A) P) {a}" 

465 
using X by (simp add: distributed_distr_eq_density) 

466 
also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)" 

467 
using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong) 

468 
also have "\<dots> = P a" 

469 
using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space) 

470 
finally show ?thesis .. 

39092  471 
qed 
35977  472 

47694  473 
lemma distributed_cong_density: 
474 
"(AE x in N. f x = g x) \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable N \<Longrightarrow> 

475 
distributed M N X f \<longleftrightarrow> distributed M N X g" 

476 
by (auto simp: distributed_def intro!: density_cong) 

477 

478 
lemma subdensity: 

479 
assumes T: "T \<in> measurable P Q" 

480 
assumes f: "distributed M P X f" 

481 
assumes g: "distributed M Q Y g" 

482 
assumes Y: "Y = T \<circ> X" 

483 
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" 

484 
proof  

485 
have "{x\<in>space Q. g x = 0} \<in> null_sets (distr M Q (T \<circ> X))" 

486 
using g Y by (auto simp: null_sets_density_iff distributed_def) 

487 
also have "distr M Q (T \<circ> X) = distr (distr M P X) Q T" 

488 
using T f[THEN distributed_measurable] by (rule distr_distr[symmetric]) 

489 
finally have "T ` {x\<in>space Q. g x = 0} \<inter> space P \<in> null_sets (distr M P X)" 

490 
using T by (subst (asm) null_sets_distr_iff) auto 

491 
also have "T ` {x\<in>space Q. g x = 0} \<inter> space P = {x\<in>space P. g (T x) = 0}" 

492 
using T by (auto dest: measurable_space) 

493 
finally show ?thesis 

494 
using f g by (auto simp add: null_sets_density_iff distributed_def) 

35977  495 
qed 
496 

47694  497 
lemma subdensity_real: 
498 
fixes g :: "'a \<Rightarrow> real" and f :: "'b \<Rightarrow> real" 

499 
assumes T: "T \<in> measurable P Q" 

500 
assumes f: "distributed M P X f" 

501 
assumes g: "distributed M Q Y g" 

502 
assumes Y: "Y = T \<circ> X" 

503 
shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0" 

504 
using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto 

505 

506 
lemma distributed_integral: 

507 
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)" 

508 
by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable 

509 
distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr) 

510 

511 
lemma distributed_transform_integral: 

512 
assumes Px: "distributed M N X Px" 

513 
assumes "distributed M P Y Py" 

514 
assumes Y: "Y = T \<circ> X" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P" 

515 
shows "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. Px x * f (T x) \<partial>N)" 

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

516 
proof  
47694  517 
have "(\<integral>x. Py x * f x \<partial>P) = (\<integral>x. f (Y x) \<partial>M)" 
518 
by (rule distributed_integral) fact+ 

519 
also have "\<dots> = (\<integral>x. f (T (X x)) \<partial>M)" 

520 
using Y by simp 

521 
also have "\<dots> = (\<integral>x. Px x * f (T x) \<partial>N)" 

522 
using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def) 

45777
c36637603821
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
hoelzl
parents:
45712
diff
changeset

523 
finally show ?thesis . 
39092  524 
qed 
36624  525 

47694  526 
lemma distributed_marginal_eq_joint: 
527 
assumes T: "sigma_finite_measure T" 

528 
assumes S: "sigma_finite_measure S" 

529 
assumes Px: "distributed M S X Px" 

530 
assumes Py: "distributed M T Y Py" 

531 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 

532 
shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)" 

533 
proof (rule sigma_finite_measure.density_unique[OF T]) 

534 
interpret ST: pair_sigma_finite S T using S T unfolding pair_sigma_finite_def by simp 

535 
show "Py \<in> borel_measurable T" "AE y in T. 0 \<le> Py y" 

536 
"(\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S) \<in> borel_measurable T" "AE y in T. 0 \<le> \<integral>\<^isup>+ x. Pxy (x, y) \<partial>S" 

537 
using Pxy[THEN distributed_borel_measurable] 

538 
by (auto intro!: Py[THEN distributed_borel_measurable] Py[THEN distributed_AE] 

539 
ST.positive_integral_snd_measurable' positive_integral_positive) 

540 

541 
show "density T Py = density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)" 

542 
proof (rule measure_eqI) 

543 
fix A assume A: "A \<in> sets (density T Py)" 

544 
have *: "\<And>x y. x \<in> space S \<Longrightarrow> indicator (space S \<times> A) (x, y) = indicator A y" 

545 
by (auto simp: indicator_def) 

546 
have "emeasure (density T Py) A = emeasure (distr M T Y) A" 

547 
unfolding Py[THEN distributed_distr_eq_density] .. 

548 
also have "\<dots> = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (space S \<times> A)" 

549 
using A Px Py Pxy 

550 
by (subst (1 2) emeasure_distr) 

551 
(auto dest: measurable_space distributed_measurable intro!: arg_cong[where f="emeasure M"]) 

552 
also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (space S \<times> A)" 

553 
unfolding Pxy[THEN distributed_distr_eq_density] .. 

554 
also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator (space S \<times> A) x \<partial>(S \<Otimes>\<^isub>M T))" 

555 
using A Pxy by (simp add: emeasure_density distributed_borel_measurable) 

556 
also have "\<dots> = (\<integral>\<^isup>+y. \<integral>\<^isup>+x. Pxy (x, y) * indicator (space S \<times> A) (x, y) \<partial>S \<partial>T)" 

557 
using A Pxy 

558 
by (subst ST.positive_integral_snd_measurable) (simp_all add: emeasure_density distributed_borel_measurable) 

559 
also have "\<dots> = (\<integral>\<^isup>+y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S) * indicator A y \<partial>T)" 

560 
using measurable_comp[OF measurable_Pair1[OF measurable_identity] distributed_borel_measurable[OF Pxy]] 

561 
using distributed_borel_measurable[OF Pxy] distributed_AE[OF Pxy, THEN ST.AE_pair] 

562 
by (subst (asm) ST.AE_commute) (auto intro!: positive_integral_cong_AE positive_integral_multc cong: positive_integral_cong simp: * comp_def) 

563 
also have "\<dots> = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" 

564 
using A by (intro emeasure_density[symmetric]) (auto intro!: ST.positive_integral_snd_measurable' Pxy[THEN distributed_borel_measurable]) 

565 
finally show "emeasure (density T Py) A = emeasure (density T (\<lambda>x. \<integral>\<^isup>+ xa. Pxy (xa, x) \<partial>S)) A" . 

566 
qed simp 

36624  567 
qed 
568 

47694  569 
lemma (in prob_space) distr_marginal1: 
570 
fixes Pxy :: "('b \<times> 'c) \<Rightarrow> real" 

571 
assumes "sigma_finite_measure S" "sigma_finite_measure T" 

572 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 

573 
defines "Px \<equiv> \<lambda>x. real (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)" 

574 
shows "distributed M S X Px" 

575 
unfolding distributed_def 

576 
proof safe 

577 
interpret S: sigma_finite_measure S by fact 

578 
interpret T: sigma_finite_measure T by fact 

579 
interpret ST: pair_sigma_finite S T by default 

580 

581 
have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" 

582 
using Pxy by (rule distributed_measurable) 

583 
then show X: "X \<in> measurable M S" 

584 
unfolding measurable_pair_iff by (simp add: comp_def) 

585 
from XY have Y: "Y \<in> measurable M T" 

586 
unfolding measurable_pair_iff by (simp add: comp_def) 

587 

588 
from Pxy show borel: "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" 

589 
by (auto intro!: ST.positive_integral_fst_measurable borel_measurable_real_of_ereal dest!: distributed_real_measurable simp: Px_def) 

39097  590 

47694  591 
interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 
592 
using XY by (rule prob_space_distr) 

593 
have "(\<integral>\<^isup>+ x. max 0 (ereal ( Pxy x)) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))" 

594 
using Pxy 

595 
by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_real_measurable distributed_real_AE) 

596 
then have Pxy_integrable: "integrable (S \<Otimes>\<^isub>M T) Pxy" 

597 
using Pxy Pxy.emeasure_space_1 

598 
by (simp add: integrable_def emeasure_density positive_integral_max_0 distributed_def borel_measurable_ereal_iff cong: positive_integral_cong) 

599 

600 
show "distr M S X = density S Px" 

601 
proof (rule measure_eqI) 

602 
fix A assume A: "A \<in> sets (distr M S X)" 

603 
with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)" 

604 
by (auto simp add: emeasure_distr 

605 
intro!: arg_cong[where f="emeasure M"] dest: measurable_space) 

606 
also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)" 

607 
using Pxy by (simp add: distributed_def) 

608 
also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" 

609 
using A borel Pxy 

610 
by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def) 

611 
also have "\<dots> = \<integral>\<^isup>+ x. ereal (Px x) * indicator A x \<partial>S" 

612 
apply (rule positive_integral_cong_AE) 

613 
using Pxy[THEN distributed_real_AE, THEN ST.AE_pair] ST.integrable_fst_measurable(1)[OF Pxy_integrable] AE_space 

614 
proof eventually_elim 

615 
fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" and i: "integrable T (\<lambda>y. Pxy (x, y))" 

616 
moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x" 

617 
by (auto simp: indicator_def) 

618 
ultimately have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = 

619 
(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) * indicator A x" 

620 
using Pxy[THEN distributed_real_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong) 

621 
also have "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) \<partial>T) = Px x" 

622 
using i by (simp add: Px_def ereal_real integrable_def positive_integral_positive) 

623 
finally show "(\<integral>\<^isup>+ y. ereal (Pxy (x, y)) * indicator (A \<times> space T) (x, y) \<partial>T) = ereal (Px x) * indicator A x" . 

624 
qed 

625 
finally show "emeasure (distr M S X) A = emeasure (density S Px) A" 

626 
using A borel Pxy by (simp add: emeasure_density) 

627 
qed simp 

628 

629 
show "AE x in S. 0 \<le> ereal (Px x)" 

630 
by (simp add: Px_def positive_integral_positive real_of_ereal_pos) 

40859  631 
qed 
632 

47694  633 
definition 
634 
"simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and> 

635 
finite (X`space M)" 

42902  636 

47694  637 
lemma simple_distributed: 
638 
"simple_distributed M X Px \<Longrightarrow> distributed M (count_space (X`space M)) X Px" 

639 
unfolding simple_distributed_def by auto 

42902  640 

47694  641 
lemma simple_distributed_finite[dest]: "simple_distributed M X P \<Longrightarrow> finite (X`space M)" 
642 
by (simp add: simple_distributed_def) 

42902  643 

47694  644 
lemma (in prob_space) distributed_simple_function_superset: 
645 
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X ` {x} \<inter> space M)" 

646 
assumes A: "X`space M \<subseteq> A" "finite A" 

647 
defines "S \<equiv> count_space A" and "P' \<equiv> (\<lambda>x. if x \<in> X`space M then P x else 0)" 

648 
shows "distributed M S X P'" 

649 
unfolding distributed_def 

650 
proof safe 

651 
show "(\<lambda>x. ereal (P' x)) \<in> borel_measurable S" unfolding S_def by simp 

652 
show "AE x in S. 0 \<le> ereal (P' x)" 

653 
using X by (auto simp: S_def P'_def simple_distributed_def intro!: measure_nonneg) 

654 
show "distr M S X = density S P'" 

655 
proof (rule measure_eqI_finite) 

656 
show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A" 

657 
using A unfolding S_def by auto 

658 
show "finite A" by fact 

659 
fix a assume a: "a \<in> A" 

660 
then have "a \<notin> X`space M \<Longrightarrow> X ` {a} \<inter> space M = {}" by auto 

661 
with A a X have "emeasure (distr M S X) {a} = P' a" 

662 
by (subst emeasure_distr) 

663 
(auto simp add: S_def P'_def simple_functionD emeasure_eq_measure 

664 
intro!: arg_cong[where f=prob]) 

665 
also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)" 

666 
using A X a 

667 
by (subst positive_integral_cmult_indicator) 

668 
(auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg) 

669 
also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' x) * indicator {a} x \<partial>S)" 

670 
by (auto simp: indicator_def intro!: positive_integral_cong) 

671 
also have "\<dots> = emeasure (density S P') {a}" 

672 
using a A by (intro emeasure_density[symmetric]) (auto simp: S_def) 

673 
finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" . 

674 
qed 

675 
show "random_variable S X" 

676 
using X(1) A by (auto simp: measurable_def simple_functionD S_def) 

677 
qed 

42902  678 

47694  679 
lemma (in prob_space) simple_distributedI: 
680 
assumes X: "simple_function M X" "\<And>x. x \<in> X ` space M \<Longrightarrow> P x = measure M (X ` {x} \<inter> space M)" 

681 
shows "simple_distributed M X P" 

682 
unfolding simple_distributed_def 

683 
proof 

684 
have "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then P x else 0))" 

685 
(is "?A") 

686 
using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X]) auto 

687 
also have "?A \<longleftrightarrow> distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (P x))" 

688 
by (rule distributed_cong_density) auto 

689 
finally show "\<dots>" . 

690 
qed (rule simple_functionD[OF X(1)]) 

691 

692 
lemma simple_distributed_joint_finite: 

693 
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" 

694 
shows "finite (X ` space M)" "finite (Y ` space M)" 

42902  695 
proof  
47694  696 
have "finite ((\<lambda>x. (X x, Y x)) ` space M)" 
697 
using X by (auto simp: simple_distributed_def simple_functionD) 

698 
then have "finite (fst ` (\<lambda>x. (X x, Y x)) ` space M)" "finite (snd ` (\<lambda>x. (X x, Y x)) ` space M)" 

699 
by auto 

700 
then show fin: "finite (X ` space M)" "finite (Y ` space M)" 

701 
by (auto simp: image_image) 

702 
qed 

703 

704 
lemma simple_distributed_joint2_finite: 

705 
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" 

706 
shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" 

707 
proof  

708 
have "finite ((\<lambda>x. (X x, Y x, Z x)) ` space M)" 

709 
using X by (auto simp: simple_distributed_def simple_functionD) 

710 
then have "finite (fst ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 

711 
"finite ((fst \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 

712 
"finite ((snd \<circ> snd) ` (\<lambda>x. (X x, Y x, Z x)) ` space M)" 

713 
by auto 

714 
then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)" 

715 
by (auto simp: image_image) 

42902  716 
qed 
717 

47694  718 
lemma simple_distributed_simple_function: 
719 
"simple_distributed M X Px \<Longrightarrow> simple_function M X" 

720 
unfolding simple_distributed_def distributed_def 

721 
by (auto simp: simple_function_def) 

722 

723 
lemma simple_distributed_measure: 

724 
"simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X ` {a} \<inter> space M)" 

725 
using distributed_count_space[of M "X`space M" X P a, symmetric] 

726 
by (auto simp: simple_distributed_def measure_def) 

727 

728 
lemma simple_distributed_nonneg: "simple_distributed M X f \<Longrightarrow> x \<in> space M \<Longrightarrow> 0 \<le> f (X x)" 

729 
by (auto simp: simple_distributed_measure measure_nonneg) 

42860  730 

47694  731 
lemma (in prob_space) simple_distributed_joint: 
732 
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px" 

733 
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)" 

734 
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)" 

735 
shows "distributed M S (\<lambda>x. (X x, Y x)) P" 

736 
proof  

737 
from simple_distributed_joint_finite[OF X, simp] 

738 
have S_eq: "S = count_space (X`space M \<times> Y`space M)" 

739 
by (simp add: S_def pair_measure_count_space) 

740 
show ?thesis 

741 
unfolding S_eq P_def 

742 
proof (rule distributed_simple_function_superset) 

743 
show "simple_function M (\<lambda>x. (X x, Y x))" 

744 
using X by (rule simple_distributed_simple_function) 

745 
fix x assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M" 

746 
from simple_distributed_measure[OF X this] 

747 
show "Px x = prob ((\<lambda>x. (X x, Y x)) ` {x} \<inter> space M)" . 

748 
qed auto 

749 
qed 

42860  750 

47694  751 
lemma (in prob_space) simple_distributed_joint2: 
752 
assumes X: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Px" 

753 
defines "S \<equiv> count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M) \<Otimes>\<^isub>M count_space (Z`space M)" 

754 
defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then Px x else 0)" 

755 
shows "distributed M S (\<lambda>x. (X x, Y x, Z x)) P" 

756 
proof  

757 
from simple_distributed_joint2_finite[OF X, simp] 

758 
have S_eq: "S = count_space (X`space M \<times> Y`space M \<times> Z`space M)" 

759 
by (simp add: S_def pair_measure_count_space) 

760 
show ?thesis 

761 
unfolding S_eq P_def 

762 
proof (rule distributed_simple_function_superset) 

763 
show "simple_function M (\<lambda>x. (X x, Y x, Z x))" 

764 
using X by (rule simple_distributed_simple_function) 

765 
fix x assume "x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M" 

766 
from simple_distributed_measure[OF X this] 

767 
show "Px x = prob ((\<lambda>x. (X x, Y x, Z x)) ` {x} \<inter> space M)" . 

768 
qed auto 

769 
qed 

770 

771 
lemma (in prob_space) simple_distributed_setsum_space: 

772 
assumes X: "simple_distributed M X f" 

773 
shows "setsum f (X`space M) = 1" 

774 
proof  

775 
from X have "setsum f (X`space M) = prob (\<Union>i\<in>X`space M. X ` {i} \<inter> space M)" 

776 
by (subst finite_measure_finite_Union) 

777 
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD 

778 
intro!: setsum_cong arg_cong[where f="prob"]) 

779 
also have "\<dots> = prob (space M)" 

780 
by (auto intro!: arg_cong[where f=prob]) 

781 
finally show ?thesis 

782 
using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def) 

783 
qed 

42860  784 

47694  785 
lemma (in prob_space) distributed_marginal_eq_joint_simple: 
786 
assumes Px: "simple_function M X" 

787 
assumes Py: "simple_distributed M Y Py" 

788 
assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy" 

789 
assumes y: "y \<in> Y`space M" 

790 
shows "Py y = (\<Sum>x\<in>X`space M. if (x, y) \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy (x, y) else 0)" 

791 
proof  

792 
note Px = simple_distributedI[OF Px refl] 

793 
have *: "\<And>f A. setsum (\<lambda>x. max 0 (ereal (f x))) A = ereal (setsum (\<lambda>x. max 0 (f x)) A)" 

794 
by (simp add: setsum_ereal[symmetric] zero_ereal_def) 

795 
from distributed_marginal_eq_joint[OF sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite 

796 
simple_distributed[OF Px] simple_distributed[OF Py] simple_distributed_joint[OF Pxy], 

797 
OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]] 

798 
y Px[THEN simple_distributed_finite] Py[THEN simple_distributed_finite] 

799 
Pxy[THEN simple_distributed, THEN distributed_real_AE] 

800 
show ?thesis 

801 
unfolding AE_count_space 

802 
apply (elim ballE[where x=y]) 

803 
apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max) 

804 
done 

805 
qed 

42860  806 

47694  807 

808 
lemma prob_space_uniform_measure: 

809 
assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" 

810 
shows "prob_space (uniform_measure M A)" 

811 
proof 

812 
show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1" 

813 
using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"] 

814 
using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A 

815 
by (simp add: Int_absorb2 emeasure_nonneg) 

816 
qed 

817 

818 
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)" 

819 
by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def) 

42860  820 

35582  821 
end 