The OR Formalization Drive

Motivation

Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)

The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses $(1,k)$-configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

Setting

Fix a finite index set $K$, positive rational coefficients $a_j$ for $j\in K$, and a rational right-hand side $a_0$. A zero–one solution is a vector with each $x_j\in\{0,1\}$ satisfying the single row

$$\sum_{j\in K}a_jx_j\le a_0. \tag{2.5}$$

The model uses the support set $x=\{j:x_j=1\}$ for such a vector. A set $S\subseteq K$ is a minimal cover when its total coefficient exceeds $a_0$, but removing any one member makes the total at most $a_0$:

$$\sum_{j\in S}a_j>a_0, \qquad \sum_{j\in S}a_j-a_k\le a_0\quad(k\in S). \tag{2.6}$$

It yields the cover inequality $\sum_{j\in S}x_j\le |S|-1$ for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when $S$ is empty.

A $(1,k)$-configuration consists of $S^*\subseteq K$, $t\notin S^*$ and an integer $2\le k\le |S^*|$. The set $S^*$ itself fits the row, while $Q\cup\{t\}$ is a minimal cover for every $k$-element subset $Q$ of $S^*$. For any $k\le r\le |S^*|$ and $r$-element $T\subseteq S^*$, its inequality is $(r-k+1)x_t+\sum_{j\in T}x_j\le r$. Crowder, Johnson and Padberg (1983), pp. 810–811

For a point $\bar x\in[0,1]^K$, the separation problem asks for a cover $s\subseteq K$ minimizing $\sum_{j\in s}(1-\bar x_j)$, subject to the strict condition $\sum_{j\in s}a_j>a_0$. This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value $z$ is therefore asserted only when a least attainable value exists.

Formalization targets

Cover separation

The goal is the paper's Section 2.3 equivalence:

$$\left(\exists S\subseteq K\text{ minimal}: \sum_{j\in S}\bar x_j>|S|-1\right) \quad\Longleftrightarrow\quad z<1,$$

where $z$ is the attained optimum of (2.12). A cover inequality cuts off $\bar x$ precisely when its left-hand side exceeds $|S|-1$. If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813

Valid inequalities and lifting

The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, $z_k$ is the maximum integer objective value in (2.10), $\bar z_k$ is the maximum in its linear relaxation, and $z_k^*=\lfloor\bar z_k\rfloor$. The claims are $z_k\le z_k^*$ and validity after adding variable $k$ with coefficient $f_k=f_0-z_k^*$. They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814

Significance

The equivalence turns a geometric question about which cover inequality excludes $\bar x$ into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.

Difficulty

Checking all subsets of $K$ directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when $\bar x_j=1$. The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814

Formalization scope

Lean uses an arbitrary finite index type for $K$, replacing the paper's indices $1,\ldots,n$. A zero–one vector is a finite support set. Row coefficients and $a_0$ are rational, as on p. 810; the point $\bar x$ and separation values are real. The target asks only that $\bar x$ lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on $a_0$.

The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions $|S|-1$ and $r-k+1$ are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.

Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set $S$. After adding $k$, it ranges over support in $S\cup\{k\}$. The final inequality covers the whole row when that set is $K$. The development must preserve the full quantifier over every $k$-subset in (2.8) and every $r$ and $T$ in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.

Selected references

• H. Crowder, E. L. Johnson and M. Padberg, Solving Large-Scale Zero-One Linear Programming Problems, Operations Research 31(5), 803–834, 1983. DOI: 10.1287/opre.31.5.803

Motivation

A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.

Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.

Setting

A reentrant line has stations $1,\dots,I$ and classes $1,\dots,K$. Fluid enters class $1$ at rate $1$, moves from class $k$ to class $k+1$ on service, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and rate $\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 traffic condition (1.7) is $\rho_i < 1$ for every $i$.

A fluid model solution is a pair $(Q, T)$: $Q_k(t) \ge 0$ is the fluid in class $k$ at time $t$ and $T_k(t)$ the cumulative service time given to class $k$ by time $t$. They satisfy, for $t \ge 0$,

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t) \quad (\mu_0 T_0(t) = t),$$

$T_k(0) = 0$ with $T_k$ nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, where $B_i(t) = \sum_{k\in C_i} T_k(t)$, is nondecreasing. The solution is work-conserving if $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

The line is of Kelly type with station means $\beta_1, \dots, \beta_I$ if $m_k = \beta_{\sigma(k)}$ for every class $k$. Its routing has no immediate feedback if $\sigma(k+1) \ne \sigma(k)$ for every $k < K$. A set of fluid solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution in the set with $|Q(0)| = \sum_k Q_k(0) = 1$ is empty from time $\delta$ on.

Formalization targets

Goal: Theorem 6.1

For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is $\delta > 0$ with

$$\sum_k Q_k(0) = 1 \ \Longrightarrow\ Q_k(t) = 0 \quad \text{for all } t \ge \delta,\ k = 1,\dots,K,$$

for every work-conserving fluid solution $(Q,T)$. The number of classes $K$ is arbitrary, of either parity, and the route may start at either station.

Milestones

The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity $G_i(t) = G_i(0) + |C_i|t - B_i(t)/\beta_i$ for $G_i = \sum_{k\in C_i} Q_k^+$, with $Q_k^+ = \sum_{l\le k} Q_l$; the comparison $W_i(t) = 0 \Rightarrow G_i(t) \le G_j(t)$; and the verification that $G_1, G_2$ meet the hypotheses of Lemma 3.2 with $\varepsilon_i = 1/\beta_i - |C_i|$.

Significance

The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line $1,2,2,2,1,1$ with all means $0.3$), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.

Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.

Difficulty

The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components $G_i = \sum_{k\in C_i}Q_k^+$ each decrease at the constant rate $1/\beta_i - |C_i|$ while station $i$ is busy. When station $i$ is idle, $G_i$ can grow, and the argument then needs the comparison $G_i \le G_j$, which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum $G = \max(G_1, G_2)$ need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd $K$ is not printed ("can be proved similarly"), and the formal goal covers it.

Formalization scope

All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.

• Classes and stations are 0-based (Fin K, Fin I). The paper's class $k$ is Lean k - 1.
• Paths are total functions ℝ → Fin K → ℝ, and every equation is imposed for $t \ge 0$ only. Derivatives are taken at $t > 0$ via HasDerivAt.
• Work conservation (1.13) is stated in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. For the continuous nondecreasing $U_i$ this is equivalent to the paper's Stieltjes condition. Lipschitz continuity of the paths is not assumed, because it follows from the model.
• $m_k > 0$ is an explicit hypothesis. $|Q(0)|$ is $\sum_k Q_k(0)$.
• Stability is Definition 1.3, which constrains only solutions with $|Q(0)| = 1$.
• The paper's Theorem 6.1 says "any work-conserving policy is stable", which is stability of the queueing network (Definition 1.1). Its proof establishes stability of the work-conserving fluid model, and the queueing-level conclusion follows from the cited Theorem 1.1 (Dai 1995). The goal is the fluid statement. Theorem 1.1 and the stochastic model are not formalized.
• Lemma 2.2 (ii) is stated with the hypothesis $\dot g \le -\varepsilon$, where the page prints $<$. This is the form in which every application uses it, and it gives a stronger lemma.
• The drift identity is stated for every Kelly-type line, which implies the printed $K = 2n$ display. The printed "$G_2(t) = G_2(t) + nt - \dots$" is read as $G_2(0) + nt - \dots$.
• Condition (b) and the Lemma 3.2 check are stated for both parities of $K$ and both starting stations. A station with no classes has its $\varepsilon_i$ left free.

The goal must not be trivialized. It quantifies over all work-conserving solutions with $|Q(0)| = 1$, and this set is nonempty: a sorry-free witness with $K = 2$ is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even $K$, or to a route starting at station 1, would weaken it.

Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. 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), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979.
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Dual decomposition of dominance constraints

A stochastic dominance constraint asks a random outcome $X$ of a decision to be at least as good as a benchmark outcome $Y$ for every risk-averse decision maker: in the second-order version, $\mathbb E[u(X)] \ge \mathbb E[u(Y)]$ for every concave nondecreasing utility $u$. Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes $X_i = G_i(z)$ that depend nonlinearly on a decision $z$.

The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the $i$-th dominance constraint are a utility function $u_i$ and an almost-sure multiplier $\theta_i$ for the coupling $X_i = G_i(z)$. The dual functional splits into a part $D_0$ that involves only the decision $z$ and one part $D_i$ per dominance constraint. This mission is about the second kind of part: Theorem 4 computes $D_i$ in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.

The underlying shortfall function $F_2(X;\eta)=\int_{-\infty}^{\eta}P[X\le\alpha]\,d\alpha$ and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $\mathcal L_1$ the integrable and $\mathcal L_\infty$ the essentially bounded random variables. Fix a bounded interval $[a,b]$ ($a\le b$) and a reference outcome $Y\in\mathcal L_1$.

The utility class $\mathcal U_1([a,b])$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge 0$. For such $u$, the left derivative $u'_-(a)$ at $a$ is that slope $c$.

The concave conjugate of $v:\mathbb R\to\mathbb R$ is

$$v^*(\xi)=\inf_{t\in\mathbb R}\,[\xi t-v(t)]\in[-\infty,+\infty).$$

For a random variable $\zeta$, $v^*(\zeta)$ is the extended-real random variable $\omega\mapsto v^*(\zeta(\omega))$.

The dual functional of one dominance constraint, eq. (34), is

$$D(w,\zeta)=\sup_{X\in\mathcal L_1}\mathbb E\big[w(X)-w(Y)-\zeta X\big]\in\overline{\mathbb R},\qquad w\in\mathcal U_1([a,b]),\ \zeta\in\mathcal L_\infty .$$

The functional of eq. (35) is $f(v,\zeta)=-\mathbb E\,v^*(\zeta)$, considered on $\mathrm{Lip}(\mathbb R)\times\mathcal L_1$, where $\mathrm{Lip}(\mathbb R)$ is the space of Lipschitz functions with norm $\|v\|_{\mathrm{Lip}}=|v(0)|+\sup_{t\ne s}|v(t)-v(s)|/|t-s|$.

Formalization targets

Goal: Theorem 4

For every $v\in\mathcal U_1([a,b])$ and every $\zeta\in\mathcal L_\infty$,

$$D(v,\zeta)=-\mathbb E\big[v^*(\zeta)+v(Y)\big].$$

The formal statement has two cases. If $0\le\zeta\le v'_-(a)$ almost surely, then $v^*(\zeta)$ is a.s. finite and integrable and the identity holds between real numbers. Otherwise $D(v,\zeta)=+\infty$.

Milestones

1. Unbounded cases (proof of Theorem 4, p. 13): $P[\zeta<0]>0 \Rightarrow D(v,\zeta)=+\infty$; and $P[\zeta>v'_-(a)]>0 \Rightarrow D(v,\zeta)=+\infty$.
2. Pointwise maximizer (p. 13): for $0\le\xi\le v'_-(a)$, the function $t\mapsto v(t)-\xi t$ attains its maximum at some $t_0\in[a,b]$, so $v^*(\xi)=\xi t_0-v(t_0)$ is finite.
3. Measurable selection (p. 13): if $0\le\zeta\le v'_-(a)$ a.s., there is a measurable $X\in[a,b]$ a.s. with $X(\omega)\in\operatorname{argmax}_t[v(t)-\zeta(\omega)t]$ a.s.
4. Effective domain (p. 13): $D(v,\zeta)<+\infty \iff 0\le\zeta\le v'_-(a)$ a.s.
5. Theorem 5 (p. 14): for $\bar v\in\mathcal U_1([a,b])$, $\bar\zeta\in\mathcal L_1$ with $0\le\bar\zeta\le\bar v'_-(a)$ a.s., and a measurable maximizer selection $X$ with values in $[a,b]$, the pair $(P_X,-X)$ is a subgradient of $f$ at $(\bar v,\bar\zeta)$:

$$f(v,\zeta)\ge f(\bar v,\bar\zeta)+\int\big(v-\bar v\big)\,dP_X-\mathbb E\big[X(\zeta-\bar\zeta)\big]\quad\text{for all }(v,\zeta)\in\mathrm{Lip}(\mathbb R)\times\mathcal L_1.$$

Significance

Theorem 4 reduces an optimization over the infinite-dimensional space $\mathcal L_1$ to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier $\zeta$ (bounded between $0$ and the slope of the utility at the left end of the interval), and it makes evaluating $D$ as cheap as evaluating $v^*$. Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.

Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on $\mathbb R$ with values in $[-\infty,+\infty)$, no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.

Difficulty

The hard step is the interchange $\sup_{X\in\mathcal L_1}\mathbb E[\,\cdot\,]=\mathbb E\sup_t[\,\cdot\,]$. The inequality "$\le$" is pointwise, but "$\ge$" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where $\zeta(\omega)=0$ or $\zeta(\omega)=v'_-(a)$ the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because $\zeta$ is only essentially bounded and the test outcomes $M\mathbb 1_{\{\zeta<0\}}$ must be shown integrable.

Formalization scope

This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions $\Omega\to\mathbb R$ on a probability space with IsProbabilityMeasure P; $\mathcal L_1$ is Integrable, $\mathcal L_\infty$ is MemLp ζ ⊤ P. The conventions and explicit readings:

• $c\ge 0$ in $\mathcal U_1([a,b])$. The paper prints $c>0$. The page calls $\mathcal U_1([a,b])$ a convex cone, which must contain $0$, and the companion optimality theorem fails with $c>0$; the formalization uses $c\ge0$.
• Left derivative $v'_-(a)$ is derivWithin v (Set.Iic a) a, never deriv v a, which is $0$ at a kink.
• Extended values. $v^*$, $D$ and $f$ are EReal-valued, so an infimum equal to $-\infty$ and a supremum equal to $+\infty$ are represented, not replaced by $0$. The supremum in $D$ is over integrable $X$ only.
• Theorem 4 in two cases. The paper's right side is an expectation of an extended-real random variable, read as $+\infty$ off the domain. The statement separates the finite case (Bochner integral of the real part, with a.s. finiteness and integrability asserted) from the infinite case, which avoids extended-real subtraction.
• $f$ equals the Bochner integral of $-v^*(\zeta)$ when $v^*(\zeta)$ is a.s. finite with integrable real part, and $+\infty$ otherwise. This is exact because $-v^*(\zeta)\ge v(0)$.
• Theorem 5 adds the hypothesis that the selection lies in $[a,b]$ a.s. As printed ("for every measurable selection") it is false: with $a=-1$, $b=0$, $\bar v(t)=\min(t,0)$, $\bar\zeta=0$ on $[0,1]$ with Lebesgue measure, the selection $X(\omega)=1/\omega$ is not integrable. The continuity of $(P_X,-X)$ as a functional is stated as $X\in\mathcal L_\infty$ and the bound $\int|v|\,dP_X\le(|v(0)|+K)(1+\mathbb E|X|)$ for $K$-Lipschitz $v$.
• The paper's index $i$ and the standing data of §4 ($Y\in\mathcal L_1$, $a\le b$) are explicit binders.

A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk $0$ at $\mp\infty$), a supremum over all measurable $X$ (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited ($v=\min(t,0)$, $\zeta=1/2$ and $\zeta=2$).

Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on $\mathbb R$, and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program. 99 (2004). Author manuscript, rev. April 2003. https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003). https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 13 (2002). https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorems 14.37, 14.60). https://doi.org/10.1007/978-3-642-02431-3

Motivation

A reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.

The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).

Setting

There are four customer classes, encountered in order $1\to2\to3\to4$. Classes $1$ and $4$ use station $1$; classes $2$ and $3$ use station $2$. Each class $k$ has a positive mean service time $m_k$ and service rate $\mu_k=1/m_k$. The external arrival rate is normalized to one. The nominal workloads are $\rho_1=m_1+m_4$ and $\rho_2=m_2+m_3$, both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.

At time $t$, $Q_k(t)\ge0$ is the amount of class-$k$ fluid, and $T_k(t)$ is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class $1$ at unit rate; completion of class $k$ feeds class $k+1$ until class $4$ exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair $(Q,T)$ with these properties is a work-conserving fluid solution.

The Lu–Kumar priority discipline gives class $4$ priority over class $1$ at station $1$, and class $2$ priority over class $3$ at station $2$. Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time $\delta>0$ empties every admissible solution with $\sum_kQ_k(0)=1$, with all queues remaining zero for $t\ge\delta$. Instability is the negation of this statement; it does not require every solution to diverge.

Formalization targets

Exact threshold

Theorem 5.1 and Remark 1 give two connected classifications, under $m_k>0$, $\rho_1<1$, and $\rho_2<1$:

$$\neg\operatorname{FluidStable}(\text{all work-conserving solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1,$$ $$\neg\operatorname{FluidStable}(\text{Lu–Kumar priority solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1.$$

The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).

Supporting targets

The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.

Significance

The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality $m_2+m_4<1$ determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary $m_2+m_4=1$, growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).

A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.

Difficulty

The ordinary load test $\rho_i<1$ controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from $\rho_1<1$ and $\rho_2<1$ to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).

Formalization scope

Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class $k$ is Lean index $k-1$. The fixed station map is $(0,1,1,0)$. Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on $t\ge0$. The external arrival rate is one, and initial size is the sum $\sum_kQ_k(0)$, since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.

Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound $\dot g\le-\varepsilon$, the version used by the paper's applications, although its displayed hypothesis prints $\dot g<-\varepsilon$. The p. 127 line involving $G_1$ prints $(1-\theta_2)Q_4$; (5.3) fixes the intended coefficient as $(1-\theta_1)Q_4$.

The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

Motivation

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.

This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar $1-1/e$ performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1

Setting

An instance consists of a finite advertiser set $A$, a finite impression-type set $I$, and allowed edges $E\subseteq A\times I$. For each type $i$, the nonnegative integer $e_i$ is its expected number of arrivals. There are $n=\sum_{i\in I}e_i>0$ arrivals. Each arrival independently has type $i$ with probability $e_i/n$. A type with $e_i=0$ remains in the graph but has zero arrival probability. On an arrival of type $i$, an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, $\mathrm{OPT}(\omega)$, is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4

The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type $i$ has capacity $e_i$. Equivalently, the selected edges form a maximum degree-capped bipartite matching $M\subseteq E$. Let $A^*$ be the advertisers covered by $M$. When type $i$ arrives, the algorithm chooses each advertiser joined to $i$ by a selected edge with probability $1/e_i$; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is $\mathrm{ALG}(\omega)$. This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5

The canonical residual cut of $M$ places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write $A_T$ for advertisers on the sink side and $I_S$ for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after $n$ independent uniform throws into $n$ bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1

Formalization targets

Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every $\varepsilon>0$, there are $\delta>0$ and $N$, uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that $n\ge N$ implies

$$\Pr\!\left[\mathrm{ALG}(\omega)\ge(1-e^{-1})\mathrm{OPT}(\omega)-\varepsilon n\right] \ge 1-e^{-\delta n}.$$

The complete bipartite family gives the tightness target. When $A=I=\{0,\ldots,n-1\}$ and every $e_i=1$, every maximum expected-instance matching is perfect. For every run, $\mathrm{OPT}=n$, and

$$\mathbb E[\mathrm{ALG}] =n\left(1-\left(1-\frac1n\right)^n\right), \qquad \lim_{n\to\infty}\frac{\mathbb E[\mathrm{ALG}]}{n}=1-e^{-1}.$$

The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity $|A^*|=|A_T|+\sum_{i\in I_S}e_i$ is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6

Significance

The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4

The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.

Difficulty

The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when $e_i>1$, so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6

Formalization scope

Advertisers and types are finite Lean types. The edge relation is a finite set, and $e_i$ and $n$ are natural numbers with $n=\sum_i e_i>0$. An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type-$i$ degree at most $e_i$. The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.

The run uses $n$ independent uniform draws from $\sum_i\{0,\ldots,e_i-1\}$. A valid labelling assigns each selected advertiser at type $i$ to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability $e_i/n$, conditional ad probability $1/e_i$ on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since $n>0$, the run sample space is nonempty; no value of $\mathrm{ALG}/\mathrm{OPT}$ at $\mathrm{OPT}=0$ is needed. The complete-graph family has $n\ge1$.

The paper writes $1-e^{-\Omega(n)}$ in both bounding passages. The Lean statements spell this out as $\forall\varepsilon>0,\ \exists\delta>0,\ \exists N,\ \forall$ instances with $n\ge N$, with $\delta,N$ preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on $\mathrm{OPT}/n$. The exact finite-$n$ expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is $\varepsilon n/2$, while its Appendix A proof yields $\varepsilon^2n/2$; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.

Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.

Selected references

• Jon Feldman, Aranyak Mehta, Vahab Mirrokni, and S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, arXiv:0905.4100v1, 2009; FOCS 2009. Preprint

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$, already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$, and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$. Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$. When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$, $D$ and $n$, but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser adjacent to $\omega(t)$: the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

$$\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],$$

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$, $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$, with the uniform distribution and $n = 3$. The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},$$

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$,

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .$$

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

1. The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$.
2. Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$, even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ($1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$, $2$, $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$. A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$, not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations "$\simeq 3/e^3$, $9/(2e^3)$, $27/(6e^3)$" of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$, the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

• "no algorithm can achieve an expected approximation of $1 - o(1)$" becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$, with $n = 3k$ tied to $k$, and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
• The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$. A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$" would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$, are welcome.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

Why coverage of an optimal value matters

Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.

The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.

Decisions, losses, and divergence neighborhoods

Let $\mathcal X\subseteq\mathbb R^d$ be a nonempty compact decision set. An observation $\xi$ has population law $P_0$, and $\ell(x;\xi)\in\mathbb R$ is the loss at decision $x$. The quantity of interest is the optimal-value functional

$$T_{\rm opt}(P)=\inf_{x\in\mathcal X}\mathbb E_P[\ell(x;\xi)].$$

The observations $\xi_1,\ldots,\xi_n$ are independent and identically distributed with law $P_0$. Write $\widehat P_n$ for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights $p_i$ with $\sum_i p_i=1$. Indexed weights also cover samples with repeated observations. For a convex divergence generator $f$ normalized by $f(1)=f'(1)=0$ and $f''(1)=2$, its divergence from the empirical law is $D_f(p\|\widehat P_n)=n^{-1}\sum_i f(np_i)$. Assumption A further requires $f$ to be three times continuously differentiable near $1$; it permits $f(0)=+\infty$.

At radius $\rho/n$, the divergence ball consists of the weights with $\sum_i f(np_i)\le\rho$. The confidence set is its image under $T_{\rm opt}$:

$$C_{n,\rho}=\{T_{\rm opt}(p):D_f(p\|\widehat P_n)\le\rho/n\}.$$

Assumption B makes $\mathcal X$ compact and requires $\ell(\cdot;\xi)$ to be Lipschitz on it with a measurable random coefficient $M(\xi)$. The theorem adds finite second moments for $M$ and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.

Formalization targets

The goal is the exact asymptotic coverage of the population optimal value, with $x^\star$ the unique optimizer and $\operatorname{Var}_{P_0}(\ell(x^\star;\xi))>0$:

$$P^*\!\left(T_{\rm opt}(P_0)\in C_{n,\rho}\right)\longrightarrow P(\chi_1^2\le\rho),\qquad \rho\ge0.$$

Here $P^*$ denotes outer probability, and $\chi_1^2$ is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of $C_{n,\rho}$; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set $C_{n,\rho}$, including both sides of that interval.

What the result provides

The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.

A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.

The mathematical obstacle

Pointwise control of each loss $\ell(x;\xi)$ is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over $x$. The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.

Formalization scope

Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first $n$ observations are indices $0,\ldots,n-1$. Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.

The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius $\rho/n$ and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is $\sup_p\inf_x$; the different minimax expression $\inf_x\sup_p$ is not substituted. The chi square target uses the standard Gaussian measure of $\{z:z^2\le\rho\}$.

Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action $H(x)$ on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.

Selected references

• John C. Duchi, Peter W. Glynn, and Hongseok Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; published in Mathematics of Operations Research 46(3), 2021. arXiv preprint

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$. At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$, and one customer either buys a product $c_t\in S_t$ or buys nothing ($c_t=0$). Given $S_t=S$, the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$:

$$p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$. The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$, $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

$$\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).$$

The seller knows $r$ and $\mathcal S$ but not $v$.

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$, $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$, and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

$$v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},$$

starting from $v^{\mathrm{UCB}}_{i,0}=1$, and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$, and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$,

$$\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .$$

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

1. The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
2. Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
3. Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$, and its rate of convergence.
4. Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$) and Lemma 4.2.
5. The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
6. The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$-cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$.

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

• Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$, as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$, and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
• Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$).
• Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$, never $v$. Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$.
• Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$, on the event that epoch $\ell$ is completed by customer $T$; uniformity in $T$ is the paper's infinite-horizon statement.
• Repairs of the page, all disclosed in the items:
  1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$.
  2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$.
  3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$.
  4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
  5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
  6. (A.14) is an inequality, since the horizon cuts the last epoch.
• Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
• No trivialization. The policy cannot see $v$, the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
• Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

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. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
• 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. doi: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. doi: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. doi:10.1287/mnsc.1030.0147
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.