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} (PiE {..n} A)) = Q (prod_emb UNIV M {..n} (PiE {..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 (PiE J F') = prod_emb UNIV M {..n} (PiE {..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 (PiE J F')) = emeasure Q (prod_emb UNIV M J (PiE 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)) ∈ PiM {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 (PiM {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 (PiM UNIV (λi. M))"
    by (simp add: sets_lim_sequence)
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 (PiE J F)"
    unfolding prod_algebra_def by auto
  then have Pi_F: "finite J" "PiE J F ∈ sets (PiM 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 (PiM {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 PiM {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) (PiM {0..<Suc n} (λi. M)) (fun_upd xa n))
         ∈ M ⨂M PiM {0..<n} (λ_. M) →M subprob_algebra (PiM {0..<Suc n} (λ_. M))"
      unfolding K'_def
      apply measurable
      apply (rule measurable_distr2[where M=M])
      apply (rule measurable_PiM_single')
      apply (simp add: split_beta')
      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_prob_algebraD)
      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) (PiE 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="PiM {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 (PiM 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 (PiE J F') = PF.emb UNIV {0..<Suc n} (PiE {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 (PiE J F')) = emeasure (C 0 (Suc n) ?U) (PiE {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))) (PiE {0..<Suc n} F) =
    (∫+y. C 1 n (case_nat y ?U) (PiE {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) (PiM UNIV (λj. M)) (case_nat y) (PF.emb UNIV J (PiE 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 (PiM {0} (λi. M))"
      using y by (auto simp: space_PiM PiE_iff extensional_def split: nat.split)
    have yM[measurable]: "?y ∈ PiM {0..<m} (λ_. M) →M PiM {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 (PiM {0..<1} (λi. M))"
      by (simp add: space_PiM PiE_def y extensional_def split: nat.split)

    have eq1: "?y -` PiE {0..<Suc n} F ∩ space (PiM {0..<n} (λ_. M)) =
        (if y ∈ F 0 then PiE {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} (PiE {0..<Suc n} F) ∩ space (PiM UNIV (λ_. M)) =
        (if y ∈ F 0 then PF.emb UNIV {0..<n} (PiE {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) (PiM {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="PiM {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) (PiM {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 ω') (PiM {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) (PiM {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) (PiE {0..<Suc n} F) =
      (distr (y.C 0 n ?U) (ΠM i∈{0..<Suc n}. M) ?y) (PiE {0..<Suc n} F)" by simp
    also have "… = ?I * y.C 0 n ?U (PiE {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} (PiE {0..<n} (F ∘ Suc)))"
      using y by (simp add: emeasure_lim_sequence_emb_I0o sets_PiM_I_finite)
    also have "… = distr (lim_sequence y) (PiM UNIV (λj. M)) ?y (PF.emb UNIV {0..<Suc n} (PiE {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))) (PiE {0..<Suc n} F) =
        emeasure (distr (lim_sequence y) (PiM UNIV (λj. M)) (case_nat y)) (PF.emb UNIV J (PiE J F'))"
      unfolding emb_eq .
  qed
  also have "… =
    emeasure (K x ⤜ (λy. distr (lim_sequence y) (PiM UNIV (λj. M)) (case_nat y))) (PF.emb UNIV J (PiE 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 (PiE J F')) =
    emeasure (K x ⤜ (λy. distr (lim_sequence y) (PiM UNIV (λj. M)) (case_nat y)))
            (PF.emb UNIV J (PiE 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 (rule measurable_prob_algebraD)
  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="PiM 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 (rule measurable_prob_algebraD)
   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)
  apply (simp add: space_lim_stream space_stream_space)
  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
    by (simp add: space_stream_filtration)
  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 (simp add: space_stream_filtration)
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›])
      apply (subst bind_assoc[where N="stream_space M" and R="stream_space M", OF measurable_prob_algebraD measurable_prob_algebraD];
          measurable)
      apply (rule bind_cong[OF refl])
      apply (simp add: space_K)
      apply (subst bind_assoc[where N="stream_space M" and R="stream_space M", OF measurable_prob_algebraD measurable_prob_algebraD];
          measurable)
      apply (rule bind_cong[OF refl])
      apply (simp add: space_lim_stream)
      apply (subst bind_return[where N="stream_space M", OF measurable_prob_algebraD])
        apply (measurable; fail) []
       apply (simp add: space_stream_space)
      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"
        by (simp add: space_K)
      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)
          apply (subst bind_assoc[where N="stream_space M" and R="stream_space M", OF measurable_prob_algebraD measurable_prob_algebraD];
            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