Probability

Motivation

Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.

The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.

The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.

Setting

Capacity allocation (§4.1). A network has $J \ge 1$ channels. Channel $j$ receives traffic at average rate $a_j > 0$ and is given capacity $\phi_j$. In equilibrium the number $n_j$ of messages at channel $j$ has the geometric law (4.1),

$$P(n_j = n) = \Big(1 - \frac{a_j}{\phi_j}\Big)\Big(\frac{a_j}{\phi_j}\Big)^n, \qquad n = 0, 1, 2, \dots,$$

which requires $\phi_j > a_j$. Its mean is $a_j/(\phi_j - a_j)$. Capacity on channel $j$ costs $f_j > 0$ per unit and the total budget is $F$, giving the cost constraint (4.2)

$$\sum_j f_j\phi_j = F.$$

The mean number of customers in the network is

$$N(\phi) = \sum_j \frac{a_j}{\phi_j - a_j},$$

and the feasible set is the set of $\phi \in \mathbb{R}^J$ with $\phi_j > a_j$ for every $j$ that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ $= N(\phi) + y(\sum_j f_j\phi_j - F)$.

Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate $\nu > 0$ at a system of $J$ compartments that is empty at time $0$. Let $p_j(s)$ be the probability that an individual is in compartment $j$ a time $s$ after its arrival; $p_j(s) \ge 0$ and $\sum_j p_j(s) \le 1$, since individuals may leave. Let $n_j(t)$ be the number of individuals in compartment $j$ at time $t > 0$, and

$$\alpha_j(t) = \int_0^t p_j(u)\,du.$$

In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and $\alpha_j(t)$ is alpha p j t.

Formalization targets

Goal: Theorem 4.1 (p. 97)

If $J \ge 1$, $a_j > 0$, $f_j > 0$ and $F > \sum_k a_k f_k$, then

$$\phi^*_j = a_j + \frac{\sqrt{a_j f_j}}{\sum_k \sqrt{a_k f_k}}\cdot\frac{F - \sum_k a_k f_k}{f_j}$$

is feasible and minimizes $N$ over the feasible set, and every other feasible $\phi$ has $N(\phi) > N(\phi^*)$.

Milestones toward the goal

1. The mean of the geometric law (4.1) is $a_j/(\phi_j - a_j)$ (p. 97).
2. For $y > 0$ the Lagrangian is minimized over $\{\phi_j > a_j\}$ by $\phi_j = a_j + \sqrt{a_j/(y f_j)}$ (proof of Theorem 4.1).
3. The choice $1/\sqrt y = (F - \sum_k a_k f_k)/\sum_k\sqrt{a_k f_k}$ makes that minimizer equal to $\phi^*$ and feasible for (4.2).

Second result: Theorem 4.2 (pp. 114–115)

The proof's generating-function identity, for $z_j \in [0,1]$,

$$E\big(z_1^{n_1(t)}\cdots z_J^{n_J(t)}\big) = \prod_{j=1}^J \exp\big[-(1 - z_j)\nu\alpha_j(t)\big],$$

and the theorem itself: $n_1(t), \dots, n_J(t)$ are independent and $n_j(t)$ is Poisson with mean $\nu\alpha_j(t)$.

Significance

Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity $a_j$ needed to carry its traffic; the remaining budget is shared in proportion to $\sqrt{a_j f_j}$, not to the traffic $a_j$. Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.

Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting $t \to \infty$ it recovers the equilibrium Poisson law of §4.5.

Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in $\mathbb{R}^J$. For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.

Difficulty

For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that $L$ is (strictly) convex on the open region $\phi_j > a_j$, and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of $\phi^*$ needs $F > \sum_k a_k f_k$, which the book leaves implicit.

For Theorem 4.2, the steps of the proof that read "conditional on $M$" have to be carried out with measure-theoretic independence. One step averages a product over $M$ independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of $J$ counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.

Formalization scope

Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.

Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: $J \ge 1$, $a_j > 0$, $f_j > 0$, $F > \sum_k a_k f_k$. Stability $\phi_j > a_j$ is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of $\phi^*$, plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that $\phi^*$ satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.

Theorem 4.2. The model is pinned down as in the proof on p. 115:

• the number $M$ of arrivals in $(0,t)$ is Poisson with mean $\nu t$;
• an i.i.d. sequence of (arrival instant, location at time $t$) pairs is independent of $M$, and only its first $M$ entries are used;
• each instant is uniform on $(0,t)$, and an individual arriving at $u$ is in compartment $j$ at time $t$ with probability $p_j(t-u)$, or has left.

"Individuals move independently" is formalized as this conditional independence. The $p_j$ are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the $J$ counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.

Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for $\mathbb{N}^J$-valued random vectors.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 4 (§4.1, pp. 95–97; §4.5, pp. 113–115).
• L. Kleinrock, Communication Nets: Stochastic Message Flow and Delay, McGraw-Hill, 1964 (reprinted Dover, 1972).
• J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (colouring and marking theorems).

Motivation

Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.

Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served $K$-server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).

Setting

There are $I$ customer types and $J$ queues. Customers of type $i$ enter the system in a Poisson stream of rate $\nu(i)>0$ and visit the queues $r(i,1),r(i,2),\dots,r(i,S(i))$ in that order before leaving; two successive stages of a route are at different queues.

Queue $j$ holds its $n_j$ customers in positions $1,\dots,n_j$. Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate $\phi_j(n_j)$, with $\phi_j(n)>0$ for $n>0$; a proportion $\gamma_j(l,n_j)$ goes to the customer in position $l$. An arriving customer takes position $l$ with probability $\delta_j(l,n_j+1)$. For each $n\ge1$, $\gamma_j(\cdot,n)$ and $\delta_j(\cdot,n)$ are probability vectors on $\{1,\dots,n\}$.

The class of the customer in position $l$ of queue $j$ is $c_j(l)=(t_j(l),s_j(l))$, his type and the stage of his route. The state of queue $j$ is $\mathbf c_j=(c_j(1),\dots,c_j(n_j))$ and the state of the network is $\mathbf C=(\mathbf c_1,\dots,\mathbf c_J)$. Its transition rates $q(\mathbf C,\mathbf D)$, displays (3.1)–(3.6), are the sums of the intensities of all events taking $\mathbf C$ to $\mathbf D$: a departure from the system (intensity $\phi_j(n_j)\gamma_j(l,n_j)$), a move from position $l$ of queue $j$ to position $m$ of the next queue $k$ (intensity $\phi_j(n_j)\gamma_j(l,n_j)\delta_k(m,n_k+1)$), and an arrival into position $m$ of the first queue $k$ of a route (intensity $\nu(i)\delta_k(m,n_k+1)$).

With $\alpha_j(i,s)=\nu(i)$ if $r(i,s)=j$ and $0$ otherwise, set

$$a_j=\sum_{i,s}\alpha_j(i,s),\qquad b_j^{-1}=\sum_{n=0}^{\infty}\frac{a_j^n}{\prod_{l=1}^{n}\phi_j(l)},\qquad \pi_j(\mathbf c_j)=b_j\prod_{l=1}^{n_j}\frac{\alpha_j(t_j(l),s_j(l))}{\phi_j(l)}.$$

Formalization targets

Goal: Theorem 3.1 (p. 61)

If every series defining $b_j^{-1}$ converges, then

$$\pi(\mathbf C)=\prod_{j=1}^{J}\pi_j(\mathbf c_j)$$

is positive, sums to $1$ over all network states, and satisfies the equilibrium equations

$$\pi(\mathbf C)\sum_{\mathbf D}q(\mathbf C,\mathbf D)=\sum_{\mathbf D}\pi(\mathbf D)\,q(\mathbf D,\mathbf C)\quad\text{for every }\mathbf C.$$

Milestones

• Theorem 3.2 (p. 62). The time-reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ are the rates of the reversed network: routes traversed backwards, $\gamma_j$ and $\delta_j$ interchanged.
• Corollary 3.4 (p. 63). Queue $j$ is independent of the rest of the network, is in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$, holds $n$ customers with probability $b_ja_j^n/\prod_{l=1}^n\phi_j(l)$ (3.7), and a customer in position $l$ is of class $(i,s)$ with probability $\alpha_j(i,s)/a_j$.
• Corollary 3.5 (p. 63). A type-$i$ customer reaching queue $j$ at stage $s$ finds it in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$.
• Lemma 3.13 (p. 89). For a multiclass queue with Poisson arrivals of rate $\nu(c)$ and departure intensities $\nu(c)\phi_c(\mathbf n)$: reversible $\Leftrightarrow$ quasi-reversible $\Leftrightarrow$ $\Phi(\mathbf n)=\phi_c(\mathbf n)\Phi(\mathbf n-\mathbf e_c)$ for some positive $\Phi$ (3.26).

Significance

Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate $a_j$, even though the actual arrival stream at queue $j$ is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).

The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.

Difficulty

The obvious first attempt, detailed balance, fails: $\pi(\mathbf C)q(\mathbf C,\mathbf D)$ and $\pi(\mathbf D)q(\mathbf D,\mathbf C)$ differ in general, because a customer's route cannot be run backwards inside the same network ($q(\mathbf D,\mathbf C)$ is usually $0$ when $q(\mathbf C,\mathbf D)>0$). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of $J$-tuples of lists, reorganized by queue length together with the identity $\sum_{\text{classes at } j}\alpha_j=a_j$.

Formalization scope

• Finite types and queues. Types are Fin I, queues Fin J; the book allows countably many types with $\sum_i\nu(i)<\infty$. A network state is a function assigning to each queue a list of classes $(i,s)$ with $r(i,s)=j$; the state space is countable and all sums over it are tsum/HasSum.
• Indexing. Stages and list positions are $0$-based in Lean; $\gamma_j(l,n)$ and $\delta_j(l,n)$ keep the book's $1$-based position argument.
• Rate level. Equilibrium means: positive, summing to $1$, and satisfying the equilibrium equations (the published KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).
• Normalizing constants. $b_j$ is defined through a tsum, which Lean sets to $0$ for a divergent series; every theorem assumes the series converges, the book's "none of $b_1,\dots,b_J$ is zero".
• No trivial instance. The goal holds for arbitrary $I$, $J$, $\nu$, routes, $\phi_j$, $\gamma_j$, $\delta_j$ subject only to the book's constraints; a proof for a single queue, or for fixed $\gamma=\delta$ disciplines, does not prove it. In Lemma 3.13 the function $\Phi$ is required to be positive, since $\Phi\equiv0$ satisfies (3.26) for every queue.

Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over $\prod_j \mathrm{List}(\cdot)$, and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://doi.org/10.2307/3212785
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Jobshop-like queueing systems, Management Science 10 (1963), 131–142. https://doi.org/10.1287/mnsc.10.1.131
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Why symmetric queues

The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.

Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.

Setting

A symmetric queue holds customers in positions $1, 2, \dots, n$, where $n$ is the number present. It operates as follows (Kelly, p. 72):

1. the service requirement of a customer is a random variable whose distribution may depend on the class of the customer;
2. a total service effort is supplied at rate $\phi(n)$, with $\phi(n) > 0$ for $n > 0$;
3. a proportion $\gamma(l, n)$ of this effort, $\sum_{l=1}^n \gamma(l, n) = 1$, goes to the customer in position $l$; when he leaves, the customers in positions $l+1, \dots, n$ move down by one;
4. an arriving customer moves into position $l \in \{1, \dots, n+1\}$ with probability $\gamma(l, n+1)$ — the same function — and the customers in positions $l, \dots, n$ move up by one.

Server-sharing ($\gamma(l, n) = 1/n$), the stack ($\gamma(n, n) = 1$, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).

Customers of class $c$ arrive in a Poisson stream of rate $\nu(c)$. On arrival a class-$c$ customer receives a refined class $(c, z)$ with probability $p(c, z)$, $\sum_z p(c, z) = 1$, and then needs $w(c, z) \ge 1$ independent stages of service, each exponentially distributed with mean $d(c, z) > 0$. The class-$c$ service requirement is therefore a mixture of gamma distributions with mean

$$a(c) = \sum_z p(c, z)\, w(c, z)\, d(c, z),$$

and the work arriving per unit time is $a = \sum_c \nu(c) a(c)$. The record of the customer in position $l$ is $\mathbf c(l) = (c(l), z(l), u(l))$, $u(l)$ the stage in progress, and $\mathbf c = (\mathbf c(1), \dots, \mathbf c(n))$ is a Markov process. Its transitions are: an arrival of class $(c,z)$ into position $l$ at stage $1$, at rate $\nu(c)p(c,z)\gamma(l, n+1)$; and, at rate $\phi(n)\gamma(l,n)/d(c(l),z(l))$, completion of the current stage of the customer in position $l$, which moves him to the next stage or, after stage $w(c(l), z(l))$, out of the queue. The normalizing constant is

$$b^{-1} = \sum_{n=0}^{\infty} \frac{a^n}{\prod_{l=1}^n \phi(l)}. \tag{3.15}$$

Formalization targets

Goal: Theorem 3.8

When (3.15) converges, the distribution

$$\pi(\mathbf c) = b \prod_{l=1}^n \frac{\nu(c(l))\, p(c(l), z(l))\, d(c(l), z(l))}{\phi(l)} \tag{3.18}$$

is the equilibrium distribution of $\mathbf c$, and under it

$$\mathbb P(n \text{ customers}) = \frac{b\,a^n}{\prod_{l=1}^n \phi(l)}, \qquad \mathbb P(\text{classes } c_1, \dots, c_n \mid n) = \prod_{l=1}^n \frac{\nu(c_l)\, a(c_l)}{a},$$

and the queue is quasi-reversible with respect to the classification $c$ and to $(c, z)$: from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).

Milestones

• Eqs. (3.14)–(3.15): the case of one refinement per class, $\pi(\mathbf c) = b\prod_l \nu(c(l))d(c(l))/\phi(l)$ with $a = \sum_c \nu(c)d(c)w(c)$.
• Eqs. (3.16)–(3.17): in that case, the law of $n$, and given $n$ independent positions of class $c$ with probability $\nu(c)d(c)w(c)/a$ and uniform stage.
• Eq. (3.18): the equilibrium distribution under gamma-mixture service.
• Lemma 3.9: mixtures of gamma distributions approximate, at continuity points, the distribution function of any positive random variable.

Significance

Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means $a(c)$. Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).

These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.

Difficulty

The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition $\gamma \equiv \delta$ is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.

Formalization scope

• The state is a List of customer records (class, refined class, stage); list index $i$ is position $l = i + 1$, and $\gamma(l, n)$, $\phi(n)$ keep the book's $1$-based indexing. The state space consists of the lists whose records have $\nu(c)p(c,z) > 0$ and $1 \le u \le w(c, z)$: records of a refined class arriving at rate zero are unreachable and excluded.
• Classes $\mathcal C$ and refinements $\mathcal Z$ are arbitrary countable types. All infinite sums are HasSum or tsum with explicit convergence hypotheses: $\sum_c \nu(c) < \infty$ (finite exit rates, the book's standing assumption of §1.1), convergence of $a(c)$, of $a$, and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.
• The statement is rate level: (3.18) is shown to satisfy the equilibrium equations of the stage process, and quasi-reversibility is its rate characterization (3.8), (3.10). That these describe the stationary process and its time reversal is the book's Chapter 1 and is not reformalized.
• Trivializing readings ruled out: the goal keeps $p$, $w$ and $d$ general (not $w \equiv 1$, which would make the result Section 3.1's exponential case); the arrival position uses the same $\gamma$ as the service split; and in Lemma 3.9 the approximants must be genuine gamma mixtures with integer shapes, which a point mass is not.
• Not planned: Theorem 3.10 (arbitrary service distributions; only an outline of proof and a continuous state space the book does not construct) and Theorem 3.11 (reversibility of the number in queue, a non-Markov process).

Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, §3.3, pp. 72–82. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://www.jstor.org/journal/japplprob
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://www.jstor.org/journal/advaapplprob
• A. D. Barbour, Networks of queues and the method of stages, Advances in Applied Probability 8 (1976), 584–591. https://www.jstor.org/journal/advaapplprob
• B. A. Sevastyanov, An ergodic theorem for Markov processes and its application to telephone systems with refusals, Theory of Probability and its Applications 2 (1957), 104–112.
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).$$

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

$$\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].$$

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

$$3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].$$

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded $q$-th moments, at the price of step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that $\sum_ne^{-c/\gamma_n}<\infty$ for every $c>0$, which allows step sizes decaying only slightly faster than $1/\log n$. The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.$$

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$. The noise is subgaussian if there is a number $\Gamma>0$ such that for all $n$ and all $\theta\in\mathbb R^d$

$$E\big(\exp\langle\theta,U_{n+1}\rangle\,\big|\,\mathcal F_n\big)\le\exp\Big(\frac\Gamma2\|\theta\|^2\Big).$$

Bounded noise, $\|U_n\|\le\sqrt\Gamma$, is an example.

Formalization targets

Goal: Proposition 4.4

For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that

$$\sum_ne^{-c/\gamma_n}<\infty\qquad\text{for each }c>0,$$

with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. The exponential supermartingale. For every $\theta\in\mathbb R^d$,

$$Z_n(\theta)=\exp\Big[\sum_{i=1}^n\langle\theta,\gamma_iU_i\rangle-\frac\Gamma2\sum_{i=1}^n\gamma_i^2\|\theta\|^2\Big]$$

is a supermartingale. 2. Directional maximal tail bound. For every unit vector $e$, $\alpha>0$, $n$ and $T>0$,

$$P\Big(\sup_{n<k\le m(\tau_n+T)}\Big\langle e,\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\rangle\ge\alpha\Big)\le\exp\Big(\frac{-\alpha^2}{2\Gamma\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2}\Big).$$

3. Eq. (18). There are $C,C'>0$ depending only on $d$ and $\Gamma$ with

$$P(\Delta(t,T)\ge\alpha)\le C\exp\Big(\frac{-\alpha^2}{C'\int_t^{t+T}\bar\gamma(s)\,ds}\Big)\qquad(t\ge0,\ T>0,\ \alpha>0).$$

4. Block comparison. $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever $\gamma_n\log n\to0$, so it admits steps that decrease far more slowly than the $\sum\gamma_n^2<\infty$ of the classical $L^2$ theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of $F$, and the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid $kT$, and the continuous-time bookkeeping of $\bar U$, $\bar\gamma$ and $\Delta$ shared with the other missions of this series.

Difficulty

The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under $\sum e^{-c/\gamma_n}<\infty$ alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation $\Delta(t,T)$ involves partial steps at both ends of $[t,t+h]$, so the bound must be stated in terms of $\int_t^{t+T}\bar\gamma$ rather than a sum over whole steps, with constants that do not depend on $t$, $T$ or $\alpha$. Finally, A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) (the paper writes $\mathbb R^m$); time is real. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ; $U_{n+1}$ is $\mathcal F_{n+1}$-strongly measurable and integrable, and $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. The subgaussian condition requires $\exp\langle\theta,U_{n+1}\rangle$ to be integrable for every $\theta$ and $n$. The summand $e^{-c/\gamma_n}$ is taken to be $0$ when $\gamma_n=0$, its limiting value. The suprema in A1 and $\Delta$ are taken in $[0,\infty]$; the supremum over an empty range of $k$ is $0$. In Eq. (18) the constants are chosen before the probability space, the algorithm and $t,T,\alpha$.

The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is $0$); a summability condition made trivial or false by the convention $c/0=0$; and the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$, $\Gamma=1$ and $\gamma_n=1/n$ satisfy every one of them.

Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997.
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979) 15–30. https://doi.org/10.1287/moor.4.1.15