Markus de Medeiros (May 08 2024 at 15:53): 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 :)
Reynald Affeldt (May 08 2024 at 21:41):There is pr 1177 on a related topic.
Markus de Medeiros (May 09 2024 at 11:17):Oh great-- I wasn't aware of this. Thanks!
Last updated: Oct 13 2024 at 01:02 UTC