# Theory Discrete_Time_Markov_Process

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

section ‹Discrete-time Markov Processes›

text ‹In this file we construct discrete-time Markov processes, e.g. with arbitrary state spaces.›

theory Discrete_Time_Markov_Process
imports Markov_Models_Auxiliary
begin

lemma measure_eqI_PiM_sequence:
fixes M :: "nat ⇒ 'a measure"
assumes *[simp]: "sets P = PiM UNIV M" "sets Q = PiM UNIV M"
assumes eq: "⋀A n. (⋀i. A i ∈ sets (M i)) ⟹
P (prod_emb UNIV M {..n} (Pi⇩E {..n} A)) = Q (prod_emb UNIV M {..n} (Pi⇩E {..n} A))"
assumes A: "finite_measure P"
shows "P = Q"
proof (rule measure_eqI_PiM_infinite[OF * _ A])
fix J :: "nat set" and F'
assume J: "finite J" "⋀i. i ∈ J ⟹ F' i ∈ sets (M i)"

define n where "n = (if J = {} then 0 else Max J)"
define F where "F i = (if i ∈ J then F' i else space (M i))" for i
then have F[simp, measurable]: "F i ∈ sets (M i)" for i
using J by auto
have emb_eq: "prod_emb UNIV M J (Pi⇩E J F') = prod_emb UNIV M {..n} (Pi⇩E {..n} F)"
proof cases
assume "J = {}" then show ?thesis
by (auto simp add: n_def F_def[abs_def] prod_emb_def PiE_def)
next
assume "J ≠ {}" then show ?thesis
by (auto simp: prod_emb_def PiE_iff F_def n_def less_Suc_eq_le ‹finite J› split: if_split_asm)
qed

show "emeasure P (prod_emb UNIV M J (Pi⇩E J F')) = emeasure Q (prod_emb UNIV M J (Pi⇩E J F'))"
unfolding emb_eq by (rule eq) fact
qed

lemma distr_cong_simp:
"M = K ⟹ sets N = sets L ⟹ (⋀x. x ∈ space M =simp=> f x = g x) ⟹ distr M N f = distr K L g"
unfolding simp_implies_def by (rule distr_cong)

subsection ‹Constructing Discrete-Time Markov Processes›

locale discrete_Markov_process =
fixes M :: "'a measure" and K :: "'a ⇒ 'a measure"
assumes K[measurable]: "K ∈ M →⇩M prob_algebra M"
begin

lemma space_K: "x ∈ space M ⟹ space (K x) = space M"
using K unfolding prob_algebra_def unfolding measurable_restrict_space2_iff
by (auto dest: subprob_measurableD)

lemma sets_K[measurable_cong]: "x ∈ space M ⟹ sets (K x) = sets M"
using K unfolding prob_algebra_def unfolding measurable_restrict_space2_iff
by (auto dest: subprob_measurableD)

lemma prob_space_K: "x ∈ space M ⟹ prob_space (K x)"
using measurable_space[OF K] by (simp add: space_prob_algebra)

definition K' :: "'a ⇒ nat ⇒ (nat ⇒ 'a) ⇒ 'a measure"
where
"K' x n' ω' = K (case_nat x ω' n')"

lemma IT_K':
assumes x: "x ∈ space M" shows "Ionescu_Tulcea (K' x) (λ_. M)"
unfolding Ionescu_Tulcea_def K'_def[abs_def]
proof safe
fix i show "(λω'. K (case i of 0 ⇒ x | Suc x ⇒ ω' x)) ∈ Pi⇩M {0..<i} (λ_. M) →⇩M subprob_algebra M"
using x by (intro measurable_prob_algebraD measurable_compose[OF _ K]) measurable
next
fix i :: nat and ω assume ω: "ω ∈ space (Pi⇩M {0..<i} (λ_. M))"
with x have "(case i of 0 ⇒ x | Suc x ⇒ ω x) ∈ space M"
by (auto simp: space_PiM split: nat.split)
then show "prob_space (K (case i of 0 ⇒ x | Suc x ⇒ ω x))"
using K unfolding measurable_restrict_space2_iff prob_algebra_def by auto
qed

definition lim_sequence :: "'a ⇒ (nat ⇒ 'a) measure"
where
"lim_sequence x = projective_family.lim UNIV (Ionescu_Tulcea.CI (K' x) (λ_. M)) (λ_. M)"

lemma
assumes x: "x ∈ space M"
shows space_lim_sequence: "space (lim_sequence x) = space (Π⇩M i∈UNIV. M)"
and sets_lim_sequence[measurable_cong]: "sets (lim_sequence x) = sets (Π⇩M i∈UNIV. M)"
and emeasure_lim_sequence_emb: "⋀J X. finite J ⟹ X ∈ sets (Π⇩M j∈J. M) ⟹
emeasure (lim_sequence x) (prod_emb UNIV (λ_. M) J X) =
emeasure (Ionescu_Tulcea.CI (K' x) (λ_. M) J) X"
and emeasure_lim_sequence_emb_I0o: "⋀n X. X ∈ sets (Π⇩M i ∈ {0..<n}. M) ⟹
emeasure (lim_sequence x) (prod_emb UNIV (λ_. M) {0..<n} X) =
emeasure (Ionescu_Tulcea.C (K' x) (λ_. M) 0 n (λx. undefined)) X"
proof -
interpret Ionescu_Tulcea "K' x" "λ_. M"
using x by (rule IT_K')
show "space (lim_sequence x) = space (Π⇩M i∈UNIV. M)"
unfolding lim_sequence_def by simp
show "sets (lim_sequence x) = sets (Π⇩M i∈UNIV. M)"
unfolding lim_sequence_def by simp

{ fix J :: "nat set" and X assume "finite J" "X ∈ sets (Π⇩M j∈J. M)"
then show "emeasure (lim_sequence x) (PF.emb UNIV J X) = emeasure (CI J) X"
unfolding lim_sequence_def by (rule lim) }
note emb = this

have up_to_I0o[simp]: "up_to {0..<n} = n" for n
unfolding up_to_def by (rule Least_equality) auto

{ fix n :: nat and X assume "X ∈ sets (Π⇩M j∈{0..<n}. M)"
then show "emeasure (lim_sequence x) (PF.emb UNIV {0..<n} X) = emeasure (C 0 n (λx. undefined)) X"
by (simp add: space_C emb CI_def space_PiM distr_id2 sets_C cong: distr_cong_simp) }
qed

lemma lim_sequence[measurable]: "lim_sequence ∈ M →⇩M prob_algebra (Π⇩M i∈UNIV. M)"
proof (intro measurable_prob_algebra_generated[OF sets_PiM Int_stable_prod_algebra prod_algebra_sets_into_space])
fix a assume [simp]: "a ∈ space M"
interpret Ionescu_Tulcea "K' a" "λ_. M"
by (rule IT_K') simp
have sp: "space (lim_sequence a) = prod_emb UNIV (λ_. M) {} (Π⇩E j∈{}. space M)" "space (CI {}) = {} →⇩E space M"
by (auto simp: space_lim_sequence space_PiM prod_emb_def PF.space_P)
show "prob_space (lim_sequence a)"
apply standard
using PF.prob_space_P[THEN prob_space.emeasure_space_1, of "{}"]
apply (simp add: sp emeasure_lim_sequence_emb del: PiE_empty_domain)
done
show "sets (lim_sequence a) = sets (Pi⇩M UNIV (λi. M))"
next
fix X :: "(nat ⇒ 'a) set" assume "X ∈ prod_algebra UNIV (λi. M)"
then obtain J :: "nat set" and F where J: "J ≠ {}" "finite J" "F ∈ J → sets M"
and X: "X = prod_emb UNIV (λ_. M) J (Pi⇩E J F)"
unfolding prod_algebra_def by auto
then have Pi_F: "finite J" "Pi⇩E J F ∈ sets (Pi⇩M J (λ_. M))"
by (auto intro: sets_PiM_I_finite)

define n where "n = (LEAST n. ∀i≥n. i ∉ J)"
have J_le_n: "J ⊆ {0..<n}"
unfolding n_def
using ‹finite J›
apply -
apply (rule LeastI2[of _ "Suc (Max J)"])
apply (auto simp: Suc_le_eq not_le[symmetric])
done

have C: "(λx. Ionescu_Tulcea.C (K' x) (λ_. M) 0 n (λx. undefined)) ∈ M →⇩M subprob_algebra (Pi⇩M {0..<n} (λ_. M))"
apply (induction n)
apply (subst measurable_cong)
apply (rule Ionescu_Tulcea.C.simps[OF IT_K'])
apply assumption
apply (rule measurable_compose[OF _ return_measurable])
apply simp
apply (subst measurable_cong)
apply (rule Ionescu_Tulcea.C.simps[OF IT_K'])
apply assumption
apply (rule measurable_bind')
apply assumption
apply (subst measurable_cong)
proof -
fix n :: nat and w assume "w ∈ space (M ⨂⇩M Pi⇩M {0..<n} (λ_. M))"
then show "(case w of (x, xa) ⇒ Ionescu_Tulcea.eP (K' x) (λ_. M) (0 + n) xa) =
(case w of (x, xa) ⇒ distr (K' x n xa) (Π⇩M i∈{0..<Suc n}. M) (fun_upd xa n))"
by (auto simp: space_pair_measure Ionescu_Tulcea.eP_def[OF IT_K'] split: prod.split)
next
fix n show "(λw. case w of (x, xa) ⇒ distr (K' x n xa) (Pi⇩M {0..<Suc n} (λi. M)) (fun_upd xa n))
∈ M ⨂⇩M Pi⇩M {0..<n} (λ_. M) →⇩M subprob_algebra (Pi⇩M {0..<Suc n} (λ_. M))"
unfolding K'_def
apply measurable
apply (rule measurable_distr2[where M=M])
apply (rule measurable_PiM_single')
subgoal for i by (cases "i = n") auto
subgoal by (auto simp: split_beta' PiE_iff extensional_def Pi_iff space_pair_measure space_PiM)
apply (rule measurable_compose[OF _ K])
apply measurable
done
qed

have "(λa. emeasure (lim_sequence a) X) ∈ borel_measurable M ⟷
(λa. emeasure (Ionescu_Tulcea.CI (K' a) (λ_. M) J) (Pi⇩E J F)) ∈ borel_measurable M"
unfolding X using J Pi_F by (intro measurable_cong emeasure_lim_sequence_emb) auto
also have "…"
apply (intro measurable_compose[OF _ measurable_emeasure_subprob_algebra[OF Pi_F(2)]])
apply (subst measurable_cong)
apply (subst Ionescu_Tulcea.CI_def[OF IT_K'])
apply assumption
apply (subst Ionescu_Tulcea.up_to_def[OF IT_K'])
apply assumption
unfolding n_def[symmetric]
apply (rule refl)
apply (rule measurable_compose[OF _ measurable_distr[OF measurable_restrict_subset[OF J_le_n]]])
apply (rule C)
done
finally show "(λa. emeasure (lim_sequence a) X) ∈ borel_measurable M" .
qed

lemma step_C:
assumes x: "x ∈ space M"
shows "Ionescu_Tulcea.C (K' x) (λ_. M) 0 1 (λ_. undefined) ⤜ Ionescu_Tulcea.C (K' x) (λ_. M) 1 n =
K x ⤜ (λy. Ionescu_Tulcea.C (K' x) (λ_. M) 1 n (case_nat y (λ_. undefined)))"
proof -
interpret Ionescu_Tulcea "K' x" "λ_. M"
using x by (rule IT_K')

have [simp]: "space (K x) ≠ {}"
using space_K[OF x] x by auto

have [simp]: "((λ_. undefined::'a)(0 := x)) = case_nat x (λ_. undefined)" for x
by (auto simp: fun_eq_iff split: nat.split)

have "C 0 1 (λ_. undefined) ⤜ C 1 n = eP 0 (λ_. undefined) ⤜ C 1 n"
using measurable_eP[of 0] measurable_C[of 1 n, measurable del]
by (simp add: bind_return[where N="Pi⇩M {0} (λ_. M)"])
also have "… = K x ⤜ (λy. C 1 n (case_nat y (λ_. undefined)))"
using measurable_C[of 1 n, measurable del] x[THEN sets_K]
by (simp add: eP_def K'_def bind_distr cong: measurable_cong_sets)
finally show "C 0 1 (λ_. undefined) ⤜ C 1 n = K x ⤜ (λy. C 1 n (case_nat y (λ_. undefined)))" .
qed

lemma lim_sequence_eq:
assumes x: "x ∈ space M"
shows "lim_sequence x = bind (K x) (λy. distr (lim_sequence y) (Π⇩M j∈UNIV. M) (case_nat y))"
(is "_ = ?B x")
proof (rule measure_eqI_PiM_infinite)
show "sets (lim_sequence x) = sets (Π⇩M j∈UNIV. M)"
using x by (rule sets_lim_sequence)
have [simp]: "space (K x) ≠ {}"
using space_K[OF x] x by auto
show "sets (?B x) = sets (Pi⇩M UNIV (λj. M))"
using x by (subst sets_bind) auto
interpret lim_sequence: prob_space "lim_sequence x"
using lim_sequence x by (auto simp: measurable_restrict_space2_iff prob_algebra_def)
show "finite_measure (lim_sequence x)"
by (rule lim_sequence.finite_measure)

interpret Ionescu_Tulcea "K' x" "λ_. M"
using x by (rule IT_K')

let ?U = "λ_::nat. undefined :: 'a"

fix J :: "nat set" and F'
assume J: "finite J" "⋀i. i ∈ J ⟹ F' i ∈ sets M"

define n where "n = (if J = {} then 0 else Max J)"
define F where "F i = (if i ∈ J then F' i else space M)" for i
then have F[simp, measurable]: "F i ∈ sets M" for i
using J by auto
have emb_eq: "PF.emb UNIV J (Pi⇩E J F') = PF.emb UNIV {0..<Suc n} (Pi⇩E {0..<Suc n} F)"
proof cases
assume "J = {}" then show ?thesis
by (auto simp add: n_def F_def[abs_def] prod_emb_def PiE_def)
next
assume "J ≠ {}" then show ?thesis
by (auto simp: prod_emb_def PiE_iff F_def n_def less_Suc_eq_le ‹finite J› split: if_split_asm)
qed

have "emeasure (lim_sequence x) (PF.emb UNIV J (Pi⇩E J F')) = emeasure (C 0 (Suc n) ?U) (Pi⇩E {0..<Suc n} F)"
using x unfolding emb_eq by (rule emeasure_lim_sequence_emb_I0o) (auto intro!: sets_PiM_I_finite)
also have "C 0 (Suc n) ?U = K x ⤜ (λy. C 1 n (case_nat y ?U))"
using split_C[of ?U 0 "Suc 0" n] step_C[OF x] by simp
also have "emeasure (K x ⤜ (λy. C 1 n (case_nat y ?U))) (Pi⇩E {0..<Suc n} F) =
(∫⇧+y. C 1 n (case_nat y ?U) (Pi⇩E {0..<Suc n} F) ∂K x)"
using measurable_C[of 1 n, measurable del] x[THEN sets_K] F x
by (intro emeasure_bind[OF  _ measurable_compose[OF _ measurable_C]])
(auto cong: measurable_cong_sets intro!: measurable_PiM_single' split: nat.split_asm)
also have "… = (∫⇧+y. distr (lim_sequence y) (Pi⇩M UNIV (λj. M)) (case_nat y) (PF.emb UNIV J (Pi⇩E J F')) ∂K x)"
proof (intro nn_integral_cong)
fix y assume "y ∈ space (K x)"
then have y: "y ∈ space M"
using x by (simp add: space_K)
then interpret y: Ionescu_Tulcea "K' y" "λ_. M"
by (rule IT_K')

let ?y = "case_nat y"
have [simp]: "?y ?U ∈ space (Pi⇩M {0} (λi. M))"
using y by (auto simp: space_PiM PiE_iff extensional_def split: nat.split)
have yM[measurable]: "?y ∈ Pi⇩M {0..<m} (λ_. M) →⇩M Pi⇩M {0..<Suc m} (λi. M)" for m
using y by (intro measurable_PiM_single') (auto simp: space_PiM PiE_iff extensional_def split: nat.split)

have y': "?y ?U ∈ space (Pi⇩M {0..<1} (λi. M))"
by (simp add: space_PiM PiE_def y extensional_def split: nat.split)

have eq1: "?y -` Pi⇩E {0..<Suc n} F ∩ space (Pi⇩M {0..<n} (λ_. M)) =
(if y ∈ F 0 then Pi⇩E {0..<n} (F∘Suc) else {})"
unfolding set_eq_iff using y sets.sets_into_space[OF F]
by (auto simp: space_PiM PiE_iff extensional_def Ball_def split: nat.split nat.split_asm)

have eq2: "?y -` PF.emb UNIV {0..<Suc n} (Pi⇩E {0..<Suc n} F) ∩ space (Pi⇩M UNIV (λ_. M)) =
(if y ∈ F 0 then PF.emb UNIV {0..<n} (Pi⇩E {0..<n} (F∘Suc)) else {})"
unfolding set_eq_iff using y sets.sets_into_space[OF F]
by (auto simp: space_PiM PiE_iff prod_emb_def extensional_def Ball_def split: nat.split nat.split_asm)

let ?I = "indicator (F 0) y"

have "C 1 n (?y ?U) = distr (y.C 0 n ?U) (Π⇩M i∈{0..<Suc n}. M) ?y"
proof (induction n)
case (Suc m)

have "C 1 (Suc m) (?y ?U) = distr (y.C 0 m ?U) (Pi⇩M {0..<Suc m} (λi. M)) ?y ⤜ eP (Suc m)"
using Suc by simp
also have "… = y.C 0 m ?U ⤜ (λx. eP (Suc m) (?y x))"
by (intro bind_distr[where K="Pi⇩M {0..<Suc (Suc m)} (λ_. M)"]) (simp_all add: y y.space_C y.sets_C cong: measurable_cong_sets)
also have "… = y.C 0 m ?U ⤜ (λx. distr (y.eP m x) (Pi⇩M {0..<Suc (Suc m)} (λi. M)) ?y)"
proof (intro bind_cong refl)
fix ω' assume ω': "ω' ∈ space (y.C 0 m ?U)"
moreover have "K' x (Suc m) (?y ω') = K' y m ω'"
by (auto simp: K'_def)
ultimately show "eP (Suc m) (?y ω') = distr (y.eP m ω') (Pi⇩M {0..<Suc (Suc m)} (λi. M)) ?y"
unfolding eP_def y.eP_def
by (subst distr_distr)
(auto simp: y.space_C y.sets_P split: nat.split cong: measurable_cong_sets
intro!: distr_cong measurable_fun_upd[where J="{0..<m}"])
qed
also have "… = distr (y.C 0 m ?U ⤜ y.eP m) (Pi⇩M {0..<Suc (Suc m)} (λi. M)) ?y"
by (intro distr_bind[symmetric, OF _ _ yM]) (auto simp: y.space_C y.sets_C cong: measurable_cong_sets)
finally show ?case
by simp
qed (use y in ‹simp add: PiM_empty distr_return›)
then have "C 1 n (case_nat y ?U) (Pi⇩E {0..<Suc n} F) =
(distr (y.C 0 n ?U) (Π⇩M i∈{0..<Suc n}. M) ?y) (Pi⇩E {0..<Suc n} F)" by simp
also have "… = ?I * y.C 0 n ?U (Pi⇩E {0..<n} (F ∘ Suc))"
by (subst emeasure_distr) (auto simp: y.sets_C y.space_C eq1 cong: measurable_cong_sets)
also have "… = ?I * lim_sequence y (PF.emb UNIV {0..<n} (Pi⇩E {0..<n} (F ∘ Suc)))"
using y by (simp add: emeasure_lim_sequence_emb_I0o sets_PiM_I_finite)
also have "… = distr (lim_sequence y) (Pi⇩M UNIV (λj. M)) ?y (PF.emb UNIV {0..<Suc n} (Pi⇩E {0..<Suc n} F))"
using y by (subst emeasure_distr) (simp_all add: eq2 space_lim_sequence)
finally show "emeasure (C 1 n (case_nat y (λ_. undefined))) (Pi⇩E {0..<Suc n} F) =
emeasure (distr (lim_sequence y) (Pi⇩M UNIV (λj. M)) (case_nat y)) (PF.emb UNIV J (Pi⇩E J F'))"
unfolding emb_eq .
qed
also have "… =
emeasure (K x ⤜ (λy. distr (lim_sequence y) (Pi⇩M UNIV (λj. M)) (case_nat y))) (PF.emb UNIV J (Pi⇩E J F'))"
using J
by (subst emeasure_bind[where N="PiM UNIV (λ_. M)"])
(auto simp: sets_K x intro!: measurable_distr2[OF _ measurable_prob_algebraD[OF lim_sequence]] cong: measurable_cong_sets)
finally show "emeasure (lim_sequence x) (PF.emb UNIV J (Pi⇩E J F')) =
emeasure (K x ⤜ (λy. distr (lim_sequence y) (Pi⇩M UNIV (λj. M)) (case_nat y)))
(PF.emb UNIV J (Pi⇩E J F'))" .
qed

lemma AE_lim_sequence:
assumes x[simp]: "x ∈ space M" and P[measurable]: "Measurable.pred (Π⇩M i∈UNIV. M) P"
shows "(AE ω in lim_sequence x. P ω) ⟷ (AE y in K x. AE ω in lim_sequence y. P (case_nat y ω))"
apply (simp add: lim_sequence_eq cong del: AE_cong)
apply (subst AE_bind)
apply measurable
apply (auto intro!: AE_cong simp add: space_K AE_distr_iff)
done

definition lim_stream :: "'a ⇒ 'a stream measure"
where
"lim_stream x = distr (lim_sequence x) (stream_space M) to_stream"

lemma space_lim_stream: "space (lim_stream x) = streams (space M)"
unfolding lim_stream_def by (simp add: space_stream_space)

lemma sets_lim_stream[measurable_cong]: "sets (lim_stream x) = sets (stream_space M)"
unfolding lim_stream_def by simp

lemma lim_stream[measurable]: "lim_stream ∈ M →⇩M prob_algebra (stream_space M)"
unfolding lim_stream_def[abs_def] by (intro measurable_distr_prob_space2[OF lim_sequence]) auto

lemma space_stream_space_M_ne: "x ∈ space M ⟹ space (stream_space M) ≠ {}"
using sconst_streams[of x "space M"] by (auto simp: space_stream_space)

lemma prob_space_lim_stream: "x ∈ space M ⟹ prob_space (lim_stream x)"
using measurable_space[OF lim_stream, of x] by (simp add: space_prob_algebra)

lemma lim_stream_eq:
assumes x: "x ∈ space M"
shows "lim_stream x = do { y ← K x; ω ← lim_stream y; return (stream_space M) (y ## ω) }"
unfolding lim_stream_def
apply (subst lim_sequence_eq[OF x])
apply (subst distr_bind[OF _ _ measurable_to_stream])
subgoal
by (auto simp: sets_K x cong: measurable_cong_sets
intro!: measurable_prob_algebraD measurable_distr_prob_space2[where M="Pi⇩M UNIV (λj. M)"] lim_sequence) []
subgoal
using x by (auto simp add: space_K)
apply (intro bind_cong refl)
apply (subst distr_distr)
apply (auto simp: space_K sets_lim_sequence x cong: measurable_cong_sets intro!: distr_cong)
apply (subst bind_return_distr')
apply (auto simp: space_stream_space_M_ne)
apply (subst distr_distr)
apply (auto simp: space_K sets_lim_sequence x to_stream_nat_case cong: measurable_cong_sets intro!: distr_cong)
done

lemma AE_lim_stream:
assumes x[simp]: "x ∈ space M" and P[measurable]: "Measurable.pred (stream_space M) P"
shows "(AE ω in lim_stream x. P ω) ⟷ (AE y in K x. AE ω in lim_stream y. P (y ## ω))"
unfolding lim_stream_eq[OF x]
by (simp_all add: space_K space_lim_stream space_stream_space AE_return AE_bind[OF measurable_prob_algebraD P] cong: AE_cong_simp)

lemma emeasure_lim_stream:
assumes x[measurable, simp]: "x ∈ space M" and A[measurable, simp]: "A ∈ sets (stream_space M)"
shows "lim_stream x A = (∫⇧+y. emeasure (lim_stream y) (((##) y) -` A ∩ space (stream_space M)) ∂K x)"
apply (subst lim_stream_eq, simp)
apply (subst emeasure_bind[OF _ _ A], simp add: prob_space.not_empty prob_space_K)
apply measurable
apply (intro nn_integral_cong)
apply (subst bind_return_distr')
apply (auto intro!: prob_space.not_empty prob_space_lim_stream simp: space_K emeasure_distr)
done

lemma lim_stream_eq_coinduct[case_names in_space step]:
fixes R :: "'a ⇒ 'a stream measure ⇒ bool"
assumes x: "R x B" "x ∈ space M"
assumes R: "⋀x B. R x B ⟹ ∃B'∈M →⇩M prob_algebra (stream_space M).
(AE y in K x. R y (B' y) ∨ lim_stream y = B' y) ∧
B = do { y ← K x; ω ← B' y; return (stream_space M) (y ## ω) }"
shows "lim_stream x = B"
using x
proof (coinduction arbitrary: x B rule: stream_space_coinduct[where M=M, case_names step])
case (step x B)
from R[OF ‹R x B›] obtain B' where B': "B' ∈ M →⇩M prob_algebra (stream_space M)"
and ae: "AE y in K x. R y (B' y) ∨ lim_stream y = B' y"
and eq: "B = K x ⤜ (λy. B' y ⤜ (λω. return (stream_space M) (y ## ω)))"
by blast
show ?case
apply (rule bexI[of _ "K x"], rule bexI[OF _ lim_stream], rule bexI[OF _ B'])
apply (intro conjI)
subgoal
using ae AE_space by eventually_elim (insert ‹x∈space M›, auto simp: space_K)
subgoal
by (rule lim_stream_eq) fact
subgoal
by (rule eq)
subgoal
using K ‹x ∈ space M› by (rule measurable_space)
done
qed

lemma prob_space_lim_sequence: "x ∈ space M ⟹ prob_space (lim_sequence x)"
using measurable_space[OF lim_sequence, of x] by (simp add: space_prob_algebra)

end

subsection ‹Strong Markov Property for Discrete-Time Markov Processes›

text ‹The filtration adopted to streams, i.e. to the \$n\$-th projection.›

definition stream_filtration :: "'a measure ⇒ enat ⇒ 'a stream measure"
where "stream_filtration M n = (SUP i∈{i::nat. i ≤ n}. vimage_algebra (streams (space M)) (λω . ω !! i) M)"

lemma measurable_stream_filtration1: "enat i ≤ n ⟹ (λω. ω !! i) ∈ stream_filtration M n →⇩M M"
by (auto intro!: measurable_SUP1 measurable_vimage_algebra1 snth_in simp: stream_filtration_def)

lemma measurable_stream_filtration2:
"f ∈ space N → streams (space M) ⟹ (⋀i. enat i ≤ n ⟹ (λx. f x !! i) ∈ N →⇩M M) ⟹ f ∈ N →⇩M stream_filtration M n"
by (auto simp: stream_filtration_def enat_0
intro!: measurable_SUP2 measurable_vimage_algebra2 elim!: allE[of _ "0::nat"])

lemma space_stream_filtration: "space (stream_filtration M n) = space (stream_space M)"
by (auto simp add: space_stream_space space_Sup_eq_UN stream_filtration_def enat_0 elim!: allE[of _ 0])

lemma sets_stream_filteration_le_stream_space: "sets (stream_filtration M n) ⊆ sets (stream_space M)"
unfolding sets_stream_space_eq stream_filtration_def
by (intro SUP_subset_mono le_measureD2) (auto simp: space_Sup_eq_UN enat_0 elim!: allE[of _ 0])

interpretation stream_filtration: filtration "space (stream_space M)" "stream_filtration M"
proof
show "space (stream_filtration M i) = space (stream_space M)" for i
show "sets (stream_filtration M i) ⊆ sets (stream_filtration M j)" if "i ≤ j" for i j
proof (rule le_measureD2)
show "stream_filtration M i ≤ stream_filtration M j"
using ‹i ≤ j› unfolding stream_filtration_def by (intro SUP_subset_mono) auto
qed

lemma measurable_stopping_time_stream:
"stopping_time (stream_filtration M) T ⟹ T ∈ stream_space M →⇩M count_space UNIV"
using sets_stream_filteration_le_stream_space
by (subst measurable_cong_sets[OF refl sets_borel_eq_count_space[symmetric, where 'a=enat]])
(auto intro!: measurable_stopping_time simp: space_stream_filtration)

lemma measurable_stopping_time_All_eq_0:
assumes T: "stopping_time (stream_filtration M) T"
shows "{x∈space M. ∀ω∈streams (space M). T (x ## ω) = 0} ∈ sets M"
proof -
have "{ω∈streams (space M). T ω = 0} ∈ vimage_algebra (streams (space M)) (λω. ω !! 0) M"
using stopping_timeD[OF T, of 0] by (simp add: stream_filtration_def pred_def enat_0_iff)
then obtain A
where A: "A ∈ sets M"
and *: "{ω ∈ streams (space M). T ω = 0} = (λω. ω !! 0) -` A ∩ streams (space M)"
by (auto simp: sets_vimage_algebra2 streams_shd)
have "A = {x∈space M. ∀ω∈streams (space M). T (x ## ω) = 0}"
proof safe
fix x ω assume "x ∈ A" "ω ∈ streams (space M)"
then have "x ## ω ∈ {ω ∈ streams (space M). T ω = 0}"
unfolding * using A[THEN sets.sets_into_space] by auto
then show "T (x ## ω) = 0" by auto
next
fix x assume "x ∈ space M" "∀ω∈streams (space M). T (x ## ω) = 0 "
then have "∀ω∈streams (space M). x ## ω ∈ {ω ∈ streams (space M). T ω = 0}"
by simp
with ‹x∈space M› show "x ∈ A"
unfolding * by (auto simp: streams_empty_iff)
qed (use A[THEN sets.sets_into_space] in auto)
with ‹A ∈ sets M› show ?thesis by auto
qed

lemma stopping_time_0:
assumes T: "stopping_time (stream_filtration M) T"
and x: "x ∈ space M" and ω: "ω ∈ streams (space M)" "T (x ## ω) > 0"
and ω': "ω' ∈ streams (space M)"
shows "T (x ## ω') > 0"
unfolding zero_less_iff_neq_zero
proof
assume "T (x ## ω') = 0"
with x ω' have x': "x ## ω' ∈ {ω ∈ streams (space M). T ω = 0}"
by auto

have "{ω∈streams (space M). T ω = 0} ∈ vimage_algebra (streams (space M)) (λω. ω !! 0) M"
using stopping_timeD[OF T, of 0] by (simp add: stream_filtration_def pred_def enat_0_iff)
then obtain A
where A: "A ∈ sets M"
and *: "{ω ∈ streams (space M). T ω = 0} = (λω. ω !! 0) -` A ∩ streams (space M)"
by (auto simp: sets_vimage_algebra2 streams_shd)
with x' have "x ∈ A"
by auto
with ω x have "x ## ω ∈ (λω. ω !! 0) -` A ∩ streams (space M)"
by auto
with ω show False
unfolding *[symmetric] by auto
qed

lemma stopping_time_epred_SCons:
assumes T: "stopping_time (stream_filtration M) T"
and x: "x ∈ space M" and ω: "ω ∈ streams (space M)" "T (x ## ω) > 0"
shows "stopping_time (stream_filtration M) (λω. epred (T (x ## ω)))"
proof (rule stopping_timeI, rule measurable_cong[THEN iffD2])
show "ω ∈ space (stream_filtration M t) ⟹ (epred (T (x ## ω)) ≤ t) = (T (x ## ω) ≤ eSuc t)" for t ω
by (cases "T (x ## ω)" rule: enat_coexhaust)
(auto simp add: space_stream_filtration space_stream_space dest!: stopping_time_0[OF T x ω])
show "Measurable.pred (stream_filtration M t) (λw. T (x ## w) ≤ eSuc t)" for t
proof (rule measurable_compose[of "SCons x"])
show "(##) x ∈ stream_filtration M t →⇩M stream_filtration M (eSuc t)"
proof (intro measurable_stream_filtration2)
show "enat i ≤ eSuc t ⟹ (λxa. (x ## xa) !! i) ∈ stream_filtration M t →⇩M M" for i
using ‹x∈space M›
by (cases i) (auto simp: eSuc_enat[symmetric] intro!: measurable_stream_filtration1)
qed (auto simp: space_stream_filtration space_stream_space ‹x∈space M›)
qed (rule T[THEN stopping_timeD])
qed

context discrete_Markov_process
begin

lemma lim_stream_strong_Markov:
assumes x: "x ∈ space M" and T: "stopping_time (stream_filtration M) T"
shows "lim_stream x =
lim_stream x ⤜ (λω. case T ω of
enat i ⇒ distr (lim_stream (ω !! i)) (stream_space M) (λω'. stake (Suc i) ω @- ω')
| ∞     ⇒ return (stream_space M) ω)"
(is "_ = ?L T x")
using assms
proof (coinduction arbitrary: x T rule: lim_stream_eq_coinduct)
case (step x T)
note T = ‹stopping_time (stream_filtration M) T›[THEN measurable_stopping_time_stream, measurable]
define L where "L T x = ?L T x" for T x
have L[measurable (raw)]:
"(λ(x, ω). T x ω) ∈ N ⨂⇩M stream_space M →⇩M count_space UNIV ⟹
f ∈ N →⇩M M ⟹ (λx. L (T x) (f x)) ∈ N →⇩M prob_algebra (stream_space M)" for f :: "'a ⇒ 'a" and N T
unfolding L_def
by (intro measurable_bind_prob_space2[OF measurable_compose[OF _ lim_stream]] measurable_case_enat
measurable_distr_prob_space2[OF measurable_compose[OF _ lim_stream]]
measurable_return_prob_space measurable_stopping_time_stream)
auto

define S where "S x = (if ∀ω∈streams (space M). T (x##ω) = 0 then lim_stream x else L (λω. epred (T (x ## ω))) x)" for x
then have S_eq: "∀ω∈streams (space M). T (x##ω) = 0 ⟹ S x = lim_stream x"
"¬ (∀ω∈streams (space M). T (x##ω) = 0) ⟹ S x = L (λω. epred (T (x ## ω))) x" for x
by auto
have [measurable]: "S ∈ M →⇩M prob_algebra (stream_space M)"
unfolding S_def[abs_def]
by (subst measurable_If_restrict_space_iff, safe intro!: L)
(auto intro!: measurable_stopping_time_All_eq_0 step measurable_restrict_space1 lim_stream
measurable_compose[OF _ measurable_epred] measurable_compose[OF _ T]
measurable_Stream measurable_compose[OF measurable_fst]
simp: measurable_split_conv)

show ?case
unfolding L_def[symmetric]
proof (intro bexI[of _ S] conjI AE_I2)
fix y assume "y ∈ space (K x)"
then show "(∃x T. y = x ∧ S y = L T x ∧ x ∈ space M ∧ stopping_time (stream_filtration M) T) ∨
lim_stream y = S y"
using ‹x∈space M›
by (cases "∀ω∈streams (space M). T (y##ω) = 0")
(auto simp add: S_eq space_K intro!: exI[of _ "λω. epred (T (y ## ω))"] stopping_time_epred_SCons step)
next
note ‹x∈space M›[simp]
have "L T x = K x ⤜
(λy. lim_stream y ⤜ (λω. case T (y##ω) of
enat i ⇒ distr (lim_stream ((y##ω) !! i)) (stream_space M) (λω'. stake (Suc i) (y##ω) @- ω')
| ∞     ⇒ return (stream_space M) (y##ω)))" (is "_ = K x ⤜ ?L'")
unfolding L_def
apply (subst lim_stream_eq[OF ‹x∈space M›])
measurable)
apply (rule bind_cong[OF refl])
measurable)
apply (rule bind_cong[OF refl])
apply (subst bind_return[where N="stream_space M", OF measurable_prob_algebraD])
apply (measurable; fail) []
apply rule
done
also have "… = K x ⤜ (λy. S y ⤜ (λω. return (stream_space M) (y ## ω)))"
proof (intro bind_cong[of "K x"] refl)
fix y assume "y ∈ space (K x)"
then have [simp]: "y ∈ space M"
show "?L' y = S y ⤜ (λω. return (stream_space M) (y ## ω))"
proof cases
assume "∀ω∈streams (space M). T (y##ω) = 0"
with x show ?thesis
by (auto simp: S_eq space_lim_stream shift.simps[abs_def] streams_empty_iff
bind_const'[OF _ prob_space_imp_subprob_space] prob_space_lim_stream prob_space.prob_space_distr
intro!: bind_return_distr'[symmetric]
cong: bind_cong_simp)
next
assume *: "¬ (∀ω∈streams (space M). T (y##ω) = 0)"
then have T_pos: "ω ∈ streams (space M) ⟹ T (y ## ω) ≠ 0" for ω
using stopping_time_0[OF ‹stopping_time (stream_filtration M) T›, of y _ ω] by auto
show ?thesis
apply (simp add: S_eq(2)[OF *] L_def)
measurable)
apply (intro bind_cong refl)
apply (auto simp: T_pos enat_0 space_lim_stream shift.simps[abs_def] diff_Suc space_stream_space
intro!: bind_return[where N="stream_space M", OF measurable_prob_algebraD, symmetric]
bind_distr_return[symmetric]
split: nat.split enat.split)
done
qed
qed
finally show "L T x = K x ⤜ (λy. S y ⤜ (λω. return (stream_space M) (y ## ω)))" .
qed fact
qed fact

end

end
```