Quelle  Stopping_Time.thy

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

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 🚫› m

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"
    { 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 ‹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