Formalization paper on probability theory

Stream: general

[Etienne Marion]

Hi everyone! Last year I formalized the Ionescu-Tulcea theorem and the product of infinitely many probability measures, which is a direct consequence, during an internship with @Sébastien Gouëzel. The final piece of code made it to Mathlib this week. I wrote a paper about it, if you have some time to look at it I would be very grateful to have some feedback. This is the first paper I have ever written so I am happy to take any kind of comments.

Abstract: "We describe the formalization of the Ionescu-Tulcea theorem, showing the existence of a probability measure on the space of trajectories of a Markov chain, in the proof assistant Lean using the integrated library mathlib. We first present a mathematical proof before exposing the difficulties which arise when trying to formalize it, and how they were overcome. We then build on this work to formalize the construction of the product of an arbitrary family of probability measures."

Etienne-MARION_Ionescu-Tulcea.pdf

[Yaël Dillies]

That's great! I will update GibbsMeasure to use your arbitrary product of probability measures

[Jason Rute]

You may also be interested in this formalization of probability theory, including product measures, in Coq by my previous colleagues @Avi Shinnar and @Barry Trager at IBM. I think this is the paper: https://ieeexplore.ieee.org/document/9833555

One reason I mention it is that the authors also formalize a notion of dependent product measure on a dependent product sigma algebra, which is something interesting you can do in dependent type theory. (I realize I don't know the details, in particular how you manage the measurability condition on the dependent sum.)

[Etienne Marion]

Jason Rute said:

You may also be interested in this formalization of probability theory, including product measures, in Coq by my previous colleagues Avi Shinnar and Barry Trager at IBM. I think this is the paper: https://ieeexplore.ieee.org/document/9833555

One reason I mention it is that the authors also formalize a notion of dependent product measure on a dependent product sigma algebra, which is something interesting you can do in dependent type theory. (I realize I don't know the details, in particular how you manage the measurability condition on the dependent sum.)

Thank you for the pointer! Indeed it is interesting, the only formalization I had heard of was the one in Isabelle/HOL where there are no dependent types. The main difference of course is that they build a product measure directly instead of proving the more powerful Ionescu-Tulcea theorem first. Unfortunately I cannot access the paper.

[Avi Shinnar]

The condition that we required in the dependent case can be seen here: https://github.com/IBM/FormalML/blob/master/coq/ProbTheory/ProductSpaceDep.v#L37

[Rémy Degenne]

Can you explain a bit more what that line is doing? I have trouble parsing the code.

[Etienne Marion]

I think it's saying: given $b : (i : \iota) \to Set (X_i)$, we require $i \mapsto P_i(b_i)$ to be measurable, where $P_i$ is a probability measure over $X_i$ (and each $b_i$ has to be measurable).

[Jason Rute]

Here is also a talk, but I think it only covers the non-dependent versions of the definitions (but it might help for the definitions in that line): https://www.youtube.com/watch?v=TxmWPuki1NI

[Avi Shinnar]

I wrote the following up just now, but I think @Etienne Marion did a better job summarizing succinctly :-)

given X a space and Y a family of spaces indexed by elements of X
with a sigma algebra A over X and a family (B:forall a:X, SigmaAlgebra (Y a))
and probability spaces psA over A and the family psB over the corresponding family B

we require that for every "event family" b, (with type (∀ (a:X), event (B a)))
-- read this as a family of events in the dependent family B indexed by elements in X
-- so given a point a in X, it returns the corresponding event in the dependent space (B a)
the function from points in A to the probability of the corresponding member of the event family in B
be measurable (where the domain sigma algebra is the provided one and the codomain sigma algebra is the borel sigma algebra over R)

[Rémy Degenne]

If I understand correctly, you have probability measures for all the Y a, indexed by a : X, and you suppose that they are the values of a Markov kernel.

[Etienne Marion]

However I'm not sure I understand why there is this hypothesis. Does it give you something more general than just having no measurability structure on the index type? (which would amount to pick the discrete $\sigma$-algebra in your code).

[Etienne Marion]

Rémy Degenne said:

If I understand correctly, you have probability measures for all the Y a, indexed by a : X, and you suppose that they are the values of a Markov kernel.

So that would be some kind of "dependent Markov kernel".

[Rémy Degenne]

I think the construction in that file is the measure obtained by composing a measure on X and that dependent Markov kernel.