Lebesgue conditional expectation

Stream: maths

[Yaël Dillies]

In our Gibbs measure project, @Kin Yau James Wong and I need the conditional expectation of functions that are naturally ENNReal-valued. Is there a specific reason) besides that the conditional expectation is naturally constructed through projections) that we only have the Bochner conditional expectation and not the Lebesgue one?

[Yaël Dillies]

We can achieve what we want by sticking a bunch of ENNReal.toReal everywhere, but it feels like API-fighting.

[Rémy Degenne]

I'd say the same reason as usual: nobody needed it so much that they took the time to do it.
I guess it makes sense to have an ENNReal version of this, like for other integral related definitions.

[Kexing Ying]

Are you working with functions which are almost surely finite? If not then I'd think you have some extra work in order to make sense of the conditional expectation for non-integrable functions (e.g. you'll need conditional MCT)

[Yaël Dillies]

Rémy, great that's what I wanted to hear. Any suggestion for the naming scheme? condexp and lcondexp?