author  wenzelm 
Wed, 08 Apr 2015 21:49:45 +0200  
changeset 59978  c2dc7856e2e5 
parent 59778  fe5b796d6b2a 
child 60067  f1a5bcf5658f 
permissions  rwrr 
58606  1 
(* Title: HOL/Probability/Giry_Monad.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Manuel Eberl, TU München 

4 

5 
Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability 

6 
spaces. 

7 
*) 

8 

9 
theory Giry_Monad 

59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

10 
imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" 
58606  11 
begin 
12 

13 
section {* Subprobability spaces *} 

14 

15 
locale subprob_space = finite_measure + 

16 
assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1" 

17 
assumes subprob_not_empty: "space M \<noteq> {}" 

18 

19 
lemma subprob_spaceI[Pure.intro!]: 

20 
assumes *: "emeasure M (space M) \<le> 1" 

21 
assumes "space M \<noteq> {}" 

22 
shows "subprob_space M" 

23 
proof  

24 
interpret finite_measure M 

25 
proof 

26 
show "emeasure M (space M) \<noteq> \<infinity>" using * by auto 

27 
qed 

28 
show "subprob_space M" by default fact+ 

29 
qed 

30 

31 
lemma prob_space_imp_subprob_space: 

32 
"prob_space M \<Longrightarrow> subprob_space M" 

33 
by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty) 

34 

59425  35 
lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M" 
36 
unfolding subprob_space_def finite_measure_def by simp 

37 

58606  38 
sublocale prob_space \<subseteq> subprob_space 
39 
by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) 

40 

41 
lemma (in subprob_space) subprob_space_distr: 

42 
assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)" 

43 
proof (rule subprob_spaceI) 

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

45 
with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1" 

46 
by (auto simp: emeasure_distr emeasure_space_le_1) 

47 
show "space (distr M M' f) \<noteq> {}" by (simp add: assms) 

48 
qed 

49 

59000  50 
lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1" 
58606  51 
by (rule order.trans[OF emeasure_space emeasure_space_le_1]) 
52 

59000  53 
lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1" 
54 
using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure) 

55 

59427  56 
lemma (in subprob_space) nn_integral_le_const: 
57 
assumes "0 \<le> c" "AE x in M. f x \<le> c" 

58 
shows "(\<integral>\<^sup>+x. f x \<partial>M) \<le> c" 

59 
proof  

60 
have "(\<integral>\<^sup>+ x. f x \<partial>M) \<le> (\<integral>\<^sup>+ x. c \<partial>M)" 

61 
by(rule nn_integral_mono_AE) fact 

62 
also have "\<dots> \<le> c * emeasure M (space M)" 

63 
using \<open>0 \<le> c\<close> by(simp add: nn_integral_const_If) 

64 
also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule ereal_mult_left_mono) 

65 
finally show ?thesis by simp 

66 
qed 

67 

59092
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

68 
lemma emeasure_density_distr_interval: 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

69 
fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

70 
assumes [simp]: "a \<le> b" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

71 
assumes Mf[measurable]: "f \<in> borel_measurable borel" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

72 
assumes Mg[measurable]: "g \<in> borel_measurable borel" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

73 
assumes Mg'[measurable]: "g' \<in> borel_measurable borel" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

74 
assumes Mh[measurable]: "h \<in> borel_measurable borel" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

75 
assumes prob: "subprob_space (density lborel f)" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

76 
assumes nonnegf: "\<And>x. f x \<ge> 0" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

77 
assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

78 
assumes contg': "continuous_on {a..b} g'" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

79 
assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

80 
assumes range: "{a..b} \<subseteq> range h" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

81 
shows "emeasure (distr (density lborel f) lborel h) {a..b} = 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

82 
emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

83 
proof (cases "a < b") 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

84 
assume "a < b" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

85 
from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

86 
from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

87 
from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

88 
by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

89 
from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

90 
by (rule continuous_ge_on_Iii) (simp_all add: `a < b`) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

91 

d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

92 
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

93 
have A: "h ` {a..b} = {g a..g b}" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

94 
proof (intro equalityI subsetI) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

95 
fix x assume x: "x \<in> h ` {a..b}" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

96 
hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono']) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

97 
with inv and x show "x \<in> {g a..g b}" by simp 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

98 
next 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

99 
fix y assume y: "y \<in> {g a..g b}" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

100 
with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

101 
with range and inv show "y \<in> h ` {a..b}" by auto 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

102 
qed 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

103 

d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

104 
have prob': "subprob_space (distr (density lborel f) lborel h)" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

105 
by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

106 
have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

107 
\<integral>\<^sup>+x. f x * indicator (h ` {a..b}) x \<partial>lborel" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

108 
by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh]) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

109 
also note A 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

110 
also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

111 
by (rule subprob_space.subprob_emeasure_le_1) (rule prob') 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

112 
hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by auto 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

113 
with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

114 
(\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

115 
by (intro nn_integral_substitution_aux) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

116 
(auto simp: derivg_nonneg A B emeasure_density mult.commute `a < b`) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

117 
also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

118 
by (simp add: emeasure_density) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

119 
finally show ?thesis . 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

120 
next 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

121 
assume "\<not>a < b" 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

122 
with `a \<le> b` have [simp]: "b = a" by (simp add: not_less del: `a \<le> b`) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

123 
from inv and range have "h ` {a} = {g a}" by auto 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

124 
thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh]) 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

125 
qed 
d469103c0737
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents:
59048
diff
changeset

126 

58606  127 
locale pair_subprob_space = 
128 
pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2 

129 

130 
sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2" 

131 
proof 

132 
have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)" 

59559
35da1bbf234e
more canonical order of subscriptions avoids superfluous facts
haftmann
parents:
59525
diff
changeset

133 
by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono) 
58606  134 
from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1] 
135 
show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1" 

136 
by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg) 

137 
from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}" 

138 
by (simp add: space_pair_measure) 

139 
qed 

140 

59425  141 
lemma subprob_space_null_measure_iff: 
142 
"subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}" 

143 
by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty) 

144 

59525  145 
lemma subprob_space_restrict_space: 
146 
assumes M: "subprob_space M" 

147 
and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}" 

148 
shows "subprob_space (restrict_space M A)" 

149 
proof(rule subprob_spaceI) 

150 
have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)" 

151 
using A by(simp add: emeasure_restrict_space space_restrict_space) 

152 
also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M) 

153 
finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" . 

154 
next 

155 
show "space (restrict_space M A) \<noteq> {}" 

156 
using A by(simp add: space_restrict_space) 

157 
qed 

158 

58606  159 
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where 
160 
"subprob_algebra K = 

161 
(\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)" 

162 

163 
lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}" 

164 
by (auto simp add: subprob_algebra_def space_Sup_sigma) 

165 

166 
lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N" 

167 
by (simp add: subprob_algebra_def) 

168 

169 
lemma measurable_emeasure_subprob_algebra[measurable]: 

170 
"a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)" 

171 
by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def) 

172 

59000  173 
lemma subprob_measurableD: 
174 
assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M" 

175 
shows "space (N x) = space S" 

176 
and "sets (N x) = sets S" 

177 
and "measurable (N x) K = measurable S K" 

178 
and "measurable K (N x) = measurable K S" 

179 
using measurable_space[OF N x] 

180 
by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq) 

181 

59048  182 
ML {* 
183 

184 
fun subprob_cong thm ctxt = ( 

185 
let 

186 
val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm 

59582  187 
val free = thm' > Thm.concl_of > HOLogic.dest_Trueprop > dest_comb > fst > 
59048  188 
dest_comb > snd > strip_abs_body > head_of > is_Free 
189 
in 

190 
if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt) 

191 
else ([], ctxt) 

192 
end 

193 
handle THM _ => ([], ctxt)  TERM _ => ([], ctxt)) 

194 

195 
*} 

196 

197 
setup \<open> 

198 
Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong) 

199 
\<close> 

200 

58606  201 
context 
202 
fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)" 

203 
begin 

204 

205 
lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)" 

206 
using measurable_space[OF K] by (simp add: space_subprob_algebra) 

207 

208 
lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N" 

209 
using measurable_space[OF K] by (simp add: space_subprob_algebra) 

210 

211 
lemma measurable_emeasure_kernel[measurable]: 

212 
"A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M" 

213 
using measurable_compose[OF K measurable_emeasure_subprob_algebra] . 

214 

215 
end 

216 

217 
lemma measurable_subprob_algebra: 

218 
"(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow> 

219 
(\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow> 

220 
(\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow> 

221 
K \<in> measurable M (subprob_algebra N)" 

222 
by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def) 

223 

59778  224 
lemma measurable_submarkov: 
225 
"K \<in> measurable M (subprob_algebra M) \<longleftrightarrow> 

226 
(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 

227 
(\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)" 

228 
proof 

229 
assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 

230 
(\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)" 

231 
then show "K \<in> measurable M (subprob_algebra M)" 

232 
by (intro measurable_subprob_algebra) auto 

233 
next 

234 
assume "K \<in> measurable M (subprob_algebra M)" 

235 
then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 

236 
(\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)" 

237 
by (auto dest: subprob_space_kernel sets_kernel) 

238 
qed 

239 

58606  240 
lemma space_subprob_algebra_empty_iff: 
241 
"space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}" 

242 
proof 

243 
have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)" 

244 
by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI) 

245 
then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}" 

246 
by auto 

247 
next 

248 
assume "space N = {}" 

249 
hence "sets N = {{}}" by (simp add: space_empty_iff) 

250 
moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}" 

251 
by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric]) 

252 
ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra) 

253 
qed 

254 

59048  255 
lemma nn_integral_measurable_subprob_algebra': 
59000  256 
assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" 
257 
shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B") 

258 
using f 

259 
proof induct 

260 
case (cong f g) 

261 
moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B" 

262 
by (intro measurable_cong nn_integral_cong cong) 

263 
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 

264 
ultimately show ?case by simp 

265 
next 

266 
case (set B) 

267 
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B" 

268 
by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra) 

269 
ultimately show ?case 

270 
by (simp add: measurable_emeasure_subprob_algebra) 

271 
next 

272 
case (mult f c) 

273 
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B" 

59048  274 
by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 
59000  275 
ultimately show ?case 
59048  276 
using [[simp_trace_new]] 
59000  277 
by simp 
278 
next 

279 
case (add f g) 

280 
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B" 

59048  281 
by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) 
59000  282 
ultimately show ?case 
283 
by (simp add: ac_simps) 

284 
next 

285 
case (seq F) 

286 
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B" 

287 
unfolding SUP_apply 

59048  288 
by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) 
59000  289 
ultimately show ?case 
290 
by (simp add: ac_simps) 

291 
qed 

292 

59048  293 
lemma nn_integral_measurable_subprob_algebra: 
294 
"f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" 

295 
by (subst nn_integral_max_0[symmetric]) 

296 
(auto intro!: nn_integral_measurable_subprob_algebra') 

297 

58606  298 
lemma measurable_distr: 
299 
assumes [measurable]: "f \<in> measurable M N" 

300 
shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" 

301 
proof (cases "space N = {}") 

302 
assume not_empty: "space N \<noteq> {}" 

303 
show ?thesis 

304 
proof (rule measurable_subprob_algebra) 

305 
fix A assume A: "A \<in> sets N" 

306 
then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow> 

307 
(\<lambda>M'. emeasure M' (f ` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)" 

308 
by (intro measurable_cong) 

59048  309 
(auto simp: emeasure_distr space_subprob_algebra 
310 
intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"]) 

58606  311 
also have "\<dots>" 
312 
using A by (intro measurable_emeasure_subprob_algebra) simp 

313 
finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" . 

59048  314 
qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets) 
58606  315 
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) 
316 

59000  317 
lemma emeasure_space_subprob_algebra[measurable]: 
318 
"(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)" 

319 
proof 

320 
have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M") 

321 
by (rule measurable_emeasure_subprob_algebra) simp 

322 
also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M" 

323 
by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) 

324 
finally show ?thesis . 

325 
qed 

326 

59978  327 
(* TODO: Rename. This name is too general  Manuel *) 
59000  328 
lemma measurable_pair_measure: 
329 
assumes f: "f \<in> measurable M (subprob_algebra N)" 

330 
assumes g: "g \<in> measurable M (subprob_algebra L)" 

331 
shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))" 

332 
proof (rule measurable_subprob_algebra) 

333 
{ fix x assume "x \<in> space M" 

334 
with measurable_space[OF f] measurable_space[OF g] 

335 
have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)" 

336 
by auto 

337 
interpret F: subprob_space "f x" 

338 
using fx by (simp add: space_subprob_algebra) 

339 
interpret G: subprob_space "g x" 

340 
using gx by (simp add: space_subprob_algebra) 

341 

342 
interpret pair_subprob_space "f x" "g x" .. 

343 
show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales 

344 
show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)" 

345 
using fx gx by (simp add: space_subprob_algebra) 

346 

347 
have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B" 

348 
using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 

349 
have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 

350 
emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))" 

351 
by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure) 

352 
hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L  A) = 

353 
...  emeasure (f x \<Otimes>\<^sub>M g x) A" 

354 
using emeasure_compl[OF _ P.emeasure_finite] 

355 
unfolding sets_eq 

356 
unfolding sets_eq_imp_space_eq[OF sets_eq] 

357 
by (simp add: space_pair_measure G.emeasure_pair_measure_Times) 

358 
note 1 2 sets_eq } 

359 
note Times = this(1) and Compl = this(2) and sets_eq = this(3) 

360 

361 
fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)" 

362 
show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M" 

363 
using Int_stable_pair_measure_generator pair_measure_closed A 

364 
unfolding sets_pair_measure 

365 
proof (induct A rule: sigma_sets_induct_disjoint) 

366 
case (basic A) then show ?case 

367 
by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong) 

368 
(auto intro!: measurable_emeasure_kernel f g) 

369 
next 

370 
case (compl A) 

371 
then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)" 

372 
by (auto simp: sets_pair_measure) 

373 
have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))  

374 
emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M") 

375 
using compl(2) f g by measurable 

376 
thus ?case by (simp add: Compl A cong: measurable_cong) 

377 
next 

378 
case (union A) 

379 
then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A" 

380 
by (auto simp: sets_pair_measure) 

381 
then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow> 

382 
(\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M" 

383 
by (intro measurable_cong suminf_emeasure[symmetric]) 

384 
(auto simp: sets_eq) 

385 
also have "\<dots>" 

386 
using union by auto 

387 
finally show ?case . 

388 
qed simp 

389 
qed 

390 

391 
lemma restrict_space_measurable: 

392 
assumes X: "X \<noteq> {}" "X \<in> sets K" 

393 
assumes N: "N \<in> measurable M (subprob_algebra K)" 

394 
shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))" 

395 
proof (rule measurable_subprob_algebra) 

396 
fix a assume a: "a \<in> space M" 

397 
from N[THEN measurable_space, OF this] 

398 
have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K" 

399 
by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 

400 
then interpret subprob_space "N a" 

401 
by simp 

402 
show "subprob_space (restrict_space (N a) X)" 

403 
proof 

404 
show "space (restrict_space (N a) X) \<noteq> {}" 

405 
using X by (auto simp add: space_restrict_space) 

406 
show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1" 

407 
using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1) 

408 
qed 

409 
show "sets (restrict_space (N a) X) = sets (restrict_space K X)" 

410 
by (intro sets_restrict_space_cong) fact 

411 
next 

412 
fix A assume A: "A \<in> sets (restrict_space K X)" 

413 
show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M" 

414 
proof (subst measurable_cong) 

415 
fix a assume "a \<in> space M" 

416 
from N[THEN measurable_space, OF this] 

417 
have [simp]: "sets (N a) = sets K" "space (N a) = space K" 

418 
by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 

419 
show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)" 

420 
using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps) 

421 
next 

422 
show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M" 

423 
using A X 

424 
by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra]) 

425 
(auto simp: sets_restrict_space) 

426 
qed 

427 
qed 

428 

58606  429 
section {* Properties of return *} 
430 

431 
definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where 

432 
"return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)" 

433 

434 
lemma space_return[simp]: "space (return M x) = space M" 

435 
by (simp add: return_def) 

436 

437 
lemma sets_return[simp]: "sets (return M x) = sets M" 

438 
by (simp add: return_def) 

439 

440 
lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L" 

441 
by (simp cong: measurable_cong_sets) 

442 

443 
lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N" 

444 
by (simp cong: measurable_cong_sets) 

445 

59000  446 
lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N" 
447 
by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def) 

448 

449 
lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x" 

450 
by (auto simp add: return_def dest: sets_eq_imp_space_eq) 

451 

58606  452 
lemma emeasure_return[simp]: 
453 
assumes "A \<in> sets M" 

454 
shows "emeasure (return M x) A = indicator A x" 

455 
proof (rule emeasure_measure_of[OF return_def]) 

456 
show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed) 

457 
show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def) 

458 
from assms show "A \<in> sets (return M x)" unfolding return_def by simp 

459 
show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)" 

460 
by (auto intro: countably_additiveI simp: suminf_indicator) 

461 
qed 

462 

463 
lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)" 

464 
by rule simp 

465 

466 
lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)" 

467 
by (intro prob_space_return prob_space_imp_subprob_space) 

468 

59000  469 
lemma subprob_space_return_ne: 
470 
assumes "space M \<noteq> {}" shows "subprob_space (return M x)" 

471 
proof 

472 
show "emeasure (return M x) (space (return M x)) \<le> 1" 

473 
by (subst emeasure_return) (auto split: split_indicator) 

474 
qed (simp, fact) 

475 

476 
lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x" 

477 
unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator) 

478 

58606  479 
lemma AE_return: 
480 
assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P" 

481 
shows "(AE y in return M x. P y) \<longleftrightarrow> P x" 

482 
proof  

483 
have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x" 

484 
by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator) 

485 
also have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> (AE y in return M x. P y)" 

486 
by (rule AE_cong) auto 

487 
finally show ?thesis . 

488 
qed 

489 

490 
lemma nn_integral_return: 

491 
assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M" 

492 
shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x" 

493 
proof 

494 
interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`]) 

495 
have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms 

496 
by (intro nn_integral_cong_AE) (auto simp: AE_return) 

497 
also have "... = g x" 

498 
using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp 

499 
finally show ?thesis . 

500 
qed 

501 

59000  502 
lemma integral_return: 
503 
fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" 

504 
assumes "x \<in> space M" "g \<in> borel_measurable M" 

505 
shows "(\<integral>a. g a \<partial>return M x) = g x" 

506 
proof 

507 
interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`]) 

508 
have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms 

509 
by (intro integral_cong_AE) (auto simp: AE_return) 

510 
then show ?thesis 

511 
using prob_space by simp 

512 
qed 

513 

514 
lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)" 

58606  515 
by (rule measurable_subprob_algebra) (auto simp: subprob_space_return) 
516 

517 
lemma distr_return: 

518 
assumes "f \<in> measurable M N" and "x \<in> space M" 

519 
shows "distr (return M x) N f = return N (f x)" 

520 
using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr) 

521 

59000  522 
lemma return_restrict_space: 
523 
"\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>" 

524 
by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space) 

525 

526 
lemma measurable_distr2: 

527 
assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N" 

528 
assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)" 

529 
shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)" 

530 
proof  

531 
have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N) 

532 
\<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)" 

533 
proof (rule measurable_cong) 

534 
fix x assume x: "x \<in> space L" 

535 
have gx: "g x \<in> space (subprob_algebra M)" 

536 
using measurable_space[OF g x] . 

537 
then have [simp]: "sets (g x) = sets M" 

538 
by (simp add: space_subprob_algebra) 

539 
then have [simp]: "space (g x) = space M" 

540 
by (rule sets_eq_imp_space_eq) 

541 
let ?R = "return L x" 

542 
from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N" 

543 
by simp 

544 
interpret subprob_space "g x" 

545 
using gx by (simp add: space_subprob_algebra) 

546 
have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)" 

547 
by (simp add: space_pair_measure) 

548 
show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r") 

549 
proof (rule measure_eqI) 

550 
show "sets ?l = sets ?r" 

551 
by simp 

552 
next 

553 
fix A assume "A \<in> sets ?l" 

554 
then have A[measurable]: "A \<in> sets N" 

555 
by simp 

556 
then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) ` A \<inter> space (?R \<Otimes>\<^sub>M g x))" 

557 
by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets) 

558 
also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' ` A \<inter> space M) \<partial>?R)" 

559 
apply (subst emeasure_pair_measure_alt) 

560 
apply (rule measurable_sets[OF _ A]) 

561 
apply (auto simp add: f_M' cong: measurable_cong_sets) 

562 
apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"]) 

563 
apply (auto simp: space_subprob_algebra space_pair_measure) 

564 
done 

565 
also have "\<dots> = emeasure (g x) (f x ` A \<inter> space M)" 

566 
by (subst nn_integral_return) 

567 
(auto simp: x intro!: measurable_emeasure) 

568 
also have "\<dots> = emeasure ?l A" 

569 
by (simp add: emeasure_distr f_M' cong: measurable_cong_sets) 

570 
finally show "emeasure ?l A = emeasure ?r A" .. 

571 
qed 

572 
qed 

573 
also have "\<dots>" 

574 
apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) 

575 
apply (rule return_measurable) 

576 
apply measurable 

577 
done 

578 
finally show ?thesis . 

579 
qed 

580 

581 
lemma nn_integral_measurable_subprob_algebra2: 

59048  582 
assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" 
59000  583 
assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)" 
584 
shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" 

585 
proof  

59048  586 
note nn_integral_measurable_subprob_algebra[measurable] 
587 
note measurable_distr2[measurable] 

59000  588 
have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M" 
59048  589 
by measurable 
59000  590 
then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" 
59048  591 
by (rule measurable_cong[THEN iffD1, rotated]) 
592 
(simp add: nn_integral_distr) 

59000  593 
qed 
594 

595 
lemma emeasure_measurable_subprob_algebra2: 

596 
assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" 

597 
assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" 

598 
shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" 

599 
proof  

600 
{ fix x assume "x \<in> space M" 

601 
then have "Pair x ` Sigma (space M) A = A x" 

602 
by auto 

603 
with sets_Pair1[OF A, of x] have "A x \<in> sets N" 

604 
by auto } 

605 
note ** = this 

606 

607 
have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)" 

608 
by (auto simp: fun_eq_iff) 

609 
have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" 

610 
apply measurable 

611 
apply (subst measurable_cong) 

612 
apply (rule *) 

613 
apply (auto simp: space_pair_measure) 

614 
done 

615 
then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M" 

616 
by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L) 

617 
then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" 

618 
apply (rule measurable_cong[THEN iffD1, rotated]) 

619 
apply (rule nn_integral_indicator) 

620 
apply (simp add: subprob_measurableD[OF L] **) 

621 
done 

622 
qed 

623 

624 
lemma measure_measurable_subprob_algebra2: 

625 
assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" 

626 
assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" 

627 
shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M" 

628 
unfolding measure_def 

629 
by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms]) 

630 

58606  631 
definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))" 
632 

633 
lemma select_sets1: 

634 
"sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))" 

635 
unfolding select_sets_def by (rule someI) 

636 

637 
lemma sets_select_sets[simp]: 

638 
assumes sets: "sets M = sets (subprob_algebra N)" 

639 
shows "sets (select_sets M) = sets N" 

640 
unfolding select_sets_def 

641 
proof (rule someI2) 

642 
show "sets M = sets (subprob_algebra N)" 

643 
by fact 

644 
next 

645 
fix L assume "sets M = sets (subprob_algebra L)" 

646 
with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)" 

647 
by (intro sets_eq_imp_space_eq) simp 

648 
show "sets L = sets N" 

649 
proof cases 

650 
assume "space (subprob_algebra N) = {}" 

651 
with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L] 

652 
show ?thesis 

653 
by (simp add: eq space_empty_iff) 

654 
next 

655 
assume "space (subprob_algebra N) \<noteq> {}" 

656 
with eq show ?thesis 

657 
by (fastforce simp add: space_subprob_algebra) 

658 
qed 

659 
qed 

660 

661 
lemma space_select_sets[simp]: 

662 
"sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N" 

663 
by (intro sets_eq_imp_space_eq sets_select_sets) 

664 

665 
section {* Join *} 

666 

667 
definition join :: "'a measure measure \<Rightarrow> 'a measure" where 

668 
"join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" 

669 

670 
lemma 

671 
shows space_join[simp]: "space (join M) = space (select_sets M)" 

672 
and sets_join[simp]: "sets (join M) = sets (select_sets M)" 

673 
by (simp_all add: join_def) 

674 

675 
lemma emeasure_join: 

59048  676 
assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N" 
58606  677 
shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
678 
proof (rule emeasure_measure_of[OF join_def]) 

679 
show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" 

680 
proof (rule countably_additiveI) 

681 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A" 

682 
have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)" 

59048  683 
using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra) 
58606  684 
also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" 
685 
proof (rule nn_integral_cong) 

686 
fix M' assume "M' \<in> space M" 

687 
then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)" 

688 
using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra) 

689 
qed 

690 
finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" . 

691 
qed 

692 
qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg) 

693 

694 
lemma measurable_join: 

695 
"join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)" 

696 
proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra) 

697 
fix A assume "A \<in> sets N" 

698 
let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))" 

699 
have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B" 

700 
proof (rule measurable_cong) 

701 
fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))" 

702 
then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')" 

703 
by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`) 

704 
qed 

705 
also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B" 

59048  706 
using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] 
58606  707 
by (rule nn_integral_measurable_subprob_algebra) 
708 
finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" . 

709 
next 

710 
assume [simp]: "space N \<noteq> {}" 

711 
fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))" 

712 
then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)" 

713 
apply (intro nn_integral_mono) 

714 
apply (auto simp: space_subprob_algebra 

715 
dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) 

716 
done 

717 
with M show "subprob_space (join M)" 

718 
by (intro subprob_spaceI) 

719 
(auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1) 

720 
next 

721 
assume "\<not>(space N \<noteq> {})" 

722 
thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff) 

723 
qed (auto simp: space_subprob_algebra) 

724 

59048  725 
lemma nn_integral_join': 
726 
assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" 

727 
and M[measurable_cong]: "sets M = sets (subprob_algebra N)" 

58606  728 
shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)" 
729 
using f 

730 
proof induct 

731 
case (cong f g) 

732 
moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g" 

733 
by (intro nn_integral_cong cong) (simp add: M) 

734 
moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)" 

735 
by (intro nn_integral_cong cong) 

736 
(auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) 

737 
ultimately show ?case 

738 
by simp 

739 
next 

740 
case (set A) 

741 
moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 

742 
by (intro nn_integral_cong nn_integral_indicator) 

743 
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 

744 
ultimately show ?case 

745 
using M by (simp add: emeasure_join) 

746 
next 

747 
case (mult f c) 

748 
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 

59048  749 
using mult M M[THEN sets_eq_imp_space_eq] 
750 
by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 

58606  751 
also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 
59048  752 
using nn_integral_measurable_subprob_algebra[OF mult(3)] 
58606  753 
by (intro nn_integral_cmult mult) (simp add: M) 
754 
also have "\<dots> = c * (integral\<^sup>N (join M) f)" 

755 
by (simp add: mult) 

756 
also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)" 

59048  757 
using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets) 
58606  758 
finally show ?case by simp 
759 
next 

760 
case (add f g) 

761 
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)" 

59048  762 
using add M M[THEN sets_eq_imp_space_eq] 
763 
by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra) 

58606  764 
also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)" 
59048  765 
using nn_integral_measurable_subprob_algebra[OF add(1)] 
766 
using nn_integral_measurable_subprob_algebra[OF add(5)] 

58606  767 
by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg) 
768 
also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)" 

769 
by (simp add: add) 

770 
also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)" 

59048  771 
using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets) 
58606  772 
finally show ?case by (simp add: ac_simps) 
773 
next 

774 
case (seq F) 

775 
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)" 

59048  776 
using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply 
58606  777 
by (intro nn_integral_cong nn_integral_monotone_convergence_SUP) 
59048  778 
(auto simp add: space_subprob_algebra) 
58606  779 
also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)" 
59048  780 
using nn_integral_measurable_subprob_algebra[OF seq(1)] seq 
58606  781 
by (intro nn_integral_monotone_convergence_SUP) 
782 
(simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono ) 

783 
also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))" 

784 
by (simp add: seq) 

785 
also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)" 

59048  786 
using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) 
787 
(simp_all add: M cong: measurable_cong_sets) 

58606  788 
finally show ?case by (simp add: ac_simps) 
789 
qed 

790 

59048  791 
lemma nn_integral_join: 
792 
assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)" 

793 
shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)" 

794 
apply (subst (1 3) nn_integral_max_0[symmetric]) 

795 
apply (rule nn_integral_join') 

796 
apply (auto simp: f) 

797 
done 

798 

58606  799 
lemma join_assoc: 
59048  800 
assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))" 
58606  801 
shows "join (distr M (subprob_algebra N) join) = join (join M)" 
802 
proof (rule measure_eqI) 

803 
fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))" 

804 
then have A: "A \<in> sets N" by simp 

805 
show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A" 

806 
using measurable_join[of N] 

807 
by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg 

59048  808 
sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M] 
809 
intro!: nn_integral_cong emeasure_join) 

58606  810 
qed (simp add: M) 
811 

812 
lemma join_return: 

813 
assumes "sets M = sets N" and "subprob_space M" 

814 
shows "join (return (subprob_algebra N) M) = M" 

815 
by (rule measure_eqI) 

816 
(simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra 

817 
measurable_emeasure_subprob_algebra nn_integral_return assms) 

818 

819 
lemma join_return': 

820 
assumes "sets N = sets M" 

821 
shows "join (distr M (subprob_algebra N) (return N)) = M" 

822 
apply (rule measure_eqI) 

823 
apply (simp add: assms) 

824 
apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)") 

825 
apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) 

826 
apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable) 

827 
done 

828 

829 
lemma join_distr_distr: 

830 
fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure" 

831 
assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N" 

832 
shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l") 

833 
proof (rule measure_eqI) 

834 
fix A assume "A \<in> sets ?r" 

835 
hence A_in_N: "A \<in> sets N" by simp 

836 

837 
from assms have "f \<in> measurable (join M) N" 

838 
by (simp cong: measurable_cong_sets) 

839 
moreover from assms and A_in_N have "f`A \<inter> space R \<in> sets R" 

840 
by (intro measurable_sets) simp_all 

841 
ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f`A \<inter> space R) \<partial>M" 

842 
by (simp_all add: A_in_N emeasure_distr emeasure_join assms) 

843 

844 
also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N 

845 
proof (intro nn_integral_cong, subst emeasure_distr) 

846 
fix M' assume "M' \<in> space M" 

847 
from assms have "space M = space (subprob_algebra R)" 

848 
using sets_eq_imp_space_eq by blast 

849 
with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast 

850 
show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms) 

851 
have "space M' = space R" by (rule sets_eq_imp_space_eq) simp 

852 
thus "emeasure M' (f ` A \<inter> space R) = emeasure M' (f ` A \<inter> space M')" by simp 

853 
qed 

854 

855 
also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)" 

856 
by (simp cong: measurable_cong_sets add: assms measurable_distr) 

857 
hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 

858 
emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A" 

859 
by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra) 

860 
finally show "emeasure ?r A = emeasure ?l A" .. 

861 
qed simp 

862 

863 
definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where 

864 
"bind M f = (if space M = {} then count_space {} else 

865 
join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))" 

866 

867 
adhoc_overloading Monad_Syntax.bind bind 

868 

869 
lemma bind_empty: 

870 
"space M = {} \<Longrightarrow> bind M f = count_space {}" 

871 
by (simp add: bind_def) 

872 

873 
lemma bind_nonempty: 

874 
"space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)" 

875 
by (simp add: bind_def) 

876 

877 
lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}" 

878 
by (auto simp: bind_def) 

879 

880 
lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}" 

881 
by (simp add: bind_def) 

882 

59048  883 
lemma sets_bind[simp, measurable_cong]: 
884 
assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}" 

58606  885 
shows "sets (bind M f) = sets N" 
59048  886 
using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq) 
58606  887 

888 
lemma space_bind[simp]: 

59048  889 
assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}" 
58606  890 
shows "space (bind M f) = space N" 
59048  891 
using assms by (intro sets_eq_imp_space_eq sets_bind) 
58606  892 

893 
lemma bind_cong: 

894 
assumes "\<forall>x \<in> space M. f x = g x" 

895 
shows "bind M f = bind M g" 

896 
proof (cases "space M = {}") 

897 
assume "space M \<noteq> {}" 

898 
hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast 

899 
with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast 

900 
with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong) 

901 
qed (simp add: bind_empty) 

902 

903 
lemma bind_nonempty': 

904 
assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M" 

905 
shows "bind M f = join (distr M (subprob_algebra N) f)" 

906 
using assms 

907 
apply (subst bind_nonempty, blast) 

908 
apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast) 

909 
apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]]) 

910 
done 

911 

912 
lemma bind_nonempty'': 

913 
assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}" 

914 
shows "bind M f = join (distr M (subprob_algebra N) f)" 

915 
using assms by (auto intro: bind_nonempty') 

916 

917 
lemma emeasure_bind: 

918 
"\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk> 

919 
\<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" 

920 
by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra) 

921 

59048  922 
lemma nn_integral_bind: 
923 
assumes f: "f \<in> borel_measurable B" 

59000  924 
assumes N: "N \<in> measurable M (subprob_algebra B)" 
925 
shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)" 

926 
proof cases 

927 
assume M: "space M \<noteq> {}" show ?thesis 

928 
unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr] 

929 
by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]]) 

930 
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space) 

931 

932 
lemma AE_bind: 

933 
assumes P[measurable]: "Measurable.pred B P" 

934 
assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)" 

935 
shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)" 

936 
proof cases 

937 
assume M: "space M = {}" show ?thesis 

938 
unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space) 

939 
next 

940 
assume M: "space M \<noteq> {}" 

59048  941 
note sets_kernel[OF N, simp] 
59000  942 
have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))" 
59048  943 
by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator) 
59000  944 

945 
have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0" 

59048  946 
by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B] 
59000  947 
del: nn_integral_indicator) 
948 
also have "\<dots> = (AE x in M. AE y in N x. P y)" 

949 
apply (subst nn_integral_0_iff_AE) 

950 
apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra]) 

951 
apply measurable 

952 
apply (intro eventually_subst AE_I2) 

59048  953 
apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N] 
954 
intro!: AE_iff_measurable[symmetric]) 

59000  955 
done 
956 
finally show ?thesis . 

957 
qed 

958 

959 
lemma measurable_bind': 

960 
assumes M1: "f \<in> measurable M (subprob_algebra N)" and 

961 
M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" 

962 
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" 

963 
proof (subst measurable_cong) 

964 
fix x assume x_in_M: "x \<in> space M" 

965 
with assms have "space (f x) \<noteq> {}" 

966 
by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty) 

967 
moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)" 

968 
by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl]) 

969 
(auto dest: measurable_Pair2) 

970 
ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 

971 
by (simp_all add: bind_nonempty'') 

972 
next 

973 
show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)" 

974 
apply (rule measurable_compose[OF _ measurable_join]) 

975 
apply (rule measurable_distr2[OF M2 M1]) 

976 
done 

977 
qed 

58606  978 

59048  979 
lemma measurable_bind[measurable (raw)]: 
59000  980 
assumes M1: "f \<in> measurable M (subprob_algebra N)" and 
981 
M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" 

982 
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" 

983 
using assms by (auto intro: measurable_bind' simp: measurable_split_conv) 

984 

985 
lemma measurable_bind2: 

986 
assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)" 

987 
shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)" 

988 
using assms by (intro measurable_bind' measurable_const) auto 

989 

990 
lemma subprob_space_bind: 

991 
assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)" 

992 
shows "subprob_space (M \<guillemotright>= f)" 

993 
proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"]) 

994 
show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" 

995 
by (rule measurable_bind, rule measurable_ident_sets, rule refl, 

996 
rule measurable_compose[OF measurable_snd assms(2)]) 

997 
from assms(1) show "M \<in> space (subprob_algebra M)" 

998 
by (simp add: space_subprob_algebra) 

999 
qed 

58606  1000 

59000  1001 
lemma (in prob_space) prob_space_bind: 
1002 
assumes ae: "AE x in M. prob_space (N x)" 

1003 
and N[measurable]: "N \<in> measurable M (subprob_algebra S)" 

1004 
shows "prob_space (M \<guillemotright>= N)" 

1005 
proof 

1006 
have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)" 

1007 
by (subst emeasure_bind[where N=S]) 

59048  1008 
(auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong) 
59000  1009 
also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)" 
1010 
using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1) 

1011 
finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1" 

1012 
by (simp add: emeasure_space_1) 

1013 
qed 

1014 

1015 
lemma (in subprob_space) bind_in_space: 

1016 
"A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)" 

59048  1017 
by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind) 
59000  1018 
unfold_locales 
1019 

1020 
lemma (in subprob_space) measure_bind: 

1021 
assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N" 

1022 
shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M" 

1023 
proof  

1024 
interpret Mf: subprob_space "M \<guillemotright>= f" 

1025 
by (rule subprob_space_bind[OF _ f]) unfold_locales 

1026 

1027 
{ fix x assume "x \<in> space M" 

1028 
from f[THEN measurable_space, OF this] interpret subprob_space "f x" 

1029 
by (simp add: space_subprob_algebra) 

1030 
have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1" 

1031 
by (auto simp: emeasure_eq_measure subprob_measure_le_1) } 

1032 
note this[simp] 

1033 

1034 
have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" 

1035 
using subprob_not_empty f X by (rule emeasure_bind) 

1036 
also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M" 

1037 
by (intro nn_integral_cong) simp 

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

1039 
by (intro nn_integral_eq_integral integrable_const_bound[where B=1] 

1040 
measure_measurable_subprob_algebra2[OF _ f] pair_measureI X) 

1041 
(auto simp: measure_nonneg) 

1042 
finally show ?thesis 

1043 
by (simp add: Mf.emeasure_eq_measure) 

58606  1044 
qed 
1045 

1046 
lemma emeasure_bind_const: 

1047 
"space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 

1048 
emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 

1049 
by (simp add: bind_nonempty emeasure_join nn_integral_distr 

1050 
space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg) 

1051 

1052 
lemma emeasure_bind_const': 

1053 
assumes "subprob_space M" "subprob_space N" 

1054 
shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 

1055 
using assms 

1056 
proof (case_tac "X \<in> sets N") 

1057 
fix X assume "X \<in> sets N" 

1058 
thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms 

1059 
by (subst emeasure_bind_const) 

1060 
(simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1) 

1061 
next 

1062 
fix X assume "X \<notin> sets N" 

1063 
with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 

1064 
by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty 

1065 
space_subprob_algebra emeasure_notin_sets) 

1066 
qed 

1067 

1068 
lemma emeasure_bind_const_prob_space: 

1069 
assumes "prob_space M" "subprob_space N" 

1070 
shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X" 

1071 
using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 

1072 
prob_space.emeasure_space_1) 

1073 

59000  1074 
lemma bind_return: 
1075 
assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M" 

1076 
shows "bind (return M x) f = f x" 

1077 
using sets_kernel[OF assms] assms 

1078 
by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty' 

1079 
cong: subprob_algebra_cong) 

1080 

1081 
lemma bind_return': 

1082 
shows "bind M (return M) = M" 

1083 
by (cases "space M = {}") 

1084 
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 

1085 
cong: subprob_algebra_cong) 

1086 

1087 
lemma distr_bind: 

1088 
assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}" 

1089 
assumes f: "f \<in> measurable K R" 

1090 
shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))" 

1091 
unfolding bind_nonempty''[OF N] 

1092 
apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)]) 

1093 
apply (rule f) 

1094 
apply (simp add: join_distr_distr[OF _ f, symmetric]) 

1095 
apply (subst distr_distr[OF measurable_distr, OF f N(1)]) 

1096 
apply (simp add: comp_def) 

1097 
done 

1098 

1099 
lemma bind_distr: 

1100 
assumes f[measurable]: "f \<in> measurable M X" 

1101 
assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}" 

1102 
shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))" 

1103 
proof  

1104 
have "space X \<noteq> {}" "space M \<noteq> {}" 

1105 
using `space M \<noteq> {}` f[THEN measurable_space] by auto 

1106 
then show ?thesis 

1107 
by (simp add: bind_nonempty''[where N=K] distr_distr comp_def) 

1108 
qed 

1109 

1110 
lemma bind_count_space_singleton: 

1111 
assumes "subprob_space (f x)" 

1112 
shows "count_space {x} \<guillemotright>= f = f x" 

1113 
proof 

1114 
have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto 

1115 
have "count_space {x} = return (count_space {x}) x" 

1116 
by (intro measure_eqI) (auto dest: A) 

1117 
also have "... \<guillemotright>= f = f x" 

1118 
by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms) 

1119 
finally show ?thesis . 

1120 
qed 

1121 

1122 
lemma restrict_space_bind: 

1123 
assumes N: "N \<in> measurable M (subprob_algebra K)" 

1124 
assumes "space M \<noteq> {}" 

1125 
assumes X[simp]: "X \<in> sets K" "X \<noteq> {}" 

1126 
shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)" 

1127 
proof (rule measure_eqI) 

59048  1128 
note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp] 
1129 
note N_space = sets_eq_imp_space_eq[OF N_sets, simp] 

1130 
show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))" 

1131 
by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]]) 

59000  1132 
fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)" 
1133 
with X have "A \<in> sets K" "A \<subseteq> X" 

59048  1134 
by (auto simp: sets_restrict_space) 
59000  1135 
then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A" 
1136 
using assms 

1137 
apply (subst emeasure_restrict_space) 

59048  1138 
apply (simp_all add: emeasure_bind[OF assms(2,1)]) 
59000  1139 
apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]]) 
1140 
apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra 

1141 
intro!: nn_integral_cong dest!: measurable_space) 

1142 
done 

59048  1143 
qed 
59000  1144 

58606  1145 
lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N" 
1146 
by (intro measure_eqI) 

1147 
(simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space) 

1148 

1149 
lemma bind_return_distr: 

1150 
"space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f" 

1151 
apply (simp add: bind_nonempty) 

1152 
apply (subst subprob_algebra_cong) 

1153 
apply (rule sets_return) 

1154 
apply (subst distr_distr[symmetric]) 

1155 
apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') 

1156 
done 

1157 

1158 
lemma bind_assoc: 

1159 
fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure" 

1160 
assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)" 

1161 
shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)" 

1162 
proof (cases "space M = {}") 

1163 
assume [simp]: "space M \<noteq> {}" 

1164 
from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}" 

1165 
by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) 

1166 
from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" 

1167 
by (simp add: sets_kernel) 

1168 
have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast 

1169 
note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]] 

1170 
sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]] 

1171 
note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)] 

1172 

1173 
have "bind M (\<lambda>x. bind (f x) g) = 

1174 
join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))" 

1175 
by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def 

1176 
cong: subprob_algebra_cong distr_cong) 

1177 
also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) = 

1178 
distr (distr (distr M (subprob_algebra N) f) 

1179 
(subprob_algebra (subprob_algebra R)) 

1180 
(\<lambda>x. distr x (subprob_algebra R) g)) 

1181 
(subprob_algebra R) join" 

1182 
apply (subst distr_distr, 

1183 
(blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+ 

1184 
apply (simp add: o_assoc) 

1185 
done 

1186 
also have "join ... = bind (bind M f) g" 

1187 
by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong) 

1188 
finally show ?thesis .. 

1189 
qed (simp add: bind_empty) 

1190 

1191 
lemma double_bind_assoc: 

1192 
assumes Mg: "g \<in> measurable N (subprob_algebra N')" 

1193 
assumes Mf: "f \<in> measurable M (subprob_algebra M')" 

1194 
assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N" 

1195 
shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g" 

1196 
proof 

1197 
have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 

1198 
do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}" 

1199 
using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg 

1200 
measurable_compose[OF _ return_measurable] simp: measurable_split_conv) 

1201 
also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable 

1202 
hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 

1203 
do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}" 

1204 
apply (intro ballI bind_cong bind_assoc) 

1205 
apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp) 

1206 
apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg) 

1207 
done 

1208 
also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'" 

1209 
by (intro sets_eq_imp_space_eq sets_kernel[OF Mf]) 

1210 
with measurable_space[OF Mh] 

1211 
have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}" 

1212 
by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure) 

1213 
finally show ?thesis .. 

1214 
qed 

1215 

59048  1216 
lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)" 
1217 
by (simp add: space_subprob_algebra) unfold_locales 

1218 

59000  1219 
lemma (in pair_prob_space) pair_measure_eq_bind: 
1220 
"(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" 

1221 
proof (rule measure_eqI) 

1222 
have ps_M2: "prob_space M2" by unfold_locales 

1223 
note return_measurable[measurable] 

1224 
show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" 

59048  1225 
by (simp_all add: M1.not_empty M2.not_empty) 
59000  1226 
fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" 
1227 
show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A" 

59048  1228 
by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] 
59000  1229 
intro!: nn_integral_cong) 
1230 
qed 

1231 

1232 
lemma (in pair_prob_space) bind_rotate: 

1233 
assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)" 

1234 
shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))" 

1235 
proof  

1236 
interpret swap: pair_prob_space M2 M1 by unfold_locales 

1237 
note measurable_bind[where N="M2", measurable] 

1238 
note measurable_bind[where N="M1", measurable] 

1239 
have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)" 

1240 
by (auto simp: space_subprob_algebra) unfold_locales 

1241 
have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 

1242 
(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)" 

1243 
by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N]) 

1244 
also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)" 

1245 
unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] .. 

1246 
also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)" 

1247 
unfolding swap.pair_measure_eq_bind[symmetric] 

1248 
by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong) 

1249 
also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))" 

1250 
by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N]) 

1251 
finally show ?thesis . 

1252 
qed 

1253 

58608  1254 
section {* Measures form a $\omega$chain complete partial order *} 
58606  1255 

1256 
definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where 

1257 
"SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)" 

1258 

1259 
lemma 

1260 
assumes const: "\<And>i j. sets (M i) = sets (M j)" 

1261 
shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp) 

1262 
and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st) 

1263 
proof  

1264 
have "(\<Union>i. sets (M i)) = sets (M i)" 

1265 
using const by auto 

1266 
moreover have "(\<Union>i. space (M i)) = space (M i)" 

1267 
using const[THEN sets_eq_imp_space_eq] by auto 

1268 
moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))" 

1269 
by (auto dest: sets.sets_into_space) 

1270 
ultimately show ?sp ?st 

1271 
by (simp_all add: SUP_measure_def) 

1272 
qed 

1273 

1274 
lemma emeasure_SUP_measure: 

1275 
assumes const: "\<And>i j. sets (M i) = sets (M j)" 

1276 
and mono: "mono (\<lambda>i. emeasure (M i))" 

1277 
shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)" 

1278 
proof cases 

1279 
assume "A \<in> sets (SUP_measure M)" 

1280 
show ?thesis 

1281 
proof (rule emeasure_measure_of[OF SUP_measure_def]) 

1282 
show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)" 

1283 
proof (rule countably_additiveI) 

1284 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)" 

1285 
then have "\<And>i j. A i \<in> sets (M j)" 

1286 
using sets_SUP_measure[of M, OF const] by simp 

1287 
moreover assume "disjoint_family A" 

1288 
ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))" 

1289 
using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure) 

1290 
qed 

1291 
show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)" 

1292 
by (auto simp: positive_def intro: SUP_upper2) 

1293 
show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))" 

1294 
using sets.sets_into_space by auto 

1295 
qed fact 

1296 
next 

1297 
assume "A \<notin> sets (SUP_measure M)" 

1298 
with sets_SUP_measure[of M, OF const] show ?thesis 

1299 
by (simp add: emeasure_notin_sets) 

1300 
qed 

1301 

59425  1302 
lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M" 
1303 
by (cases "space M = {}") 

1304 
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 

1305 
cong: subprob_algebra_cong) 

1306 

1307 
lemma (in prob_space) distr_const[simp]: 

1308 
"c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c" 

1309 
by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1) 

1310 

1311 
lemma return_count_space_eq_density: 

1312 
"return (count_space M) x = density (count_space M) (indicator {x})" 

1313 
by (rule measure_eqI) 

1314 
(auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator) 

1315 

58606  1316 
end 