WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Markov chain

Revision #3512 → #4058 · back to history

modifiedMarkov chain / Markov process5c36b14d57ac
FieldFrom #3512To #4058
noteMathlib has Markov kernels and Ionescu-Tulcea trajectory measures (`ProbabilityTheory.trajMeasure`) that yield Markov processes by iteration, but no single bundled `MarkovProcess`/`MarkovChain` definition.Mathlib has Markov kernels and Ionescu-Tulcea trajectory measures (`ProbabilityTheory.Kernel.trajMeasure`) that yield Markov processes by iteration, but no single bundled `MarkovProcess`/`MarkovChain` definition.
modifiedMarkov chain with memory (order m)84aee3c5d61b
FieldFrom #3512To #4058
anchors[{"section":"Variations","snippet":"A Markov chain with memory (or a Markov chain of order m ) where m is finite"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{}&\\Pr(X_{n}=x_{n}\\mid X_{n-1}=x_{n-1},X_{n-2}=x_{n-2},\\dots ,X_{1}=x_{1})\\\\=&\\Pr(X_{n}=x_{n}\\mid X_{n-1}=x_{n-1},X_{n-2}=x_{n-2},\\dots ,X_{n-m}=x_{n-m}){\\text{ for }}n>m\\end{aligned}}}"}][{"section":"Variations","snippet":"A Markov chain with memory (or a Markov chain of order m ) where m is finite"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{}&\\Pr(X_{n}=x_{n}\\mid X_{n-1}=x_{n-1},X_{n-2}=x_{n-2},\\dots ,X_{1}=x_{1})\\\\=&\\Pr(X_{n}=x_{n}\\mid X_{n-1}=x_{n-1},X_{n-2}=x_{n-2},\\dots ,X_{n-m}=x_{n-m}){\\text{ for }}n>m\\end{aligned}}}"}]
addedTransition rate matrix (Q-matrix)e6bd2e3a2136
addedKolmogorov forward equatione6e632ae5688
addedChapman–Kolmogorov equationc0dbeeda6c4c
modifiedMean hitting timeb80430c7848a
FieldFrom #3512To #4058
mathlib.moduleMathlib.Probability.Process.HittingTime.leanMathlib.Probability.Process.HittingTime