Markov categories PR

Stream: mathlib4

[Jacob Reinhold]

Hi all! I've opened a PR to add Markov categories to mathlib: https://github.com/leanprover-community/mathlib4/pull/29657

The PR includes the basic MarkovCategory typeclass, a proof that cartesian categories are Markov categories, and FinStoch (finite stochastic matrices) as a concrete example.

I'm not an expert in this area; I've been learning it while implementing. I'd appreciate review for mathematical correctness, idiomatic Lean style, and whether mathlib wants this at all. I kept the PR small on purpose, although the FinStoch/Monoidal.lean proofs were a bit tricky for me (I suspect there's an easier way to go about it). If there's interest, future PRs could add conditional independence, sufficient statistics, and connections to existing probability theory.

Would anyone be willing to take a look? Happy to answer questions or make changes based on feedback.

[David Michael Roberts]

Have you considered doing CD monoidal categories, and then Markov categories as a special case?

[Jacob Reinhold]

I can implement copy-discard categories with Markov as a special case (adding del_natural seems to be the only change in my implementation at least).

The main consideration here is if anyone would actually be interested in CD monoidal categories and use it; I definitely have use cases for Markov categories—and there appears to be active research on Markov categories—but I don't clearly have a use-case for CD categories, so YAGNI. Implementing only Markov categories requires less work to maintain and is easier to review.

It's not a hard change though, I can submit another PR with a CopyDiscardCategory and MarkovCategory as a special case for comparison.

[Dominic Steinitz]

Great that you are doing this but I have neither the time nor the expertise to review. You might try contacting Paolo Perrone or Sam Staton. They (or maybe just Sam) work on probabilistic programming languages (as well as Markov Categories) with one written in Haskell. I would guess they are sympathetic to formalisation (and maybe they are already working on it).

[Matteo Cipollina]

This would be a great addition. In case you have missed it, we also have PF theorem currently being PRd , in particular below version for stochastic matrices could be relevant as it will give some nice properties to FinStoch:
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Stochastic.lean
You may want also to keep an eye on #28728 and future to keep mutual compatibility with some proposed defs in the current PR, like the definitions of Irreducible and Primitive matrices used in the PF and based on Quiver API, and ones on Cyclic Quivers and Aperiodic matrices which are ready and will follow in the next PRs .
#maths > Formalizing Perron-Frobenius

[David Michael Roberts]

@Jacob Reinhold it just seems to me to be the mathlib way, that's all.

[David Michael Roberts]

It feels like formalising AB5 abelian categories without formalising abelian categories, rather than doing abelian categories and adding AB5 as an additional condition.

[Jacob Reinhold]

@David Michael Roberts Sounds reasonable to me. Working on this.

[Jacob Reinhold]

FYI, implemented copy-discard categories and Markov categories as an extension of them here.

[Joël Riou]

You should obviously split this in smaller PRs. You may tag #29657 as WIP, and start a new PR which would basically just add Monoidal.CommComonObj and CopyDiscardCategory.Basic. (150-250 lines a reasonable length for a PR; we try to refrain frolm adding significantly more than that at a time.)

[Jacob Reinhold]

Figured. Will do

[Jacob Reinhold]

Keeping it even smaller for the first of the PR stack: https://github.com/leanprover-community/mathlib4/pull/29919 @Joël Riou