The OR Formalization Drive

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

Online Network Revenue Management Using Thompson Sampling: Bayesian Regret of TS-fixedResearch Paper

Motivation

A retailer who sells several products from shared, non-replenishable inventory over a finite season must set prices without knowing how demand responds to them. Every price posted is both a sale and an experiment. This is the network revenue management problem with demand learning, and it sits between two literatures: dynamic pricing with inventory, where demand is known and the fluid linear program of Gallego and van Ryzin (1997) is the standard benchmark, and multi-armed bandits, where learning is the whole problem but there are no resource constraints.

Ferreira, Simchi-Levi and Wang (Oper. Res. 2018) combine Thompson sampling with a linear-programming step: sample a demand model from the posterior, solve the fluid LP for that model, and randomize prices according to its solution. The same paper extends the scheme to continuous price sets, contextual pricing and bandits with knapsacks.

Timeline of the relevant results:

1997: Gallego and van Ryzin introduce the fluid LP upper bound for network revenue management with known demand.
2012: Besbes and Zeevi give a non-Bayesian network pricing algorithm with worst-case regret $O(K^{5/3}T^{2/3}\sqrt{\log T})$ .
2013: Badanidiyuru, Kleinberg and Slivkins (bandits with knapsacks) give worst-case regret $O(\sqrt{KT\log T})$ .
2013–2014: Bubeck and Liu and Russo and Van Roy give prior-free Bayesian regret bounds for Thompson sampling in unconstrained bandits.
2018: Ferreira, Simchi-Levi and Wang prove the $O(\sqrt{TK\log K})$ Bayesian regret bound for TS-fixed (Theorem 1), the target of this mission.

Setting

There are $N$ products and $M$ resources. One unit of product $i$ consumes $a_{ij}\ge0$ units of resource $j$ , and resource $j$ starts with inventory $I_j\ge0$ that is never replenished. The season has $T$ periods. In each period the retailer posts one of $K$ price vectors $p_k=(p_{1k},\dots,p_{Nk})$ or a shut-off price $p_\infty$ under which demand is zero.

Given the posted price $p_k$ , the demand vector $D(t)\in\mathbb R^N_+$ has law $F(\cdot\,;p_k,\theta)$ , where $\theta\in\Theta$ is unknown and drawn from a known, arbitrary prior $\mu_0$ . Demand is independent of the past given the posted price and $\theta$ , and is bounded: $D_i(t)\in[0,\bar d_i]$ . Write $d_{ik}(\rho)$ for the mean demand of product $i$ under $p_k$ and parameter $\rho$ , and $d=d(\theta)$ .

When inventory covers all demand, all demand is sold. Otherwise the satisfied demand $\tilde D(t)$ satisfies $0\le\tilde D_i(t)\le D_i(t)$ , leaves every inventory nonnegative, and leaves at least one resource at zero; no other rule is imposed. Revenue is $\mathrm{Rev}(T)=\sum_t\sum_i\tilde D_i(t)P_i(t)$ .

For a mean-demand matrix $d$ and capacities $c_j=I_j/T$ , the linear program $\mathrm{LP}(d)$ is

\max_{x\ge0}\ \sum_{k=1}^K\Bigl(\sum_{i=1}^N p_{ik}d_{ik}\Bigr)x_k\quad\text{s.t.}\quad\sum_{k=1}^K\Bigl(\sum_{i=1}^N a_{ij}d_{ik}\Bigr)x_k\le c_j\ \ \forall j,\qquad\sum_{k=1}^K x_k\le1,

with optimal value $\mathrm{OPT}(d)$ .

TS-fixed (Algorithm 1): in each period, sample $\theta(t)$ from the posterior of $\theta$ given the history of posted prices and observed demands; let $x(t)$ be an optimal solution of $\mathrm{LP}(d(\theta(t)))$ ; post $p_k$ with probability $x_k(t)$ and $p_\infty$ with the remaining probability; observe demand and update the posterior.

Finally $p_{\max}=\max_k\sum_ip_{ik}\bar d_i$ and $p^j_{\max}=\max_{i:a_{ij}\neq0,\,k}p_{ik}/a_{ij}$ .

Formalization targets

Goal: Theorem 1 against the LP benchmark

For $K\ge2$ , $T\ge1$ , every prior, every bounded demand family, every admissible fulfilment rule and every run of TS-fixed,

\mathbb E\bigl[\mathrm{OPT}(d)\bigr]\cdot T-\mathbb E\bigl[\mathrm{Rev}(T)\bigr]\ \le\ \Bigl(18\,p_{\max}+37\sum_{i=1}^N\sum_{j=1}^M p^j_{\max}a_{ij}\bar d_i\Bigr)\sqrt{TK\log K}.

The paper prints this bound for $\mathrm{BayesRegret}(T)=\mathbb E[\mathrm{Rev}^*(T)]-\mathbb E[\mathrm{Rev}(T)]$ , where $\mathrm{Rev}^*$ is the revenue of the optimal policy that knows $\theta$ ; see Formalization scope for why the LP benchmark is stated instead.

Milestones

The article states Theorem 1 and says that its proof is in the online appendix (Supplemental Material at the DOI). The article itself contains no numbered lemma. The milestone list is therefore empty; the appendix's lemmas will be added as milestones once the appendix is held.

Significance

The bound is prior-free and has explicit constants that depend only on prices, consumption rates and demand bounds. Its dependence on $T$ matches the $\Omega(\sqrt{KT})$ lower bound for Bayesian regret in unconstrained bandits with rewards in $[0,1]$ , a special case of the model with no inventory constraints (Bubeck and Cesa-Bianchi 2012, Theorem 3.5). It shows that the posterior-sampling principle survives the addition of resource constraints, lost sales and randomized LP-based pricing, and it is the template for the paper's later results (TS-update, contextual pricing, bandits with knapsacks).

The theorem is proved on paper but, as far as a platform search shows, not formalized anywhere. The platform has a formal proof of the unconstrained Bayesian Thompson sampling bound $\sqrt{kn\log k/2}$ (BanditAlgorithm.thompson_sampling_bayesian_regret, Lattimore–Szepesvári Theorem 36.5) and an open single-product deterministic upper bound in revenue management (RevenueManagement.deterministic_upper_bound). Neither has inventory, an LP subroutine, or lost sales. A formal proof here would supply the first machine-checked analysis of Thompson sampling under resource constraints and would check the paper's constants.

Difficulty

In an unconstrained bandit, Thompson sampling's regret reduces to a sum of per-period gaps between an upper confidence bound and the sampled reward, because the sampled optimal arm and the true optimal arm are identically distributed given the history. Here the action is a randomized mixture $x(t)$ from an LP, the reward is not additive in the prices chosen, and revenue is lost when inventory runs out. Two quantities must be controlled: the revenue the algorithm would collect if all demand could be served, and the revenue lost to stock-outs. The second depends on the random time at which each resource is exhausted under a pricing rule that was optimized for a sampled, not the true, demand, and on an arbitrary fulfilment rule once some resource is empty. Standard bandit arguments do not bound such lost sales, which are a nonlinear function of the whole trajectory.

Formalization scope

Lean representation. Products, resources and price vectors are indexed by Fin N, Fin M, Fin K; the posted price is an Option (Fin K) with none the shut-off price. Periods are 0-based ( $t=0,\dots,T-1$ stands for the paper's $1,\dots,T$ ). $\Theta$ is a standard Borel space with a probability measure $\mu_0$ ; demand is a Markov kernel $F$ from $\Theta\times$ Fin K to $\mathbb R^N$ , bounded in $[0,\bar d_i]$ for every parameter. A run of TS-fixed is a family of random variables on a probability space satisfying, almost surely and via conditional expectations: $\theta\sim\mu_0$ ; the posterior-sampling property of $\theta(t)$ given everything before period $t$ ; the price draw with probabilities $x(\theta(t))$ for a measurable optimal LP selection $x$ ; the demand law given the past, $\theta(t)$ and the posted price; and fulfilment rules (a)/(b). The logarithm is natural. Prices, consumption and inventory are nonnegative (implicit in the paper). $\mathrm{OPT}(d)$ is a supremum over a nonempty bounded feasible set, so it has no junk value.

Corrections to the printed statement.

$K\ge2$ is added. At $K=1$ the printed right-hand side is $0$ , yet on a one-price instance with Bernoulli $(0.8)$ demand, $I=T/2$ and a point-mass prior, TS-fixed loses about $0.2p\sqrt T$ in expectation.
The LP benchmark replaces $\mathbb E[\mathrm{Rev}^*(T)]$ . Section 3.1.1 bounds $\mathbb E[\mathrm{Rev}^*(T)\mid d]$ by $\mathrm{OPT}(d)\cdot T$ , citing Gallego–van Ryzin. Under the paper's fulfilment rule this fails when products use disjoint resources: with two products, $I=(T,1)$ , $p_1=(1,0)$ , $p_2=(1/2,0)$ and deterministic demand $(1,1)$ , the known- $\theta$ policy earns at least $T$ while $\mathrm{OPT}(d)\cdot T=1$ . The paper states that its proof bounds the gap to "the LP benchmark defined in Section 3.1.1" (p. 1594), and the last display of Section 3.1.1 bounds $\mathrm{BayesRegret}(T)$ by exactly $\mathbb E[\mathrm{OPT}(d)]\cdot T-\mathbb E[\mathrm{Rev}(T)]$ . Wherever the Gallego–van Ryzin bound holds, the corrected goal implies the printed one.

Ruled out. A bound for the "ideal" revenue $\sum_iD_i(t)P_i(t)$ instead of the satisfied revenue, or for an arbitrary policy whose prices are merely close to the LP solution, is not Theorem 1; the goal carries the full TS-fixed run and the lost-sales accounting.

Infrastructure needed. Posterior-sampling identities for general (standard Borel) priors, a Hoeffding/Azuma-type concentration for bounded demand along the price-selection process, LP sensitivity with respect to the mean-demand matrix, and a pathwise bound on lost sales under an arbitrary fulfilment rule. The LP and fluid-benchmark definitions are reusable for later missions on TS-update (Theorem 2), contextual pricing (Theorem 4) and bandits with knapsacks (Theorem 5). Contributions welcome: proofs of the goal, and formal statements of the online appendix's lemmas.

Selected references

K. J. Ferreira, D. Simchi-Levi, H. Wang, Online Network Revenue Management Using Thompson Sampling, Operations Research 66(6):1586–1602, 2018. https://doi.org/10.1287/opre.2018.1755
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
O. Besbes, A. Zeevi, Blind Network Revenue Management, Operations Research 60(6):1537–1550, 2012. https://doi.org/10.1287/opre.1120.1057
A. Badanidiyuru, R. Kleinberg, A. Slivkins, Bandits with Knapsacks, FOCS 2013. https://arxiv.org/abs/1305.2545
S. Bubeck, C.-Y. Liu, Prior-free and Prior-dependent Regret Bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1311.0466
D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650
S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 36. https://doi.org/10.1017/9781108571401

3 thms1 active userReviewed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

Motivation

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

1967, Klein: the cycle-canceling algorithm, without an iteration bound.
1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ( $(v,w)\in E$ iff $(w,v)\in E$ , so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$ , the cost being antisymmetric: $c(v,w)=-c(w,v)$ .

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$ . Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$ , and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$ ; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$ . Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$ , the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$ , and ε-optimality: for $\varepsilon\ge0$ , $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$ , and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ( $\varepsilon(f)=-\mu(f)$ for nonoptimal $f$ , where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$ ), Lemma 3.6 ( $m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$ ), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$ , an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$ . Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$ :

Theorem 3.9: the paper prints $O(nm^2\log n)$ ; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$ . Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Optimizing Strategic Safety Stock Placement in Supply Chains: Binding Base Stocks Are Optimal in a Serial System without Guaranteed Internal ServiceResearch Paper

Motivation

Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.

The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.

Setting

A serial supply chain has $N$ stages. Stage $1$ is the demand node and stage $i$ supplies stage $i-1$ for $i = 2, \dots, N$ . Time is discrete, with periods $t \in \mathbb{Z}$ . Stage $i$ has a deterministic lead time $T_i \in \mathbb{N}$ and a base stock $B_i \in \mathbb{R}$ . It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.

The end-item demand in period $t$ is $d(t)$ . The window demand is $d(a, b] = d(a+1) + \dots + d(b)$ , which is $0$ when $a \ge b$ . The demand bound $D : \mathbb{N} \to \mathbb{R}$ gives $D(\tau)$ , the maximum possible end-item demand over $\tau$ periods, with $D(0) = 0$ .

The backlog $Q_i(t)$ is the amount the customer of stage $i$ has ordered but not yet received. It satisfies the recursion (A1):

Q_i(t) = \bigl[d(t - T_i, t] + Q_{i+1}(t - T_i) - B_i\bigr]^+, \qquad Q_{N+1} \equiv 0 .

Unrolling it gives the closed max-form (A2). The external customer receives 100% service when $Q_1(t) = 0$ for all $t$ . When demand never exceeds its bound, this is ensured by the service constraints

B_1 + \dots + B_i \ge D(T_1 + \dots + T_i), \qquad i = 1, \dots, N. \tag{A3}

Let $h_i$ be the holding cost at stage $i$ and $e_i = h_i - h_{i+1}$ the echelon holding cost. After constant terms are dropped, the expected holding cost gives program $\mathbf P^*$ :

\min_B\ \sum_{i=1}^N h_i B_i - \sum_{i=2}^N e_{i-1} E[Q_i] \quad\text{s.t. (A3) and } B_i \ge 0 .

Demand is random, and $E[Q_i]$ is the expected backlog at stage $i$ in a period $t$ .

Formalization targets

Goal: the Result, Eq. (A6)

If the echelon holding costs are nonnegative and $D$ is nondecreasing, then an optimal solution of $\mathbf P^*$ is

B_1 = D(T_1), \qquad B_i = D(T_1 + \dots + T_i) - D(T_1 + \dots + T_{i-1}), \quad i = 2, \dots, N. \tag{A6}

Formally, (A6) is feasible, and for every period $t$ its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible $B$ . The weaker claim that "some optimal solution binds all of (A3)" would not be enough.

Milestones

Eq. (A2). The closed max-form of $Q_i(t)$ , derived from the recursion (A1).
Eq. (A3). Under the demand bound $d(a, a+s] \le D(s)$ , the constraints (A3) force $Q_1 \equiv 0$ (sufficiency).
(A6) is feasible and is the unique binding solution of (A3).
Backlog bounds under a transfer. Moving $\Delta \ge 0$ units of base stock from stage $k$ to stage $k+1$ leaves $E[Q_i]$ unchanged for $i > k+1$ and raises it by at most $\Delta$ for $i \le k$ . It lowers $E[Q_{k+1}]$ by at most $\Delta$ .
Eqs. (A7)–(A8). For $k < N$ , the transfer that makes the $k$ -th constraint binding keeps the vector feasible and does not raise the objective.
The case $k = N$ . Lowering $B_N$ until the $N$ -th constraint binds does not raise the objective.

Significance

The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.

The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.

Difficulty

The objective is not linear in $B$ . Each $E[Q_i]$ is a convex, nonsmooth function of $B_i, \dots, B_N$ through the maximum in (A2), and the objective subtracts these terms, so $\mathbf P^*$ minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on $\mathbf P^*$ , and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.

Formalization scope

Stages are natural numbers read on the range $\{1, \dots, N\}$ . Lead times are natural numbers cast to $\mathbb{Z}$ . Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function $\mathbb{N} \to \mathbb{R}$ , and only indices $1, \dots, N$ are read. The backlog is defined by the recursion (A1), computed in $N + 1 - i$ steps, with $Q_i \equiv 0$ for $i > N$ . The closed form (A2) is a theorem. Randomness is a probability space $(\Omega, \mu)$ with a demand path $d(\omega, \cdot)$ whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.

The page's informal words are read as follows:

"The echelon holding costs are nonnegative" means $h_i - h_{i+1} \ge 0$ for $1 \le i < N$ , and $h_N \ge 0$ , i.e. $e_N \ge 0$ with $h_{N+1} := 0$ . The case $k = N$ of the proof uses $h_N \ge 0$ . Without it the Result is false ( $N = 1$ , $h_1 < 0$ ).
$D(0) = 0$ is the paper's convention (§2, p. 70) and is added as a hypothesis. Without it (A6) can be infeasible ( $D \equiv -1$ is nondecreasing).
" $D(\,)$ is a nondecreasing function" means Monotone D on $\mathbb{N}$ .
"An optimal solution to $\mathbf P^*$ " means feasible, with objective at most that of every feasible vector.
" $E[Q_i]$ " means the expectation of $Q_i(t)$ at a fixed period $t$ . Every statement holds for all $t$ , and stationarity is not assumed. The paper writes $E[Q_i]$ without $t$ because its demand is stationary, and this reading is at least as strong.
The demand bound $d(a, a+s] \le D(s)$ appears only in milestone 2. The Result does not use it, so it is not a hypothesis of the goal.
Eq. (A3) is formalized in the sufficiency direction only. The page's necessity remark ("as we assume that the demand bounds can be realized") is not stated.

A non-integrable backlog would make its Bochner integral $0$ and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.

Useful contributions include a proof of (A2) by downward induction on stages, the integrability of $Q_i(t)$ , the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.

Selected references

S. C. Graves and S. P. Willems, Optimizing Strategic Safety Stock Placement in Supply Chains, Manufacturing & Service Operations Management 2(1):68–83, 2000. https://doi.org/10.1287/msom.2.1.68.23267
K. F. Simpson, In-Process Inventories, Operations Research 6(6):863–873, 1958. https://doi.org/10.1287/opre.6.6.863
K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed., 2019. https://doi.org/10.1002/9781119584445

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.

The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.

Timeline:

1961, Vickrey: second-price auctions make truthful bidding a dominant strategy for a single object.
1971, Clarke: pivot payments for public-good decisions with deterministic valuations.
1972, Marschak–Radner: the economic theory of teams, with information and decision structures but a common payoff.
1973, Groves: compensation $C_i^{II}$ based on the head's conditional expectation of the other units' payoffs; Theorem 1 proves optimality in a conglomerate with independent component states and one round of communication.
1977, Green–Laffont: in the complete-information setting, Groves-type payments are the only ones that make truth-telling dominant (Econometrica 45(2)).
1979, d'Aspremont–Gérard-Varet: Bayesian incentive-compatible mechanisms with expected externality payments (J. Public Econ. 11(1)).

The conglomerate model

The organization consists of a head (component $0$ ) and finitely many subunits $i = 1, \dots, n$ . Each component $k$ has its own random component state $s_k \in S_k$ , and the components are independent: the state of the environment $s = (s_0, s_1, \dots, s_n)$ is distributed according to the product law $P(s) = P_0(s_0) \prod_{i} P_i(s_i)$ (Condition S.2).

Every member plays a strategy $\beta_k = (\zeta_k, \gamma_k, \delta_k)$ made of an observation strategy $\zeta_k$ on its own state, a message strategy $\gamma_k$ and a decision strategy $\delta_k$ (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes $\zeta_0(s_0)$ and sends $\gamma_0^i(\zeta_0(s_0))$ to subunit $i$ ; the subunit, with information $y_i(s) = [\zeta_i(s_i), \gamma_0^i(\zeta_0(s_0))]$ , sends back $\gamma_i(y_i(s))$ ; the head's information is $y_0(s) = [\zeta_0(s_0), \{\gamma_i(y_i(s))\}_{i}]$ (3.1). Decisions are $\delta_i(y_i(s))$ and $\delta_0(y_0(s))$ .

The organization payoff is a sum of components (Condition S.4),

\omega_0(\beta, s) = \sum_{i=1}^n v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + v_0[\delta_0(y_0(s)), s_0],

and $\bar\omega_0(\beta) = E[\omega_0(\beta, s)]$ . Each $v_i$ accrues directly to subunit $i$ (Condition S.5). Strategy sets $B_0, B_1, \dots, B_n$ are given; $\beta/\beta_i$ denotes $\beta$ with subunit $i$ 's strategy replaced by $\beta_i$ . Two strategies $\beta_i', \beta_i''$ are equivalent if $\bar\omega_0(\beta/\beta_i') = \bar\omega_0(\beta/\beta_i'')$ for every $\beta \in B$ .

Assumption A requires a $\beta^* \in B$ maximizing $\bar\omega_0$ over $B$ such that, for each subunit, $\bar\omega_0(\beta^*) > \bar\omega_0(\beta^*/\beta_i)$ whenever $\beta_i \in B_i$ is not equivalent to $\beta_i^*$ .

An incentive structure $W = \{\omega_i\}$ pays subunit $i$ the amount $\omega_i(\beta, s)$ . The class $\mathscr{J}$ (3.2) consists of those of the form $\omega_i = v_i[\dots] + C_i(y_0(s))$ : own payoff plus a compensation computed from the head's information only. $W$ is optimal (2.6) if $\beta_i^*$ maximizes $\bar\omega_i(\beta^*/\beta_i)$ over $B_i$ , uniquely up to equivalence.

Formalization targets

Goal: Theorem 1 (p. 625)

With $C_i^{II}(y_0) = \sum_{j \ne i} E\big[v_j[\delta_j^*(y_j^*(s)), \delta_0^*(y_0^*(s)); s_j] \,\big|\, y_0^*(s) = y_0\big] - A_i$ , the sum running over all components $j \in \{0, \dots, n\}$ other than $i$ and the expectation taken under $\beta^*$ (3.3), the structure $\omega_i^{II} = v_i[\dots] + C_i^{II}(y_0(s))$ lies in $\mathscr{J}$ and satisfies, for every subunit $i$ and every $\beta_i \in B_i$ ,

\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*), \qquad \text{with strict inequality if } \beta_i \not\equiv \beta_i^*.

It holds for every $\beta^*$ satisfying Assumption A, all strategy sets and all constants $A_i$ .

Milestones

The Appendix Lemma: the sets of states consistent with the head's information under $\beta^*/\beta_i$ and under $\beta^*$ have the same projections onto every component other than $i$ .
The right-hand side of (A.2): the head's conditional expectation factorizes over the independent components.
(A.2) for a subunit $j \ne i$ , and 4. (A.2) for the head's component $j = 0$ : the expected payoff of component $j$ under $\beta^*/\beta_i$ equals the expected value of its conditional expectation.
(A.1): $\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)$ for all $\beta_i \in B_i$ .

Significance

Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.

Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.

Difficulty

The tempting argument conditions on the head's information $y_0^*(s) = y_0$ under $\beta^*$ and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that $\gamma_i^*$ never sends: the conditioning event then has probability zero under $\beta^*$ , and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under $\beta^*$ in every coordinate the deviation touches, while the compensation is computed as if $\beta^*$ were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.

Formalization scope

Every component state space $S_k$ is a finite type with weights that are nonnegative and sum to one; the joint law is the product of these weights and expectations are finite sums. The paper allows general probability spaces; the finite case covers the whole argument and gives conditional expectations at a point an elementary meaning.
Subunits form a finite index type; the head is a separate component with its own observation, message and decision types. Observation, message and decision spaces are fixed types per component.
Information (3.1) follows the single exchange of messages the paper describes in §4.A (p. 627): the head's message to subunit $i$ is a function of the head's observation. As printed, (3.1) is circular; this protocol is the paper's own resolution.
$C_i^{II}$ is used in factorized form: the head's term conditions only the head's state on the head's observation, and subunit $j$ 's term conditions only $s_j$ on the message $j$ sent. A separate milestone states that this equals the literal conditional expectation of (3.3) whenever the conditioning event has positive probability. The literal elementary quotient takes the value $0$ on null events, and with it Theorem 1 is false (one subunit that can send an unused message suffices); the factorized form is what the Appendix computes. The sum in (3.3) includes the head's component $v_0$ .
Equivalence of strategies is footnote 5's, over all $\beta \in B$ ; optimality includes the strict inequality for non-equivalent deviations. A formalization that replaces equivalence by equality of strategies, fixes $B_i = \{\beta_i^*\}$ , drops the strict inequality, or assumes (A.1) as a hypothesis is not this theorem.
The Lemma carries the added hypothesis that the set $B(s)$ is nonempty; the paper's proof presumes it and the statement is false without it.

Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.

Selected references

T. Groves, Incentives in Teams, Econometrica 41(4):617–631, 1973. https://doi.org/10.2307/1914085
J. Marschak and R. Radner, Economic Theory of Teams, Yale University Press, 1972.
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1):8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11:17–33, 1971. https://doi.org/10.1007/BF01726210
J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45(2):427–438, 1977. https://doi.org/10.2307/1911219
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and Incomplete Information, Journal of Public Economics 11(1):25–45, 1979. https://doi.org/10.1016/0047-2727(79)90043-4

7 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 1: Logarithmic Regret of Online Gradient DescentResearch Paper

Motivation

Online convex optimization is a repeated game between a learner and an adversary. In each round $t=1,\dots,T$ the learner commits to a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$ ; only then is a convex cost function $f_t$ revealed, and the learner pays $f_t(x_t)$ . The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.

Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order $1/\sqrt t$ has regret $O(GD\sqrt T)$ for any convex costs with gradients bounded by $G$ on a set of diameter $D$ , and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes $1/(Ht)$ has regret only logarithmic in $T$ once every cost function is $H$ -strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.

Setting

Fix $n\in\mathbb N$ and a nonempty, closed, bounded, convex set $\mathcal P\subseteq\mathbb R^n$ , with the Euclidean norm $\|\cdot\|_2$ (§2.1, p. 171).

Cost functions. A sequence $f_1,f_2,\dots:\mathbb R^n\to\mathbb R$ . Write $\nabla f_t(x)$ for the gradient and $\nabla^2 f_t(x)$ for the Hessian.
Gradient bound. A number $G$ with $\|\nabla f_t(x)\|_2\le G$ for all $x\in\mathcal P$ and all rounds $t$ (p. 172).
$H$ -strong convexity (p. 172). For $H>0$ , $f$ is $H$ -strongly convex on $\mathcal P$ when it is twice differentiable and $\nabla^2 f(x)\succeq H I_n$ for every $x\in\mathcal P$ , i.e. $v^\top\nabla^2 f(x)v\ge H\|v\|_2^2$ for all $v$ .
Euclidean projection. $\Pi_{\mathcal P}(y)$ is the point of $\mathcal P$ nearest to $y$ , $\Pi_{\mathcal P}(y)=\arg\min_{x\in\mathcal P}\|x-y\|_2$ (IsProj P y z).
Online Gradient Descent (Fig. 1, p. 174), with step sizes $\eta_1,\eta_2,\dots$ : $x_1\in\mathcal P$ is arbitrary, and in iteration $t>1$

x_t=\Pi_{\mathcal P}\bigl(x_{t-1}-\eta_t\nabla f_{t-1}(x_{t-1})\bigr)

(IsOGDRun P η f x).

Regret (p. 171): $\mathrm{Regret}_T=\sum_{t=1}^T f_t(x_t)-\min_{x\in\mathcal P}\sum_{t=1}^T f_t(x)$ , and $\mathrm{Regret}_T(\mathrm{OGD})$ is its supremum over all cost sequences.

Formalization targets

Goal: Theorem 1 (p. 175)

For $H>0$ , cost functions that are $H$ -strongly convex on $\mathcal P$ with gradients bounded by $G$ on $\mathcal P$ , and any run of Online Gradient Descent whose step after round $t$ is $\eta_{t+1}=1/(Ht)$ , for every $T\ge1$ and every $u\in\mathcal P$ :

\sum_{t=1}^{T}\bigl(f_t(x_t)-f_t(u)\bigr)\ \le\ \frac{G^2}{2H}\,\bigl(1+\log T\bigr).

This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at $T=1$ the bound reads $G^2/(2H)$ .

Milestones

Eq. (1), the strong-convexity inequality: for $x,y\in\mathcal P$ , $2(f(x)-f(y))\le 2\nabla f(x)^\top(x-y)-H\|y-x\|_2^2$ .
Lemma 8 with $A=I_n$ : for a convex $\mathcal P$ , $z=\Pi_{\mathcal P}(y)$ and $a\in\mathcal P$ , $\|y-a\|_2^2\ge\|z-a\|_2^2$ . This is already on the platform, proved, as UnderstandingML.projection_lemma, and is reused as a reference item.
Eq. (2), the one-step inequality: for $z=\Pi_{\mathcal P}(x-\eta g)$ , $\eta>0$ , $\|g\|_2\le G$ and $u\in\mathcal P$ , $2g^\top(x-u)\le(\|x-u\|_2^2-\|z-u\|_2^2)/\eta+\eta G^2$ .

The last step of the argument is the harmonic-sum bound $\sum_{t=1}^T 1/t\le 1+\log T$ , which Mathlib already provides (harmonic_le_one_add_log).

Significance

The result. Theorem 1 separates two regimes of online convex optimization: $\Theta(\sqrt T)$ regret for general convex costs and $O(\log T)$ for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the $O(\log T/T)$ rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain $O(n\log T)$ regret.

Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.

Difficulty

The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round $t$ must be $1/(Ht)$ . Reading Fig. 1 literally with $\eta_t=1/(Ht)$ makes the step after round $t$ equal to $1/(H(t+1))$ , and the sum then leaves an uncancelled term $\frac H2\|x_1-x^*\|_2^2$ that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of $\mathcal P$ ; convexity of $\mathcal P$ keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.

Formalization scope

Points are EuclideanSpace ℝ (Fin n), so $\|\cdot\|$ is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of $\mathbb R^n$ , as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to $(v,v)$ . Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of $\mathcal P$ ), which is unique for nonempty closed convex $\mathcal P$ .

Choices and corrections relative to the printed text:

Step-size index. Theorem 1 prints "step sizes $\eta_t=\frac1{Ht}$ ", while its proof sets $\eta_{t+1}=1/(Ht)$ for the step after round $t$ . The goal uses the proof's indexing, as a hypothesis η (t + 1) = 1 / (H * t) for $t\ge1$ on the step sizes of Fig. 1.
Eq. (2). The paper prints " $5\nabla_t^\top(x_t-x^*)$ "; the $5$ is a typo for $2$ , and the milestone states $2$ . The verbatim milestone text keeps the printed $5$ .
Regret. Regret is stated against every comparator $u\in\mathcal P$ ; the minimum over the compact set $\mathcal P$ is attained, so this is the paper's statement. The expectation in the paper's regret is vacuous for this deterministic algorithm, and the supremum over cost sequences is the universal quantifier over $f$ .
Hypotheses. Strong convexity and the gradient bound are required for the rounds $1,\dots,T$ only. Convexity of each $f_t$ , a standing assumption of §2.2, follows from $H$ -strong convexity on the convex set $\mathcal P$ and is not added. No diameter bound enters Theorem 1.

A regret bound written with a real ⨅/sInf over $\mathcal P$ , or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in $\mathcal P$ and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, $f_t(x)=\frac H2\|x\|_2^2$ with $G=H$ meets all of them.

Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite $A$ (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.

Selected references

E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022 (Theorem 3.3). https://arxiv.org/abs/1909.05207
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014 (Lemma 14.9, the projection lemma). https://doi.org/10.1017/CBO9781107298019

5 thms5 active usersReviewed

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 2: Logarithmic Regret of the Online Newton StepResearch Paper

Motivation

Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round $t=1,\dots,T$ a player picks a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$ , and only then learns a convex cost function $f_t$ and pays $f_t(x_t)$ . Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret $O(\sqrt T)$ for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.

Many costs met in practice have more curvature than bare convexity. The log-loss $f(x)=-\log(x^\top a)$ of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in $T$ for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.

Timeline:

2003 — Zinkevich: $O(\sqrt T)$ regret for general convex costs by online gradient descent.
2006–2007 — Hazan, Agarwal, Kale (COLT 2006; Mach Learn 2007): $O(\log T)$ regret for strongly convex costs by gradient descent, and $O(n\log T)$ regret for exp-concave costs by ONS, Follow the Approximate Leader, and exponentially weighted online optimization.
2016 — Hazan, Introduction to Online Convex Optimization (Found. Trends Optim., arXiv:1909.05207): textbook treatment of ONS with modified parameters.

Setting

The decision set $\mathcal P\subseteq\mathbb R^n$ is nonempty, closed, bounded and convex, and $D$ bounds its diameter: $\|x-y\|\le D$ for all $x,y\in\mathcal P$ , with the Euclidean norm. The costs $f_1,f_2,\dots$ are real functions, differentiable at every point of $\mathcal P$ , with gradient bound $\|\nabla f_t(x)\|\le G$ on $\mathcal P$ . A cost is $\alpha$ -exp-concave ( $\alpha>0$ ) if $x\mapsto\exp(-\alpha f_t(x))$ is concave on $\mathcal P$ .

For a matrix $A$ , the generalized projection $\Pi^A_{\mathcal P}(y)$ is a point of $\mathcal P$ minimising $(y-x)^\top A(y-x)$ over $x\in\mathcal P$ .

The Online Newton Step fixes

\beta=\tfrac12\min\Big\{\frac1{4GD},\alpha\Big\},\qquad \varepsilon=\frac1{\beta^2D^2},

writes $\nabla_t=\nabla f_t(x_t)$ and $A_t=\sum_{i=1}^t\nabla_i\nabla_i^\top+\varepsilon I_n$ , plays an arbitrary $x_1\in\mathcal P$ , and then

x_{t+1}=\Pi^{A_t}_{\mathcal P}\Big(x_t-\frac1\beta A_t^{-1}\nabla_t\Big).

The regret after $T$ rounds against a comparator $u\in\mathcal P$ is $\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)$ ; the paper's regret is its maximum over $u\in\mathcal P$ .

In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.

Formalization targets

Goal: Theorem 2 with $n\log T\ge4$

For every run of ONS, every horizon $T$ with $n\log T\ge 4$ , and every $u\in\mathcal P$ ,

\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le 5\Big(\frac1\alpha+GD\Big)\,n\log T.

The added condition $n\log T\ge4$ is what makes the printed constant correct (see Formalization scope).

Milestones

Lemma 3 (p. 177): for $0<\beta\le\frac12\min\{1/(4GD),\alpha\}$ and $x,y\in\mathcal P$ ,

f(x)\ge f(y)+\nabla f(y)^\top(x-y)+\tfrac\beta2\big(\nabla f(y)^\top(x-y)\big)^2 .

Lemma 8 (p. 188): for convex $\mathcal P$ , $A\succeq0$ , $z=\Pi^A_{\mathcal P}(y)$ and $a\in\mathcal P$ : $(y-a)^\top A(y-a)\ge(z-a)^\top A(z-a)$ .
The display on p. 178: for every run of ONS and $u\in\mathcal P$ ,

\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le\frac1{2\beta}\sum_{t=1}^T\nabla_t^\top A_t^{-1}\nabla_t+\frac1{2\beta}.

Lemma 12 (p. 191): for $A\succeq B\succ0$ , $A^{-1}\bullet(A-B)\le\log(|A|/|B|)$ .
Lemma 11 (p. 190): if $\|u_t\|\le r$ , $\varepsilon>0$ and $V_t=\sum_{\tau\le t}u_\tau u_\tau^\top+\varepsilon I_n$ , then $\sum_{t=1}^Tu_t^\top V_t^{-1}u_t\le n\log(r^2T/\varepsilon+1)$ .

Significance

Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in $T$ , at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.

The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with $V_{t-1}$ and a $\min(1,\cdot)$ , a different statement) and the Euclidean case $A=I$ of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with $\gamma=\frac12\min\{1/(GD),\alpha\}$ and bound $2(1/\alpha+GD)n\log T$ ) is an open private draft with different parameters.

Difficulty

The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes $1/(Ht)$ , needs a uniform lower bound $H>0$ on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential $\sum_t\nabla_t^\top A_t^{-1}\nabla_t$ and a projection in the norm of $A_t$ rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index $0$ is unused. Cost functions are ambient functions $\mathbb R^n\to\mathbb R$ , differentiable at the points of $\mathcal P$ , with $\nabla f_t$ given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. $D$ enters only as an upper bound on distances in $\mathcal P$ . The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.

Corrections and added hypotheses:

Theorem 2 is false as printed at $T=1$ . Take $n=1$ , $\mathcal P=[-1,1]$ , $f_1(x)=x^2$ , $\alpha=\frac12$ , $G=D=2$ and $x_1=1$ : the regret is $1$ and the bound is $0$ . The paper's proof gives $4(1/\alpha+GD)(n\log T+1)$ for $T\ge2$ ; the final sentence drops the additive $1/(2\beta)$ of the p. 178 display. The goal adds $n\log T\ge4$ , under which the printed constant $5$ follows.
$G,D,\alpha>0$ are assumed wherever $\beta$ or $\varepsilon$ appear: they are the non-degeneracy the formulas presuppose (in Lean, $1/0=0$ ).
Lemma 3 adds $0<\beta$ ; the proof divides by $\beta$ .
Lemma 11 adds $\varepsilon>0$ and reads the printed $\sum_{\tau=1}^tu_tu_t^\top$ as $\sum_{\tau=1}^tu_\tau u_\tau^\top$ .
Lemma 12's product $\bullet$ is the entrywise inner product $\sum_{i,j}C_{ij}E_{ij}$ , written out as a double sum.
The printed " $f_t:\mathcal P\to\mathbb R^n$ " is read as $f_t:\mathcal P\to\mathbb R$ , and " $\Pi^{A_t}_{S_n}$ " on p. 177 as $\Pi^{A_t}_{\mathcal P}$ .

Regret is stated against every comparator $u\in\mathcal P$ , never as a real infimum ⨅ over $\mathcal P$ , which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's $\beta$ , $\varepsilon$ and $A_t$ . A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with $f_t(x)=\|x\|^2/2$ , $\alpha=1$ , $G=1$ , $D=2$ is a model.

A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, $\operatorname{tr}$ and $\det$ ); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of $\log\det$ .

Selected references

E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016); 2nd ed. arXiv:1909.05207. https://arxiv.org/abs/1909.05207

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 3: Logarithmic Regret of Follow the Approximate LeaderResearch Paper

Motivation

Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret $\Theta(\sqrt T)$ over $T$ rounds is optimal; for costs with curvature it can be logarithmic.

Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with $O(\log T)$ regret for $\alpha$ -exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.

Timeline. Zinkevich (2003) proved $O(\sqrt T)$ regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with $O(n \log T)$ regret for exp-concave costs.

Setting

The decision set $P \subseteq \mathbb{R}^n$ is nonempty, convex, closed and bounded, and $D$ bounds its diameter: $\|y - z\|_2 \le D$ for $y, z \in P$ . In rounds $t = 1, 2, \dots$ the player picks $x_t \in P$ and then pays $f_t(x_t)$ , where $f_t$ is a cost function differentiable at the points of $P$ with gradient norm $\|\nabla f_t(x)\| \le G$ on $P$ . The cost $f_t$ is $\alpha$ -exp-concave ( $\alpha > 0$ ) if $x \mapsto \exp(-\alpha f_t(x))$ is concave on $P$ . The regret over $T$ rounds against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$ .

Follow the Leader plays $x_t \in \arg\min_{x \in P} \sum_{\tau=1}^{t-1} f_\tau(x)$ (any point of $P$ in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter $\beta$ plays FTL on the approximate costs

\tilde f_\tau(x) = f_\tau(x_\tau) + \nabla_\tau^\top(x - x_\tau) + \frac{\beta}{2}(x - x_\tau)^\top \nabla_\tau\nabla_\tau^\top (x - x_\tau), \qquad \nabla_\tau = \nabla f_\tau(x_\tau).

In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory $x$ .

Formalization targets

Goal: Theorem 6

With $\beta = \tfrac12 \min\{1/(4GD), \alpha\}$ , every FTAL run on $\alpha$ -exp-concave costs satisfies, for every $T \ge 1$ and $u \in P$ ,

\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr) \le 64\left(\frac1\alpha + GD\right) n\,(\log T + 1).

This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.

Milestones

Lemma 3: an $\alpha$ -exp-concave cost with gradients bounded by $G$ lies above the paraboloid $f(y) + \nabla f(y)^\top(x-y) + \frac\beta2 (\nabla f(y)^\top (x - y))^2$ on $P$ .
Lemma 9: regret on lower surrogates that touch the costs at the played points dominates the true regret.
Lemma 10: $\sum_t f_t(x_{t+1}) \le \sum_t f_t(u)$ for an FTL run ("be the leader").
Lemma 12: $A^{-1} \bullet (A - B) \le \log(|A|/|B|)$ for $A \succeq B \succ 0$ .
Lemma 11: $\sum_{t=1}^T u_t^\top V_t^{-1} u_t \le n\log(r^2T/\varepsilon + 1)$ with $V_t = \sum_{\tau \le t} u_\tau u_\tau^\top + \varepsilon I$ .
Theorem 5 (corrected constant): FTL on costs $g_t(v_t^\top x)$ with $\|v_t\| \le R$ , $|g_t'| \le b$ , $g_t'' \ge a$ has regret at most $\frac{nb^2}{a}\log\bigl(\frac{a^2D^2R^2T^2}{b^2} + 1\bigr) + \frac{b^2}{a}$ .

Significance

Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves $O(n\log T)$ regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.

On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.

Difficulty

The obvious attempt, bounding each term $f_t(x_t) - f_t(x_{t+1})$ by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like $\log T$ , with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small $T$ , so the constants must be tracked exactly rather than asymptotically.

Formalization scope

Points are in EuclideanSpace ℝ (Fin n) so that $\|\cdot\|$ is the Euclidean norm; cost functions are functions on all of $\mathbb{R}^n$ , differentiable at the points of $P$ , with Mathlib's gradient. Rounds are $1$ -based; $x_0$ and $f_0$ are unused. $D$ is any upper bound on pairwise distances in $P$ . Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.

Regret is always stated against every comparator $u \in P$ . A formalization with a real-valued ⨅/sInf over $P$ , or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's $\beta$ , would be trivial or false, and is excluded: the goal carries IsFTALRun with $\beta = \frac12\min\{1/(4GD),\alpha\}$ .

Corrections and conventions relative to the printed paper:

Theorem 5: the printed bound $\frac{2nb^2}{a}[\log(DRaT/b) + 1]$ is false when $DRaT/b < 1/e$ . The milestone states the bound the paper's proof gives, $\frac{nb^2}{a}\log(\frac{a^2D^2R^2T^2}{b^2} + 1) + \frac{b^2}{a}$ , which implies the printed one when $DRaT \ge b$ . Derivatives are deriv with explicit differentiability at the points $v_t^\top x$ , $x \in P$ .
Lemma 10: printed with $x_t = \arg\min \sum_{\tau=1}^{t} f_\tau$ , under which it is false at $T = 1$ ; the proof and its use require the FTL index $\sum_{\tau=1}^{t-1}$ , which is stated.
Lemma 11: the typo $\sum_\tau u_t u_t^\top$ is read as $\sum_\tau u_\tau u_\tau^\top$ , and $\varepsilon > 0$ is stated.
Lemma 3: $\beta > 0$ is added (the proof divides by $\beta$ ), and $G, D > 0$ so that $1/(4GD)$ is meaningful.
Theorem 6: " $f_t : P \to \mathbb{R}^n$ " is read as $\mathbb{R}$ -valued; only first-order differentiability is assumed; $G, D > 0$ . The theorem is true as printed, although the paper's route through the printed Theorem 5 is invalid for $T < 16$ .
Only version 1 of FTAL is formalized; Lemma 4 (equivalence with the pseudoinverse form) is out of scope.

Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality $|A| \le (\operatorname{tr} A/n)^n$ . Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.

Selected references

E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
A. Kalai, S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71 (2005), 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016). https://arxiv.org/abs/1909.05207

9 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

Logarithmic Regret Algorithms for Online Convex Optimization 4: Logarithmic Regret of Exponentially Weighted Online OptimizationResearch Paper

Motivation

In online convex optimization a player repeatedly chooses a point $x_t$ from a convex set $P \subseteq \mathbb{R}^n$ , after which an adversary reveals a convex cost function $f_t$ and the player pays $f_t(x_t)$ . The player's regret after $T$ rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).

For general convex costs the best achievable regret is of order $\sqrt{T}$ . Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, $\alpha$ -exp-concavity, brings the regret down to order $\log T$ , and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of $P$ .

Timeline.

1991: Cover's universal portfolio algorithm attains regret $O(n \log T)$ for online portfolio selection, whose log-loss is $1$ -exp-concave (Cover 1991).
1997: Blum and Kalai give a short analysis of the universal portfolio with transaction costs, using a shrinking argument around the best portfolio (Blum and Kalai 1997/1999).
2003: Kalai and Vempala give a polynomial-time randomized implementation of Cover's algorithm via random walks (JMLR 3, 2003).
2007: Hazan, Agarwal and Kale state EWOO for general $\alpha$ -exp-concave costs and prove the regret bound of Theorem 7, alongside the Online Newton Step and Follow the Approximate Leader.

Setting

Fix $n \ge 0$ and a set $P \subseteq \mathbb{R}^n$ that is nonempty, closed, bounded and convex, with positive Lebesgue volume $\mathrm{vol}(P)$ . Fix $\alpha > 0$ . The cost functions are $f_1, f_2, \dots : \mathbb{R}^n \to \mathbb{R}$ , each continuous on $P$ and $\alpha$ -exp-concave on $P$ : the function $h_t(x) = e^{-\alpha f_t(x)}$ is concave on $P$ (LogRegretOCO.EWOO.IsExpConcave).

EWOO keeps the weights

w_t(x) = \exp\Bigl(-\alpha \sum_{\tau=1}^{t-1} f_\tau(x)\Bigr) = \prod_{\tau=1}^{t-1} h_\tau(x),

and on round $t$ plays the $w_t$ -weighted mean of $P$ ,

x_t = \frac{\int_P x\, w_t(x)\, dx}{\int_P w_t(x)\, dx}

(LogRegretOCO.EWOO.ewooPoint). In particular $x_1$ is the centroid of $P$ , and each $x_t$ depends only on $f_1, \dots, f_{t-1}$ . The regret against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$ .

Formalization targets

Goal: Theorem 7

For every $T \ge 1$ and every $u \in P$ ,

\sum_{t=1}^{T} f_t(x_t) - \sum_{t=1}^{T} f_t(u) \;\le\; \frac{1}{\alpha}\, n\, \bigl(1 + \log(T+1)\bigr).

This is the paper's printed constant. The paper's proof yields the slightly sharper $\frac{1}{\alpha}\bigl(1 + n\log(T+1)\bigr)$ ; the printed form is the goal.

Milestones

The proof in §3.4 (p. 187) passes through five displays, each a milestone:

Jensen for the weighted mean (first display on p. 187): $h_t(x_t) \ge \int_P h_t\, w_t \,/ \int_P w_t$ .
Eq. (18): $\prod_{\tau=1}^t h_\tau(x_\tau) \ge \int_P \prod_{\tau=1}^t h_\tau \,/\, \mathrm{vol}(P)$ .
The nearby set $S = \{\frac{T}{T+1}x^* + \frac{1}{T+1}y : y \in P\}$ : for $x \in S$ , $h_t(x) \ge \frac{T}{T+1}h_t(x^*)$ and $\prod_{\tau=1}^T h_\tau(x) \ge \frac1e \prod_{\tau=1}^T h_\tau(x^*)$ .
Volume of $S$ : $\mathrm{vol}(S) = \mathrm{vol}(P)/(T+1)^n$ .
Multiplicative regret bound (last display on p. 187): $\prod_{\tau=1}^T h_\tau(x_\tau) \ge \frac{1}{e(T+1)^n}\prod_{\tau=1}^T h_\tau(x^*)$ .

Significance

The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant $n/\alpha$ that does not depend on the size of $P$ or on the gradients of the costs. Specialised to the log-loss $f_t(x) = -\log(r_t^\top x)$ on the simplex, where $\alpha = 1$ , it recovers the $O(n\log T)$ regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound $G$ and diameter $D$ and pay a factor $(1/\alpha + GD)$ .

Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, $(n/\alpha)\log T + 2/\alpha$ , appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in $\mathbb{R}^n$ , the change of volume under homothety, and the elementary inequality $(1 + 1/T)^T \le e$ . A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.

Difficulty

The pieces are classical, but they have to be assembled in measure-theoretic form. The point $x_t$ is a Bochner integral of a vector-valued function over $P$ , and its membership in $P$ and the Jensen inequality both require the normalised weight $w_t\,dx/\int_P w_t$ to be a genuine probability measure on $P$ , with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that $P$ be closed and have positive volume.

The second obstacle is that Eq. (18) compares the algorithm with an average of the product $\prod h_\tau$ over all of $P$ , while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in $T$ destroys the logarithmic rate. Controlling this loss in $n$ dimensions, with a constant independent of the shape and size of $P$ , is the heart of the argument.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from $1$ : the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of $\mathbb{R}^n$ ; only their values on $P$ enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for $x_t$ equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.

Conventions and corrections relative to the printed text:

Regret against every comparator. The regret is stated as $\sum_t (f_t(x_t) - f_t(u)) \le$ bound for every $u \in P$ , never through a real-valued ⨅ or sInf over $P$ , which in Lean would return a junk value off its intended domain and trivialize the statement.
Positive volume volume P ≠ 0 is added: the algorithm divides by $\int_P w_t$ , which the paper leaves implicit. Without it Lean's convention $0^{-1} = 0$ would set $x_t = 0$ .
Continuity of each $f_t$ on $P$ is the paper's standing assumption (§2.2: costs twice differentiable and convex) weakened to what the argument uses; it makes every integral in the development an integral of an integrable function.
Typos. Theorem 7's " $f_t : P \to \mathbb{R}^n$ " is read as real-valued, and its " $\exp(-\alpha f(x))$ " as $\exp(-\alpha f_t(x))$ . The set-builder " $S = \{x \in S \mid \dots\}$ " defines $S$ in terms of itself and is read as the set of all $\frac{T}{T+1}x^* + \frac{1}{T+1}y$ , $y \in P$ ; the printed " $S = x^* + \frac{1}{T+1}P$ " is a translate of that set with the same volume.
Comparator. The paper's $x^*$ is a minimizer of $\sum_t f_t$ ; milestones 3 and 5 are stated for every $x^* \in P$ , which implies the minimizer case.
Constant. The printed $\frac{1}{\alpha}n(1+\log(T+1))$ is stated, although the proof gives the sharper $\frac{1}{\alpha}(1 + n\log(T+1))$ .
Not in scope. The randomized variant (sampling $x_t$ with density proportional to $w_t$ , "in expectation") and the running-time discussion of §3.4.1 have no separate proof in the paper.

Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound $(T/(T+1))^T \ge 1/e$ . Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.

Selected references

E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
A. Blum, A. Kalai, Universal portfolios with and without transaction costs, Machine Learning 35 (1999), 193–205 (COLT 1997). https://doi.org/10.1023/A:1007530728748
A. Kalai, S. Vempala, Efficient algorithms for universal portfolios, Journal of Machine Learning Research 3 (2003), 423–440. https://www.jmlr.org/papers/v3/kalai02a.html
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022; arXiv:1909.05207, Theorem 4.4. https://arxiv.org/abs/1909.05207

9 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Operations Research+1·Captain: mikedeng1

Methods of Conjugate Gradients for Solving Linear Systems I: Finite Termination of the Conjugate Gradient MethodResearch Paper

Motivation

Solving a linear system $Ax = k$ with a large symmetric positive definite matrix $A$ is a basic task of scientific computing: it arises from discretized elliptic equations, least-squares problems and the Newton steps of optimization methods. In 1952 Magnus Hestenes and Eduard Stiefel published the conjugate gradient method (cg-method) (J. Res. Natl. Bur. Stand. 49 (1952) 409–436). The method uses $A$ only through matrix–vector products and stores a few vectors. The paper's abstract states its central property in one sentence: "The solution is given in $n$ steps."

The paper obtains this property from a more general scheme, the method of conjugate directions (cd-method), which also contains Gaussian elimination as a special case. Its argument has two parts. Every cd-method with nonzero directions reaches the solution within $n$ steps (Theorem 4:2). The cg-method is a cd-method (Theorem 5:2), which follows from the orthogonality and conjugacy relations of Theorem 5:1. This mission formalizes that chain.

Setting

Vectors are real $n$ -tuples, with scalar product $(x, y) = x_1y_1 + \cdots + x_ny_n$ and squared length $|x|^2 = (x, x)$ . The matrix $A$ is real, $n \times n$ , symmetric and positive definite, which is the paper's standing assumption (p. 410). The solution $h$ satisfies $Ah = k$ . The residual of an estimate $x$ is $r = k - Ax$ . Two vectors $x, y$ are conjugate when $(x, Ay) = 0$ .

The cg-method (eq. (3:1), p. 411) starts from an arbitrary estimate $x_0$ and sets $p_0 = r_0 = k - Ax_0$ . Given $x_i$ , $r_i$ , $p_i$ , it computes

a_i = \frac{|r_i|^2}{(p_i, Ap_i)},\quad x_{i+1} = x_i + a_i p_i,\quad r_{i+1} = r_i - a_i Ap_i,\quad b_i = \frac{|r_{i+1}|^2}{|r_i|^2},\quad p_{i+1} = r_{i+1} + b_i p_i.

In Lean the iterates are cgIter A k x₀ i, a structure with fields x, r, p. The step length is cgA.

The cd-method (Section 4, p. 412) chooses an arbitrary first direction $p_0$ and then sets $x_{i+1} = x_i + a_i p_i$ with $a_i = (p_i, r_i)/(p_i, Ap_i)$ and $r_i = k - Ax_i$ . Each new direction $p_{i+1}$ may be any vector conjugate to $p_0, \dots, p_i$ . Because the directions are free, a cd-run is a property of sequences: IsCDRun A k x r p.

Formalization targets

Goal: finite termination of the cg-method

For every $n$ , every symmetric positive definite $A$ , every $k$ and $h$ with $Ah = k$ , and every initial estimate $x_0$ ,

\exists\, m \le n:\quad x_m = h,

where $x_m$ is the $m$ -th cg iterate. This is the statement of the abstract and of Section 3 (p. 410): "one will reach an estimate $x_m$ ( $m \le n$ ) at which $r_m = 0$ . This estimate is the desired solution $h$ ."

Milestones

Theorem 4:1 (p. 412). For every cd-run, the directions are mutually conjugate (4:3a). The residual $r_i$ is orthogonal to $p_0, \dots, p_{i-1}$ (4:3b). The products $(p_i, r_j)$ are the same for all $j \le i$ (4:3c). Hence $a_i = (p_i, r_0)/(p_i, Ap_i)$ (4:4).
Theorem 4:2 (p. 412). Every cd-run whose directions $p_0, \dots, p_{n-1}$ are nonzero has $x_m = h$ for some $m \le n$ .
Theorem 5:1 (p. 414), in four items. For the cg-method:
- (5:3a) $(r_i, r_j) = 0$ for $i \ne j$ ;
- (5:3b) $(p_i, Ap_j) = 0$ for $i \ne j$ ;
- (5:3c) $(p_i, r_j) = 0$ for $i < j$ and $(p_i, r_j) = |r_i|^2$ for $i \ge j$ ;
- (5:3d) $(r_i, Ap_i) = (p_i, Ap_i)$ , and $(r_i, Ap_j) = 0$ for $i \ne j, j + 1$ .
Theorem 5:5, eq. (5:10) (p. 416):

a_i = \frac{|r_i|^2}{(p_i, Ap_i)} = \frac{(p_i, r_i)}{(p_i, Ap_i)} = \frac{(p_i, r_0)}{(p_i, Ap_i)}.

Theorem 5:2, first sentence (p. 415). The cg-method is a cd-method: its iterates satisfy IsCDRun.

Significance

Finite termination is the property that distinguishes the conjugate gradient method from stationary iterations such as Jacobi or Gauss–Seidel. It explains why the method can be used as a direct solver in exact arithmetic. It is the starting point for the later theory of Krylov subspace methods. The relations of Theorem 5:1 are the checks the paper recommends for monitoring a computation (eq. (3:3)). They are also the input to the paper's further results on the monotone decrease of the error (Section 6) and on the connection with orthogonal polynomials (Sections 14–18).

The result has been proved since 1952 and appears in every numerical linear algebra textbook. As far as a search of the Prove2Me catalog shows (September 2026), it has no machine-checked proof there. The only conjugate gradient material on the platform is a Hilbert-space convergence result for a different recurrence. This mission adds a faithful formal version of the original recursion (3:1) and of the cd-method. It also adds the complete termination argument, organized as in the paper. The definitions and the Theorem 5:1 relations are reusable by any later formalization of Krylov methods, including the second mission of this series on the decrease of the error $|h - x_i|$ .

Difficulty

The obvious argument says that the residuals are mutually orthogonal, so at most $n$ of them are nonzero. That argument is only as good as the orthogonality, and Theorem 5:1 must be established by a simultaneous induction over four families of relations. The recursion defines $r_{i+1}$ by an update, not as $k - Ax_{i+1}$ , so even $r_i = k - Ax_i$ needs a proof. Orthogonality of $r_{i+1}$ to the earlier residuals needs the conjugacy of the earlier directions, and conjugacy of $p_{i+1}$ needs the orthogonality of the earlier residuals. Neither family can be proved first.

A second obstacle is the passage from orthogonality to termination. A cd-run with a zero direction stalls, so Theorem 4:2 needs the directions $p_0, \dots, p_{n-1}$ to be nonzero. The cg directions become zero exactly when the solution is reached, so applying Theorem 4:2 to cg needs a case split at the first vanishing residual.

Formalization scope

Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), and $Ax$ is Matrix.mulVec (*ᵥ). The hypothesis on $A$ is Mathlib's Matrix.PosDef, which includes symmetry. The solution enters only through the hypothesis A *ᵥ h = k. Indices are 0-based, as in the paper.

The cg iteration is total and has no stopping test. Once $r_m = 0$ , Lean's convention $x/0 = 0$ gives $p_m = 0$ and $a_m = 0$ . From then on the iteration stays at $x_m$ , with zero residuals and directions. For this reason the relations of Theorem 5:1 are stated for all indices without guards: after termination they hold trivially.

Two formulations would make the goal trivial, and neither is used. One is a stopping test or step that refers to $h$ or to $A^{-1}k$ . The other replaces (3:1b), (3:1d) or (3:1e) by the equivalent formulas (3:2a), (3:2b) or $r_{i+1} = k - Ax_{i+1}$ , which would move Theorem 5:5 and part of Theorem 5:2 into the definition. The iteration is (3:1) literally.

The cd-method's implicit hypothesis, that the directions $p_0, \dots, p_{n-1}$ are nonzero, is an explicit binder of Theorem 4:2. Without it the statement fails (take $p_0 = 0$ ). The hypothesis is satisfiable: the cg run with nonzero residuals is one example.

A complete development needs the standard facts that mutually conjugate nonzero vectors are linearly independent and that $n$ independent vectors span $\mathbb{R}^n$ . It also needs the induction behind Theorem 5:1. Contributions welcome beyond the milestones include the converse half of Theorem 5:2, the relation (5:2) expressing $p_k$ through $r_0, \dots, r_k$ , and Theorem 4:5 (the cd-method computes $A^{-1}$ ).

Selected references

M. R. Hestenes and E. Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, Journal of Research of the National Bureau of Standards 49(6), 409–436, 1952. https://doi.org/10.6028/jres.049.044
L. Fox, H. D. Huskey and J. H. Wilkinson, Notes on the solution of algebraic linear simultaneous equations, Quarterly Journal of Mechanics and Applied Mathematics 1(1), 149–173, 1948 (the cd-method from a different point of view; cited in the paper's Section 4 footnote). https://doi.org/10.1093/qjmam/1.1.149
G. H. Golub and C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins University Press, 2013, §11.3 (textbook account of the method).

11 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis Operations Research+1·Captain: mikedeng1

Methods of Conjugate Gradients for Solving Linear Systems II: Each Conjugate Gradient Step Shortens the Error VectorResearch Paper

Motivation

The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems $Ax=k$ with a symmetric positive definite matrix $A$ . It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most $n$ steps, and a method of successive approximations whose intermediate estimates are useful in their own right.

The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the $A$ -weighted error $f(x)=(h-x,A(h-x))$ , and the residual $|k-Ax_i|$ need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance $|h-x_i|$ from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.

Timeline:

1952: Hestenes and Stiefel introduce the method and prove, in one paper, finite termination (Theorems 4:2 and 5:2), the monotone decrease of the error function $f$ (Theorem 6:1), and the monotone decrease of the Euclidean error (Theorem 6:3). The later literature on cg as an iterative method for large sparse systems takes these properties as its starting point.

Setting

Let $A$ be a real $n\times n$ matrix that is symmetric and positive definite, let $k\in\mathbb{R}^n$ , and let $h$ be the solution of $Ah=k$ . Write $(x,y)=x_1y_1+\cdots+x_ny_n$ and $|x|^2=(x,x)$ . From an arbitrary starting point $x_0$ , the cg-method (5:1) computes estimates $x_i$ , residuals $r_i$ and direction vectors $p_i$ by

p_0=r_0=k-Ax_0,\quad a_i=\frac{|r_i|^2}{(p_i,Ap_i)},\quad x_{i+1}=x_i+a_ip_i,\quad r_{i+1}=r_i-a_iAp_i,\quad b_i=\frac{|r_{i+1}|^2}{|r_i|^2},\quad p_{i+1}=r_{i+1}+b_ip_i .

The error vector of $x_i$ is $y_i=h-x_i$ . The error function (4:5) is $f(x)=(h-x,A(h-x))$ , which is nonnegative and vanishes only at $x=h$ . The Rayleigh quotient (4:12) of a vector $z\neq 0$ is $\mu(z)=(z,Az)/|z|^2$ . The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for $a_i$ , errorFun A h x and rayleigh A z.

Formalization targets

Goal: Theorem 6:3

For every step that the method performs, that is, every $i$ with $r_i\neq 0$ ,

|y_i|^2-|y_{i+1}|^2=\frac{f(x_{i+1})+f(x_i)}{\mu(p_i)}\qquad\text{and}\qquad |y_{i+1}|<|y_i| .

The paper writes the step from $x_{i-1}$ to $x_i$ ; the Lean statement shifts the index by one. The goal holds for every dimension $n$ , every symmetric positive definite $A$ , every $k$ and every $x_0$ .

Milestones

Theorems 4:2 and 5:2: some $m\le n$ has $x_m=h$ .
Theorem 5:3, (5:6a): $(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2$ for $i\le j$ .
Theorem 6:1, (6:1): $f(x_i)-f(x_{i+1})=a_i|r_i|^2=\mu(p_i)|x_i-x_{i+1}|^2$ .
Theorem 6:1, (6:2): $f(x_i)-f(x_j)=\sum_{l=i}^{j-1}a_l|r_l|^2$ for $i<j$ .
Section 6, (6:6): $(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)$ .

Significance

The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the $A$ -norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.

The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.

Difficulty

The obvious argument does not reach the conclusion. The method decreases $f(x)=(y,Ay)$ at every step, but a decrease in this $A$ -weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for $f$ can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.

A second difficulty is bookkeeping at the end of the run. The recursion divides by $|r_i|^2$ and by $(p_i,Ap_i)$ , which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis $r_i\neq 0$ exactly because the strict inequality fails once $x_i=h$ .

Formalization scope

Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), $Ax$ is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution $h$ is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention $t/0=0$ makes it stay at $h$ with $r_i=p_i=0$ once $r_m=0$ . Lengths appear squared, as $(y,y)$ . The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries $r_i\neq 0$ .

Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination ( $x_m=h$ ) or any bound on $i$ : it quantifies over every cg run and every step that takes place. And it is about the Euclidean length $|h-x_i|$ , not the error function $f$ (that is Theorem 6:1, a different and weaker statement) and not the residual.

A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of $(p,Ap)$ for $p\neq 0$ . These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.

Selected references

M. R. Hestenes and E. Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6), 409–436, 1952. https://doi.org/10.6028/jres.049.044 (publisher's scan: https://nvlpubs.nist.gov/nistpubs/jres/049/jresv49n6p409_A1b.pdf)

9 thms3 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Markov-Renewal Programming. I: Formulation, Finite Return Models: Policy Iteration Finds an Optimal Stationary Policy for the Discounted Infinite-Horizon Markov-Renewal ProgramResearch Paper

Motivation

Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.

Timeline:

1954: Lévy, Smith and Takács independently introduce Markov-renewal and semi-Markov processes; Pyke later surveys them.
1960: Howard, Dynamic Programming and Markov Processes, introduces policy iteration for finite discrete-time Markov decision processes.
1962: Blackwell, Discrete Dynamic Programming, shows that for the discounted discrete-time problem a stationary policy is optimal among all policies.
1963: Jewell formulates Markov-renewal programming, with a continuous discount factor α, and carries Howard's algorithm and Blackwell's stationarity result over to it. Part II of the paper treats the undiscounted (infinite-return) models.

Setting

A Markov-renewal program has a finite set of states $S$ (the paper's $i = 1, \dots, N$ ) and a finite, nonempty set of alternatives (the paper's $z = 1, \dots, Z$ ), each available in every state. For each alternative $z$ and states $i, j$ it specifies:

a transition probability $p^z_{ij} \ge 0$ , with $\sum_j p^z_{ij} = 1$ ;
a sojourn-time distribution $F^z_{ij}$ , the law of the time $\tau$ between entering $i$ and moving to $j$ , with $\tau \ge 0$ and $F^z_{ij}(0) = 0$ ;
for each continuous discount factor $\alpha > 0$ , a real number $\rho^z_{ij}(\alpha)$ , the expected discounted return earned during that transition.

The Laplace–Stieltjes transform $\tilde f^z_{ij}(s) = \int_0^\infty e^{-st}\,dF^z_{ij}(t)$ is the expected discount $\mathbb E[e^{-s\tau}]$ over one interval. The average one-step return is $\rho^z_i(\alpha) = \sum_j p^z_{ij}\rho^z_{ij}(\alpha)$ , and for a vector of returns $v$ the test quantity is

\rho^z_i(\alpha) + \sum_j p^z_{ij}\,\tilde f^z_{ij}(\alpha)\,v_j .

A stationary policy is a map $d : S \to A$ ; a nonstationary policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of such maps, $\pi_k$ being used at the $k$ -th transition. The $n$ -step return $V^\pi_i(n)$ of a policy, with boundary rewards $V_i(0,\alpha)$ , is the test quantity of $\pi_0(i)$ applied to the $(n-1)$ -step return of the shifted policy; the optimal $n$ -step return $V_i(n,\alpha)$ of equation (6) replaces $\pi_0(i)$ by a maximum over $z$ . The value-determination equations (15) of a stationary policy $d$ are $v_i = \rho^{d(i)}_i(\alpha) + \sum_j p^{d(i)}_{ij}\tilde f^{d(i)}_{ij}(\alpha) v_j$ .

The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.

Formalization targets

Goal (p. 947)

For every $\alpha > 0$ : (15) has a unique solution for every stationary policy, and every run $(d_k, v_k)$ of Fig. 1 reaches $d_{K+1} = d_K$ with $K < Z^N$ , where

\lim_{n\to\infty} V^{d_K}_i(n) = (v_K)_i,\qquad \lim_{n\to\infty} V^\pi_i(n) \le (v_K)_i \ \ \forall \pi,\qquad \lim_{n\to\infty} V_i(n,\alpha) = (v_K)_i ,

for every state $i$ and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".

Milestones

p. 945: $0 \le p^z_{ij}\tilde f^z_{ij}(s) < 1$ for $s > 0$ .
Claim (a): (15) has exactly one solution for each stationary policy.
Eq. (15): the $n$ -step return of a stationary policy converges to a solution of (15).
p. 946: $I - \tilde q(\alpha)$ is invertible and $([I-\tilde q(\alpha)]^{-1})_{ii} \ge 1$ .
Claim (b): a change of policy raises the return of some state and lowers none.
Claim (c): a policy reproduced by the improvement step is optimal among stationary policies.
Claim (d): a run of Fig. 1 terminates within $Z^N$ cycles.
Eq. (14): $V_i(n,\alpha)$ converges, independently of the boundary rewards, to a solution of $v_i = \max_z\{\rho^z_i(\alpha) + \sum_j p^z_{ij}\tilde f^z_{ij}(\alpha) v_j\}$ .
p. 946: some stationary policy's return dominates the limiting return of every nonstationary policy.

Significance

The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers $\tilde f^z_{ij}(\alpha)$ , so the same algorithm serves any sojourn-time law. For fixed $\alpha$ the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).

The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.

Difficulty

The discount over one transition, $\tilde f^z_{ij}(\alpha)$ , varies with $i$ , $j$ and $z$ , so the problem is not a constant- $\gamma$ contraction of textbook form; the relevant bound is that every row of $\tilde q(\alpha)$ sums to less than one, which rests on $F^z_{ij}(0) = 0$ . Entries in $[0, 1)$ alone, the paper's stated justification of Claim (a), do not make $I - \tilde q(\alpha)$ invertible: the $2 \times 2$ matrix with every entry $1/2$ has entries in $[0,1)$ , yet $I$ minus it is singular.

Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.

Formalization scope

States and alternatives are finite types; alternatives are nonempty. Every alternative is available in every state.
$F^z_{ij}$ is a probability measure on $\mathbb R$ with no mass on $(-\infty, 0]$ . The transform is integrated over $(0, \infty)$ , which carries all the mass.
The one-transition returns $\rho^z_{ij}(\alpha)$ are arbitrary real numbers, a generalization of the paper's Stieltjes integral (4), which is not formalized. The reward functions $R^z_{ij}(t\mid\tau)$ do not appear.
Returns of policies are defined by the one-step recursion (the policy form of (6)); the Markov-renewal process is not built as a stochastic process.
Policies are the paper's: deterministic and Markov, nonstationary ones indexed by the number of transitions made. Randomized and history-dependent policies are not in the comparison class.
The following informal words are read as follows. "Solve the set of simultaneous equations": (15) has exactly one solution. "Strictly increases the expected return of at least one state": no state's return decreases and one strictly increases, under the hypothesis that the policy changed. "No other policy can lead to higher expected returns" in Claim (c): no stationary policy. "Terminates in a finite number of cycles": two successive policies coincide at some cycle $K < Z^N$ . "If there is no improvement in the test quantity, retain the same alternative": the old alternative is kept whenever it attains the maximum. "Optimal" and "as good as any nonstationary policy": the limiting return of the returned policy dominates that of every policy from every state, for all boundary rewards. " $\lim_{n\to\infty} V_i(n,\alpha)$ ": the limit is proved to exist. " $\max_z$ ": a maximum over the finite nonempty set of alternatives.
Eq. (14) is printed with $v_i(\alpha)$ inside the sum over $j$ ; the formalization uses $v_j(\alpha)$ , as (6), (15) and Fig. 1 do.
Every statement fixes one $\alpha > 0$ . The undiscounted models (16)–(19), the finite-time and mixed-horizon models (9)–(13), and the infinite-time case of the stationarity result are out of scope.
The return of a policy is never defined through a matrix inverse, whose Mathlib value for a singular matrix is $0$ ; (15) is a predicate, and the goal asserts unique solvability, so a vacuous reading through junk inverses or assumed limits is excluded.

Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.

Selected references

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
W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2), 719–726, 1962. https://doi.org/10.1214/aoms/1177704593
R. Pyke, Markov Renewal Processes: Definitions and Preliminary Properties, Annals of Mathematical Statistics 32(4), 1231–1242, 1961. https://doi.org/10.1214/aoms/1177704863
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 7.2–7.3.

12 thms3 active usersReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 1: First-Fit and Best-Fit Have Asymptotic Worst-Case Ratio 17/10Research Paper

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.

Timeline:

1972. Garey, Graham and Ullman announce that First-Fit uses at most about $1.7$ times the optimal number of bins (Proc. 4th ACM STOC, 1972); Johnson's thesis (MIT, 1973) develops the analysis.
1974. Johnson, Demers, Ullman, Garey and Graham prove $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list, and give lists with $FF(L)=BF(L)>1.7L^*-8$ for every optimum $L^*=k$ , so the asymptotic worst-case ratio of both rules is exactly $\tfrac{17}{10}$ (SIAM J. Comput. 3(4)). This paper is the source of the mission.
1976–2014. The additive constant is lowered: Garey, Graham, Johnson and Yao (1976) show $FF(L)\le\lceil 1.7L^*\rceil$ , and Dósa and Sgall prove the tight bound $FF(L)\le\lfloor 1.7L^*\rfloor$ (STACS 2013) and the same bound for Best-Fit (ICALP 2014).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$ ; values may repeat. A bin has capacity $1$ , and its level is the sum of the numbers in it. The optimum $L^*$ is the minimum number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$ .

Both rules place $a_1,\dots,a_n$ in this order into bins $B_1,B_2,\dots$ , each initially at level $0$ , and never move an element once placed.

First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ .
Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, taking the least index among ties.

$FF(L)$ and $BF(L)$ are the numbers of nonempty bins at the end. The worst-case ratio at optimum $k$ is

R_{FF}(k)=\sup\Bigl\{\frac{FF(L)}{L^*}:L^*=k\Bigr\},\qquad R_{BF}(k)=\sup\Bigl\{\frac{BF(L)}{L^*}:L^*=k\Bigr\}.

The analysis also uses a weighting function $W:[0,1]\to[0,1]$ , piecewise linear with $W(\alpha)=\tfrac65\alpha$ on $[0,\tfrac16]$ , $\tfrac95\alpha-\tfrac1{10}$ on $(\tfrac16,\tfrac13]$ , $\tfrac65\alpha+\tfrac1{10}$ on $(\tfrac13,\tfrac12]$ and $1$ on $(\tfrac12,1]$ , and the coarseness of a bin of a completed packing: the largest $1-\operatorname{level}(B')$ over the bins $B'$ of smaller index, and $0$ for the first bin.

Formalization targets

Goal: the asymptotic ratio (Corollary of Section 2, p. 306)

\lim_{k\to\infty}R_{FF}(k)=1.7\qquad\text{and}\qquad\lim_{k\to\infty}R_{BF}(k)=1.7.

The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.

Milestones, in the order the proof uses them

Claim 2.2.1 (p. 304): a bin with total size at most $1$ has $\sum_i W(b_i)\le\tfrac{17}{10}$ .
Claim 2.2.2 (p. 305): in an FF or BF packing, every element placed into a bin before the bin was more than half full exceeds the bin's coarseness.
Claim 2.2.3 (p. 305): a bin of coarseness $\alpha<\tfrac12$ whose level exceeds $1-\alpha$ has weight at least $1$ .
Claim 2.2.4 (p. 306): a bin of coarseness $\alpha<\tfrac12$ with weight $1-\beta$ , $\beta>0$ , either holds a single element at most $\tfrac12$ or has level at most $1-\alpha-\tfrac59\beta$ .
Theorem 2.2 (p. 304): $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list.
Theorem 2.1 (p. 301): for every $k\ge1$ there is a list with $L^*=k$ and $FF(L)=BF(L)>1.7L^*-8$ .

A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with $L^*=10$ and $FF(L)=BF(L)=17$ .

Significance

The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about $70\%$ more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant $\tfrac{17}{10}$ is the reference point for later on-line algorithms.

The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the $1.7L^*+2$ upper bound and of the lower-bound construction.

Difficulty

The first idea, charging each bin its level, gives only $FF(L)\le 2L^*+1$ : at most one bin is at most half full. The ratio $\tfrac{17}{10}$ comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near $\tfrac16,\tfrac13,\tfrac12$ , p. 301) gives only the ratio $\tfrac53$ ; reaching $\tfrac{17}{10}$ needs a list on which both rules waste space in every medium bin, for every $k$ , while $L^*$ is still known exactly.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$ ), and every statement assumes it. $L^*$ is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most $1$ . A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least $j$ " over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict $\beta+a_i\le1$ , and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are $0$ -based. Coarseness is computed in the completed packing. $W$ is a function ℝ → ℝ and is only ever applied to elements of $(0,1]$ . $R_{FF}(k)$ and $R_{BF}(k)$ are suprema in the extended nonnegative reals $[0,\infty]$ , and the limit is taken there.

A real-valued supremum would be $0$ on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.

Claim 2.2.4 is printed with alternative (i) " $m=1$ and $b_1<\tfrac12$ ", which is false: First-Fit on $(0.6,0.5)$ gives a counterexample. The mission states it with $b_1\le\tfrac12$ , which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.

The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most $1$ , at most one bin is at most half full, the history determines the final packing), and the computation of $L^*$ for the explicit lists of Theorem 2.1 and Fig. 3.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
M. R. Garey, R. L. Graham, J. D. Ullman, Worst-case analysis of memory allocation algorithms, Proc. 4th ACM STOC, 1972.
D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, MIT, 1973.
M. R. Garey, R. L. Graham, D. S. Johnson, A. C. Yao, Resource constrained scheduling as generalized bin packing, J. Combinatorial Theory Ser. A 21, 1976.
G. Dósa, J. Sgall, First Fit bin packing: A tight analysis, STACS 2013, LIPIcs 20:538–549. https://doi.org/10.4230/LIPIcs.STACS.2013.538
G. Dósa, J. Sgall, Optimal analysis of Best Fit bin packing, ICALP 2014, LNCS 8572.

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 2: First-Fit and Best-Fit with Bounded Item SizesResearch Paper

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$ . When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$ .

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$ . The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$ .

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$ . Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$ . The level of a bin is the sum of the numbers in it. For a real $\alpha>0$ , write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$ .

First-Fit ( $FF$ ) considers bins $B_1,B_2,\dots$ , all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ . Best-Fit ( $BF$ ) is the same except that, among the bins with $\beta\le 1-a_i$ , it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$ , an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$ .

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$ ; likewise for $BF$ .

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$ , then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$ .

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$ ,

FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$ , $\tfrac43$ when at most $\tfrac13$ , and tends to $1$ as the maximum item size tends to $0$ . Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$ . Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$ , and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$ ); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$ " over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$ , $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$ , $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$ , never a default value, and at $k=0$ the only admissible list is empty and the value is $0$ . The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$ ", which is weaker than $L\subseteq(0,\alpha]$ .

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$ , and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$ , $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

7 thms4 active usersReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 3: First-Fit Decreasing and Best-Fit Decreasing Use at Most 11/9 L* + 4 BinsResearch Paper

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.

This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most $\tfrac{11}{9}$ of the optimum, plus an additive constant, is ever used, and that the factor $\tfrac{11}{9}$ cannot be improved.

Timeline.

1973: D. S. Johnson's MIT thesis proves $FFD(L)\le \tfrac{11}{9}L^*+4$ ; the argument exceeds 75 pages.
1974: Johnson, Demers, Ullman, Garey and Graham publish the bound for FFD and BFD, with a complete proof of the reduction from BFD to FFD and an outline of the FFD argument.
1985: B. S. Baker gives a shorter proof of $FFD(L)\le\tfrac{11}{9}L^*+3$ (J. Algorithms 6).
1991: M. Yue publishes a proof of $FFD(L)\le\tfrac{11}{9}L^*+1$ .
2007: G. Dósa determines the tight additive constant, $FFD(L)\le\tfrac{11}{9}L^*+\tfrac{6}{9}$ (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$ ; values may repeat. A bin has capacity $1$ ; its level is the sum of the numbers placed in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be distributed so that no bin has level exceeding $1$ .

The bins $B_1,B_2,\dots$ start empty and the elements are placed one at a time, in list order.

First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ .
Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, the one of least index among ties.
First-Fit Decreasing (FFD) and Best-Fit Decreasing (BFD) first arrange $L$ into nonincreasing order and then apply FF, respectively BF.

$FFD(L)$ and $BFD(L)$ are the numbers of bins that receive at least one element.

Two auxiliary notions from the paper's proof also appear among the milestones. The position $(j,k)$ of an element in a packing means that it is the $k$ -th element placed into bin $j$ . The weight $W(X)$ of a collection of elements is defined through $k$ -pieces, the elements in $(\tfrac1{k+1},\tfrac1k]$ . Each element has the weight $w_1(x)=\lfloor 1/x\rfloor^{-1}$ . A pair $(x,y)$ with $x$ a $k$ -piece and $kx+y\le1$ has the discounted weight $w_2(x,y)=w_1(x)+\tfrac{k-1}{k}w_1(y)$ , and any other pair has $w_1(x)+w_1(y)$ . $W(X)$ is the least total weight over all ways of grouping $X$ into singletons and pairs.

Formalization targets

Goal: Theorem 3.2

For every list $L$ ,

FFD(L)\le \frac{11}{9}L^*+4\qquad\text{and}\qquad BFD(L)\le\frac{11}{9}L^*+4 .

The constants are the paper's. Both halves are part of the goal.

Milestones, in the order the argument uses them

Lemma 3.3. If $FFD(L)>rL^*+d$ with $r,d\ge1$ , the list $L'$ keeping only the elements exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$ ; the same for BFD. With $r=\tfrac{11}{9}$ this reduces the goal to lists in $(\tfrac2{11},1]$ .
Claims 3.4.5 and 3.4.6, two steps of the proof of Theorem 3.4 that concern only the FFD packing $PF$ and the BFD run. On $[\tfrac16,1]$ , BFD places every element exceeding $\tfrac13$ exactly where FFD does. Among the remaining positions of $PF$ , the lexicographic order of positions respects the order of the sorted list.
Theorem 3.4. If $L\subseteq[\tfrac16,1]$ , then $BFD(L)\le FFD(L)$ . This transfers the bound from FFD to BFD on $(\tfrac2{11},1]$ .
Lemma 4.2. For every integer $N\ge4$ and $L\subseteq(\tfrac1N,\tfrac12]$ ,

W(L)\ge FFD(L)-N+2 .

The reduced assertion (Section 4, p. 314). If $L\subseteq(\tfrac2{11},1]$ , then

FFD(L)\le\frac{11}{9}L^*+4 .

Theorem 3.1, the matching lower bound: for each $k\ge1$ there is a list with $L^*=k$ and $FFD(L)=BFD(L)>\tfrac{11}{9}L^*-2$ .

Significance

The bound makes FFD and BFD, which run in $O(n\log n)$ time, the reference heuristics for off-line bin packing. The $\tfrac{11}{9}$ bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines $\lim_{k\to\infty}R_{FFD}(k)=\lim_{k\to\infty}R_{BFD}(k)=\tfrac{11}{9}$ , where $R_A(k)$ is the largest ratio $A(L)/L^*$ over lists with $L^*=k$ .

The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the $\tfrac{11}{9}$ bound is present in Mathlib or on the platform.

Difficulty

The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least $1$ and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio $\tfrac{11}{9}$ . Summing $w_1$ over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total $w_1$ -weight well above $\tfrac{11}{9}$ . The paper's remedy is a weight defined on pairs, $W(X)$ , which discounts elements that could share a bin with a larger one. Even with $W$ , the bins of FFD whose largest element exceeds $\tfrac12$ do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.

The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with $BFD(L)=\tfrac{10}{9}FFD(L)$ . Theorem 3.4 works only because Lemma 3.3 first removes all elements below $\tfrac2{11}$ .

Formalization scope

Lists are L : List ℝ with the predicate IsList L ( $0<a\le1$ for every element), assumed by every statement. $L^*$ is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most $1$ . A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least $j$ " over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted $L$ . Positions are $0$ -based pairs (bin, place in bin) read off the run.

$W$ sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: $[\tfrac16,1]$ is closed in Theorem 3.4, $(\tfrac2{11},1]$ is open at $\tfrac2{11}$ , and Lemma 4.2 has $\tfrac1N<a\le\tfrac12$ .

A weakened goal, such as $FFD(L)\le\tfrac{11}{9}L^*+c$ with a larger $c$ , a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities $(*)$ , $(**)$ of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps $f$ , $g$ .

A complete development needs basic lemmas about FF and BF runs (levels stay at most $1$ , a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of $L^*$ under deletion, and $L^*\ge\sum_i a_i$ . These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper above).
B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, Journal of Algorithms 6(1):49–70, 1985. https://doi.org/10.1016/0196-6774(85)90018-5
M. Yue, A simple proof of the inequality FFD(L) ≤ 11/9 OPT(L) + 1, ∀L, for the FFD bin-packing algorithm, Acta Mathematicae Applicatae Sinica 7(4):321–331, 1991.
G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, LNCS 4614:1–11, 2007. https://doi.org/10.1007/978-3-540-74450-4_1

10 thms3 active usersReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 4: First-Fit Decreasing Uses at Most 71/60 L* + 5 Bins When No Item Exceeds 1/2Research Paper

Motivation

Bin packing asks how to place a list of items with sizes in $(0,1]$ into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.

Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound $FFD(L)\le\frac{11}{9}L^*+4$ , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds $1/2$ , FFD uses at most $\frac{71}{60}L^*+5$ bins. That result is the subject of this mission.

Timeline:

1973: D. S. Johnson's MIT thesis, Near-optimal bin packing algorithms, contains the complete proofs of the $11/9$ and $71/60$ bounds.
1974: Johnson, Demers, Ullman, Garey and Graham publish the $71/60$ bound for lists in $(0,1/2]$ (Theorem 4.1) with a proof that is complete except for parts of two lemmas, and show by example that $71/60$ cannot be lowered.
1985: B. S. Baker gives a shorter proof of the $11/9$ bound for FFD (J. Algorithms 6, 1985).
2007: G. Dósa determines the tight additive constant $6/9$ in the $11/9$ bound (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$ ; values may repeat. A bin has capacity $1$ ; its level is the sum of the numbers in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed with no bin level exceeding $1$ .

First-Fit places $a_1,a_2,\dots$ in order into bins $B_1,B_2,\dots$ , each initially at level $0$ : $a_i$ goes into the bin of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ . First-Fit Decreasing first arranges $L$ into nonincreasing order and then runs First-Fit. $FFD(L)$ is the number of bins it uses.

The proof uses a weight $W$ on finite sets of elements. For an integer $k\ge1$ , $x$ is a $k$ -piece if $x\in(\frac1{k+1},\frac1k]$ , and a $k$ -bin is a bin whose largest element is a $k$ -piece. Set $w_1(x)=\lfloor 1/x\rfloor^{-1}$ . A pair $(x,y)$ obeys relation $k$ if $x$ is a $k$ -piece and $kx+y\le1$ ; then $w_2(x,y)=w_1(x)+\frac{k-1}{k}w_1(y)$ , and otherwise $w_2(x,y)=w_1(x)+w_1(y)$ . For a partition $\pi$ of $X$ into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,

w_{12}(\pi)=\sum_{\{x\}\in\pi}w_1(x)+\sum_{(x,y)\in\pi}w_2(x,y),\qquad W(X)=\min_\pi w_{12}(\pi).

BASIC is the set of elements of $L$ that are $k$ -pieces lying in a $k$ -bin of the FFD packing of $L$ , for some $k$ ; SURPLUS is the rest of $L$ .

Formalization targets

Goal: Theorem 4.1

\text{for every list } L\subseteq(0,\tfrac12]:\qquad FFD(L)\le\frac{71}{60}L^*+5 .

The constants are those printed in the paper. The multiplicative constant $71/60$ is best possible.

Milestones

Lemma 3.3 (FFD part): if $FFD(L)>rL^*+d$ with $r,d\ge1$ , the list $L'$ of the elements of $L$ exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$ .
Claim 4.2.1: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $\sum_{x\in\mathrm{BASIC}}w_1(x)\ge FFD(L)-\sum_{j=2}^{N-1}\frac{j-1}{j}$ .
Claim 4.2.2: for $N\ge4$ , $L\subseteq(\frac1N,\frac12]$ and every partition $\pi$ of $L$ into one- and two-element sets, $w_{12}(\pi)\ge w_1(\mathrm{BASIC})-\sum_{j=3}^{N-1}\frac1j$ .
Lemma 4.2: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $W(L)\ge FFD(L)-N+2$ .
Subadditivity: $W(X_1\cup\dots\cup X_k)\le\sum_i W(X_i)$ .
Lemma 4.3: if $X\subseteq(\frac17,\frac12]$ and $\sum_{x\in X}x\le1$ , then $W(X)\le\frac{71}{60}$ .

A companion item states the Remark after Theorem 4.1: for every $N\ge1$ there is a list with all elements below $1/3$ , $L^*=60N$ and $FFD(L)=71N$ .

Significance

Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the $11/9$ bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that $71/60$ is exact for items in $(0,1/2]$ , and the Corollary on p. 322 extends the analysis to the asymptotic ratio $R^\alpha_{FFD}$ when items are bounded by $\alpha\in(8/29,1/2]$ .

The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.

Difficulty

The obvious weight $w_1$ alone fails. Claim 4.2.1 shows that $w_1(\mathrm{BASIC})$ covers the FFD bins, but many sets $X$ of elements with sum at most $1$ have $w_1(X)>71/60$ , for example two $2$ -pieces, a $5$ -piece and a $6$ -piece. The pair discounts of $w_2$ repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation $k$ lies in a bin of type $k'<k$ . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in $X$ and the relations they obey.

Formalization scope

A list is L : List ℝ with IsList L ( $0<a\le1$ for each element) in every statement. $L^*$ is optBins L, the least $b$ such that some map from positions to Fin b has every bin sum at most $1$ . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least $j$ ". The fit test is $\beta+a\le1$ . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are $0$ -based.

$W(X)$ sorts $X$ into nonincreasing order and minimises $w_{12}$ over the involutions of its positions: fixed points are singletons, and a pair $i<\sigma(i)$ is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In $w_2$ , $k=\lfloor1/x\rfloor$ is the piece type of the first element. Sums $\sum_{j=2}^{N-1}$ are over Finset.Icc 2 (N - 1) with $N\ge4$ .

The goal's range is $(0,1/2]$ . The restriction to $(1/7,1/2]$ belongs only to the proof, through Lemma 3.3. Stating the goal for $(1/7,1/2]$ , weakening $71/60$ or $5$ , or making $W$ an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis $N\ge4$ . The Remark's printed range $0<\varepsilon\le5/87$ is a misprint: its FFD packing needs $\varepsilon<1/174$ , and the companion item states only the existence claim.

Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the $11/9$ bound (mission 3 of this series) and for the bounded- $\alpha$ corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3(4):299–325, 1974. https://doi.org/10.1137/0203025
D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper).
B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, J. Algorithms 6, 1985.
G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, Lecture Notes in Computer Science 4614, 2007.

9 thms3 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

Critical-Path Planning and Scheduling I: Critical Jobs Occur Only When the Completion Time Is the Earliest, and Then Form a Path from Origin to TerminusResearch Paper

Motivation

The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.

The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.

Setting

A project network has $n+1$ events labelled $0,1,\dots,n$ with $n \ge 1$ : event $0$ is the origin and event $n$ the terminus. A job is an arrow from an event $i$ to an event $j$ , written job $(i,j)$ ; the jobs form a finite set $P$ of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:

every job has $i < j$ (events are labelled so that the head of an arrow has the larger label);
origin precedes and terminus follows every event: for every event $k$ there are chains of jobs from $0$ to $k$ and from $k$ to $n$ .

Each job has a real duration $y_{ij}$ . The earliest event times $t^{(0)}$ are given by display (1) of the paper,

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and, for a project completion time $\lambda \ge t_n^{(0)}$ , the latest event times $t^{(1)}$ by display (2),

t_n^{(1)} = \lambda,\qquad t_i^{(1)} = \min\,[\,t_j^{(1)} - y_{ij} \mid i<j,\ (i,j)\in P\,],\quad 0\le i\le n-1.

The maximum time available for job $(i,j)$ is $t_j^{(1)} - t_i^{(0)}$ . The job is critical if this equals its duration, $t_j^{(1)} - t_i^{(0)} = y_{ij}$ , and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events $0 = v_0, v_1, \dots, v_k = n$ with every $(v_{r-1}, v_r)$ a critical job of $P$ .

In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.

Formalization targets

Goal: critical jobs force $\lambda = t_n^{(0)}$ and a critical path (p. 163)

For every project network, durations $y$ and completion time $\lambda \ge t_n^{(0)}$ ,

\bigl(\exists (i,j)\in P,\ t_j^{(1)} - t_i^{(0)} = y_{ij}\bigr) \;\Longrightarrow\; \lambda = t_n^{(0)} \ \wedge\ \exists\ \text{a critical path}.

This is the paper's "A project will contain critical jobs only when $\lambda = t_n^{(0)}$ . If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.

Milestones

Display (1), pp. 162–163. $t^{(0)}$ is the least vector $t$ with $t_0 = 0$ and $y_{ij} \le t_j - t_i$ for every job.
Display (2), p. 163. For $\lambda \ge t_n^{(0)}$ , $t_n^{(1)} = \lambda$ and $t^{(1)}$ is the greatest vector $t$ with $t_n \le \lambda$ and $y_{ij} \le t_j - t_i$ for every job.
Critical or floater, p. 163. For $\lambda \ge t_n^{(0)}$ , $t_i^{(0)} \le t_i^{(1)}$ for every event, and every job is critical or a floater: $t_j^{(1)} - t_i^{(0)} \ge y_{ij}$ .
Delay of a critical job, p. 163. Lengthening a critical job by $\delta \ge 0$ raises $t_n^{(0)}$ by exactly $\delta$ .

Significance

The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify $t^{(0)}$ and $t^{(1)}$ with extreme solutions of the system of difference constraints $y_{ij} \le t_j - t_i$ , which the paper's own §3 uses to build the project cost curve.

Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.

Difficulty

The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation $t_j^{(1)} - t_i^{(0)} = y_{ij}$ mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.

Formalization scope

Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.

The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real $\lambda$ ; the paper's assumption $\lambda \ge t_n^{(0)}$ is a hypothesis of every theorem that uses them.

Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints $y_{ij} \le t_j - t_i$ (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of $\delta$ in $t_n^{(0)}$ for $\delta \ge 0$ .

A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking $t^{(0)}$ and $t^{(1)}$ as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.

Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints $y_{ij} \le t_j - t_i$ , which are reusable for the companion mission on the project cost curve.

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Papers presented at the December 1–3, 1959, Eastern Joint IRE-AIEE-ACM Computer Conference, pp. 160–173, 1959. doi:10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), pp. 296–320, 1961. doi:10.1287/opre.9.3.296
P. Brucker and S. Knust, Complex Scheduling, 2nd ed., Springer, 2012. doi:10.1007/978-3-642-23929-8

7 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Critical-Path Planning and Scheduling II: The Project Cost Curve Is Non-Increasing, Piecewise Linear and ConvexResearch Paper

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$ , is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$ . Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$ : an arrow from event $i$ to event $j$ . As in the paper, labels increase along arrows ( $i < j$ for every $(i,j) \in P$ ), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$ , the earliest event times are given by recursion (1):

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$ , and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$ , $b_{ij} \ge 0$ . The project (direct) cost is

\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).

A schedule for $\lambda$ is a pair $(y,t)$ with

\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$ . Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$ , and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$ . The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$ .

Milestones

Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$ .
Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$ .
$\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$ .

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$ . The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$ . The hypotheses $0\le d_{ij}\le D_{ij}$ , $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$ , for every $\lambda \in \Lambda$ . All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

a junk-valued infimum off $\Lambda$ plays no role;
$C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
piecewise linearity requires finitely many pieces that cover all of $\Lambda$ ;
all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$ , as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$ .
Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$ . It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$ . "Every" is false: when all $a_{ij}=0$ , the all-crash durations are optimal for every $\lambda$ .

A complete development needs:

the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
a parametric-LP or polyhedral argument for finitely many linear pieces;
basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

10 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Path-Finding Methods for Linear Programming I: Centering with Weights on the Weighted Central PathResearch Paper

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider the linear program

\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .

The slack of a point $x$ is $s(x)=Ax-b$ , and the interior is $S^0=\{x : Ax>b\}$ , the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$ , the weighted penalized objective is

f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$ .

Write $S_x=\mathrm{diag}(s(x))$ , $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and the centrality are

\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$ , and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$ .

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$ ), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$ ), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$ ), and uniformity $\|\vec g(s)\|_\infty\le2$ .

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$ , let $x^{(old)}\in S^0$ , $s^{(old)}=s(x^{(old)})$ , and

x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$ , then $x^{(new)}\in S^0$ and

\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$ , the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$ , $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$ ,

\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$ , and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$ :

\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$ , $c_r$ and $\sqrt{c_1}$ . The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$ , $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$ , which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$ , $\frac1{4}$ , $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$ , so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$ : without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$ , while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$ , and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$ ; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$ , $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
Size as an upper bound. Definition 4's " $c_1(\vec g)=\|\vec g(s)\|_1$ " is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$ .
Lemma 3's $r$ ranges over $r\ge0$ , and $\gamma(x,w)$ means $\gamma(s(x),w)$ .
Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$ , equal to $0$ for $m=0$ ).
The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$ , spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

6 thms2 active usersReviewed

Convex Optimization Linear algebra Linear Optimization+2·Captain: mikedeng1

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$ , where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$ , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$ , and $1\le n<m$ . For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$ , $W=\mathrm{diag}(w)$ , $W^\alpha=\mathrm{diag}(w_i^\alpha)$ , and $A_s=S^{-1}A$ . For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$ .

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$ , and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$ , with $G(s)=\mathrm{diag}(g(s))$ , $G'(s)$ the Jacobian of $g$ at $s$ , and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$ :

Size: $\|g(s)\|_1\le c_1$ ;
Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$ ;
Step consistency: $c_r\ge1$ and for all $r\ge c_r$ , $y\in\mathbb R^m$ : $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$ ;
Uniformity: $\|g(s)\|_\infty\le2$ .

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$ ,

\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$ , and the resulting $g$ is a weight function with

c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .

Milestones: the three bullets of Theorem 1

Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$ .
Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$ .
Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$ .

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ -iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$ -sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$ . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$ , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$ ) and $A^\top W^\alpha A$ (which defines $g$ ). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$ , $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$ -norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$ , and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$ , and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$ ).
$1\le n<m$ . $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$ ; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
Reading of $\alpha$ : the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$ , giving $\alpha\in(0,1)$ .
Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$ , while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$ ).
The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$ .
$g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$ . Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

7 thms2 active usersReviewed

Computational Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$ . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ( $L_\infty$ ) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$ .

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$ .
1984. Megiddo extends the method to every fixed $d$ , with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$ . Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$ . An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$ , and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$ . Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$ . It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$ , then $A$ row by row, then $b$ . A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$ , answers whether $a^Tx^*<b$ , $=b$ or $>b$ . Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$ , the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

One query settles half of $n$ hyperplanes on the line ( $A(1)=1$ , $B(1)=\tfrac12$ ).
$v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$ , so there is a basis in which all $a_{ij}\ne0$ .
For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$ , $H_k$ .
A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$ , and the middle hyperplane settles one of them.
Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
$C(d)\log n$ queries settle all $n$ hyperplanes.
If a hyperplane contains no optimal point, all optimal points lie on one side of it.
The oracle, Case I: at an optimum relative to $\{x_d=0\}$ , two auxiliary systems decide the side or certify global optimality.
The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$ , systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$ , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$ , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$ . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$ , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$ . The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$ . The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$ . A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$ , where the page's last sentence says $\{x_d<0\}$ . The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$ , the hypothesis its argument uses, since linear independence alone does not give it.
Not included. Approach II and its bound $O(n(\log n)^{d^2})$ , the remarks on slowly growing $d$ , the randomized variants, and the applications of §1.
Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

16 thms5 active usersReviewed

The OR Formalization Drive

Missions

Online Network Revenue Management Using Thompson Sampling: Bayesian Regret of TS-fixedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 against the LP benchmark

Milestones

Significance

Difficulty

Formalization scope

Selected references

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.9, with the proof's constant

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimizing Strategic Safety Stock Placement in Supply Chains: Binding Base Stocks Are Optimal in a Serial System without Guaranteed Internal ServiceResearch Paper

Motivation

Setting

Formalization targets

Goal: the Result, Eq. (A6)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

The conglomerate model

Formalization targets

Goal: Theorem 1 (p. 625)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Regret Algorithms for Online Convex Optimization 1: Logarithmic Regret of Online Gradient DescentResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 175)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Regret Algorithms for Online Convex Optimization 2: Logarithmic Regret of the Online Newton StepResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 with nlog⁡T≥4n\log T\ge4nlogT≥4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Regret Algorithms for Online Convex Optimization 3: Logarithmic Regret of Follow the Approximate LeaderResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Regret Algorithms for Online Convex Optimization 4: Logarithmic Regret of Exponentially Weighted Online OptimizationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7

Milestones

Significance

Difficulty

Goal: Theorem 2 with $n\log T\ge4$