condexp as a map between L¹s

Stream: mathlib4

[Yury G. Kudryashov]

Do we have conditional expectation as a map between L¹ spaces w.r.t. different σ-algebras? Or as a self-map with a property that the result is a.e.-measurable w.r.t. the other σ-algebra?

[Rémy Degenne]

There is this: docs#MeasureTheory.condexpL1Clm , with docs#MeasureTheory.aestronglyMeasurable'_condexpL1Clm

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

What are the right assumptions to have this in L^p?

[Yury G. Kudryashov]

(p > 1)

[Rémy Degenne]

For p = 2 we have docs#MeasureTheory.condexpL2 (we build it first in L2, then extend to L1). We don't have anything already made for other p.

If your measure is finite then for any p > 1 Lp is a subset of L1, which means that the conditional expectation is well defined on Lp. The image of a Lp function is also in Lp by Jensen's inequality for the function ||.||^p (we don't have Jensen's inequality for condexp).

In "Analysis in Banach spaces (volume 1)", lemma 2.6.30, they have it for a sigma-finite measure instead of finite, but their conditional expectation is defined slightly more generally than ours: they use sigma-integrable functions, while ours is meaningful only for integrable functions. I did not add the notion of sigma-integrability to mathlib.

[Yury G. Kudryashov]

Thank you for the explanation!