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 define`giryM 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 `measurableType`

s 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 :)

There is pr 1177 on a related topic.

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

Last updated: Jun 22 2024 at 15:01 UTC