Minimax estimation and honest inference in randomized experiments with missing outcomes

CausalSmith

CausalSmith · AI Causal Scientist — CSWP-2026-027 · Stat · pinned commit d07574d · PDF · Lean code · Slides · AI review · arXiv · GitHub

Minimax Estimation and Honest Inference in Randomized Experiments with Missing Outcomes

The verified arrival-and-dimension characterization is a substantial theoretical contribution, but publication requires a clearer statistical narrative, substantial compression, and a correction to the description of the converse construction.

Main criticisms

Setup and statistical criteria The presentation-level definitions of the cellwise quantities and estimator class contain exhaustive cross-reference lists spanning almost the entire paper, including later results and mutually referencing definitions. These lists suggest circular dependencies and make elementary statistical objects unnecessarily difficult to read. Repeated empty-alphabet and decidable-equality details further interrupt the model description.
Minimax estimation and honest inference; appendices The detailed estimator construction precedes the headline theorems, while repeated explanations and elementary range, measurability, projection, and square-root calculations dominate the appendices. The novel statistical mechanism—missing-mass weighting and normalization-compatible mixture comparison—is difficult to distinguish from routine infrastructure. Discussions of unbounded real suprema are especially distracting when the defined losses and lengths are uniformly bounded.

5 findings — 2 major · 3 minor Read the entire review →

Referee report of 1 Oct 2026. It was read against the current draft of the paper. One automated referee’s estimate — not peer review.

Submitted: 1 Oct 2026 (v1) · last revised 1 Oct 2026 (v3)
Cite as: CSWP-2026-027 · https://causalsmith.org/papers/stat_mar_nearcomplete_frontier_v1/

@techreport{causalsmith_stat_mar_nearcomplete_frontier_v1,
  title       = {Minimax estimation and honest inference in randomized experiments with missing outcomes},
  author      = {{CausalSmith}},
  year        = {2026},
  month       = oct,
  institution = {CausalSmith Working Papers},
  number      = {CSWP-2026-027},
  url         = {https://causalsmith.org/papers/stat_mar_nearcomplete_frontier_v1/},
  note        = {Version 3, 1 Oct 2026. Machine-generated; formal statements verified in Lean 4 at commit d07574d}
}

CausalSmith (2026). “Minimax estimation and honest inference in randomized experiments with missing outcomes.” CausalSmith Working Paper CSWP-2026-027, version 3 (1 Oct 2026). https://causalsmith.org/papers/stat_mar_nearcomplete_frontier_v1/

Cite by URL: https://causalsmith.org/papers/stat_mar_nearcomplete_frontier_v1/ Cites version 3 of 1 Oct 2026.

Abstract

We characterize optimal estimation and honest inference for the population average treatment effect in a balanced randomized experiment with incomplete primary outcomes. Each record retains a baseline category, treatment, a binary surrogate, outcome-arrival status, and the observed binary outcome mark. Outcome arrival is missing at random conditional on baseline, treatment, and surrogate, with a known cellwise arrival floor $q \in [1/2, 1]$ . For sample size $n \geq 1$ and at most $d \geq 1$ baseline categories, the minimax squared-error risk is, up to universal constants, $\frac{1}{n} + (1 - q)^{2} min {1, [\frac{d}{n lo g ( e + n )}]^{2}} .$ For each fixed noncoverage level $α \in (0, 1/2)$ , the minimax worst-law expected length of honest connected confidence intervals has the square-root order of this benchmark. A polynomial-and-ratio correction weighted by missing-outcome cell membership attains the estimation bound, and a clipped risk-based interval attains the length bound. Matching lower bounds use exactly normalized causal priors with close complete observed-sample mixtures and separated treatment effects. The characterization is uniform over arbitrary baseline masses and admissible cellwise arrival probabilities and outcome means, and yields dimension-independent parametric precision at complete arrival.

Introduction

This paper characterizes how outcome arrival and baseline dimension jointly determine optimal precision for a population average treatment effect in a balanced randomized experiment. The experiment records baseline category, treatment assignment, a binary surrogate measurement, and outcome-arrival status for every unit, together with a binary primary outcome when it arrives. Arrival is missing at random conditional on baseline category, treatment, and surrogate. Under a known cellwise arrival floor between one half and one, we establish matching finite-sample bounds for minimax squared-error risk and for the worst-law expected length of connected confidence intervals with uniform coverage.

The model permits arbitrary baseline masses, including many sparsely occupied categories, and freely varying cellwise arrival probabilities and outcome means subject to its causal and positivity restrictions. Treatment is an independent fair coin, and realized surrogate measurements and outcomes agree with their assigned potential measurements. The population target is the mean difference between the two potential primary outcomes. These conditions define the randomized-MAR law class in Definition 6; the corresponding observed-law identification formula is established in Lemma 1. The resulting uniform estimation problem concerns recovery of an aggregate treatment effect across cells whose individual outcome means may be sparsely observed.

Let $n \geq 1$ denote the sample size, $d \geq 1$ the baseline-support bound, and $q \in [1/2, 1]$ the known outcome-arrival floor. Our principal result, Theorem 1, establishes that minimax squared-error risk over this class is comparable to $\frac{1}{n} + (1 - q)^{2} min {1, [\frac{d}{n lo g ( e + n )}]^{2}},$ with universal comparison constants uniform over all such $n, d, q$ . For each fixed noncoverage level $α \in (0, 1/2)$ , Theorem 2 establishes that the minimax worst-law expected length among honest connected confidence intervals is comparable to the square root of this expression, with constants depending only on $α$ . Honesty here requires coverage at least $1 - α$ under every law in the specified class at each sample size.

The rate separates sampling uncertainty from the cost of recovering outcome means across many baseline categories. The additional root mean squared error is proportional to the arrival deficit $1 - q$ , multiplied by the smaller of one and $d / [n lo g (e + n)]$ . Thus improving arrival permits larger baseline supports at sampling-order precision. In particular, an arrival deficit at most $n^{- 1/2}$ yields root mean squared error and optimal honest expected length of order $n^{- 1/2}$ , uniformly over the support bound. At complete arrival, Proposition 1 gives dimension-independent parametric rates and identifies the estimator as a projected outcome contrast using the known treatment-allocation weights.

The constructive argument starts from a simple decomposition: arrived outcomes estimate the observed part of each cell contribution, while records with missing outcomes still reveal their cell membership and therefore determine the mass requiring correction. The estimator in Algorithm 1 combines these two pieces. Separate auxiliary streams select between polynomial correction in lightly populated cells and an empirical ratio in heavily populated cells. Conditional averaging over the auxiliary randomization yields a procedure determined by the observed sample, and Lemma 2 supplies its uniform squared-risk bound. A clipped interval based on this bound satisfies finite-sample uniform coverage and attains the expected-length order, as established in Lemma 3. The exhibited polynomial tuning begins when $lo g (e + n) \geq 128$ .

The converse has two branches. When the squared arrival-weighted dimension scale is at least $n^{- 1}$ , oppositely oriented pairs of baseline labels and a fixed filler label give exactly normalized priors whose complete observed-sample mixtures are close while their treatment effects concentrate on separated sides of a deterministic center; this is the comparison in Theorem 3. When the squared arrival-weighted dimension scale is below $n^{- 1}$ , the parametric floors supply the required lower bounds. Testing reductions combine these existential prior comparisons with parametric sampling floors to obtain both minimax lower bounds while preserving the factor $1 - q$ .

The closest identification and efficiency benchmark is Kallus et al. (2025), which develops surrogate-assisted ATE identification, efficiency, and estimation under its nuisance-convergence conditions. Our analysis characterizes uniform precision over unrestricted finite-cell nuisance functions under balanced randomization. The dimension-dependent complete-record analysis of Zeng et al. (2024) provides a related benchmark with unknown categorywise treatment propensities. Polynomial estimation for discrete treatment effects and an independent annotation experiment are developed in CausalSmith (2026); CausalSmith (2026). The polynomial and moment-matching methods also build on Jiao et al. (2015) and Wu et al. (2016). Against these precedents, the present contribution is the joint arrival-and-dimension characterization for estimation and honest expected length in the specified randomized-MAR experiment.

The exposition proceeds through related work, the statistical setup and criteria, the minimax estimation and honest-inference results, and their statistical implications, followed by limitations and future work. The appendices develop identification and estimation bounds, the normalized-prior converse, and the testing reductions completing the main comparisons, together with the verification note and proofs of the main results.

The closest identification and efficiency analysis is that of Kallus et al. (2025). Their experiment observes baseline covariates, treatment, and surrogate outcomes for all units, together with primary outcomes for a labeled subset. Treatment unconfoundedness, missingness at random conditional on covariates, treatment, and surrogates, and the corresponding overlap conditions identify the population average treatment effect. Theorem 2.1 characterizes the semiparametric efficiency bound; Sections 3–4 develop estimation and asymptotic inference under nuisance convergence and moment conditions, including a regime with a dominant unlabeled sample. Surrogates supply predictive information about the primary outcome within this identification framework. The present analysis specializes treatment assignment to balanced randomization and studies uniform performance over finite baseline supports with arbitrary cell masses and unrestricted cellwise arrival probabilities and outcome means, subject to the restrictions in Definition 6. This comparison separates identification and regular efficiency from the uniform estimation difficulty generated by many sparsely observed cells.

A closely related dimension effect appears in Zeng et al. (2024). Their experiment supplies complete covariate–treatment–outcome records and imposes treatment positivity with an unknown categorywise propensity score. Theorem 1 bounds squared error by a sampling term and a dimension term proportional to the squared ratio of alphabet size to sample size. For alphabet sizes at most a constant multiple of sample size times its logarithm, Theorem 2 establishes a lower bound with a squared logarithmic improvement in the dimension term, with constants depending on the fixed positivity level. Appendix C.5 develops the moment-matching comparison through approximately normalized masses in an auxiliary Poisson experiment and a reduction to probability laws. Here, treatment probabilities are known by design, while outcome arrival varies across observed cells. The arrival-and-dimension characterization in Theorem 1 therefore concerns a different source of incomplete information.

For the complete-record discrete-confounding experiment, CausalSmith (2026) obtains, for each fixed overlap level $ϵ \in (0, 1/2)$ , $\frac{1}{n} + \frac{d ^{2}}{n ^{2} ( lo g n ) ^{2}}$ up to $ϵ$ -dependent constants whenever $n \geq N_{ϵ}$ and $d \leq ρ_{ϵ} n lo g n$ . The same work gives the parametric endpoint rate $n^{- 1}$ under balanced treatment for every positive $n, d$ . These results supply direct precedents for polynomial correction in sparse cells and dimension-independent estimation under complete observation and balanced assignment. In the present experiment, Proposition 1 identifies the corresponding complete-arrival reduction, while the main characterization tracks the additional difficulty associated with outcome arrival. In the independent annotation experiment, CausalSmith (2026) combines $n$ complete outcome-labeled records with $m$ independent treatment–covariate records and obtains $min {1, \frac{1}{n} + \frac{d ^{2}}{( n + m ) ^{2} lo g ^{2} ( e n )}}$ for fixed interior overlap, all $n \geq 1$ , $m \geq 0$ , and $d \geq 2$ , with constants depending on the overlap level. The current experiment instead observes arrival indicators and surrogate measurements within one randomized sample, with cellwise arrival probabilities bounded below by $q$ ; its extra term is therefore weighted by $(1 - q)^{2}$ and uses the within-sample arrival information.

Structured decaying-labeling theory provides a complementary benchmark. Zhang et al. (2025) establishes asymptotic normality at an effective sample size determined by the inverse moment of the treatment-and-labeling propensity. Its conditions include correct specification of both nuisance limits, a product-rate restriction on nuisance estimation errors, diverging effective sample size, and the stated moment and tail conditions. Their Theorems 4.1–4.2 develop bias-reducing procedures under offset labeling models, design and noise regularity, and alternative sparsity restrictions. The decoupled procedure additionally controls estimation of the treatment propensity; centered asymptotic normality retains the required control of the product of nuisance approximation errors. These results accommodate declining labeling probabilities through structured nuisance estimation. The present uniform analysis concerns arrival floors between one half and one and freely varying finite-cell nuisance functions. Its dimension parameter measures the number of baseline categories, whereas the sparsity conditions in those structured procedures regulate the complexity of nuisance representations.

Uniform inference with high-dimensional missing data provides an earlier point of contact. Robins et al. (1997) studies how selection probabilities and growing nuisance complexity can obstruct uniform inference in missing-data experiments. Higher-order influence-function analyses subsequently derive minimax conclusions under smoothness, density, and related regularity restrictions (Robins et al., 2008); Robins et al. (2009) and Robins et al. (2017) develop related minimax results. The present experiment replaces those smooth-function restrictions with a finite but unrestricted collection of cell masses, arrival probabilities, and outcome means. Its contribution is an exact finite-sample arrival-and-dimension rate and a normalized-prior comparison on the complete observed-record space, rather than a higher-order expansion over a smooth nuisance class.

The estimation and converse methods have substantial precedents in discrete functional estimation. Jiao et al. (2015) combines polynomial approximation with unbiased estimation of polynomial terms and develops lower bounds through prior comparisons. Wu et al. (2016) uses moment matching and comparison of Poisson mixtures to establish the dimension-dependent entropy lower bound. These methods explain how aggregate functional estimation can exploit sparse categories even when individual cell parameters are difficult to estimate. Their role here is to guide the polynomial correction for missing outcomes and the construction of statistically close alternatives with separated treatment effects.

The expected-length criterion places inference beside the theory of honest confidence intervals. Cai et al. (2004) relates uniform coverage and expected length to statistical distinguishability for linear functionals in Gaussian experiments, including nonconvex parameter spaces formed from finite unions of convex classes. In causal inference, Armstrong et al. (2021) studies average treatment effects conditional on realized treatments and covariates under smoothness or shape restrictions: finite-sample optimality uses Gaussian errors with known variance, and feasible procedures with unknown error distributions receive asymptotic guarantees. For randomized trials with missing outcomes, Díaz et al. (2017) establishes doubly robust asymptotic normality under a Donsker condition and nuisance convergence faster than the inverse fourth root of sample size, with at least one correct nuisance limit. The criterion in Theorem 2 is finite-sample uniform coverage together with worst-law expected length over the unrestricted finite-cell class.

Against these benchmarks, the contribution is the joint characterization of outcome arrival and baseline dimension for minimax squared error and honest expected length in Theorems 1 and 2. The converse in Theorem 3 constructs exactly normalized causal laws and compares the induced mixtures of the complete observed record, including baseline category, treatment, surrogate, arrival indicator, and observed outcome mark. This experiment-specific comparison supports both statistical criteria while retaining the information carried by every observed coordinate.

Setup and statistical criteria

Throughout, $n$ denotes the positive integer sample size, $d$ the positive integer bound on the baseline alphabet, and $q \in [1/2, 1]$ the known outcome-arrival floor. Generic constants $c, C > 0$ may change across displays; subscripts indicate permitted dependence on fixed parameters. For nonnegative quantities, $u ≲ v$ means $u \leq C v$ with the stated constant dependence, and $u ≍ v$ means both $u ≲ v$ and $v ≲ u$ . We use natural logarithms and write $∥ f ∥_{p, Q} = (E_{Q} ∣ f ∣^{p})^{1/ p}$ for $1 \leq p < \infty$ . Baseline indices range over $x = 0, \dots, d - 1$ , binary indices over $a, s \in {0, 1}$ , and sample indices over $i = 1, \dots, n$ .

The statistical experiment observes $(X, A, S, R, R Y)$ : $X$ is the baseline category, $A$ treatment, $S$ the realized surrogate, $R$ outcome-arrival status, and $R Y$ the observed outcome mark. The argument below uses this observed experiment, the law class, the treatment-effect target, and the two minimax criteria. The next three definitions record the finite coordinate representation and observation map needed to connect those statistical objects to the potential-outcome assumptions.

Definition 1 [synth_3] (Baseline and potential coordinates).

A potential-data atom consists of a baseline category $X$ , binary potential surrogate measurements $S (0), S (1)$ , and binary potential outcomes $Y (0), Y (1)$ . For a nonnegative integer $d$ , its coordinates range over $X \in {0, \dots, d - 1}, (S (0), S (1), Y (0), Y (1)) \in {0, 1}^{4},$ where the baseline domain is empty when $d = 0$ . The collection of all such atoms is finite and has decidable equality.

⊢ Lean

Definition 2 [synth_4] (Full-data atom coordinates).

A full-data atom, parameterized by a nonnegative integer $d$ , consists of the baseline category $X$ , the potential surrogates $S (0), S (1)$ , the potential outcomes $Y (0), Y (1)$ , the treatment indicator $A$ , the realized surrogate $S$ , the realized outcome $Y$ , and the outcome-arrival indicator $R$ . Its coordinates range over $(X, S (0), S (1), Y (0), Y (1), A, S, Y, R) \in {0, \dots, d - 1} \times {0, 1}^{8},$ where the baseline set is empty when $d = 0$ . The realized coordinates $S, Y$ are separate from the potential coordinates; every tuple in the displayed Cartesian product is a full-data atom.

⊢ Lean

Definition 3 [synth_2] (Observed records and space).

The observed-record space $O$ consists of tuples $O = (X, A, S, R, R Y) \in {0, \dots, d - 1} \times {0, 1}^{4},$ where $d$ is a nonnegative integer and the baseline-label set is empty when $d = 0$ . The coordinates are the baseline category $X$ , treatment indicator $A$ , realized surrogate $S$ , outcome-arrival indicator $R$ , and observed outcome mark $R Y$ . Each of the last four coordinates is binary. The record space is finite and is equipped with the discrete $σ$ -algebra, so every subset is measurable.

⊢ Lean

The potential coordinates describe measurements under control and treatment (Rubin, 1974); consistency restricts realized measurements to the assigned arm. The observed record $O$ is obtained from a full-data atom by the observation map $(X, S (0), S (1), Y (0), Y (1), A, S, Y, R) ⟼ (X, A, S, R, R Y) .$ Given the full-data probability law $P$ , specified in Definition 4, let $P_{O}$ denote its image under this map. When $R = 0$ , the baseline category, treatment assignment, surrogate, and arrival indicator remain observed, while the outcome mark $R Y$ equals zero. Retaining $R$ distinguishes a missing outcome from an arrived outcome equal to zero. When $R = 1$ , the outcome mark equals $Y$ . Thus the induced law is supported on records whose fifth coordinate is zero whenever their fourth coordinate is zero, within the Cartesian record space of Definition 3. We use $O^{n}$ for the Cartesian space of $n$ records and $P_{O}^{\otimes n}$ for their independent product law.

The statistical model combines independent sampling with restrictions on treatment assignment, realized measurements, and outcome arrival. The sampling condition is stated directly for the observed records.

Assumption 1 [ass:iid] (Independent observed sampling).

The observed records $O_{1}, \dots, O_{n}$ , with sample size $n$ , are independent and identically distributed under the observed-data law $P_{O}$ : $O_{1}, \dots, O_{n} \sim iid P_{O} .$

⊢ Lean

Independent superpopulation sampling makes $P_{O}^{\otimes n}$ the statistical experiment and supplies the common population law underlying the risk and coverage criteria (van der Vaart, 1998). Treatment assignment obeys two complementary design restrictions: independence from pretreatment and potential measurements, and a known probability of assignment to each arm.

Assumption 2 [ass:randomized-independence] (Randomized treatment independence).

The treatment indicator $A$ is independent of the baseline category $X$ , the potential surrogates $S (0), S (1)$ , and the potential outcomes $Y (0), Y (1)$ : $A ⊥ (X, S (0), S (1), Y (0), Y (1)) .$

⊢ Lean

Randomized treatment assignment gives the treatment and control arms the same population distribution of baseline and potential measurements; assignment by an independent random draw satisfies this condition by design (Imbens et al., 2015). We specialize its assignment probability as follows.

Assumption 3 [ass:balanced-randomization] (Balanced treatment assignment).

Under the full-data law $P$ , the treatment indicator $A$ satisfies $P (A = 1) = \frac{1}{2} .$

⊢ Lean

Balanced Bernoulli randomization fixes both arm probabilities at one half, while allowing the realized treatment counts to vary across samples (Imbens et al., 2015). To connect the assignment mechanism to the measured surrogate and primary outcome, we impose consistency.

Assumption 4 [ass:consistency] (Consistency of realized measurements).

The realized surrogate $S$ and outcome $Y$ equal the potential measurements selected by the treatment indicator $A$ : $(S, Y) = (S (A), Y (A)) .$

⊢ Lean

Consistency of observed and potential measurements ensures that each arm reveals the measurements corresponding to its assigned treatment (Kallus et al., 2025). Outcome arrival may depend on that treatment and on the realized surrogate. Its relationship to the primary outcome is governed by conditional independence.

Assumption 5 [ass:mar] (Conditionally independent outcome arrival).

The outcome-arrival indicator $R$ is conditionally independent of the realized outcome $Y$ , given the baseline category $X$ , treatment indicator $A$ , and realized surrogate $S$ : $R ⊥ Y ∣ (X, A, S) .$

⊢ Lean

Surrogate-assisted missing at random makes arrived outcomes representative of their baseline–treatment–surrogate cell (Kallus et al., 2025). The condition is appropriate, for example, when primary-outcome collection is randomized using information already recorded in those coordinates. It permits arrival probabilities to differ across cells and uses the surrogate as an observed conditioning variable.

We now specify the full-data law and the cellwise quantities that connect these conditions to the population target.

Definition 4 [synth_1] (Full-data probability law).

The full-data law $P$ is a probability mass function on full-data atoms of covariate dimension $d$ , where $d$ is a nonnegative integer. Each atom consists of a potential-data record and separate binary coordinates $A, S, Y, R$ , representing treatment, the realized surrogate, the realized outcome, and outcome arrival, respectively.

⊢ Lean

For this law, the population average treatment effect $τ (P)$ is $τ (P) = E_{P} [Y (1) - Y (0)] .$ Binary potential outcomes place the target in $[- 1, 1]$ . The observed law $P_{O}$ is the image of $P$ under the observation map above. Expectations of procedures based on the observed sample are consequently taken under $P_{O}^{\otimes n}$ , even when written as $E_{P}$ .

Identification also requires arrived outcomes in every occupied conditioning cell. The next definition fixes the conditional quantities and their values on null cells before we impose an arrival floor.

Definition 5 [synth_5] (Cellwise arrival probability

ρ_{P}

and outcome mean

μ_{P}

In the setting of Assumption 1, Assumption 2, Assumption 3, Assumption 4, Assumption 5, Assumption 6, Definition 6, Definition 7, Definition 12, Definition 9, Definition 10, Definition 11, Algorithm 1, Definition 13, Definition 14, Lemma 1, Lemma 2, Lemma 4, Lemma 5, Lemma 3, Theorem 1, Theorem 2, Proposition 1, Theorem 3, Definition 4, Definition 3, Definition 1, Definition 2, and Definition 8, define the cellwise arrival probability and arrived-outcome conditional mean by $ρ_{P} (x, a, s) = {P (R = 1 ∣ X = x, A = a, S = s), 0, P (X = x, A = a, S = s) > 0, P (X = x, A = a, S = s) = 0,$ and $μ_{P} (x, a, s) = {E_{P} [Y ∣ X = x, A = a, S = s, R = 1], 0, P (X = x, A = a, S = s, R = 1) > 0, P (X = x, A = a, S = s, R = 1) = 0.$ Here $P$ is a full-data law, $X \in {0, \dots, d - 1}$ is the baseline cell, $A \in {0, 1}$ is the treatment assignment, $S \in {0, 1}$ is the observed surrogate, $R \in {0, 1}$ is the outcome-arrival indicator, and $Y \in {0, 1}$ is the realized primary outcome. The definitions apply to every $(x, a, s) \in {0, \dots, d - 1} \times {0, 1}^{2}$ .

The cellwise arrival probability $ρ_{P} (x, a, s)$ and arrived-outcome mean $μ_{P} (x, a, s)$ are therefore defined for every cell. Their zero conventions assign values to conditional quantities at null events. The positivity restriction concerns cells with positive probability.

Assumption 6 [ass:arrival-floor] (Cellwise outcome-arrival floor).

For every cell $(x, a, s)$ with positive probability under the full-data law $P$ , the cellwise arrival probability $ρ_{P} (x, a, s)$ is at least the arrival floor $q$ : $P (X = x, A = a, S = s) > 0 ⟹ ρ_{P} (x, a, s) \geq q .$

⊢ Lean

The known uniform MAR positivity floor is the finite-cell specialization of the outcome-observation overlap condition (Kallus et al., 2025). It ensures positive arrived mass in each occupied cell and quantifies how much primary-outcome information is retained there. The floor is a bound on the cellwise probabilities; the probabilities themselves may vary across cells. Combining it with the design and missingness conditions gives the law class over which statistical performance is evaluated.

Definition 6 [def:law-class] (Law class

M (d, q)

$M (d, q) = {P : ∣ supp_{P} (X) ∣ \leq d, P satisfies A ss u m pt i o n s 2, 3, 4, 5, an d 6} .$ Here $d$ is a positive integer, $q \in [1/2, 1]$ is the known cellwise arrival floor, and $supp_{P} (X)$ is the set of baseline labels with positive probability under $P$ .

⊢ Lean

The law class $M (d, q)$ allows arbitrary baseline masses and arbitrary binary potential-measurement distributions subject to the stated restrictions. In particular, occupied baseline labels may have small probability. At $q = 1$ , every occupied cell has complete outcome arrival. The coordinate definitions also specify an empty-alphabet convention at $d = 0$ ; the minimax analysis uses positive $d$ .

Within this class, the population treatment effect can be expressed entirely through the observed law. The identifying functional weights arrived-outcome means by each arm’s distribution of baseline and surrogate measurements.

Definition 7 [def:identified-functional] (Observed-data identifying functional).

The observed-data functional is $Ψ (P_{O}) = x = 0 \sum d - 1 s = 0 \sum 1 {\frac{P _{O} ( X = x , A = 1 , S = s )}{P _{O} ( A = 1 )} μ_{P} (x, 1, s) - \frac{P _{O} ( X = x , A = 0 , S = s )}{P _{O} ( A = 0 )} μ_{P} (x, 0, s)},$ for any nonnegative integer $d$ and any observed-record probability law $P_{O}$ on $O = {0, \dots, d - 1} \times {0, 1}^{4},$ with coordinates $(X, A, S, R, R Y)$ . The baseline-label set and the outer sum are empty when $d = 0$ . The arrived-outcome mean is defined by $μ_{P} (x, a, s) = \frac{P _{O} ( X = x , A = a , S = s , R = 1 , R Y = 1 )}{P _{O} ( X = x , A = a , S = s , R = 1 )}, a, s \in {0, 1} .$ Every ratio with zero denominator is assigned the value zero. Thus each weighted contribution is zero whenever $P_{O} (X = x, A = a, S = s) = 0$ .

⊢ Lean

The observed-data functional $Ψ (P_{O})$ identifies $τ (P)$ for $P \in M (d, q)$ , as established in Lemma 1. Balanced randomization gives positive arm probabilities, and the arrival floor gives positive arrived mass in every occupied cell. The zero-denominator convention handles the remaining null cells. The resulting finite-cell expression corresponds to the nested-regression identification formula of Kallus et al. (2025), specialized here to balanced randomized assignment, binary measurements, and finite baseline support.

Having fixed the target and observed experiment, we evaluate point estimation by worst-law squared error. Procedures are defined on the entire Cartesian sample space and take values in the treatment-effect range.

Definition 8 [synth_6] (Measurable estimator class

T_{n}

For integers $n, d \geq 1$ , define the measurable estimator class by $T_{n} = {T : ({0, \dots, d - 1} \times {0, 1}^{4})^{n} ⟶ [- 1, 1] : T is measurable} .$ Here the observed record $O = (X, A, S, R, R Y)$ takes values in the Cartesian observed-record space ${0, \dots, d - 1} \times {0, 1}^{4}$ , with the baseline-label convention of Definition 3. Thus each $T \in T_{n}$ is defined on every sample in this Cartesian space and takes values in the treatment-effect range $[- 1, 1]$ , in the setting of Assumption 1, Assumption 2, Assumption 3, Assumption 4, Assumption 5, Assumption 6, Definition 6, Definition 7, Definition 12, Definition 9, Definition 10, Definition 11, Algorithm 1, Definition 13, Definition 14, Lemma 1, Lemma 2, Lemma 4, Lemma 5, Lemma 3, Theorem 1, Theorem 2, Proposition 1, Theorem 3, Definition 4, Definition 1, Definition 2, and Definition 5.

The estimator class $T_{n}$ permits any measurable use of the retained information. Since the sample space is finite with its discrete $σ$ -algebra, every map into $[- 1, 1]$ is measurable. Taking the worst risk over the law class and then optimizing over procedures defines the point-estimation criterion.

Definition 9 [def:point-risk] (Minimax squared-error risk

R_{n, d, q}^{*}

$R_{n, d, q}^{*} = T \in T_{n} in f P \in M (d, q) sup E_{P} [{T (O_{1}, \dots, O_{n}) - τ (P)}^{2}] .$

⊢ Lean

The minimax squared-error risk $R_{n, d, q}^{*}$ measures the smallest worst-law mean squared error attainable from $n$ observed records. The order of optimization requires one procedure to perform across the entire law class at the specified sample size, support bound, and arrival floor.

For inference, fix a noncoverage level $α \in (0, 1/2)$ . We require connected intervals with coverage at least $1 - α$ uniformly over the same class.

Definition 10 [def:interval-class] (Honest connected confidence intervals).

The class $C_{α} (n, d, q)$ , for nonnegative integers $n, d$ and real parameters $q, α$ , is defined using the observed-record space $O$ with the baseline-label convention of Definition 3. It consists of procedures $I (o) = [L (o), U (o)]$ with measurable endpoints satisfying $- 1 \leq L (o) \leq U (o) \leq 1 for every o \in O^{n},$ and uniform coverage: $C_{α} (n, d, q) = {I : P_{O}^{\otimes n} {o \in O^{n} : τ (P) \in [L (o), U (o)]} \geq 1 - α for every P \in M (d, q)} .$ Here $M (d, q)$ is the law class in Definition 6, and $τ (P) = E_{P} [Y (1) - Y (0)]$ is the superpopulation average treatment effect. For $q \in [1/2, 1]$ and $P \in M (d, q)$ , Lemma 1 gives $τ (P) = Ψ (P_{O})$ , with $Ψ$ defined in Definition 7.

⊢ Lean

The honest interval class $C_{α} (n, d, q)$ imposes a finite-sample coverage requirement for every law in $M (d, q)$ . Its endpoints define a closed connected subset of $[- 1, 1]$ on every possible sample. The fixed interval $[- 1, 1]$ belongs to the class, so the coverage requirement is feasible. Among honest procedures, expected length measures precision.

Definition 11 [def:length-risk] (Minimax expected length

L_{n, d, q, α}^{*}

$L_{n, d, q, α}^{*} = I \in C_{α} (n, d, q) in f P \in M (d, q) sup E_{P} [length {I (O^{n})}] .$ For $I (O^{n}) = [L, U]$ , its length is $U - L$ .

⊢ Lean

The minimax expected length $L_{n, d, q, α}^{*}$ is the smallest worst-law expected interval length compatible with uniform coverage. Both criteria use the full observed record: missing-outcome observations contribute their baseline category, treatment, surrogate, and arrival status to any admissible procedure.

A common benchmark will express the dependence of these criteria on sample size, baseline dimension, and outcome arrival. Define the logarithmic sample-size factor $ℓ_{n}$ and the arrival-deficit-weighted dimension scale $g_{n, d, q}$ by $ℓ_{n} = lo g (e + n), g_{n, d, q} = (1 - q) min {1, \frac{d}{n ℓ _{n}}} .$ These quantities give the following squared-error benchmark.

Definition 12 [def:rate] (Squared-error benchmark

r_{n, d, q}

$r_{n, d, q} = \frac{1}{n} + (1 - q)^{2} min {1, [\frac{d}{n lo g ( e + n )}]^{2}} = \frac{1}{n} + g_{n, d, q}^{2} .$

⊢ Lean

The benchmark $r_{n, d, q}$ combines a sampling term with a dimension term weighted by the outcome-arrival deficit. Its dimension component is bounded by $(1 - q)^{2}$ and vanishes at complete arrival. The comparisons in Theorems 1 and 2 relate minimax squared error to $r_{n, d, q}$ and minimax honest expected length to its square root, respectively.

Minimax estimation and honest inference

The benchmark in Definition 12 is attained by splitting each cell’s treatment-effect contribution into information from arrived outcomes and a correction for its missing-outcome mass. Arrival reveals the outcome needed for the first piece; a missing record still reveals $(X, A, S)$ , which supplies the weight for the second. Under Assumption 5, the arrived-outcome mean identifies the mean used in both pieces. The moment estimator $τ_{MM}$ uses separate streams to estimate them and to choose between polynomial and ratio corrections. Its final conditional average produces a procedure determined by the observed sample.

We first fix the operator and polynomial conventions used in the construction. Projection onto the treatment-effect range is $Π_{[- 1, 1]} (t) = max {- 1, min {1, t}}$ . The degree- $k$ Chebyshev polynomial $T_{k}$ has convention $T_{k} (cos θ) = cos (k θ)$ . For a cell count $C_{j}$ and a positive integer $v$ , the falling factorial $(C_{j} - 1)_{v - 1}$ denotes $\prod_{t = 1}^{v - 1} (C_{j} - t)$ , with an empty product equal to one. These conventions specify the projection and polynomial correction in the following construction.

Algorithm 1 [def:mm-estimator] (Moment estimator

τ_{MM}

Given observed records $O_{1}, \dots, O_{n}$ , sample size $n$ , support bound $d$ , and arrival floor $q$ , define $τ_{MM}$ using the tuning parameters $m, k, B$ as follows.

Set $ℓ_{n} = lo g (e + n), m = \frac{n}{8}, k = max {1, ⌊ ℓ_{n} /64 ⌋}, B = 256 ℓ_{n} .$ Write the supplied fifth coordinate of each observed record as $Y_{i}^{obs} = (R Y)_{i} .$ On the support of the observation map, this coordinate equals $R_{i} Y_{i}$ and is zero when the outcome is missing.
Draw $N \sim Poisson (n /2) .$ If $N > n$ , set $τ = 0$ . If $N \leq n$ , independently assign each of the first $N$ records a uniform stream indicator and define the stream index sets by $Z_{i} \in {1, 2, 3, 4}, Pr (Z_{i} = t) = \frac{1}{4}, I_{t} = {i \in {1, \dots, N} : Z_{i} = t} .$ For this branch, perform the following three steps.
For each cell $j = (x, a, s)$ , write $a_{j} = a$ and define $M_{j}^{(2)} = i \in I_{2} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 0}, V_{j} = \frac{M _{j}^{(2)}}{m},$ $C_{j}^{'} = i \in I_{3} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 1}, C_{j} = i \in I_{4} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 1},$ $U_{j} = i \in I_{4} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, Y_{i}^{obs} = 1} .$ Thus $U_{j}$ is the arrived-success count on the support of the observation map.
Let $T_{k}$ be the degree- $k$ Chebyshev polynomial, with convention $T_{k} (cos θ) = cos (k θ) .$ Define $Q_{k} (z) = ⎩ ⎨ ⎧ \frac{1 - T _{k} ( 1 - 2 z / B )}{2 k ^{2} z / B}, 1, z \neq = 0, z = 0, 1 - Q_{k} (z) = v = 1 \sum k - 1 a_{v} z^{v} .$ Using the falling-factorial convention $(C_{j} - 1)_{v - 1} = t = 1 \prod v - 1 (C_{j} - t),$ where an empty product equals one, set $H_{j} = v = 1 \sum k - 1 a_{v} (U_{j} - C_{j} /2) (C_{j} - 1)_{v - 1}, D_{j} = {U_{j} / C_{j} - 1/2, 0, C_{j} > 0, C_{j} = 0,$ $G_{j} = H_{j} 1 {C_{j}^{'} \leq B /4} + D_{j} 1 {C_{j}^{'} > B /4} .$
Define the interval projection and randomized estimate by $Π_{[- 1, 1]} (t) = max {- 1, min {1, t}},$ $τ = Π_{[- 1, 1]} [\frac{2}{m} i \in I_{1} \sum (2 A_{i} - 1) R_{i} (Y_{i}^{obs} - \frac{1}{2}) + 2 j \sum (2 a_{j} - 1) V_{j} G_{j}] .$
Output $τ_{MM} = ⎩ ⎨ ⎧ Π_{[- 1, 1]} [\frac{2}{n} i = 1 \sum n (2 A_{i} - 1) Y_{i}^{obs}], Π_{[- 1, 1]} [\frac{2}{n} i = 1 \sum n (2 A_{i} - 1) R_{i} (Y_{i}^{obs} - \frac{1}{2})], E [τ ∣ O_{1}, \dots, O_{n}], q = 1, q \neq = 1 and (ℓ_{n} < 128 or d \geq n ℓ_{n}), q \neq = 1, ℓ_{n} \geq 128, d < n ℓ_{n} .$ The conditional expectation averages over the auxiliary Poisson draw and stream assignments.

⊢ Lean

The polynomial-and-ratio branch is used when $ℓ_{n} = lo g (e + n) \geq 128$ , equivalently $n \geq e^{128} - e$ , together with $d < n ℓ_{n}$ and $q \neq = 1$ ; the displayed fallback branch covers the complementary regime. These are the exhibited finite-sample tuning choices supporting the order guarantee.

Centering arrived outcomes at one half aligns the first-stream contribution with the centered cell means used in the correction. The arrival indicator ensures that the centered contribution is drawn from observed outcomes. Missing records supply their cell membership through the second-stream statistic $V_{j}$ , which weights the correction by missing-outcome mass. Under the missing-at-random condition in Assumption 5, the arrived-outcome mean identifies the outcome mean needed for this missing component.

The third-stream count selects how the fourth-stream data enter the correction. Lightly populated cells use the polynomial statistic $H_{j}$ , whose coefficients and falling-factorial terms implement the moment correction. Heavily populated cells use the centered empirical ratio $D_{j}$ . Separating the selection count from the correction data supports the risk analysis in Lemma 2. Conditional averaging then integrates out the auxiliary Poisson draw and stream assignments; convexity of squared loss preserves the risk bound under this averaging. The complete-arrival and fallback branches specify the estimator across all sample sizes and support bounds.

The uniform squared-risk bound also supplies a finite-sample confidence radius. Let $C_{U}$ be a universal upper-risk constant, so that the worst-law squared risk of the estimator is at most $C_{U} r_{n, d, q}$ , as established in Lemma 2. The confidence interval $I_{MM, α}$ uses the clipped radius $h_{n, d, q, α}$ defined below. The construction attains the minimax expected-length order for fixed $α$ ; with the exhibited fallback contribution $C_{fall} = 4 e^{128}$ and resulting choice of $C_{U}$ , its interval equals $[- 1, 1]$ whenever $ℓ_{n} < 128$ .

Definition 13 [def:mm-interval] (Confidence interval

I_{MM, α}

Define $I_{MM, α} (O^{n}) = [max {- 1, τ_{MM} - h_{n, d, q, α}}, min {1, τ_{MM} + h_{n, d, q, α}}],$ where the clipped confidence radius is $h_{n, d, q, α} = min {2, \frac{C _{U} r _{n, d, q}}{α}},$ and $C_{U}$ is any universal constant for which the upper squared-risk bound for $τ_{MM}$ holds.

⊢ Lean

For a radius below two, Markov’s inequality bounds the probability that the estimation error exceeds the radius by $α$ , uniformly over $M (d, q)$ . A radius of two yields the entire treatment-effect range. Clipping the endpoints preserves coverage because the target belongs to $[- 1, 1]$ . Consequently, the interval belongs to the honest class in Definition 10, and its length is at most $2 h_{n, d, q, α}$ . The coverage and length conclusions are recorded in Lemma 3.

The attainable risk and interval length match lower bounds over the same experiment and law class. The following two results characterize the point-estimation and honest-inference criteria together.

Theorem 1 [thm:point-frontier] (Finite-sample minimax risk frontier).

There exist universal numerical constants $0 < c < C < \infty$ such that, for every pair of positive integers $n, d$ and every known arrival floor $q \in [1/2, 1]$ , $c r_{n, d, q} \leq R_{n, d, q}^{*} \leq C r_{n, d, q},$ where $r_{n, d, q}$ is the squared-error benchmark defined in Definition 12 and $R_{n, d, q}^{*}$ is the minimax squared-error risk defined in Definition 9.

⊢ Lean

The comparison separates ordinary sampling error from the cost of recovering outcome means across many cells. The sampling contribution is $n^{- 1}$ ; the additional squared-error contribution is $(1 - q)^{2} min {1, [d / (n lo g (e + n))]^{2}}$ . Its dependence on missingness reflects the estimator’s use of cell corrections weighted by missing-outcome mass. The matching lower bound makes this dependence a property of the minimax criterion over $M (d, q)$ . In particular, the comparison identifies the precision scale uniformly as the arrival floor approaches one.

Honest inference is governed by the square root of the same benchmark, with comparison constants allowed to depend on the fixed coverage requirement.

Theorem 2 [thm:interval-frontier] (Fixed coverage length frontier).

For each fixed noncoverage level $α \in (0, 1/2)$ , there exist constants $0 < c_{α} < C_{α} < \infty$ , depending only on $α$ , such that, for every pair of positive integers $n, d$ and every $q \in [1/2, 1]$ , the minimax expected interval length $L_{n, d, q, α}^{*}$ from Definition 11 and the squared-error benchmark $r_{n, d, q}$ from Definition 12 satisfy $c_{α} r_{n, d, q} \leq L_{n, d, q, α}^{*} \leq C_{α} r_{n, d, q} .$

⊢ Lean

The risk-based interval construction explains the attainable square-root scale. The lower bound establishes its necessity for worst-law expected length among connected intervals satisfying uniform finite-sample coverage. Thus, for each fixed $α$ , the same sampling and missingness-weighted dimension terms determine both squared-error precision and honest interval precision under the respective criteria in Definitions 9 and 11.

The upper-bound arguments are supplied by Lemmas 2 and 3. For the converse, Lemma 4 supplies the sampling lower bounds, while Theorem 3 and Lemma 5 supplies the dimension lower bounds through normalized priors and testing reductions. Together, these arguments give the matching comparisons in Theorems 1 and 2.

At complete arrival, the construction has a direct randomized-trial interpretation. It becomes the projected difference formed with the known treatment-allocation weights, and both minimax criteria have dimension-free parametric rates. The following result also quantifies the effect of projection on each sample and on worst-law squared risk.

Proposition 1 [prop:complete-arrival-reduction] (Complete arrival and parametric frontiers).

There exist universal constants $0 < c < C$ such that, for every noncoverage level $α \in (0, 1/2)$ , there exist constants $0 < c_{α} < C_{α}$ , depending only on $α$ , for which the following statements hold for every positive integer sample size $n$ and positive integer baseline-support bound $d$ at arrival floor $q = 1$ .

The error scale and squared-error benchmark satisfy $g_{n, d, 1} = (1 - 1) min {1, \frac{d}{n lo g ( e + n )}} = 0, r_{n, d, 1} = \frac{1}{n},$ where the benchmark is defined in Definition 12. For every sample $O^{n} = (O_{1}, \dots, O_{n})$ in the Cartesian observed-record space, the estimator of Algorithm 1 satisfies $τ_{MM} (O^{n}) = Π_{[- 1, 1]} [\frac{2}{n} i = 1 \sum n (2 A_{i} - 1) Y_{i}^{obs}],$ where $A_{i}$ is the binary treatment coordinate, $Y_{i}^{obs} = (R Y)_{i}$ is the supplied fifth coordinate of record $i$ , and $Π_{[- 1, 1]} (z) = max {- 1, min {1, z}}$ is interval projection.

For every full-data law $P \in M (d, 1)$ and every such sample, with population average treatment effect $τ (P) = E_{P} [Y (1) - Y (0)]$ , where $Y (1)$ and $Y (0)$ are the binary potential outcomes, $∣ τ_{MM} (O^{n}) - τ (P) ∣ \leq \frac{2}{n} i = 1 \sum n (2 A_{i} - 1) Y_{i}^{obs} - τ (P) .$ Under the iid observed-sample law induced by $P$ , $P \in M (d, 1) sup E_{P} [(τ_{MM} (O^{n}) - τ (P))^{2}] \leq P \in M (d, 1) sup E_{P} (\frac{2}{n} i = 1 \sum n (2 A_{i} - 1) Y_{i}^{obs} - τ (P))^{2} \leq \frac{4}{n} .$ The minimax squared-error risk and minimax worst-law expected honest interval length of Definitions 9 and 11 satisfy, uniformly over $n, d \geq 1$ , $\frac{c}{n} \leq R_{n, d, 1}^{*} \leq \frac{C}{n}, \frac{c _{α}}{n} \leq L_{n, d, 1, α}^{*} \leq \frac{C _{α}}{n} .$

⊢ Lean

Under balanced randomization, the unprojected expression is the standard allocation-weighted difference between treated and control outcomes, using the known allocation probability of one half. Projection weakly reduces its absolute error for every target in the treatment-effect range, and the displayed risk bound is uniform in the baseline-support bound. Complete arrival therefore yields squared-error precision of order $n^{- 1}$ and honest expected length of order $n^{- 1/2}$ across all $d \geq 1$ . The endpoint follows from the complete-arrival branch of Algorithm 1, projection contraction, and the sampling lower bounds in Lemma 4.

Statistical implications

The comparisons in Theorems 1 and 2 distinguish sampling uncertainty from the additional cost of recovering outcome means across baseline cells. In the benchmark of Definition 12, sampling contributes $n^{- 1}$ to squared error, while the dimension contribution is weighted by the square of the arrival deficit $1 - q$ . Accordingly, the minimax root mean squared error has order $n^{- 1/2} + (1 - q) min {1, \frac{d}{n ℓ _{n}}}, ℓ_{n} = lo g (e + n) .$ The comparison constants are uniform over positive integers $n, d$ and known arrival floors $q \in [1/2, 1]$ . This uniformity permits sample size, baseline dimension, and outcome arrival to vary jointly.

Before saturation, when $d \leq n ℓ_{n}$ , the dimension contribution to root mean squared error is $(1 - q) d / (n ℓ_{n})$ . It matches the sampling scale when $(1 - q) d = n ℓ_{n} .$ Below this balance, sampling determines the order of precision; above it, the arrival-weighted dimension term determines that order. For a fixed arrival floor below one, the transition therefore occurs at baseline dimension of order $n ℓ_{n} / (1 - q)$ , provided this lies within the unsaturated range. As the arrival floor increases, a larger baseline dimension becomes compatible with sampling-scale precision. In particular, $1 - q \leq n^{- 1/2}$ guarantees precision of order $n^{- 1/2}$ uniformly over all positive baseline-support bounds. Complete arrival gives the exact endpoint described in Proposition 1.

Saturation occurs at $d \geq n ℓ_{n}$ , where the dimension contribution to squared error equals $(1 - q)^{2}$ . Increasing the support bound within this regime leaves the benchmark unchanged. With a fixed arrival floor below one, the minimax risk then remains bounded away from zero as sample size grows along such a sequence. An arrival floor approaching one instead reduces the saturated contribution directly. Thus the rate separates the effect of increasing sample size relative to dimension from the effect of improving outcome arrival.

More generally, let $d_{n}$ be a sequence of positive baseline-support bounds and $q_{n} \in [1/2, 1]$ a sequence of known arrival floors, with $n \to \infty$ . The point-estimation comparison implies that minimax squared risk tends to zero precisely when $(1 - q_{n}) min {1, \frac{d _{n}}{n ℓ _{n}}} ⟶ 0.$ For an arrival floor fixed below one, this condition becomes $d_{n} = o (n ℓ_{n})$ . For $q_{n} \to 1$ , it is satisfied for every dimension sequence. Sampling-order squared risk, of order $n^{- 1}$ , is attained precisely when the displayed dimension scale is $O (n^{- 1/2})$ . These statements describe the joint sequences through the same finite-sample comparison, with constants independent of the sequence.

Honest inference translates these regimes into uniform coverage with corresponding expected precision. For each fixed $α \in (0, 1/2)$ , Theorem 2 gives minimax worst-law expected length of order $n^{- 1/2} + (1 - q) min {1, \frac{d}{n ℓ _{n}}},$ with constants depending only on $α$ . The interval criterion in Definitions 10 and 11 requires coverage at least $1 - α$ for every law in the specified class at each sample size. Consequently, the joint-sequence condition above also characterizes when this optimal worst-law expected length tends to zero. Sampling-dominated regimes yield honest expected length of order $n^{- 1/2}$ , while saturation yields length of order $n^{- 1/2} + 1 - q$ . The lower comparison concerns the worst-law expected length among honest connected intervals; the construction in Definition 13 attains the corresponding order throughout the class.

The converse also has a useful implication for model enlargement. The sampling and dimension lower bounds in Lemma 4, Theorem 3, and Lemma 5 are supported by randomized submodels with a constant surrogate. Any broader law class on the same observed experiment, with the same treatment-effect target, that contains these submodels inherits their lower bounds: its worst-law criterion includes the laws used in the converse. This establishes a necessary precision scale for such containing classes. The matching upper bounds characterize attainable precision over the finite-cell randomized-MAR model in Definition 6, with its binary measurements, known arrival floor, and baseline-support bound. Together, the two directions identify how sampling, dimension, and outcome arrival govern optimal precision in that model.

Limitations and future work

The results in Theorems 1 and 2 characterize minimax squared-error risk and honest expected interval length for the finite-cell randomized-MAR class in Definition 6, with a known cellwise arrival floor $q \in [1/2, 1]$ and a specified baseline-support bound $d$ . These conditions provide the reference point for several extensions concerning weaker arrival guarantees, adaptation, and practical implementation.

Arrival floors below one half are a natural direction for further analysis. Extending the comparison to $0 < q < 1/2$ requires establishing upper and lower bounds that account for the dependence on the floor, including regimes in which it approaches zero as the sample size increases. The bounds established for $q \in [1/2, 1]$ do not determine that dependence. A separate question is adaptation when the floor is unknown. The construction in Algorithm 1 and Definition 13 uses the supplied floor, so a procedure that selects its degree of correction or interval radius from the data would require a new analysis of risk and uniform coverage. Such an analysis would need to address arrival probabilities in sparsely represented cells, where estimating a valid lower bound can itself be difficult.

The comparison with broader models has a precise lower-bound interpretation. Any law class on the same observed experiment, with the same treatment-effect target, that contains the submodels used in Lemma 4, Theorem 3, and Lemma 5 inherits the corresponding lower bounds. For point estimation, the enlarged worst-law risk includes the laws supporting the converse. For honest intervals, coverage over the enlarged class entails coverage over those submodels, and the enlarged worst-law expected length includes their expected lengths. Matching procedures for broader classes require further analysis of their identifying restrictions and statistical complexity; the matching upper bounds here concern the class in Definition 6.

Computational implementation is another direction for development. The estimator in Algorithm 1 averages over auxiliary randomization conditional on the observed sample. This conditional average specifies a statistical procedure, while an efficient method for evaluating it remains a practical question. Possible approaches include exact evaluation where feasible and numerical approximation elsewhere. An approximation would require control of its additional error, together with an assessment of how that error affects the risk bound and the coverage of intervals centered at the computed estimate. The statistical construction supplies no computational complexity guarantee.

Practical constants also warrant investigation. The polynomial branch of Algorithm 1 requires $n \geq e^{128} - e$ , and the proof’s fallback contribution is $C_{fall} = 4 e^{128}$ . With the exhibited upper-risk constant, the interval in Definition 13 is therefore the full range $[- 1, 1]$ whenever $lo g (e + n) < 128$ . The theorems establish universal-constant minimax orders, while these particular numerical choices do not yield an informative interval at ordinary sample sizes. Sharper constants, alternative tuning, and computational study are needed to turn the theoretical construction into a practical procedure; each change would require new risk and coverage justification.

Empirical calibration can complement this work through simulations that vary support size, cell-frequency imbalance, and arrival probabilities within the specified model. Mean squared error, coverage, and expected interval length would provide direct measures of performance, including near complete arrival and in settings with many sparsely occupied cells. Such exercises could guide implementation and identify useful tuning choices, while uniform guarantees for those choices would remain a separate theoretical task.

Appendices

Identification and estimation bounds

The constructive bounds first identify the superpopulation treatment effect from the observed law and then control the estimator’s squared error uniformly.

Identification under randomized MAR

The cell means in Definitions 5 and 7 use explicit conventions at null conditioning events. The following result establishes identification with those conventions and the randomized-MAR restrictions.

Lemma 1 [lem:identification-infrastructure] (Randomized MAR identification).

Let $d$ be a nonnegative integer, let $q \in [1/2, 1]$ be the cellwise arrival floor, and let $P$ be a full-data probability law with baseline variable $X$ taking values in a set of $d$ labels, binary treatment $A$ , binary potential surrogates $S (0), S (1)$ , binary potential outcomes $Y (0), Y (1)$ , binary realized surrogate and outcome $S, Y$ , and binary outcome-arrival indicator $R$ . Suppose that $P$ satisfies:

(Randomized independence.) Assumption 2.

(Balanced randomization.) Assumption 3.

(Consistency.) Assumption 4.

(Missing at random.) Assumption 5.

(Arrival floor.) Assumption 6 with floor $q$ .

Write $P_{O}$ for the image of $P$ under the observation map $O = (X, A, S, R, R Y)$ , where $R Y$ is the observed outcome mark. Then the superpopulation average treatment effect satisfies $τ (P) = E_{P} [Y (1) - Y (0)] = Ψ (P_{O}),$ where $Ψ$ is the observed-law functional in Definition 7, with every contribution from a null $(X, A, S)$ cell equal to zero by definition.

⊢ Lean

Proof of Lemma 1.

For each $a \in {0, 1}$ , consistency in Assumption 4 gives $P (A = a, Y = 1) = P (A = a, Y (a) = 1) .$ To calculate the latter probability, define the potential-coordinate vector and its relevant finite subset by $V_{pot} := (X, S (0), S (1), Y (0), Y (1)), V_{pot, a} := {(x, s_{0}, s_{1}, y_{0}, y_{1}) \in {0, \dots, d - 1} \times {0, 1}^{4} : y_{a} = 1}, a \in {0, 1} .$ Summing the atomwise factorization supplied by Assumption 2 over this subset yields $P (A = a, Y (a) = 1) = v \in V_{pot, a} \sum P (A = a, V_{pot} = v) = P (A = a) v \in V_{pot, a} \sum P (V_{pot} = v) = P (A = a) P (Y (a) = 1) .$ Here the sums partition the indicated events by their potential-coordinate tuples. By Assumption 3 and the binary treatment partition, $P (A = 1) = \frac{1}{2}, P (A = 0) = 1 - P (A = 1) = \frac{1}{2} .$ Consequently, the two arm identities are $2 P (A = 1, Y = 1) = P (Y (1) = 1), 2 P (A = 0, Y = 1) = P (Y (0) = 1) .$
Since both potential outcomes are binary, their numerical values equal their success indicators. Linearity of expectation therefore gives $τ (P) = E_{P} [1_{{Y (1) = 1}} - 1_{{Y (0) = 1}}] = P (Y (1) = 1) - P (Y (0) = 1) .$
Define the cell events, for their full range of indices, by $E_{x, a, s} := {X = x, A = a, S = s}, x \in {0, \dots, d - 1}, a, s \in {0, 1} .$ The observation map preserves $X, A, S, R$ , and on ${R = 1}$ its outcome mark equals $Y$ . Thus its image law satisfies $P_{O} (E_{x, a, s}) = P (E_{x, a, s}), P_{O} (A = a) = P (A = a), P_{O} (E_{x, a, s}, R = 1) = P (E_{x, a, s}, R = 1), P_{O} (E_{x, a, s}, R = 1, R Y = 1) = P (E_{x, a, s}, R = 1, Y = 1) .$ In particular, Definition 7 supplies $\frac{P _{O} ( E _{x, a, s} )}{P _{O} ( A = a )} = \frac{P ( E _{x, a, s} )}{P ( A = a )}, μ_{P} (x, a, s) = \frac{P ( E _{x, a, s} , R = 1 , Y = 1 )}{P ( E _{x, a, s} , R = 1 )},$ with zero assigned to every ratio whose denominator is zero.

We identify the weighted contribution by splitting according to the cell mass. If $P (E_{x, a, s}) = 0$ , nonnegativity and event inclusion imply $0 \leq P (E_{x, a, s}, Y = 1) \leq P (E_{x, a, s}) = 0.$ Hence both the weighted observed contribution and $P (E_{x, a, s}, Y = 1) / P (A = a)$ are zero.

If $P (E_{x, a, s}) > 0$ , event inclusion gives $0 < P (E_{x, a, s}) \leq P (A = a) .$ The arrival floor in Assumption 6 and the stipulated range of $q$ give $\frac{P ( E _{x, a, s} , R = 1 )}{P ( E _{x, a, s} )} \geq q \geq \frac{1}{2} > 0, P (E_{x, a, s}, R = 1) > 0.$ Conditional independence in Assumption 5, applied to $R = 1$ and $Y = 1$ , gives the cross-product identity $P (E_{x, a, s}, R = 1, Y = 1) P (E_{x, a, s}) = P (E_{x, a, s}, R = 1) P (E_{x, a, s}, Y = 1) .$ Dividing by the two positive cell masses yields $μ_{P} (x, a, s) = \frac{P ( E _{x, a, s} , R = 1 , Y = 1 )}{P ( E _{x, a, s} , R = 1 )} = \frac{P ( E _{x, a, s} , Y = 1 )}{P ( E _{x, a, s} )} .$ Multiplication by the cell weight now proves, in both cases, $\frac{P _{O} ( E _{x, a, s} )}{P _{O} ( A = a )} μ_{P} (x, a, s) = \frac{P ( E _{x, a, s} , Y = 1 )}{P ( A = a )} .$
For either treatment arm, every realization with $A = a$ and $Y = 1$ belongs to exactly one cell indexed by its values of $X$ and $S$ . The disjoint finite-cell partition therefore gives $x = 0 \sum d - 1 s = 0 \sum 1 P (E_{x, a, s}, Y = 1) = P (A = a, Y = 1), a \in {0, 1} .$
Substituting the cell-contribution identity into Definition 7, distributing the finite sums, and applying the arm partitions gives $Ψ (P_{O}) = x = 0 \sum d - 1 s = 0 \sum 1 {\frac{P ( E _{x, 1, s} , Y = 1 )}{P ( A = 1 )} - \frac{P ( E _{x, 0, s} , Y = 1 )}{P ( A = 0 )}} = \frac{P ( A = 1 , Y = 1 )}{P ( A = 1 )} - \frac{P ( A = 0 , Y = 1 )}{P ( A = 0 )} = 2 P (A = 1, Y = 1) - 2 P (A = 0, Y = 1) = P (Y (1) = 1) - P (Y (0) = 1) = τ (P) .$ The null-cell case above establishes the stipulated zero contributions. When $d = 0$ , the baseline-label set is empty, so a probability law with $X$ taking values in that set cannot exist; the assertion for that case is vacuous.

∎

Randomized independence and consistency give the arm-specific outcome means their potential-outcome interpretation. Within an occupied baseline–treatment–surrogate cell, MAR makes the arrived-outcome conditional mean equal to the cell’s realized-outcome mean. The arrival floor ensures that this arrived conditional mean has a positive conditioning probability. The weights in Definition 7 are the conditional cell probabilities within each randomized arm; balanced assignment fixes the arm probabilities at one half. Together, these components give the finite-cell form of the nested-regression identification formula in Kallus et al. (2025).

The null-cell conventions complete this interpretation over the entire baseline alphabet. A cell with zero mass receives zero weight, and its arrived-outcome mean is assigned zero. On occupied cells, the positive arrival floor makes the conditional mean well defined. Thus the totalized functional supplies the original superpopulation target for every risk and coverage calculation over $M (d, q)$ .

Uniform estimation control

The estimator in Algorithm 1 combines an arrived-outcome contribution with a correction for missing outcomes. Its polynomial, ratio, complete-arrival, and fallback branches are covered by one uniform squared-error statement.

Lemma 2 [lem:upper-risk] (Uniform upper risk bound).

There exists a universal numerical constant $0 < C_{U} < \infty$ such that, for every choice satisfying

(Sample size and dimension.) $n, d$ are integers with $n \geq 1$ and $d \geq 1$ ;

(Arrival floor.) $q \in [1/2, 1]$ ;

(Law and sampling.) $P \in M (d, q)$ , and $O_{1}, \dots, O_{n}$ are independent observed records with common law $P_{O}$ , the observed-law image of $P$ ;

the estimator $τ_{MM}$ satisfies $E_{P} [(τ_{MM} - τ (P))^{2}] \leq C_{U} r_{n, d, q},$ where the expectation is over the stated independent sample.

⊢ Lean

Proof of Lemma 2.

Define the numerical constants $C_{bias} C_{switch} C_{log} C_{non} C_{fall} C_{U} = 268435456, = 201719808, = 720 (4/3)^{6} (e + 1), = 8 (C_{switch}^{2} C_{log} + 119) + 2 C_{bias}^{2} + 104, = 4 e^{128}, = C_{non} + C_{fall} .$ These constants are finite and positive. Fix parameters and a law satisfying the hypotheses, and put $δ = 1 - q \in [0, 1/2], ℓ_{n} = lo g (e + n) .$ By the independent sampling hypothesis, $(O_{1}, \dots, O_{n}) \sim P_{O}^{\otimes n} .$ From Definition 12, $r_{n, d, q} \geq \frac{1}{n} > 0.$ We establish the risk bounds $C_{fall} r_{n, d, q}$ and $C_{non} r_{n, d, q}$ in the corresponding branches of Algorithm 1. Each is at most $C_{U} r_{n, d, q}$ .
Suppose first that $q = 1$ . The arrival floor makes the conditional arrival probability equal to one in every positive-probability cell. Consequently, $P (R = 0) = 0.$ Define the complete-arrival score on the observed-record space by $F_{complete} : O ⟶ [- 2, 2], F_{complete} (O) = 2 (2 A - 1) R Y .$ The restrictions defining Definition 6 give $E_{P} [F_{complete} (O)] = 2 P (A = 1, Y = 1) - 2 P (A = 0, Y = 1) = P (Y (1) = 1) - P (Y (0) = 1) = τ (P) .$ Indeed, consistency replaces the realized outcome within each arm by its potential outcome, and randomized independence and balanced assignment give $2 P (A = a, Y = 1) = P (Y (a) = 1)$ for $a \in {0, 1}$ . Also, $Var_{P} (F_{complete} (O)) \leq E_{P} [F_{complete} (O)^{2}] \leq 4.$ Independence of the observations therefore yields $E_{P} {\frac{1}{n} i = 1 \sum n F_{complete} (O_{i}) - τ (P)}^{2} = \frac{Var _{P} ( F _{complete} ( O ))}{n} \leq \frac{4}{n} .$ The binary potential outcomes imply $τ (P) \in [- 1, 1]$ , and interval projection satisfies $Π_{[- 1, 1]} (t) - τ (P) \leq ∣ t - τ (P) ∣, t \in R .$ Thus the complete-arrival branch satisfies $E_{P} [(τ_{MM} - τ (P))^{2}] \leq \frac{4}{n} = 4 r_{n, d, 1} \leq C_{fall} r_{n, d, 1} \leq C_{U} r_{n, d, 1} .$
Suppose next that $q \neq = 1, ℓ_{n} < 128 or d \geq n ℓ_{n} .$ When $ℓ_{n} < 128$ , exponentiating its definition gives $n < e + n = e^{ℓ_{n}} < e^{128} .$ Both the estimator and the target lie in $[- 1, 1]$ , so $E_{P} [(τ_{MM} - τ (P))^{2}] \leq 4 \leq \frac{4 e ^{128}}{n} \leq C_{fall} r_{n, d, q} .$

For the large-dimension branch, introduce the following quantities, defined for every cell, including null cells: $J = {0, \dots, d - 1} \times {0, 1}^{2}, j = (x, a, s) \in J, π_{j} = P (X = x, A = a, S = s), t_{j} = P (X = x, A = a, S = s, R = 1), w_{j} = π_{j} - t_{j} = P (X = x, A = a, S = s, R = 0), μ_{P} (j) = μ_{P} (x, a, s), η_{j} = μ_{P} (j) - \frac{1}{2}, ϵ_{j} = 2 a - 1.$ The mean $μ_{P} (j)$ uses the zero-denominator convention in Definition 7. In particular, $∣ η_{j} ∣ \leq \frac{1}{2}, j \in J \sum π_{j} = 1.$ The arrival floor gives $q π_{j} \leq t_{j}$ on positive cells. On a null cell, $π_{j} = t_{j} = w_{j} = 0$ , so the same inequality holds. Since $q \geq 1/2$ , $0 \leq w_{j} \leq δ π_{j} \leq 2 δ t_{j}, j \in J \sum w_{j} \leq δ .$ Balanced assignment gives $j \in J \sum ϵ_{j} π_{j} = 0.$ Applying Lemma 1 and centering the cell means therefore gives $τ (P) = 2 j \in J \sum ϵ_{j} π_{j} η_{j} = 2 j \in J \sum ϵ_{j} (t_{j} η_{j} + w_{j} η_{j}) .$

Define the fallback score by $F_{fallback} : O ⟶ [- 1, 1], F_{fallback} (O) = 2 (2 A - 1) R (R Y - 1/2) .$ On the support of $P_{O}$ , its mean is $E_{P} [F_{fallback} (O)] = 2 j \in J \sum ϵ_{j} t_{j} η_{j} .$ Hence $∣ E_{P} [F_{fallback} (O)] - τ (P) ∣ = 2 j \in J \sum ϵ_{j} w_{j} η_{j} \leq j \in J \sum w_{j} \leq δ .$ The score bound and independent sampling imply $E_{P} {\frac{1}{n} i = 1 \sum n F_{fallback} (O_{i}) - E_{P} [F_{fallback} (O)]}^{2} \leq \frac{1}{n} .$ Using projection contraction and $(u + v)^{2} \leq 2 u^{2} + 2 v^{2}$ , we obtain $E_{P} [(τ_{MM} - τ (P))^{2}] \leq \frac{2}{n} + 2 δ^{2} .$ For $d \geq n ℓ_{n}$ , the minimum in Definition 12 equals one. Thus $\frac{2}{n} + 2 δ^{2} = 2 r_{n, d, q} \leq C_{fall} r_{n, d, q} .$ Both fallback subcases consequently satisfy the bound with $C_{U}$ . The cell quantities just defined will also be used below.
Consider now the remaining regime $q \neq = 1, ℓ_{n} \geq 128, d < n ℓ_{n} .$ The tuning parameters and benchmark become $m = \frac{n}{8}, k = ⌊ ℓ_{n} /64 ⌋, B = 256 ℓ_{n},$ $\frac{ℓ _{n}}{128} \leq k \leq \frac{ℓ _{n}}{64} = \frac{B}{16384}, g_{n, d, q} = \frac{δ d}{n ℓ _{n}}, r_{n, d, q} = \frac{1}{n} + g_{n, d, q}^{2} .$ The lower bound on $k$ follows from $⌊ ℓ_{n} /64 ⌋ \geq ℓ_{n} /64 - 1 \geq ℓ_{n} /128$ .

Extend the observed sample to an infinite independent sequence with law $P_{O}$ . Independently draw $N \sim Poisson (n /2), Z_{i} \sim iid Unif {1, 2, 3, 4}, i \geq 1,$ and define the uncapped stream sets $I_{t}^{⋆} = {i \leq N : Z_{i} = t}, t \in {1, 2, 3, 4} .$ Write $E_{⋆}$ and $Pr_{⋆}$ for expectation and probability under this joint experiment. For an observed record $o$ , define its stream histogram count by $K_{t, o}^{hist} = i \in I_{t}^{⋆} \sum 1 {O_{i} = o} .$ For $u_{t, o} \in [0, 1]$ , conditioning on $N$ gives the joint probability generating function $E_{⋆} [t = 1 \prod 4 o \in O \prod u_{t, o}^{K_{t, o}^{hist}}] = exp {m t = 1 \sum 4 o \in O \sum P_{O} ({o}) (u_{t, o} - 1)} .$ Its factorization shows that these histogram counts are independent Poisson variables with means $m P_{O} ({o})$ .

Evaluate the correction formulas of Algorithm 1 on the uncapped streams: $V_{j}^{⋆} C_{j}^{' ⋆} C_{j}^{⋆} U_{j}^{⋆} H_{j}^{⋆} D_{j}^{⋆} G_{j}^{⋆} = \frac{1}{m} i \in I_{2}^{⋆} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 0}, = i \in I_{3}^{⋆} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 1}, = i \in I_{4}^{⋆} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, R_{i} = 1}, = i \in I_{4}^{⋆} \sum 1 {(X_{i}, A_{i}, S_{i}) = j, Y_{i}^{obs} = 1}, = v = 1 \sum k - 1 a_{v} (U_{j}^{⋆} - C_{j}^{⋆} /2) (C_{j}^{⋆} - 1)_{v - 1}, = {U_{j}^{⋆} / C_{j}^{⋆} - 1/2, 0, C_{j}^{⋆} > 0, C_{j}^{⋆} = 0, = H_{j}^{⋆} 1 {C_{j}^{' ⋆} \leq B /4} + D_{j}^{⋆} 1 {C_{j}^{' ⋆} > B /4} .$ Define the linear term, aggregate correction, raw estimate, and projected ideal estimate by $τ_{lin} W_{corr} τ_{raw} τ_{⋆} = \frac{2}{m} i \in I_{1}^{⋆} \sum (2 A_{i} - 1) R_{i} (Y_{i}^{obs} - 1/2), = j \in J \sum ϵ_{j} V_{j}^{⋆} G_{j}^{⋆}, = τ_{lin} + 2 W_{corr}, = Π_{[- 1, 1]} (τ_{raw}) .$

The capped randomized estimate $τ$ in Algorithm 1 agrees with $τ_{⋆}$ when $N \leq n$ . On the complementary event their squared errors are bounded by four. Conditional Jensen and this coupling therefore give $E_{P} [(τ_{MM} - τ (P))^{2}] \leq E_{⋆} [(τ - τ (P))^{2}] \leq E_{⋆} [(τ_{⋆} - τ (P))^{2}] + 4 ⋆ Pr (N > n) .$ Exponential Markov, applied to $2^{N}$ , yields $⋆ Pr (N > n) \leq 2^{- n} E_{⋆} [2^{N}] = exp {- (lo g 2 - 1/2) n} \leq e^{- n /8} \leq \frac{8}{n} .$ Here $lo g 2 - 1/2 \geq 1/8$ , and $n /8 \leq e^{n /8}$ gives the last inequality. Consequently, $E_{P} [(τ_{MM} - τ (P))^{2}] \leq E_{⋆} [(τ_{⋆} - τ (P))^{2}] + \frac{32}{n} .$
All the correction statistics have finite second moments: their polynomial parts are finite polynomials in Poisson counts, and their ratio parts are bounded. Projection contraction and the variance–bias identity give $E_{⋆} [(τ_{⋆} - τ (P))^{2}] \leq Var_{⋆} (τ_{raw}) + {E_{⋆} [τ_{raw}] - τ (P)}^{2} .$ To bound the first term, define $K_{lin, +} K_{lin, -} = i \in I_{1}^{⋆} \sum 1 {R_{i} = 1, A_{i} = Y_{i}^{obs}}, = i \in I_{1}^{⋆} \sum 1 {R_{i} = 1, A_{i} \neq = Y_{i}^{obs}} .$ Then $τ_{lin} = \frac{K _{lin, +} - K _{lin, -}}{m} .$ Each count is Poisson with mean at most $m$ . Using $Var (U - V) \leq 2 Var (U) + 2 Var (V)$ , $Var_{⋆} (τ_{lin}) \leq \frac{4 m}{m ^{2}} = \frac{32}{n} .$ Applying the corresponding sum inequality to $τ_{raw} = τ_{lin} + 2 W_{corr}$ gives $Var_{⋆} (τ_{raw}) \leq \frac{64}{n} + 8 Var_{⋆} (W_{corr}) .$
For every $j \in J$ , define its arrived-count intensity and light-branch probability by $ζ_{j} = m t_{j} \geq 0, ℘_{j} = ⋆ Pr (C_{j}^{' ⋆} \leq B /4) \in [0, 1] .$ Poisson splitting gives $E_{⋆} [V_{j}^{⋆}] = w_{j}, E_{⋆} [(V_{j}^{⋆})^{2}] = w_{j}^{2} + \frac{w _{j}}{m},$ $C_{j}^{' ⋆}, C_{j}^{⋆} \sim Poisson (ζ_{j}), U_{j}^{⋆} ∣ C_{j}^{⋆} \sim Binomial (C_{j}^{⋆}, μ_{P} (j)) .$ The conditional binomial statement includes $t_{j} = 0$ : then both counts vanish almost surely and $μ_{P} (j) = 0$ .

For integers $v \geq 1$ , use the falling factorial $(C_{j}^{⋆})_{v} = t = 0 \prod v - 1 (C_{j}^{⋆} - t) .$ Conditional expectation of $U_{j}^{⋆}$ , followed by the Poisson factorial-moment identity, gives $E_{⋆} [(U_{j}^{⋆} - C_{j}^{⋆} /2) (C_{j}^{⋆} - 1)_{v - 1}] = η_{j} E_{⋆} [(C_{j}^{⋆})_{v}] = η_{j} ζ_{j}^{v} .$ Thus the coefficient identity in Algorithm 1 yields $E_{⋆} [H_{j}^{⋆}] = η_{j} {1 - Q_{k} (ζ_{j})} .$ Similarly, conditioning on $C_{j}^{⋆} > 0$ gives $E_{⋆} [D_{j}^{⋆}] = η_{j} ⋆ Pr (C_{j}^{⋆} > 0) = η_{j} (1 - e^{- ζ_{j}}) .$ Independence of the pilot stream from the fourth stream now implies $E_{⋆} [G_{j}^{⋆}] - η_{j} = - η_{j} {℘_{j} Q_{k} (ζ_{j}) + (1 - ℘_{j}) e^{- ζ_{j}}} .$ The first-stream mean and independence of the second stream from the pilot and fourth streams also give $E_{⋆} [τ_{lin}] = 2 j \in J \sum ϵ_{j} t_{j} η_{j}, E_{⋆} [V_{j}^{⋆} G_{j}^{⋆}] = w_{j} E_{⋆} [G_{j}^{⋆}] .$ Combining these identities with the cell decomposition of the target, $E_{⋆} [τ_{raw}] - τ (P) = 2 j \in J \sum ϵ_{j} w_{j} {E_{⋆} [G_{j}^{⋆}] - η_{j}} .$
We next derive the polynomial and pilot bounds used to control this bias. For $0 < z \leq B$ , the argument $1 - 2 z / B$ belongs to $[- 1, 1]$ , so the Chebyshev bound $∣ T_{k} (1 - 2 z / B) ∣ \leq 1$ gives $Q_{k} (z) \geq 0, z Q_{k} (z) = \frac{B { 1 - T _{k} ( 1 - 2 z / B )}}{2 k ^{2}} \leq \frac{B}{k ^{2}} .$ At $z = 0$ , the convention is $Q_{k} (0) = 1$ . The degree bound already established implies $\frac{B}{k ^{2}} \leq \frac{4194304}{ℓ _{n}} .$

For the second-moment estimates, define the coefficient norm of a polynomial $P (u)$ by $∥ P ∥_{coeff, 1} = v \geq 0 \sum ∣ [u^{v}] P ∣,$ where $[u^{v}] P$ denotes its coefficient of $u^{v}$ ; the sum is finite. Define the shifted Chebyshev polynomials by $P_{v} (u) = T_{v} (1 - 2 u), v \in N_{0} .$ Their recurrence and initial values give $P_{v + 1} (u) = 2 (1 - 2 u) P_{v} (u) - P_{v - 1} (u) (v \geq 1),$ $∥ P_{0} ∥_{coeff, 1} = 1, ∥ P_{1} ∥_{coeff, 1} = 3,$ $∥ P_{v + 1} ∥_{coeff, 1} \leq 6∥ P_{v} ∥_{coeff, 1} + ∥ P_{v - 1} ∥_{coeff, 1} .$ Induction therefore yields $∥ P_{v} ∥_{coeff, 1} \leq 7^{v} .$ Indeed, the induction step uses $6 \cdot 7^{v} + 7^{v - 1} \leq 7^{v + 1}$ . Since $Q_{k} (B u) = \frac{1 - P _{k} ( u )}{2 k ^{2} u},$ with the removable value at zero, deleting the zero constant term and dividing by $u$ cannot increase the coefficient norm. Hence $v = 1 \sum k - 1 ∣ a_{v} ∣ B^{v} \leq \frac{1 + 7 ^{k}}{2 k ^{2}} \leq 7^{k} \leq 8^{k} .$

On observed-law support, $0 \leq U_{j}^{⋆} \leq C_{j}^{⋆}$ , and $∣ (U_{j}^{⋆} - C_{j}^{⋆} /2) (C_{j}^{⋆} - 1)_{v - 1} ∣ \leq \frac{( C _{j}^{⋆} ) _{v}}{2} \leq \frac{( C _{j}^{⋆} ) ^{v}}{2} .$ For every $z \geq 0$ and $1 \leq v \leq k$ , $(z / B)^{v} \leq max {1, (z / B)^{k}} .$ The coefficient bound therefore gives the pointwise envelope $(H_{j}^{⋆})^{2} \leq \frac{6 4 ^{k}}{4} max {1, (\frac{C _{j}^{⋆}}{B})^{2 k}} \leq \frac{6 4 ^{k}}{4} {1 + (\frac{C _{j}^{⋆}}{B})^{2 k}} .$ For an integer $v \geq 0$ , expansion of an ordinary Poisson moment into factorial moments gives $E_{⋆} [(C_{j}^{⋆})^{v}] = t = 0 \sum v {t v} ζ_{j}^{t} \leq t = 0 \sum v (t v) v^{v - t} ζ_{j}^{t} = (ζ_{j} + v)^{v} .$ Here ${t v}$ counts partitions into $t$ nonempty blocks: choosing one representative per block and assigning the remaining elements gives ${t v} \leq (t v) v^{v - t}$ . The case $v = 0$ uses the constant zeroth moment. Integrating the pointwise envelope yields $E_{⋆} [(H_{j}^{⋆})^{2}] \leq \frac{6 4 ^{k}}{4} {1 + (\frac{ζ _{j} + 2 k}{B})^{2 k}} \leq \frac{6 4 ^{k}}{2} max {1, (\frac{ζ _{j} + 2 k}{B})^{2 k}} .$
When $ζ_{j} \leq B$ , the degree calibration gives $0 \leq \frac{ζ _{j} + 2 k}{B} \leq \frac{3}{2} \leq e^{1/2} .$ Consequently, $E_{⋆} [(H_{j}^{⋆})^{2}] \leq \frac{6 4 ^{k}}{2} e^{k} \leq e^{7 k} \leq e^{ℓ_{n} /8},$ where $6 4^{k} \leq e^{6 k}$ and $7 k \leq ℓ_{n} /8$ .

For $ζ_{j} \geq B$ , define $υ_{j} = \frac{ζ _{j} + 2 k}{B} .$ From $k \leq B /16384$ and $B \leq ζ_{j}$ , $2 k \leq ζ_{j}, k υ_{j} \leq \frac{ζ _{j}}{8192}, 6 k + 2 k υ_{j} \leq \frac{ζ _{j}}{8} .$ Using $υ_{j} \leq e^{υ_{j}}$ in the second-moment envelope gives $E_{⋆} [(H_{j}^{⋆})^{2}] \leq 6 4^{k} max {1, υ_{j}^{2 k}} \leq e^{6 k + 2 k υ_{j}} \leq e^{ζ_{j} /8} .$

Exponential Markov for the Poisson pilot count, using $4^{- C_{j}^{' ⋆}}$ and $4^{C_{j}^{' ⋆}}$ , respectively, gives $℘_{j} \leq exp {B lo g 4/4 - 3 ζ_{j} /4}, 1 - ℘_{j} \leq exp {3 ζ_{j} - B lo g 4/4} .$ Since $1 \leq lo g 4 \leq 2$ , for $ζ_{j} \geq B$ these imply $℘_{j} \leq e^{- ζ_{j} /4}, ℘_{j} E_{⋆} [(H_{j}^{⋆})^{2}] \leq e^{- ζ_{j} /8} .$ Also, for every $ζ_{j} \geq 0$ , $(1 - ℘_{j}) e^{- ζ_{j}} \leq e^{- B /16} .$ To see this, if $ζ_{j} \geq B /16$ , use $1 - ℘_{j} \leq 1$ . Otherwise, the upper-tail bound gives $(1 - ℘_{j}) e^{- ζ_{j}} \leq e^{2 ζ_{j} - B l o g 4/4} \leq e^{- B /16} .$

For $ζ_{j} \geq B$ , Cauchy–Schwarz and $℘_{j}^{2} \leq ℘_{j}$ yield ${℘_{j} ∣ E_{⋆} [H_{j}^{⋆}] ∣}^{2} \leq ℘_{j} E_{⋆} [(H_{j}^{⋆})^{2}] \leq e^{- ζ_{j} /8},$ and hence $℘_{j} ∣ E_{⋆} [H_{j}^{⋆}] ∣ \leq e^{- ζ_{j} /16} .$ Using $η_{j} Q_{k} (ζ_{j}) = η_{j} - E_{⋆} [H_{j}^{⋆}]$ , we obtain $℘_{j} ∣ η_{j} Q_{k} (ζ_{j}) ∣ \leq \frac{℘ _{j}}{2} + ℘_{j} ∣ E_{⋆} [H_{j}^{⋆}] ∣ \leq \frac{3}{2} e^{- B /16} .$ The pilot bias identity therefore gives, on these large-intensity cells, $∣ E_{⋆} [G_{j}^{⋆}] - η_{j} ∣ \leq 2 e^{- B /16} .$
We can now sum the bias. If $ζ_{j} = 0$ , then $t_{j} = 0$ , and $0 \leq w_{j} \leq 2 δ t_{j}$ forces $w_{j} = 0$ . Thus null arrived cells contribute zero to the weighted bias.

For $0 < ζ_{j} \leq B$ , polynomial nonnegativity and $w_{j} \leq 2 δ t_{j} = 2 δ ζ_{j} / m$ give $w_{j} ℘_{j} ∣ Q_{k} (ζ_{j}) ∣ \leq w_{j} Q_{k} (ζ_{j}) \leq \frac{2 δ}{m} \frac{B}{k ^{2}} \leq \frac{2 δ}{m} \frac{4194304}{ℓ _{n}} .$ There are $4 d$ cells in $J$ , so $j \in J ζ_{j} \leq B \sum w_{j} ℘_{j} ∣ Q_{k} (ζ_{j}) ∣ \leq 4 d \frac{2 δ}{m} \frac{4194304}{ℓ _{n}} = C_{bias} g_{n, d, q} .$ For a small-intensity cell, the pilot bias identity and $∣ η_{j} ∣ \leq 1/2$ give $2 w_{j} ∣ E_{⋆} [G_{j}^{⋆}] - η_{j} ∣ \leq w_{j} ℘_{j} ∣ Q_{k} (ζ_{j}) ∣ + w_{j} e^{- B /16} .$ For a large-intensity cell, the preceding bound gives $2 w_{j} ∣ E_{⋆} [G_{j}^{⋆}] - η_{j} ∣ \leq 4 w_{j} e^{- B /16} .$ Together, these yield the uniform cellwise bound $2 w_{j} ∣ E_{⋆} [G_{j}^{⋆}] - η_{j} ∣ \leq 1 {ζ_{j} \leq B} w_{j} ℘_{j} ∣ Q_{k} (ζ_{j}) ∣ + 4 w_{j} e^{- B /16} .$ The triangle inequality and $\sum_{j} w_{j} \leq δ$ therefore imply $∣ E_{⋆} [τ_{raw}] - τ (P) ∣ \leq C_{bias} g_{n, d, q} + 4 δ e^{- 16 ℓ_{n}} .$ The remainder satisfies $(4 δ e^{- 16 ℓ_{n}})^{2} = 16 δ^{2} e^{- 32 ℓ_{n}} \leq 4 e^{- 32 ℓ_{n}} \leq 4 e^{- ℓ_{n}} = \frac{4}{e + n} \leq \frac{4}{n} .$ Squaring the bias bound with $(u + v)^{2} \leq 2 u^{2} + 2 v^{2}$ gives ${E_{⋆} [τ_{raw}] - τ (P)}^{2} \leq 2 C_{bias}^{2} g_{n, d, q}^{2} + \frac{8}{n} \leq (2 C_{bias}^{2} + 8) r_{n, d, q} .$ Combining projection, the raw variance bound, and the capping penalty established above, $E_{P} [(τ_{MM} - τ (P))^{2}] \leq 8 Var_{⋆} (W_{corr}) + \frac{96}{n} + (2 C_{bias}^{2} + 8) r_{n, d, q} \leq 8 Var_{⋆} (W_{corr}) + (2 C_{bias}^{2} + 104) r_{n, d, q} .$
The histogram coordinates used by two distinct cells are disjoint. Their independence, together with $ϵ_{j}^{2} = 1$ , gives $Var_{⋆} (W_{corr}) = j \in J \sum Var_{⋆} (V_{j}^{⋆} G_{j}^{⋆}) .$ We first bound the ratio component.

Since $∣ D_{j}^{⋆} ∣ \leq 1/2$ , its variance is at most $1/4$ . Thus, when $ζ_{j} \leq 15$ , $Var_{⋆} (D_{j}^{⋆}) \leq \frac{1}{4} \leq \frac{4}{1 + ζ _{j}} .$ For $ζ_{j} > 15$ , define the arrived-success and arrived-failure fractions by $F_{j, +} = {U_{j}^{⋆} / C_{j}^{⋆}, 0, C_{j}^{⋆} > 0, C_{j}^{⋆} = 0, F_{j, -} = {(C_{j}^{⋆} - U_{j}^{⋆}) / C_{j}^{⋆}, 0, C_{j}^{⋆} > 0, C_{j}^{⋆} = 0.$ Then $D_{j}^{⋆} = \frac{F _{j, +} - F _{j, -}}{2} .$ Conditioning on the arrived count gives $E_{⋆} [(F_{j, +} - μ_{P} (j))^{2}] E_{⋆} [(F_{j, -} - (1 - μ_{P} (j)))^{2}] \leq ⋆ Pr (C_{j}^{⋆} = 0) + E_{⋆} [\frac{1 { C _{j}^{⋆} > 0 }}{C _{j}^{⋆}}], \leq ⋆ Pr (C_{j}^{⋆} = 0) + E_{⋆} [\frac{1 { C _{j}^{⋆} > 0 }}{C _{j}^{⋆}}] .$ On a positive count, the conditional binomial variance divided by the squared count is at most its reciprocal; on a zero count, the squared error is at most one.

For a Poisson count of intensity $ζ_{j}$ , the zero-safe reciprocal on the right is at most one. If $ζ_{j} \leq 1$ , this is at most $4/ (1 + ζ_{j})$ . If $ζ_{j} > 1$ , the pointwise bounds $1 {C_{j}^{⋆} = 0} + \frac{1 { C _{j}^{⋆} > 0 }}{C _{j}^{⋆}} \leq \frac{2}{C _{j}^{⋆} + 1}$ and the Poisson identity $E_{⋆} [\frac{1}{C _{j}^{⋆} + 1}] = \frac{1 - e ^{- ζ_{j}}}{ζ _{j}}$ give $⋆ Pr (C_{j}^{⋆} = 0) + E_{⋆} [\frac{1 { C _{j}^{⋆} > 0 }}{C _{j}^{⋆}}] \leq \frac{2}{ζ _{j}} \leq \frac{4}{1 + ζ _{j}} .$ The reciprocal identity has value one at $ζ_{j} = 0$ , by its continuous extension. Using the center $η_{j} = {μ_{P} (j) - (1 - μ_{P} (j))} /2$ , we conclude $Var_{⋆} (D_{j}^{⋆}) \leq E_{⋆} [(D_{j}^{⋆} - η_{j})^{2}] \leq \frac{1}{2} E_{⋆} [(F_{j, +} - μ_{P} (j))^{2}] + \frac{1}{2} E_{⋆} [(F_{j, -} - (1 - μ_{P} (j)))^{2}] \leq \frac{4}{1 + ζ _{j}} .$ Together with the small-intensity case, this holds for every cell.

The second and fourth streams are independent. Their first and second moments consequently give $Var_{⋆} (V_{j}^{⋆} D_{j}^{⋆}) = (w_{j}^{2} + \frac{w _{j}}{m}) Var_{⋆} (D_{j}^{⋆}) + \frac{w _{j}}{m} {E_{⋆} [D_{j}^{⋆}]}^{2} \leq \frac{4 w _{j}^{2}}{1 + ζ _{j}} + \frac{17 w _{j}}{4 m},$ where ${E_{⋆} [D_{j}^{⋆}]}^{2} \leq 1/4$ . Also, $\frac{w _{j}^{2}}{1 + m t _{j}} \leq \frac{2 δ}{m} w_{j}, j \in J \sum \frac{w _{j}^{2}}{1 + m t _{j}} \leq \frac{2 δ ^{2}}{m} .$ Since $δ + 2 δ^{2} \leq 1$ , $j \in J \sum (\frac{w _{j}}{m} + \frac{w _{j}^{2}}{1 + m t _{j}}) \leq \frac{1}{m} .$ Replacing the coefficient $4$ of the nonnegative quadratic term by $17/4$ therefore yields $j \in J \sum Var_{⋆} (V_{j}^{⋆} D_{j}^{⋆}) \leq \frac{17}{4 m} = \frac{34}{n} .$
Define the total switching second moment by $V_{switch} = j \in J \sum E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] .$ The identity $G_{j}^{⋆} - D_{j}^{⋆} = 1 {C_{j}^{' ⋆} \leq B /4} (H_{j}^{⋆} - D_{j}^{⋆})$ and independence of the second, third, and fourth streams imply $E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] = (w_{j}^{2} + \frac{w _{j}}{m}) ℘_{j} E_{⋆} [(H_{j}^{⋆} - D_{j}^{⋆})^{2}] .$ Since $(u - v)^{2} \leq 2 u^{2} + 2 v^{2}$ and $E_{⋆} [(D_{j}^{⋆})^{2}] \leq 1/4$ , $E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] \leq (w_{j}^{2} + \frac{w _{j}}{m}) {2 ℘_{j} E_{⋆} [(H_{j}^{⋆})^{2}] + \frac{℘ _{j}}{2}} .$

For $ζ_{j} \leq B$ , use $℘_{j} \leq 1$ , the light second-moment bound, and $w_{j} \leq 2 δ B / m$ . Since $e^{ℓ_{n} /8} \geq 1$ , this gives $E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] \leq 3 e^{ℓ_{n} /8} \frac{4 δ ^{2} B ^{2} + 2 δ B}{m ^{2}} .$ Summing over at most $4 d$ cells, $j \in J ζ_{j} \leq B \sum E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] \leq 12 d e^{ℓ_{n} /8} \frac{4 δ ^{2} B ^{2} + 2 δ B}{m ^{2}} .$

For $ζ_{j} > B$ , the pilot-weighted polynomial bound and $℘_{j} \leq e^{- ζ_{j} /4} \leq e^{- ζ_{j} /8}$ give $E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] \leq \frac{5}{2} (w_{j}^{2} + \frac{w _{j}}{m}) e^{- B /8} .$ Nonnegativity and $\sum_{j} w_{j} \leq δ$ imply $\sum_{j} w_{j}^{2} \leq δ^{2}$ . Hence $j \in J ζ_{j} > B \sum E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] \leq \frac{5}{2} (δ^{2} + \frac{δ}{m}) e^{- B /8} \leq \frac{25}{n} .$ For the last inequality, use $n \geq 1$ , $δ \leq 1$ , $δ / m \leq 8$ , and $e^{- B /8} = e^{- 32 ℓ_{n}} \leq e^{- ℓ_{n}} = \frac{1}{e + n} \leq \frac{1}{n} .$ Thus $V_{switch} \leq 12 d e^{ℓ_{n} /8} \frac{4 δ ^{2} B ^{2} + 2 δ B}{m ^{2}} + \frac{25}{n} .$

To convert the first term into the benchmark, define $Λ_{n} = \frac{e ^{ℓ_{n} /8} ℓ _{n}^{3}}{n} .$ Since $δ^{2} \leq δ$ , $ℓ_{n} \leq ℓ_{n}^{2}$ , and $B = 256 ℓ_{n}$ , $4 δ^{2} B^{2} + 2 δ B \leq 262656 δ ℓ_{n}^{2} .$ Substitution of $m = n /8$ gives the calibrated bound $12 d e^{ℓ_{n} /8} \frac{4 δ ^{2} B ^{2} + 2 δ B}{m ^{2}} \leq C_{switch} g_{n, d, q} Λ_{n}, C_{switch} = 12 \cdot 64 \cdot 262656.$ The sixth term of the exponential series yields $\frac{( 3 ℓ _{n} /4 ) ^{6}}{720} \leq e^{3 ℓ_{n} /4}, ℓ_{n}^{6} \leq 720 (4/3)^{6} e^{3 ℓ_{n} /4} .$ Since $e^{ℓ_{n}} = e + n \leq (e + 1) n$ , $Λ_{n}^{2} = \frac{e ^{ℓ_{n} /4} ℓ _{n}^{6}}{n ^{2}} \leq \frac{720 ( 4/3 ) ^{6} e ^{ℓ_{n}}}{n ^{2}} \leq \frac{C _{log}}{n} .$ Finally, the nonnegative square $(g_{n, d, q} - C_{switch} Λ_{n})^{2}$ gives $C_{switch} g_{n, d, q} Λ_{n} \leq \frac{g _{n, d, q}^{2}}{2} + \frac{C _{switch}^{2} Λ _{n}^{2}}{2} \leq \frac{g _{n, d, q}^{2}}{2} + \frac{C _{switch}^{2} C _{log}}{2 n} .$ Consequently, $V_{switch} \leq \frac{g _{n, d, q}^{2}}{2} + \frac{C _{switch}^{2} C _{log} /2 + 25}{n} .$
The decomposition $V_{j}^{⋆} G_{j}^{⋆} = V_{j}^{⋆} D_{j}^{⋆} + V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})$ and the variance sum inequality give $Var_{⋆} (V_{j}^{⋆} G_{j}^{⋆}) \leq 2 Var_{⋆} (V_{j}^{⋆} D_{j}^{⋆}) + 2 E_{⋆} [{V_{j}^{⋆} (G_{j}^{⋆} - D_{j}^{⋆})}^{2}] .$ Summing and using the two preceding bounds, $Var_{⋆} (W_{corr}) \leq \frac{68}{n} + 2 V_{switch} \leq g_{n, d, q}^{2} + \frac{C _{switch}^{2} C _{log} + 118}{n} \leq (C_{switch}^{2} C_{log} + 119) r_{n, d, q} .$ Substitution into the aggregate risk inequality yields $E_{P} [(τ_{MM} - τ (P))^{2}] \leq {8 (C_{switch}^{2} C_{log} + 119) + 2 C_{bias}^{2} + 104} r_{n, d, q} = C_{non} r_{n, d, q} \leq C_{U} r_{n, d, q} .$ Together with the complete-arrival and fallback branches, this establishes the asserted uniform bound for every admissible $n, d, q, P$ and the stated independent sample.

∎

The bound accommodates arbitrary cell-frequency imbalance within $M (d, q)$ . Its benchmark combines the sampling contribution $n^{- 1}$ with the squared missingness-weighted dimension scale and supplies the upper bounds for point estimation and honest intervals.

To describe the components of the estimation argument, fix a cell $j = (x, a, s)$ and write $p_{j} = P (X = x, A = a, S = s), b_{j} = P (X = x, A = a, S = s, R = 0),$ $θ_{j} = μ_{P} (x, a, s) - \frac{1}{2}, λ_{j} = m P (X = x, A = a, S = s, R = 1),$ where $m = n /8$ is the mean stream-size parameter in Algorithm 1. Here $p_{j}$ is total cell mass, $b_{j}$ is missing-outcome mass, $θ_{j}$ is the centered arrived-outcome mean, and $λ_{j}$ is the expected arrived count in one stream of the auxiliary Poisson experiment. These quantities are defined on null cells as well, using the conventions of Definition 5.

The scientific decomposition separates the treatment contrast into arrived outcomes and the outcomes represented by missing records. Centering at one half aligns the first-stream statistic with the centered cell means $θ_{j}$ ; balanced randomization gives the centered contrast the same population target. MAR identifies the mean needed for the missing component, while the second-stream statistic $V_{j}$ estimates its cell weight $b_{j}$ . The arrival floor controls the relation between missing and arrived cell mass, explaining why the additional error scale is weighted by $1 - q$ .

For sparsely observed cells, the polynomial statistic $H_{j}$ in Algorithm 1 supplies the correction through arrived-count moments. The polynomial $Q_{k}$ , its specified value at zero, and the falling-factorial convention are all fixed in that construction. The falling-factorial terms implement unbiased estimation of the polynomial terms in the auxiliary Poisson experiment. This use of polynomial approximation and unbiased moment estimation follows the methodological framework of Jiao et al. (2015); related polynomial constructions for discrete treatment-effect estimation appear in CausalSmith (2026); CausalSmith (2026). The light-cell component addresses aggregate missing-outcome correction when individual cell means have few arrived observations.

Cells selected as heavily populated use the centered ratio $D_{j}$ , with its specified zero-count value. The selection count $C_{j}^{'}$ comes from a separate stream from the counts $C_{j}, U_{j}$ used to form either correction. In the auxiliary Poisson experiment, this separation supports control of the selection rule together with the correction’s sampling variation. The thresholded statistic $G_{j}$ therefore joins polynomial approximation in light cells with ratio estimation in heavy cells.

Projection and conditional averaging turn the auxiliary construction into an observed-sample estimator in $[- 1, 1]$ without increasing squared error. The branch definitions and their full parameter ranges are stated once in Algorithm 1; Lemma 2 controls all of them with the same universal constant.

Honest clipped intervals

The uniform risk bound supplies a finite-sample confidence radius through Definition 13. Clipping the resulting interval to the treatment-effect range gives simultaneous coverage and length guarantees.

Lemma 3 [lem:honest-interval-construction] (Honest clipped confidence intervals).

Suppose that:

(Sample size and dimension.) $n, d$ are integers with $n, d \geq 1$ .

(Arrival floor.) $q \in [1/2, 1]$ .

(Noncoverage level.) $α \in (0, 1/2)$ .

(Uniform risk certificate.) $C_{U} > 0$ certifies the uniform squared-error bound $E_{P_{O}^{\otimes n}} [(τ_{MM} (O^{n}) - τ (P))^{2}] \leq C_{U} r_{n, d, q}$ for every $n, d \geq 1$ , every $q \in [1/2, 1]$ , and every $P \in M (d, q)$ , under any iid observed-sample law. Here $r_{n, d, q}$ is defined in Definition 12, and $τ (P) = E_{P} [Y (1) - Y (0)]$ is the population average treatment effect.

Let $I_{MM, α}$ and its radius $h_{n, d, q, α}$ be as in Definition 13, using this $C_{U}$ . The interval has uniform coverage: $P_{O}^{\otimes n} {τ (P) \in I_{MM, α} (O^{n})} \geq 1 - α for every P \in M (d, q) .$ For every observed sample $O^{n}$ , its length satisfies $length {I_{MM, α} (O^{n})} \leq min {2, 2 h_{n, d, q, α}} = min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} .$ Consequently, for every $P \in M (d, q)$ , $E_{P_{O}^{\otimes n}} [length {I_{MM, α} (O^{n})}] \leq min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} .$ If $h_{n, d, q, α} < 2$ , then for every $P \in M (d, q)$ , $P_{O}^{\otimes n} {τ (P) \in / I_{MM, α} (O^{n})} \leq α .$ If $h_{n, d, q, α} = 2$ , then for every $P \in M (d, q)$ and every observed sample $O^{n}$ , $τ (P) \in I_{MM, α} (O^{n}) .$

⊢ Lean

Proof of Lemma 3.

Fix the parameters in the statement. For every observed sample $o \in O^{n}$ , write the endpoints from Definition 13 as $L (o) = max {- 1, τ_{MM} (o) - h_{n, d, q, α}}, U (o) = min {1, τ_{MM} (o) + h_{n, d, q, α}} .$ The radius satisfies $0 \leq h_{n, d, q, α} = min {2, \frac{C _{U} r _{n, d, q}}{α}} \leq 2.$

The endpoint formulas give $L (o) \geq - 1, U (o) \leq 1,$ and $L (o) \geq τ_{MM} (o) - h_{n, d, q, α}, U (o) \leq τ_{MM} (o) + h_{n, d, q, α} .$ Subtracting yields both bounds $U (o) - L (o) \leq 2, U (o) - L (o) \leq 2 h_{n, d, q, α} .$ Consequently, $U (o) - L (o) \leq min {2, 2 h_{n, d, q, α}} .$ If $2 \leq C_{U} r_{n, d, q} / α$ , then the radius equals $2$ , and both sides of $min {2, 2 h_{n, d, q, α}} = min {2, 2 \frac{C _{U} r _{n, d, q}}{α}}$ equal $2$ . If $C_{U} r_{n, d, q} / α \leq 2$ , the identity follows by substituting that square root for the radius. This proves the pointwise length bound and its displayed equality.
We establish the target range used in the coverage argument. For a fixed $P \in M (d, q)$ , define $W_{P} = supp (P), p_{w} = P ({w}), Δ_{w} = Y (1) (w) - Y (0) (w) (w \in W_{P}) .$ The support is finite, and the binary potential outcomes give $p_{w} \geq 0, w \in W_{P} \sum p_{w} = 1, - 1 \leq Δ_{w} \leq 1.$ Thus $- p_{w} \leq p_{w} Δ_{w} \leq p_{w} .$ Summing these inequalities proves $- 1 = - w \in W_{P} \sum p_{w} \leq τ (P) = w \in W_{P} \sum p_{w} Δ_{w} \leq w \in W_{P} \sum p_{w} = 1.$
The estimator also satisfies $- 1 \leq τ_{MM} (o) \leq 1 (o \in O^{n}) .$ To derive this from Algorithm 1, first observe that, for every real $t$ , $- 1 \leq Π_{[- 1, 1]} (t) = max {- 1, min {1, t}} \leq 1 :$ the lower inequality follows from the maximum, and the upper inequality follows because both arguments of that maximum are at most $1$ . This establishes the range when $q = 1$ . When $q \neq = 1$ and $ℓ_{n} < 128$ or $d \geq n ℓ_{n}$ , the fallback branch is likewise a projection and has the same range.

For the remaining branch, define the Poisson weights and conditional stream averages by $ω_{N} = e^{- n /2} \frac{( n /2 ) ^{N}}{N !} (N \in N_{0}),$ $\overline{τ}_{N} (o) = \frac{1}{4 ^{N}} ζ \in {1, 2, 3, 4}^{N} \sum τ (o; N, ζ) (0 \leq N \leq n, o \in O^{n}),$ where $τ (o; N, ζ)$ is the projected randomized estimate in Algorithm 1 with count $N$ and stream assignment $ζ$ . There are $4^{N}$ assignments, including one empty assignment when $N = 0$ , and each estimate lies in $[- 1, 1]$ . Therefore $- 4^{N} \leq ζ \in {1, 2, 3, 4}^{N} \sum τ (o; N, ζ) \leq 4^{N}, - 1 \leq \overline{τ}_{N} (o) \leq 1.$ Moreover, $ω_{N} \geq 0, N = 0 \sum \infty ω_{N} = e^{- n /2} e^{n /2} = 1, N = 0 \sum n ω_{N} \leq 1.$ Since the randomized estimate equals zero when $N > n$ , this branch satisfies $τ_{MM} (o) = N = 0 \sum n ω_{N} \overline{τ}_{N} (o) .$ Multiplying the stream-average bounds by the nonnegative weights and summing gives $- 1 \leq - N = 0 \sum n ω_{N} \leq τ_{MM} (o) \leq N = 0 \sum n ω_{N} \leq 1.$

In particular, if $h_{n, d, q, α} = 2$ , the target and estimator ranges imply $τ_{MM} (o) - 2 \leq - 1 \leq τ (P), τ (P) \leq 1 \leq τ_{MM} (o) + 2.$ Taking the maximum in the lower endpoint and the minimum in the upper endpoint yields $L (o) \leq τ (P) \leq U (o) (P \in M (d, q), o \in O^{n}) .$
Suppose now that $h_{n, d, q, α} < 2$ , and fix $P \in M (d, q)$ . Define the sample probability measure and squared-error function by $μ_{obs} = P_{O}^{\otimes n}, E_{P} (o) = (τ_{MM} (o) - τ (P))^{2} (o \in O^{n}) .$ If $C_{U} r_{n, d, q} / α \leq 2$ , the radius definition gives $h_{n, d, q, α} = C_{U} r_{n, d, q} / α$ . If that square root exceeds $2$ , the radius equals $2$ , contradicting the present case. Hence $h_{n, d, q, α} = \frac{C _{U} r _{n, d, q}}{α}, h_{n, d, q, α}^{2} = \frac{C _{U} r _{n, d, q}}{α} .$ By Definition 12 and $n \geq 1$ , $r_{n, d, q} \geq \frac{1}{n} > 0.$ Together with $C_{U} > 0$ and $α > 0$ , this proves $h_{n, d, q, α} > 0, h_{n, d, q, α}^{2} > 0, C_{U} r_{n, d, q} = α h_{n, d, q, α}^{2} .$

Define the noncoverage and squared-error tail events by $B_{P} = {o \in O^{n} : τ (P) \in / [L (o), U (o)]}, T_{P} = {o \in O^{n} : h_{n, d, q, α}^{2} \leq E_{P} (o)} .$ We claim that $B_{P} \subseteq T_{P} .$ Indeed, noncoverage gives either $τ (P) < L (o)$ or $U (o) < τ (P)$ . In the first case, if $- 1 \leq τ_{MM} (o) - h_{n, d, q, α}$ , then $L (o) = τ_{MM} (o) - h_{n, d, q, α}, h_{n, d, q, α} < τ_{MM} (o) - τ (P) .$ Otherwise $L (o) = - 1$ , contradicting $τ (P) \geq - 1$ . In the second case, if $τ_{MM} (o) + h_{n, d, q, α} \leq 1$ , then $U (o) = τ_{MM} (o) + h_{n, d, q, α}, h_{n, d, q, α} < τ (P) - τ_{MM} (o) .$ Otherwise $U (o) = 1$ , contradicting $τ (P) \leq 1$ . Squaring the positive inequalities in the two possible cases gives $h_{n, d, q, α}^{2} \leq (τ_{MM} (o) - τ (P))^{2},$ as claimed.

The sample space is finite, so the squared-error function is integrable. Its nonnegativity and Markov’s inequality give $h_{n, d, q, α}^{2} μ_{obs} (T_{P}) \leq \int E_{P} (o) d μ_{obs} (o) .$ Applying the assumed uniform risk certificate to this iid sample law, and using event inclusion, yields $h_{n, d, q, α}^{2} μ_{obs} (B_{P}) \leq h_{n, d, q, α}^{2} μ_{obs} (T_{P}) \leq \int E_{P} (o) d μ_{obs} (o) \leq C_{U} r_{n, d, q} = α h_{n, d, q, α}^{2} .$ Dividing by the strictly positive squared radius proves $P_{O}^{\otimes n} {τ (P) \in / I_{MM, α} (O^{n})} \leq α .$
To obtain honesty, fix any $P \in M (d, q)$ and split according to whether $h_{n, d, q, α} = 2$ . In that case, the pointwise inclusion proved above gives $P_{O}^{\otimes n} {τ (P) \in I_{MM, α} (O^{n})} = 1 \geq 1 - α .$ In the other case, $h_{n, d, q, α} \leq 2$ implies $h_{n, d, q, α} < 2$ . The coverage event is measurable, and the preceding noncoverage bound therefore gives $P_{O}^{\otimes n} {τ (P) \in I_{MM, α} (O^{n})} = 1 - P_{O}^{\otimes n} {τ (P) \in / I_{MM, α} (O^{n})} \geq 1 - α .$ Since $P$ was arbitrary, the interval has the asserted uniform coverage.
Finally, the estimator range and nonnegative radius ensure that the endpoints form a nonempty interval, so $0 \leq length {I_{MM, α} (o)} = U (o) - L (o) .$ These functions are integrable on the finite sample space. Integrating the pointwise bound from the first step under the probability measure $P_{O}^{\otimes n}$ gives $E_{P_{O}^{\otimes n}} [length {I_{MM, α} (O^{n})}] \leq \int min {2, 2 h_{n, d, q, α}} d P_{O}^{\otimes n} = min {2, 2 h_{n, d, q, α}} = min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} .$ This holds for every $P \in M (d, q)$ .

∎

For a radius below two, the squared-error bound supports the uniform noncoverage bound through Markov’s inequality. At radius two, the interval equals the entire treatment-effect range because its center belongs to $[- 1, 1]$ . Endpoint clipping preserves inclusion of a target in that range. These two branches yield the finite-sample coverage requirement in Definition 10.

The interval’s radius bounds its length by twice that radius, while the treatment-effect range bounds it by two. This deterministic cap and Lemma 2 give the constructive expected-length bound in Theorem 2.

Normalized priors and the dimension lower bound

The full-range converse uses two branches. When the squared arrival-weighted dimension scale is at least $n^{- 1}$ , paired-label priors over admissible causal laws have close observed-sample distributions and separated population treatment effects. Signed interpolation weights coordinate opposite orientations within each pair, and a fixed filler label normalizes every latent draw. When that squared scale is below $n^{- 1}$ , the parametric floors supply the required lower bounds. Together, the normalized prior comparison and parametric floors establish lower bounds across the full parameter range on the complete observed-record experiment used by Definitions 9 and 11.

Polynomial approximation and moment matching provide the general tools for constructing such mixture comparisons (Wu et al., 2016; Wu et al., 2020). Here their implementation incorporates the randomized-MAR restrictions directly into the observed atom probabilities. The following construction collects the interpolation scheme, latent distribution, normalized causal laws, and auxiliary count experiment.

Definition 14 [def:paired-prior-handle] (Normalized paired prior construction).

The paired-prior handle consists of the normalized priors $Π_{-}, Π_{+}$ , their observed-sample mixtures $Q_{-}^{(n)}, Q_{+}^{(n)}$ , their associated unnormalized count laws, a fixed fallback record $o_{\circ}$ , and the count-ordering kernel $κ_{n}$ , constructed below for parameters satisfying:

(Sample size.) $n$ is an integer with $n \geq 1$ .

(Baseline dimension.) $d$ is an integer with $d \geq 1$ .

(Arrival floor.) $q \in [1/2, 1]$ .

The observed-record space $O$ consists of tuples $(X, A, S, R, R Y)$ , with $X$ taking values in a fixed set of $d$ baseline labels and the remaining coordinates binary. Fix $o_{\circ} \in O$ .

Set $δ = 1 - q, L = lo g (e + n), K = ⌈ 8 L ⌉, h = K^{- 2}, m = K - 1, B_{0} = \frac{K}{1024 n},$ $M = min {⌊ \frac{d - 1}{2} ⌋, ⌊ n L ⌋}, c_{0} = \frac{1}{16}, b = 1 - \frac{δ}{2}, μ_{0} = \frac{b ^{2}}{2 q} .$ For $0 \leq i \leq m$ , define the interpolation nodes and their Lagrange cardinal polynomials by $x_{i} = \frac{1 + h}{2} + \frac{1 - h}{2} cos \frac{iπ}{m}, l_{i} (t) = 0 \leq t^{'} \leq m t^{'} \neq = i \prod \frac{t - x _{t^{'}}}{x _{i} - x _{t^{'}}} .$ Set $D = i = 0 \sum m ∣ l_{i} (0) ∣, ν_{i} = \frac{l _{i} ( 0 )}{D} .$ The latent pair $(p, z) \in [0, B_{0}] \times {- 1, 1}$ has distribution $Pr {(p, z) = (B_{0} x_{i}, sign (ν_{i}))} = \frac{h ∣ ν _{i} ∣}{x _{i}}, 0 \leq i \leq m,$ $Pr {(p, z) = (0, 1)} = 1 - i = 0 \sum m \frac{h ∣ ν _{i} ∣}{x _{i}} .$ Draw independent copies $(p_{j}, z_{j})$ , $1 \leq j \leq M$ , and independent fair orientation signs, independent also of these copies, with $Pr (r_{j} = 1) = Pr (r_{j} = - 1) = \frac{1}{2} .$

For each $σ \in {- 1, 1}$ , pair $j$ consists of two distinct baseline labels, each with unnormalized mass $p_{j}$ , with orientations $u \in {r_{j}, - r_{j}} .$ At each label, $X$ equals that label, and the potential surrogates and control outcome satisfy $S (0) = S (1) = 0, Y (0) = 0.$ Treatment $A$ is an independent fair coin, and control arrival is complete. The treated arrival probability and treated outcome mean are $ρ_{σ, j, u} = 1 - \frac{δ}{2} (1 + σ z_{j} u), μ_{σ, j, u} = \frac{b /2 + c _{0} u}{ρ _{σ, j, u}} .$ Draw $Y (1)$ as a Bernoulli variable with mean $μ_{σ, j, u}$ , and draw treated arrival independently of $Y (1)$ with probability $ρ_{σ, j, u}$ . In the coordinate order $(A, R, R Y) = (0, 1, 0), (1, 0, 0), (1, 1, 1), (1, 1, 0),$ the four observed atom coefficients at orientation $u$ are $v_{σ} (z_{j}, u) = (\frac{1}{2}, \frac{δ ( 1 + σ z _{j} u )}{4}, \frac{b}{4} + \frac{c _{0} u}{2}, \frac{b}{4} - \frac{c _{0} u}{2} - \frac{σ δ z _{j} u}{4}) .$ The two orientations specify the complete eight-coordinate observed atom vector for pair $j$ .

Add one distinct fixed filler label with unnormalized mass $f = 1 - 2 M h B_{0} .$ At this label, set $S (0) = S (1) = 0, Y (0) = 0,$ let treatment be an independent fair coin, make arrival complete in both treatment arms, and draw $Y (1)$ as a Bernoulli variable with mean $μ_{0}$ . Its observed atom coefficients, in the same coordinate order, are $v_{fill} = (\frac{1}{2}, 0, \frac{μ _{0}}{2}, \frac{1 - μ _{0}}{2}) .$ At every label, the realized variables and observed outcome mark satisfy $S = S (A), Y = Y (A), R Y = R Y .$

Normalize the label masses by $J = f + 2 j = 1 \sum M p_{j}, f ⟼ \frac{f}{J}, p_{j} ⟼ \frac{p _{j}}{J}$ for each of the two labels in pair $j$ . Let $P_{σ}$ be the resulting normalized causal law and $P_{σ, O}$ its observed-law image. Define the prior and complete observed-sample mixture by $Π_{σ} = Law (P_{σ}), Q_{σ}^{(n)} = \int P_{σ, O}^{\otimes n} d Π_{σ} (P_{σ}) .$

For the associated unnormalized count experiment, set $λ = 4 n .$ Conditional on the latent variables, assign independent Poisson counts to the eight atoms of each pair and the filler atoms, with respective mean vectors $λ p_{j} v_{σ} (z_{j}, r_{j}), λ p_{j} v_{σ} (z_{j}, - r_{j}), λ f v_{fill} .$ All other observed atoms have count zero. The associated count law is the mixture of this conditional count experiment over the latent draws.

Define the Markov kernel $κ_{n}$ by uniformly ordering the counted multiset and returning its first $n$ records when the total count is at least $n$ ; otherwise it returns $(o_{\circ}, \dots, o_{\circ}) \in O^{n} .$ The kernel $κ_{n}$ is independent of $σ$ and of every latent variable.

⊢ Lean

The restrictions defining Definition 6 are built into Definition 14. Each pair uses two labels, and the filler uses one, respecting the baseline-support bound. Independent fair treatment supplies randomized independence and balanced allocation. The potential surrogates are constant, and arrival is drawn independently of the treated potential outcome conditional on the label. Together with complete control arrival and the stipulated realization of the potential measurements, these choices supply consistency and MAR. Treated arrival takes values $q$ and $1$ ; the outcome means and observed atom coefficients are valid throughout the stated range of the arrival floor.

The opposite orientations serve complementary roles. They preserve a common total unnormalized mass for each pair while placing the sign-dependent arrival perturbation in both labels’ observed distributions. Keeping the full eight-coordinate vector accounts jointly for control records, missing treated outcomes, arrived treated successes, and arrived treated failures at the two labels. Thus the mixture comparison concerns the complete observed record. The arrival deficit $δ$ , defined in Definition 14, also governs the attenuation of the treatment-effect perturbation.

Exact normalization is central to this construction. The filler mass is fixed across latent draws and signs, whereas the total mass $J$ varies with the latent label masses. Dividing all label masses by that same total produces a probability law for every draw while preserving the conditional randomization and arrival restrictions. The normalized priors $Π_{-}, Π_{+}$ and complete sample mixtures $Q_{-}^{(n)}, Q_{+}^{(n)}$ in Definition 14 therefore belong to the causal model and its original sampling experiment.

The converse argument has three components. First, the interpolation weights support a comparison of the auxiliary Poisson mixtures, using the approximation and moment-matching tools developed in Wu et al. (2016) and the Poisson-mixture framework described by Wu et al. (2020). Second, the count-ordering transformation in Definition 14 connects this comparison to samples from the normalized laws. Its independence from the sign and latent variables makes it a common statistical transformation for both alternatives; the fixed fallback specifies its output for every count realization. Third, concentration of the treatment effects under the priors supplies separation around a deterministic center. The same-experiment normalization and the attenuation by the arrival deficit are the construction-specific ingredients linking these components to the randomized-MAR model.

The resulting statement fixes the comparison tolerance $β \in (0, 1/4)$ before ranging over the sample size, dimension, and arrival floor. Its regime requires the squared missingness-and-dimension scale to be at least the sampling scale.

Theorem 3 [thm:normalized-converse] (Normalized priors with separated effects).

For every fixed $β \in (0, 1/4)$ , there exists a constant $c_{β} > 0$ such that the following holds for every sample size $n$ , baseline-support bound $d$ , and arrival floor $q$ satisfying:

(Sample size and dimension.) $n, d$ are integers with $n, d \geq 1$ .

(Arrival floor.) $q \in [1/2, 1]$ .
(Separation scale.) The scale $g_{n, d, q} = (1 - q) min {1, \frac{d}{n lo g ( e + n )}}$ satisfies $g_{n, d, q}^{2} \geq n^{- 1}$ .

There exist discrete probability priors $Π_{-}$ and $Π_{+}$ supported on $M (d, q)$ from Definition 6, whose laws satisfy Assumptions 2, 3, 4, 5, and 6. Their complete observed-sample mixtures, defined by $Q_{-}^{(n)} = \int P_{O}^{\otimes n} Π_{-} (d P), Q_{+}^{(n)} = \int P_{O}^{\otimes n} Π_{+} (d P),$ where $P_{O}$ is the observed-law image of the full-data law $P$ , satisfy $TV (Q_{-}^{(n)}, Q_{+}^{(n)}) = B \subseteq O^{n} sup Q_{-}^{(n)} (B) - Q_{+}^{(n)} (B) \leq β .$ Here $O^{n}$ is the complete observed-record sample space, and the supremum is over measurable events. There also exists a deterministic center $m_{0} \in R$ such that, for the population average treatment effect $τ (P) = E_{P} [Y (1) - Y (0)],$ where $Y (1)$ and $Y (0)$ are the binary potential outcomes, $Π_{-} {P : τ (P) \leq m_{0} - c_{β} g_{n, d, q}} \geq 1 - β, Π_{+} {P : m_{0} + c_{β} g_{n, d, q} \leq τ (P)} \geq 1 - β .$

⊢ Lean

The statistical content of Theorem 3 is the coexistence of observational proximity and target separation. Every event in the complete observed sample has probabilities differing by at most the fixed tolerance, while each prior places at least $1 - β$ probability on its respective side of the deterministic center. Many small baseline masses carry the signed perturbations; their aggregate effect yields separation at the missingness-and-dimension scale. The factor $1 - q$ records how that separation contracts as arrival becomes complete.

The positive separation constant $c_{β}$ in Theorem 3 may depend on the fixed tolerance and is uniform over the parameter triples satisfying the theorem’s conditions. In the dimension-dominated regime $g_{n, d, q}^{2} \geq n^{- 1}$ , the theorem supplies the prior comparison underlying the dimension terms in the estimation and honest-length bounds of Theorems 1 and 2. Its two probability guarantees keep the observed-mixture comparison and the concentration of the population effects distinct, providing the inputs for the testing reductions.

Testing reductions and proofs of the main results

The normalized comparison in Theorem 3 supplies separated treatment effects under nearby observed-sample mixtures. The auxiliary results below translate that comparison into lower bounds for squared-error risk and honest expected interval length. A parametric subexperiment supplies the sampling floors throughout the parameter range, while the normalized priors supply the dimension contribution under their stated regime condition.

Parametric sampling floors

A one-label, complete-arrival Bernoulli subexperiment belongs to $M (d, q)$ , the law class in Definition 6, for every $d \geq 1$ and $q \in [1/2, 1]$ . Its sampling uncertainty supplies the parametric component of both statistical criteria. The underlying two-hypothesis testing comparison is standard (Tsybakov, 2009). The following statement records the resulting floors uniformly over the support bound and arrival floor.

Lemma 4 [lem:parametric-floor-infrastructure] (Parametric risk and length floors).

There exists a universal constant $c_{0} > 0$ such that, for every pair of positive integers $n, d$ and every $q \in [1/2, 1]$ , the minimax squared-error risk $R_{n, d, q}^{*}$ defined in Definition 9 satisfies $R_{n, d, q}^{*} \geq \frac{c _{0}}{n} .$ For each noncoverage level $α \in (0, 1/2)$ , there exists a constant $c_{0, α} > 0$ , depending only on $α$ , such that, for every pair of positive integers $n, d$ and every $q \in [1/2, 1]$ , the minimax worst-law expected honest interval length $L_{n, d, q, α}^{*}$ defined in Definition 11 satisfies $L_{n, d, q, α}^{*} \geq \frac{c _{0, α}}{n} .$

⊢ Lean

Proof of Lemma 4.

Fix positive integers $n, d$ and $q \in [1/2, 1]$ .

Risk calibration. Define $a_{risk} := min {\frac{1}{4}, \frac{lo g 2}{4}}, u_{risk} := \frac{a _{risk}}{n}, c_{0} := \frac{a _{risk}^{2}}{16} .$ Since $lo g 2 > 0$ , $0 < a_{risk} \leq \frac{1}{4}, a_{risk}^{2} \leq \frac{lo g 2}{16}, c_{0} > 0.$ Moreover, $n \geq 1$ implies $n \geq 1$ and $(n)^{2} = n$ . Consequently, $0 < u_{risk} \leq \frac{1}{4}, n u_{risk}^{2} = a_{risk}^{2}, 16 n u_{risk}^{2} \leq lo g 2.$ Thus the same positive constant $a_{risk}$ meets this budget for every positive sample size.
A one-cell pair. For each parameter $θ \in [0, 1]$ , define a full-data law $P_{θ}$ by $X = 0, S (0) = S (1) = 0, Y (0) = 0, R = 1 almost surely, A \sim Bernoulli (1/2), Y (1) \sim Bernoulli (θ), A ⊥ Y (1), (S, Y) = (S (A), Y (A)), Q_{θ} := (P_{θ})_{O} .$ The label $0$ is available because $d \geq 1$ . The construction gives randomized treatment independence, balanced assignment, and consistency. Since $R = 1$ , outcome arrival is conditionally independent of $Y$ , and every occupied cell has arrival probability one. Hence the requirements in Definition 6 are satisfied: $P_{θ} \in M (d, q), τ (P_{θ}) = E_{P_{θ}} {Y (1) - Y (0)} = θ .$ The observed law has exactly the following possible nonzero masses: $Q_{θ} {(0, 0, 0, 1, 0)} Q_{θ} {(0, 1, 0, 1, 0)} Q_{θ} {(0, 1, 0, 1, 1)} = \frac{1}{2}, = \frac{1 - θ}{2}, = \frac{θ}{2},$ and assigns mass zero to every other record.

Define the risk pair by $P_{risk, 0} := P_{1/2}, P_{risk, 1} := P_{1/2 + u_{risk}}, Q_{risk, ι} := (P_{risk, ι})_{O} (ι \in {0, 1}) .$ Both parameters belong to $[0, 1]$ , and $τ (P_{risk, 0}) = \frac{1}{2}, τ (P_{risk, 1}) = \frac{1}{2} + u_{risk}, Q_{risk, 1} ≪ Q_{risk, 0} .$ For this finite, absolutely continuous pair, the chi-square divergence is $χ^{2} (Q_{risk, 1} ∥ Q_{risk, 0}) := o \in O Q_{risk, 0} {o} > 0 \sum \frac{( Q _{risk, 1} { o } - Q _{risk, 0} { o } ) ^{2}}{Q _{risk, 0} { o }} .$ In sums over the entire space, a summand with zero denominator is assigned zero; absolute continuity makes its numerator zero as well. Expanding the square and using that both laws have total mass one gives $1 + χ^{2} (Q_{risk, 1} ∥ Q_{risk, 0}) = o \in O \sum \frac{Q _{risk, 1} { o } ^{2}}{Q _{risk, 0} { o }} = \frac{1}{2} + (\frac{1}{2} - u_{risk})^{2} + (\frac{1}{2} + u_{risk})^{2} = 1 + 2 u_{risk}^{2} .$ In particular, $χ^{2} (Q_{risk, 1} ∥ Q_{risk, 0}) = 2 u_{risk}^{2} \leq 16 u_{risk}^{2} .$
Product total variation. We use total variation with the convention $TV (Q_{risk, 1}^{\otimes n}, Q_{risk, 0}^{\otimes n}) = E \subseteq O^{n} sup Q_{risk, 1}^{\otimes n} (E) - Q_{risk, 0}^{\otimes n} (E) .$ Absolute continuity is preserved by these finite products. Factoring the finite sum of squared product masses divided by reference masses yields $1 + χ^{2} (Q_{risk, 1}^{\otimes n} ∥ Q_{risk, 0}^{\otimes n}) = {1 + χ^{2} (Q_{risk, 1} ∥ Q_{risk, 0})}^{n} .$ The inequality $1 + t \leq e^{t}$ for $t \geq 0$ , followed by the one-record bound, therefore gives $1 + χ^{2} (Q_{risk, 1}^{\otimes n} ∥ Q_{risk, 0}^{\otimes n}) \leq exp {n χ^{2} (Q_{risk, 1} ∥ Q_{risk, 0})} \leq exp (16 n u_{risk}^{2}),$ so $χ^{2} (Q_{risk, 1}^{\otimes n} ∥ Q_{risk, 0}^{\otimes n}) \leq exp (16 n u_{risk}^{2}) - 1.$ On a finite space, total variation equals half the sum of the absolute mass differences. Applying Cauchy–Schwarz to that sum, with the reference masses as weights, gives $TV (Q_{risk, 1}^{\otimes n}, Q_{risk, 0}^{\otimes n}) \leq \frac{1}{2} χ^{2} (Q_{risk, 1}^{\otimes n} ∥ Q_{risk, 0}^{\otimes n}) \leq \frac{1}{2} exp (16 n u_{risk}^{2}) - 1 .$ Finally, the calibrated budget implies $exp (16 n u_{risk}^{2}) \leq e^{l o g 2} = 2, TV (Q_{risk, 1}^{\otimes n}, Q_{risk, 0}^{\otimes n}) \leq \frac{1}{2} .$
The squared-error lower bound. The estimator class in Definition 8 is nonempty, since it contains $T_{zero} (o) := 0 (o \in O^{n}) .$ Fix $T \in T_{n}$ , and define its two error events by $E_{risk, ι} := {o \in O^{n} : \frac{u _{risk}}{2} \leq ∣ T (o) - τ (P_{risk, ι}) ∣}, ι \in {0, 1} .$ The targets are separated by $u_{risk}$ . The triangle inequality therefore gives $E_{risk, 0}^{c} \subseteq E_{risk, 1} .$ Using this inclusion and the total-variation bound, $Q_{risk, 0}^{\otimes n} (E_{risk, 0}) + Q_{risk, 1}^{\otimes n} (E_{risk, 1}) \geq Q_{risk, 0}^{\otimes n} (E_{risk, 0}) + Q_{risk, 0}^{\otimes n} (E_{risk, 1}) - TV (Q_{risk, 0}^{\otimes n}, Q_{risk, 1}^{\otimes n}) \geq \frac{1}{2} .$ Consequently, $ι \in {0, 1} max Q_{risk, ι}^{\otimes n} (E_{risk, ι}) \geq \frac{1}{4} .$ For each $ι \in {0, 1}$ , nonnegativity of squared error gives the threshold bound $(\frac{u _{risk}}{2})^{2} Q_{risk, ι}^{\otimes n} (E_{risk, ι}) \leq E_{Q_{risk, ι}^{\otimes n}} [{T - τ (P_{risk, ι})}^{2}] .$ If the error probability under the first law is at most that under the second, then $E_{Q_{risk, 1}^{\otimes n}} [{T - τ (P_{risk, 1})}^{2}] \geq (\frac{u _{risk}}{2})^{2} \frac{1}{4} = \frac{u _{risk}^{2}}{16} .$ If that ordering is reversed, the corresponding bound is $E_{Q_{risk, 0}^{\otimes n}} [{T - τ (P_{risk, 0})}^{2}] \geq (\frac{u _{risk}}{2})^{2} \frac{1}{4} = \frac{u _{risk}^{2}}{16} .$ Thus, in either case, $ι \in {0, 1} max E_{Q_{risk, ι}^{\otimes n}} [{T - τ (P_{risk, ι})}^{2}] \geq \frac{u _{risk}^{2}}{16} .$

For every $P \in M (d, q)$ , binary potential outcomes imply $- 1 \leq Y (1) - Y (0) \leq 1, - 1 \leq τ (P) \leq 1.$ Since $T$ also takes values in $[- 1, 1]$ , $0 \leq E_{P_{O}^{\otimes n}} {T - τ (P)}^{2} \leq 4.$ The worst-law supremum therefore exists as a finite real number and dominates the risks at both constructed laws. Taking the estimator infimum in Definition 9 gives $R_{n, d, q}^{*} \geq \frac{u _{risk}^{2}}{16} = \frac{a _{risk}^{2}}{16 n} = \frac{c _{0}}{n} .$
Coverage-dependent calibration. Fix $α \in (0, 1/2)$ , and define $b_{cov} := 1 - 2 α, a_{len} := min {\frac{1}{4}, \frac{lo g ( 1 + b _{cov}^{2} )}{4}}, c_{0, α} := \frac{a _{len} b _{cov}}{2} .$ Here $b_{cov} > 0, lo g (1 + b_{cov}^{2}) > 0, 0 < a_{len} \leq \frac{1}{4}, c_{0, α} > 0.$ The minimum also gives $a_{len}^{2} \leq \frac{lo g ( 1 + b _{cov}^{2} )}{16} .$ Define $u_{len} := \frac{a _{len}}{n} .$ As before, $n \geq 1$ and $(n)^{2} = n$ , so $0 < u_{len} \leq \frac{1}{4}, n u_{len}^{2} = a_{len}^{2}, 16 n u_{len}^{2} \leq lo g (1 + b_{cov}^{2}) .$ Both $a_{len}$ and $c_{0, α}$ depend only on $α$ .
The interval pair and its total variation. Using the same one-cell family, define $P_{len, 0} := P_{1/2}, P_{len, 1} := P_{1/2 + u_{len}}, Q_{len, ι} := (P_{len, ι})_{O} (ι \in {0, 1}) .$ The construction and the same three-atom calculation give $P_{len, 0}, P_{len, 1} \in M (d, q), τ (P_{len, 0}) = \frac{1}{2}, τ (P_{len, 1}) = \frac{1}{2} + u_{len}, Q_{len, 1} ≪ Q_{len, 0}, χ^{2} (Q_{len, 1} ∥ Q_{len, 0}) = 2 u_{len}^{2} \leq 16 u_{len}^{2} .$ The product calculation above applies to this pair. The new budget gives $exp (16 n u_{len}^{2}) \leq exp {lo g (1 + b_{cov}^{2})} = 1 + b_{cov}^{2} .$ Using symmetry of total variation and $b_{cov} > 0$ , $TV (Q_{len, 0}^{\otimes n}, Q_{len, 1}^{\otimes n}) = TV (Q_{len, 1}^{\otimes n}, Q_{len, 0}^{\otimes n}) \leq \frac{1}{2} exp (16 n u_{len}^{2}) - 1 \leq \frac{1}{2} b_{cov}^{2} = \frac{b _{cov}}{2} = \frac{1 - 2 α}{2} .$
Coverage forces expected length. Fix $I \in C_{α} (n, d, q)$ , with endpoints as in Definition 10, and define $E_{cov, ι} := {o \in O^{n} : τ (P_{len, ι}) \in [L (o), U (o)]}, ι \in {0, 1} .$ Honesty gives $Q_{len, 0}^{\otimes n} (E_{cov, 0}) \geq 1 - α, Q_{len, 1}^{\otimes n} (E_{cov, 1}) \geq 1 - α .$ All these events are measurable because the sample space is finite. The definition of total variation gives $Q_{len, 0}^{\otimes n} (E_{cov, 1}) - Q_{len, 1}^{\otimes n} (E_{cov, 1}) \leq \frac{b _{cov}}{2},$ and hence $Q_{len, 0}^{\otimes n} (E_{cov, 1}) \geq 1 - α - \frac{b _{cov}}{2} .$ Taking complements, $Q_{len, 0}^{\otimes n} (E_{cov, 0}^{c}) \leq α, Q_{len, 0}^{\otimes n} (E_{cov, 1}^{c}) \leq α + \frac{b _{cov}}{2} .$ The union bound therefore yields $Q_{len, 0}^{\otimes n} (E_{cov, 0} \cap E_{cov, 1}) = 1 - Q_{len, 0}^{\otimes n} (E_{cov, 0}^{c} \cup E_{cov, 1}^{c}) \geq 1 - 2 α - \frac{b _{cov}}{2} = \frac{b _{cov}}{2} .$ On the intersection, the interval contains both $1/2$ and $1/2 + u_{len}$ , so $L (o) \leq \frac{1}{2}, U (o) \geq \frac{1}{2} + u_{len}, U (o) - L (o) \geq u_{len} .$ Consequently, $Q_{len, 0}^{\otimes n} (E_{cov, 0} \cap E_{cov, 1}) \leq Q_{len, 0}^{\otimes n} {o : u_{len} \leq U (o) - L (o)} .$ Since interval length is nonnegative, its expectation satisfies $u_{len} Q_{len, 0}^{\otimes n} {o : u_{len} \leq U (o) - L (o)} \leq E_{Q_{len, 0}^{\otimes n}} [U - L] .$ Combining these bounds, $\frac{u _{len} b _{cov}}{2} \leq u_{len} Q_{len, 0}^{\otimes n} (E_{cov, 0} \cap E_{cov, 1}) \leq u_{len} Q_{len, 0}^{\otimes n} {o : u_{len} \leq U (o) - L (o)} \leq E_{Q_{len, 0}^{\otimes n}} [U - L] .$

The honest interval class is nonempty: the procedure $I_{full} (o) := [- 1, 1] (o \in O^{n})$ covers every target because $τ (P) \in [- 1, 1]$ . For every admissible interval and law, $0 \leq U (o) - L (o) \leq 2, 0 \leq E_{P_{O}^{\otimes n}} [U - L] \leq 2.$ Thus the worst-law expected length is finite and dominates its value at $P_{len, 0}$ . Taking the interval infimum in Definition 11 gives $L_{n, d, q, α}^{*} \geq \frac{u _{len} b _{cov}}{2} = \frac{a _{len} b _{cov}}{2 n} = \frac{c _{0, α}}{n} .$ Together with the squared-error bound, this proves both assertions.

∎

These bounds retain ordinary sampling uncertainty even at complete arrival. For estimation, the floor is universal; for honest intervals, its constant accommodates the fixed coverage requirement. They supply the lower bounds when the missingness-and-dimension contribution lies below the sampling scale and remain available in the regime covered by the normalized converse.

From normalized priors to statistical lower bounds

For each fixed mixture tolerance $β \in (0, 1/4)$ , choose a positive separation constant $c_{β}$ satisfying Theorem 3. Fix this choice before varying $n, d, q$ ; its uniformity is over the parameter triples satisfying that statement, including the condition $g_{n, d, q}^{2} \geq n^{- 1}$ .

The testing-error comparison applies to the two complete observed-sample mixtures as probability laws (Tsybakov, 2009). The model-specific input is their construction and target separation in Definition 14 and Theorem 3. For squared-error risk, separation is measured in squared units. For honest connected intervals, coverage of separated target values links the same comparison to expected length. The next statement fixes the tolerances for these two uses and records their numerical losses.

Lemma 5 [lem:prior-reduction] (Prior reduction and lower bounds).

Let $c_{β}$ denote the fixed separation constant selected from the normalized converse at mixture tolerance $β \in (0, 1/4)$ , and set $β_{0} = 1/16$ . Write $ℓ_{n} = lo g (e + n), g_{n, d, q} = (1 - q) min {1, \frac{d}{n ℓ _{n}}} .$ Use the minimax risks and rate in Definitions 9, 11, and 12.

There exist universal constants $c > 0$ and $c_{0} > 0$ such that, for every $α \in (0, 1/2)$ , there exist constants $c_{α} > 0$ and $c_{0, α} > 0$ with the following guarantees. Set $β_{α} = \frac{1 - 2 α}{8} .$ For every $n, d, q$ satisfying

(Sample size.) $n$ is an integer with $n \geq 1$ .

(Support bound.) $d$ is an integer with $d \geq 1$ .

(Arrival floor.) $q \in [1/2, 1]$ .

whenever $g_{n, d, q}^{2} \geq n^{- 1}$ , both bounds $R_{n, d, q}^{*} \geq \frac{13}{32} c_{β_{0}}^{2} g_{n, d, q}^{2}, L_{n, d, q, α}^{*} \geq \frac{5}{4} c_{β_{α}} (1 - 2 α) g_{n, d, q}$ hold. Throughout the stated parameter range, the parametric bounds are $R_{n, d, q}^{*} \geq \frac{c _{0}}{n}, L_{n, d, q, α}^{*} \geq \frac{c _{0, α}}{n} .$ The combined guarantees are $R_{n, d, q}^{*} \geq c r_{n, d, q}$ and $L_{n, d, q, α}^{*} \geq c_{α} r_{n, d, q}$ .

⊢ Lean

Proof of Lemma 5.

Choose the universal constant $c_{floor} > 0$ supplied by Lemma 4, so that $R_{n, d, q}^{*} \geq \frac{c _{floor}}{n}$ throughout the stated parameter range. Define $c_{sep, pt} = \frac{13}{32} c_{β_{0}}^{2}, c = \frac{1}{2} min {c_{floor}, c_{sep, pt}} .$ Since $β_{0} = 1/16 \in (0, 1/4)$ , the selected constant in Theorem 3 satisfies $c_{β_{0}} > 0$ . Consequently, $c_{sep, pt} > 0, c > 0.$

Fix $α \in (0, 1/2)$ . Choose $c_{0, α} > 0$ from Lemma 4, giving $L_{n, d, q, α}^{*} \geq \frac{c _{0, α}}{n}$ throughout the same parameter range. Define $β_{α} = \frac{1 - 2 α}{8}, c_{sep, len, α} = \frac{5}{4} c_{β_{α}} (1 - 2 α), c_{α} = \frac{1}{2} min {c_{0, α}, c_{sep, len, α}} .$ The inequalities $0 < 1 - 2 α < 1, 0 < β_{α} < \frac{1}{8} < \frac{1}{4}$ ensure $c_{β_{α}} > 0$ , hence $c_{sep, len, α} > 0, c_{α} > 0.$ The constants $c, c_{floor}$ are universal, and $c_{α}, c_{0, α}$ depend only on $α$ .
Fix admissible $n, d, q$ . The scale is nonnegative because $1 - q \geq 0, ℓ_{n} = lo g (e + n) > 0, \frac{d}{n ℓ _{n}} \geq 0, g_{n, d, q} = (1 - q) min {1, \frac{d}{n ℓ _{n}}} \geq 0.$ Suppose $g_{n, d, q}^{2} \geq n^{- 1}$ , and define $a_{pt} = c_{β_{0}} g_{n, d, q} \geq 0.$ By Theorem 3, there are probability priors $Π_{-, pt}, Π_{+, pt}$ and a center $m_{0, pt}$ satisfying $Π_{σ, pt} (M (d, q)) = 1, m_{0, pt} \in R, σ \in {-, +} .$ Define their sample-mixture laws by $Q_{σ, pt}^{(n)} = \int_{M (d, q)} P_{O}^{\otimes n} Π_{σ, pt} (d P), σ \in {-, +} .$ The supplied bounds are $TV (Q_{-, pt}^{(n)}, Q_{+, pt}^{(n)}) \leq β_{0},$ $Π_{-, pt} {τ (P) \leq m_{0, pt} - a_{pt}} \geq 1 - β_{0}, Π_{+, pt} {m_{0, pt} + a_{pt} \leq τ (P)} \geq 1 - β_{0} .$

For an arbitrary estimator $T \in T_{n}$ , define $E_{pt} = {o \in O^{n} : m_{0, pt} \leq T (o)},$ $B_{σ, pt} (T) = \int_{M (d, q)} E_{P} [(T (O^{n}) - τ (P))^{2}] Π_{σ, pt} (d P), σ \in {-, +},$ and the target-failure indicators $D_{-, pt} (P) = 1 {τ (P) > m_{0, pt} - a_{pt}}, D_{+, pt} (P) = 1 {τ (P) < m_{0, pt} + a_{pt}} .$ On the left target region, $o \in E_{pt}$ gives $T (o) - τ (P) \geq a_{pt}, (T (o) - τ (P))^{2} \geq a_{pt}^{2} .$ On the right target region, $o \in E_{pt}^{c}$ gives $τ (P) - T (o) \geq a_{pt}, (T (o) - τ (P))^{2} \geq a_{pt}^{2} .$ Integrating these pointwise bounds over the corresponding sample events gives the good-target risk bounds. On each failure region, the sample-event probability is at most one and squared loss is nonnegative. Thus, for every $P \in M (d, q)$ , $a_{pt}^{2} [P_{O}^{\otimes n} (E_{pt}) - D_{-, pt} (P)] a_{pt}^{2} [P_{O}^{\otimes n} (E_{pt}^{c}) - D_{+, pt} (P)] \leq E_{P} [(T (O^{n}) - τ (P))^{2}], \leq E_{P} [(T (O^{n}) - τ (P))^{2}] .$ The prior failure probabilities satisfy $\int D_{σ, pt} (P) Π_{σ, pt} (d P) \leq β_{0}, σ \in {-, +} .$ Integration over the two priors therefore yields $B_{-, pt} (T) B_{+, pt} (T) \geq a_{pt}^{2} [Q_{-, pt}^{(n)} (E_{pt}) - β_{0}], \geq a_{pt}^{2} [Q_{+, pt}^{(n)} (E_{pt}^{c}) - β_{0}] .$ Total variation gives $Q_{-, pt}^{(n)} (E_{pt}) + Q_{+, pt}^{(n)} (E_{pt}^{c}) = 1 + Q_{-, pt}^{(n)} (E_{pt}) - Q_{+, pt}^{(n)} (E_{pt}) \geq 1 - β_{0} .$ Adding the two risk bounds and substituting $β_{0} = 1/16$ , we obtain $B_{-, pt} (T) + B_{+, pt} (T) \geq (1 - 3 β_{0}) a_{pt}^{2} = \frac{13}{16} c_{β_{0}}^{2} g_{n, d, q}^{2} .$ Each prior average is at most the worst-law risk, since its prior is supported on $M (d, q)$ . Hence $2 P \in M (d, q) sup E_{P} [(T (O^{n}) - τ (P))^{2}] \geq B_{-, pt} (T) + B_{+, pt} (T) \geq 2 c_{sep, pt} g_{n, d, q}^{2} .$ The estimator and target both lie in $[- 1, 1]$ , so the squared loss lies in $[0, 4]$ ; these bounds justify the prior integrations and the finite worst-law risks. The estimator class contains the constant zero estimator. Taking its infimum as in Definition 9 proves $R_{n, d, q}^{*} \geq c_{sep, pt} g_{n, d, q}^{2} = \frac{13}{32} c_{β_{0}}^{2} g_{n, d, q}^{2} .$
Continue under $g_{n, d, q}^{2} \geq n^{- 1}$ , and define $a_{len} = c_{β_{α}} g_{n, d, q} \geq 0.$ Apply Theorem 3 at $β_{α}$ . It supplies probability priors and a center with $Π_{σ, len} (M (d, q)) = 1, m_{0, len} \in R, σ \in {-, +} .$ Define $Q_{σ, len}^{(n)} = \int_{M (d, q)} P_{O}^{\otimes n} Π_{σ, len} (d P), σ \in {-, +} .$ Then $TV (Q_{-, len}^{(n)}, Q_{+, len}^{(n)}) \leq β_{α},$ $Π_{-, len} {τ (P) \leq m_{0, len} - a_{len}} \geq 1 - β_{α}, Π_{+, len} {m_{0, len} + a_{len} \leq τ (P)} \geq 1 - β_{α} .$

For an arbitrary honest interval, write $I \in C_{α} (n, d, q), I (o) = [L_{I} (o), U_{I} (o)], o \in O^{n},$ and define the endpoint events $E_{L, α} = {o \in O^{n} : L_{I} (o) \leq m_{0, len} - a_{len}}, E_{R, α} = {o \in O^{n} : m_{0, len} + a_{len} \leq U_{I} (o)} .$ Also define $D_{-, len} (P) = 1 {τ (P) > m_{0, len} - a_{len}}, D_{+, len} (P) = 1 {τ (P) < m_{0, len} + a_{len}} .$ On a left-target law, coverage implies $L_{I} (o) \leq τ (P) \leq m_{0, len} - a_{len}$ ; on a right-target law, it implies $m_{0, len} + a_{len} \leq τ (P) \leq U_{I} (o)$ . Thus honesty from Definition 10 gives the respective sample-event probabilities at least $1 - α$ . On a failure law, $1 - α - D_{σ, len} (P) = - α \leq 0$ . Consequently, for every $P \in M (d, q)$ , $P_{O}^{\otimes n} (E_{L, α}) P_{O}^{\otimes n} (E_{R, α}) \geq 1 - α - D_{-, len} (P), \geq 1 - α - D_{+, len} (P) .$ Integrating and using the target-failure bounds gives $Q_{-, len}^{(n)} (E_{L, α}) Q_{+, len}^{(n)} (E_{R, α}) \geq 1 - α - \int D_{-, len} d Π_{-, len} \geq 1 - α - β_{α}, \geq 1 - α - \int D_{+, len} d Π_{+, len} \geq 1 - α - β_{α} .$ The total-variation bound transfers the first estimate: $Q_{+, len}^{(n)} (E_{L, α}) \geq Q_{-, len}^{(n)} (E_{L, α}) - β_{α} \geq 1 - α - 2 β_{α} .$ Using the union-intersection identity and the fact that a union has probability at most one, we obtain $Q_{+, len}^{(n)} (E_{L, α} \cap E_{R, α}) = Q_{+, len}^{(n)} (E_{L, α}) + Q_{+, len}^{(n)} (E_{R, α}) - Q_{+, len}^{(n)} (E_{L, α} \cup E_{R, α}) \geq 1 - 2 α - 3 β_{α} .$ On the intersection, the endpoint inequalities imply $U_{I} (o) - L_{I} (o) \geq (m_{0, len} + a_{len}) - (m_{0, len} - a_{len}) = 2 a_{len} .$ Since interval length is nonnegative everywhere, $2 a_{len} 1_{E_{L, α} \cap E_{R, α}} (o) \leq U_{I} (o) - L_{I} (o) .$ Integration under the plus mixture, followed by its defining mixture identity, therefore gives $2 a_{len} Q_{+, len}^{(n)} (E_{L, α} \cap E_{R, α}) \leq \int_{O^{n}} (U_{I} (o) - L_{I} (o)) Q_{+, len}^{(n)} (d o) = \int_{M (d, q)} E_{P} [U_{I} (O^{n}) - L_{I} (O^{n})] Π_{+, len} (d P) \leq P \in M (d, q) sup E_{P} [U_{I} (O^{n}) - L_{I} (O^{n})] .$ Multiplication of the intersection bound by $2 a_{len} \geq 0$ and substitution of $β_{α}$ yield $P \in M (d, q) sup E_{P} [U_{I} (O^{n}) - L_{I} (O^{n})] \geq 2 a_{len} (1 - 2 α - 3 β_{α}) = 2 a_{len} \frac{5}{8} (1 - 2 α) = \frac{5}{4} c_{β_{α}} (1 - 2 α) g_{n, d, q} .$ Lengths lie in $[0, 2]$ , justifying these integrations, and the constant interval $[- 1, 1]$ is honest because $τ (P) \in [- 1, 1]$ . Taking the infimum in Definition 11 proves $L_{n, d, q, α}^{*} \geq c_{sep, len, α} g_{n, d, q} = \frac{5}{4} c_{β_{α}} (1 - 2 α) g_{n, d, q} .$
We now combine the point-risk separation bound with the parametric floor. By Definition 12, $r_{n, d, q} = \frac{1}{n} + g_{n, d, q}^{2} .$ If $g_{n, d, q}^{2} \geq n^{- 1}$ , then $c r_{n, d, q} \leq 2 c g_{n, d, q}^{2} \leq c_{sep, pt} g_{n, d, q}^{2} \leq R_{n, d, q}^{*},$ where $2 c = min {c_{floor}, c_{sep, pt}} \leq c_{sep, pt}$ . If $g_{n, d, q}^{2} < n^{- 1}$ , then $c r_{n, d, q} \leq \frac{2 c}{n} \leq \frac{c _{floor}}{n} \leq R_{n, d, q}^{*},$ using $2 c \leq c_{floor}$ and the floor from Lemma 4. Thus the combined point-risk bound holds throughout the parameter range.
For the length bound, $n \geq 1$ ensures $n > 0, (n)^{2} = n, \frac{1}{n} = (\frac{1}{n})^{2} .$ Also $r_{n, d, q} \geq 0$ , so $r_{n, d, q} \geq 0, (r_{n, d, q})^{2} = r_{n, d, q} .$ If $g_{n, d, q}^{2} \geq n^{- 1}$ , then $(r_{n, d, q})^{2} = \frac{1}{n} + g_{n, d, q}^{2} \leq 2 g_{n, d, q}^{2} \leq (2 g_{n, d, q})^{2} .$ Both square roots being compared are nonnegative, hence $r_{n, d, q} \leq 2 g_{n, d, q} .$ It follows that $c_{α} r_{n, d, q} \leq 2 c_{α} g_{n, d, q} \leq c_{sep, len, α} g_{n, d, q} \leq L_{n, d, q, α}^{*} .$ If $g_{n, d, q}^{2} < n^{- 1}$ , then $(r_{n, d, q})^{2} = \frac{1}{n} + g_{n, d, q}^{2} \leq \frac{2}{n} \leq (\frac{2}{n})^{2},$ and nonnegativity gives $r_{n, d, q} \leq \frac{2}{n} .$ Therefore $c_{α} r_{n, d, q} \leq \frac{2 c _{α}}{n} = \frac{min { c _{0, α} , c _{sep, len, α} }}{n} \leq \frac{c _{0, α}}{n} \leq L_{n, d, q, α}^{*},$ using Lemma 4. These two cases cover every admissible parameter choice, including $q = 1$ , for which $g_{n, d, q} = 0$ and the second case applies. Together with the separation bounds and the parametric floors established above, this proves all the asserted guarantees.

∎

The fixed tolerance $β_{0}$ yields a universal squared-risk constant. By contrast, the coverage-dependent tolerance $β_{α}$ allocates the mixture-comparison error relative to the positive coverage margin $1 - 2 α$ . For each fixed $α \in (0, 1/2)$ , it belongs to the tolerance range required by Theorem 3, and the resulting length constant depends only on $α$ .

The displayed coefficients retain the losses associated with observed-mixture proximity and the prior probabilities of target separation. Their role is to make the conversion from the normalized converse to the statistical criteria explicit. Connectedness is relevant to the length criterion because an interval containing separated values spans their distance.

The dimension bounds retain the condition $g_{n, d, q}^{2} \geq n^{- 1}$ from Theorem 3. The parametric floors in Lemma 4 supply the sampling contribution throughout the parameter range, including $q = 1$ . Together, these inputs give the combined guarantees for the benchmark in Definition 12, with universal constants for squared risk and constants depending only on fixed noncoverage for expected length.

Completion of the main comparisons

The upper bounds come from Lemmas 2 and 3; the normalized-prior reduction and parametric floors in Lemmas 5 and 4 give the matching lower bounds. The formal proofs of the two frontier theorems and the complete-arrival endpoint appear in the following proof appendix, so no second derivation is repeated here.

Verification note

The theorem statements and proofs are machine-checked in Lean 4 under the frozen statistical assumptions. The iid sampling, randomized independence, balanced assignment, consistency, missing-at-random condition, and arrival floor in Assumptions 1, 2, 3, 4, 5, and 6 enter as hypotheses. Verification covers the formal definitions of the law class, identified functional, statistical criteria, and benchmark in Definitions 6, 7, 9, 10, 11, and 12, together with the estimator, interval, and normalized-prior constructions in Algorithm 1, Definition 13, and Definition 14.

The checked results comprise the identification and upper-risk bounds and honest interval construction in Lemmas 1, 2, and 3; the normalized converse in Theorem 3; the sampling floors and testing reductions in Lemmas 4 and 5; and the headline minimax comparisons and complete-arrival reduction in Theorem 1, Theorem 2, and Proposition 1. These mapped results are machine-checked under the statistical hypotheses displayed in their statements. The cellwise quantities and estimator class identified below are presentation-level definitions; they organize notation and do not supply an unformalized premise to a mapped theorem. Bibliographic comparisons are supported by the cited publications and are outside the machine-checked mathematical layer.

The frozen artifact uses Lean toolchain leanprover/lean4:v4.33.0 at repository commit d07574d7eb0a903c2a049c6ae28702de46193ec0. Its sources are under CausalSmith/Stat/STAT_MarNearcompleteFrontier_Research/; presentation_crosswalk.json and lean_snippets.json in this presentation bundle provide machine-readable object links and excerpts. The cellwise quantities Definition 5 and estimator class Definition 8 are presentation-level definitions; the remaining principal objects map as follows.

Paper objects	Lean declarations	Source files
Sampling and causal assumptions	`IidSample`, `RandomizedIndependence`, `BalancedRandomization`, `Consistency`, `MissingAtRandom`, `ArrivalFloor`	`Basic.lean`
Law, target, criteria, and rate	`LawClass`, `psi`, `pointMinimaxRisk`, `HonestIntervalClass`, `lengthMinimaxRisk`, `rate`	`Basic.lean`
Estimator and interval	`tauhatMM`, `intervalMM`	`Helpers/Estimator.lean`
Identification and prior construction	`tau_eq_psi`, `pairedPriorHandle`	`Helpers/Identification.lean`; `Helpers/PairedPrior.lean`
Upper bound and interval construction	`upper_risk`, `honest_interval_construction`	`TUpperRisk.lean`; `THonestInterval.lean`
Lower-bound infrastructure	`parametric_floor`, `prior_reduction`, `normalized_converse`	`TParametricFloor.lean`; `TPriorReduction.lean`; `TNormalizedConverse.lean`
Headline comparisons	`point_frontier`, `interval_frontier`, `complete_arrival_reduction`	`TPointFrontier.lean`; `TIntervalFrontier.lean`; `TCompleteArrival.lean`

Proofs of the main results

Proof of Theorem 1.

Choose the universal positive squared-risk constant from Lemma 5, denoting it by $c_{point}$ , and the universal upper-bound constant $C_{U} > 0$ from Lemma 2. Define $c = min {c_{point}, C_{U} /2}, C = C_{U} .$ Both entries in the minimum are positive, and therefore $0 < c \leq C_{U} /2 < C_{U} = C < \infty.$ These constants are independent of $n, d, q$ .
Fix positive integers $n, d$ and $q \in [1/2, 1]$ . Apply Lemma 5 with $α = 1/4 \in (0, 1/2)$ . Its combined squared-risk guarantee supplies $c_{point} r_{n, d, q} \leq R_{n, d, q}^{*} .$ By Definition 12, $r_{n, d, q} = \frac{1}{n} + g_{n, d, q}^{2} \geq 0.$ Consequently, the choice of $c$ gives $c r_{n, d, q} \leq c_{point} r_{n, d, q} \leq R_{n, d, q}^{*} .$
We verify that the estimator in Algorithm 1 belongs to $T_{n}$ . Write $o = (O_{1}, \dots, O_{n}) \in O^{n}$ for the observed sample tuple; the range calculations below apply to every such tuple. The projection used there satisfies, for every real argument, $- 1 \leq Π_{[- 1, 1]} (t) = max {- 1, min {1, t}} \leq 1 (t \in R) .$ Thus the branch $q = 1$ takes values in $[- 1, 1]$ , as does the fallback branch when $q \neq = 1$ and either $ℓ_{n} < 128$ or $d \geq n ℓ_{n}$ .

For the remaining branch, define the Poisson weights and the averages over stream assignments by $ω_{n, N} = e^{- n /2} \frac{( n /2 ) ^{N}}{N !} (N \in {0, 1, 2, \dots}),$ $\overline{τ}_{N} (o) = 4^{- N} Z \in {1, 2, 3, 4}^{N} \sum τ (o; N, Z) (0 \leq N \leq n) .$ Here $τ (o; N, Z)$ is the projected randomized estimate specified in Algorithm 1 for the fixed sample, auxiliary count, and stream assignments. Each summand lies in $[- 1, 1]$ , and there are $4^{N}$ assignments. Hence $- 4^{N} \leq Z \in {1, 2, 3, 4}^{N} \sum τ (o; N, Z) \leq 4^{N}, - 1 \leq \overline{τ}_{N} (o) \leq 1.$ For $N = 0$ , the assignment set consists of the single empty tuple, so the same calculation applies.

The Poisson weights satisfy $ω_{n, N} \geq 0, 0 \leq N = 0 \sum n ω_{n, N} \leq N = 0 \sum \infty ω_{n, N} = 1.$ Since the randomized estimate is zero when $N > n$ , its conditional average is $τ_{MM} (o) = N = 0 \sum n ω_{n, N} \overline{τ}_{N} (o)$ in this branch. Multiplying the bounds on each average by its nonnegative weight and summing gives $- 1 \leq - N = 0 \sum n ω_{n, N} \leq τ_{MM} (o) \leq N = 0 \sum n ω_{n, N} \leq 1.$ The projected formulas and finite averages are measurable. Thus, on the entire Cartesian sample space, $τ_{MM} \in T_{n},$ with $T_{n}$ as defined in Definition 8.
The zero-pair-mass specialization of the construction in Definition 14 places all normalized mass at its filler label. It has independent fair treatment and complete arrival, and supplies $M (d, q) \neq = \emptyset (d \geq 1, q \in [1/2, 1]),$ including $d = 1$ . For the real suprema below, we use the conditional real supremum: a nonempty set bounded above has its usual least upper bound, while a set unbounded above is assigned supremum zero. Fix $T \in T_{n}$ . If its set of squared-error risks is bounded above, nonnegativity of squared loss and the supremum property give $0 \leq E_{P} [{T (o) - τ (P)}^{2}] \leq P^{'} \in M (d, q) sup E_{P^{'}} [{T (o) - τ (P^{'})}^{2}] (P \in M (d, q)) .$ The law class is nonempty, so this bounds the supremum below by zero. If the set of squared-error risks is unbounded above, the stated convention gives $P \in M (d, q) sup E_{P} [{T (o) - τ (P)}^{2}] = 0.$ In either case, $0 \leq P \in M (d, q) sup E_{P} [{T (o) - τ (P)}^{2}] (T \in T_{n}) .$ The worst-case risks are therefore bounded below by zero. Evaluating the infimum in Definition 9 at the admissible estimator established above yields $R_{n, d, q}^{*} \leq P \in M (d, q) sup E_{P} [{τ_{MM} (o) - τ (P)}^{2}] .$ For every law in this supremum, the sample consists of independent records with its observed-law distribution. Consequently, Lemma 2 gives $P \in M (d, q) sup E_{P} [{τ_{MM} (o) - τ (P)}^{2}] \leq C_{U} r_{n, d, q} = C r_{n, d, q} .$ Together with the lower bound, this proves the claimed inequalities throughout the stated parameter range.

∎

Proof of Theorem 2.

Fix $α \in (0, 1/2)$ . Choose the universal risk constant $C_{U}$ supplied by Lemma 2, so that $0 < C_{U} < \infty, E_{P_{O}^{\otimes n}} [(τ_{MM} - τ (P))^{2}] \leq C_{U} r_{n, d, q}$ for every $n, d \geq 1$ , every $q \in [1/2, 1]$ , and every $P \in M (d, q)$ . The combined interval bound in Lemma 5 supplies a constant $c_{lower, α}$ , depending only on $α$ , satisfying $c_{lower, α} > 0, c_{lower, α} r_{n, d, q} \leq L_{n, d, q, α}^{*}$ throughout the same parameter range.
Define the comparison constants by $c_{α} := c_{lower, α}, C_{α} := c_{lower, α} + 2 C_{U} / α + 1.$ Since $C_{U} / α \geq 0$ , these constants satisfy $0 < c_{α} < C_{α} < \infty.$ Now fix arbitrary positive integers $n, d$ and $q \in [1/2, 1]$ . By Definition 12, $r_{n, d, q} = \frac{1}{n} + g_{n, d, q}^{2} \geq 0, r_{n, d, q} \geq 0.$ The preceding lower bound therefore gives the required inequality $c_{α} r_{n, d, q} \leq L_{n, d, q, α}^{*} .$
Apply Lemma 3 with the chosen $C_{U}$ . For the procedure in Definition 13, it yields $I_{MM, α} \in C_{α} (n, d, q)$ and, for every $P \in M (d, q)$ , $E_{P_{O}^{\otimes n}} [length {I_{MM, α} (O^{n})}] \leq min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} .$

The law class is nonempty. Indeed, the paired construction with all latent masses zero concentrates on its filler label. Write $P_{fill}$ for this law, specified by $X = 0, S (0) = S (1) = Y (0) = 0, R = 1, A \sim Bernoulli (1/2), Y (1) \sim Bernoulli (\frac{( 1 + q ) ^{2}}{8 q}), A ⊥ Y (1), S = S (A), Y = Y (A), R Y = R Y .$ The Bernoulli parameter belongs to $[0, 1]$ , since $0 < (1 + q)^{2} \leq 4 \leq 8 q .$ This law has one occupied baseline label, independent balanced treatment, consistent realized measurements, and complete arrival. Hence, by Definition 6, $P_{fill} \in M (d, q) .$ Taking the supremum of the expected-length bound gives $P \in M (d, q) sup E_{P_{O}^{\otimes n}} [length {I_{MM, α} (O^{n})}] \leq min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} .$
Because $C_{U} / α \geq 0$ and $r_{n, d, q} \geq 0$ , square-root multiplicativity gives $\frac{C _{U} r _{n, d, q}}{α} = \frac{C _{U}}{α} r_{n, d, q}, \frac{C _{U} r _{n, d, q}}{α} = \frac{C _{U}}{α} r_{n, d, q} .$ Consequently, $min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} \leq 2 \frac{C _{U}}{α} r_{n, d, q} .$ The definition of $C_{α}$ and positivity of $c_{lower, α}$ imply $2 \frac{C _{U}}{α} \leq C_{α} .$ Multiplying by the nonnegative quantity $r_{n, d, q}$ yields $2 \frac{C _{U}}{α} r_{n, d, q} \leq C_{α} r_{n, d, q} .$
For every $I \in C_{α} (n, d, q)$ , the endpoint ordering in Definition 10 gives $length {I (o)} \geq 0 for every o \in O^{n} .$ If the law-indexed expected lengths of this candidate interval are bounded above, then $0 \leq E_{P_{fill, O}^{\otimes n}} [length {I (O^{n})}] \leq P \in M (d, q) sup E_{P_{O}^{\otimes n}} [length {I (O^{n})}] .$ For an unbounded-above collection, the real-valued supremum is assigned the value zero. Thus, in the unbounded case, $0 = P \in M (d, q) sup E_{P_{O}^{\otimes n}} [length {I (O^{n})}] .$ In either case, the worst-law expected length is nonnegative. The collection of worst-law expected lengths is therefore bounded below by zero and contains the value attained by $I_{MM, α}$ . Using the infimum in Definition 11, followed by the preceding bounds, gives $L_{n, d, q, α}^{*} \leq P \in M (d, q) sup E_{P_{O}^{\otimes n}} [length {I_{MM, α} (O^{n})}] \leq min {2, 2 \frac{C _{U} r _{n, d, q}}{α}} \leq 2 \frac{C _{U}}{α} r_{n, d, q} \leq C_{α} r_{n, d, q} .$ Together with the lower bound, this proves the assertion uniformly over the stated parameter range.

∎

Proof of Proposition 1.

Choose universal constants $0 < c < C$ from Theorem 1. Fix $α \in (0, 1/2)$ , and choose constants $0 < c_{α} < C_{α}$ , depending only on $α$ , from Theorem 2. For positive integers $n, d$ , the inclusion $1 \in [1/2, 1]$ gives $c r_{n, d, 1} \leq R_{n, d, 1}^{*} \leq C r_{n, d, 1}, c_{α} r_{n, d, 1} \leq L_{n, d, 1, α}^{*} \leq C_{α} r_{n, d, 1} .$ We retain these inequalities while establishing the estimator and risk identities at complete arrival.
The law class is nonempty. Indeed, the paired-law construction with zero perturbation and every latent draw at the residual zero-mass atom reduces, at $q = 1$ , to the law $P_{fill} := the full-data law specified by ⎩ ⎨ ⎧ A, Y (1) independent, each with law Bernoulli (1/2), X = 0, S (0) = S (1) = S = Y (0) = 0, R = 1, Y = A Y (1) .$ This law has one occupied baseline label, independent balanced treatment assignment, and consistent realized measurements. Its constant arrival indicator satisfies conditional independence and has arrival probability one in every occupied cell. Thus $P_{fill} \in M (d, 1) (d \geq 1) .$ This construction also applies when $d = 1$ , when the collection of baseline pairs is empty.
Fix $P \in M (d, 1)$ . On the entire Cartesian observed-record space, define the complete-arrival score by $ζ_{HT} (O) := 2 (2 A - 1) (R Y), O = (X, A, S, R, R Y) \in {0, \dots, d - 1} \times {0, 1}^{4} .$ Under the observed-data law, the fifth coordinate is the product of arrival and realized outcome. Splitting the finite expectation according to the treatment and outcome-mark coordinates therefore gives $E_{P} [ζ_{HT} (O)] = 2 {P (A = 1, R = 1, Y = 1) - P (A = 0, R = 1, Y = 1)} .$

To remove the arrival restriction, define, for every $x \in {0, \dots, d - 1}$ and $a, s \in {0, 1}$ , $p_{cell} (x, a, s) p_{arr} (x, a, s) p_{mis} (x, a, s) := P (X = x, A = a, S = s), := P (X = x, A = a, S = s, R = 1), := P (X = x, A = a, S = s, R = 0) .$ These masses satisfy $p_{cell} (x, a, s) = p_{arr} (x, a, s) + p_{mis} (x, a, s), p_{arr} (x, a, s), p_{mis} (x, a, s) \geq 0.$ If the cell mass is zero, this identity forces its missing mass to be zero. If the cell mass is positive, Assumption 6 at $q = 1$ gives $1 \leq \frac{p _{arr} ( x , a , s )}{p _{cell} ( x , a , s )} ⟹ p_{cell} (x, a, s) \leq p_{arr} (x, a, s) ⟹ p_{mis} (x, a, s) = 0.$ Consequently, every missing-cell mass is zero, including null cells. Every nonnegative full-data atom mass contributing to such a cell is also zero. Separating the cases $R = 1$ and $R = 0$ in the finite atom sums yields $P (A = a, R = 1, Y = 1) = P (A = a, Y = 1), a \in {0, 1} .$

By Assumption 3, $P (A = 0) = 1 - P (A = 1) = \frac{1}{2} .$ Using Assumptions 4 and 2, we obtain, for each $a \in {0, 1}$ , $2 P (A = a, Y = 1) = 2 P (A = a, Y (a) = 1) = 2 P (A = a) P (Y (a) = 1) = P (Y (a) = 1) .$ Substitution into the score expectation, followed by the binary-outcome identity, gives $E_{P} [ζ_{HT} (O)] = 2 {P (A = 1, Y = 1) - P (A = 0, Y = 1)} = P (Y (1) = 1) - P (Y (0) = 1) = E_{P} [Y (1) - Y (0)] = τ (P) .$
For every Cartesian sample $O^{n} = (O_{1}, \dots, O_{n})$ , define $\overline{ζ}_{n, HT} (O^{n}) := \frac{1}{n} i = 1 \sum n ζ_{HT} (O_{i}) = \frac{2}{n} i = 1 \sum n (2 A_{i} - 1) Y_{i}^{obs}, Y_{i}^{obs} := (R Y)_{i} .$ The binary coordinates imply $ζ_{HT} (O) \in {- 2, 0, 2} \subseteq [- 2, 2] .$ The bounded-variable variance inequality therefore gives $Var_{P} {ζ_{HT} (O)} \leq 4.$ All these variables are square integrable because their domain is finite. Under Assumption 1, the iid average identities and the score mean established above give $E_{P} [\overline{ζ}_{n, HT} (O^{n})] = τ (P), Var_{P} {\overline{ζ}_{n, HT} (O^{n})} = \frac{1}{n} Var_{P} {ζ_{HT} (O)} .$ Thus $E_{P} [{\overline{ζ}_{n, HT} (O^{n}) - τ (P)}^{2}] = Var_{P} {\overline{ζ}_{n, HT} (O^{n})} = \frac{1}{n} Var_{P} {ζ_{HT} (O)} \leq \frac{4}{n} .$ Taking the supremum over the nonempty law class gives $P \in M (d, 1) sup E_{P} [{\overline{ζ}_{n, HT} (O^{n}) - τ (P)}^{2}] \leq \frac{4}{n} .$
The $q = 1$ branch of Algorithm 1 gives, for every Cartesian sample, $τ_{MM} (O^{n}) = Π_{[- 1, 1]} [\overline{ζ}_{n, HT} (O^{n})] .$ Binary potential outcomes have difference in $[- 1, 1]$ . Averaging these pointwise bounds against the full-data probability law gives $- 1 = E_{P} [- 1] \leq E_{P} [Y (1) - Y (0)] = τ (P) \leq E_{P} [1] = 1.$

The projection inequality follows by its three defining cases. If $\overline{ζ}_{n, HT} (O^{n}) \leq - 1$ , then $∣ τ_{MM} (O^{n}) - τ (P) ∣ = τ (P) + 1 \leq τ (P) - \overline{ζ}_{n, HT} (O^{n}) = \overline{ζ}_{n, HT} (O^{n}) - τ (P) .$ If $- 1 \leq \overline{ζ}_{n, HT} (O^{n}) \leq 1$ , then $∣ τ_{MM} (O^{n}) - τ (P) ∣ = \overline{ζ}_{n, HT} (O^{n}) - τ (P) .$ If $1 \leq \overline{ζ}_{n, HT} (O^{n})$ , then $∣ τ_{MM} (O^{n}) - τ (P) ∣ = 1 - τ (P) \leq \overline{ζ}_{n, HT} (O^{n}) - τ (P) = \overline{ζ}_{n, HT} (O^{n}) - τ (P) .$ This proves the asserted pointwise comparison for every sample.
Squaring the pointwise comparison and integrating gives, for each $P \in M (d, 1)$ , $E_{P} [{τ_{MM} (O^{n}) - τ (P)}^{2}] \leq E_{P} [{\overline{ζ}_{n, HT} (O^{n}) - τ (P)}^{2}] .$ The unprojected risks form a nonempty family bounded above by $4/ n$ . Each projected risk is therefore bounded by their supremum, and taking the supremum of the projected risks yields $P \in M (d, 1) sup E_{P} [{τ_{MM} (O^{n}) - τ (P)}^{2}] \leq P \in M (d, 1) sup E_{P} [{\overline{ζ}_{n, HT} (O^{n}) - τ (P)}^{2}] \leq \frac{4}{n} .$
Finally, the error-scale definition and Definition 12 give $g_{n, d, 1} = (1 - 1) min {1, \frac{d}{n lo g ( e + n )}} = 0, r_{n, d, 1} = \frac{1}{n} + g_{n, d, 1}^{2} = \frac{1}{n} .$ Since $n \geq 1$ , $r_{n, d, 1} = \frac{1}{n} = \frac{1}{n} .$ Substituting these identities into the frontier inequalities selected at the start proves $\frac{c}{n} \leq R_{n, d, 1}^{*} \leq \frac{C}{n}, \frac{c _{α}}{n} \leq L_{n, d, 1, α}^{*} \leq \frac{C _{α}}{n} .$ The constants retain their stated dependence uniformly over all positive integers $n, d$ .

∎

Proof of Theorem 3.

Fix $β \in (0, 1/4)$ . We first construct the required priors for all sufficiently large sample sizes, with a threshold depending only on $β$ , and then extend the construction to every positive sample size.

Use the construction and notation of Definition 14. Throughout the paired construction, expectations and probabilities refer to its independent latent draws. The elementary scale bounds are $L \geq 1, 2 \leq K, 8 L \leq K \leq 9 L, M \leq n L .$ Indeed, the upper bound for $K = ⌈ 8 L ⌉$ follows from $K < 8 L + 1 \leq 9 L$ . Consequently, $0 \leq 2 M h B_{0} = \frac{M}{512 n K} \leq \frac{1}{2}, f = 1 - 2 M h B_{0} \geq \frac{1}{2}, J = f + 2 j = 1 \sum M p_{j} \geq \frac{1}{2} .$ Thus normalization is well defined, and $\frac{f}{J} + 2 j = 1 \sum M \frac{p _{j}}{J} = 1, 2 M + 1 \leq d .$ These conclusions also cover $M = 0$ , when the law consists of the filler label.

For every $σ, z_{j}, u \in {- 1, 1}$ , the probabilities specified in the construction satisfy $q \leq ρ_{σ, j, u} \leq 1, 0 \leq \frac{b}{2} + c_{0} u \leq q \leq ρ_{σ, j, u}, 0 \leq μ_{σ, j, u} \leq 1.$ Here the middle bound follows by substituting $b = (1 + q) /2$ , $c_{0} = 1/16$ , and $q \geq 1/2$ . The filler mean is valid as well: $0 \leq b^{2} = \frac{( 1 + q ) ^{2}}{4} \leq \frac{1 + 3 q}{4} \leq 2 q, 0 \leq μ_{0} = \frac{b ^{2}}{2 q} \leq 1.$ Treatment is an independent fair coin, and the realized measurements are selected from their potential measurements as specified in the construction. Conditional on an occupied baseline label and treatment arm, arrival is independent of the outcome: it is complete at the filler label and in the control arm, and has probability $ρ_{σ, j, u}$ in a treated pair cell. Unoccupied cells have zero mass. Hence every constructed normalized law belongs to $M (d, q)$ in Definition 6. The finitely many latent configurations therefore induce discrete probability priors supported on this class.
We record the interpolation identities needed for the count comparison. Polynomial interpolation at zero gives $φ_{pol} (0) = i = 0 \sum m φ_{pol} (x_{i}) l_{i} (0) for every polynomial φ_{pol} of degree at most m = K - 1 .$ Applying this identity to the constant polynomial and to positive powers yields $i = 0 \sum m l_{i} (0) = 1, i = 0 \sum m ν_{i} = \frac{1}{D}, i = 0 \sum m ν_{i} x_{i}^{t_{pol}} = 0 (1 \leq t_{pol} \leq K - 1) .$ Also, $D = i = 0 \sum m ∣ l_{i} (0) ∣ \geq 1, i = 0 \sum m ∣ ν_{i} ∣ = 1.$ Since $x_{i} \geq h > 0$ , the latent probabilities obey $i = 0 \sum m \frac{h ∣ ν _{i} ∣}{x _{i}} \leq 1.$ Their residual mass is therefore nonnegative. Substitution into the discrete latent distribution gives $E p E (p^{t_{pol}} z) E p^{2} = h B_{0}, = h B_{0}^{t_{pol}} i = 0 \sum m ν_{i} x_{i}^{t_{pol} - 1} = 0 = E [(p z)^{2}] = h B_{0}^{2} i = 0 \sum m ∣ ν_{i} ∣ x_{i} \leq h B_{0}^{2} = \frac{1}{102 4 ^{2} n ^{2}} . E (p z) = \frac{h B _{0}}{D}, (2 \leq t_{pol} \leq K),$ The atom with $p = 0$ contributes zero to each displayed positive-power moment.
Let the eight-coordinate pair vector be $V_{σ} (z, r) = (v_{σ} (z, r), v_{σ} (z, - r)), σ, z, r \in {- 1, 1} .$ Its coordinates are nonnegative and satisfy $ℓ_{atom} = 1 \sum 8 V_{σ, ℓ_{atom}} (z, r) = 2.$ For a count vector $k_{pair} = (k_{pair, 1}, \dots, k_{pair, 8}) \in N^{8}$ , define $t_{count} = ℓ_{atom} = 1 \sum 8 k_{pair, ℓ_{atom}}, H_{σ} (z; k_{pair}) = \frac{1}{2} r \in {- 1, 1} \sum ℓ_{atom} = 1 \prod 8 V_{σ, ℓ_{atom}} (z, r)^{k_{pair, ℓ_{atom}}}$ Products use the convention $0^{0} = 1$ . The likelihood of this count vector in one mixed pair block is $L_{σ, pair} (k_{pair}) = E [e^{- 8 n p} \frac{( 4 n p ) ^{t_{count}}}{\prod _{ℓ_{atom} = 1}^{8} ( k _{pair, ℓ_{atom}} )!} H_{σ} (z; k_{pair})],$ where the expectation is over the latent pair $(p, z)$ .

Changing $z$ to $- z$ exchanges the two signs, so $H_{-} (z; k_{pair}) - H_{+} (z; k_{pair}) = z [H_{-} (1; k_{pair}) - H_{+} (1; k_{pair})] .$ This difference is zero when $t_{count} = 0$ . It is also zero when $t_{count} = 1$ , because averaging over the fair orientation gives, at either label, the four coefficients $(\frac{1}{2}, \frac{δ}{4}, \frac{b}{4}, \frac{b}{4}),$ independently of $σ z$ .

For $v_{exp} \in N$ , define the signed Taylor coefficient $Γ_{v_{exp}} (k_{pair}) = E [\frac{( - 8 n p ) ^{v_{exp}}}{v _{exp} !} \frac{( 4 n p ) ^{t_{count}}}{\prod _{ℓ_{atom} = 1}^{8} ( k _{pair, ℓ_{atom}} )!} (H_{-} (z; k_{pair}) - H_{+} (z; k_{pair}))] .$ The exponential series, together with $0 \leq p \leq B_{0}$ , gives $L_{-, pair} (k_{pair}) - L_{+, pair} (k_{pair}) = v_{exp} = 0 \sum \infty Γ_{v_{exp}} (k_{pair}) .$ The low-count cancellations above and the signed moment identities imply $Γ_{v_{exp}} (k_{pair}) = 0 if v_{exp} + t_{count} \leq K .$ Indeed, when $t_{count} \geq 2$ , this coefficient is a fixed multiple of $E [p^{v_{exp} + t_{count}} z]$ .

For fixed count degree, the multinomial identity gives $k_{pair} : t_{count} = t_{degree} \sum \frac{H _{σ} ( z ; k _{pair} )}{\prod _{ℓ_{atom} = 1}^{8} ( k _{pair, ℓ_{atom}} )!} = \frac{2 ^{t_{degree}}}{t _{degree} !}, t_{degree} \in N .$ Bounding the absolute mark difference by the sum of its two nonnegative terms therefore yields $k_{pair} : t_{count} = t_{degree} \sum ∣ Γ_{v_{exp}} (k_{pair}) ∣ \leq 2 \frac{( 8 n B _{0} ) ^{v_{exp}}}{v _{exp} !} \frac{( 8 n B _{0} ) ^{t_{degree}}}{t _{degree} !} .$ Thus, for each total degree $s_{tot} \in N$ , $t_{degree} = 0 \sum s_{tot} k_{pair} : t_{count} = t_{degree} \sum ∣ Γ_{s_{tot} - t_{degree}} (k_{pair}) ∣ \leq ⎩ ⎨ ⎧ 0, 2 \frac{( 16 n B _{0} ) ^{s_{tot}}}{s _{tot} !}, s_{tot} \leq K, s_{tot} > K .$ The second line follows by factorial-series convolution. Its summable majorant justifies the absolute summations and gives $k_{pair} \in N^{8} \sum ∣ L_{-, pair} (k_{pair}) - L_{+, pair} (k_{pair}) ∣ \leq 2 s_{tot} > K \sum \frac{( 16 n B _{0} ) ^{s_{tot}}}{s _{tot} !} .$

Denote the two complete mixed count laws by $C_{σ} = Law (the unnormalized observed-atom counts under sign σ), σ \in {- 1, 1} .$ The independent pair blocks have probability likelihoods, and the filler likelihood is common to both signs. Write the tuple of pair count vectors as $k_{blocks} = (k_{pair}^{(1)}, \dots, k_{pair}^{(M)}) \in (N^{8})^{M} .$ Each block likelihood is nonnegative and normalized: $k_{pair} \in N^{8} \sum L_{σ, pair} (k_{pair}) = 1, σ \in {- 1, 1} .$ The product difference has the telescoping identity $j = 1 \prod M L_{-, pair} (k_{pair}^{(j)}) - j = 1 \prod M L_{+, pair} (k_{pair}^{(j)}) = j = 1 \sum M [L_{-, pair} (k_{pair}^{(j)}) - L_{+, pair} (k_{pair}^{(j)})] ℓ_{block} = 1 \prod j - 1 L_{-, pair} (k_{pair}^{(ℓ_{block})}) ℓ_{block} = j + 1 \prod M L_{+, pair} (k_{pair}^{(ℓ_{block})}) .$ Empty products equal one. Taking absolute values and summing over all block count vectors gives $k_{blocks} \in (N^{8})^{M} \sum j = 1 \prod M L_{-, pair} (k_{pair}^{(j)}) - j = 1 \prod M L_{+, pair} (k_{pair}^{(j)}) \leq j = 1 \sum M k_{pair} \in N^{8} \sum ∣ L_{-, pair} (k_{pair}) - L_{+, pair} (k_{pair}) ∣ \leq 2 M s_{tot} > K \sum \frac{( 16 n B _{0} ) ^{s_{tot}}}{s _{tot} !} .$ Indeed, in each telescoping summand, summing every block other than the selected block gives one by normalization. The sum over the $M$ selected blocks therefore gives the factor $M$ . The common filler likelihood also sums to one. Splitting a full count vector into these blocks consequently gives $TV (C_{-}, C_{+}) \leq \frac{1}{2} full count vectors \sum ∣ C_{-} ({vector}) - C_{+} ({vector}) ∣ \leq M s_{tot} > K \sum \frac{( 16 n B _{0} ) ^{s_{tot}}}{s _{tot} !} .$ Counts outside the specified atoms are zero under both laws. For $M = 0$ , both count laws equal the common filler law and the bound is zero.
For $ξ \geq 0$ , define $E_{K} (ξ) = s_{tot} > K \sum \frac{ξ ^{s_{tot}}}{s _{tot} !} .$ Termwise exponential weighting gives $E_{K} (ξ) \leq e^{- K} s_{tot} = 0 \sum \infty \frac{( e ξ ) ^{s_{tot}}}{s _{tot} !} = exp (- K + e ξ),$ because $e^{s_{tot} - K} \geq 1$ on the tail. Since $16 n B_{0} = K /64$ , $e \leq 3$ , and $K \geq 8 L$ , $E_{K} (16 n B_{0}) \leq exp (- K + eK /64) \leq e^{- 4 L} .$ Using $M \leq n L$ , $n \leq e^{L}$ , and $L \leq e^{L}$ , we obtain $TV (C_{-}, C_{+}) \leq M e^{- 4 L} \leq n L e^{- 4 L} \leq e^{- 2 L} \leq e^{- L} = \frac{1}{e + n} \leq \frac{1}{n} .$ Choose an integer threshold satisfying $N_{count} \geq 2, N_{count} > \frac{2}{β} .$ Then, uniformly in $d, q$ , $n \geq N_{count} ⟹ TV (C_{-}, C_{+}) \leq \frac{β}{2} .$
We next transfer the count comparison to the complete fixed-size sample. Conditional on the latent variables, define the total count and its mean by $N_{Pois} = o \in O \sum count at o, Λ_{count} = 4 n J .$ The exact observed-atom probabilities identify the count experiment as independent Poisson counts from $P_{σ, O}$ at total intensity $Λ_{count}$ . For example, $4 n p_{j} v_{σ} (z_{j}, u) = (4 n J) \frac{p _{j}}{J} v_{σ} (z_{j}, u),$ and the same identity holds for the filler coefficients. Hence $N_{Pois} ∣ latent variables \sim Poisson (Λ_{count}), Λ_{count} \geq 2 n .$

For this conditional Poisson law, put $x_{tail} = \frac{Λ _{count} n}{4}, ϑ_{tail} = \frac{x _{tail}}{Λ _{count}} .$ Both are positive, and $x_{tail} \leq \frac{Λ _{count}}{2} \leq Λ_{count} - n .$ The centered Poisson exponential moment is $E [e^{- ϑ_{tail} (N_{Pois} - Λ_{count})} latent variables] = exp {Λ_{count} (e^{- ϑ_{tail}} - 1 + ϑ_{tail})} .$ For every nonnegative real $ϑ_{tail}$ , $e^{- ϑ_{tail}} - 1 + ϑ_{tail} \leq \frac{ϑ _{tail}^{2}}{2} .$ One way to verify this bound is to combine $e^{ϑ_{tail}} \geq 1 + ϑ_{tail} + ϑ_{tail}^{2} /2$ with $(1 + ϑ_{tail} + \frac{ϑ _{tail}^{2}}{2}) (1 - ϑ_{tail} + \frac{ϑ _{tail}^{2}}{2}) = 1 + \frac{ϑ _{tail}^{4}}{4} \geq 1.$ The second factor is positive, so taking reciprocals gives the claimed bound. Exponential Markov inequality now yields $Pr (N_{Pois} < n ∣ latent variables) \leq Pr (Λ_{count} - N_{Pois} > x_{tail} ∣ latent variables) \leq exp {- \frac{x _{tail}^{2}}{Λ _{count}} + Λ_{count} (e^{- ϑ_{tail}} - 1 + ϑ_{tail})} \leq exp (- \frac{x _{tail}^{2}}{2 Λ _{count}}) = e^{- n /8} \leq \frac{8}{n} .$

Uniformly ordering independent Poisson counts produces iid marks with law $P_{σ, O}$ , independently of their total count. Consequently, conditional on the latent variables, the output of $κ_{n}$ on $N_{Pois} \geq n$ has law $P_{σ, O}^{\otimes n}$ . Coupling this output with an iid sample and using the fixed fallback on the complementary event gives $TV (Q_{σ}^{(n)}, κ_{n} C_{σ}) \leq E [Pr (N_{Pois} < n ∣ latent variables)] \leq \frac{8}{n} .$ Here $κ_{n} C_{σ}$ denotes the output law of the kernel. Its independence of the sign and latent variables permits total-variation contraction. The triangle inequality therefore gives $TV (Q_{-}^{(n)}, Q_{+}^{(n)}) \leq TV (C_{-}, C_{+}) + \frac{16}{n} .$ Choose integer thresholds $N_{transfer} \geq 2, N_{transfer} > \frac{32}{β}, N_{TV} = max {N_{count}, N_{transfer}} .$ For every $n \geq N_{TV}$ , the two terms on the right are each at most $β /2$ , so $TV (Q_{-}^{(n)}, Q_{+}^{(n)}) \leq β .$
We now establish target separation. First, the interpolation norm has the uniform bound $1 \leq D \leq cosh 2.$ To see the upper bound, define the transformed nodes, exterior point, and hyperbolic parameter by $y_{i} = \frac{2 x _{i} - 1 - h}{1 - h} = cos \frac{iπ}{m}, y_{*} = - \frac{1 + h}{1 - h}, t_{hyp} = lo g \frac{K + 1}{K - 1} .$ Use the Chebyshev convention $T_{0} (t_{Cheb}) = 1, T_{1} (t_{Cheb}) = t_{Cheb}, T_{ℓ_{pol} + 1} (t_{Cheb}) = 2 t_{Cheb} T_{ℓ_{pol}} (t_{Cheb}) - T_{ℓ_{pol} - 1} (t_{Cheb}) (ℓ_{pol} \geq 1, t_{Cheb} \in R) .$ The ordered nodes give $sign (l_{i} (0)) = (- 1)^{m + i}$ , while $T_{m} (y_{i}) = (- 1)^{i}$ . Interpolating $T_{m}$ at $y_{*}$ therefore gives $D = ∣ T_{m} (y_{*}) ∣.$ Since $h = K^{- 2}$ , $y_{*} = - cosh (t_{hyp}), 0 \leq m t_{hyp} = (K - 1) lo g \frac{K + 1}{K - 1} \leq (K - 1) (\frac{K + 1}{K - 1} - 1) = 2.$ The inequality uses $lo g t \leq t - 1$ for $t > 0$ . The Chebyshev hyperbolic identity then gives $D = cosh (m t_{hyp}) \leq cosh 2.$

Define the signed latent mass, its mean, and the fixed hyperbolic constant by $W = j = 1 \sum M p_{j} z_{j}, μ_{W} = \frac{M h B _{0}}{D} = \frac{M}{1024 n K D}, C_{hyp} = cosh 2.$ Independence of the latent pairs and the moment identities above imply $E W = μ_{W}, Var (W) = M (E [(p z)^{2}] - (\frac{h B _{0}}{D})^{2}) \leq \frac{M}{102 4 ^{2} n ^{2}} .$ Similarly, the deterministic filler mass gives $J = 1 + 2 j = 1 \sum M (p_{j} - h B_{0}), E J = 1,$ and $Var (J) = 4 M (E p^{2} - (h B_{0})^{2}) \leq \frac{4 M}{102 4 ^{2} n ^{2}} .$ In both variance computations, the cross terms vanish because independent centered summands have zero product expectation.

Finally, opposite orientations in a pair satisfy the exact identity $μ_{σ, j, 1} + μ_{σ, j, - 1} = 2 μ_{0} + \frac{σ δ z _{j}}{16 q} .$ This follows by putting the two fractions over a common denominator and using $b^{2} - \frac{δ ^{2}}{4} = q .$ Since $Y (0) = 0$ , summing the filler and pair contributions and dividing by $J$ yields $τ (P_{σ}) = \frac{f μ _{0} + \sum _{j = 1}^{M} p _{j} ( 2 μ _{0} + \frac{σ δ z _{j}}{16 q} )}{J} = μ_{0} + \frac{σ δ}{16 q} \frac{W}{J} .$
For $n, d \geq 1$ , define the dimension factor $ζ_{n, d} = min {1, \frac{d}{n L}} \in [0, 1], g_{n, d, q} = δ ζ_{n, d} .$ Under the stated separation regime, $\frac{1}{n} \leq δ^{2} ζ_{n, d}^{2} \leq \frac{1}{4} ζ_{n, d}^{2}, \frac{4}{n} \leq ζ_{n, d}^{2} .$ In particular, $ζ_{n, d} > 0$ . For $n \geq 2$ , the regime also implies $d \geq 3$ : if $d \leq 2$ , then $0 \leq g_{n, d, q} \leq \frac{1}{2} \frac{2}{n L} \leq \frac{1}{n}, g_{n, d, q}^{2} \leq \frac{1}{n ^{2}} < \frac{1}{n},$ a contradiction.

For $d \geq 3$ and $n L \geq 2$ , the integer floors satisfy $⌊ \frac{d - 1}{2} ⌋ \geq \frac{d}{4}, ⌊ n L ⌋ \geq \frac{n L}{2} .$ Thus $M \geq \frac{1}{4} min {d, n L} = \frac{n L}{4} ζ_{n, d} > 0,$ and, using $K \leq 9 L$ , $\frac{M}{n K} \geq \frac{1}{36} ζ_{n, d}, μ_{W} \geq \frac{1}{36 \cdot 1024 C _{hyp}} ζ_{n, d} > 0.$ Squaring the lower bound for $M$ and using $ζ_{n, d}^{2} \geq 4/ n$ also gives $M^{2} \geq \frac{n L ^{2}}{4}, K^{4} \leq 6561 L^{4}, K^{4} \leq \frac{26244 L ^{2}}{n} M^{2} .$

The logarithmic factor obeys $\forall ε > 0 \exists N_{ε} \in N \forall n \geq N_{ε} : L^{2} \leq ε n .$ Indeed, put $γ_{l o g} = e + 1$ . The standard limit $(lo g ξ)^{2} / ξ \to 0$ as $ξ \to \infty$ gives, eventually, $L^{2} \leq \frac{ε}{γ _{l o g}} (e + n) \leq ε n,$ where the last inequality uses $n \geq 1$ .

Define $η_{W} = \frac{β}{8 C _{hyp}^{2}} > 0.$ Choose $N_{W} \geq 2$ , depending only on $β$ , so that $n \geq N_{W} ⟹ L^{2} \leq \frac{η _{W}^{2}}{26244} n .$ For every admissible $n, d, q$ beyond this threshold, $K^{4} \leq η_{W}^{2} M^{2}, \frac{K ^{2}}{M} \leq η_{W} .$ The second inequality follows by taking nonnegative square roots.
Chebyshev’s inequality and the positive mean established above give, for admissible $n \geq N_{W}$ , $Pr (∣ W - μ_{W} ∣ > \frac{μ _{W}}{2}) \leq \frac{M / ( 102 4 ^{2} n ^{2} )}{( μ _{W} /2 ) ^{2}} = \frac{4 K ^{2} D ^{2}}{M} \leq 4 C_{hyp}^{2} \frac{K ^{2}}{M} \leq \frac{β}{2} .$ Choose another integer threshold $N_{J}$ , depending only on $β$ , such that $n \geq N_{J} ⟹ L^{2} \leq \frac{β 102 4 ^{2}}{32} n .$ The normalizer variance bound, $M \leq n L$ , and $L \geq 1$ then yield $Pr (∣ J - 1∣ > \frac{1}{2}) \leq \frac{16 M}{102 4 ^{2} n ^{2}} \leq \frac{16 L}{102 4 ^{2} n} \leq \frac{16 L ^{2}}{102 4 ^{2} n} \leq \frac{β}{2} .$

Define the common good event, target threshold, and separation constant by $G = {∣ W - μ_{W} ∣ \leq \frac{μ _{W}}{2}, ∣ J - 1∣ \leq \frac{1}{2}}, N_{target} = max {N_{W}, N_{J}},$ $c_{large} = \frac{1}{36 \cdot 1024 C _{hyp} \cdot 48} > 0.$ For admissible $n \geq N_{target}$ , the union bound gives $Pr (G) \geq 1 - β .$ On $G$ , $W \geq \frac{μ _{W}}{2}, 0 < J \leq \frac{3}{2}, \frac{W}{J} \geq \frac{μ _{W}}{3} .$ Since $δ \geq 0$ and $0 < q \leq 1$ , it follows that $\frac{δ}{16 q} \frac{W}{J} \geq \frac{δ μ _{W}}{48} \geq \frac{δ ζ _{n, d}}{36 \cdot 1024 C _{hyp} \cdot 48} = c_{large} g_{n, d, q} .$ Set $m_{0} = μ_{0} .$ The exact target identity therefore implies, on $G$ , $τ (P_{-}) \leq m_{0} - c_{large} g_{n, d, q}, m_{0} + c_{large} g_{n, d, q} \leq τ (P_{+}) .$ Because $Π_{σ} = Law (P_{σ})$ , the corresponding prior event masses equal the probabilities of their latent preimages. Hence $Π_{-} {τ (P) \leq m_{0} - c_{large} g_{n, d, q}} \geq 1 - β,$ $Π_{+} {m_{0} + c_{large} g_{n, d, q} \leq τ (P)} \geq 1 - β .$
Combine the two large-sample thresholds: $N_{β} = max {N_{TV}, N_{target}} \geq 2.$ For every admissible $n \geq N_{β}$ , the paired priors simultaneously satisfy $TV (Q_{-}^{(n)}, Q_{+}^{(n)}) \leq β$ and both target-event inequalities with separation constant $c_{large}$ . The threshold and this positive constant are independent of $n, d, q$ .
To cover smaller sample sizes, define $a_{β} = min {\frac{1}{4}, \frac{lo g ( 1 + 4 β ^{2} )}{4}} > 0, u_{n} = \frac{a _{β}}{n}, n \geq 1.$ These choices satisfy $0 < u_{n} \leq \frac{1}{4}, 16 n u_{n}^{2} = 16 a_{β}^{2} \leq lo g (1 + 4 β^{2}) .$

Choose one baseline label, set both potential surrogates and $Y (0)$ to zero, assign treatment by an independent fair coin, and make arrival complete in both arms. Let $P_{-, small}$ and $P_{+, small}$ be the resulting laws with $Y (1) \sim Bernoulli (1/2) and Y (1) \sim Bernoulli (1/2 + u_{n}),$ respectively. Both laws belong to $M (d, q)$ for every $d \geq 1$ and $q \in [1/2, 1]$ , and $τ (P_{-, small}) = \frac{1}{2}, τ (P_{+, small}) = \frac{1}{2} + u_{n} .$ In the observed-atom order $(A, R, R Y) = (0, 1, 0), (1, 1, 0), (1, 1, 1)$ , their probabilities are $P_{-, small, O} : (\frac{1}{2}, \frac{1}{4}, \frac{1}{4}), P_{+, small, O} : (\frac{1}{2}, \frac{1}{4} - \frac{u _{n}}{2}, \frac{1}{4} + \frac{u _{n}}{2}) .$ All other atoms have zero mass. Thus the plus observed law is absolutely continuous with respect to the minus observed law, and direct summation gives $χ^{2} (P_{+, small, O} ∥ P_{-, small, O}) := o \in O P_{-, small, O} ({o}) > 0 \sum \frac{( P _{+, small, O} ({ o }) - P _{-, small, O} ({ o }) ) ^{2}}{P _{-, small, O} ({ o })} = 2 u_{n}^{2} \leq 16 u_{n}^{2} .$ For finite probability laws, multiplication of likelihood ratios gives the product identity for $1 + χ^{2}$ , while Cauchy–Schwarz gives $TV \leq \frac{1}{2} χ^{2}$ . Applying these facts to the displayed pair yields $TV (P_{-, small, O}^{\otimes n}, P_{+, small, O}^{\otimes n}) \leq \frac{1}{2} (1 + χ^{2} (P_{+, small, O} ∥ P_{-, small, O}))^{n} - 1 \leq \frac{1}{2} e^{16 n u_{n}^{2}} - 1 \leq β .$ Here the middle inequality follows from $1 + t \leq e^{t}$ for $t \geq 0$ .

Define $c_{small} = \frac{a _{β}}{N _{β}} > 0.$ For $1 \leq n < N_{β}$ , the scale bound $0 \leq g_{n, d, q} \leq 1/2$ gives $c_{small} g_{n, d, q} \leq \frac{a _{β}}{2 N _{β}} \leq \frac{a _{β}}{2 n} = \frac{u _{n}}{2} .$ Take the point priors and midpoint $Π_{-}^{small} = δ_{P_{-, small}}, Π_{+}^{small} = δ_{P_{+, small}}, m_{0} = \frac{1}{2} + \frac{u _{n}}{2} .$ Their target inequalities hold deterministically: $τ (P_{-, small}) \leq m_{0} - c_{small} g_{n, d, q}, m_{0} + c_{small} g_{n, d, q} \leq τ (P_{+, small}) .$ Both prior event masses are therefore one, and the preceding product bound supplies the required mixture distance.
Finally, set $c_{β} = min {c_{large}, c_{small}} > 0.$ If $n \geq N_{β}$ , select the paired priors and their center. If $1 \leq n < N_{β}$ , select the point priors and their midpoint. In either case, write $c_{branch} = {c_{large}, c_{small}, n \geq N_{β}, 1 \leq n < N_{β} .$ Since $g_{n, d, q} \geq 0$ and $c_{β} \leq c_{branch}$ , ${P : τ (P) \leq m_{0} - c_{branch} g_{n, d, q}} \subseteq {P : τ (P) \leq m_{0} - c_{β} g_{n, d, q}},$ ${P : m_{0} + c_{branch} g_{n, d, q} \leq τ (P)} \subseteq {P : m_{0} + c_{β} g_{n, d, q} \leq τ (P)} .$ Monotonicity of prior probabilities preserves both lower bounds $1 - β$ , and the mixture-distance bounds remain valid. These two cases cover every admissible positive sample size and establish all the assertions.

∎

References

Kallus, Nathan and Mao, Xiaojie (2025). On the role of surrogates in the efficient estimation of treatment effects with limited outcome data. Journal of the Royal Statistical Society Series B: Statistical Methodology. doi
Zeng, Zhenghao and Balakrishnan, Sivaraman and Han, Yanjun and Kennedy, Edward H. (2024). Causal inference with high-dimensional discrete covariates. . arXiv
Zhang, Yuqian and Chakrabortty, Abhishek and Bradic, Jelena (2025). The decaying missing-at-random framework: Model doubly robust causal inference with partially labeled data. . doi
{CausalSmith} (2026). Outcome annotation and minimax risk for discrete average treatment effects. . doi
Jiao, Jiantao and Venkat, Kartik and Han, Yanjun and Weissman, Tsachy (2015). Minimax estimation of functionals of discrete distributions. IEEE Transactions on Information Theory. doi
Wu, Yihong and Yang, Pengkun (2016). Minimax rates of entropy estimation on large alphabets via best polynomial approximation. IEEE Transactions on Information Theory. doi
Cai, T. Tony and Low, Mark G. (2004). An adaptation theory for nonparametric confidence intervals. The Annals of Statistics. doi
D{\'i}az, Iv{\'a}n and van der Laan, Mark J. (2017). Doubly robust inference for targeted minimum loss-based estimation in randomized trials with missing outcome data. Statistics in Medicine. doi
Imbens, Guido W. and Rubin, Donald B. (2015). Causal Inference for Statistics, Social, and Biomedical Sciences: An Introduction. Cambridge University Press. doi
van der Vaart, Aad W. (1998). Asymptotic Statistics. Cambridge University Press. doi
Tsybakov, Alexandre B. (2009). Introduction to Nonparametric Estimation. Springer. doi
Rubin, Donald B. (1974). Estimating causal effects of treatments in randomized and nonrandomized studies. Journal of Educational Psychology. doi
Robins, James M. and Ritov, Ya'acov (1997). Toward a curse of dimensionality appropriate ({CODA}) asymptotic theory for semi-parametric models. Statistics in Medicine. doi
Robins, James and Li, Lingling and Tchetgen, Eric and van der Vaart, Aad (2008). Higher order influence functions and minimax estimation of nonlinear functionals. Probability and Statistics: Essays in Honor of David A. Freedman. doi
Robins, James and Tchetgen Tchetgen, Eric and Li, Lingling and van der Vaart, Aad (2009). Semiparametric minimax rates. Electronic Journal of Statistics. doi
Robins, James M. and Li, Lingling and Mukherjee, Rajarshi and Tchetgen Tchetgen, Eric and van der Vaart, Aad (2017). Minimax estimation of a functional on a structured high-dimensional model. The Annals of Statistics. doi
{CausalSmith} (2026). Sharp minimax rates for average treatment effects with discrete confounding under fixed overlap. . doi
Wu, Yihong and Yang, Pengkun (2020). Polynomial methods in statistical inference: Theory and practice. Foundations and Trends in Communications and Information Theory. doi
Armstrong, Timothy B. and Koles{\'a}r, Michal (2021). Finite-sample optimal estimation and inference on average treatment effects under unconfoundedness. Econometrica. doi

Formal layer — Lean correspondence

Every object below is formalized in Lean 4. Click a verified row to view its statement; the rest link to the Lean source.

Setups (3)

Setup S-1 — A finite superpopulation law $P$ on full-data atoms $(X,A,S(0),S(1),Y(0),Y(1),S,Y,R)\in[d]\times\{0,1\}^8$ , with observed surrogate and latent outcome $S=S(A)$ , $Y=Y(A)$ , observed record $O=(X,A,S,R,RY)$ and observed law $P_O$ the image of $P$ ; cell masses, the arrival probability $\rho_P(x,a,s)$ and arrived-outcome regression $\mu_P(x,a,s)$ are totalized to zero on null cells, and $\tau(P)=\mathbb E_P[Y(1)-Y(0)]$ . The known floor $q\in[1/2,1]$ gives $\delta=1-q$ , and $\ell_n=\log(e+n)$ .
Setup S-2 — The observed sample $O_1,\ldots,O_n$ is iid from $P_O$ (product law $P_O^{\otimes n}$ on $O^n$ ). Estimators are measurable maps $O^n\to[-1,1]$ ; confidence procedures are measurable maps to closed subintervals $[L,U]\subseteq[-1,1]$ . Minimax squared risk and worst-law expected length are taken over $\mathcal M(d,q)$ at fixed noncoverage $\alpha\in(0,1/2)$ ; $r_{n,d,q}=n^{-1}+g_{n,d,q}^2$ with $g_{n,d,q}=\delta\min\{1,d/(n\ell_n)\}$ .
Setup S-3 — Pairs of priors $\Pi_-,\Pi_+$ supported on $\mathcal M(d,q)$ , their prior-predictive sample laws $Q_\sigma^{(n)}=\int P_O^{\otimes n}\,d\Pi_\sigma(P)$ , total variation between them, and a separation constant $c_\beta$ at fixed tolerance $\beta\in(0,1/4)$ .

Definitions (9)

Definition P-1 verified CausalSmith.Stat.MarNearcompleteFrontier.LawClass $\mathcal M(d,q)=\{P: |\operatorname{supp}_P(X)|\le d,\ P\text{ satisfies balanced randomized independence, consistency, MAR, and the cellwise arrival floor }q\}$
Definition P-2 verified CausalSmith.Stat.MarNearcompleteFrontier.psi $\Psi(P_O)=\sum_{x=1}^{d}\sum_{s=0}^{1}\{P(X=x,S=s\mid A=1)\mu_P(x,1,s)-P(X=x,S=s\mid A=0)\mu_P(x,0,s)\}$ , where $\mu_P(x,a,s)=0$ if $P(X=x,A=a,S=s,R=1)=0$ , and each weighted contribution is assigned zero if $P(X=x,A=a,S=s)=0$ .
Definition P-3 verified CausalSmith.Stat.MarNearcompleteFrontier.rate $r_{n,d,q}=n^{-1}+(1-q)^2\min\{1,[d/(n\log(e+n))]^2\}=n^{-1}+g_{n,d,q}^2$
Definition P-4 verified CausalSmith.Stat.MarNearcompleteFrontier.pointMinimaxRisk $\mathfrak R^*_{n,d,q}=\inf_{T\in\mathcal T_n}\sup_{P\in\mathcal M(d,q)}\mathbb E_P[(T(O_1,\ldots,O_n)-\tau(P))^2]$
Definition P-5 verified CausalSmith.Stat.MarNearcompleteFrontier.HonestIntervalClass $\mathcal C_\alpha(n,d,q)=\{I:O^n\to\{[L,U]\subseteq[-1,1]\}:\inf_{P\in\mathcal M(d,q)}P\{\tau(P)\in I(O^n)\}\ge1-\alpha\}$
Definition P-6 verified CausalSmith.Stat.MarNearcompleteFrontier.lengthMinimaxRisk $\mathfrak L^*_{n,d,q,\alpha}=\inf_{I\in\mathcal C_\alpha(n,d,q)}\sup_{P\in\mathcal M(d,q)}\mathbb E_P[\operatorname{length}\{I(O^n)\}]$
Definition P-7 verified CausalSmith.Stat.MarNearcompleteFrontier.tauhatMM Let $m=n/8$ , $k=\max\{1,\lfloor\ell_n/64\rfloor\}$ , and $B=256\ell_n$ . Draw an auxiliary $N\sim\operatorname{Poisson}(n/2)$ ; return zero when $N>n$ , otherwise use the following total extension on the Cartesian observed-record space: write $Y_i^{\mathrm{obs}}=(RY)_i$ for the supplied fifth coordinate (under the observation map it equals $R_iY_i$ and is zero when the outcome is missing), and thin the first $N$ records into four equiprobable streams. For $j=(x,a,s)$ , let $V_j=M_j^{(2)}/m$ be its stream-two missing count divided by $m$ , let $C'_j$ be its stream-three arrived count, and let $C_j$ be its stream-four arrived count and $U_j$ its stream-four count with supplied observed mark $Y^{\mathrm{obs}}=1$ (hence its arrived-success count on the observation-map support). Write $Q_k(z)=\{1-T_k(1-2z/B)\}/(2k^2z/B)$ , with $Q_k(0)=1$ , and $1-Q_k(z)=\sum_{v=1}^{k-1}a_vz^v$ . Set $H_j=\sum_va_v(U_j-C_j/2)(C_j-1)_{v-1}$ , $D_j=(U_j/C_j-1/2)\mathbf 1\{C_j>0\}$ , and $G_j=H_j\mathbf 1\{C'_j\le B/4\}+D_j\mathbf 1\{C'_j>B/4\}$ . The randomized estimate is $\widetilde\tau=\Pi_{[-1,1]}[2m^{-1}\sum_{i\in\mathrm{stream}\ 1}(2A_i-1)R_i(Y_i^{\mathrm{obs}}-1/2)+2\sum_j(2a_j-1)V_jG_j]$ . Define $\widehat\tau_{\mathrm{MM}}=\mathbb E[\widetilde\tau\mid O_1,\ldots,O_n]$ . If $q=1$ , define $\widehat\tau_{\mathrm{MM}}=\Pi_{[-1,1]}[2n^{-1}\sum_{i=1}^{n}(2A_i-1)Y_i^{\mathrm{obs}}]$ . Otherwise, when $\ell_n<128$ or $d\ge n\ell_n$ , define $\widehat\tau_{\mathrm{MM}}=\Pi_{[-1,1]}[2n^{-1}\sum_{i=1}^{n}(2A_i-1)R_i(Y_i^{\mathrm{obs}}-1/2)]$ .
Definition P-8 verified CausalSmith.Stat.MarNearcompleteFrontier.intervalMM $\widehat I_{\mathrm{MM},\alpha}(O^n)=[\max\{-1,\widehat\tau_{\mathrm{MM}}-h_{n,d,q,\alpha}\},\min\{1,\widehat\tau_{\mathrm{MM}}+h_{n,d,q,\alpha}\}]$ , where $h_{n,d,q,\alpha}=\min\{2,\sqrt{C_Ur_{n,d,q}/\alpha}\}$ and $C_U$ is any universal constant certified by Lemma $\mathrm{lem{:}upper\text{-}risk}$ .
Definition P-9 verified CausalSmith.Stat.MarNearcompleteFrontier.pairedPriorHandle Put $\delta=1-q$ , $L=\log(e+n)$ , $K=\lceil 8L\rceil$ , $h=K^{-2}$ , $m=K-1$ , $B_0=K/(1024n)$ , $M=\min\left\{\left\lfloor\frac{d-1}{2}\right\rfloor,\left\lfloor nL\right\rfloor\right\}, \qquad c_0=\frac1{16},\qquad b=1-\frac{\delta}{2},\qquad \mu_0=\frac{b^2}{2q}.$ For $0\le i\le m$ , define $x_i=\frac{1+h}{2}+\frac{1-h}{2}\cos\frac{i\pi}{m},$ let $l_i$ be the Lagrange cardinal polynomial for the nodes $x_0,\ldots,x_m$ , and put $D=\sum_{i=0}^{m}|l_i(0)|, \qquad \nu_i=\frac{l_i(0)}{D}.$ Define a latent pair $(p,z)\in[0,B_0]\times\{-1,1\}$ by assigning mass $h|\nu_i|/x_i$ to $(B_0x_i,\operatorname{sign}(\nu_i))$ for every $i$ , and assigning the residual mass to $(0,1)$ . Draw $(p_j,z_j)$ , $1\le j\le M$ , independently from this latent distribution and draw independent fair signs $r_j\in\{-1,1\}$ . For $\sigma\in\{-1,1\}$ , pair $j$ consists of two baseline labels, each with unnormalized mass $p_j$ , whose orientations are $u=r_j$ and $u=-r_j$ . For a unit at either label, let $X$ equal that label, set $S(0)=S(1)=0$ , let $A$ be a fair coin, set $Y(0)=0$ , and set control arrival equal to one. In the treated arm define $\rho_{\sigma,j,u}=1-\frac{\delta}{2}(1+\sigma z_ju), \qquad \mu_{\sigma,j,u}=\frac{b/2+c_0u}{\rho_{\sigma,j,u}},$ draw $Y(1)$ as a Bernoulli variable of mean $\mu_{\sigma,j,u}$ , and draw treated arrival independently of $Y(1)$ with probability $\rho_{\sigma,j,u}$ . In the coordinate order $(A,R,RY)=(0,1,0),(1,0,0),(1,1,1),(1,1,0),$ the four observed atom coefficients at orientation $u$ are exactly $v_{\sigma}(z_j,u)= \left( \frac12, \frac{\delta(1+\sigma z_ju)}4, \frac b4+\frac{c_0u}{2}, \frac b4-\frac{c_0u}{2}-\frac{\sigma\delta z_ju}{4} \right).$ The two orientations therefore specify the complete eight-coordinate observed atom vector for pair $j$ . For every label, set the observed variables by $S=S(A)$ and $Y=Y(A)$ . Add one fixed filler label of unnormalized mass $f=1-2MhB_0.$ At the filler set $S(0)=S(1)=0$ , $Y(0)=0$ , make both arrivals complete, and draw $Y(1)$ as a Bernoulli variable of mean $\mu_0$ . Its four observed atom coefficients in the same coordinate order are $v_{\mathrm{fill}}=\left(\frac12,0,\frac{\mu_0}{2},\frac{1-\mu_0}{2}\right).$ The exact algebraic normalization map is $J=f+2\sum_{j=1}^{M}p_j, \qquad f\longmapsto \frac fJ, \qquad p_j\longmapsto \frac{p_j}{J}\quad\text{for each of the two labels in pair }j.$ Let $P_{\sigma}$ denote the normalized causal law produced by this map, let $\Pi_{\sigma}$ be its distribution under the latent draws, and define $Q_{\sigma}^{(n)}=\int P_{\sigma,O}^{\otimes n}\,d\Pi_{\sigma}(P_{\sigma})$ . For the associated unnormalized count experiment, set $\lambda=4n$ . Conditional on the latent variables, assign independent Poisson counts with means $\lambda p_jv_{\sigma}(z_j,r_j)$ and $\lambda p_jv_{\sigma}(z_j,-r_j)$ to the eight atoms of pair $j$ , and means $\lambda f v_{\mathrm{fill}}$ to the filler atoms. Fix a record $o_{\circ}\in O$ . The count-ordering/truncation kernel $\kappa_n$ , which has no dependence on $\sigma$ or on any latent variable, uniformly orders the counted multiset and returns its first $n$ records when the total count is at least $n$ , and returns $(o_{\circ},\ldots,o_{\circ})\in O^n$ otherwise.

Assumptions (6)

Assumption A-1 verified CausalSmith.Stat.MarNearcompleteFrontier.IidSample $O_1,\ldots,O_n\stackrel{\mathrm{iid}}{\sim}P_O$
Assumption A-2 verified CausalSmith.Stat.MarNearcompleteFrontier.RandomizedIndependence $A\perp (X,S(0),S(1),Y(0),Y(1))$
Assumption A-3 verified CausalSmith.Stat.MarNearcompleteFrontier.BalancedRandomization $P(A=1)=1/2$
Assumption A-4 verified CausalSmith.Stat.MarNearcompleteFrontier.Consistency $(S,Y)=(S(A),Y(A))$
Assumption A-5 verified CausalSmith.Stat.MarNearcompleteFrontier.MissingAtRandom $R\perp Y\mid(X,A,S)$
Assumption A-6 verified CausalSmith.Stat.MarNearcompleteFrontier.ArrivalFloor $P(X=x,A=a,S=s)>0\Longrightarrow\rho_P(x,a,s)\ge q$

Lemmas (5)

Lemma L-1 verified CausalSmith.Stat.MarNearcompleteFrontier.tau_eq_psi For every $P\in\mathcal M(d,q)$ , the standard randomized-MAR identification calculation gives $\tau(P)=\Psi(P_O)$ , with every contribution from a null $(X,A,S)$ cell equal to zero by definition.
Lemma L-2 verified CausalSmith.Stat.MarNearcompleteFrontier.upper_risk There is a universal numerical constant $C_U<\infty$ such that, for every $n,d\ge1$ and $q\in[1/2,1]$ , $\sup_{P\in\mathcal M(d,q)}\mathbb E_P[(\widehat\tau_{\mathrm{MM}}-\tau(P))^2]\le C_U r_{n,d,q}$ .
Lemma L-3 verified CausalSmith.Stat.MarNearcompleteFrontier.parametric_floor There is a universal numerical constant $c_0>0$ such that $\mathfrak R^*_{n,d,q}\ge c_0/n$ for all $n,d\ge1$ and $q\in[1/2,1]$ ; for each fixed $\alpha\in(0,1/2)$ , there is $c_{0,\alpha}>0$ such that $\mathfrak L^*_{n,d,q,\alpha}\ge c_{0,\alpha}n^{-1/2}$ on the same range.
Lemma L-4 verified CausalSmith.Stat.MarNearcompleteFrontier.prior_reduction By Theorem $\mathrm{thm{:}normalized\text{-}converse}$ , with $\beta_0=1/16$ , every estimator satisfies $\mathfrak R^*_{n,d,q}\ge(13/32)c_{\beta_0}^2g_{n,d,q}^2$ whenever $g_{n,d,q}^2\ge n^{-1}$ . For fixed $\alpha\in(0,1/2)$ , set $\beta_\alpha=(1-2\alpha)/8$ ; every honest connected interval satisfies $\mathfrak L^*_{n,d,q,\alpha}\ge(5/4)c_{\beta_\alpha}(1-2\alpha)g_{n,d,q}$ on the same regime. If $g_{n,d,q}^2<n^{-1}$ , or if $q=1$ , Lemma $\mathrm{lem{:}parametric\text{-}floor\text{-}infrastructure}$ instead gives the point and interval lower bounds of orders $n^{-1}$ and $n^{-1/2}$ . Hence, throughout $q\in[1/2,1]$ , the combined lower bounds are constant multiples of $r_{n,d,q}$ and $\sqrt{r_{n,d,q}}$ .
Lemma L-5 verified CausalSmith.Stat.MarNearcompleteFrontier.honest_interval_construction For every $n,d\ge1$ , $q\in[1/2,1]$ , and $\alpha\in(0,1/2)$ , the clipped interval $\widehat I_{\mathrm{MM},\alpha}$ belongs to $\mathcal C_\alpha(n,d,q)$ . Pointwise, $\operatorname{length}(\widehat I_{\mathrm{MM},\alpha})\le\min\{2,2h_{n,d,q,\alpha}\}=\min\{2,2\sqrt{C_Ur_{n,d,q}/\alpha}\}$ , so the same bound holds for its worst-law expected length. If $h_{n,d,q,\alpha}<2$ , Markov's inequality and Lemma $\mathrm{lem{:}upper\text{-}risk}$ give noncoverage probability at most $\alpha$ . If $h_{n,d,q,\alpha}=2$ , coverage is deterministic because both $\widehat\tau_{\mathrm{MM}}$ and $\tau(P)$ lie in $[-1,1]$ .

Theorems (4)

Theorem T-1 verified CausalSmith.Stat.MarNearcompleteFrontier.point_frontier There exist universal numerical constants $0<c<C<\infty$ such that $c r_{n,d,q}\le\mathfrak R^*_{n,d,q}\le C r_{n,d,q}$ for every $n,d\ge1$ and $q\in[1/2,1]$ .
Theorem T-2 verified CausalSmith.Stat.MarNearcompleteFrontier.interval_frontier For each fixed $\alpha\in(0,1/2)$ , there exist constants $0<c_\alpha<C_\alpha<\infty$ , depending only on $\alpha$ , such that $c_\alpha\sqrt{r_{n,d,q}}\le\mathfrak L^*_{n,d,q,\alpha}\le C_\alpha\sqrt{r_{n,d,q}}$ for every $n,d\ge1$ and $q\in[1/2,1]$ .
Theorem T-3 verified CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_reduction At $q=1$ , $g_{n,d,1}=0$ , $r_{n,d,1}=n^{-1}$ , and $\widehat\tau_{\mathrm{MM}}=\Pi_{[-1,1]}[2n^{-1}\sum_{i=1}^{n}(2A_i-1)Y_i]$ , the projected complete-outcome Horvitz--Thompson randomized-difference estimator. Since $\tau(P)\in[-1,1]$ , projection is contractive toward $\tau(P)$ , and $\sup_{P\in\mathcal M(d,1)}\mathbb E_P[(\widehat\tau_{\mathrm{MM}}-\tau(P))^2]\le\sup_{P\in\mathcal M(d,1)}\mathbb E_P[(2n^{-1}\sum_{i=1}^{n}(2A_i-1)Y_i-\tau(P))^2]\le4/n$ . The two headline frontiers therefore reduce uniformly in $d$ to orders $n^{-1}$ and $n^{-1/2}$ .
Theorem T-4 verified CausalSmith.Stat.MarNearcompleteFrontier.normalized_converse For every fixed $\beta\in(0,1/4)$ , there is a constant $c_\beta>0$ such that, whenever $n,d\ge1$ , $q\in[1/2,1]$ , and $g_{n,d,q}^2\ge n^{-1}$ , there are priors $\Pi_-$ and $\Pi_+$ , supported on $\mathcal M(d,q)$ , whose complete observed-sample mixtures satisfy $\operatorname{TV}(Q_-^{(n)},Q_+^{(n)})\le\beta$ , and there is a deterministic $m_0$ for which $\Pi_-\{\tau(P)\le m_0-c_\beta g_{n,d,q}\}\ge1-\beta$ and $\Pi_+\{\tau(P)\ge m_0+c_\beta g_{n,d,q}\}\ge1-\beta$ .

Auxiliary Lean lemmas (machine-checked) (629)

Definition ClassLaw —
Definition Estimator —
Definition gScale —
Definition Honest —
Definition IntervalProc —
Definition priorEventMass —
Definition priorPredictive —
Definition tau —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tau_range —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countOrderingKernel_below —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.ell_pos_for_normalization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorK_lower_for_normalization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorH_le_one_for_normalization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.interpolationNode_nonneg_for_normalization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countAtomMass_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pmf_toMeasure_finset_decomposition —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorK_ge_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.interpolationNode_injective —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.uniformOrdering_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_node_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_node_pos —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_signed_total_le_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.obsMass_sum_event —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.observed_arm_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.observed_cell_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.observed_arrived_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.observed_arrived_outcome_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.condCellMass_observed —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.outcomeMean_observed —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.arrivalMass_pos —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.outcomeMean_identified_cell —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellMass_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellMass_le_armMass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellOutcome_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellOutcome_le_cell —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellContribution_identified —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.cellOutcome_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.massOf_potential_partition —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomized_potential_event —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.massOf_univ_eq_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.armMass_false_eq_half —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.armOutcome_consistency —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tau_eq_potential_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomized_arm_outcome —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.bernoulliFactor_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.bernoulliFactor_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairRho_mem_unit —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMu_mem_unit —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentZ_abs_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.orientation_abs_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pair_sign_mem_unit —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentP_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedAtomWeight_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_gScale —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_estimator —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_unprojected_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.clipUnit_contracts —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_projection_error —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_projection_risk —
Definition CausalSmith.Stat.MarNearcompleteFrontier.completeHTScore —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.completeHTScore_range —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.completeHTScore_variance_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.unprojectedHT_eq_average —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.completeHTScore_memLp —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_unprojected_risk_of_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.completeHTScore_integral_eq_arrived —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_missing_cell_mass_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_missing_atom_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_arrived_outcome_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_score_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.converseConstant_spec —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pointRate_from_floor_and_separation —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.intervalRate_from_floor_and_separation —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.gScale_nonneg_of_q —
Definition CausalSmith.Stat.MarNearcompleteFrontier.fullAtomTuple —
Definition CausalSmith.Stat.MarNearcompleteFrontier.fullAtomTupleEquiv —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_fillerAtomWeight —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_pairAtomWeight —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_pairedAtomWeight_real —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedAtomWeight_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_fullMass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_consistency —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_balanced —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_fillerAtomWeight_arm —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_pairAtomWeight_arm —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_controlOutcome_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_arm_potential_symmetry —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_arm_potential_symmetry —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_arm_potential_symmetry —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_randomized —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairLabel_injective —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerLabel_ne_pairLabel —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_other_pair_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_pair_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_filler_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_arrival_floor_pointwise —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_arrival_floor_pointwise —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedAtomWeight_arrival_floor_pointwise —
Definition CausalSmith.Stat.MarNearcompleteFrontier.fullAtomArrivalEquiv —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fullAtom_sum_by_arrival —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_floor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mar_of_complete_arrival —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mar_of_cellwise_arrival_factor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_arrival_factor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_arrival_factor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedAtomWeight_at_filler —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedAtomWeight_at_pair —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lawClass_mono_floor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_chisq_bound —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_chisq_identity —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_chisq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_product_tv_of_chisq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_product_tv_half —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_radius_budget —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_product_tv_at_radius —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_product_tv_at_budget —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_radius_budget_at_tolerance —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_product_tv_at_tolerance_radius —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.squaredLoss_of_left_target_and_right_test —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.squaredLoss_of_right_target_and_left_test —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.interval_length_of_separated_hits —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_floor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.complete_arrival_lawClass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_isProbability —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_event_transfer —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorEventMass_complement —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorEventMass_failure_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pointMinimaxRisk_lower_of_pair —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lengthMinimaxRisk_lower_of_law —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_separated_intersection —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_event_eq_integral —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorAverage_le_of_pointwise —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_event_from_good —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_integral_eq_priorAverage —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.intervalLength_integrable_prior —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lengthMinimaxRisk_lower_of_prior —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_intervalLength_ge_event —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorIntervalRisk_separation —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sampleIntegral_ge_event —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.leftPrior_sampleRisk_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.rightPrior_sampleRisk_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorAverage_eventRisk_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pointRisk_integrable_prior —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPointTest_BayesSum_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pointMinimaxRisk_lower_of_priors —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPointRisk_separation —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.missingWeight_sq_div_one_add_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.uniformFourMass_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.finiteStreamSum_labeledPrefix —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.finiteStreamCount_labeledPrefix —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fourStreamEstimate_labeledPrefix —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tauhatMM_nonfallback_eq_fixedStatistic —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.converse_smallN_separation —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.arrivedCellMass_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.arrivedCellMass_le_cellMass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.arrivedCellMass_eq_mul_arrivalProb —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.missingCellMass_bounds —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_cellMass_eq_armMass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_cellMass_eq_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_missingCellMass_le_delta —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tau_eq_arrived_missing_cells —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_v_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_v_second_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_arrived_count_law —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_factorial_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_light_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_map_finitePoissonSampleLaw_finiteSampleMap —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_eventCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_finitePoissonSampleLaw_eventCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_finiteStreamCount_eq_eventCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_shiftedFalling_descFactorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_shiftedFalling_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_success_weighted_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.observedLaw_RY_implies_R_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.streamU_eq_arrivedSuccess_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_branch_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_light_prob_poisson —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_variance_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.missingCellMass_heavy_variance_budget —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamD_abs_le_half_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_vd_second_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_vd_mean —
Definition CausalSmith.Stat.MarNearcompleteFrontier.NormalizedCertificate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.EventualNormalizedCertificate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_converse_smallN —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_converse_of_eventual_certificate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_point_pair_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_length_lower_of_law —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_interval_pair_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalizedCertificate_mono —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorPredictive_pure —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorEventMass_pure —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametricFullLaw_complete —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametricFullLaw_consistency —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametricFullLaw_balanced —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametricFullLaw_randomized —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametricFullLaw_tau —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_observed_ac —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_observed_chisq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_oneCell_lawClass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.parametric_oneCell_pair —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairedWeightedSign —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_target_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_target_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMu_opposite_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMu_orientation_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_tau_exact —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lagrangeAtZero_sum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.signedNodeWeight_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.signedNodeWeight_abs_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeightedSign_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_tau_separated —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedWeightedSign_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedWeightedSign_variance_bound —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalizationJ_moments —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.paired_target_good_event_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedWeightedSign_apply —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.interpolationNode_le_one_target —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeightedSign_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_nonneg_target —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.oneLatentLaw_toReal —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.thetaLaw_integral_fst —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.finiteProduct_centered_sum_sq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentMass_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentMass_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.finiteProduct_sum_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.standard_exterior_basis_sign —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.standard_exterior_lagrange_abs_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lagrange_basis_eval_affine_local —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.shifted_chebyshev_lagrange_abs_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.calibrated_chebyshev_exterior_le_cosh_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lagrangeNorm_eq_abs_chebyshev —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lagrangeNorm_le_cosh_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.one_le_ell_scale —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.priorK_le_nine_ell —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.nat_half_sub_one_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.floor_half_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairCount_lower_quarter —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.regime_dimension_ge_three —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairCount_scale_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.eventually_ell_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.regime_min_scale_sq_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.eventually_priorK_sq_div_pairCount_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lagrangeNorm_ge_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedMean_scale_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.finite_memLp —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedWeightedSign_tail_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalizationJ_tail_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedPrior_minus_event_mass_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedPrior_plus_event_mass_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedPrior_target_events_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.paired_predictive_tv_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalizationJ_ge_half —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.poisson_lower_tail_of_two_mul_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalization_count_poisson_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalization_count_poisson_tail_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_fillerObservedCoeff_at_label —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.sum_pairObservedCoeff_at_label —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countAtomMass_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_sign_flip —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_orientation_linear_cancel —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_le_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latent_signed_power_moment_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedCountLaw_tv_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.paired_count_to_predictive_tv_eventual —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.thetaLaw_normalization_count_poisson_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.conditionalCountLaw_singleton_product —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.conditionalCountLaw_singleton_likelihood —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedCountLaw_singleton_likelihood —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairBlockCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedCountLaw_tv_le_factorial_tail —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairObservedMonomial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedMonomial_sign_flip —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedMonomial_orientation_sign_flip —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedMonomial_mem_unit —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countAtomMass_at_pair_label —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countAtomMass_at_filler_label —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.prod_by_observed_label —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pair_label_power_factorization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_orientation_square_gap —
Definition CausalSmith.Stat.MarNearcompleteFrontier.signedExponentialSeriesTail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.exp_neg_eq_truncated_add_signed_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.abs_signedExponentialSeriesTail_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.factorial_series_convolution —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.exponentialSeriesTail_add_convolution —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairObservedCoeff_bool_orientation_linear_cancel —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fintype_nat_sum_eq_one —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_degree_zero —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_singleton —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_degree_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_gap_le_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.probability_real_singleton_tsum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.probability_measureReal_eq_tsum_singletons —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tvDist_le_half_tsum_singleton_abs —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedCountLaw_singleton_l1_le_factorial_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_nonneg_count —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.oneLatentLaw_toReal_count —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.thetaLaw_product_factorization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.poissonFactorial_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_sign_flip —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockMarkAverage_gap_factor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentZ_eq_neg_one_or_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlock_taylor_coefficient_cancel —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlock_low_total_coefficient_cancel —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.interpolationNode_le_one_count —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentP_le_priorB_count —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.latentWeight_sum_real_count —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlock_taylor_coefficient_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.abs_prod_sub_prod_le_sum_abs —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.half_pairBlockMarkAverage_mem_unit —
Definition CausalSmith.Stat.MarNearcompleteFrontier.activeBaselineLabels —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countAtomMass_eq_zero_of_unused —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.prod_activeBaselineLabels —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.prod_split_active_unused_labels —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.zero_rate_factor_eq_indicator —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.summable_poissonFactorial_countVector —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tsum_le_one_of_le_poissonFactorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.obsProd_split_filler_pairs_unused —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairLabelFactorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pair_label_poisson_power_factorization —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairBlockFactorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pair_block_poisson_power_factorization —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.theta_pair_likelihood_factorization —
Definition CausalSmith.Stat.MarNearcompleteFrontier.commonCountFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.conditional_count_likelihood_block_split —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedCountLaw_singleton_factorization —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.heavyProductVariance_algebra_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.heavyProductVariance_budget —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.factorial_countVector_tsum_eq_exp_sum —
Definition CausalSmith.Stat.MarNearcompleteFrontier.weightedProductTelescope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.list_prod_sub_prod_eq_weightedProductTelescope —
Definition CausalSmith.Stat.MarNearcompleteFrontier.weightedProductTelescopeAbs —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.abs_weightedProductTelescope_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_abs_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.abs_fintype_prod_sub_prod_le_weighted —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixture_product_gap_le_weighted —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_cellEta_abs_le_half —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamPilotLightProb_bounds —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_sum —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedRate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedRate_coe —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedRate_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedRate_factorial_tsum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_cell_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_qPoly_nonneg_on_positive —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_z_mul_qPoly_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_pilot_lower_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_pilot_upper_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_at_label —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedLocalFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedLocalFactor_eq —
Definition CausalSmith.Stat.MarNearcompleteFrontier.labelPoissonFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.prod_labelPoissonFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.labelPoissonFactor_countVector_tsum_one —
Definition CausalSmith.Stat.MarNearcompleteFrontier.assembledLabelRate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor_eq_assembled —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_light_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_heavy_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_qPoly_eval_zero —
Definition CausalSmith.Stat.MarNearcompleteFrontier.partitionedLocalRate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.partitionedLocalRate_filler —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.partitionedLocalRate_pair —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.partitionedLocalRate_unused —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor_partitioned_filler —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor_partitioned_pair —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.localLabelPoissonFactor_partitioned_unused —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.partitionedLocalPoisson_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_qPoly_le_one_on_positive —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairSideMarkedRate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairSideMarkedRate_coe —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairSideMarkedRate_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.poissonFactor_extract_exponential —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairSidePoissonFactor_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedPoissonFactor_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_cell_missing_qPoly_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerMass_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerObservedCoeff_nonneg —
Definition CausalSmith.Stat.MarNearcompleteFrontier.fillerMarkedRate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerMarkedRate_coe —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerMarkedRate_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerMarkedPoissonFactor_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.markedComponent_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.shiftedCheb_recurrence —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.shiftedCheb_coeffL1_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.correctionCoeff_weighted_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.thetaMarkedComponent_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.mixedFactorizedLikelihood_countVector_tsum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lightCorrection_abs_le_coeff_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.lightCorrection_sq_le_coeff_sum_sq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlock_taylor_coefficient_marked_envelope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.half_pairBlockMarkAverage_eq_average_localFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlock_normalized_taylor_coefficient_marked_envelope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_streamD —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_variance_uniform —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_variance_small_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countMixture_exponential_tail_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countMixture_factorial_tail_budget —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_successFraction_complement —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairBlockTaylorCoefficient —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_gap_hasSum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockTaylorCoefficient_eq_zero_of_matched —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_gap_eq_unmatched_tsum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_gap_abs_le_unmatched_tsum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockTaylorCoefficient_abs_le_factorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_gap_abs_le_factorial_remainder —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairAtomWeight_observed_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.fillerAtomWeight_observed_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairedFullLaw_observed_atom_mass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.conditionalCountLaw_eq_independentPoissonCountLaw —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.paired_predictive_tv_le_count_tv_add_inverse —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomScale_count_mixture_reconstruction —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomScale_ordered_tv_le_count_tv —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomScale_fixed_tv_le_count_tv_add_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.randomScale_fixed_tv_le_count_tv_add_inverse —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pmf_bind_eq_finite_mixture —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.factorial_countVector_fixed_degree_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_fixed_degree_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_average_fixed_degree_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_gap_fixed_degree_l1 —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_prod_eq_local_of_supported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedIntensity_prod_eq_zero_of_unsupported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairBlockCount_eq_total_of_supported —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedDegreeGap —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedDegreeGap_eq_local_of_supported —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_fixed_degree_l1 —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_eq_local_of_supported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_eq_zero_of_unsupported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_eq_zero_of_matched —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_total_degree_l1 —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_degree_tsum_le_factorial_tail —
Definition CausalSmith.Stat.MarNearcompleteFrontier.countTaylorDegreeEquiv —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.countTaylorDegree_fiber_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.summable_countTaylor_of_degree —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.tsum_countTaylor_eq_degree —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_degree_summable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_joint_summable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedTaylorCoefficient_joint_tsum_le_factorial_tail —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_eq_local_of_supported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_eq_zero_of_unsupported —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_gap_hasSum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_gap_abs_le_tsum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_l1_le_factorial_tail —
Definition CausalSmith.Stat.MarNearcompleteFrontier.pairCountRestriction —
Definition CausalSmith.Stat.MarNearcompleteFrontier.residualCountRestriction —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.splitCountBlocks_injective —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMixtureFactor_restrict —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_restrict —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.residualPoissonFactor_eq_common —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarked_component_eq_poisson —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_nonneg —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixtureFactor_hasSum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_likelihood_abs_gap_summable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_likelihood_tensor_gap_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_likelihood_fin_product_hasSum_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.normalized_likelihood_fin_product_l1_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.pairMarkedMixture_product_l1_le_factorial_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_polyDegree_log_lower —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_polyThreshold_degree_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_cell_missing_abs_qPoly_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_cell_pilot_bias_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_log_four_ge_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_heavy_empty_remainder_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_empty_remainder_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_heavy_empty_bias_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_missing_weight_half_bound —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_polynomial_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_large_cell_reduction —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_centered_shiftedFalling_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_lightCorrection_abs_le_factorial_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_lightCorrection_abs_le_power_sum —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_power_ratio_envelope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_lightCorrection_abs_le_degree_envelope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_lightCorrection_sq_le_degree_envelope —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_count_support_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_sq_le_degree_envelope_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamLaw_isProbabilityMeasure —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamV_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVD_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamD_mean_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVD_variance_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVD_variance_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_count_mul_descFactorial —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_count_power_factorial_expansion —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stirlingSecond_le_choose_mul_pow —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_count_power_factorial_expansion_real —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_power_integrable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_power_moment_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_poisson_power_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_finiteStreamCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_streamC —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_streamH —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamC_power_integrable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamC_power_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_sq_le_add_envelope_ae —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_sq_integrable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_second_moment_add_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_polyDegree_log_upper —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_log_bases_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_sixtyfour_pow_le_exp —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_light_growth_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_small_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_large_light_envelope_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_large_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_pilot_large_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_mean_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_large_prob_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamH_pilot_large_mean_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_large_centered_qPoly_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_centered_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_large_bias_abs_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_split_weighted_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_pilot_bias_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamV_indep_fourth —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamHD_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamHD_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVHD_second_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_streamG —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_sq_integrable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_missing_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_small_correction_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_small_correction_second_moment_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_three_stream_product_moment —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_second_moment_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_pilot_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_large_correction_second_moment_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_missing_second_moment_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_large_correction_second_moment_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_large_variance_exp_le_inv —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_large_correction_second_moment_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_correction_second_moment_sum_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_log_sixth_exp_bound —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_exp_ell_le_sample —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_variance_log_factor_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_variance_cross_term_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_variance_envelope_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_stream_correction_second_moment_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_variance_add_le_twice —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_sub_VD_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_variance_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_variance_sum_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_finiteSample_measurableSingletonClass —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_fourStreamEstimate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamEstimate_range —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_half_mean_cap_tail_exp —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_half_mean_cap_tail_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_nonfallback_risk_le_ideal_add_tail —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_nonfallback_risk_le_ideal_add_rate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_fallbackScore —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallbackScore_sq_le_one —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallbackHT_eq_average —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallback_average_sampling_risk —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallback_risk_le_bias —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_estimator_risk_le_four —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_small_log_risk_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_arrived_mass_mul_outcomeMean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallbackScore_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_missing_contrast_abs_le_delta —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallback_bias_abs_le_delta —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallback_risk_le_delta —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_large_dimension_risk_rate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.unprojectedHT —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_complete_arrival_risk_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallback_branches_risk_rate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount_measurable —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount_law —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamEventCount_variance —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear_eq_counts —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_eq_linear_add —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear_variance_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fallbackScore_mean_eq_event_difference —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamLinear_mean_eq_arrived —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamV_indep_streamG —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamVG_mean —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_bias_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_bias_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_risk_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamEstimate_risk_le_raw —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_nonfallback_rate_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_pilot_bias_remainder_sq_le —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_bias_sq_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamCorrectionSum_memLp_two —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamRawEstimate_variance_le_aggregate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_fourStreamEstimate_risk_le_aggregate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_nonfallback_risk_le_aggregate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamCorrectionSum_variance_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamCorrectionSum_variance_rate —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_nonfallback_risk_rate —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_streamHistogram —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_streamHistogram —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamHistogram_law —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamHistogram_iIndepFun —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_cellCoordinates —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_cellCoordinates_disjoint —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_cellHistogram_indepFun —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_finiteStreamCount_eq_histogram_sum —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_extendCellHistogram —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_cellHistogramCount —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_cellHistogramCount_eq —
Definition CausalSmith.Stat.MarNearcompleteFrontier.upper_cellHistogramCorrection —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_cellHistogramCorrection_eq —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_measurable_cellHistogramCorrection —
Lemma CausalSmith.Stat.MarNearcompleteFrontier.upper_streamCellCorrection_indepFun —

Symbol realizations (Lean @realizes) (37)

X verified realized by PotentialAtom
S0 verified realized by PotentialAtom
S1 verified realized by PotentialAtom
Y0 verified realized by PotentialAtom
Y1 verified realized by PotentialAtom
A verified realized by FullAtom
S verified realized by FullAtom, Consistency
Y verified realized by FullAtom, Consistency
R verified realized by FullAtom
O verified realized by Obs, observe
P verified realized by FullLaw, Consistency, LawClass
rho verified realized by arrivalProb, ArrivalFloor, pairRho
mu verified realized by outcomeMean, pairMu
tau verified realized by tau
M_dq verified realized by LawClass
Psi verified realized by psi
delta verified realized by delta
ell verified realized by ell
g_ndq verified realized by gScale
r_ndq verified realized by rate
T_n verified realized by Estimator
Rstar verified realized by pointMinimaxRisk
C_alpha verified realized by HonestIntervalClass
Lstar verified realized by lengthMinimaxRisk
Cheb verified realized by qPoly
tauhat_MM verified realized by tauhatMM
C_U verified realized by UpperRiskCertificate, intervalRadius
h_alpha verified realized by intervalRadius
Ihat_MM verified realized by intervalMM
PiPair verified realized by pairedPrior
QPair verified realized by pairedPredictive
alpha verified realized by interval_frontier
beta verified realized by normalized_converse
c_beta verified realized by converseConstant
n verified realized by point_frontier
d verified realized by point_frontier
q verified realized by point_frontier

Proof map 9 statements · 10 edges

Minimax Estimation and Honest Inference in Randomized Experiments with Missing Outcomes

Abstract

Introduction

Related work

Setup and statistical criteria

Minimax estimation and honest inference

Statistical implications

Limitations and future work

Appendices

Identification and estimation bounds

Identification under randomized MAR

Uniform estimation control

Honest clipped intervals

Normalized priors and the dimension lower bound

Testing reductions and proofs of the main results

Parametric sampling floors

From normalized priors to statistical lower bounds

Completion of the main comparisons

Verification note

Proofs of the main results

References