HOL-Probability: move stopping time from AFP/Markov_Models
authorhoelzl
Thu Oct 20 18:41:59 2016 +0200 (2016-10-20)
changeset 64320ba194424b895
parent 64319 a33bbac43359
child 64321 95be866e49fc
HOL-Probability: move stopping time from AFP/Markov_Models
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
src/HOL/Library/Stream.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/Stopping_Time.thy
src/HOL/Probability/Stream_Space.thy
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Thu Oct 20 18:41:58 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Thu Oct 20 18:41:59 2016 +0200
     1.3 @@ -345,6 +345,14 @@
     1.4    "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
     1.5    unfolding insert_def by (rule sets.Un) auto
     1.6  
     1.7 +lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
     1.8 +proof -
     1.9 +  have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set"
    1.10 +    by (intro sets.countable_UN') auto
    1.11 +  then show ?thesis
    1.12 +    by auto
    1.13 +qed
    1.14 +
    1.15  lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    1.16    unfolding Compl_eq_Diff_UNIV by simp
    1.17  
     2.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Oct 20 18:41:58 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Oct 20 18:41:59 2016 +0200
     2.3 @@ -56,6 +56,15 @@
     2.4      by simp
     2.5  qed
     2.6  
     2.7 +instance enat :: second_countable_topology
     2.8 +proof
     2.9 +  show "\<exists>B::enat set set. countable B \<and> open = generate_topology B"
    2.10 +  proof (intro exI conjI)
    2.11 +    show "countable (range lessThan \<union> range greaterThan::enat set set)"
    2.12 +      by auto
    2.13 +  qed (simp add: open_enat_def)
    2.14 +qed
    2.15 +
    2.16  instance ereal :: second_countable_topology
    2.17  proof (standard, intro exI conjI)
    2.18    let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
     3.1 --- a/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:58 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Measurable.thy	Thu Oct 20 18:41:59 2016 +0200
     3.3 @@ -646,6 +646,14 @@
     3.4    shows "liminf A \<in> sets M"
     3.5  by (subst liminf_SUP_INF, auto)
     3.6  
     3.7 +lemma measurable_case_enat[measurable (raw)]:
     3.8 +  assumes f: "f \<in> M \<rightarrow>\<^sub>M count_space UNIV" and g: "\<And>i. g i \<in> M \<rightarrow>\<^sub>M N" and h: "h \<in> M \<rightarrow>\<^sub>M N"
     3.9 +  shows "(\<lambda>x. case f x of enat i \<Rightarrow> g i x | \<infinity> \<Rightarrow> h x) \<in> M \<rightarrow>\<^sub>M N"
    3.10 +  apply (rule measurable_compose_countable[OF _ f])
    3.11 +  subgoal for i
    3.12 +    by (cases i) (auto intro: g h)
    3.13 +  done
    3.14 +
    3.15  hide_const (open) pred
    3.16  
    3.17  end
     4.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Oct 20 18:41:58 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Oct 20 18:41:59 2016 +0200
     4.3 @@ -1469,6 +1469,9 @@
     4.4  lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
     4.5    by (rule measure_eqI) (auto simp: emeasure_distr)
     4.6  
     4.7 +lemma distr_id2: "sets M = sets N \<Longrightarrow> distr N M (\<lambda>x. x) = N"
     4.8 +  by (rule measure_eqI) (auto simp: emeasure_distr)
     4.9 +
    4.10  lemma measure_distr:
    4.11    "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
    4.12    by (simp add: emeasure_distr measure_def)
    4.13 @@ -3516,6 +3519,11 @@
    4.14    finally show ?thesis .
    4.15  qed
    4.16  
    4.17 +lemma measurable_SUP2:
    4.18 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f \<in> measurable N (M i)) \<Longrightarrow>
    4.19 +    (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i:I. M i)"
    4.20 +  by (auto intro!: measurable_Sup2)
    4.21 +
    4.22  lemma sets_Sup_sigma:
    4.23    assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
    4.24    shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
     5.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 20 18:41:58 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 20 18:41:59 2016 +0200
     5.3 @@ -458,6 +458,11 @@
     5.4         (fastforce simp: topological_space_class.topological_basis_def)+
     5.5  qed
     5.6  
     5.7 +instance nat :: second_countable_topology
     5.8 +proof
     5.9 +  show "\<exists>B::nat set set. countable B \<and> open = generate_topology B"
    5.10 +    by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def)
    5.11 +qed
    5.12  
    5.13  lemma countable_separating_set_linorder1:
    5.14    shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y))"
     6.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 20 18:41:58 2016 +0200
     6.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Oct 20 18:41:59 2016 +0200
     6.3 @@ -1131,6 +1131,9 @@
     6.4  lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
     6.5    by (cases x rule: ennreal_cases) auto
     6.6  
     6.7 +lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
     6.8 +  by (cases x) auto
     6.9 +
    6.10  subsection \<open>Coercion from @{typ enat} to @{typ ennreal}\<close>
    6.11  
    6.12  
     7.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:58 2016 +0200
     7.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Oct 20 18:41:59 2016 +0200
     7.3 @@ -662,7 +662,7 @@
     7.4  lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
     7.5    using sfilter_Stream[of P "shd s" "stl s"] by simp
     7.6  
     7.7 -lemma sfilter_eq: 
     7.8 +lemma sfilter_eq:
     7.9    assumes "ev (holds P) s"
    7.10    shows "sfilter P s = x ## s' \<longleftrightarrow>
    7.11      P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
    7.12 @@ -685,7 +685,7 @@
    7.13  proof
    7.14    assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
    7.15    proof (coinduction arbitrary: s rule: alw_coinduct)
    7.16 -    case (stl s) 
    7.17 +    case (stl s)
    7.18      then have "ev (holds P) s"
    7.19        by blast
    7.20      from this stl show ?case
    7.21 @@ -694,7 +694,7 @@
    7.22  next
    7.23    assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
    7.24    proof (coinduction arbitrary: s rule: alw_coinduct)
    7.25 -    case (stl s) 
    7.26 +    case (stl s)
    7.27      then have "ev (holds P) s"
    7.28        by blast
    7.29      from this stl show ?case
    7.30 @@ -767,4 +767,22 @@
    7.31  lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
    7.32    by (simp add: HLD_def)
    7.33  
    7.34 +lemma pigeonhole_stream:
    7.35 +  assumes "alw (HLD s) \<omega>"
    7.36 +  assumes "finite s"
    7.37 +  shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
    7.38 +proof -
    7.39 +  have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
    7.40 +    using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
    7.41 +  from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
    7.42 +  show ?thesis
    7.43 +    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
    7.44 +qed
    7.45 +
    7.46 +lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
    7.47 +proof
    7.48 +  assume "ev P \<omega>" then show "((\<lambda>xs. \<not> P xs) suntil P) \<omega>"
    7.49 +    by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
    7.50 +qed (auto simp: ev_suntil)
    7.51 +
    7.52  end
     8.1 --- a/src/HOL/Library/Stream.thy	Thu Oct 20 18:41:58 2016 +0200
     8.2 +++ b/src/HOL/Library/Stream.thy	Thu Oct 20 18:41:59 2016 +0200
     8.3 @@ -242,7 +242,7 @@
     8.4  lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)"
     8.5    by (induct n arbitrary: m s) auto
     8.6  
     8.7 -partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
     8.8 +partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
     8.9    "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
    8.10  
    8.11  lemma sdrop_while_SCons[code]:
    8.12 @@ -342,7 +342,7 @@
    8.13    by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
    8.14  
    8.15  lemma sset_cycle[simp]:
    8.16 -  assumes "xs \<noteq> []" 
    8.17 +  assumes "xs \<noteq> []"
    8.18    shows "sset (cycle xs) = set xs"
    8.19  proof (intro set_eqI iffI)
    8.20    fix x
    8.21 @@ -408,6 +408,14 @@
    8.22  lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
    8.23    by (simp add: streams_iff_sset)
    8.24  
    8.25 +lemma streams_empty_iff: "streams S = {} \<longleftrightarrow> S = {}"
    8.26 +proof safe
    8.27 +  fix x assume "x \<in> S" "streams S = {}"
    8.28 +  then have "sconst x \<in> streams S"
    8.29 +    by (intro sconst_streams)
    8.30 +  then show "x \<in> {}"
    8.31 +    unfolding \<open>streams S = {}\<close> by simp
    8.32 +qed (auto simp: streams_empty)
    8.33  
    8.34  subsection \<open>stream of natural numbers\<close>
    8.35  
    8.36 @@ -442,11 +450,11 @@
    8.37  lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
    8.38    by (cases ws) auto
    8.39  
    8.40 -lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
    8.41 +lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then
    8.42    shd s ! n else flat (stl s) !! (n - length (shd s)))"
    8.43    by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less)
    8.44  
    8.45 -lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> 
    8.46 +lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow>
    8.47    sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
    8.48  proof safe
    8.49    fix x assume ?P "x : ?L"
     9.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:58 2016 +0200
     9.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:59 2016 +0200
     9.3 @@ -1778,4 +1778,10 @@
     9.4    shows "space (M \<bind> f) = space B"
     9.5    using M by (intro space_bind[OF sets_kernel[OF f]]) auto
     9.6  
     9.7 +lemma bind_distr_return:
     9.8 +  "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> g \<in> N \<rightarrow>\<^sub>M L \<Longrightarrow> space M \<noteq> {} \<Longrightarrow>
     9.9 +    distr M N f \<bind> (\<lambda>x. return L (g x)) = distr M L (\<lambda>x. g (f x))"
    9.10 +  by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]])
    9.11 +     (auto intro!: bind_return_distr')
    9.12 +
    9.13  end
    10.1 --- a/src/HOL/Probability/Probability.thy	Thu Oct 20 18:41:58 2016 +0200
    10.2 +++ b/src/HOL/Probability/Probability.thy	Thu Oct 20 18:41:59 2016 +0200
    10.3 @@ -13,6 +13,7 @@
    10.4    Stream_Space
    10.5    Conditional_Expectation
    10.6    Essential_Supremum
    10.7 +  Stopping_Time
    10.8  begin
    10.9  
   10.10  end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Thu Oct 20 18:41:59 2016 +0200
    11.3 @@ -0,0 +1,262 @@
    11.4 +(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
    11.5 +
    11.6 +section {* Stopping times *}
    11.7 +
    11.8 +theory Stopping_Time
    11.9 +  imports "../Analysis/Analysis"
   11.10 +begin
   11.11 +
   11.12 +subsection \<open>Stopping Time\<close>
   11.13 +
   11.14 +text \<open>This is also called strong stopping time. Then stopping time is T with alternative is
   11.15 +  \<open>T x < t\<close> measurable.\<close>
   11.16 +
   11.17 +definition stopping_time :: "('t::linorder \<Rightarrow> 'a measure) \<Rightarrow> ('a \<Rightarrow> 't) \<Rightarrow> bool"
   11.18 +where
   11.19 +  "stopping_time F T = (\<forall>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
   11.20 +
   11.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"
   11.22 +  unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
   11.23 +
   11.24 +lemma stopping_timeD: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t)"
   11.25 +  by (auto simp: stopping_time_def)
   11.26 +
   11.27 +lemma stopping_timeD2: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. t < T x)"
   11.28 +  unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic)
   11.29 +
   11.30 +lemma stopping_timeI[intro?]: "(\<And>t. Measurable.pred (F t) (\<lambda>x. T x \<le> t)) \<Longrightarrow> stopping_time F T"
   11.31 +  by (auto simp: stopping_time_def)
   11.32 +
   11.33 +lemma measurable_stopping_time:
   11.34 +  fixes T :: "'a \<Rightarrow> 't::{linorder_topology, second_countable_topology}"
   11.35 +  assumes T: "stopping_time F T"
   11.36 +    and M: "\<And>t. sets (F t) \<subseteq> sets M" "\<And>t. space (F t) = space M"
   11.37 +  shows "T \<in> M \<rightarrow>\<^sub>M borel"
   11.38 +proof (rule borel_measurableI_le)
   11.39 +  show "{x \<in> space M. T x \<le> t} \<in> sets M" for t
   11.40 +    using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def)
   11.41 +qed
   11.42 +
   11.43 +lemma stopping_time_const: "stopping_time F (\<lambda>x. c)"
   11.44 +  by (auto simp: stopping_time_def)
   11.45 +
   11.46 +lemma stopping_time_min:
   11.47 +  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. min (T x) (S x))"
   11.48 +  by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
   11.49 +
   11.50 +lemma stopping_time_max:
   11.51 +  "stopping_time F T \<Longrightarrow> stopping_time F S \<Longrightarrow> stopping_time F (\<lambda>x. max (T x) (S x))"
   11.52 +  by (auto simp: stopping_time_def intro!: pred_intros_logic)
   11.53 +
   11.54 +section \<open>Filtration\<close>
   11.55 +
   11.56 +locale filtration =
   11.57 +  fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure"
   11.58 +  assumes space_F: "\<And>i. space (F i) = \<Omega>"
   11.59 +  assumes sets_F_mono: "\<And>i j. i \<le> j \<Longrightarrow> sets (F i) \<le> sets (F j)"
   11.60 +begin
   11.61 +
   11.62 +subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
   11.63 +
   11.64 +definition pre_sigma :: "('a \<Rightarrow> 't) \<Rightarrow> 'a measure"
   11.65 +where
   11.66 +  "pre_sigma T = sigma \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
   11.67 +
   11.68 +lemma space_pre_sigma: "space (pre_sigma T) = \<Omega>"
   11.69 +  unfolding pre_sigma_def using sets.space_closed[of "F _"]
   11.70 +  by (intro space_measure_of) (auto simp: space_F)
   11.71 +
   11.72 +lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)"
   11.73 +  by (simp add: pre_sigma_def emeasure_sigma)
   11.74 +
   11.75 +lemma sigma_algebra_pre_sigma:
   11.76 +  assumes T: "stopping_time F T"
   11.77 +  shows "sigma_algebra \<Omega> {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
   11.78 +  unfolding sigma_algebra_iff2
   11.79 +proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI)
   11.80 +  show "{A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)} \<subseteq> Pow \<Omega>"
   11.81 +    using sets.space_closed[of "F _"] by (auto simp: space_F)
   11.82 +next
   11.83 +  fix A t assume "A \<in> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
   11.84 +  then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)"
   11.85 +    using T stopping_timeD[measurable] by auto
   11.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}"
   11.87 +    by (auto simp: space_F)
   11.88 +  finally show "{\<omega> \<in> \<Omega> - A. T \<omega> \<le> t} \<in> sets (F t)" .
   11.89 +next
   11.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)}"
   11.91 +  then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
   11.92 +    by auto
   11.93 +  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
   11.94 +    by auto
   11.95 +  finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
   11.96 +qed auto
   11.97 +
   11.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)}"
   11.99 +  unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
  11.100 +
  11.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)"
  11.102 +  unfolding sets_pre_sigma by auto
  11.103 +
  11.104 +lemma pred_pre_sigmaI:
  11.105 +  assumes T: "stopping_time F T"
  11.106 +  shows "(\<And>t. Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P"
  11.107 +  unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp
  11.108 +
  11.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)"
  11.110 +  unfolding sets_pre_sigma by auto
  11.111 +
  11.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)"
  11.113 +  using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F)
  11.114 +
  11.115 +lemma measurable_stopping_time_pre_sigma:
  11.116 +  assumes T: "stopping_time F T" shows "T \<in> pre_sigma T \<rightarrow>\<^sub>M borel"
  11.117 +proof (intro borel_measurableI_le sets_pre_sigmaI[OF T])
  11.118 +  fix t t'
  11.119 +  have "{\<omega>\<in>space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))"
  11.120 +    using T unfolding pred_def[symmetric] by (rule stopping_timeD)
  11.121 +  also have "\<dots> \<subseteq> sets (F t)"
  11.122 +    by (rule sets_F_mono) simp
  11.123 +  finally show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)"
  11.124 +    by (simp add: space_pre_sigma space_F)
  11.125 +qed
  11.126 +
  11.127 +lemma mono_pre_sigma:
  11.128 +  assumes T: "stopping_time F T" and S: "stopping_time F S"
  11.129 +    and le: "\<And>\<omega>. \<omega> \<in> \<Omega> \<Longrightarrow> T \<omega> \<le> S \<omega>"
  11.130 +  shows "sets (pre_sigma T) \<subseteq> sets (pre_sigma S)"
  11.131 +  unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T]
  11.132 +proof safe
  11.133 +  interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
  11.134 +    using T by (rule sigma_algebra_pre_sigma)
  11.135 +  fix A t assume A: "\<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)"
  11.136 +  then have "A \<subseteq> \<Omega>"
  11.137 +    using sets_into_space by auto
  11.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)"
  11.139 +    using stopping_timeD[OF S] by (auto simp: pred_def)
  11.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}"
  11.141 +    using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans)
  11.142 +  finally show "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)"
  11.143 +    by auto
  11.144 +qed
  11.145 +
  11.146 +lemma stopping_time_less_const:
  11.147 +  assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
  11.148 +proof -
  11.149 +  guess D :: "'t set" by (rule countable_dense_setE)
  11.150 +  note D = this
  11.151 +  show ?thesis
  11.152 +  proof cases
  11.153 +    assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"
  11.154 +    { fix t' assume "t' < t"
  11.155 +      with * have "{t' <..< t} \<noteq> {}"
  11.156 +        by fastforce
  11.157 +      with D(2)[OF _ this]
  11.158 +      have "\<exists>d\<in>D. t'< d \<and> d < t"
  11.159 +        by auto }
  11.160 +    note ** = this
  11.161 +
  11.162 +    show ?thesis
  11.163 +    proof (rule measurable_cong[THEN iffD2])
  11.164 +      show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>{r\<in>D. r < t}. T \<omega> \<le> r)" for \<omega>
  11.165 +        by (auto dest: ** intro: less_imp_le)
  11.166 +      show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>{r \<in> D. r < t}. T w \<le> r)"
  11.167 +        by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto
  11.168 +    qed
  11.169 +  next
  11.170 +    assume "\<not> (\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t)"
  11.171 +    then obtain t' where t': "t' < t" "\<And>t''. t'' < t \<Longrightarrow> t'' \<le> t'"
  11.172 +      by (auto simp: not_less[symmetric])
  11.173 +    show ?thesis
  11.174 +    proof (rule measurable_cong[THEN iffD2])
  11.175 +      show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega>
  11.176 +        using t' by auto
  11.177 +      show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')"
  11.178 +        using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto
  11.179 +    qed
  11.180 +  qed
  11.181 +qed
  11.182 +
  11.183 +lemma stopping_time_eq_const: "stopping_time F T \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = t)"
  11.184 +  unfolding eq_iff using stopping_time_less_const[of T t]
  11.185 +  by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] )
  11.186 +
  11.187 +lemma stopping_time_less:
  11.188 +  assumes T: "stopping_time F T" and S: "stopping_time F S"
  11.189 +  shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)"
  11.190 +proof (rule pred_pre_sigmaI[OF T])
  11.191 +  fix t
  11.192 +  obtain D :: "'t set"
  11.193 +    where [simp]: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)"
  11.194 +    using countable_separating_set_linorder2 by auto
  11.195 +  show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)"
  11.196 +  proof (rule measurable_cong[THEN iffD2])
  11.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)"
  11.198 +    { fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
  11.199 +      then have "T \<omega> < min t (S \<omega>)"
  11.200 +        by auto
  11.201 +      then obtain r where "r \<in> D" "T \<omega> \<le> r" "r < min t (S \<omega>)"
  11.202 +        by (metis semidense_D)
  11.203 +      then have "\<exists>s\<in>{s\<in>D. s \<le> t}. T \<omega> \<le> s \<and> s < S \<omega>"
  11.204 +        by auto }
  11.205 +    then show "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" for \<omega>
  11.206 +      by (auto simp: not_le)
  11.207 +    show "Measurable.pred (F t) ?f"
  11.208 +      by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
  11.209 +                stopping_time_le_const predE stopping_time_eq_const T S)
  11.210 +         auto
  11.211 +  qed
  11.212 +qed
  11.213 +
  11.214 +end
  11.215 +
  11.216 +lemma stopping_time_SUP_enat:
  11.217 +  fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)"
  11.218 +  shows "(\<And>i. stopping_time F (T i)) \<Longrightarrow> stopping_time F (SUP i. T i)"
  11.219 +  unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
  11.220 +
  11.221 +lemma less_eSuc_iff: "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)"
  11.222 +  by (cases a) auto
  11.223 +
  11.224 +lemma stopping_time_Inf_enat:
  11.225 +  fixes F :: "enat \<Rightarrow> 'a measure"
  11.226 +  assumes F: "filtration \<Omega> F"
  11.227 +  assumes P: "\<And>i. Measurable.pred (F i) (P i)"
  11.228 +  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
  11.229 +proof (rule stopping_timeI, cases)
  11.230 +  fix t :: enat assume "t = \<infinity>" then show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
  11.231 +    by auto
  11.232 +next
  11.233 +  fix t :: enat assume "t \<noteq> \<infinity>"
  11.234 +  moreover
  11.235 +  { fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
  11.236 +    with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)"
  11.237 +      unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) }
  11.238 +  ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)"
  11.239 +    by (auto intro!: Inf_lower2)
  11.240 +  show "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)"
  11.241 +    unfolding * using filtration.sets_F_mono[OF F, of _ t] P
  11.242 +    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
  11.243 +qed
  11.244 +
  11.245 +lemma stopping_time_Inf_nat:
  11.246 +  fixes F :: "nat \<Rightarrow> 'a measure"
  11.247 +  assumes F: "filtration \<Omega> F"
  11.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>"
  11.249 +  shows "stopping_time F (\<lambda>\<omega>. Inf {i. P i \<omega>})"
  11.250 +  unfolding stopping_time_def
  11.251 +proof (intro allI, subst measurable_cong)
  11.252 +  fix t \<omega> assume "\<omega> \<in> space (F t)"
  11.253 +  then have "\<omega> \<in> \<Omega>"
  11.254 +    using filtration.space_F[OF F] by auto
  11.255 +  from wf[OF this] have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)"
  11.256 +    by (rule LeastI2_wellorder_ex) auto
  11.257 +  then show "(Inf {i. P i \<omega>} \<le> t) = (\<exists>i\<in>{..t}. P i \<omega>)"
  11.258 +    by (simp add: Inf_nat_def Bex_def)
  11.259 +next
  11.260 +  fix t from P show "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)"
  11.261 +    using filtration.sets_F_mono[OF F, of _ t]
  11.262 +    by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
  11.263 +qed
  11.264 +
  11.265 +end
    12.1 --- a/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:58 2016 +0200
    12.2 +++ b/src/HOL/Probability/Stream_Space.thy	Thu Oct 20 18:41:59 2016 +0200
    12.3 @@ -446,6 +446,17 @@
    12.4      by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
    12.5  qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
    12.6  
    12.7 +lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))"
    12.8 +proof (induction xs)
    12.9 +  case (Cons x xs)
   12.10 +  note this[measurable]
   12.11 +  have "sstart \<Omega> (x # xs) = {\<omega>\<in>space (stream_space (count_space UNIV)). \<omega> \<in> sstart \<Omega> (x # xs)}"
   12.12 +    by (auto simp: space_stream_space)
   12.13 +  also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
   12.14 +    unfolding in_sstart by measurable
   12.15 +  finally show ?case .
   12.16 +qed (auto intro!: streams_sets)
   12.17 +
   12.18  primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
   12.19  where
   12.20    "scylinder S [] = streams S"