Markov chains ?

Stream: Is there code for X?

[Sophie Morel]

Are Markov chains in mathlib ? I couldn't find them, but I do not claim to be an expert searcher. If not, do you know if somebody working on formalizing them ? I am interested in discrete-time, and mostly in discrete space too.

[Sebastien Gouezel]

They're not there yet, but @Rémy Degenne is working on the prerequisites on kernels, towards a general theory. See for instance the directory (in mathlib3) probability/kernel/.

[Sophie Morel]

Thank! Do you know if he intends to do Markov chains after that ?

[Sebastien Gouezel]

I guess that's the plan, but I have no idea about the time scale.

[Rémy Degenne]

I am indeed adding prerequisites for Markov decision processes (MDP), which become Markov chains if you choose a policy. That means that I'll have to add everything needed for markov chains along the way. I am not taking the quick route though, and it will take time: I try to develop each notion needed in a general enough setting, in order to not get only MDPs at the end, but also a good foundation for other probability results.

[Rémy Degenne]

My next step is to define conditional independence, but the way I want to do it requires a refactor of the current definition of independence, and that has already been ported. So the project is on hold until the end of the port (which is imminent :) )and will resume in mathlib 4.

[Kevin Buzzard]

You are already allowed to edit and add stuff to mathlib4

[Yury G. Kudryashov]

AFAIK, refactors are not allowed yet.

[Kevin Buzzard]

Yeah that would be probably going a bit too far right now, maybe wait about 10 days until the port is done :-)

[Rémy Degenne]

The refactor would break at least one proof in an unported file and would change the imports of several ported and unported files. Attempting to do it now would create a mess. Allowed or not, it's much better to do it once everything is ported.

[Johan Commelin]

Which is hopefully about 2 weeks from now.

[Scott Morrison]

At this point it seems we are okay with golfing proofs, adding new lemmas, add new files, but not reorganising or refactoring.

[Sophie Morel]

Rémy Degenne said:

I am indeed adding prerequisites for Markov decision processes (MDP), which become Markov chains if you choose a policy. That means that I'll have to add everything needed for markov chains along the way. I am not taking the quick route though, and it will take time: I try to develop each notion needed in a general enough setting, in order to not get only MDPs at the end, but also a good foundation for other probability results.

Gotcha, thank you for explaining your plans !