Quelle Stopping_Time.thy Sprache: Isabelle

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

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 -
  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 \<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

quality97%

¤ 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.0.15Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.