All missions

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$, how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

$$s = \lambda + \gamma\sqrt{\lambda},$$

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$, its mean and variance are both $\lambda$, so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$. The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

• The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
• Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
• Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$, the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$-th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$, the number of arrivals in $(0, t]$. This is a Poisson process of rate $\lambda$.

Customers are numbered $k = 0, 1, 2, \dots$; customer $k$ arrives at $\tau_{k+1}$, is served at once, and has service time $D_k$. Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$. The number of busy servers is

$$N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.$$

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$. Each customer carries a class label $J_k$, the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$. The class-$i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$.

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$, then

$$P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots$$

The law depends on the service-time distribution only through its mean.

Milestones

1. Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$, pathwise.
2. Proof of Proposition 2.4 (p. 712): for $t \ge 1$, $A(t) - A(t-1)$ has the same law as $A(1)$.
3. Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$.
4. §2.5, splitting (p. 713): the class-$i$ arrivals form independent Poisson streams of rates $\lambda p_i$; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
5. §2.5, "Hence" (p. 713): for $t > \max_i d_i$, the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$, and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$, connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$.

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$, the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$-server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

• a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
• Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
• the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$.

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$: the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

• The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
• The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
• Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$, and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$, avoiding pushforwards of possibly non-measurable maps.
• Standing conventions: service rate $1$; the system starts empty at time $0$; arrival counted at $t$, departure not; "steady state" means the law at each fixed $t > \max_i d_i$, with no limit $t \to \infty$; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$, and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$. Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
• Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

• W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

Motivation

Temporal-difference learning, TD($\lambda$), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of $K$ fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors $\phi(i)$, and counterexamples in which related algorithms diverge.

Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD($\lambda$) with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator $\Pi T^{(\lambda)}$ and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.

Timeline:

• 1988: Sutton introduces TD($\lambda$) and proves convergence in the mean for TD(0) on absorbing chains with linearly independent features.
• 1992: Dayan extends convergence in the mean to general $\lambda$.
• 1994: Jaakkola, Jordan and Singh, and Tsitsiklis, prove almost-sure convergence for lookup tables, using maximum-norm contraction.
• 1996: Tsitsiklis and Van Roy prove almost-sure convergence with linear function approximation and the error bound below.

Setting

A Markov chain $i_0, i_1, \dots$ lives on a finite or countably infinite state space $S$, with transition matrix $P = (p_{ij})$. A transition from $i$ to $j$ costs $g(i,j)$, and $\alpha \in (0,1)$ is a discount factor. The cost-to-go is

$$J^*(i) = E\Big[\sum_{t=0}^\infty \alpha^t g(i_t,i_{t+1}) \,\Big|\, i_0 = i\Big].$$

Basis functions $\phi_1,\dots,\phi_K : S \to \mathbb R$ give the feature vector $\phi(i) \in \mathbb R^K$ and the approximation $\tilde J(i,r) = r'\phi(i)$, written $\Phi' r$ as a vector over $S$.

Starting from an arbitrary $r_0$, TD($\lambda$) with $\lambda \in [0,1]$ and step sizes $\gamma_t$ forms the eligibility vector $z_t = \sum_{k=0}^t (\alpha\lambda)^{t-k}\phi(i_k)$ and the temporal difference $d_t = g(i_t,i_{t+1}) + \alpha\phi(i_{t+1})'r_t - \phi(i_t)'r_t$, and updates $r_{t+1} = r_t + \gamma_t d_t z_t$.

Let $\pi$ be the invariant distribution, $D = \mathrm{diag}(\pi)$, $\|J\|_D^2 = \sum_i \pi(i)J(i)^2$, and $L_2(S,D) = \{J : \|J\|_D < \infty\}$. Write $\Pi = \Phi'(\Phi D\Phi')^{-1}\Phi D$ for the $D$-orthogonal projection onto $\{\Phi'r\}$. The operator $T^{(\lambda)}$ averages $m$-stage truncated costs:

$$(T^{(\lambda)}J)(i) = (1-\lambda)\sum_{m=0}^\infty \lambda^m E\Big[\sum_{t=0}^m \alpha^t g(i_t,i_{t+1}) + \alpha^{m+1}J(i_{m+1}) \,\Big|\, i_0 = i\Big],$$

for $\lambda < 1$, and $T^{(1)}J = J^*$. The paper makes four assumptions:

1. the chain has a unique invariant distribution with $\pi(i) > 0$, $E_0[g^2] < \infty$, and finite $J^*$;
2. the $\phi_k$ are linearly independent with $E_0[\phi_k^2] < \infty$;
3. polynomial moment growth and summable mixing conditions, relative to coordinates $\sigma(i) \in \mathbb R^N$ of the states;
4. nonnegative, nonincreasing step sizes with $\sum\gamma_t = \infty$ and $\sum\gamma_t^2 < \infty$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1–4: $J^* \in L_2(S,D)$; for every $\lambda \in [0,1]$, TD($\lambda$) converges with probability 1, from every initial state and every $r_0$, to a vector $r^*$; $r^*$ is the unique solution of

$$\Pi T^{(\lambda)}(\Phi' r^*) = \Phi' r^*;$$

and

$$\|\Phi' r^* - J^*\|_D \le \frac{\|\Pi J^* - J^*\|_D}{1 - \alpha(1-\lambda)/(1-\lambda\alpha)}.$$

Milestones

• Lemma 1: $\|PJ\|_D \le \|J\|_D$.
• Lemma 2: $J^*$ is finite, lies in $L_2(S,D)$, and $J^* = \sum_t(\alpha P)^t\bar g$.
• Lemma 3: $T^{(\lambda)}$ maps $L_2(S,D)$ into itself and has a closed-form series.
• Lemma 4: $T^{(\lambda)}$ is a $\|\cdot\|_D$-contraction with modulus $\alpha(1-\lambda)/(1-\alpha\lambda)$.
• Lemma 5: $\Pi T^{(\lambda)}$ has a unique fixed point $\Phi'r^*$, with the error bound above.
• Lemma 6: steady-state moments of $\phi$ and $z_t$.
• Lemma 7: the steady-state mean step is $E_0[s(r,X_t)] = \Phi D(T^{(\lambda)}(\Phi'r) - \Phi'r)$.
• Lemma 8: $(r - r^*)'E_0[s(r,X_t)] < 0$ for $r \neq r^*$.
• Theorem 2: a stochastic approximation theorem with Markov noise.
• §6: $A = E_0[A(X_t)]$ is negative definite and $Ar^* + b = 0$.

Significance

Theorem 1 says that TD($\lambda$), run on-line along a single trajectory, converges for every $\lambda$, and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as $\lambda \to 1$ the limit approaches the best approximation $\Pi J^*$, and that for smaller $\lambda$ the error can grow by at most a factor $(1-\alpha\lambda)/(1-\alpha)$. The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, $\|\cdot\|_D$, which holds only when states are sampled along the chain.

The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:

• a Lean model of countable-state Markov chains with costs, their path law, the weighted space $L_2(S,D)$ and the projection $\Pi$, which is reusable for later work on linear TD, LSTD and approximate policy evaluation;
• the deterministic layer (Lemmas 1–5, 7, 8), which is self-contained functional analysis on $L_2(S,D)$;
• Theorem 2, a stochastic approximation theorem with Markov noise, which the paper quotes from Benveniste, Métivier and Priouret (1987) without proof. A formal proof of it would be a library result in its own right.

Difficulty

The obvious approach treats TD($\lambda$) as a noisy version of the deterministic iteration $\bar r_{t+1} = \bar r_t + \gamma_t\Phi D(T^{(\lambda)}(\Phi'\bar r_t) - \Phi'\bar r_t)$. It fails at the noise. The increments $s(r_t,X_t)$ are driven by the Markov process $X_t = (i_t,i_{t+1},z_t)$, not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with $z_{-1} = 0$ rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: $\Pi$ is a nonexpansion of $\|\cdot\|_D$ only because $D$ is the invariant distribution of the same chain that defines $T^{(\lambda)}$.

Formalization scope

$S$ is a countable type with the discrete $\sigma$-algebra, $P$ a Markov kernel ($p_{ij} = P(i)(\{j\})$, $P^m$ the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:

• $\alpha \in (0,1)$ and $\lambda \in [0,1]$;
• "with probability 1" is almost-sure convergence under the path law from each deterministic initial state;
• $J^*$ and $T^{(\lambda)}$ are defined by the page's path expectations, not by the series of Lemmas 2 and 3;
• $L_2(S,D)$ membership is summability of $\pi(i)J(i)^2$;
• Assumption 1(c) means absolute integrability of the discounted cost series;
• vector norms are Euclidean and matrix norms Frobenius (equivalent to the induced norm and used only under existential constants);
• $(\Phi D\Phi')^{-1}$ is Lean's matrix inverse, invertible under Assumptions 1(a) and 2;
• the steady-state process of Lemmas 6–8 is any two-sided chain on a probability space with the stationary finite-dimensional distributions.

Lean's integral of a non-integrable function and sum of a non-summable series are $0$. A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.

The development needs the following:

• Markov-chain path measures and stationary two-sided chains;
• Bochner integrals of vector-valued functions;
• the Cauchy–Schwarz inequality on $L_2(S,D)$;
• a Markov-noise stochastic approximation theorem.

Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from $\pi$ and $P$ (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.

Selected references

• J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT LIDS report LIDS-P-2322, 1996; IEEE Transactions on Automatic Control 42(5):674–690, 1997. https://doi.org/10.1109/9.580874
• A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990 (French original 1987). https://doi.org/10.1007/978-3-642-75894-2
• R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3:9–44, 1988. https://doi.org/10.1007/BF00115009
• P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8:341–362, 1992. https://doi.org/10.1007/BF00992701
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the convergence of stochastic iterative dynamic programming algorithms, Neural Computation 6(6):1185–1201, 1994. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous stochastic approximation and Q-learning, Machine Learning 16:185–202, 1994. https://doi.org/10.1007/BF00993306

Motivation

In a wireless multihop network, a switch, or a parallel computer, transmissions interfere: two links that share a receiver, or two crossbar paths that share a port, cannot be active in the same time slot. The scheduler must choose, slot by slot, a set of links that may operate together and decide which traffic each one carries. The basic question is which arrival rates a network can sustain at all, and whether a single scheduling rule sustains every one of them without knowing the rates.

Tassiulas and Ephremides answered both questions in 1992 for a general slotted model with interference constraints, multihop routing and several traffic classes (IEEE Trans. Automat. Control 37(12):1936–1948). Their policy, here called $\pi_0$, weighs each link by the largest queue-length difference it can reduce and activates a maximum-weight feasible set. It is the origin of the max-weight and back-pressure scheduling rules that later became standard in switch scheduling (McKeown, Mekkittikul, Anantharam and Walrand, 1999) and in stochastic network optimization (Georgiadis, Neely and Tassiulas, 2006).

Setting

A constrained queueing network has $L$ nodes, $N$ servers (links) and $J$ customer classes. Server $i$ moves customers from its origin node $q(i)$ to its destination node $h(i)$. Class $j$ leaves the network on reaching a node of its destination set $V_j$; at every other node $l$ it has a queue $(l,j)$, whose length at the end of slot $t$ is $X_{lj}(t)\in\mathbb N$.

The constraint set $S$ is the family of sets of servers that may be active in the same slot. Assumption C.1 says that every subset of an activation set is an activation set. In each slot a stationary policy, given the state $x=X(t-1)$, chooses a set of servers in $S$ and the class each active server serves; an activation rule never activates more servers of queue $(l,j)$ than there are customers $x_{lj}$. The class of all such rules is $H$. An activated server $i$ completes its service with probability $m_i$, independently. New arrivals $A_{lj}(t)$ are i.i.d. over slots, independent across queues and of the services, with finite second moments and means $a_{lj}$. Under a stationary rule the vector $X(t)$ is a Markov chain on $\mathbb N^{\{\text{queues}\}}$.

The chain is stable (Definition 3.1) if, from every transient state, it enters a closed communicating class with probability one, and every state of a closed communicating class is positive recurrent. The stability region $C_\pi$ of a policy is the set of rate vectors $a$ for which the system is stable under $\pi$; the stability region of the system is $C=\bigcup_{\pi\in H}C_\pi$.

A family $f=(f_{ij})\ge0$ is an $a$-admissible flow if it satisfies flow conservation, $a_{lj}=\sum_{q(i)=l}f_{ij}-\sum_{h(i)=l}f_{ij}$ at every queue; $\hat f_i=\sum_jf_{ij}$ is its total flow through server $i$. With $\mathrm{co}(S)$ the convex hull of the indicator vectors of the activation sets,

$$C'=\{a\ge0:\ \exists f\in F_a,\ c\in\mathrm{co}(S),\ m_i^{-1}\hat f_i<c_i\text{ if }\hat f_i>0,\ \hat f_i=0\text{ if }c_i=0\}.$$

Formalization targets

Goal: Theorem 3.2

$$C'\subset C\subset\bar C',\qquad C'\subset C_{\pi_0}\subset C\subset\bar C_{\pi_0}.$$

The system stability region is pinned between $C'$ and its closure, and policy $\pi_0$, whatever its tie-breaking, stabilizes every rate vector in $C'$. Inclusions are not strict.

Milestones

1. Lemma A.1: $\mathrm{co}(S)$ is closed under $0\le a\le c$ (under C.1).
2. Lemma 3.1: $\bar C'=\{a:\exists f\in F_a,\ c\in\mathrm{co}(S),\ M^{-1}\hat f\le c\}$.
3. Theorem 3.1: a function bounded below with drift $\le-\epsilon$ outside a finite set, and finite conditional expectation on it, makes a countable chain stable in the sense of Definition 3.1.
4. (A.6)–(A.7): for $V(x)=\sum_{l,j}x_{lj}^2$, the one-step drift under $\pi_0$ is finite everywhere and below $-\epsilon$ once $V(x)\ge b$.
5. Lemma 3.2: $C'\subset C_{\pi_0}$.
6. Lemma 3.3: for $a\notin\bar C'$, the system is unstable under every policy in $H$.

An optional item states the claim of Remark 1: if $a\in\bar C'\setminus C'$, then $\delta a\notin\bar C'$ for every $\delta>1$.

Significance

Theorem 3.2 shows that a throughput-optimal stationary policy exists, which is not obvious: stability regions of different policies need not be nested, so a policy whose region contains all the others has to be exhibited. It also describes the system stability region by a deterministic flow condition, $C'$, which can be checked without simulating any policy. The same drift argument underlies the stability proofs of max-weight switch schedulers, back-pressure routing and the drift-plus-penalty method.

The result is proved in the paper, with a proof sketched in places (Theorem 3.1 is called "a trivial extension of Foster's criteria", Lemma A.1 is omitted, Lemma 3.3 is argued by ergodicity in a paragraph). As far as a search of the platform shows, none of these statements has a machine-checked proof: Foster's criterion is posed on the platform only for irreducible chains on $\mathbb N$, and the back-pressure results already posed concern fluid models of other networks. A complete formal development would supply the reducible-chain Foster criterion, the convex-geometry lemma on $\mathrm{co}(S)$, the quadratic drift computation and the ergodic converse.

Difficulty

The obvious argument is a quadratic Lyapunov drift bound, but it does not go through as is in three places. First, the drift bound needs a direction of decrease from every large state: the largest queue must be connected to a destination through servers that can actually be activated, which is where assumption C.2 and the topology of $S$ enter (A.21)–(A.24). Second, stage 3 of $\pi_0$ defers some activations to respect the rule "no service for nonexisting customers", so the chosen schedule is not exactly maximum-weight and the loss has to be bounded uniformly. Third, the chain is in general reducible, so Foster's criterion for irreducible chains does not apply; the extension must show that every closed class meets the finite exceptional set and that transient states are left almost surely. The converse, Lemma 3.3, needs a law-of-large-numbers argument for an arbitrary stationary rule on a positive recurrent class, together with compactness of acyclic flows (Lemma 3.1).

Formalization scope

Nodes, servers and classes are Fin L, Fin N, Fin J (0-based). $S$ is a Set (Finset (Fin N)); a queue is a pair $(l,j)$ with $l\notin V_j$, and a state is a function from queues to $\mathbb N$. A multiclass activation vector assigns to each server an optional class. The transition matrix of the queue-length chain is written out explicitly as a sum over arrival vectors and Bernoulli service outcomes; Definition 3.1 is stated through this matrix (first-entry probabilities, essential states, positive recurrence), with values in $[0,\infty]$.

Conventions committed to, and hypotheses added relative to the page:

• Standing assumptions of the goal: C.1; $\emptyset\in S$ (the idle schedule is always allowed); $0<m_i\le1$; and C.2 in a topological form, a chain of servers from every non-destination node of class $j$ to $V_j$ (stronger than the printed sentence, which covers only nodes that class $j$ can reach).
• Every single server is an activation set, $\{i\}\in S$. The proof of Lemma 3.2 uses this at (A.24) without stating it; without it a server that can never be activated breaks the drift bound and Lemma 3.2.
• Stability regions quantify over laws. $C_\pi$ is the set of nonnegative rate vectors for which the chain is stable for every arrival law with finite second moments and those means. $C'$ is intersected with $a\ge0$.
• $\pi_0$ is a family. Statements hold for every rule satisfying the three stages, with arbitrary tie-breaking.
• Expectations of unbounded functions are real series with explicit summability, so a divergent expectation is never read as $0$.

A formalization in which $C_\pi$ asks for stability under one convenient arrival law, or in which negative rates are admitted, or in which $\pi_0$ is one fixed tie-break, would be a different theorem; the definitions rule each of these out.

Infrastructure needed: hitting probabilities and positive recurrence for countable chains (reusable beyond this mission), convex hulls of finite point sets, a cycle-cancelling bound for multicommodity flows, and the ergodic theorem for positive recurrent chains. Proofs of any milestone, and reusable lemmas on countable Markov chains, are welcome.

Selected references

• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Trans. Automat. Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3):355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• N. McKeown, A. Mekkittikul, V. Anantharam and J. Walrand, Achieving 100% throughput in an input-queued switch, IEEE Trans. Commun. 47(8):1260–1267, 1999. https://doi.org/10.1109/26.780463
• L. Georgiadis, M. J. Neely and L. Tassiulas, Resource allocation and cross-layer control in wireless networks, Found. Trends Netw. 1(1):1–144, 2006. https://doi.org/10.1561/1300000001

Motivation

A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class $k$ incurs a linear delay cost $c_k$ per unit of waiting time and needs mean service time $1/\mu_k$, the classical $c\mu$ rule (serve the waiting class with the largest $c_k\mu_k$) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the $c\mu$ rule is no longer optimal.

Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized $c\mu$ rule: with nondecreasing convex delay costs $C_k$ and marginal costs $c_k = C_k'$, serve the class with the largest index $\mu_k c_k(\cdot)$ evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.

Setting

There are $d$ job classes. In the $n$th system, the $i$th class-$k$ job arrives after an interarrival time $u^n_{k,i}>0$ and needs service $v^n_{k,i}\ge 0$. $A^n_k(t)$ counts class-$k$ arrivals in $[0,t]$ and $S^n_k(x)$ counts class-$k$ completions within $x$ units of server time. A policy is an allocation $T^n=(T^n_k)$, where $T^n_k(t)$ is the time in $[0,t]$ spent on class $k$. From it come the headcount $N^n_k = A^n_k - S^n_k\circ T^n_k$, the workload $W^n_k(t) = V^n_k(A^n_k(t)) - T^n_k(t)$ (work present in class $k$), the class-FIFO delay $\tau^n_k(t)=\inf\{s\ge0: W^n_k(t)\le T^n_k(t+s)-T^n_k(t)\}$ of a job arriving at $t$, and the cumulative cost $J^n(t)=\sum_k\sum_{i\le A^n_k(t)} C^n_k(\tau^n_{k,i})$. Feasible policies are continuous, nondecreasing and work conserving.

The $n$th system runs on $[0,n]$ and is studied at the diffusion scale: $\tilde W^n_k(t)=W^n_k(nt)/\sqrt n$, $\tilde N^n_k$, $\tilde\tau^n_k$ likewise, and $\tilde J^n(t)=J^n(nt)/n$. Arrival and service processes expand as $A^n(nt)=n\bar A^n(t)+\sqrt n\,\tilde A^n(t)+o(\sqrt n)$ and $S^n(nt)=n\bar S^n(t)+\sqrt n\,\tilde S^n(t)+o(\sqrt n)$. Assumption 1 asks that these terms converge, with rates $\lambda=\bar A^{*\prime}>0$, $\mu=\bar S^{*\prime}>0$, and that the system is in heavy traffic: $\sqrt n(R^n_+-e)\to\tilde c^*$, where $R^n_k=(\bar S^n_k)^{-1}\circ\bar A^n_k$ and $\rho_k=\lambda_k/\mu_k$ is the traffic intensity. Assumption 2 asks that the costs scale, $C^n(\sqrt n\,\cdot)\to C^*(\cdot)$, and Assumption 3 that $C^*$ be strictly convex and $\mathcal C^1$.

The scaled total workload has a policy-independent limit $\tilde W^*_+=\varphi(\tilde L^*_++\tilde c^*)$, with $\varphi$ the one-dimensional reflection map. The key static problem splits a total $y$ among classes:

$$g\circ y(t)=\arg\min_{x\in\mathbb R^d_+,\ \sum_k x_k=y(t)}\ \sum_k\lambda_k(t)\,C^*_k\Big(\frac{x_k}{\rho_k(t)}\Big). \tag{43}$$

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

$$\max_{k,l}\Big\|\mu_kc^*_k\Big(\frac{\tilde W^n_k}{\rho_k}\Big)-\mu_lc^*_l\Big(\frac{\tilde W^n_l}{\rho_l}\Big)\Big\|\to0, \tag{51}$$

the costs and delays converge,

$$\tilde J^n\to\tilde J^*=\sum_k\int\lambda_kC^*_k\Big(\frac{[g\circ\tilde W^*_+]_k}{\rho_k}\Big)dt,\qquad \tilde\tau^n\to\frac{g\circ\tilde W^*_+}{\rho}. \tag{52–53}$$

Milestones

Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 ($\mu_k\tilde W^n_k-\tilde N^n_k\to0$); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of $g$ (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound

$$\liminf_n\tilde J^n(t)\ge\tilde J^*(t)\qquad\text{for every feasible policy sequence.}\tag{44}$$

Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.

Significance

The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the $c\mu$ rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.

Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of $\mu$. No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.

Difficulty

The obvious route is to show that $\tilde W^n$ converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of $\tilde W^n$ and must instead compare the cost of an arbitrary split of $\tilde W^n_+$ with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of $\tilde W^n$ must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of $\tilde T^n$ over windows of length $O(n^{-1/2})$, and cost convergence needs the convergence of the costs $C^n$ applied to delays of order $\sqrt n$.

Formalization scope

Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:

• Classes are Fin d; job indices start at $1$; every "→" between functions is uniform convergence ((11)), on $[0,1]$ unless stated; $\liminf$ is written as "eventually $\ge$ bound $-\varepsilon$".
• The scaled processes are defined exactly, with $\bar T^n=\bar L^n=R^n$ ((69), (75)); the inverse in (14) is the generalized inverse on $[0,1]$.
• The $o(n^{1/2})$ terms of (12)–(13) are uniform in $t$. The trends converge in $\mathcal C^1$, not only in $\mathcal C$. Without this, $\bar A^n,\bar S^n$ can oscillate on the $n^{-1/2}$ scale and (33)–(34) and Proposition 3 fail. The service expansion holds on server time $[0,2n]$, so that for $d=1$ in heavy traffic the service times of jobs arriving before $n$ are covered.
• $\mu_k$ in (20), (36), (41), (46)–(51) is $\mu_k(R^*_k(t))$, the service rate in real time, so $\rho_k=\lambda_k/\mu_k(R^*_k)$.
• (38) is uniform on compacts. Assumption 3's interior clause is imposed where $\tilde W^*_+(t)>0$. At $\tilde W^*_+(t)=0$ no point of $\Omega=\{0\}$ is interior, and the literal clause would make the goal vacuous.
• For the heavy-traffic limit and goal, feasible policies satisfy F1 (without adaptedness), F2–F4, $W_k\ge0$, work conservation (used by $W^n_+=\varphi(X^n)$), and every job finishes. Proposition 6 uses a broader cost-admissible class that permits idleness with work waiting. Class-FIFO is built into the delay (9).
• The delays of jobs arriving near the horizon depend on post-horizon service. We require the allocation on every bounded diffusion-scale window after $n$ to advance at the first-order rates $\rho_k(1)$. This explicit boundary hypothesis keeps Propositions 2, 4, 5, and 7 on the paper's full $[0,1]$.
• Lemma 1 additionally assumes a common Lipschitz bound on the first-order partial-sum trends. Uniform convergence alone permits jumps of order $\sqrt n$; the bound repairs that omission. Uniqueness of the solution of (43) is stated under strict convexity: "convex increasing" (p. 820) does not give it. (35) is stated without the implication from $\tilde\tau^n$ back to $\tilde W^n$, which fails in the uniform topology.
• $\tilde J^*$ integrates the optimal value of (43), so Proposition 6 needs no choice of minimizer.

A trivializing formalization is ruled out: no theorem assumes the convergence of $\tilde W^n$ or $\tilde W^n_+$, the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for $d=1$.

Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform $o(\sqrt n)$ errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.

Selected references

• J. A. Van Mieghem, Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule, Ann. Appl. Probab. 5(3) (1995) 809–833. https://doi.org/10.1214/aoap/1177004706
• C. Buyukkoc, P. Varaiya, J. Walrand, The cμ rule revisited, Adv. Appl. Probab. 17 (1985) 237–238.
• J. M. Harrison, Brownian Motion and Stochastic Flow Systems, Wiley, 1985 (reflection map).
• D. L. Iglehart, W. Whitt, Multiple channel queues in heavy traffic. I, Adv. Appl. Probab. 2 (1970) 150–177.
• A. Mandelbaum, A. L. Stolyar, Scheduling flexible servers with convex delay costs: heavy-traffic optimality of the generalized cμ-rule, Oper. Res. 52(6) (2004) 836–855. https://doi.org/10.1287/opre.1040.0156

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$, $j\in\mathbb Z$, be independent, identically distributed random variables in $[0,1]$. The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$. Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$, moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$. The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$.

Fix $\theta>1$ and $0<\gamma<1$. Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$. Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$. A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$, with $T_j=\infty$ if it never does. For $b>0$, $\log_b x$ means the logarithm in base $b$, and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

$$\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.$$

When $\gamma\theta>1$, the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

$$\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.$$

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$. The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$.

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$, then

$$\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.$$

The second clause describes the supercritical case. If $\gamma\theta>1$, $n_k\to\infty$, and $\{\log_\theta n_k\}\to\varepsilon$, then for each $x>0$,

$$P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).$$

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$; the two passage-time results use base $1/\gamma$, exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$. The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$, their accumulation produces a logarithmic correction; at $\gamma\theta>1$, the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$, $0<\gamma<1$, $\gamma\theta\ge1$. The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$.

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

• Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

Motivation

Nonparametric regression estimates the conditional mean $E(Y\mid X=x)$ of a real response $Y$ given a predictor $X\in\mathbb R^d$ without assuming that it belongs to a finite-dimensional family. Most practical estimators of this kind are local averages: kernel estimators (Nadaraya 1964, Watson 1964), nearest-neighbor rules (Cover and Hart 1967), and their many variants all predict at a point $X$ by a weighted average $\sum_i W_{ni}(X)Y_i$ of the observed responses, with weights that depend only on the predictors.

C. J. Stone's 1977 paper in the Annals of Statistics (DOI 10.1214/aos/1176343886) asked when such a rule is consistent: when it converges to the true regression function in $L^r$ for every joint distribution of $(X,Y)$ with $E|Y|^r<\infty$, without smoothness or moment assumptions beyond that. Its Theorem 1 answers the question in terms of five conditions on the weights alone. The result is the standard starting point for distribution-free regression theory; it is the first theorem of the monograph of Györfi, Kohler, Krzyżak and Walk (2002), where it is called Stone's theorem, and it underlies the universal consistency of nearest-neighbor, kernel and partitioning estimates.

Setting

Let $\mu$ be a probability measure on $\mathbb R^d$ and let $X, X_1, X_2,\dots$ be independent with law $\mu$. A sequence of weights $\{W_n\}$ assigns to each $n\ge1$ and each point $(x,x_1,\dots,x_n)$ real numbers

$$W_{ni}(x) = W_{ni}(x, x_1,\dots,x_n),\qquad 1\le i\le n .$$

The weights are nonnegative if every $W_{ni}\ge0$ and probability weights if in addition $\sum_i W_{ni}(x)=1$.

When $(X,Y),(X_1,Y_1),(X_2,Y_2),\dots$ are i.i.d. with $Y$ real valued, the estimate of $E(Y\mid X)$ is

$$\hat E_n(Y\mid X) = \sum_{i=1}^n W_{ni}(X)\,Y_i .$$

The sequence $\{W_n\}$ is consistent if, for every such joint distribution with $X$-marginal $\mu$ and every $r\ge1$ with $E|Y|^r<\infty$,

$$\lim_{n\to\infty} E\big|\hat E_n(Y\mid X) - E(Y\mid X)\big|^r = 0 .$$

The five conditions of Theorem 1 are:

1. there is a $C\ge1$ with $E\sum_i|W_{ni}(X)|f(X_i)\le C\,Ef(X)$ for every nonnegative Borel $f$ and every $n\ge1$;
2. there is a $D\ge1$ with $P\big(\sum_i|W_{ni}(X)|\le D\big)=1$ for every $n\ge1$;
3. $\sum_i|W_{ni}(X)|\,I_{\{\|X_i-X\|>a\}}\to0$ in probability for every $a>0$;
4. $\sum_i W_{ni}(X)\to1$ in probability;
5. $\max_i|W_{ni}(X)|\to0$ in probability.

Formalization targets

Goal: Theorem 1 (p. 598)

$$\text{(1)–(5)}\ \Longrightarrow\ \{W_n\}\text{ consistent},$$

and conversely, if $\{W_n\}$ is consistent, then (4) and (5) hold; if moreover $W_n\ge0$ for all $n\ge1$, then (3) holds; and if $W_n\ge0$ and (2) holds, then (1) holds. The goal is the full theorem, both directions, as one statement.

Milestones (§10, pp. 607–610)

• Proposition 1: under (1)–(3), $E\sum_i|W_{ni}(X)||f(X_i)-f(X)|^r\to0$ whenever $r\ge1$ and $E|f(X)|^r<\infty$.
• Propositions 2 and 3: for nonnegative weights (respectively for $W_{ni}^2$), bounds on $\liminf$ and $\limsup$ of $E\sum_i W_{ni}(X)f(X_i)$ in terms of constants $M_n\le\sum_i W_{ni}(X)\le N_n$ holding with probability tending to one.
• Proposition 5: under (1)–(4), $\sum_i W_{ni}(X)f(X_i)\to f(X)$ in $L^r$.
• Proposition 6: nonnegative weights that reproduce every bounded continuous $f$ in probability satisfy (3).
• Proposition 7: if $\limsup_n E\sum_i W_{ni}(X)f(X_i)<\infty$ for every integrable nonnegative $f$, a single pair $(n_0, C)$ works for all $f$.
• Proposition 8: if $\sum_i W_{ni}(X)Y_i\to0$ in probability for independent standard normal $Y_i$, then $\sum_i W^2_{ni}(X)\to0$ in probability.

Significance

The result. Theorem 1 reduces a statement about all joint distributions of $(X,Y)$ to properties of the weights under the law of $X$ alone. For probability weights, conditions (2) and (4) hold automatically, and (1), (3), (5) become necessary and sufficient (Corollary 1). This is how Stone proves that nearest-neighbor weights with suitably vanishing coefficients are universally consistent (Theorem 2 of the paper), and how consistency transfers to estimators of conditional quantiles and to approximate Bayes rules in classification and decision problems (Sections 7–8). Condition (1), the only condition that is not a convergence statement, is the one that later work on kernel and partitioning estimates had to verify by geometric covering arguments.

Formalizing it. The theorem is proved in the paper and in textbooks; it has no machine-checked proof that we know of. A formalization produces a reusable criterion: any later development of local-averaging estimators can discharge consistency by checking five conditions about the predictor distribution. The supporting propositions are of independent use: Proposition 1 is an $L^r$ approximation lemma for weighted empirical averages, and Proposition 7 is a uniform-boundedness principle for sequences of positive operators on $L^1(\mu)$.

Difficulty

The sufficiency half combines three ingredients that have to fit together at the level of measure theory: approximation of an arbitrary $L^r$ function by continuous functions with compact support, uniformly over $n$ through condition (1); a variance computation for the noise term that conditions on the predictors; and a truncation argument to pass from bounded responses and $r=2$ to all $r\ge1$. The natural first idea, to apply a weak law of large numbers to $\sum_i W_{ni}(X)Y_i$, fails because the weights are dependent on all of $X, X_1,\dots,X_n$ and are not identically distributed.

The necessity half needs separate arguments for each condition: a test-function argument with bounded continuous $f$ for (3), a contradiction argument summing a sequence of functions $f_\nu$ for (1), and a Gaussian anti-concentration argument for (5), which is where the auxiliary normal variables of the paper enter.

Formalization scope

• Data. The i.i.d. sequence $X, X_1, X_2,\dots$ is the coordinate process of the product measure $\mu^{\otimes\mathbb N}$ on $(\mathbb R^d)^{\mathbb N}$, coordinate $0$ being $X$. "Whenever $(X,Y),(X_1,Y_1),\dots$ are i.i.d." is encoded by quantifying over every Markov kernel $\kappa$ from $\mathbb R^d$ to $\mathbb R$ (the conditional law of $Y$ given $X$); the pairs are the coordinates of $(\mu\otimes\kappa)^{\otimes\mathbb N}$ and $E(Y\mid X=x)=\int y\,\kappa(x,dy)$. Every joint law with $X$-marginal $\mu$ arises in this way.
• Standing assumptions. The paper's assumption (p. 596) that independent standard normal variables are available on the probability space is supplied by the kernel $\kappa\equiv N(0,1)$. The weights are assumed jointly Borel in $(x,x_1,\dots,x_n)$; the paper treats $W_{ni}(X)$ as random variables without saying so.
• Conventions. Expectations of nonnegative quantities (in (1), in $E|Y|^r$, in the $L^r$ distances and in Propositions 1–3, 5, 7) are lower Lebesgue integrals in $[0,\infty]$, and the $\liminf$/$\limsup$ of Propositions 2, 3, 7 are in $[0,\infty]$, so no infinite expectation is silently read as $0$. Convergence in probability is Mathlib's TendstoInMeasure. Sample indices are $0$-based. Conditions on individual $n$ are stated for $n\ge1$.
• Correction of the print. The definition of consistency on p. 597 prints "$r>1$"; the proof of Theorem 1 (p. 611, (13)) and the rest of the paper work with every $r\ge1$, which is the formalized reading.
• Not a trivialization. The goal quantifies over every conditional law $\kappa$ and every real $r\ge1$; a version for bounded $Y$ or for $r=2$ only would be weaker than the theorem, and the converse parts conclude the conditions (1), (3), (4), (5) themselves.
• Infrastructure. A complete development needs products of probability measures and their coordinate processes, Lusin-type density of compactly supported continuous functions in $L^r(\mu)$, conditional variance computations given finitely many coordinates, and the Gaussian tail bound. These pieces are reusable well beyond this mission. Proofs of individual propositions, and of either direction of Theorem 1 separately, are welcome contributions.

Selected references

• C. J. Stone, Consistent nonparametric regression, Ann. Statist. 5(4), 595–645, 1977. https://doi.org/10.1214/aos/1176343886
• L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
• T. M. Cover, P. E. Hart, Nearest neighbor pattern classification, IEEE Trans. Inform. Theory 13(1), 21–27, 1967. https://doi.org/10.1109/TIT.1967.1053964
• E. A. Nadaraya, On estimating regression, Theory Probab. Appl. 9(1), 141–142, 1964. https://doi.org/10.1137/1109020
• G. S. Watson, Smooth regression analysis, Sankhyā Ser. A 26(4), 359–372, 1964. https://www.jstor.org/stable/25049340