src/HOL/Probability/Stopping_Time.thy
changeset 64320 ba194424b895
child 66453 cc19f7ca2ed6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Thu Oct 20 18:41:59 2016 +0200
     1.3 @@ -0,0 +1,262 @@
     1.4 +(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
     1.5 +
     1.6 +section {* Stopping times *}
     1.7 +
     1.8 +theory Stopping_Time
     1.9 +  imports "../Analysis/Analysis"
    1.10 +begin
    1.11 +
    1.12 +subsection \<open>Stopping Time\<close>
    1.13 +
    1.14 +text \<open>This is also called strong stopping time. Then stopping time is T with alternative is
    1.15 +  \<open>T x < t\<close> measurable.\<close>
    1.16 +
    1.17 +definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool"
    1.18 +where
    1.19 +  "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
    1.20 +
    1.21 +lemma 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"
    1.22 +  unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
    1.23 +
    1.24 +lemma stopping_timeD: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t)"
    1.25 +  by (auto simp: stopping_time_def)
    1.26 +
    1.27 +lemma stopping_timeD2: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. t < T x)"
    1.28 +  unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic)
    1.29 +
    1.30 +lemma stopping_timeI[intro?]: "(\<And>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t)) \<Longrightarrow> stopping_time F T"
    1.31 +  by (auto simp: stopping_time_def)
    1.32 +
    1.33 +lemma measurable_stopping_time:
    1.34 +  fixes T :: "'a \<Rightarrow> 't::{linorder_topology, second_countable_topology}"
    1.35 +  assumes T: "stopping_time F T"
    1.36 +    and M: "\<And>t. sets (F t) \<subseteq> sets M" "\<And>t. space (F t) = space M"
    1.37 +  shows "T \<in> M \<rightarrow>\<^sub>M borel"
    1.38 +proof (rule borel_measurableI_le)
    1.39 +  show "{x \<in> space M. T x \<le> t} \<in> sets M" for t
    1.40 +    using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def)
    1.41 +qed
    1.42 +
    1.43 +lemma stopping_time_const: "stopping_time F (\<lambda>x. c)"
    1.44 +  by (auto simp: stopping_time_def)
    1.45 +
    1.46 +lemma stopping_time_min:
    1.47 +  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. min (T x) (S x))"
    1.48 +  by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
    1.49 +
    1.50 +lemma stopping_time_max:
    1.51 +  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. max (T x) (S x))"
    1.52 +  by (auto simp: stopping_time_def intro!: pred_intros_logic)
    1.53 +
    1.54 +section \<open>Filtration\<close>
    1.55 +
    1.56 +locale filtration =
    1.57 +  fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure"
    1.58 +  assumes space_F: "\<And>i. space (F i) = \<Omega>"
    1.59 +  assumes sets_F_mono: "\<And>i j. i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)"
    1.60 +begin
    1.61 +
    1.62 +subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
    1.63 +
    1.64 +definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure"
    1.65 +where
    1.66 +  "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
    1.67 +
    1.68 +lemma space_pre_sigma: "space (pre_sigma T) = \<Omega>"
    1.69 +  unfolding pre_sigma_def using sets.space_closed[of "F _"]
    1.70 +  by (intro space_measure_of) (auto simp: space_F)
    1.71 +
    1.72 +lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)"
    1.73 +  by (simp add: pre_sigma_def emeasure_sigma)
    1.74 +
    1.75 +lemma sigma_algebra_pre_sigma:
    1.76 +  assumes T: "stopping_time F T"
    1.77 +  shows "sigma_algebra \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
    1.78 +  unfolding sigma_algebra_iff2
    1.79 +proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI)
    1.80 +  show "{A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)} \<subseteq> Pow \<Omega>"
    1.81 +    using sets.space_closed[of "F _"] by (auto simp: space_F)
    1.82 +next
    1.83 +  fix A t assume "A \<in> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
    1.84 +  then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)"
    1.85 +    using T stopping_timeD[measurable] by auto
    1.86 +  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}"
    1.87 +    by (auto simp: space_F)
    1.88 +  finally show "{\<omega> \<in> \<Omega> - A. T \<omega> \<le> t} \<in> sets (F t)" .
    1.89 +next
    1.90 +  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)}"
    1.91 +  then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
    1.92 +    by auto
    1.93 +  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
    1.94 +    by auto
    1.95 +  finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
    1.96 +qed auto
    1.97 +
    1.98 +lemma 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)}"
    1.99 +  unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
   1.100 +
   1.101 +lemma 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)"
   1.102 +  unfolding sets_pre_sigma by auto
   1.103 +
   1.104 +lemma pred_pre_sigmaI:
   1.105 +  assumes T: "stopping_time F T"
   1.106 +  shows "(\<And>t. Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P"
   1.107 +  unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp
   1.108 +
   1.109 +lemma 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)"
   1.110 +  unfolding sets_pre_sigma by auto
   1.111 +
   1.112 +lemma stopping_time_le_const: "stopping_time F T \<Longrightarrow> s \<le> t \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<le> s)"
   1.113 +  using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F)
   1.114 +
   1.115 +lemma measurable_stopping_time_pre_sigma:
   1.116 +  assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel"
   1.117 +proof (intro borel_measurableI_le sets_pre_sigmaI[OF T])
   1.118 +  fix t t'
   1.119 +  have "{\<omega>\<in>space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))"
   1.120 +    using T unfolding pred_def[symmetric] by (rule stopping_timeD)
   1.121 +  also have "\<dots> \<subseteq> sets (F t)"
   1.122 +    by (rule sets_F_mono) simp
   1.123 +  finally show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)"
   1.124 +    by (simp add: space_pre_sigma space_F)
   1.125 +qed
   1.126 +
   1.127 +lemma mono_pre_sigma:
   1.128 +  assumes T: "stopping_time F T" and S: "stopping_time F S"
   1.129 +    and le: "\<And>\<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> T \<omega> \<le> S \<omega>"
   1.130 +  shows "sets (pre_sigma T) \<subseteq> sets (pre_sigma S)"
   1.131 +  unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T]
   1.132 +proof safe
   1.133 +  interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
   1.134 +    using T by (rule sigma_algebra_pre_sigma)
   1.135 +  fix A t assume A: "\<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
   1.136 +  then have "A \<subseteq> \<Omega>"
   1.137 +    using sets_into_space by auto
   1.138 +  from A have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} \<in> sets (F t)"
   1.139 +    using stopping_timeD[OF S] by (auto simp: pred_def)
   1.140 +  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}"
   1.141 +    using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans)
   1.142 +  finally show "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)"
   1.143 +    by auto
   1.144 +qed
   1.145 +
   1.146 +lemma stopping_time_less_const:
   1.147 +  assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
   1.148 +proof -
   1.149 +  guess D :: "'t set" by (rule countable_dense_setE)
   1.150 +  note D = this
   1.151 +  show ?thesis
   1.152 +  proof cases
   1.153 +    assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"
   1.154 +    { fix t' assume "t' < t"
   1.155 +      with * have "{t' <..< t} \<noteq> {}"
   1.156 +        by fastforce
   1.157 +      with D(2)[OF _ this]
   1.158 +      have "\<exists>d\<in>D. t'< d \<and> d < t"
   1.159 +        by auto }
   1.160 +    note ** = this
   1.161 +
   1.162 +    show ?thesis
   1.163 +    proof (rule measurable_cong[THEN iffD2])
   1.164 +      show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>{r\<in>D. r < t}. T \<omega> \<le> r)" for \<omega>
   1.165 +        by (auto dest: ** intro: less_imp_le)
   1.166 +      show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>{r \<in> D. r < t}. T w \<le> r)"
   1.167 +        by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto
   1.168 +    qed
   1.169 +  next
   1.170 +    assume "\<not> (\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t)"
   1.171 +    then obtain t' where t': "t' < t" "\<And>t''. t'' < t \<Longrightarrow> t'' \<le> t'"
   1.172 +      by (auto simp: not_less[symmetric])
   1.173 +    show ?thesis
   1.174 +    proof (rule measurable_cong[THEN iffD2])
   1.175 +      show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega>
   1.176 +        using t' by auto
   1.177 +      show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')"
   1.178 +        using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto
   1.179 +    qed
   1.180 +  qed
   1.181 +qed
   1.182 +
   1.183 +lemma stopping_time_eq_const: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = t)"
   1.184 +  unfolding eq_iff using stopping_time_less_const[of T t]
   1.185 +  by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] )
   1.186 +
   1.187 +lemma stopping_time_less:
   1.188 +  assumes T: "stopping_time F T" and S: "stopping_time F S"
   1.189 +  shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)"
   1.190 +proof (rule pred_pre_sigmaI[OF T])
   1.191 +  fix t
   1.192 +  obtain D :: "'t set"
   1.193 +    where [simp]: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)"
   1.194 +    using countable_separating_set_linorder2 by auto
   1.195 +  show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)"
   1.196 +  proof (rule measurable_cong[THEN iffD2])
   1.197 +    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)"
   1.198 +    { fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
   1.199 +      then have "T \<omega> < min t (S \<omega>)"
   1.200 +        by auto
   1.201 +      then obtain r where "r \<in> D" "T \<omega> \<le> r" "r < min t (S \<omega>)"
   1.202 +        by (metis semidense_D)
   1.203 +      then have "\<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> s < S \<omega>"
   1.204 +        by auto }
   1.205 +    then show "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" for \<omega>
   1.206 +      by (auto simp: not_le)
   1.207 +    show "Measurable.pred (F t) ?f"
   1.208 +      by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
   1.209 +                stopping_time_le_const predE stopping_time_eq_const T S)
   1.210 +         auto
   1.211 +  qed
   1.212 +qed
   1.213 +
   1.214 +end
   1.215 +
   1.216 +lemma stopping_time_SUP_enat:
   1.217 +  fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)"
   1.218 +  shows "(\<And>i. stopping_time F (T i)) \<Longrightarrow> stopping_time F (SUP i. T i)"
   1.219 +  unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
   1.220 +
   1.221 +lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)"
   1.222 +  by (cases a) auto
   1.223 +
   1.224 +lemma stopping_time_Inf_enat:
   1.225 +  fixes F :: "enat \<Rightarrow> 'a measure"
   1.226 +  assumes F: "filtration \<Omega> F"
   1.227 +  assumes P: "\<And>i. Measurable.pred (F i) (P i)"
   1.228 +  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
   1.229 +proof (rule stopping_timeI, cases)
   1.230 +  fix t :: enat assume "t = \<infinity>" then show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
   1.231 +    by auto
   1.232 +next
   1.233 +  fix t :: enat assume "t \<noteq> \<infinity>"
   1.234 +  moreover
   1.235 +  { fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
   1.236 +    with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)"
   1.237 +      unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) }
   1.238 +  ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)"
   1.239 +    by (auto intro!: Inf_lower2)
   1.240 +  show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
   1.241 +    unfolding * using filtration.sets_F_mono[OF F, of _ t] P
   1.242 +    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
   1.243 +qed
   1.244 +
   1.245 +lemma stopping_time_Inf_nat:
   1.246 +  fixes F :: "nat \<Rightarrow> 'a measure"
   1.247 +  assumes F: "filtration \<Omega> F"
   1.248 +  assumes P: "\<And>i. Measurable.pred (F i) (P i)" and wf: "\<And>i \<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> \<exists>n. P n \<omega>"
   1.249 +  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
   1.250 +  unfolding stopping_time_def
   1.251 +proof (intro allI, subst measurable_cong)
   1.252 +  fix t \<omega> assume "\<omega> \<in> space (F t)"
   1.253 +  then have "\<omega> \<in> \<Omega>"
   1.254 +    using filtration.space_F[OF F] by auto
   1.255 +  from wf[OF this] have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)"
   1.256 +    by (rule LeastI2_wellorder_ex) auto
   1.257 +  then show "(Inf {i. P i \<omega>} \<le> t) = (\<exists>i\<in>{..t}. P i \<omega>)"
   1.258 +    by (simp add: Inf_nat_def Bex_def)
   1.259 +next
   1.260 +  fix t from P show "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)"
   1.261 +    using filtration.sets_F_mono[OF F, of _ t]
   1.262 +    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
   1.263 +qed
   1.264 +
   1.265 +end