Theory Stochastic_Process

(*  Author:     Ata Keskin, TU München 
*)

theory Stochastic_Process
imports Filtered_Measure Measure_Space_Supplement "HOL-Probability.Independent_Family"
begin      

section ‹Stochastic Processes›

subsection ‹Stochastic Process›

text ‹A stochastic process is a collection of random variables, indexed by a type typ‹'b›.›

locale stochastic_process =
  fixes M t0 and X :: "'b :: {second_countable_topology, order_topology, t2_space} ⇒ 'a ⇒ 'c :: {second_countable_topology, banach}"
  assumes random_variable[measurable]: "⋀i. t0 ≤ i ⟹ X i ∈ borel_measurable M"
begin

definition left_continuous where "left_continuous = (AE ξ in M. ∀t. continuous (at_left t) (λi. X i ξ))"
definition right_continuous where "right_continuous = (AE ξ in M. ∀t. continuous (at_right t) (λi. X i ξ))"

end

lemma stochastic_process_const_fun:
  assumes "f ∈ borel_measurable M"
  shows "stochastic_process M t0 (λ_. f)" using assms by (unfold_locales)

lemma stochastic_process_const:
  shows "stochastic_process M t0 (λi _. c i)" by (unfold_locales) simp

text ‹In the following segment, we cover basic operations on stochastic processes.›

context stochastic_process
begin

lemma compose_stochastic:
  assumes "⋀i. t0 ≤ i ⟹ f i ∈ borel_measurable borel"
  shows "stochastic_process M t0 (λi ξ. (f i) (X i ξ))"
  by (unfold_locales) (intro measurable_compose[OF random_variable assms]) 

lemma norm_stochastic: "stochastic_process M t0 (λi ξ. norm (X i ξ))" by (fastforce intro: compose_stochastic)

lemma scaleR_right_stochastic:
  assumes "stochastic_process M t0 Y"
  shows "stochastic_process M t0 (λi ξ. (Y i ξ) *R (X i ξ))"
  using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp

lemma scaleR_right_const_fun_stochastic: 
  assumes "f ∈ borel_measurable M" 
  shows "stochastic_process M t0 (λi ξ. f ξ *R (X i ξ))" 
  by (unfold_locales) (intro borel_measurable_scaleR assms random_variable)

lemma scaleR_right_const_stochastic: "stochastic_process M t0 (λi ξ. c i *R (X i ξ))"
  by (unfold_locales) simp

lemma add_stochastic:
  assumes "stochastic_process M t0 Y"
  shows "stochastic_process M t0 (λi ξ. X i ξ + Y i ξ)"
  using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp

lemma diff_stochastic:
  assumes "stochastic_process M t0 Y"
  shows "stochastic_process M t0 (λi ξ. X i ξ - Y i ξ)"
  using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp

lemma uminus_stochastic: "stochastic_process M t0 (-X)" using scaleR_right_const_stochastic[of "λ_. -1"] by (simp add: fun_Compl_def)

lemma partial_sum_stochastic: "stochastic_process M t0 (λn ξ. ∑i∈{t0..n}. X i ξ)" by (unfold_locales) simp

lemma partial_sum'_stochastic: "stochastic_process M t0 (λn ξ. ∑i∈{t0..<n}. X i ξ)" by (unfold_locales) simp

end

lemma stochastic_process_sum:
  assumes "⋀i. i ∈ I ⟹ stochastic_process M t0 (X i)"
  shows "stochastic_process M t0 (λk ξ. ∑i ∈ I. X i k ξ)" using assms[THEN stochastic_process.random_variable] by (unfold_locales, auto)

subsubsection ‹Natural Filtration›

text ‹The natural filtration induced by a stochastic process term‹X› is the filtration generated by all events involving the process up to the time index term‹t›, i.e. ‹F t = σ({X s | s. s ≤ t})›.›

definition natural_filtration :: "'a measure ⇒ 'b ⇒ ('b ⇒ 'a ⇒ 'c :: topological_space) ⇒ 'b :: {second_countable_topology, order_topology} ⇒ 'a measure" where
  "natural_filtration M t0 Y = (λt. family_vimage_algebra (space M) {Y i | i. i ∈ {t0..t}} borel)"

abbreviation "nat_natural_filtration ≡ λM. natural_filtration M (0 :: nat)"
abbreviation "real_natural_filtration ≡ λM. natural_filtration M (0 :: real)"

lemma space_natural_filtration[simp]: "space (natural_filtration M t0 X t) = space M" unfolding natural_filtration_def space_family_vimage_algebra ..

lemma sets_natural_filtration: "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A. A ∈ borel})"
  unfolding natural_filtration_def sets_family_vimage_algebra by (intro sigma_sets_eqI) blast+

lemma sets_natural_filtration': 
  assumes "borel = sigma UNIV S"
  shows "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A. A ∈ S})"
proof (subst sets_natural_filtration, intro sigma_sets_eqI, clarify)
  fix i and A :: "'a set" assume asm: "i ∈ {t0..t}" "A ∈ sets borel"
  hence "A ∈ sigma_sets UNIV S" unfolding assms by simp
  thus "X i -` A ∩ space M ∈ sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M |A. A ∈ S})"
  proof (induction)
    case (Compl a)
    have "X i -` (UNIV - a) ∩ space M = space M - (X i -` a ∩ space M)" by blast
    then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger
  next
    case (Union a)
    have "X i -` ⋃ (range a) ∩ space M = ⋃ (range (λj. X i -` a j ∩ space M))" by blast
    then show ?case using Union(2)[THEN sigma_sets.Union] by presburger
  qed (auto intro: asm sigma_sets.Empty)
qed (intro sigma_sets.Basic, force simp add: assms)

lemma sets_natural_filtration_open: 
  "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A. open A})"
  using sets_natural_filtration' by (force simp only: borel_def mem_Collect_eq)

lemma sets_natural_filtration_oi: 
  "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A :: _ :: {linorder_topology, second_countable_topology} set. A ∈ range greaterThan})" 
  by (rule sets_natural_filtration'[OF borel_Ioi])

lemma sets_natural_filtration_io:
  "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A :: _ :: {linorder_topology, second_countable_topology} set. A ∈ range lessThan})" 
  by (rule sets_natural_filtration'[OF borel_Iio])

lemma sets_natural_filtration_ci:
  "sets (natural_filtration M t0 X t) = sigma_sets (space M) (⋃i∈{t0..t}. {X i -` A ∩ space M | A :: real set. A ∈ range atLeast})" 
  by (rule sets_natural_filtration'[OF borel_Ici])

context stochastic_process
begin

lemma subalgebra_natural_filtration: 
  shows "subalgebra M (natural_filtration M t0 X i)" 
  unfolding subalgebra_def using measurable_family_iff_sets by (force simp add: natural_filtration_def)

lemma filtered_measure_natural_filtration: 
  shows "filtered_measure M (natural_filtration M t0 X) t0"
    by (unfold_locales) (intro subalgebra_natural_filtration, simp only: sets_natural_filtration, intro sigma_sets_subseteq, force) 

text ‹In order to show that the natural filtration constitutes a filtered ‹σ›-finite measure, we need to provide a countable exhausting set in the preimage of term‹X t0›.›

lemma sigma_finite_filtered_measure_natural_filtration:
  assumes exhausting_set: "countable A" "(⋃A) = space M" "⋀a. a ∈ A ⟹ emeasure M a ≠ ∞" "⋀a. a ∈ A ⟹ ∃b ∈ borel. a = X t0 -` b ∩ space M"
    shows "sigma_finite_filtered_measure M (natural_filtration M t0 X) t0"
proof (unfold_locales)
  have "A ⊆ sets (restr_to_subalg M (natural_filtration M t0 X t0))" using exhausting_set by (simp add: sets_restr_to_subalg[OF subalgebra_natural_filtration] sets_natural_filtration) fast
  moreover have "⋃ A = space (restr_to_subalg M (natural_filtration M t0 X t0))" unfolding space_restr_to_subalg using exhausting_set by simp
  moreover have "∀a∈A. emeasure (restr_to_subalg M (natural_filtration M t0 X t0)) a ≠ ∞" using calculation(1) exhausting_set(3) 
    by (auto simp add: sets_restr_to_subalg[OF subalgebra_natural_filtration] emeasure_restr_to_subalg[OF subalgebra_natural_filtration])
  ultimately show "∃A. countable A ∧ A ⊆ sets (restr_to_subalg M (natural_filtration M t0 X t0)) ∧ ⋃ A = space (restr_to_subalg M (natural_filtration M t0 X t0)) ∧ (∀a∈A. emeasure (restr_to_subalg M (natural_filtration M t0 X t0)) a ≠ ∞)" using exhausting_set by blast
  show "⋀i j. ⟦t0 ≤ i; i ≤ j⟧ ⟹ sets (natural_filtration M t0 X i) ⊆ sets (natural_filtration M t0 X j)" using filtered_measure.subalgebra_F[OF filtered_measure_natural_filtration] by (simp add: subalgebra_def)
qed (auto intro: subalgebra_natural_filtration)

lemma finite_filtered_measure_natural_filtration:
  assumes "finite_measure M"
  shows "finite_filtered_measure M (natural_filtration M t0 X) t0" 
  using finite_measure.axioms[OF assms] filtered_measure_natural_filtration by intro_locales

end

text ‹Filtration generated by independent variables.›

lemma (in prob_space) indep_set_natural_filtration:
  assumes "t0 ≤ s" "s < t" "indep_vars (λ_. borel) X {t0..}"
  shows "indep_set (natural_filtration M t0 X s) (vimage_algebra (space M) (X t) borel)"
proof -
  have "indep_sets (λi. {X i -` A ∩ space M |A. A ∈ sets borel}) (⋃(range (case_bool {t0..s} {t})))" 
    using assms 
    by (intro assms(3)[unfolded indep_vars_def, THEN conjunct2, THEN indep_sets_mono]) (auto simp add: case_bool_if)
  thus ?thesis unfolding indep_set_def using assms
    by (intro indep_sets_cong[THEN iffD1, OF refl _ indep_sets_collect_sigma[of "λi. {X i -` A ∩ space M | A. A ∈ borel}" "case_bool {t0..s} {t}"]])
       (simp add: sets_natural_filtration sets_vimage_algebra split: bool.split, simp, intro Int_stableI, clarsimp, metis sets.Int vimage_Int Int_commute Int_left_absorb Int_left_commute, force simp add: disjoint_family_on_def split: bool.split)
qed

subsection ‹Adapted Process›

text ‹We call a collection a stochastic process term‹X› adapted if term‹X i› is term‹F i›-borel-measurable for all indices term‹i :: 't›.›
                                
locale adapted_process = filtered_measure M F t0 for M F t0 and X :: "_ ⇒ _ ⇒ _ :: {second_countable_topology, banach}" +
  assumes adapted[measurable]: "⋀i. t0 ≤ i ⟹ X i ∈ borel_measurable (F i)"
begin

lemma adaptedE[elim]:
  assumes "⟦⋀j i. t0 ≤ j ⟹ j ≤ i ⟹ X j ∈ borel_measurable (F i)⟧ ⟹ P"
  shows P
  using assms using adapted by (metis dual_order.trans borel_measurable_subalgebra sets_F_mono space_F)

lemma adaptedD:
  assumes "t0 ≤ j" "j ≤ i" 
  shows "X j ∈ borel_measurable (F i)" using assms adaptedE by meson

end

lemma (in filtered_measure) adapted_process_const_fun:
  assumes "f ∈ borel_measurable (F t0)"
  shows "adapted_process M F t0 (λ_. f)"
  using measurable_from_subalg subalgebra_F assms by (unfold_locales) blast

lemma (in filtered_measure) adapted_process_const:
  shows "adapted_process M F t0 (λi _. c i)" by (unfold_locales) simp


text ‹Again, we cover basic operations.›

context adapted_process
begin

lemma compose_adapted:
  assumes "⋀i. t0 ≤ i ⟹ f i ∈ borel_measurable borel"
  shows "adapted_process M F t0 (λi ξ. (f i) (X i ξ))"
  by (unfold_locales) (intro measurable_compose[OF adapted assms])

lemma norm_adapted: "adapted_process M F t0 (λi ξ. norm (X i ξ))" by (fastforce intro: compose_adapted)

lemma scaleR_right_adapted:
  assumes "adapted_process M F t0 R"
  shows "adapted_process M F t0 (λi ξ. (R i ξ) *R (X i ξ))"
  using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp
  
lemma scaleR_right_const_fun_adapted:
  assumes "f ∈ borel_measurable (F t0)" 
  shows "adapted_process M F t0 (λi ξ. f ξ *R (X i ξ))"
  using assms by (fast intro: scaleR_right_adapted adapted_process_const_fun)

lemma scaleR_right_const_adapted: "adapted_process M F t0 (λi ξ. c i *R (X i ξ))" by (unfold_locales) simp

lemma add_adapted:
  assumes "adapted_process M F t0 Y"
  shows "adapted_process M F t0 (λi ξ. X i ξ + Y i ξ)"
  using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp

lemma diff_adapted:
  assumes "adapted_process M F t0 Y"
  shows "adapted_process M F t0 (λi ξ. X i ξ - Y i ξ)"
  using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp

lemma uminus_adapted: "adapted_process M F t0 (-X)" using scaleR_right_const_adapted[of "λ_. -1"] by (simp add: fun_Compl_def)

lemma partial_sum_adapted: "adapted_process M F t0 (λn ξ. ∑i∈{t0..n}. X i ξ)" 
proof (unfold_locales)
  fix i :: 'b
  have "X j ∈ borel_measurable (F i)" if "t0 ≤ j" "j ≤ i" for j using that adaptedE by meson
  thus "(λξ. ∑i∈{t0..i}. X i ξ) ∈ borel_measurable (F i)" by simp
qed

lemma partial_sum'_adapted: "adapted_process M F t0 (λn ξ. ∑i∈{t0..<n}. X i ξ)" 
proof (unfold_locales)
  fix i :: 'b
  have "X j ∈ borel_measurable (F i)" if "t0 ≤ j" "j < i" for j using that adaptedE by fastforce
  thus "(λξ. ∑i∈{t0..<i}. X i ξ) ∈ borel_measurable (F i)" by simp
qed

end

text ‹In the dicrete time case, we have the following lemmas which will be useful later on.›

lemma (in nat_filtered_measure) partial_sum_Suc_adapted:
  assumes "adapted_process M F 0 X"
  shows "adapted_process M F 0 (λn ξ. ∑i<n. X (Suc i) ξ)"
proof (unfold_locales)
  interpret adapted_process M F 0 X using assms by blast
  fix i
  have "X j ∈ borel_measurable (F i)" if "j ≤ i" for j using that adaptedD by blast
  thus "(λξ. ∑i<i. X (Suc i) ξ) ∈ borel_measurable (F i)" by auto
qed

lemma (in enat_filtered_measure) partial_sum_eSuc_adapted:
  assumes "adapted_process M F 0 X"
  shows "adapted_process M F 0 (λn ξ. ∑i<n. X (eSuc i) ξ)"
proof (unfold_locales)
  interpret adapted_process M F 0 X using assms by blast
  fix i
  have "X (eSuc j) ∈ borel_measurable (F i)" if "j < i" for j using that adaptedD by (simp add: ileI1)
  thus "(λξ. ∑i<i. X (eSuc i) ξ) ∈ borel_measurable (F i)" by auto
qed

lemma (in filtered_measure) adapted_process_sum:
  assumes "⋀i. i ∈ I ⟹ adapted_process M F t0 (X i)"
  shows "adapted_process M F t0 (λk ξ. ∑i ∈ I. X i k ξ)" 
proof -
  {
    fix i k assume "i ∈ I" and asm: "t0 ≤ k"
    then interpret adapted_process M F t0 "X i" using assms by simp
    have "X i k ∈ borel_measurable M" "X i k ∈ borel_measurable (F k)" using measurable_from_subalg subalgebras adapted asm by (blast, simp)
  }
  thus ?thesis by (unfold_locales) simp
qed

text ‹An adapted process is necessarily a stochastic process.›

sublocale adapted_process ⊆ stochastic_process using measurable_from_subalg subalgebras adapted by (unfold_locales) blast

text ‹A stochastic process is always adapted to the natural filtration it generates.›

lemma (in stochastic_process) adapted_process_natural_filtration: "adapted_process M (natural_filtration M t0 X) t0 X"
  using filtered_measure_natural_filtration
  by (intro_locales) (auto simp add: natural_filtration_def intro!: adapted_process_axioms.intro measurable_family_vimage_algebra) 

subsection ‹Progressively Measurable Process›

locale progressive_process = filtered_measure M F t0 for M F t0 and X :: "_ ⇒ _ ⇒ _ :: {second_countable_topology, banach}" +
  assumes progressive[measurable]: "⋀t. t0 ≤ t ⟹ (λ(i, x). X i x) ∈ borel_measurable (restrict_space borel {t0..t} ⨂M F t)"
begin

lemma progressiveD:
  assumes "S ∈ borel"
  shows "(λ(j, ξ). X j ξ) -` S ∩ ({t0..i} × space M) ∈ (restrict_space borel {t0..i} ⨂M F i)" 
  using measurable_sets[OF progressive, OF _ assms, of i]
  by (cases "t0 ≤ i") (auto simp add: space_restrict_space sets_pair_measure space_pair_measure)

end

lemma (in filtered_measure) progressive_process_const_fun:
  assumes "f ∈ borel_measurable (F t0)"
  shows "progressive_process M F t0 (λ_. f)"
proof (unfold_locales)
  fix i assume asm: "t0 ≤ i"
  have "f ∈ borel_measurable (F i)" using borel_measurable_mono[OF order.refl asm] assms by blast
  thus "case_prod (λ_. f) ∈ borel_measurable (restrict_space borel {t0..i} ⨂M F i)" using measurable_compose[OF measurable_snd] by simp
qed

lemma (in filtered_measure) progressive_process_const:
  assumes "c ∈ borel_measurable borel"
  shows "progressive_process M F t0 (λi _. c i)"
  using assms by (unfold_locales) (auto simp add: measurable_split_conv intro!: measurable_compose[OF measurable_fst] measurable_restrict_space1)

context progressive_process
begin

lemma compose_progressive:
  assumes "case_prod f ∈ borel_measurable borel"
  shows "progressive_process M F t0 (λi ξ. (f i) (X i ξ))"
proof
  fix i assume asm: "t0 ≤ i"
  have "(λ(j, ξ). (j, X j ξ)) ∈ (restrict_space borel {t0..i} ⨂M F i) →M borel ⨂M borel" 
    using progressive[OF asm] measurable_fst''[OF measurable_restrict_space1, OF measurable_id] 
    by (auto simp add: measurable_pair_iff measurable_split_conv)
  moreover have "(λ(j, ξ). f j (X j ξ)) = case_prod f o ((λ(j, y). (j, y)) o (λ(j, ξ). (j, X j ξ)))" by fastforce
  ultimately show "(λ(j, ξ). (f j) (X j ξ)) ∈ borel_measurable (restrict_space borel {t0..i} ⨂M F i)" using assms by (simp add: borel_prod)
qed

lemma norm_progressive: "progressive_process M F t0 (λi ξ. norm (X i ξ))" using measurable_compose[OF progressive borel_measurable_norm] by (unfold_locales) simp

lemma scaleR_right_progressive:
  assumes "progressive_process M F t0 R"
  shows "progressive_process M F t0 (λi ξ. (R i ξ) *R (X i ξ))"
  using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms)
  
lemma scaleR_right_const_fun_progressive: 
  assumes "f ∈ borel_measurable (F t0)" 
  shows "progressive_process M F t0 (λi ξ. f ξ *R (X i ξ))"
  using assms by (fast intro: scaleR_right_progressive progressive_process_const_fun)

lemma scaleR_right_const_progressive: 
  assumes "c ∈ borel_measurable borel"
  shows "progressive_process M F t0 (λi ξ. c i *R (X i ξ))" 
  using assms by (fastforce intro: scaleR_right_progressive progressive_process_const)

lemma add_progressive:
  assumes "progressive_process M F t0 Y"
  shows "progressive_process M F t0 (λi ξ. X i ξ + Y i ξ)"
  using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms)

lemma diff_progressive:
  assumes "progressive_process M F t0 Y"
  shows "progressive_process M F t0 (λi ξ. X i ξ - Y i ξ)"
  using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms)

lemma uminus_progressive: "progressive_process M F t0 (-X)" using scaleR_right_const_progressive[of "λ_. -1"] by (simp add: fun_Compl_def)

end

text ‹A progressively measurable process is also adapted.›

sublocale progressive_process ⊆ adapted_process using measurable_compose_rev[OF progressive measurable_Pair1'] 
  unfolding prod.case space_restrict_space
  by unfold_locales simp

text ‹In the discrete setting, adaptedness is equivalent to progressive measurability.›

theorem (in nat_filtered_measure) progressive_iff_adapted: "progressive_process M F 0 X ⟷ adapted_process M F 0 X"
proof (intro iffI)
  assume asm: "progressive_process M F 0 X"
  interpret progressive_process M F 0 X by (rule asm)
  show "adapted_process M F 0 X" ..
next
  assume asm: "adapted_process M F 0 X"
  interpret adapted_process M F 0 X by (rule asm) 
  show "progressive_process M F 0 X"
  proof (unfold_locales, intro borel_measurableI)
    fix S :: "'b set" and i :: nat assume open_S: "open S"
    {
      fix j assume asm: "j ≤ i"
      hence "X j -` S ∩ space M ∈ F i" using adaptedD[of j, THEN measurable_sets] space_F open_S by fastforce
      moreover have "case_prod X -` S ∩ {j} × space M = {j} × (X j -` S ∩ space M)" for j by fast
      moreover have "{j :: nat} ∈ restrict_space borel {0..i}" using asm by (simp add: sets_restrict_space_iff)
      ultimately have "case_prod X -` S ∩ {j} × space M ∈ restrict_space borel {0..i} ⨂M F i" by simp
    }
    hence "(λj. (λ(x, y). X x y) -` S ∩ {j} × space M) ` {..i} ⊆ restrict_space borel {0..i} ⨂M F i" by blast
    moreover have "case_prod X -` S ∩ space (restrict_space borel {0..i} ⨂M F i) = (⋃j≤i. case_prod X -` S ∩ {j} × space M)" unfolding space_pair_measure space_restrict_space space_F by force  
    ultimately show "case_prod X -` S ∩ space (restrict_space borel {0..i} ⨂M F i) ∈ restrict_space borel {0..i} ⨂M F i" by (metis sets.countable_UN)
  qed
qed

theorem (in enat_filtered_measure) progressive_iff_adapted: "progressive_process M F 0 X ⟷ adapted_process M F 0 X"
proof (intro iffI)
  assume asm: "progressive_process M F 0 X"
  interpret progressive_process M F 0 X by (rule asm)
  show "adapted_process M F 0 X" ..
next
  assume asm: "adapted_process M F 0 X"
  interpret adapted_process M F 0 X by (rule asm) 
  show "progressive_process M F 0 X"
  proof (unfold_locales, intro borel_measurableI)
    fix S :: "'b set" and i :: enat assume open_S: "open S"
    {
      fix j assume asm: "j ≤ i"
      hence "X j -` S ∩ space M ∈ F i" using adaptedD[of j, THEN measurable_sets] space_F open_S by fastforce
      moreover have "case_prod X -` S ∩ {j} × space M = {j} × (X j -` S ∩ space M)" for j by fast
      moreover have "{j :: enat} ∈ restrict_space borel {0..i}" using asm by (simp add: sets_restrict_space_iff)
      ultimately have "case_prod X -` S ∩ {j} × space M ∈ restrict_space borel {0..i} ⨂M F i" by simp
    }
    hence "(λj. (λ(x, y). X x y) -` S ∩ {j} × space M) ` {..i} ⊆ restrict_space borel {0..i} ⨂M F i" by blast
    moreover have "case_prod X -` S ∩ space (restrict_space borel {0..i} ⨂M F i) = (⋃j≤i. case_prod X -` S ∩ {j} × space M)" unfolding space_pair_measure space_restrict_space space_F by force  
    ultimately show "case_prod X -` S ∩ space (restrict_space borel {0..i} ⨂M F i) ∈ restrict_space borel {0..i} ⨂M F i" by (metis sets.countable_UN)
  qed
qed

subsection ‹Predictable Process›

text ‹We introduce the constant term‹ΣP› to denote the predictable ‹σ›-algebra.›

context linearly_filtered_measure
begin

definition ΣP :: "('b × 'a) measure" where predictable_sigma: "ΣP ≡ sigma ({t0..} × space M) ({{s<..t} × A | A s t. A ∈ F s ∧ t0 ≤ s ∧ s < t} ∪ {{t0} × A | A. A ∈ F t0})"

lemma space_predictable_sigma[simp]: "space ΣP = ({t0..} × space M)" unfolding predictable_sigma space_measure_of_conv by blast

lemma sets_predictable_sigma: "sets ΣP = sigma_sets ({t0..} × space M) ({{s<..t} × A | A s t. A ∈ F s ∧ t0 ≤ s ∧ s < t} ∪ {{t0} × A | A. A ∈ F t0})" 
  unfolding predictable_sigma using space_F sets.sets_into_space by (subst sets_measure_of) fastforce+

lemma measurable_predictable_sigma_snd:
  assumes "countable ℐ" "ℐ ⊆ {{s<..t} | s t. t0 ≤ s ∧ s < t}" "{t0<..} ⊆ (⋃ℐ)"
  shows "snd ∈ ΣP →M F t0"
proof (intro measurableI)
  fix S :: "'a set" assume asm: "S ∈ F t0"
  have countable: "countable ((λI. I × S) ` ℐ)" using assms(1) by blast
  have "(λI. I × S) ` ℐ ⊆ {{s<..t} × A | A s t. A ∈ F s ∧ t0 ≤ s ∧  s < t}" using sets_F_mono[OF order_refl, THEN subsetD, OF _ asm] assms(2) by blast
  hence "(⋃I∈ℐ. I × S) ∪ {t0} × S ∈ ΣP" unfolding sets_predictable_sigma using asm by (intro sigma_sets_Un[OF sigma_sets_UNION[OF countable] sigma_sets.Basic] sigma_sets.Basic) blast+
  moreover have "snd -` S ∩ space ΣP = {t0..} × S" using sets.sets_into_space[OF asm] by fastforce
  moreover have "{t0} ∪ {t0<..} = {t0..}" by auto
  moreover have "(⋃I∈ℐ. I × S) ∪ {t0} × S = {t0..} × S" using assms(2,3) calculation(3) by fastforce
  ultimately show "snd -` S ∩ space ΣP ∈ ΣP" by argo
qed (auto)

lemma measurable_predictable_sigma_fst:
  assumes "countable ℐ" "ℐ ⊆ {{s<..t} | s t. t0 ≤ s ∧ s < t}" "{t0<..} ⊆ (⋃ℐ)"
  shows "fst ∈ ΣP →M borel"
proof -
  have "A × space M ∈ sets ΣP" if "A ∈ sigma_sets {t0..} {{s<..t} | s t. t0 ≤ s ∧ s < t}" for A unfolding sets_predictable_sigma using that 
  proof (induction rule: sigma_sets.induct)
    case (Basic a)
    thus ?case using space_F sets.top by blast
  next
    case (Compl a)
    have "({t0..} - a) × space M = {t0..} × space M - a × space M" by blast
    then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger
  next
    case (Union a)
    have "⋃ (range a) × space M = ⋃ (range (λi. a i × space M))" by blast
    then show ?case using Union(2)[THEN sigma_sets.Union] by presburger
  qed (auto)
  moreover have "restrict_space borel {t0..} = sigma {t0..} {{s<..t} | s t. t0 ≤ s ∧ s < t}"
  proof -
    have "sigma_sets {t0..} ((∩) {t0..} ` sigma_sets UNIV (range greaterThan)) = sigma_sets {t0..} {{s<..t} |s t. t0 ≤ s ∧ s < t}"
    proof (intro sigma_sets_eqI ; clarify)
      fix A :: "'b set" assume asm: "A ∈ sigma_sets UNIV (range greaterThan)"
      thus "{t0..} ∩ A ∈ sigma_sets {t0..} {{s<..t} |s t. t0 ≤ s ∧ s < t}"
      proof (induction rule: sigma_sets.induct)
        case (Basic a)
        then obtain s where s: "a = {s<..}" by blast
        show ?case
        proof (cases "t0 ≤ s")
          case True
          hence *: "{t0..} ∩ a = (⋃i ∈ ℐ. {s<..} ∩ i)" using s assms(3) by force
          have "((∩) {s<..} ` ℐ) ⊆ sigma_sets {t0..} {{s<..t} | s t. t0 ≤ s ∧ s < t}"
          proof (clarify)
            fix A assume "A ∈ ℐ"
            then obtain s' t' where A: "A = {s'<..t'}" "t0 ≤ s'" "s' < t'" using assms(2) by blast
            hence "{s<..} ∩ A = {max s s'<..t'}" by fastforce
            moreover have "t0 ≤ max s s'" using A True by linarith
            moreover have "max s s' < t'" if "s < t'" using A that by linarith
            moreover have "{s<..} ∩ A = {}" if "¬ s < t'" using A that by force
            ultimately show "{s<..} ∩ A ∈ sigma_sets {t0..} {{s<..t} |s t. t0 ≤ s ∧ s < t}" by (cases "s < t'") (blast, simp add: sigma_sets.Empty)
          qed
          thus ?thesis unfolding * using assms(1) by (intro sigma_sets_UNION) auto
        next
          case False
          hence "{t0..} ∩ a = {t0..}" using s by force
          thus ?thesis using sigma_sets_top by auto
        qed
      next
        case (Compl a)
        have "{t0..} ∩ (UNIV - a) = {t0..} - ({t0..} ∩ a)" by blast
        then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger
      next
        case (Union a)
        have "{t0..} ∩ ⋃ (range a) = ⋃ (range (λi. {t0..} ∩ a i))" by blast
        then show ?case using Union(2)[THEN sigma_sets.Union] by presburger
      qed (simp add: sigma_sets.Empty)
    next 
      fix s t assume asm: "t0 ≤ s" "s < t"
      hence *: "{s<..t} = {s<..} ∩ ({t0..} - {t<..})" by force
      have "{s<..} ∈ sigma_sets {t0..} ((∩) {t0..} ` sigma_sets UNIV (range greaterThan))" using asm by (intro sigma_sets.Basic) auto
      moreover have "{t0..} - {t<..} ∈ sigma_sets {t0..} ((∩) {t0..} ` sigma_sets UNIV (range greaterThan))" using asm by (intro sigma_sets.Compl sigma_sets.Basic) auto
      ultimately show "{s<..t} ∈ sigma_sets {t0..} ((∩) {t0..} ` sigma_sets UNIV (range greaterThan))" unfolding * Int_range_binary[of "{s<..}"] by (intro sigma_sets_Inter[OF _ binary_in_sigma_sets]) auto        
    qed
    thus ?thesis unfolding borel_Ioi restrict_space_def emeasure_sigma by (force intro: sigma_eqI)
  qed
  ultimately have "restrict_space borel {t0..} ⨂M sigma (space M) {} ⊆ sets ΣP" 
    unfolding sets_pair_measure space_restrict_space space_measure_of_conv
    using space_predictable_sigma sets.sigma_algebra_axioms[of ΣP] 
    by (intro sigma_algebra.sigma_sets_subset) (auto simp add: sigma_sets_empty_eq sets_measure_of_conv)
  moreover have "space (restrict_space borel {t0..} ⨂M sigma (space M) {}) = space ΣP" by (simp add: space_pair_measure)
  moreover have "fst ∈ restrict_space borel {t0..} ⨂M sigma (space M) {} →M borel" by (fastforce intro: measurable_fst''[OF measurable_restrict_space1, of "λx. x"]) 
  ultimately show ?thesis by (meson borel_measurable_subalgebra)
qed

end

locale predictable_process = linearly_filtered_measure M F t0 for M F t0 and X :: "_ ⇒ _ ⇒ _ :: {second_countable_topology, banach}" +
  assumes predictable: "(λ(t, x). X t x) ∈ borel_measurable ΣP"
begin

lemmas predictableD = measurable_sets[OF predictable, unfolded space_predictable_sigma]

end

lemma (in nat_filtered_measure) measurable_predictable_sigma_snd':
  shows "snd ∈ ΣP →M F 0"
  by (intro measurable_predictable_sigma_snd[of "range (λx. {Suc x})"]) (force | simp add: greaterThan_0)+

lemma (in nat_filtered_measure) measurable_predictable_sigma_fst':
  shows "fst ∈ ΣP →M borel"
  by (intro measurable_predictable_sigma_fst[of "range (λx. {Suc x})"]) (force | simp add: greaterThan_0)+

lemma (in enat_filtered_measure) measurable_predictable_sigma_snd':
  shows "snd ∈ ΣP →M F 0"
  by (intro measurable_predictable_sigma_snd[of "{{0<..∞}}"]) force+

lemma (in enat_filtered_measure) measurable_predictable_sigma_fst':
  shows "fst ∈ ΣP →M borel"
  by (intro measurable_predictable_sigma_fst[of "{{0<..∞}}"]) force+

lemma (in real_filtered_measure) measurable_predictable_sigma_snd':
  shows "snd ∈ ΣP →M F 0"
  using real_arch_simple by (intro measurable_predictable_sigma_snd[of "range (λx::nat. {0<..real (Suc x)})"]) (fastforce intro: add_increasing)+

lemma (in real_filtered_measure) measurable_predictable_sigma_fst':
  shows "fst ∈ ΣP →M borel"
  using real_arch_simple by (intro measurable_predictable_sigma_fst[of "range (λx::nat. {0<..real (Suc x)})"]) (fastforce intro: add_increasing)+

lemma (in ennreal_filtered_measure) measurable_predictable_sigma_snd':
  shows "snd ∈ ΣP →M F 0"
  by (intro measurable_predictable_sigma_snd[of "{{0<..∞}}"]) force+

lemma (in ennreal_filtered_measure) measurable_predictable_sigma_fst':
  shows "fst ∈ ΣP →M borel"
  by (intro measurable_predictable_sigma_fst[of "{{0<..∞}}"]) force+

text ‹We show sufficient conditions for functions constant in one argument to constitute a predictable process. In contrast to the cases before, this is not a triviality.›

lemma (in linearly_filtered_measure) predictable_process_const_fun:
  assumes "snd ∈ ΣP →M F t0" "f ∈ borel_measurable (F t0)"
    shows "predictable_process M F t0 (λ_. f)"
  using measurable_compose_rev[OF assms(2)] assms(1) by (unfold_locales) (auto simp add: measurable_split_conv)

lemma (in nat_filtered_measure) predictable_process_const_fun'[intro]:
  assumes "f ∈ borel_measurable (F 0)"
  shows "predictable_process M F 0 (λ_. f)"
  using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd'])

lemma (in enat_filtered_measure) predictable_process_const_fun'[intro]:
  assumes "f ∈ borel_measurable (F 0)"
  shows "predictable_process M F 0 (λ_. f)"
  using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd'])

lemma (in real_filtered_measure) predictable_process_const_fun'[intro]:
  assumes "f ∈ borel_measurable (F 0)"
  shows "predictable_process M F 0 (λ_. f)"
  using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd'])

lemma (in ennreal_filtered_measure) predictable_process_const_fun'[intro]:
  assumes "f ∈ borel_measurable (F 0)"
  shows "predictable_process M F 0 (λ_. f)"
  using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd'])

lemma (in linearly_filtered_measure) predictable_process_const:
  assumes "fst ∈ borel_measurable ΣP" "c ∈ borel_measurable borel"
  shows "predictable_process M F t0 (λi _. c i)"
  using assms by (unfold_locales) (simp add: measurable_split_conv)

lemma (in linearly_filtered_measure) predictable_process_const_const[intro]:
  shows "predictable_process M F t0 (λ_ _. c)"
  by (unfold_locales) simp

lemma (in nat_filtered_measure) predictable_process_const'[intro]:
  assumes "c ∈ borel_measurable borel"
  shows "predictable_process M F 0 (λi _. c i)"
  using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst'])

lemma (in enat_filtered_measure) predictable_process_const'[intro]:
  assumes "c ∈ borel_measurable borel"
  shows "predictable_process M F 0 (λi _. c i)"
  using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst'])

lemma (in real_filtered_measure) predictable_process_const'[intro]:
  assumes "c ∈ borel_measurable borel"
  shows "predictable_process M F 0 (λi _. c i)"
  using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst'])

lemma (in ennreal_filtered_measure) predictable_process_const'[intro]:
  assumes "c ∈ borel_measurable borel"
  shows "predictable_process M F 0 (λi _. c i)"
  using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst'])

context predictable_process
begin

lemma compose_predictable:
  assumes "fst ∈ borel_measurable ΣP" "case_prod f ∈ borel_measurable borel"
  shows "predictable_process M F t0 (λi ξ. (f i) (X i ξ))"
proof
  have "(λ(i, ξ). (i, X i ξ)) ∈ ΣP →M borel ⨂M borel" using predictable assms(1) by (auto simp add: measurable_pair_iff measurable_split_conv)
  moreover have "(λ(i, ξ). f i (X i ξ)) = case_prod f o (λ(i, ξ). (i, X i ξ))" by fastforce
  ultimately show "(λ(i, ξ). f i (X i ξ)) ∈ borel_measurable ΣP" unfolding borel_prod using assms by simp
qed

lemma norm_predictable: "predictable_process M F t0 (λi ξ. norm (X i ξ))" using measurable_compose[OF predictable borel_measurable_norm] 
  by (unfold_locales) (simp add: prod.case_distrib)

lemma scaleR_right_predictable:
  assumes "predictable_process M F t0 R"
  shows "predictable_process M F t0 (λi ξ. (R i ξ) *R (X i ξ))"
  using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv)

lemma scaleR_right_const_fun_predictable: 
  assumes "snd ∈ ΣP →M F t0" "f ∈ borel_measurable (F t0)" 
  shows "predictable_process M F t0 (λi ξ. f ξ *R (X i ξ))"
  using assms by (fast intro: scaleR_right_predictable predictable_process_const_fun)

lemma scaleR_right_const_predictable: 
  assumes "fst ∈ borel_measurable ΣP" "c ∈ borel_measurable borel"
  shows "predictable_process M F t0 (λi ξ. c i *R (X i ξ))" 
  using assms by (fastforce intro: scaleR_right_predictable predictable_process_const)

lemma scaleR_right_const'_predictable: "predictable_process M F t0 (λi ξ. c *R (X i ξ))" 
  by (fastforce intro: scaleR_right_predictable)

lemma add_predictable:
  assumes "predictable_process M F t0 Y"
  shows "predictable_process M F t0 (λi ξ. X i ξ + Y i ξ)"
  using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv)

lemma diff_predictable:
  assumes "predictable_process M F t0 Y"
  shows "predictable_process M F t0 (λi ξ. X i ξ - Y i ξ)"
  using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv)

lemma uminus_predictable: "predictable_process M F t0 (-X)" using scaleR_right_const'_predictable[of "-1"] by (simp add: fun_Compl_def)

end

text ‹Every predictable process is also progressively measurable.›

sublocale predictable_process ⊆ progressive_process
proof (unfold_locales)
  fix i :: 'b assume asm: "t0 ≤ i"
  {
    fix S :: "('b × 'a) set" assume "S ∈ {{s<..t} × A | A s t. A ∈ F s ∧ t0 ≤ s ∧ s < t} ∪ {{t0} × A | A. A ∈ F t0}"
    hence "(λx. x) -` S ∩ ({t0..i} × space M) ∈ restrict_space borel {t0..i} ⨂M F i"
    proof
      assume "S ∈ {{s<..t} × A | A s t. A ∈ F s ∧ t0 ≤ s ∧ s < t}"
      then obtain s t A where S_is: "S = {s<..t} × A" "t0 ≤ s" "s < t" "A ∈ F s" by blast
      hence "(λx. x) -` S ∩ ({t0..i} × space M) = {s<..min i t} × A" using sets.sets_into_space[OF S_is(4)] by auto
      then show ?thesis using S_is sets_F_mono[of s i] by (cases "s ≤ i") (fastforce simp add: sets_restrict_space_iff)+
    next
      assume "S ∈ {{t0} × A | A. A ∈ F t0}"
      then obtain A where S_is: "S = {t0} × A" "A ∈ F t0" by blast
      hence "(λx. x) -` S ∩ ({t0..i} × space M) = {t0} × A" using asm sets.sets_into_space[OF S_is(2)] by auto
      thus ?thesis using S_is(2) sets_F_mono[OF order_refl asm] asm by (fastforce simp add: sets_restrict_space_iff)
    qed
    hence "(λx. x) -` S ∩ space (restrict_space borel {t0..i} ⨂M F i) ∈ restrict_space borel {t0..i} ⨂M F i" by (simp add: space_pair_measure space_F[OF asm])
  }
  moreover have "{{s<..t} × A |A s t. A ∈ sets (F s) ∧ t0 ≤ s ∧ s < t} ∪ {{t0} × A |A. A ∈ sets (F t0)} ⊆ Pow ({t0..} × space M)" using sets.sets_into_space by force
  ultimately have "(λx. x) ∈ restrict_space borel {t0..i} ⨂M F i →M ΣP" using space_F[OF asm] by (intro measurable_sigma_sets[OF sets_predictable_sigma]) (fast, force simp add: space_pair_measure)
  thus "case_prod X ∈ borel_measurable (restrict_space borel {t0..i} ⨂M F i)" using predictable by simp
qed

text ‹The following lemma characterizes predictability in a discrete-time setting.›

lemma (in nat_filtered_measure) sets_in_filtration:
  assumes "(⋃i. {i} × A i) ∈ ΣP"
  shows "A (Suc i) ∈ F i" "A 0 ∈ F 0"
  using assms unfolding sets_predictable_sigma
proof (induction "(⋃i. {i} × A i)" arbitrary: A)
  case Basic
  {
    assume "∃S. (⋃i. {i} × A i) = {0} × S"
    then obtain S where S: "(⋃i. {i} × A i) = {0} × S" by blast
    hence "S ∈ F 0" using Basic by (fastforce simp add: times_eq_iff)
    moreover have "A i = {}" if "i ≠ 0" for i using that S unfolding bot_nat_def[symmetric] by blast
    moreover have "A 0 = S" using S by blast
    ultimately have "A 0 ∈ F 0" "A (Suc i) ∈ F i" for i by auto
  }
  note * = this
  {
    assume "∄S. (⋃i. {i} × A i) = {0} × S"
    then obtain s t B where B: "(⋃i. {i} × A i) = {s<..t} × B" "B ∈ sets (F s)" "s < t" using Basic by auto
    hence "A i = B" if "i ∈ {s<..t}" for i using that by fast
    moreover have "A i = {}" if "i ∉ {s<..t}" for i using B that by fastforce
    ultimately have "A 0 ∈ F 0" "A (Suc i) ∈ F i" for i using B sets_F_mono 
      by (simp, metis less_Suc_eq_le sets.empty_sets subset_eq bot_nat_0.extremum greaterThanAtMost_iff)
      
  }
  note ** = this
  show "A (Suc i) ∈ sets (F i)" "A 0 ∈ F 0" using *(2)[of i] *(1) **(2)[of i] **(1) by blast+
next
  case Empty
  {
    case 1
    then show ?case using Empty by simp
  next
    case 2
    then show ?case using Empty by simp
  }
next
  case (Compl a)
  have a_in: "a ⊆ {0..} × space M" using Compl(1) sets.sets_into_space sets_predictable_sigma space_predictable_sigma by metis
  hence A_in: "A i ⊆ space M" for i using Compl(4) by blast
  have a: "a = {0..} × space M - (⋃i. {i} × A i)" using a_in Compl(4) by blast
  also have "... = - (⋂j. - ({j} × (space M - A j)))" by blast
  also have "... = (⋃j. {j} × (space M - A j))" by blast
  finally have *: "(space M - A (Suc i)) ∈ F i" "(space M - A 0) ∈ F 0" using Compl(2,3) by auto
  {
    case 1
    then show ?case using * A_in by (metis bot_nat_0.extremum double_diff sets.Diff sets.top sets_F_mono sets_le_imp_space_le space_F)
 next
    case 2
    then show ?case using * A_in by (metis bot_nat_0.extremum double_diff sets.Diff sets.top sets_F_mono sets_le_imp_space_le space_F)
  }
next
  case (Union a)
  have a_in: "a i ⊆ {0..} × space M" for i using Union(1) sets.sets_into_space sets_predictable_sigma space_predictable_sigma by metis
  hence A_in: "A i ⊆ space M" for i using Union(4) by blast
  have "snd x ∈ snd ` (a i ∩ ({fst x} × space M))" if "x ∈ a i" for i x using that a_in by fastforce
  hence a_i: "a i = (⋃j. {j} × (snd ` (a i ∩ ({j} × space M))))" for i by force
  have A_i: "A i = snd ` (⋃ (range a) ∩ ({i} × space M))" for i unfolding Union(4) using A_in by force 
  have *: "snd ` (a j ∩ ({Suc i} × space M)) ∈ F i" "snd ` (a j ∩ ({0} × space M)) ∈ F 0" for j using Union(2,3)[OF a_i] by auto
  {
    case 1
    have "(⋃j. snd ` (a j ∩ ({Suc i} × space M))) ∈ F i" using * by fast
    moreover have "(⋃j. snd ` (a j ∩ ({Suc i} × space M))) = snd ` (⋃ (range a) ∩ ({Suc i} × space M))" by fast
    ultimately show ?case using A_i by metis
  next
    case 2
    have "(⋃j. snd ` (a j ∩ ({0} × space M))) ∈ F 0" using * by fast
    moreover have "(⋃j. snd ` (a j ∩ ({0} × space M))) = snd ` (⋃ (range a) ∩ ({0} × space M))" by fast
    ultimately show ?case using A_i by metis
  }
qed

text ‹This leads to the following useful fact.›

lemma (in nat_filtered_measure) predictable_implies_adapted_Suc: 
  assumes "predictable_process M F 0 X"
  shows "adapted_process M F 0 (λi. X (Suc i))"
proof (unfold_locales, intro borel_measurableI)
  interpret predictable_process M F 0 X by (rule assms)
  fix S :: "'b set" and i assume open_S: "open S"
  have "{Suc i} = {i<..Suc i}" by fastforce
  hence "{Suc i} × space M ∈ ΣP" using space_F[symmetric, of i] unfolding sets_predictable_sigma by (intro sigma_sets.Basic) blast
  moreover have "case_prod X -` S ∩ (UNIV × space M) ∈ ΣP" unfolding atLeast_0[symmetric] using open_S by (intro predictableD, simp add: borel_open)
  ultimately have "case_prod X -` S ∩ ({Suc i} × space M) ∈ ΣP" unfolding sets_predictable_sigma using space_F sets.sets_into_space
    by (subst Times_Int_distrib1[of "{Suc i}" UNIV "space M", simplified], subst inf.commute, subst Int_assoc[symmetric], subst Int_range_binary) 
       (intro sigma_sets_Inter binary_in_sigma_sets, fast)+
  moreover have "case_prod X -` S ∩ ({Suc i} × space M) = {Suc i} × (X (Suc i) -` S ∩ space M)" by (auto simp add: le_Suc_eq)
  moreover have "... = (⋃j. {j} × (if j = Suc i then (X (Suc i) -` S ∩ space M) else {}))" by (force split: if_splits)
  ultimately have "(⋃j. {j} × (if j = Suc i then (X (Suc i) -` S ∩ space M) else {})) ∈ ΣP" by argo
  thus "X (Suc i) -` S ∩ space (F i) ∈ sets (F i)" using sets_in_filtration[of "λj. if j = Suc i then (X (Suc i) -` S ∩ space M) else {}"] space_F[OF zero_le] by presburger
qed

text ‹The following lemma characterizes predictability in the discrete setting.›

theorem (in nat_filtered_measure) predictable_process_iff: "predictable_process M F 0 X ⟷ adapted_process M F 0 (λi. X (Suc i)) ∧ X 0 ∈ borel_measurable (F 0)"
proof (intro iffI)
  assume asm: "adapted_process M F 0 (λi. X (Suc i)) ∧ X 0 ∈ borel_measurable (F 0)"
  interpret adapted_process M F 0 "λi. X (Suc i)" using asm by blast
  have "(λ(x, y). X x y) ∈ borel_measurable ΣP"
  proof (intro borel_measurableI)
    fix S :: "'b set" assume open_S: "open S"
    have "{i} × (X i -` S ∩ space M) ∈ sets ΣP" for i 
    proof (cases i)
      case 0
      then show ?thesis unfolding sets_predictable_sigma 
        using measurable_sets[OF _ borel_open[OF open_S], of "X 0" "F 0"] asm by auto
    next
      case (Suc i)
      have "{Suc i} = {i<..Suc i}" by fastforce
      then show ?thesis unfolding sets_predictable_sigma 
        using measurable_sets[OF adapted borel_open[OF open_S], of i] 
        by (intro sigma_sets.Basic, auto simp add: Suc)
    qed
    moreover have "(λ(x, y). X x y) -` S ∩ space ΣP = (⋃i. {i} × (X i -` S ∩ space M))" by fastforce
    ultimately show "(λ(x, y). X x y) -` S ∩ space ΣP ∈ sets ΣP" by simp
  qed
  thus "predictable_process M F 0 X" by (unfold_locales)
next
  assume asm: "predictable_process M F 0 X"
  interpret predictable_process M F 0 X using asm by blast
  show "adapted_process M F 0 (λi. X (Suc i)) ∧ X 0 ∈ borel_measurable (F 0)" using predictable_implies_adapted_Suc asm by auto
qed

corollary (in nat_filtered_measure) predictable_processI[intro!]:
  assumes "X 0 ∈ borel_measurable (F 0)" "⋀i. X (Suc i) ∈ borel_measurable (F i)"
  shows "predictable_process M F 0 X"
  unfolding predictable_process_iff
  using assms
  by (meson adapted_process.intro adapted_process_axioms_def filtered_measure_axioms)
                                                                            
end