Theory HOL-Probability.Stopping_Time
section ‹Stopping times›
theory Stopping_Time
imports "HOL-Analysis.Analysis"
begin
subsection ‹Stopping Time›
text ‹This is also called strong stopping time. Then stopping time is T with alternative is
‹T x < t› measurable.›
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 →⇩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 ‹Filtration›
locale filtration =
fixes Ω :: "'a set" and F :: "'t::{linorder_topology, second_countable_topology} ⇒ '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 ‹$\sigma$-algebra of a Stopping Time›
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 →⇩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 Ω "{A. ∀t. {ω∈A. T ω ≤ t} ∈ 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 ‹A ⊆ Ω› 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 -
obtain D :: "'t set"
where D: "countable D" "⋀X. open X ⟹ X ≠ {} ⟹ ∃d∈D. d ∈ X"
using countable_dense_setE by auto
show ?thesis
proof cases
assume *: "∀t'<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'' < 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 ‹t'<t› 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 ω assume "T ω ≤ t" "T ω ≠ t" "T ω < S ω"
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 ω assume "Inf {i. P i ω} ≤ t"
with ‹t ≠ ∞› have "(∃i≤t. P i ω)"
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 ω assume "ω ∈ 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