Theory Example_B
theory Example_B
imports "../Classifying_Markov_Chain_States"
begin
section ‹Example B› text_raw ‹\label{ex:B}›
text ‹
We now formalize the following Markov chain:
\begin{center}
\begin{tikzpicture}[thick]
\begin{scope} [rotate = 45]
\path [fill, color = gray!30] (7.5, -6) ellipse(3 and 1) ;
\end{scope}
\node (bot2) at (7, -0.5) {} ;
\node[draw, circle] (1) at ( 8, -0.5) {$0$} ;
\node[draw, circle] (2) at ( 9, 0.5) {$1$} ;
\node[draw, circle] (3) at (10, 1.5) {$2$} ;
\node (inft) at (10.7, 2.6) {} ;
\node (infb) at (11, 2) {} ;
\node (inf1) at (10.5, 2) {} ;
\node (inf2) at (11.5, 3) {} ;
\path[->, >=latex]
(bot2) edge (1)
(1) edge [loop below] node [right] {$\frac{2}{3}$} (1)
edge [bend left=30] node [above] {$\frac{1}{3}$} (2)
(2) edge [bend left=30] node [below] {$\frac{2}{3}$} (1)
edge [bend left=30] node [above] {$\frac{1}{3}$} (3)
(3) edge [bend left=30] node [below] {$\frac{2}{3}$} (2)
edge [bend left=30] node [above] {} (inft)
(infb) edge [bend left=30] node [above] {} (3) ;
\path (inf1) edge [loosely dotted] (inf2) ;
\end{tikzpicture}
\end{center}
As state space we have the set of natural numbers, the transition function @{term tau} has three
cases:
›
definition K :: "nat ⇒ nat pmf" where
"K x = map_pmf (λTrue ⇒ x + 1 | False ⇒ x - 1) (bernoulli_pmf (1/3))"
text ‹For the special case when @{term "x = (0::nat)"} we have @{term "x - 1 = (0::nat)"} and hence
@{term "tau 0 0 = 2 / 3"}.›
text ‹We pack this transition function into a discrete Markov kernel.›
text ‹We call the locale of the Markov chain ‹B›, hence all constants and theorems
from this Markov chain get a ‹B› prefix.›