Stream: Is there code for X?

Topic: Conditional Expectation on Banach Spaces

Ata Keskin (Apr 25 2023 at 12:07):

Hi. Is there any formalization on conditional expectation in Banach Spaces? I am looking for something similar to this document in mathlib. I saw that we already have it for real valued functions, formalized by @Sebastien Gouezel, which uses the Radon-Nikodym derivative. However I believe this argument can't be used to construct conditional expectation in general Banach Spaces (at least not directly without having the Radon-Nikodym property and also a formalization of vector measures).

Sebastien Gouezel (Apr 26 2023 at 10:56):

My argument can be used to construct the conditional expectation of a characteristic function of a measurable set s (i.e., of the function equal to c on s and to 0 outside of s), even when c is in a Banach space: this is essentially a one-dimensional problem. However, to construct the general conditional expectation you would need to start from this and extend it by linearity to all simple functions, and then by density to all integrable functions. As far as I know, this has not been formalized in Isabelle yet (although it shouldn't be more complicated than the construction of Bochner integral).

Ata Keskin (Apr 26 2023 at 12:17):

I was first thinking of generalizing Lp spaces first to Bochner spaces (ie. Lp spaces of banach space valued functions) and then defining the conditional expectation of $f$ w.r.t the subalgebra $\mathcal{H}$ as the projection of $f$ onto the subspace $\mathcal{L}^p(\Omega, \mathcal{H}) \subset \mathcal{L}^p(\Omega)$ of $\mathcal{H}$-measurable functions.

When using the approach you suggested, I faced a problem in the density step:
Given a measure space $(\Omega, \mathcal{F}, \mu)$, the density of a function $f$ gives me a measure $\nu_f$, such that $\nu_f(A) = \int_A f \;d\mu$. However when $f$ is Banach valued, this does not make sense, since measures in Isabelle are always real valued. However, I think we can take the following approach:

Let $\nu_f$ be the density of the function $x \mapsto \lVert f(x) \rVert$. This way, we can define the conditional expectation as:

$$\text{cond\_exp} = \frac{f(x)}{\lVert f(x) \rVert} \cdot \frac{d\nu_f}{d\mu}$$

This way, we have:

$$\int_A \text{cond\_exp} \;d\mu = \int_A \frac{f(x)}{\lVert f(x) \rVert} \;d\nu_f = \int_A f(x) \cdot \frac{\lVert f(x) \rVert}{\lVert f(x) \rVert} \;d\mu = \int_A f \;d\mu$$

I think this should work, but I'd be really glad if you could confirm this. I am quite new to this area so I might be talking nonsense and I appreciate every feedback :smile:

Sebastien Gouezel (Apr 28 2023 at 12:14):

You should not need to use densities at all, since densities taking values in Banach are not well behaved in general. In the approach I outlined, you only use densities to define the conditional expectation of a rela-valued function. Then, for Banach space valued functions, this gives you the conditional expectation of characteristic functions (just multiply the real-valued characteristic function of your set with an element of your Banach space), then of simple functions (by linearity), and then you need to argue that this extends continuously to all L^1 functions, just as in the definition of the Bochner integral. These are the steps we have followed in Lean, and it works very well.

Your idea to project on L^2(\Omega, H) will not work out well unless H is a Hilbert space.

Ata Keskin (Apr 29 2023 at 14:33):

Sebastien Gouezel said:

You should not need to use densities at all, since densities taking values in Banach are not well behaved in general. In the approach I outlined, you only use densities to define the conditional expectation of a rela-valued function. Then, for Banach space valued functions, this gives you the conditional expectation of characteristic functions (just multiply the real-valued characteristic function of your set with an element of your Banach space), then of simple functions (by linearity), and then you need to argue that this extends continuously to all L^1 functions, just as in the definition of the Bochner integral. These are the steps we have followed in Lean, and it works very well.

Your idea to project on L^2(\Omega, H) will not work out well unless H is a Hilbert space.

I see. Thank you very much for your help and thorough explanation! :smile:

Last updated: May 06 2024 at 12:29 UTC