Treatment Locality in A/B TestingResearch Paper
Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.
theorem TreatmentLocality.differentiable_estimator_variance_dominance_of_measurable
{S : Type*} [Fintype S] [DecidableEq S]
[MeasurableSpace S] [MeasurableSingletonClass S]
(M : Model S) (ν : Measure (Step S)) [IsProbabilityMeasure ν]
(hinv : Kernel.Invariant (expKernel M) ν)
(huni : MarkovChainCLT.UniformlyErgodic (expKernel M) ν)
(hL2 : M.RewardL2)
(f : EstInput S → ℝ) (hfm : Measurable f) (f' : EstInput S →L[ℝ] ℝ)
(hf : HasFDerivAt f f' (meanObs M .AB ν)) :
meanObs M .AB ν = meanObs M .IS ν
∧ (∀ Γ : Scheme, TendstoInDistribution
(fun (T : ℕ) (ω : ℕ → Step S) =>
Real.sqrt T * (f (empAvg M Γ T ω) - f (meanObs M .AB ν)))
atTop (id : ℝ → ℝ) (fun _ => MarkovChainCLT.chainMeasure (expKernel M) ν)
(gaussianReal 0
(MarkovChainCLT.asymptoticVariance (expKernel M) ν
(fun z => f' (estObs M Γ z))).toNNReal))
∧ lagCovMatrix M .AB ν = lagCovMatrix M .IS ν
∧ (∀ p q : EstIdx S, idxState p = M.crucial ∨ idxState q = M.crucial →
instCovMatrix M .AB ν p q = instCovMatrix M .IS ν p q)
∧ Matrix.PosSemidef (instCovMatrix M .AB ν - instCovMatrix M .IS ν)
∧ Matrix.PosSemidef (asymCovMatrix M .AB ν - asymCovMatrix M .IS ν) := by sorryTheorem 9 of arXiv:2407.19618, with the estimator required to be measurable.
Consider an SST model run under the mixed policy , with the experiment-tuple chain uniformly ergodic with stationary law and square-integrable rewards. Let for be a differentiable estimator: is Fréchet-differentiable at the mean statistics. Then:
- Same asymptotic bias — the mean statistics of the two schemes coincide, so both estimators are centred at the same limit value .
- Asymptotic normality — for each scheme, with the asymptotic variance of the linearized observable.
- Decomposition and dominance — writing : the temporal parts agree, ; the instantaneous parts agree on every row and column attached to the crucial state , so the variance at the treated state cannot be reduced; the difference is positive semidefinite; and consequently 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 . Fréchet-differentiability at the single point does not supply it: with non-measurable is differentiable at with derivative 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 as differentiable, and Appendix EC.3.2 uses " 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 .
Frontier · Open leaf nodes
No open leaves. Every sub-goal is proved or awaiting decomposition.
Recent activity
- ACCEPTEDLukeBerneseAug 21, 2026