Missions · Prove2Me

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Convergence Properties of the Nelder–Mead Simplex Method in Low Dimensions II: In Dimension 1 with ρ = 1, the Interval Diameter Halves Every M Iterations, M Depending Only on χ and γResearch Paper

Motivation

The Nelder–Mead simplex method (Nelder and Mead, 1965) is a derivative-free method for unconstrained minimization. It keeps a simplex of $n+1$ points in $\mathbb R^n$ and replaces the worst vertex by a reflected, expanded or contracted trial point, using only comparisons of function values. It is one of the most widely used methods in practice, available in standard numerical libraries and scientific software, and it is also known for having very little supporting theory. McKinnon (1998) gave a strictly convex function in dimension 2 on which the method converges to a nonstationary point.

Lagarias, Reeds, Wright and Wright (1998) gave the first convergence results for the method as originally stated. In dimension 1 they proved that, for a strictly convex function with bounded level sets, both endpoints of the Nelder–Mead interval converge to the minimizer when $\rho\chi \ge 1$ (their Theorem 4.1). For the standard reflection coefficient $\rho = 1$ they proved more: the convergence is eventually M-step linear, with a number of steps that depends only on the expansion and contraction coefficients (their Theorem 4.2). This mission formalizes that rate result and the move-sequence lemmas it rests on.

Setting

Let $f:\mathbb R\to\mathbb R$ . A one-dimensional simplex is a pair of vertices $\Delta = (x_1, x_2)$ ordered so that $f(x_1)\le f(x_2)$ : $x_1$ is the best and $x_2$ the worst vertex. The method has four coefficients satisfying

\rho>0,\qquad \chi>1,\qquad \chi>\rho,\qquad 0<\gamma<1,\qquad 0<\sigma<1. \tag{2.1}

This mission fixes $\rho=1$ , so (2.1) becomes $\chi>1$ , $0<\gamma<1$ , $0<\sigma<1$ . The trial points are

x_r = x_1 + (x_1-x_2),\quad x_e = x_1 + \chi(x_1-x_2),\quad x_c = x_1 + \gamma(x_1-x_2),\quad x_{cc} = x_1 - \gamma(x_1-x_2).

With $f_1=f(x_1)$ , $f_2=f(x_2)$ , $f_r=f(x_r)$ and so on, one iteration is:

if $f_r<f_1$ , an expansion accepting $x_e$ when $f_e<f_r$ , and otherwise a reflection accepting $x_r$ ;
if $f_1\le f_r<f_2$ , an outside contraction accepting $x_c$ when $f_c\le f_r$ , and otherwise a shrink;
if $f_r\ge f_2$ , an inside contraction accepting $x_{cc}$ when $f_{cc}<f_2$ , and otherwise a shrink.

A shrink replaces $x_2$ by $x_1+\sigma(x_2-x_1)$ . The worst vertex is discarded and the accepted point $v$ joins $x_1$ ; it becomes the best vertex exactly when $f(v)<f(x_1)$ . Iterating from a nondegenerate initial pair $\Delta_0$ ( $x_1\neq x_2$ ) gives the run $\Delta_0,\Delta_1,\ldots$ , and $\operatorname{diam}(\Delta_k) = |x_1^{(k)}-x_2^{(k)}|$ . A contraction means an outside or inside contraction.

Under $\rho=1$ each move multiplies the diameter by a fixed factor: $1$ for a reflection, $\chi$ for an expansion and $\gamma$ for either contraction. The paper's bracketing index $K$ (its Lemma 4.2) is the first iteration with $f_1^{(K)}\le f_e^{(K)}$ . Two integers control the move sequences after $K$ :

r^* = \lceil\chi-1\rceil,\qquad j^* = \max\{\,j\ge 0 : \chi+\chi^2+\cdots+\chi^j < N_{NM}\,\},\qquad N_{NM} = \max(\chi,1/\gamma).

Formalization targets

Goal: Theorem 4.2 (p. 130)

For all $\chi>1$ and $0<\gamma<1$ there is an integer $M$ such that for every $0<\sigma<1$ , every strictly convex $f$ with bounded level sets and every nondegenerate ordered $\Delta_0$ , the index $K$ exists and

\operatorname{diam}(\Delta_{k+M})\le \tfrac12\operatorname{diam}(\Delta_k)\qquad\text{for all }k\ge K.

The goal fixes no value of $M$ ; the paper's proof gives one, but any $M$ depending only on $\chi$ and $\gamma$ proves the theorem.

Milestones

Lemma 4.6 (p. 131): at most $r^*$ consecutive reflections, and no expansion immediately after a reflection.
Corollary 4.1 (p. 131): a contraction occurs at some iteration in $[K, K+r^*]$ .
Lemma 4.7 (p. 132): after a contraction, no block of consecutive expansions is longer than $j^*$ .
Lemma 4.8 (p. 133): there is $\varphi<1$ depending only on $\chi,\gamma$ such that the simplex after a contraction and the simplex after the next contraction satisfy $\operatorname{diam}(\Delta')\le\varphi\operatorname{diam}(\Delta)$ .

Significance

Theorem 4.2 is a rate statement for a method whose global behaviour is mostly unexplained. It shows that in dimension 1 with $\rho=1$ the method behaves like a bracketing line search: once the minimizer is bracketed, the interval shrinks geometrically, and the number of iterations per halving is bounded independently of $f$ and of the starting interval. With the standard coefficients $\chi=2$ , $\gamma=\tfrac12$ the value of $M$ constructed in the paper's proof is $M=4$ . The intermediate lemmas describe which move sequences the method can produce after the minimizer is bracketed.

The paper's results are proved; to our knowledge none of them has a machine-checked proof. This mission produces a formal model of the one-dimensional method with the paper's tie-breaking rules, and formal statements of the rate theorem and its supporting lemmas. Proving them is the remaining work, including the one-dimensional bracketing and proximity results of the paper's §4.2, which the proofs use and which are posed as a separate mission of this series.

Difficulty

The rate does not follow from a per-iteration bound: a reflection keeps the diameter and an expansion multiplies it by $\chi>1$ , so the diameter can grow for several consecutive iterations. A contraction-only argument fails for this reason. The theorem needs a bound on how long the method can avoid contracting and on how much expansion can happen between two contractions. Both bounds come from strict convexity applied along the line through the current interval, together with the location of the minimizer relative to the vertices (the proximity property of §4.2), and they must hold uniformly in $f$ . Making the constants uniform, so that $M$ and $\varphi$ depend only on $\chi$ and $\gamma$ , is the delicate part. Before $K$ no such control holds, which is why the theorem only speaks about $k\ge K$ .

Formalization scope

The state is an ordered pair p : ℝ × ℝ with p.1 the best vertex $x_1$ and p.2 the worst vertex $x_2$ ; run f 1 χ γ σ p0 k is $\Delta_k$ , and moveAt f χ γ σ p0 k is the type of iteration $k$ . The coefficient $\rho=1$ is substituted into the algorithm. The ordering rule is the paper's insertion rule (new point first iff $f(v)<f(x_1)$ , ties to the higher index); the printed formula $j=\max\{\ell \mid f(v)<f(x_{\ell+1})\}$ contradicts the paper's own example on p. 118 and is read as its words describe. The expansion step accepts the better of $x_r$ and $x_e$ , the outside contraction is accepted on $f_c\le f_r$ , the inside contraction on $f_{cc}<f_2$ .

Standing assumptions carried by every statement: (2.1) with $\rho=1$ ; $f$ strictly convex on $\mathbb R$ (StrictConvexOn ℝ Set.univ f); bounded level sets ( $\{x : f(x)\le\mu\}$ bounded for every $\mu$ ); and $\Delta_0$ nondegenerate and ordered. Corollary 4.1 prints only $\rho=1$ ; the remaining conditions of (2.1) are the section's standing assumptions. $r^*$ is the natural-number ceiling $\lceil\chi-1\rceil$ ; $j^*$ is computed by a bounded search over $0\le j\le\lceil N_{NM}\rceil$ , which loses nothing for $\chi>1$ . The uniformity of $M$ in Theorem 4.2 and of $\varphi$ in Lemma 4.8 is encoded by quantifier order: they are chosen after $\chi,\gamma$ and before $\sigma$ , $f$ , $\Delta_0$ .

The goal's conclusion includes the existence of the bracketing index $K$ (the paper's Lemma 4.2), so the halving claim cannot hold vacuously for a run that is never bracketed; a statement that lets $M$ depend on $f$ or $\Delta_0$ is a different and much weaker theorem and is ruled out by the quantifier order.

A complete development needs: the one-dimensional facts about strictly convex functions (the paper's Lemma 4.1), the absence of shrink steps under strict convexity (Lemma 3.5 for $n=1$ ), the bracketing and proximity lemmas of §4.2, and the move-sequence and diameter-product arguments of §4.3. The model of the one-dimensional method and the convexity lemmas are reusable for the series' first mission (convergence of both endpoints). Proofs of individual milestones, and of the §4.2 lemmas as local results, are welcome.

Selected references

J. C. Lagarias, J. A. Reeds, M. H. Wright, P. E. Wright, Convergence properties of the Nelder–Mead simplex method in low dimensions, SIAM J. Optim. 9(1):112–147, 1998. https://doi.org/10.1137/S1052623496303470
J. A. Nelder, R. Mead, A simplex method for function minimization, Computer Journal 7(4):308–313, 1965. https://doi.org/10.1093/comjnl/7.4.308
K. I. M. McKinnon, Convergence of the Nelder–Mead simplex method to a nonstationary point, SIAM J. Optim. 9(1):148–158, 1998. https://doi.org/10.1137/S1052623496303482

7 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Simulation Output Analysis Using Standardized Time Series 3: No g in 𝓜 Makes g(σB) Almost Surely Constant, So the Length Bound Is Not AttainedResearch Paper

Motivation

A steady-state simulation produces a single long output path $Y=\{Y(t):t\ge0\}$ , and the quantity of interest is its long-run mean $\mu$ . The central difficulty of simulation output analysis is that the observations are correlated, so the classical confidence interval $\bar Y_n(1)\pm z\,\hat\sigma/\sqrt n$ needs a consistent estimate of the time-average variance constant $\sigma^2$ , which is hard to obtain. The method of standardized time series (STS), introduced by Schruben (1983) and put on a general footing by Glynn and Iglehart (Math. Oper. Res. 15 (1990)), avoids estimating $\sigma$ : it divides the centred sample mean by a functional $g$ of the whole sample path that scales like $\sigma$ , so that $\sigma$ cancels in the limit. Batch means, the area estimator and other procedures used in simulation software are all instances of this construction.

Cancelling $\sigma$ has a price. Glynn and Iglehart show (their Corollary 4.16) that every STS interval has asymptotic expected length at least $2\sigma\Phi^{-1}(1-\delta/2)/\sqrt n$ , the length of the interval that knows $\sigma$ , and (4.23) that this bound is the infimum over all admissible $g$ . This mission formalizes the next question the paper asks and answers: is the infimum attained? Proposition 4.26 says it is not, and the companion results quantify the residual randomness of the interval length.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform metric $\rho(x,y)=\sup_t|x(t)-y(t)|$ and its Borel $\sigma$ -algebra; $k(t)=t$ , and $C_0[0,1]=\{x\in C[0,1]:x(0)=0\}$ . For $g:C[0,1]\to\mathbb R$ , $D(g)$ is the set of points at which $g$ is not continuous. On a probability space $(\Omega,\mathcal F,P)$ , $B$ is a standard Brownian motion, viewed as a random element of $C[0,1]$ .

Assumption (2.1). There are finite constants $\mu$ and $\sigma>0$ such that $X_n\Rightarrow\sigma B$ in $C[0,1]$ , where

X_n(t)=n^{1/2}\big(\bar Y_n(t)-\mu t\big),\qquad \bar Y_n(t)=\frac1n\int_0^{nt}Y(s)\,ds,\quad 0\le t\le1 .

The class $\mathcal M$ (2.3) consists of the measurable $g:C[0,1]\to\mathbb R$ with

$g(ax)=a\,g(x)$ for $a>0$ ;
$g(x-\beta k)=g(x)$ for $\beta\in\mathbb R$ ;
$P\{g(B)>0\}=1$ ;
$P\{B\in D(g)\}=0$ .

With $H(x)=P\{B(1)/g(B)\le x\}$ and $\alpha,\beta$ chosen so that $H(\beta)-H(\alpha)=1-\delta$ , the interval $[\bar Y_n(1)-g(\bar Y_n)\beta,\ \bar Y_n(1)-g(\bar Y_n)\alpha]$ (2.10) is an asymptotic $100(1-\delta)\%$ confidence interval for $\mu$ , of width $L_n=g(\bar Y_n)(\beta-\alpha)$ .

Formalization targets

Goal: Proposition 4.26

For every $\sigma>0$ there is no $g\in\mathcal M$ such that, for some $\alpha>0$ ,

P\{g(\sigma B)=\alpha\sigma\}=1. \qquad (4.25)

By the paper's discussion before (4.25), attaining the lower bound of Corollary 4.16 with some $g\in\mathcal M$ requires (4.25); the goal therefore says that the bound is attained by no $g\in\mathcal M$ . The goal is stated in terms of (4.25) and not of the limit (4.24), so it does not depend on the expected-length machinery of Corollary 4.16.

Milestones (the steps of the proof, pp. 13–14)

For $|z|<\eta$ : $P\{|B(t)-z|<\eta,\ \max_{0\le s\le t}|B(s)|<2\eta\}>0$ .
(4.27): $P\{\rho(\sigma B,x)<\varepsilon\}>0$ for every $x\in C_0[0,1]$ and $\varepsilon>0$ .
If the range of $g$ over every $\varepsilon$ -neighbourhood of $x$ contains $\{\alpha\sigma:\sigma>0\}$ , then $x\in D(g)$ .
Under (2.3i) and (4.25), $C_0[0,1]\subseteq D(g)$ .

Companions

$g(B)$ is nondegenerate for every $g\in\mathcal M$ (p. 14).
Proposition 4.32: if $\{g^2(X_n)\}$ is uniformly integrable, then

\lim_{n\to\infty}nE(L_n-EL_n)^2=\sigma^2E\big(g(B)-Eg(B)\big)^2(\beta-\alpha)^2>0 .

Significance

The result closes the expected-length analysis of STS intervals: the bound $2\sigma\Phi^{-1}(1-\delta/2)$ is the exact infimum over $\mathcal M$ but no single standardization reaches it, so every STS procedure is strictly worse, in expected length, than the interval with known $\sigma$ . The companion results explain why: $g(B)$ is never degenerate, so $n^{1/2}L_n$ converges to a nondegenerate random limit and the interval length fluctuates at order $n^{-1/2}$ , while intervals built on a consistent estimator of $\sigma$ (the regenerative method, Proposition 4.34) fluctuate only at order $n^{-1}$ . This is the quantitative trade-off a practitioner faces when choosing between STS and variance-estimation methods.

The paper's results are proved; none of them is formalized. The mission produces machine-checked versions of a support property of Wiener measure on $C[0,1]$ (every path started at $0$ is in the support), which is reusable well beyond simulation, and of the deterministic step that turns such a support property into everywhere-discontinuity of a functional.

Difficulty

The goal's statement is elementary, but its proof needs a quantitative fact about Brownian paths: the law of $\sigma B$ charges every uniform ball around every path in $C_0[0,1]$ . The natural first attempt, using that $g$ is continuous $P$ -almost everywhere and constant almost surely on $\sigma B$ , fails without this fact, because almost-sure statements say nothing about any particular path $x$ . Mathlib provides Brownian finite-dimensional laws and independent increments, but no small-ball or support estimate for Brownian motion in the uniform metric, so (4.27) has to be built from scratch. A second subtlety is that (4.25) is given for one $\sigma$ only; the homogeneity (2.3i) is what upgrades it to all scales, and that upgrade is what makes the range of $g$ near $x$ unbounded.

Proposition 4.32 needs, in addition, the passage from weak convergence of $g(X_n)$ to convergence of second moments under uniform integrability, in the space $C[0,1]$ .

Formalization scope

$C[0,1]$ is C(unitInterval, ℝ) with its sup norm; $\rho$ is dist. Mathlib has no measurable structure on it at this commit, so the Borel $\sigma$ -algebra is declared in the mission's definitions file.
$B$ is a measurable map $\Omega\to C[0,1]$ whose coordinates agree, for every $\omega$ , with a process satisfying Mathlib's IsBrownianReal. "Measurable" in $\mathcal M$ means Borel measurable.
$D(g)$ is the set where $g$ is not continuous; $P\{B\in D(g)\}$ is the outer measure of the preimage, so no measurability of $D(g)$ is assumed.
Assumption (2.1) is a structure: joint measurability of $Y$ , local integrability of its paths (the implicit condition that makes $\bar Y_n$ defined), $\bar Y_n$ pinned pointwise by its integral formula, $\sigma>0$ , and convergence in distribution of $X_n$ to $\sigma B$ . The index $n$ ranges over $\mathbb N$ .
$P\{\cdot\}=1$ is "almost surely". $0<\delta<1$ is added where the confidence level appears.
The paper writes " $D(g)=C_0[0,1]$ " at the end of the proof of Proposition 4.26; its argument proves only $C_0[0,1]\subseteq D(g)$ , which is what milestone 4 states.
Proposition 4.32 uses Bochner integrals; its uniform-integrability hypothesis makes every integral there finite.

The goal is a negation of an existence statement, so it would be trivially true if $\mathcal M$ were empty or if the Brownian hypothesis were unsatisfiable. Neither holds: $\mathcal M$ contains the batch-means functionals of the paper's Example 3.1 (p. 5), and the goal assumes nothing about small balls, (4.27) or continuity of $g$ . Those appear only as milestones.

Contributions welcome: the support theorem for Brownian motion in $C[0,1]$ (milestones 1–2), any of the deterministic steps, and the moment-convergence argument of Proposition 4.32.

Selected references

P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
P. Billingsley, Convergence of Probability Measures, Wiley, 1968. https://doi.org/10.1002/9780470316962

8 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection III: On Instances Separated by Δ(v) the UCB Policy Has Regret at Most B₁N² log T/Δ(v) + B₂Research Paper

Motivation

A retailer with limited shelf or screen space must choose which subset of its products to show each arriving customer. Which assortment earns the most depends on customer preferences, and those are unknown at first: the seller learns them from the purchases it observes. This is dynamic assortment selection, and it is a standard model in online retail and revenue management. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 67(5), 2019; preprint arXiv:1706.03880v2) study it under the multinomial logit (MNL) choice model as the MNL-Bandit problem. They propose an epoch-based upper-confidence-bound policy (Algorithm 1) that needs no prior knowledge of the parameters.

Their worst-case guarantee (Theorem 1) is regret of order $\sqrt{NT\log NT}$ . Many instances are easier than the worst case: the best assortment beats every other feasible assortment by a fixed margin. For such well-separated instances, earlier policies obtained logarithmic regret, but only when told a lower bound on that margin:

Rusmevichientong, Shen and Shmoys (2010), $O(N^2\log^2 T)$ ;
Sauré and Zeevi (2013), $O(N\log T)$ for fixed cardinality.

This mission formalizes the paper's §6.1, which shows that the same parameter-free Algorithm 1 adapts to the separation.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$ and unknown attraction parameters $v_i\ge0$ . The no-purchase option has weight $v_0=1$ . Offered an assortment $S$ , a customer buys $i\in S$ with probability $v_i/(1+\sum_{j\in S}v_j)$ and buys nothing with probability $1/(1+\sum_{j\in S}v_j)$ (2.1). The expected revenue of $S$ is

R(S,\mathbf v)=\frac{\sum_{i\in S}r_iv_i}{1+\sum_{j\in S}v_j}\quad(2.2).

Feasible assortments form a family $\mathcal S$ defined by totally unimodular constraints $A\,x(S)\le b$ (2.3). Assumption 4.1 asks that $v_i\le v_0=1$ for all $i$ and that $\mathcal S$ be closed under taking subsets.

A policy chooses $S_t\in\mathcal S$ from the past choices. The regret after $T$ customers is $\mathrm{Reg}_\pi(T,\mathbf v)=T\,R(S^*,\mathbf v)-\mathbb E_\pi\sum_{t=1}^TR(S_t,\mathbf v)$ , where $S^*$ maximizes $R(\cdot,\mathbf v)$ over $\mathcal S$ (2.6).

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ until a customer buys nothing. It keeps three statistics for each product $i$ :

$T_i(\ell)$ , the number of epochs up to $\ell$ that offered $i$ ;
$\bar v_{i,\ell}$ , the average number of purchases of $i$ per such epoch;
the upper confidence bound $v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,48\log(\sqrt N\ell+1)/T_i(\ell)}+48\log(\sqrt N\ell+1)/T_i(\ell)$ .

The next epoch offers an assortment maximizing the MNL revenue computed with $v^{\mathrm{UCB}}$ in place of $\mathbf v$ .

The separation of an instance is the gap between the optimal and the second-best expected revenue among feasible assortments,

\Delta(\mathbf v)=\min_{S\in\mathcal S:\,R(S,\mathbf v)\neq R(S^*,\mathbf v)}\big(R(S^*,\mathbf v)-R(S,\mathbf v)\big)\quad(6.1).

The analysis uses the threshold $\tau=4NC\log NT/\Delta^2(\mathbf v)$ (6.2), with $C=\max\{C_1^2,C_2\}$ , $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ . It also uses good epochs: those in which every $v^{\mathrm{UCB}}_{i,\ell}$ lies above $v_i$ and within the confidence width of Lemma 4.1.

Formalization targets

Goal: Theorem 3 (p. 20)

There are absolute constants $B_1,B_2$ such that for every instance satisfying Assumption 4.1 with $r_i\in[0,1]$ , every tie-breaking rule and every $T$ ,

\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,\frac{N^2\log T}{\Delta(\mathbf v)}+B_2.

The constants are not fixed, so the goal survives any improvement of them.

Milestones

Lemma 4.1 (p. 13): $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability $\ge1-6/(N\ell)$ , and $v^{\mathrm{UCB}}_{i,\ell}-v_i\le C_1\sqrt{v_i\log(\sqrt N\ell+1)/T_i(\ell)}+C_2\log(\sqrt N\ell+1)/T_i(\ell)$ with probability $\ge1-7/(N\ell)$ .
Lemma 4.3 (p. 14): $(1+\sum_{j\in S}v_j)(\tilde R(S)-R(S,\mathbf v))$ is at most the sum of these widths over the offered set, with probability $\ge1-13/\ell$ .
Lemma 6.1 (p. 20): in a good epoch, if every offered product has $T_i(\ell)\ge\tau$ , the offered assortment is optimal.
Lemma 6.2 (p. 20): at most $N\tau$ good epochs offer a sub-optimal assortment.
Corollary C.1 (p. 48): at most $N\log NT$ epochs offer a product with $T_i(\ell)<\log NT$ .
(C.5) (p. 48): the regret is at most $\mathbb E_\pi\sum_{\ell\le L}(1+V(S_\ell))(R(S^*,\mathbf v)-R(S_\ell,\mathbf v))$ .

Companion: Corollary 6.1 (p. 21)

Under the cardinality constraint $|S|\le K$ : $\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,NK\log NT/\Delta(\mathbf v)+B_2$ .

Significance

The result. Theorem 3 shows that one policy is simultaneously near-optimal in the worst case (Theorem 1, $\tilde O(\sqrt{NT})$ , matched by the lower bound of Theorem 2 up to logarithms) and logarithmic on separated instances. It does so without being told $\Delta(\mathbf v)$ , which the separation-based policies of Rusmevichientong et al. and Sauré–Zeevi require. Under a cardinality constraint, Corollary 6.1 matches the order of Sauré–Zeevi's bound.

Formalizing it. The theorem is proved in the paper (Appendix C), and no machine-checked version exists. A formal proof has to make several things precise:

Algorithm 1 as a function of the observed history;
the epoch structure of a finite horizon;
the pathwise counting arguments of Lemmas 6.1–6.2 and Corollary C.1;
the probabilistic estimates inherited from the worst-case analysis.

Two printed details need care, and the formal statements fix them: Appendix C defines good epochs with "or" where both inequalities are meant, and Lemma 6.2's proof skips one case.

Difficulty

The counting part looks routine but depends on indexing. The bounds that are good at the end of epoch $\ell$ select the assortment of epoch $\ell+1$ , so "a good epoch offering a sub-optimal set" pairs two consecutive epochs. A per-product count of under-sampled epochs is then off by one per product, so the printed bound $N\tau$ does not follow from the statement of Lemma 6.1 by counting alone.

The probabilistic part is the harder one. The per-epoch purchase counts are geometric with mean $v_i$ only conditionally on adaptively chosen assortments. The confidence statements must hold uniformly over a random number of samples, and the regret must be converted from customers to epochs, whose lengths are random and truncated at $T$ . A union bound over all epochs costs a factor $\log T$ , and that factor has to stay within the claimed $N^2\log T/\Delta$ .

Formalization scope

Products are Fin N (0-based), and choices are Option (Fin N) with none the no-purchase option. A policy maps the past choices to an assortment. The law of a length- $T$ history is the product of MNL probabilities, so every expectation is a finite sum. Revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1, and $R(S^*,\mathbf v)$ is a Finset.sup' over the nonempty family $\mathcal S$ . Algorithm 1 is defined as an explicit state machine and never reads $\mathbf v$ . Ties in its argmax are broken by an arbitrary selector, and every statement quantifies over all selectors.

Standing assumptions carried by every statement:

$0\le v_i\le1$ ;
$r_i\in[0,1]$ ;
the totally unimodular form of $\mathcal S$ ;
closure under subsets;
nonemptiness of $\mathcal S$ (needed for $S^*$ to exist).

Disclosed conventions:

UCB before sampling. $v^{\mathrm{UCB}}_{i,\ell}=1$ while $T_i(\ell)=0$ .
Degenerate separation. $\Delta(\mathbf v)=1$ when every feasible assortment is optimal; the regret is then $0$ .
Lemma 4.1 constants. $C_1,C_2$ take the values established in the proof of Lemma 4.1.
Probabilistic lemmas. They are stated for every horizon $T$ as probabilities that epoch $\ell$ is completed and the bound fails.
Lemma 4.3. The printed free index $i$ is read as the sum over the offered set, and $\tilde R$ uses the bounds of the preceding epoch.
(C.5). It is stated as " $\le$ ", since the last epoch is truncated at $T$ .

The constants $B_1,B_2$ are quantified before every other object. A constant depending on $N$ , $\mathbf v$ or $\Delta$ would make the theorem say only that regret is finite. The policy is pinned to Algorithm 1, not to any optimistic rule.

Contributions are welcome at every level:

the pathwise lemmas (6.1, 6.2, C.1), which need no probability;
the epoch rewriting (C.5);
the concentration Lemmas 4.1 and 4.3, shared with the companion mission on Theorem 1;
reusable infrastructure: MNL choice probabilities and finite-horizon history laws for adaptive policies.

Selected references

S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. https://doi.org/10.1287/opre.2018.1832 ; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880v2
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. https://doi.org/10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. https://doi.org/10.1287/msom.2013.0429
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147

9 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: marwahaha

3SUM in O(n^1.999112) Time on a Word RAMResearch Paper

Improve deterministic integer 3SUM to $O(n^{1.999112})$ time in the foundation mission’s word-RAM model.

The existing Corollary 26 routine admits the tighter bound $O(wD^{0.436}+n^2/D^{0.064})$ . Keep $D=\lfloor n^{1/18}\rfloor$ and change the grouping parameter to $g=\lceil D^{0.032}\rceil$ , implemented using the integer root of $D^4$ of order $125$ . Balancing the instance costs and scans gives an Exact Triangle saving of $2/1125$ , and the verified 3SUM reduction gives $n^{2249/1125+o(1)}$ time.

The supporting theorem establishes every rational exponent $r>2249/1125=1.999111\ldots$ , including $1.999112$ . This changes the algorithm’s grouping parameter and improves the earlier cutoff $1.999125$ . All other model definitions and the shared reduction lemmas are reused.

3 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: marwahaha

3SUM in O(n^1.99913) Time on a Word RAMResearch Paper

Prove deterministic $O(n^{1.99913})$ time for 3SUM on polynomially bounded integers, using the same word-RAM model and definitions as the foundation mission.

The existing uniform Exact Triangle bound has saving $\delta=0.00175$ . The verified 3SUM reduction yields $n^{2-\delta/2+o(1)}=n^{1.999125+o(1)}$ time, so every fixed rational exponent above $1.999125$ is attainable, including $1.99913$ . This mission sharpens the bound extracted from the existing algorithm.

The supporting theorem covers all rational $r>1.999125$ ; it does not assert an exact $O(n^{1.999125})$ bound. The proof reuses the shared, proved APSP and 3SUM lemmas from Anthropic’s formalization.

3 thms2 active usersReviewed

Algorithmic Game Theory Markov Chain Probability·Captain: mikedeng1

The Evolution of Conventions III: In 2 × 2 Games with Two Strict Equilibria, the Generically Stable Equilibria of Adaptive Play Are the Weakly Risk Dominant OnesResearch Paper

Motivation

Many games have several strict Nash equilibria, and equilibrium analysis alone does not say which one a population will settle on. Harsanyi and Selten (1988) proposed risk dominance as a selection criterion for $2\times2$ games: of two strict equilibria, select the one whose basin is "larger" in a precise payoff sense. That criterion is axiomatic. H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) derives a selection from a dynamic model instead: boundedly rational players with finite memory, incomplete information about the past and occasional mistakes. Its Theorem 3 says that, in $2\times2$ games, the dynamic selection and risk dominance coincide.

Timeline.

1984. Freidlin and Wentzell develop the theory of small random perturbations of dynamical systems, including the tree characterization of limiting stationary measures.
1990. Foster and Young introduce stochastic stability for evolutionary processes with vanishing noise.
1993. Kandori, Mailath and Rob prove that in symmetric $2\times2$ games with a single population, the long-run equilibrium of a mutation process is the risk dominant one. Young (1993) proves the same selection for adaptive play, a two-population model with sampling from a finite memory, for every $2\times2$ game with two strict equilibria, not only symmetric ones. Its Example 3 shows that in $3\times3$ games the selected equilibrium can differ from both the risk dominant and the Pareto optimal one.

Setting

A finite game $\Gamma$ has players $i$ with finite strategy sets $S_i$ and payoffs $u_i(s)$ . Fix a memory $m$ and a sample size $k$ with $1\le k\le m$ . A state is the sequence $h$ of the last $m$ plays (strategy-tuples), oldest first; a successor of $h$ drops the oldest play and appends a new one. In each period each player draws a sample of $k$ of the $m$ recorded plays and chooses a best reply to it (maximizing total payoff against the sampled plays). The choice probabilities $p_i(s\mid h)$ form a best-reply distribution: $p_i(s\mid h)>0$ exactly when $s$ is a best reply to some sample of size $k$ . This gives adaptive play $P^0$ , display (1).

With mistakes, each player $i$ independently experiments with probability $\varepsilon\lambda_i$ and then plays $s$ with probability $q_i(s\mid h)>0$ . This gives the perturbed chain $P^\varepsilon$ of display (2). It has a unique stationary distribution $\mu^\varepsilon$ . A state $h$ is stochastically stable if $\lim_{\varepsilon\to0}\mu^\varepsilon_h>0$ . A convention is $m$ repetitions of a strict pure Nash equilibrium. With $L_\Gamma$ the longest shortest best-reply path to a strict equilibrium, a strict equilibrium is generically stable if its convention is stochastically stable for all sufficiently large $k$ and all $m$ with $k\le m/(L_\Gamma+2)$ .

For a $2\times2$ game in normal form, with Row's payoffs $a_{rc}$ and Column's $b_{rc}$ satisfying $a_{11}>a_{21}$ , $b_{11}>b_{12}$ , $a_{22}>a_{12}$ , $b_{22}>b_{21}$ , set

R_1=\min\Big\{\tfrac{a_{11}-a_{21}}{a_{11}-a_{12}-a_{21}+a_{22}},\tfrac{b_{11}-b_{12}}{b_{11}-b_{12}-b_{21}+b_{22}}\Big\},\qquad R_2=\min\Big\{\tfrac{a_{22}-a_{12}}{a_{11}-a_{12}-a_{21}+a_{22}},\tfrac{b_{22}-b_{21}}{b_{11}-b_{12}-b_{21}+b_{22}}\Big\}.

$(1,1)$ weakly risk dominates $(2,2)$ if $R_1\ge R_2$ .

Formalization targets

Goal: Theorem 3 (p. 72)

(1,1)\text{ generically stable}\iff R_1\ge R_2,\qquad (2,2)\text{ generically stable}\iff R_2\ge R_1.

This holds for every $2\times2$ game in normal form, for every best-reply distribution and every admissible experimentation.

Milestones, in the order the proof uses them

$P^\varepsilon$ is irreducible and aperiodic and has a unique stationary distribution (§6, pp. 67–68).
(2) is a regular perturbation of (1): $P^\varepsilon\to P^0$ , and $P^\varepsilon_{hh'}$ is of exact order $\varepsilon^{r(h,h')}$ , with $r(h,h')$ the number of mistakes (Appendix, p. 77).
Theorem 2 (p. 69): the stochastically stable states are those in the recurrent classes of $P^0$ of minimum stochastic potential, independently of $\lambda$ and $q$ .
Corollary (p. 70): for weakly acyclic games with $k\le m/(L_\Gamma+2)$ , the stable states are the conventions of minimum stochastic potential.
The $2\times2$ case is acyclic with $L_\Gamma=1$ , and for $k\le m/3$ the recurrent classes of $P^0$ are $\{h_1\}$ and $\{h_2\}$ (p. 70).
$r_{12}=\lceil R_1k\rceil$ and 7. $r_{21}=\lceil R_2k\rceil$ (pp. 71–72).
If $R_1>R_2$ , then $h_1$ is the unique stable convention, and if $R_1=R_2$ , both are, for all large $k$ and $m\ge3k$ (p. 72).

Significance

Theorem 3 gives a dynamic foundation for risk dominance: an equilibrium selection criterion defined from payoffs alone is the long-run outcome of a decentralized learning process with sampling and rare mistakes. It requires no symmetry between the two player roles. Theorem 2 makes stochastic stability computable: a limit of stationary distributions is reduced to a minimum-weight arborescence over recurrent classes. That reduction is what the $2\times2$ computation, and later applications of the method to bargaining and contracting, rely on. The equivalence of the $R$ -form with the product form $(a_{11}-a_{21})(b_{11}-b_{12})\ge(a_{22}-a_{12})(b_{22}-b_{21})$ of Harsanyi and Selten is elementary algebra and is not a target here.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The mission produces formal statements of the model (adaptive play, its perturbation, stochastic stability, resistance and stochastic potential) that are reusable for other stochastic-stability results. Closing the goal also requires formalizing Young's finite version of the Freidlin–Wentzell theorem, the subject of the companion mission The Evolution of Conventions II.

Difficulty

The paper's argument has two hard parts. The first is Theorem 2: identifying the limit of $\mu^\varepsilon$ requires the Markov chain tree theorem (the stationary distribution of an irreducible chain as a ratio of sums over spanning in-trees) together with an order-of-magnitude analysis in $\varepsilon$ . The second is the exact resistance $\lceil R_1k\rceil$ . The page constructs a path with that many mistakes (Table 1), but the matching lower bound, that no combination of mistakes by both players does better, is only asserted. It needs an argument about the first period in which some player's best reply switches. A naive count of single-player mistake runs gives only the upper bound. The tie case of (5) also matters: equality makes strategy 2 a best reply, which is why the ceiling and not the floor appears.

Formalization scope

Players are a finite type and strategies finite types. A state is Fin m → (∀ i, S i) with position 0 the oldest play. A sample is a set of $k$ positions, and a best reply maximizes the summed payoff against the sampled plays. Transition matrices are Matrix H H ℝ. Stochastic stability is a one-sided limit $\varepsilon\to0^+$ of the stationary distributions of $P^\varepsilon$ , over the admissible range $0<\varepsilon$ , $\varepsilon\lambda_i\le1$ . Resistances are natural numbers on successor pairs. Recurrent classes are the essential classes of $P^0$ , and $i$ -trees are parent maps on the set of classes that reach the root. " $k\le m/(L_\Gamma+2)$ " is the natural-number inequality $k(L_\Gamma+2)\le m$ . In the $2\times2$ game, players and strategies are Fin 2, with the paper's $1,2$ written as 0, 1.

Two corrected slips are recorded in the statements. On p. 68 the recurrent classes are "of $P^\varepsilon$ " for $P^0$ , and on p. 77 "the process $P^\varepsilon$ defined in (1)" is $P^0$ .

Trivializing formalizations are ruled out. Stochastic stability is defined from stationary distributions, not from resistances, and generic stability is defined from stochastic stability, not from $\lceil R_1k\rceil$ versus $\lceil R_2k\rceil$ . Both definitions quantify over every best-reply distribution and every admissible $(\lambda,q)$ rather than a fixed sampling law. "Sufficiently large $k$ " is an eventual statement with a threshold, not "for some $k$ ".

A complete development needs Markov chain stationary distributions on finite spaces, the Markov chain tree theorem, limits of rational functions of $\varepsilon$ , and the combinatorics of sampling in $2\times2$ games. The perturbation theory (milestones 1–3) is reusable for any finite stochastic-stability model. Contributions to the tree theorem and to the two resistance computations are particularly welcome.

Related platform work: stochastic fictitious play (StochFictPlay.*, Hofbauer–Sandholm) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra) study other learning dynamics in games. The sibling missions The Evolution of Conventions I (Theorem 1, convergence of adaptive play) and II (Theorem 4, regular perturbations of Markov chains) formalize the results this mission's milestones invoke.

Selected references

H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988.
M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
D. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984. https://doi.org/10.1007/978-1-4684-0176-9

45 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 3: Under Box Uncertainty, Worst-Case CVaR Minimization (16)–(20) Is Equivalent to the Linear Program (24)–(30)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the expected loss in the worst $(1-\beta)$ fraction of outcomes. Rockafellar and Uryasev showed that, for a finite set of scenarios, minimizing CVaR is a linear program whenever the loss is linear in the decision (Rockafellar–Uryasev 2000; 2002). That linear program needs the scenario probabilities, and in practice they are estimates. Zhu and Fukushima (2009) replace the single distribution by a set of distributions and minimize the worst-case CVaR over that set. The resulting problem, (16)–(20) below, contains a maximization over distributions inside a constraint, which no standard solver accepts directly.

This mission treats the first of the two cases the paper works out explicitly: the scenario probabilities are only known to lie in a box around a nominal distribution. Proposition 2 of the paper shows that the worst-case problem is then equivalent to a single problem, (24)–(30), with finitely many explicit constraints. The tool is linear programming duality applied to the inner maximization.

Setting

A decision $x \in \mathbb R^n$ is chosen from a set $\mathcal X \subseteq \mathbb R^n$ . The random vector takes one of $S$ values $y_{[1]}, \dots, y_{[S]} \in \mathbb R^m$ , and $f(x, y)$ is the loss of decision $x$ in outcome $y$ . A distribution over the scenarios is a vector $\pi \in \mathbb R^S$ . Vectors are compared componentwise, $e$ is the all-ones vector, and $\beta \in (0,1)$ is the confidence level.

The box uncertainty set (21) is built from a nominal distribution $\pi^0$ and bounds $\underline\eta, \overline\eta \in \mathbb R^S$ :

\mathcal P_\pi^B = \{\pi : \pi = \pi^0 + \eta,\ e^\top\eta = 0,\ \underline\eta \le \eta \le \overline\eta\}.

Problem (16)–(20) minimizes $\theta$ over $(x, u, \alpha, \theta) \in \mathbb R^n \times \mathbb R^S \times \mathbb R \times \mathbb R$ subject to

x \in \mathcal X,\qquad \max_{\pi \in \mathcal P_\pi^B} \alpha + \tfrac{1}{1-\beta}\pi^\top u \le \theta,\qquad u_k \ge f(x, y_{[k]}) - \alpha,\quad u_k \ge 0\ (k = 1, \dots, S).

By Theorem 2 of the paper its optimal value is the minimum of the worst-case CVaR over $\mathcal X$ .

For fixed $u$ , the worst case over the box involves the linear program (22) and its dual (23):

\gamma^*(u) = \max_{\eta}\{u^\top\eta : e^\top\eta = 0,\ \underline\eta \le \eta \le \overline\eta\},\qquad \min_{(z,\xi,\omega)}\{\overline\eta^\top\xi + \underline\eta^\top\omega : e z + \xi + \omega = u,\ \xi \ge 0,\ \omega \le 0\}.

Problem (24)–(30) minimizes $\theta$ over $(x, u, z, \xi, \omega, \alpha, \theta)$ subject to $x \in \mathcal X$ ,

\alpha + \tfrac{1}{1-\beta}(\pi^0)^\top u + \tfrac{1}{1-\beta}(\overline\eta^\top\xi + \underline\eta^\top\omega) \le \theta,\qquad e z + \xi + \omega = u,\quad \xi \ge 0,\quad \omega \le 0,

and the same constraints $u_k \ge f(x, y_{[k]}) - \alpha$ , $u_k \ge 0$ . A point solves a problem when it is feasible and no feasible point has a smaller $\theta$ .

Formalization targets

Goal: Proposition 2 (p. 1159)

If $(x^*, u^*, z^*, \xi^*, \omega^*, \alpha^*, \theta^*)$ solves (24)–(30), then $(x^*, u^*, \alpha^*, \theta^*)$ solves (16)–(20).
If $(\tilde x^*, \tilde u^*, \tilde\alpha^*, \tilde\theta^*)$ solves (16)–(20) and $(\tilde z^*, \tilde\xi^*, \tilde\omega^*)$ is an optimal solution of (23) with $u = \tilde u^*$ , then $(\tilde x^*, \tilde u^*, \tilde z^*, \tilde\xi^*, \tilde\omega^*, \tilde\alpha^*, \tilde\theta^*)$ solves (24)–(30).
In the situation of 2, an optimal solution of (23) exists.

Milestones, in the order the paper's argument uses them

The decomposition before (22) (p. 1159): if (22) is feasible, then

\max_{\pi \in \mathcal P_\pi^B} \alpha + \tfrac{1}{1-\beta}\pi^\top u = \alpha + \tfrac{1}{1-\beta}(\pi^0)^\top u + \tfrac{\gamma^*(u)}{1-\beta},

and both maxima are attained.

Weak duality for (22)–(23): $u^\top\eta \le \overline\eta^\top\xi + \underline\eta^\top\omega$ for feasible points of the two programs, hence $\gamma^*(u) \le \overline\eta^\top\xi + \underline\eta^\top\omega$ .
Strong duality for (22)–(23): if (22) is feasible, (23) has an optimal solution, with value $\gamma^*(u)$ .
Feasibility transfer from (24)–(30) to (16)–(20), by projection.
Feasibility transfer from (16)–(20) to (24)–(30), by appending an optimal solution of (23).

Significance

Proposition 2 makes worst-case CVaR minimization under box uncertainty computable with standard software. When $f$ is linear in $x$ and $\mathcal X$ is a polyhedron, (24)–(30) is a linear program whose size grows only linearly in $S$ , and when $f$ is convex in $x$ and $\mathcal X$ is convex it is a convex program. The robust portfolio models of §3 of the paper rest on this reformulation. Setting $\underline\eta = \overline\eta = 0$ recovers the Rockafellar–Uryasev linear program (Remark 2 of the paper).

Proposition 2 is proved in the paper. As far as is known, neither it nor the duality pair (22)–(23) has a machine-checked proof; this mission would supply one. The development also exercises LP duality for a specific bounded-variable program, one with a single equality constraint, in a form that can be reused by other robust-optimization reformulations over boxes.

Difficulty

The obvious argument says "replace the max by its dual". Two steps need care. First, the inner maximum is over a polytope that may be empty, and the substitution of (18) by (26)–(28) is correct only when the box is nonempty; it must be shown that an optimal solution of either problem forces the box to be nonempty. Second, the equivalence is a statement about optimal solutions, not feasible ones, so both directions need the comparison of objective values over all feasible points of the other problem. The printed proof assumes in each direction that some optimal solution with a smaller objective exists, where only a feasible one is available; the argument must be run with feasible points. Strong duality for (22)–(23) is a genuine LP duality theorem: Mathlib does not provide it in this form, and it must be derived from a general duality or Farkas-type result.

Formalization scope

Vectors are Fin S → ℝ and Fin n → ℝ, compared pointwise, with zero-based indices. Dot products are ⬝ᵥ, and $e^\top\eta$ is ∑ k, η k. Points of the three problems are structures (Var16, Var24, Dual23) with fields named as in the paper. The factor $\frac{1}{1-\beta}$ is (1 - β)⁻¹, and every theorem assumes $0 < \beta < 1$ .

Committed readings:

Constraint (18), printed as " $\max_{\pi \in \mathcal P_\pi^B} \ldots \le \theta$ ", is stated as "for all $\pi \in \mathcal P_\pi^B$ ". The two agree whenever the maximum exists, and the $\forall$ form stays correct on an empty box. A real supremum there would silently become the constraint $0 \le \theta$ .
$\gamma^*(u)$ is a real supremum, and every statement using it assumes (22) feasible.
"Solves" means feasible and minimal in $\theta$ (IsMinOn). Feasibility alone would make the proposition trivial and is ruled out.
Clause 3 of the goal states the existence of an optimal solution of (23). Without it, clause 2 could hold vacuously.
No hypothesis is placed on $f$ , $\mathcal X$ , $\pi^0$ , $\underline\eta$ or $\overline\eta$ . The paper intends $\pi^0 + \underline\eta \ge 0$ and $\pi^0$ a distribution, but Proposition 2 holds without these assumptions.

Needed infrastructure: LP strong duality for the pair (22)–(23), derivable from Mathlib's Farkas lemma or from LP duality theorems already on the platform; finite sums and dot products. Proofs of the milestones, of the goal from the milestones, and of a general bounded-variable LP duality lemma are all welcome.

Not in scope: the ellipsoidal case (31)–(40), Remark 2, and the portfolio instances of §3.

Selected references

S. Zhu, M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar, S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2:21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar, S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26:1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
A. Ben-Tal, A. Nemirovski, Robust Optimization — Methodology and Applications, Mathematical Programming Ser. B 92:453–480, 2002. https://doi.org/10.1007/s101070100286

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Old and New Methods for Lost-Sales Inventory Systems 1: Under Any Policy in Z(s) the State Enters X(s) and Never Leaves, So Every State Outside X(s) Is TransientResearch Paper

Why the lost-sales state space matters

The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number $L$ of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an $L$ -dimensional state space.

Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class $Z(s)$ that contains the usual heuristics. This mission formalizes that section: the reduced state space $X(s)$ , the policy class $Z(s)$ , and Claim 1, which says that states outside $X(s)$ are transient.

Setting

Fix the lead time $L\ge 1$ . The state is the $L$ -vector $x=(x_0,\dots,x_{L-1})$ : $x_0$ is the stock on hand after this period's delivery, and $x_l$ ( $1\le l\le L-1$ ) is the order that arrives $l$ periods later, so $x_{L-1}$ is the most recent order. Given the state $x$ , an order $z\ge 0$ and a demand $d\ge 0$ , the next state is

x_+ = \bigl([x_0-d]^+ + x_1,\ x_2,\ \dots,\ x_{L-1},\ z\bigr),\qquad [a]^+=\max(a,0).

Demands in successive periods are independent with a common law $D$ on $[0,\infty)$ .

The pipeline partial sums are $v_l=\sum_{m=l}^{L-1}x_m$ for $l=0,\dots,L-1$ and $v_L=0$ ; $v_0$ is the inventory position and $v_{L-1}=x_{L-1}$ the most recent order. A level vector is $s=(s_0,\dots,s_L)$ with $s_0\ge s_1\ge\dots\ge s_L\ge 0$ . For a level vector $s$ ,

X(s)=\{x\ge 0:\ v_l\le s_l,\ l=0,\dots,L-1\},

and $Z(s)$ is the set of stationary policies $z$ (an order $z(x)\ge 0$ in each state $x\ge 0$ ) with $z(x)=0$ for $x\notin X(s)$ and $v_l+z(x)\le s_l$ for $l=0,\dots,L$ and $x\in X(s)$ . The vector base-stock policy with parameter $s$ is

z_s(x)=\bigl[\min\{s_l-v_l,\ l=0,\dots,L\}\bigr]^+,

equation (5) of the paper with a general $s$ in place of Morton's $\bar s$ . Under a stationary policy $z$ , from an initial state $x$ and along a demand path $(d_t)$ , the state process is $x_0=x$ , $x_{t+1}=(x_t)_+$ with order $z(x_t)$ and demand $d_t$ . In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.

Formalization targets

Goal: Claim 1 (p. 1259)

For a level vector $s$ , a policy $z\in Z(s)$ , i.i.d. demands with law $D$ on $[0,\infty)$ and $P(d>0)>0$ , and any initial state $x\ge 0$ , almost surely

\exists\,T\ \forall\,t\ge T:\quad x_t\in X(s).

The paper's word is "transient"; the statement above says that every state outside $X(s)$ , indeed the whole complement, is visited only finitely often.

Milestones

(5) and §4: for every level vector $s$ , $z_s\in Z(s)$ .
Invariance (proof of Claim 1): $x\in X(s)$ , $z\in Z(s)$ , $d\ge 0$ imply $x_+\in X(s)$ .
Entrance (proof of Claim 1): along a demand path with $d_t\ge 0$ and $\sum_{t<n}d_t\to\infty$ , the process started at any $x\ge 0$ visits $X(s)$ .

A further item records the paper's remark that $X(s)$ and $Z(s)$ are increasing in $s$ .

Significance

Claim 1 lets the dynamic program be solved on the compact set $X(\bar s)$ with policies restricted to $Z(\bar s)$ , which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since $Z(s)$ contains the vector base-stock policies and, for $s$ large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.

The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of $X(s)$ . Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.

Difficulty

The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside $X(s)$ the policy orders nothing, so the process can only reach $X(s)$ through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with $x_0>s_0$ fixed forever) and holds only almost surely, from independence and $P(d>0)>0$ . The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.

Formalization scope

States are Fin L → ℝ with $L\ge 1$ in the goal; theorems quantify over nonnegative states. The vector $(x,z)$ is Fin.snoc x z; $v$ takes a natural-number index and vanishes at $l\ge L$ , so $v_L=0$ .
Level vectors are Fin (L+1) → ℝ, antitone with nonnegative last entry. $X(s)$ constrains $v_0,\dots,v_{L-1}$ ; $Z(s)$ constrains $v_l+z(x)$ for $l=0,\dots,L$ .
Policies are deterministic stationary functions of the state, with no measurability required. The zero condition and the sign condition of $Z(s)$ range over states $x\ge 0$ (the paper's state space); over all of $\mathbb R^L$ the vector base-stock policy would not be in $Z(s)$ .
Demand is a probability measure $D$ on $\mathbb R$ with $D((-\infty,0))=0$ ; the demand sequence is the coordinate process under Measure.infinitePi (fun _ : ℕ => D). The hypothesis $D((0,\infty))>0$ is added to the paper's assumptions; without it the claim is false.
"Transient" is read as: almost surely the state lies in $X(s)$ from some period on.
Ruled out: the goal is neither the invariance statement alone, which says nothing about states outside $X(s)$ , nor the pathwise entrance statement with divergent cumulative demand assumed, which drops the probabilistic content.

A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.

Selected references

P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5):1256–1263, 2008. https://doi.org/10.1287/opre.1070.0471
T. Morton, Bounds on the Solution of the Lagged Optimal Inventory Equation with No Demand Backlogging and Proportional Costs, SIAM Review 11:572–576, 1969 (as cited in Zipkin 2008).
T. Morton, The Near-Myopic Nature of the Lagged-Proportional-Cost Inventory Problem with Lost Sales, Operations Research 19(7):1708–1716, 1971. https://doi.org/10.1287/opre.19.7.1708
R. Levi, G. Janakiraman, M. Nagarajan, Provably Near-Optimal Balancing Policies for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research, 2008 (forthcoming at the time of Zipkin 2008).

5 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

On the Structure of Lost-Sales Inventory Models 1: In the Transformed State v = J⁻¹x, the Optimal Cost Functions f̄_t(v) and ḡ_t(v, ζ) Are L♮-ConvexResearch Paper

Motivation

The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an $L$ -dimensional vector, and no simple policy is optimal.

Its structure has a long history:

Karlin and Scarf (1958) formulated the model and showed, for lead time one and continuous demand, that the optimal order decreases in on-hand inventory with slope bounded by one.
Morton (1969) extended these qualitative properties to general lead times, again by differentiating the optimal cost function, which required smooth demand distributions.
Zipkin (2008), the paper formalized here, recovered and unified both results with a change of state variables and a single structural property, L♮-convexity, from discrete convex analysis (Murota 2003). The argument needs no smoothness and works for discrete as well as continuous demand.

Setting

Time is discrete. In each period the order due arrives, a new order $z\ge0$ is placed, demand $d\ge0$ occurs, and a holding or penalty cost is charged. The lead time $L\ge1$ is an integer. The original state $x=(x_0,\dots,x_{L-1})$ records on-hand inventory $x_0$ followed by the orders in transit. Demands are independent with a common law $\mu$ . The costs are linear and stationary: unit procurement cost $c$ , unit holding cost $\hat h$ , unit lost-sales penalty $p$ , and discount factor $\gamma$ .

The transformed state is the vector of partial sums $v_l=\sum_{k=l}^{L-1}x_k$ , $0\le l<L$ , with the convention $v_L=0$ . It ranges over the cone

V=\{v\in\mathbb R^L : v_0\ge v_1\ge\dots\ge v_{L-1}\ge 0\}.

The transformed order is $\zeta=-z\le0$ . With $e$ the all-ones vector, the state moves to

v_+=\big([v_0-v_1-d]^+ + v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e .

The one-period cost is $\hat q(u)=\hat hu^+ + pu^-$ on $u=y-d$ , where $y=v_0-v_1$ is the on-hand stock, and $\hat q^0(y)=E[\hat q(y-d)]$ . With $k$ periods to go, the optimal cost functions are

\bar f_0\equiv0,\qquad \bar g_k(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E\big[\bar f_k(v_+)\big],\qquad \bar f_{k+1}(v)=\inf_{\zeta\le0}\bar g_k(v,\zeta).

A function $\varphi$ is submodular on a set $S\subseteq\mathbb R^n$ if $\varphi(x\vee y)+\varphi(x\wedge y)\le\varphi(x)+\varphi(y)$ for all $x,y\in S$ , with $\vee,\wedge$ the componentwise maximum and minimum. A function $f:V\to\mathbb R$ is L♮-convex if $\psi(v,\zeta)=f(v-\zeta e)$ is submodular on $V\times\Re^-$ . A function $g(v,\zeta)$ on $V\times\Re^-$ is L♮-convex if $g\big((v,\zeta)-\xi(e,1)\big)$ is submodular in $(v,\zeta,\xi)$ over $v\in V$ , $\zeta\le\xi\le0$ .

Formalization targets

Goal: Theorem 4 (p. 939)

For every number of periods to go $k$ ,

\bar f_k \text{ is L♮-convex on } V \quad\text{and}\quad \bar g_k \text{ is L♮-convex on } V\times\Re^- .

The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.

Milestones, in the order the proof uses them

Lemma 1 (p. 938): if $f(v)$ is L♮-convex, so is $\psi(v,\zeta)=f(v-\zeta e)$ .
Lemma 2 (p. 939): if $g(v,\zeta)$ is L♮-convex, so is $f(v)=\min_{\zeta\le0}g(v,\zeta)$ .
Optimal filling (proof of Theorem 4): in the end-of-period program (3), filling as much demand as possible is optimal ( $a=\min\{d,v_0-v_1\}$ ). Consequently $\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+)$ .
$\psi_t$ is L♮-convex: the objective $\psi_t(v_+,v,\zeta)=\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}[(v_+,v_2,\dots,v_{L-1},0)-\zeta e]$ of program (4) is L♮-convex on its constraint set.
$\bar\kappa_t$ is L♮-convex: the end-of-period cost $\bar\kappa_t(v,\zeta\mid d)$ is L♮-convex in $(v,\zeta)$ for each $d$ .
$\bar g_t$ is L♮-convex: if $\bar f_{t+1}$ is L♮-convex, so is $\bar g_t=-\gamma^Lc\zeta+E_d[\bar\kappa_t]$ , by (5).

Significance

The result. L♮-convexity of $\bar f_t$ implies that $\bar f_t$ is submodular and convex in the transformed state. L♮-convexity of $\bar g_t$ yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order $\bar z_t(v)$ is nonincreasing in $v$ and changes by at most $\omega$ when every component of $v$ increases by $\omega$ . These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:

a formal L♮-convexity theory on real cones (the shift characterization, its preservation under partial minimization, and its preservation under expectation);
a checked version of the induction behind Theorem 4;
a verified model of the lost-sales recursion in the transformed state, which missions on Corollary 5 and the later sections can import.

Difficulty

The obvious argument works with ordinary convexity and submodularity in the original state $x$ . It stalls: the lost-sales transition $[x_0-d]^+$ is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in $x$ . The paper's structure appears only in the partial sums $v$ . Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over $\zeta$ (Lemma 2). Proving plain submodularity of $\bar f_t$ on $V$ therefore does not close the induction.

A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.

A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of $d\mapsto\bar f_k(v_+)$ , and these come from the model rather than from the definitions.

Formalization scope

Representation. States are functions Fin L → ℝ, indexed $0,\dots,L-1$ as in the paper. A helper returns $v_l$ for $l<L$ and $0$ at $l=L$ . A function $g(v,\zeta)$ is encoded on Fin (L+1) → ℝ with $\zeta$ last. The objective $\psi_t$ of (4) is encoded on Fin (L+2) → ℝ with coordinates $(v_+,v_0,\dots,v_{L-1},\zeta)$ . The order is componentwise.
L♮-convexity on a domain $D$ : $(x,\xi)\mapsto f(x-\xi e)$ is submodular on $\{\xi\le0,\ x\in D,\ x-\xi e\in D\}$ , with $e$ the all-ones vector on every coordinate. For $D=V$ this is the paper's definition verbatim. This is the paper's definition, not Murota's translation-submodularity form, and it is stated on real vectors. The platform's discrete-convexity library (DiscreteConvex.LConvexFunctions.*) works on $\mathbb Z^V$ with values in $\mathbb R\cup\{+\infty\}$ , a different domain and definition, and is not reused.
Time. Data are stationary, so the paper's $\bar f_t$ depends on $t$ only through the number of periods to go $k=T+L+1-t$ , and "for all $t$ " is "for all $k$ ". The minimum over $z\ge0$ is taken in every period, as printed in (1).
Explicit readings of the paper's phrases.
- "min" (over $\zeta\le0$ , over $v_+$ , over $(a,w)$ ) is an infimum over the constraint set. In the model every cost is nonnegative, so the infimum is genuine. The generic Lemma 2 assumes the values bounded below, and the generic milestone 5 assumes the continuation nonnegative on $V$ .
- "the $d_t$ are independent and nonnegative": one law $\mu$ with $\mu(-\infty,0)=0$ , since data are stationary.
- "unit cost", "discount rate": $c,\hat h,p\ge0$ and $0<\gamma\le1$ .
- Finite mean demand is added: without it $\hat q^0$ is infinite.
- "the optimal $a=\min\{d,v_0-v_1\}$ ": stated as the equality of the infimum of program (4) with its value at $v_+=\max(v_0-d,v_1)$ .
Ruled out. A statement that holds because a value function is the junk constant $0$ (constants are L♮-convex), plain submodularity on $V$ in place of the shift condition, quantification over all of $\mathbb R^L$ instead of $V$ , and a goal about an arbitrary function assumed to satisfy the recursion. None of these is the paper's theorem; the goal is stated for the recursion itself.
Not in scope. "L♮-convex implies convex" for a generic function, which is false without regularity (a non-measurable additive function is L♮-convex in this sense); Lemma 3 and Corollary 5, for a follow-up mission that references Theorem 4; the smooth-case Hessian discussion; the infinite-horizon remarks.
Welcome contributions. Reusable lemmas on submodularity over sublattices of $\mathbb R^n$ (partial minimization, Topkis 2.7.6), on preservation of submodularity under integration, and on measurability of the value functions.

Selected references

P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4) (2008) 937–944. https://doi.org/10.1287/opre.1070.0482
S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11(4) (1969) 572–596. https://doi.org/10.1137/1011090
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.

8 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 2: For a Compact Convex Set of Discrete Distributions, Worst-Case CVaR Equals min_α max_π G_β(x, α, π)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level $\beta$ it is, roughly, the expected loss in the worst $(1-\beta)$ fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.

That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold $\alpha$ . This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).

Setting

A decision $x \in \mathbb R^n$ incurs the loss $f(x,y)$ , where $y \in \mathbb R^m$ is random. In the discrete model $y$ takes the finitely many values $y_{[1]},\dots,y_{[S]}$ , the scenarios, with probabilities $\pi_1,\dots,\pi_S$ , where $\pi_k \ge 0$ and $\sum_k \pi_k = 1$ . Fix a confidence level $0<\beta<1$ and write $[t]^+ = \max\{t,0\}$ . The Rockafellar–Uryasev function for the distribution $\pi$ is

G_\beta(x,\alpha,\pi) = \alpha + \frac{1}{1-\beta}\sum_{k=1}^S \pi_k\,[f(x,y_{[k]})-\alpha]^+, \qquad \alpha\in\mathbb R,

and the CVaR of the loss at $x$ under $\pi$ is

\mathrm{CVaR}_\beta(x,\pi) = \min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

The distribution is not known; it is only known to lie in an ambiguity set $\mathcal P_\pi \subseteq \mathbb R^S$ of probability vectors. The worst-case CVaR at $x$ is

\mathrm{WCVaR}_\beta(x) = \sup_{\pi\in\mathcal P_\pi}\mathrm{CVaR}_\beta(x,\pi) = \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and $\mathcal P_\pi$ as a set P of vectors Fin S → ℝ.

Formalization targets

Goal: Theorem 2 (p. 1159)

If $\mathcal P_\pi$ is a nonempty compact convex set of probability vectors, then for each $x$

\mathrm{WCVaR}_\beta(x) = \min_{\alpha\in\mathbb R}\max_{\pi\in\mathcal P_\pi} G_\beta(x,\alpha,\pi),

with the inner maximum attained for every $\alpha$ and the outer minimum attained at some $\alpha_0$ . The statement fixes no constants and no particular ambiguity set.

Milestones (the steps of the paper's proof, p. 1167)

$G_\beta(x,\alpha,\pi)$ is convex in $\alpha$ for each probability vector $\pi$ and affine in $\pi$ for each $\alpha$ .
There is one nonempty closed bounded interval $\mathcal A$ such that, for every $\pi\in\mathcal P_\pi$ , $\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi) = \min_{\alpha\in\mathcal A} G_\beta(x,\alpha,\pi)$ .
Lemma 1 (p. 1157, Ky Fan's minimax theorem): for convex–concave, suitably semicontinuous $\phi$ on a product of nonempty compact convex sets, $\min_x\max_y\phi = \max_y\min_x\phi$ .
Lemma 1 on $\mathcal A\times\mathcal P_\pi$ : $\max_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathcal A}G_\beta = \min_{\alpha\in\mathcal A}\max_{\pi\in\mathcal P_\pi}G_\beta$ .
The min-max inequality $\inf_{\alpha\in\mathbb R}\sup_{\pi\in\mathcal P_\pi}G_\beta(x,\alpha,\pi) \ge \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R}G_\beta(x,\alpha,\pi)$ .

Significance

Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in $\pi$ . Minimizing $\mathrm{WCVaR}_\beta(x)$ over decisions $x$ is therefore the single minimization problem (16)–(20) of the paper in the variables $(x,u,\alpha,\theta)$ , whose only nonstandard constraint is $\max_{\pi\in\mathcal P_\pi}(\alpha+\frac{1}{1-\beta}\pi^Tu)\le\theta$ . For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of $\sup_\pi$ and $\min_\alpha$ underlies many later distributionally robust CVaR models.

The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of $G_\beta$ in $\alpha$ , the reduction of the threshold to a compact interval uniform over $\mathcal P_\pi$ , and the passage from the compact interval back to all of $\mathbb R$ .

Difficulty

The obvious approach applies a minimax theorem directly to $G_\beta$ on $\mathbb R\times\mathcal P_\pi$ . That fails because $\mathbb R$ is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every $\pi\in\mathcal P_\pi$ simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of $\mathbb R$ , which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.

Formalization scope

Conventions committed to in the Lean statements:

Scenarios are indexed zero-based by Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).
The confidence level satisfies $0<\beta<1$ in every statement (the paper says only that $\beta$ is a confidence level, usually above $0.9$ ).
$\mathrm{CVaR}_\beta(x,\pi)$ is defined as the paper does for discrete distributions, as the minimum of $G_\beta(x,\cdot,\pi)$ , encoded as the real infimum of its values; $\mathrm{WCVaR}_\beta(x)$ is the real supremum of the image of $\mathcal P_\pi$ . Both are true infima and suprema under the hypotheses carried by every theorem.
Theorem 2's hypothesis " $\mathcal P_\pi$ is a compact convex set" is completed by two standing assumptions of §2.2: $\mathcal P_\pi$ consists of probability vectors, and it is nonempty. Without the first, $G_\beta(x,\cdot,\pi)$ can be unbounded below and the real infimum returns a junk value; without the second the supremum is over the empty set.
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the paper omits and which are needed for the extrema to exist; its conclusion is a saddle point, equivalent to the attained min–max equality.
In the goal, the right-hand side exhibits an explicit minimizer $\alpha_0$ and the inner maximum is shown to be attained; neither is replaced by a bare infimum or supremum.

No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over $\alpha$ must be witnessed.

The development needs only finite sums, convexity on $\mathbb R$ and on the simplex, compactness of $\mathcal P_\pi$ and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax Theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 1: Under Mixture Distribution Uncertainty, Worst-Case CVaR Equals the Minimum over α of max_i F^i_β(x, α)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level $\beta$ is the minimum over a scalar $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.

The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set $\mathcal P$ of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of $\mathcal P$ , minimizing it remains a tractable convex program. This mission formalizes the first of these results, for $\mathcal P$ the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.

Setting

A decision $x\in\mathbb R^n$ and a random vector $y\in\mathbb R^m$ determine a loss $f(x,y)\in\mathbb R$ . A confidence level $\beta$ satisfies $0<\beta<1$ (in applications $\beta\ge0.9$ ). Write $[t]^+=\max\{t,0\}$ .

For a probability distribution $P$ of $y$ under which $f(x,\cdot)$ is integrable, the Rockafellar–Uryasev function is

F_\beta(x,\alpha)=\alpha+\frac1{1-\beta}\int_{\mathbb R^m}[f(x,y)-\alpha]^+\,dP(y),\qquad\alpha\in\mathbb R, \tag{1}

and CVaR is its minimum over $\alpha$ :

\mathrm{CVaR}_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha). \tag{2}

Fix $l\ge1$ likelihood distributions $P^1,\dots,P^l$ on $\mathbb R^m$ and let $\Lambda=\{\lambda\in\mathbb R^l:\lambda_i\ge0,\ \sum_i\lambda_i=1\}$ be the probability simplex. The ambiguity set is the set of mixtures

\mathcal P_M=\Big\{\textstyle\sum_{i=1}^l\lambda_iP^i:\ \lambda\in\Lambda\Big\},

and the worst-case CVaR of $x$ is

\mathrm{WCVaR}_\beta(x)=\sup_{\lambda\in\Lambda}\ \mathrm{CVaR}_\beta(x)\ \text{ under }\ \textstyle\sum_i\lambda_iP^i. \tag{3}

Write $F^i_\beta(x,\alpha)$ for the function (1) with $P=P^i$ , $F^{\mathcal L}_\beta(x,\alpha)=\max_{i\in\mathcal L}F^i_\beta(x,\alpha)$ with $\mathcal L=\{1,\dots,l\}$ , and $H_\beta(x,\alpha,\lambda)$ for the function (1) of the mixture $\sum_i\lambda_iP^i$ .

Formalization targets

Goal: Theorem 1

For every $x$ with $f(x,\cdot)$ integrable under every $P^i$ ,

\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\ \max_{i\in\mathcal L}F^i_\beta(x,\alpha),

with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of $l$ functions on the right.

Milestones

The milestones follow the paper's appendix proof (pp. 1166–1167) in order:

(53): $H_\beta(x,\alpha,\lambda)=\sum_i\lambda_iF^i_\beta(x,\alpha)$ for $\lambda\in\Lambda$ .
(54): $\mathrm{WCVaR}_\beta(x)=\max_{\lambda\in\Lambda}\min_{\alpha}H_\beta(x,\alpha,\lambda)$ , both extrema attained.
The minimizer set of $F_\beta(x,\cdot)$ is a nonempty closed bounded interval $[\underline\alpha^*,\overline\alpha^*]$ .
Minimizers of a nonnegative combination of two convex functions on $\mathbb R$ lie between the extreme endpoints of their minimizer intervals.
Every minimizer of $H_\beta(x,\cdot,\lambda)$ lies in $\mathcal A=[\min_i\underline\alpha^*_i,\max_i\overline\alpha^*_i]$ , and the minimum over $\mathbb R$ is attained in $\mathcal A$ .
Lemma 1, the minimax equality for convex–concave functions on compact convex sets.
(55): $\max_\lambda\min_{\mathbb R}H_\beta=\max_\lambda\min_{\mathcal A}H_\beta=\min_{\mathcal A}\max_\lambda H_\beta$ .
(56)–(57): $\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)$ .
(58)–(59): $\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)=\max_iF^i_\beta(x,\alpha)$ .

An additional item states Corollary 1: $(x^*,\alpha^*)$ minimizes $F^{\mathcal L}_\beta$ over $\mathcal X\times\mathbb R$ exactly when $x^*$ minimizes $\mathrm{WCVaR}_\beta$ over $\mathcal X$ and $\alpha^*$ minimizes $F^{\mathcal L}_\beta(x^*,\cdot)$ .

Significance

The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each $F^i_\beta$ is jointly convex in $(x,\alpha)$ when $f$ is convex in $x$ , $F^{\mathcal L}_\beta$ is convex, and Corollary 1 turns robust CVaR minimization into one convex program in $(x,\alpha)$ ; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of $F_\beta$ is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.

Difficulty

The obvious argument is to exchange $\sup_\lambda$ and $\min_\alpha$ in $\sup_\lambda\min_\alpha\sum_i\lambda_iF^i_\beta(x,\alpha)$ , since the function is convex in $\alpha$ and affine in $\lambda$ . Minimax theorems for this exchange need compactness of one of the two sets, and the variable $\alpha$ ranges over all of $\mathbb R$ . The step that has to be supplied is a localization: all minimizers in $\alpha$ , for every $\lambda$ at once, lie in one compact interval $\mathcal A$ determined by the minimizer sets of the components. This in turn requires knowing that each $F^i_\beta(x,\cdot)$ has a nonempty bounded minimizer set, which uses $0<\beta<1$ and integrability of the loss: at $\beta=0$ the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over $\Lambda$ is a maximum only because the inner minimum depends continuously on $\lambda$ .

Formalization scope

Distributions are probability measures on Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].
Every theorem assumes $0<\beta<1$ , that each $P^i$ is a probability measure, and that $f(x,\cdot)$ is integrable under each $P^i$ (the paper's $E|f(x,y)|<\infty$ ).
CVaR is defined by (2) as the infimum of the values of $F_\beta(x,\cdot)$ ; the tail-mean definition and the Rockafellar–Uryasev identity between the two are not part of the mission. The mixture is the finite sum of measures $\sum_i\lambda_iP^i$ , $\Lambda$ is Mathlib's stdSimplex, and WCVaR is the supremum of the image of $\Lambda$ .
Every min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value $0$ .
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the printed statement omits and without which the extrema need not exist.
The definitions $F_\beta$ , CVaR, mixture and WCVaR are reusable for any risk-measure development; the interval property of $\arg\min F_\beta$ is of independent use. Proofs of any milestone, and lemmas on the Rockafellar–Uryasev function for general measures, are welcome.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

11 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

A Scheduling Model for Reduced CPU Energy: For P(s) = s², the Average Rate Heuristic Has Competitive Ratio Between 4 and 8Research Paper

Why processor speed changes the scheduling problem

A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.

The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function $P(s)$ , so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.

Jobs, schedules, and the average-rate rule

Fix a nondegenerate time window $[t_0,t_1]$ . A finite job instance $J$ assigns each job $j$ an arrival time $a_j$ , deadline $b_j>a_j$ , and nonnegative required work $R_j$ in CPU cycles. Every job window $[a_j,b_j]$ lies inside $[t_0,t_1]$ . A schedule $S=(s,\operatorname{job})$ has nonnegative processor speed $s(t)$ and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:

\int_{a_j}^{b_j}s(t)\,\mathbf 1\{\operatorname{job}(t)=j\}\,dt=R_j \qquad\text{for every }j.

For a power function $P$ , its energy is $E_P(S)=\int_{t_0}^{t_1}P(s(t))\,dt$ . An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval $[z,z']$ is the total work of jobs whose full windows it contains, divided by $z'-z$ . An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.

Each job's density is $d_j=R_j/(b_j-a_j)$ , extended as a step function equal to $d_j$ on $[a_j,b_j]$ and zero elsewhere. AVR runs at speed $\sum_j d_j(t)$ and chooses the earliest-deadline available job. For quadratic power, its energy is

\operatorname{AVR}(J)=\int_{t_0}^{t_1}\left(\sum_jd_j(t)\right)^2dt.

The competitive ratio is the least upper bound of $\operatorname{AVR}(J)/\operatorname{OPT}(J)$ over instances, where $\operatorname{OPT}(J)$ is the least feasible energy §4, p. 376, Eq. (2).

Formalization targets

The goal is the paper's Theorem 2, p. 381:

4\le r\le 8\qquad(P(s)=s^2).

The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.

The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives $F_A\le4\operatorname{OPT}_A$ and $F_B\le4\operatorname{OPT}_B$ ; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real $p\ge2$ :

p^p\le r_p\le 2^{p-1}p^p.

That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.

What the bounds provide

The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.

The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.

The main difficulty

The simple calculation $\left(\sum_j d_j(t)\right)^2$ exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.

Formalization scope

Jobs use Fin n, allowing the empty instance. The instance requires $t_0<t_1$ , $a_j<b_j$ , containment in the window, and $R_j\ge0$ . A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.

Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.

Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent $e\ge1$ , the limiting ratios at $e=1$ and $e=3/2$ , and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.

The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.

Selected references

Frances Yao, Alan Demers, and Scott Shenker, A Scheduling Model for Reduced CPU Energy, Proceedings of the 36th IEEE Symposium on Foundations of Computer Science, 1995, pp. 374–382. DOI 10.1109/SFCS.1995.492493.

19 thms2 active usersReviewed

Analysis Operations Research Probability+1·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 4: Time Reversal Is a J₁ Isometry and Reversal from the Origin Is 2-LipschitzResearch Paper

Why time reversal matters

Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).

The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod $J_1$ distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).

Paths, distances, and reversal

Let $S$ be a complete separable metric group, written additively, with identity $0$ and metric $m$ . The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let $D$ contain the càdlàg paths $x:[0,1]\to S$ , meaning paths that are right continuous and possess left limits. Section 8 additionally requires $x(1)=x(1-)$ , so the terminal value agrees with the value approached from earlier times. Let $D_\theta=\{x\in D:x(0)=0\}$ . These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).

The uniform distance is $\rho(x,y)=\sup_{0\le t\le1}m(x(t),y(t))$ . A time change $\lambda\in\Lambda$ is an increasing homeomorphism of $[0,1]$ onto itself; $e(t)=t$ is the identity time change. The $J_1$ distance used in the paper is

d(x,y)=\inf_{\lambda\in\Lambda} \max\{\rho(\lambda,e),\rho(x,y\circ\lambda)\}.

Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent $J_1$ metric (Whitt 1980, p. 70).

The reverse-time map reads the left limit at the reflected time:

R(x)(t)= \begin{cases} x((1-t)-),&0\le t<1,\\ x(0),&t=1, \end{cases} \qquad r(x)(t)=R(x)(t)-x(1).

The left limit is essential: the direct value $x(1-t)$ places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives $R(x)(0)=x(1)$ , so $r(x)(0)=0$ . Whitt also uses the reflected time change $(-r)(\lambda)(t)=1-\lambda(1-t)$ in the proof (Whitt 1980, pp. 83–84).

Formalization targets

The goal is Whitt's Theorem 8.1. For every $x,y\in D$ ,

d(Rx,Ry)=d(x,y),\qquad d(rx,ry)\le 2d(x,y).

The second inequality also applies when both paths lie in $D_\theta$ , since $D_\theta\subseteq D$ . The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).

The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in $\Lambda$ ; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through $(-r)(\lambda)$ . Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).

What the result gives

An isometry preserves every $J_1$ distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for $r$ makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.

Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for $D$ .

Mathematical difficulty

The immediate idea $t\mapsto x(1-t)$ does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without $x(1)=x(1-)$ , the shifted reverse path need not start at the identity. The $J_1$ assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).

Formalization scope

Lean represents paths as total functions $\mathbb R\to S$ ; all path conditions, metrics, and equality claims read only $[0,1]$ . Càdlàg membership requires right continuity and left limits within the interval, with $x(1)=x(1-)$ included in $D$ . Completeness and separability are explicit because the paper calls $S$ a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by $S=\mathbb R^k$ ; the paper uses additive notation but does not separately state commutativity.

The paper's $\Lambda$ is encoded by strict increase, continuity, and surjectivity on $[0,1]$ , which characterize increasing homeomorphisms there. The paper's $d$ is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for $\rho$ and $d$ , avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping $D$ membership: it is an explicit hypothesis, and the zero path over $\mathbb R$ satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the $J_1$ distance $d$ , not the uniform distance $\rho$ , and $R$ reads the left limit $x((1-t)-)$ , not the value $x(1-t)$ .

The proof's first sentence says the maps are one-to-one and onto. The map $r:D\to D_\theta$ forgets an additive offset and is not injective on all of $D$ ; the formal milestone expresses involution for $R$ on $D$ and for the restriction of $r$ to $D_\theta$ . One identity printed for $r$ with $x\in D_\theta$ also holds for every $x\in D$ ; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.

Selected references

Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67.

7 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 2: An Envelope of Order γ and Tsybakov Noise Exponent q Give Geometric Noise Exponent (q+1)γ/dResearch Paper

Motivation

A binary classifier is learned from a sample of a distribution $P$ on $X \times \{-1, 1\}$ , and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on $P$ no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard $P$ is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function $\eta(x) = P(y = 1 \mid x)$ .

Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure $|2\eta - 1|\,dP_X$ lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on $\eta$ near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.

Setting

Let $X \subset \mathbb R^d$ be compact and let $P$ be a distribution on $X \times \{-1, 1\}$ with marginal $P_X$ and regression function $\eta(x) = P(y = 1 \mid x) \in [0, 1]$ . The classes of $P$ are $X_{-1} = \{\eta < \tfrac12\}$ , $X_1 = \{\eta > \tfrac12\}$ and $X_0 = \{\eta = \tfrac12\}$ , all intersected with $X$ . The distance to the decision boundary is

\tau_x = d(x, X_0 \cup X_1) \text{ on } X_{-1}, \qquad \tau_x = d(x, X_0 \cup X_{-1}) \text{ on } X_1, \qquad \tau_x = 0 \text{ otherwise},

with $d(x, A)$ the Euclidean distance of $x$ to $A$ (equation (7), p. 7).

Tsybakov noise exponent $q \in [0, \infty]$ (Definition 2.2, p. 6): for some $C > 0$ and all sufficiently small $t > 0$ , $P_X(|2\eta - 1| \le t) \le C t^q$ .
Geometric noise exponent $\alpha > 0$ (Definition 2.3, p. 7): for some $C > 0$ ,

\int_X |2\eta(x) - 1|\, e^{-\tau_x^2/t}\, P_X(dx) \le C\, t^{\alpha d/2}, \qquad t > 0.

Envelope of order $\gamma > 0$ (Definition 2.5, p. 8): for some $c_\gamma > 0$ , $|2\eta(x) - 1| \le c_\gamma \tau_x^\gamma$ for $P_X$ -almost all $x \in X$ .

In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.

Formalization targets

Goal: Theorem 2.6 (p. 8)

If $P$ has an envelope of order $\gamma > 0$ and Tsybakov noise exponent $q \in [0, \infty)$ , then

q \ge 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \frac{(q+1)\gamma}{d}, \qquad 0 \le q < 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \alpha \text{ for all } 0 < \alpha < \frac{(q+1)\gamma}{d}.

Both clauses are stated, as one conjunction.

Milestones

Display (33), pp. 18–19. Under the Tsybakov bound for all $s > 0$ with constant $C$ and the envelope bound with constant $c_\gamma$ , for all $t > 0$ and $\tau \ge 0$ :

\mathbb E_{P_X}\big(|2\eta - 1|\, e^{-\tau_x^2/t}\big) \le C\tau^{q+1} + \exp\big(-(\tau/c_\gamma)^{2/\gamma} t^{-1}\big).

The $\tau$ -estimate, p. 19. With $\hat a = c_\gamma^{2/\gamma}(q+1)$ , for all small $t > 0$ the equation $\tau^{q+1} = \exp(-(\tau/c_\gamma)^{2/\gamma}t^{-1})$ has a positive solution, and every positive solution satisfies $\tau \le (\hat a\gamma/2)^{\gamma/2}\,(t\ln\frac{1}{\hat a t})^{\gamma/2}$ .
Theorem 2.6, case $0 \le q < 1$ .
Theorem 2.6, case $q \ge 1$ .

Significance

Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of $\eta$ at the decision boundary. Example: with $d = 1$ , $X = [-1, 1]$ , $P_X$ uniform and $\eta(x) = (1 + x)/2$ , the distribution has envelope order $1$ and Tsybakov exponent $1$ , hence geometric noise exponent $2$ .

The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, $\tau_x$ and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.

Difficulty

The case $0 \le q < 1$ is elementary once the right splitting level is chosen: the expectation is split at a level $\tau$ of $|2\eta - 1|$ , and $\tau$ is then tuned to $t$ . Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value $(q+1)\gamma/d$ , but not the critical value itself: a logarithmic factor is lost.

Reaching the critical exponent when $q \ge 1$ is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces $L_{q,\infty}$ and $L_{q',1}$ and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of $|2\eta - 1|$ . The obvious approach, the same splitting as for $q < 1$ , does not work: it always loses the logarithm.

Formalization scope

Representation of $P$ . $P$ is given by $\mu = P_X$ , a probability measure on EuclideanSpace ℝ (Fin d) with $\mu(X^c) = 0$ , and a measurable version $\eta$ of the regression function with values in $[0,1]$ everywhere. Every Borel distribution on $X \times \{-1,1\}$ has this form, and the paper defines $\tau_x$ "for some choice of $\eta$ ".
Pinned convention $d(x, \emptyset) := 0$ . The paper leaves $d(x, \emptyset)$ undefined. Lean's Metric.infDist gives $0$ . For Theorem 2.6 both readings give a true statement. Under the reading $\infty$ , the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of $\eta$ with an empty class. The convention is chosen for agreement with the companion mission.
Integrals. All integrals are $[0,\infty]$ -valued Lebesgue integrals of nonnegative integrands (lintegral), so a bound can never hold through a junk value of a non-integrable function.
Added hypotheses. $d \ge 1$ , because the exponent $(q+1)\gamma/d$ divides by $d$ . In the second clause, $\alpha > 0$ : this is the range of Definition 2.3, not a new restriction.
Display (33). It is stated for every $q \ge 0$ , where it holds verbatim, and for $t > 0$ (the page writes $t \ge 0$ , but $t^{-1}$ is undefined at $0$ ). Its hypotheses are the all- $t$ form of (5), which by the remark on p. 6 is equivalent to Definition 2.2 for $q < \infty$ up to the constant, and (10) with its constant named. The page's equality that splits the integral is not stated separately.
Printed slip. The proof on p. 19 ends "for the case $0 < q < 1$ ", while the statement covers $q = 0$ . The milestone is stated for $0 \le q < 1$ ; the argument works verbatim at $q = 0$ .
Small $t$ . In Definition 2.2, "sufficiently small" is a threshold $t_0 \in (0,1)$ . The $\tau$ -estimate has its threshold chosen before $t$ and $\tau$ , and it also states the existence of a solution, which the page presupposes.
No trivializing reading. The hypotheses are satisfiable: the example in Significance meets all of them. $\tau_x$ is not identically $0$ there, since it equals $|x|$ . So the goal cannot hold vacuously.
Not formalized. The Lorentz-space step (30) and the rearrangement estimate (32) are not milestones. Contributions of Lorentz quasi-norms or a layer-cake lemma are welcome as supporting theorems.

The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.

Selected references

I. Steinwart, C. Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 575–607, 2007. arXiv reprint: https://arxiv.org/abs/0708.1838 ; DOI: https://doi.org/10.1214/009053606000001226
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Bounded Rationality in Newsvendor Models I: Under Uniform Demand the Logit Newsvendor's Order Is Truncated Normal and Its Mean Is Pulled from x* Toward the MidpointResearch Paper

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $x$ units at unit cost $c$ before a random demand $D$ is observed, sells $\min(D, x)$ units at price $p$ , and loses unsold units. Its optimal order is the critical fractile $x^* = F^{-1}(1 - c/p)$ of the demand distribution $F$ . Laboratory experiments show that human subjects do not order $x^*$ . Schweitzer and Cachon (Management Science 46(3), 2000) gave subjects uniform demand on $[0, 300]$ and found that the average order lay below $x^*$ for a high-margin product and above $x^*$ for a low-margin product: orders are pulled toward the center of the demand range.

Su (Manufacturing & Service Operations Management 10(4), 2008) explains this pattern with a model of bounded rationality: the decision maker does not pick the best order with certainty, but picks better orders more often, through a logit choice rule. This mission formalizes the first results of that paper, the case of uniform demand, where the logit order has an explicit law and the pull toward the center can be proved exactly. The source is the published MSOM 2008 article; all page numbers are its printed pages.

Setting

A decision maker with utility $u$ over an interval $S \subseteq \mathbb R$ and bounded-rationality parameter $\beta > 0$ makes a random choice $Y$ with the logit density

\psi(y) = \frac{e^{u(y)/\beta}}{\int_S e^{u(v)/\beta}\,dv}, \qquad y \in S,

and $\psi(y) = 0$ off $S$ (eq. (2), p. 571). Large $\beta$ means noisy choices; small $\beta$ concentrates the choice near the maximizer of $u$ .

In the newsvendor problem the price $p$ and unit cost $c$ satisfy $0 < c < p$ . Demand $D$ has density $f$ and distribution function $F$ . The expected profit of ordering $x$ units is

\pi(x) = p\,\mathbb E\min(D, x) - c x \qquad \text{(eq. (3), p. 572)},

and the optimal solution $x^*$ is its maximizer. The behavioral solution $X^\flat$ is the logit choice with utility $u = \pi$ over the decision domain $S$ , the smallest interval containing the support of $f$ (eq. (4), p. 572).

This mission takes uniform demand $D \sim U[a, b]$ with $b > a \ge 0$ : $f = 1/(b-a)$ on $[a, b]$ and $S = [a, b]$ . The midpoint of the demand range is $m = (a + b)/2$ . Two parameters recur:

\mu = b - \frac{c}{p}(b - a), \qquad \sigma^2 = \beta\,\frac{b-a}{p}.

A truncated normal law on $[a, b]$ with parameters $\mu, \sigma^2$ has density proportional to $e^{-(x-\mu)^2/2\sigma^2}$ on $[a, b]$ and zero elsewhere (eq. (37), p. 586). Write $\phi$ and $\Phi$ for the standard normal density and distribution function.

Formalization targets

Goal: Proposition 3 (p. 577), midpoint bias

x^* > m \implies \mathbb E X^\flat < x^*, \qquad x^* < m \implies \mathbb E X^\flat > x^*.

The goal is stated for every $\beta > 0$ and every $0 < c < p$ , with $x^*$ any maximizer of $\pi$ over $\mathbb R$ ; it fixes only the sign of the bias, not its size.

Milestones

Eq. (5), p. 572. On $[a, b]$ , $\pi(x) = Ax^2 + Bx + C$ with $A = -p/(2(b-a))$ , $B = pb/(b-a) - c$ , $C = -pa^2/(2(b-a))$ .
The optimum, pp. 572–573. $\pi$ is maximized over $\mathbb R$ exactly at $\mu$ , and $F(\mu) = 1 - c/p$ , so $x^* = F^{-1}(1 - c/p) = \mu$ .
Proposition 1, pp. 572–573. The density of $X^\flat$ equals the truncated normal density on $[a,b]$ with parameters $\mu$ and $\sigma^2$ .
Corollary 1, p. 573.

\mathbb E X^\flat = \mu - \sigma\,\frac{\phi((b-\mu)/\sigma) - \phi((a-\mu)/\sigma)}{\Phi((b-\mu)/\sigma) - \Phi((a-\mu)/\sigma)}. \qquad (8)

Significance

Proposition 3 gives a single mechanism, noise in the choice of the order, that produces both directions of the bias observed by Schweitzer and Cachon: under uniform demand, a high-profit product ( $x^* > m$ ) is underordered on average and a low-profit product ( $x^* < m$ ) is overordered. Proposition 1 gives the full law of the boundedly rational order, which is what makes the model testable: the paper fits the truncated normal law to experimental order data and estimates $\beta$ (§5). Corollary 1 is the closed-form mean used in that fit and in Proposition 3.

These results are proved in the paper by direct computation; none of them has a machine-checked proof. The mission adds a checked development of the continuous logit choice model on an interval, of the truncated normal law and its mean, and of the uniform-demand newsvendor profit, together with exact statements of what the paper's informal phrases mean (see Formalization scope).

Difficulty

Each step is elementary on paper, but the formal content sits in the integrals. Expected sales $\mathbb E\min(D, x)$ must be computed as a piecewise integral to obtain eq. (5), and the maximizer must be identified over all of $\mathbb R$ , not only on $[a, b]$ , which needs the profit outside the support as well. Proposition 1 is an identity between two normalized densities, so both normalizing integrals must be shown positive and finite. Corollary 1 requires the mean of a truncated Gaussian in terms of Mathlib's Gaussian density and distribution function, which is not in Mathlib. For Proposition 3, the natural shortcut "the mean of a truncated normal is $\mu$ " is false whenever $\mu \ne m$ , and it is exactly the asymmetry of the truncation that produces the bias.

Formalization scope

All quantities are real numbers, with the paper's standing assumptions as hypotheses: $b > a \ge 0$ , $0 < c < p$ (the page states $p > c$ ; $c > 0$ is read so that $x^*$ lies inside $(a, b)$ ), and $\beta > 0$ (eq. (2) divides by $\beta$ ; $\beta = 0$ , perfect rationality, is a limit, not a value of the formula). The decision domain is the closed interval $[a, b]$ ; the logit density is zero off it, and expectations are integrals over $\mathbb R$ . The parameter $\sigma$ is the positive square root of $\beta(b-a)/p$ , and $\phi$ , $\Phi$ are Mathlib's gaussianPDFReal 0 1 and the distribution function of gaussianReal 0 1.

Corrections and readings relative to the printed text:

Eq. (5) is stated for $x \in [a, b]$ only; outside it $\pi$ is linear.
Proposition 1 says the truncated normal has "mean $\mu$ and variance $\sigma^2$ "; these are the parameters before truncation (as in eq. (37)), and the statement is the equality of densities. The mean of $X^\flat$ is (8), not $\mu$ .
In Proposition 3, " $f$ constant over $[a, b]$ " is read as uniform demand on $[a,b]$ , as in its proof. The conclusions are inequalities on $\mathbb E X^\flat$ , because the §6 preamble (p. 577) defines "overorders" and "underorders" with the inequalities swapped relative to the proof (p. 586); the formal statement follows the proof.

The optimal solution $x^*$ in the goal is a hypothesis that $x^*$ maximizes $\pi$ over $\mathbb R$ , never a variable set to a closed form by fiat; milestone 2 shows the hypothesis is satisfiable and identifies $x^*$ . No statement holds vacuously through a junk value: on $[a, b]$ with $a < b$ the logit normalizer is the integral of a continuous positive function over an interval of positive length, and the denominator of (8) is positive because $\sigma > 0$ .

Reusable beyond this mission: the logit density on an interval, the truncated normal density, and its mean formula. Proofs of any milestone, and of the mean of a truncated normal law in general, are welcome.

Selected references

X. Su, Bounded Rationality in Newsvendor Models, Manufacturing & Service Operations Management 10(4):566–589, 2008. https://doi.org/10.1287/msom.1070.0200
M. E. Schweitzer, G. P. Cachon, Decision Bias in the Newsvendor Problem with a Known Demand Distribution: Experimental Evidence, Management Science 46(3):404–420, 2000. https://doi.org/10.1287/mnsc.46.3.404.12070

8 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Understanding the Efficiency of Multi-Server Service Systems II: In the M/M/s Queue with (1 − ρ)√s = γ, the Wait of a Delayed Customer Is Exponential with Mean 1/(γ√s)Research Paper

Motivation

A service system with several servers can use a larger fraction of its capacity than a single-server system while still giving customers an acceptable wait. The design question is how much unused capacity is needed as the number of servers grows. Ward Whitt's study begins with a factory manager deciding whether to put four machines in one work area. It uses queueing models to connect the number of machines, their utilization, and the delays customers experience. The proposed utilization rule, $(1-\rho)\sqrt{s}=\gamma$ , keeps the unused fraction $1-\rho$ proportional to $1/\sqrt{s}$ as the number of servers $s$ changes (Whitt 1992, pp. 708–710).

The paper distinguishes the chance that a customer waits at all from the length of the wait once a delay occurs. That distinction matters when a staffing choice must control a long wait rather than merely the fraction of customers who wait. The exact $M/M/s$ result in §3.1 gives a benchmark for the paper's later approximations to more general arrival and service processes (Whitt 1992, pp. 719–720).

Setting

An $M/M/s$ queue has Poisson arrivals at rate $\lambda$ , $s$ identical servers, independent exponential service times, unlimited waiting room, and first-come first-served service. Time is measured so that each server's service rate is one. The server utilization is $\rho=\lambda/s$ . We consider $s\geq1$ and $0<\lambda<s$ , so the queue has a stationary distribution. Let $p_n$ be the stationary probability that $n$ customers are in the system. Its state process is a birth–death process: arrivals occur at rate $\lambda$ and departures from state $n$ occur at rate $\min(n,s)$ .

Let $W$ be an arriving customer's steady-state time in the queue before service begins. An arrival finding fewer than $s$ customers starts service at once. An arrival finding $s+j$ customers waits for $j+1$ service completions while all servers are occupied. In the formal model, the law of $W$ has an atom at zero of mass $\sum_{n<s}p_n$ and, for each $j\geq0$ , a gamma component with shape $j+1$ , rate $s$ , and weight $p_{s+j}$ . The arrival-state weights use the Poisson-arrivals-see-time-averages property. This construction represents the FCFS waiting time independently of any claim about its eventual conditional distribution.

For an event $W>0$ of positive probability, $\mathcal L(W\mid W>0)$ denotes the conditional waiting-time law. The paper calls a customer delayed exactly when $W>0$ . The scale parameter $\gamma$ is defined by the utilization equation $(1-\rho)\sqrt{s}=\gamma$ ; because $\rho<1$ , this equation makes $\gamma$ positive.

Formalization targets

The supporting target is the §3.1 statement that a delayed customer's waiting time is exponential with rate $s(1-\rho)$ , equivalently with mean $1/[s(1-\rho)]$ :

\mathcal L(W\mid W>0)=\operatorname{Exp}\bigl(s(1-\rho)\bigr).

The goal is Proposition 3.1 under the utilization equation. It records both the entire conditional tail and its mean, for every $x\geq0$ :

\mathbb P(W>x\mid W>0)=e^{-\gamma\sqrt{s}\,x}, \qquad \mathbb E[W\mid W>0]=\frac{1}{\gamma\sqrt{s}}.

The goal also asserts $\mathbb P(W>0)>0$ , so these conditional quantities are defined. The scan of Proposition 3.1 prints the exponent without $x$ and the mean denominator with $\sqrt2$ ; the statement here uses the values determined by the preceding exponential-law sentence and by the paragraph following the proposition (Whitt 1992, pp. 719–720).

Significance

The result gives an exact delay distribution for the Markovian multi-server system. With $s$ servers and the utilization equation held fixed, the conditional tail at any positive threshold and the mean wait of a delayed customer both depend on $s$ through $\gamma\sqrt{s}$ . Thus the same rule that organizes the probability-of-delay discussion has a definite implication for customers who actually wait. It is also the exact comparison point for the paper's later, explicitly approximate analysis of general $G/G/s$ queues (Whitt 1992, §3.2).

Formalizing this result supplies a reusable representation of the stationary FCFS waiting-time law as a mixture of Erlang distributions, together with a precise connection between birth–death state probabilities and delay. The related platform items QueueingFundamentals.BirthDeath.mmc_steady_state and QueueingFundamentals.BirthDeath.erlang_c_formula state the stationary state probabilities and the probability of delay, respectively; both are open and neither states this waiting-time law. The open QueueingFundamentals.BirthDeath.halfin_whitt concerns the heavy-traffic limit for the $M/M/c$ case, a different target. The current result is known mathematically from Whitt's 1992 paper; this mission asks for its machine-checked proof in the specified model.

Difficulty

The conditional distribution is not immediate from an individual service time. A delayed arrival can encounter any queue length $s+j$ , so its waiting time is a gamma law whose shape varies with $j$ . The stationary probabilities provide the weights of infinitely many such components. Showing that this whole mixture has one exponential law requires a relation among the stationary tail probabilities and control of the infinite sum. The same mixture must have a well-defined first moment for the conditional mean formula.

Formalization scope

Lean uses a natural number $s\geq1$ , a real arrival rate $0<\lambda<s$ , and a real sequence $p_n$ satisfying the published QueueingFundamentals.BirthDeath.IsSteadyState predicate with constant birth rate $\lambda$ and death rate $\min(n,s)$ . That predicate includes nonnegativity, total mass one, and the global balance equations. Its published definition is imported as a reference. Service rate is exactly one, as fixed in §2.1 of the paper. The conditional waiting-time law is a measure on real time, with a point mass at zero and a countable gamma mixture. The positive-time restriction of this measure expresses conditioning in the milestone; real measure values and an integral express the tail and mean in the goal.

The formal hypotheses spell out positive arrival rate, at least one server, and subcritical utilization. These make the stationary law and the positive exponential rate meaningful. The goal states positive delay probability before dividing by it. The waiting-time law is built from stationary queue lengths and service completions, rather than being defined as exponential; proving that it becomes exponential is the mathematical task. Solvers may develop reusable measure-mixture identities, stationary-tail facts, and gamma or exponential distribution results. The approximation formulas of §3.2 and the paper's numerical tables are outside this mission.

Selected references

Ward Whitt, Understanding the Efficiency of Multi-Server Service Systems, Management Science 38(5):708–723, 1992. DOI: 10.1287/mnsc.38.5.708.

4 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research III: Minimum Average Journey Time on Alternative Routes — Equal Marginal Times ε and the Closed Forms (32)–(33)Research Paper

Motivation

J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259) introduced the two criteria that still organise traffic assignment. When a flow of traffic can choose between several routes from one origin to one destination, the paper (p. 345) considers two ways the traffic might divide:

the journey times on all the routes actually used are equal, and less than those that a single vehicle would experience on any unused route;
the average journey time is a minimum.

The first is now called Wardrop's first principle, or user equilibrium: no driver can shorten their trip by switching route. The second, Wardrop's second principle, is the system optimum: it "minimizes the vehicle-hours spent on the journey". The gap between the two is the quantity later studied as the price of anarchy of selfish routing (Roughgarden and Tardos, J. ACM 2002), and the marginal-cost characterisation of the system optimum underlies congestion pricing (Beckmann, McGuire and Winsten, Studies in the Economics of Transportation, 1956).

This mission formalizes the paper's solution of criterion (2) on parallel routes, section (2) Minimum Average Time, pp. 345–347. Mission II of the same series treats criterion (1) on the same model.

Setting

A total additional flow $Q$ is divided among $D$ alternative routes $i = 1, \dots, D$ . Route $i$ carries an additional flow $q_i$ and has journey time, equation (22),

t_i(q_i) = \frac{b_i}{1 - q_i/p_i},

where $b_i > 0$ is the journey time on route $i$ with no additional flow and $p_i > 0$ is the additional flow at which its speed would fall to zero (routeTime b p i x). A feasible split of $Q$ is a vector $q$ with $0 \le q_i < p_i$ for every $i$ and $\sum_i q_i = Q$ (IsFeasible p Q q).

The number of additional vehicles on route $i$ at an instant is $z_i = q_i t_i$ , and $Z = \sum_i z_i$ (totalExtra b p q). The average journey time is, equations (25)–(26),

T = \sum_{i=1}^D \frac{q_i t_i}{Q} = \frac{Z}{Q}

(avgTime b p Q q). Criterion (2) asks for a feasible split $q$ with $T(q) \le T(z)$ for every feasible split $z$ (IsMinAvgTime b p Q q).

The marginal journey time of route $i$ is $d(q_i t_i)/dq_i$ , the rate at which $Z$ grows when flow is added to that route. For a threshold $\varepsilon$ , $U(\varepsilon) = \{i : b_i < \varepsilon\}$ (usedSet b ε) is the set of routes whose marginal time at zero flow lies below $\varepsilon$ ; with the routes labelled so that $b_1 < \dots < b_D$ it is the paper's "first $j$ routes".

Formalization targets

Goal: the closed forms (32)–(33)

For $b_i, p_i > 0$ and $0 < Q < \sum_i p_i$ , every split $q$ minimizing $T$ admits a threshold $\varepsilon > 0$ with $\sum_{i \in U} p_i > Q$ , where $U = U(\varepsilon)$ , such that

q_h = \begin{cases} p_h\left\{1 - \dfrac{\left(\sum_{i\in U} p_i - Q\right)\sqrt{b_h}}{\sum_{i\in U} p_i\sqrt{b_i}}\right\}, & b_h < \varepsilon,\\[1ex] 0, & \text{otherwise,}\end{cases} \qquad T = \frac1Q\left\{\frac{\left(\sum_{i\in U} p_i\sqrt{b_i}\right)^2}{\sum_{i\in U} p_i - Q} - \sum_{i\in U} p_i b_i\right\}.

Milestones

(29)–(30): $d(q_i t_i)/dq_i = b_i/(1 - q_i/p_i)^2$ , equal to $b_i$ at $q_i = 0$ .
(27)–(28): at a minimum, all routes in use have the same marginal time $\varepsilon$ .
A route $j$ with $b_j \ge \varepsilon$ is not used.
The routes in use are exactly those with $b_i < \varepsilon$ , and on them $1 - q_i/p_i = \sqrt{b_i/\varepsilon}$ .
(31): $\sum_{i\in U} p_i - Q = \sum_{i\in U} p_i\sqrt{b_i/\varepsilon}$ .

A companion theorem states that a minimizing split exists whenever $0 < Q < \sum_i p_i$ .

Significance

The closed forms give the system-optimal assignment on parallel routes with the travel-time law (22) explicitly: which routes carry traffic, how much, and the resulting average time. Together with the equal-times solution (23)–(24) of mission II they quantify, for this model, how much average time selfish route choice costs; the paper's Fig. 8 compares the two numerically and finds the difference small in its example. The marginal-time conditions (27)–(28) are the parallel-route instance of the general statement that a system optimum is an equilibrium with respect to marginal costs.

The derivation on pp. 346–347 is a first-order argument that the paper does not make rigorous: it assumes a minimizer exists, that it satisfies the stationarity condition, and leaves (32)–(33) to "a few lines of algebra". This mission produces the rigorous version, including existence. No machine-checked statement of (27)–(33) is on the platform; the related platform items on Wardrop equilibria concern the Beckmann potential and atomic congestion games, not the system optimum of this model.

Difficulty

The stationarity condition (27) comes from moving an infinitesimal flow between two routes in use. Turning this into a theorem needs the one-sided version at unused routes, since $q_j = 0$ is a boundary point and the condition there is an inequality, and needs the constraint $\sum_i q_i = Q$ to be preserved by the perturbation. The step "only the first $j$ routes will be in use" is the converse direction: a route with $b_i < \varepsilon$ that carries no flow must be shown to contradict minimality, not just to violate the equal-marginals equation.

Existence is not a compactness argument on a closed set: the feasible set is open in the direction $q_i \to p_i$ , where $q_i t_i \to \infty$ , and that coercivity has to be used. The algebra from (31) to (32)–(33) is routine once the set $U$ and the value of $\varepsilon$ are fixed.

Formalization scope

Routes are indexed by Fin D; all quantities are real. The standing hypotheses are $b_i > 0$ , $p_i > 0$ , $0 < Q$ and $Q < \sum_i p_i$ ; without the last the feasible set is empty and every statement about a minimizer is vacuous, and with $Q \le 0$ the average time $Z/Q$ is undefined. Feasibility requires $q_i < p_i$ , of the minimizer and of every competitor: at $q_i = p_i$ Lean evaluates $b_i/0$ as $0$ , which would let a "minimizer" place flow at capacity for free. The paper's labelling $b_1 < \dots < b_D$ is not assumed; "the first $j$ routes" is $U(\varepsilon)$ . Marginal times are written in the closed form (29), and milestone 1 identifies that form with the derivative via HasDerivAt. Minimality is stated for $T$ , the paper's criterion, not for $Z$ .

Corrected slip. The paper prints the denominator of (33) as $\sum_{i=1}^j p_i b_i$ . The formalization uses $\sum_{i=1}^j p_i\sqrt{b_i}$ : from (31), $1/\sqrt\varepsilon = (\sum p_i - Q)/\sum p_i\sqrt{b_i}$ , and $q_h = p_h(1 - \sqrt{b_h/\varepsilon})$ . The printed form is not dimensionally consistent and gives wrong flows, e.g. for $b = (4, 9)$ , $p = (10, 10)$ , $Q = 35/3$ . Equation (32) is correct as printed.

The goal cannot be satisfied trivially: the threshold $\varepsilon$ is existential and the flows and $T$ are pinned to explicit formulas, and the companion existence theorem shows the hypothesis IsMinAvgTime is met for every admissible $Q$ . The route time and feasible split come from the shared WardropTraffic.EqualTimes.Setting definition; this mission adds the total and average time and criterion (2). Proofs of any item, including the existence theorem and a uniqueness statement (the objective is strictly convex), are welcome.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
T. Roughgarden, É. Tardos, How bad is selfish routing?, J. ACM 49(2) (2002), 236–259. https://doi.org/10.1145/506147.506153

8 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Understanding the Efficiency of Multi-Server Service Systems I: With Poisson Arrivals and Finitely Many Service-Time Values of Mean 1, the Number of Busy Servers in M/G/∞ Is Poisson(λ)Research Paper

Motivation

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

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

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

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

Timeline:

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

Setting

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

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

Significance

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

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

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

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

Difficulty

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

Formalization scope

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

Selected references

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

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal 1: Iterative Rounding Finds a Spanning Tree of Cost at Most the LP Optimum with Every Degree at Most B_v + 1Research Paper

Motivation

A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.

The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of $B_v+2$ ; an earlier unweighted local-search result attained a $+1$ degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the $+1$ allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.

Setting

Let $V$ be a finite vertex set and $E$ a finite set of unordered, non-loop edges. A spanning tree $T\subseteq E$ connects every vertex without a cycle. Every edge $e$ has a real cost $c_e$ , so $c(T)=\sum_{e\in T}c_e$ . Each vertex $v$ has an integer upper bound $B_v$ on its tree degree $d_T(v)$ . A feasible original solution has $d_T(v)\le B_v$ for all $v$ .

The paper studies a broader connecting-tree problem. A forest $F$ is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges $E$ disjoint from $F$ . A set $H\subseteq E$ is an $F$ -tree if $H\cup F$ is a spanning tree. Degree bounds are active only at vertices in $W\subseteq V$ , and $d_H(v)$ counts edges of $H$ , not edges of $F$ . The initial spanning-tree problem is the case $F=\varnothing$ and $W=V$ Singh–Lau 2007, p. 665.

For an edge set $Q$ and vertex set $S$ , write $Q(S)$ for edges of $Q$ with both endpoints in $S$ , and $\delta_E(v)$ for edges of $E$ incident to $v$ . The LP-MBDCT relaxation has a nonnegative variable $x_e$ for each $e\in E$ . It requires $x(E)=|V|-|F|-1$ , requires $x(E(S))\le |S|-|F(S)|-1$ for every nonempty union $S$ of supernodes, and requires $x(\delta_E(v))\le B_v$ for $v\in W$ . Its objective is $\sum_{e\in E}c_ex_e$ . At $F=\varnothing$ , $W=V$ , this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.

Formalization targets

Theorem 1.2: bounded-degree spanning trees

For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree $T$ satisfying

d_T(v)\le B_v+1\quad(v\in V),\qquad c(T)\le\sum_{e\in E}c_ex_e\quad\text{for every LP-feasible }x.

In particular, $c(T)$ is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most $2|V|-1$ iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.

Theorem 4.2 and its milestones

The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state $(E,B,W,F)$ , with $d_H(v)\le B_v+1$ only for $v\in W$ . The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.

Significance

The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.

This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.

Difficulty

Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.

Formalization scope

Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.

Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.

The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most $B_v+1$ would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.

Selected references

Mohit Singh and Lap Chi Lau, Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal, Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), 2007, pp. 661–670. DOI: 10.1145/1250790.1250887.

8 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

The G/GI/N Queue in the Halfin–Whitt Regime 3: The Number in a Non-Idling G/GI/N System Satisfies the Infinite-Server System Equation (2.8)Research Paper

Motivation

A many-server queue has $N$ identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers $N$ grows with the arrival rate $\lambda_N$ so that $\sqrt N(1-\lambda_N/N)\to\beta$ : servers are almost fully used, yet only a vanishing fraction of customers waits.

Halfin and Whitt (1981, Oper. Res. 29) identified the regime and proved a diffusion limit for exponential service times ( $GI/M/N$ ).
Puhalskii and Reiman (2000, Adv. Appl. Probab. 32) treated phase-type service distributions ( $GI/PH/N$ ).
Reed (2009, arXiv:0912.2837), the source of this mission, obtained the fluid and diffusion limits of the number in system for the $G/GI/N$ queue with a general service-time distribution, assuming only a finite mean. Its approach rests on a sample-path identity, the system equation (2.8), which writes the number in system of the $N$ -server queue through quantities of an infinite-server queue fed by the same arrivals.

This mission formalizes that identity and the proposition that yields it.

Setting

Fix one realisation of the queue (Reed, §2, p. 6).

There are $N$ servers. At time $0-$ there are $Q_0$ customers; the first $\min(Q_0,N)$ are in service, with residual service times $\tilde\eta_i$ , and the other $(Q_0-N)^+$ wait.
Customers then arrive at times $0\le\tau_1\le\tau_2\le\cdots$ (with $\tau_0=0$ ); the arrival process is $A(t)=\#\{i\ge1:\tau_i\le t\}$ . Arrivals at time $0$ are counted in $A(0)$ , so in general $Q(0)\ne Q_0$ .
The $i$ -th customer to enter service after time $0-$ has service time $\eta_i$ . Service is first come first served, so the first $(Q_0-N)^+$ of these are the initial waiting customers and the $i$ -th arrival has service time $\eta_{(Q_0-N)^++i}$ .
$w_i\ge0$ is the waiting time of the $i$ -th arrival and $\tilde w_i\ge0$ that of the initial customer $N+i$ .
$F$ is the service-time distribution, with tail $G=1-F$ , and $F_0$ the residual service-time distribution, with tail $\bar F_0$ ; both are carried by $[0,\infty)$ .

The number in system is (2.2):

Q(t)=\sum_{i=1}^{\min(Q_0,N)}1\{\tilde\eta_i>t\}+\sum_{i=1}^{(Q_0-N)^+}1\{\tilde w_i+\eta_i>t\}+\sum_{i=1}^{A(t)}1\{\tau_i+w_i+\eta_{(Q_0-N)^++i}>t\}.

Centring each indicator at its (conditional) mean produces the terms

W_0(t)=\sum_{i=1}^{\min(Q_0,N)}\big(1\{\tilde\eta_i>t\}-\bar F_0(t)\big),\qquad A_G(t)=\int_0^tG(t-s)\,dA(s),\qquad I(t)=\min(Q_0,N)\bar F_0(t)+(Q_0-N)^+G(t),

and $M_2(t)$ , the analogous centred sum (2.5) over the customers who entered service after time $0-$ . $A_G(t)$ is the conditional mean number in a $G/GI/\infty$ queue fed by the same arrivals.

A sample path is non-idling if for every $t\ge0$

(Q(t)-N)^+=\sum_{i=1}^{(Q_0-N)^+}1\{t<\tilde w_i\}+\sum_{i=1}^{A(t)}1\{\tau_i\le t<\tau_i+w_i\},

that is, the customers waiting at time $t$ are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served $N$ -server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).

Formalization targets

Goal: the system equation (2.8), p. 9

For a non-idling sample path and every $t\ge 0$ ,

Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\int_0^t\big(Q(t-s)-N\big)^+\,dF(s).

Milestones

The first two equalities of the proof of Proposition 2.1 (p. 8): $\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\sum_{i\le A(t)}\int_0^\infty 1\{t-(\tau_i+w_i)<s\le t-\tau_i\}\,dF(s)$ .
The "reverse argument" of the proof (p. 9): $\int_0^t\sum_{i\le(Q_0-N)^+}1\{\tilde w_i>t-s\}\,dF(s)=\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)$ .
Proposition 2.1 (p. 8): for a non-idling path and $t\ge0$ ,

\sum_{i=1}^{A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)=\int_0^t(Q(t-s)-N)^+\,dF(s)-\sum_{i=1}^{(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big).

The decomposition (2.7) (p. 7): $Q(t)=I(t)+W_0(t)+M_2(t)+A_G(t)+\sum_{i\le(Q_0-N)^+}\big(G(t-\tilde w_i)-G(t)\big)+\sum_{i\le A(t)}\big(G(t-\tau_i-w_i)-G(t-\tau_i)\big)$ .

Significance

The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing $Q-N=x+\int_0^t(Q(t-s)-N)^+dF(s)$ with $x=I+W_0+M_2+A_G-N$ shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of $z(t)=x(t)+\int_0^t(z(t-s)+a)^+dB(s)$ . The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the $N$ -server queue has no closed equation in terms of quantities whose limits are known.

Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the $G/GI/N$ queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.

Difficulty

The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against $F$ , of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer $i$ 's service time falls in a window of length $w_i$ " to "customer $i$ is waiting at time $t-s$ ", after which the sum over customers must be recognised, at each time $t-s$ , as the waiting count of the non-idling identity, with the arrivals counted up to $A(t-s)$ rather than $A(t)$ . A second point is the treatment of an atom of $F$ at $0$ : the half-open windows $(t-\tau_i-w_i,\,t-\tau_i]$ and the closed integration range $[0,t]$ must match, and $G(x)=1$ for $x<0$ is used whenever a customer is still waiting.

Formalization scope

Paths are data, not random. A sample path is a structure holding $N$ , $Q_0$ and the sequences $\tilde\eta,\eta,\tau,w,\tilde w:\mathbb N\to\mathbb R$ , indexed from $1$ as in the paper. The arrival times are primary and $A(t)$ is their counting function; for a counting process with $A(0-)=0$ this is the same data as the paper's $\tau_i=\inf\{t\ge0:A(t)\ge i\}$ . The encoding has infinitely many arrivals, finitely many in each bounded interval.
Distributions are probability measures $\mu$ (for $F$ ) and $\mu_0$ (for $F_0$ ) on $\mathbb R$ with no mass on $(-\infty,0)$ , and $G(x)=\mu((x,\infty))$ for every real $x$ . The paper's i.i.d. assumptions and the mean- $1$ assumption on $F$ are not used by these pathwise identities and are omitted.
Integrals $\int_0^t\cdot\,dF(s)$ are over the closed interval $[0,t]$ , an atom of $F$ at $0$ included; $A_G(t)$ , a Stieltjes integral against the counting measure of arrivals, is the finite sum $\sum_{i\le A(t)}G(t-\tau_i)$ .
Non-idling is a hypothesis on the sample path, exactly the identity displayed above. No hypothesis mentions (2.8), Proposition 2.1 or an integral against $F$ , and $Q$ is not a free function: it is defined by (2.2). Integrability of $s\mapsto(Q(t-s)-N)^+$ is part of what must be proved, not assumed. The hypotheses are jointly satisfiable, so the goal is not vacuous.
Needed infrastructure: finite sums, set integrals of indicator functions against a finite measure on $\mathbb R$ , and the identity $G(a)-G(b)=\mu((a,b])$ . All of it is in Mathlib.

Related platform items: WhittEfficiency.IS.* (the $M/G/\infty$ queue with Poisson arrivals, the infinite-server object behind $A_G$ ) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.

Selected references

J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. arXiv:0912.2837v1. https://arxiv.org/abs/0912.2837 , https://doi.org/10.1214/09-AAP609
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29, 1981, 567–588. https://doi.org/10.1287/opre.29.3.567 (MR629195)
A. A. Puhalskii and M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Adv. Appl. Probab. 32, 2000, 564–595. https://mathscinet.ams.org/mathscinet-getitem?mr=1778580

8 thms2 active usersReviewed

Dynamic Programming Machine Learning Markov Chain+2·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 1: Linear TD(λ) Converges with Probability 1 to the Fixed Point of ΠT^(λ), with Error ≤ ‖ΠJ* − J*‖_D/(1 − α(1−λ)/(1−αλ))Research Paper

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 11)

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

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

and

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

Milestones

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

Significance

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

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

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

Difficulty

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

Formalization scope

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

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

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

The development needs the following:

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

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

Selected references

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

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

Strategy-Proofness and Arrow's Conditions 3: With Indifference Allowed, a Strategy-Proof Voting Procedure with at Least Three Possible Outcomes Is DictatorialResearch Paper

Motivation

A committee that chooses one alternative by voting would like a procedure under which nobody gains by misreporting their preferences. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) showed that, once at least three outcomes are possible, the only voting procedures with this property are dictatorial. The theorem is the starting point of the theory of strategy-proof mechanisms and of implementation theory.

Most proofs, including the main argument of Satterthwaite's paper, assume strict ballots: no voter is indifferent between two distinct alternatives. Real ballots, and most economic models of preferences, allow indifference. The last section of Satterthwaite's paper carries the theorem over to ballots that are arbitrary weak orders, by decomposing a voting procedure into a tie-breaking function followed by a strict voting procedure. This mission formalizes that extension.

Timeline. Gibbard (1973) proved the impossibility for game forms; the 1974 discussion paper formalized here proved it for strict ballots by induction on the number of voters (Theorem 1), allowing the range of the procedure to be a proper subset of the alternatives, and extended it to weak orders (Theorem 1′). Later short proofs (Barberà 1983; Benoît 2000; Reny 2001) also treat strict ballots.

Setting

A committee is a finite set $I_n$ of $n$ individuals and a finite set $S_m$ of $m$ alternatives. A weak order $R$ on $S_m$ is a complete and transitive relation, with $x\,R\,y$ read " $x$ is preferred or indifferent to $y$ "; its strict part is $x\,\bar R\,y$ iff $x\,R\,y$ and not $y\,R\,x$ . The weak orders form $\pi_m$ . A strong order is a weak order with no indifference between distinct alternatives; the strong orders form $\rho_m\subseteq\pi_m$ . A ballot set is $B=(B_1,\dots,B_n)\in\pi_m^n$ .

A voting procedure is a map $v:\pi_m^n\to S_m$ . Its range is $T_p=v(\pi_m^n)$ , with $p=|T_p|$ . A strict voting procedure is a map $\nu:\rho_m^n\to S_m$ .

$v$ is strategy-proof if there are no ballot set $B$ , individual $i$ and ballot $B_i'\in\pi_m$ with

v(B_1,\dots,B_i',\dots,B_n)\ \bar B_i\ v(B_1,\dots,B_i,\dots,B_n).

For a strict procedure, ballot sets and substituted ballots are strong orders.

$v$ is dictatorial if some individual $i$ exists such that, for every ballot set $B$ , the outcome $v(B)$ is among the $B_i$ -maximal elements of $T_p$ : $v(B)\,B_i\,y$ for all $y\in T_p$ .

A tie-breaking function is a map $\alpha:\pi_m^n\to\rho_m^n$ that keeps every strict preference: if $C=\alpha(B)$ then $x\,\bar B_i\,y$ implies $x\,\bar C_i\,y$ . It is regular if there are fixed strong orders $Q_1,\dots,Q_n$ such that every indifference $x\,B_i\,y$ , $y\,B_i\,x$ is broken as $Q_i$ breaks it.

Formalization targets

Goal: Theorem 1′ (p. 43)

For $n\ge 2$ and $m\ge p\ge 3$ , every strategy-proof voting procedure on weak-order ballots is dictatorial:

v \text{ strategy-proof},\ |T_p|\ge 3 \ \Longrightarrow\ \exists\, i\ \forall B\in\pi_m^n\ \forall y\in T_p:\ v(B)\,B_i\,y.

The converse fails once indifference is admissible: a dictator's ties may be broken by a manipulable rule, such as a Borda count of the other ballots (pp. 10–11). The goal is therefore a one-way implication.

Milestones

Theorem 1 (p. 11), the strict case: for $n\ge 1$ and $p\ge 3$ , a strict voting procedure is strategy-proof if and only if it is dictatorial.
Lemma 9, first sentence (p. 41): if $v=\nu\circ\gamma$ with $\nu$ strict and strategy-proof and $\gamma$ a regular tie-breaking function, then $v$ is strategy-proof.
Lemma 9, second sentence (p. 41): every strategy-proof $v$ can be written $v=\nu\circ\alpha$ with $\nu$ strict and strategy-proof and $\alpha$ a tie-breaking function, not necessarily regular.

Significance

The result shows that allowing voters to express indifference does not escape the Gibbard–Satterthwaite impossibility: the dictatorial conclusion survives, and only the equivalence is lost. It is the form of the theorem most directly applicable to economic environments, where preference domains usually contain indifference, and the decomposition of Lemma 9 is the device by which strict-ballot results are transferred to weak-order ballots throughout §6 of the paper, including the weak-order version of Arrow's theorem.

The theorem is proved and classical. What is not yet available is a machine-checked proof of the weak-order version with a range that may be a proper subset of the alternatives. The strict, full-range case is proved on the platform (AGT.gibbard_satterthwaite, on strict total orders with a surjective rule); the strict case with an arbitrary range of size at least three is the goal of the companion mission on strict committees. This mission adds the decomposition of Lemma 9 and the extension to indifference.

Difficulty

The obvious route is to restrict a strategy-proof $v$ to strict ballot sets, apply the strict theorem, and conclude. Two steps fail. First, the restriction's range may a priori be smaller than $T_p$ , so the hypothesis $p\ge 3$ need not transfer. Second, knowing that $v$ is dictatorial on strict ballot sets says nothing directly about ballot sets with indifference: one needs, for each $B$ , a strict refinement $C$ of $B$ with $v(C)=v(B)$ , and the refinement of one individual's ballot may depend on the others' ballots. Lemma 9's second sentence is exactly the existence of such refinements, and the tie-breaking function it produces is generally not regular.

Formalization scope

Lean commits to the following conventions, all in the definitions file StrategyProofArrow.WeakGS.Basic:

Individuals and alternatives are finite types ι and A; $n$ and $m$ are their cardinalities. The theorems state $n\ge 1$ or $n\ge 2$ as printed, and $m\ge 3$ where the paper's standing committee assumption is all that applies (Lemma 9). $m\ge p$ is automatic.
A weak order is a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct alternatives, so a strict ballot is literally a weak ballot.
Voting procedures are total functions on profiles of weak orders (resp. strong orders). There are no inadmissible inputs, and the range $T_p$ is Set.range v.
Strategy-proofness compares outcomes by the strict part of the true ballot; the substituted ballot is any weak order (any strong order in the strict case).
The paper defines dictatorship through a function $f^i_T$ that selects some $B_i$ -maximal element of $T_p$ with an unspecified tie-break. Lean states the equivalent condition that $v(B)$ is $B_i$ -maximal in $T_p$ , without fixing a tie-break. Fixing one would make Theorem 1′ false.
The tie-breaking condition is stated once for all $x,y$ ; the paper's two clauses are the same condition with $x,y$ renamed. $\alpha(B)_i$ may depend on all of $B$ .
In Lemma 9 the page prints the composition with a Latin $v$ on both sides; it is read as $\nu^{nm}[\gamma(B)]$ , as the sentence and proof require.

A trivializing formalization would measure manipulation by the weak relation $B_i$ instead of its strict part, which makes "strategy-proof" nearly unsatisfiable and the goal vacuous; the definitions use the strict part, and a sorry-free check confirms that a strategy-proof procedure with range of size 3 exists.

A complete development needs the strict Gibbard–Satterthwaite theorem with partial range (milestone 1) and the refinement construction of Lemma 9. The weak-order and tie-breaking vocabulary is reusable for the weak-order Arrow theorem of the companion mission. Proofs of any milestone, and alternative proofs of the goal that bypass Lemma 9, are welcome.

Selected references

M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
S. Barberà, Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard–Satterthwaite Theorem, International Economic Review 24 (1983) 413–417. https://doi.org/10.2307/2648754
J.-P. Benoît, The Gibbard–Satterthwaite Theorem: A Simple Proof, Economics Letters 69 (2000) 319–322. https://doi.org/10.1016/S0165-1765(00)00312-8
P. J. Reny, Arrow's Theorem and the Gibbard–Satterthwaite Theorem: A Unified Approach, Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3

6 thms2 active usersReviewed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Stability Properties of Constrained Queueing Systems and Scheduling Policies for Maximum Throughput in Multihop Radio Networks I: Policy π₀ Is Throughput-Optimal, C′ ⊂ C_π₀ ⊂ C ⊂ C̄′Research Paper

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 3.2

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

9 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A D.C. Optimization Algorithm for Solving the Trust-Region Subproblem I: A Point x Solves the D.C. Program min(g − h) if and only if ∂_εh(x) ⊂ ∂_εg(x) for Every ε > 0Research Paper

Motivation

A d.c. program minimizes a difference of two convex functions. Many nonconvex problems of practical interest have this form: every function with a locally Lipschitz gradient on $\mathbb R^n$ is d.c., the class is closed under finite sums, products and finite suprema, and constrained problems enter through indicator functions. Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) use this structure to build the DCA, an algorithm for the trust-region subproblem $\min\{\tfrac12 x^\top Ax+b^\top x:\|x\|\le r\}$ , a basic step of trust-region methods in nonlinear optimization. The algorithm rests on a duality theory for d.c. programs, which §3.1 of the paper sets out. This mission is the global half of that theory.

Timeline.

1978–1979: J. F. Toland introduces the duality $\inf(g-h)=\inf(h^*-g^*)$ and the inclusions between primal and dual solution sets, in a general setting of linear spaces in separating duality (J. Math. Anal. Appl. 66 (1978); Bull. Soc. Math. France, Mémoire 60 (1979), pp. 177–183, numdam).
1988: J.-B. Hiriart-Urruty proves that $x$ minimizes $g-h$ if and only if $\partial_\varepsilon h(x)\subset\partial_\varepsilon g(x)$ for every $\varepsilon>0$ , through the behaviour of the $\varepsilon$ -directional derivative as a function of $\varepsilon$ (From convex optimization to non convex optimization. Part I, in Nonsmooth Optimization and Related Topics, Plenum, 1988; reference [9] of the paper). The same year Pham Dinh and Elbernoussi introduce the DCA on the basis of d.c. duality (reference [23]).
1998: Pham Dinh and Le Thi give a short proof of Hiriart-Urruty's condition through the d.c. duality (Theorem 3.1, p. 483) and use the duality to design and analyse the DCA for the trust-region subproblem.

Setting

Let $X=\mathbb R^n$ with its canonical inner product $\langle\cdot,\cdot\rangle$ , and identify the dual space $Y$ with $X$ . Functions take values in $\mathbb R\cup\{+\infty\}$ . A function $\theta$ is in $\Gamma_0(X)$ if it is convex, lower semicontinuous, never $-\infty$ , and finite at some point. Its effective domain is $\operatorname{dom}\theta=\{x:\theta(x)<+\infty\}$ , and its conjugate is

\theta^*(y)=\sup\{\langle x,y\rangle-\theta(x):x\in X\}.

For $x_0\in\operatorname{dom}\theta$ , the subdifferential $\partial\theta(x_0)$ is the set of $y$ with $\theta(x)\ge\theta(x_0)+\langle x-x_0,y\rangle$ for all $x$ . For $\varepsilon>0$ the $\varepsilon$ -subdifferential is

\partial_\varepsilon\theta(x_0)=\{y\in Y:\theta(x)\ge\theta(x_0)+\langle x-x_0,y\rangle-\varepsilon\ \ \forall x\in X\}.

Given $g,h\in\Gamma_0(X)$ , the d.c. program and its dual are

\text{(P)}\quad\alpha=\inf\{g(x)-h(x):x\in X\},\qquad \text{(D)}\quad\alpha=\inf\{h^*(y)-g^*(y):y\in Y\},

with the convention $+\infty-(+\infty)=+\infty$ . Throughout, the paper assumes the inclusions

\operatorname{dom}g\subset\operatorname{dom}h,\qquad\operatorname{dom}h^*\subset\operatorname{dom}g^*.\tag{3}

$\mathcal P$ and $\mathcal D$ denote the solution sets of (P) and (D).

Formalization targets

Goal: Theorem 3.1(i), p. 483

For every $x\in\operatorname{dom}h$ ,

x\in\mathcal P\iff\partial_\varepsilon h(x)\subset\partial_\varepsilon g(x)\quad\forall\varepsilon>0.

Milestones (the proof on pp. 483–484)

d.c. duality (§3, pp. 481–482): $\inf\{g-h\}=\inf\{h^*-g^*\}$ .
(6)–(7) (p. 483): $x^*\in\mathcal P$ iff $x^*\in\operatorname{dom}g$ and $g(x^*)+g^*(y)\le h(x^*)+h^*(y)$ for all $y\in\operatorname{dom}h^*$ .
(8) (p. 484): for $x^*\in\operatorname{dom}h$ , the inclusions $\partial_\varepsilon h(x^*)\subset\partial_\varepsilon g(x^*)$ for all $\varepsilon>0$ are equivalent to $\langle x^*,y\rangle+\varepsilon\ge h(x^*)+h^*(y)\Rightarrow\langle x^*,y\rangle+\varepsilon\ge g(x^*)+g^*(y)$ for all $\varepsilon>0$ and $y$ .
(7) ⇔ (8) (p. 484), for $x^*\in\operatorname{dom}h$ .

Companions

Theorem 3.1(ii): for $y\in\operatorname{dom}g^*$ , $y\in\mathcal D\iff\partial_\varepsilon g^*(y)\subset\partial_\varepsilon h^*(y)$ for all $\varepsilon>0$ .
Theorem 3.1(iii): $\bigcup\{\partial h(x):x\in\mathcal P\}\subset\mathcal D\subset\operatorname{dom}h^*$ , with equality in the first inclusion when $g^*$ is subdifferentiable on $\mathcal D$ .
Theorem 3.1(iv): $\bigcup\{\partial g^*(y):y\in\mathcal D\}\subset\mathcal P\subset\operatorname{dom}g$ , with equality when $h$ is subdifferentiable on $\mathcal P$ .

Significance

The result. Theorem 3.1(i) characterizes global minimizers of a nonconvex function by inclusions between convex objects. It is a certificate of global optimality that uses only convex analysis. Parts (iii) and (iv) say that a solution of either program yields a solution of the other through a subgradient. This is the mechanism of the DCA, which alternates $y^k\in\partial h(x^k)$ , $x^{k+1}\in\partial g^*(y^k)$ . The paper notes that condition (i) is hard to use in an algorithm and that the DCA rests on local conditions instead. The global condition remains the reference statement that the local theory and the DCA approximate.

Formalizing it. All results here are classical and proved on paper. Parts (iii) and (iv) are proved in references the paper cites, not in the paper itself. None of them has a machine-checked proof on the platform. The mission provides a Lean layer for d.c. programming on $\mathbb R^n$ : the convention-respecting difference, the $\varepsilon$ -subdifferential, the standing assumptions, and the primal and dual solution sets. Missions II and III of the series reuse this layer for local optimality and for the convergence of the DCA.

Difficulty

The paper's proof is short, but each step uses a fact that needs separate work. The duality requires the biconjugation $h=h^{**}$ for $h\in\Gamma_0$ , and an exchange of two infima in the extended reals under the convention $+\infty-(+\infty)=+\infty$ . The step (7) ⇔ (8) has a hidden case: a point of $\operatorname{dom}h\setminus\operatorname{dom}g$ . Ruling it out needs $\partial_\varepsilon h(x^*)\neq\emptyset$ for $\varepsilon>0$ , a nontrivial property of lower semicontinuous proper convex functions. The obvious approach, computing with real numbers, fails because $g$ , $h$ , $g^*$ and $h^*$ all take the value $+\infty$ , and the extended-real arithmetic of Lean does not follow the paper's convention.

Formalization scope

Space. $X=Y$ is EuclideanSpace ℝ (Fin n). Functions are EReal-valued.
Published definitions. $\Gamma_0$ is ThreeOpSplitting.ConvexRates.IsProperClosedConvex, $\partial$ is InertialFB.IFB.IsSubgradient, and the conjugate is CondatPD.FinDim.conj, an extended-real supremum over all of $X$ .
Convention. Mathlib has $\top-\top=\bot$ . Every difference $g-h$ and $h^*-g^*$ of the paper is the explicit dcSub, which returns $+\infty$ when the first term is $+\infty$ . $\mathcal P$ , $\mathcal D$ and $\alpha$ are defined through it.
Domains. The $\varepsilon$ -subdifferential is empty outside the domain, as in the paper's definition. Theorem 3.1(i) is stated for $x\in\operatorname{dom}h$ , the case its proof treats. For $x\notin\operatorname{dom}h$ the right-hand side holds vacuously while $x\notin\mathcal P$ . Every solution lies in $\operatorname{dom}g\subset\operatorname{dom}h$ , and for $x\in\operatorname{dom}h\setminus\operatorname{dom}g$ both sides are false, so the restriction loses nothing. Part (ii) is restricted to $y\in\operatorname{dom}g^*$ for the same reason.
Standing assumptions. $g,h\in\Gamma_0$ and the inclusions (3) are a hypothesis of every item. Finiteness of $\alpha$ is not assumed: when $\alpha=-\infty$ , both solution sets are empty.
Not a trivialization. Defining the $\varepsilon$ -subdifferential without the domain clause, or using Mathlib's subtraction for $g-h$ , would change the theorem: the first makes every $y$ an $\varepsilon$ -subgradient at points where the function is $+\infty$ , and the second sets $g-h=-\infty$ wherever $g$ and $h$ are both $+\infty$ , since Lean's $\top-\top=\bot$ . The goal does not mention (6), (7), (8) or the duality.
Parts (iii) and (iv) include the paper's "in particular" sufficient conditions, with the relative interior written as Mathlib's intrinsicInterior, and the "in this case" inclusions into $\operatorname{dom}\partial g^*\cap\operatorname{dom}\partial h^*$ and $\operatorname{dom}\partial g\cap\operatorname{dom}\partial h$ .
Contributions welcome. Biconjugation and Fenchel–Young for EReal-valued functions on EuclideanSpace in the conventions of CondatPD.FinDim.conj, nonemptiness of $\varepsilon$ -subdifferentials, and the extended-real infimum exchange. These are reusable well beyond d.c. programming.

Selected references

Pham Dinh Tao and Le Thi Hoai An, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM J. Optim. 8(2):476–505, 1998. https://doi.org/10.1137/S1052623494274313
J. F. Toland, Duality in nonconvex optimization, J. Math. Anal. Appl. 66:399–415, 1978. https://doi.org/10.1016/0022-247X(78)90243-3
J. F. Toland, On subdifferential calculus and duality in nonconvex optimization, Bull. Soc. Math. France, Mémoire 60:177–183, 1979. http://www.numdam.org/item/MSMF_1979__60__177_0/
J.-B. Hiriart-Urruty, From convex optimization to non convex optimization. Part I: Necessary and sufficient conditions for global optimality, in Nonsmooth Optimization and Related Topics, Ettore Majorana Internat. Sci. Ser. Phys. Sci. 43, Plenum Press, New York, 1988 (no persistent link; cited as [9] in the paper above).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

9 thms2 active usersReviewed

Analysis Operations Research Optimization+1·Captain: mikedeng1

Dynamic Scheduling with Convex Delay Costs: The Generalized cμ Rule: Policies Equalizing the Indices μ_k c_k(W_k/ρ_k) Attain the Heavy-Traffic Lower Bound on Cumulative Delay CostResearch Paper

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal: Proposition 7

Under Assumptions 1–3, for feasible policies with

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

the costs and delays converge,

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

16 thms2 active usersReviewed

All missions

Convergence Properties of the Nelder–Mead Simplex Method in Low Dimensions II: In Dimension 1 with ρ = 1, the Interval Diameter Halves Every M Iterations, M Depending Only on χ and γResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.2 (p. 130)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Simulation Output Analysis Using Standardized Time Series 3: No g in 𝓜 Makes g(σB) Almost Surely Constant, So the Length Bound Is Not AttainedResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.26

Milestones (the steps of the proof, pp. 13–14)

Companions

Significance

Difficulty

Formalization scope

Selected references

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection III: On Instances Separated by Δ(v) the UCB Policy Has Regret at Most B₁N² log T/Δ(v) + B₂Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 20)

Milestones

Companion: Corollary 6.1 (p. 21)

Significance

Difficulty

Formalization scope

Selected references

3SUM in O(n^1.999112) Time on a Word RAMResearch Paper

3SUM in O(n^1.99913) Time on a Word RAMResearch Paper

The Evolution of Conventions III: In 2 × 2 Games with Two Strict Equilibria, the Generically Stable Equilibria of Adaptive Play Are the Weakly Risk Dominant OnesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 72)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 3: Under Box Uncertainty, Worst-Case CVaR Minimization (16)–(20) Is Equivalent to the Linear Program (24)–(30)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 1159)

Milestones, in the order the paper's argument uses them

Significance

Difficulty

Formalization scope

Selected references

Old and New Methods for Lost-Sales Inventory Systems 1: Under Any Policy in Z(s) the State Enters X(s) and Never Leaves, So Every State Outside X(s) Is TransientResearch Paper

Why the lost-sales state space matters

Setting

Formalization targets

Goal: Claim 1 (p. 1259)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Structure of Lost-Sales Inventory Models 1: In the Transformed State v = J⁻¹x, the Optimal Cost Functions f̄_t(v) and ḡ_t(v, ζ) Are L♮-ConvexResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 939)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 2: For a Compact Convex Set of Discrete Distributions, Worst-Case CVaR Equals min_α max_π G_β(x, α, π)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1159)