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