58606
|
1 |
(* Title: HOL/Probability/Stream_Space.thy
|
|
2 |
Author: Johannes Hölzl, TU München *)
|
|
3 |
|
58588
|
4 |
theory Stream_Space
|
|
5 |
imports
|
|
6 |
Infinite_Product_Measure
|
|
7 |
"~~/src/HOL/Datatype_Examples/Stream"
|
|
8 |
begin
|
|
9 |
|
|
10 |
lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
|
|
11 |
by (cases s) simp
|
|
12 |
|
|
13 |
lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
|
|
14 |
by (cases n) simp_all
|
|
15 |
|
|
16 |
definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
|
|
17 |
"to_stream X = smap X nats"
|
|
18 |
|
|
19 |
lemma to_stream_nat_case: "to_stream (case_nat x X) = x ## to_stream X"
|
|
20 |
unfolding to_stream_def
|
|
21 |
by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def)
|
|
22 |
|
|
23 |
definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where
|
|
24 |
"stream_space M =
|
|
25 |
distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream"
|
|
26 |
|
|
27 |
lemma space_stream_space: "space (stream_space M) = streams (space M)"
|
|
28 |
by (simp add: stream_space_def)
|
|
29 |
|
|
30 |
lemma streams_stream_space[intro]: "streams (space M) \<in> sets (stream_space M)"
|
|
31 |
using sets.top[of "stream_space M"] by (simp add: space_stream_space)
|
|
32 |
|
|
33 |
lemma stream_space_Stream:
|
|
34 |
"x ## \<omega> \<in> space (stream_space M) \<longleftrightarrow> x \<in> space M \<and> \<omega> \<in> space (stream_space M)"
|
|
35 |
by (simp add: space_stream_space streams_Stream)
|
|
36 |
|
|
37 |
lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
|
|
38 |
unfolding stream_space_def by (rule distr_cong) auto
|
|
39 |
|
|
40 |
lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
|
|
41 |
using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
|
|
42 |
|
|
43 |
lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"
|
|
44 |
by (auto intro!: measurable_vimage_algebra1
|
|
45 |
simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def)
|
|
46 |
|
|
47 |
lemma measurable_snth[measurable]: "(\<lambda>\<omega>. \<omega> !! n) \<in> measurable (stream_space M) M"
|
|
48 |
using measurable_snth_PiM measurable_component_singleton by (rule measurable_compose) simp
|
|
49 |
|
|
50 |
lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M"
|
|
51 |
using measurable_snth[of 0] by simp
|
|
52 |
|
|
53 |
lemma measurable_stream_space2:
|
|
54 |
assumes f_snth: "\<And>n. (\<lambda>x. f x !! n) \<in> measurable N M"
|
|
55 |
shows "f \<in> measurable N (stream_space M)"
|
|
56 |
unfolding stream_space_def measurable_distr_eq2
|
|
57 |
proof (rule measurable_vimage_algebra2)
|
|
58 |
show "f \<in> space N \<rightarrow> streams (space M)"
|
|
59 |
using f_snth[THEN measurable_space] by (auto simp add: streams_iff_sset sset_range)
|
|
60 |
show "(\<lambda>x. op !! (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))"
|
|
61 |
proof (rule measurable_PiM_single')
|
|
62 |
show "(\<lambda>x. op !! (f x)) \<in> space N \<rightarrow> UNIV \<rightarrow>\<^sub>E space M"
|
|
63 |
using f_snth[THEN measurable_space] by auto
|
|
64 |
qed (rule f_snth)
|
|
65 |
qed
|
|
66 |
|
|
67 |
lemma measurable_stream_coinduct[consumes 1, case_names shd stl, coinduct set: measurable]:
|
|
68 |
assumes "F f"
|
|
69 |
assumes h: "\<And>f. F f \<Longrightarrow> (\<lambda>x. shd (f x)) \<in> measurable N M"
|
|
70 |
assumes t: "\<And>f. F f \<Longrightarrow> F (\<lambda>x. stl (f x))"
|
|
71 |
shows "f \<in> measurable N (stream_space M)"
|
|
72 |
proof (rule measurable_stream_space2)
|
|
73 |
fix n show "(\<lambda>x. f x !! n) \<in> measurable N M"
|
|
74 |
using `F f` by (induction n arbitrary: f) (auto intro: h t)
|
|
75 |
qed
|
|
76 |
|
|
77 |
lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)"
|
|
78 |
by (rule measurable_stream_space2) (simp add: sdrop_snth)
|
|
79 |
|
|
80 |
lemma measurable_stl[measurable]: "(\<lambda>\<omega>. stl \<omega>) \<in> measurable (stream_space M) (stream_space M)"
|
|
81 |
by (rule measurable_stream_space2) (simp del: snth.simps add: snth.simps[symmetric])
|
|
82 |
|
|
83 |
lemma measurable_to_stream[measurable]: "to_stream \<in> measurable (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M)"
|
|
84 |
by (rule measurable_stream_space2) (simp add: to_stream_def)
|
|
85 |
|
|
86 |
lemma measurable_Stream[measurable (raw)]:
|
|
87 |
assumes f[measurable]: "f \<in> measurable N M"
|
|
88 |
assumes g[measurable]: "g \<in> measurable N (stream_space M)"
|
|
89 |
shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)"
|
|
90 |
by (rule measurable_stream_space2) (simp add: Stream_snth)
|
|
91 |
|
|
92 |
lemma measurable_smap[measurable]:
|
|
93 |
assumes X[measurable]: "X \<in> measurable N M"
|
|
94 |
shows "smap X \<in> measurable (stream_space N) (stream_space M)"
|
|
95 |
by (rule measurable_stream_space2) simp
|
|
96 |
|
|
97 |
lemma measurable_stake[measurable]:
|
|
98 |
"stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
|
|
99 |
by (induct i) auto
|
|
100 |
|
|
101 |
lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
|
|
102 |
proof -
|
|
103 |
interpret product_prob_space "\<lambda>_. M" UNIV by default
|
|
104 |
show ?thesis
|
|
105 |
by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
|
|
106 |
qed
|
|
107 |
|
|
108 |
lemma (in prob_space) nn_integral_stream_space:
|
|
109 |
assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
|
|
110 |
shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)"
|
|
111 |
proof -
|
|
112 |
interpret S: sequence_space M
|
|
113 |
by default
|
|
114 |
interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
|
|
115 |
by default
|
|
116 |
|
|
117 |
have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)"
|
|
118 |
by (subst stream_space_eq_distr) (simp add: nn_integral_distr)
|
|
119 |
also have "\<dots> = (\<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))"
|
|
120 |
by (subst S.PiM_iter[symmetric]) (simp add: nn_integral_distr)
|
|
121 |
also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) (x, X))) \<partial>S.S \<partial>M)"
|
|
122 |
by (subst S.nn_integral_fst) simp_all
|
|
123 |
also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## to_stream X) \<partial>S.S \<partial>M)"
|
|
124 |
by (auto intro!: nn_integral_cong simp: to_stream_nat_case)
|
|
125 |
also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M \<partial>M)"
|
|
126 |
by (subst stream_space_eq_distr)
|
|
127 |
(simp add: nn_integral_distr cong: nn_integral_cong)
|
|
128 |
finally show ?thesis .
|
|
129 |
qed
|
|
130 |
|
|
131 |
lemma (in prob_space) emeasure_stream_space:
|
|
132 |
assumes X[measurable]: "X \<in> sets (stream_space M)"
|
|
133 |
shows "emeasure (stream_space M) X = (\<integral>\<^sup>+t. emeasure (stream_space M) {x\<in>space (stream_space M). t ## x \<in> X } \<partial>M)"
|
|
134 |
proof -
|
|
135 |
have eq: "\<And>x xs. xs \<in> space (stream_space M) \<Longrightarrow> x \<in> space M \<Longrightarrow>
|
|
136 |
indicator X (x ## xs) = indicator {xs\<in>space (stream_space M). x ## xs \<in> X } xs"
|
|
137 |
by (auto split: split_indicator)
|
|
138 |
show ?thesis
|
|
139 |
using nn_integral_stream_space[of "indicator X"]
|
|
140 |
apply (auto intro!: nn_integral_cong)
|
|
141 |
apply (subst nn_integral_cong)
|
|
142 |
apply (rule eq)
|
|
143 |
apply simp_all
|
|
144 |
done
|
|
145 |
qed
|
|
146 |
|
|
147 |
lemma (in prob_space) prob_stream_space:
|
|
148 |
assumes P[measurable]: "{x\<in>space (stream_space M). P x} \<in> sets (stream_space M)"
|
|
149 |
shows "\<P>(x in stream_space M. P x) = (\<integral>\<^sup>+t. \<P>(x in stream_space M. P (t ## x)) \<partial>M)"
|
|
150 |
proof -
|
|
151 |
interpret S: prob_space "stream_space M"
|
|
152 |
by (rule prob_space_stream_space)
|
|
153 |
show ?thesis
|
|
154 |
unfolding S.emeasure_eq_measure[symmetric]
|
|
155 |
by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong)
|
|
156 |
qed
|
|
157 |
|
|
158 |
lemma (in prob_space) AE_stream_space:
|
|
159 |
assumes [measurable]: "Measurable.pred (stream_space M) P"
|
|
160 |
shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))"
|
|
161 |
proof -
|
|
162 |
interpret stream: prob_space "stream_space M"
|
|
163 |
by (rule prob_space_stream_space)
|
|
164 |
|
|
165 |
have eq: "\<And>x X. indicator {x. \<not> P x} (x ## X) = indicator {X. \<not> P (x ## X)} X"
|
|
166 |
by (auto split: split_indicator)
|
|
167 |
show ?thesis
|
|
168 |
apply (subst AE_iff_nn_integral, simp)
|
|
169 |
apply (subst nn_integral_stream_space, simp)
|
|
170 |
apply (subst eq)
|
|
171 |
apply (subst nn_integral_0_iff_AE, simp)
|
|
172 |
apply (simp add: AE_iff_nn_integral[symmetric])
|
|
173 |
done
|
|
174 |
qed
|
|
175 |
|
|
176 |
lemma (in prob_space) AE_stream_all:
|
|
177 |
assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
|
|
178 |
shows "AE x in stream_space M. stream_all P x"
|
|
179 |
proof -
|
|
180 |
{ fix n have "AE x in stream_space M. P (x !! n)"
|
|
181 |
proof (induct n)
|
|
182 |
case 0 with P show ?case
|
|
183 |
by (subst AE_stream_space) (auto elim!: eventually_elim1)
|
|
184 |
next
|
|
185 |
case (Suc n) then show ?case
|
|
186 |
by (subst AE_stream_space) auto
|
|
187 |
qed }
|
|
188 |
then show ?thesis
|
|
189 |
unfolding stream_all_def by (simp add: AE_all_countable)
|
|
190 |
qed
|
|
191 |
|
|
192 |
end
|