Operations Research

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance I: Quadratic Potential Functions Bound Mean Response Times in Open NetworksResearch Paper

Motivation

Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.

Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).

Timeline:

1980–1988: Coffman and Mitrani, then Federgruen and Groenevelt — the achievable performance vectors of a single-station multiclass queue form a polytope described by conservation laws.
Early 1990s: Kumar (reference [Kuma] of the paper), using a potential-function argument he attributes to Meyn, derives a single lower bound on the mean number in system for re-entrant lines with deterministic routing (described on p. 16 of the paper).
1992–1994: Bertsimas, Paschalidis and Tsitsiklis — parametric families of linear bounds for general open networks with Markovian routing (Theorem 4.1), and the nonparametric polyhedron (Theorems 4.2–4.4), shown to be at least as tight.

Setting

A network has $N$ single-server stations and $R$ job classes. Class $r$ is served at station $\sigma(r)$ , and $C_i$ is the set of classes served at station $i$ . Class- $r$ jobs arrive from outside as a Poisson stream of rate $\lambda_{0r}$ , service times are exponential with rate $\mu_r$ , and after service a class- $r$ job becomes a class- $s$ job with probability $p_{rs}$ or leaves with probability $p_{r0}=1-\sum_s p_{rs}$ . The traffic equations

\lambda_r=\lambda_{0r}+\sum_{r'}\lambda_{r'}p_{r'r}\qquad(15)

have a unique solution $\lambda$ (the network is open), and $\sum_{r\in C_i}\lambda_r/\mu_r<1$ at every station.

The state $\vec n=(n_1,\dots,n_R)$ counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write $B_r$ for the event that station $\sigma(r)$ serves class $r$ , and $B_{0i}$ for the event that station $i$ is idle. Under such a policy $\vec n(t)$ is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution $\pi$ and that $E_\pi[n_r^2]<\infty$ for all $r$ . Let $\bar n_r=E_\pi[n_r]$ , which equals $\lambda_rx_r$ with $x_r$ the mean response time of class $r$ (Little's law), and define

I_{rr'}=E_\pi[1\{B_r\}n_{r'}],\qquad N_{ir'}=E_\pi[1\{B_{0i}\}n_{r'}].

For a set $S$ of classes, f-parameters are reals $f(r)\ge 0$ for $r\in S$ such that $\mu_r\big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))+\sum_{r'\notin S}p_{rr'}f(r)\big]$ is nonnegative and the same for all $r\in C_i\cap S$ ; that common value is $f_i$ , and $f_i=0$ when $C_i\cap S=\emptyset$ (restriction (17)). The sums over $r'\notin S$ include the exit $r'=0$ .

Formalization targets

Goal: Theorem 4.1

For every policy satisfying Assumption A, every $S$ and every f-parameters satisfying (17),

\sum_{r\in S}\lambda_rf(r)x_r\ \ge\ \frac{N'(S)}{D'(S)},

where

N'(S)=\sum_{r\in S}\lambda_{0r}f^2(r)+\sum_{r\notin S}\lambda_r\sum_{r'\in S}p_{rr'}f^2(r')+\sum_{r\in S}\lambda_r\Big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))^2+\sum_{r'\notin S}p_{rr'}f^2(r)\Big],

D'(S)=2\Big[\sum_{i=1}^Nf_i-\sum_{r\in S}\lambda_{0r}f(r)\Big].

The formal goal is the product form $N'(S)\le D'(S)\sum_{r\in S}f(r)\bar n_r$ .

Milestones

The utilization identity $E_\pi[1\{B_r\}]=\lambda_r/\mu_r$ (pp. 16 and 19).
Theorem 4.2: the linear equalities (24), (25) between $\bar n_r$ and $I_{rr'}$ .
Theorem 4.3: $\sum_{r\in C_i}I_{rr'}+N_{ir'}=\bar n_{r'}$ (28).
Theorem 4.4: any nonnegative $(x,I,N)$ satisfying (24), (25), (28), with $\bar n_r=\lambda_rx_r$ in those equalities, satisfies every inequality of Theorem 4.1. This statement is deterministic.

Significance

Theorem 4.1 gives, for each choice of $S$ and $f$ , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost $\sum_r c_rx_r$ subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables $(\bar n,I,N)$ implies all of these inequalities at once, so the parametric search over $f$ is unnecessary.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.

Difficulty

Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions ( $n_r$ , $n_rn_{r'}$ ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending $\sum_n\pi(n)(\mathcal Gg)(n)=0$ to quadratic $g$ needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify $\mu_rE_\pi[1\{B_r\}]$ with $\lambda_r$ . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because $f\ge0$ on $S$ , $f_i\ge0$ and at most one class per station is in service.

Formalization scope

Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs $\tau_k$ of the paper are not built: the paper notes that its expectations at $\tau_k$ are expectations under the invariant distribution of $\vec n(t)$ .

Conventions fixed in Lean:

$\lambda_rx_r$ appears only as the mean number in system $\bar n_r$ (Little's law, used by the paper on pp. 11 and 20); response times are not formalized.
Sums over $r'\notin S$ include the exit $r'=0$ (p. 15).
f-parameters are nonnegative on $S$ (p. 9).
The network is open: (15) has a unique solution, and $\lambda$ is an input constrained by (15), never defined from the policy.
(18) is stated multiplied by $D'(S)$ , which avoids Lean's $x/0=0$ and is (18) whenever $D'(S)>0$ .

A quotient-form statement of (18) would be trivially true when $D'(S)=0$ , and defining $\lambda_r$ as $\mu_rE_\pi[1\{B_r\}]$ would make the utilization identity hold by definition; both are excluded.

Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA, 1992; Ann. Appl. Probab. 4(1), 1994. https://doi.org/10.1214/aoap/1177005200
C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queuing network control, Math. Oper. Res. 24(2), 1999. https://doi.org/10.1287/moor.24.2.293

8 thms2 active usersReviewed

Probability Stochastic Systems Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Motivation

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of $T$ periods, decides whether to place an order, pays a fixed cost $K$ for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.

Timeline:

Scarf (1960) proved that $(s,S)$ policies are optimal for independent demands with fixed costs; with correlated demand the optimal policy is a state-dependent $(s_t(f_t), S_t(f_t))$ rule that is hard to compute.
Levi, Pál, Roundy and Shmoys (2007) gave the dual-balancing 2-approximation for the model without fixed costs (§4) and the triple-balancing 3-approximation for the stochastic lot-sizing problem (§6, Theorem 6.1), both for arbitrarily correlated demand.

Setting

There are periods $t=1,\dots,T$ on a probability space $(\Omega,\mathcal F,\mu)$ with a filtration $(\mathcal F_t)$ : $\mathcal F_t$ is the information available at the beginning of period $t$ . The data are a fixed ordering cost $K\ge0$ , per-unit holding costs $h_t\ge0$ , per-unit backlogging penalties $p_t\ge0$ , an initial inventory level $x_1\in\mathbb R$ , and nonnegative demands $D_t$ . The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that $D_t$ is $\mathcal F_t$ -measurable: the demand of a period is known when the period begins. For every period $s$ there is a conditional joint distribution $I_s$ of the demands given $\mathcal F_s$ , under which every conditional mean $E[D_t\mid f_s]$ is finite.

A feasible policy is an order process $Q=(Q_t)$ with $Q_t\ge0$ and $Q_t$ determined by $\mathcal F_t$ . Its inventory levels are $x_t=x_1+\sum_{j<t}(Q_j-D_j)$ before ordering and $y_t=x_t+Q_t$ after ordering, and its cost is

\mathcal C(Q)=\sum_{t=1}^T\Bigl(K\,\mathbb 1(Q_t>0)+h_t(y_t-D_t)^++p_t(D_t-y_t)^+\Bigr).

The triple-balancing policy TB uses two rules. Let $s^*$ be the last period before $s$ in which TB ordered ( $s^*=0$ if none). Rule 1: TB orders in period $s$ if and only if, without an order in $s$ , the accumulated backlogging cost over $(s^*,s]$ would exceed $K$ . Rule 2: when it orders in $s<T$ , it orders

q_s^B=\max\{q\ge0:\ E[H_s^B(q)\mid f_s]\le K\},\qquad H_s^B(q)=\sum_{j=s}^T h_j\bigl(q-(D_{[s,j]}-x_s)^+\bigr)^+,

the largest quantity whose expected marginal holding cost over $[s,T]$ is at most $K$ . When it orders in period $T$ , it orders exactly enough to clear the backorders and meet $D_T$ . Let $N$ be the number of orders TB places.

Formalization targets

Goal: Theorem 6.1

For every instance, the triple-balancing policy TB and every feasible policy $P$ satisfy

E[\mathcal C(TB)]\le 3\,E[\mathcal C(P)].

The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.

Milestones

§6.1, Rule 2 observation. In a period where TB orders, $D_s\le y_s^{TB}$ : no backorders remain at the end of the period.
Lemma 6.1. $K\cdot E[N]\le E[\mathcal C(P)]$ for every feasible $P$ .
Lemma 6.2. $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\cdot E[N]$ for every feasible $P$ .

Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when $h_T>0$ .

Significance

The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).

The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event $N=0$ . It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.

Difficulty

The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.

Formalization scope

Periods are natural numbers $1,\dots,T$ , demands and orders are real-valued, and data at indices outside $1,\dots,T$ are unused.
Information is a MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and " $D_t$ known at the start of period $t$ " means $D_t$ is $\mathcal F_t$ -measurable.
The conditional distributions $I_s$ are model data: Markov kernels to demand paths that are $\mathcal F_s$ -measurable regular conditional distributions of the demand path. At every outcome they make $D_s$ deterministic, demands nonnegative and the conditional means $E[D_t\mid f_s]$ finite.
Expected costs, $E[N]$ and the conditional expectation in Rule 2 are lower Lebesgue integrals in $[0,\infty]$ . Lemma 6.2 is stated additively, $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\,E[N]$ , which is the paper's inequality whenever the expectations are finite.
The comparison policy is an arbitrary feasible policy, not an optimal one. The paper's proofs use only feasibility, and this form implies the paper's whenever an optimum exists, without any existence hypothesis.
TB is the predicate "feasible and satisfies Rules 1 and 2 at every period and outcome". The rules determine the policy uniquely. Rule 1 uses a strict "exceeds $K$ ", and the period- $T$ order is $D_T-x_T$ .

Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every $q$ , because it uses kernel integrals in $[0,\infty]$ . Infinite expected costs cannot be read as $0$ . The policy class is not empty, because a separate theorem gives existence under $h_T>0$ (without some positive holding cost on $[s,T]$ the maximum in Rule 2 does not exist).

Contributions welcome: proofs of the existence theorems (measurable selection of $q_s^B$ , versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.

Selected references

R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. https://doi.org/10.1287/moor.1060.0205
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.

7 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 5: The Maximum Likelihood Estimator Exists with Probability Tending to One and Is Consistent and Asymptotically NormalResearch Paper

Motivation

The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative $i$ with probability proportional to $e^{z_i\theta}$ , where $z_i$ is a vector of observed attributes and $\theta$ an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate $\theta$ by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.

Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.

Setting

Observations are indexed serially, $m = 0, 1, 2, \dots$ , as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation $m$ offers $J_m \ge 1$ alternatives, and alternative $i$ carries a vector $z_{im} \in \mathbb R^K$ of independent variables. For a parameter $\theta \in \mathbb R^K$ the selection probabilities are

P_{im}(\theta) = \frac{e^{z_{im}\theta}}{\sum_{j=1}^{J_m} e^{z_{jm}\theta}}, \qquad \bar z_m(\theta) = \sum_{i} P_{im}(\theta)\, z_{im}.

The data are generated at a true parameter $\theta^0$ : the chosen alternatives $Y_0, Y_1, \dots$ are independent random variables with $\Pr(Y_m = i) = P_{im}(\theta^0)$ . The log-likelihood of the first $q$ observations is $L^q(\theta) = \sum_{m<q}\log P_{Y_m m}(\theta)$ . The moment matrix of observation $m$ is

\Omega_m = \sum_{i} P_{im}(\theta^0)\,(z_{im}-\bar z_m)(z_{im}-\bar z_m)', \qquad \bar z_m = \bar z_m(\theta^0).

Axiom 7 asks that $J_m \le J_*$ and $|z_{im}| \le M$ uniformly, and that $\frac1q\sum_{m<q}\Omega_m$ converge to a positive definite matrix $\Omega$ . Axiom 6, for a given sample, asks that no nonzero $\gamma$ satisfy $(z_{jm} - z_{Y_m m})\gamma \le 0$ for all observed $m$ and all $j$ . A maximum likelihood estimator $\hat\theta^q$ is a measurable choice of a maximizer of $L^q$ , wherever one exists.

Formalization targets

Goal: Lemma 6

\hat\theta^q \xrightarrow{\Pr} \theta^0 \quad\text{and}\quad \sqrt q\,\Omega^{1/2}(\hat\theta^q - \theta^0) \xrightarrow{d} N(0, I_K) \qquad (q \to \infty).

Milestones

Axiom 7 implies Axiom 5 (the full-rank condition) in all sufficiently large samples.
Equation (42): $P_{im}(\theta) \ge 1/(J_* e^{2M|\theta|})$ .
Lemma 5: $\Pr(\text{Axiom 6 holds and } L^q \text{ attains its maximum}) \to 1$ .
Equation (43): the first three derivatives of $\log P_{im}$ are bounded by $2M$ , $4M^2$ , $8M^3$ .
Equation (46): each score $\nabla\log P_{Y_m m}(\theta^0)$ has mean zero.
Equation (47): each expected Hessian equals $-\Omega_m$ .
Consistency of $\hat\theta^q$ .
Equation (58): $q^{-1/2}\,\Omega^{-1/2}\sum_{m<q}\nabla\log P_{Y_m m}(\theta^0) \xrightarrow{d} N(0, I_K)$ .

Significance

The result. Lemma 6 is what licenses reading $\hat\theta^q$ as approximately $N(\theta^0, q^{-1}\Omega^{-1})$ , so that the diagonal of the inverse information matrix estimates the sampling variances and $q(\hat\theta^q-\theta^0)'\Omega(\hat\theta^q-\theta^0)$ is asymptotically $\chi^2_K$ . Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction $\gamma$ of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.

Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization $1/q$ in (58), which must be $1/\sqrt q$ , and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.

Difficulty

The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around $\theta^0$ , controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances $\Omega_m$ that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin K); $z\theta$ is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.
The paper's $N$ trials with $R_n$ repetitions are the special case of the serial indexing in which consecutive observations repeat their data; the sample size $\sum_n R_n$ is $q$ .
Axiom 7's limit (27) is taken in its serial form (48), with $P$ evaluated at $\theta^0$ .
The estimator is any measurable selection that maximizes $L^q$ whenever $L^q$ has a maximum, and is unconstrained otherwise. Requiring a maximizer for every sample would be unsatisfiable, since Axiom 6 fails with positive probability, and would make the goal vacuous; this convention rules that out.
Consistency is TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. $\Omega^{1/2}$ is the positive semidefinite square root CFC.sqrt.
Needed infrastructure: derivatives of log-sum-exp, a law of large numbers for bounded independent vectors, and a multivariate Lindeberg–Feller theorem. Mathlib provides the one-dimensional i.i.d. central limit theorem only. Contributions of these general results as separate theorems are welcome.

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966 (Lindeberg–Feller theorem, pp. 256–258).
C. R. Rao, Linear Statistical Inference and Its Applications, Wiley (cited by McFadden as Rao (1968), pp. 347–351, for the asymptotic $\chi^2$ test).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Probability Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 1: An (8+3e)-Competitive Algorithm for the Weighted Secretary ProblemResearch Paper

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$ , each with a nonnegative value $v(e)$ , and $K$ goods indexed in decreasing order of nonnegative weight:

w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$ . Its value is $\sum_{k=1}^K v(s(k))w(k)$ . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$ , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$ , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$ , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$ , observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$ . A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$ .

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$ , which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$ :

\mathrm{OPT}\le(8+3e)\,\mathbb E[A].

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$ . Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class- $i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$ , the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$ . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$ . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$ . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$ , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

7 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain·Captain: mikedeng1

Discrete Dynamic Programming 2: A Stationary Policy Is Nearly Optimal as the Discount Factor Tends to 1 Exactly When It Maximizes x(g) and, Among Those, y(g)Research Paper

Motivation

A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor $\beta$ tends to $1$ the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats $\beta = 1$ as a limit of $\beta < 1$ : it expands the discounted return of a stationary policy in powers of $1-\beta$ and reads off which policies remain good as $\beta \to 1$ . The two leading coefficients of that expansion, the gain $x(f)$ and the bias $y(f)$ , became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).

Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all $\beta$ near $1$ (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through $x$ and $y$ . Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders ( $n$ -discount optimality).

Setting

There are finitely many states $s \in S$ and a finite nonempty set $A$ of actions. Action $a$ in state $s$ pays an income $i(s,a) \in \mathbb R$ and moves the system to $s'$ with probability $q(s' \mid s,a)$ . $F$ is the finite set of decision rules $f : S \to A$ . A policy is a sequence $\pi = \{f_1, f_2, \dots\}$ of decision rules; $f^{(\infty)}$ uses $f$ every day, and $(g, \pi)$ uses $g$ first and then $\pi$ . For $f \in F$ , $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s' \mid s,f(s)))_{s,s'}$ . The discounted return of $\pi$ is the vector

V_\beta(\pi) = \sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\, r(f_{n+1}), \qquad 0 \le \beta < 1,

and $V_\beta(f)$ abbreviates $V_\beta(f^{(\infty)})$ . Vectors are compared coordinatewise; $w_1 > w_2$ means $w_1 \ge w_2$ and $w_1 \neq w_2$ . A policy is β-optimal if its return dominates that of every policy, and $U(\beta)$ is the return of a β-optimal policy. It is optimal if it is β-optimal for all $\beta$ sufficiently near $1$ , and nearly optimal if $U(\beta) - V_\beta(\pi) \to 0$ as $\beta \to 1$ .

For any Markov matrix $Q$ , the limit matrix $Q^*$ is the limit of $(I + Q + \cdots + Q^N)/(N+1)$ , and the deviation matrix is $H = (I - Q + Q^*)^{-1} - Q^*$ . For a rule $f$ , $Q^*(f)$ and $H(f)$ are those of $Q(f)$ , and

x(f) = Q^*(f)\, r(f), \qquad y(f) = H(f)\, r(f).

With $p(s,a)w = \sum_{s'} q(s' \mid s,a) w_{s'}$ , the set $G(s,f)$ consists of the actions $a$ with $p(s,a)x(f) > x_s(f)$ , or with $p(s,a)x(f) = x_s(f)$ and $i(s,a) + p(s,a)y(f) > x_s(f) + y_s(f)$ ; $E(s,f)$ consists of those with equality in both.

Formalization targets

Goal: Theorem 4(e)

For any $f_0$ with $G(s,f_0) = \varnothing$ for all $s$ :

x(f_0) \ge x(g)\ \ \forall g \in F;\qquad \exists f^* \in F^* := \{g : x(g) = x(f_0)\}\ \text{with}\ y(f^*) \ge y(g)\ \forall g \in F^*;

g^{(\infty)} \text{ is nearly optimal} \iff x(g) = x(f^*) \text{ and } y(g) = y(f^*).

Milestones and intermediate results

Milestones: Lemma 1(b) ( $\operatorname{rank}(I-Q) + \operatorname{rank} Q^* = S$ ), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).

The mission also states, as intermediate results:

Lemma 1(a), (c), (d): for every Markov matrix, convergence of the Cesàro means to a Markov $Q^*$ with $QQ^* = Q^*Q = Q^*Q^* = Q^*$ ; unique solvability of $Qx = x$ , $Q^*x = Q^*c$ ; nonsingularity of $I - Q + Q^*$ , $\sum_n \beta^n (Q^n - Q^*) \to H$ and the identities for $H$ .
Theorem 4(a): $V_\beta(f) = x(f)/(1-\beta) + y(f) + o(1)$ , with $x(f), y(f)$ the unique solutions of their linear systems; display (2), the same expansion for $(g, f^{(\infty)})$ .
Theorem 3 and its Corollary for fixed $\beta < 1$ , and the first assertion of 4(e).

Significance

Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income $x$ , then of the bias $y$ . It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.

The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.

Difficulty

Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where $Q^n$ does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single $f^*$ whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through $U(\beta)$ .

Formalization scope

States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's $f_1$ . $V_\beta$ is a real tsum. $Q^*$ is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; $H(\beta)$ is a matrix tsum, whose summability for $0 \le \beta < 1$ is part of Lemma 1(d); $H$ uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). $x(f)$ and $y(f)$ are defined by the closed forms $Q^*(f)r(f)$ and $H(f)r(f)$ from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along $\beta \to 1^-$ . "Nearly optimal" is encoded without $U$ : for every $\varepsilon > 0$ , for all β in some interval $(\beta_0, 1)$ , every policy's return is at most $V_\beta(\pi) + \varepsilon$ in every coordinate; this is equivalent to $U(\beta) - V_\beta(\pi) \to 0$ because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set $G(s,f)$ .

A formalization in which optimality or near optimality is tested only against stationary policies, or in which $Q^*$ is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.

Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.

Selected references

D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
B. L. Miller and A. F. Veinott, Discrete Dynamic Programming with a Small Interest Rate, Ann. Math. Statist. 40(2):366–370, 1969.
A. F. Veinott, Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization·Captain: mikedeng1

Consensus of Subjective Probabilities: The Pari-Mutuel Method: Equilibrium Track Probabilities Exist and Are UniqueResearch Paper

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$ , is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$ .

The subjective probability matrix $P=(p_{ij})$ is $m\times n$ ; $p_{ij}$ is the probability, in the opinion of $B_i$ , that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$ .
Bettor $B_i$ has a budget $b_i>0$ , with the unit of money chosen so that $\sum_i b_i=1$ .
Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$ . Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$ .

The paper's variational problem is

\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$ , $D$ , the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

$\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
$\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
(8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
Every $\pi_j$ of (6) is positive (p. 167).
EXISTENCE THEOREM: for every maximizer $\bar\xi$ , (6)–(7) are equilibrium probabilities and bets (p. 167).
Every equilibrium has $\pi_j>0$ (p. 168).
For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
If $\pi>0$ , $\bar\pi\ge0$ , both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$ , then $\bar\pi=\pi$ (p. 168).
UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$ , the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$ , and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$ , so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$ , fails: $\varphi$ is concave but not strictly concave in $\xi$ , and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$ , which the paper uses without proof.

Formalization scope

Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$ , $\sum_i b_i=1$ ) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$ .
Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$ . This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$ . Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
$D$ has column sums one, as in (5).
$\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
Ruled out: a version of (3) with real division ( $x/0=0$ ) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ( $\log0=0$ ) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394

12 thms2 active usersReviewed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 2: Logarithmic Regret for N ArmsResearch Paper

Motivation

Thompson Sampling is the oldest heuristic for the multi-armed bandit problem: proposed by Thompson in 1933, it plays each arm with the posterior probability that the arm is the best one. It is simple to implement, performs well empirically (Chapelle and Li, NIPS 2011), and has been used in production systems such as click-through-rate prediction for search advertising. For a long time, however, no finite-time regret guarantee was known for it: the analyses available before 2012 gave only $o(T)$ regret.

Agrawal and Goyal (arXiv:1111.1797, COLT 2012) gave the first logarithmic bounds on the expected regret of Thompson Sampling. This mission formalizes their bound for the general case of $N$ arms (their Theorem 2). A companion mission of the same series formalizes their two-armed bound (Theorem 1), whose proof is independent.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least of order $\sum_i \frac{\Delta_i}{D(\mu_i\|\mu_1)}\ln T$ . Auer, Cesa-Bianchi and Fischer (2002) showed that UCB1 achieves $O(\sum_i \ln T/\Delta_i)$ in finite time. Agrawal and Goyal (2012) proved $O((\sum_a 1/\Delta_a^2)^2\ln T)$ for Thompson Sampling with $N$ arms; Kaufmann, Korda and Munos (2012) and Agrawal and Goyal (2013) later proved the asymptotically optimal constant for Bernoulli rewards.

Setting

A stochastic $N$ -armed bandit has arms $1,\dots,N$ . Arm $i$ , when played, yields a random reward drawn from a fixed distribution $\nu_i$ supported in $[0,1]$ , with mean $\mu_i$ ; rewards of an arm are i.i.d. and independent of the other arms. Arm $1$ is assumed to be the unique optimal arm, $\mu_1>\mu_i$ for $i\ne1$ , and $\Delta_i=\mu_1-\mu_i>0$ is the gap of arm $i$ .

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$ , a count $S_i$ of successes and $F_i$ of failures, both starting at $0$ . In each round $t$ it draws $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$ independently for every arm, plays $i(t)=\arg\max_i\theta_i(t)$ , observes a reward $\tilde r_t\sim\nu_{i(t)}$ , performs a Bernoulli trial with success probability $\tilde r_t$ , and increments $S_{i(t)}$ on success and $F_{i(t)}$ on failure.

The expected regret in time $T$ is

\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu^*-\mu_{i(t)})\Big],\qquad \mu^*=\max_i\mu_i,

the expectation being over the rewards, the Bernoulli trials and the posterior samples.

The proof works with the reward stacks $Z_{i,m}$ : the outcome of the $m$ -th Bernoulli trial of arm $i$ , all independent. Then $s(j)=\sum_{m\le j}Z_{1,m}$ , the number of successes in the first $j$ plays of arm $1$ , is a $\mathrm{Binomial}(j,\mu_1)$ random variable. The other objects of the proof are the threshold $L_i=24\ln T/\Delta_i^2$ , the saturated set $C(t)$ of suboptimal arms with at least $L_i$ plays before round $t$ , the intervals $I_j$ between the $j$ -th and $(j+1)$ -th plays of arm $1$ , and the counts $\gamma_j$ and $V_j^{\ell,a}$ defined in §4.

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $N\ge2$ , every instance as above and every horizon $T\ge2$ ,

\mathbb E[\mathcal R(T)]\le C\Big(\sum_{a=2}^N\frac{1}{\Delta_a^2}\Big)^2\ln T .

$C$ does not depend on $N$ , on the reward distributions or on $T$ .

Milestones

Lemma 4: with $E(t)$ the event that every saturated arm's sample lies within $\Delta_i/2$ of its mean, $\Pr(E(t))\ge1-4(N-1)/T^2$ , also conditionally on $s(j)=s$ .
Lemma 5 (Eq. (7)): the expected regret from saturated arms inside $I_j$ is at most $\mathbb E\big[\mathbb E[\gamma_j+1\mid s(j)]\sum_a\Delta_a\mathbb E[\min\{X(j,s(j),\mu_a+\Delta_a/2),T\}\mid s(j)]\big]$ .
Lemma 1: $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$ , where $X(j,s,y)$ counts the trials before an independent $\mathrm{Beta}(s+1,j-s+1)$ sample exceeds $y$ .
Lemma 3: a three-case bound on $\mathbb E[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]]$ in terms of the Bernoulli KL divergence $D$ between $y$ and $\mu_1$ .

Significance

The result. Theorem 2 shows that Thompson Sampling, a randomized Bayesian heuristic, achieves regret logarithmic in the horizon for any number of arms with bounded rewards, matching the order in $T$ of the Lai–Robbins lower bound. Its dependence on the gaps, $(\sum_a\Delta_a^{-2})^2$ , is worse than UCB1's; the paper's own Remark 1 and later work improve it. The proof introduced the device of bounding the waiting time between plays of the optimal arm through geometric variables with Beta-cdf parameters (Lemmas 1 and 3), which reappears in later analyses of Thompson Sampling.

Formalizing it. The theorem is proved on paper; it has not been machine-checked. Bandit theory in Lean (bandit environments, regret, UCB-type analyses) is still young, and no Beta–Bernoulli Thompson Sampling result is formalized. The mission produces a Lean model of Algorithm 2 for general $[0,1]$ rewards with the paper's stack coupling, the §4 bookkeeping of saturated arms and intervals, and the paper's lemmas as separate targets.

Difficulty

Two difficulties are specific to the $N$ -armed analysis. First, the arm that competes with arm $1$ changes over time: the set of saturated arms grows, and which saturated arm is "best" depends on the history, so the waiting time between plays of arm $1$ cannot be compared with a single geometric variable as in the two-armed case. Second, the number $\gamma_j$ of rounds at which arm $1$ 's sample is large but arm $1$ is not played is not independent of the counts $V_j^{\ell,a}$ : both depend on the same posterior samples, and Lemma 5 needs a careful conditioning on the history to separate them. The obvious union bound over arms, treating each suboptimal arm as in the two-armed proof, fails because it ignores the interruptions by unsaturated arms, whose number is the source of the squared sum in the bound.

Formalization scope

Probability space. Algorithm 2 is realized on a product of three independent i.i.d. tables: Beta draws indexed by (arm, round, successes, failures), rewards indexed by (arm, round) and uniform variables indexed by (arm, round); the Bernoulli trial of a round succeeds when the played arm's uniform variable is below its reward. The law of the run is that of Algorithm 2, which runs for every round $t=1,2,\dots$ . $s(j)$ is the number of successful trials among the first $j$ plays of arm $1$ in this infinite run (possibly after the horizon $T$ ), so it is a $\mathrm{Binomial}(j,\mu_1)$ random variable for every $j$ , as the paper's independent $Z_{1,m}$ make it. Ties in the arg max (probability $0$ ) go to the smallest index.
Indexing. Arms are Fin N, and Lean arm 0 is the paper's arm $1$ . Rounds are $0,\dots,T-1$ ; Lean round $t$ is the paper's round $t+1$ . Sums over $a=2,\dots,N$ are sums over $a\ne0$ .
Expectations are lower Lebesgue integrals in $[0,\infty]$ , which has no junk value for non-integrable functions. Conditional expectations given $s(j)$ are written as finite sums over the values of $s(j)$ .
The $O(\cdot)$ . The paper writes $O(\cdot)$ in the sense of its footnote 1 ( $f(n)\le c\,g(n)$ for $n\ge n_0$ ). The goal states it with one universal constant $C$ , quantified before $N$ , the instance and $T$ , for every $T\ge2$ . The explicit constants printed in App. D are not formalized: expanding the paper's Eq. (21) gives terms $288(N-1)(\ln T)\sum_a\Delta_a^{-2}$ and $48(N-1)^2$ where the paper prints $288(\ln T)\sum_i\Delta_i^{-2}$ , and Eq. (22) drops a factor $\ln T$ in its $192/\Delta_a^2$ term. The $O(\cdot)$ claim does not depend on these slips; a statement pinned to the printed numerals might be false.
Ruled out. A constant depending on $N$ , on the means or on $T$ ; a fixed number of arms; Bernoulli rewards only; or any algorithm other than Algorithm 2 would each make the goal a different and weaker theorem. The statement quantifies over all $N\ge2$ and all reward distributions on $[0,1]$ .
Not included. Eq. (8), the bound $\sum_{j}\mathbb E[\gamma_j\mid s(j)]\le\sum_uL_u+4(N-1)$ "for all instantiations", is not a milestone: each term is conditioned on a different $s(j)$ , and the pointwise reading does not follow from the argument given. Remark 1 (an alternate bound) and App. A (several optimal arms) are not part of this mission.
Contributions welcome: Beta–Binomial identities, geometric waiting times, Hoeffding bounds for binomial cdfs, and the stopping-time arguments behind Lemma 5. Lemma 1 and Lemma 3 are shared with the two-armed mission of this series.

Selected references

S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3, 2012. https://arxiv.org/abs/1111.1797
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25, 1933. https://doi.org/10.1093/biomet/25.3-4.285
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling
E. Kaufmann, N. Korda and R. Munos, Thompson Sampling: an asymptotically optimal finite-time analysis, ALT 2012. https://arxiv.org/abs/1205.4217
S. Agrawal and N. Goyal, Further optimal regret bounds for Thompson Sampling, AISTATS 2013. https://arxiv.org/abs/1209.3353

11 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 2: Given α ≥ c(C_OPT), the Weighted Potential-Function Algorithm Never Fails and Pays at Most (6+o(1)) α log m log nResearch Paper

Motivation

Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).

The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio $O(\log m \log n)$ , where $n$ is the number of elements and $m$ the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).

This mission formalizes the core of the weighted result: the algorithm that is given a value $\alpha$ at least the optimal cost, and its guarantee (Theorem 3.4).

Setting

The ground set $X$ has $n = |X|$ elements and the family $\mathcal S$ has $m = |\mathcal S|$ sets; every set $S$ has a cost $c_S > 0$ . Both are known to the algorithm in advance. For an element $j$ , $\mathcal S_j$ denotes the sets containing $j$ . Elements of an unknown subset of $X$ arrive one at a time in a sequence $\sigma$ ; on arrival each must be covered by a chosen set. The chosen family $\mathcal C$ can only grow. $\mathcal C_{OPT}$ is any family covering every arriving element, and $c(\mathcal C_{OPT}) = \sum_{S \in \mathcal C_{OPT}} c_S$ .

The algorithm is given $\alpha \ge c(\mathcal C_{OPT})$ . It discards sets costing more than $\alpha$ , buys sets costing at most $\alpha/m$ outright, and rescales costs; on the resulting normalized instance $1 \le c_S \le m$ and $c_S \le \alpha$ for every set (p. 365).

The algorithm keeps a weight $w_S > 0$ for every set, initially $w_S = 1/m^2$ ; the weight of an element is $w_j = \sum_{S \in \mathcal S_j} w_S$ . With $C$ the set of covered elements and $\chi_{\mathcal C}$ the indicator of $\mathcal C$ , the potential is

\Phi = \sum_{j \notin C} n^{2 w_j} + n \cdot \exp\Big(\frac{1}{2\alpha} \sum_{S \in \mathcal S} \big(c_S \chi_{\mathcal C}(S) - 3 w_S c_S \log n\big)\Big),

with natural logarithms throughout. When $j$ arrives with $w_j \ge 1$ nothing happens; otherwise the algorithm performs weight augmentation steps while $w_j < 1$ . In a step, for each $S \in \mathcal S_j$ : (a) $w_S \leftarrow w_S (1 + \frac{1}{n c_S})$ ; (b) if $S \notin \mathcal C$ , add $S$ to $\mathcal C$ when $\Phi$ does not exceed its value before (a); (c) if $\Phi$ has increased, return FAIL.

In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.

Formalization targets

Goal: Theorem 3.4

On the normalized instance, with $\mathcal C_{OPT}$ covering $\sigma$ , $c(\mathcal C_{OPT}) \le \alpha$ , and $n \cdot n^{2/m} + n < n^2$ , every reachable configuration is a running state (never FAIL) in which (i) every $j \in X$ with $w_j \ge 1$ is covered, and (ii)

\sum_{S \in \mathcal C} c_S \le 3 \log n \Big(1 + \Big(1 + \frac1n\Big)\alpha \log\Big(m^2\Big(1+\frac1n\Big)\Big)\Big) + 2\alpha \log n = (6 + o(1))\,\alpha \log m \log n.

Milestones

Lemma 3.1 (p. 365): the number $N$ of augmentation steps satisfies $N \le \sum_{S \in \mathcal C_{OPT}} (n c_S + 1)\log(m^2(1 + 1/n)) \le (n+1)\alpha\log(m^2(1+1/n))$ .
Lemma 3.2 (p. 366): throughout, $\sum_S w_S c_S \le 1 + N/n \le 1 + (1 + 1/n)\alpha\log(m^2(1+1/n))$ .
Lemma 3.3 (p. 366): a per-set step with $c_S \le \alpha$ never increases $\Phi$ ; in particular the algorithm never fails.

The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant $\Phi < n^2$ assumed) is included as a supporting reference.

Significance

Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of $\alpha$ described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic $O(\log m \log n)$ -competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.

The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant $\Phi < n^2$ to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis $c_S \le \alpha$ . Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the $o(1)$ terms replaced by explicit expressions.

Difficulty

The cost bound in the last step is short once two facts about the run are available: that $\Phi$ stays below $n^2$ , and that the fractional cost $\sum_S w_S c_S$ stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add $S$ or not) does not increase $\Phi$ ; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most $\alpha$ . The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers $n^{2 w_j}$ , where the initial bound $\Phi < n^2$ is a genuine size condition on $n$ and $m$ .

Formalization scope

The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits $\mathcal S_j$ is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by $\mathcal C_{OPT}$ .

Conventions: costs, weights and $\alpha$ are real; $n$ and $m$ are the cardinalities of the finite types cast to $\mathbb R$ ; $\log$ is Real.log; $n^{2 w_j}$ and $n^{2/m}$ are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:

Lemma 3.1: $(2 + o(1)) n\alpha\log m$ becomes $(n+1)\alpha\log(m^2(1+1/n))$ ;
Lemma 3.2: $(2 + o(1))\alpha\log m$ becomes $1 + (1+1/n)\alpha\log(m^2(1+1/n))$ , together with the intermediate bound $1 + N/n$ ;
Theorem 3.4 (ii): $(6 + o(1))\alpha\log m\log n$ becomes $3\log n\,(1 + (1+1/n)\alpha\log(m^2(1+1/n))) + 2\alpha\log n$ ;
"n and m large" becomes the hypothesis $n \cdot n^{2/m} + n < n^2$ used for the initial potential (it holds, for instance, when $n \ge 4$ and $m \ge 3$ ).

The goal is a statement about the configurations the algorithm actually reaches from $w_S = 1/m^2$ and the empty cover. Taking the invariant $\Phi < n^2$ or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown $\alpha$ is not part of this mission.

A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.

Selected references

N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2):361–370, 2009. https://doi.org/10.1137/060661946
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):93–263, 2009. https://doi.org/10.1561/0400000024

10 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 3: Every Deterministic Online Algorithm Has Competitive Ratio at Least kr on the Block FamilyResearch Paper

Motivation

In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.

The paper gives a deterministic online algorithm whose cost is within a factor $O(\log m \log n)$ of the offline optimum, where $n$ is the number of elements and $m$ the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of $m$ and $n$ , every deterministic online algorithm has competitive ratio $\Omega\big(\log n \log m / (\log\log m + \log\log n)\big)$ . The lower bound is the reason the $\log m \log n$ product, rather than the $\ln n$ of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.

This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.

Setting

A ground set $X$ and a family $\mathcal F$ of distinct subsets of $X$ are fixed and known to the algorithm; $m = |\mathcal F|$ . An adversary presents elements $x_1, x_2, \dots$ of $X$ one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm $A$ , on the arrival of $x_t$ , sees the earlier arrivals $(x_1, \dots, x_{t-1})$ and $x_t$ , and adds a finite family $A\big((x_1,\dots,x_{t-1}), x_t\big) \subseteq \mathcal F$ of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of $\mathcal F$ , that element lies in a chosen set. After an arrival sequence $\sigma$ the chosen collection is $\mathcal C_A(\sigma)$ , and since every set has unit cost, the cost is $|\mathcal C_A(\sigma)|$ . The offline optimum $\mathrm{OPT}(\sigma)$ is the least number of members of $\mathcal F$ covering the elements of $\sigma$ . The competitive ratio of $A$ is at least $\rho$ when some arrival sequence $\sigma$ has $\mathrm{OPT}(\sigma) \ge 1$ and $|\mathcal C_A(\sigma)| \ge \rho\,\mathrm{OPT}(\sigma)$ .

Two families are used.

The bit family: $X = \{0, \dots, 2^k - 1\}$ and $F_i = \{ j : \text{bit } i \text{ of } j \text{ is on}\}$ for $1 \le i \le k$ .
The block family: $k r^2$ disjoint blocks $X_1, \dots, X_{kr^2}$ of $2^k$ elements each; $X_b(t)$ is the set of elements of block $X_b$ whose $t$ th bit is on. For an $r$ -set $R = \{b_1 < \dots < b_r\}$ of blocks and bit locations $I = (i_1, \dots, i_r)$ ,

F_{R,I} = \bigcup_{t=1}^r X_{b_t}(i_t),

and the family consists of all $F_{R,I}$ ; it has $m = \binom{kr^2}{r} k^r$ members.

Formalization targets

Goal: Proposition 4.2

For all positive integers $k, r$ and all $n, m$ with

n \ge 2^{k+1} k r^2, \qquad 2^{2^k k r^2} \ge m \ge \binom{kr^2}{r} k^r,

there is a family $\mathcal F$ of exactly $m$ distinct subsets of an $n$ -element set such that for every valid deterministic online algorithm $A$ there is a nonempty arrival sequence $\sigma$ , covered by a single member of $\mathcal F$ , with

|\mathcal C_A(\sigma)| \ge kr = kr \cdot \mathrm{OPT}(\sigma).

The goal leaves the instance existential, as the paper does, and keeps both bounds on $m$ and the bound on $n$ exactly as printed.

Milestones

Proposition 4.1. On the bit family, $|\mathcal F| = k$ ; every valid deterministic algorithm can be forced to cost $k$ on a sequence with $\mathrm{OPT} = 1$ ; and some valid algorithm has cost at most $k \cdot |C|$ for every offline cover $C$ . So the best deterministic competitive ratio is exactly $k = \log_2 n$ .
The adversary claim of Section 4 (p. 369). On the block family, every valid deterministic algorithm can be forced to choose $kr$ sets by at most $kr$ arrivals that a single set covers.

A supporting item (not a milestone) records the count $|\mathcal F| = \binom{kr^2}{r} k^r$ of the block family.

Significance

The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing $r$ of order $\log m / (\log\log m + \log\log n)$ and $k$ of order $\log n$ turns it into the asymptotic bound $\Omega\big(\log n \log m/(\log\log m + \log\log n)\big)$ , which shows that the paper's $O(\log m \log n)$ algorithm is optimal among deterministic algorithms up to a $\log\log m + \log\log n$ factor. Without it, the gap between the $\ln n$ achievable offline and the $\log m \log n$ achieved online would be unexplained. Proposition 4.1 alone gives the matching bound $\log_2 n$ when $m = \log_2 n$ .

Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.

Difficulty

The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only $k$ sets. To force $kr$ sets with $\mathrm{OPT} = 1$ , the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most $1 + (r-1)k$ blocks after $k$ steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly $n$ elements and exactly $m$ distinct sets without creating sets that help cover the adversary's elements.

Formalization scope

The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit $i$ (1-based) of $j$ is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).

The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set ( $\mathrm{OPT} = 1$ ), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies $\text{cost} \ge kr \cdot \mathrm{OPT}$ as $0 \ge 0$ .

The statements contain no $O(\cdot)$ : every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of $r$ and $k$ , is excluded, as are the remarks on the trivial ratio- $m$ and $O(\sqrt n)$ algorithms.

Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.

Selected references

N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The online set cover problem, Proc. 35th ACM STOC, 2003, pp. 100–105. https://doi.org/10.1145/780542.780558
U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
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):93–263, 2009. https://doi.org/10.1561/0400000024

6 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 1: A Deterministic O(log m log n)-Competitive Algorithm for Unweighted Online Set CoverResearch Paper

Motivation

Set cover asks for the fewest sets from a family $\mathcal S$ of $m$ subsets of a ground set $X$ of $n$ elements whose union contains $X$ . It is NP-hard, and the best ratio achievable in polynomial time is $\Theta(\log n)$ (Feige 1998, doi:10.1145/285055.285059).

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance $(X,\mathcal S)$ is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set $X'\subseteq X$ of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.

The question is how much an algorithm loses against an offline adversary who knows $X'$ and covers it with a family $\mathcal C_{OPT}$ . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor $O(\log m\log n)$ of $|\mathcal C_{OPT}|$ . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.

Setting

An instance consists of a finite ground set $X$ with $n=|X|$ elements and a finite family $\mathcal S$ of $m=|\mathcal S|$ sets. For an element $j$ , $\mathcal S_j$ is the collection of sets containing $j$ . Every set has cost $1$ , so the cost of a family is its number of members.

The adversary gives a sequence $\sigma$ of elements (the given elements form $X'$ ). A family $\mathcal C_{OPT}\subseteq\mathcal S$ covers $\sigma$ if each element of $\sigma$ lies in some member of it.

The algorithm keeps a weight $w_S>0$ for every set, initially $w_S=1/(2m)$ , and a cover $\mathcal C$ , initially empty. The weight of an element is $w_j=\sum_{S\in\mathcal S_j}w_S$ , and $C$ is the set of elements covered by members of $\mathcal C$ . The potential is

\Phi=\sum_{j\notin C}n^{2w_j}.

When the adversary gives an element $j$ :

if $w_j\ge1$ , nothing changes;
otherwise a weight augmentation is performed: (a) $k$ is the minimal integer with $2^k w_j>1$ ; (b) every $S\in\mathcal S_j$ gets the weight $2^k w_S$ ; (c) at most $4\log n$ sets from $\mathcal S_j$ are added to $\mathcal C$ , so that $\Phi$ does not exceed its value before the augmentation.

Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on $\sigma$ is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.

Formalization targets

Goal: Theorem 2.3

For $n\ge2$ , every arrival sequence $\sigma$ , and every family $\mathcal C_{OPT}$ covering $\sigma$ : a run of the algorithm on $\sigma$ exists, and every run ends with a cover $\mathcal C$ that covers every element of $\sigma$ and satisfies

|\mathcal C|\;\le\;\lceil 4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2).

The paper states $|\mathcal C|=O(|\mathcal C_{OPT}|\log m\log n)$ ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.

Milestones

Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most

|\mathcal C_{OPT}|\cdot(\log_2 m+2).

Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family $F\subseteq\mathcal S_j$ with $|F|\le\lceil4\ln n\rceil$ such that

\Phi_e\le\Phi_s,

where $\Phi_s$ is the potential before the iteration and $\Phi_e$ the potential after it, computed with the augmented weights and the cover $\mathcal C\cup F$ .

Significance

The theorem shows that online set cover over a known instance admits a deterministic $O(\log m\log n)$ -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves $o\!\left(\frac{\log m\log n}{\log\log m+\log\log n}\right)$ over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.

The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.

Difficulty

The central step is Lemma 2.2: a family of at most $\lceil4\ln n\rceil$ sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of $\mathcal S_j$ can exceed the cardinality bound, since $\mathcal S_j$ may contain up to $m$ sets. Adding nothing, or a single set, can increase $\Phi$ : every uncovered element sharing a set with $j$ has its weight raised, and its term $n^{2w}$ grows by a factor up to $n^{2\delta}$ . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of $n$ .

The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs $n\ge2$ and a careful treatment of the initial potential, which is at most $n^2$ and equals $n^2$ when every element lies in every set.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight ( $w_j$ ) and coveredBy ( $j\in C$ ). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. $n=|E|$ and $m=|T|$ . Weights are real numbers; $n^{2w_j}$ is the real power.

The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.

Explicit forms of the paper's asymptotic and unspecified quantities:

the paper's " $4\log n$ " sets per augmentation is $\lceil 4\ln n\rceil$ (natural logarithm, rounded up: the proof repeats a random choice that many times and needs $(1-\delta/2)^{4\log n}\le n^{-2\delta}$ );
Lemma 2.1's $\log m+2$ is $\log_2 m+2=\log_2(4m)$ (weights grow from $1/(2m)$ to at most $2$ by factors at least $2$ );
Theorem 2.3's $O(|\mathcal C_{OPT}|\log m\log n)$ is $\lceil4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2)$ ;
$k$ ranges over natural numbers; for $w_j<1$ the minimal integer with $2^kw_j>1$ is one;
the paper's remark "(Clearly, $2^k\cdot w_j<2$ .)" is not encoded; the correct bound is $\le2$ ( $w_j=1/2$ gives $k=2$ ) and is not a hypothesis anywhere.

The goal adds the hypothesis $n\ge2$ , which the paper's $\log n$ assumes tacitly: for $n=1$ no set may be added and the element is never covered.

Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.

A complete development needs elementary real analysis (Real.rpow, Real.log, $1-x\le e^{-x}$ ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.

Selected references

N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
U. Feige, A Threshold of ln n for Approximating Set Cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
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):93–263, 2009. https://doi.org/10.1561/0400000024

7 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 1: Independence of Irrelevant Alternatives with a Universal Benchmark Yields Logit Selection ProbabilitiesResearch Paper

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$ . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$ , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$ ; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$ , chooses $x\in B$ . For every $s$ and possible $B$ , $x\mapsto P(x\mid s,B)$ is a probability vector on $B$ . Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

Axiom 1 (IIA). For all possible $B$ , all $s$ and all $x,y\in B$ : $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$ .
Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$ , all $s$ , all $x\in B$ .
Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$ , and $p_{xx}=\tfrac12$ by definition.
The function $V$ . $V(s,x,z)=\log(p_{xz}/p_{zx})$ .
Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$ , with $v(s,x)=V(s,x,z)$ , for every $s$ , every possible $B$ (containing $z$ or not) and every $x\in B$ :

P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$ , Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$ .
Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$ .
Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$ .
Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
Equation (10): for a benchmark $z\in B$ , $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$ .

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$ . The goal requires a single $v$ for all sets, including sets that do not contain $z$ , where neither Equation (10) nor the axioms on $B$ alone say anything about $z$ . A second subtlety is the diagonal: $\{x,x\}=\{x\}$ , so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$ , never as "for each $B$ there is a $v$ ", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

7 thms2 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 1: Deterministic Double Greedy Achieves 1/3 of the OptimumResearch Paper

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$ . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$ , a randomized local search achieving $2/5$ , and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$ .
Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$ -approximation (this mission) and a randomized linear-time $1/2$ -approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ , and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$ . In iteration $i = 1, \dots, n$ it computes

a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$ , $Y_i = Y_{i-1}$ ; otherwise $X_i = X_{i-1}$ , $Y_i = Y_{i-1} \setminus \{u_i\}$ . A tie adds $u_i$ . After $n$ iterations $X_n = Y_n$ , which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$ , which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$ . In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$ ,

X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).

Milestones

Lemma II.1. For every $1 \le i \le n$ , $a_i + b_i \ge 0$ .
The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$ .
Lemma II.2. For every $1 \le i \le n$ ,

f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].

The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$ .
Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$ .

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$ , is the template the paper then refines into the randomized $1/2$ -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$ , which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$ , not against $OPT$ . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$ ") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$ .
The tie rule is line 5's $a_i \ge b_i$ : ties add $u_i$ .
Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$ , because $f(OPT)$ may be $0$ .
Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$ -approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$ , without which $f \equiv 0$ would satisfy it.
Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$ . A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$ " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

9 thms2 active usersReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 6: An Attractor Whose Basin Meets the Attainable Set Contains the Limit Set with Positive ProbabilityResearch Paper

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing step sizes $\gamma_n$ and a noise term $U_{n+1}$ . Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$ . In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$ . Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$ , and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$ : a continuous map $(t,x)\mapsto\Phi_t(x)$ with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ .

A set $A$ is invariant if $\Phi_t(A)=A$ for all $t\ge0$ , and positively invariant if $\Phi_t(A)\subset A$ .
An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$ .
A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$ , for every $T>0$ .
The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$ .
For $T>0$ , $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$ .

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$ , adapted to a filtration $(\mathcal F_t)_{t\ge0}$ . The standing assumption of Section 7 is that for all $\delta>0$ , $T>0$ and $t\ge0$ ,

P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$ .

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$ . $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$ , and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$ , then

P\big(L(X)\subset A\big)>0 .

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$ , there are $T,\delta>0$ , depending only on $U$ (and on $\Phi$ , $A$ ), such that for every process satisfying the standing assumption and every $t\ge0$

P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).

Milestones

Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$ .
Lemma 7.1, in three parts:
- $\mathrm{Att}(X)$ is closed;
- it is positively invariant;
- it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$ . That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
A probabilistic step that applies (24) at the random time when $X$ first enters $U$ . That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$ , for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$ " and "sup $<\delta$ " are exact even when the supremum is infinite or not attained.
The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
$w$ is required to be both nonincreasing in $t$ and convergent to $0$ .
The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$ .
Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$ , not inclusion.
The almost-sure clause of Lemma 7.1 is stated for separable $M$ . Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$ , and a probability bound $w$ without monotonicity.

A complete development needs:

limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
measurability of path functionals of continuous processes;
conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

11 thms2 active usersReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 3: Martingale Noise with Bounded q-th Moments and Summable γ_n^(1+q/2) Satisfies Assumption A1 Almost SurelyResearch Paper

Motivation

A stochastic approximation algorithm is a recursion

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

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

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or $F$ is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$ . A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded $q$ -th moments and step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$ . The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.

Setting

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

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

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

Assumption A1 asks that for every $T>0$

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

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

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

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

Formalization targets

Goal: Proposition 4.2

For a Robbins–Monro algorithm and some real $q\ge2$ , if

\sup_nE\big(\|U_{n+1}\|^q\big)<\infty\qquad\text{and}\qquad\sum_n\gamma_n^{1+q/2}<\infty,

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

Milestones

Eq. (13), an instance of Burkholder's inequality with a universal constant $C_q$ :

E\Big\{\sup_{n<k\le m(\tau_n+T)}\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|^q\Big\}\le C_q\,E\Big\{\Big[\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2\|U_{i+1}\|^2\Big]^{q/2}\Big\}.

Inequality (14), for finite families with $\alpha_i\ge0$ , $u>1$ , $0<\delta<1$ :

\Big(\sum_i|\alpha_i\beta_i|\Big)^u\le\Big(\sum_i\alpha_i^{\delta u/(u-1)}\Big)^{u-1}\sum_i\alpha_i^{(1-\delta)u}|\beta_i|^u.

Eq. (16): for every $T>0$ there is $C(q,T)$ with $E(\Delta(t,T)^q)\le C(q,T)\int_t^{t+T}\bar\gamma^{q/2}(s)\,ds$ for all $t\ge0$ .
Eq. (17): $\sum_{k\ge0}E(\Delta(kT,T)^q)<\infty$ for every $T>0$ .
Block comparison: $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$ .

Significance

Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With $q=2$ it covers step sizes with $\sum\gamma_n^2<\infty$ (for example $\gamma_n=1/n$ ) and noise with bounded variance; larger $q$ trades stronger moment assumptions for slower decay of the steps, down to $\sum\gamma_n^{1+q/2}<\infty$ . Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of $F$ ; the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in $L^q$ , and the continuous-time bookkeeping of the step processes $\bar U$ , $\bar\gamma$ and the noise deviation $\Delta$ , shared by the other missions of this series.

Difficulty

The obvious argument controls each window by Doob's $L^2$ maximal inequality and sums over windows. That works for $q=2$ only. For $q>2$ the second moment of the window sums is not summable under $\sum\gamma_n^{1+q/2}<\infty$ , and one needs an $L^q$ maximal inequality whose right-hand side is the $q/2$ -th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to $\Delta(t,T)$ requires handling partial steps at both ends of $[t,t+h]$ . A second subtlety is that A1 quantifies over all $T>0$ : the almost-sure statement must hold on a single event of full probability for every $T$ , not on an event that depends on $T$ .

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d); time is real; $q$ is a real number with $q\ge2$ , and all powers are real powers of nonnegative quantities. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$ , and their values at $0$ are unused, as the paper indexes them from $1$ . The filtration is a Mathlib Filtration ℕ, $U_{n+1}$ is required to be $\mathcal F_{n+1}$ -strongly measurable and integrable, and the martingale difference condition is $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. Expectations of nonnegative quantities, the suprema in A1 and $\Delta$ , and the moment bound are taken in $[0,\infty]$ , so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of $k$ is $0$ .

The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each $T$ , A1 holds almost surely" in place of "almost surely, A1 holds for all $T$ ", and $q$ fixed to $2$ or restricted to integers.

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

Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probability Theory and Related Fields 74 (1987), 403–428.
D. L. Burkholder, Distribution function inequalities for martingales, Annals of Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. W. Stroock, Probability Theory: An Analytic View, Cambridge University Press, 1993.
H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.

10 thms2 active usersReviewed

Linear Optimization Optimization Probability+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$ , right-hand sides $y_1,\ldots,y_n\in\mathbb R$ , and an objective vector $z\in\mathbb R^d$ :

\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$ -element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$ : $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$ . The first phase solves the relaxed program LP′ from the objective $A_I\alpha$ .

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$ . For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$ , together with two artificial constraints at first coordinates $1$ and $-1$ . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$ .

For positive right-hand sides, an optimal polar simplex is a $d$ -subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$ . The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$ . Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$ , where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$ . The algorithm has separate random choices of $\mathcal I$ and $\alpha$ .

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$ . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$ , there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$ , the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$ , not standard deviation $\sigma$ . The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$ .

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$ , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$ , so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$ . The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$ . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

22 thms2 active usersReviewed

Discrete Geometry Linear Optimization Optimization+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 1: The Expected Shadow of a Gaussian-Perturbed Polytope Has Polynomially Many VerticesResearch Paper

Why the shadow of a perturbed polytope matters

The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints $n$ , the dimension $d$ and $1/\sigma$ (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).

Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order $nd^3/\sigma^6$ — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on $n$ to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained $O(d^2\sqrt{\log n}\,\sigma^{-2})$ for small $\sigma$ .

Setting

Fix $d\ge3$ and $n>d$ . The data are vectors $a_1,\dots,a_n\in\mathbb R^d$ , the constraint vectors of the linear program $\max\langle z|x\rangle$ subject to $\langle a_i|x\rangle\le1$ for all $i$ . Each $a_i$ is a Gaussian of standard deviation $\sigma$ centered at a point $\bar a_i$ with $\|\bar a_i\|\le1$ : it has density

\mu_i(a)=\Big(\tfrac{1}{\sqrt{2\pi}\,\sigma}\Big)^d e^{-\|a-\bar a_i\|^2/2\sigma^2},

and the $a_i$ are independent (joint density $\prod_i\mu_i(a_i)$ ).

For a direction $q\in\mathbb R^d$ , $\mathrm{optSimp}_q(a_1,\dots,a_n)$ is the set of index sets $I\subseteq\{1,\dots,n\}$ with $|I|=d$ such that $(a_i)_{i\in I}$ is linearly independent, the simplex $\triangle(A_I)=\mathrm{ConvHull}(a_i:i\in I)$ is a facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ , and $q$ lies in the cone $\{\sum_{i\in I}\alpha_ia_i:\alpha_i\ge0\}$ . In polar terms, $I$ is the set of tight constraints at the vertex of the feasible polyhedron that maximizes $\langle q|x\rangle$ .

For linearly independent $t,z$ , the shadow $\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)$ is the set of index sets $I$ that belong to $\mathrm{optSimp}_q$ for some nonzero $q\in\mathrm{Span}(t,z)$ . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane $\mathrm{Span}(t,z)$ ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally

\mathcal D(n,d,\sigma)=\frac{58{,}888{,}678\,nd^3}{\min\big(\sigma,\,1/(3\sqrt{d\ln n})\big)^6}.

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

\mathbb E_{a_1,\dots,a_n}\big[\,|\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)|\,\big]\le\mathcal D(n,d,\sigma)

for every $d\ge3$ , $n>d$ , every pair of linearly independent $t,z$ , every $\sigma>0$ and all centers of norm at most $1$ .

Milestones

The milestones follow the paper's proof, leaves first.

Probability tools: the chi-square bound (Corollary 2.4.6), the combination lemma (Lemma 2.3.5), almost polynomial densities (Lemma 2.3.7), and comparing Gaussian tails (Lemma 2.4.11).
Reduction: the measure of the event $P=\{\|a_i\|\le2\ \forall i\}$ (Proposition 4.0.5), and the discretization of the shadow into $m$ equally spaced directions (Lemma 4.0.6).
Angle bound: the probability, conditioned on $P$ , that the ray through a fixed unit vector $q$ passes within angle $\varepsilon$ of the boundary of its optimal facet is $O(nd^3\varepsilon/\sigma^6)$ (Lemma 4.0.7, from Lemma 4.0.11).
Distance and incidence: in Blaschke coordinates $a_i=R_\omega b_i+sq$ , a deterministic split (Lemma 4.0.12), a distance bound (Lemmas 4.1.1–4.1.3) and an angle-of-incidence bound (Lemmas 4.2.1–4.2.3).

Significance

The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.

Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.

Difficulty

The obvious approach is to count, for each candidate facet $I$ , the probability that $I$ appears in the shadow; there are $\binom nd$ candidates, so a union bound is exponential in $d$ . The paper avoids this by discretizing the angle of $q$ (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between $q$ and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of $a_1,\dots,a_d$ , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal $\omega$ , offset $s$ and in-plane coordinates $b_i$ (Corollary 2.5.3), whose Jacobian contributes the factors $\langle\omega|q\rangle$ and $\mathrm{Vol}(\triangle(b))$ . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence $\langle\omega|q\rangle$ are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's $\{1,\dots,d\}$ is $\{i:i<d\}$ . The Gaussian of standard deviation $\sigma$ centered at $c$ is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of $[0,\infty]$ -valued counts, and their measurability is part of each conclusion. "Density proportional to $\nu$ " and conditional probabilities are stated cross-multiplied, $\int_{E}\nu\le\text{bound}\cdot\int\nu$ , so no $0/0$ appears.

The shadow is the set of index sets $I$ , and the direction $q=0$ is excluded. Including it would add every facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ to the shadow, since $0$ lies in every cone, and make the goal false. $\mathrm{ang}(q,\emptyset)=\infty$ is represented exactly in $[0,\infty]$ , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions $d\ge3$ , $n>d$ and $\sigma\le1/(3\sqrt{d\ln n})$ (Lemma 4.2.3 is false without a bound on $\sigma$ ), unit length of the reference vector $q$ , $s\ge0$ , and $\varepsilon>0$ for strict inequalities. Lemma 2.3.7 is stated with $\le$ rather than the page's $<$ , which fails in an edge case.

Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on $S^{d-1}$ (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.

Selected references

D. A. Spielman, S.-H. Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003. https://arxiv.org/abs/cs/0111050v7
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. https://doi.org/10.1145/990308.990310
K. H. Borgwardt, The Simplex Method: A Probabilistic Analysis, Springer, 1987.
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, 159–175.
A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005, 387–396.
R. Vershynin, Beyond Hirsch conjecture: walks on random polytopes and smoothed complexity of the simplex method, SIAM J. Comput. 39(2):646–678, 2009. https://doi.org/10.1137/070683386
D. Dadush, S. Huiberts, A friendly smoothed analysis of the simplex method, STOC 2018; arXiv:1711.05667. https://arxiv.org/abs/1711.05667

29 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

Multi-parameter Mechanism Design and Sequential Posted Pricing 4: A 6.75-Approximate Truthful Posted-Price Menu for Unit-Demand Buyers of Multiple ItemsResearch Paper

Motivation

A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least $1/6.75$ of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).

Setting

Single-parameter problem (BSMD). Finitely many agents $i$ have independent private values $v_i \sim F_i$ , each with a density on a bounded interval. A seller may serve any set in a downward-closed set system $\mathcal J$ . A deterministic mechanism $M$ maps reported values $v$ to a served set $M(v) \in \mathcal J$ and payments $\pi_i(v)$ ; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_v[\sum_i \pi_i(v)]$ . For prices $p$ , agent $i$ desires service if $p_i \le v_i$ , and $\mathcal S_v$ is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is

\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{v}\Big[\min_{S \in \mathcal S_v} \sum_{i \in S} p_i\Big],

a lower bound on the revenue of posting the prices $p$ to the agents in an adversarial order.

Multi-parameter unit-demand problem (BMUMD). There are $m$ buyers and a finite set $J$ of services, partitioned into the groups $J_i$ of services targeted at buyer $i$ . Buyer $i$ has value $v_j$ for each $j \in J_i$ , all values independent with $v_j \sim F_j$ , and the set system $\mathcal J \subseteq 2^J$ is unit-demand: $|S \cap J_i| \le 1$ for feasible $S$ . A mechanism $\mathcal A$ is truthful if no buyer gains by misreporting its whole vector $(v_j)_{j \in J_i}$ , and individually rational if a buyer receiving $j$ pays at most $v_j$ and a buyer receiving nothing pays $0$ .

Copies. The instance $\mathcal I^{\mathrm{copies}}$ replaces each buyer $i$ by $|J_i|$ single-parameter agents, one per service $j \in J_i$ with value $v_j$ , under the same $\mathcal J$ .

Price menus. Given prices $(p_j)$ and an arrival order $\sigma$ , the price-menu mechanism approaches the buyers in order; buyer $i$ is offered the services of $J_i$ that can still be feasibly allocated, at prices $p_j$ , and buys a utility-maximizing one if some has $p_j \le v_j$ .

Multiple copies of items. With items $K$ and $\mathrm{cap}(k)$ copies of item $k$ , services are pairs $(i,k)$ and a set of services is feasible if it gives each buyer at most one item and uses at most $\mathrm{cap}(k)$ copies of $k$ : the intersection of two partition matroids.

Formalization targets

Goal: Theorem 14

For regular distributions there are prices $p$ such that, for every arrival order $\sigma$ , the price-menu mechanism $\mathcal P_\sigma$ is truthful and

\mathcal R^{\mathcal A} \le \tfrac{27}{4}\,\mathcal R^{\mathcal P_\sigma}

for every individually rational, truthful deterministic mechanism $\mathcal A$ .

Milestones

Truthful BMUMD mechanisms are weakly monotone (p. 13), and the allocation of $\mathcal A^{\mathrm{copies}}$ is monotone in each $v_j$ (p. 13).
Lemma 3: $\mathcal R^{\mathcal A} \le \mathcal R^{\mathcal A'}$ for some truthful $\mathcal A'$ on $\mathcal I^{\mathrm{copies}}$ .
The price-menu mechanism allocates a maximal feasible set of services (p. 14).
Theorem 4: if $\mathcal R^{M'} \le \alpha\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M'$ on $\mathcal I^{\mathrm{copies}}$ , then $\mathcal R^{\mathcal A} \le \alpha\,\mathcal R^{\mathcal P_\sigma}$ for every $\sigma$ and every truthful IR $\mathcal A$ .
Lemma 2 (regular part): $\mathcal R^M \le \sum_i p^M_i q^M_i$ , with $q^M_i$ the probability that $M$ serves $i$ and $F_i(p^M_i) = 1 - q^M_i$ .
Theorem 19 (existence form): a revenue-optimal truthful mechanism exists.
The claim $c_i \ge 4/9$ of App. D.4: under $\sum_{i' \in P} q_{i'} \le \mathrm{cap}(P)/3$ in every part, with probability at least $4/9$ neither part of $i$ is full without $i$ .
Theorem 13: for two partition matroids there are prices with $\mathcal R^M \le \tfrac{27}{4}\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M$ .

Significance

The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.

All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant $6.75$ , and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.

Difficulty

Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.

Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by $1/3$ . The step that is easy to get wrong is the probability that an agent is considered: the events "part $P_1$ is not full" and "part $P_2$ is not full" depend on overlapping agents, so the product bound $(2/3)(2/3)$ does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.

Formalization scope

Distributions (P1): each $F_j$ has a measurable density, strictly positive on a bounded interval $[\underline v_j, \overline v_j] \subseteq [0, \infty)$ , with no mass outside. Values are independent (product prior).
Regularity (P2): the virtual value $\phi(v) = v - (1 - F(v))/f(v)$ is non-decreasing on the support. It is assumed in Lemma 2, Theorem 19, Theorem 13 and the goal. Theorem 14 does not state it, but its proof goes through Theorem 13, which the paper proves for regular distributions; the non-regular extension (App. E, randomized prices) is out of scope, as is the second paragraph of Lemma 2.
Mechanisms (P3): deterministic; dominant-strategy truthful with misreports in the support (a buyer misreports all coordinates of $J_i$ at once); single-parameter IR is ex-post nonnegative utility; multi-parameter IR is the paper's ( $\pi_i \le v_j$ if served $j$ , $\pi_i = 0$ if unserved); allocation events and payments measurable, payments integrable.
Benchmarks (P4): Myerson's mechanism is not constructed. "Approximates $\mathcal R^{\mathcal M}$ " is stated against every truthful mechanism, and Lemma 3 and Theorem 19 in existence form.
Price menus: ties between utility-maximizing services are broken by a fixed enumeration of $J$ ; a service of utility $0$ is bought. Theorem 4 assumes $\alpha \ge 0$ .
Dropped: the last sentence of Theorem 14 (polynomial-time computability of the prices) has no cost model here.
Constant: $6.75$ is written $27/4$ everywhere.
Not trivializable: the prices in Theorem 13 and the goal are chosen before the mechanism, and the benchmark includes every truthful mechanism, so a degenerate price vector cannot meet the bound; $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over a nonempty finite class.

Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.

Selected references

S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
S. Chawla, J. D. Hartline, R. Kleinberg, Algorithmic Pricing via Virtual Valuations, EC 2007. https://arxiv.org/abs/0711.3203
A. M. Manelli, D. R. Vincent, Multidimensional mechanism design: Revenue maximization and the multiple-good monopoly, Journal of Economic Theory 137(1), 2007. https://doi.org/10.1016/j.jet.2006.12.007
T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc. 56, 1960. https://doi.org/10.1017/S0305004100034241

15 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Optimal Policies for a Multi-Echelon Inventory Problem: The Two-Echelon Optimal Cost Splits into the Isolated Installation-1 Cost Plus a Function of Echelon StockResearch Paper

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$ , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$ . The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$ , $\alpha\ge0$ .

The state at the start of a period is $(x_1,w_1,x_2)$ : $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$ . Installation 1 pays the expected holding and shortage cost (1),

L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$ ,

C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$ , $\hat C_0\equiv0$ :

\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$ ,

C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$ , as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$ , with $f_n$ of (7) (p. 480).
Convexity of every $f_n$ (§2 item 3, p. 478).
Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$ .
Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.

Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$ .

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$ . When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$ . The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$ . Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$ . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$ . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$ ; $\varphi\ge0$ with $\int_0^\infty\varphi=1$ ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$ ) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$ , no convexity of $\tilde L$ , no $K=0$ and no sign condition on $w_1$ is assumed.
Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$ ; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$ ; outside it the feasible set of (14) is empty.
The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$ , and $f_n\equiv0$ for $n\le2$ .

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$ , and of any milestone are welcome.

Selected references

A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

8 thms2 active usersReviewed

Completed

Dynamic Programming Graph Theory Theoretical Computer Science·Captain: mikedeng1

Algorithm 97: Shortest Path: Floyd's Procedure Computes the Shortest Path Length Between Every Pair of PointsResearch Paper

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$ . The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$ ; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$ . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$ ; a missing link gives length $\infty$ . Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$ , this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$ , then row $j$ , then column $k$ , each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$ . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$ , using chains of one or more links. Its comment asserts

\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$ ,

\operatorname{shortestPath}(w)(i,j)=\infty.

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$ , every matrix $w$ with no negative cycle, and all points $i,j$ ,

\operatorname{shortestPath}(w)(i,j)=d_w(i,j).

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$ . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$ ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$ , the procedure changes that entry to $-2$ , although the shortest simple closed path has length $-1$ . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

6 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$ . Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$ , so $D(0) = H(0) = 0$ . For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$ , let $\tilde C(i) = c_i - H(i-1)$ , and let

S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$ .

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$ ,

F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$ .

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$ , with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$ . Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$ .

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$ . The $j$ th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$ , for every potential cumulative demand in some open interval above $D(j)$ .

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$ , ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$ , with equal $\tilde C$ -values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$ . Then

S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}

Milestones

In attack order:

identity (1a) for the carrying costs;
Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$ ;
the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$ ;
the strict chains (7)–(8) of the Appendix;
Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$ ;
Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$ , $g(k+1) \le g(k)$ removes $i_k$ , and $g(r) = \infty$ removes $i_r$ .

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$ , up to a term that does not depend on $l$ .

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$ , and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

equal slopes, where $G = \pm\infty$ ;
several lines meeting at one point;
the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$ , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$ . Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final " $< \infty$ " of (6) is part of the condition.
Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
Disclosed change 1, $\Omega(j)$ . The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$ . This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$ ".
Disclosed change 2, Lemma 2(d). The printed hypothesis " $c_{k,l} < c_l$ " duplicates part (c) and is read as " $c_{k,l} = c_l$ ". The equivalence " $\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$ " is stated under $A(k,l) \ne 0$ , since $A(k,l) = 0$ gives $G = +\infty$ by (5).
Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$ : rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$ , never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
Reusable infrastructure. The model, the recursion (2), $A$ , $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

16 thms2 active usersReviewed

Completed

Optimization Stochastic Systems·Captain: mikedeng1

An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems: Algorithm OPT Returns an Optimal Reorder Point and Order QuantityResearch Paper

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$ , an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$ . It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$ . In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$ , has the form

C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}

The paper's standing assumptions on $G$ are:

$-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
$\lim_{|y|\to\infty}G(y)=\infty$ .

The sequence $y_Q$ . Let $y_1$ be an integer minimizing $G$ . Given $y_1,\dots,y_Q$ , let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$ , and set

y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$ , and

C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$ , $Q=1$ , $C^*=S$ , $r=y_1-1$ , $R=y_1+1$ . Each pass compares $G(r)$ and $G(R)$ ; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$ . The output is the final $(r,Q)$ .

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$ , stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

§2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$ .
Figure 1 (p. 809): $y_{Q+1}$ has the least $G$ -value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$ .
Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$ .
Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$ .
Display before (6): $\min_r C(r,Q)=C^*(Q)$ .
(6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$ , and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$ .
Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$ .

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$ , an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$ . Because it uses only the form (1) and the unimodality of $-G$ , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$ .

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$ .

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$ , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$ : "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$ , not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$ , and fails for constant $G$ .

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$ , $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

Types. $G:\mathbb Z\to\mathbb R$ , $\kappa\in\mathbb R$ with $\kappa>0$ , reorder points in $\mathbb Z$ , order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$ , so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$ .
Assumptions. " $-G$ unimodal" is NegUnimodal G: $\exists m$ , $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$ . " $\lim_{|y|\to\infty}G=\infty$ " is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$ -weights it holds for every function.
The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$ , as the paper defines them, is the first milestone.
The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$ , $C^*\le G(R)$ ; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$ , under the paper's simplification $y_1>0$ ; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$ , which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$ . Lemma 2's " $Q^*$ " is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise " $r^*(Q)=L(Q)-1$ " means $L(Q)-1$ is an optimal reorder point.
Ruled out. Defining the algorithm's output as an argmin of $C$ , or by searching for Lemma 2's $q$ , would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

10 thms2 active usersReviewed

Graph Theory Linear Optimization Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources VIII: A Vertex Schedule Maximizes the Net Present Value iff Its Spanning-Tree Subprojects Have the Right SignsTextbook

Motivation

Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.

This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ , $n\ge1$ , where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Temporal constraints are the arcs of a project network $N=\langle V,E;\delta\rangle$ : an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ requires $S_j-S_i\ge\delta_{ij}$ for the start times $S_i$ . A maximum project duration $\bar d$ is the arc $\langle n+1,0\rangle$ with weight $-\bar d$ . The time-feasible region is

\mathcal S_T=\{S\in\mathbb R^{n+2}_{\ge0}\mid S_0=0,\ S_j-S_i\ge\delta_{ij}\ (\langle i,j\rangle\in E)\}.

Let $0<\beta\le1$ be the discount rate ( $\beta=1/(1+I)$ for an interest rate $I$ ) and $c_i^F\in\mathbb R$ the cash flow of activity $i$ , paid at its completion time $C_i=S_i+p_i$ . The problem (3.9.1) is

\text{minimize } f(S)=-\sum_{i\in V}c_i^F\beta^{S_i+p_i}\quad\text{subject to } S\in\mathcal S_T,

and a minimizer is a time-optimal schedule. A vertex of $\mathcal S_T$ is an extreme point. A spanning tree $G=\langle V,E^G\rangle$ is associated with $S$ if $E^G\subseteq E$ , $E^G$ has $n+1$ arcs and a connected underlying undirected graph, and $S$ is the unique solution of $S_0=0$ , $S_j-S_i=\delta_{ij}$ for $\langle i,j\rangle\in E^G$ . Deleting a tree arc $\langle i,j\rangle$ splits $G$ into two subtrees; $V_{ij}$ is the node set of the one not containing $0$ . The arc is forward if the tree path from $0$ passes it from $i$ to $j$ and backward otherwise, and

npv^{ij}(S)=\sum_{h\in V_{ij}}c_h^F\beta^{S_h+p_h}

is the net present value of the subproject $V_{ij}$ . Finally, $f$ is binary-monotone if it is monotone on every line $\{S+\lambda z\ge0\mid\lambda\in\mathbb R\}$ with direction $z\in\{0,1\}^{n+2}$ (Definition 3.3.2).

Formalization targets

Goal: Proposition 3.9.2, pinned reading

Assume every node is reached from $0$ by a path of nonnegative length (the standing convention of §1.2) and let $S$ be a vertex of $\mathcal S_T$ .

\text{(sufficiency)}\quad G \text{ associated with } S,\ \ npv^{ij}(S)\ge0 \text{ on forward arcs},\ npv^{ij}(S)\le0 \text{ on backward arcs}\ \Longrightarrow\ S \text{ time-optimal};

\text{(necessity, } \beta<1)\quad S \text{ time-optimal}\ \Longrightarrow\ \exists\, G \text{ associated with } S \text{ satisfying the sign conditions}.

The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.

Milestones

§3.3.5: the net present value objective is binary-monotone and sum-separable.
§3.9.1: if $\mathcal S_T$ is nonempty and bounded, some vertex of $\mathcal S_T$ is time-optimal.
Proposition 3.2.16: every vertex of $\mathcal S_T$ has an associated spanning tree, an outtree rooted at $0$ if the vertex is a minimal point.
Proposition 3.5.4: a directed forest with at least one node has a source with at most one successor or a sink with exactly one predecessor.

Significance

Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.

The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.

Difficulty

The objective $f$ is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of $\mathcal S_T$ is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than $n+1$ temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree $V_{ij}$ , forward and backward orientation relative to the root) have to be connected to the geometry of $\mathcal S_T$ through Proposition 3.2.16, whose proof in the book is a citation.

Formalization scope

Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ . $\beta^x$ is Real.rpow, and every statement assumes $0<\beta\le1$ as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of $n+1$ arcs whose SimpleGraph.fromRel is connected; $V_{ij}$ is the set of nodes not reachable from $0$ once the arc is deleted.

Three readings are committed and disclosed in the item statements. Necessity is stated only for $\beta<1$ : at $\beta=1$ the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from $0$ to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by $S_i\ge0$ rather than by arcs of $N$ , and necessity fails. The existence of an optimal vertex assumes $\mathcal S_T$ nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns $PS\infty|temp,\bar d|f$ only.

The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of $N$ that are binding at $S$ and determine $S$ uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1 (p. 203), §3.3.5 (pp. 224–225), §3.5.2 (p. 252), §3.9.1 (pp. 333–334). https://doi.org/10.1007/978-3-540-24800-2
A. H. Russell, "Cash flows in networks", Management Science 16 (1970), 357–373. https://doi.org/10.1287/mnsc.16.5.357
R. C. Grinold, "The payment scheduling problem", Naval Research Logistics Quarterly 19 (1972), 123–136.
C. Schwindt, J. Zimmermann, "A steepest ascent approach to maximizing the net present value of projects", Mathematical Methods of Operations Research 53 (2001), 435–450.
C. Schwindt, J. Zimmermann, "Parametrische Optimierung als Instrument zur Bewertung von Investitionsprojekten", Zeitschrift für Betriebswirtschaft 72 (2002), 593–617.
R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993.
C. Berge, Graphs and Hypergraphs, North-Holland, Amsterdam, 1976.

9 thms2 active usersReviewed

Convex Optimization Linear algebra Optimization·Captain: mikedeng1

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$ , so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$ . The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$ . The primal SDP and dual SDP are

\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$ .

For a positive integer $r\le n$ , the low-rank program is

(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$ , and $S(y)=C-\sum_i y_iA_i$ . A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$ . The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$ , obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$ , $S^*=S(y^*)$ , $S^*R^*=0$ . If $\hat R$ is a local minimum of $(N_{r+1})$ , then

X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.

Milestones

The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$ , $\nabla_RL(R,y)=2SR$ , and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$ .
Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$ , and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$ .
Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$ .
Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$ .

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$ ; if the zero-column extension is still a local minimum of $(N_{r+1})$ , the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$ : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$ ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$ , and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$ , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems III: Contextual Bandits and the Banditron Mistake BoundTextbook

Motivation

In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.

This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, $N$ experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of $K$ labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret $O(n^{2/3})$ .

Setting

There are $K \ge 2$ arms (or labels) $\{1,\dots,K\}$ and rounds $t = 1, \dots, n$ .

Adversarial losses. At round $t$ an adversary assigns losses $\ell_{i,t} \in [0,1]$ to the arms and may adapt to the forecaster's past plays $I_1, \dots, I_{t-1}$ . The forecaster draws $I_t$ at random from a distribution $p_t$ that depends on what it has observed, and it observes only $\ell_{I_t,t}$ . Expectations $\mathbb E$ are over the forecaster's draws.

Side information. Each round carries a context $s_t$ from a finite set $\mathcal S$ , and the sequence $s_1, s_2, \dots$ is fixed in advance. The pseudo-regret against context-to-arm maps is

\overline R^{\mathcal S}_n = \max_{g:\mathcal S\to\{1,\dots,K\}} \mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \ell_{g(s_t),t}\Big].

The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.

Expert advice. At each round each of $N$ experts $j$ proposes a distribution $\xi^j_t$ over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is

\overline R^{\mathrm{ctx}}_n = \max_{k=1,\dots,N}\mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \mathbb E_{i\sim\xi^k_t}\ell_{i,t}\Big].

Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.

Bandit multiclass. The examples $(x_t, y_t) \in \mathbb R^d \times \{1,\dots,K\}$ are fixed in advance, with $\|x_t\| = 1$ (Euclidean). A $K\times d$ matrix $U$ classifies $x$ by $\arg\max_i (Ux)_i$ . Its multiclass hinge loss on round $t$ is $\ell_t(U) = [1 - (Ux_t)_{y_t} + \max_{i\neq y_t}(Ux_t)_i]_+$ . Write $L_n(U) = \sum_{t\le n}\ell_t(U)$ for the cumulative hinge loss, $\bar L_n(U) = L_n(U)/n$ for its average, and $\|U\|$ for the Frobenius norm. The multiclass Perceptron predicts $\hat y_t = \arg\max_i (W_tx_t)_i$ and, after seeing $y_t$ , adds $x_t$ to row $y_t$ and subtracts it from row $\hat y_t$ . The Banditron (p. 58) predicts $Y_t$ from $p_{i,t} = (1-\gamma)\mathbb 1_{\hat y_t = i} + \gamma/K$ . It observes only $\mathbb 1_{Y_t = y_t}$ and updates $W_{t+1} = W_t + \widetilde X_t$ , where $(\widetilde X_t)_{i,j} = x_{t,j}\big(\mathbb 1_{Y_t=y_t}\mathbb 1_{Y_t=i}/p_{i,t} - \mathbb 1_{\hat y_t=i}\big)$ . Its number of mistakes is $M_n = \sum_{t\le n}\mathbb 1_{Y_t\neq y_t}$ .

Formalization targets

Goal: Theorem 4.7 (Banditron)

For $n \ge 8K$ , $\gamma = (K/n)^{1/3}$ , every example sequence as above and every $K\times d$ matrix $U$ ,

\mathbb E\,M_n \le L_n(U) + \Big(1 + \|U\|\sqrt{2\bar L_n(U)}\Big)K^{1/3}n^{2/3} + 2\|U\|^2K^{2/3}n^{1/3} + \sqrt2\,\|U\|K^{1/6}n^{1/3}.

Milestones

Multiclass Perceptron bound (Section 4.4, p. 57). For every $n \ge 1$ and $U$ , $\sum_{t\le n}\mathbb 1_{\hat y_t\ne y_t} \le L_n(U) + 2\|U\|^2 + \|U\|\sqrt{2n\bar L_n(U)}$ .
Theorem 4.1 (p. 44). S-Exp3 satisfies $\overline R^{\mathcal S}_n \le \sqrt{2n|\mathcal S|K\ln K}$ .
Theorem 4.2 (p. 46), with corrected constants. Exp4 without mixing satisfies $\overline R^{\mathrm{ctx}}_n \le \sqrt{2nK\ln N}$ for $\eta_t = \sqrt{2\ln N/(nK)}$ , and $\overline R^{\mathrm{ctx}}_n \le 2\sqrt{nK\ln N}$ for $\eta_t = \sqrt{\ln N/(tK)}$ .
Theorem 4.3 (p. 50), with corrected learning rate. Let the plays be drawn from distributions $q_t$ with $q_{i,t}\ge\varepsilon > 0$ , and let Exp3 run on the estimates $\ell_{i,t}\mathbb 1_{I_t=i}/q_{i,t}$ with $\eta = \sqrt{2\varepsilon\ln K/n}$ . Then $\max_k \mathbb E\big[\sum_t \mathbb E_{i\sim p_t}\ell_{i,t} - \sum_t\ell_{k,t}\big] \le \sqrt{(2n/\varepsilon)\ln K}$ .

Significance

Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most $O(K^{1/3}n^{2/3})$ mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays $O(\sqrt n)$ . The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.

The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.

Difficulty

The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks $\langle U, W_{n+1}\rangle$ and $\|W_{n+1}\|^2$ . It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order $K/\gamma$ on rounds where $\hat y_t \neq y_t$ and of order $\gamma$ otherwise. Combining these into one inequality for $\sum_t\mathbb P(\hat y_t\neq y_t)$ and then for $\mathbb E M_n$ requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.

Formalization scope

Rounds and laws. Rounds are numbered from $0$ in Lean (Lean round $t$ is the book's round $t+1$ ). Every forecaster is a sampling rule from past plays to weights on Fin K. The law of the first $n$ plays is the product $\prod_t p_t(\omega_t\mid\omega_{<t})$ over sequences $\omega : \mathrm{Fin}\,n\to\mathrm{Fin}\,K$ , and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.
Argmax. $\hat y_t$ uses any argmax selector; all tie-breaking rules are covered.
Norms. $\|x_t\| = 1$ is the Euclidean condition $\sum_j x_{t,j}^2 = 1$ ; $\|U\|$ is the Frobenius norm written out explicitly.
Infima and maxima. Each " $\inf_U$ " and " $\max_k$ " of the book is stated as "for every $U$ " or "for every $k$ ", which is equivalent.
Explicit constants. Every bound is the one printed or, for the corrected items, the one the proof yields. No $O(\cdot)$ appears.
Corrected misprints. Theorem 4.7 prints the examples in $\mathbb R^d\times\{-1,+1\}$ ; labels are in $\{1,\dots,K\}$ . Theorem 4.2 prints $\sqrt{2nN\ln K}$ and $2\sqrt{nN\ln K}$ ; the proof gives $\sqrt{2nK\ln N}$ and $2\sqrt{nK\ln N}$ . Theorem 4.3 prints $\eta = \sqrt{2\ln K/(nK)}$ ; (4.7) follows from the proof with $\eta = \sqrt{2\varepsilon\ln K/n}$ .
Parameter range. At $n = 8K$ the Banditron's $\gamma$ equals $1/2$ , outside the box's open interval $(0,1/2)$ . The proof uses only $\gamma\le 1/2$ , so $n = 8K$ is included.
Ruling out trivial forms. Theorem 4.1 is stated for the explicit S-Exp3 forecaster, not as an existence claim, so no forecaster tuned to the losses can witness it. The losses and the advice are allowed to adapt, so a proof for oblivious sequences does not suffice.
Left out. Theorem 4.4 (Exp4 with mixing) is proved in the book only by reference. The argument that reference suggests yields $\tfrac32\gamma n + K\ln N/\gamma$ , not the printed $\gamma n/2 + K\ln N/\gamma$ . Theorem 4.5 is stated with $O(\cdot)$ , Theorem 4.6 "for some constant $c$ ", and Eq. (4.8) is left to the reader.

Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721 ; https://doi.org/10.1561/2200000024
S. M. Kakade, S. Shalev-Shwartz, A. Tewari, Efficient Bandit Algorithms for Online Multiclass Prediction, ICML 2008. https://doi.org/10.1145/1390156.1390212
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
O.-A. Maillard, R. Munos, Adaptive Bandits: Towards the Best History-Dependent Strategy, AISTATS 2011. https://proceedings.mlr.press/v15/maillard11a.html

11 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ .

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$ , whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$ ; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ .

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$ . For a fixed procedure $R$ started at $X_0 = i$ , let $W'_t$ and $W''_t$ be the expected costs at time $t$ . The ratio criterion is

\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.

For a single cost set $w$ with expected costs $W_t$ , the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$ .

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$ .

Steps of the proof (milestones)

Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$ .
For any procedure $R$ , $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$ .
Under Assumption A, for $R^* \in C''$ , $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$ .
For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$ , with $\pi$ the stationary distribution of $(p_{sj})$ .

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$ , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$ , $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$ ; $Q_R(i)$ with Derman's normalization ( $T+1$ terms divided by $T$ ); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$ ; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$ ; and membership of a procedure in $C'$ with probabilities $D$ . All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$ , which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$ ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$ .

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6):938–948, 1963. https://doi.org/10.1287/opre.11.6.938
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

7 thms2 active usersReviewed

Operations Research

Missions

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance I: Quadratic Potential Functions Bound Mean Response Times in Open NetworksResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Conditional Logit Analysis of Qualitative Choice Behavior 5: The Maximum Likelihood Estimator Exists with Probability Tending to One and Is Consistent and Asymptotically NormalResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Secretary Problems: Weights and Discounts 1: An (8+3e)-Competitive Algorithm for the Weighted Secretary ProblemResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Discrete Dynamic Programming 2: A Stationary Policy Is Nearly Optimal as the Discount Factor Tends to 1 Exactly When It Maximizes x(g) and, Among Those, y(g)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(e)

Milestones and intermediate results

Significance

Difficulty

Formalization scope

Selected references

Consensus of Subjective Probabilities: The Pari-Mutuel Method: Equilibrium Track Probabilities Exist and Are UniqueResearch Paper

Motivation

Setting

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 2: Logarithmic Regret for N ArmsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Online Set Cover Problem 2: Given α ≥ c(C_OPT), the Weighted Potential-Function Algorithm Never Fails and Pays at Most (6+o(1)) α log m log nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4

Milestones

Significance

Difficulty

Formalization scope

Selected references