author  nipkow 
Mon, 13 Sep 2010 11:13:15 +0200  
changeset 39302  d7728f65b353 
parent 39198  f967a16dfcdd 
child 40859  de0b30e6c2d2 
permissions  rwrr 
35582  1 
theory Probability_Space 
39083  2 
imports Lebesgue_Integration Radon_Nikodym 
35582  3 
begin 
4 

5 
locale prob_space = measure_space + 

38656  6 
assumes measure_space_1: "\<mu> (space M) = 1" 
7 

8 
sublocale prob_space < finite_measure 

9 
proof 

10 
from measure_space_1 show "\<mu> (space M) \<noteq> \<omega>" by simp 

11 
qed 

12 

13 
context prob_space 

35582  14 
begin 
15 

16 
abbreviation "events \<equiv> sets M" 

38656  17 
abbreviation "prob \<equiv> \<lambda>A. real (\<mu> A)" 
35582  18 
abbreviation "prob_preserving \<equiv> measure_preserving" 
19 
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s" 

20 
abbreviation "expectation \<equiv> integral" 

21 

22 
definition 

23 
"indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" 

24 

25 
definition 

26 
"indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" 

27 

28 
definition 

38656  29 
"distribution X = (\<lambda>s. \<mu> ((X ` s) \<inter> (space M)))" 
35582  30 

36624  31 
abbreviation 
32 
"joint_distribution X Y \<equiv> distribution (\<lambda>x. (X x, Y x))" 

35582  33 

39097  34 
lemma (in prob_space) distribution_cong: 
35 
assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x" 

36 
shows "distribution X = distribution Y" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

37 
unfolding distribution_def fun_eq_iff 
39097  38 
using assms by (auto intro!: arg_cong[where f="\<mu>"]) 
39 

40 
lemma (in prob_space) joint_distribution_cong: 

41 
assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x" 

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

43 
shows "joint_distribution X Y = joint_distribution X' Y'" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

44 
unfolding distribution_def fun_eq_iff 
39097  45 
using assms by (auto intro!: arg_cong[where f="\<mu>"]) 
46 

38656  47 
lemma prob_space: "prob (space M) = 1" 
48 
unfolding measure_space_1 by simp 

35582  49 

38656  50 
lemma measure_le_1[simp, intro]: 
51 
assumes "A \<in> events" shows "\<mu> A \<le> 1" 

52 
proof  

53 
have "\<mu> A \<le> \<mu> (space M)" 

54 
using assms sets_into_space by(auto intro!: measure_mono) 

55 
also note measure_space_1 

56 
finally show ?thesis . 

57 
qed 

35582  58 

59 
lemma prob_compl: 

38656  60 
assumes "A \<in> events" 
61 
shows "prob (space M  A) = 1  prob A" 

62 
using `A \<in> events`[THEN sets_into_space] `A \<in> events` measure_space_1 

63 
by (subst real_finite_measure_Diff) auto 

35582  64 

65 
lemma indep_space: 

66 
assumes "s \<in> events" 

67 
shows "indep (space M) s" 

38656  68 
using assms prob_space by (simp add: indep_def) 
35582  69 

38656  70 
lemma prob_space_increasing: "increasing M prob" 
71 
by (auto intro!: real_measure_mono simp: increasing_def) 

35582  72 

73 
lemma prob_zero_union: 

74 
assumes "s \<in> events" "t \<in> events" "prob t = 0" 

75 
shows "prob (s \<union> t) = prob s" 

38656  76 
using assms 
35582  77 
proof  
78 
have "prob (s \<union> t) \<le> prob s" 

38656  79 
using real_finite_measure_subadditive[of s t] assms by auto 
35582  80 
moreover have "prob (s \<union> t) \<ge> prob s" 
38656  81 
using assms by (blast intro: real_measure_mono) 
35582  82 
ultimately show ?thesis by simp 
83 
qed 

84 

85 
lemma prob_eq_compl: 

86 
assumes "s \<in> events" "t \<in> events" 

87 
assumes "prob (space M  s) = prob (space M  t)" 

88 
shows "prob s = prob t" 

38656  89 
using assms prob_compl by auto 
35582  90 

91 
lemma prob_one_inter: 

92 
assumes events:"s \<in> events" "t \<in> events" 

93 
assumes "prob t = 1" 

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

95 
proof  

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

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

99 
by blast 

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

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

35582  102 
qed 
103 

104 
lemma prob_eq_bigunion_image: 

105 
assumes "range f \<subseteq> events" "range g \<subseteq> events" 

106 
assumes "disjoint_family f" "disjoint_family g" 

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

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

109 
using assms 

110 
proof  

38656  111 
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 
112 
by (rule real_finite_measure_UNION[OF assms(1,3)]) 

113 
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" 

114 
by (rule real_finite_measure_UNION[OF assms(2,4)]) 

115 
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp 

35582  116 
qed 
117 

118 
lemma prob_countably_zero: 

119 
assumes "range c \<subseteq> events" 

120 
assumes "\<And> i. prob (c i) = 0" 

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

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

124 
using real_finite_measurable_countably_subadditive[OF assms(1)] 

125 
by (simp add: assms(2) suminf_zero summable_zero) 

126 
show "0 \<le> prob (\<Union> i :: nat. c i)" by (rule real_pinfreal_nonneg) 

35582  127 
qed 
128 

129 
lemma indep_sym: 

130 
"indep a b \<Longrightarrow> indep b a" 

131 
unfolding indep_def using Int_commute[of a b] by auto 

132 

133 
lemma indep_refl: 

134 
assumes "a \<in> events" 

135 
shows "indep a a = (prob a = 0) \<or> (prob a = 1)" 

136 
using assms unfolding indep_def by auto 

137 

138 
lemma prob_equiprobable_finite_unions: 

38656  139 
assumes "s \<in> events" 
140 
assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" 

35582  141 
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" 
38656  142 
shows "prob s = real (card s) * prob {SOME x. x \<in> s}" 
35582  143 
proof (cases "s = {}") 
38656  144 
case False hence "\<exists> x. x \<in> s" by blast 
35582  145 
from someI_ex[OF this] assms 
146 
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast 

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

38656  148 
using real_finite_measure_finite_singelton[OF s_finite] by simp 
35582  149 
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto 
38656  150 
also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}" 
151 
using setsum_constant assms by (simp add: real_eq_of_nat) 

35582  152 
finally show ?thesis by simp 
38656  153 
qed simp 
35582  154 

155 
lemma prob_real_sum_image_fn: 

156 
assumes "e \<in> events" 

157 
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" 

158 
assumes "finite s" 

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

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

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

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

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

167 
proof (rule real_finite_measure_finite_Union) 

168 
show "finite s" by fact 

169 
show "\<And>i. i \<in> s \<Longrightarrow> e \<inter> f i \<in> events" by fact 

170 
show "disjoint_family_on (\<lambda>i. e \<inter> f i) s" 

171 
using disjoint by (auto simp: disjoint_family_on_def) 

172 
qed 

173 
finally show ?thesis . 

35582  174 
qed 
175 

176 
lemma distribution_prob_space: 

39089  177 
assumes S: "sigma_algebra S" "random_variable S X" 
38656  178 
shows "prob_space S (distribution X)" 
35582  179 
proof  
39089  180 
interpret S: measure_space S "distribution X" 
181 
using measure_space_vimage[OF S(2,1)] unfolding distribution_def . 

38656  182 
show ?thesis 
183 
proof 

184 
have "X ` space S \<inter> space M = space M" 

185 
using `random_variable S X` by (auto simp: measurable_def) 

39089  186 
then show "distribution X (space S) = 1" 
187 
using measure_space_1 by (simp add: distribution_def) 

35582  188 
qed 
189 
qed 

190 

191 
lemma distribution_lebesgue_thm1: 

192 
assumes "random_variable s X" 

193 
assumes "A \<in> sets s" 

38656  194 
shows "real (distribution X A) = expectation (indicator (X ` A \<inter> space M))" 
35582  195 
unfolding distribution_def 
196 
using assms unfolding measurable_def 

38656  197 
using integral_indicator by auto 
35582  198 

199 
lemma distribution_lebesgue_thm2: 

38656  200 
assumes "sigma_algebra S" "random_variable S X" and "A \<in> sets S" 
201 
shows "distribution X A = 

202 
measure_space.positive_integral S (distribution X) (indicator A)" 

203 
(is "_ = measure_space.positive_integral _ ?D _") 

35582  204 
proof  
38656  205 
interpret S: prob_space S "distribution X" using assms(1,2) by (rule distribution_prob_space) 
35582  206 

207 
show ?thesis 

38656  208 
using S.positive_integral_indicator(1) 
35582  209 
using assms unfolding distribution_def by auto 
210 
qed 

211 

212 
lemma finite_expectation1: 

38656  213 
assumes "finite (X`space M)" and rv: "random_variable borel_space X" 
35582  214 
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X ` {r} \<inter> space M))" 
38656  215 
proof (rule integral_on_finite(2)[OF assms(2,1)]) 
216 
fix x have "X ` {x} \<inter> space M \<in> sets M" 

217 
using rv unfolding measurable_def by auto 

218 
thus "\<mu> (X ` {x} \<inter> space M) \<noteq> \<omega>" using finite_measure by simp 

219 
qed 

35582  220 

221 
lemma finite_expectation: 

38656  222 
assumes "finite (space M)" "random_variable borel_space X" 
223 
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * real (distribution X {r}))" 

224 
using assms unfolding distribution_def using finite_expectation1 by auto 

225 

35582  226 
lemma prob_x_eq_1_imp_prob_y_eq_0: 
227 
assumes "{x} \<in> events" 

38656  228 
assumes "prob {x} = 1" 
35582  229 
assumes "{y} \<in> events" 
230 
assumes "y \<noteq> x" 

231 
shows "prob {y} = 0" 

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

233 

38656  234 
lemma distribution_empty[simp]: "distribution X {} = 0" 
235 
unfolding distribution_def by simp 

236 

237 
lemma distribution_space[simp]: "distribution X (X ` space M) = 1" 

238 
proof  

239 
have "X ` X ` space M \<inter> space M = space M" by auto 

240 
thus ?thesis unfolding distribution_def by (simp add: measure_space_1) 

241 
qed 

242 

243 
lemma distribution_one: 

244 
assumes "random_variable M X" and "A \<in> events" 

245 
shows "distribution X A \<le> 1" 

246 
proof  

247 
have "distribution X A \<le> \<mu> (space M)" unfolding distribution_def 

248 
using assms[unfolded measurable_def] by (auto intro!: measure_mono) 

249 
thus ?thesis by (simp add: measure_space_1) 

250 
qed 

251 

252 
lemma distribution_finite: 

253 
assumes "random_variable M X" and "A \<in> events" 

254 
shows "distribution X A \<noteq> \<omega>" 

255 
using distribution_one[OF assms] by auto 

256 

35582  257 
lemma distribution_x_eq_1_imp_distribution_y_eq_0: 
258 
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X" 

38656  259 
(is "random_variable ?S X") 
260 
assumes "distribution X {x} = 1" 

35582  261 
assumes "y \<noteq> x" 
262 
shows "distribution X {y} = 0" 

263 
proof  

38656  264 
have "sigma_algebra ?S" by (rule sigma_algebra_Pow) 
265 
from distribution_prob_space[OF this X] 

266 
interpret S: prob_space ?S "distribution X" by simp 

267 

268 
have x: "{x} \<in> sets ?S" 

269 
proof (rule ccontr) 

270 
assume "{x} \<notin> sets ?S" 

35582  271 
hence "X ` {x} \<inter> space M = {}" by auto 
38656  272 
thus "False" using assms unfolding distribution_def by auto 
273 
qed 

274 

275 
have [simp]: "{y} \<inter> {x} = {}" "{x}  {y} = {x}" using `y \<noteq> x` by auto 

276 

277 
show ?thesis 

278 
proof cases 

279 
assume "{y} \<in> sets ?S" 

280 
with `{x} \<in> sets ?S` assms show "distribution X {y} = 0" 

281 
using S.measure_inter_full_set[of "{y}" "{x}"] 

282 
by simp 

283 
next 

284 
assume "{y} \<notin> sets ?S" 

35582  285 
hence "X ` {y} \<inter> space M = {}" by auto 
38656  286 
thus "distribution X {y} = 0" unfolding distribution_def by auto 
287 
qed 

35582  288 
qed 
289 

290 
end 

291 

35977  292 
locale finite_prob_space = prob_space + finite_measure_space 
293 

36624  294 
lemma finite_prob_space_eq: 
38656  295 
"finite_prob_space M \<mu> \<longleftrightarrow> finite_measure_space M \<mu> \<and> \<mu> (space M) = 1" 
36624  296 
unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def 
297 
by auto 

298 

299 
lemma (in prob_space) not_empty: "space M \<noteq> {}" 

300 
using prob_space empty_measure by auto 

301 

38656  302 
lemma (in finite_prob_space) sum_over_space_eq_1: "(\<Sum>x\<in>space M. \<mu> {x}) = 1" 
303 
using measure_space_1 sum_over_space by simp 

36624  304 

305 
lemma (in finite_prob_space) positive_distribution: "0 \<le> distribution X x" 

38656  306 
unfolding distribution_def by simp 
36624  307 

308 
lemma (in finite_prob_space) joint_distribution_restriction_fst: 

309 
"joint_distribution X Y A \<le> distribution X (fst ` A)" 

310 
unfolding distribution_def 

311 
proof (safe intro!: measure_mono) 

312 
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" 

313 
show "x \<in> X ` fst ` A" 

314 
by (auto intro!: image_eqI[OF _ *]) 

315 
qed (simp_all add: sets_eq_Pow) 

316 

317 
lemma (in finite_prob_space) joint_distribution_restriction_snd: 

318 
"joint_distribution X Y A \<le> distribution Y (snd ` A)" 

319 
unfolding distribution_def 

320 
proof (safe intro!: measure_mono) 

321 
fix x assume "x \<in> space M" and *: "(X x, Y x) \<in> A" 

322 
show "x \<in> Y ` snd ` A" 

323 
by (auto intro!: image_eqI[OF _ *]) 

324 
qed (simp_all add: sets_eq_Pow) 

325 

326 
lemma (in finite_prob_space) distribution_order: 

327 
shows "0 \<le> distribution X x'" 

328 
and "(distribution X x' \<noteq> 0) \<longleftrightarrow> (0 < distribution X x')" 

329 
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution X {x}" 

330 
and "r \<le> joint_distribution X Y {(x, y)} \<Longrightarrow> r \<le> distribution Y {y}" 

331 
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution X {x}" 

332 
and "r < joint_distribution X Y {(x, y)} \<Longrightarrow> r < distribution Y {y}" 

333 
and "distribution X {x} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" 

334 
and "distribution Y {y} = 0 \<Longrightarrow> joint_distribution X Y {(x, y)} = 0" 

335 
using positive_distribution[of X x'] 

336 
positive_distribution[of "\<lambda>x. (X x, Y x)" "{(x, y)}"] 

337 
joint_distribution_restriction_fst[of X Y "{(x, y)}"] 

338 
joint_distribution_restriction_snd[of X Y "{(x, y)}"] 

339 
by auto 

340 

39097  341 
lemma (in finite_prob_space) distribution_mono: 
342 
assumes "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" 

343 
shows "distribution X x \<le> distribution Y y" 

344 
unfolding distribution_def 

345 
using assms by (auto simp: sets_eq_Pow intro!: measure_mono) 

346 

347 
lemma (in finite_prob_space) distribution_mono_gt_0: 

348 
assumes gt_0: "0 < distribution X x" 

349 
assumes *: "\<And>t. \<lbrakk> t \<in> space M ; X t \<in> x \<rbrakk> \<Longrightarrow> Y t \<in> y" 

350 
shows "0 < distribution Y y" 

351 
by (rule less_le_trans[OF gt_0 distribution_mono]) (rule *) 

352 

353 
lemma (in finite_prob_space) sum_over_space_distrib: 

354 
"(\<Sum>x\<in>X`space M. distribution X {x}) = 1" 

355 
unfolding distribution_def measure_space_1[symmetric] using finite_space 

356 
by (subst measure_finitely_additive'') 

357 
(auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=\<mu>]) 

358 

359 
lemma (in finite_prob_space) sum_over_space_real_distribution: 

360 
"(\<Sum>x\<in>X`space M. real (distribution X {x})) = 1" 

361 
unfolding distribution_def prob_space[symmetric] using finite_space 

362 
by (subst real_finite_measure_finite_Union[symmetric]) 

363 
(auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob]) 

364 

365 
lemma (in finite_prob_space) finite_sum_over_space_eq_1: 

366 
"(\<Sum>x\<in>space M. real (\<mu> {x})) = 1" 

367 
using sum_over_space_eq_1 finite_measure by (simp add: real_of_pinfreal_setsum sets_eq_Pow) 

368 

369 
lemma (in finite_prob_space) distribution_finite: 

370 
"distribution X A \<noteq> \<omega>" 

371 
using finite_measure[of "X ` A \<inter> space M"] 

372 
unfolding distribution_def sets_eq_Pow by auto 

373 

374 
lemma (in finite_prob_space) real_distribution_gt_0[simp]: 

375 
"0 < real (distribution Y y) \<longleftrightarrow> 0 < distribution Y y" 

376 
using assms by (auto intro!: real_pinfreal_pos distribution_finite) 

377 

378 
lemma (in finite_prob_space) real_distribution_mult_pos_pos: 

379 
assumes "0 < distribution Y y" 

380 
and "0 < distribution X x" 

381 
shows "0 < real (distribution Y y * distribution X x)" 

382 
unfolding real_of_pinfreal_mult[symmetric] 

383 
using assms by (auto intro!: mult_pos_pos) 

384 

385 
lemma (in finite_prob_space) real_distribution_divide_pos_pos: 

386 
assumes "0 < distribution Y y" 

387 
and "0 < distribution X x" 

388 
shows "0 < real (distribution Y y / distribution X x)" 

389 
unfolding divide_pinfreal_def real_of_pinfreal_mult[symmetric] 

390 
using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos) 

391 

392 
lemma (in finite_prob_space) real_distribution_mult_inverse_pos_pos: 

393 
assumes "0 < distribution Y y" 

394 
and "0 < distribution X x" 

395 
shows "0 < real (distribution Y y * inverse (distribution X x))" 

396 
unfolding divide_pinfreal_def real_of_pinfreal_mult[symmetric] 

397 
using assms distribution_finite[of X x] by (cases "distribution X x") (auto intro!: mult_pos_pos) 

398 

399 
lemma (in prob_space) distribution_remove_const: 

400 
shows "joint_distribution X (\<lambda>x. ()) {(x, ())} = distribution X {x}" 

401 
and "joint_distribution (\<lambda>x. ()) X {((), x)} = distribution X {x}" 

402 
and "joint_distribution X (\<lambda>x. (Y x, ())) {(x, y, ())} = joint_distribution X Y {(x, y)}" 

403 
and "joint_distribution X (\<lambda>x. ((), Y x)) {(x, (), y)} = joint_distribution X Y {(x, y)}" 

404 
and "distribution (\<lambda>x. ()) {()} = 1" 

405 
unfolding measure_space_1[symmetric] 

406 
by (auto intro!: arg_cong[where f="\<mu>"] simp: distribution_def) 

35977  407 

39097  408 
lemma (in finite_prob_space) setsum_distribution_gen: 
409 
assumes "Z ` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y ` {f x}) \<inter> space M" 

410 
and "inj_on f (X`space M)" 

411 
shows "(\<Sum>x \<in> X`space M. distribution Y {f x}) = distribution Z {c}" 

412 
unfolding distribution_def assms 

413 
using finite_space assms 

414 
by (subst measure_finitely_additive'') 

415 
(auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def 

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

417 

418 
lemma (in finite_prob_space) setsum_distribution: 

419 
"(\<Sum>x \<in> X`space M. joint_distribution X Y {(x, y)}) = distribution Y {y}" 

420 
"(\<Sum>y \<in> Y`space M. joint_distribution X Y {(x, y)}) = distribution X {x}" 

421 
"(\<Sum>x \<in> X`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution Y Z {(y, z)}" 

422 
"(\<Sum>y \<in> Y`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Z {(x, z)}" 

423 
"(\<Sum>z \<in> Z`space M. joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)}) = joint_distribution X Y {(x, y)}" 

424 
by (auto intro!: inj_onI setsum_distribution_gen) 

425 

426 
lemma (in finite_prob_space) setsum_real_distribution_gen: 

427 
assumes "Z ` {c} \<inter> space M = (\<Union>x \<in> X`space M. Y ` {f x}) \<inter> space M" 

428 
and "inj_on f (X`space M)" 

429 
shows "(\<Sum>x \<in> X`space M. real (distribution Y {f x})) = real (distribution Z {c})" 

430 
unfolding distribution_def assms 

431 
using finite_space assms 

432 
by (subst real_finite_measure_finite_Union[symmetric]) 

433 
(auto simp add: disjoint_family_on_def sets_eq_Pow inj_on_def 

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

435 

436 
lemma (in finite_prob_space) setsum_real_distribution: 

437 
"(\<Sum>x \<in> X`space M. real (joint_distribution X Y {(x, y)})) = real (distribution Y {y})" 

438 
"(\<Sum>y \<in> Y`space M. real (joint_distribution X Y {(x, y)})) = real (distribution X {x})" 

439 
"(\<Sum>x \<in> X`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution Y Z {(y, z)})" 

440 
"(\<Sum>y \<in> Y`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Z {(x, z)})" 

441 
"(\<Sum>z \<in> Z`space M. real (joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)})) = real (joint_distribution X Y {(x, y)})" 

442 
by (auto intro!: inj_onI setsum_real_distribution_gen) 

443 

444 
lemma (in finite_prob_space) real_distribution_order: 

445 
shows "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution X {x})" 

446 
and "r \<le> real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r \<le> real (distribution Y {y})" 

447 
and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution X {x})" 

448 
and "r < real (joint_distribution X Y {(x, y)}) \<Longrightarrow> r < real (distribution Y {y})" 

449 
and "distribution X {x} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" 

450 
and "distribution Y {y} = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" 

451 
using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"] 

452 
using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"] 

453 
using real_pinfreal_nonneg[of "joint_distribution X Y {(x, y)}"] 

454 
by auto 

455 

456 
lemma (in prob_space) joint_distribution_remove[simp]: 

457 
"joint_distribution X X {(x, x)} = distribution X {x}" 

458 
unfolding distribution_def by (auto intro!: arg_cong[where f="\<mu>"]) 

459 

460 
lemma (in finite_prob_space) distribution_1: 

461 
"distribution X A \<le> 1" 

462 
unfolding distribution_def measure_space_1[symmetric] 

463 
by (auto intro!: measure_mono simp: sets_eq_Pow) 

464 

465 
lemma (in finite_prob_space) real_distribution_1: 

466 
"real (distribution X A) \<le> 1" 

467 
unfolding real_pinfreal_1[symmetric] 

468 
by (rule real_of_pinfreal_mono[OF _ distribution_1]) simp 

469 

470 
lemma (in finite_prob_space) uniform_prob: 

471 
assumes "x \<in> space M" 

472 
assumes "\<And> x y. \<lbrakk>x \<in> space M ; y \<in> space M\<rbrakk> \<Longrightarrow> prob {x} = prob {y}" 

473 
shows "prob {x} = 1 / real (card (space M))" 

474 
proof  

475 
have prob_x: "\<And> y. y \<in> space M \<Longrightarrow> prob {y} = prob {x}" 

476 
using assms(2)[OF _ `x \<in> space M`] by blast 

477 
have "1 = prob (space M)" 

478 
using prob_space by auto 

479 
also have "\<dots> = (\<Sum> x \<in> space M. prob {x})" 

480 
using real_finite_measure_finite_Union[of "space M" "\<lambda> x. {x}", simplified] 

481 
sets_eq_Pow inj_singleton[unfolded inj_on_def, rule_format] 

482 
finite_space unfolding disjoint_family_on_def prob_space[symmetric] 

483 
by (auto simp add:setsum_restrict_set) 

484 
also have "\<dots> = (\<Sum> y \<in> space M. prob {x})" 

485 
using prob_x by auto 

486 
also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp 

487 
finally have one: "1 = real (card (space M)) * prob {x}" 

488 
using real_eq_of_nat by auto 

489 
hence two: "real (card (space M)) \<noteq> 0" by fastsimp 

490 
from one have three: "prob {x} \<noteq> 0" by fastsimp 

491 
thus ?thesis using one two three divide_cancel_right 

492 
by (auto simp:field_simps) 

39092  493 
qed 
35977  494 

39092  495 
lemma (in prob_space) prob_space_subalgebra: 
496 
assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)" 

497 
shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>" 

498 
proof  

499 
interpret N: measure_space "M\<lparr> sets := N \<rparr>" \<mu> 

500 
using measure_space_subalgebra[OF assms] . 

501 
show ?thesis 

502 
proof qed (simp add: measure_space_1) 

35977  503 
qed 
504 

39092  505 
lemma (in prob_space) prob_space_of_restricted_space: 
506 
assumes "\<mu> A \<noteq> 0" "\<mu> A \<noteq> \<omega>" "A \<in> sets M" 

507 
shows "prob_space (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)" 

508 
unfolding prob_space_def prob_space_axioms_def 

509 
proof 

510 
show "\<mu> (space (restricted_space A)) / \<mu> A = 1" 

511 
using `\<mu> A \<noteq> 0` `\<mu> A \<noteq> \<omega>` by (auto simp: pinfreal_noteq_omega_Ex) 

512 
have *: "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" by (simp add: mult_commute) 

513 
interpret A: measure_space "restricted_space A" \<mu> 

514 
using `A \<in> sets M` by (rule restricted_measure_space) 

515 
show "measure_space (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)" 

516 
proof 

517 
show "\<mu> {} / \<mu> A = 0" by auto 

518 
show "countably_additive (restricted_space A) (\<lambda>S. \<mu> S / \<mu> A)" 

519 
unfolding countably_additive_def psuminf_cmult_right * 

520 
using A.measure_countably_additive by auto 

521 
qed 

522 
qed 

523 

524 
lemma finite_prob_spaceI: 

525 
assumes "finite (space M)" "sets M = Pow(space M)" "\<mu> (space M) = 1" "\<mu> {} = 0" 

526 
and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B" 

527 
shows "finite_prob_space M \<mu>" 

528 
unfolding finite_prob_space_eq 

529 
proof 

530 
show "finite_measure_space M \<mu>" using assms 

531 
by (auto intro!: finite_measure_spaceI) 

532 
show "\<mu> (space M) = 1" by fact 

533 
qed 

36624  534 

535 
lemma (in finite_prob_space) finite_measure_space: 

39097  536 
fixes X :: "'a \<Rightarrow> 'x" 
38656  537 
shows "finite_measure_space \<lparr>space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)" 
538 
(is "finite_measure_space ?S _") 

39092  539 
proof (rule finite_measure_spaceI, simp_all) 
36624  540 
show "finite (X ` space M)" using finite_space by simp 
39097  541 
next 
542 
fix A B :: "'x set" assume "A \<inter> B = {}" 

543 
then show "distribution X (A \<union> B) = distribution X A + distribution X B" 

544 
unfolding distribution_def 

545 
by (subst measure_additive) 

546 
(auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow) 

36624  547 
qed 
548 

39097  549 
lemma (in finite_prob_space) finite_prob_space_of_images: 
550 
"finite_prob_space \<lparr> space = X ` space M, sets = Pow (X ` space M)\<rparr> (distribution X)" 

551 
by (simp add: finite_prob_space_eq finite_measure_space) 

552 

553 
lemma (in prob_space) joint_distribution_commute: 

554 
"joint_distribution X Y x = joint_distribution Y X ((\<lambda>(x,y). (y,x))`x)" 

555 
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) 

556 

557 
lemma (in finite_prob_space) real_distribution_order': 

558 
shows "real (distribution X {x}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" 

559 
and "real (distribution Y {y}) = 0 \<Longrightarrow> real (joint_distribution X Y {(x, y)}) = 0" 

560 
using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_fst, of X Y "{(x, y)}"] 

561 
using real_of_pinfreal_mono[OF distribution_finite joint_distribution_restriction_snd, of X Y "{(x, y)}"] 

562 
using real_pinfreal_nonneg[of "joint_distribution X Y {(x, y)}"] 

563 
by auto 

564 

39096  565 
lemma (in finite_prob_space) finite_product_measure_space: 
39097  566 
fixes X :: "'a \<Rightarrow> 'x" and Y :: "'a \<Rightarrow> 'y" 
39096  567 
assumes "finite s1" "finite s2" 
568 
shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2)\<rparr> (joint_distribution X Y)" 

569 
(is "finite_measure_space ?M ?D") 

39097  570 
proof (rule finite_measure_spaceI, simp_all) 
571 
show "finite (s1 \<times> s2)" 

39096  572 
using assms by auto 
39097  573 
show "joint_distribution X Y (s1\<times>s2) \<noteq> \<omega>" 
574 
using distribution_finite . 

575 
next 

576 
fix A B :: "('x*'y) set" assume "A \<inter> B = {}" 

577 
then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B" 

578 
unfolding distribution_def 

579 
by (subst measure_additive) 

580 
(auto intro!: arg_cong[where f=\<mu>] simp: sets_eq_Pow) 

39096  581 
qed 
582 

39097  583 
lemma (in finite_prob_space) finite_product_measure_space_of_images: 
39096  584 
shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, 
585 
sets = Pow (X ` space M \<times> Y ` space M) \<rparr> 

586 
(joint_distribution X Y)" 

587 
using finite_space by (auto intro!: finite_product_measure_space) 

588 

39085  589 
section "Conditional Expectation and Probability" 
590 

591 
lemma (in prob_space) conditional_expectation_exists: 

39083  592 
fixes X :: "'a \<Rightarrow> pinfreal" 
593 
assumes borel: "X \<in> borel_measurable M" 

594 
and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)" 

595 
shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N. 

596 
positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)" 

597 
proof  

598 
interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu> 

599 
using prob_space_subalgebra[OF N_subalgebra] . 

600 

601 
let "?f A" = "\<lambda>x. X x * indicator A x" 

602 
let "?Q A" = "positive_integral (?f A)" 

603 

604 
from measure_space_density[OF borel] 

605 
have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q" 

606 
by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra]) 

607 
then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q . 

608 

609 
have "P.absolutely_continuous ?Q" 

610 
unfolding P.absolutely_continuous_def 

611 
proof (safe, simp) 

612 
fix A assume "A \<in> N" "\<mu> A = 0" 

613 
moreover then have f_borel: "?f A \<in> borel_measurable M" 

614 
using borel N_subalgebra by (auto intro: borel_measurable_indicator) 

615 
moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A ` {0<..} \<inter> space M) \<inter> A" 

616 
by (auto simp: indicator_def) 

617 
moreover have "\<mu> \<dots> \<le> \<mu> A" 

618 
using `A \<in> N` N_subalgebra f_borel 

619 
by (auto intro!: measure_mono Int[of _ A] measurable_sets) 

620 
ultimately show "?Q A = 0" 

621 
by (simp add: positive_integral_0_iff) 

622 
qed 

623 
from P.Radon_Nikodym[OF Q this] 

624 
obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)" 

625 
"\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)" 

626 
by blast 

39084  627 
with N_subalgebra show ?thesis 
628 
by (auto intro!: bexI[OF _ Y(1)]) 

39083  629 
qed 
630 

39085  631 
definition (in prob_space) 
632 
"conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>) 

633 
\<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))" 

634 

635 
abbreviation (in prob_space) 

39092  636 
"conditional_prob N A \<equiv> conditional_expectation N (indicator A)" 
39085  637 

638 
lemma (in prob_space) 

639 
fixes X :: "'a \<Rightarrow> pinfreal" 

640 
assumes borel: "X \<in> borel_measurable M" 

641 
and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)" 

642 
shows borel_measurable_conditional_expectation: 

643 
"conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)" 

644 
and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow> 

645 
positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) = 

646 
positive_integral (\<lambda>x. X x * indicator C x)" 

647 
(is "\<And>C. C \<in> N \<Longrightarrow> ?eq C") 

648 
proof  

649 
note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] 

650 
then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)" 

651 
unfolding conditional_expectation_def by (rule someI2_ex) blast 

652 

653 
from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C" 

654 
unfolding conditional_expectation_def by (rule someI2_ex) blast 

655 
qed 

656 

39091  657 
lemma (in sigma_algebra) factorize_measurable_function: 
658 
fixes Z :: "'a \<Rightarrow> pinfreal" and Y :: "'a \<Rightarrow> 'c" 

659 
assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M" 

660 
shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) 

661 
\<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))" 

662 
proof safe 

663 
interpret M': sigma_algebra M' by fact 

664 
have Y: "Y \<in> space M \<rightarrow> space M'" using assms unfolding measurable_def by auto 

665 
from M'.sigma_algebra_vimage[OF this] 

666 
interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . 

667 

668 
{ fix g :: "'c \<Rightarrow> pinfreal" assume "g \<in> borel_measurable M'" 

669 
with M'.measurable_vimage_algebra[OF Y] 

670 
have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" 

671 
by (rule measurable_comp) 

672 
moreover assume "\<forall>x\<in>space M. Z x = g (Y x)" 

673 
then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow> 

674 
g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)" 

675 
by (auto intro!: measurable_cong) 

676 
ultimately show "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" 

677 
by simp } 

678 

679 
assume "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y)" 

680 
from va.borel_measurable_implies_simple_function_sequence[OF this] 

681 
obtain f where f: "\<And>i. va.simple_function (f i)" and "f \<up> Z" by blast 

682 

683 
have "\<forall>i. \<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" 

684 
proof 

685 
fix i 

686 
from f[of i] have "finite (f i`space M)" and B_ex: 

687 
"\<forall>z\<in>(f i)`space M. \<exists>B. B \<in> sets M' \<and> (f i) ` {z} \<inter> space M = Y ` B \<inter> space M" 

688 
unfolding va.simple_function_def by auto 

689 
from B_ex[THEN bchoice] guess B .. note B = this 

690 

691 
let ?g = "\<lambda>x. \<Sum>z\<in>f i`space M. z * indicator (B z) x" 

692 

693 
show "\<exists>g. M'.simple_function g \<and> (\<forall>x\<in>space M. f i x = g (Y x))" 

694 
proof (intro exI[of _ ?g] conjI ballI) 

695 
show "M'.simple_function ?g" using B by auto 

696 

697 
fix x assume "x \<in> space M" 

698 
then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i ` {z} \<inter> space M) x::pinfreal)" 

699 
unfolding indicator_def using B by auto 

700 
then show "f i x = ?g (Y x)" using `x \<in> space M` f[of i] 

701 
by (subst va.simple_function_indicator_representation) auto 

702 
qed 

703 
qed 

704 
from choice[OF this] guess g .. note g = this 

705 

706 
show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)" 

707 
proof (intro ballI bexI) 

708 
show "(SUP i. g i) \<in> borel_measurable M'" 

709 
using g by (auto intro: M'.borel_measurable_simple_function) 

710 
fix x assume "x \<in> space M" 

711 
have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp 

712 
also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand 

713 
using g `x \<in> space M` by simp 

714 
finally show "Z x = (SUP i. g i) (Y x)" . 

715 
qed 

716 
qed 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
39089
diff
changeset

717 

35582  718 
end 