author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51683  baefa3b461c2 
child 53015  a1119cf551e8 
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 

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

12 
locale prob_space = finite_measure + 
47694  13 
assumes emeasure_space_1: "emeasure M (space M) = 1" 
38656  14 

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

15 
lemma prob_spaceI[Pure.intro!]: 
47694  16 
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

17 
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

18 
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

19 
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

20 
proof 
47694  21 
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

22 
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

23 
show "prob_space M" by default fact 
38656  24 
qed 
25 

40859  26 
abbreviation (in prob_space) "events \<equiv> sets M" 
47694  27 
abbreviation (in prob_space) "prob \<equiv> measure M" 
28 
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

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

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

33 
proof (rule prob_spaceI) 

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

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

36 
by (auto simp: emeasure_distr emeasure_space_1) 

43339  37 
qed 
38 

40859  39 
lemma (in prob_space) prob_space: "prob (space M) = 1" 
47694  40 
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

41 

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

42 
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

43 
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

44 

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

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

47 

47694  48 
lemma (in prob_space) measure_le_1: "emeasure M X \<le> 1" 
49 
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

50 

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

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

43339  57 
qed (insert assms, auto) 
58 

40859  59 
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

60 
assumes A: "A \<in> events" 
38656  61 
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

62 
using finite_measure_compl[OF A] by (simp add: prob_space) 
35582  63 

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

66 
proof 

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

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

69 
using `A \<in> events`[THEN sets.sets_into_space] by auto 
47694  70 
with AE_E2[OF ae] `A \<in> events` have "1  emeasure M A = 0" 
71 
by (simp add: emeasure_compl emeasure_space_1) 

72 
then show "prob A = 1" 

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

74 
next 

75 
assume prob: "prob A = 1" 

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

77 
proof (rule AE_I) 

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

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

80 
using `A \<in> events` prob 

81 
by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def) 

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

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

84 
qed 

85 
qed 

86 

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

88 
proof 

89 
assume "AE x in M. False" 

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

91 
then show False 

92 
by (subst (asm) AE_in_set_eq_1) auto 

93 
qed simp 

94 

95 
lemma (in prob_space) AE_prob_1: 

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

97 
proof  

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

99 
by (metis measure_notin_sets zero_neq_one) 

100 
with AE_in_set_eq_1 assms show ?thesis by simp 

101 
qed 

102 

50098  103 
lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P" 
104 
by (cases P) (auto simp: AE_False) 

105 

106 
lemma (in prob_space) AE_contr: 

107 
assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>" 

108 
shows False 

109 
proof  

110 
from ae have "AE \<omega> in M. False" by eventually_elim auto 

111 
then show False by auto 

112 
qed 

113 

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

49786  116 
assumes gt: "AE x in M. X x < b" 
43339  117 
shows "expectation X < b" 
118 
proof  

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

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

121 
by (intro integral_less_AE_space) auto 
43339  122 
then show ?thesis using prob_space by simp 
123 
qed 

124 

125 
lemma (in prob_space) expectation_greater: 

126 
assumes [simp]: "integrable M X" 

49786  127 
assumes gt: "AE x in M. a < X x" 
43339  128 
shows "a < expectation X" 
129 
proof  

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

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

132 
by (intro integral_less_AE_space) auto 
43339  133 
then show ?thesis using prob_space by simp 
134 
qed 

135 

136 
lemma (in prob_space) jensens_inequality: 

137 
fixes a b :: real 

49786  138 
assumes X: "integrable M X" "AE x in M. X x \<in> I" 
43339  139 
assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" 
140 
assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" 

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

142 
proof  

46731  143 
let ?F = "\<lambda>x. Inf ((\<lambda>t. (q x  q t) / (x  t)) ` ({x<..} \<inter> I))" 
49786  144 
from X(2) AE_False have "I \<noteq> {}" by auto 
43339  145 

146 
from I have "open I" by auto 

147 

148 
note I 

149 
moreover 

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

151 
with X have "a < expectation X" 

152 
by (intro expectation_greater) auto } 

153 
moreover 

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

155 
with X have "expectation X < b" 

156 
by (intro expectation_less) auto } 

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

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

159 
moreover 

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

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

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
50419
diff
changeset

162 
by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } 
43339  163 
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X  x)) ` I)" 
164 
by simp 

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

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
50419
diff
changeset

166 
proof (rule cSup_least) 
43339  167 
show "(\<lambda>x. q x + ?F x * (expectation X  x)) ` I \<noteq> {}" 
168 
using `I \<noteq> {}` by auto 

169 
next 

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

171 
then guess x .. note x = this 

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

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

49786  176 
apply (intro integral_mono_AE integral_add integral_cmult integral_diff 
177 
lebesgue_integral_const X q) 

178 
apply (elim eventually_elim1) 

179 
apply (intro convex_le_Inf_differential) 

180 
apply (auto simp: interior_open q) 

181 
done 

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

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

185 
qed 

186 

50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

187 
subsection {* Introduce binder for probability *} 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

188 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

189 
syntax 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

190 
"_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _'))") 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

191 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

192 
translations 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

193 
"\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

194 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

195 
definition 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

196 
"cond_prob M P Q = \<P>(\<omega> in M. P \<omega> \<and> Q \<omega>) / \<P>(\<omega> in M. Q \<omega>)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

197 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

198 
syntax 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

199 
"_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _ \<bar>/ _'))") 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

200 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

201 
translations 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

202 
"\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

203 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

204 
lemma (in prob_space) AE_E_prob: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

205 
assumes ae: "AE x in M. P x" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

206 
obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

207 
proof  
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

208 
from ae[THEN AE_E] guess N . 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

209 
then show thesis 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

210 
by (intro that[of "space M  N"]) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

211 
(auto simp: prob_compl prob_space emeasure_eq_measure) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

212 
qed 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

213 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

214 
lemma (in prob_space) prob_neg: "{x\<in>space M. P x} \<in> events \<Longrightarrow> \<P>(x in M. \<not> P x) = 1  \<P>(x in M. P x)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

215 
by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric]) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

216 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

217 
lemma (in prob_space) prob_eq_AE: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

218 
"(AE x in M. P x \<longleftrightarrow> Q x) \<Longrightarrow> {x\<in>space M. P x} \<in> events \<Longrightarrow> {x\<in>space M. Q x} \<in> events \<Longrightarrow> \<P>(x in M. P x) = \<P>(x in M. Q x)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

219 
by (rule finite_measure_eq_AE) auto 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

220 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

221 
lemma (in prob_space) prob_eq_0_AE: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

222 
assumes not: "AE x in M. \<not> P x" shows "\<P>(x in M. P x) = 0" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

223 
proof cases 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

224 
assume "{x\<in>space M. P x} \<in> events" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

225 
with not have "\<P>(x in M. P x) = \<P>(x in M. False)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

226 
by (intro prob_eq_AE) auto 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

227 
then show ?thesis by simp 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

228 
qed (simp add: measure_notin_sets) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

229 

50098  230 
lemma (in prob_space) prob_Collect_eq_0: 
231 
"{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)" 

232 
using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure) 

233 

234 
lemma (in prob_space) prob_Collect_eq_1: 

235 
"{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)" 

236 
using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp 

237 

238 
lemma (in prob_space) prob_eq_0: 

239 
"A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)" 

240 
using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"] 

241 
by (auto simp add: emeasure_eq_measure Int_def[symmetric]) 

242 

243 
lemma (in prob_space) prob_eq_1: 

244 
"A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)" 

245 
using AE_in_set_eq_1[of A] by simp 

246 

50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

247 
lemma (in prob_space) prob_sums: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

248 
assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

249 
assumes Q: "{x\<in>space M. Q x} \<in> events" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

250 
assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

251 
shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

252 
proof  
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

253 
from ae[THEN AE_E_prob] guess S . note S = this 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

254 
then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

255 
by (auto simp: disjoint_family_on_def) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

256 
from S have ae_S: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

257 
"AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n. {x\<in>space M. P n x} \<inter> S)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

258 
"\<And>n. AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

259 
using ae by (auto dest!: AE_prob_1) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

260 
from ae_S have *: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

261 
"\<P>(x in M. Q x) = prob (\<Union>n. {x\<in>space M. P n x} \<inter> S)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

262 
using P Q S by (intro finite_measure_eq_AE) auto 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

263 
from ae_S have **: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

264 
"\<And>n. \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

265 
using P Q S by (intro finite_measure_eq_AE) auto 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

266 
show ?thesis 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

267 
unfolding * ** using S P disj 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

268 
by (intro finite_measure_UNION) auto 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

269 
qed 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

270 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

271 
lemma (in prob_space) cond_prob_eq_AE: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

272 
assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

273 
assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

274 
shows "cond_prob M P Q = cond_prob M P' Q'" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

275 
using P Q 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

276 
by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj) 
50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

277 

382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

278 

40859  279 
lemma (in prob_space) joint_distribution_Times_le_fst: 
47694  280 
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 
281 
\<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" 

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

40859  283 

284 
lemma (in prob_space) joint_distribution_Times_le_snd: 

47694  285 
"random_variable MX X \<Longrightarrow> random_variable MY Y \<Longrightarrow> A \<in> sets MX \<Longrightarrow> B \<in> sets MY 
286 
\<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" 

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

40859  288 

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

289 
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

290 

47694  291 
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

292 
proof 
47694  293 
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1" 
49776  294 
by (simp add: M2.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

295 
qed 
40859  296 

47694  297 
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

298 
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

299 
assumes prob_space: "\<And>i. prob_space (M i)" 
42988  300 

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

301 
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i 
42988  302 
by (rule prob_space) 
303 

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

304 
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I 
42988  305 

306 
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

307 
proof 
47694  308 
show "emeasure (\<Pi>\<^isub>M i\<in>I. M i) (space (\<Pi>\<^isub>M i\<in>I. M i)) = 1" 
309 
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

310 
qed 
42988  311 

312 
lemma (in finite_product_prob_space) prob_times: 

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

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

315 
proof  

47694  316 
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)" 
317 
using X by (simp add: emeasure_eq_measure) 

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

42988  319 
using measure_times X by simp 
47694  320 
also have "\<dots> = ereal (\<Prod>i\<in>I. measure (M i) (X i))" 
321 
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

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

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

324 

47694  325 
section {* Distributions *} 
42892  326 

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

36624  329 

47694  330 
lemma 
50003  331 
assumes "distributed M N X f" 
332 
shows distributed_distr_eq_density: "distr M N X = density N f" 

333 
and distributed_measurable: "X \<in> measurable M N" 

334 
and distributed_borel_measurable: "f \<in> borel_measurable N" 

335 
and distributed_AE: "(AE x in N. 0 \<le> f x)" 

336 
using assms by (simp_all add: distributed_def) 

337 

338 
lemma 

339 
assumes D: "distributed M N X f" 

340 
shows distributed_measurable'[measurable_dest]: 

341 
"g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N" 

342 
and distributed_borel_measurable'[measurable_dest]: 

343 
"h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" 

344 
using distributed_measurable[OF D] distributed_borel_measurable[OF D] 

345 
by simp_all 

39097  346 

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

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

350 
by (simp_all add: distributed_def borel_measurable_ereal_iff) 

35977  351 

50003  352 
lemma 
353 
assumes D: "distributed M N X (\<lambda>x. ereal (f x))" 

354 
shows distributed_real_measurable'[measurable_dest]: 

355 
"h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L" 

356 
using distributed_real_measurable[OF D] 

357 
by simp_all 

358 

359 
lemma 

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

361 
shows joint_distributed_measurable1[measurable_dest]: 

362 
"h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S" 

363 
and joint_distributed_measurable2[measurable_dest]: 

364 
"h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T" 

365 
using measurable_compose[OF distributed_measurable[OF D] measurable_fst] 

366 
using measurable_compose[OF distributed_measurable[OF D] measurable_snd] 

367 
by auto 

368 

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

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

39097  372 
proof  
47694  373 
have "emeasure M (X ` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}" 
50003  374 
using X a A by (simp add: emeasure_distr) 
47694  375 
also have "\<dots> = emeasure (density (count_space A) P) {a}" 
376 
using X by (simp add: distributed_distr_eq_density) 

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

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

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

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

381 
finally show ?thesis .. 

39092  382 
qed 
35977  383 

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

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

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

388 

389 
lemma subdensity: 

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

391 
assumes f: "distributed M P X f" 

392 
assumes g: "distributed M Q Y g" 

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

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

395 
proof  

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

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

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

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

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

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

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

403 
using T by (auto dest: measurable_space) 

404 
finally show ?thesis 

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

35977  406 
qed 
407 

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

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

411 
assumes f: "distributed M P X f" 

412 
assumes g: "distributed M Q Y g" 

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

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

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

416 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

417 
lemma distributed_emeasure: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

418 
"distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X ` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)" 
50003  419 
by (auto simp: distributed_AE 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

420 
distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

421 

3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

422 
lemma distributed_positive_integral: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

423 
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)" 
50003  424 
by (auto simp: distributed_AE 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

425 
distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

426 

47694  427 
lemma distributed_integral: 
428 
"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)" 

50003  429 
by (auto simp: distributed_real_AE 
47694  430 
distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr) 
431 

432 
lemma distributed_transform_integral: 

433 
assumes Px: "distributed M N X Px" 

434 
assumes "distributed M P Y Py" 

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

436 
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

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

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

441 
using Y by simp 

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

443 
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

444 
finally show ?thesis . 
39092  445 
qed 
36624  446 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

447 
lemma (in prob_space) distributed_unique: 
47694  448 
assumes Px: "distributed M S X Px" 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

449 
assumes Py: "distributed M S X Py" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

450 
shows "AE x in S. Px x = Py x" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

451 
proof  
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

452 
interpret X: prob_space "distr M S X" 
50003  453 
using Px by (intro prob_space_distr) simp 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

454 
have "sigma_finite_measure (distr M S X)" .. 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

455 
with sigma_finite_density_unique[of Px S Py ] Px Py 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

456 
show ?thesis 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

457 
by (auto simp: distributed_def) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

458 
qed 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

459 

3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

460 
lemma (in prob_space) distributed_jointI: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

461 
assumes "sigma_finite_measure S" "sigma_finite_measure T" 
50003  462 
assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T" 
463 
assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x" 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

464 
assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

465 
emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

466 
shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

467 
unfolding distributed_def 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

468 
proof safe 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

469 
interpret S: sigma_finite_measure S by fact 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

470 
interpret T: sigma_finite_measure T by fact 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

471 
interpret ST: pair_sigma_finite S T by default 
47694  472 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

473 
from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

474 
let ?E = "{a \<times> b a b. a \<in> sets S \<and> b \<in> sets T}" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

475 
let ?P = "S \<Otimes>\<^isub>M T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

476 
show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R") 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

477 
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]]) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

478 
show "?E \<subseteq> Pow (space ?P)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

479 
using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

480 
show "sets ?L = sigma_sets (space ?P) ?E" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

481 
by (simp add: sets_pair_measure space_pair_measure) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

482 
then show "sets ?R = sigma_sets (space ?P) ?E" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

483 
by simp 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

484 
next 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

485 
interpret L: prob_space ?L 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

486 
by (rule prob_space_distr) (auto intro!: measurable_Pair) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

487 
show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

488 
using F by (auto simp: space_pair_measure) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

489 
next 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

490 
fix E assume "E \<in> ?E" 
50003  491 
then obtain A B where E[simp]: "E = A \<times> B" 
492 
and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

493 
have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

494 
by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

495 
also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)" 
50003  496 
using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

497 
also have "\<dots> = emeasure ?R E" 
50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49795
diff
changeset

498 
by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

499 
intro!: positive_integral_cong split: split_indicator) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

500 
finally show "emeasure ?L E = emeasure ?R E" . 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

501 
qed 
50003  502 
qed (auto simp: f) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

503 

3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

504 
lemma (in prob_space) distributed_swap: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

505 
assumes "sigma_finite_measure S" "sigma_finite_measure T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

506 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

507 
shows "distributed M (T \<Otimes>\<^isub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

508 
proof  
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

509 
interpret S: sigma_finite_measure S by fact 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

510 
interpret T: sigma_finite_measure T by fact 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

511 
interpret ST: pair_sigma_finite S T by default 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

512 
interpret TS: pair_sigma_finite T S by default 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

513 

50003  514 
note Pxy[measurable] 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

515 
show ?thesis 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

516 
apply (subst TS.distr_pair_swap) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

517 
unfolding distributed_def 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

518 
proof safe 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

519 
let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

520 
show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D" 
50003  521 
by auto 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

522 
with Pxy 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

523 
show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

524 
by (subst AE_distr_iff) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

525 
(auto dest!: distributed_AE 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

526 
simp: measurable_split_conv split_beta 
51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51475
diff
changeset

527 
intro!: measurable_Pair) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

528 
show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))" 
50003  529 
using Pxy by auto 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

530 
{ fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

531 
let ?B = "(\<lambda>(x, y). (y, x)) ` A \<inter> space (S \<Otimes>\<^isub>M T)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

532 
from sets.sets_into_space[OF A] 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

533 
have "emeasure M ((\<lambda>x. (Y x, X x)) ` A \<inter> space M) = 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

534 
emeasure M ((\<lambda>x. (X x, Y x)) ` ?B \<inter> space M)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

535 
by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

536 
also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))" 
50003  537 
using Pxy A by (intro distributed_emeasure) auto 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

538 
finally have "emeasure M ((\<lambda>x. (Y x, X x)) ` A \<inter> space M) = 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

539 
(\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

540 
by (auto intro!: positive_integral_cong split: split_indicator) } 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

541 
note * = this 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

542 
show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

543 
apply (intro measure_eqI) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

544 
apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1]) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

545 
apply (subst positive_integral_distr) 
50003  546 
apply (auto intro!: * simp: comp_def split_beta) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

547 
done 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

548 
qed 
36624  549 
qed 
550 

47694  551 
lemma (in prob_space) distr_marginal1: 
552 
assumes "sigma_finite_measure S" "sigma_finite_measure T" 

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

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

554 
defines "Px \<equiv> \<lambda>x. (\<integral>\<^isup>+z. Pxy (x, z) \<partial>T)" 
47694  555 
shows "distributed M S X Px" 
556 
unfolding distributed_def 

557 
proof safe 

558 
interpret S: sigma_finite_measure S by fact 

559 
interpret T: sigma_finite_measure T by fact 

560 
interpret ST: pair_sigma_finite S T by default 

561 

50003  562 
note Pxy[measurable] 
563 
show X: "X \<in> measurable M S" by simp 

47694  564 

50003  565 
show borel: "Px \<in> borel_measurable S" 
566 
by (auto intro!: T.positive_integral_fst_measurable simp: Px_def) 

39097  567 

47694  568 
interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 
50003  569 
by (intro prob_space_distr) simp 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

570 
have "(\<integral>\<^isup>+ x. max 0 ( Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))" 
47694  571 
using Pxy 
50003  572 
by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

573 

47694  574 
show "distr M S X = density S Px" 
575 
proof (rule measure_eqI) 

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

50003  577 
with X measurable_space[of Y M T] 
578 
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)" 

579 
by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"]) 

47694  580 
also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)" 
581 
using Pxy by (simp add: distributed_def) 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

582 
also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" 
47694  583 
using A borel Pxy 
50003  584 
by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

585 
also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S" 
47694  586 
apply (rule positive_integral_cong_AE) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

587 
using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space 
47694  588 
proof eventually_elim 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

589 
fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)" 
47694  590 
moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x" 
591 
by (auto simp: indicator_def) 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

592 
ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x" 
50003  593 
by (simp add: eq positive_integral_multc cong: positive_integral_cong) 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

594 
also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

595 
by (simp add: Px_def ereal_real positive_integral_positive) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

596 
finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" . 
47694  597 
qed 
598 
finally show "emeasure (distr M S X) A = emeasure (density S Px) A" 

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

600 
qed simp 

601 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

602 
show "AE x in S. 0 \<le> Px x" 
47694  603 
by (simp add: Px_def positive_integral_positive real_of_ereal_pos) 
40859  604 
qed 
605 

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

606 
lemma (in prob_space) distr_marginal2: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

607 
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

608 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

609 
shows "distributed M T Y (\<lambda>y. (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

610 
using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

611 

3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

612 
lemma (in prob_space) distributed_marginal_eq_joint1: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

613 
assumes T: "sigma_finite_measure T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

614 
assumes S: "sigma_finite_measure S" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

615 
assumes Px: "distributed M S X Px" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

616 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

617 
shows "AE x in S. Px x = (\<integral>\<^isup>+y. Pxy (x, y) \<partial>T)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

618 
using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

619 

3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

620 
lemma (in prob_space) distributed_marginal_eq_joint2: 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

621 
assumes T: "sigma_finite_measure T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

622 
assumes S: "sigma_finite_measure S" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

623 
assumes Py: "distributed M T Y Py" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

624 
assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

625 
shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

626 
using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

627 

49795  628 
lemma (in prob_space) distributed_joint_indep': 
629 
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 

50003  630 
assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py" 
49795  631 
assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 
632 
shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" 

633 
unfolding distributed_def 

634 
proof safe 

635 
interpret S: sigma_finite_measure S by fact 

636 
interpret T: sigma_finite_measure T by fact 

637 
interpret ST: pair_sigma_finite S T by default 

638 

639 
interpret X: prob_space "density S Px" 

640 
unfolding distributed_distr_eq_density[OF X, symmetric] 

50003  641 
by (rule prob_space_distr) simp 
49795  642 
have sf_X: "sigma_finite_measure (density S Px)" .. 
643 

644 
interpret Y: prob_space "density T Py" 

645 
unfolding distributed_distr_eq_density[OF Y, symmetric] 

50003  646 
by (rule prob_space_distr) simp 
49795  647 
have sf_Y: "sigma_finite_measure (density T Py)" .. 
648 

649 
show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)" 

650 
unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y] 

651 
using distributed_borel_measurable[OF X] distributed_AE[OF X] 

652 
using distributed_borel_measurable[OF Y] distributed_AE[OF Y] 

50003  653 
by (rule pair_measure_density[OF _ _ _ _ T sf_Y]) 
49795  654 

50003  655 
show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto 
49795  656 

50003  657 
show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto 
49795  658 

659 
show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)" 

51683
baefa3b461c2
generalize Borelset properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
hoelzl
parents:
51475
diff
changeset

660 
apply (intro ST.AE_pair_measure borel_measurable_le Pxy borel_measurable_const) 
49795  661 
using distributed_AE[OF X] 
662 
apply eventually_elim 

663 
using distributed_AE[OF Y] 

664 
apply eventually_elim 

665 
apply auto 

666 
done 

667 
qed 

668 

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

671 
finite (X`space M)" 

42902  672 

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

675 
unfolding simple_distributed_def by auto 

42902  676 

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

42902  679 

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

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

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

684 
shows "distributed M S X P'" 

685 
unfolding distributed_def 

686 
proof safe 

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

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

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

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

691 
proof (rule measure_eqI_finite) 

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

693 
using A unfolding S_def by auto 

694 
show "finite A" by fact 

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

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

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

698 
by (subst emeasure_distr) 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

699 
(auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2 
47694  700 
intro!: arg_cong[where f=prob]) 
701 
also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)" 

702 
using A X a 

703 
by (subst positive_integral_cmult_indicator) 

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

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

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

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

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

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

710 
qed 

711 
show "random_variable S X" 

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

713 
qed 

42902  714 

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

717 
shows "simple_distributed M X P" 

718 
unfolding simple_distributed_def 

719 
proof 

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

721 
(is "?A") 

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

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

724 
by (rule distributed_cong_density) auto 

725 
finally show "\<dots>" . 

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

727 

728 
lemma simple_distributed_joint_finite: 

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

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

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

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

735 
by auto 

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

737 
by (auto simp: image_image) 

738 
qed 

739 

740 
lemma simple_distributed_joint2_finite: 

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

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

743 
proof  

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

745 
using X by (auto simp: simple_distributed_def simple_functionD) 

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

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

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

749 
by auto 

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

751 
by (auto simp: image_image) 

42902  752 
qed 
753 

47694  754 
lemma simple_distributed_simple_function: 
755 
"simple_distributed M X Px \<Longrightarrow> simple_function M X" 

756 
unfolding simple_distributed_def distributed_def 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

757 
by (auto simp: simple_function_def measurable_count_space_eq2) 
47694  758 

759 
lemma simple_distributed_measure: 

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

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

762 
by (auto simp: simple_distributed_def measure_def) 

763 

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

765 
by (auto simp: simple_distributed_measure measure_nonneg) 

42860  766 

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

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

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

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

772 
proof  

773 
from simple_distributed_joint_finite[OF X, simp] 

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

775 
by (simp add: S_def pair_measure_count_space) 

776 
show ?thesis 

777 
unfolding S_eq P_def 

778 
proof (rule distributed_simple_function_superset) 

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

780 
using X by (rule simple_distributed_simple_function) 

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

782 
from simple_distributed_measure[OF X this] 

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

784 
qed auto 

785 
qed 

42860  786 

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

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

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

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

792 
proof  

793 
from simple_distributed_joint2_finite[OF X, simp] 

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

795 
by (simp add: S_def pair_measure_count_space) 

796 
show ?thesis 

797 
unfolding S_eq P_def 

798 
proof (rule distributed_simple_function_superset) 

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

800 
using X by (rule simple_distributed_simple_function) 

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

802 
from simple_distributed_measure[OF X this] 

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

804 
qed auto 

805 
qed 

806 

807 
lemma (in prob_space) simple_distributed_setsum_space: 

808 
assumes X: "simple_distributed M X f" 

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

810 
proof  

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

812 
by (subst finite_measure_finite_Union) 

813 
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD 

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

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

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

817 
finally show ?thesis 

818 
using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def) 

819 
qed 

42860  820 

47694  821 
lemma (in prob_space) distributed_marginal_eq_joint_simple: 
822 
assumes Px: "simple_function M X" 

823 
assumes Py: "simple_distributed M Y Py" 

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

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

826 
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)" 

827 
proof  

828 
note Px = simple_distributedI[OF Px refl] 

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

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

49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

831 
from distributed_marginal_eq_joint2[OF 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

832 
sigma_finite_measure_count_space_finite 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

833 
sigma_finite_measure_count_space_finite 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

834 
simple_distributed[OF Py] simple_distributed_joint[OF Pxy], 
47694  835 
OF Py[THEN simple_distributed_finite] Px[THEN simple_distributed_finite]] 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

836 
y 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

837 
Px[THEN simple_distributed_finite] 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

838 
Py[THEN simple_distributed_finite] 
47694  839 
Pxy[THEN simple_distributed, THEN distributed_real_AE] 
840 
show ?thesis 

841 
unfolding AE_count_space 

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

843 
done 

844 
qed 

42860  845 

50419  846 
lemma distributedI_real: 
847 
fixes f :: "'a \<Rightarrow> real" 

848 
assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E" 

849 
and A: "range A \<subseteq> E" "(\<Union>i::nat. A i) = space M1" "\<And>i. emeasure (distr M M1 X) (A i) \<noteq> \<infinity>" 

850 
and X: "X \<in> measurable M M1" 

851 
and f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x" 

852 
and eq: "\<And>A. A \<in> E \<Longrightarrow> emeasure M (X ` A \<inter> space M) = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M1)" 

853 
shows "distributed M M1 X f" 

854 
unfolding distributed_def 

855 
proof (intro conjI) 

856 
show "distr M M1 X = density M1 f" 

857 
proof (rule measure_eqI_generator_eq[where A=A]) 

858 
{ fix A assume A: "A \<in> E" 

859 
then have "A \<in> sigma_sets (space M1) E" by auto 

860 
then have "A \<in> sets M1" 

861 
using gen by simp 

862 
with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A" 

863 
by (simp add: emeasure_distr emeasure_density borel_measurable_ereal 

864 
times_ereal.simps[symmetric] ereal_indicator 

865 
del: times_ereal.simps) } 

866 
note eq_E = this 

867 
show "Int_stable E" by fact 

868 
{ fix e assume "e \<in> E" 

869 
then have "e \<in> sigma_sets (space M1) E" by auto 

870 
then have "e \<in> sets M1" unfolding gen . 

871 
then have "e \<subseteq> space M1" by (rule sets.sets_into_space) } 

872 
then show "E \<subseteq> Pow (space M1)" by auto 

873 
show "sets (distr M M1 X) = sigma_sets (space M1) E" 

874 
"sets (density M1 (\<lambda>x. ereal (f x))) = sigma_sets (space M1) E" 

875 
unfolding gen[symmetric] by auto 

876 
qed fact+ 

877 
qed (insert X f, auto) 

878 

879 
lemma distributedI_borel_atMost: 

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

881 
assumes [measurable]: "X \<in> borel_measurable M" 

882 
and [measurable]: "f \<in> borel_measurable borel" and f[simp]: "AE x in lborel. 0 \<le> f x" 

883 
and g_eq: "\<And>a. (\<integral>\<^isup>+x. f x * indicator {..a} x \<partial>lborel) = ereal (g a)" 

884 
and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)" 

885 
shows "distributed M lborel X f" 

886 
proof (rule distributedI_real) 

887 
show "sets lborel = sigma_sets (space lborel) (range atMost)" 

888 
by (simp add: borel_eq_atMost) 

889 
show "Int_stable (range atMost :: real set set)" 

890 
by (auto simp: Int_stable_def) 

891 
have vimage_eq: "\<And>a. (X ` {..a} \<inter> space M) = {x\<in>space M. X x \<le> a}" by auto 

892 
def A \<equiv> "\<lambda>i::nat. {.. real i}" 

893 
then show "range A \<subseteq> range atMost" "(\<Union>i. A i) = space lborel" 

894 
"\<And>i. emeasure (distr M lborel X) (A i) \<noteq> \<infinity>" 

895 
by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq) 

896 

897 
fix A :: "real set" assume "A \<in> range atMost" 

898 
then obtain a where A: "A = {..a}" by auto 

899 
show "emeasure M (X ` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>lborel)" 

900 
unfolding vimage_eq A M_eq g_eq .. 

901 
qed auto 

902 

903 
lemma (in prob_space) uniform_distributed_params: 

904 
assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" 

905 
shows "A \<in> sets MX" "measure MX A \<noteq> 0" 

906 
proof  

907 
interpret X: prob_space "distr M MX X" 

908 
using distributed_measurable[OF X] by (rule prob_space_distr) 

909 

910 
show "measure MX A \<noteq> 0" 

911 
proof 

912 
assume "measure MX A = 0" 

913 
with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X] 

914 
show False 

915 
by (simp add: emeasure_density zero_ereal_def[symmetric]) 

916 
qed 

917 
with measure_notin_sets[of A MX] show "A \<in> sets MX" 

918 
by blast 

919 
qed 

920 

47694  921 
lemma prob_space_uniform_measure: 
922 
assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" 

923 
shows "prob_space (uniform_measure M A)" 

924 
proof 

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

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

927 
using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A 
47694  928 
by (simp add: Int_absorb2 emeasure_nonneg) 
929 
qed 

930 

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

932 
by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def) 

42860  933 

35582  934 
end 