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