probability

Stream: Is there code for X?

[Jalex Stark]

I remember some people talking about how it's hard to think of a good API for probability (with random variables and independence and all that) in the context of proving the existence of special graphs with the probabilistic method

[Jalex Stark]

do we have any nontrivial theorems involving an infinite sequence of random variables on the same space, say a central limit theorem?

[Jalex Stark]

If not, I think that "prove anything that looks like a central limit theorem, and then study it to understand what is needed from the probability API" is a good line of work

[Johan Commelin]

We have a whole bunch of stuff on measure spaces. But nothing specialised to probability. At some point there was a PR by @Koundinya Vajjha. I don't know what happened to it. Maybe it can be resurrected?

[Jalex Stark]

Yeah, I agree that the measure spaces are mature enough that it should be easy to do probability on top of

[Koundinya Vajjha]

Apologies. I do have a tiny probability theory library up in a different repo, but it's out of date and breaks with current mathlib. I keep putting it off but I promise to devote some time to it the next couple of weeks and will try to PR.

[Patrick Massot]

PR, PR, PR before it's too late. Every Lean code that is not PRed to mathlib is doomed to bit rot.

[Jalex Stark]

link to your repo?

[Koundinya Vajjha]

Jalex Stark said:

link to your repo?

https://github.com/jtristan/stump-learnable/tree/master/src/lib/attributed

[David Wärn]

This looks quite nice! I can see a pi-instance for measurable spaces, and binary products for measure spaces: is there a pi-instance for probability spaces somewhere?

[Koundinya Vajjha]

no, sorry. isn't that https://en.wikipedia.org/wiki/Ionescu-Tulcea_theorem?

[Koundinya Vajjha]

I think proving Ionescu Tulcea was originally what @Johannes Hölzl was aiming at

[David Wärn]

Hmm I haven't seen that. I'm thinking of something like question 14 here (countability is beside the point)
http://www.dpmms.cam.ac.uk/study/II/Probability%2BMeasure/ex2.pdf
It seems to me like you have all the ingredients for this construction, but it's maybe a bit technical

[Johan Commelin]

@Koundinya Vajjha Would you mind starting a github project over at https://github.com/leanprover-community/mathlib/projects with little stubs of what you think should be done?

[Jalex Stark]

I guess what I want from a probability interface is to just expose the "algebra of random variables". The fact that this can be modeled with measure spaces should be left on the inside

[Sebastien Gouezel]

Jalex Stark said:

I guess what I want from a probability interface is to just expose the "algebra of random variables". The fact that this can be modeled with measure spaces should be left on the inside

Many interesting theorems in probability really depend on the fact that you have a measure space, and that the notion of "almost surely" is well behaved. Think of the strong law of large numbers, or the martingale convergence theorem, for instance.

[Jalex Stark]

how much well behavedness do you need? isn't it enough to know that countable intersections of almost sure events are almost sure?

[Mario Carneiro]

isn't that basically a measure space?

[Mario Carneiro]

or at least a sigma algebra

[Mario Carneiro]

I don't know how you intend to say anything quantitative about probabilities themselves without a measure though

[Reid Barton]

I think the idea behind "algebra of random variables" is that you want to avoid committing to the idea that random variables are functions at all

[Reid Barton]

or at least, you want to avoid committing to the idea that they are functions on some specific measure space $\Omega$

[Mario Carneiro]

but you can still ask probability questions about them?

[Jalex Stark]

yes

[Mario Carneiro]

then can't you reverse engineer a measure space from that?

[Sebastien Gouezel]

What really matters is not that they are functions, but their joint distribution, as a measure on $\mathbb{R}^{\mathbb{N}}$ if you are considering real-valued random variables indexed by integers for instance.

[Reid Barton]

They still have expectations, for example. Except for the ones that don't, and that is where things start to get a bit tricky...

[Jalex Stark]

Mario Carneiro said:

then can't you reverse engineer a measure space from that?

yes, once you've given any finite amount of information about your variables, there's surely some "minimal" measure space + functions from it that models the things you've said

[Jalex Stark]

but you want to remain agnostic about whether you're using the minimal one or an arbitrary extension of it

[Mario Carneiro]

I was thinking of using all the possible questions you could ask about the variables

[Mario Carneiro]

(not finite)

[Jalex Stark]

sure, that will have a minimal model by a measure space

[Jalex Stark]

and we remain agnostic about whether or not we're adding more variables later

[Mario Carneiro]

that seems difficult to do in lean

[Mario Carneiro]

you can't just add elements to a type, not without rejiggering everything on top

[Jalex Stark]

i agree that it's hard

[Jalex Stark]

I don't think it's adding complexity though

[Reid Barton]

It's similar to how you might do a computation using "indeterminates", which you could think of as happening in a polynomial or power series ring, but then later you might introduce another indeterminate.

[Jalex Stark]

if you "do probability" with measure spaces then you're going to be dealing with these extensions of your measure space all the time

[Mario Carneiro]

if you have a measure space you already have all random variables that could ever exist, so adding a new one is trivial

[Reid Barton]

You only have the ones that exist on that space. The kind of thing you would want to add is a new variable that's independent from all of those (e.g., by forming a product measure space)

[Jalex Stark]

if I want to add a new one with the constraint that it's independent from all the ones I have talked about before, without extending the space, that's not trivial
I guess the way you'd do it is to extend to a product space and then apply an isomorphism of measure spaces between the original space and its extension

[Jalex Stark]

and the point is that it would be nice to have machinery that does that for you

[Jalex Stark]

you have to keep track of the notion of "random variables that are in scope for this discussion"

[Jalex Stark]

but you already have to do that when doing probability informally anyway

[Mario Carneiro]

Color me skeptical

[Reid Barton]

The funny thing is that type theory gets to have this built in

[Jalex Stark]

gets what built in?

[Reid Barton]

It basically took all the good ideas for itself but doesn't reexport them to the internal language

[Reid Barton]

having a variable context that can be extended by lambdas, etc

[Jalex Stark]

Mario Carneiro said:

Color me skeptical

I'm taking your comment to mean "the things you're describing sounds possible in principle, but I bet if I thought about it for a while I would find a different way to do probability that felt easier and/or more natural"

[Mario Carneiro]

You would need to first do it the hard way enough times for us to notice the pattern and abstract it into a tactic

[Mario Carneiro]

this is not the kind of design you are likely to get right on the first try

[Mario Carneiro]

I need to see some of these probability arguments where you are dynamically adding variables to give guidance about how best to model them

[Sebastien Gouezel]

As I said, this "minimal model" is exactly the joint distribution of all your random variables on $\mathbb{R}^{\mathbb{N}}$ (i.e., the image of your probability on $\Omega$ under the map $\omega \mapsto (X_0(\omega), X_1(\omega), \dotsc)$), and your new random variable is just the $n$-th coordinate.

[Johan Commelin]

At POPL I had an interesting discussion with Neel Krishnaswami, and he explained that he was working on some DSL in DTT that captured the semantics of probability theory in a way interesting to the working probability theorist. Maybe we should ask him to explain it in more detail. (I guess that most of my first sentence is nonsense on the nose.)

[Jalex Stark]

I think DTT is dependent type theory, what DSL?

[Kevin Buzzard]

Domain specific language?

[Johan Commelin]

domain specific language

[Jalex Stark]

cool, thanks

[Kevin Buzzard]

I put the question mark because I have no idea what this means ;-)

[Jalex Stark]

my guess is it means "programming language where you're always working inside of some specific monad"

[Mario Carneiro]

in this context it probably means that you can do things like Jalex suggested like create new random variables and put them together in a monad

[Sebastien Gouezel]

The Giry monad, right?

[Mario Carneiro]

I've been told there is some foundational issue with higher order functions in the Giry monad though

[Mario Carneiro]

which makes the denotation of "probabilistic programs" dubious

[Koundinya Vajjha]

The category of measurable spaces isn't Cartesian closed. (There isn't a canonical measurable space structure on the function type which makes the evaluation maps measurable). So the Giry monad can't eat higher order functions and so you can use it to denotate only a small uninteresting subset of probabilistic programming languages.

[Koundinya Vajjha]

But there have been other gadgets ("Quasi-Borel Spaces") which overcome this issue IIRC.

[Alex J. Best]

Koundinya Vajjha said:

Apologies. I do have a tiny probability theory library up in a different repo, but it's out of date and breaks with current mathlib. I keep putting it off but I promise to devote some time to it the next couple of weeks and will try to PR.

I've updated (almost all of?) this to a recent mathlib over at https://github.com/alexjbest/stump-learnable

[Kenny Lau]

everything not PR’d is lost in time — Ancient Chinese Proverb

[Martin Zinkevich]

Hi all,
I was working on probability and measure theory as well, and was pointed to this thread.

I looked over your code, and noticed you have the basic stuff, as well as advancements like the Giray Monad.

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Radon-Nikodym.20Theorem

Specifically, see:

https://github.com/google/formal-ml/blob/master/src/formal_ml/probability_space.lean

There are a lot of design questions that it would be good to talk about:

1. random variables/measurable functions/events/measurable sets as types?
   This allows for there to be semirings, et cetera. OTOH, more stuff to unfold. A key point was thinking about a measurable function
   as a function from a measurable space to another measurable space, and a random variable as a function from a probability space
   to a measurable space, such that expectation and probability of random variables and events could be explicit.

2. Syntactic sugar? I was impressed that you could write Pr[A ∧ᵣ B]≤ Pr[A], and E[X + Y]=E[X] + E[Y]
   I think that this lift from the complexities and details of measure theory may be important for wider adoption.

3. probability_space or probability_measure? This question is perhaps the most deep, as going both ways will split the code needlessly. Either is better than going both ways.

4. independent variables/identical variables: these are very important to me as a ML researcher.

Anyway, we should figure out how to get more probability theory into mathlib.

[Johan Commelin]

The Giry monad is now in mathlib, btw

[Adam Topaz]

NB: https://github.com/leanprover-community/mathlib/blob/ae72826a13a0ce58bf75cc58c0c2219b567df2fa/src/measure_theory/giry_monad.lean#L16

[Adam Topaz]

I.e. mathlib's Giry monad has all measures.

[Adam Topaz]

Unless there is another Giry monad in mathlib that I don't know about @Johan Commelin ?

[Reid Barton]

I wouldn't be too surprised if this was just because it predated the existence of probability measures

[Adam Topaz]

Yeah I'm sure this is the case, but I don't think mathlib has the monadic structure on probability measures. I would be happy to be wrong.

[Martin Zinkevich]

Giry monads aside, what are the thoughts on probability spaces versus probability measures?

-Marty

[Adam Topaz]

Is a probability space the same thing as a measurable space endowed with a probability measure? If so, this is essentially a bundled vs. unbundled question.

[Adam Topaz]

What are the morphisms in the category of probability spaces?

[Martin Zinkevich]

Hmmm...I am not sure how to answer that (I don't understand category theory).

Here is my best effort to answer your question literally:

Okay, measurable spaces are over sets, and probability space is with respect to a measurable space. So these are our objects.

Consider probability space PA over A. If you have a function f:A -> B, then:
Define measurable space MB over B such that B' is measurable iff its preimage in A is measurable.
Define probability measure PB over B such that the measure of any measurable B' is the measure of its preimage in A.

So each function from any set A to any set B serves as a morphism. An identity function serves as an identity. Composition of functions
gives the composite morphism. This function would be a measurable function from MA to MB, but not necessarily the only one.

From a category perspective, this is a "subcategory" of all measure spaces. I don't think it has an initial object.

In machine learning, we normally think about a single, "undefined" probability space. You could think about this as an initial object (insofar as the objects we are concerned with, as opposed to in the category of all probability spaces). We often don't think deeply about the nature of this probability space. What is important to us is the random variables defined as function from that probability space to other more meaningful sets, such as the reals, booleans, integers, et cetera. In these domains, what is measurable or not matters. Having a single initial object in our minds allows us to talk about the independence of any two arbitrary random variables in our model, whereas if we define each random variable more directly on its most obvious space (e.g., define a Gaussian as a probability space on the reals, or a binomial as a probability space on the natural numbers), then I can't talk about how they relate. However, mapping back to a "local" probability space is useful if I want to talk about integration.

From a category perspective, this is a "subcategory" of all unsigned measure spaces.

[Adam Topaz]

Okay I think I understand. The objects in the category are pairs $(X,\mu)$ where $X$ is a measurable space and $\mu$ is a measure (which so happens to be a probability measure in this case). And a morphism of pairs $(X,\mu) \to (X',\mu')$ is a measurable function $f : X \to X'$ such that for all measurable subsets $Y$ in $X'$, one has $\mu(f^{-1}(Y)) = \mu'(Y)$. Is this the category? This is asking for an equality of measures/functions on the nose, which seems problematic, no? Wouldn't something like this docs#measure_theory.ae_eq_fun have better properties?

[Adam Topaz]

I'm not really sure what you mean by ""undefined" probability space"

[Reid Barton]

The earlier discussion on this same topic from around May 15 actually discussed this concept a bit.

[Adam Topaz]

I think it would be interesting to construct this category in lean, where morphisms extend functions are defined "amost everyone" and agree "amost everywhere", etc.

[Reid Barton]

This paper proposes what seems to me a sensible categorical framework for this style of probabilistic reasoning, though I don't know what the implications are for formalization:
https://drops.dagstuhl.de/opus/volltexte/2017/8051/pdf/LIPIcs-CALCO-2017-1.pdf

[Adam Topaz]

Looks interesting. I think Voevodsky had some notes on a categorical foundation of probability theory.

[Martin Zinkevich]

Okay, I am a little confused. Perhaps I should not have mentioned the Giry monad. :-)
My primary interest is not in using category theory, but in being able to talk about probability and expectation.
If no categories were added, I would be fine. As I said, I don't understand category theory. I am not opposed to what you are suggesting, I just don't understand it.

I do like the idea of thinking about real random variables as a ring and ennreal random variables as a semiring, but that does not require category theory. I am excited about writing things like:
E[X * Y] = E[X] * E[Y]
E[2 * X] = E[X] + E[X]
Pr[X<Y ∧ᵣ B]
And so forth, so I can do machine learning. If category theory helps me in some way (such as being related to how all the theorems seem impossibly short in lean), then I am all for it.

Am I missing something? I know category theory is useful in Haskell programming, but I don't yet understand enough about mathlib and Lean. Does designing with category theory help me avoid disasters in the future?
-Marty

[Johan Commelin]

@Martin Zinkevich I think you can safely ignore category theory for the time being. Can you explain more about what is needed to get the nice notation that you wrote about above?
At some point, I've heard Neel Krishnaswami talk about some interesting ideas for making probability theory "possible" in type theoretic theorem provers. The problem (as I understood from him, again, I'm not a probability theorist) is that typical proofs in the area don't fit nicely in the DTT paradigm. So you need some sort of DSL on top of it, in order to add extra dimensions(?) [i.e. new random variables] to you probability space whenever you need them half-way a proof.

Does this make sense? If someone can make sense of what I'm saying, then it might be worth contacting Neel (he doesn't seem to be on this Zulip) in order to get some good advice on design decisions.

[Reid Barton]

I think the problem is precisely that nobody really knows how to formalize the style of argument used in probability theory. Of course we can "lower" any specific such argument into a proof in which the random variables become measurable functions on specific probability spaces and then formalize it, but this leaves something to be desired. Trying to understand probabilistic arguments on their own terms is an active topic in applied category theory, which isn't meant to imply that the eventual solution necessarily involves adopting a bunch of category theory, but just that there seems to be some real conceptual problem to solve here.

[Reid Barton]

For those who already speak the lingo, though, it seems plausible that these probabilistic arguments are really happening in the sheaf semantics of the topos described in that paper, so that when we assert the existence of a "fresh" random variable $Z$ which is independent of $X$, $Y$, ..., that variable $Z$ might only exist after we base change along a cover $\Omega' \to \Omega$ and pull back $X$, $Y$, ... to random variables on $\Omega'$.

[Reid Barton]

In any case, it's probably a good idea to start out by defining "a random variable on sample space $\Omega$ valued in $\mathbb{R}$", and defining expectation, proving linearity of expectation, etc., at least to the point where we can formalize the sorts of arguments that are supposedly awkward in this style, since it seems like the eventual underlying argument will have to be of this form anyways, and we'll learn more about these arguments by actually trying to formalize them.

[Reid Barton]

And maybe it turns out that the direct approach is adequate somehow (for example can we just pick $\Omega$ so large that for any countable collection of random variables on $\Omega$, we can still find a new random variable which is independent of them?)

[Kevin Buzzard]

Can someone explain why this whole probability thing is even an issue? I thought measure theory solved the problem of making probability theory rigorous. What is missing from the standard measure theory approach? Why isn't there just some dictionary expection -> some integral, standard deviation -> some integral etc?

[Reid Barton]

I'll try to cook up an example, but at a high level the issue is sort of like: if we want to talk about the local behavior of a function at a point, why don't we just use εs and δs? What's the deal with filters and germs?

[Kevin Buzzard]

I see -- so the issue is really that there is some interface problem, rather than a mathematical one?

[Reid Barton]

So suppose I'm interested in random graphs on $n$ vertices, and I've got a real-valued function $X$ of a graph that I'd like to think of as a random variable, and I want to prove a statement about the expectation of $X$.

[Reid Barton]

That's fine--we can define $\Omega$ to be the set of all graphs on $n$ vertices, and equip it with a probability measure $\mu$, and define $X$ as a function $X : \Omega \to \mathbb{R}$, and define the expectation as the integral of $X$ with respect to $\mu$--no problem so far.

[Reid Barton]

So, let's say we've managed to write down the statement of our proposition.

[Reid Barton]

Now maybe the proof, for whatever reason, starts like this:
Define a new random variable $Y$ as follows: flip a coin, and if it's heads return $X$; otherwise return $0$.

[Reid Barton]

Where obviously the coin flip is meant to be independent of the random graph we're talking about

[Reid Barton]

So, now I guess we have a problem because there is literally no "random variable" $Y : \Omega \to \mathbb{R}$ which has the correct relationship to $X$ (if I failed to set up the situation correctly, replace it with a better one :upside_down:).

[Reid Barton]

So, at this point we could apply what I guess would be the standard interpretation of this, and introduce a new sample space $\Omega' = \Omega \times \{\mathsf{heads}, \mathsf{tails}\}$ with the product measure, which comes with a measure-preserving projection $\pi : \Omega' \to \Omega$.

[Reid Barton]

Now, wherever we had $X$ before, we replace it by $X' := X \circ \pi : \Omega' \to \mathbb{R}$, and apply theorems that say things like (because $\pi$ is measure-preserving) the expectation of $X'$ is the same as the expectation of $X$, and so on, and so it doesn't really matter whether we talk about $X$ or $X'$.

[Kevin Buzzard]

Aah I see, you've said enough. Thanks.

[Kevin Buzzard]

In my brain, Y somehow operates in a different universe, but you have to take the product of these universes if you want to relate Y to stuff going on in another universe.

[Reid Barton]

This sheaf theory stuff is appealing to me because this "you might need to pull back everything in sight along a suitable map (cover) $\Omega' \to \Omega$, and then a thing will exist" is exactly what happens in the interpretation of the existential quantifier in the sheaf semantics, so you can use it to interpret the existential statement "there exists a random variable independent of $X$ with such-and-such distribution".

[Reid Barton]

So, to summarize, trying to find an $\Omega''''$ large enough that the whole argument works is sort of like trying to find an $\varepsilon''''$ small enough that the whole argument works, except instead of an inequality $\varepsilon'''' < \cdots < \varepsilon$ you have a map $\Omega'''' \to \cdots \to \Omega$ to keep track of, which is what makes it into a category theory problem and not an order theory one.
($\varepsilon$ is really controlling a set $(x - \varepsilon, x + \varepsilon)$ around $x$, so there are the same maps in the $\varepsilon$ case too, but everything is pinned down as an open subset of some ambient space.)

[Kevin Buzzard]

Thanks for this very coherent explanation.

[Reid Barton]

You can find other analogies in algebra--when you "adjoin an indeterminate" $Y$ (~ an independent random variable) to a ring $R$ then the map $R \to R[Y]$ that you implicitly apply everywhere is really pulling back "functions" on $\Omega = \mathrm{Spec}\, R$ along the cover $\Omega' = \mathrm{Spec}\, R[Y] \to \Omega$.

[Reid Barton]

And routinely regarding elements of $R$ (say $R = k[X]$) as also being elements of $R[Y] = k[X, Y]$ is something we do in algebra, that can be similarly annoying for formalization.

[Jacques Carette]

Mathematicians routinely elide obvious canonical injections. What formalization reveals is that, at least using current technology, these tend to chain badly. What I mean is that inserting 1 of these is no problem, but in general situations when you have to insert 10 of them in a working environment with 100s of potential coercions (aka canonical injections) in scope, it all grinds to a halt.

[Reid Barton]

Right, and what maybe doesn't transfer between otherwise analogous domains is that perhaps in algebra, say, you pretty much only ever insert a single coercion $R \to R[Y]$, while in probability theory you need to make a whole bunch of these extensions as you carry out some complex argument. (I'm not saying the situation is necessarily this way for these particular areas, though my guess would be that this is at least somewhat correct.)

[Jacques Carette]

But even in Algebra, you want to be careful about too much polymorphism. R[X] has properties that R[X,Y] does not have. So it would be a disaster if you use some term that is inferred to be in R[X] at one point, prove something using that extra property, then push it to R[X,Y] and have that property come along for free. This kind of laisser-faire leads to real bugs in computer algebra systems.

[Kevin Buzzard]

I am confident in the ability of the mathematicians using polynomials here that they are able to know when they are working in R[X] and when they are working in R[X,Y]. I absolutely agree that this informal "set-theoretic" world which mathematicians drop into when they are considering a collection of e.g. subrings of a ring is a very powerful intuition, but it cannot always be made to work, e.g. when you don't know how big your universe needs to be at the beginning of the argument (it might involve adjoining n indeterminates later, where n is a number which will only come out of a later calculation). If you don't know how big you want to be when you start, you're forced to build up rather than go down to subsets. The first time I discovered this I generated some huge thread in #maths called something like "algebra is not scaling for me". Since then I've understood the situation much better and am hoping that Kenny's is_scalar_tower tricks will help me in that particular situation.

[Jacques Carette]

This is the kind of knowledge that I'd love to find a way to capture. Right now, it is too ephemeral. Once the principled way of dealing with some fragile situation is found, especially when the principled way of doing things is really no harder than the 'sloppy' way, it needs to be highlighted. I already love it when I see lots of mathematicians here talk about API and the like. Of course, mathematicians have been using the equivalent of APIs for a long time (what's a Ring after all?), what isn't as well known is that "theories" as a whole have APIs too. And that not all APIs scale equally well. Bill Farmer and I have written about this in our papers High Level Theories from CICM 2008, and with Michael Kohlhase in Realms: A Structure for Consolidating Knowledge about Mathematical Theories at CICM 2014.

[Patrick Massot]

In principle there are formalization papers for disseminating this knowledge.

[Jacques Carette]

I agree, but I'm afraid that a lot of little gems would never end up being published. There is no good "Formalization Letters" kind of journal for 1-2 page papers. Both math and CS do themselves a disservice by forcing publishable chunks to be so large. [I hate slicing-and-dicing, don't get me wrong. A 20 page paper that has 1 page's worth of new material should never get published as is. If it were a <= 2 page paper, that's a different thing.]

[Kevin Buzzard]

We have Comptes Rendus but this is often for research announcements of larger stuff. I once disproved a conjecture of some fairly well-known guy, and the result could easily be described in just a few pages, so I wrote that up and sent it to Comptes Rendus and it got accepted.

[Martin Zinkevich]

To get back to Reid's example with a coin flip and a random variable.

In general, the approach used is that we assume that a single probability space exists, and then we define whatever functions necessary from it.

The coin flip could either be defined as an event or a random variable from P to bool.measurable_space.

C:P →r bool.measurable_space
X:P →r (borel real)

Then, one can define

Y=(indicator (C =r true)) * X

Here,C =r true is the event that C equals true. The indicator operator is a random variable that equals 1 if (C =r true), and zero otherwise. This is a very common tool we use in machine learning, and it is useful for things such as "how many examples are classified correctly?".
random_variable_independent_pair C X indicates that these two variables are independent.

So, here is an example of what we could write using probability_space.lean and real_random_variable.lean above:

lemma indicator_product {Ω:Type*} {P:probability_space Ω} {X Y:P →r borel nnreal} {C:P →r bool.measurable_space}:
  random_variable_independent_pair X C →
  Y = (indicator (rv_eq C (const_random_variable tt))) * X →
  E[Y] = Pr[rv_eq C (const_random_variable tt)] * E[X] := sorry

rv_eq C (const_random_variable tt) is basically (C =r true).

There are some caveats: random_variable_independent_pair technically requires two random variables of equal type right now, but there is no
reason that the codomains need to be equal. Obviously, a better equality event notation would be nice.

But, from a mathematical perspective, this is very close to what you are talking about.

[Johan Commelin]

@Martin Zinkevich pro tip: #backticks

[Kenny Lau]

@Reid Barton Is Giry monad a solution to the aforementioned problem? If not, what can solve it?

[Adam Topaz]

With the Giry monad the (measure associated Y) can be written with do notation approx like this

do a <- Bernoulli,
  b <- X,
  return a * b

I'm not really sure what problem you're referring to @Kenny Lau

[Kenny Lau]

Reid Barton said:

So, now I guess we have a problem because there is literally no "random variable" $Y : \Omega \to \mathbb{R}$ which has the correct relationship to $X$ (if I failed to set up the situation correctly, replace it with a better one :upside_down:).

[Kenny Lau]

this problem

[Adam Topaz]

And expected values should be thought of as the structure map for an algebra of the Giry monad

[Reid Barton]

Well, I'm assuming the proof really wants to talk about random variables and not just their distributions, which is what the Giry monad is about.

[Adam Topaz]

From the point of view of the Giry monad, real valued random variables are "just" probability distributions on the reals which happen to be pushforwards of some distribution under some measurable map. The problem is the question of how to reason about such things...

[Adam Topaz]

BTW, I really like the sheaf theoretic point of view in the paper that @Reid Barton mentioned.

[Lars Ericson]

I am new to Lean, please forgive me if this question is naive or already has an answer.

Let $\Omega$ be a nonempty set, the sample space.

Let set $\mathcal F$ of subsets of $\Omega$ be a $\sigma$-algebra so that

• $\Omega \in \mathcal F$
• $\Omega \setminus F \in \mathcal F$ if $F \in \mathcal F$
• $\bigcup_{n=1}^{\infty} F_n \in \mathcal F$ if all $F_i \in \mathcal F$

Let $P: \mathcal F \rightarrow [0,1]$ be a probability measure so that

• $P(\Omega) = 1$
• $P(\Omega \setminus F) = 1-P(F)$
• $P(\bigcup_{n=1}^{\infty} F_n) = \sum_{n=1}^\infty P(F_n)$

Let's call the triple $S = (\Omega, \mathcal F, P)$ a probability space. Let's say $S$ has type $T$, $S: T$. How do I express $T$ in Lean?

[Kevin Buzzard]

You could make a probability_space structure. I've never really engaged with the measure theory library in Lean but it would not surprise me at all if a lot of these definitions are already there, for example I'm pretty sure measure spaces or measurable spaces are there

[Bryan Gin-ge Chen]

The docs for measure_theory.measure_space in mathlib (and other files in measure_theory) might be helpful.

[Adam Topaz]

docs#measure_theory.probability_measure is in mathlib, so it would be easy to create such structures with current mathlib

[Adam Topaz]

I would take a look at how, for example, docs#category_theory.bundled is defined and try to mimic (or even use?) that

[Lars Ericson]

Thanks for helping me think about this. I am coming to Lean with the hopes of being able to resolve some questions I posted on StackExchange over the last year or so, namely (in rough order of generality/complexity):

• What is the probability space of typical real univariate probability distributions?
• Extending the concept of distribution function to any totally or partially ordered measurable space
• Construction of the probability space of the Wiener process

Lean is the perfect fit for these questions. I'm a beginner to Lean so I will be working my way through the book and when I'm done with that I will try to transfer the above topics into a Lean setting.

These questions arose while I was reading KPS1994 which raises the notion of a probability space on page 3 and then quickly drops it in a constructive sense thereafter. If you read the comments in the StackExchange posts, most mathematicians don't seem to think it's really worth thinking about, i.e. that "probability space" is kind of a throwaway concept. I've been struggling with it for a year. I even went to the extent of trying to formalize the types in sympy. The result was very unsatisfying. Lean to the rescue! Probability space is actually a fairly slippery concept to pin down and almost everybody takes it for granted. I am looking forward to a satisfying solution in Lean.

Ultimately this will also involve having a proper representation of the real numbers as Dedekind cuts. I think this is already built in. A rigorous fundamental definition of the construction of reals is needed I think to provide a rigorous definition of things like probability measure. Some of that is already done in Lean but I think there is more to do.