All missions

Motivation

Many systems consist of a finite number of sites whose states influence one another only locally: fruit trees in an orchard that are diseased or healthy, power sources that are working or broken, individuals holding one of several views. Chapter 9 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) asks which joint distributions such systems have in equilibrium. Earlier chapters of the book produce product-form distributions in which the components are independent; spatial models instead give a limited dependence, and §9.1 makes that notion precise through Markov fields.

The central characterization, that a positive random field is Markov with respect to a graph exactly when it factorizes over the cliques of that graph, is the theorem of Hammersley and Clifford (1971, unpublished manuscript), with published proofs by Besag (1974), Grimmett (1973) and Preston (1973). It underlies Gibbs random fields in statistical mechanics, spatial statistics, image analysis and graphical models. Kelly's §§9.2–9.3 then use it to identify the equilibrium distributions of interacting-particle Markov processes ("spatial processes"), connecting it to reversibility and partial balance.

Setting

There are $J$ sites, the vertices of a finite graph $G$; $\partial j$ is the set of neighbours of site $j$ and $G-j$ the set of sites other than $j$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and a state is $\mathbf n=(n_1,\dots,n_J)$ in $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. For a set of sites $H$, $\mathbf n_H$ is the vector of attributes of the sites in $H$. The operator $T_j^m$ changes the attribute of site $j$ to $m$.

A random field is a function $\pi$ on $\mathcal S$ with $\pi(\mathbf n)>0$ for every state and $\sum_{\mathbf n}\pi(\mathbf n)=1$. The conditional probability that site $j$ has attribute $n_j$ given all other sites is

$$P(n_j\mid\mathbf n_{G-j}) = \frac{\pi(\mathbf n)}{\sum_{m\in\mathcal N_j}\pi(T_j^m\mathbf n)}. \qquad (9.1)$$

$\pi$ is a Markov field if $P(n_j\mid\mathbf n_{G-j}) = P(n_j\mid\mathbf n_{\partial j})$ for every $j$ and $\mathbf n$ (9.2): the attribute of a site depends on the rest of the system only through its neighbours. A simplex is a single site or a set of sites any two of which are neighbours; $\mathcal C$ is the set of simplices of $G$.

A spatial process is a Markov process $\mathbf n(t)$ on $\mathcal S$ with rates $q$ such that (i) only one component changes at a time, (ii) $q(\mathbf n,T_j^m\mathbf n)$ depends on $\mathbf n$ only through $n_j$ and $\mathbf n_{\partial j}$, and (iii) $T_j^m\mathbf n$ can be reached from $\mathbf n$ by transitions that do not alter $\mathbf n_{G-j}$. The general spatial process of §9.3 has rates

$$q(\mathbf n,T_j^m\mathbf n)=\lambda_j(n_j,m)\,\frac{\Phi(\mathbf n)}{\Phi_{G-j}(\mathbf n_{G-j})} \qquad (9.15)$$

for positive functions $\Phi$, $\Phi_{G-j}$.

Formalization targets

Goal: Theorem 9.2 (p. 186)

A random field $\pi$ is a Markov field if and only if

$$\pi(\mathbf n) = B\prod_{C\in\mathcal C}\phi_C(\mathbf n_C), \qquad \mathbf n\in\mathcal S, \qquad (9.5)$$

for some constant $B$ and functions $\phi_C$.

Milestones

• Lemma 9.1 (p. 185): the conditional probabilities $P(n_j\mid\mathbf n_{G-j})$, $j\in G$, $\mathbf n\in\mathcal S$, determine the random field uniquely.
• Theorem 9.3 (p. 189): the equilibrium distribution of a reversible spatial process is a Markov field.
• Theorem 9.4 (p. 193): for the rates (9.15), with $\alpha_j>0$ solving $\alpha_j(n)\sum_m\lambda_j(n,m)=\sum_m\alpha_j(m)\lambda_j(m,n)$ (9.16), the equilibrium distribution is

$$\pi(\mathbf n) = B\,\frac{\prod_{j=1}^J\alpha_j(n_j)}{\Phi(\mathbf n)}, \qquad (9.17)$$

and it satisfies the partial balance equations (9.18) site by site.

Significance

Theorem 9.2 turns a statement about conditional laws, which is how local interaction is usually specified, into an explicit parametrization of the joint law by clique potentials. On a lattice with binary attributes it reduces a Markov field to one parameter per site and one per pair of adjacent sites, giving the form $\pi(\mathbf n)=B\alpha^M\beta^R$ (9.9). Theorem 9.3 shows that local, reversible dynamics produce Markov-field equilibria, and Theorem 9.4 gives a family of non-reversible processes, containing the closed migration process of Chapter 2, whose equilibria are still explicit; its partial balance equations are the bridge to §9.4.

All four results are classical and proved in the book. They are not, to our knowledge, machine-checked in this discrete form. The platform has an open statement of Hammersley–Clifford in a different setting, HighDimStat.GraphicalModels.thm11_8_hammersley_clifford (Wainwright, High-Dimensional Statistics, Theorem 11.8): a random vector in $\mathbb R^V$ with a strictly positive Lebesgue density and the global (separation) Markov property. Neither statement implies the other as formalized, so this mission poses Kelly's finite, local version separately. A formal proof here also gives reusable infrastructure: conditional probabilities of a distribution on a finite product space, and factorizations over the cliques of a graph.

Difficulty

The "if" direction is routine. The "only if" direction is where the content lies: the functions $\phi_C$ must be produced from $\pi$ alone, and a product over the cliques of $G$ must reproduce $\pi$ at every state, not only at the states whose nonzero attributes sit on a single clique. The natural first idea, one factor per site read off from the conditional laws, fails as soon as two sites interact. The Markov property must also be brought from its explicit form (9.2), which involves a marginal over the non-neighbours, into a usable statement about $\pi$ itself. Strict positivity is essential: without it the "only if" direction is false (Exercise 9.2.2). For Theorem 9.3, condition (iii) cannot be dropped: Exercise 9.2.2 gives a reversible process satisfying (i) and (ii) whose equilibrium is not a Markov field, so any argument that uses only the local form of the rates fails.

Formalization scope

• Sites form an arbitrary finite type V with decidable equality; attributes at site j form a finite type N j, which may differ between sites. States are dependent functions (j : V) → N j, and $T_j^m\mathbf n$ is Function.update n j m. The graph is a Mathlib SimpleGraph V, so $\partial j$ is G.neighborSet j.
• A random field is a real function, positive at every state, with finite sum $1$. $P(n_j\mid\mathbf n_{\partial j})$ is the conditional probability computed from $\pi$ (a ratio of finite sums), so (9.2) is stated literally.
• Simplices are the nonempty cliques of the given graph $G$, including single sites. The factorization ranges over exactly these sets; a product over all subsets of sites, or over the cliques of the complete graph, would make the goal trivially true and is ruled out.
• Theorems 9.3 and 9.4 are read at the level of rates: "equilibrium distribution of a reversible process" is a positive distribution summing to one in detailed balance with $q$ (the published KellyStochasticNetworks.DetailedBalance), and "equilibrium distribution" in 9.4 is a positive distribution summing to one satisfying the equilibrium equations (KellyStochasticNetworks.FullBalance), together with its uniqueness under irreducibility. The Markov process itself is not constructed. The state space is always finite, so all sums are finite.
• Contributions welcome: proofs of any item, general lemmas on conditional laws over finite product spaces, and a formal account of the general Hammersley–Clifford theorem that both this mission and the Wainwright statement could use.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 9. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• J. Besag, Spatial interaction and the statistical analysis of lattice systems, J. Roy. Statist. Soc. B 36 (1974), 192–236. https://doi.org/10.1111/j.2517-6161.1974.tb00999.x
• G. R. Grimmett, A theorem about random fields, Bull. London Math. Soc. 5 (1973), 81–84. https://doi.org/10.1112/blms/5.1.81
• C. J. Preston, Generalized Gibbs states and Markov random fields, Adv. Appl. Probab. 5 (1973), 242–261. https://doi.org/10.2307/1426035
• M. J. Wainwright, High-Dimensional Statistics, Cambridge University Press, 2019, Theorem 11.8. https://doi.org/10.1017/9781108627771

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

Many optimization problems in statistics, signal processing and control are posed over sets of matrices with a constraint that makes them curved: matrices of fixed rank, matrices with orthonormal columns, symmetric matrices with a prescribed spectrum. Algorithms on such sets ("optimization on manifolds") compute a step in the tangent space at the current point, as in a vector space, and then need a rule that brings the point $x+u$ back to the set. A retraction is such a rule; the notion was introduced by Adler, Dedieu, Margulies, Martens and Shub for Newton's method on Riemannian manifolds (IMA J. Numer. Anal. 2002) and is the basic building block of the algorithms in Absil, Mahony and Sepulchre's monograph (Princeton, 2008). Any retraction preserves the local convergence of Newton's method, so the choice among retractions is about cost and convenience.

The most natural candidate is to project $x+u$ back onto the manifold: take the nearest point. Absil and Malick (SIAM J. Optim. 2012; preprint HAL hal-00651608) show in §3.1 that this projective retraction is always a valid retraction of maximal smoothness, and then compute it for fixed-rank, spectral and Stiefel manifolds. The underlying fact, that the nearest-point map onto a $C^k$ submanifold is locally single-valued and $C^{k-1}$, is classical (the paper cites Lewis and Malick, Math. Oper. Res. 2008); the paper gives a short proof through the inverse function theorem on the normal bundle. This mission formalizes §3.1: that lemma and the resulting retraction.

Setting

Let $\mathcal E$ be a Euclidean space, a finite-dimensional real inner product space, of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a submanifold of class $C^k$ and dimension $d$ around $\bar x$ if $\bar x\in\mathcal M$ and there are an open neighbourhood $U_{\mathcal E}$ of $\bar x$ and a $C^k$ diffeomorphism $\varphi$ from $U_{\mathcal E}$ onto an open subset of $\mathbb R^n$ with

$$\mathcal M\cap U_{\mathcal E}=\{x\in U_{\mathcal E}:\ \varphi_{d+1}(x)=\cdots=\varphi_n(x)=0\}.$$

The tangent space $T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ spanned by the tangent cone of $\mathcal M$ at $x$, and the normal space is $N_{\mathcal M}(x)=T_{\mathcal M}(x)^\perp$. The tangent bundle and normal bundle are $T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in T_{\mathcal M}(x)\}$ and $N\mathcal M=\{(x,v):x\in\mathcal M,\ v\in N_{\mathcal M}(x)\}$, subsets of $\mathcal E\times\mathcal E$. $P_{T_{\mathcal M}(x)}$ denotes the orthogonal projector onto $T_{\mathcal M}(x)$.

The projection of $x\in\mathcal E$ onto $\mathcal M$ is the set of nearest points,

$$P_{\mathcal M}(x)=\operatorname{argmin}\{\|x-y\|:\ y\in\mathcal M\},$$

which may be empty (if $\mathcal M$ is not closed) or contain several points (if $\mathcal M$ is not convex).

A map $R$ from $T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if on some neighbourhood $\mathcal U$ of $(\bar x,0)$ in $T\mathcal M$ it is of class $C^{k-1}$, satisfies $R(x,0)=x$, and $\mathrm DR(x,\cdot)(0)=\mathrm{id}_{T_{\mathcal M}(x)}$ for $(x,0)\in\mathcal U$.

The formal retraction predicate includes $k\ge2$ and a local submanifold chart at $\bar x$; this ensures that its base point lies on $\mathcal M$.

Formalization targets

Goal: Proposition 3.2 (projective retraction)

For $\mathcal M$ a $C^k$ submanifold ($k\ge2$) around $\bar x$, the map

$$R(x,u)=P_{\mathcal M}(x+u),\qquad (x,u)\in T\mathcal M,$$

is single-valued near $(\bar x,0)$ in $T\mathcal M$, and this single value is a retraction around $\bar x$.

Milestones

1. (3.2) If $p\in P_{\mathcal M}(x)$ and $\mathcal M$ is a $C^k$ submanifold around $p$, then $p\in\mathcal M$ and $x-p\in N_{\mathcal M}(p)$.
2. (3.3) $T_{N\mathcal M}(\bar x,0)=T_{\mathcal M}(\bar x)\times N_{\mathcal M}(\bar x)$.
3. Lemma 3.1 There is $\delta>0$ such that on $B(\bar x,\delta)$ the projection $P_{\mathcal M}$ is a single point $P(x)$, the map $P$ is $C^{k-1}$, and

$$\mathrm DP_{\mathcal M}(\bar x)=P_{T_{\mathcal M}(\bar x)}.$$

Significance

The projective retraction is the reference retraction on an embedded submanifold: it exists for every $C^k$ submanifold, it has the maximal smoothness $C^{k-1}$ allowed by the tangent bundle, and it is the one practitioners compute first (truncated SVD for fixed-rank matrices, polar factor for the Stiefel manifold). Section 4 of the paper shows that it is moreover second order and generalizes it to projections along arbitrary smooth fields of transverse subspaces; Lemma 3.1 is the model of that argument. Lemma 3.1 on its own is a basic tool well beyond retractions: local single-valuedness and smoothness of the nearest-point map underlies the local convergence analysis of alternating projections on manifolds and the theory of prox-regular sets.

All statements here are proved results. No machine-checked proof of them is known to exist: Mathlib has the inverse function theorem, tangent cones and orthogonal projections onto subspaces, but no embedded submanifolds of a Euclidean space with their normal bundle and no nearest-point map onto non-convex sets. The mission produces these statements in Lean and invites proofs of them.

Difficulty

The obvious argument writes the nearest point as a critical point of $y\mapsto\|x-y\|^2$ on $\mathcal M$ and applies the implicit function theorem. Two things break. First, existence: $\mathcal M$ is not assumed closed, so a nearest point exists only because $\mathcal M$ is locally closed near $\bar x$ and points of $\mathcal M$ far from $\bar x$ are farther from $x$ than $\bar x$ is. Second, uniqueness: critical points are not unique in general, and the implicit function theorem only describes critical points near a given one. Uniqueness needs a quantitative argument that every nearest point of $x$ lies in the region where $(p,v)\mapsto p+v$ on the normal bundle is injective. Finally, the normal bundle is itself only a $C^{k-1}$ manifold, whose tangent space at $(\bar x,0)$ must be identified before the inverse function theorem applies; this is milestone (3.3).

Formalization scope

The ambient space is any type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $k\ge2$ stated as a hypothesis (so that $k-1$ in ℕ is honest). The paper's standing assumption "$\mathcal M$ is a submanifold of class $C^k$ ($k\ge2$) and dimension $d$" enters only as the local hypothesis IsSubmanifoldAt k d M xbar, exactly as Lemma 3.1 and Proposition 3.2 state it ("around $\bar x$"). The chart is an OpenPartialHomeomorph onto EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. No closedness of $\mathcal M$ is assumed, because the paper does not assume it.

The projection is the platform predicate IsMetricProjection M x z ($z\in\mathcal M$ and $\|x-z\|\le\|x-w\|$ for all $w\in\mathcal M$); single-valuedness is stated as equality of the set of such $z$ with a singleton, which asserts existence and uniqueness. A formalization that only states "some selection is $C^{k-1}$", or uses $\subseteq$ (satisfied by the empty set), would drop the main claim and is ruled out. The tangent space is the span of Mathlib's tangentConeAt; "class $C^{k-1}$ on a neighbourhood in $T\mathcal M$" is ContDiffOn on $O\cap T\mathcal M$ with $O$ open; $\mathrm DR(x,\cdot)(0)=\mathrm{id}$ is a HasFDerivAt statement on the normed space $T_{\mathcal M}(x)$; $P_{T_{\mathcal M}(\bar x)}$ is Submodule.starProjection.

A complete development needs: the tangent space of a slice submanifold equals the image of the chart's derivative, the normal bundle as a $C^{k-1}$ manifold, an inverse function theorem on it, and compactness of $\mathcal M\cap\bar B(\bar x,r)$ for small $r$. These are reusable for the other missions of this series (fixed-rank, spectral and Stiefel manifolds, and the retractor construction of Section 4), and contributions of such general lemmas as intermediate theorems are welcome.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (preprint: https://hal.science/hal-00651608, version 2, the basis of the statement indices here)
• R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens and M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22:359–390, 2002. https://doi.org/10.1093/imanum/22.3.359
• P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291

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 a multi-armed bandit problem a learner chooses one of $K$ actions in each of $n$ rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order $\sum_i \log(n)/\Delta_i$, logarithmic in $n$. In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order $\sqrt{nK}$, which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay $\sqrt n$ even when the rewards are i.i.d.

Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).

Setting

There are $K\ge2$ arms and $n\ge K$ rounds. On round $t$ the algorithm draws an arm $I_t$ from a probability vector $p_t=(p_{1,t},\dots,p_{K,t})$ computed from the history it has observed. At the same time a reward vector $g_t\in[0,1]^K$ is fixed, and the algorithm observes only $g_{I_t,t}$.

• Adversarial model. The vector $g_t$ is chosen by an adaptive adversary: a function of the arms $I_1,\dots,I_{t-1}$ played earlier, but not of $I_t$. The regret is $R_n=\max_i\sum_{t=1}^n g_{i,t}-\sum_{t=1}^n g_{I_t,t}$.
• Stochastic model. There are distributions $\nu_1,\dots,\nu_K$ on $[0,1]$ with means $\mu_i$, and all $g_{i,t}\sim\nu_i$ are independent. The pseudo-regret is $\overline R_n=\sum_{t=1}^n(\max_i\mu_i-\mu_{I_t})$. The gap of arm $i$ is $\Delta_i=\max_j\mu_j-\mu_i$, and the minimal gap is $\Delta=\min_{i:\Delta_i>0}\Delta_i$.

The analysis uses importance-weighted estimates $\widetilde H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}\mathbb 1_{\{I_s=i\}}/p_{i,s}$, the sample means $\widehat H_{i,t}$, the averages $H_{i,t}=\frac1t\sum_{s\le t}g_{i,s}$, and the play counts $T_i(t)$.

SAO (Algorithm 1 of the paper) takes a parameter $\beta>1$. It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate $\widetilde H_{i,t}$ falls far below the best active one. The probability of a deactivated arm then decays as $q_i\tau_i/t$, where $\tau_i$ is the deactivation time and $q_i$ the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round $\tau_0$, SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.

Formalization targets

Goal: Theorem 4.1, high-probability form

For every $\delta\in(0,1)$ let $\beta=10Kn^3\delta^{-1}$. With probability at least $1-\delta$, SAO with parameter $\beta$ satisfies, in the stochastic model (whenever some arm has $\Delta_i>0$),

$$\overline R_n\le\frac{260K(1+\log K)\log^2(\beta)}{\Delta},$$

and, against every adaptive adversary with rewards in $[0,1]$,

$$R_n\le60(1+\log K)(1+\log n)\sqrt{nK\log(\beta)+5K^2\log^2(\beta)}+200K^2\log^2(\beta).$$

Milestones

The milestones follow the paper's proof in order:

• Freedman's inequality (Theorem 4.3) in the paper's two-sided form, and its variance-adaptive form, Lemma 4.4.
• The concentration lemmas for SAO's estimates (Lemmas 4.5, 4.6, 4.7) and the Exp3.P phase (Lemma 4.8).
• The two good events of §4.1, (21)–(25).
• The deterministic consequences on those events: Exp3.P is never started in the stochastic model; suboptimal arms are deactivated by time $260K\log(\beta)/\Delta_i^2$; $\sum_iq_i\le1+\log K$, (27); and the adversarial regret bound of §4.3.
• The two halves of Theorem 4.1.

Significance

The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets $O(K\log K\log^2(n/\delta)/\Delta)$ pseudo-regret on stochastic rewards and $\tilde O(\sqrt{nK})$ regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.

The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.

Difficulty

Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to $\widetilde H_{i,t}$. The variance of the importance-weighted estimate grows like $\sum_s1/p_{i,s}$, which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with $\max(t-\tau_i,0)/(q_i\tau_it)$. In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.

Formalization scope

All declarations live in the namespace BestBothWorlds.SAO.

• Arms and paths. Arms are Fin K and rounds are $1,\dots,n$. An arm path is Fin n → Fin K.
• Algorithms and adversaries. An algorithm is a deterministic map from the observed history to a probability vector. A deterministic adaptive adversary is a map from the list of earlier arms to a reward vector; randomized adversaries are mixtures of these.
• Probabilities. For a fixed adversary, the probability of an event is $\sum_{I\in E}\prod_tp_{I_t,t}$. In the stochastic model this is integrated against the product law of the reward table.
• Logarithms and constants. Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with $\beta=10Kn^3\delta^{-1}$.
• SAO. It is defined exactly as Algorithm 1. Arms are tested in order within a round, and the active set changes during the loop. Test (13) is false when $T_i(t)=0$, and test (14) is false when $\tau_i=1$.
• Exp3.P. After the switch, Exp3.P runs from scratch for $n-\tau_0$ rounds. Its parameters are those of Bubeck–Cesa-Bianchi Theorem 3.2 with confidence $K/\beta$, and $\gamma$ and $\beta_{\mathrm P}$ are clipped at $1$.
• §4 notation. $\tau_0$, $\tau_i\leftarrow\min(\tau_i,\tau_0)$ and $q_i=p_{i,\min(\tau_i,\tau_0)}$ are computed from the run, never assumed.

A trivializing formalization is ruled out. The goal's hypotheses concern only the instance ($K$, $n$, $\delta$, the distributions or the adversary). The algorithm's quantities ($\tau_0$, $\tau_i$, $q_i$, the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.

The expectation form of Theorem 4.1 ($O(\cdot)$ bounds with $\beta=n^4$), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.

Selected references

• S. Bubeck and A. Slivkins, The best of both worlds: stochastic and adversarial bandits, COLT 2012; arXiv:1202.4473v1. https://arxiv.org/abs/1202.4473
• S. Bubeck and N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://doi.org/10.1561/2200000024
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, N. Cesa-Bianchi, Y. Freund and R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• Y. Seldin and A. Slivkins, One practical algorithm for both stochastic and adversarial bandits, ICML 2014. https://proceedings.mlr.press/v32/seldinb14.html
• J. Zimmert and Y. Seldin, Tsallis-INF: an optimal algorithm for stochastic and adversarial bandits, JMLR 22, 2021. https://jmlr.org/papers/v22/19-753.html

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$: an order placed in period $t$ arrives in period $t + L$. Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$. Ordering costs are zero ($c_t = 0$), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$.

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$; $\mathcal F_t$ is the information at the beginning of period $t$, and $D_t$ is $\mathcal F_{t+1}$-measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$-measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

$$H^P_t = \sum_{j=t+L}^{T} h_j\,\bigl(Q^P_t - (D_{[t,j]} - X^P_t)^+\bigr)^+, \qquad \Pi^P_t = p_{t+L}\,\bigl(D_{[t,t+L]} - Y^P_t\bigr)^+ .$$

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$, and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

$$E\bigl[H^B_t \mid \mathcal F_t\bigr] = E\bigl[\Pi^B_t \mid \mathcal F_t\bigr] \quad\text{almost surely.}$$

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$,

$$E[\mathcal C(B)] \;\le\; 2\,E[\mathcal C(P)] .$$

The paper writes $P = OPT$; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

1. Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$.
2. Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$, $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
3. Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$, $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$, which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$, so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

• Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$.
• Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
• Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$, so an infinite expected cost is never read as $0$.
• The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$, so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$) cannot satisfy it vacuously. The existence item rules out an empty policy class.
• Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
• Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$; both are typos, and the formalization uses $X_t$ and $p_{t+L}$.

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$-measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
• D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.