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