CausalSmith · AI Causal Scientist — exp_rollout_chebyshev_minimax_tv_envelope_rollout_design · Experimentation · AI reviewer score 5.8/10 · pinned commit 4e6bd94 · PDF · Lean code · Slides · arXiv · GitHub

Chebyshev Rollout Schedules for Polynomial Extrapolation under Low-Order Interference

Abstract

This paper studies how to place measurement rounds in a finite-population rollout experiment when the target is the full-adoption contrast but the rollout budget stops at a treated fraction $q < 1$ . Under static rollout consistency, a degree- $β$ polynomial restriction on the rollout mean curve, and a common round-mean variance envelope—restrictions that low-order interference motivates but that we impose rather than derive from a microfounded interference model—unbiased linear estimation reduces to a polynomial extrapolation problem from $[0, q]$ to $1$ . For a fixed schedule, the worst-case variance over the positive-semidefinite covariance class meeting this diagonal envelope equals the variance scale times the squared $ℓ^{1}$ (total-variation) norm of the polynomial-exact weights. The resulting diagonal-envelope amplification criterion, defined over linear unbiased estimators, attains its minimax value up to multiplicative constants at shifted Chebyshev-Lobatto measurement fractions when $q \leq q_{m a x} < 1$ and the number of rollout intervals satisfies $k \geq c β$ for some $c > 1$ . The minimax amplification is of order $(\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β},$ up to constants depending only on $q_{m a x}$ and the oversampling ratio. For the exact nested rollout covariance problem, the same Chebyshev schedule is rate-feasible through the envelope upper bound, and exact optimality under the true rollout covariance structure is posed as a separate covariance-specific design question.

Introduction

Rollout experiments often measure outcomes before full adoption. A platform may expose a small treated fraction before scaling a feature, a policy maker may expand access in stages, or a researcher may observe several rollout fractions strictly below the endpoint at which everyone is treated. Under interference, the treated-fraction mean response follows a rollout curve that can extend beyond the convex-combination structure of two no-interference potential outcomes. The full-adoption contrast must then be inferred from the response curve traced out by the rollout.

This paper studies the design problem of where to place the rollout measurement fractions. The estimand is the endpoint contrast $m_{P} (1) - m_{P} (0)$ , while the experiment observes round means on the truncated interval $[0, q]$ , with $q \leq q_{m a x} < 1$ . The design variable is the ordered schedule of treated fractions between the untreated baseline and the budget endpoint. The analysis is finite-population and design-based. Assumption 1 gives a static rollout potential-outcome interpretation indexed by contemporaneous assignments; Assumption 2 restricts the rollout mean curve to be a polynomial of degree at most $β$ ; and Assumption 3 bounds each round mean variance by a common scale $σ_{0}^{2} / n$ .

Under these conditions, the statistical problem becomes a polynomial extrapolation problem. Lemma 1 identifies the endpoint contrast with the sum of the nonconstant coefficients of the rollout mean curve. Definition 3 then characterizes linear weights that are unbiased for every degree- $β$ rollout mean curve by exactness on the monomials $1, u, \dots, u^{β}$ . Theorem 1 shows that, when cross-round covariances are left unrestricted except for positive semidefiniteness and the diagonal variance envelope, the worst-case variance bound for a linear unbiased estimator, sharp over the positive-semidefinite covariance class meeting the diagonal envelope, is $\frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ Thus the schedule affects the envelope risk only through the smallest squared $ℓ^{1}$ (total-variation, TV) norm of polynomial-exact weights, the amplification criterion $A_{β} (p)$ in Definition 5.

The main design result is Theorem 2. For any fixed low-budget cap $q_{m a x} \in (0, 1)$ , any oversampling ratio $c > 1$ , and any $k \geq c β$ , every admissible schedule has amplification at least a constant times $(\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β},$ uniformly over $0 < q \leq q_{m a x}$ . The shifted Chebyshev-Lobatto schedule in Definition 4 attains the same rate up to a constant depending only on $c$ and $q_{m a x}$ . The result is therefore a rate-minimax statement for the envelope criterion: low-budget extrapolation carries an exponential cost in the polynomial order, and endpoint-clustered Chebyshev-Lobatto placement controls the exponent that is unavoidable under the stated envelope.

The full-budget boundary clarifies what drives this cost. Proposition 2 shows that when $q = 1$ , $k = β$ , and the equal-spacing schedule $p^{eq} (β, 1)$ is used, the endpoint contrast can be estimated by the difference between the final and baseline round means with amplification at most $4$ , independent of $β$ . The exponential factor in Theorem 2 is therefore specifically the price of estimating an endpoint outside the observed rollout interval.

The exact nested covariance problem is kept separate. Definition 6 leaves inside the minimax problem the covariance matrix that a fully specified rollout law would generate, and Remark 1 poses exact optimality for that narrower problem. The proved one-sided comparison in Lemma 2 bounds the exact finite-population risk by the envelope amplification criterion at every admissible schedule. Consequently, Proposition 3 establishes the displayed low-budget exponential upper bound for the exact rollout risk attained by the Chebyshev-Lobatto schedule.

The paper contributes to the design-based interference literature by making the treated-fraction schedule itself the object of minimax analysis. Classical potential-outcome formulations treat no-interference experiments as the baseline case (Rubin, 1974; Imbens et al., 2015), while social-interaction and interference settings make spillovers part of the estimand and the dependence structure (Manski, 1993; Manski, 2013). Modern work has developed exposure mappings, randomization-based estimators, graph cluster designs, and randomization tests under interference (Aronow et al., 2017; Sävje et al., 2017; Eckles et al., 2017; Ugander et al., 2013; Athey et al., 2017; Basse et al., 2019; Puelz et al., 2019). The closest line of work is the low-order network-interference and rollout literature, where polynomial structure permits identification of global treatment effects from partial exposure or staged adoption (Cortez et al., 2022; Cortez-Rodriguez et al., 2022; Cortez-Rodriguez et al., 2024; Eichhorn et al., 2024). The present analysis keeps that polynomial-extrapolation structure and answers a new design question: conditional on a rollout budget, where should measurement fractions be placed to minimize the worst-case diagonal-envelope variance amplification among polynomial-exact linear estimators? Low-order interference motivates the imposed degree- $β$ polynomial mean restriction, while the contribution translates that restriction and the variance envelope into a sharp rollout-schedule design result.

The answer uses classical ideas from optimal design and approximation theory. Polynomial-regression design and equivalence theory provide the language for optimizing measurement locations (Smith, 1918; Kiefer et al., 1959; Kiefer, 1974; Pukelsheim, 1993), and Chebyshev systems explain why endpoint-spread nodes control polynomial extrapolation (Karlin et al., 1966). Here those approximation facts enter through the dual representation in Lemma 3: minimizing the $ℓ^{1}$ norm of unbiased weights is equivalent to controlling the largest endpoint contrast among degree- $β$ polynomials bounded at the schedule nodes. The paper translates the classical Chebyshev endpoint-extrapolation phenomenon and minimum- $ℓ^{1}$ optimal-recovery duality into a finite-population rollout measurement-schedule criterion under the round-mean variance envelope. To our knowledge, the resulting amplification criterion and Chebyshev-Lobatto rollout schedule are new design objects in that literature. The appendix records the formal verification scope for the paper’s formal statements and proofs.

Setup and Assumptions

We work with a finite-population rollout design. The population consists of a finite unit set $U_{n}$ with $n$ units. The experimenter chooses a sequence of rollout measurement rounds indexed by $j = 0, \dots, k$ , and the contemporaneous assignment vector at round $j$ is $Z_{j}$ . Let $Ω$ denote the finite assignment space generated by the rollout randomization, and let $π$ be the probability mass function on $Ω$ . For any design-measurable random variable $X$ , $E_{π} X$ , $Var_{π} (X)$ , and $Cov_{π} (X_{1}, X_{2})$ denote the corresponding finite-sum expectation, variance, and covariance under $π$ . The specific assignment law—how treatment is nested across rounds and how each target fraction is implemented—is not further specified here, because every result uses only the round-mean variance envelope of Assumption 3. The exact cross-round covariance a fully specified rollout law would induce is not part of the verified formal layer; it enters only through the symbolic benchmark $R_{exact}$ of the discussion, which we treat as a placeholder for future covariance-restricted design problems rather than as a fully specified finite-population object. Throughout, the schedule entries $p_{j}$ are target treated fractions and the formal results treat them as real design points in $[0, 1]$ ; in a finite population these targets may require rounding to feasible treatment counts. The formal results treat the realized measurement fractions as the schedule nodes, so unbiasedness holds exactly at those realized fractions; any gap between a target fraction and the realized fraction is a finite-sample perturbation of the moment conditions in Definition 3, outside the formal scope.

The potential-outcome notation is finite-population notation: $Y_{i} (Z_{j})$ is unit $i$ ’s outcome under the assignment vector realized at measurement $j$ , and $\overset{ˉ}{Y}_{j}$ is the observed finite-population round mean. The static rollout condition fixes the interpretation of these objects.

Assumption 1 [ass:static-rollout-consistency] (Static Rollout Consistency).

At each rollout measurement $j$ , the observed round mean is $\overset{ˉ}{Y}_{j} = n^{- 1} i \in U_{n} \sum Y_{i} (Z_{j}) .$ The potential outcomes $Y_{i} (Z_{j})$ depend on the contemporaneous assignment vector $Z_{j}$ , but not on earlier rollout steps.

⊢ Lean

Assumption 1 is the static rollout potential-outcomes condition with no carryover. It permits arbitrary contemporaneous interference through the assignment vector while ruling out lagged treatment histories as separate arguments of the potential outcome, as in static rollout formulations for interference designs (Cortez-Rodriguez et al., 2024).

A schedule is an ordered vector $p$ of treated fractions. The rollout budget $q$ is the final treated fraction, so the design observes the response curve only on $[0, q]$ , even though the target contrast compares $u = 0$ with $u = 1$ .

Definition 1 [def:budgeted-schedule-class] (Budgeted schedule class

S_{k, q}

The budgeted schedule class is $S_{k, q} = {p \in [0, 1]^{k + 1} : p_{0} = 0 and 0 < p_{1} < \dots < p_{k} = q} .$

⊢ Lean

Definition 1 makes the design variable explicit. The econometrician controls the placement of the rollout measurement fractions between the untreated baseline and the budget $q$ ; the strict inequalities guarantee distinct interior interpolation nodes for the polynomial problem below.

The mean response curve under a law $P$ is $m_{P} (u)$ . The low-order interference restriction used here is that the design mean along the rollout path is a polynomial of degree at most $β$ .

Assumption 2 [ass:beta-order-polynomial] (Polynomial Rollout Mean).

For every law $P$ , the rollout mean curve satisfies $m_{P} (u) = ℓ = 0 \sum β a_{P, ℓ} u^{ℓ}$ for all $u \in [0, 1]$ .

⊢ Lean

Assumption 2 is the beta-order rollout polynomial identity condition. It summarizes low-order interference along the treated-fraction path by requiring the average response to be exhausted by powers $u^{0}, \dots, u^{β}$ , a restriction used in polynomial exposure and rollout representations of interference (Cortez et al., 2022). This form arises, for instance, when each unit’s outcome depends on the assignment vector only through interactions of order at most $β$ among units, and the rollout assigns treatment so that, at target fraction $u$ , the probability that any fixed set of $ℓ \leq β$ units is jointly treated is a polynomial in $u$ of degree $ℓ$ (as under independent Bernoulli assignment at rate $u$ ; fixed-count or rounded rollout schemes satisfy this only approximately, since their joint-treatment probabilities are not exactly $u^{ℓ}$ ); averaging the bounded-order response over that assignment then yields a degree- $β$ polynomial mean curve, with $β$ the maximum interaction order. Absent such bounded-order structure the result should be read as an optimal-extrapolation theorem for an imposed degree- $β$ mean curve rather than a generic interference-design guarantee; because the target $u = 1$ lies outside the observed interval, misspecifying $β$ biases the extrapolated endpoint contrast, and this bias is amplified precisely in the low-budget regime. The endpoint contrast studied below is $τ_{P} = m_{P} (1) - m_{P} (0)$ .

The next restriction is a sharp variance envelope that isolates the effect of treated-fraction placement from additional covariance structure.

Assumption 3 [ass:round-mean-variance-envelope] (Round-Mean Variance Envelope).

For every law $P$ , every admissible schedule $p$ , and every rollout measurement $j$ , $Var_{π} (\overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} .$

⊢ Lean

Assumption 3 is specific to this analysis. It bounds each round mean by the common scale $σ_{0}^{2}$ / $n$ while leaving the cross-round covariance signs and magnitudes otherwise unrestricted subject to positive semidefiniteness. This is the envelope under which the worst-case variance reduces to an amplification problem for the estimator weights. The scale $σ_{0}^{2}$ absorbs both the outcome magnitudes and the design’s cross-unit dependence. Boundedness of outcomes alone does not control it: under common or strongly dependent randomization a finite-population round mean can have variance of order $1$ rather than $1/ n$ . The envelope holds with $σ_{0}^{2}$ a fixed constant when outcomes are bounded and the design induces only weak (for example, bounded-neighborhood) cross-unit dependence, as under independent or locally dependent Bernoulli assignment; under stronger dependence the round-mean variance decays more slowly in $n$ , and the results then apply with $σ_{0}^{2}$ read as the relevant (possibly $n$ -dependent) envelope scale, with the amplification bounds interpreted at that scaling.

For the low-budget results, the budget remains uniformly below full rollout.

Assumption 4 [ass:low-budget-cap] (Low-Budget Cap).

The rollout budget and its cap satisfy $0 < q_{m a x} and q \leq q_{m a x} < 1.$

⊢ Lean

Assumption 4 is also specific to this analysis. The cap $q_{m a x}$ keeps the problem in the extrapolation regime: the target endpoint $u = 1$ lies outside the observed interval $[0, q]$ . The boundary case $q = 1$ is therefore separated from the low-budget rate calculations. Every result invoking this assumption also imposes $q > 0$ ; when $q = 0$ the budgeted schedule class $S_{k, q}$ is empty, so the operative low-budget regime is $0 < q \leq q_{m a x} < 1$ .

The admissible law class collects the preceding restrictions and pins the design expectation of each round mean to the polynomial curve at the corresponding schedule point.

Definition 2 [def:rollout-law-class] (Rollout law class

P_{β}

The rollout law class is $P_{β} = {P : P satisfies Assumption 1, Assumption 2, and Assumption 3, and E_{π} [\overset{ˉ}{Y}_{j}] = m_{P} (p_{j}) for every j = 0, \dots, k} .$

⊢ Lean

Thus $P_{β}$ is a finite-population law class indexed by the common polynomial order and variance scale, with the schedule entering through the evaluation points $p_{j}$ . The condition $E_{π} [\overset{ˉ}{Y}_{j}] = m_{P} (p_{j})$ is the bridge between the randomization distribution and the deterministic polynomial approximation problem.

We estimate the endpoint contrast with a linear rollout estimator $\overset{τ}{^}_{w, p} = j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j},$ where $w$ is a vector of weights applied to the observed round means. Unbiasedness over all degree- $β$ rollout mean curves is equivalent to exactness on the monomial basis.

Definition 3 [def:unbiased-weight-set] (Unbiased weight set

W_{β} (p)

For a schedule $p = (p_{0}, \dots, p_{k})$ , the set of unbiased weights of order $β$ is $W_{β} (p) = {w \in R^{k + 1} : j = 0 \sum k w_{j} p_{j}^{0} = 0 and j = 0 \sum k w_{j} p_{j}^{ℓ} = 1 for every ℓ = 1, \dots, β} .$

⊢ Lean

Here $p_{j}^{0}$ denotes the constant monomial $1$ for every $j$ , including $p_{0} = 0$ . The first equation in Definition 3 removes the intercept $m_{P} (0)$ . The remaining equations reproduce the contribution of each nonconstant monomial to $m_{P} (1) - m_{P} (0)$ , so any $w \in W_{β} (p)$ gives a design-unbiased linear estimator for every law in Definition 2, whenever the set is nonempty.

The schedules compared in the main theorem are shifted Chebyshev-Lobatto schedules. They place more measurements near the endpoints of the observed interval, the usual geometry for controlling polynomial extrapolation.

Definition 4 [def:chebyshev-schedule] (Chebyshev schedule

p^{Ch} (k, q)

For $j = 0, \dots, k$ , the shifted Chebyshev-Lobatto node on $[0, q]$ is $p_{j}^{Ch} (k, q) = \frac{q}{2} {1 - cos (\frac{π j}{k})} .$ The shifted Chebyshev-Lobatto schedule is $p^{Ch} (k, q) = (p_{0}^{Ch} (k, q), \dots, p_{k}^{Ch} (k, q)) .$

⊢ Lean

We write $p^{Ch}$ for this schedule when $k$ and $q$ are clear. For comparison with a more elementary design, the equally spaced $β + 1$ -node schedule is $p^{eq} (β, q)$ , with entries $p_{j}^{eq} (β, q) = q j / β$ for $j = 0, \dots, β$ .

The variance envelope makes the relevant design criterion the smallest possible $ℓ^{1}$ amplification among unbiased weights.

Definition 5 [def:amplification-criterion] (Amplification criterion

A_{β} (p)

For a schedule $p$ , the amplification criterion is $A_{β} (p) = w \in W_{β} (p) in f (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ The minimax amplification over budgeted schedules is $M_{β, k, q} = p \in S_{k, q} in f A_{β} (p) .$

⊢ Lean

The quantity $A_{β} (p)$ records the best worst-case variance multiplier available at a fixed schedule under the total-variation variance envelope. The minimax quantity $M_{β, k, q}$ then optimizes that multiplier over the admissible treated-fraction placements in Definition 1.

Finally, it is useful to distinguish the envelope criterion from the exact finite-population covariance problem. For a law $P$ and schedule $p$ , let $Γ_{P} (p)$ be the design covariance matrix of the vector $(\overset{ˉ}{Y}_{0}, \dots, \overset{ˉ}{Y}_{k})$ .

Definition 6 [def:exact-nested-risk] (Exact nested risk

R_{exact} (β, k, q)

The exact nested risk is $R_{exact} (β, k, q) = p \in S_{k, q} in f w \in W_{β} (p) in f P \in P_{β} sup w^{'} Γ_{P} (p) w,$ where $Γ_{P} (p)$ is the design covariance matrix of the rollout round means under law $P$ and schedule $p$ .

⊢ Lean

Definition 6 leaves the true nested-rollout covariance matrix inside the minimax problem. The exact risk $R_{exact}$ is therefore the finite-population benchmark, while Definition 5 is the sharp envelope problem solved in the main results.

Main Results

The setup in Definition 2 reduces the identification problem to a polynomial endpoint problem. The first result records the corresponding identity for the target contrast: under the static rollout interpretation and the degree- $β$ rollout mean restriction, the estimand is the sum of the nonconstant coefficients of the rollout mean curve.

Lemma 1 [prop:rollout-polynomial-identity] (Rollout Polynomial Identity).

For any finite assignment space $Ω$ , population size $n$ , number of rollout intervals $k$ , polynomial order $β$ , contemporaneous assignment vectors $Z_{j}$ , potential outcomes $Y_{i} (Z_{j})$ , round means $\overset{ˉ}{Y}_{j}$ , rollout mean curve $m_{P}$ , and polynomial coefficients $(a_{P, ℓ})_{ℓ \geq 0}$ , suppose Assumption 1 and Assumption 2 hold. Then $m_{P} (1) - m_{P} (0) = ℓ = 1 \sum β a_{P, ℓ} .$ Thus the endpoint treatment contrast satisfies $τ_{P} = m_{P} (1) - m_{P} (0) = ℓ = 1 \sum β a_{P, ℓ} .$

⊢ Lean

The proof is deferred to Section B.

Lemma 1 identifies the polynomial target: any design-unbiased estimator of the nonconstant polynomial coefficients is also unbiased for the endpoint contrast. The subsequent results add sampling variability and optimize the placement of rollout measurements.

The next theorem turns this identity into a design criterion under the variance envelope in Assumption 3. The point is that, once cross-round covariances are left unrestricted except for positive semidefiniteness and the diagonal envelope, the worst-case variance of a linear unbiased estimator is governed by the squared $ℓ^{1}$ norm of its weights.

Theorem 1 [thm:tv-envelope-design] (TV Envelope Design Bound).

Let $n, k, β$ be integers, let $q \in R$ , and let $σ_{0}^{2} \in R$ . Fix a finite assignment space $Ω$ , a finite design $π$ on $Ω$ , rollout assignment vectors $Z_{0}, \dots, Z_{k}$ , round means $\overset{ˉ}{Y}_{0}, \dots, \overset{ˉ}{Y}_{k}$ , a rollout mean curve $m_{P}$ , polynomial coefficients $a_{P, ℓ}$ , and a schedule $p = (p_{0}, \dots, p_{k})$ . Suppose that

(Order.) $1 \leq β \leq k$ .
(Envelope scale.) $σ_{0}^{2} \geq 0$ .
(Schedule.) $p \in S_{k, q}$ , in the sense of Definition 1.
(Law class.) The design, rollout variables, round means, mean curve, coefficients, envelope scale, and schedule satisfy the rollout law-class restrictions $P_{β}$ in Definition 2.

Then $W_{β} (p)$ , as defined in Definition 3, is nonempty. Moreover, for every $w \in W_{β} (p)$ , $E_{π} [j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}] = m_{P} (1) - m_{P} (0)$ and $Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ For every such $w$ , there also exists a positive semidefinite $(k + 1) \times (k + 1)$ matrix $Γ$ such that $Γ_{j j} \leq \frac{σ _{0}^{2}}{n} for every j = 0, \dots, k,$ and $i = 0 \sum k j = 0 \sum k w_{i} Γ_{ij} w_{j} = \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ Consequently, with $A_{β} (\cdot)$ and $M_{β, k, q}$ as in Definition 5, $in f ⎩ ⎨ ⎧ v : \exists w \in W_{β} (p) with v = \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} ⎭ ⎬ ⎫ = \frac{σ _{0}^{2}}{n} A_{β} (p),$ and $in f {v : \exists p^{'} \in S_{k, q} with v = \frac{σ _{0}^{2}}{n} A_{β} (p^{'})} = \frac{σ _{0}^{2}}{n} M_{β, k, q} .$ Finally, if $p^{⋆} \in S_{k, q}$ satisfies $A_{β} (p^{⋆}) = M_{β, k, q},$ then for every $p^{'} \in S_{k, q}$ , $\frac{σ _{0}^{2}}{n} A_{β} (p^{⋆}) \leq \frac{σ _{0}^{2}}{n} A_{β} (p^{'}) .$

⊢ Lean

Theorem 1 separates three roles that are otherwise easy to conflate. The law class determines which linear combinations are unbiased; the envelope scale contributes the common factor $σ_{0}^{2} / n$ ; and the schedule affects risk only through the feasible set of polynomial-exact weights. Thus the schedule problem is the minimization of $A_{β} (p)$ over $S_{k, q}$ , a finite-dimensional optimal-design problem in the tradition of polynomial extrapolation and minimax design (Smith, 1918; Kiefer et al., 1959; Kiefer, 1974; Pukelsheim, 1993; Karlin et al., 1966).

A simple benchmark is obtained by using exactly $β + 1$ equally spaced measurements on $[0, q]$ . This benchmark is useful because it shows that unbiased extrapolation is feasible without oversampling. It also gives a (possibly large) universal upper bound on the amplification of naive spacing when $q$ is small; because Proposition 1 is only an upper bound, it does not by itself certify that equal spacing is unstable or suboptimal in a matching lower-bound sense.

Proposition 1 [prop:equal-spacing-benchmark] (Equal-Spacing Amplification Bound).

For every integer $β \geq 1$ and every $q \in (0, 1]$ , let $p^{eq} (β, q)_{j} = \frac{q j}{β}, j = 0, \dots, β .$ Then $p^{eq} (β, q)_{j} \in [0, 1]$ for every $j = 0, \dots, β$ , and, with $A_{β}$ as in Definition 5, $A_{β} (p^{eq} (β, q)) \leq 9 (\frac{β}{q})^{2 β} .$

⊢ Lean

Proposition 1 is not a minimax statement. It provides a scale against which the Chebyshev result below should be read: equal spacing gives a universal upper bound, but the base of this upper bound grows with $β / q$ , consistent with the difficulty of extrapolating from $[0, q]$ to $1$ using evenly spaced nodes (the bound is one-sided and does not by itself establish a matching instability).

The full-budget boundary is qualitatively different. When $q = 1$ , the target endpoint is observed, so no extrapolation is needed.

Proposition 2 [prop:no-extrapolation-boundary] (Full-Budget Endpoint Rule).

For every polynomial order $β \geq 1$ , take $k = β$ and use the equal-spacing schedule $p^{eq} (β, 1)$ . Define the weight vector $w = (w_{0}, \dots, w_{β})$ by $w_{0} = - 1, w_{β} = 1, w_{j} = 0 for 1 \leq j \leq β - 1.$ Then $w \in W_{β} (p^{eq} (β, 1))$ , where $W_{β} (\cdot)$ is the unbiased weight set in Definition 3. Consequently, for the amplification criterion in Definition 5, $A_{β} (p^{eq} (β, 1)) \leq 4.$

⊢ Lean

Proposition 2 explains why the low-budget assumption is imposed separately in Assumption 4. At full rollout, the endpoint contrast can be estimated by the difference between the final and baseline round means, with amplification bounded independently of $β$ . The exponential behavior in the next theorem is therefore specific to endpoint extrapolation.

Chebyshev-Lobatto placement is the schedule that controls this extrapolation cost. The theorem below compares every admissible schedule to the shifted Chebyshev-Lobatto schedule from Definition 4, uniformly over budgets bounded away from one. The oversampling ratio $c$ permits more than the minimum $β + 1$ measurements, which is the regime in which the discrete Lobatto grid norms the relevant continuous polynomial problem.

Theorem 2 [thm:chebyshev-minimax] (Chebyshev Minimax Amplification).

Fix a budget cap $q_{m a x} \in (0, 1)$ . There exists a constant $C_{-} (q_{m a x}) > 0$ such that, for every oversampling ratio $c > 1$ , there exists a constant $C_{+} (c, q_{m a x}) > 0$ with the following property.

For every pair of integers $β, k$ , every rollout budget $q$ , and every schedule $p$ , suppose that

(Order and oversampling.) $β \geq 1$ and $k \geq c β$ .
(Low-budget regime.) $q > 0$ and the low-budget cap condition of Assumption 4 holds for $(q, q_{m a x})$ .
(Admissible schedule.) When $p$ is used below, $p \in S_{k, q}$ as in Definition 1.

Then, with $A_{β} (\cdot)$ and $M_{β, k, q}$ as in Definition 5 and $p^{Ch} (k, q)$ as in Definition 4, $A_{β} (p) \geq C_{-} (q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β},$ and $A_{β} (p^{Ch} (k, q)) \leq C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$ Moreover, the minimax amplification satisfies the matching two-sided bound $C_{-} (q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} \leq M_{β, k, q} \leq C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$

⊢ Lean

Theorem 2 gives the main schedule result. For fixed $q \leq q_{m a x} < 1$ and $k \geq c β$ , no admissible schedule can improve the amplification exponent beyond the displayed Chebyshev base, while the shifted Chebyshev-Lobatto schedule attains the same rate up to constants depending only on $q_{m a x}$ and $c$ . Under the envelope criterion, the rate-optimal schedule clusters measurements near $0$ and $q$ , as in Chebyshev-Lobatto extrapolation; heuristically the experimenter concentrates measurements near the interval endpoints, where controlling the polynomial extrapolation to $u = 1$ is most demanding. The low-budget cost remains exponential in the polynomial order, but Chebyshev-Lobatto placement controls the exponent that the total-variation variance envelope makes unavoidable.

To make the exponential base concrete, Table 1 reports the low-budget Chebyshev base $(1 + 1 - q)^{2} / q$ alongside the equal-spacing upper-bound base $β / q$ implied by Proposition 1, for several budgets $q$ . The Chebyshev base is at most $4/ q$ and is independent of $β$ , whereas the equal-spacing upper-bound base grows linearly in $β$ (Proposition 1 bounds equal-spacing amplification from above only, so this column is an upper-bound base, not a certified rate); the amplification is the corresponding base raised to the power $2 β$ , and the constants $C_{-} (q_{m a x}), C_{+} (c, q_{m a x})$ of Theorem 2 depend only on $q_{m a x}$ and $c$ .

Low-budget amplification bases (the amplification is the base raised to the power $2 β$ ). The Chebyshev base is $β$ -independent and at most $4/ q$ ; the equal-spacing base scales with $β / q$ .
$q$	Chebyshev base $(1 + 1 - q)^{2} / q$	bound $4/ q$	equal-spacing upper-bound base $β / q$
$0.05$	$78.0$	$80.0$	$20 β$
$0.1$	$38.0$	$40.0$	$10 β$
$0.2$	$17.9$	$20.0$	$5 β$
$0.5$	$5.83$	$8.0$	$2 β$

Discussion and Extensions

The envelope result in Theorem 1 is deliberately conservative about the covariance structure of a nested rollout. It permits any positive semidefinite covariance matrix whose diagonal entries satisfy the round-mean variance envelope, and it therefore turns the schedule problem into a polynomial amplification problem. The exact finite-population problem in Definition 6 is narrower: the covariance matrix is the true design covariance matrix $Γ_{P} (p)$ induced by the rollout law that generates the observed round means. The specific covariance restrictions this law imposes beyond the diagonal variance envelope are not encoded in the verified formal layer; accordingly $R_{exact}$ is treated here as a symbolic benchmark, and the only verified comparison between the exact and envelope problems is the one-sided variance-envelope inequality of Lemma 2. That extra structure may matter for finite-sample optimality, even though the envelope criterion already gives an interpretable design rule that is sharp over the positive-semidefinite diagonal-envelope covariance class.

Exact-covariance scope and limitations

The distinction is important for the status of Chebyshev-Lobatto placement. Theorem 2 proves rate-minimax optimality up to constants for the total-variation envelope criterion $A_{β} (p)$ and $M_{β, k, q}$ . Exact optimality with $Γ_{P} (p)$ left inside the minimax risk is the stronger covariance-specific question recorded separately below.

Remark 1 [oeq:exact-nested-minimax] (Exact nested optimality).

Fix a finite assignment space $Ω$ with rollout randomization $π$ , population size $n$ , and variance-envelope scale $σ_{0}^{2}$ . Fix a budget cap $q_{m a x}$ with $0 < q_{m a x} < 1$ , let $c > 1$ , let $β \geq 1$ , set $k = ⌈ c β ⌉$ , and take $q$ with $0 < q \leq q_{m a x}$ . Under these hypotheses the shifted Chebyshev-Lobatto schedule $p^{Ch} (k, q)$ is admissible, so that $p^{Ch} (k, q) \in S_{k, q} .$ For the exact finite-population nested-rollout minimax problem $R_{exact} (β, k, q) = p \in S_{k, q} in f w \in W_{β} (p) in f P \in P_{β} sup w^{'} Γ_{P} (p) w,$ where $Γ_{P} (p)$ is the true design covariance matrix of the monotone Bernoulli rollout and $P_{β}$ includes the static-rollout, $β$ -polynomial, variance-envelope, and mean-curve-pinning restrictions, the open question is whether the fixed Chebyshev-Lobatto exact risk attains the nested infimum: $w \in W_{β} (p^{Ch} (k, q)) in f P \in P_{β} sup w^{'} Γ_{P} (p^{Ch} (k, q)) w = R_{exact} (β, k, q) .$ This statement is only the exact-optimality question for $p^{Ch} (k, q)$ ; it does not assert the separate rate-feasibility bound.

⊢ Lean

Remark 1 keeps exact optimality separate from rate feasibility. The equality displayed there characterizes the optimizer of the true nested covariance problem and is stronger than achieving the same exponential order as the envelope benchmark. Establishing such an equality calls for the covariance restrictions implied by monotone Bernoulli rollout designs in addition to the diagonal variance envelope. Related finite-population interference designs suggest that these restrictions can be substantive, especially when exposure mappings, clustered assignments, or dependency neighborhoods impose additional structure on covariances (Cortez-Rodriguez et al., 2024; Eichhorn et al., 2024; Jiang et al., 2023; Cai et al., 2023).

The results below state the rate implication delivered by the one-sided envelope comparison. The exact nested risk is bounded above by the envelope amplification criterion at every admissible schedule. Therefore any schedule that is good for the envelope problem is automatically feasible for the exact finite-population risk.

Lemma 2 [lem:exact-risk-envelope-upper] (Exact Risk Envelope Bound).

Let $Ω$ be a finite assignment space equipped with rollout randomization $π$ . For any population size $n$ , any integers $k$ and $β$ , any real numbers $q$ and $σ_{0}^{2}$ , and any schedule $p = (p_{0}, \dots, p_{k})$ , suppose that

(Order.) $β \geq 1$ .
(Number of rollout intervals.) $k \geq β$ .
(Budget.) $0 < q \leq 1$ .
(Variance scale.) $σ_{0}^{2} \geq 0$ .
(Budgeted schedule.) $p \in S_{k, q}$ , as in Definition 1.

Then $w \in W_{β} (p) in f P \in P_{β} sup w^{'} Γ_{P} (p) w \leq \frac{σ _{0}^{2}}{n} A_{β} (p),$ with $W_{β} (p)$ as in Definition 3, $P_{β}$ as in Definition 2, and $A_{β} (p)$ as in Definition 5. Consequently, $R_{exact} (β, k, q) \leq \frac{σ _{0}^{2}}{n} M_{β, k, q},$ where $R_{exact} (β, k, q)$ is as in Definition 6 and $M_{β, k, q}$ is as in Definition 5.

⊢ Lean

The proof is deferred to Section B.

Lemma 2 is a one-sided comparison. It places the exact covariance minimax risk below the envelope risk because the envelope allows a larger class of covariance matrices than those generated by the rollout law. A matching lower bound and characterization of the exact-risk minimizing schedule constitute the remaining exact-covariance problem.

Combining this comparison with the Chebyshev upper bound gives the finite-population feasibility statement relevant for low-budget rollout design. With $k = ⌈ c β ⌉$ , the shifted Chebyshev-Lobatto schedule attains the same exponential rate for the exact risk upper bound as it does for the envelope criterion.

Proposition 3 [lem:exact-chebyshev-rate-feasible] (Feasible Chebyshev Rate).

Fix an oversampling constant $c$ and a budget cap $q_{m a x}$ such that $c > 1$ and $0 < q_{m a x} < 1$ . Then there exists a constant $C_{+} (c, q_{m a x}) > 0$ such that, for every population size $n$ , polynomial order $β$ , number of rollout intervals $k$ , finite assignment space $Ω$ , finite design $π$ on $Ω$ , rollout budget $q$ , and variance-envelope scale $σ_{0}^{2}$ , the following conditions imply the stated bound:

(Order.) $β \geq 1$ .
(Budget.) $q > 0$ and $q$ satisfies the low-budget cap with $q_{m a x}$ in Assumption 4.
(Variance scale.) $σ_{0}^{2} \geq 0$ .
(Chebyshev size.) $k = ⌈ c β ⌉$ .
(Schedule.) $p = p^{Ch} (k, q)$ is the shifted Chebyshev-Lobatto schedule of Definition 4.

Under these conditions, $w \in W_{β} (p^{Ch} (k, q)) in f P \in P_{β} sup Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β},$ where $W_{β} (p^{Ch} (k, q))$ is the unbiased weight set of Definition 3, and the supremum ranges over rollout laws $P \in P_{β}$ satisfying Definition 2 at the schedule $p^{Ch} (k, q)$ with variance-envelope scale $σ_{0}^{2}$ .

⊢ Lean

Proposition 3 gives a practical interpretation of the main theorem for the original rollout experiment. Independently of exact nested optimality, the Chebyshev-Lobatto schedule has infimum worst-case exact variance over unbiased linear estimators bounded by the displayed low-budget exponential rate. Thus the envelope solution supplies a feasible exact-risk design with controlled finite-population risk.

Future work

Several extensions are natural. Clustered rollouts would replace unit-level monotone Bernoulli assignment with group-level assignment and would require tracking how cluster size and within-cluster exposure affect the round-mean covariance matrix. Mixed designs that combine rollout fractions with saturation, encouragement, or exposure-based randomization would add further design variables beyond the treated-fraction schedule, connecting the present extrapolation problem to recent work on clustered and network experiments (Chen et al., 2025; Fan et al., 2025; Bhadra et al., 2025; Schröder et al., 2026). Adjacent staggered-rollout efficiency work outside network interference is also relevant for positioning the rollout-design question (Roth et al., 2021). The Chebyshev argument suggests that endpoint placement should remain central whenever the estimand extrapolates beyond the observed rollout range, with a design-specific minimax object for each extension.

Appendices

Proofs and Verification

This appendix collects the auxiliary statements that support the envelope design result and the low-budget Chebyshev rate. The first part translates the rollout-weight problem into a real-polynomial optimal-recovery problem; the second part records the Chebyshev approximation inequalities; the final part returns these inequalities to the admissible rollout schedules and to the variance envelope. The appendix states the mathematical ingredients under the modeling assumptions introduced in the main text.

The bridge from rollout weights to approximation is the duality between minimum $ℓ^{1}$ norm weights and bounded polynomial extrapolation. In the notation of Definition 3, the moment equations make each admissible weight vector a linear functional on degree- $β$ polynomials. The dual norm of this functional is exactly the largest endpoint contrast among polynomials bounded at the chosen schedule nodes.

Lemma 3 [lem:amplification-dual-norm] (Dual Norm Amplification).

Let $β, k \in N$ and let $p = (p_{0}, \dots, p_{k})$ be a real-valued schedule whose nodes are distinct. Suppose that the unbiased weight set $W_{β} (p)$ in Definition 3 is nonempty. Then $w \in W_{β} (p) in f j = 0 \sum k ∣ w_{j} ∣ = sup {∣ r (1) - r (0) ∣ : r \in R [x], de g (r) \leq β, 0 \leq j \leq k max ∣ r (p_{j}) ∣ \leq 1} .$ Consequently, for the amplification criterion $A_{β} (p)$ in Definition 5, $A_{β} (p) = (sup {∣ r (1) - r (0) ∣ : r \in R [x], de g (r) \leq β, 0 \leq j \leq k max ∣ r (p_{j}) ∣ \leq 1})^{2} .$

⊢ Lean

Proof of Lemma 3.

Throughout write $N = {j = 0 \sum k ∣ w_{j} ∣ : w \in W_{β} (p)}, A = ⎩ ⎨ ⎧ (j = 0 \sum k ∣ w_{j} ∣)^{2} : w \in W_{β} (p) ⎭ ⎬ ⎫,$ and $D = sup {∣ r (1) - r (0) ∣ : r \in R [x], de g (r) \leq β, 0 \leq j \leq k max ∣ r (p_{j}) ∣ \leq 1} .$ Call a polynomial $r$ admissible if $de g (r) \leq β$ and $max_{0 \leq j \leq k} ∣ r (p_{j}) ∣ \leq 1$ , so that $D$ is the supremum of $∣ r (1) - r (0) ∣$ over admissible $r$ .

Step 1: the moment form of unbiasedness. Rewrite the unbiasedness equations in the single moment form $j = 0 \sum k w_{j} p_{j}^{ℓ} = {0, 1, ℓ = 0, 1 \leq ℓ \leq β, 0 \leq ℓ \leq β .$ This is equivalent to $w \in W_{β} (p)$ : the case $ℓ = 0$ is the zeroth-moment equation in Definition 3, while each positive $ℓ \leq β$ is one of its remaining moment equations. Consequently $N$ is exactly the set of attainable $ℓ^{1}$ norms for this moment system, and the assumed nonemptiness of $W_{β} (p)$ gives primal feasibility: $N \neq = \emptyset$ and $A \neq = \emptyset$ .

Step 2: representation identity. For every $w \in W_{β} (p)$ and every real polynomial $r$ with $de g (r) \leq β$ , $r (1) - r (0) = j = 0 \sum k w_{j} r (p_{j}) .$ Indeed, writing $r (x) = \sum_{ℓ = 0}^{β} c_{ℓ} x^{ℓ}$ and exchanging the two finite sums, $j = 0 \sum k w_{j} r (p_{j}) = ℓ = 0 \sum β c_{ℓ} j = 0 \sum k w_{j} p_{j}^{ℓ} = ℓ = 1 \sum β c_{ℓ} = r (1) - r (0),$ where the middle equality is the moment form of Step 1 and the last uses $r (1) = \sum_{ℓ = 0}^{β} c_{ℓ}$ and $r (0) = c_{0}$ .

Step 3: weak duality. Let $w \in W_{β} (p)$ and let $r$ be admissible. By Step 2 and the triangle inequality, $∣ r (1) - r (0) ∣ = j = 0 \sum k w_{j} r (p_{j}) \leq j = 0 \sum k ∣ w_{j} ∣ ∣ r (p_{j}) ∣ \leq j = 0 \sum k ∣ w_{j} ∣,$ the last step because $∣ r (p_{j}) ∣ \leq 1$ for every node. Thus every value $∣ r (1) - r (0) ∣$ is bounded above by every element of $N$ . Since $N \neq = \emptyset$ , the set of dual values is bounded above, so $D$ is a finite real number, and $D \leq in f N .$ Moreover the zero polynomial is admissible with $∣ r (1) - r (0) ∣ = 0$ , so $0$ belongs to the dual value set and $D \geq 0.$

Step 4: strong duality. There exists $w^{⋆} \in W_{β} (p)$ with $j = 0 \sum k ∣ w_{j}^{⋆} ∣ \leq D .$ Indeed, by Step 2 the endpoint value $r (1) - r (0)$ depends on $r$ only through the node-value vector $(r (p_{j}))_{j = 0}^{k}$ , so it defines a linear functional on the subspace of $R^{k + 1}$ spanned by such vectors; by the definition of $D$ that functional is dominated there by the sublinear majorant $x \mapsto D max_{0 \leq j \leq k} ∣ x_{j} ∣$ . Extending it to all of $R^{k + 1}$ under the same majorant, its coordinate values $w_{j}^{⋆}$ again satisfy the moment equations of Step 1, hence $w^{⋆} \in W_{β} (p)$ ; and evaluating the extension at the sign vector $ε_{j} = sign (w_{j}^{⋆})$ gives $\sum_{j} ∣ w_{j}^{⋆} ∣ \leq D max_{j} ∣ ε_{j} ∣ = D$ . In particular $in f N \leq D$ , which combined with Step 3 gives the first assertion, $w \in W_{β} (p) in f j = 0 \sum k ∣ w_{j} ∣ = sup {∣ r (1) - r (0) ∣ : de g (r) \leq β, 0 \leq j \leq k max ∣ r (p_{j}) ∣ \leq 1} .$

Step 5: the squared identity. The set $A$ is nonempty by Step 1 and bounded below by $0$ , so $in f A$ is a well-defined real number. For every $w \in W_{β} (p)$ we have $0 \leq D \leq \sum_{j} ∣ w_{j} ∣$ by Steps 3 and 4, hence $D^{2} \leq (\sum_{j} ∣ w_{j} ∣)^{2}$ ; taking the infimum over $A$ gives $D^{2} \leq in f A .$ Conversely, the weight $w^{⋆}$ of Step 4 satisfies $0 \leq \sum_{j} ∣ w_{j}^{⋆} ∣ \leq D$ , and therefore $in f A \leq (j = 0 \sum k ∣ w_{j}^{⋆} ∣)^{2} \leq D^{2} .$ Thus $in f A = D^{2}$ . Since Definition 5 defines $A_{β} (p)$ as precisely this infimum, the claimed squared formula follows.

∎

Lemma 3 is the point at which the econometric design problem becomes the real polynomial optimal-recovery problem. The schedule affects the right-hand side only through the locations at which the polynomial is constrained. Hence minimax placement of rollout fractions is equivalent, under the envelope criterion, to choosing nodes that make bounded interpolation on $[0, q]$ as stable as possible for the endpoint contrast $r (1) - r (0)$ .

The approximation bounds used for that comparison are standard Chebyshev facts adapted to the extrapolation geometry. The first is the exterior extremal property: among degree- $β$ polynomials bounded by one on $[- 1, 1]$ , the Chebyshev polynomial controls growth outside the interval (Karlin et al., 1966; Pukelsheim, 1993).

Lemma 4 [lem:chebyshev-exterior-extremal] (Exterior Chebyshev Extremal Bound).

Let $β$ be a positive integer. For every real polynomial $P$ and every exterior point $x_{0}$ , suppose that

(Degree bound.) $de g (P) \leq β$ .
(Unit interval bound.) For every $x \in [- 1, 1]$ , $∣ P (x) ∣ \leq 1$ .
(Exterior point.) $x_{0} > 1$ .

Then $∣ P (x_{0}) ∣ \leq T_{β} (x_{0}),$ where $T_{β}$ is the Chebyshev polynomial of the first kind of degree $β$ .

⊢ Lean

Proof of Lemma 4.

Let $s = {0, \dots, β}$ , and let $v_{i}$ , $i \in s$ , be the Chebyshev extremal nodes $v_{i} = cos \frac{π i}{β}, i = 0, \dots, β .$ The node map $i \mapsto v_{i}$ is injective on $s$ , so the interpolation nodes are distinct. For $i = 0, \dots, β$ , let $L_{i}$ be the Lagrange basis polynomial for these nodes, $L_{i} (x) = 0 \leq j \leq β j \neq = i \prod \frac{x - v _{j}}{v _{i} - v _{j}} .$ Since $∣ s ∣ = β + 1$ , any polynomial $Q$ with $de g (Q) \leq β$ has degree strictly less than the number of nodes, and the same is true for $T_{β}$ . Hence both polynomials are recovered from their node values by Lagrange interpolation.

First prove the one-sided claim: if $de g (Q) \leq β$ and $∣ Q (x) ∣ \leq 1$ for every $x \in [- 1, 1]$ , then $Q (x_{0}) \leq T_{β} (x_{0}) .$ Interpolating $Q$ at the nodes and evaluating at $x_{0}$ gives $Q (x_{0}) = i = 0 \sum β Q (v_{i}) L_{i} (x_{0}) .$ The same interpolation argument for $T_{β}$ gives $T_{β} (x_{0}) = i = 0 \sum β T_{β} (v_{i}) L_{i} (x_{0}) .$ For $x_{0} > 1$ , the signed exterior coefficients satisfy $(- 1)^{i} L_{i} (x_{0}) \geq 0, i = 0, \dots, β .$ Indeed, every numerator factor obeys $x_{0} - v_{j} > 0$ , because each Chebyshev node lies in $[- 1, 1]$ and $x_{0} > 1$ . For the denominator, the Chebyshev-node monotonicity used in this sign calculation gives $v_{i} < v_{j}$ when $j < i$ and $v_{j} < v_{i}$ when $i < j$ . Thus the denominator has exactly $i$ negative factors, and multiplying by $(- 1)^{i}$ makes the denominator sign positive. Combining these signs in the product formula for $L_{i}$ yields the displayed inequality.

Since $v_{i} \in [- 1, 1]$ , the interval bound on $Q$ gives $∣ Q (v_{i}) ∣ \leq 1$ , and multiplying by the sign $(- 1)^{i}$ preserves this absolute-value bound. Therefore $(- 1)^{i} Q (v_{i}) \leq 1.$ The Chebyshev extremal-node identity gives $T_{β} (v_{i}) = (- 1)^{i}, i = 0, \dots, β .$ Inserting the factor $(- 1)^{i} (- 1)^{i} = 1$ and multiplying the last inequality by the nonnegative coefficient $(- 1)^{i} L_{i} (x_{0})$ yields, for each $i$ , $Q (v_{i}) L_{i} (x_{0}) = ((- 1)^{i} Q (v_{i})) ((- 1)^{i} L_{i} (x_{0})) \leq (- 1)^{i} L_{i} (x_{0}) = T_{β} (v_{i}) L_{i} (x_{0}) .$ Summing over $i = 0, \dots, β$ and using the two interpolation displays proves the one-sided claim.

Apply this claim first to $Q = P$ , obtaining $P (x_{0}) \leq T_{β} (x_{0})$ . Apply it again to $Q = - P$ ; the degree bound and interval bound are unchanged, so $- P (x_{0}) \leq T_{β} (x_{0})$ . The two inequalities give $- T_{β} (x_{0}) \leq P (x_{0}) \leq T_{β} (x_{0}),$ and hence $∣ P (x_{0}) ∣ \leq T_{β} (x_{0}) .$

∎

For the rollout application, the polynomial is controlled at the finite set of measurement nodes. Oversampled Chebyshev-Lobatto grids pass from this nodewise control to uniform control on the interval. The next statement records the required discrete norming step, conditional on the Ehlich–Zeller mesh inequality.

Lemma 5 [lem:oversampled-chebyshev-lobatto-norming] (Oversampled Lobatto Norming).

Suppose the Ehlich–Zeller Chebyshev–Lobatto mesh inequality holds: for every pair of nonnegative integers $β, k$ and every real polynomial $R$ with $de g (R) \leq β$ and $β < k$ , $∣ R (x) ∣ \leq \frac{1}{cos ( π β / ( 2 k ))} 0 \leq j \leq k max R (- cos (\frac{π j}{k}))$ for every $x \in [- 1, 1]$ . Then, for every real oversampling ratio $c$ with $c > 1$ , there exists a real constant $K (c) > 0$ such that the following holds. For every pair of nonnegative integers $β, k$ and every real polynomial $R$ satisfying

(Positive order.) $β \geq 1$ ,
(Oversampling.) $k \geq c β$ ,
(Degree bound.) $de g (R) \leq β$ ,

one has, for every $x \in [- 1, 1]$ , $∣ R (x) ∣ \leq K (c) 0 \leq j \leq k max R (- cos (\frac{π j}{k})) .$

⊢ Lean

Proof of Lemma 5.

Fix $c > 1$ , and set $K (c) = \frac{1}{cos ( π / ( 2 c ))} .$ Since $c > 1$ , the angle $π / (2 c)$ lies strictly between $0$ and $π /2$ , so $cos (π / (2 c)) > 0$ and $K (c) > 0$ . Now let $β \geq 1$ , $k \geq c β$ , and $de g (R) \leq β$ , and abbreviate $N = 0 \leq j \leq k max R (- cos (\frac{π j}{k})) .$ Since $c > 1$ and $β \geq 1 > 0$ , we have $0 < β < c β \leq k,$ so in particular $β < k$ and $k > 0$ . The assumed Ehlich–Zeller mesh inequality therefore applies and gives, for every $x \in [- 1, 1]$ , $∣ R (x) ∣ \leq \frac{1}{cos ( π β / ( 2 k ))} N .$ It remains only to bound the secant factor uniformly. From $k \geq c β$ , $k > 0$ and $c > 0$ , $\frac{β}{k} \leq \frac{1}{c}, hence 0 \leq \frac{π β}{2 k} = \frac{π}{2} \cdot \frac{β}{k} \leq \frac{π}{2 c} .$ Also $π / (2 c) < π /2 \leq π$ , so both angles lie in $[0, π]$ . Since cosine is decreasing on $[0, π]$ , this implies $cos (π / (2 c)) \leq cos (π β / (2 k)),$ and positivity of $cos (π / (2 c))$ gives $\frac{1}{cos ( π β / ( 2 k ))} \leq \frac{1}{cos ( π / ( 2 c ))} = K (c) .$ The quantity $N$ is nonnegative, being a maximum of absolute values, so multiplying the last inequality by $N$ and chaining with the Ehlich–Zeller bound gives, for every $x \in [- 1, 1]$ , $∣ R (x) ∣ \leq \frac{1}{cos ( π β / ( 2 k ))} N \leq K (c) N = K (c) 0 \leq j \leq k max R (- cos (\frac{π j}{k})),$ which is the claim.

∎

Lemma 5 explains why the main theorem imposes $k \geq c β$ with $c > 1$ . Oversampling prevents a degree- $β$ polynomial from taking large values between adjacent Lobatto nodes while remaining small at the nodes. The constant $K (c)$ is allowed to depend on the oversampling ratio, but not on $β$ , $k$ , or the rollout budget.

The affine map from $[0, q]$ to $[- 1, 1]$ sends the target endpoint $u = 1$ to the exterior point $x_{q} = 2/ q - 1$ . The corresponding Chebyshev multiplier $λ (q) = x_{q} + x_{q}^{2} - 1$ gives the low-budget exponential base. Uniformity over $q \leq q_{m a x} < 1$ is recorded next.

Lemma 6 [lem:continuous-chebyshev-endpoint-bound] (Continuous Chebyshev Endpoint Bound).

Fix $q_{m a x}$ with $0 < q_{m a x} < 1$ . Then there exist constants $C (q_{m a x}) > 0$ and $c (q_{m a x}) > 0$ such that, for every $β \in N$ and every $q \in R$ , if

(Degree.) $1 \leq β$ ,
(Budget.) $0 < q \leq q_{m a x}$ ,
(Exterior notation.) $x_{q} = 2/ q - 1$ and $λ (q) = x_{q} + x_{q}^{2} - 1$ ,

then both of the following hold: $for every real polynomial R with de g (R) \leq β and x \in [- 1, 1] sup ∣ R (x) ∣ \leq 1, ∣ R (x_{q}) - R (- 1) ∣ \leq C (q_{m a x}) λ (q)^{β},$ and $T_{β} (x_{q}) - 1 \geq c (q_{m a x}) λ (q)^{β} .$

⊢ Lean

Proof of Lemma 6.

Put $\overset{x}{ˉ} = \frac{2}{q _{m a x}} - 1, \overset{ˉ}{λ} = \overset{x}{ˉ} + \overset{x}{ˉ}^{2} - 1 .$ Since $0 < q_{m a x} < 1$ we have $2/ q_{m a x} > 2$ , hence $\overset{x}{ˉ} > 1$ ; and since $\overset{x}{ˉ}^{2} - 1 \geq 0$ this gives $\overset{ˉ}{λ} \geq \overset{x}{ˉ} > 1$ . Choose $C (q_{m a x}) = 2, c (q_{m a x}) = \frac{1}{2} (1 - \overset{ˉ}{λ}^{- 1})^{2} .$ Both are positive: $\overset{ˉ}{λ} > 1$ gives $0 < \overset{ˉ}{λ}^{- 1} < 1$ , so $1 - \overset{ˉ}{λ}^{- 1} > 0$ .

Now let $β \geq 1$ and $0 < q \leq q_{m a x}$ , and write $x_{q} = \frac{2}{q} - 1, λ (q) = x_{q} + x_{q}^{2} - 1 .$ Then $q \leq q_{m a x} < 1$ , so exactly as above $x_{q} > 1$ and $λ (q) > 1$ . Moreover $q \leq q_{m a x}$ gives $2/ q_{m a x} \leq 2/ q$ and therefore $1 \leq \overset{x}{ˉ} \leq x_{q},$ and on $[1, \infty)$ the map $t \mapsto t + t^{2} - 1$ is nondecreasing, since it equals $e^{arcosh t}$ and both $arcosh$ and the exponential are nondecreasing. Hence $\overset{ˉ}{λ} \leq λ (q) .$

Chebyshev evaluation at the exterior point. Write $x_{q} = cosh a$ with $a = arcosh (x_{q}) \geq 0$ , which is legitimate because $x_{q} \geq 1$ . Then $T_{β} (cosh a) = cosh (β a)$ , while $e^{a} = x_{q} + x_{q}^{2} - 1 = λ (q)$ , so $T_{β} (x_{q}) = cosh (β a) = \frac{e ^{β a} + e ^{- β a}}{2} = \frac{λ ( q ) ^{β} + λ ( q ) ^{- β}}{2} .$

Upper bound. Let $R$ be a real polynomial with $de g (R) \leq β$ and $∣ R (x) ∣ \leq 1$ for $x \in [- 1, 1]$ . By Lemma 4, applied at the exterior point $x_{q} > 1$ , $∣ R (x_{q}) ∣ \leq T_{β} (x_{q}) .$ Also $- 1 \in [- 1, 1]$ , so $∣ R (- 1) ∣ \leq 1$ , and therefore $∣ R (x_{q}) - R (- 1) ∣ \leq ∣ R (x_{q}) ∣ + ∣ R (- 1) ∣ \leq T_{β} (x_{q}) + 1.$ Since $λ (q) \geq 1$ and $β \geq 1$ we have $λ (q)^{- β} \leq 1 \leq λ (q)^{β}$ , whence $\frac{λ ( q ) ^{β} + λ ( q ) ^{- β}}{2} + 1 \leq \frac{λ ( q ) ^{β} + λ ( q ) ^{β}}{2} + λ (q)^{β} = 2 λ (q)^{β} .$ Combining the last three displays proves $∣ R (x_{q}) - R (- 1) ∣ \leq 2 λ (q)^{β} = C (q_{m a x}) λ (q)^{β} .$

Lower bound. The same evaluation formula and the algebraic identity $\frac{λ ( q ) ^{β} + λ ( q ) ^{- β}}{2} - 1 = \frac{1}{2} (1 - λ (q)^{- β})^{2} λ (q)^{β}$ (valid because $λ (q)^{β} > 0$ ; expand the right-hand side) reduce the claim to a monotonicity step. Since $1 < \overset{ˉ}{λ} \leq λ (q)$ and $β \geq 1$ , $\overset{ˉ}{λ} \leq λ (q) \leq λ (q)^{β}, hence λ (q)^{- β} \leq \overset{ˉ}{λ}^{- 1},$ so that $0 \leq 1 - \overset{ˉ}{λ}^{- 1} \leq 1 - λ (q)^{- β}$ and therefore $(1 - \overset{ˉ}{λ}^{- 1})^{2} \leq (1 - λ (q)^{- β})^{2}$ . Multiplying by $\frac{1}{2} λ (q)^{β} > 0$ gives $T_{β} (x_{q}) - 1 = \frac{λ ( q ) ^{β} + λ ( q ) ^{- β}}{2} - 1 \geq \frac{1}{2} (1 - \overset{ˉ}{λ}^{- 1})^{2} λ (q)^{β} = c (q_{m a x}) λ (q)^{β} .$ This proves both assertions.

∎

Lemma 6 supplies the continuous upper and lower endpoint calculations behind Theorem 2. The first inequality controls the extrapolation contrast for every bounded polynomial; the second shows that the Chebyshev polynomial itself has the corresponding order of growth. After rescaling from $[- 1, 1]$ back to $[0, q]$ , this is the source of the factor $((1 + 1 - q)^{2} / q)^{2 β}$ in the amplification criterion.

The remaining deterministic ingredients connect the approximation statements to the rollout schedule class. First, the shifted Chebyshev-Lobatto nodes used in Definition 4 are admissible budgeted schedules.

Lemma 7 [lem:chebyshev-schedule-admissible] (Chebyshev Schedule Admissibility).

For every integer $k \geq 1$ and every $q \in (0, 1]$ , the shifted Chebyshev–Lobatto schedule $p^{Ch} (k, q)$ of Definition 4 is an element of the budgeted schedule class $S_{k, q}$ of Definition 1. Equivalently, its coordinates all lie in $[0, 1]$ , it starts at $0$ , is strictly increasing across the rollout measurement indices, and ends at $q$ .

⊢ Lean

Proof of Lemma 7.

Let $k \geq 1$ and $0 < q \leq 1$ , so that $k > 0$ and the nodes $p_{j}^{Ch} (k, q) = \frac{q}{2} (1 - cos \frac{π j}{k}), j = 0, \dots, k,$ are well defined. By Definition 1 it suffices to check four things: that every coordinate lies in $[0, 1]$ , that the schedule starts at $0$ , that it is strictly increasing in $j$ , and that it ends at $q$ .

Range. The inequalities $- 1 \leq cos (π j / k) \leq 1$ give $0 \leq 1 - cos (π j / k) \leq 2$ , and multiplying by $q /2 > 0$ yields $0 \leq p_{j}^{Ch} (k, q) = \frac{q}{2} (1 - cos \frac{π j}{k}) \leq \frac{q}{2} \cdot 2 = q \leq 1.$ Hence $p_{j}^{Ch} (k, q) \in [0, 1]$ for every $j = 0, \dots, k$ .

Endpoints. At $j = 0$ , $cos 0 = 1$ , so $p_{0}^{Ch} (k, q) = \frac{q}{2} (1 - 1) = 0;$ at $j = k$ , $π k / k = π$ and $cos π = - 1$ , so $p_{k}^{Ch} (k, q) = \frac{q}{2} (1 - (- 1)) = q .$

Strict increase. If $0 \leq a < b \leq k$ , then, since $k > 0$ , $0 \leq \frac{π a}{k} < \frac{π b}{k} \leq π .$ Cosine is strictly decreasing on $[0, π]$ , hence $cos \frac{π b}{k} < cos \frac{π a}{k},$ so that $1 - cos \frac{π a}{k} < 1 - cos \frac{π b}{k},$ and multiplication by the positive number $q /2$ gives $p_{a}^{Ch} (k, q) < p_{b}^{Ch} (k, q) .$ The coordinates are therefore in $[0, 1]$ , start at $0$ , are strictly increasing, and end at $q$ , so $p^{Ch} (k, q) \in S_{k, q}$ .

∎

The admissibility statement matters because Theorem 2 compares the Chebyshev schedule to all elements of $S_{k, q}$ . It verifies that endpoint clustering at $0$ and $q$ is compatible with the strict monotonicity imposed by Definition 1.

A separate feasibility issue is the existence of polynomially unbiased weights. Distinct budgeted nodes provide enough interpolation information once the number of rollout intervals is at least the polynomial order.

Lemma 8 [lem:unbiased-weight-set-nonempty] (Nonempty Unbiased Weights).

Let $q \in R$ , let $β$ and $k$ be integers, and let $p = (p_{0}, \dots, p_{k})$ be a rollout schedule. Suppose that

(Order.) $β \geq 1$ .
(Enough nodes.) $k \geq β$ .
(Budgeted schedule.) $p \in S_{k, q}$ , with $S_{k, q}$ as in Definition 1.

Then the unbiased weight set $W_{β} (p)$ of Definition 3 is nonempty. Equivalently, there exists a weight vector $w = (w_{0}, \dots, w_{k})$ such that $w \in W_{β} (p)$ .

⊢ Lean

Proof of Lemma 8.

Because $p \in S_{k, q}$ , the entries $p_{0} < p_{1} < \dots < p_{k}$ are strictly increasing in Definition 1, hence the $k + 1$ nodes are pairwise distinct. Let $L_{j}$ be the Lagrange basis polynomial for the full collection of nodes, $L_{j} (t) = 0 \leq i \leq k i \neq = j \prod \frac{t - p _{i}}{p _{j} - p _{i}}, j = 0, \dots, k,$ and define the endpoint weights $w_{j} = L_{j} (1) - L_{j} (0), j = 0, \dots, k .$ Fix $0 \leq ℓ \leq β$ and let $e_{ℓ} (t) = t^{ℓ}$ , a polynomial of degree $ℓ \leq β \leq k$ , hence of degree strictly less than the number $k + 1$ of nodes. Lagrange interpolation on the $k + 1$ distinct nodes therefore reproduces it exactly, $e_{ℓ} (t) = j = 0 \sum k e_{ℓ} (p_{j}) L_{j} (t) = j = 0 \sum k p_{j}^{ℓ} L_{j} (t) .$ Evaluating at $t = 1$ and at $t = 0$ gives $1^{ℓ} = j = 0 \sum k p_{j}^{ℓ} L_{j} (1), 0^{ℓ} = j = 0 \sum k p_{j}^{ℓ} L_{j} (0),$ and subtracting the second from the first yields $j = 0 \sum k w_{j} p_{j}^{ℓ} = 1^{ℓ} - 0^{ℓ} .$ For $ℓ = 0$ this is $1 - 1 = 0$ , while for every $1 \leq ℓ \leq β$ it is $1 - 0 = 1$ . These are exactly the moment equations of Definition 3 defining $W_{β} (p)$ . Thus the vector $w = (w_{0}, \dots, w_{k})$ belongs to $W_{β} (p)$ , and the set is nonempty.

∎

Lemma 8 justifies the infima over $W_{β} (p)$ in Definition 5 for the schedules used in the main results. Econometrically, $k \geq β$ gives at least $β + 1$ distinct measurements, which is the finite-dimensional requirement for exactness on the monomial basis $1, u, \dots, u^{β}$ .

The last auxiliary statement is the variance-envelope calculation. It establishes the squared $ℓ^{1}$ norm as the sharp worst-case envelope over positive semidefinite covariance matrices with the stated diagonal bound.

Lemma 9 [lem:variance-envelope-sharpness] (Sharp Variance Envelope).

For any population size $n$ , final rollout index $k$ , finite assignment space $Ω$ with rollout randomization $π$ , rollout-round statistics $X_{0}, \dots, X_{k}$ , variance scale $σ_{0}^{2}$ , and weight vector $w = (w_{0}, \dots, w_{k})$ , suppose that

(Nonnegative scale.) $σ_{0}^{2} \geq 0$ .
(Round variance envelope.) Assumption 3 holds for $X_{0}, \dots, X_{k}$ with scale $σ_{0}^{2} / n$ .

Then $Var_{π} (j = 0 \sum k w_{j} X_{j}) \leq \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ Moreover, there exists a positive semidefinite matrix $Γ \in R^{(k + 1) \times (k + 1)}$ such that $Γ_{j j} \leq \frac{σ _{0}^{2}}{n} for every j = 0, \dots, k,$ and $i = 0 \sum k j = 0 \sum k w_{i} Γ_{ij} w_{j} = \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$

⊢ Lean

Proof of Lemma 9.

Write $s = \frac{σ _{0}^{2}}{( n : R )},$ interpreting the quotient as the total real division used in the statement; in particular the quotient is defined also when $n = 0$ . Since $σ_{0}^{2} \geq 0$ and the real cast of a natural number is nonnegative, this gives $s \geq 0$ .

Covariance bound. For real random variables $U, V$ on $Ω$ , the design covariance is the finite sum $Cov_{π} (U, V) = z \in Ω \sum π (z) (U (z) - E_{π} U) (V (z) - E_{π} V) .$ Applying Cauchy–Schwarz to the vectors with entries $π (z) (U (z) - E_{π} U)$ and $π (z) (V (z) - E_{π} V)$ gives $Cov_{π} (U, V) \leq Var_{π} (U) Var_{π} (V) .$ Applying the same bound to $- U$ and using $Var_{π} (- U) = Var_{π} (U)$ gives $∣ Cov_{π} (U, V) ∣ \leq Var_{π} (U) Var_{π} (V) .$ For each $i, j$ , Assumption 3 gives $Var_{π} (X_{i}) \leq s$ and $Var_{π} (X_{j}) \leq s$ . Hence $∣ Cov_{π} (X_{i}, X_{j}) ∣ \leq Var_{π} (X_{i}) Var_{π} (X_{j}) \leq s s = s,$ where the last equality uses $s \geq 0$ .

Variance bound. By bilinearity of the design covariance, the variance of the weighted sum expands as $Var_{π} (j = 0 \sum k w_{j} X_{j}) = i = 0 \sum k j = 0 \sum k w_{i} w_{j} Cov_{π} (X_{i}, X_{j}) .$ Termwise, $w_{i} w_{j} Cov_{π} (X_{i}, X_{j}) \leq ∣ w_{i} w_{j} Cov_{π} (X_{i}, X_{j}) ∣ = ∣ w_{i} ∣ ∣ w_{j} ∣ ∣ Cov_{π} (X_{i}, X_{j}) ∣ \leq ∣ w_{i} ∣ ∣ w_{j} ∣ s .$ Summing and factoring the double sum therefore gives $Var_{π} (j = 0 \sum k w_{j} X_{j}) \leq i = 0 \sum k j = 0 \sum k ∣ w_{i} ∣ ∣ w_{j} ∣ s = s (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ Substituting $s = σ_{0}^{2} / (n : R)$ gives the stated variance bound.

Sharpness. Define $ε_{j} = {1, - 1, w_{j} \geq 0, w_{j} < 0, j = 0, \dots, k,$ and set $Γ_{ij} = s ε_{i} ε_{j} .$ This matrix is positive semidefinite, since it is $s$ times the rank-one outer product $ε ε^{'}$ and $s \geq 0$ . Equivalently, for every $v \in R^{k + 1}$ , $i = 0 \sum k j = 0 \sum k v_{i} Γ_{ij} v_{j} = s (j = 0 \sum k v_{j} ε_{j})^{2} \geq 0.$ Since $ε_{j}^{2} = 1$ , each diagonal entry satisfies $Γ_{j j} = s ε_{j}^{2} = s = \frac{σ _{0}^{2}}{( n : R )},$ and hence obeys the required diagonal bound. Finally, the definition of $ε_{j}$ gives $w_{j} ε_{j} = ∣ w_{j} ∣$ for every $j$ , so $i = 0 \sum k j = 0 \sum k w_{i} Γ_{ij} w_{j} = s (j = 0 \sum k w_{j} ε_{j})^{2} = s (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ Substituting $s = σ_{0}^{2} / (n : R)$ gives the desired positive semidefinite matrix and equality.

∎

Lemma 9 completes the connection between approximation and variance. The upper bound follows from the diagonal variance envelope and positive semidefiniteness; the sharpness clause establishes $A_{β} (p)$ as the smallest uniform envelope criterion when cross-round covariances are otherwise unrestricted. Theorem 1 therefore optimizes this sharp criterion directly.

Verification note.

The theorem statements and proofs for the formal results displayed in this paper are machine-checked in Lean 4. The checked development covers the finite-design variance algebra over a finite assignment space, the $ℓ^{1} / ℓ^{\infty}$ dual amplification calculation, the positive-semidefinite variance-envelope sharpness argument, and the real-polynomial approximation objects used in the Chebyshev and Lobatto bounds. The potential-outcome consistency restriction in Assumption 1, the polynomial rollout restriction in Assumption 2, the law-class pinning in Definition 2, and the round-mean variance envelope in Assumption 3 enter as hypotheses. For modularity, Lemma 5 is displayed conditionally on the Ehlich–Zeller Chebyshev–Lobatto mesh inequality (Ehlich and Zeller, Schwankung von Polynomen zwischen Gitterpunkten, Math. Z. 86 (1964), 41–44), which appears as an explicit hypothesis of that lemma. The accompanying Lean development additionally proves the Ehlich–Zeller inequality through a Bernstein–Szegő differential-inequality argument, thereby discharging this classical approximation-theory input. A machine-readable crosswalk from each displayed statement to its checked Lean declaration accompanies the paper, together with the Lean and mathlib versions and the build instructions needed to reproduce the verification.

Proofs of the main results

Proof of Lemma 1.

The static consistency hypothesis of Assumption 1 is part of the rollout environment and fixes the interpretation of $\overset{ˉ}{Y}_{j}$ , but the endpoint calculation uses only the polynomial mean assumption of Assumption 2.

Both endpoints $u = 1$ and $u = 0$ belong to $[0, 1]$ , so the degree- $β$ expansion applies at each. Evaluating at $u = 1$ gives $m_{P} (1) = ℓ = 0 \sum β a_{P, ℓ} 1^{ℓ} = ℓ = 0 \sum β a_{P, ℓ},$ because $1^{ℓ} = 1$ for every $ℓ$ . Evaluating the same expansion at $u = 0$ gives $m_{P} (0) = ℓ = 0 \sum β a_{P, ℓ} 0^{ℓ} = a_{P, 0},$ since $0^{ℓ} = 0$ for every $ℓ \geq 1$ , while the $ℓ = 0$ term is $a_{P, 0} \cdot 0^{0} = a_{P, 0}$ . Finally, the finite sum over ${0, \dots, β}$ splits into its constant term and the positive-degree terms: $ℓ = 0 \sum β a_{P, ℓ} = a_{P, 0} + ℓ = 1 \sum β a_{P, ℓ} .$ This finite-sum identity is obtained by induction on $β$ , adjoining the top endpoint $ℓ = β + 1$ to both sides at each step. Substituting the two endpoint evaluations into this split and cancelling the constant term $a_{P, 0}$ yields $m_{P} (1) - m_{P} (0) = (a_{P, 0} + ℓ = 1 \sum β a_{P, ℓ}) - a_{P, 0} = ℓ = 1 \sum β a_{P, ℓ} .$

∎

Proof of Theorem 1.

Let $κ := \frac{σ _{0}^{2}}{n},$ with the convention that this real quotient is total, so the quotient is zero when the natural population size is zero. Since $σ_{0}^{2} \geq 0$ and $n \geq 0$ , this gives $κ \geq 0$ .

We use this nonnegativity through the following elementary scaling rule for infima, applied twice below. Let $S \subseteq R$ be nonempty and bounded below, and let $κ \geq 0$ . Then $κ S = {κ u : u \in S}$ is again nonempty and bounded below, and $in f {κ u : u \in S} = κ in f S .$ For $κ > 0$ this is the standard homogeneity of the infimum; for $κ = 0$ both sides equal $0$ . Each application below is preceded by a verification that the set being scaled is nonempty and bounded below.

First, $W_{β} (p)$ is nonempty. Indeed, the order hypothesis gives $β \geq 1$ , the theorem assumes $k \geq β$ , and $p \in S_{k, q}$ . Hence Lemma 8 applies and gives a weight vector $w \in W_{β} (p)$ .
Fix now any $w \in W_{β} (p)$ . By linearity of the design expectation and by the defining mean-curve restriction $E_{π} [\overset{ˉ}{Y}_{j}] = m_{P} (p_{j})$ in $P_{β}$ of Definition 2, $E_{π} [j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}] = j = 0 \sum k w_{j} E_{π} [\overset{ˉ}{Y}_{j}] = j = 0 \sum k w_{j} m_{P} (p_{j}) .$ Since $p \in S_{k, q}$ , every node $p_{j}$ lies in $[0, 1]$ , so the degree- $β$ polynomial condition in $P_{β}$ gives $m_{P} (p_{j}) = ℓ = 0 \sum β a_{P, ℓ} p_{j}^{ℓ} .$ Substituting and interchanging the two finite sums, $j = 0 \sum k w_{j} m_{P} (p_{j}) = ℓ = 0 \sum β a_{P, ℓ} j = 0 \sum k w_{j} p_{j}^{ℓ} .$ Splitting off the constant term and inserting the moment equations in Definition 3, $j = 0 \sum k w_{j} p_{j}^{0} = 0, j = 0 \sum k w_{j} p_{j}^{ℓ} = 1 (1 \leq ℓ \leq β),$ the last display equals $a_{P, 0} j = 0 \sum k w_{j} p_{j}^{0} + ℓ = 1 \sum β a_{P, ℓ} j = 0 \sum k w_{j} p_{j}^{ℓ} = a_{P, 0} \cdot 0 + ℓ = 1 \sum β a_{P, ℓ} \cdot 1 = ℓ = 1 \sum β a_{P, ℓ} .$ By Lemma 1, whose hypotheses are the static-rollout and $β$ -polynomial members of $P_{β}$ , this is $m_{P} (1) - m_{P} (0)$ , proving the unbiasedness identity.
For the variance statement, apply Lemma 9 with $X_{j} = \overset{ˉ}{Y}_{j}$ . Its hypotheses are the nonnegative-scale assumption $σ_{0}^{2} \geq 0$ and the round-mean variance-envelope component of $P_{β}$ . Therefore $Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2},$ and the same lemma supplies a positive semidefinite matrix $Γ$ with $Γ_{j j} \leq \frac{σ _{0}^{2}}{n} for all j, i = 0 \sum k j = 0 \sum k w_{i} Γ_{ij} w_{j} = \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} .$
For the fixed schedule $p$ , the set whose infimum appears on the left-hand side of the first envelope identity is exactly the scalar multiple $⎩ ⎨ ⎧ v : \exists w \in W_{β} (p), v = κ (j = 0 \sum k ∣ w_{j} ∣)^{2} ⎭ ⎬ ⎫ = κ \cdot ⎩ ⎨ ⎧ u : \exists w \in W_{β} (p), u = (j = 0 \sum k ∣ w_{j} ∣)^{2} ⎭ ⎬ ⎫ .$ The unscaled set is nonempty by the first step and is bounded below by $0$ , since its elements are squares. Hence the usual nonnegative-scalar infimum rule applies to this set, and Definition 5 identifies its infimum as $A_{β} (p)$ . With $κ \geq 0$ , $in f ⎩ ⎨ ⎧ v : \exists w \in W_{β} (p), v = \frac{σ _{0}^{2}}{n} (j = 0 \sum k ∣ w_{j} ∣)^{2} ⎭ ⎬ ⎫ = \frac{σ _{0}^{2}}{n} A_{β} (p) .$
The same scalar-infimum step applies after also varying the schedule. Namely, ${v : \exists p^{'} \in S_{k, q}, v = κ A_{β} (p^{'})} = κ \cdot {u : \exists p^{'} \in S_{k, q}, u = A_{β} (p^{'})} .$ This unscaled schedule set is nonempty because the fixed schedule $p$ belongs to $S_{k, q}$ . It is bounded below by $0$ : for every schedule $r$ , $A_{β} (r) \geq 0$ , because $A_{β} (r)$ is the real infimum of squared total-variation norms, with the same convention covering the empty feasible-weight case. Applying the nonnegative-scalar infimum rule and then Definition 5, $in f {v : \exists p^{'} \in S_{k, q}, v = \frac{σ _{0}^{2}}{n} A_{β} (p^{'})} = \frac{σ _{0}^{2}}{n} M_{β, k, q} .$
Finally, suppose $p^{⋆} \in S_{k, q}$ and $A_{β} (p^{⋆}) = M_{β, k, q} .$ For any $p^{'} \in S_{k, q}$ , the value $A_{β} (p^{'})$ belongs to the set ${u : \exists r \in S_{k, q}, u = A_{β} (r)} .$ The same uniform nonnegativity $A_{β} (r) \geq 0$ for all schedules $r$ makes this set bounded below by $0$ . Therefore the defining infimum satisfies $M_{β, k, q} \leq A_{β} (p^{'}) .$ Using $A_{β} (p^{⋆}) = M_{β, k, q}$ , we get $A_{β} (p^{⋆}) \leq A_{β} (p^{'})$ . Multiplication by the nonnegative scalar $κ = σ_{0}^{2} / n$ preserves the inequality, so $\frac{σ _{0}^{2}}{n} A_{β} (p^{⋆}) \leq \frac{σ _{0}^{2}}{n} A_{β} (p^{'}),$ as required.

∎

Proof of Proposition 1.

Let $p_{j} = q j / β$ for $j = 0, \dots, β$ . Since $β \geq 1$ , $q > 0$ , and $q \leq 1$ , each coordinate is nonnegative, and $j \leq β$ gives $0 \leq p_{j} = \frac{q j}{β} \leq q \leq 1.$ Thus $p_{j} \in [0, 1]$ for every $j = 0, \dots, β$ .

For the amplification bound, use the Lagrange endpoint weights on the equal grid. The grid is injective, since $p_{j} = p_{m}$ forces $q j / β = q m / β$ and hence $j = m$ because $q > 0$ and $β > 0$ ; so the Lagrange basis polynomials $L_{j} (t) = 0 \leq m \leq β m \neq = j \prod \frac{t - p _{m}}{p _{j} - p _{m}}, j = 0, \dots, β,$ are well defined, and we set $w_{j} = L_{j} (1) - L_{j} (0), j = 0, \dots, β .$ By Lagrange interpolation on the $β + 1$ distinct nodes, these weights reproduce $r (1) - r (0)$ for every polynomial $r$ of degree at most $β$ ; applied to the monomials $1, u, \dots, u^{β}$ , this is exactly $w \in W_{β} (p)$ as in Definition 3. Since $A_{β} (p)$ is the infimum in Definition 5 over the nonempty set $W_{β} (p)$ , this feasible $w$ gives $A_{β} (p) \leq (j = 0 \sum β ∣ w_{j} ∣)^{2} .$

Set $y = β / q$ . Since $q \leq 1 \leq β$ , we have $y \geq 1$ , and hence $y^{β} \geq 1$ .

The value at $1$ . Fix $j$ . Each factor of $L_{j} (1)$ is controlled separately: from $0 \leq p_{m} \leq q \leq 1$ we get $∣1 - p_{m} ∣ \leq 1$ , while $p_{j} - p_{m} = \frac{q}{β} (j - m), so ∣ p_{j} - p_{m} ∣ = \frac{q}{β} ∣ j - m ∣.$ There are exactly $β$ indices $m \neq = j$ in ${0, \dots, β}$ , so multiplying the $β$ factor bounds gives $∣ L_{j} (1) ∣ = m \neq = j \prod \frac{∣1 - p _{m} ∣}{∣ p _{j} - p _{m} ∣} \leq m \neq = j \prod \frac{β / q}{∣ j - m ∣} = \frac{y ^{β}}{\prod _{m \neq = j} ∣ j - m ∣} .$ The remaining product is a factorial pair: splitting the indices below and above $j$ , $0 \leq m \leq β m \neq = j \prod ∣ j - m ∣ = (m = 0 \prod j - 1 (j - m)) (m = j + 1 \prod β (m - j)) = j! (β - j)! .$ Hence $∣ L_{j} (1) ∣ \leq \frac{y ^{β}}{j ! ( β - j )!} .$ Summing over $j$ requires the binomial identity $j = 0 \sum β \frac{1}{j ! ( β - j )!} = \frac{1}{β !} j = 0 \sum β \frac{β !}{j ! ( β - j )!} = \frac{2 ^{β}}{β !} \leq 2,$ where the first equality rescales each term by $β!$ , the second sums the binomial coefficients $β! / (j! (β - j)!)$ over $j = 0, \dots, β$ , and the last inequality is $2^{β} \leq 2 β!$ , valid for every $β \geq 1$ by induction (the base case $β = 1$ reads $2 \leq 2$ , and the step multiplies the left side by $2$ and the right side by $β + 1 \geq 2$ ). Therefore $j = 0 \sum β ∣ L_{j} (1) ∣ \leq y^{β} j = 0 \sum β \frac{1}{j ! ( β - j )!} \leq 2 y^{β} .$

The value at $0$ . The node $p_{0}$ is exactly $0$ , so $L_{j} (0) = L_{j} (p_{0})$ is the Lagrange basis polynomial evaluated at a node: it equals $1$ for $j = 0$ and $0$ for $j \neq = 0$ . Hence $j = 0 \sum β ∣ L_{j} (0) ∣ = 1.$

Conclusion. By the triangle inequality applied termwise to $w_{j} = L_{j} (1) - L_{j} (0)$ , $j = 0 \sum β ∣ w_{j} ∣ \leq j = 0 \sum β ∣ L_{j} (1) ∣ + j = 0 \sum β ∣ L_{j} (0) ∣ \leq 2 y^{β} + 1 \leq 3 y^{β},$ where the last inequality uses $y^{β} \geq 1$ . Both sides are nonnegative, so squaring and substituting $y = β / q$ yields $A_{β} (p^{eq} (β, q)) \leq (j = 0 \sum β ∣ w_{j} ∣)^{2} \leq (3 y^{β})^{2} = 9 (\frac{β}{q})^{2 β} .$

∎

Proof of Proposition 2.

At the full budget $q = 1$ and with $k = β$ , the equal-spacing schedule has entries $p_{j}^{eq} (β, 1) = \frac{j}{β}, j = 0, \dots, β, so in particular p_{0}^{eq} (β, 1) = 0, p_{β}^{eq} (β, 1) = 1.$ Write $p_{j} = p_{j}^{eq} (β, 1)$ and $w_{0} = - 1, w_{β} = 1, w_{j} = 0 (1 \leq j \leq β - 1) .$ Because $β \geq 1$ , the first and last grid indices are distinct, i.e. $β \neq = 0$ , so the two prescriptions $w_{0} = - 1$ and $w_{β} = 1$ do not conflict and the vector $w$ is well defined.

The moment equations. Only the indices $j = 0$ and $j = β$ carry nonzero weight. For the zeroth moment, $p_{j}^{0} = 1$ for every $j$ (including $p_{0} = 0$ ), so $j = 0 \sum β w_{j} p_{j}^{0} = w_{0} + w_{β} = (- 1) + 1 = 0.$ Now fix $1 \leq ℓ \leq β$ . Since $p_{0} = 0$ gives $p_{0}^{ℓ} = 0^{ℓ} = 0$ and $p_{β} = 1$ gives $p_{β}^{ℓ} = 1$ , $j = 0 \sum β w_{j} p_{j}^{ℓ} = w_{0} p_{0}^{ℓ} + w_{β} p_{β}^{ℓ} = - 0^{ℓ} + 1^{ℓ} = 1,$ with all interior terms vanishing because their weights are zero. These are exactly the moment equations of Definition 3, so $w \in W_{β} (p^{eq} (β, 1))$ .

The amplification bound. By Definition 5, $A_{β} (p^{eq} (β, 1))$ is the infimum of $(\sum_{j} ∣ w_{j}^{'} ∣)^{2}$ over $w^{'} \in W_{β} (p^{eq} (β, 1))$ , a set of nonnegative numbers, so the feasible $w$ just exhibited gives $A_{β} (p^{eq} (β, 1)) \leq (j = 0 \sum β ∣ w_{j} ∣)^{2} .$ The absolute values contribute only at $j = 0$ and $j = β$ , so $j = 0 \sum β ∣ w_{j} ∣ = ∣ - 1∣ + ∣1∣ = 1 + 1 = 2.$ Therefore $A_{β} (p^{eq} (β, 1)) \leq 2^{2} = 4.$

∎

Proof of Theorem 2.

The constants. By Lemma 6, applied with the cap $q_{m a x}$ , choose constants $C_{ep} (q_{m a x}) > 0$ and $c_{ep} (q_{m a x}) > 0$ such that, writing $x_{q} = 2/ q - 1$ and $λ (q) = x_{q} + x_{q}^{2} - 1,$ the following two bounds hold for every $β \geq 1$ and every $0 < q \leq q_{m a x}$ : first, every real polynomial $R$ with $de g (R) \leq β$ and $sup_{x \in [- 1, 1]} ∣ R (x) ∣ \leq 1$ satisfies $∣ R (x_{q}) - R (- 1) ∣ \leq C_{ep} (q_{m a x}) λ (q)^{β};$ and second, $T_{β} (x_{q}) - 1 \geq c_{ep} (q_{m a x}) λ (q)^{β} .$ These constants are chosen before the oversampling ratio is fixed, so set $C_{-} (q_{m a x}) = c_{ep} (q_{m a x})^{2} > 0.$ Now fix $c > 1$ . The Ehlich–Zeller Chebyshev–Lobatto mesh inequality used as the premise of Lemma 5 is available in the following form: for every pair of nonnegative integers $β, k$ , every real polynomial $R$ with $de g (R) \leq β$ and $β < k$ , and every $x \in [- 1, 1]$ , $∣ R (x) ∣ \leq \frac{1}{cos ( π β / ( 2 k ))} 0 \leq j \leq k max R (- cos (\frac{π j}{k})) .$

Applying Lemma 5 with this mesh inequality, choose $K (c) > 0$ with the property that every real polynomial $R$ of degree at most $β$ obeys $sup_{x \in [- 1, 1]} ∣ R (x) ∣ \leq K (c) max_{0 \leq j \leq k} ∣ R (- cos (π j / k)) ∣$ whenever $β \geq 1$ and $k \geq c β$ , and set $C_{+} (c, q_{m a x}) = (K (c) C_{ep} (q_{m a x}))^{2} > 0.$
Standing consequences of the hypotheses. Fix $β, k, q$ satisfying the hypotheses. The low-budget-regime hypothesis gives $q > 0$ , and the low-budget cap of Assumption 4 gives $q \leq q_{m a x} < 1$ ; hence $q \leq 1$ , $q < 1$ , and $0 < q \leq 1$ . Since $k \geq c β$ , $c > 1$ , and $β \geq 1$ , we have $β \leq c β \leq k$ , and in particular $k \geq 1$ . Therefore Lemma 7 gives $p^{Ch} (k, q) \in S_{k, q} .$

The exterior parameter is the exponential base in the statement: $λ (q) = \frac{( 1 + 1 - q ) ^{2}}{q} .$ Indeed, $x_{q}^{2} - 1 = (2/ q - 1)^{2} - 1 = 4/ q^{2} - 4/ q = 4 (1 - q) / q^{2}$ , which is nonnegative because $q < 1$ , so $x_{q}^{2} - 1 = 2 1 - q / q$ ; adding $x_{q} = (2 - q) / q$ gives $λ (q) = (2 - q + 2 1 - q) / q$ , and expanding $(1 + 1 - q)^{2} = 1 + 2 1 - q + (1 - q) = 2 - q + 2 1 - q$ identifies the two expressions.

Finally, for any schedule $p^{'} \in S_{k, q}$ we record the dual quantity of Lemma 3, $D (p^{'}) = sup {∣ r (1) - r (0) ∣ : r \in R [x], de g (r) \leq β, 0 \leq j \leq k max ∣ r (p_{j}^{'}) ∣ \leq 1},$ and note that $D (p^{'}) \geq 0$ because the zero polynomial is feasible.
Lower bound at an arbitrary $p \in S_{k, q}$ . Since $β \geq 1$ , $β \leq k$ , and $p \in S_{k, q}$ , Lemma 8 makes $W_{β} (p)$ nonempty; and the strict ordering $p_{0} < \dots < p_{k}$ required by Definition 1 makes the nodes distinct. Thus Lemma 3 applies and gives $A_{β} (p) = D (p)^{2} .$

Consider the test polynomial $r (u) = T_{β} (\frac{2 u}{q} - 1) .$ Its degree is at most $β$ , being the composition of the degree- $β$ polynomial $T_{β}$ with an affine map. For every rollout node, $p \in S_{k, q}$ gives $p_{j} \geq p_{0} = 0$ and, by monotonicity, $p_{j} \leq p_{k} = q$ ; hence $0 \leq p_{j} \leq q, so \frac{2 p _{j}}{q} - 1 \in [- 1, 1],$ and since $∣ T_{β} ∣ \leq 1$ on $[- 1, 1]$ we get $∣ r (p_{j}) ∣ \leq 1$ . Therefore $r$ is feasible in the supremum defining $D (p)$ . Its endpoint values are $r (1) = T_{β} (\frac{2}{q} - 1) = T_{β} (x_{q}), r (0) = T_{β} (- 1) .$ The endpoint lower bound from Lemma 6 gives $T_{β} (x_{q}) - 1 \geq c_{ep} (q_{m a x}) λ (q)^{β} .$ Since $x_{q} > 1$ we have $T_{β} (x_{q}) \geq 1 > 0$ , so $∣ T_{β} (x_{q}) ∣ = T_{β} (x_{q})$ ; and $∣ T_{β} (- 1) ∣ \leq 1$ . The reverse triangle inequality therefore yields $T_{β} (x_{q}) - 1 \leq ∣ T_{β} (x_{q}) ∣ - ∣ T_{β} (- 1) ∣ \leq ∣ T_{β} (x_{q}) - T_{β} (- 1) ∣ = ∣ r (1) - r (0) ∣ \leq D (p) .$ Hence $D (p) \geq c_{ep} (q_{m a x}) λ (q)^{β} \geq 0$ , and squaring both nonnegative sides, $A_{β} (p) = D (p)^{2} \geq c_{ep} (q_{m a x})^{2} λ (q)^{2 β} = C_{-} (q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$
Upper bound at the Chebyshev–Lobatto schedule. The schedule $p^{Ch} (k, q)$ is admissible by Lemma 7. Together with $β \geq 1$ and $β \leq k$ , Lemma 8 makes $W_{β} (p^{Ch} (k, q))$ nonempty; the strict ordering in $p^{Ch} (k, q) \in S_{k, q}$ gives distinct nodes. Thus Lemma 3 gives $A_{β} (p^{Ch} (k, q)) = D (p^{Ch} (k, q))^{2}$ , and it suffices to bound the dual supremum. Let $r$ be any polynomial with $de g (r) \leq β$ and $max_{0 \leq j \leq k} ∣ r (p_{j}^{Ch} (k, q)) ∣ \leq 1$ , and put $R (x) = r (\frac{q}{2} (x + 1)) .$ Then $de g (R) \leq β$ , again because the inner map is affine. At the Lobatto abscissae the inner map reproduces the schedule, $\frac{q}{2} (- cos \frac{π j}{k} + 1) = \frac{q}{2} (1 - cos \frac{π j}{k}) = p_{j}^{Ch} (k, q), j = 0, \dots, k,$ so $R (- cos (π j / k)) = r (p_{j}^{Ch} (k, q))$ and therefore $0 \leq j \leq k max R (- cos \frac{π j}{k}) \leq 1.$ The oversampled norming inequality supplied by Lemma 5 with the displayed Ehlich–Zeller mesh input applies because $β \geq 1$ , $k \geq c β$ , and $de g (R) \leq β$ . It gives $∣ R (x) ∣ \leq K (c) \cdot 1 = K (c) (x \in [- 1, 1]) .$ Thus $S = K (c)^{- 1} R$ satisfies $de g (S) \leq β$ and $∣ S (x) ∣ \leq 1$ on $[- 1, 1]$ . The inner affine map sends the two relevant points to the two endpoints, $\frac{q}{2} (x_{q} + 1) = \frac{q}{2} \cdot \frac{2}{q} = 1, \frac{q}{2} (- 1 + 1) = 0,$ so $R (x_{q}) = r (1)$ and $R (- 1) = r (0)$ , and hence $S (x_{q}) = K (c)^{- 1} r (1)$ and $S (- 1) = K (c)^{- 1} r (0)$ . Applying the endpoint upper bound from Lemma 6 to $S$ gives $K (c)^{- 1} ∣ r (1) - r (0) ∣ = ∣ S (x_{q}) - S (- 1) ∣ \leq C_{ep} (q_{m a x}) λ (q)^{β},$ that is, $∣ r (1) - r (0) ∣ \leq K (c) C_{ep} (q_{m a x}) λ (q)^{β}$ . Taking the supremum over all such $r$ gives $0 \leq D (p^{Ch} (k, q)) \leq K (c) C_{ep} (q_{m a x}) λ (q)^{β}$ , and squaring both nonnegative sides, $A_{β} (p^{Ch} (k, q)) \leq (K (c) C_{ep} (q_{m a x}))^{2} λ (q)^{2 β} = C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$
The two-sided minimax bound. The first two displayed inequalities of the statement are exactly the bounds just proved. For the minimax lower bound, the universal lower estimate obtained from Lemma 8, Lemma 3, and Lemma 6 holds for every $p \in S_{k, q}$ , and the schedule class is nonempty because $p^{Ch} (k, q) \in S_{k, q}$ ; so the common bound is a lower bound for the nonempty set ${A_{β} (p) : p \in S_{k, q}}$ , and passing to its infimum gives $M_{β, k, q} \geq C_{-} (q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$

For the minimax upper bound, that set is bounded below by $0$ and contains $A_{β} (p^{Ch} (k, q))$ , so its infimum is at most that value; chaining with the Chebyshev upper bound obtained from Lemma 7, Lemma 5, and Lemma 6, $M_{β, k, q} \leq A_{β} (p^{Ch} (k, q)) \leq C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$ This proves the claimed two-sided minimax estimate.

∎

Proof of Lemma 2.

Write $s = σ_{0}^{2} / n$ , where division by $n$ is real division by the natural cast of $n$ used in the real-valued risk definitions; when $n = 0$ , this quotient is the total real quotient and equals $0$ . Since $σ_{0}^{2} \geq 0$ and $(n : R) \geq 0$ , we have $s \geq 0$ . By Definition 6, $Γ_{P} (p)$ is the design covariance matrix of $(\overset{ˉ}{Y}_{0}, \dots, \overset{ˉ}{Y}_{k})$ , so that for every weight vector $w$ $w^{'} Γ_{P} (p) w = Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) .$ All infima and suprema below are the real-valued operations appearing in Definition 6 and Definition 5. Thus an empty law-value supremum has value $0$ , and if every element of a law-value set is at most a nonnegative number $B$ , then its supremum is at most $B$ .

An order-theoretic comparison of infima. Both assertions use the following elementary fact for these real-valued infima. Let $F, G \subseteq R$ , let $c \geq 0$ , suppose $F$ is nonempty and bounded below and $G$ is nonempty, and suppose that $for every g \in G there is f \in F with f \leq c g .$ Then $in f F \leq c in f G .$ Indeed, scalar multiplication by $c \geq 0$ commutes with the real-valued infimum in the form $c in f G = in f {c g : g \in G}$ . Since $F$ is nonempty and bounded below, $in f F$ is a lower bound for $F$ . For each $g \in G$ , the witness $f \in F$ gives $in f F \leq f \leq c g$ , so $in f F$ is a lower bound for ${c g : g \in G}$ . Hence $in f F \leq in f {c g : g \in G} = c in f G$ .

Step 1: the fixed-schedule bound for every admissible schedule. Fix any $p^{'} \in S_{k, q}$ and apply the fact with $c = s$ and $F = {P \in P_{β} sup Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) : w \in W_{β} (p^{'})}, G = ⎩ ⎨ ⎧ (j = 0 \sum k ∣ w_{j} ∣)^{2} : w \in W_{β} (p^{'}) ⎭ ⎬ ⎫ .$ Since $β \geq 1$ , $k \geq β$ , and $p^{'} \in S_{k, q}$ , Lemma 8 supplies some $w \in W_{β} (p^{'})$ , so both $F$ and $G$ are nonempty. Moreover $F$ is bounded below by $0$ : every element of each law-value set is a design variance, hence is nonnegative, and the real-valued supremum of such a set is nonnegative, including the empty case. For the link condition, take $g = (\sum_{j} ∣ w_{j} ∣)^{2} \in G$ and let $f \in F$ be the element indexed by the same $w$ . For every law value appearing in this supremum, Definition 2 gives the round-mean variance envelope for $\overset{ˉ}{Y}_{0}, \dots, \overset{ˉ}{Y}_{k}$ with scale $σ_{0}^{2} / n$ . Hence Lemma 9 gives $Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq s (j = 0 \sum k ∣ w_{j} ∣)^{2} .$ The right-hand side is independent of the law value and is nonnegative, so the real-valued supremum over the law-value set is at most this same quantity. Thus $f \leq s g$ . The fact therefore applies, and since $in f G = A_{β} (p^{'})$ by Definition 5, $w \in W_{β} (p^{'}) in f P \in P_{β} sup w^{'} Γ_{P} (p^{'}) w \leq s w \in W_{β} (p^{'}) in f (j = 0 \sum k ∣ w_{j} ∣)^{2} = \frac{σ _{0}^{2}}{n} A_{β} (p^{'}) .$ Applying this to the given schedule $p$ proves the first assertion, $w \in W_{β} (p) in f P \in P_{β} sup w^{'} Γ_{P} (p) w \leq \frac{σ _{0}^{2}}{n} A_{β} (p) .$

Step 2: passing to the nested risk. Apply the same fact a second time, now with $c = s$ and $F = {w \in W_{β} (p^{'}) in f P \in P_{β} sup w^{'} Γ_{P} (p^{'}) w : p^{'} \in S_{k, q}}, G = {A_{β} (p^{'}) : p^{'} \in S_{k, q}} .$ By Definition 6 and Definition 5, $in f F = R_{exact} (β, k, q)$ and $in f G = M_{β, k, q}$ . Both sets are nonempty because the given schedule satisfies $p \in S_{k, q}$ . The set $F$ is bounded below by $0$ : for each schedule $p^{'}$ , every fixed-weight law supremum is nonnegative by the preceding nonnegativity argument, and the corresponding real-valued infimum over weights is therefore nonnegative. The link condition is exactly the fixed-schedule bound from Step 1: for $g = A_{β} (p^{'})$ , take the element of $F$ indexed by the same $p^{'}$ . Hence $R_{exact} (β, k, q) \leq \frac{σ _{0}^{2}}{n} p^{'} \in S_{k, q} in f A_{β} (p^{'}) = \frac{σ _{0}^{2}}{n} M_{β, k, q} .$

∎

Proof of Proposition 3.

By Theorem 2, applied with the fixed cap $q_{m a x}$ and the oversampling constant $c > 1$ , there is a constant $C_{+} (c, q_{m a x}) > 0$ such that, whenever $β \geq 1$ , $k \geq c β$ , $q > 0$ , and the low-budget cap holds, $A_{β} (p^{Ch} (k, q)) \leq C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β} .$

This is the constant used in the statement; it depends only on $c$ and $q_{m a x}$ .

Now fix $n, β, k, Ω, π, q, σ_{0}^{2}$ satisfying the hypotheses of the lemma, and write $p^{Ch} = p^{Ch} (k, q)$ .

The hypotheses of the two inputs hold. Since $k = ⌈ c β ⌉$ is the least integer at or above $c β$ , and since $c > 1$ and $β \geq 1$ give $β \leq c β$ , we have $β \leq c β \leq k .$ In particular $k \geq β \geq 1$ , so $k \geq 1$ . The low-budget cap of Assumption 4 gives $q \leq q_{m a x} < 1$ , which together with $q > 0$ yields $0 < q \leq 1.$ Therefore Lemma 7 applies and gives $p^{Ch} \in S_{k, q} .$

Finally, write $s = σ_{0}^{2} / n$ , interpreting the quotient as the total real division used in the risk definitions; in particular the quotient is defined also when $n = 0$ , where it equals $0$ . Since $σ_{0}^{2} \geq 0$ and the real cast of a natural number is nonnegative, this gives $s = \frac{σ _{0}^{2}}{n} \geq 0$ uniformly over the whole range of population sizes, with no case distinction.

Envelope comparison at the Chebyshev schedule. For any weight vector $w$ , the exact quadratic form is by definition the design variance of the corresponding linear rollout estimator, $w^{'} Γ_{P} (p^{Ch}) w = Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}),$ because $Γ_{P} (p)$ is the design covariance matrix of $(\overset{ˉ}{Y}_{0}, \dots, \overset{ˉ}{Y}_{k})$ . Applying the fixed-schedule part of Lemma 2 to the admissible schedule $p^{Ch}$ , whose hypotheses $β \geq 1$ , $k \geq β$ , $0 < q \leq 1$ , $σ_{0}^{2} \geq 0$ and $p^{Ch} \in S_{k, q}$ were just verified, gives $w \in W_{β} (p^{Ch}) in f P \in P_{β} sup Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} A_{β} (p^{Ch}) .$

Conclusion. Since $s = σ_{0}^{2} / n \geq 0$ , multiplying the Chebyshev upper bound for $A_{β} (p^{Ch})$ by $σ_{0}^{2} / n$ preserves the inequality, so chaining the last two displays gives $w \in W_{β} (p^{Ch}) in f P \in P_{β} sup Var_{π} (j = 0 \sum k w_{j} \overset{ˉ}{Y}_{j}) \leq \frac{σ _{0}^{2}}{n} A_{β} (p^{Ch}) \leq \frac{σ _{0}^{2}}{n} C_{+} (c, q_{m a x}) (\frac{( 1 + 1 - q ) ^{2}}{q})^{2 β},$ which is the asserted bound.

∎

References

Rubin, Donald B. (1974). Estimating Causal Effects of Treatments in Randomized and Nonrandomized Studies. Journal of Educational Psychology. doi
Imbens, Guido W. and Rubin, Donald B. (2015). Causal Inference for Statistics, Social, and Biomedical Sciences. Cambridge University Press. doi
Manski, Charles F. (1993). Identification of Endogenous Social Effects: The Reflection Problem. The Review of Economic Studies. doi
Manski, Charles F. (2013). Identification of Treatment Response with Social Interactions. The Econometrics Journal. doi
Aronow, Peter M. and Samii, Cyrus (2017). Estimating Average Causal Effects Under General Interference, with Application to a Social Network Experiment. The Annals of Applied Statistics. doi
Fredrik Sävje and Peter M. Aronow and Michael G. Hudgens (2017). Average treatment effects in the presence of unknown interference. . arXiv
Eckles, Dean and Karrer, Brian and Ugander, Johan (2017). Design and Analysis of Experiments in Networks: Reducing Bias from Interference. Journal of Causal Inference. doi
Ugander, Johan and Karrer, Brian and Backstrom, Lars and Kleinberg, Jon (2013). Graph cluster randomization. Proceedings of the 19th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. doi
Athey, Susan and Eckles, Dean and Imbens, Guido W. (2017). Exact<i>p</i>-Values for Network Interference. Journal of the American Statistical Association. doi
Basse, Guillaume and Feller, Avi and Toulis, Panos (2019). Randomization Tests of Causal Effects Under Interference. Biometrika. doi
Puelz, David and Basse, Guillaume and Feller, Avi and Toulis, Panos (2019). A Graph-Theoretic Approach to Randomization Tests of Causal Effects Under General Interference. . arXiv
Cortez, Mayleen and Eichhorn, Matthew and Yu, Christina Lee (2022). Staggered Rollout Designs Enable Causal Inference Under Interference Without Network Knowledge. . arXiv
Cortez-Rodriguez, Mayleen and Eichhorn, Matthew and Yu, Christina Lee (2022). Exploiting Neighborhood Interference with Low Order Interactions under Unit Randomized Design. . arXiv
Cortez-Rodriguez, Mayleen and Eichhorn, Matthew and Yu, Christina Lee (2024). Analysis of Two-Stage Rollout Designs with Clustering for Causal Inference under Network Interference. . arXiv
Eichhorn, Matthew and Khan, Samir and Ugander, Johan and Yu, Christina Lee (2024). Low-Order Outcomes and Clustered Designs: Combining Design and Analysis for Causal Inference under Network Interference. . arXiv
Jiang, Yiming and Wang, He (2023). Causal Inference under Network Interference Using a Mixture of Randomized Experiments. . arXiv
Cai, Chencheng and Zhang, Xu and Airoldi, Edoardo M. (2023). Independent-Set Design of Experiments for Estimating Treatment and Spillover Effects under Network Interference. . arXiv
Roth, Jonathan and Sant'Anna, Pedro H. C. (2021). Efficient Estimation for Staggered Rollout Designs. . arXiv
Chen, Xinyuan and Li, Fan (2025). Model-Assisted Inference for Dynamic Causal Effects in Staggered Rollout Cluster Randomized Experiments. . arXiv
Fan, Xinyuan and Leng, Chenlei and Wu, Weichi (2025). Causal Inference under Interference: Regression Adjustment and Optimality. . arXiv
Bhadra, Subhankar and Schweinberger, Michael (2025). Causal Inference Under Network Interference. . arXiv
Maresa Schröder and Miruna Oprescu and Stefan Feuerriegel and Nathan Kallus (2026). Causal Inference on Networks under Misspecified Exposure Mappings: A Partial Identification Framework. . arXiv
Smith, Kirstine (1918). On the Standard Deviations of Adjusted and Interpolated Values of an Observed Polynomial Function and Its Constants and the Guidance They Give Towards a Proper Choice of the Distribution of Observations. Biometrika. doi
Kiefer, Jack and Wolfowitz, Jacob (1959). Optimum Designs in Regression Problems. The Annals of Mathematical Statistics. doi
Kiefer, J. (1974). General Equivalence Theory for Optimum Designs (Approximate Theory). The Annals of Statistics. doi
Pukelsheim, Friedrich (1993). Optimal Design of Experiments. Wiley.
Karlin, Samuel and Studden, William J. (1966). Tchebycheff Systems: With Applications in Analysis and Statistics. Wiley-Interscience.

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 (2)

Setup S-1 — Finite-population monotone-Bernoulli rollout DESIGN world: the only randomness is the experimenter's rollout randomization pi over a finite assignment space; round means bar_Y_j are real random variables of the realized assignment, and E_pi/Var_pi/Cov_pi are finite-sum design moments. This is exactly the abstraction of Causalean's FiniteDesign probability layer. — FiniteDesign Ω = PMF over a finite assignment space with FiniteDesign.E/Var/Cov as finite sums (Design.lean:45-217). bar_Y_j : Ω → ℝ are round-mean random variables; Var_pi(bar_Y_j) is FiniteDesign.Var, Gamma_P(p) is the (k+1)x(k+1) FiniteDesign.Cov matrix, hat_tau_{w,p} = ∑ w_j bar_Y_j. FiniteDesign.Var_linear_comb / Var_const_mul / Cov_* supply the design-variance algebra reused by the variance-layer lemmas. The paper takes the potential-outcome / static-rollout consistency and the per-round variance ENVELOPE as threaded Prop assumptions (inherited setup + novel envelope), so Y_i(z), Z_j, U_n, m_P, a_{P,ell}, tau_P are exposed at the abstract FiniteDesign level rather than via a bespoke PO structure — the highest-leverage reuse decision, matching the paper's honest scope (novelty is the approximation-theoretic design object, not new PO machinery). Surveyed Causalean PO substrate (PotentialOutcome.lean, Exposure.lean, HT/*): those target Horvitz–Thompson measure/measurability estimation under exposure mappings and DERIVE design variance from network structure; this paper instead ASSUMES the round-variance envelope, so the HT variance derivations (var_htMean_le, EdgeVarianceBound, CompoundVariance) are a different abstraction and not a fit — recorded as bypass-justified.
Setup S-2 — Real / polynomial ℓ¹ optimal-recovery ambient: budgeted node schedules, linear-unbiased weight vectors, the ℓ¹ amplification criterion and its minimax value, and the Chebyshev / equal-spacing grids are pure real-analytic objects over ℝ, Fin (k+1) → ℝ, and Polynomial ℝ (Mathlib). No design/PMF object appears in these definitions or in the approximation-theoretic lemmas. — bypass-justified: the amplification criterion A_beta(p) = inf over W_beta(p) of (∑|w_j|)² is a pure ℓ¹/ℓ∞-dual optimal-recovery quantity over polynomial-unbiased weight vectors; the Causalean design world (FiniteDesign) is at a different abstraction (measure of a randomization) and does not fit these purely algebraic-analytic objects. Searched Causalean experimentation substrate for 'amplification / minimax schedule / Chebyshev node / budgeted design' (npm search concepts, lean_local_search FiniteDesign/Optimality/Minimax/Neyman): Optimality/Minimax.lean is Neyman-allocation design minimax, not node-placement ℓ¹ amplification — not found. Mathlib supplies Polynomial.Chebyshev.T ℝ n and the Extremal/RootsExtrema Chebyshev API used by the endpoint lemmas.

Definitions (7)

Definition P-1 verified CausalSmith.Experimentation.RolloutChebyshev.BudgetedSchedule S_{k,q} = { p in [0,1]^(k+1) : p_0 = 0 and 0 < p_1 < ... < p_k = q }
Definition P-2 verified CausalSmith.Experimentation.RolloutChebyshev.RolloutLawClass P_beta = { P : ass:static-rollout-consistency and ass:beta-order-polynomial and ass:round-mean-variance-envelope }
Definition P-3 verified CausalSmith.Experimentation.RolloutChebyshev.UnbiasedWeights W_beta(p) = { w in R^(k+1) : sum_{j=0}^k w_j p_j^0 = 0 and sum_{j=0}^k w_j p_j^ell = 1 for ell = 1, ..., beta }
Definition P-4 verified CausalSmith.Experimentation.RolloutChebyshev.chebyshevSchedule p_j^Ch(k,q) = q { 1 - cos(pi j / k) } / 2 for j = 0, ..., k, and p^Ch(k,q) = (p_0^Ch(k,q), ..., p_k^Ch(k,q)).
Definition P-5 verified CausalSmith.Experimentation.RolloutChebyshev.minimaxAmplification A_beta(p) = inf_{w in W_beta(p)} (sum_{j=0}^k |w_j|)^2 and M_{beta,k,q} = inf_{p in S_{k,q}} A_beta(p).
Definition P-6 verified CausalSmith.Experimentation.RolloutChebyshev.exactNestedRisk R_exact(beta,k,q) = inf_{p in S_{k,q}} inf_{w in W_beta(p)} sup_{P in P_beta} w' Gamma_P(p) w.
Definition P-7 verified CausalSmith.Experimentation.RolloutChebyshev.exactNestedMinimaxQuestion Under ass:low-budget-cap, with beta>=1, k=ceil(c beta), q in (0,q_max], and the admissible Chebyshev schedule p^Ch(k,q) in S_{k,q} (lem:chebyshev-schedule-admissible), does the shifted Chebyshev-Lobatto schedule also solve the exact finite-population nested-rollout minimax problem R_exact(beta,k,q), where Gamma_P(p) is the true covariance matrix of the monotone Bernoulli rollout rather than the total-variation variance envelope? The Chebyshev schedule is rate-feasible for R_exact by thm:chebyshev-minimax (the Chebyshev-schedule amplification upper bound) together with lem:exact-risk-envelope-upper (the envelope-to-exact-risk bridge); exact optimality is open.

Assumptions (4)

Assumption A-1 verified CausalSmith.Experimentation.RolloutChebyshev.StaticRolloutConsistency At each rollout measurement j, the observed round mean equals bar_Y_j = n^(-1) sum_{i in U_n} Y_i(Z_j), and the potential outcomes depend on the contemporaneous assignment vector Z_j but not on earlier rollout steps.
Assumption A-2 verified CausalSmith.Experimentation.RolloutChebyshev.BetaOrderPolynomial For every law P, the rollout mean curve satisfies m_P(u) = sum_{ell=0}^beta a_{P,ell} u^ell for all u in [0,1].
Assumption A-3 verified CausalSmith.Experimentation.RolloutChebyshev.RoundMeanVarianceEnvelope For every law P, every admissible schedule p, and every rollout measurement j, Var_pi(bar_Y_j) <= sigma_0^2 / n.
Assumption A-4 verified CausalSmith.Experimentation.RolloutChebyshev.LowBudgetCap q <= q_max < 1.

Lemmas (12)

Lemma L-1 verified CausalSmith.Experimentation.RolloutChebyshev.rollout_polynomial_identity Under ass:static-rollout-consistency and ass:beta-order-polynomial, tau_P = m_P(1) - m_P(0) = sum_{ell=1}^beta a_{P,ell}.
Lemma L-2 verified CausalSmith.Experimentation.RolloutChebyshev.equal_spacing_benchmark Let p^eq(beta,q) = (0, q / beta, 2 q / beta, ..., q). There exists a universal positive constant C_eq (one may take C_eq = 9) such that A_beta(p^eq(beta,q)) <= C_eq (beta / q)^(2 beta) for every integer beta >= 1 and every q in (0,1].
Lemma L-3 verified CausalSmith.Experimentation.RolloutChebyshev.no_extrapolation_boundary At the full-budget boundary q = 1, the equal-spacing schedule p^eq(beta,1) admits the endpoint rule w_0 = -1, w_beta = 1, and w_j = 0 for j = 1, ..., beta - 1; hence w belongs to W_beta(p^eq(beta,1)) and A_beta(p^eq(beta,1)) <= 4.
Lemma L-4 verified CausalSmith.Experimentation.RolloutChebyshev.amplification_dual_norm For a schedule p with distinct nodes and with W_beta(p) nonempty, inf_{w in W_beta(p)} sum_j |w_j| equals sup{|r(1)-r(0)| : r is a real polynomial of degree at most beta and max_j |r(p_j)|<=1}. Consequently A_beta(p) is the square of this dual norm.
Lemma L-5 verified CausalSmith.Experimentation.RolloutChebyshev.chebyshev_exterior_extremal Assume beta>=1. For every real polynomial P of degree at most beta with sup_{x in [-1,1]} |P(x)|<=1 and every x_0>1, one has |P(x_0)| <= T_beta(x_0).
Lemma L-6 verified CausalSmith.Experimentation.RolloutChebyshev.oversampled_chebyshev_lobatto_norming For each c>1 there is a finite constant K(c) such that, for every beta>=1, every integer k>=c beta, and every real polynomial R of degree at most beta, sup_{x in [-1,1]} |R(x)| <= K(c) max_{0<=j<=k} |R(-cos(pi j/k))|.
Lemma L-7 verified CausalSmith.Experimentation.RolloutChebyshev.continuous_chebyshev_endpoint_bound Let q in (0,1), x_q=2/q-1, lambda(q)=x_q+sqrt(x_q^2-1), and rho(q)=q lambda(q)=(1+sqrt(1-q))^2. For every degree-beta polynomial R with sup_{x in [-1,1]}|R(x)|<=1, |R(x_q)-R(-1)| <= C(q_max) lambda(q)^beta uniformly over q in (0,q_max]; and the Chebyshev polynomial T_beta gives the matching lower order T_beta(x_q)-1 >= c(q_max) lambda(q)^beta.
Lemma L-8 verified CausalSmith.Experimentation.RolloutChebyshev.chebyshev_schedule_admissible For every integer k>=1 and q in (0,1], the shifted Chebyshev-Lobatto schedule p^Ch(k,q) belongs to S_{k,q}.
Lemma L-9 verified CausalSmith.Experimentation.RolloutChebyshev.unbiased_weight_set_nonempty Assume beta>=1 and k>=beta. For every schedule p in S_{k,q}, the unbiased linear weight set W_beta(p) is nonempty.
Lemma L-10 verified CausalSmith.Experimentation.RolloutChebyshev.variance_envelope_sharpness If X_0,...,X_k are square-integrable rollout-round statistics with Var_pi(X_j)<=sigma_0^2/n for every j, then Var_pi(sum_j w_j X_j) <= sigma_0^2 n^(-1) (sum_j |w_j|)^2 for every real w. Moreover this bound is sharp over covariance matrices whose diagonal entries are bounded by sigma_0^2/n.
Lemma L-11 verified CausalSmith.Experimentation.RolloutChebyshev.exact_risk_envelope_upper Assume beta>=1 and k>=beta. For every q in (0,1] and every p in S_{k,q}, inf_{w in W_beta(p)} sup_{P in P_beta} w' Gamma_P(p) w <= (sigma_0^2/n) A_beta(p). Consequently R_exact(beta,k,q) <= (sigma_0^2/n) M_{beta,k,q}.
Lemma L-12 verified CausalSmith.Experimentation.RolloutChebyshev.exact_chebyshev_rate_feasible Fix c>1, beta>=1, k=ceil(c beta), q in (0,q_max], and rho(q)=(1+sqrt(1-q))^2. The admissible shifted Chebyshev-Lobatto schedule satisfies inf_{w in W_beta(p^Ch(k,q))} sup_{P in P_beta} w' Gamma_P(p^Ch(k,q)) w <= (sigma_0^2/n) C_+(c,q_max) (rho(q)/q)^(2 beta). Consequently R_exact(beta,k,q) <= (sigma_0^2/n) C_+(c,q_max) (rho(q)/q)^(2 beta).

Theorems (2)

Theorem T-1 verified CausalSmith.Experimentation.RolloutChebyshev.tv_envelope_design Assume beta>=1 and k>=beta. For every schedule p in S_{k,q} and every weight vector w in W_beta(p), the estimator hat_tau_{w,p} is design-unbiased for tau_P over P in P_beta, and Var_pi(hat_tau_{w,p}) <= sigma_0^2 n^(-1) (sum_{j=0}^k |w_j|)^2. Consequently, since W_beta(p) is nonempty for every p in S_{k,q}, over the sharp total-variation variance envelope the best achievable design variance for a fixed schedule p is sigma_0^2 n^(-1) A_beta(p); the dimensionless minimax amplification value over budgeted schedules is M_{beta,k,q}=inf_{p in S_{k,q}} A_beta(p); the corresponding minimax design variance over budgeted schedules is sigma_0^2 n^(-1) M_{beta,k,q}; and an optimal schedule for the variance envelope is any minimizer p^* in S_{k,q} attaining A_beta(p^*)=M_{beta,k,q}.
Theorem T-2 verified CausalSmith.Experimentation.RolloutChebyshev.chebyshev_minimax Fix c > 1 and q_max in (0,1), and define the pointwise Chebyshev base rho(q)=(1+sqrt(1-q))^2. There exist positive constants C_-(q_max) and C_+(c,q_max) such that, for every beta>=1, every integer k >= c beta, and every q in (0,q_max], every schedule p in S_{k,q} satisfies A_beta(p) >= C_-(q_max) (rho(q)/q)^(2 beta), while the shifted Chebyshev-Lobatto schedule satisfies A_beta(p^Ch(k,q)) <= C_+(c,q_max) (rho(q)/q)^(2 beta). Hence M_{beta,k,q} has pointwise low-budget exponential base rho(q)/q; as q downarrow 0 this is 4/q, the intrinsic exponent is 2 beta, and the equal-spacing beta/q factor is not minimax in beta once the rollout uses more than beta+1 nodes.

Auxiliary Lean lemmas (machine-checked) (25)

Lemma CausalSmith.Experimentation.RolloutChebyshev.lagrange_endpoint_weights_unbiased —
Lemma CausalSmith.Experimentation.RolloutChebyshev.sInf_le_mul_sInf_of_forall_exists_le —
Lemma CausalSmith.Experimentation.RolloutChebyshev.neg_one_pow_mul_le_of_abs_le_one —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_exterior_lagrange_coeff_nonneg —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_eval_eq_lambda_average —
Lemma CausalSmith.Experimentation.RolloutChebyshev.endpoint_lambda_mono —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_lambda_average_add_one_le —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_lambda_average_sub_one_ge —
Lemma CausalSmith.Experimentation.RolloutChebyshev.equalSchedule_injective —
Lemma CausalSmith.Experimentation.RolloutChebyshev.equalSchedule_lagrange_basis_eval_one_le —
Lemma CausalSmith.Experimentation.RolloutChebyshev.prod_Iic_erase_abs_sub_eq_factorial —
Lemma CausalSmith.Experimentation.RolloutChebyshev.two_pow_le_two_mul_factorial —
Lemma CausalSmith.Experimentation.RolloutChebyshev.factorial_reciprocal_sum_le_two —
Lemma CausalSmith.Experimentation.RolloutChebyshev.ehlichZellerMesh —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_lambda_eq_rho_div_q —
Lemma CausalSmith.Experimentation.RolloutChebyshev.amplification_nonneg —
Lemma CausalSmith.Experimentation.RolloutChebyshev.minimaxAmplification_le_of_budgeted —
Lemma CausalSmith.Experimentation.RolloutChebyshev.minimaxAmplification_lower_of_forall —
Lemma CausalSmith.Experimentation.RolloutChebyshev.budgetedSchedule_le_endpoint —
Lemma CausalSmith.Experimentation.RolloutChebyshev.affine_mem_Icc_neg_one_one —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_affine_natDegree_le —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_amplification_lower —
Lemma CausalSmith.Experimentation.RolloutChebyshev.lobatto_affine_comp_natDegree_le —
Lemma CausalSmith.Experimentation.RolloutChebyshev.chebyshev_amplification_upper —
Lemma CausalSmith.Experimentation.RolloutChebyshev.one_le_rhoCh —

Symbol realizations (Lean @realizes) (25)

bar_Y_j verified realized by StaticRolloutConsistency
Y_i(z) verified realized by StaticRolloutConsistency
Z_j verified realized by StaticRolloutConsistency
U_n verified realized by StaticRolloutConsistency
m_P verified realized by BetaOrderPolynomial, RolloutLawClass
a_{P,0} verified realized by BetaOrderPolynomial
... verified realized by BetaOrderPolynomial
a_{P,beta} verified realized by BetaOrderPolynomial
sigma_0^2 verified realized by RoundMeanVarianceEnvelope
q_max verified realized by LowBudgetCap
p verified realized by BudgetedSchedule
q(carrier ℝ; range (0,1] via p (last k) = q with p 0 = 0, StrictMono p, Icc clause) verified realized by BudgetedSchedule
S_{k,q} verified realized by BudgetedSchedule
W_beta(p) verified realized by UnbiasedWeights
w verified realized by UnbiasedWeights
p^Ch(k,q) verified realized by chebyshevSchedule, chebyshev_schedule_admissible
q verified realized by chebyshevSchedule, chebyshev_schedule_admissible, equal_spacing_benchmark, exactNestedMinimaxQuestion, exact_chebyshev_rate_feasible, equalSchedule, chebyshev_minimax
A_beta(p) verified realized by amplification
M_{beta,k,q} verified realized by minimaxAmplification
rho_Ch(c,q_max) verified realized by rhoCh, chebyshev_minimax, one_le_rhoCh
P_beta verified realized by RolloutLawClass
R_exact(beta,k,q) verified realized by exactNestedRisk
Gamma_P(p) verified realized by exactNestedRisk
p^eq(beta,q) verified realized by equal_spacing_benchmark, equalSchedule
c verified realized by exactNestedMinimaxQuestion, exact_chebyshev_rate_feasible, chebyshev_minimax

Proof map 14 statements · 14 edges

Chebyshev Rollout Schedules for Polynomial Extrapolation under Low-Order Interference

Abstract

Introduction

Setup and Assumptions

Main Results

Discussion and Extensions

Exact-covariance scope and limitations

Future work

Appendices

Proofs and Verification

Verification note.

Proofs of the main results

References