Formalizing Probabilistic Arguments

Stream: maths

[David Ledvinka]

Currently I have been working on (analytical) infrastructure for probability theory in mathlib, but I have been thinking ahead to how one would formulate certain probabilistic arguments and I am concerned that a lot of basic probabilistic arguments would be extremely clunky to formalize and I was wondering if anyone has any ideas on how this could be improved. A very common technique in probabiltiy theory is to introduce additional sources of randomness. I think this idea is best captured by the following quote from Terence Tao's "Topics in Random Matrix Theory": " In order to have the freedom to perform extensions every time we need to introduce a new source of randomness, we will try to adhere to the following important dogma: probability theory is only “allowed” to study concepts and perform operations which are preserved with respect to extension of the underlying sample space. As long as one is adhering strictly to this dogma, one can insert as many new sources of randomness (or reorganise existing sources of randomness) as one pleases; but if one deviates from this dogma and uses specific properties of a single sample space, then one has left the category of probability theory and must now take care when doing any subsequent operation that could alter that sample space. This dogma is an important aspect of the probabilistic way of thinking, much as the insistence on studying concepts and performing operations that are invariant with respect to coordinate changes or other symmetries is an important aspect of the modern geometric way of thinking. With this probabilistic viewpoint, we shall soon see the sample space essentially disappear from view altogether, after a few foundational issues are dispensed with."

To perform this kind of argument with current Mathlib I think you would need to construct the new source of randomness, construct the product of the samples spaces, pull everything back to the product and show that all the properties you need still hold in the product space, and then project what you need back down to the original sample space.

Even with a bunch of lemmas that proves you can do these things it still seems extremely clunky. I was thinking perhaps one could design a tactics for this purpose but I am not sure if this is reasonable? For example if I have a theorem of the form:

example {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}  {X : Ω → ℝ}
hX : Measurable X) (Xdist : μ.map f = gaussianReal 0 1) :  μ [X] = 0

and I use the tactic (say) indep_copy X. Then it would do all the projection stuff for me and give me the current proof state

{Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}  {X : Ω → ℝ}
(hX : Measurable X) (Xdist : μ.map f = gaussianReal 0 1)
{Y : Ω → ℝ} (hY : Measurable Y) (h_indep : IndepFun X Y μ)
(h_id : IdentDistrib X Y μ μ) :  μ [X] = 0

Perhaps one could design tactics that could do this sort of transformation so long as you follow the philosophy outlined in the Tao quote. Of course this is much much easier said than done but I am just curious if these seems like a reasonable idea or if anyone else has thought about other ways to overcome this problem in formalizing probability theory?

[Etienne Marion]

Maybe this topic opened by Terence is of interest.

[Lawrence Wu (llllvvuu)]

PFR does the indep copies thing:

https://teorth.github.io/pfr/docs/PFR/Mathlib/Probability/IdentDistrib.html#ProbabilityTheory.independent_copies

and the rest of this file onward

[David Ledvinka]

Thanks for pointing this out! My worry is that exactly this kind of theorem will be clunky to use in complicated cases but I will investigate how it was used in PFR (and perhaps such clunkiness can't be avoided).

[David Ledvinka]

Like even in a simple case where I want to prove something about $X$ by coupling with an independent copy $Y$, if I were to use this theorem I think I would have to use it to get two independent "copies" $X'$ and $Y'$, prove what I want about $X'$ and then using the fact that it is identically distributed with $X'$ to pass my conclusion back to $X$. This isnt too bad but more complicated examples could be worse and to me it feels like it should be possible to have a tactic that just does this automatically (using theorems like this on under the hood) so that if I put indep_copy X it gives me the exact same proof and goal state but with an independent copy of $X$ (so long as everything checks out).

[David Ledvinka]

Perhaps I am too optimistic about making arguments work like they do on paper and I'm overestimating how fiddly this is.

[Kevin Buzzard]

(double-dollars for LaTeX in Zulip, e.g. $$X$$, this doesn't display on its own line here)