author  hoelzl 
Wed, 10 Oct 2012 12:12:31 +0200  
changeset 49795  9f2fb9b25a77 
parent 49788  3c10763f5cb4 
child 50001  382bd3173584 
permissions  rwrr 
42148  1 
(* Title: HOL/Probability/Probability_Measure.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
Author: Armin Heller, TU München 

4 
*) 

5 

42148  6 
header {*Probability measure*} 
42067  7 

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

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

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

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

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

17 
proof safe 

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

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

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

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

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

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

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

25 
qed simp 

26 
qed 

27 
next 

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

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

30 
qed 

31 

32 
lemma extensional_funcset_insert_eq[simp]: 

33 
assumes "a \<notin> A" 

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

35 
apply (rule funset_eq_UN_fun_upd_I) 

36 
using assms 

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

38 

39 
lemma finite_extensional_funcset[simp, intro]: 

40 
assumes "finite A" "finite B" 

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

42 
using assms by induct auto 

43 

44 
lemma finite_PiE[simp, intro]: 

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

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

47 
proof  

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

49 
show ?thesis 

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

51 
qed 

52 

53 

54 
lemma countably_additiveI[case_names countably]: 

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

56 
shows "countably_additive M \<mu>" 

57 
using assms unfolding countably_additive_def by auto 

58 

59 
lemma convex_le_Inf_differential: 

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

61 
assumes "convex_on I f" 

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

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

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

65 
proof  

66 
show ?thesis 

67 
proof (cases rule: linorder_cases) 

68 
assume "x < y" 

69 
moreover 

70 
have "open (interior I)" by auto 

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

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

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

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

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

76 

77 
have "open (interior I)" by auto 

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

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

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

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

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

83 

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

85 
proof (rule Inf_lower2) 

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

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

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

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

90 
next 

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

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

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

94 
qed 

95 
then show ?thesis 

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

97 
next 

98 
assume "y < x" 

99 
moreover 

100 
have "open (interior I)" by auto 

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

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

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

104 
by (auto simp: dist_real_def field_simps) 

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

106 

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

108 
proof (rule Inf_greatest) 

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

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

111 
also 

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

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

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

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

116 
next 

117 
have "open (interior I)" by auto 

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

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

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

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

122 
qed 

123 
then show ?thesis 

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

125 
qed simp 

126 
qed 

127 

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

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

130 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

152 
proof (rule prob_spaceI) 

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

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

155 
by (auto simp: emeasure_distr emeasure_space_1) 

43339  156 
qed 
157 

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

160 

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

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

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

163 

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

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

166 

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

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

169 

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

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

43339  176 
qed (insert assms, auto) 
177 

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

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

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

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

185 
proof 

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

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

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

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

190 
by (simp add: emeasure_compl emeasure_space_1) 

191 
then show "prob A = 1" 

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

193 
next 

194 
assume prob: "prob A = 1" 

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

196 
proof (rule AE_I) 

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

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

199 
using `A \<in> events` prob 

200 
by (simp add: prob_compl emeasure_space_1 emeasure_eq_measure one_ereal_def) 

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

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

203 
qed 

204 
qed 

205 

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

207 
proof 

208 
assume "AE x in M. False" 

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

210 
then show False 

211 
by (subst (asm) AE_in_set_eq_1) auto 

212 
qed simp 

213 

214 
lemma (in prob_space) AE_prob_1: 

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

216 
proof  

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

218 
by (metis measure_notin_sets zero_neq_one) 

219 
with AE_in_set_eq_1 assms show ?thesis by simp 

220 
qed 

221 

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

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

49783  225 
lemma (in finite_measure) prob_zero_union: 
226 
assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0" 

227 
shows "measure M (s \<union> t) = measure M s" 

38656  228 
using assms 
35582  229 
proof  
49783  230 
have "measure M (s \<union> t) \<le> measure M s" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

236 

49783  237 
lemma (in finite_measure) prob_eq_compl: 
238 
assumes "s \<in> sets M" "t \<in> sets M" 

239 
assumes "measure M (space M  s) = measure M (space M  t)" 

240 
shows "measure M s = measure M t" 

241 
using assms finite_measure_compl by auto 

35582  242 

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

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

247 
proof  

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

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

251 
by blast 

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

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

35582  254 
qed 
255 

49783  256 
lemma (in finite_measure) prob_eq_bigunion_image: 
257 
assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M" 

35582  258 
assumes "disjoint_family f" "disjoint_family g" 
49783  259 
assumes "\<And> n :: nat. measure M (f n) = measure M (g n)" 
260 
shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)" 

35582  261 
using assms 
262 
proof  

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

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

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

49783  270 
lemma (in finite_measure) prob_countably_zero: 
271 
assumes "range c \<subseteq> sets M" 

272 
assumes "\<And> i. measure M (c i) = 0" 

273 
shows "measure M (\<Union> i :: nat. c i) = 0" 

38656  274 
proof (rule antisym) 
49783  275 
show "measure M (\<Union> i :: nat. c i) \<le> 0" 
47694  276 
using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2)) 
277 
qed (simp add: measure_nonneg) 

35582  278 

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

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

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

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

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

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

299 
assumes "finite s" 

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

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

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

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

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

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

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

313 
qed 

314 
finally show ?thesis . 

35582  315 
qed 
316 

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

49786  319 
assumes gt: "AE x in M. X x < b" 
43339  320 
shows "expectation X < b" 
321 
proof  

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

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

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

327 

328 
lemma (in prob_space) expectation_greater: 

329 
assumes [simp]: "integrable M X" 

49786  330 
assumes gt: "AE x in M. a < X x" 
43339  331 
shows "a < expectation X" 
332 
proof  

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

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

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

338 

339 
lemma (in prob_space) jensens_inequality: 

340 
fixes a b :: real 

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

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

345 
proof  

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

349 
from I have "open I" by auto 

350 

351 
note I 

352 
moreover 

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

354 
with X have "a < expectation X" 

355 
by (intro expectation_greater) auto } 

356 
moreover 

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

358 
with X have "expectation X < b" 

359 
by (intro expectation_less) auto } 

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

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

362 
moreover 

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

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

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

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

367 
by simp 

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

369 
proof (rule Sup_least) 

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

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

372 
next 

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

374 
then guess x .. note x = this 

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

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

49786  379 
apply (intro integral_mono_AE integral_add integral_cmult integral_diff 
380 
lebesgue_integral_const X q) 

381 
apply (elim eventually_elim1) 

382 
apply (intro convex_le_Inf_differential) 

383 
apply (auto simp: interior_open q) 

384 
done 

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

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

388 
qed 

389 

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

395 
shows "prob {y} = 0" 

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

397 

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

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

40859  402 

403 
lemma (in prob_space) joint_distribution_Times_le_snd: 

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

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

40859  407 

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

408 
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

409 

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

411 
proof 
47694  412 
show "emeasure (M1 \<Otimes>\<^isub>M M2) (space (M1 \<Otimes>\<^isub>M M2)) = 1" 
49776  413 
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

414 
qed 
40859  415 

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

417 
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

418 
assumes prob_space: "\<And>i. prob_space (M i)" 
42988  419 

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

420 
sublocale product_prob_space \<subseteq> M: prob_space "M i" for i 
42988  421 
by (rule prob_space) 
422 

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

423 
locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I 
42988  424 

425 
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

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

429 
qed 
42988  430 

431 
lemma (in finite_product_prob_space) prob_times: 

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

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

434 
proof  

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

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

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

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

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

443 

47694  444 
section {* Distributions *} 
42892  445 

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

36624  448 

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

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

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

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

454 
by (simp_all add: distributed_def) 

39097  455 

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

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

459 
by (simp_all add: distributed_def borel_measurable_ereal_iff) 

35977  460 

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

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

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

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

468 
using X by (simp add: distributed_distr_eq_density) 

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

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

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

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

473 
finally show ?thesis .. 

39092  474 
qed 
35977  475 

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

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

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

480 

481 
lemma subdensity: 

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

483 
assumes f: "distributed M P X f" 

484 
assumes g: "distributed M Q Y g" 

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

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

487 
proof  

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

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

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

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

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

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

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

495 
using T by (auto dest: measurable_space) 

496 
finally show ?thesis 

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

35977  498 
qed 
499 

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

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

503 
assumes f: "distributed M P X f" 

504 
assumes g: "distributed M Q Y g" 

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

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

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

508 

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

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

510 
"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)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

511 
by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

513 

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

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

515 
"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)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

516 
by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

517 
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

518 

47694  519 
lemma distributed_integral: 
520 
"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)" 

521 
by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable 

522 
distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr) 

523 

524 
lemma distributed_transform_integral: 

525 
assumes Px: "distributed M N X Px" 

526 
assumes "distributed M P Y Py" 

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

528 
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

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

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

533 
using Y by simp 

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

535 
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

536 
finally show ?thesis . 
39092  537 
qed 
36624  538 

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

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

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

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

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

544 
interpret X: prob_space "distr M S X" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

545 
using distributed_measurable[OF Px] by (rule prob_space_distr) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

547 
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

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

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

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

551 

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

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

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

554 
assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

555 
assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

556 
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

557 
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

558 
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

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

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

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

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

563 
interpret ST: pair_sigma_finite S T by default 
47694  564 

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

565 
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

566 
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

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

568 
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

569 
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

570 
show "?E \<subseteq> Pow (space ?P)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

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

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

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

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

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

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

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

579 
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

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

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

582 
fix E assume "E \<in> ?E" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

583 
then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

584 
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

585 
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

586 
also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

587 
by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

589 
also have "\<dots> = emeasure ?R E" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

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

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

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

594 
qed (auto intro!: measurable_Pair) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

595 

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

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

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

598 
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

599 
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

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

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

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

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

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

605 

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

606 
note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]] 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

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

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

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

611 
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

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

613 
by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

615 
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

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

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

618 
simp: measurable_split_conv split_beta 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

620 
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))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

621 
using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst] 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

622 
using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd] 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

624 
{ 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

625 
let ?B = "(\<lambda>(x, y). (y, x)) ` A \<inter> space (S \<Otimes>\<^isub>M T)" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

626 
from sets_into_space[OF A] 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

627 
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

628 
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

629 
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

630 
also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

631 
using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

632 
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

633 
(\<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

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

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

636 
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

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

638 
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

639 
apply (subst positive_integral_distr) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

640 
apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

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

642 
qed 
36624  643 
qed 
644 

47694  645 
lemma (in prob_space) distr_marginal1: 
646 
assumes "sigma_finite_measure S" "sigma_finite_measure T" 

647 
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

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

651 
proof safe 

652 
interpret S: sigma_finite_measure S by fact 

653 
interpret T: sigma_finite_measure T by fact 

654 
interpret ST: pair_sigma_finite S T by default 

655 

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

657 
using Pxy by (rule distributed_measurable) 

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

659 
unfolding measurable_pair_iff by (simp add: comp_def) 

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

661 
unfolding measurable_pair_iff by (simp add: comp_def) 

662 

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

663 
from Pxy show borel: "Px \<in> borel_measurable S" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

664 
by (auto intro!: ST.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def) 
39097  665 

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

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

668 
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  669 
using Pxy 
49788
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

670 
by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

671 

47694  672 
show "distr M S X = density S Px" 
673 
proof (rule measure_eqI) 

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

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

676 
by (auto simp add: emeasure_distr 

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

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

679 
using Pxy by (simp add: distributed_def) 

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

680 
also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S" 
47694  681 
using A borel Pxy 
682 
by (simp add: emeasure_density ST.positive_integral_fst_measurable(2)[symmetric] distributed_def) 

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

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

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

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

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

690 
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" 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

691 
using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong) 
3c10763f5cb4
show and use distributed_swap and distributed_jointI
hoelzl
parents:
49786
diff
changeset

692 
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

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

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

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

698 
qed simp 

699 

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

700 
show "AE x in S. 0 \<le> Px x" 
47694  701 
by (simp add: Px_def positive_integral_positive real_of_ereal_pos) 
40859  702 
qed 
703 

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

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

705 
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

706 
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

707 
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

708 
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

709 

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

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

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

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

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

714 
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

715 
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

716 
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

717 

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

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

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

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

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

722 
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

723 
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

724 
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

725 

49795  726 
lemma (in prob_space) distributed_joint_indep': 
727 
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 

728 
assumes X: "distributed M S X Px" and Y: "distributed M T Y Py" 

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

730 
shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" 

731 
unfolding distributed_def 

732 
proof safe 

733 
interpret S: sigma_finite_measure S by fact 

734 
interpret T: sigma_finite_measure T by fact 

735 
interpret ST: pair_sigma_finite S T by default 

736 

737 
interpret X: prob_space "density S Px" 

738 
unfolding distributed_distr_eq_density[OF X, symmetric] 

739 
using distributed_measurable[OF X] 

740 
by (rule prob_space_distr) 

741 
have sf_X: "sigma_finite_measure (density S Px)" .. 

742 

743 
interpret Y: prob_space "density T Py" 

744 
unfolding distributed_distr_eq_density[OF Y, symmetric] 

745 
using distributed_measurable[OF Y] 

746 
by (rule prob_space_distr) 

747 
have sf_Y: "sigma_finite_measure (density T Py)" .. 

748 

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

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

751 
using distributed_borel_measurable[OF X] distributed_AE[OF X] 

752 
using distributed_borel_measurable[OF Y] distributed_AE[OF Y] 

753 
by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y]) 

754 

755 
show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 

756 
using distributed_measurable[OF X] distributed_measurable[OF Y] 

757 
by (auto intro: measurable_Pair) 

758 

759 
show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" 

760 
by (auto simp: split_beta' 

761 
intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]] 

762 
measurable_compose[OF _ distributed_borel_measurable[OF Y]]) 

763 

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

765 
apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const) 

766 
using distributed_AE[OF X] 

767 
apply eventually_elim 

768 
using distributed_AE[OF Y] 

769 
apply eventually_elim 

770 
apply auto 

771 
done 

772 
qed 

773 

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

776 
finite (X`space M)" 

42902  777 

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

780 
unfolding simple_distributed_def by auto 

42902  781 

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

42902  784 

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

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

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

789 
shows "distributed M S X P'" 

790 
unfolding distributed_def 

791 
proof safe 

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

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

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

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

796 
proof (rule measure_eqI_finite) 

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

798 
using A unfolding S_def by auto 

799 
show "finite A" by fact 

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

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

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

803 
by (subst emeasure_distr) 

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

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

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

807 
using A X a 

808 
by (subst positive_integral_cmult_indicator) 

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

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

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

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

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

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

815 
qed 

816 
show "random_variable S X" 

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

818 
qed 

42902  819 

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

822 
shows "simple_distributed M X P" 

823 
unfolding simple_distributed_def 

824 
proof 

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

826 
(is "?A") 

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

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

829 
by (rule distributed_cong_density) auto 

830 
finally show "\<dots>" . 

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

832 

833 
lemma simple_distributed_joint_finite: 

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

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

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

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

840 
by auto 

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

842 
by (auto simp: image_image) 

843 
qed 

844 

845 
lemma simple_distributed_joint2_finite: 

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

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

848 
proof  

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

850 
using X by (auto simp: simple_distributed_def simple_functionD) 

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

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

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

854 
by auto 

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

856 
by (auto simp: image_image) 

42902  857 
qed 
858 

47694  859 
lemma simple_distributed_simple_function: 
860 
"simple_distributed M X Px \<Longrightarrow> simple_function M X" 

861 
unfolding simple_distributed_def distributed_def 

862 
by (auto simp: simple_function_def) 

863 

864 
lemma simple_distributed_measure: 

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

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

867 
by (auto simp: simple_distributed_def measure_def) 

868 

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

870 
by (auto simp: simple_distributed_measure measure_nonneg) 

42860  871 

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

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

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

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

877 
proof  

878 
from simple_distributed_joint_finite[OF X, simp] 

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

880 
by (simp add: S_def pair_measure_count_space) 

881 
show ?thesis 

882 
unfolding S_eq P_def 

883 
proof (rule distributed_simple_function_superset) 

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

885 
using X by (rule simple_distributed_simple_function) 

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

887 
from simple_distributed_measure[OF X this] 

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

889 
qed auto 

890 
qed 

42860  891 

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

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

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

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

897 
proof  

898 
from simple_distributed_joint2_finite[OF X, simp] 

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

900 
by (simp add: S_def pair_measure_count_space) 

901 
show ?thesis 

902 
unfolding S_eq P_def 

903 
proof (rule distributed_simple_function_superset) 

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

905 
using X by (rule simple_distributed_simple_function) 

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

907 
from simple_distributed_measure[OF X this] 

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

909 
qed auto 

910 
qed 

911 

912 
lemma (in prob_space) simple_distributed_setsum_space: 

913 
assumes X: "simple_distributed M X f" 

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

915 
proof  

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

917 
by (subst finite_measure_finite_Union) 

918 
(auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD 

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

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

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

922 
finally show ?thesis 

923 
using emeasure_space_1 by (simp add: emeasure_eq_measure one_ereal_def) 

924 
qed 

42860  925 

47694  926 
lemma (in prob_space) distributed_marginal_eq_joint_simple: 
927 
assumes Px: "simple_function M X" 

928 
assumes Py: "simple_distributed M Y Py" 

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

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

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

932 
proof  

933 
note Px = simple_distributedI[OF Px refl] 

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

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

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

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

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

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

939 
simple_distributed[OF Py] simple_distributed_joint[OF Pxy], 
47694  940 
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

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

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

943 
Py[THEN simple_distributed_finite] 
47694  944 
Pxy[THEN simple_distributed, THEN distributed_real_AE] 
945 
show ?thesis 

946 
unfolding AE_count_space 

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

948 
done 

949 
qed 

42860  950 

47694  951 
lemma prob_space_uniform_measure: 
952 
assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" 

953 
shows "prob_space (uniform_measure M A)" 

954 
proof 

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

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

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

958 
by (simp add: Int_absorb2 emeasure_nonneg) 

959 
qed 

960 

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

962 
by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def) 

42860  963 

35582  964 
end 