Random variables

Stream: new members

[Matthew Ho]

Hi, just starting with Lean, and starting by formalizing some information theory-related objects. I was curious about if there's a design philosophy-related reason as to why random variables are not a type in Mathlib.Probability? My understanding is that the default right now is to create a function and add the assumption that it is measurable, but I would have thought the benefits of being able to do this in one clause with something like

(x: RandomVariable \Omega  S)

might be substantial if there are sufficiently many random variables.

Thanks!

[Etienne Marion]

Hi! Whenever you add a new definition you need to add some API with it to make it usable. Since working with measurable functions has worked well up to now there isn’t any reason why we would introduce a new type which would require duplicating a lot of stuff to build said API.

[Matthew Ho]

I see, makes sense--thanks!