author | paulson <lp15@cam.ac.uk> |
Tue, 10 Nov 2015 14:43:29 +0000 | |
changeset 61610 | 4f54d2759a0b |
parent 61609 | 77b453bd616f |
parent 61565 | 352c73a689da |
child 61634 | 48e2de1b1df5 |
permissions | -rw-r--r-- |
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 {* Sub-probability 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 |
59048 | 282 |
using [[simp_trace_new]] |
59000 | 283 |
by simp |
284 |
next |
|
285 |
case (add f g) |
|
286 |
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 | 287 |
by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) |
59000 | 288 |
ultimately show ?case |
289 |
by (simp add: ac_simps) |
|
290 |
next |
|
291 |
case (seq F) |
|
292 |
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" |
|
293 |
unfolding SUP_apply |
|
59048 | 294 |
by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) |
59000 | 295 |
ultimately show ?case |
296 |
by (simp add: ac_simps) |
|
297 |
qed |
|
298 |
||
59048 | 299 |
lemma nn_integral_measurable_subprob_algebra: |
300 |
"f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" |
|
301 |
by (subst nn_integral_max_0[symmetric]) |
|
302 |
(auto intro!: nn_integral_measurable_subprob_algebra') |
|
303 |
||
58606 | 304 |
lemma measurable_distr: |
305 |
assumes [measurable]: "f \<in> measurable M N" |
|
306 |
shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" |
|
307 |
proof (cases "space N = {}") |
|
308 |
assume not_empty: "space N \<noteq> {}" |
|
309 |
show ?thesis |
|
310 |
proof (rule measurable_subprob_algebra) |
|
311 |
fix A assume A: "A \<in> sets N" |
|
312 |
then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow> |
|
313 |
(\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)" |
|
314 |
by (intro measurable_cong) |
|
59048 | 315 |
(auto simp: emeasure_distr space_subprob_algebra |
316 |
intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"]) |
|
58606 | 317 |
also have "\<dots>" |
318 |
using A by (intro measurable_emeasure_subprob_algebra) simp |
|
319 |
finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" . |
|
59048 | 320 |
qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets) |
58606 | 321 |
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) |
322 |
||
59000 | 323 |
lemma emeasure_space_subprob_algebra[measurable]: |
324 |
"(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)" |
|
325 |
proof- |
|
326 |
have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M") |
|
327 |
by (rule measurable_emeasure_subprob_algebra) simp |
|
328 |
also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M" |
|
329 |
by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) |
|
330 |
finally show ?thesis . |
|
331 |
qed |
|
332 |
||
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
333 |
lemma integral_measurable_subprob_algebra: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
334 |
fixes f :: "_ \<Rightarrow> real" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
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
|
338 |
proof - |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
proof(rule measurable_cong) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
342 |
fix M |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
343 |
assume "M \<in> space (subprob_algebra N)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
344 |
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
|
345 |
by(simp_all add: space_subprob_algebra) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
346 |
interpret subprob_space M by fact |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
then have "integrable M f" using f_measurable |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
354 |
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
|
355 |
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
|
356 |
by(simp add: real_lebesgue_integral_def) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
357 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
358 |
also have "\<dots>" by measurable |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
359 |
finally show ?thesis . |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
360 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
361 |
|
59978 | 362 |
(* TODO: Rename. This name is too general -- Manuel *) |
59000 | 363 |
lemma measurable_pair_measure: |
364 |
assumes f: "f \<in> measurable M (subprob_algebra N)" |
|
365 |
assumes g: "g \<in> measurable M (subprob_algebra L)" |
|
366 |
shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))" |
|
367 |
proof (rule measurable_subprob_algebra) |
|
368 |
{ fix x assume "x \<in> space M" |
|
369 |
with measurable_space[OF f] measurable_space[OF g] |
|
370 |
have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)" |
|
371 |
by auto |
|
372 |
interpret F: subprob_space "f x" |
|
373 |
using fx by (simp add: space_subprob_algebra) |
|
374 |
interpret G: subprob_space "g x" |
|
375 |
using gx by (simp add: space_subprob_algebra) |
|
376 |
||
377 |
interpret pair_subprob_space "f x" "g x" .. |
|
378 |
show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales |
|
379 |
show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)" |
|
380 |
using fx gx by (simp add: space_subprob_algebra) |
|
381 |
||
382 |
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" |
|
383 |
using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) |
|
384 |
have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = |
|
385 |
emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))" |
|
386 |
by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure) |
|
387 |
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) = |
|
388 |
... - emeasure (f x \<Otimes>\<^sub>M g x) A" |
|
389 |
using emeasure_compl[OF _ P.emeasure_finite] |
|
390 |
unfolding sets_eq |
|
391 |
unfolding sets_eq_imp_space_eq[OF sets_eq] |
|
392 |
by (simp add: space_pair_measure G.emeasure_pair_measure_Times) |
|
393 |
note 1 2 sets_eq } |
|
394 |
note Times = this(1) and Compl = this(2) and sets_eq = this(3) |
|
395 |
||
396 |
fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)" |
|
397 |
show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M" |
|
398 |
using Int_stable_pair_measure_generator pair_measure_closed A |
|
399 |
unfolding sets_pair_measure |
|
400 |
proof (induct A rule: sigma_sets_induct_disjoint) |
|
401 |
case (basic A) then show ?case |
|
402 |
by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong) |
|
403 |
(auto intro!: measurable_emeasure_kernel f g) |
|
404 |
next |
|
405 |
case (compl A) |
|
406 |
then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)" |
|
407 |
by (auto simp: sets_pair_measure) |
|
408 |
have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - |
|
409 |
emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M") |
|
410 |
using compl(2) f g by measurable |
|
411 |
thus ?case by (simp add: Compl A cong: measurable_cong) |
|
412 |
next |
|
413 |
case (union A) |
|
414 |
then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A" |
|
415 |
by (auto simp: sets_pair_measure) |
|
416 |
then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow> |
|
417 |
(\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M" |
|
418 |
by (intro measurable_cong suminf_emeasure[symmetric]) |
|
419 |
(auto simp: sets_eq) |
|
420 |
also have "\<dots>" |
|
421 |
using union by auto |
|
422 |
finally show ?case . |
|
423 |
qed simp |
|
424 |
qed |
|
425 |
||
426 |
lemma restrict_space_measurable: |
|
427 |
assumes X: "X \<noteq> {}" "X \<in> sets K" |
|
428 |
assumes N: "N \<in> measurable M (subprob_algebra K)" |
|
429 |
shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))" |
|
430 |
proof (rule measurable_subprob_algebra) |
|
431 |
fix a assume a: "a \<in> space M" |
|
432 |
from N[THEN measurable_space, OF this] |
|
433 |
have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K" |
|
434 |
by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) |
|
435 |
then interpret subprob_space "N a" |
|
436 |
by simp |
|
437 |
show "subprob_space (restrict_space (N a) X)" |
|
438 |
proof |
|
439 |
show "space (restrict_space (N a) X) \<noteq> {}" |
|
440 |
using X by (auto simp add: space_restrict_space) |
|
441 |
show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1" |
|
442 |
using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1) |
|
443 |
qed |
|
444 |
show "sets (restrict_space (N a) X) = sets (restrict_space K X)" |
|
445 |
by (intro sets_restrict_space_cong) fact |
|
446 |
next |
|
447 |
fix A assume A: "A \<in> sets (restrict_space K X)" |
|
448 |
show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M" |
|
449 |
proof (subst measurable_cong) |
|
450 |
fix a assume "a \<in> space M" |
|
451 |
from N[THEN measurable_space, OF this] |
|
452 |
have [simp]: "sets (N a) = sets K" "space (N a) = space K" |
|
453 |
by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) |
|
454 |
show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)" |
|
455 |
using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps) |
|
456 |
next |
|
457 |
show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M" |
|
458 |
using A X |
|
459 |
by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra]) |
|
460 |
(auto simp: sets_restrict_space) |
|
461 |
qed |
|
462 |
qed |
|
463 |
||
58606 | 464 |
section {* Properties of return *} |
465 |
||
466 |
definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where |
|
467 |
"return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)" |
|
468 |
||
469 |
lemma space_return[simp]: "space (return M x) = space M" |
|
470 |
by (simp add: return_def) |
|
471 |
||
472 |
lemma sets_return[simp]: "sets (return M x) = sets M" |
|
473 |
by (simp add: return_def) |
|
474 |
||
475 |
lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L" |
|
476 |
by (simp cong: measurable_cong_sets) |
|
477 |
||
478 |
lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N" |
|
479 |
by (simp cong: measurable_cong_sets) |
|
480 |
||
59000 | 481 |
lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N" |
482 |
by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def) |
|
483 |
||
484 |
lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x" |
|
485 |
by (auto simp add: return_def dest: sets_eq_imp_space_eq) |
|
486 |
||
58606 | 487 |
lemma emeasure_return[simp]: |
488 |
assumes "A \<in> sets M" |
|
489 |
shows "emeasure (return M x) A = indicator A x" |
|
490 |
proof (rule emeasure_measure_of[OF return_def]) |
|
491 |
show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed) |
|
492 |
show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def) |
|
493 |
from assms show "A \<in> sets (return M x)" unfolding return_def by simp |
|
494 |
show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)" |
|
495 |
by (auto intro: countably_additiveI simp: suminf_indicator) |
|
496 |
qed |
|
497 |
||
498 |
lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)" |
|
499 |
by rule simp |
|
500 |
||
501 |
lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)" |
|
502 |
by (intro prob_space_return prob_space_imp_subprob_space) |
|
503 |
||
59000 | 504 |
lemma subprob_space_return_ne: |
505 |
assumes "space M \<noteq> {}" shows "subprob_space (return M x)" |
|
506 |
proof |
|
507 |
show "emeasure (return M x) (space (return M x)) \<le> 1" |
|
508 |
by (subst emeasure_return) (auto split: split_indicator) |
|
509 |
qed (simp, fact) |
|
510 |
||
511 |
lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x" |
|
512 |
unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator) |
|
513 |
||
58606 | 514 |
lemma AE_return: |
515 |
assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P" |
|
516 |
shows "(AE y in return M x. P y) \<longleftrightarrow> P x" |
|
517 |
proof - |
|
518 |
have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x" |
|
519 |
by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator) |
|
520 |
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)" |
|
521 |
by (rule AE_cong) auto |
|
522 |
finally show ?thesis . |
|
523 |
qed |
|
524 |
||
525 |
lemma nn_integral_return: |
|
526 |
assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M" |
|
527 |
shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x" |
|
528 |
proof- |
|
529 |
interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`]) |
|
530 |
have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms |
|
531 |
by (intro nn_integral_cong_AE) (auto simp: AE_return) |
|
532 |
also have "... = g x" |
|
533 |
using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp |
|
534 |
finally show ?thesis . |
|
535 |
qed |
|
536 |
||
59000 | 537 |
lemma integral_return: |
538 |
fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
539 |
assumes "x \<in> space M" "g \<in> borel_measurable M" |
|
540 |
shows "(\<integral>a. g a \<partial>return M x) = g x" |
|
541 |
proof- |
|
542 |
interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`]) |
|
543 |
have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms |
|
544 |
by (intro integral_cong_AE) (auto simp: AE_return) |
|
545 |
then show ?thesis |
|
546 |
using prob_space by simp |
|
547 |
qed |
|
548 |
||
549 |
lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)" |
|
58606 | 550 |
by (rule measurable_subprob_algebra) (auto simp: subprob_space_return) |
551 |
||
552 |
lemma distr_return: |
|
553 |
assumes "f \<in> measurable M N" and "x \<in> space M" |
|
554 |
shows "distr (return M x) N f = return N (f x)" |
|
555 |
using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr) |
|
556 |
||
59000 | 557 |
lemma return_restrict_space: |
558 |
"\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>" |
|
559 |
by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space) |
|
560 |
||
561 |
lemma measurable_distr2: |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset
|
562 |
assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N" |
59000 | 563 |
assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)" |
564 |
shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)" |
|
565 |
proof - |
|
566 |
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
|
567 |
\<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)" |
59000 | 568 |
proof (rule measurable_cong) |
569 |
fix x assume x: "x \<in> space L" |
|
570 |
have gx: "g x \<in> space (subprob_algebra M)" |
|
571 |
using measurable_space[OF g x] . |
|
572 |
then have [simp]: "sets (g x) = sets M" |
|
573 |
by (simp add: space_subprob_algebra) |
|
574 |
then have [simp]: "space (g x) = space M" |
|
575 |
by (rule sets_eq_imp_space_eq) |
|
576 |
let ?R = "return L x" |
|
577 |
from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N" |
|
578 |
by simp |
|
579 |
interpret subprob_space "g x" |
|
580 |
using gx by (simp add: space_subprob_algebra) |
|
581 |
have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)" |
|
582 |
by (simp add: space_pair_measure) |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset
|
583 |
show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r") |
59000 | 584 |
proof (rule measure_eqI) |
585 |
show "sets ?l = sets ?r" |
|
586 |
by simp |
|
587 |
next |
|
588 |
fix A assume "A \<in> sets ?l" |
|
589 |
then have A[measurable]: "A \<in> sets N" |
|
590 |
by simp |
|
591 |
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))" |
|
592 |
by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets) |
|
593 |
also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)" |
|
594 |
apply (subst emeasure_pair_measure_alt) |
|
595 |
apply (rule measurable_sets[OF _ A]) |
|
596 |
apply (auto simp add: f_M' cong: measurable_cong_sets) |
|
597 |
apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"]) |
|
598 |
apply (auto simp: space_subprob_algebra space_pair_measure) |
|
599 |
done |
|
600 |
also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)" |
|
601 |
by (subst nn_integral_return) |
|
602 |
(auto simp: x intro!: measurable_emeasure) |
|
603 |
also have "\<dots> = emeasure ?l A" |
|
604 |
by (simp add: emeasure_distr f_M' cong: measurable_cong_sets) |
|
605 |
finally show "emeasure ?l A = emeasure ?r A" .. |
|
606 |
qed |
|
607 |
qed |
|
608 |
also have "\<dots>" |
|
609 |
apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) |
|
610 |
apply (rule return_measurable) |
|
611 |
apply measurable |
|
612 |
done |
|
613 |
finally show ?thesis . |
|
614 |
qed |
|
615 |
||
616 |
lemma nn_integral_measurable_subprob_algebra2: |
|
59048 | 617 |
assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" |
59000 | 618 |
assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)" |
619 |
shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" |
|
620 |
proof - |
|
59048 | 621 |
note nn_integral_measurable_subprob_algebra[measurable] |
622 |
note measurable_distr2[measurable] |
|
59000 | 623 |
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 | 624 |
by measurable |
59000 | 625 |
then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" |
59048 | 626 |
by (rule measurable_cong[THEN iffD1, rotated]) |
627 |
(simp add: nn_integral_distr) |
|
59000 | 628 |
qed |
629 |
||
630 |
lemma emeasure_measurable_subprob_algebra2: |
|
631 |
assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" |
|
632 |
assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" |
|
633 |
shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" |
|
634 |
proof - |
|
635 |
{ fix x assume "x \<in> space M" |
|
636 |
then have "Pair x -` Sigma (space M) A = A x" |
|
637 |
by auto |
|
638 |
with sets_Pair1[OF A, of x] have "A x \<in> sets N" |
|
639 |
by auto } |
|
640 |
note ** = this |
|
641 |
||
642 |
have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)" |
|
643 |
by (auto simp: fun_eq_iff) |
|
644 |
have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" |
|
645 |
apply measurable |
|
646 |
apply (subst measurable_cong) |
|
647 |
apply (rule *) |
|
648 |
apply (auto simp: space_pair_measure) |
|
649 |
done |
|
650 |
then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M" |
|
651 |
by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L) |
|
652 |
then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" |
|
653 |
apply (rule measurable_cong[THEN iffD1, rotated]) |
|
654 |
apply (rule nn_integral_indicator) |
|
655 |
apply (simp add: subprob_measurableD[OF L] **) |
|
656 |
done |
|
657 |
qed |
|
658 |
||
659 |
lemma measure_measurable_subprob_algebra2: |
|
660 |
assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" |
|
661 |
assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" |
|
662 |
shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M" |
|
663 |
unfolding measure_def |
|
664 |
by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms]) |
|
665 |
||
58606 | 666 |
definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))" |
667 |
||
668 |
lemma select_sets1: |
|
669 |
"sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))" |
|
670 |
unfolding select_sets_def by (rule someI) |
|
671 |
||
672 |
lemma sets_select_sets[simp]: |
|
673 |
assumes sets: "sets M = sets (subprob_algebra N)" |
|
674 |
shows "sets (select_sets M) = sets N" |
|
675 |
unfolding select_sets_def |
|
676 |
proof (rule someI2) |
|
677 |
show "sets M = sets (subprob_algebra N)" |
|
678 |
by fact |
|
679 |
next |
|
680 |
fix L assume "sets M = sets (subprob_algebra L)" |
|
681 |
with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)" |
|
682 |
by (intro sets_eq_imp_space_eq) simp |
|
683 |
show "sets L = sets N" |
|
684 |
proof cases |
|
685 |
assume "space (subprob_algebra N) = {}" |
|
686 |
with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L] |
|
687 |
show ?thesis |
|
688 |
by (simp add: eq space_empty_iff) |
|
689 |
next |
|
690 |
assume "space (subprob_algebra N) \<noteq> {}" |
|
691 |
with eq show ?thesis |
|
692 |
by (fastforce simp add: space_subprob_algebra) |
|
693 |
qed |
|
694 |
qed |
|
695 |
||
696 |
lemma space_select_sets[simp]: |
|
697 |
"sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N" |
|
698 |
by (intro sets_eq_imp_space_eq sets_select_sets) |
|
699 |
||
700 |
section {* Join *} |
|
701 |
||
702 |
definition join :: "'a measure measure \<Rightarrow> 'a measure" where |
|
703 |
"join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" |
|
704 |
||
705 |
lemma |
|
706 |
shows space_join[simp]: "space (join M) = space (select_sets M)" |
|
707 |
and sets_join[simp]: "sets (join M) = sets (select_sets M)" |
|
708 |
by (simp_all add: join_def) |
|
709 |
||
710 |
lemma emeasure_join: |
|
59048 | 711 |
assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N" |
58606 | 712 |
shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" |
713 |
proof (rule emeasure_measure_of[OF join_def]) |
|
714 |
show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" |
|
715 |
proof (rule countably_additiveI) |
|
716 |
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A" |
|
717 |
have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)" |
|
59048 | 718 |
using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra) |
58606 | 719 |
also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" |
720 |
proof (rule nn_integral_cong) |
|
721 |
fix M' assume "M' \<in> space M" |
|
722 |
then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)" |
|
723 |
using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra) |
|
724 |
qed |
|
725 |
finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" . |
|
726 |
qed |
|
727 |
qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg) |
|
728 |
||
729 |
lemma measurable_join: |
|
730 |
"join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)" |
|
731 |
proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra) |
|
732 |
fix A assume "A \<in> sets N" |
|
733 |
let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))" |
|
734 |
have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B" |
|
735 |
proof (rule measurable_cong) |
|
736 |
fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))" |
|
737 |
then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')" |
|
738 |
by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`) |
|
739 |
qed |
|
740 |
also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B" |
|
59048 | 741 |
using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] |
58606 | 742 |
by (rule nn_integral_measurable_subprob_algebra) |
743 |
finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" . |
|
744 |
next |
|
745 |
assume [simp]: "space N \<noteq> {}" |
|
746 |
fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))" |
|
747 |
then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)" |
|
748 |
apply (intro nn_integral_mono) |
|
749 |
apply (auto simp: space_subprob_algebra |
|
750 |
dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) |
|
751 |
done |
|
752 |
with M show "subprob_space (join M)" |
|
753 |
by (intro subprob_spaceI) |
|
754 |
(auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1) |
|
755 |
next |
|
756 |
assume "\<not>(space N \<noteq> {})" |
|
757 |
thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff) |
|
758 |
qed (auto simp: space_subprob_algebra) |
|
759 |
||
59048 | 760 |
lemma nn_integral_join': |
761 |
assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" |
|
762 |
and M[measurable_cong]: "sets M = sets (subprob_algebra N)" |
|
58606 | 763 |
shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)" |
764 |
using f |
|
765 |
proof induct |
|
766 |
case (cong f g) |
|
767 |
moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g" |
|
768 |
by (intro nn_integral_cong cong) (simp add: M) |
|
769 |
moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)" |
|
770 |
by (intro nn_integral_cong cong) |
|
771 |
(auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
|
772 |
ultimately show ?case |
|
773 |
by simp |
|
774 |
next |
|
775 |
case (set A) |
|
776 |
moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" |
|
777 |
by (intro nn_integral_cong nn_integral_indicator) |
|
778 |
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) |
|
779 |
ultimately show ?case |
|
780 |
using M by (simp add: emeasure_join) |
|
781 |
next |
|
782 |
case (mult f c) |
|
783 |
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 | 784 |
using mult M M[THEN sets_eq_imp_space_eq] |
785 |
by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) |
|
58606 | 786 |
also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" |
59048 | 787 |
using nn_integral_measurable_subprob_algebra[OF mult(3)] |
58606 | 788 |
by (intro nn_integral_cmult mult) (simp add: M) |
789 |
also have "\<dots> = c * (integral\<^sup>N (join M) f)" |
|
790 |
by (simp add: mult) |
|
791 |
also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)" |
|
59048 | 792 |
using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets) |
58606 | 793 |
finally show ?case by simp |
794 |
next |
|
795 |
case (add f g) |
|
796 |
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 | 797 |
using add M M[THEN sets_eq_imp_space_eq] |
798 |
by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra) |
|
58606 | 799 |
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 | 800 |
using nn_integral_measurable_subprob_algebra[OF add(1)] |
801 |
using nn_integral_measurable_subprob_algebra[OF add(5)] |
|
58606 | 802 |
by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg) |
803 |
also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)" |
|
804 |
by (simp add: add) |
|
805 |
also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)" |
|
59048 | 806 |
using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets) |
58606 | 807 |
finally show ?case by (simp add: ac_simps) |
808 |
next |
|
809 |
case (seq F) |
|
810 |
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 | 811 |
using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply |
58606 | 812 |
by (intro nn_integral_cong nn_integral_monotone_convergence_SUP) |
59048 | 813 |
(auto simp add: space_subprob_algebra) |
58606 | 814 |
also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)" |
59048 | 815 |
using nn_integral_measurable_subprob_algebra[OF seq(1)] seq |
58606 | 816 |
by (intro nn_integral_monotone_convergence_SUP) |
817 |
(simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono ) |
|
818 |
also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))" |
|
819 |
by (simp add: seq) |
|
820 |
also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)" |
|
59048 | 821 |
using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) |
822 |
(simp_all add: M cong: measurable_cong_sets) |
|
58606 | 823 |
finally show ?case by (simp add: ac_simps) |
824 |
qed |
|
825 |
||
59048 | 826 |
lemma nn_integral_join: |
827 |
assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)" |
|
828 |
shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)" |
|
829 |
apply (subst (1 3) nn_integral_max_0[symmetric]) |
|
830 |
apply (rule nn_integral_join') |
|
831 |
apply (auto simp: f) |
|
832 |
done |
|
833 |
||
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
834 |
lemma measurable_join1: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
835 |
"\<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
|
836 |
\<Longrightarrow> f \<in> measurable (join M) K" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
837 |
by(simp add: measurable_def) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
838 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
839 |
lemma |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
840 |
fixes f :: "_ \<Rightarrow> real" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
841 |
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
|
842 |
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
|
843 |
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
|
844 |
and fin: "finite_measure M" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
845 |
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
|
846 |
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
|
847 |
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
|
848 |
proof(case_tac [!] "space N = {}") |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
849 |
assume *: "space N = {}" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
850 |
show ?integrable |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
851 |
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
|
852 |
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
|
853 |
proof(rule integral_cong) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
854 |
fix M' |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
855 |
assume "M' \<in> space M" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
856 |
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
|
857 |
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
|
858 |
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
|
859 |
qed simp |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
860 |
then show ?integral |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
861 |
using M * by(simp add: integral_empty) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
862 |
next |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
863 |
assume *: "space N \<noteq> {}" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
864 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
865 |
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
|
866 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
867 |
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
|
868 |
by(rule measurable_join1) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
869 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
870 |
{ fix f M' |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
871 |
assume [measurable]: "f \<in> borel_measurable N" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
872 |
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
|
873 |
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
|
874 |
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
|
875 |
proof(rule AE_I2) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
876 |
fix x |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
877 |
assume "x \<in> space M'" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
878 |
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
|
879 |
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
|
880 |
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
|
881 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
882 |
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
|
883 |
by(rule nn_integral_mono_AE) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
884 |
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
|
885 |
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
|
886 |
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
|
887 |
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
|
888 |
note bounded1 = this |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
889 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
890 |
have bounded: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
891 |
"\<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
|
892 |
\<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
|
893 |
proof - |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
894 |
fix f |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
895 |
assume [measurable]: "f \<in> borel_measurable N" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
896 |
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
|
897 |
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
|
898 |
by(rule nn_integral_join[OF _ M]) simp |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
899 |
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
|
900 |
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
|
901 |
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
|
902 |
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
|
903 |
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
|
904 |
finally show "?thesis f" by simp |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
905 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
906 |
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
|
907 |
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
|
908 |
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
|
909 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
910 |
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
|
911 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
912 |
note [measurable] = nn_integral_measurable_subprob_algebra |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
913 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
914 |
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
|
915 |
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
|
916 |
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
|
917 |
by(simp add: nn_integral_join[OF _ M]) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
918 |
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
|
919 |
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
|
920 |
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
|
921 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
922 |
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
|
923 |
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
|
924 |
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
|
925 |
by(simp add: nn_integral_join[OF _ M]) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
926 |
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
|
927 |
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
|
928 |
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
|
929 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
930 |
have f_pos1: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
931 |
"\<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
|
932 |
\<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
|
933 |
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
|
934 |
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
|
935 |
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
|
936 |
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
|
937 |
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
|
938 |
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
|
939 |
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
|
940 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
941 |
have f_neg1: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
942 |
"\<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
|
943 |
\<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
|
944 |
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
|
945 |
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
|
946 |
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
|
947 |
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
|
948 |
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
|
949 |
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
|
950 |
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
|
951 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
952 |
from \<open>?integrable\<close> |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
953 |
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
|
954 |
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
|
955 |
also note int_f |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
956 |
also note int_mf |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
957 |
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
|
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 |
((\<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
|
960 |
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
|
961 |
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
|
962 |
using f_pos |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
963 |
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
|
964 |
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
|
965 |
using f_neg |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
966 |
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
|
967 |
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
|
968 |
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
|
969 |
\<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
|
970 |
by simp |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
971 |
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
|
972 |
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
|
973 |
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
|
974 |
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
|
975 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
976 |
fix M' |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
977 |
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
|
978 |
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
|
979 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
980 |
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
|
981 |
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
|
982 |
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
|
983 |
have "integrable M' f" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
984 |
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
|
985 |
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
|
986 |
by(simp add: real_lebesgue_integral_def) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
987 |
qed simp_all |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
988 |
finally show ?integral by simp |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
989 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
990 |
|
58606 | 991 |
lemma join_assoc: |
59048 | 992 |
assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))" |
58606 | 993 |
shows "join (distr M (subprob_algebra N) join) = join (join M)" |
994 |
proof (rule measure_eqI) |
|
995 |
fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))" |
|
996 |
then have A: "A \<in> sets N" by simp |
|
997 |
show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A" |
|
998 |
using measurable_join[of N] |
|
999 |
by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg |
|
59048 | 1000 |
sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M] |
1001 |
intro!: nn_integral_cong emeasure_join) |
|
58606 | 1002 |
qed (simp add: M) |
1003 |
||
1004 |
lemma join_return: |
|
1005 |
assumes "sets M = sets N" and "subprob_space M" |
|
1006 |
shows "join (return (subprob_algebra N) M) = M" |
|
1007 |
by (rule measure_eqI) |
|
1008 |
(simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra |
|
1009 |
measurable_emeasure_subprob_algebra nn_integral_return assms) |
|
1010 |
||
1011 |
lemma join_return': |
|
1012 |
assumes "sets N = sets M" |
|
1013 |
shows "join (distr M (subprob_algebra N) (return N)) = M" |
|
1014 |
apply (rule measure_eqI) |
|
1015 |
apply (simp add: assms) |
|
1016 |
apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)") |
|
1017 |
apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) |
|
1018 |
apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable) |
|
1019 |
done |
|
1020 |
||
1021 |
lemma join_distr_distr: |
|
1022 |
fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure" |
|
1023 |
assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N" |
|
1024 |
shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l") |
|
1025 |
proof (rule measure_eqI) |
|
1026 |
fix A assume "A \<in> sets ?r" |
|
1027 |
hence A_in_N: "A \<in> sets N" by simp |
|
1028 |
||
1029 |
from assms have "f \<in> measurable (join M) N" |
|
1030 |
by (simp cong: measurable_cong_sets) |
|
1031 |
moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" |
|
1032 |
by (intro measurable_sets) simp_all |
|
1033 |
ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M" |
|
1034 |
by (simp_all add: A_in_N emeasure_distr emeasure_join assms) |
|
1035 |
||
1036 |
also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N |
|
1037 |
proof (intro nn_integral_cong, subst emeasure_distr) |
|
1038 |
fix M' assume "M' \<in> space M" |
|
1039 |
from assms have "space M = space (subprob_algebra R)" |
|
1040 |
using sets_eq_imp_space_eq by blast |
|
1041 |
with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast |
|
1042 |
show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms) |
|
1043 |
have "space M' = space R" by (rule sets_eq_imp_space_eq) simp |
|
1044 |
thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp |
|
1045 |
qed |
|
1046 |
||
1047 |
also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)" |
|
1048 |
by (simp cong: measurable_cong_sets add: assms measurable_distr) |
|
1049 |
hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = |
|
1050 |
emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A" |
|
1051 |
by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra) |
|
1052 |
finally show "emeasure ?r A = emeasure ?l A" .. |
|
1053 |
qed simp |
|
1054 |
||
1055 |
definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where |
|
1056 |
"bind M f = (if space M = {} then count_space {} else |
|
1057 |
join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))" |
|
1058 |
||
1059 |
adhoc_overloading Monad_Syntax.bind bind |
|
1060 |
||
1061 |
lemma bind_empty: |
|
1062 |
"space M = {} \<Longrightarrow> bind M f = count_space {}" |
|
1063 |
by (simp add: bind_def) |
|
1064 |
||
1065 |
lemma bind_nonempty: |
|
1066 |
"space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)" |
|
1067 |
by (simp add: bind_def) |
|
1068 |
||
1069 |
lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}" |
|
1070 |
by (auto simp: bind_def) |
|
1071 |
||
1072 |
lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}" |
|
1073 |
by (simp add: bind_def) |
|
1074 |
||
59048 | 1075 |
lemma sets_bind[simp, measurable_cong]: |
1076 |
assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}" |
|
58606 | 1077 |
shows "sets (bind M f) = sets N" |
59048 | 1078 |
using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq) |
58606 | 1079 |
|
1080 |
lemma space_bind[simp]: |
|
59048 | 1081 |
assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}" |
58606 | 1082 |
shows "space (bind M f) = space N" |
59048 | 1083 |
using assms by (intro sets_eq_imp_space_eq sets_bind) |
58606 | 1084 |
|
1085 |
lemma bind_cong: |
|
1086 |
assumes "\<forall>x \<in> space M. f x = g x" |
|
1087 |
shows "bind M f = bind M g" |
|
1088 |
proof (cases "space M = {}") |
|
1089 |
assume "space M \<noteq> {}" |
|
1090 |
hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast |
|
1091 |
with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast |
|
1092 |
with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong) |
|
1093 |
qed (simp add: bind_empty) |
|
1094 |
||
1095 |
lemma bind_nonempty': |
|
1096 |
assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M" |
|
1097 |
shows "bind M f = join (distr M (subprob_algebra N) f)" |
|
1098 |
using assms |
|
1099 |
apply (subst bind_nonempty, blast) |
|
1100 |
apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast) |
|
1101 |
apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]]) |
|
1102 |
done |
|
1103 |
||
1104 |
lemma bind_nonempty'': |
|
1105 |
assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}" |
|
1106 |
shows "bind M f = join (distr M (subprob_algebra N) f)" |
|
1107 |
using assms by (auto intro: bind_nonempty') |
|
1108 |
||
1109 |
lemma emeasure_bind: |
|
1110 |
"\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk> |
|
1111 |
\<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" |
|
1112 |
by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra) |
|
1113 |
||
59048 | 1114 |
lemma nn_integral_bind: |
1115 |
assumes f: "f \<in> borel_measurable B" |
|
59000 | 1116 |
assumes N: "N \<in> measurable M (subprob_algebra B)" |
1117 |
shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)" |
|
1118 |
proof cases |
|
1119 |
assume M: "space M \<noteq> {}" show ?thesis |
|
1120 |
unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr] |
|
1121 |
by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]]) |
|
1122 |
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space) |
|
1123 |
||
1124 |
lemma AE_bind: |
|
1125 |
assumes P[measurable]: "Measurable.pred B P" |
|
1126 |
assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)" |
|
1127 |
shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)" |
|
1128 |
proof cases |
|
1129 |
assume M: "space M = {}" show ?thesis |
|
1130 |
unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space) |
|
1131 |
next |
|
1132 |
assume M: "space M \<noteq> {}" |
|
59048 | 1133 |
note sets_kernel[OF N, simp] |
59000 | 1134 |
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 | 1135 |
by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator) |
59000 | 1136 |
|
1137 |
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 | 1138 |
by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B] |
59000 | 1139 |
del: nn_integral_indicator) |
1140 |
also have "\<dots> = (AE x in M. AE y in N x. P y)" |
|
1141 |
apply (subst nn_integral_0_iff_AE) |
|
1142 |
apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra]) |
|
1143 |
apply measurable |
|
1144 |
apply (intro eventually_subst AE_I2) |
|
59048 | 1145 |
apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N] |
1146 |
intro!: AE_iff_measurable[symmetric]) |
|
59000 | 1147 |
done |
1148 |
finally show ?thesis . |
|
1149 |
qed |
|
1150 |
||
1151 |
lemma measurable_bind': |
|
1152 |
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
|
1153 |
M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" |
59000 | 1154 |
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" |
1155 |
proof (subst measurable_cong) |
|
1156 |
fix x assume x_in_M: "x \<in> space M" |
|
1157 |
with assms have "space (f x) \<noteq> {}" |
|
1158 |
by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty) |
|
1159 |
moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)" |
|
1160 |
by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl]) |
|
1161 |
(auto dest: measurable_Pair2) |
|
1162 |
ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" |
|
1163 |
by (simp_all add: bind_nonempty'') |
|
1164 |
next |
|
1165 |
show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)" |
|
1166 |
apply (rule measurable_compose[OF _ measurable_join]) |
|
1167 |
apply (rule measurable_distr2[OF M2 M1]) |
|
1168 |
done |
|
1169 |
qed |
|
58606 | 1170 |
|
59048 | 1171 |
lemma measurable_bind[measurable (raw)]: |
59000 | 1172 |
assumes M1: "f \<in> measurable M (subprob_algebra N)" and |
1173 |
M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" |
|
1174 |
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" |
|
1175 |
using assms by (auto intro: measurable_bind' simp: measurable_split_conv) |
|
1176 |
||
1177 |
lemma measurable_bind2: |
|
1178 |
assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)" |
|
1179 |
shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)" |
|
1180 |
using assms by (intro measurable_bind' measurable_const) auto |
|
1181 |
||
1182 |
lemma subprob_space_bind: |
|
1183 |
assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)" |
|
1184 |
shows "subprob_space (M \<guillemotright>= f)" |
|
1185 |
proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"]) |
|
1186 |
show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" |
|
1187 |
by (rule measurable_bind, rule measurable_ident_sets, rule refl, |
|
1188 |
rule measurable_compose[OF measurable_snd assms(2)]) |
|
1189 |
from assms(1) show "M \<in> space (subprob_algebra M)" |
|
1190 |
by (simp add: space_subprob_algebra) |
|
1191 |
qed |
|
58606 | 1192 |
|
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1193 |
lemma |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1194 |
fixes f :: "_ \<Rightarrow> real" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1195 |
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
|
1196 |
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
|
1197 |
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
|
1198 |
and fin: "finite_measure M" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1199 |
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
|
1200 |
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
|
1201 |
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
|
1202 |
proof(case_tac [!] "space M = {}") |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1203 |
assume [simp]: "space M \<noteq> {}" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1204 |
interpret finite_measure M by(rule fin) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1205 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1206 |
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
|
1207 |
using f_measurable f_bounded |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1208 |
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
|
1209 |
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
|
1210 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1211 |
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
|
1212 |
using f_measurable f_bounded |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1213 |
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
|
1214 |
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
|
1215 |
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
|
1216 |
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
|
1217 |
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
|
1218 |
|
59000 | 1219 |
lemma (in prob_space) prob_space_bind: |
1220 |
assumes ae: "AE x in M. prob_space (N x)" |
|
1221 |
and N[measurable]: "N \<in> measurable M (subprob_algebra S)" |
|
1222 |
shows "prob_space (M \<guillemotright>= N)" |
|
1223 |
proof |
|
1224 |
have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)" |
|
1225 |
by (subst emeasure_bind[where N=S]) |
|
59048 | 1226 |
(auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong) |
59000 | 1227 |
also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)" |
1228 |
using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1) |
|
1229 |
finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1" |
|
1230 |
by (simp add: emeasure_space_1) |
|
1231 |
qed |
|
1232 |
||
1233 |
lemma (in subprob_space) bind_in_space: |
|
1234 |
"A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)" |
|
59048 | 1235 |
by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind) |
59000 | 1236 |
unfold_locales |
1237 |
||
1238 |
lemma (in subprob_space) measure_bind: |
|
1239 |
assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N" |
|
1240 |
shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M" |
|
1241 |
proof - |
|
1242 |
interpret Mf: subprob_space "M \<guillemotright>= f" |
|
1243 |
by (rule subprob_space_bind[OF _ f]) unfold_locales |
|
1244 |
||
1245 |
{ fix x assume "x \<in> space M" |
|
1246 |
from f[THEN measurable_space, OF this] interpret subprob_space "f x" |
|
1247 |
by (simp add: space_subprob_algebra) |
|
1248 |
have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1" |
|
1249 |
by (auto simp: emeasure_eq_measure subprob_measure_le_1) } |
|
1250 |
note this[simp] |
|
1251 |
||
1252 |
have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" |
|
1253 |
using subprob_not_empty f X by (rule emeasure_bind) |
|
1254 |
also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M" |
|
1255 |
by (intro nn_integral_cong) simp |
|
1256 |
also have "\<dots> = \<integral>x. measure (f x) X \<partial>M" |
|
1257 |
by (intro nn_integral_eq_integral integrable_const_bound[where B=1] |
|
1258 |
measure_measurable_subprob_algebra2[OF _ f] pair_measureI X) |
|
1259 |
(auto simp: measure_nonneg) |
|
1260 |
finally show ?thesis |
|
1261 |
by (simp add: Mf.emeasure_eq_measure) |
|
58606 | 1262 |
qed |
1263 |
||
1264 |
lemma emeasure_bind_const: |
|
1265 |
"space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> |
|
1266 |
emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" |
|
1267 |
by (simp add: bind_nonempty emeasure_join nn_integral_distr |
|
1268 |
space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg) |
|
1269 |
||
1270 |
lemma emeasure_bind_const': |
|
1271 |
assumes "subprob_space M" "subprob_space N" |
|
1272 |
shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" |
|
1273 |
using assms |
|
1274 |
proof (case_tac "X \<in> sets N") |
|
1275 |
fix X assume "X \<in> sets N" |
|
1276 |
thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms |
|
1277 |
by (subst emeasure_bind_const) |
|
1278 |
(simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1) |
|
1279 |
next |
|
1280 |
fix X assume "X \<notin> sets N" |
|
1281 |
with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" |
|
1282 |
by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty |
|
1283 |
space_subprob_algebra emeasure_notin_sets) |
|
1284 |
qed |
|
1285 |
||
1286 |
lemma emeasure_bind_const_prob_space: |
|
1287 |
assumes "prob_space M" "subprob_space N" |
|
1288 |
shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X" |
|
1289 |
using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space |
|
1290 |
prob_space.emeasure_space_1) |
|
1291 |
||
59000 | 1292 |
lemma bind_return: |
1293 |
assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M" |
|
1294 |
shows "bind (return M x) f = f x" |
|
1295 |
using sets_kernel[OF assms] assms |
|
1296 |
by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty' |
|
1297 |
cong: subprob_algebra_cong) |
|
1298 |
||
1299 |
lemma bind_return': |
|
1300 |
shows "bind M (return M) = M" |
|
1301 |
by (cases "space M = {}") |
|
1302 |
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' |
|
1303 |
cong: subprob_algebra_cong) |
|
1304 |
||
1305 |
lemma distr_bind: |
|
1306 |
assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}" |
|
1307 |
assumes f: "f \<in> measurable K R" |
|
1308 |
shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))" |
|
1309 |
unfolding bind_nonempty''[OF N] |
|
1310 |
apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)]) |
|
1311 |
apply (rule f) |
|
1312 |
apply (simp add: join_distr_distr[OF _ f, symmetric]) |
|
1313 |
apply (subst distr_distr[OF measurable_distr, OF f N(1)]) |
|
1314 |
apply (simp add: comp_def) |
|
1315 |
done |
|
1316 |
||
1317 |
lemma bind_distr: |
|
1318 |
assumes f[measurable]: "f \<in> measurable M X" |
|
1319 |
assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}" |
|
1320 |
shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))" |
|
1321 |
proof - |
|
1322 |
have "space X \<noteq> {}" "space M \<noteq> {}" |
|
1323 |
using `space M \<noteq> {}` f[THEN measurable_space] by auto |
|
1324 |
then show ?thesis |
|
1325 |
by (simp add: bind_nonempty''[where N=K] distr_distr comp_def) |
|
1326 |
qed |
|
1327 |
||
1328 |
lemma bind_count_space_singleton: |
|
1329 |
assumes "subprob_space (f x)" |
|
1330 |
shows "count_space {x} \<guillemotright>= f = f x" |
|
1331 |
proof- |
|
1332 |
have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto |
|
1333 |
have "count_space {x} = return (count_space {x}) x" |
|
1334 |
by (intro measure_eqI) (auto dest: A) |
|
1335 |
also have "... \<guillemotright>= f = f x" |
|
1336 |
by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms) |
|
1337 |
finally show ?thesis . |
|
1338 |
qed |
|
1339 |
||
1340 |
lemma restrict_space_bind: |
|
1341 |
assumes N: "N \<in> measurable M (subprob_algebra K)" |
|
1342 |
assumes "space M \<noteq> {}" |
|
1343 |
assumes X[simp]: "X \<in> sets K" "X \<noteq> {}" |
|
1344 |
shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)" |
|
1345 |
proof (rule measure_eqI) |
|
59048 | 1346 |
note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp] |
1347 |
note N_space = sets_eq_imp_space_eq[OF N_sets, simp] |
|
1348 |
show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))" |
|
1349 |
by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]]) |
|
59000 | 1350 |
fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)" |
1351 |
with X have "A \<in> sets K" "A \<subseteq> X" |
|
59048 | 1352 |
by (auto simp: sets_restrict_space) |
59000 | 1353 |
then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A" |
1354 |
using assms |
|
1355 |
apply (subst emeasure_restrict_space) |
|
59048 | 1356 |
apply (simp_all add: emeasure_bind[OF assms(2,1)]) |
59000 | 1357 |
apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]]) |
1358 |
apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra |
|
1359 |
intro!: nn_integral_cong dest!: measurable_space) |
|
1360 |
done |
|
59048 | 1361 |
qed |
59000 | 1362 |
|
60067
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1363 |
lemma bind_restrict_space: |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1364 |
assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1365 |
and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1366 |
shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1367 |
(is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f") |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1368 |
proof - |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1369 |
let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1370 |
let ?x = "Eps ?P" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1371 |
let ?c = "null_measure (f ?x)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1372 |
from A have "?P ?x" by-(rule someI_ex, blast) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1373 |
hence "?x \<in> space (restrict_space M A)" by(simp add: space_restrict_space) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1374 |
with f have "f ?x \<in> space (subprob_algebra N)" by(rule measurable_space) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1375 |
hence sps: "subprob_space (f ?x)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1376 |
and sets: "sets (f ?x) = sets N" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1377 |
by(simp_all add: space_subprob_algebra) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1378 |
have "space (f ?x) \<noteq> {}" using sps by(rule subprob_space.subprob_not_empty) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1379 |
moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1380 |
ultimately have c: "?c \<in> space (subprob_algebra N)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1381 |
by(simp add: space_subprob_algebra subprob_space_null_measure) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1382 |
from f A c have f': "?f \<in> measurable M (subprob_algebra N)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1383 |
by(simp add: measurable_restrict_space_iff) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1384 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1385 |
from A have [simp]: "space M \<noteq> {}" by blast |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1386 |
|
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1387 |
have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1388 |
using assms by(simp add: space_restrict_space bind_nonempty'') |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1389 |
also have "\<dots> = join (distr M (subprob_algebra N) ?f)" |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1390 |
by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong) |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1391 |
also have "\<dots> = ?rhs" using f' by(simp add: bind_nonempty'') |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1392 |
finally show ?thesis . |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1393 |
qed |
f1a5bcf5658f
lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents:
59978
diff
changeset
|
1394 |
|
58606 | 1395 |
lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N" |
1396 |
by (intro measure_eqI) |
|
1397 |
(simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space) |
|
1398 |
||
1399 |
lemma bind_return_distr: |
|
1400 |
"space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f" |
|
1401 |
apply (simp add: bind_nonempty) |
|
1402 |
apply (subst subprob_algebra_cong) |
|
1403 |
apply (rule sets_return) |
|
1404 |
apply (subst distr_distr[symmetric]) |
|
1405 |
apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') |
|
1406 |
done |
|
1407 |
||
61359
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
61169
diff
changeset
|
1408 |
lemma bind_return_distr': |
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
61169
diff
changeset
|
1409 |
"space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (\<lambda>x. return N (f x)) = distr M N f" |
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
61169
diff
changeset
|
1410 |
using bind_return_distr[of M f N] by (simp add: comp_def) |
e985b52c3eb3
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
hoelzl
parents:
61169
diff
changeset
|
1411 |
|
58606 | 1412 |
lemma bind_assoc: |
1413 |
fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure" |
|
1414 |
assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)" |
|
1415 |
shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)" |
|
1416 |
proof (cases "space M = {}") |
|
1417 |
assume [simp]: "space M \<noteq> {}" |
|
1418 |
from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}" |
|
1419 |
by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) |
|
1420 |
from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" |
|
1421 |
by (simp add: sets_kernel) |
|
1422 |
have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast |
|
1423 |
note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]] |
|
1424 |
sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]] |
|
1425 |
note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)] |
|
1426 |
||
1427 |
have "bind M (\<lambda>x. bind (f x) g) = |
|
1428 |
join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))" |
|
1429 |
by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def |
|
1430 |
cong: subprob_algebra_cong distr_cong) |
|
1431 |
also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) = |
|
1432 |
distr (distr (distr M (subprob_algebra N) f) |
|
1433 |
(subprob_algebra (subprob_algebra R)) |
|
1434 |
(\<lambda>x. distr x (subprob_algebra R) g)) |
|
1435 |
(subprob_algebra R) join" |
|
1436 |
apply (subst distr_distr, |
|
1437 |
(blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+ |
|
1438 |
apply (simp add: o_assoc) |
|
1439 |
done |
|
1440 |
also have "join ... = bind (bind M f) g" |
|
1441 |
by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong) |
|
1442 |
finally show ?thesis .. |
|
1443 |
qed (simp add: bind_empty) |
|
1444 |
||
1445 |
lemma double_bind_assoc: |
|
1446 |
assumes Mg: "g \<in> measurable N (subprob_algebra N')" |
|
1447 |
assumes Mf: "f \<in> measurable M (subprob_algebra M')" |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61359
diff
changeset
|
1448 |
assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N" |
58606 | 1449 |
shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g" |
1450 |
proof- |
|
1451 |
have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = |
|
1452 |
do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}" |
|
1453 |
using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg |
|
1454 |
measurable_compose[OF _ return_measurable] simp: measurable_split_conv) |
|
1455 |
also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable |
|
1456 |
hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = |
|
1457 |
do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}" |
|
1458 |
apply (intro ballI bind_cong bind_assoc) |
|
1459 |
apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp) |
|
1460 |
apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg) |
|
1461 |
done |
|
1462 |
also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'" |
|
1463 |
by (intro sets_eq_imp_space_eq sets_kernel[OF Mf]) |
|
1464 |
with measurable_space[OF Mh] |
|
1465 |
have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}" |
|
1466 |
by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure) |
|
1467 |
finally show ?thesis .. |
|
1468 |
qed |
|
1469 |
||
59048 | 1470 |
lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)" |
1471 |
by (simp add: space_subprob_algebra) unfold_locales |
|
1472 |
||
59000 | 1473 |
lemma (in pair_prob_space) pair_measure_eq_bind: |
1474 |
"(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" |
|
1475 |
proof (rule measure_eqI) |
|
1476 |
have ps_M2: "prob_space M2" by unfold_locales |
|
1477 |
note return_measurable[measurable] |
|
1478 |
show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" |
|
59048 | 1479 |
by (simp_all add: M1.not_empty M2.not_empty) |
59000 | 1480 |
fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" |
1481 |
show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A" |
|
59048 | 1482 |
by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] |
59000 | 1483 |
intro!: nn_integral_cong) |
1484 |
qed |
|
1485 |
||
1486 |
lemma (in pair_prob_space) bind_rotate: |
|
1487 |
assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)" |
|
1488 |
shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))" |
|
1489 |
proof - |
|
1490 |
interpret swap: pair_prob_space M2 M1 by unfold_locales |
|
1491 |
note measurable_bind[where N="M2", measurable] |
|
1492 |
note measurable_bind[where N="M1", measurable] |
|
1493 |
have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)" |
|
1494 |
by (auto simp: space_subprob_algebra) unfold_locales |
|
1495 |
have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = |
|
1496 |
(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)" |
|
1497 |
by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N]) |
|
1498 |
also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)" |
|
1499 |
unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] .. |
|
1500 |
also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)" |
|
1501 |
unfolding swap.pair_measure_eq_bind[symmetric] |
|
1502 |
by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong) |
|
1503 |
also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))" |
|
1504 |
by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N]) |
|
1505 |
finally show ?thesis . |
|
1506 |
qed |
|
1507 |
||
58608 | 1508 |
section {* Measures form a $\omega$-chain complete partial order *} |
58606 | 1509 |
|
1510 |
definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where |
|
1511 |
"SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)" |
|
1512 |
||
1513 |
lemma |
|
1514 |
assumes const: "\<And>i j. sets (M i) = sets (M j)" |
|
1515 |
shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp) |
|
1516 |
and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st) |
|
1517 |
proof - |
|
1518 |
have "(\<Union>i. sets (M i)) = sets (M i)" |
|
1519 |
using const by auto |
|
1520 |
moreover have "(\<Union>i. space (M i)) = space (M i)" |
|
1521 |
using const[THEN sets_eq_imp_space_eq] by auto |
|
1522 |
moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))" |
|
1523 |
by (auto dest: sets.sets_into_space) |
|
1524 |
ultimately show ?sp ?st |
|
1525 |
by (simp_all add: SUP_measure_def) |
|
1526 |
qed |
|
1527 |
||
1528 |
lemma emeasure_SUP_measure: |
|
1529 |
assumes const: "\<And>i j. sets (M i) = sets (M j)" |
|
1530 |
and mono: "mono (\<lambda>i. emeasure (M i))" |
|
1531 |
shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)" |
|
1532 |
proof cases |
|
1533 |
assume "A \<in> sets (SUP_measure M)" |
|
1534 |
show ?thesis |
|
1535 |
proof (rule emeasure_measure_of[OF SUP_measure_def]) |
|
1536 |
show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)" |
|
1537 |
proof (rule countably_additiveI) |
|
1538 |
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)" |
|
1539 |
then have "\<And>i j. A i \<in> sets (M j)" |
|
1540 |
using sets_SUP_measure[of M, OF const] by simp |
|
1541 |
moreover assume "disjoint_family A" |
|
1542 |
ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))" |
|
1543 |
using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure) |
|
1544 |
qed |
|
1545 |
show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)" |
|
1546 |
by (auto simp: positive_def intro: SUP_upper2) |
|
1547 |
show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))" |
|
1548 |
using sets.sets_into_space by auto |
|
1549 |
qed fact |
|
1550 |
next |
|
1551 |
assume "A \<notin> sets (SUP_measure M)" |
|
1552 |
with sets_SUP_measure[of M, OF const] show ?thesis |
|
1553 |
by (simp add: emeasure_notin_sets) |
|
1554 |
qed |
|
1555 |
||
59425 | 1556 |
lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M" |
1557 |
by (cases "space M = {}") |
|
1558 |
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' |
|
1559 |
cong: subprob_algebra_cong) |
|
1560 |
||
1561 |
lemma (in prob_space) distr_const[simp]: |
|
1562 |
"c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c" |
|
1563 |
by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1) |
|
1564 |
||
1565 |
lemma return_count_space_eq_density: |
|
1566 |
"return (count_space M) x = density (count_space M) (indicator {x})" |
|
1567 |
by (rule measure_eqI) |
|
1568 |
(auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator) |
|
1569 |
||
58606 | 1570 |
end |