src/HOL/Probability/Stopping_Time.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 67226 ec32cdaab97b
permissions -rw-r--r--
removed legacy input syntax
     1 (* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
     2 
     3 section \<open>Stopping times\<close>
     4 
     5 theory Stopping_Time
     6   imports "HOL-Analysis.Analysis"
     7 begin
     8 
     9 subsection \<open>Stopping Time\<close>
    10 
    11 text \<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 
    14 definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool"
    15 where
    16   "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
    17 
    18 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"
    19   unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
    20 
    21 lemma 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 
    24 lemma 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 
    27 lemma 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 
    30 lemma 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"
    35 proof (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)
    38 qed
    39 
    40 lemma stopping_time_const: "stopping_time F (\<lambda>x. c)"
    41   by (auto simp: stopping_time_def)
    42 
    43 lemma 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 
    47 lemma 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 
    51 section \<open>Filtration\<close>
    52 
    53 locale 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)"
    57 begin
    58 
    59 subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
    60 
    61 definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure"
    62 where
    63   "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
    64 
    65 lemma 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 
    69 lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)"
    70   by (simp add: pre_sigma_def emeasure_sigma)
    71 
    72 lemma 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
    76 proof (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)
    79 next
    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)" .
    86 next
    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)" .
    93 qed auto
    94 
    95 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)}"
    96   unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
    97 
    98 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)"
    99   unfolding sets_pre_sigma by auto
   100 
   101 lemma 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 
   106 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)"
   107   unfolding sets_pre_sigma by auto
   108 
   109 lemma 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 
   112 lemma measurable_stopping_time_pre_sigma:
   113   assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel"
   114 proof (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)
   122 qed
   123 
   124 lemma 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]
   129 proof 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
   141 qed
   142 
   143 lemma stopping_time_less_const:
   144   assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
   145 proof -
   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
   178 qed
   179 
   180 lemma 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 
   184 lemma 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>)"
   187 proof (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
   209 qed
   210 
   211 end
   212 
   213 lemma 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 
   218 lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)"
   219   by (cases a) auto
   220 
   221 lemma 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>})"
   226 proof (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
   229 next
   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])
   240 qed
   241 
   242 lemma 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
   248 proof (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)
   256 next
   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])
   260 qed
   261 
   262 end