There is a definition that has always left nagging questions in my mind. To set it up, let $(\Omega, \cal{A}, (\cal{F}_t)_{t\geq 0}, P)$ be a filtered probability space. From Comets & Meyre's *Calcul stochastique et modèles de diffusions*,

**Definition 3.2.** A real-valued function $\phi$ on $\mathbb{R}^+\times \Omega$ is *progressively measurable* if, for all $t\in \mathbb{R}^+$, the mapping $(s,\omega) \mapsto \phi(s, \omega)$ on $[0, t]\times \Omega$ is $\cal{B}[0,t] \otimes \cal{F}_t$-measurable.

Clear enough. The authors go on to define $M^2(\mathbb{R}^+)$ to define the set (space) of all progressively measurable stochastic processes $\phi$ such that

$\mathbf{E}\int_{\mathbb{R}^+} \phi^2(t, \omega) dt < \infty$.

(This formula is verbatim from the book.)

My question is: does one simply interpret the expression on the left as a double integral à la the Fubini-Tonelli theorem, $\int_\Omega\int_{R^+} \ldots dt dP$, and if so, does progressive measurability ensure that $\phi$ is $\cal{B}(\mathbb{R}^+)\otimes \cal{A}$ measurable, so that this interpretation makes sense?

My attempts to realize $\phi$ as the limit of a sequence of measurable functions (like $\phi|_{[0, n]\times\Omega}$) have yielded nothing to convince me yet.