author  wenzelm 
Sat, 28 Nov 2015 23:59:08 +0100  
changeset 61753  865bb718bdb9 
parent 61634  48e2de1b1df5 
child 61808  fc1556774cfe 
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 

61169  28 
show "subprob_space M" by standard fact+ 
58606  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 

60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

41 
lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

42 
by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

43 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

44 
lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

45 
by(simp add: null_measure_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

46 

58606  47 
lemma (in subprob_space) subprob_space_distr: 
48 
assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)" 

49 
proof (rule subprob_spaceI) 

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

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

52 
by (auto simp: emeasure_distr emeasure_space_le_1) 

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

54 
qed 

55 

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

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

61 

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

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

65 
proof  

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

67 
by(rule nn_integral_mono_AE) fact 

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

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

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

71 
finally show ?thesis by simp 

72 
qed 

73 

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

74 
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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
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

83 
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

84 
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

85 
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

86 
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

87 
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

88 
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

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

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

91 
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

92 
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

93 
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

94 
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

95 
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

96 
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

97 

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

98 
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

99 
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

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

101 
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

102 
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

103 
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

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

105 
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

106 
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

107 
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

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

109 

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

110 
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

111 
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

112 
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

113 
\<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

114 
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

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

116 
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

117 
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

118 
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

119 
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

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

121 
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

122 
(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

123 
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

124 
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

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

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

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

128 
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

129 
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

130 
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

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

132 

58606  133 
locale pair_subprob_space = 
134 
pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2 

135 

61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61424
diff
changeset

136 
sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2" 
58606  137 
proof 
138 
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

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

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

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

144 
by (simp add: space_pair_measure) 

145 
qed 

146 

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

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

150 

59525  151 
lemma subprob_space_restrict_space: 
152 
assumes M: "subprob_space M" 

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

154 
shows "subprob_space (restrict_space M A)" 

155 
proof(rule subprob_spaceI) 

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

157 
using A by(simp add: emeasure_restrict_space space_restrict_space) 

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

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

160 
next 

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

162 
using A by(simp add: space_restrict_space) 

163 
qed 

164 

58606  165 
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where 
166 
"subprob_algebra K = 

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

168 

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

170 
by (auto simp add: subprob_algebra_def space_Sup_sigma) 

171 

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

173 
by (simp add: subprob_algebra_def) 

174 

175 
lemma measurable_emeasure_subprob_algebra[measurable]: 

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

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

178 

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

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

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

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

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

185 
using measurable_space[OF N x] 

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

187 

59048  188 
ML {* 
189 

190 
fun subprob_cong thm ctxt = ( 

191 
let 

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

59582  193 
val free = thm' > Thm.concl_of > HOLogic.dest_Trueprop > dest_comb > fst > 
59048  194 
dest_comb > snd > strip_abs_body > head_of > is_Free 
195 
in 

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

197 
else ([], ctxt) 

198 
end 

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

200 

201 
*} 

202 

203 
setup \<open> 

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

205 
\<close> 

206 

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

209 
begin 

210 

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

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

213 

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

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

216 

217 
lemma measurable_emeasure_kernel[measurable]: 

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

219 
using measurable_compose[OF K measurable_emeasure_subprob_algebra] . 

220 

221 
end 

222 

223 
lemma measurable_subprob_algebra: 

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

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

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

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

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

229 

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

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

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

234 
proof 

235 
assume "(\<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 
then show "K \<in> measurable M (subprob_algebra M)" 

238 
by (intro measurable_subprob_algebra) auto 

239 
next 

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

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

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

243 
by (auto dest: subprob_space_kernel sets_kernel) 

244 
qed 

245 

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

248 
proof 

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

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

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

252 
by auto 

253 
next 

254 
assume "space N = {}" 

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

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

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

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

259 
qed 

260 

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

264 
using f 

265 
proof induct 

266 
case (cong f g) 

267 
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" 

268 
by (intro measurable_cong nn_integral_cong cong) 

269 
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 

270 
ultimately show ?case by simp 

271 
next 

272 
case (set B) 

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

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

275 
ultimately show ?case 

276 
by (simp add: measurable_emeasure_subprob_algebra) 

277 
next 

278 
case (mult f c) 

279 
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  280 
by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 
59000  281 
ultimately show ?case 
282 
by simp 

283 
next 

284 
case (add f g) 

285 
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  286 
by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) 
59000  287 
ultimately show ?case 
288 
by (simp add: ac_simps) 

289 
next 

290 
case (seq F) 

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

292 
unfolding SUP_apply 

59048  293 
by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) 
59000  294 
ultimately show ?case 
295 
by (simp add: ac_simps) 

296 
qed 

297 

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

300 
by (subst nn_integral_max_0[symmetric]) 

301 
(auto intro!: nn_integral_measurable_subprob_algebra') 

302 

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

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

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

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

308 
show ?thesis 

309 
proof (rule measurable_subprob_algebra) 

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

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

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

313 
by (intro measurable_cong) 

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

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

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

59048  319 
qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets) 
58606  320 
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) 
321 

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

324 
proof 

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

326 
by (rule measurable_emeasure_subprob_algebra) simp 

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

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

329 
finally show ?thesis . 

330 
qed 

331 

60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

332 
lemma integral_measurable_subprob_algebra: 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

333 
fixes f :: "_ \<Rightarrow> real" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

334 
assumes f_measurable [measurable]: "f \<in> borel_measurable N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

335 
and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

336 
shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

337 
proof  
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

338 
note [measurable] = nn_integral_measurable_subprob_algebra 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

339 
have "?thesis \<longleftrightarrow> (\<lambda>M. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M)  real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

340 
proof(rule measurable_cong) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

341 
fix M 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

342 
assume "M \<in> space (subprob_algebra N)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

343 
hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

344 
by(simp_all add: space_subprob_algebra) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

345 
interpret subprob_space M by fact 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

346 
have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

347 
by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

348 
also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

349 
also have "\<dots> \<le> ereal (max B 0) * 1" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

350 
by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

351 
finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

352 
then have "integrable M f" using f_measurable 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

353 
by(auto intro: integrableI_bounded) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

354 
thus "(\<integral> x. f x \<partial>M) = real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M)  real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M)" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

355 
by(simp add: real_lebesgue_integral_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

356 
qed 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

357 
also have "\<dots>" by measurable 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

358 
finally show ?thesis . 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

359 
qed 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

360 

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

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

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

366 
proof (rule measurable_subprob_algebra) 

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

368 
with measurable_space[OF f] measurable_space[OF g] 

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

370 
by auto 

371 
interpret F: subprob_space "f x" 

372 
using fx by (simp add: space_subprob_algebra) 

373 
interpret G: subprob_space "g x" 

374 
using gx by (simp add: space_subprob_algebra) 

375 

376 
interpret pair_subprob_space "f x" "g x" .. 

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

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

379 
using fx gx by (simp add: space_subprob_algebra) 

380 

381 
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" 

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

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

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

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

386 
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) = 

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

388 
using emeasure_compl[OF _ P.emeasure_finite] 

389 
unfolding sets_eq 

390 
unfolding sets_eq_imp_space_eq[OF sets_eq] 

391 
by (simp add: space_pair_measure G.emeasure_pair_measure_Times) 

392 
note 1 2 sets_eq } 

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

394 

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

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

397 
using Int_stable_pair_measure_generator pair_measure_closed A 

398 
unfolding sets_pair_measure 

399 
proof (induct A rule: sigma_sets_induct_disjoint) 

400 
case (basic A) then show ?case 

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

402 
(auto intro!: measurable_emeasure_kernel f g) 

403 
next 

404 
case (compl A) 

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

406 
by (auto simp: sets_pair_measure) 

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

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

409 
using compl(2) f g by measurable 

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

411 
next 

412 
case (union A) 

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

414 
by (auto simp: sets_pair_measure) 

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

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

417 
by (intro measurable_cong suminf_emeasure[symmetric]) 

418 
(auto simp: sets_eq) 

419 
also have "\<dots>" 

420 
using union by auto 

421 
finally show ?case . 

422 
qed simp 

423 
qed 

424 

425 
lemma restrict_space_measurable: 

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

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

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

429 
proof (rule measurable_subprob_algebra) 

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

431 
from N[THEN measurable_space, OF this] 

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

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

434 
then interpret subprob_space "N a" 

435 
by simp 

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

437 
proof 

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

439 
using X by (auto simp add: space_restrict_space) 

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

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

442 
qed 

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

444 
by (intro sets_restrict_space_cong) fact 

445 
next 

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

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

448 
proof (subst measurable_cong) 

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

450 
from N[THEN measurable_space, OF this] 

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

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

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

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

455 
next 

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

457 
using A X 

458 
by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra]) 

459 
(auto simp: sets_restrict_space) 

460 
qed 

461 
qed 

462 

58606  463 
section {* Properties of return *} 
464 

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

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

467 

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

469 
by (simp add: return_def) 

470 

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

472 
by (simp add: return_def) 

473 

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

475 
by (simp cong: measurable_cong_sets) 

476 

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

478 
by (simp cong: measurable_cong_sets) 

479 

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

482 

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

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

485 

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

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

489 
proof (rule emeasure_measure_of[OF return_def]) 

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

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

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

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

494 
by (auto intro: countably_additiveI simp: suminf_indicator) 

495 
qed 

496 

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

498 
by rule simp 

499 

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

501 
by (intro prob_space_return prob_space_imp_subprob_space) 

502 

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

505 
proof 

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

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

508 
qed (simp, fact) 

509 

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

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

512 

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

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

516 
proof  

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

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

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

520 
by (rule AE_cong) auto 

521 
finally show ?thesis . 

522 
qed 

523 

524 
lemma nn_integral_return: 

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

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

527 
proof 

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

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

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

531 
also have "... = g x" 

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

533 
finally show ?thesis . 

534 
qed 

535 

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

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

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

540 
proof 

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

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

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

544 
then show ?thesis 

545 
using prob_space by simp 

546 
qed 

547 

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

58606  549 
by (rule measurable_subprob_algebra) (auto simp: subprob_space_return) 
550 

551 
lemma distr_return: 

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

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

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

555 

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

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

559 

560 
lemma measurable_distr2: 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset

561 
assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N" 
59000  562 
assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)" 
563 
shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)" 

564 
proof  

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

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset

566 
\<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)" 
59000  567 
proof (rule measurable_cong) 
568 
fix x assume x: "x \<in> space L" 

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

570 
using measurable_space[OF g x] . 

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

572 
by (simp add: space_subprob_algebra) 

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

574 
by (rule sets_eq_imp_space_eq) 

575 
let ?R = "return L x" 

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

577 
by simp 

578 
interpret subprob_space "g x" 

579 
using gx by (simp add: space_subprob_algebra) 

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

581 
by (simp add: space_pair_measure) 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset

582 
show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r") 
59000  583 
proof (rule measure_eqI) 
584 
show "sets ?l = sets ?r" 

585 
by simp 

586 
next 

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

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

589 
by simp 

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

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

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

593 
apply (subst emeasure_pair_measure_alt) 

594 
apply (rule measurable_sets[OF _ A]) 

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

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

597 
apply (auto simp: space_subprob_algebra space_pair_measure) 

598 
done 

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

600 
by (subst nn_integral_return) 

601 
(auto simp: x intro!: measurable_emeasure) 

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

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

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

605 
qed 

606 
qed 

607 
also have "\<dots>" 

608 
apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) 

609 
apply (rule return_measurable) 

610 
apply measurable 

611 
done 

612 
finally show ?thesis . 

613 
qed 

614 

615 
lemma nn_integral_measurable_subprob_algebra2: 

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

619 
proof  

59048  620 
note nn_integral_measurable_subprob_algebra[measurable] 
621 
note measurable_distr2[measurable] 

59000  622 
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  623 
by measurable 
59000  624 
then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" 
59048  625 
by (rule measurable_cong[THEN iffD1, rotated]) 
626 
(simp add: nn_integral_distr) 

59000  627 
qed 
628 

629 
lemma emeasure_measurable_subprob_algebra2: 

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

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

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

633 
proof  

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

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

636 
by auto 

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

638 
by auto } 

639 
note ** = this 

640 

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

642 
by (auto simp: fun_eq_iff) 

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

644 
apply measurable 

645 
apply (subst measurable_cong) 

646 
apply (rule *) 

647 
apply (auto simp: space_pair_measure) 

648 
done 

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

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

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

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

653 
apply (rule nn_integral_indicator) 

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

655 
done 

656 
qed 

657 

658 
lemma measure_measurable_subprob_algebra2: 

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

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

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

662 
unfolding measure_def 

663 
by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms]) 

664 

58606  665 
definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))" 
666 

667 
lemma select_sets1: 

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

669 
unfolding select_sets_def by (rule someI) 

670 

671 
lemma sets_select_sets[simp]: 

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

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

674 
unfolding select_sets_def 

675 
proof (rule someI2) 

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

677 
by fact 

678 
next 

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

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

681 
by (intro sets_eq_imp_space_eq) simp 

682 
show "sets L = sets N" 

683 
proof cases 

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

685 
with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L] 

686 
show ?thesis 

687 
by (simp add: eq space_empty_iff) 

688 
next 

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

690 
with eq show ?thesis 

691 
by (fastforce simp add: space_subprob_algebra) 

692 
qed 

693 
qed 

694 

695 
lemma space_select_sets[simp]: 

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

697 
by (intro sets_eq_imp_space_eq sets_select_sets) 

698 

699 
section {* Join *} 

700 

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

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

703 

704 
lemma 

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

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

707 
by (simp_all add: join_def) 

708 

709 
lemma emeasure_join: 

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

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

714 
proof (rule countably_additiveI) 

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

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

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

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

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

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

723 
qed 

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

725 
qed 

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

727 

728 
lemma measurable_join: 

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

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

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

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

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

734 
proof (rule measurable_cong) 

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

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

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

738 
qed 

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

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

743 
next 

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

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

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

747 
apply (intro nn_integral_mono) 

748 
apply (auto simp: space_subprob_algebra 

749 
dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) 

750 
done 

751 
with M show "subprob_space (join M)" 

752 
by (intro subprob_spaceI) 

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

754 
next 

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

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

757 
qed (auto simp: space_subprob_algebra) 

758 

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

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

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

764 
proof induct 

765 
case (cong f g) 

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

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

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

769 
by (intro nn_integral_cong cong) 

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

771 
ultimately show ?case 

772 
by simp 

773 
next 

774 
case (set A) 

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

776 
by (intro nn_integral_cong nn_integral_indicator) 

777 
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 

778 
ultimately show ?case 

779 
using M by (simp add: emeasure_join) 

780 
next 

781 
case (mult f c) 

782 
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  783 
using mult M M[THEN sets_eq_imp_space_eq] 
784 
by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 

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

789 
by (simp add: mult) 

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

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

794 
case (add f g) 

795 
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  796 
using add M M[THEN sets_eq_imp_space_eq] 
797 
by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra) 

58606  798 
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  799 
using nn_integral_measurable_subprob_algebra[OF add(1)] 
800 
using nn_integral_measurable_subprob_algebra[OF add(5)] 

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

803 
by (simp add: add) 

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

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

808 
case (seq F) 

809 
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  810 
using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply 
58606  811 
by (intro nn_integral_cong nn_integral_monotone_convergence_SUP) 
59048  812 
(auto simp add: space_subprob_algebra) 
58606  813 
also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)" 
59048  814 
using nn_integral_measurable_subprob_algebra[OF seq(1)] seq 
58606  815 
by (intro nn_integral_monotone_convergence_SUP) 
816 
(simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono ) 

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

818 
by (simp add: seq) 

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

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

58606  822 
finally show ?case by (simp add: ac_simps) 
823 
qed 

824 

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

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

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

829 
apply (rule nn_integral_join') 

830 
apply (auto simp: f) 

831 
done 

832 

60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

833 
lemma measurable_join1: 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

834 
"\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk> 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

835 
\<Longrightarrow> f \<in> measurable (join M) K" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

836 
by(simp add: measurable_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

837 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

838 
lemma 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

839 
fixes f :: "_ \<Rightarrow> real" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

840 
assumes f_measurable [measurable]: "f \<in> borel_measurable N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

841 
and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

842 
and M [measurable_cong]: "sets M = sets (subprob_algebra N)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

843 
and fin: "finite_measure M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

844 
and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

845 
shows integrable_join: "integrable (join M) f" (is ?integrable) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

846 
and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

847 
proof(case_tac [!] "space N = {}") 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

848 
assume *: "space N = {}" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

849 
show ?integrable 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

850 
using M * by(simp add: real_integrable_def measurable_def nn_integral_empty) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

851 
have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

852 
proof(rule integral_cong) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

853 
fix M' 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

854 
assume "M' \<in> space M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

855 
with sets_eq_imp_space_eq[OF M] have "space M' = space N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

856 
by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

857 
with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

858 
qed simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

859 
then show ?integral 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

860 
using M * by(simp add: integral_empty) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

861 
next 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

862 
assume *: "space N \<noteq> {}" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

863 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

864 
from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

865 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

866 
have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

867 
by(rule measurable_join1) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

868 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

869 
{ fix f M' 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

870 
assume [measurable]: "f \<in> borel_measurable N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

871 
and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

872 
and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

873 
have "AE x in M'. ereal (f x) \<le> ereal B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

874 
proof(rule AE_I2) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

875 
fix x 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

876 
assume "x \<in> space M'" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

877 
with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M] 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

878 
have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

879 
from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

880 
qed 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

881 
then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

882 
by(rule nn_integral_mono_AE) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

883 
also have "\<dots> = ereal B * emeasure M' (space M')" by(simp) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

884 
also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

885 
also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

886 
finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp } 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

887 
note bounded1 = this 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

888 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

889 
have bounded: 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

890 
"\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk> 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

891 
\<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

892 
proof  
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

893 
fix f 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

894 
assume [measurable]: "f \<in> borel_measurable N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

895 
and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

896 
have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

897 
by(rule nn_integral_join[OF _ M]) simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

898 
also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

899 
using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded] 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

900 
by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

901 
also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

902 
also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

903 
finally show "?thesis f" by simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

904 
qed 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

905 
have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

906 
and f_neg: "(\<integral>\<^sup>+ x. ereal ( f x) \<partial>join M) \<noteq> \<infinity>" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

907 
using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

908 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

909 
show ?integrable using f_pos f_neg by(simp add: real_integrable_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

910 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

911 
note [measurable] = nn_integral_measurable_subprob_algebra 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

912 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

913 
have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

914 
by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

915 
also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

916 
by(simp add: nn_integral_join[OF _ M]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

917 
also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

918 
by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

919 
finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" . 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

920 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

921 
have "(\<integral>\<^sup>+ x.  f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 ( f x) \<partial>join M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

922 
by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

923 
also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 ( f x) \<partial>M' \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

924 
by(simp add: nn_integral_join[OF _ M]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

925 
also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

926 
by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

927 
finally have int_mf: "(\<integral>\<^sup>+ x.  f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M)" . 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

928 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

929 
have f_pos1: 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

930 
"\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk> 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

931 
\<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

932 
using f_measurable by(auto intro!: bounded1 dest: f_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

933 
have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

934 
using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

935 
hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

936 
by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

937 
from f_pos have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M'))" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

938 
by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

939 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

940 
have f_neg1: 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

941 
"\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk> 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

942 
\<Longrightarrow> (\<integral>\<^sup>+ x. ereal ( f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

943 
using f_measurable by(auto intro!: bounded1 dest: f_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

944 
have "AE M' in M. (\<integral>\<^sup>+ x.  f x \<partial>M') \<noteq> \<infinity>" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

945 
using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

946 
hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M)" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

947 
by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

948 
from f_neg have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M'))" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

949 
by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

950 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

951 
from \<open>?integrable\<close> 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

952 
have "ereal (\<integral> x. f x \<partial>join M) = (\<integral>\<^sup>+ x. f x \<partial>join M)  (\<integral>\<^sup>+ x.  f x \<partial>join M)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

953 
by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1)) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

954 
also note int_f 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

955 
also note int_mf 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

956 
also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)  (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M) = 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

957 
((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)  (\<integral>\<^sup>+ M'.  \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M))  
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

958 
((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M)  (\<integral>\<^sup>+ M'.  \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M))" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

959 
by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

960 
also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)  (\<integral>\<^sup>+ M'.  \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) = \<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

961 
using f_pos 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

962 
by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric]) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

963 
also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M)  (\<integral>\<^sup>+ M'.  \<integral>\<^sup>+ x.  f x \<partial>M' \<partial>M) = \<integral> M'. real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M') \<partial>M" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

964 
using f_neg 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

965 
by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

966 
also note ereal_minus(1) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

967 
also have "(\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M)  (\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M') \<partial>M) = 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

968 
\<integral>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M')  real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M') \<partial>M" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

969 
by simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

970 
also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

971 
proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

972 
show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

973 
by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

974 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

975 
fix M' 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

976 
assume "M' \<in> space M" "emeasure M' (space M') \<le> B'" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

977 
then interpret finite_measure M' by(auto intro: finite_measureI) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

978 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

979 
from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M] 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

980 
have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

981 
hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

982 
have "integrable M' f" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

983 
by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset

984 
then show "real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M')  real_of_ereal (\<integral>\<^sup>+ x.  f x \<partial>M') = \<integral> x. f x \<partial>M'" 
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

985 
by(simp add: real_lebesgue_integral_def) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

986 
qed simp_all 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

987 
finally show ?integral by simp 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

988 
qed 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

989 

58606  990 
lemma join_assoc: 
59048  991 
assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))" 
58606  992 
shows "join (distr M (subprob_algebra N) join) = join (join M)" 
993 
proof (rule measure_eqI) 

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

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

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

997 
using measurable_join[of N] 

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

59048  999 
sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M] 
1000 
intro!: nn_integral_cong emeasure_join) 

58606  1001 
qed (simp add: M) 
1002 

1003 
lemma join_return: 

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

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

1006 
by (rule measure_eqI) 

1007 
(simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra 

1008 
measurable_emeasure_subprob_algebra nn_integral_return assms) 

1009 

1010 
lemma join_return': 

1011 
assumes "sets N = sets M" 

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

1013 
apply (rule measure_eqI) 

1014 
apply (simp add: assms) 

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

1016 
apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) 

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

1018 
done 

1019 

1020 
lemma join_distr_distr: 

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

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

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

1024 
proof (rule measure_eqI) 

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

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

1027 

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

1029 
by (simp cong: measurable_cong_sets) 

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

1031 
by (intro measurable_sets) simp_all 

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

1033 
by (simp_all add: A_in_N emeasure_distr emeasure_join assms) 

1034 

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

1036 
proof (intro nn_integral_cong, subst emeasure_distr) 

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

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

1039 
using sets_eq_imp_space_eq by blast 

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

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

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

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

1044 
qed 

1045 

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

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

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

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

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

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

1052 
qed simp 

1053 

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

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

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

1057 

1058 
adhoc_overloading Monad_Syntax.bind bind 

1059 

1060 
lemma bind_empty: 

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

1062 
by (simp add: bind_def) 

1063 

1064 
lemma bind_nonempty: 

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

1066 
by (simp add: bind_def) 

1067 

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

1069 
by (auto simp: bind_def) 

1070 

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

1072 
by (simp add: bind_def) 

1073 

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

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

1079 
lemma space_bind[simp]: 

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

1084 
lemma bind_cong: 

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

1086 
shows "bind M f = bind M g" 

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

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

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

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

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

1092 
qed (simp add: bind_empty) 

1093 

1094 
lemma bind_nonempty': 

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

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

1097 
using assms 

1098 
apply (subst bind_nonempty, blast) 

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

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

1101 
done 

1102 

1103 
lemma bind_nonempty'': 

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

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

1106 
using assms by (auto intro: bind_nonempty') 

1107 

1108 
lemma emeasure_bind: 

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

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

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

1112 

59048  1113 
lemma nn_integral_bind: 
1114 
assumes f: "f \<in> borel_measurable B" 

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

1117 
proof cases 

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

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

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

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

1122 

1123 
lemma AE_bind: 

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

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

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

1127 
proof cases 

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

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

1130 
next 

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

59048  1132 
note sets_kernel[OF N, simp] 
59000  1133 
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  1134 
by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator) 
59000  1135 

1136 
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  1137 
by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B] 
59000  1138 
del: nn_integral_indicator) 
1139 
also have "\<dots> = (AE x in M. AE y in N x. P y)" 

1140 
apply (subst nn_integral_0_iff_AE) 

1141 
apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra]) 

1142 
apply measurable 

1143 
apply (intro eventually_subst AE_I2) 

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

59000  1146 
done 
1147 
finally show ?thesis . 

1148 
qed 

1149 

1150 
lemma measurable_bind': 

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

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset

1152 
M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" 
59000  1153 
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" 
1154 
proof (subst measurable_cong) 

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

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

1157 
by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty) 

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

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

1160 
(auto dest: measurable_Pair2) 

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

1162 
by (simp_all add: bind_nonempty'') 

1163 
next 

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

1165 
apply (rule measurable_compose[OF _ measurable_join]) 

1166 
apply (rule measurable_distr2[OF M2 M1]) 

1167 
done 

1168 
qed 

58606  1169 

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

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

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

1175 

1176 
lemma measurable_bind2: 

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

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

1179 
using assms by (intro measurable_bind' measurable_const) auto 

1180 

1181 
lemma subprob_space_bind: 

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

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

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

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

1186 
by (rule measurable_bind, rule measurable_ident_sets, rule refl, 

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

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

1189 
by (simp add: space_subprob_algebra) 

1190 
qed 

58606  1191 

60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1192 
lemma 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1193 
fixes f :: "_ \<Rightarrow> real" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1194 
assumes f_measurable [measurable]: "f \<in> borel_measurable K" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1195 
and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1196 
and N [measurable]: "N \<in> measurable M (subprob_algebra K)" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1197 
and fin: "finite_measure M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1198 
and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ereal B'" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1199 
shows integrable_bind: "integrable (bind M N) f" (is ?integrable) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1200 
and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1201 
proof(case_tac [!] "space M = {}") 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1202 
assume [simp]: "space M \<noteq> {}" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1203 
interpret finite_measure M by(rule fin) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1204 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1205 
have "integrable (join (distr M (subprob_algebra K) N)) f" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1206 
using f_measurable f_bounded 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1207 
by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1208 
then show ?integrable by(simp add: bind_nonempty''[where N=K]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1209 

f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1210 
have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \<integral> M'. integral\<^sup>L M' f \<partial>distr M (subprob_algebra K) N" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1211 
using f_measurable f_bounded 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1212 
by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1213 
also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M" 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1214 
by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1215 
finally show ?integral by(simp add: bind_nonempty''[where N=K]) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1216 
qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty) 
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset

1217 

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

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

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

1222 
proof 

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

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

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

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

1229 
by (simp add: emeasure_space_1) 

1230 
qed 

1231 

1232 
lemma (in subprob_space) bind_in_space: 

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

59048  1234 
by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind) 
59000  1235 
unfold_locales 
1236 

1237 
lemma (in subprob_space) measure_bind: 

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

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

1240 
proof  

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

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

1243 

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

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

1246 
by (simp add: space_subprob_algebra) 

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

1248 
by (auto simp: emeasure_eq_measure subprob_measure_le_1) } 

1249 
note this[simp] 

1250 

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

1252 
using subprob_not_empty f X by (rule emeasure_bind) 

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

1254 
by (intro nn_integral_cong) simp 

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

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

1257 
measure_measurable_subprob_algebra2[OF _ f] pair_measureI X) 

1258 
(auto simp: measure_nonneg) 

1259 
finally show ?thesis 

1260 
by (simp add: Mf.emeasure_eq_measure) 

58606  1261 
qed 
1262 

1263 
lemma emeasure_bind_const: 

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

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

1266 
by (simp add: bind_nonempty emeasure_join nn_integral_distr 

1267 
space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg) 

1268 

1269 
lemma emeasure_bind_const': 

1270 
assumes "subprob_space M" "subprob_space N" 

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

1272 
using assms 

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

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

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

1276 
by (subst emeasure_bind_const) 

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

1278 
next 

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

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