Stream: math-comp analysis

Topic: Subtyping for the Giry Monad

view this post on Zulip Markus de Medeiros (May 08 2024 at 15:53):

Hello, I'm working on porting the construction of the Giry monad from mathlib to mathcomp-analysis, and I'm running into a hierarchy issue when I try to apply it to probability spaces which I'm not sure how to best solve.

So far I've managed to put a measurableType on measure T R by following the usual construction (generate a sigma algebra out of the preimage of every evaluation map). Overall this lets me definegiryM T : measurableType ..., so I can express types like giryM (giryM T). This seems to be enough to define all of the monad operations I'd want to use (though I haven't actually proven any of the laws yet : )).

Now I'm trying to also support the Giry monad on subprobability T R and probability T R. Ultimately this should just amount to restricting the space of measures I take the preimage into when doing the construction, however, I can't figure out how to express this in a way that will leave me with measurableTypes for subprobability and probability (this is necessary to express eg. the monadic join).

I believe the core issue is that I'm trying to turn a sigma-algebra of a parent type into a measurableType of a subtype-- has this issue come up before? Any help appreciated :)

view this post on Zulip Reynald Affeldt (May 08 2024 at 21:41):

There is pr 1177 on a related topic.

view this post on Zulip Markus de Medeiros (May 09 2024 at 11:17):

Oh great-- I wasn't aware of this. Thanks!

Last updated: Jun 22 2024 at 15:01 UTC