# Theory Example_A

theory Example_A
imports "../Classifying_Markov_Chain_States"
begin

section ‹Example A› text_raw ‹\label{ex:A}›

text ‹

We formalize the following Markov chain:

\begin{center}
\begin{tikzpicture}[thick]

\path [fill, color = gray!30] (0, 0) circle(0.6) ;

\path [fill, color = gray!30] (1, 1) circle(0.6) ;

\path [fill, color = gray!30] (4.5, 0.66) ellipse(2 and 1.9) ;

\node (bot)  at (-1, 0) {} ;

\node[draw,circle] (A)  at (0, 0) {$A$} ;

\node[draw,circle] (B)  at (1, 1) {$B$} ;

\node[draw,circle] (C1) at (3, 0) {$C_1$} ;

\node[draw,circle] (C2) at (6, 0) {$C_2$} ;

\node[draw,circle] (C3) at (4.5, 2) {$C_3$} ;

\path[->, >=latex]
(bot) edge (A)
(A)   edge                node [above] {$\frac{1}{2}$} (B)
edge                node [below] {$\frac{1}{2}$} (C1)
(B)   edge [loop above]   node [left]  {$\frac{1}{2}$} (B)
edge [out = 0]      node [above] {$\frac{1}{2}$} (C1)
(C1)  edge [loop above]   node [above] {$\frac{1}{3}$} (C1)
edge [bend left=15] node [above] {$\frac{1}{3}$} (C2)
edge [bend left=15] node [above] {$\frac{1}{3}$} (C3)
(C2)  edge [loop right]   node [above] {$\frac{1}{3}$} (C2)
edge [bend left=15] node [above] {$\frac{1}{3}$} (C1)
edge [bend left=15] node [above] {$\frac{1}{3}$} (C3)
(C3)  edge [loop right]   node [above] {$\frac{1}{2}$} (C3)
edge [bend left=15] node [above] {$\frac{1}{4}$} (C1)
edge [bend left=15] node [above] {$\frac{1}{4}$} (C2) ;

\end{tikzpicture}
\end{center}

First we define the state space as its own type:

›

datatype state = A | B | C1 | C2 | C3

text ‹Now the state space is ‹UNIV :: state set››

lemma UNIV_state: "UNIV = {A, B, C1, C2, C3}"
using state.nchotomy by auto

instance state :: finite

text ‹The transition function ‹tau› is easily defined using the case statement, this allows
us to give a sparse specification as all ‹0› cases are collected at the end.›

definition tau :: "state ⇒ state ⇒ real" where
"tau s t = (case (s, t) of
(A,  B)  ⇒ 1 / 2 | (A,  C1) ⇒ 1 / 2
| (B,  B)  ⇒ 1 / 2 | (B,  C1) ⇒ 1 / 2
| (C1, C1) ⇒ 1 / 3 | (C1, C2) ⇒ 1 / 3 | (C1, C3) ⇒ 1 / 3
| (C2, C1) ⇒ 1 / 3 | (C2, C2) ⇒ 1 / 3 | (C2, C3) ⇒ 1 / 3
| (C3, C1) ⇒ 1 / 4 | (C3, C2) ⇒ 1 / 4 | (C3, C3) ⇒ 1 / 2
| _ ⇒ 0)"

lift_definition K :: "state ⇒ state pmf" is tau
by (auto simp: tau_def nn_integral_count_space_finite UNIV_state split: state.split simp del: ennreal_plus)

text ‹We use the ‹finite_pmf›-locale which introduces the point measure ‹tau.M›, and
provides us with the necessary simplifier setup.›

interpretation A: MC_syntax K .

subsection ‹The essential classs @{term "{C1, C2, C3}"}›

context
begin

interpretation pmf_as_function .

lemma A_E_eq:
"set_pmf (K x) = (case x of A ⇒ {B, C1} | B ⇒ {B, C1} | _ ⇒ {C1, C2, C3})"
using state.nchotomy by transfer (auto simp: tau_def split: prod.split state.split)

lemma A_essential: "A.essential_class {C1, C2, C3}"
by (rule A.essential_classI2) (auto simp: A_E_eq)

lemma A_aperiodic: "A.aperiodic {C1, C2, C3}"
unfolding A.aperiodic_def
proof safe
have eq: "⋀x'. (if x' = C1 then 1 else 0) = indicator {C1} x'" by auto

show "{C1, C2, C3} ∈ UNIV // A.communicating"
using A_essential by (simp add: A.essential_class_def)
then have "A.period {C1, C2, C3} = Gcd (A.period_set C1)"
by (rule A.period_eq) simp
also have "… = 1"
by (rule Gcd_nat_eq_one) (simp add: A_E_eq A.period_set_def A.p_Suc' A.p_0 eq measure_pmf_single pmf_positive)
finally show "A.period {C1, C2, C3} = 1" .
qed

subsection ‹The stationary distribution ‹n››

text ‹Similar to ‹tau› we introduce ‹n› using the ‹finite_pmf›-locale.›

lift_definition n :: "state pmf" is "λC1 ⇒ 0.3 | C2 ⇒ 0.3 | C3 ⇒ 0.4 | _ ⇒ 0"
by (auto simp: UNIV_state nn_integral_count_space_finite split: state.split)

lemma stationary_distribution_N: "A.stationary_distribution n"
unfolding A.stationary_distribution_def
apply (auto intro!: pmf_eqI simp: pmf_bind integral_measure_pmf[of UNIV])
apply transfer
apply (auto simp: UNIV_state tau_def split: state.split)
done

lemma exclusive_N[simp]: "set_pmf n = {C1, C2, C3}"
using state.nchotomy by transfer (auto split: state.splits)

end

lemma n_is_limit:
assumes x: "x ∈ {C1, C2, C3}" and y: "y ∈ {C1, C2, C3}"
shows "(A.p x y) ⇢ pmf n y"
using A.stationary_distribution_imp_p_limit[OF A_aperiodic A_essential _ stationary_distribution_N _ x y]
by simp

lemma C_is_pos_recurrent: "x ∈ {C1, C2, C3} ⟹ A.pos_recurrent x"
using A.stationary_distributionD(1)[OF A_essential _ stationary_distribution_N] by auto

lemma C_recurrence_time:
assumes x: "x ∈ {C1, C2, C3}"
shows "A.U' x x = 1 / pmf n x"
proof -
from A.stationary_distributionD(2)[OF A_essential _ stationary_distribution_N _]
have "A.stat {C1, C2, C3} = n" by simp
with x have "1 / pmf n x = 1 / emeasure (A.stat {C1, C2, C3}) {x}"
by (simp add: emeasure_pmf_single pmf_positive divide_ennreal ennreal_1[symmetric] del: ennreal_1)
also have "… = A.U' x x"
unfolding A.stat_def using x
by (subst emeasure_point_measure_finite) (simp_all add:  A.U'_def)
finally show ?thesis ..
qed

end