Stationary distribution of Markov chains

Stream: Is there code for X?

[Markus de Medeiros]

Are there any results proven for the stationary distributions of (discrete time + discrete state) Markov chains?

[David Ledvinka]

I don't even think Markov process or the Markov property are defined. As is the case with Martingales I think the initial theory should be given in as general as possible setting and then can become more specialized as it becomes harder to treat the theory in a unified way

[David Ledvinka]

Transition kernels are defined however (and a bunch of theory for them). I suppose you could define stationary measure of a Transition kernel.

[Markus de Medeiros]

Thanks!

[Rémy Degenne]

We have a definition https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Kernel/Invariance.html#ProbabilityTheory.Kernel.Invariant but nothing about it

[Matteo Cipollina]

FYI there is some basic framework in this direction here (as part of our ongoing formalization of neural networks) https://github.com/or4nge19/HopfieldNet/blob/master/HopfieldNet/Markov.lean, but the Markov chains part is still at a very early stage yet and an ongoing WIP