Theory Trace_Space_Equals_Markov_Processes
subsection ‹Trace Space equal to Markov Chains›
theory Trace_Space_Equals_Markov_Processes
imports Discrete_Time_Markov_Chain
begin
text ‹
We can construct for each time-homogeneous discrete-time Markov chain a corresponding
probability space using @{theory Markov_Models.Discrete_Time_Markov_Chain}. The constructed probability space
has the same probabilities.
›
locale Time_Homogeneous_Discrete_Markov_Process = M?: prob_space +
fixes S :: "'s set" and X :: "nat ⇒ 'a ⇒ 's"
assumes X [measurable]: "⋀t. X t ∈ measurable M (count_space UNIV)"
assumes S: "countable S" "⋀n. AE x in M. X n x ∈ S"
assumes MC: "⋀n s s'.
𝒫(ω in M. ∀t≤n. X t ω = s t ) ≠ 0 ⟹
𝒫(ω in M. X (Suc n) ω = s' ¦ ∀t≤n. X t ω = s t ) =
𝒫(ω in M. X (Suc n) ω = s' ¦ X n ω = s n )"
assumes TH: "⋀n m s t.
𝒫(ω in M. X n ω = t) ≠ 0 ⟹ 𝒫(ω in M. X m ω = t) ≠ 0 ⟹
𝒫(ω in M. X (Suc n) ω = s ¦ X n ω = t) = 𝒫(ω in M. X (Suc m) ω = s ¦ X m ω = t)"
begin
context
begin
interpretation pmf_as_measure .
lift_definition I :: "'s pmf" is "distr M (count_space UNIV) (X 0)"
proof -
let ?X = "distr M (count_space UNIV) (X 0)"
interpret X: prob_space ?X
by (auto simp: prob_space_distr)
have "AE x in ?X. measure ?X {x} ≠ 0"
using S by (subst X.AE_support_countable) (auto simp: AE_distr_iff intro!: exI[of _ S])
then show "prob_space ?X ∧ sets ?X = UNIV ∧ (AE x in ?X. measure ?X {x} ≠ 0)"
by (simp add: prob_space_distr AE_support_countable)
qed
lemma I_in_S:
assumes "pmf I s ≠ 0" shows "s ∈ S"
proof -
from ‹pmf I s ≠ 0› have "0 ≠ 𝒫(x in M. X 0 x = s)"
by transfer (auto simp: measure_distr vimage_def Int_def conj_commute)
also have "𝒫(x in M. X 0 x = s) = 𝒫(x in M. X 0 x = s ∧ s ∈ S)"
using S(2)[of 0] by (intro M.finite_measure_eq_AE) auto
finally show ?thesis
by (cases "s ∈ S") auto
qed
lift_definition K :: "'s ⇒ 's pmf" is
"λs. with (λn. 𝒫(ω in M. X n ω = s) ≠ 0)
(λn. distr (uniform_measure M {ω∈space M. X n ω = s}) (count_space UNIV) (X (Suc n)))
(uniform_measure (count_space UNIV) {s})"
proof (rule withI)
fix s n assume *: "𝒫(ω in M. X n ω = s) ≠ 0"
let ?D = "distr (uniform_measure M {ω∈space M. X n ω = s}) (count_space UNIV) (X (Suc n))"
have D: "prob_space ?D"
by (intro prob_space.prob_space_distr prob_space_uniform_measure)
(auto simp: M.emeasure_eq_measure *)
then interpret D: prob_space ?D .
have sets_D: "sets ?D = UNIV"
by simp
moreover have "AE x in ?D. measure ?D {x} ≠ 0"
unfolding D.AE_support_countable[OF sets_D]
proof (intro exI[of _ S] conjI)
show "countable S" by (rule S)
show "AE x in ?D. x ∈ S"
using * S(2)[of "Suc n"] by (auto simp add: AE_distr_iff AE_uniform_measure M.emeasure_eq_measure)
qed
ultimately show "prob_space ?D ∧ sets ?D = UNIV ∧ (AE x in ?D. measure ?D {x} ≠ 0)"
using D by blast
qed (auto intro!: prob_space_uniform_measure AE_uniform_measureI)
lemma pmf_K:
assumes n: "0 < 𝒫(ω in M. X n ω = s)"
shows "pmf (K s) t = 𝒫(ω in M. X (Suc n) ω = t ¦ X n ω = s)"
proof (transfer fixing: n s t)
let ?P = "λn. 𝒫(ω in M. X n ω = s) ≠ 0"
let ?D = "λn. distr (uniform_measure M {ω∈space M. X n ω = s}) (count_space UNIV) (X (Suc n))"
let ?U = "uniform_measure (count_space UNIV) {s}"
show "measure (with ?P ?D ?U) {t} = 𝒫(ω in M. X (Suc n) ω = t ¦ X n ω = s)"
proof (rule withI)
fix n' assume "?P n'"
moreover have "X (Suc n') -` {t} ∩ space M = {x∈space M. X (Suc n') x = t}"
by auto
ultimately show "measure (?D n') {t} = 𝒫(ω in M. X (Suc n) ω = t ¦ X n ω = s)"
using n M.measure_uniform_measure_eq_cond_prob[of "λx. X (Suc n') x = t" "λx. X n' x = s"]
by (auto simp: measure_distr M.emeasure_eq_measure simp del: measure_uniform_measure intro!: TH)
qed (insert n, simp)
qed
lemma pmf_K2:
"(⋀n. 𝒫(ω in M. X n ω = s) = 0) ⟹ pmf (K s) t = indicator {t} s"
apply (transfer fixing: s t)
apply (rule withI)
apply (auto split: split_indicator)
done
end
sublocale K: MC_syntax K .
lemma bind_I_K_eq_M: "K.T' I = distr M K.S (λω. to_stream (λn. X n ω))" (is "_ = ?D")
proof (rule stream_space_eq_sstart)
note streams_sets[measurable]
note measurable_abs_UNIV[measurable (raw)]
note sstart_sets[measurable]
{ fix s assume "s ∈ S"
from K.AE_T_enabled[of s] have "AE ω in K.T s. ω ∈ streams S"
proof eventually_elim
fix ω assume "K.enabled s ω" from this ‹s∈S› show "ω ∈ streams S"
proof (coinduction arbitrary: s ω)
case streams
then have 1: "pmf (K s) (shd ω) ≠ 0"
by (simp add: K.enabled.simps[of s] set_pmf_iff)
have "shd ω ∈ S"
proof cases
assume "∃n. 0 < 𝒫(ω in M. X n ω = s)"
then obtain n where "0 < 𝒫(ω in M. X n ω = s)" by auto
with 1 have 2: "𝒫(ω' in M. X (Suc n) ω' = shd ω ∧ X n ω' = s) ≠ 0"
by (simp add: pmf_K cond_prob_def)
show "shd ω ∈ S"
proof (rule ccontr)
assume "shd ω ∉ S"
with S(2)[of "Suc n"] have "𝒫(ω' in M. X (Suc n) ω' = shd ω ∧ X n ω' = s) = 0"
by (intro M.prob_eq_0_AE) auto
with 2 show False by contradiction
qed
next
assume "¬ (∃n. 0 < 𝒫(ω in M. X n ω = s))"
then have "pmf (K s) (shd ω) = indicator {shd ω} s"
by (intro pmf_K2) (auto simp: not_less measure_le_0_iff)
with 1 ‹s∈S› show ?thesis
by (auto split: split_indicator_asm)
qed
with streams show ?case
by (cases ω) (auto simp: K.enabled.simps[of s])
qed
qed }
note AE_streams = this
show "prob_space (K.T' I)"
by (rule K.prob_space_T')
show "prob_space ?D"
by (rule M.prob_space_distr) simp
show "AE x in K.T' I. x ∈ streams S"
by (auto simp add: K.AE_T' set_pmf_iff I_in_S AE_distr_iff streams_Stream intro!: AE_streams)
show "AE x in ?D. x ∈ streams S"
by (simp add: AE_distr_iff to_stream_in_streams AE_all_countable S)
show "sets (K.T' I) = sets (stream_space (count_space UNIV))"
by (simp add: K.sets_T')
show "sets ?D = sets (stream_space (count_space UNIV))"
by simp
fix xs' assume "xs' ≠ []" "xs' ∈ lists S"
then obtain s xs where xs': "xs' = s # xs" and s: "s ∈ S" and xs: "xs ∈ lists S"
by (auto simp: neq_Nil_conv del: in_listsD)
have "emeasure (K.T' I) (sstart S xs') = (∫⇧+s. emeasure (K.T s) {ω∈space K.S. s ## ω ∈ sstart S xs'} ∂I)"
by (rule K.emeasure_T') measurable
also have "… = (∫⇧+s'. emeasure (K.T s) (sstart S xs) * indicator {s} s' ∂I)"
by (intro arg_cong2[where f=emeasure] nn_integral_cong)
(auto split: split_indicator simp: emeasure_distr vimage_def space_stream_space neq_Nil_conv xs')
also have "… = pmf I s * emeasure (K.T s) (sstart S xs)"
by (auto simp add: max_def emeasure_pmf_single intro: mult_ac)
also have "emeasure (K.T s) (sstart S xs) = ennreal (∏i<length xs. pmf (K ((s#xs)!i)) (xs!i))"
using xs s
proof (induction arbitrary: s)
case Nil then show ?case
by (simp add: K.T.emeasure_eq_1_AE AE_streams)
next
case (Cons t xs)
have "emeasure (K.T s) (sstart S (t # xs)) =
emeasure (K.T s) {x∈space (K.T s). shd x = t ∧ stl x ∈ sstart S xs}"
by (intro arg_cong2[where f=emeasure]) (auto simp: space_stream_space)
also have "… = (∫⇧+t'. emeasure (K.T t') {x∈space K.S. t' = t ∧ x ∈ sstart S xs} ∂K s)"
by (subst K.emeasure_Collect_T) auto
also have "… = (∫⇧+t'. emeasure (K.T t) (sstart S xs) * indicator {t} t' ∂K s)"
by (intro nn_integral_cong) (auto split: split_indicator simp: space_stream_space)
also have "… = emeasure (K.T t) (sstart S xs) * pmf (K s) t"
by (simp add: emeasure_pmf_single max_def)
finally show ?case
by (simp add: lessThan_Suc_eq_insert_0 zero_notin_Suc_image prod.reindex Cons
prod_nonneg ennreal_mult[symmetric])
qed
also have "pmf I s * ennreal (∏i<length xs. pmf (K ((s#xs)!i)) (xs!i)) =
𝒫(x in M. ∀i≤length xs. X i x = (s # xs) ! i)"
using xs s
proof (induction xs rule: rev_induct)
case Nil
have "pmf I s = prob {x ∈ space M. X 0 x = s}"
by transfer (simp add: vimage_def Int_def measure_distr conj_commute)
then show ?case
by simp
next
case (snoc t xs)
let ?l = "length xs" and ?lt = "length (xs @ [t])" and ?xs' = "s # xs @ [t]"
have "ennreal (pmf I s) * (∏i<?lt. pmf (K ((?xs') ! i)) ((xs @ [t]) ! i)) =
(ennreal (pmf I s) * (∏i<?l. pmf (K ((s # xs) ! i)) (xs ! i))) * pmf (K ((s # xs) ! ?l)) t"
by (simp add: lessThan_Suc mult_ac nth_append append_Cons[symmetric] prod_nonneg ennreal_mult[symmetric]
del: append_Cons)
also have "… = 𝒫(x in M. ∀i≤?l. X i x = (s # xs) ! i) * pmf (K ((s # xs) ! ?l)) t"
using snoc by (simp add: ennreal_mult[symmetric])
also have "… = 𝒫(x in M. ∀i≤?lt. X i x = (?xs') ! i)"
proof cases
assume "𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i) = 0"
moreover have "𝒫(x in M. ∀i≤?lt. X i x = (?xs') ! i) ≤ 𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i)"
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
moreover have "𝒫(x in M. ∀i≤?l. X i x = (s # xs) ! i) ≤ 𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i)"
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
ultimately show ?thesis
by (simp add: measure_le_0_iff)
next
assume "𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i) ≠ 0"
then have *: "0 < 𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i)"
unfolding less_le by simp
moreover have "𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i) ≤ 𝒫(ω in M. X ?l ω = (s # xs) ! ?l)"
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
ultimately have "𝒫(ω in M. X ?l ω = (s # xs) ! ?l) ≠ 0"
by auto
then have "pmf (K ((s # xs) ! ?l)) t = 𝒫(ω in M. X ?lt ω = ?xs' ! ?lt ¦ X ?l ω = (s # xs) ! ?l)"
by (subst pmf_K) (auto simp: less_le)
also have "… = 𝒫(ω in M. X ?lt ω = ?xs' ! ?lt ¦ ∀i≤?l. X i ω = (s # xs) ! i)"
using * MC[of ?l "λi. (s # xs) ! i" "?xs' ! ?lt"] by simp
also have "… = 𝒫(ω in M. ∀i≤?lt. X i ω = ?xs' ! i) / 𝒫(ω in M. ∀i≤?l. X i ω = (s # xs) ! i)"
unfolding cond_prob_def
by (intro arg_cong2[where f="(/)"] arg_cong2[where f=measure]) (auto simp: nth_Cons nth_append split: nat.splits)
finally show ?thesis
using * by simp
qed
finally show ?case .
qed
also have "… = emeasure ?D (sstart S xs')"
proof -
have "AE x in M. ∀i. X i x ∈ S"
using S(2) by (simp add: AE_all_countable)
then have "AE x in M. (∀i≤length xs. X i x = (s # xs) ! i) = (to_stream (λn. X n x) ∈ sstart S xs')"
proof eventually_elim
fix x assume "∀i. X i x ∈ S"
then have "to_stream (λn. X n x) ∈ streams S"
by (auto simp: streams_iff_snth to_stream_def)
then show "(∀i≤length xs. X i x = (s # xs) ! i) = (to_stream (λn. X n x) ∈ sstart S xs')"
by (simp add: sstart_eq xs' to_stream_def less_Suc_eq_le del: sstart.simps(1) in_sstart)
qed
then show ?thesis
by (auto simp: emeasure_distr M.emeasure_eq_measure intro!: M.finite_measure_eq_AE)
qed
finally show "emeasure (K.T' I) (sstart S xs') = emeasure ?D (sstart S xs')" .
qed (rule S)
end
lemma (in MC_syntax) is_THDTMC:
fixes I :: "'s pmf"
defines "U ≡ (SIGMA s:UNIV. K s)⇧* `` I"
shows "Time_Homogeneous_Discrete_Markov_Process (T' I) U (λn ω. ω !! n)"
proof -
have [measurable]: "U ∈ sets (count_space UNIV)"
by auto
interpret prob_space "T' I"
by (rule prob_space_T')
{ fix s t I
have "⋀t s. 𝒫(ω in T s. s = t) = indicator {t} s"
using T.prob_space by (auto split: split_indicator)
moreover then have "⋀t t' s. 𝒫(ω in T s. shd ω = t' ∧ s = t) = pmf (K t) t' * indicator {t} s"
by (subst prob_T) (auto split: split_indicator simp: pmf.rep_eq)
ultimately have "𝒫(ω in T' I. shd (stl ω) = t ∧ shd ω = s) = 𝒫(ω in T' I. shd ω = s) * pmf (K s) t"
by (simp add: prob_T' pmf.rep_eq) }
note start_eq = this
{ fix n s t assume "𝒫(ω in T' I. ω !! n = s) ≠ 0"
moreover have "𝒫(ω in T' I. ω !! (Suc n) = t ∧ ω !! n = s) = 𝒫(ω in T' I. ω !! n = s) * pmf (K s) t"
proof (induction n arbitrary: I)
case (Suc n) then show ?case
by (subst (1 2) prob_T') (simp_all del: space_T add: T_eq_T')
qed (simp add: start_eq)
ultimately have "𝒫(ω in T' I. stl ω !! n = t ¦ ω !! n = s) = pmf (K s) t"
by (simp add: cond_prob_def field_simps) }
note TH = this
{ fix n ω' t assume "𝒫(ω in T' I. ∀i≤n. ω !! i = ω' i) ≠ 0"
moreover have "𝒫(ω in T' I. ω !! (Suc n) = t ∧ (∀i≤n. ω !! i = ω' i)) =
𝒫(ω in T' I. ∀i≤n. ω !! i = ω' i) * pmf (K (ω' n)) t"
proof (induction n arbitrary: I ω')
case (Suc n)
have *[simp]: "⋀s P. measure (T' (K s)) {x. s = ω' 0 ∧ P x} =
measure (T' (K (ω' 0))) {x. P x} * indicator {ω' 0} s"
by (auto split: split_indicator)
from Suc[of _ "λi. ω' (Suc i)"] show ?case
by (subst (1 2) prob_T')
(simp_all add: T_eq_T' all_Suc_split[where P="λi. i ≤ Suc n ⟶ Q i" for n Q] conj_commute conj_left_commute sets_eq_imp_space_eq[OF sets_T'])
qed (simp add: start_eq)
ultimately have "𝒫(ω in T' I. stl ω !! n = t ¦ ∀i≤n. ω !! i = ω' i) = pmf (K (ω' n)) t"
by (simp add: cond_prob_def field_simps) }
note MC = this
{ fix n ω' assume "𝒫(ω in T' I. ∀t≤n. ω !! t = ω' t) ≠ 0"
moreover have "𝒫(ω in T' I. ∀t≤n. ω !! t = ω' t) ≤ 𝒫(ω in T' I. ω !! n = ω' n)"
by (auto intro!: finite_measure_mono_AE simp: sets_T' sets_eq_imp_space_eq[OF sets_T'])
ultimately have "𝒫(ω in T' I. ω !! n = ω' n) ≠ 0"
by (auto simp: neq_iff not_less measure_le_0_iff) }
note MC' = this
show ?thesis
proof
show "countable U"
unfolding U_def by (rule countable_reachable countable_Image countable_set_pmf)+
show "⋀t. (λω. ω !! t) ∈ measurable (T' I) (count_space UNIV)"
by (subst measurable_cong_sets[OF sets_T' refl]) simp
next
fix n
have "∀x∈I. AE y in T x. (x ## y) !! n ∈ U"
unfolding U_def
proof (induction n arbitrary: I)
case 0 then show ?case
by auto
next
case (Suc n)
{ fix x assume "x ∈ I"
have "AE y in T x. y !! n ∈ (SIGMA x:UNIV. K x)⇧* `` K x"
apply (subst AE_T_iff)
apply (rule measurable_compose[OF measurable_snth], simp)
apply (rule Suc)
done
moreover have "(SIGMA x:UNIV. K x)⇧* `` K x ⊆ (SIGMA x:UNIV. K x)⇧* `` I"
using ‹x ∈ I› by (auto intro: converse_rtrancl_into_rtrancl)
ultimately have "AE y in T x. y !! n ∈ (SIGMA x:UNIV. K x)⇧* `` I"
by (auto simp: subset_eq) }
then show ?case
by simp
qed
then show "AE x in T' I. x !! n ∈ U"
by (simp add: AE_T')
qed (simp_all add: TH MC MC')
qed
end