Theorem 9 of arXiv:2407.19618, with the estimator required to be measurable.

Consider an SST model $M$ run under the mixed policy $\pi^{1/2}$, with the experiment-tuple chain uniformly ergodic with stationary law $\nu$ and square-integrable rewards. Let $\hat\Delta_\Gamma=f(K^t_\Gamma,K^c_\Gamma,R^t_\Gamma,R^c_\Gamma)$ for $\Gamma\in\{AB,IS\}$ be a differentiable estimator: $f$ is Fréchet-differentiable at the mean statistics. Then:

1. Same asymptotic bias — the mean statistics of the two schemes coincide, so both estimators are centred at the same limit value $f(\ell)$.
2. Asymptotic normality — for each scheme, $\sqrt T(\hat\Delta_\Gamma-f(\ell))\xrightarrow{d}N(0,\sigma_\Gamma^2)$ with $\sigma_\Gamma^2=\nabla f^\top\Sigma_\Gamma\nabla f$ the asymptotic variance of the linearized observable.
3. Decomposition and dominance — writing $\Sigma_\Gamma=\Sigma^{inst}_\Gamma+\Sigma^{cov}_\Gamma$: the temporal parts agree, $\Sigma^{cov}_{IS}=\Sigma^{cov}_{AB}$; the instantaneous parts agree on every row and column attached to the crucial state $s^1$, so the variance at the treated state cannot be reduced; the difference $\Sigma^{inst}_{AB}-\Sigma^{inst}_{IS}$ is positive semidefinite; and consequently $\Sigma_{IS}\preceq\Sigma_{AB}$ in the Loewner order.

Information sharing never increases the asymptotic variance of any differentiable estimator, and the entire reduction happens away from the treated state.

Why measurability appears. The asymptotic-normality clause asserts convergence in distribution, which in Mathlib carries an almost-everywhere measurability obligation on each $\omega\mapsto f(\text{empirical statistics}(\omega))$. Fréchet-differentiability at the single point $\ell$ does not supply it: $f(v)=\|v-\ell\|^2\mathbf 1_A(v)$ with $A$ non-measurable is differentiable at $\ell$ with derivative $0$ and measurable nowhere else, and the empirical statistics have a non-atomic law as soon as the rewards do. The paper's Definition 1 treats $f$ as differentiable, and Appendix EC.3.2 uses "$f$ is differentiable (and thus continuous)", so the hypothesis is present in the source and costs nothing; it is stated explicitly here because the formal conclusion needs it.

The measurability hypothesis is used only for the asymptotic-normality clause. The other four clauses are pure identities about the covariance structure of the two schemes and hold for an arbitrary $f$.