Operations Research

Motivation

Network revenue managers sell access to limited capacity over time. An airline, for example, may have several products that use the same seat inventory, with some products earning more revenue than others. The decision to accept a request must be made when it arrives, before future requests are known. A standard way to guide that decision is to solve a deterministic linear program using expected demand, then use its optimal allocation as a probability of acceptance. As inventory changes, one can solve the program again. Bumpensanti and Wang study how often to do so, and show that frequent re-solving has a real limitation when the linear program is degenerate: on a particular instance its expected loss grows at least as the square root of the selling horizon. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 3.1 and 5.1.

The same paper gives an infrequent re-solving policy with uniformly bounded regret and an upper bound of order $\sqrt T$ for the frequent re-solving policy. The lower-bound result is the counterpart that identifies a case where that order cannot be removed by the frequent policy itself. It uses a two-class example small enough to expose the issue without other network complications. Bumpensanti and Wang, arXiv:1802.06192v3, Theorem 1 and Propositions 2–3.

Setting

There is one resource, initially with $T$ units of capacity, and two customer classes. Class $j$ arrives through an independent Poisson process of rate one. Accepting a customer uses one unit of capacity and earns price $r_j$, where $0<r_2<r_1$. Rejected requests earn nothing, and unused capacity has no terminal value. The higher-price class has priority in the deterministic allocation, but its realized demand is random. The horizon $T$ is a positive integer, divided into $T$ periods of length one. Bumpensanti and Wang, arXiv:1802.06192v3, Section 2, pp. 7–9, and Appendix C.1, p. 32.

At the start of a period with $k$ periods left and capacity $c$, the deterministic linear program (DLP) chooses rates $x_1,x_2$ that maximize $r_1x_1+r_2x_2$ subject to $x_1+x_2\le c/k$ and $0\le x_j\le1$. In this instance its first coordinate is $x_1=\min\{c/k,1\}$. The frequent re-solving policy (FR) accepts each class-$j$ request in that period with probability $x_j$, provided capacity remains. It re-solves the DLP at the next period with the new capacity. This is Algorithm 2 specialized to the example. Bumpensanti and Wang, arXiv:1802.06192v3, Algorithm 2, p. 11, and Appendix D, p. 42.

The hindsight optimum knows the total demand from both classes at the end of the horizon and chooses the best feasible allocation using that information. Its expected value is $v^{\mathrm{HO}}(T,T)$; the first argument is horizon length and the second is initial capacity. Let $v^{\mathrm{FR}}(T,T)$ be the frequent policy's expected revenue. Since hindsight has more information, their difference is a regret benchmark. The formulation uses the paper's hindsight linear program, which is exact on this unit-consumption instance. Bumpensanti and Wang, arXiv:1802.06192v3, Eq. (3) and Definition 1, p. 9.

Formalization targets

Main result

For every pair of prices $0<r_2<r_1$, there are $M>0$ and $T_0\ge1$ such that, for all integer $T\ge T_0$ and every optimal DLP selector used by FR,

$$v^{\mathrm{HO}}(T,T)-v^{\mathrm{FR}}(T,T)\ge M\sqrt T.$$

This specializes Proposition 2's existence statement to the explicit family in its Appendix C.1 proof. The constant may depend on the prices, but is chosen before the selector and the horizon. The benchmark is the hindsight value, as in the proposition. Bumpensanti and Wang, arXiv:1802.06192v3, Proposition 2, p. 18, and Appendix C.1, pp. 32–34.

Supporting results

The milestones record the optimal DLP allocation on the example and two clauses of Lemma 7. The latter estimate the probabilities that the high-price arrival count is moderately below its mean in the first third and moderately above its mean in the last third. With $T'$ an integer phase length and $N\sim\operatorname{Poisson}(T')$, the first bound is

$$\mathbb P(T'-4\sqrt{T'}\le N\le T'-3\sqrt{T'}) \ge 0.0013-0.9496/\sqrt{T'}.$$

The third-phase bound uses the standard normal cumulative distribution function $\Phi$ and the unrounded constant $\Phi(7)-\Phi(6)$. Bumpensanti and Wang, arXiv:1802.06192v3, Lemma 7 and Eqs. (49)–(53), p. 40.

Significance

This result shows that solving the DLP every period does not, by itself, give a horizon-independent expected loss. The example has only one resource and two customer classes; the gap cannot be attributed to a large network. The paper's separate bounded-regret result uses a different re-solving schedule and acceptance rule, so formalizing this lower bound helps distinguish guarantees for the two policies. Together with the upper bound for FR, it identifies the square-root order as the relevant scale for this policy on the example. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 4–5.

The mathematical proposition is proved in the cited paper; the Lean goal here remains an open theorem statement. Formalizing it requires precise interfaces for a Poisson arrival model, a capacity-limited randomized policy, a hindsight LP benchmark, and asymptotic lower bounds. Those interfaces can be reused in later revenue-management results, while the two-class instance gives a concrete check on the conventions.

Difficulty

The initial DLP solution allocates the average capacity to the high-price class. A simple intuition might therefore predict that repeated re-solving preserves capacity for that class. The remaining-capacity ratio, however, responds to realized arrivals; when the ratio rises above one, the re-solved LP assigns positive acceptance probability to the lower-price class. The policy then spends capacity before later high-price arrivals are known. The lower-bound analysis needs a path event that controls arrivals through the middle phase and a joint event involving the policy's accepted requests. Marginal Poisson counts alone do not determine those admissions. Bumpensanti and Wang, arXiv:1802.06192v3, Appendix C.1, pp. 32–34.

Formalization scope

Lean uses Fin 2 for classes and Fin 1 for the resource. The general model takes positive Poisson rates, nonnegative prices and nonnegative consumption. On the lower-bound instance the rates and consumptions equal one, capacity equals $T$, and prices satisfy $0<r_2<r_1$. These are the operational standing assumptions of the paper's Section 2 and the positive-price reading used by the example. Optimal DLP ties are represented by quantifying over every selector. The LP value is the published RLPBidPrice.Unbiased.piValue definition, evaluated on nonnegative capacity vectors; the rate and capacity conventions make its real supremum well posed.

The window law superposes the independent class Poisson processes into a Poisson total count, independent class labels, and independent Bernoulli acceptance marks. A fold over ordered arrivals applies Algorithm 2's capacity check after every acceptance. The expected hindsight value sums over independent total demand counts, and the FR value is a backward recursion over the remaining unit periods. The target's $M$ is strictly positive and fixed before the horizon, so neither a zero constant nor a horizon-dependent constant can satisfy it trivially.

The two Lemma 7 milestones cover only $Q_1$ and $Q_3$. Its continuous-time $Q_2$ event and the joint admission event require a path probability space and are outside this draft. Equation (52) yields $\Phi(7)-\Phi(6)$; the printed $9.8531\times10^{-10}$ rounds that value upward. The source proof divides $T$ into three exact integer-length phases, while Proposition 2 is stated for all sufficiently large $T$; this gap requires attention in a complete proof. The source here is arXiv:1802.06192v3, whose printed and PDF page numbers coincide.

Selected references

• Bumpensanti, P. and Wang, H., A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv preprint arXiv:1802.06192v3, 2018. PDF.

Why priority rules in reentrant lines matter

Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.

Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.

Timeline:

• 1991. Lu and Kumar exhibit a two-station reentrant line that is unstable under a static priority rule with every workload below one.
• 1993. Kumar proves stability of FBFS and LBFS for discrete deterministic reentrant lines.
• 1995. Dai shows that stability of the fluid model implies positive Harris recurrence of the stochastic network.
• 1996. Dai and Weiss prove that the FBFS and LBFS fluid models of every reentrant line are stable (Theorems 4.3 and 4.4), and with Dai's theorem obtain stability of the stochastic networks.

Setting

A reentrant line has $I$ stations and $K$ classes. All fluid follows one route: it enters as class $1$, becomes class $k+1$ when class $k$ is completed, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$, and $\mu_k = 1/m_k$. The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$. The exogenous arrival rate is $1$. The standing assumption of the paper is

$$\rho_i < 1 \qquad (i = 1,\dots,I). \tag{1.7}$$

A fluid model solution is a pair of paths $Q(t) = (Q_k(t))_k$, the fluid levels, and $T(t) = (T_k(t))_k$, the cumulative service time given to each class, such that for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t), \qquad Q_k(t) \ge 0,$$

with $\mu_0T_0(t) = t$; each $T_k$ starts at $0$ and is nondecreasing; and the idle time $U_i(t) = t - \sum_{k\in C_i}T_k(t)$ of each station is nondecreasing.

A buffer priority discipline is a permutation $\pi$ of the classes; a class $k$ has priority over a class $l$ at the same station when $\pi(k) < \pi(l)$. Write $H_k = \{l \in C_{\sigma(k)} : \pi(l) \le \pi(k)\}$, $T_k^+ = \sum_{l\in H_k}T_l$, $U_k^+(t) = t - T_k^+(t)$ and $W_k^+ = \sum_{l\in H_k} m_l Q_l$. Under preemptive resume, $U_k^+$ may increase only at times when $W_k^+ = 0$ (condition (4.4)): a station never idles toward the classes of priority at least that of $k$ while any of them holds fluid. FBFS is $\pi(k) = k$, so earlier steps of the route have priority.

The fluid model is stable (Definition 1.3) if there is a time $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

Formalization targets

Goal: Theorem 4.3

For every reentrant line with $m_k > 0$ and (1.7),

$$\text{the fluid model (1.8)–(1.12), (4.4) with } \pi(k) = k \text{ is stable.}$$

The goal asserts existence of an emptying time; it does not fix the value.

Milestones

1. Lemma 2.2 (i): a nonnegative function has zero derivative wherever it vanishes and is differentiable.
2. Lemma 2.2 (ii): an absolutely continuous nonnegative $g$ whose derivative is at most $-\varepsilon$ wherever $g > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
3. Proposition 4.2: at a regular time of a priority fluid model, an empty buffer has equal in- and out-flow rates, and at each station the highest-priority nonempty class satisfies $\sum_{k\in H_{k_0}} m_kd_k = 1$ while lower-priority classes have zero out-flow.
4. Inductive step (proof of Theorem 4.3): once buffers $1,\dots,k-1$ stay empty from $t_{k-1}$ on, buffer $k$ is empty from $t_k = t_{k-1} + Q_k(t_{k-1})m_k/(1 - \sum_{l\in H_k} m_l)$ on.
5. Emptying time (proof of Theorem 4.3): every solution with $|Q(0)| = 1$ is empty from

$$\delta = \sum_{k=1}^K m_k\frac{\prod_{l=1}^{k-1}(1-\sum_{j\in H_l\setminus\{l\}}m_j)}{\prod_{l=1}^{k}(1-\sum_{j\in H_l}m_j)}$$

on, which gives the goal with an explicit constant.

Significance

Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.

Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.

Difficulty

The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer $k-1$ is empty" is not enough. Finally, the explicit constant $\delta$ requires bounding the content of buffer $k$ at time $t_{k-1}$ by the total content, which may have grown since time $0$.

Formalization scope

• Classes and stations are Fin K and Fin I, 0-based: the paper's class $k$ is Lean index $k-1$.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed on $t \ge 0$ only, and derivatives are taken at $t > 0$.
• Conditions (1.13) and (4.4) are in interval form (ConstantWhile): the idle process is constant on every interval of $[0,\infty)$ on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.
• Lipschitz continuity of the paths is not assumed; it follows from the monotonicity conditions.
• $m_k > 0$ is an explicit hypothesis; the paper takes it for granted.
• Priorities are Equiv.Perm (Fin K), FBFS is the identity; $|Q(0)|$ is $\sum_k Q_k(0)$.
• In Lemma 2.2 (ii) the printed strict "$\dot g(t) < -\varepsilon$" is relaxed to "$\le -\varepsilon$", as every application requires; absolute continuity is dropped from Lemma 2.2 (i), where it is not needed. Both changes strengthen the lemma.
• In the inductive step, "stay empty for $t > t_{k-1}$" is read as $t \ge t_{k-1}$, and the case $Q_k(t_{k-1}) = 0$ is included.
• The stochastic network is not formalized; only the fluid model is.

A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with $|Q(0)| = 1$, so stability is not vacuous.

Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1) (1996) 115–134. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1) (1995) 49–77. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13 (1993) 87–110. https://doi.org/10.1007/BF01149327
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12) (1991) 1406–1416. https://doi.org/10.1109/9.106159

Motivation

Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown demand (facilities, servers, sensors that must serve clients as they appear) and is the prototype for a family of online covering problems.

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009) gave the first deterministic algorithm, with competitive ratio $O(\log m\log n)$ for $n$ elements and $m$ sets, and showed that no deterministic algorithm does better than $\Omega(\log m\log n/(\log\log m+\log\log n))$ on some instances. Buchbinder and Naor (Math. Oper. Res. 2009) recast the fractional part of that algorithm as an instance of a general online primal-dual scheme for covering and packing linear programs, and turned an offline pessimistic estimator of Srinivasan into an online potential function. The result, in their Section 5.1, is a deterministic algorithm whose ratio $O(\log d\log(n/OPT))$ depends on the maximum element frequency $d$ instead of the number of sets $m$, and on the ratio $n/OPT$ instead of $n$.

Timeline:

• 2003 (conference), 2009 (journal): Alon et al., deterministic $O(\log m\log n)$ for unweighted online set cover, with a potential $\sum_{j\notin C} n^{2w_j}$.
• 2005 (conference), 2009 (journal): Buchbinder and Naor, the general online fractional covering/packing scheme, and the derandomized rounding of this mission.

Setting

A set-cover instance consists of a finite ground set $X$ of $n$ elements and a finite family $\mathcal S$ of $m$ sets. For an element $e$, $\mathcal S_e$ is the collection of sets containing $e$, and $d$ bounds its size: $|\mathcal S_e|\le d$ for every $e$ (the frequency). In the unweighted problem every set costs $1$.

Elements arrive in a list $\sigma$. The algorithm maintains:

• fractional weights $w(s)\ge 0$ for the sets, produced by the paper's Section 3 scheme with $\{0,1\}$ coefficients: when an element $e$ arrives that is not yet fractionally covered ($\sum_{s\in\mathcal S_e}w(s)<1$), its dual variable $y(e)$ is raised to the least value at which

$$w(s)=\max\Big\{w(s),\ \tfrac1d\Big(\exp\Big(\tfrac{B}{2c(s)}\textstyle\sum_{k:\ s\ni e_k}y(e_k)\Big)-1\Big)\Big\}\qquad(s\ni e)$$

gives $\sum_{s\in\mathcal S_e}w(s)\ge 1$; here $B>0$ is a parameter;

• a cover $\mathcal C\subseteq\mathcal S$ that only grows; $C$ is the set of elements covered by $\mathcal C$.

With $f(e)=\min\{1,\exp(-\alpha+\alpha\sum_{s\ni e}w(s))\}$, the potential is $\Phi=\Phi_1+\Phi_2$ with

$$\Phi_1=1-\prod_{e\in X\setminus C}\big(1-f(e)\big),\qquad \Phi_2=\exp\Big(\sum_{s\in\mathcal S}\big((\ln 2)\chi_{\mathcal C}(s)-\alpha w(s)\big)-OPT\Big),$$

where $OPT$ is the optimum number of sets covering the arrived elements, assumed known, $r=e\ln(e/(e-1))$ and $\alpha=\max\{1,\ln(rn/OPT)\}$. The rounding rule: each time the weight of a set $s$ is augmented, $s$ is added to $\mathcal C$ if this does not increase $\Phi$.

Formalization targets

Goal: Lemma 5.2

Every arriving element is covered by $\mathcal C$, and at every time

$$|\mathcal C|\ \le\ \frac{\big(2\alpha\ln(1+d)+1\big)\,OPT}{\ln 2},\qquad \alpha=\max\Big\{1,\ln\frac{rn}{OPT}\Big\}.$$

This is the paper's $OPT\cdot O(\log d\log(n/OPT))$ with the constant its proof gives.

Milestones

1. Theorem 3.2 (covering half): for every $B>0$, the $\{0,1\}$ scheme with frequency bound $\ell$ yields a fractional cover of cost at most $2\ln(1+\ell)$ times that of any fractional cover.
2. Lemma 5.1 (i): initially $\Phi\le 1$; $\Phi>0$ in every state.
3. Lemma 5.1 (ii): after the weight of a set is augmented by $\delta\ge0$, taking the set or excluding it leaves $\Phi$ no larger than before.

Significance

The bound improves Alon et al.'s $O(\log m\log n)$ whenever sets are many but each element lies in few of them ($d\ll m$), and whenever the optimum is large compared with $n$. It also shows that the fractional part and the rounding part of an online covering algorithm can be designed separately: any online fractional solution with a competitive guarantee can be rounded deterministically by an online potential function. The same method gives the routing result of Section 5.2 of the paper.

As far as is known, none of these results is machine-checked. Related formal work on the platform covers Alon et al.'s algorithm and its $O(\log m\log n)$ bound (a different potential and a different fractional update), and the general covering scheme of Buchbinder and Naor's monograph; neither states Lemma 5.1 or Lemma 5.2, nor Theorem 3.2 for the $\{0,1\}$ scheme with $\ell$ in place of $n$. A complete development here would give a verified derandomized rounding argument, reusable for other online covering problems.

Difficulty

The difficulty is not in the final inequality, which follows from $\Phi_2\le1$ in one line, but in keeping $\Phi\le1$ throughout. The decision to take a set must be made with no knowledge of future elements, and the potential has to account for elements that may never arrive: $\Phi_1$ ranges over the whole ground set. Lemma 5.1 (ii) asks that, for every current state, one of the two decisions does not increase a non-linear function of all uncovered elements at once and this must hold for every state, not only for the states a particular run reaches. On the fractional side, Theorem 3.2 is only asserted, "along the same lines" as Theorem 3.1, so its constant has to be re-derived with $\ell$ in place of $n$ and with the scheme's continuous increase made discrete.

A tempting shortcut is to bound $|\mathcal C|$ by the number of rounds or by $\sum_s w(s)$ directly; neither gives a logarithmic factor in $n/OPT$, which comes only from the choice of $\alpha$ in $\Phi$.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (elements E, set indices T, incidence elemSets, positive costs c), with elementWeight and coveredBy. Unit costs are the hypothesis ∀ s, inst.c s = 1 in Lemma 5.2; Theorem 3.2 is stated for general positive costs. Logarithms are natural (Real.log), because they invert Real.exp.

Committed conventions:

• The fractional scheme is the discrete form of the continuous increase: in each round $y(e)$ is the least $t\ge0$ (an sInf) at which the new constraint holds. Arrival lists may repeat elements; an element already covered changes nothing.
• The rounding treats each set's increase within a round as one augmentation; the augmented sets are processed one at a time in the order of a list ord containing every set, and a set is added when $\Phi(w+\delta_s\mathbf 1_s,\mathcal C\cup\{s\})\le\Phi(w,\mathcal C)$. Lemma 5.2 holds for every order.
• The algorithm is a function, so every run exists.
• $OPT$ is a natural number $\ge1$ bounding the size of some cover of the arrived elements; $d\ge1$ bounds the frequency of every element. At the true optimum and the maximum frequency this is the paper's statement.
• Explicit constants replacing $O(\cdot)$: Theorem 3.2's $O(\log\ell)$ is $2\ln(1+\ell)$; Lemma 5.2's $OPT\cdot O(\log d\log(n/OPT))$ is $(2\alpha\ln(1+d)+1)\,OPT/\ln2$ with $\alpha=\max\{1,\ln(rn/OPT)\}$.
• The proof of Lemma 5.1 (i) on p. 13 prints $d$ where $r$ is meant ("$\exp(-dne^{-\alpha})$", "$\alpha\ge\ln(dn/OPT)$"); the statement uses $r$, and $r$ is printed "$e\ln(e/e-1)$" for $e\ln(e/(e-1))$.

Not in scope: the packing half of Theorem 3.2, Theorem 3.1 for general coefficients, and the doubling wrapper of p. 12 that removes the assumption that $OPT$ is known. The guarantee is for the algorithm run with the stated $\alpha$; a formalization in which $\Phi$'s product ranges only over arrived elements, or in which the weights or the chosen family are free variables constrained by hypotheses instead of being produced by the algorithm ($OPT$ is an input of the algorithm, as the page assumes it known), would be a different and weaker statement and is ruled out.

Contributions welcome: proofs of the three milestones and of the goal, and general lemmas about the fractional round (attainment of the least $t$, monotonicity of the weights) that other online covering missions can reuse.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0363
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946
• A. Srinivasan, Improved approximation guarantees for packing and covering integer programs, SIAM Journal on Computing 29(2), 1999. https://doi.org/10.1137/S0097539796314240
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

Motivation

Network revenue management decides, in real time, which customer requests to accept when every request consumes a bundle of scarce, perishable resources: seats on several flight legs of an itinerary, room-nights of a multi-night hotel stay, bandwidth on several links. The exact dynamic program is intractable for realistic networks, so practice and theory rely on heuristics built from a deterministic linear program (DLP) that replaces random demand by its mean. The question is how much revenue such heuristics lose.

The classical answer (Gallego and van Ryzin 1994, 1997; Talluri and van Ryzin 1998) is that solving the DLP once and following its solution loses $O(\sqrt T)$ over a horizon of length $T$. Re-solving the DLP as capacity is consumed was long believed to help, and Jasin and Kumar (2012) proved that re-solving in every period has bounded loss if the DLP solution is nondegenerate. Bumpensanti and Wang (arXiv:1802.06192v3) showed that the nondegeneracy condition matters: frequent re-solving can lose $\Omega(\sqrt T)$ on degenerate instances. They then proposed a policy, Infrequent Re-solving with Thresholding (IRT), whose loss is bounded by a constant independent of the horizon and of the capacities, with no nondegeneracy assumption. This mission formalizes that result.

Setting

There are $n$ customer classes $j \in [n]$ and $m$ resources $l \in [m]$. Class-$j$ customers arrive as independent Poisson processes of rate $\lambda_j > 0$ on $[0, T]$. Accepting a class-$j$ customer earns $r_j \ge 0$ and consumes $a_{lj} \ge 0$ units of resource $l$; $A = (a_{lj})$ is the bill-of-materials matrix with columns $A_j$, and $C \in \mathbb R^m_{\ge 0}$ is the initial capacity. A customer can be accepted only if $A_j \le C'$ componentwise, $C'$ being the remaining capacity; leftover capacity is worthless at $T$.

The DLP with right-hand side $b$ is

$$\max_x \Big\{ \sum_j r_j x_j \ \Big|\ \sum_j A_j x_j \le b,\ 0 \le x_j \le \lambda_j \Big\},$$

and $v^{\mathrm{DLP}}(T, C)$ is $T$ times its value at $b = C/T$. The hindsight optimum is $v^{\mathrm{HO}}(T, C) = \mathbb E[V^{\mathrm{HO}}]$, where $V^{\mathrm{HO}}$ is the value of the same LP with capacity $C$ and the realized demands $\Lambda_j(T) \sim \mathrm{Poisson}(\lambda_j T)$ as upper bounds. It bounds the expected revenue of every non-anticipating policy, and the regret of a policy $\pi$ is $v^{\mathrm{HO}} - v^\pi$.

A probabilistic allocation on a window accepts each class-$j$ arrival with a fixed probability $p_j$ when capacity allows. The IRT policy uses $\tau_u = T^{(5/6)^u}$ and re-solving times $t^*_u = T - \tau_u$ for $u = 0, \dots, K$, where $K = \lceil \log\log T / \log(6/5)\rceil$. At $t^*_u$ it solves the DLP with right-hand side $C(t^*_u)/\tau_u$ (remaining capacity over remaining time), obtaining $x^u$. In the epochs $u < K$ it accepts class $j$ with probability $0$ if $x^u_j < \lambda_j\tau_u^{-1/4}$, else $1$ if $x^u_j > \lambda_j(1 - \tau_u^{-1/4})$, else $x^u_j/\lambda_j$; in the last epoch $[t^*_K, T]$ it uses $x^K_j/\lambda_j$. The family $\mathrm{IRT}^{K'}$ re-solves $K'$ times on the same schedule; $\mathrm{IRT}^0$ is static probabilistic allocation (SPA), and $\mathrm{HO}^{K'}$ follows $\mathrm{IRT}^{K'}$ until $t^*_{K'}$ and then earns the hindsight optimum of what remains.

Formalization targets

Goal: Theorem 1 (p. 16)

There is a constant $M = M(\lambda, r, A)$ such that for every horizon $T \in \{1, 2, \dots\}$ and every capacity vector $C \ge 0$,

$$v^{\mathrm{HO}}(T, C) - v^{\mathrm{IRT}}(T, C) \le M .$$

The constant is not fixed; the content is its independence of $T$, of $C$, and of the optimal LP solution chosen at each re-solve.

Milestones

• $v^{\mathrm{HO}} \le v^{\mathrm{DLP}}$ (Sec. 2.2.2, p. 9).
• Lemma 4 (p. 37): $\mathbb P(|X - \mu| \ge x) \le 2e^{-x^2/(3\mu)}$ for $X \sim \mathrm{Poisson}(\mu)$, $0 < x \le \mu$.
• Proposition 5 (p. 27): $v^{\mathrm{DLP}} - v^{\mathrm{SPA}} \le M\sqrt T$, uniformly in $C$.
• Proposition 1 (p. 16): with one re-solve at $T - T^{5/6}$,

$$v^{\mathrm{HO}} - v^{\mathrm{HO}^1} \le M T e^{-\kappa T^{1/6}},\qquad v^{\mathrm{HO}} - v^{\mathrm{IRT}^1} \le M T e^{-\kappa T^{1/6}} + M T^{5/12}.$$

• Eq. (13) (p. 29): for every $K'$,

$$v^{\mathrm{HO}} - v^{\mathrm{IRT}^{K'}} \le M\sum_{u=0}^{K'-1} T^{(5/6)^u} e^{-\kappa T^{(5/6)^u/6}} + M T^{(5/6)^{K'}/2}.$$

• p. 30: $T^{(5/6)^{K}} \le e$, and the right-hand side of (13) at $K' = K(T)$ is bounded uniformly in $T \ge 1$.

Significance

The result separates two design choices in re-solving heuristics: how often to re-solve and how to turn an LP solution into a control. It shows that re-solving only $O(\log\log T)$ times, combined with rounding nearly-degenerate acceptance probabilities to $0$ or $1$, is enough for bounded regret, and that the constant is uniform over all capacity-to-horizon ratios, so degenerate DLP solutions, which occur only at particular ratios, cause no loss of order. Since $v^{\mathrm{HO}} \ge v^*$, it also shows that the hindsight optimum is within a constant of the optimal policy's value in this model.

The result is proved on paper but not machine-checked. A formalization would produce a reusable Poisson-arrival revenue-management model, a precise account of the regret decomposition over re-solving epochs, and an independent check of a proof with known gaps (see Difficulty). No part of it is formalized on the platform.

Difficulty

The obvious argument compares the policy with the DLP solution and controls the deviation of Poisson demand by its standard deviation; this gives only $O(\sqrt T)$, because the DLP value exceeds the hindsight optimum by order $\sqrt T$ and the lost sales accumulate. Bounded regret needs a comparison with the hindsight LP, path by path: the acceptances made before the last re-solve must remain extendable to a hindsight-optimal solution with overwhelming probability. This requires LP sensitivity of the hindsight solution to the random right-hand side, uniformly over the degenerate cases, and the printed proof's statement of it (Lemma 5) is false as printed: on a two-class, single-resource instance its interval for $\bar z_1$ is empty. A correct argument needs a proximity bound for optimal LP solutions under a change of the demand bounds, summed over all classes, not only over $J_\lambda = \{j : x^*_j = \lambda_j\}$. The analysis of the schedule (the sum over epochs in (13)) is elementary but the printed chain of inequalities on p. 30 uses a monotonicity that fails for large arguments.

Formalization scope

All objects are in the definition item ResolvingNRM.IRT.Model. Classes are Fin n, resources Fin m, A : Matrix (Fin m) (Fin n) ℝ. LP values reuse piValue from the published RLPBidPrice.Unbiased.Model; the hindsight LP is over real $z$, as in (3). Expectations are explicit sums of Poisson weights. A window of probabilistic allocation is represented by its Poisson count of arrivals, i.i.d. classes with law $\lambda_j/\sum_i\lambda_i$ and independent Bernoulli acceptance coins, the standard representation for controls constant on the window. Policies are backward recursions over the re-solving epochs. Ties in the LP are left open: a policy takes an arbitrary optimal-solution selector, and every theorem quantifies over all selectors after its constants.

Conventions and deviations from the page, each disclosed in the item concerned:

• Standing assumptions of Sec. 2 (p. 7), left implicit there: $\lambda_j > 0$, $r \ge 0$, $A \ge 0$, $C \ge 0$.
• "$O(g)$" is read as: there is $M$, depending only on $(\lambda, r, A)$, with the bound $\le M g(T)$ for all $T \ge 1$ (or $T > 0$) and all $C \ge 0$.
• Milestones applied to sub-horizons $T^{(5/6)^u}$ take a real $T$; the goal takes $T \in \mathbb N$.
• Lemma 4 is stated for $0 < x \le \mu$; as printed (all $x > 0$) it is false, e.g. $\mu = 1$, $x = 5$.
• In Proposition 1 and (13), $\kappa > 0$ is existential and uniform in $C$; the printed $\kappa$ depends on $J_\lambda$ and is derived through Lemma 5.
• (13) is stated for every number $K'$ of re-solves.
• Algorithm 3 prints the re-solve right-hand side as $C(t^*_k)/\tau_k$; it is read with index $u$.
• For $1 \le T \le e$ the formula for $K$ is undefined or negative; the formalization takes $K = 0$, so IRT is SPA there.
• The optimal policy value $v^*$ and the paper's constant $\alpha$ are not defined; Lemmas 5 and 6 are not stated.

A statement that lets $M$ depend on $T$ or $C$, compares IRT with the DLP instead of the hindsight optimum, uses a fixed number of re-solves, or assumes a nondegenerate or vertex LP solution is trivial or a different theorem, and is ruled out by the quantifier order of the goal. The milestone $T^{(5/6)^K} \le e$ has a sorry-free local check.

Welcome contributions: LP proximity results (Cook–Gerards–Schrijver–Tardos type), Poisson concentration, superposition and thinning of Poisson processes, and lemmas on expectations of LP values. The source is arXiv:1802.06192v3; its printed page numbers equal the PDF page numbers.

Selected references

• P. Bumpensanti, H. Wang, A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv:1802.06192v3, 2018; Management Science 66(7), 2020. https://arxiv.org/abs/1802.06192
• S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2), 2012. https://doi.org/10.1287/moor.1110.0530
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• K. Talluri, G. van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11), 1998. https://doi.org/10.1287/mnsc.44.11.1577
• M. Reiman, Q. Wang, An Asymptotically Optimal Policy for a Quantity-Based Network Revenue Management Problem, Mathematics of Operations Research 33(2), 2008. https://doi.org/10.1287/moor.1070.0288
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity Theorems in Integer Linear Programming, Mathematical Programming 34, 1986. https://doi.org/10.1007/BF01582230

Motivation

Operations research has long studied the stochastic problem $\min_{z\in\mathcal Z}\mathbb E[c(z;Y)]$: choose a decision $z$ before an uncertain quantity $Y$ (demand, prices, returns) is revealed. In practice the decision maker also observes covariates $X$ before deciding (web-search volume before stocking a product, weather before routing a shipment) and should solve the conditional problem instead. Bertsimas and Kallus (arXiv:1402.5481v4; Management Science 66(3), 2020) proposed predictive prescriptions: reweight historical observations $(x^i,y^i)$ by how relevant they are to the current $x$, using weights borrowed from a nonparametric regression method, and minimize the reweighted sample cost. Their asymptotic theorems guarantee that this procedure converges to the decision that full knowledge of the conditional distribution would give.

The unconditional special case, sample average approximation (SAA) with i.i.d. draws of $Y$ and no covariate, has a classical consistency theory (Dupačová–Wets 1988; Shapiro 2003). This mission conditions that theory on $X$, with $k$-nearest-neighbour weights.

Setting

Decisions $z$ lie in a set $\mathcal Z\subseteq\mathbb R^{d_z}$, covariates $X$ in $\mathcal X\subseteq\mathbb R^{d_x}$, uncertainty $Y$ in $\mathcal Y\subseteq\mathbb R^{d_y}$; all three spaces carry the Euclidean norm. A cost $c(z;y)\in\mathbb R$ is given. Let $\mu$ be the joint law of $(X,Y)$, $\mu_X$ the law of $X$ and $\mu_{Y|x}$ the conditional law of $Y$ given $X=x$. The conditional cost and the full-information problem (2) are

$$C(z\mid x)=\mathbb E\big[c(z;Y)\mid X=x\big],\qquad v^*(x)=\min_{z\in\mathcal Z}C(z\mid x),\qquad \mathcal Z^*(x)=\arg\min_{z\in\mathcal Z}C(z\mid x).$$

The data are $S_N=\{(x^1,y^1),\dots,(x^N,y^N)\}$, the first $N$ terms of an i.i.d. sequence with law $\mu$. The kNN weights (12) are $w_{N,i}(x)=\frac1k\mathbb I[x^i$ is one of the $k$ nearest neighbours of $x$ among $x^1,\dots,x^N]$, with ties among equidistant points broken by lower index first. The predictive prescription (3) is any

$$\hat z_N(x)\in\arg\min_{z\in\mathcal Z}\ \widehat C_N(z\mid x),\qquad \widehat C_N(z\mid x)=\sum_{i=1}^N w_{N,i}(x)\,c(z;y^i).$$

The paper's standing assumptions: Assumption 3 ($\mathbb E|c(z;Y)|<\infty$ for every $z\in\mathcal Z$, and $\mathcal Z^*(x)\ne\emptyset$ for a.e. $x$); Assumption 4 ($c(z;y)$ is equicontinuous in $z$, uniformly over $y\in\mathcal Y$); Assumption 5 ($\mathcal Z$ closed and nonempty, and either bounded, or $c$ is bounded below for large $\|z\|$ and for each $x$ there is a set $D_x$ of positive conditional probability on which $c(z;y)\to\infty$ uniformly as $\|z\|\to\infty$).

Definition 1. $\hat z_N$ is asymptotically optimal if, with probability 1, for $\mu_X$-a.e. $x$, $C(\hat z_N(x)\mid x)\to v^*(x)$; it is consistent if, with probability 1, for $\mu_X$-a.e. $x$, $\inf_{z\in\mathcal Z^*(x)}\|\hat z_N(x)-z\|\to0$.

Formalization targets

Goal: Theorem 5 (kNN), p. 19 (= Theorem 15, p. 43)

Under Assumptions 3, 4, 5 and i.i.d. sampling, with $k=\min\{\lceil CN^\delta\rceil,N-1\}$, $C>0$, $0<\delta<1$: with probability 1, for $\mu_X$-a.e. $x$, $\mathcal Z^*(x)$ is nonempty, the argmin is eventually nonempty, and every selection $\hat z_N(x)$ from it satisfies

$$\lim_{N\to\infty}C(\hat z_N(x)\mid x)=v^*(x)\qquad\text{and}\qquad\lim_{N\to\infty}\inf_{z\in\mathcal Z^*(x)}\|\hat z_N(x)-z\|=0 .$$

The goal covers both cases of Assumption 5, including unbounded $\mathcal Z$ such as the newsvendor's $[0,\infty)$.

Milestones, in the order the proof uses them

1. Walk step (proof of Theorem 15, p. 47). For any measurable $h$ with $\mathbb E|h(Y)|<\infty$, $\sum_i w_{N,i}(x)h(y^i)\to\mathbb E[h(Y)\mid X=x]$ a.s., for $\mu_X$-a.e. $x$.
2. Lemma 7 (p. 47). Fixed-$z$ and fixed-$D$ almost-sure convergence upgrade to convergence for all $z\in\mathcal Z$ simultaneously and weak convergence $\hat\mu_{Y|x,N}\to\mu_{Y|x}$, off one null set.
3. Lemma 5 (p. 45). Along one sample path, pointwise convergence $\widehat C_N(\cdot\mid x)\to C(\cdot\mid x)$ is uniform on compact subsets of $\mathcal Z$.
4. Lemma 6, case 1 (pp. 45–47). For bounded $\mathcal Z$, the minima and minimizers of $\widehat C_N(\cdot\mid x)$ converge to $v^*(x)$ and to $\mathcal Z^*(x)$.

Significance

Theorem 5 says that a decision computed from data alone, with no model of the conditional distribution, performs asymptotically as well as the decision a decision maker with full knowledge of $\mu_{Y|x}$ would take, for almost every covariate value and under mild conditions on the cost. It justifies the kNN prescription in the paper's newsvendor and shipment-planning experiments, and its proof skeleton (a pointwise strong law for the weights, then Lemmas 5–7) is reused for kernel, local-linear and recursive-kernel weights (Theorems 6–9), which could follow as missions of the same shape.

The result is proved in the paper; it has not been machine-checked anywhere. Formalizing it requires a strong law for nearest-neighbour regression with integrable responses (Walk 2010, building on Devroye, Györfi, Krzyżak and Lugosi 1994), which Mathlib does not have, and a careful treatment of conditional laws at a point. One of the paper's lemmas (Lemma 6) is false as printed for unbounded $\mathcal Z$; the formalization isolates the correct statement.

Difficulty

The deterministic optimization part (Lemmas 5 and 6 for bounded $\mathcal Z$) is a compactness argument. The central difficulty is the probabilistic input. A natural first idea, applying the strong law of large numbers to $\widehat C_N(z\mid x)$, fails: the kNN weights depend on all of $x^1,\dots,x^N$ and on $x$, the effective sample size $k_N$ grows sublinearly, and convergence is required for almost every $x$ simultaneously, including $x$ that are atoms of $\mu_X$ where ties are the rule. A second difficulty is the exchange of quantifiers: the strong law gives a null set depending on $z$ and on the set $D$, and the conclusion needs one null set for all $z\in\mathcal Z$. Finally, for unbounded $\mathcal Z$ the minimizers of $\widehat C_N(\cdot\mid x)$ must be kept bounded, and weak convergence of $\hat\mu_{Y|x,N}$ alone does not do so.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d), so kNN distances and $\|z-z'\|$ are Euclidean. The data are a measurable, mutually independent sequence S i : Ω → ℝ^{d_x} × ℝ^{d_y} with each term of law $\mu$; samples are indexed from $0$. The following readings are explicit in the Lean:

• $\mu_{Y|x}$ is the fixed version μ.condKernel x of the conditional law, and $C(z\mid x)$ is its Bochner integral; Assumption 5's "for every $x\in\mathcal X$" refers to this version, and $D_x$ is measurable.
• Quantifier order is "with probability 1, for $\mu_X$-a.e. $x$" (Definition 1), and the selection $\hat z_N$ is quantified inside both a.e. quantifiers: $\mathcal Z^*(x)$ is nonempty, the argmin is nonempty for all large $N$, and every sequence lying in it for all large $N$ is covered.
• $v^*(x)$ is never a real infimum; it is read as $C(z^\star\mid x)$ for $z^\star\in\mathcal Z^*(x)$, nonempty a.e. by Assumption 3.
• Ties are broken lower-index-first, so the weights sum to $1$ for $N\ge2$; at $N\le1$ the formula gives $k=0$ and all weights $0$.
• Lemmas 5–7 assume weights that are eventually nonnegative and sum to $1$, the reading of the paper's $\mathbb E_{\hat\mu_{Y|x,N}}$ notation; weak convergence is tested against bounded continuous functions.
• Lemma 6 is posed for bounded $\mathcal Z$ only, without its unused weak-convergence hypothesis; the goal is posed for both cases.

A formalization that replaces the conditional law by an arbitrary kernel unrelated to $\mu$, takes $\hat z_N$ to be a fixed measurable selection chosen outside the almost-sure quantifier, or reads $\inf_{z\in\mathcal Z^*(x)}$ on an empty set as $0$ without Assumption 3 would trivialize or weaken the result and is ruled out by the statements above.

Needed infrastructure: nearest-neighbour ranks and their combinatorics (Stone's lemma: a point is among the $k$ nearest neighbours of at most a bounded number of others), a strong law for kNN regression, portmanteau-type characterizations of weak convergence for weighted empirical measures, and stability of minimizers under locally uniform convergence. The kNN strong law and the stability lemmas are reusable well beyond this mission. Related platform items, credited but not reused (they concern unconditional SAA): SolutionQuality.SRP.prop1_i, SolutionQuality.SRP.prop1_ii, SolutionQuality.SRP.fbar_tendstoUniformlyOn (Bayraksan–Morton 2006) and DupacovaWets.Consistency.consistency_of_measurable_estimates (Dupačová–Wets 1988). Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481v4 , https://doi.org/10.1287/mnsc.2018.3253
• H. Walk, Strong laws of large numbers and nonparametric estimation, in Recent Developments in Applied Probability and Statistics, Physica-Verlag, 2010. https://doi.org/10.1007/978-3-7908-2598-5_8
• L. Devroye, L. Györfi, A. Krzyżak, G. Lugosi, On the strong universal consistency of nearest neighbor regression function estimates, Annals of Statistics 22(3), 1994. https://doi.org/10.1214/aos/1176325633
• J. Dupačová, R. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4), 1988. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Monte Carlo sampling methods, in Handbooks in OR & MS 10, 2003. https://doi.org/10.1016/S0927-0507(03)10006-0

Motivation

Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule $z(\cdot)$ from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.

The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.

Setting

Covariates $x$ take values in a measurable space $\mathcal X$, the uncertain quantity $y$ in a measurable space $\mathcal Y$, and decisions $z$ in $\mathbb R^{d}$, unconstrained. Data are an i.i.d. sample $S_N=((x^1,y^1),\dots,(x^N,y^N))$ from a probability measure $\mu$ on $\mathcal X\times\mathcal Y$, and $S_N^x=(x^1,\dots,x^N)$ is its covariate part. A cost $c(z;y)$ is incurred when decision $z$ meets outcome $y$. A decision rule is a measurable map $z(\cdot):\mathcal X\to\mathbb R^d$; $\mathcal F$ is a class of decision rules. Its expected cost is $\mathbb E[c(z(X);Y)]$, and its empirical cost is $\frac1N\sum_{i=1}^N c(z(x^i);y^i)$, the objective of problem (4).

The empirical multivariate Rademacher complexity of $\mathcal F$ (Definition 3) on a sample $s_1,\dots,s_N$ is

$$\widehat{\mathfrak R}_N(\mathcal F;S_N)=\mathbb E_\sigma\Big[\frac2N\sup_{g\in\mathcal F}\sum_{i=1}^N\sum_{k=1}^d\sigma_{ik}\,g_k(s_i)\Big],$$

with $\sigma_{ik}$ independent uniform signs, and the marginal complexity $\mathfrak R_N(\mathcal F)$ is its expectation over the sample. For real-valued classes ($d=1$) these are the usual Rademacher complexities with factor $2/N$ and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.

Formalization targets

Goal: Theorem 13 (out-of-sample guarantees)

If $0\le c(z;y)\le\bar c$ and $|c(z;y)-c(z';y)|\le L\|z-z'\|_\infty$, then for any $\delta>0$ each of the following holds with probability at least $1-\delta$:

$$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+\bar c\sqrt{\frac{\log(1/\delta)}{2N}}+L\,\mathfrak R_N(\mathcal F)\quad\forall z\in\mathcal F,\tag{26}$$ $$\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+3\bar c\sqrt{\frac{\log(2/\delta)}{2N}}+L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)\quad\forall z\in\mathcal F.\tag{27}$$

In particular they hold for the empirical risk minimizer. The goal is stated for a general class $\mathcal F$, not only the linear rules (25).

Milestones

1. Lemma 1 (comparison): for $\mathcal G=\{(x,y)\mapsto c(f(x);y):f\in\mathcal F\}$, $\widehat{\mathfrak R}_N(\mathcal G;S_N)\le L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)$ and $\mathfrak R_N(\mathcal G)\le L\,\mathfrak R_N(\mathcal F)$.
2. Theorem 14 (29): for a class $\mathcal G$ of functions with values in $[0,\bar g]$, with probability at least $1-\delta$, $\mathbb E g\le\frac1N\sum_i g(u^i)+\bar g\sqrt{\log(1/\delta)/(2N)}+\mathfrak R_N(\mathcal G)$ for all $g\in\mathcal G$.
3. Theorem 14 (30): the data-dependent version with $3\bar g\sqrt{\log(2/\delta)/(2N)}+\widehat{\mathfrak R}_N(\mathcal G;S_N)$.

Significance

Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as $N\to\infty$.

The results are known: (29) and (30) for $[0,\bar g]$-valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the $\infty$-norm vector comparison inequality of Lemma 1 with constant $1$. None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant $\sqrt{8\ln(2/\delta)/n}$), Maurer's Euclidean vector contraction with constant $\sqrt2$ (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.

Difficulty

The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a $d$-dimensional output; applying it coordinatewise loses a factor of $d$, and Euclidean vector contraction loses $\sqrt2$ and uses the wrong norm. Lemma 1 needs an argument specific to the $\infty$-norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.

Formalization scope

Decisions are Fin d → ℝ, whose Lean norm is the $\infty$-norm; $\mathcal X$, $\mathcal Y$ are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with $N\ge1$. The following readings are explicit:

• Each "with probability at least $1-\delta$, … for all $z\in\mathcal F$" is a bound $\le\delta$ on the outer measure of the set of samples where the inequality fails for some $z$; the quantifier over the class is inside the event.
• Empirical complexities are in EReal (an unbounded class gives $+\infty$), marginal ones are lower Lebesgue integrals in $[0,\infty]$; $0\cdot\infty=0$.
• The paper assumes only $\sup c\le\bar c$ (resp. $|g|\le\bar g$). With that alone (26) and (29) are false — a two-point outcome with a constant rule violates them with probability $1/2$ — so the costs are assumed to take values in $[0,\bar c]$, keeping every printed constant.
• The undefined $\delta',\delta''$ are $\delta$ (the i.i.d. case of the paper's Theorem 21); the Lipschitz denominator printed as $\|z_k-z'_k\|_\infty$ is $\|z-z'\|_\infty$.
• Decision rules and the cost are measurable and the class is pointwise separable (a countable subclass approximates every member pointwise). The paper takes probabilities and expectations of suprema over the class without comment; without such a convention the statement fails for pathological classes.

A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk $0$ for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.

Selected references

• D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481 , https://doi.org/10.1287/mnsc.2018.3253
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, JMLR 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• M. Ledoux, M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/
• A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, ALT 2016. https://arxiv.org/abs/1605.00251

Motivation

Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.

The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.

Setting

Fix a dimension $n\ge1$ and a continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Problem (1) minimizes $f(x)$ over the nonnegative orthant $\mathbb R_+^n=\{x:x^i\ge0\text{ for every }i\}$. The positive part $[z]^+$ replaces each negative coordinate of $z$ by zero. A feasible $x$ is critical when every partial derivative $\partial_i f(x)$ is nonnegative and $\partial_i f(x)=0$ wherever $x^i>0$. This is the paper's componentwise first-order condition.

For a feasible iterate $x_k$, the binding set is $B(x_k)=\{i:x_k^i=0\}$. The paper selects a larger working set $I_k^+$ using a fixed $\varepsilon>0$ and the projected-gradient residual $w_k=\|x_k-[x_k-M\nabla f(x_k)]^+\|$, where $M$ is fixed, diagonal and positive definite. More precisely, $I_k^+$ contains the indices with $0\le x_k^i\le\min(\varepsilon,w_k)$ and $\partial_i f(x_k)>0$. The matrix $D_k$ is symmetric positive definite and has zero off-diagonal entries in the rows indexed by $I_k^+$. The projected arc and update are

$$p_k=D_k\nabla f(x_k),\qquad x_k(a)=[x_k-a p_k]^+,\qquad x_{k+1}=x_k(\beta^{m_k}).$$

Here $0<\beta<1$, and $m_k$ is the first nonnegative integer passing the paper's two-sum Armijo test (37), with $0<\sigma<1/2$. One sum uses the scaled gradient outside $I_k^+$; the other uses the actual projected displacement on $I_k^+$. These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.

Formalization targets

The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:

$$I_k^+=B(x_k)=B(x^*)\quad\text{for all sufficiently late }k.$$

The goal is Proposition 4. Let $f$ be convex and $C^2$, let $x^*$ be the unique minimizer on $\mathbb R_+^n$ satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is $D_k=H_k^{-1}$, where $H_k$ retains Hessian entries except for off-diagonal entries touching $I_k^+$. Then

$$x_k\longrightarrow x^*,\qquad \forall c>0\ \exists K\ \forall k\ge K:\ \|x_{k+1}-x^*\|\le c\|x_k-x^*\|.$$

If the Hessian is Lipschitz in a neighborhood of $x^*$, the same proposition states an at-least-quadratic error bound: $\|x_{k+1}-x^*\|\le C\|x_k-x^*\|^2$ eventually for some $C>0$. The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.

Significance

Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.

Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.

Difficulty

A positive definite matrix by itself does not make projection along $[x-aD\nabla f(x)]^+$ a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set $I^+(x)$ can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged $I_k^+$ and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's $M$ is diag μ with every $\mu^i>0$. The run predicate includes a feasible initial point and the first acceptable integer $m_k$, and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs $D_k$ from $H_k$ and does not assume its invertibility, admissibility, convergence or eventual active-set equality.

Assumption (C) includes local $C^2$ smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no $x\ge0$ restriction, so neither does the Lean hypothesis.

A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.

Selected references

• Dimitri P. Bertsekas, Projected Newton Methods for Optimization Problems with Simple Constraints, SIAM Journal on Control and Optimization 20(2), 221–246, 1982. DOI: 10.1137/0320018.