1(* Author: Johannes H��lzl <hoelzl@in.tum.de> *) 2 3section \<open>Stopping times\<close> 4 5theory Stopping_Time 6 imports "HOL-Analysis.Analysis" 7begin 8 9subsection \<open>Stopping Time\<close> 10 11text \<open>This is also called strong stopping time. Then stopping time is T with alternative is 12 \<open>T x < t\<close> measurable.\<close> 13 14definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool" 15where 16 "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))" 17 18lemma stopping_time_cong: "(\<And>t x. x \<in> space (F t) \<Longrightarrow> T x = S x) \<Longrightarrow> stopping_time F T = stopping_time F S" 19 unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp 20 21lemma stopping_timeD: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t)" 22 by (auto simp: stopping_time_def) 23 24lemma stopping_timeD2: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. t < T x)" 25 unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic) 26 27lemma stopping_timeI[intro?]: "(\<And>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t)) \<Longrightarrow> stopping_time F T" 28 by (auto simp: stopping_time_def) 29 30lemma measurable_stopping_time: 31 fixes T :: "'a \<Rightarrow> 't::{linorder_topology, second_countable_topology}" 32 assumes T: "stopping_time F T" 33 and M: "\<And>t. sets (F t) \<subseteq> sets M" "\<And>t. space (F t) = space M" 34 shows "T \<in> M \<rightarrow>\<^sub>M borel" 35proof (rule borel_measurableI_le) 36 show "{x \<in> space M. T x \<le> t} \<in> sets M" for t 37 using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def) 38qed 39 40lemma stopping_time_const: "stopping_time F (\<lambda>x. c)" 41 by (auto simp: stopping_time_def) 42 43lemma stopping_time_min: 44 "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. min (T x) (S x))" 45 by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic) 46 47lemma stopping_time_max: 48 "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. max (T x) (S x))" 49 by (auto simp: stopping_time_def intro!: pred_intros_logic) 50 51section \<open>Filtration\<close> 52 53locale filtration = 54 fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure" 55 assumes space_F: "\<And>i. space (F i) = \<Omega>" 56 assumes sets_F_mono: "\<And>i j. i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)" 57begin 58 59subsection \<open>$\sigma$-algebra of a Stopping Time\<close> 60 61definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure" 62where 63 "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}" 64 65lemma space_pre_sigma: "space (pre_sigma T) = \<Omega>" 66 unfolding pre_sigma_def using sets.space_closed[of "F _"] 67 by (intro space_measure_of) (auto simp: space_F) 68 69lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)" 70 by (simp add: pre_sigma_def emeasure_sigma) 71 72lemma sigma_algebra_pre_sigma: 73 assumes T: "stopping_time F T" 74 shows "sigma_algebra \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}" 75 unfolding sigma_algebra_iff2 76proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI) 77 show "{A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)} \<subseteq> Pow \<Omega>" 78 using sets.space_closed[of "F _"] by (auto simp: space_F) 79next 80 fix A t assume "A \<in> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}" 81 then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)" 82 using T stopping_timeD[measurable] by auto 83 also have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} = {\<omega> \<in> \<Omega> - A. T \<omega> \<le> t}" 84 by (auto simp: space_F) 85 finally show "{\<omega> \<in> \<Omega> - A. T \<omega> \<le> t} \<in> sets (F t)" . 86next 87 fix AA :: "nat \<Rightarrow> 'a set" and t assume "range AA \<subseteq> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}" 88 then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t 89 by auto 90 also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t}" 91 by auto 92 finally show "{\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t} \<in> sets (F t)" . 93qed auto 94 95lemma sets_pre_sigma: "stopping_time F T \<Longrightarrow> sets (pre_sigma T) = {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}" 96 unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma]) 97 98lemma sets_pre_sigmaI: "stopping_time F T \<Longrightarrow> (\<And>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)) \<Longrightarrow> A \<in> sets (pre_sigma T)" 99 unfolding sets_pre_sigma by auto 100 101lemma pred_pre_sigmaI: 102 assumes T: "stopping_time F T" 103 shows "(\<And>t. Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P" 104 unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp 105 106lemma sets_pre_sigmaD: "stopping_time F T \<Longrightarrow> A \<in> sets (pre_sigma T) \<Longrightarrow> {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)" 107 unfolding sets_pre_sigma by auto 108 109lemma stopping_time_le_const: "stopping_time F T \<Longrightarrow> s \<le> t \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<le> s)" 110 using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F) 111 112lemma measurable_stopping_time_pre_sigma: 113 assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel" 114proof (intro borel_measurableI_le sets_pre_sigmaI[OF T]) 115 fix t t' 116 have "{\<omega>\<in>space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))" 117 using T unfolding pred_def[symmetric] by (rule stopping_timeD) 118 also have "\<dots> \<subseteq> sets (F t)" 119 by (rule sets_F_mono) simp 120 finally show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)" 121 by (simp add: space_pre_sigma space_F) 122qed 123 124lemma mono_pre_sigma: 125 assumes T: "stopping_time F T" and S: "stopping_time F S" 126 and le: "\<And>\<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> T \<omega> \<le> S \<omega>" 127 shows "sets (pre_sigma T) \<subseteq> sets (pre_sigma S)" 128 unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T] 129proof safe 130 interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}" 131 using T by (rule sigma_algebra_pre_sigma) 132 fix A t assume A: "\<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)" 133 then have "A \<subseteq> \<Omega>" 134 using sets_into_space by auto 135 from A have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} \<in> sets (F t)" 136 using stopping_timeD[OF S] by (auto simp: pred_def) 137 also have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} = {\<omega>\<in>A. S \<omega> \<le> t}" 138 using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans) 139 finally show "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)" 140 by auto 141qed 142 143lemma stopping_time_less_const: 144 assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)" 145proof - 146 guess D :: "'t set" by (rule countable_dense_setE) 147 note D = this 148 show ?thesis 149 proof cases 150 assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t" 151 { fix t' assume "t' < t" 152 with * have "{t' <..< t} \<noteq> {}" 153 by fastforce 154 with D(2)[OF _ this] 155 have "\<exists>d\<in>D. t'< d \<and> d < t" 156 by auto } 157 note ** = this 158 159 show ?thesis 160 proof (rule measurable_cong[THEN iffD2]) 161 show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>{r\<in>D. r < t}. T \<omega> \<le> r)" for \<omega> 162 by (auto dest: ** intro: less_imp_le) 163 show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>{r \<in> D. r < t}. T w \<le> r)" 164 by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto 165 qed 166 next 167 assume "\<not> (\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t)" 168 then obtain t' where t': "t' < t" "\<And>t''. t'' < t \<Longrightarrow> t'' \<le> t'" 169 by (auto simp: not_less[symmetric]) 170 show ?thesis 171 proof (rule measurable_cong[THEN iffD2]) 172 show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega> 173 using t' by auto 174 show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')" 175 using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto 176 qed 177 qed 178qed 179 180lemma stopping_time_eq_const: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = t)" 181 unfolding eq_iff using stopping_time_less_const[of T t] 182 by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] ) 183 184lemma stopping_time_less: 185 assumes T: "stopping_time F T" and S: "stopping_time F S" 186 shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)" 187proof (rule pred_pre_sigmaI[OF T]) 188 fix t 189 obtain D :: "'t set" 190 where [simp]: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)" 191 using countable_separating_set_linorder2 by auto 192 show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)" 193 proof (rule measurable_cong[THEN iffD2]) 194 let ?f = "\<lambda>\<omega>. if T \<omega> = t then \<not> S \<omega> \<le> t else \<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> \<not> (S \<omega> \<le> s)" 195 { fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>" 196 then have "T \<omega> < min t (S \<omega>)" 197 by auto 198 then obtain r where "r \<in> D" "T \<omega> \<le> r" "r < min t (S \<omega>)" 199 by (metis semidense_D) 200 then have "\<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> s < S \<omega>" 201 by auto } 202 then show "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" for \<omega> 203 by (auto simp: not_le) 204 show "Measurable.pred (F t) ?f" 205 by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect 206 stopping_time_le_const predE stopping_time_eq_const T S) 207 auto 208 qed 209qed 210 211end 212 213lemma stopping_time_SUP_enat: 214 fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)" 215 shows "(\<And>i. stopping_time F (T i)) \<Longrightarrow> stopping_time F (SUP i. T i)" 216 unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable) 217 218lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)" 219 by (cases a) auto 220 221lemma stopping_time_Inf_enat: 222 fixes F :: "enat \<Rightarrow> 'a measure" 223 assumes F: "filtration \<Omega> F" 224 assumes P: "\<And>i. Measurable.pred (F i) (P i)" 225 shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})" 226proof (rule stopping_timeI, cases) 227 fix t :: enat assume "t = \<infinity>" then show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)" 228 by auto 229next 230 fix t :: enat assume "t \<noteq> \<infinity>" 231 moreover 232 { fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t" 233 with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)" 234 unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) } 235 ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)" 236 by (auto intro!: Inf_lower2) 237 show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)" 238 unfolding * using filtration.sets_F_mono[OF F, of _ t] P 239 by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F]) 240qed 241 242lemma stopping_time_Inf_nat: 243 fixes F :: "nat \<Rightarrow> 'a measure" 244 assumes F: "filtration \<Omega> F" 245 assumes P: "\<And>i. Measurable.pred (F i) (P i)" and wf: "\<And>i \<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> \<exists>n. P n \<omega>" 246 shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})" 247 unfolding stopping_time_def 248proof (intro allI, subst measurable_cong) 249 fix t \<omega> assume "\<omega> \<in> space (F t)" 250 then have "\<omega> \<in> \<Omega>" 251 using filtration.space_F[OF F] by auto 252 from wf[OF this] have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)" 253 by (rule LeastI2_wellorder_ex) auto 254 then show "(Inf {i. P i \<omega>} \<le> t) = (\<exists>i\<in>{..t}. P i \<omega>)" 255 by (simp add: Inf_nat_def Bex_def) 256next 257 fix t from P show "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)" 258 using filtration.sets_F_mono[OF F, of _ t] 259 by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F]) 260qed 261 262end 263