(* Author: Johannes Hölzl <[email protected]> *)
section \<open>Stopping times\<close>
theory Stopping_Time
imports "HOL-Analysis.Analysis"
begin
subsection \<open>Stopping Time\<close>
text \<open>This is also called strong stopping time. Then stopping time is T with alternative is
\<open>T x < t\<close> measurable.\<close>
definition stopping_time :: "('t::linorder \ 'a measure) \ ('a \ 't) \ bool"
where
"stopping_time F T = (\t. Measurable.pred (F t) (\x. T x \ t))"
lemma stopping_time_cong: "(\t x. x \ space (F t) \ T x = S x) \ stopping_time F T = stopping_time F S"
unfolding stopping_time_def by (intro arg_cong[where f=All] ext measurable_cong) simp
lemma stopping_timeD: "stopping_time F T \ Measurable.pred (F t) (\x. T x \ t)"
by (auto simp: stopping_time_def)
lemma stopping_timeD2: "stopping_time F T \ Measurable.pred (F t) (\x. t < T x)"
unfolding not_le[symmetric] by (auto intro: stopping_timeD Measurable.pred_intros_logic)
lemma stopping_timeI[intro?]: "(\t. Measurable.pred (F t) (\x. T x \ t)) \ stopping_time F T"
by (auto simp: stopping_time_def)
lemma measurable_stopping_time:
fixes T :: "'a \ 't::{linorder_topology, second_countable_topology}"
assumes T: "stopping_time F T"
and M: "\t. sets (F t) \ sets M" "\t. space (F t) = space M"
shows "T \ M \\<^sub>M borel"
proof (rule borel_measurableI_le)
show "{x \ space M. T x \ t} \ sets M" for t
using stopping_timeD[OF T] M by (auto simp: Measurable.pred_def)
qed
lemma stopping_time_const: "stopping_time F (\x. c)"
by (auto simp: stopping_time_def)
lemma stopping_time_min:
"stopping_time F T \ stopping_time F S \ stopping_time F (\x. min (T x) (S x))"
by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
lemma stopping_time_max:
"stopping_time F T \ stopping_time F S \ stopping_time F (\x. max (T x) (S x))"
by (auto simp: stopping_time_def intro!: pred_intros_logic)
section \<open>Filtration\<close>
locale filtration =
fixes \<Omega> :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} \<Rightarrow> 'a measure"
assumes space_F: "\i. space (F i) = \"
assumes sets_F_mono: "\i j. i \ j \ sets (F i) \ sets (F j)"
begin
subsection \<open>$\sigma$-algebra of a Stopping Time\<close>
definition pre_sigma :: "('a \ 't) \ 'a measure"
where
"pre_sigma T = sigma \ {A. \t. {\\A. T \ \ t} \ sets (F t)}"
lemma space_pre_sigma: "space (pre_sigma T) = \"
unfolding pre_sigma_def using sets.space_closed[of "F _"]
by (intro space_measure_of) (auto simp: space_F)
lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\_. 0)"
by (simp add: pre_sigma_def emeasure_sigma)
lemma sigma_algebra_pre_sigma:
assumes T: "stopping_time F T"
shows "sigma_algebra \ {A. \t. {\\A. T \ \ t} \ sets (F t)}"
unfolding sigma_algebra_iff2
proof (intro sigma_algebra_iff2[THEN iffD2] conjI ballI allI impI CollectI)
show "{A. \t. {\ \ A. T \ \ t} \ sets (F t)} \ Pow \"
using sets.space_closed[of "F _"] by (auto simp: space_F)
next
fix A t assume "A \ {A. \t. {\ \ A. T \ \ t} \ sets (F t)}"
then have "{\ \ space (F t). T \ \ t} - {\ \ A. T \ \ t} \ sets (F t)"
using T stopping_timeD[measurable] by auto
also have "{\ \ space (F t). T \ \ t} - {\ \ A. T \ \ t} = {\ \ \ - A. T \ \ t}"
by (auto simp: space_F)
finally show "{\ \ \ - A. T \ \ t} \ sets (F t)" .
next
fix AA :: "nat \ 'a set" and t assume "range AA \ {A. \t. {\ \ A. T \ \ t} \ sets (F t)}"
then have "(\i. {\ \ AA i. T \ \ t}) \ sets (F t)" for t
by auto
also have "(\i. {\ \ AA i. T \ \ t}) = {\ \ \(AA ` UNIV). T \ \ t}"
by auto
finally show "{\ \ \(AA ` UNIV). T \ \ t} \ sets (F t)" .
qed auto
lemma sets_pre_sigma: "stopping_time F T \ sets (pre_sigma T) = {A. \t. {\\A. T \ \ t} \ sets (F t)}"
unfolding pre_sigma_def by (rule sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma])
lemma sets_pre_sigmaI: "stopping_time F T \ (\t. {\\A. T \ \ t} \ sets (F t)) \ A \ sets (pre_sigma T)"
unfolding sets_pre_sigma by auto
lemma pred_pre_sigmaI:
assumes T: "stopping_time F T"
shows "(\t. Measurable.pred (F t) (\\. P \ \ T \ \ t)) \ Measurable.pred (pre_sigma T) P"
unfolding pred_def space_F space_pre_sigma by (intro sets_pre_sigmaI[OF T]) simp
lemma sets_pre_sigmaD: "stopping_time F T \ A \ sets (pre_sigma T) \ {\\A. T \ \ t} \ sets (F t)"
unfolding sets_pre_sigma by auto
lemma stopping_time_le_const: "stopping_time F T \ s \ t \ Measurable.pred (F t) (\\. T \ \ s)"
using stopping_timeD[of F T] sets_F_mono[of _ t] by (auto simp: pred_def space_F)
lemma measurable_stopping_time_pre_sigma:
assumes T: "stopping_time F T" shows "T \ pre_sigma T \\<^sub>M borel"
proof (intro borel_measurableI_le sets_pre_sigmaI[OF T])
fix t t'
have "{\\space (F (min t' t)). T \ \ min t' t} \ sets (F (min t' t))"
using T unfolding pred_def[symmetric] by (rule stopping_timeD)
also have "\ \ sets (F t)"
by (rule sets_F_mono) simp
finally show "{\ \ {x \ space (pre_sigma T). T x \ t'}. T \ \ t} \ sets (F t)"
by (simp add: space_pre_sigma space_F)
qed
lemma mono_pre_sigma:
assumes T: "stopping_time F T" and S: "stopping_time F S"
and le: "\\. \ \ \ \ T \ \ S \"
shows "sets (pre_sigma T) \ sets (pre_sigma S)"
unfolding sets_pre_sigma[OF S] sets_pre_sigma[OF T]
proof safe
interpret sigma_algebra \<Omega> "{A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
using T by (rule sigma_algebra_pre_sigma)
fix A t assume A: "\t. {\\A. T \ \ t} \ sets (F t)"
then have "A \ \"
using sets_into_space by auto
from A have "{\\A. T \ \ t} \ {\\space (F t). S \ \ t} \ sets (F t)"
using stopping_timeD[OF S] by (auto simp: pred_def)
also have "{\\A. T \ \ t} \ {\\space (F t). S \ \ t} = {\\A. S \ \ t}"
using \<open>A \<subseteq> \<Omega>\<close> sets_into_space[of A] le by (auto simp: space_F intro: order_trans)
finally show "{\\A. S \ \ t} \ sets (F t)"
by auto
qed
lemma stopping_time_less_const:
assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\\. T \ < t)"
proof -
guess D :: "'t set" by (rule countable_dense_setE)
note D = this
show ?thesis
proof cases
assume *: "\t't''. t' < t'' \ t'' < t"
{ fix t' assume "t' < t"
with * have "{t' <..< t} \ {}"
by fastforce
with D(2)[OF _ this]
have "\d\D. t'< d \ d < t"
by auto }
note ** = this
show ?thesis
proof (rule measurable_cong[THEN iffD2])
show "T \ < t \ (\r\{r\D. r < t}. T \ \ r)" for \
by (auto dest: ** intro: less_imp_le)
show "Measurable.pred (F t) (\w. \r\{r \ D. r < t}. T w \ r)"
by (intro measurable_pred_countable stopping_time_le_const[OF T] countable_Collect D) auto
qed
next
assume "\ (\t't''. t' < t'' \ t'' < t)"
then obtain t' where t': "t' < t" "\t''. t'' < t \ t'' \ t'"
by (auto simp: not_less[symmetric])
show ?thesis
proof (rule measurable_cong[THEN iffD2])
show "T \ < t \ T \ \ t'" for \
using t' by auto
show "Measurable.pred (F t) (\w. T w \ t')"
using \<open>t'<t\<close> by (intro stopping_time_le_const[OF T]) auto
qed
qed
qed
lemma stopping_time_eq_const: "stopping_time F T \ Measurable.pred (F t) (\\. T \ = t)"
unfolding eq_iff using stopping_time_less_const[of T t]
by (intro pred_intros_logic stopping_time_le_const) (auto simp: not_less[symmetric] )
lemma stopping_time_less:
assumes T: "stopping_time F T" and S: "stopping_time F S"
shows "Measurable.pred (pre_sigma T) (\\. T \ < S \)"
proof (rule pred_pre_sigmaI[OF T])
fix t
obtain D :: "'t set"
where [simp]: "countable D" and semidense_D: "\x y. x < y \ (\b\D. x \ b \ b < y)"
using countable_separating_set_linorder2 by auto
show "Measurable.pred (F t) (\\. T \ < S \ \ T \ \ t)"
proof (rule measurable_cong[THEN iffD2])
let ?f = "\\. if T \ = t then \ S \ \ t else \s\{s\D. s \ t}. T \ \ s \ \ (S \ \ s)"
{ fix \<omega> assume "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
then have "T \ < min t (S \)"
by auto
then obtain r where "r \ D" "T \ \ r" "r < min t (S \)"
by (metis semidense_D)
then have "\s\{s\D. s \ t}. T \ \ s \ s < S \"
by auto }
then show "(T \ < S \ \ T \ \ t) = ?f \" for \
by (auto simp: not_le)
show "Measurable.pred (F t) ?f"
by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
stopping_time_le_const predE stopping_time_eq_const T S)
auto
qed
qed
end
lemma stopping_time_SUP_enat:
fixes T :: "nat \ ('a \ enat)"
shows "(\i. stopping_time F (T i)) \ stopping_time F (SUP i. T i)"
unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
lemma less_eSuc_iff: "a < eSuc b \ (a \ b \ a \ \)"
by (cases a) auto
lemma stopping_time_Inf_enat:
fixes F :: "enat \ 'a measure"
assumes F: "filtration \ F"
assumes P: "\i. Measurable.pred (F i) (P i)"
shows "stopping_time F (\\. Inf {i. P i \})"
proof (rule stopping_timeI, cases)
fix t :: enat assume "t = \" then show "Measurable.pred (F t) (\\. Inf {i. P i \} \ t)"
by auto
next
fix t :: enat assume "t \ \"
moreover
{ fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
with \<open>t \<noteq> \<infinity>\<close> have "(\<exists>i\<le>t. P i \<omega>)"
unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"] simp: less_eSuc_iff) }
ultimately have *: "\\. Inf {i. P i \} \ t \ (\i\{..t}. P i \)"
by (auto intro!: Inf_lower2)
show "Measurable.pred (F t) (\\. Inf {i. P i \} \ t)"
unfolding * using filtration.sets_F_mono[OF F, of _ t] P
by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
qed
lemma stopping_time_Inf_nat:
fixes F :: "nat \ 'a measure"
assumes F: "filtration \ F"
assumes P: "\i. Measurable.pred (F i) (P i)" and wf: "\i \. \ \ \ \ \n. P n \"
shows "stopping_time F (\\. Inf {i. P i \})"
unfolding stopping_time_def
proof (intro allI, subst measurable_cong)
fix t \<omega> assume "\<omega> \<in> space (F t)"
then have "\ \ \"
using filtration.space_F[OF F] by auto
from wf[OF this] have "((LEAST n. P n \) \ t) = (\i\t. P i \)"
by (rule LeastI2_wellorder_ex) auto
then show "(Inf {i. P i \} \ t) = (\i\{..t}. P i \)"
by (simp add: Inf_nat_def Bex_def)
next
fix t from P show "Measurable.pred (F t) (\w. \i\{..t}. P i w)"
using filtration.sets_F_mono[OF F, of _ t]
by (intro pred_intros_countable_bounded) (auto simp: pred_def filtration.space_F[OF F])
qed
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
