Proof of Splitting of the Observation Record Space at an Intermediate Time

Cells of the record spaces are written $C^a_\emptyset$ and $C^a_{k,v}$ for the horizon $a$; for $k\ge1$ the cell $C^a_{k,v}$ carries, by The Observation Record Space, the transport along $t\mapsto(k,t,v)$ of the restriction of $(\mathbb{R}^k,\mathcal{B}_k,\lambda_k)$ to the ordered time simplex $D_k(a)$, and $C^a_\emptyset$ carries the one-point measure space structure.

Claim 1. Let $r=(k,t,v)\in\mathbf{R}_T$ and $\kappa=k_r(s)$. If $\kappa\ge1$ then $0<t_1<\dots<t_\kappa\le s$, so the prefix times lie in $D_\kappa(s)$ and the marks in $\{1,\dots,\tilde{l}\}^\kappa$; for $\kappa=0$ the prefix is the empty record. Hence $\pi_s(r)\in\mathbf{R}_s$. If $k-\kappa\ge1$ then $t_{\kappa+1}>s$ by the definition of $\kappa$, so $0<t_{\kappa+1}-s<\dots<t_k-s\le T-s$ and $\iota_s(r)\in\mathbf{R}_{T-s}$. For $\varrho=(\kappa,\tau,w)\in\mathbf{R}_s$ and $r'=(k',t',v')\in\mathbf{R}_{T-s}$: when the respective blocks are nonempty, $\tau_\kappa\le s<s+t'_1$ and $s+t'_{k'}\le T$, so the concatenated time tuple is strictly increasing with entries in $(0,T]$, and $\varrho\oplus_s r'\in\mathbf{R}_T$. Exactly the first $\kappa$ concatenated times are at most $s$, so $k_{\varrho\oplus_s r'}(s)=\kappa$, whence $\pi_s(\varrho\oplus_s r')=\varrho$ and $\iota_s(\varrho\oplus_s r')=r'$; conversely, for every $r\in\mathbf{R}_T$ the definitions give $\pi_s(r)\oplus_s\iota_s(r)=r$ directly. Thus $\oplus_s$ is a bijection with the asserted inverse.

Claim 2. The products $C\times C'$ of a cell of $\mathbf{R}_s$ and a cell of $\mathbf{R}_{T-s}$ form a countable partition of $\mathbf{R}_s\times\mathbf{R}_{T-s}$; each product of a member of a cell $\sigma$-algebra with a member of a cell $\sigma$-algebra lies in $\mathcal{R}_s\otimes\mathcal{R}_{T-s}$, since cell-measurable sets are measurable in the disjoint union by claim 4(a) of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions and the product $\sigma$-algebra contains products of measurable sets. A preimage under $\oplus_s$ is the countable union of the preimages under its restrictions to the sets $C\times C'$, so it suffices to show each restricted preimage is measurable.

Fix $C=C^s_{\kappa,w}$ and $C'=C^{T-s}_{k',v'}$ with $\kappa,k'\ge1$ (when a block is empty the same argument applies with that block omitted; the restriction to $C^s_\emptyset\times C^{T-s}_\emptyset$ is constant, hence measurable). The restriction of $\oplus_s$ maps $C\times C'$ into $C^T_{\kappa+k',(w,v')}$. Let $B\in\mathcal{R}_T$; by claims 1 and 2 of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions, $B\cap C^T_{\kappa+k',(w,v')}$ corresponds under the transport to a set $\tilde{B}\in\mathcal{B}_{\kappa+k'}$ with $\tilde{B}\subseteq D_{\kappa+k'}(T)$. Under the transports of $C$ and $C'$, the restricted preimage of $B$ corresponds to the preimage of $\tilde{B}$ under $\varphi(\tau,t')=(\tau,\ s+t')$ on $D_\kappa(s)\times D_{k'}(T-s)$. Identifying $\mathbb{R}^\kappa\times\mathbb{R}^{k'}$ with $\mathbb{R}^{\kappa+k'}$ elementwise, the $\sigma$-algebras $\mathcal{B}_\kappa\otimes\mathcal{B}_{k'}$ and $\mathcal{B}_{\kappa+k'}$ coincide: both are generated by the rectangles with Borel sides, by claim 2 of Finite Products of Lebesgue Measure and Coordinate Integration on $\mathbb{R}^l$. For such a rectangle $A_1\times\dots\times A_{\kappa+k'}$, $\varphi^{-1}\bigl(A_1\times\dots\times A_{\kappa+k'}\bigr)=\Bigl(\prod_{j\le\kappa}A_j\times\prod_{j>\kappa}(A_j-s)\Bigr)\cap\bigl(D_\kappa(s)\times D_{k'}(T-s)\bigr),$ and each translate $A_j-s$ is Borel by Translation Invariance of Lebesgue Measure and the Lebesgue Integral. Rectangles generate, and preimages preserve countable set operations, so $\varphi$ is measurable by the generator criterion of Measurable Function and Real-Valued Measurable Function, and the restricted preimage of $B$ lies in the transported product structure, hence in $\mathcal{R}_s\otimes\mathcal{R}_{T-s}$. Summing over the cell pairs proves the measurability of $\oplus_s$.

For $\pi_s$ and $\iota_s$: fix a cell $C^T_{k,v}$ with $k\ge1$ and, for $\kappa\in\{0,\dots,k\}$, let $E_\kappa\subseteq C^T_{k,v}$ be the set of its records with exactly $\kappa$ event times at most $s$; under the transport, $E_\kappa$ corresponds to the set of $t\in D_k(T)$ with $t_\kappa\le s<t_{\kappa+1}$ (the first constraint absent for $\kappa=0$, the second for $\kappa=k$), which is a finite intersection of preimages of Borel rectangles, hence Borel. The sets $E_0,\dots,E_k$ partition $C^T_{k,v}$. On $E_\kappa$, the map $\pi_s$ takes values in the cell $C^s_{\kappa,(v_1,\dots,v_\kappa)}$ and corresponds to $(t_1,\dots,t_k)\mapsto(t_1,\dots,t_\kappa)$, and $\iota_s$ takes values in $C^{T-s}_{k-\kappa,(v_{\kappa+1},\dots,v_k)}$ and corresponds to $(t_1,\dots,t_k)\mapsto(t_{\kappa+1}-s,\dots,t_k-s)$, in each case followed by the respective transports, measurability into the disjoint unions being checked cell by cell by claim 4(b) of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions; preimages of Borel rectangles under these maps are Borel rectangles crossed with full coordinate lines, translated in the second case (Translation Invariance of Lebesgue Measure and the Lebesgue Integral), intersected with $E_\kappa$. So both restrictions are measurable, and countable unions over $\kappa$ and the cells (the cell $C^T_\emptyset$ mapping constantly to the empty records) complete claim 2.

Claim 3. Both $\rho_s\otimes\rho_{T-s}$ and $\rho_T$ are finite measures. Let $B\in\mathcal{R}_T$. By countable additivity over the partition of claim 2, $(\rho_s\otimes\rho_{T-s})\bigl((\oplus_s)^{-1}(B)\bigr)=\sum_{C,C'}(\rho_s\otimes\rho_{T-s})\bigl((\oplus_s)^{-1}(B)\cap(C\times C')\bigr).$ Fix $C=C^s_{\kappa,w}$ and $C'=C^{T-s}_{k',v'}$ and let $\tilde{B}\in\mathcal{B}_{\kappa+k'}$ correspond to $B\cap C^T_{\kappa+k',(w,v')}$ as in claim 2. By the Tonelli theorem for the product measure and the restriction and transport identities of claims 1, 2, and 4(a) of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions, $(\rho_s\otimes\rho_{T-s})\bigl((\oplus_s)^{-1}(B)\cap(C\times C')\bigr)=\int_{\mathbb{R}^{\kappa}}\mathbf{1}_{D_\kappa(s)}(\tau)\Bigl(\int_{\mathbb{R}^{k'}}\mathbf{1}_{D_{k'}(T-s)}(t')\,\mathbf{1}_{\tilde{B}}(\tau,\ s+t')\,d\lambda_{k'}(t')\Bigr)d\lambda_{\kappa}(\tau).$ Writing the inner integral as an iterated integral over the $k'$ coordinates by claim 3 of Finite Products of Lebesgue Measure and Coordinate Integration on $\mathbb{R}^l$ and applying Translation Invariance of Lebesgue Measure and the Lebesgue Integral in each coordinate, it equals $\int_{\mathbb{R}^{k'}}\mathbf{1}_{\tilde{B}}(\tau,u')\,\mathbf{1}_{\{u':\ s<u'_1<\dots<u'_{k'}\le T\}}(u')\,d\lambda_{k'}(u')$. Reassembling the two blocks by Tonelli and claim 3 of Finite Products of Lebesgue Measure and Coordinate Integration on $\mathbb{R}^l$, the summand equals $\lambda_{\kappa+k'}(\tilde{B}\cap F_\kappa)$, where $F_\kappa\subseteq D_{\kappa+k'}(T)$ is the Borel set of tuples with exactly $\kappa$ coordinates at most $s$. For a fixed target cell $C^T_{k,v}$, as $\kappa$ runs over $\{0,\dots,k\}$ with $k'=k-\kappa$ and the mark split of $v$ determined by $\kappa$, the sets $F_\kappa$ partition $D_k(T)$, so by additivity the summands with target cell $C^T_{k,v}$ sum to $\lambda_k$ of the transported $B\cap C^T_{k,v}$, which is $\rho_T(B\cap C^T_{k,v})$ by claims 1, 2, and 4(a) of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions; the empty-record cell contributes $\rho_T(B\cap C^T_\emptyset)$ directly, both sides being the unit mass or zero; and in the mixed cell pairs with exactly one empty block, the factor for the empty block is the unit mass of the one-point measure space (claim 3 of Assembly of Measure Spaces: Restriction, Transport, One-Point Spaces, and Countable Disjoint Unions) and the same computation applies to the remaining block. Summing over the countably many cells gives $(\rho_s\otimes\rho_{T-s})((\oplus_s)^{-1}(B))=\rho_T(B)$, which is the asserted image-measure identity. The displayed integral identity follows by the integration identity for image measures in Image Measures, Measures with Densities, and Change of Variables applied to $\oplus_s$, followed by the Tonelli theorem for the iterated form.