Operations Research

Completed

Combinatorics Graph Theory·Captain: mikedeng1

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 2: Near the Optimal Ratio, a Maximum-Weight Initial Set Is ρ-MaximalResearch Paper

Motivation

The single-machine sequencing problem with precedence constraints, written $1\mid\mathrm{prec}\mid\sum w_jC_j$ , asks for an order of $n$ jobs on one machine that respects a given acyclic digraph of precedences and minimizes the weighted sum of completion times. It is NP-hard in general (Lawler 1978; Lenstra and Rinnooy Kan 1978), and much of its structural theory goes through a decomposition due to Sidney (Sidney 1975): find an initial set of jobs of maximum weight-to-processing-time ratio, schedule it first, and recurse on the rest. Sidney's decomposition underlies the series-parallel algorithm of the same report, the 2-approximation algorithms for the general problem, and the vertex-cover view of Chudak–Hochbaum, Correa–Schulz and Ambühl–Mastrolilli.

The decomposition is only usable if a ratio-maximal initial set can be found efficiently. Section 7 of E. L. Lawler's report Sequencing jobs to minimize total weighted completion time subject to precedence constraints (IRIA-LABORIA Rapport de Recherche No. 205, December 1976; journal version in Annals of Discrete Mathematics 2, 1978) gives the polynomial algorithm: a binary search on the ratio, where each trial value is tested by one minimum-cut computation in an auxiliary network. This mission formalizes the correctness of that procedure.

Timeline.

1970: Rhys (Management Science 17) solves the selection problem, the bipartite case of a maximum-weight closed set, by minimum cut.
1975: Sidney introduces the decomposition into ratio-maximal initial sets.
1976: Lawler (this report) reduces the search for a ratio-maximal initial set to $O(\log n + \log w^* + \log p^*)$ minimum-cut computations.
1976: Picard (Management Science 22) treats the maximal closure of a general graph by the same network.

Setting

A finite set $N$ of $n=|N|$ jobs carries an acyclic digraph $G=(N,A)$ ; job $i$ must precede job $j$ when $G$ has a directed path from $i$ to $j$ . Job $j$ has an integer processing time $p_j\ge1$ and an integer weight $w_j$ of either sign.

An initial set of $N$ is a set $I\subseteq N$ that contains, with each of its jobs, every predecessor of that job. The ratio of a nonempty set is

\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},

and a nonempty initial set $I^*$ is ρ-maximal if $\rho(I^*)\ge\rho(I)$ for every nonempty initial set $I$ . Its ratio $\rho^*$ is the optimal ratio.

For a trial value $\rho$ , the trial weights are $\bar w_j=w_j-\rho p_j$ . A maximum-weight initial set for $\bar w$ is computed in the network $G^*$ : add a source $s$ and a sink $t$ , give the arc $(s,j)$ capacity $\max(0,-w_j)$ , the arc $(j,t)$ capacity $\max(0,w_j)$ , and every arc of $G$ capacity $+\infty$ . An $(s,t)$ cutset is a partition $(S,T)$ of the nodes with $s\in S$ , $t\in T$ , of capacity $c(S,T)=\sum_{i\in S}\sum_{j\in T}c_{ij}$ .

The integer data satisfy $-w^*\le w_j\le w^*$ and $1\le p_j\le p^*$ , and $\varepsilon=1/(np^*)^2$ .

Formalization targets

Goal: the last step of the binary search

If $\rho\le\rho^*\le\rho+\varepsilon$ , then every nonempty initial set $I$ of maximum trial weight,

\sum_{j\in I'}(w_j-\rho p_j)\le\sum_{j\in I}(w_j-\rho p_j)\quad\text{for all initial sets } I',

is ρ-maximal. This is the paper's sentence "At this point the smallest value in the interval is chosen for a trial value ρ. … In either case, the maximum weight initial set I which is determined is ρ-maximal" (pp. 16–17).

Milestones

Finite-capacity cutsets of $G^*$ correspond to initial sets $I=T-\{t\}$ (p. 14).
A finite cutset has capacity $\sum_{j\in N}\max(0,w_j)-\sum_{j\in I}w_j$ (p. 15).
A minimum cutset yields a maximum-weight initial set (p. 15).
Cases 1–3: a maximum-weight set of positive, negative or zero trial weight shows that $\rho$ is too small, too large, or optimal (pp. 15–16).
Every attainable ratio lies in $[-w^*,w^*]$ (p. 16).
Two distinct attainable ratios differ by at least $1/(np^*)^2$ (p. 16).

Significance

The goal is what makes Sidney's decomposition algorithmic: a ρ-maximal initial set can be found by a polynomial number of minimum-cut computations, with the bound $2\log_2 n+\log_2 w^*+2\log_2 p^*+1$ on the number of trial values. Ratio-maximal initial sets are the first step of every Sidney-decomposition-based algorithm for $1\mid\mathrm{prec}\mid\sum w_jC_j$ , and the cut network is the standard reduction of maximum-weight closure to minimum cut, used across open-pit mining, project selection and parametric optimization.

The results are classical and proved in the report. No machine-checked version of the closure–cut correspondence, the ratio-separation bound, or the binary-search correctness is known to exist in Lean or on Prove2Me. The mission produces a reusable formal account of initial sets, the network $G^*$ with infinite capacities, and the parametric test of a ratio.

Difficulty

Each step is short on paper; the difficulty is in the corners the paper does not discuss. The paper's "maximum weight initial set" ranges over all initial sets, and the empty set has weight $0$ . At $\rho=\rho^*$ the empty set is a maximizer and is not ρ-maximal, so the final step needs a nonempty maximizer; and Case 2, read literally over all initial sets, can never occur. The argument at the left end of the interval also needs the separation bound in the right direction: the printed display ends with " $<$ ", while the argument needs " $\ge$ ". Finally, initial sets are closed under predecessors along paths, while a cut only sees single arcs, so the correspondence between finite cuts and initial sets needs the arcs of $G$ to stay inside $N$ .

Formalization scope

Jobs are a Finset N in a type ι; the precedence digraph is a relation G with every arc inside N and no directed cycle, and "must precede" is Relation.TransGen G. Weights and processing times are real in the general statements and integers cast to reals in the integer-data statements. Lean evaluates $\rho(\emptyset)=0/0$ as $0$ ; ρ-maximality and every statement about attainable ratios therefore range over nonempty sets. Capacities take values in WithTop ℝ, with $+\infty=\top$ ; a pair of nodes that is not an arc of $G^*$ has capacity $0$ , and an infinite cut has capacity $\top$ . A cutset is given by its sink side $T\subseteq\{s,t\}\cup N$ .

Added hypotheses and corrected slips, all disclosed in the items:

the goal assumes the maximum-weight initial set $I$ is nonempty (the empty-set corner above);
Cases 2 and 3 maximize over nonempty initial sets;
the separation bound is stated with $\ge$ , against the printed " $<$ ";
the capacity display's first line, printed $\sum_{j\in S}c_{sj}$ , is read as $\sum_{j\in T}c_{sj}$ , as its second line shows;
the interval $[-w^*,w^*]$ and the separation bound are stated for every nonempty subset of $N$ , a slight generalisation.

A trivializing formalization is ruled out: the goal assumes neither Case 1 nor Case 3, nor the separation bound, nor anything about cuts; those appear only as milestones. The running-time statements of §7 and the binary search loop itself are out of scope.

A complete development needs finite sums over finsets, path closure of initial sets, and extended-real arithmetic in WithTop ℝ. The cut network with infinite capacities and the closure correspondence are reusable for any maximum-weight closure problem. Proofs of the milestones, and of the goal from Cases 1 and 3 with the separation bound, are welcome.

Selected references

E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, 1976. https://hal.science/hal-04716371v1 ; journal version Annals of Discrete Mathematics 2 (1978) 75–90, https://doi.org/10.1016/S0167-5060(08)70323-6
J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975) 283–298. https://doi.org/10.1287/opre.23.2.283
J. M. W. Rhys, A selection problem of shared fixed costs and network flows, Management Science 17 (1970) 200–207. https://doi.org/10.1287/mnsc.17.3.200
J.-C. Picard, Maximal closure of a graph and applications to combinatorial problems, Management Science 22 (1976) 1268–1272. https://doi.org/10.1287/mnsc.22.11.1268

11 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 3: The Nonquadratic Method of Multipliers for Linear Equality Constraints ConvergesResearch Paper

Motivation

The method of multipliers (augmented Lagrangian method) of Hestenes and Powell is one of the standard algorithms for constrained convex optimization. Each iteration minimizes the Lagrangian plus a quadratic penalty on the constraint residual, then updates the multiplier estimate. Rockafellar showed in 1976 that this method is the proximal point algorithm applied to the dual problem (Rockafellar, Math. Oper. Res. 1976), which explains its global convergence for convex programs without differentiability or constraint qualifications on the primal side.

The quadratic penalty is not the only one used in practice. Exponential and other nonquadratic penalties produce twice-differentiable augmented Lagrangians and were studied by Kort and Bertsekas and by Tseng and Bertsekas. Eckstein (Math. Oper. Res. 18(1), 1993, 202–226) gave a uniform convergence theory for such methods. He replaces the squared Euclidean distance in the proximal point algorithm by the D-function of a Bregman function $h$ , proves convergence of the resulting algorithm for every maximal monotone operator (Theorem 1), and then derives nonquadratic multiplier methods by applying it to the dual of a convex program. This mission covers the linear-equality-constrained case, §4.1 and Theorem 6 of that paper.

Setting

Let $f : \mathbb R^n \to (-\infty, +\infty]$ be convex and lower semicontinuous, let $A$ be an $m \times n$ matrix, $b \in \mathbb R^m$ , and $X \subseteq \mathbb R^n$ closed and convex, with $\inf\{f(x) \mid x \in X\} < \infty$ . The problem is

\text{minimize } f(x) \quad\text{such that}\quad Ax = b,\ x \in X. \tag{7}

Write $\delta_X$ for the indicator function of $X$ ( $0$ on $X$ , $+\infty$ off $X$ ) and $f_X = f + \delta_X$ . The dual functional is

d(p) = \inf_{x \in X}\bigl\{ f(x) + \langle p, Ax - b\rangle \bigr\}, \qquad p \in \mathbb R^m,

assumed not identically $-\infty$ . An optimal multiplier (Lagrange multiplier) is a maximizer of $d$ over $\mathbb R^m$ .

For an open set $S$ , a Bregman function with zone $S$ is a function $h : \bar S \to \mathbb R$ that is continuously differentiable on $S$ , strictly convex and continuous on $\bar S$ , and satisfies the level-set and limit conditions (iv)–(vi) of Definition 1 on its D-function $D_h(x, y) = h(x) - h(y) - \langle \nabla h(y), x - y \rangle$ . Here the zone is all of $\mathbb R^m$ , and $\nabla h$ is assumed onto $\mathbb R^m$ . Let $h^*(z) = \sup_p\{\langle p, z\rangle - h(p)\}$ be the convex conjugate of $h$ , and let $c_k > 0$ with $\inf_k c_k > 0$ . The nonquadratic method of multipliers generates $\{(x^k, p^k)\}$ by

x^{k+1} \in \operatorname*{arg\,min}_{x \in X}\Bigl\{ f(x) + \tfrac{1}{c_k}\, h^*\bigl(\nabla h(p^k) + c_k(Ax - b)\bigr)\Bigr\}, \qquad p^{k+1} = \nabla h^*\bigl(\nabla h(p^k) + c_k(Ax^{k+1} - b)\bigr). \tag{9}

For $h(p) = \frac12\|p\|^2$ this is the classical method of multipliers. A run of the general Bregman proximal point algorithm for an operator $T$ is a sequence with $\frac{1}{c_k}(\nabla h(x^k) - \nabla h(x^{k+1})) \in T(x^{k+1})$ for all $k$ .

Formalization targets

Goal: Theorem 6 (pp. 212–213)

Under the assumptions above:

\exists\, p^\star \text{ optimal} \;\Longrightarrow\; p^k \to \text{some optimal multiplier, and every limit point of } \{x^k\} \text{ solves (7)};

\nexists\, p^\star \text{ optimal} \;\Longrightarrow\; \{p^k\} \text{ is unbounded}.

The statement fixes no penalty: it holds for every Bregman function with zone $\mathbb R^m$ and surjective gradient. It makes no claim that $\{x^k\}$ converges, which is false in general.

Milestones

Theorem 1 (pp. 206–207): for a maximal monotone $T$ and a Bregman function $h$ with zone $S$ , $\bar S \supseteq \operatorname{dom} T$ , a run of the Bregman proximal point algorithm converges to a zero of $T$ when one exists, under either (C1) $S \supseteq \overline{\operatorname{dom} T}$ or (C2) $T = \partial f$ for a closed proper convex $f$ . If $T$ has no zero and (C1) holds, the run is unbounded.
Proof of Theorem 6, p. 213: the multipliers produced by (9) form a Bregman proximal point run on $\partial(-d)$ ,

p^{k+1} = \bigl(\nabla h + c_k \partial(-d)\bigr)^{-1}\bigl(\nabla h(p^k)\bigr).

Proof of Theorem 6, p. 214: if $p^k \to p^\star$ with $p^\star$ optimal, then $Ax^k \to b$ , and every limit point $x^\infty$ of $\{x^k\}$ satisfies $Ax^\infty = b$ , $-A^{\mathsf T}p^\star \in \partial f_X(x^\infty)$ , and solves (7).

An additional item states the existence clause of Theorem 6: if the row space of $A$ meets $\operatorname{ri}(\operatorname{im} \partial(f + \delta_X))$ , or $f$ and $X$ are polyhedral and the row space meets $\operatorname{im} \partial(f + \delta_X)$ , then (9) has an infinite run from every starting point $(x^0, p^0)$ .

Significance

Theorem 6 gives global convergence of a whole family of augmented Lagrangian methods at once, with the penalty chosen through $h$ . For instance, Example 5 of the paper obtains the method with penalty $\frac{1}{r c_k}\sum_i |\mu_i + c_k(A_i x - b_i)|^r$ for any $r > 1$ . Its multiplier sequence behaves exactly as the dual proximal point iterates do, and it detects dual unsolvability through divergence of $\{p^k\}$ . Primal limit points are optimal without any assumption beyond existence of a Lagrange multiplier.

The result has a published proof (Eckstein 1993) but, to our knowledge, no machine-checked proof. Formalizing it requires a formal treatment of Bregman functions and of the Bregman proximal point algorithm (Theorem 1). It also requires the subdifferential calculus of the dual functional: conjugates, the chain rule $\partial(g \circ A^{\mathsf T})$ , and the inverse relation between $\nabla h$ and $\nabla h^*$ . The milestones isolate the reduction of (9) to Theorem 1 and the primal recovery argument, each of which can be proved independently of the others.

Difficulty

The reduction step is where a direct argument fails. Showing that $p^{k+1}$ is a proximal point of $\partial(-d)$ needs the inclusion $-(Ax^{k+1} - b) \in \partial(-d)(p^{k+1})$ , where $-d(p) = (f_X)^*(-A^{\mathsf T}p) + \langle b, p\rangle$ is a composition of a conjugate with a linear map. The subdifferential chain rule holds with equality only under a qualification condition. The argument must therefore use only the inclusion that holds unconditionally, together with the optimality condition for the $x$ -subproblem, which needs differentiability of $h^*$ everywhere (supplied by $\operatorname{im} \nabla h = \mathbb R^m$ and strict convexity of $h$ ). On the primal side, $\{x^k\}$ need not be bounded or convergent, so primal optimality can only be asserted for limit points, through closedness of the graph of $\partial f_X$ . Theorem 1 itself rests on the Bregman conditions (iv)–(vi), which replace the Fejér monotonicity of the Euclidean proximal point argument.

Formalization scope

$\mathbb R^k$ is EuclideanSpace ℝ (Fin k). $A$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalent to an $m \times n$ matrix), and $A^{\mathsf T}$ is its adjoint. Theorem 1 is stated on any finite-dimensional real inner product space.
Functions into $(-\infty, +\infty]$ are EReal-valued with "never $-\infty$ " as a hypothesis. $\partial f$ uses the published IsSubgradient; convexity is convexity of the epigraph (IsConvexFn). Maximal monotonicity, dom and zer are the published ThreeOpSplitting.Convergence definitions. The conjugate $h^*$ is the published fenchelConjugate, an EReal supremum.
(9) uses the real value of $h^*$ . This is faithful because $\operatorname{im}\nabla h = \mathbb R^m$ makes $h^*$ finite everywhere. Finiteness of $h^*$ is a consequence, never a hypothesis. The arg min in (9) is a minimality predicate, not a choice function, since the minimizer need not be unique.
Recursion (3) is encoded through its equivalent form (4). Condition (vi) of Definition 1 is stated on the natural domain $\bar S \times S$ of $D_h$ .
"Limit point" means subsequential limit, and "unbounded" means the range of the sequence is not bounded. In the existence clause, ri is Mathlib's intrinsicInterior, and polyhedral sets and functions are finite intersections of closed half-spaces (for functions, of the epigraph).
The paper's typo "monontone" in Theorem 1 is read as "monotone".
The convergence claims must not be weakened to their trivial instances. A formalization that assumes $\{x^k\}$ converges, or adds finiteness of $h^*$ or boundedness of $\{p^k\}$ as a hypothesis, or encodes (9) with a choice function, does not state Theorem 6.
Reusable beyond this mission: the Bregman function structure and Theorem 1 (shared with the other missions of this series), and the dual-functional and conjugate facts for linearly constrained programs. Contributions toward the conjugate calculus ( $\nabla h^* = (\nabla h)^{-1}$ , the chain rule inclusion) are welcome.

Selected references

J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1) (1993) 202–226. https://doi.org/10.1287/moor.18.1.202
R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2) (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
Y. Censor, S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3) (1992) 451–464. https://doi.org/10.1007/BF00940051
P. Tseng, D. P. Bertsekas, On the convergence of the exponential multiplier method for convex programming, Mathematical Programming 60 (1993) 1–19. https://doi.org/10.1007/BF01580598

9 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Residual Life Time at Great Age 5: If |c − ((1 − F)/F′)′| ≤ ε for t ≥ t₀, the Residual Life Normed by (1 − F(t))/F′(t) Is Within ε of Π_{0,c} for t ≥ t₀Research Paper

Motivation

The residual life time of a lifetime $X$ at age $t$ is the excess $X - t$ given survival, $X > t$ . How it behaves at great ages is a question in reliability (remaining life of an item that has already lasted long), in insurance and demography (remaining life at old age), and in the peaks-over-threshold method of extreme value statistics, where exceedances over a high threshold are modelled by a generalized Pareto law.

Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974) 792–804) determined every possible limit law of the suitably normed residual life as $t \to \infty$ , and their domains of attraction. For continuous limits, the classical sufficient conditions are von Mises' conditions (1936) on the derivative of $(1 - F)/F'$ . Section 4 of the paper goes further: it gives inequalities that hold at every finite age $t \ge t_0$ , not only in the limit. This mission formalizes that finite- $t$ result, the Corollary to Theorem 7.

Timeline: von Mises (1936) gives sufficient conditions for domains of attraction of extreme value laws; Balkema and de Haan (1974) prove the limit theorems for residual life and the finite- $t$ bounds formalized here; Pickands (1975, Ann. Statist. 3, 119–131) proves the corresponding approximation by the generalized Pareto law for excesses, the result now known as the Pickands–Balkema–de Haan theorem.

Setting

Let $X$ be a real random variable with distribution function $F$ . The residual life distribution function at age $t$ is

F_t(x) = P\{X - t \le x \mid X > t\}.

Assume $F$ has a positive, differentiable density $F'$ for $t \ge t_0$ , and define the norming function

a(t) = \frac{1 - F(t)}{F'(t)} \qquad (t \ge t_0),

the reciprocal of the hazard rate. The normed residual life is $(X - t)/a(t)$ given $X > t$ , with distribution function $P\{(X - t)/a(t) \le x \mid X > t\} = F_t(x\,a(t))$ .

The comparison laws are the distribution functions $\Pi_{0,c}$ , $c \in \mathbb R$ , all vanishing for $x < 0$ :

for $c > 0$ , $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $x \ge 0$ (a generalized Pareto law);
for $c = 0$ , $\Pi_{0,0}(x) = \Pi(x) = 1 - e^{-x}$ for $x \ge 0$ (the exponential law);
for $c < 0$ , $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $0 \le x \le |c|^{-1}$ , and $1$ beyond (bounded support).

Formalization targets

Goal: the Corollary to Theorem 7

If $c \ge 0$ and $\varepsilon \ge 0$ satisfy $|c - a'(t)| \le \varepsilon$ for $t \ge t_0$ , then

\left|\Pi_{0,c}(x) - P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\}\right| \le \varepsilon \qquad \text{for all } x \text{ and all } t \ge t_0 .

Milestones

The bounds (13): if $c_1 \le a' \le c_2$ on $[t_0, \infty)$ , then $1 + c_1 x \le a(t + x a(t))/a(t) \le 1 + c_2 x$ for $t \ge t_0$ , $x \ge 0$ .
The exponential representation

P\left\{\frac{X - t}{a(t)} > x \,\middle|\, X > t\right\} = \frac{1 - F(t + x a(t))}{1 - F(t)} = \exp\left(-\int_0^x \frac{a(t)}{a(t + s a(t))}\, ds\right).

Theorem 7: if $c_1 \le a'(t) \le c_2$ for $t \ge t_0$ , then

\Pi_{0,c_2}(x) \le P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\} \le \Pi_{0,c_1}(x) \qquad (t \ge t_0,\ x \in \mathbb R).

$\sigma(u) = u^{-2}(e^{-u} - 1 + u) = \int_0^1\int_0^t e^{-us}\,ds\,dt$ is positive and decreasing.
Lemma 4: $0 \le -(\partial/\partial c)\Pi_{0,c}(x) < 1$ for $c > -1$ , $x \ne 0$ , $cx \ne -1$ .
$|\Pi_{0,c}(x) - \Pi_{0,c_0}(x)| \le |c - c_0|$ for $c \ge 0$ and all real $c_0$ , $x$ .

The goal is the Corollary because it is the paper's final statement of Section 4: a single parameter $c$ and a single error $\varepsilon$ , with no limit taken. Theorem 7 is the stronger two-parameter sandwich it rests on.

Significance

The result. Theorem 7 and its Corollary are a quantitative, non-asymptotic form of the von Mises condition $\frac{d}{dt}\frac{1-F(t)}{F'(t)} \to c$ . If the derivative of the reciprocal hazard stays within $\varepsilon$ of $c$ from age $t_0$ on, then at every such age the normed excess distribution is uniformly within $\varepsilon$ of the generalized Pareto (or exponential) law $\Pi_{0,c}$ . Letting $\varepsilon \to 0$ along $t_0 \to \infty$ recovers convergence to $\Pi_{0,c}$ , and the bound itself quantifies the error of the generalized Pareto approximation used in threshold-exceedance modelling.

Formalizing it. The result is proved in the paper (1974), with short proofs. To our knowledge no part of it has a machine-checked proof. The mission produces checked versions of the theorem, the corollary and the elementary lemmas about the family $\Pi_{0,c}$ : its monotonicity and Lipschitz dependence on the parameter $c$ , including across the case change at $c = 0$ . Those facts about the generalized Pareto family are reusable in any formal development of extreme value statistics.

Difficulty

The analytic content is elementary, but several steps hide case analysis. The Lipschitz bound in $c$ requires the derivative of $\Pi_{0,c}(x)$ in $c$ across $c = 0$ , where the formula changes from $1 - (1+cx)^{-1/c}$ to $1 - e^{-x}$ , and across the boundary $cx = -1$ of the support when $c < 0$ , where the function is not differentiable. The bound $-\partial_c \Pi_{0,c} < 1$ is not a crude estimate: it reduces to the comparison $\sigma(u) < \sigma(-\psi)$ for the function $\sigma(u) = u^{-2}(e^{-u} - 1 + u)$ , which needs its strict monotonicity on all of $\mathbb R$ , including $u = 0$ where the closed form is undefined. In Theorem 7 the lower bound $1 + c_1 x$ in (13) becomes negative for $c_1 < 0$ and large $x$ ; this is exactly where the comparison law $\Pi_{0,c_1}$ reaches $1$ , and the argument must handle it. The orientation is easy to get wrong: the upper bound $c_2$ on the derivative gives the lower bound $\Pi_{0,c_2}$ , since $\Pi_{0,c}(x)$ decreases in $c$ .

Formalization scope

The source is the published Annals of Probability article (DOI 10.1214/aop/1176996548); page numbers are the journal's.

The law of $X$ is a probability measure μ on ℝ, $F$ is Mathlib's cdf μ, and $F_t(x) = \mu((t, t+x]) / \mu((t, \infty))$ . The normed probability $P\{(X-t)/a(t) \le x \mid X > t\}$ is $F_t(x\,a(t))$ .
"Positive, differentiable density for $t \ge t_0$ " is: for $t \ge t_0$ , cdf μ has derivative $f(t) > 0$ and $f$ has derivative $f'(t)$ , both within $[t_0, \infty)$ ; nothing is assumed to the left of $t_0$ .
The derivative $\frac{d}{dt}a(t)$ is a named function $a'$ with HasDerivWithinAt on $[t_0, \infty)$ ; it is the derivative the density hypothesis already provides, so this adds no assumption. Bare deriv is not used.
Completion of $\Pi_{0,c}$ for $c < 0$ . The paper (p. 801) prints the formula only for $0 \le x \le |c|^{-1}$ . The formalization sets $\Pi_{0,c}(x) = 1$ for $x > |c|^{-1}$ , as "distribution function" requires and as the proof of Lemma 4 uses (" $\Pi_{0,c}(x)$ is constant on both components of $\{c > -1\}\setminus R$ "). The formula gives $1$ at $x = |c|^{-1}$ , so the completion is continuous.
$\Pi_{0,0}$ is a separate branch ( $1 - e^{-x}$ ), not the formula with $1/0$ .
$\sigma$ is defined as $\int_0^1\int_0^t e^{-us}\,ds\,dt$ , and the closed form $u^{-2}(e^{-u} - 1 + u)$ for $u \ne 0$ is part of milestone 4. "Decreasing" is stated as strictly decreasing, which is what the proof of Lemma 4 uses ( $\sigma(u) < \sigma(-\psi)$ ).
Lemma 4 states the differentiability of $c \mapsto \Pi_{0,c}(x)$ at $c$ together with the bound $0 \le -d < 1$ on its derivative $d$ .
The bounds (13) are stated in both printed forms.
No sign condition is added on $c_1, c_2$ in Theorem 7; $c_1$ may be any real number, and $c - \varepsilon$ in the Corollary may be negative.

A trivializing formalization is ruled out: the conclusion is a bound at every real $x$ and every $t \ge t_0$ with $a(t) > 0$ , the conditional probability divides by $\mu((t,\infty)) > 0$ (which the density hypothesis implies), and the hypotheses are satisfied by, for example, the exponential law ( $a \equiv 1$ , $c = 0$ ) and the Pareto law $1 - (1+x)^{-\alpha}$ ( $a(t) = (1+t)/\alpha$ , $c = 1/\alpha$ ).

A complete development needs the fundamental theorem of calculus with one-sided derivatives, a change of variables in interval integrals, and calculus of Real.rpow in the exponent parameter. The lemmas on $\Pi_{0,c}$ and $\sigma$ are reusable beyond this mission; proofs of any milestone are welcome independently.

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

10 thms3 active usersReviewed

Dynamic Programming Machine Learning Probability+1·Captain: mikedeng1

Stable Function Approximation in Dynamic Programming II: In a Nondiscounted MDP with All Policies Proper, Value Iteration Through a Self-Weighted Averager ConvergesResearch Paper

Motivation

Value iteration solves a Markov decision process by repeatedly applying the Bellman backup to a table of state values. When the state space is too large for a table, the values are stored in a function approximator instead: each backup is followed by a fit, and the fitted function is backed up again. This approximate value iteration is the basis of fitted dynamic programming and of much of reinforcement learning, and it was known in the early 1990s to diverge for common approximators such as linear regression and neural networks (Boyan and Moore, 1995, cited in the report as [BM95]).

Gordon's technical report (Stable Function Approximation in Dynamic Programming, CMU-CS-95-103, 1995; conference version at ICML 1995) identified a class of approximators, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a grid), for which the combination is stable. For discounted problems stability follows from a norm argument. For nondiscounted problems, where the backup contracts only in a weighted norm, that argument fails, and the report proves convergence by a different route: approximate value iteration is exact value iteration on a derived MDP. This mission formalizes that route and its conclusion, Corollary 4.1 (p. 11).

Setting

A finite nondiscounted Markov decision process $M$ has non-goal states $x=1,\dots,n$ , a finite nonempty action set $U(x)$ at each state, an expected one-step cost $c_{xa}$ , and transition probabilities $p_{axy}\ge 0$ with $\sum_y p_{axy}\le 1$ . The missing mass $1-\sum_y p_{axy}$ is the probability of moving to a cost-free absorbing goal state, which the paper calls state $1$ . A value function is a vector $V\in\mathbb R^n$ ; the goal's value is $0$ . The parallel value backup is

(T_M V)(x)=\min_{a\in U(x)}\Bigl[c_{xa}+\sum_y p_{axy}V(y)\Bigr],

and with a discount factor $\gamma$ the sum is multiplied by $\gamma$ . A policy $\mu$ chooses an admissible action at each state; it is proper if, from every starting state, the probability of having reached the goal after $t$ steps tends to $1$ .

An averager $A$ consists of constants $k_y$ , nonnegative weights $\beta_y$ and nonnegative weights $\beta_{yz}$ ( $z$ ranging over all states, the goal included) with $\beta_y+\sum_z\beta_{yz}=1$ . Its mapping is $M_A(V)(y)=\beta_yk_y+\sum_z\beta_{yz}V(z)$ . Two operators $M_F$ and $T$ are compatible if $(M_F\circ T)^k(V_0)$ converges from every initial guess $V_0$ .

The derived MDP $M'$ has the same states and actions, transition probabilities $p'_{axz}=\sum_y p_{axy}\beta_{yz}$ to non-goal states $z$ , the rest of the mass going to the goal, and costs $c'_{xa}=c_{xa}+\gamma\sum_{y}p_{axy}\beta_yk_y$ .

The states are layered by distance from the goal: $S_1=\{1\}$ , $U_k=\bigcup_{j<k}S_j$ , and $S_k$ is the set of states outside $U_k$ from which every action reaches $U_k$ with positive probability. Write $k(x)$ for the index of the layer containing $x$ . The averager is self-weighted for $M$ if for every state $y$ either $\beta_y>0$ or $\beta_{yx}>0$ for some state $x$ with $k(x)\le k(y)$ .

Formalization targets

Goal: Corollary 4.1 (p. 11)

If every policy of $M$ is proper and $A$ is self-weighted for $M$ , then for every initial guess $V_0$ both

(M_A\circ T_M)^k(V_0)\quad\text{and}\quad(T_M\circ M_A)^k(V_0)

converge as $k\to\infty$ . The first is the page's " $T_M$ and $M_A$ are compatible", the second its "approximate value iteration … will converge".

Milestones

Theorem 4.1 (Derived MDP, p. 7): $T_{M'}=T_M\circ M_A$ , for every discount factor and for the nondiscounted backup.
Exhaustiveness (p. 10, after [BT89]): if all policies of $M$ are proper, every state lies in some layer $S_k$ .
$M'$ terminates (p. 10): if all policies of $M$ are proper and $A$ is self-weighted, there is $m>0$ such that under every policy of $M'$ and from every state the goal is reached within $m$ steps with positive probability; in particular every policy of $M'$ is proper.
Theorem 2.3 (p. 4), in its all-policies-terminate case: value iteration converges from any initial guess. This is the published, proved item BertsekasDP.ssp_main_theorem.

A further item, Theorem 6.1 (p. 12), says the limit is $V^*$ when the optimal value function is a fixed point of $M_A$ , under self-weighting or under positive costs with $k\ge 0$ .

Significance

The corollary gives a checkable, purely combinatorial condition on the approximator and the transition graph under which fitted value iteration on a stochastic shortest path problem cannot diverge. Weight decay ( $\beta_y>0$ everywhere) and any averager that only ever averages a state's value with values no farther from the goal satisfy it. The derived-MDP identity, Theorem 4.1, is the tool the rest of the report builds on (§5, §6.1, Appendix A): it reduces questions about approximate dynamic programming with averagers (convergence, the limit's error, the online Q-learning variant) to questions about an ordinary MDP.

The results are proved in the report, in prose. They have no machine-checked version. The formal development needed here is a finite stochastic shortest path theory (proper policies, the layer partition, termination bounds) on top of the published model BertsekasSSPModel and the proved BertsekasDP.ssp_main_theorem.

Difficulty

The obvious argument fails. If all policies of $M$ are proper, $T_M$ contracts in some weighted max norm, and $M_A$ is a nonexpansion in the unweighted max norm, but $M_A$ can expand the weighted norm, so the composition need not contract. Figure 4 of the report gives a three-state chain and an averager, replacing $V(2)$ by $V(3)$ , for which approximate value iteration diverges. The proof therefore has to go through $M'$ and show that self-weighting makes $M'$ terminate under every policy. That is a probabilistic statement about all, possibly nonstationary, policies of a new process, derived from a layer structure of the old one. Exhaustiveness of the layers itself needs a policy-construction argument.

Formalization scope

The MDP is the published BertsekasSSPModel n C: non-goal states Fin n, a finite action type C with admissible sets M.U i, costs M.g, and transition probabilities M.p whose deficit is the probability of termination. Gordon's state 1 is this implicit termination state: its value is $0$ by construction, and where the partition and the averager's goal weight need to name it, it is none : Option (Fin n). This realises the page's two "without loss of generality" steps (state 1 cost-free and absorbing; $\beta_1=1$ , $k_1=0$ ). The nondiscounted backup is BertsekasSSPBellmanOp M, the discounted one BertsekasDiscountedBellmanOp M γ.

The averager acts on whole value functions over the state set. An approximator that fits only a sample $X_0$ of states is the special case $\beta_{yx}=0$ for $x\notin X_0$ . "All policies proper" quantifies over stationary policies μ : Fin n → C with admissible actions, as on p. 3. Self-weightedness is stated through layer membership, which agrees with the page's $k(x)$ whenever the partition is exhaustive (milestone 2). Theorem 6.1 takes $V^*$ as a real fixed point of the backup; under either of its cases such a fixed point is unique and optimal. Convergence is in $\mathbb R^n$ , which is the same as convergence in max norm.

The goal's hypotheses concern $M$ and $A$ only. A formalization that assumed properness of the derived MDP, dropped the "every action" quantifier in the layers (making the partition and self-weighting weaker notions), or dropped $k(x)\le k(y)$ (making every averager with a positive weight self-weighted) would be a different theorem.

Reusable beyond this mission: the layer partition and its exhaustiveness, and the termination bound for the derived model, are general finite stochastic shortest path facts. Contributions to any milestone are welcome, and so are proofs of the definitions-level lemmas they rely on.

Selected references

G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995. Conference version in Proceedings of the 12th International Conference on Machine Learning (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. ([BT89] in the report.)
D. P. Bertsekas and J. N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, Morgan Kaufmann, 1995. ([BM95] in the report.)

8 thms3 active usersReviewed

Optimization Probability Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 3: With One Markdown or Markup Allowed, Thresholds x_n < z_n Give the Optimal PolicyResearch Paper

Motivation

Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.

Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).

Setting

There are three prices $p_1 < p < p_2$ . At price $p_i$ demand is a Poisson process of intensity $\lambda_i$ , and at $p$ of intensity $\lambda$ , with

\lambda_1 > \lambda > \lambda_2, \qquad r_1 > r > r_2, \qquad r_i = p_i\lambda_i,\ r = p\lambda,

all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section $p_1$ is the lower price; the initial price is $p$ .

A seller with $n$ units and time-to-go $t$ sells at $p$ and may switch once, to $p_1$ or to $p_2$ . Write $N(\cdot)$ for the demand process at $p$ and $N_i(\cdot)$ for that at $p_i$ .

$J^i(n,t;s) = (p - p_i)E\min(n,N(s)) + p_iE\min(n, N(s) + N_i(t-s))$ is the expected revenue of switching to $p_i$ after $s$ time units.
$J(n,t;0) = \max\{J^1(n,t;0), J^2(n,t;0)\}$ is the revenue of switching at once to the better alternative, and $J(n,t;t) = pE\min(n,N(t))$ the revenue of never switching.
The optimal revenue is

J(n,t) = \sup_{\tau \in \mathcal T} E\bigl[p\min(n,N(\tau)) + J(n - N(\tau), t - \tau; 0)\bigr],

where $\mathcal T$ is the set of stopping times of the history of $N$ with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.

$G^i(n,t) = r - r_i - p_i(\lambda - \lambda_i)P(N_i(t) \ge n)$ .
$\Delta^i(n,t) = J(n,t;t) - J^i(n,t;0)$ and $\Delta(n,t) = J^1(n,t;0) - J^2(n,t;0)$ , with first positive zeros $t^i_n$ and $t_n$ .

Formalization targets

Goal: Theorem 3 (pp. 1385–1386)

Under the paper's assumption $t^1_n < t_n < t^2_n$ for every $n$ , there are strictly increasing sequences $(x_n)$ , $(z_n)$ with

x_n < t^1_n < t_n < t^2_n < z_n

such that $J(n,t) = V(n,t)$ , where $V(n,t) = J(n,t;0) + F(n,t)$ for $x_n \le t \le z_n$ and $V(n,t) = J(n,t;0)$ otherwise. The excess $F(n,\cdot)$ equals $H^1(n,\cdot)$ on $[x_n,t_n]$ and $H^2(n,\cdot)$ on $[t_n,z_n]$ . Each $H^i$ solves

\frac{\partial H}{\partial t} = -\lambda H + L^i(n,t), \qquad L^i(n,t) = G^i(n,t) + \lambda\bigl[V(n-1,t) - J^i(n-1,t;0)\bigr],

with $H^1(n,x_n) = 0$ and $H^2(n,t_n) = H^1(n,t_n)$ . The thresholds are $x_n = \inf\{t \ge 0 : L^1(n,t) = 0\}$ and $z_n = \inf\{t \ge t_n : H^2(n,t) \le 0\}$ .

Milestones

(16), p. 1385: $\partial J^i(n,t;0)/\partial t = r - \lambda[J^i(n,t;0) - J^i(n-1,t;0)] - G^i(n,t)$ .
Lemma 2, p. 1379, in both cases: the zeros of $G(n,\cdot)$ increase strictly in $n$ , and $G(n,\cdot)$ changes sign exactly once.
Lemma 3, p. 1382, in both cases: $J(n,t;t) - J(n,t;0)$ changes sign exactly once at a strictly increasing sequence $t_n$ , and is monotone beyond it.
Lemma 1, p. 1378: a verification criterion identifying $J(n,t)$ as the solution of a system of differential equations and inequalities.

Significance

Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With $m$ units left and time-to-go $u$ , the seller marks down at once when $u$ falls below $x_m$ , marks up at once when $u$ exceeds $z_m$ , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of $2n$ numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.

Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.

Difficulty

The value $J(n,t)$ is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock $n+1$ are defined through $V(n,\cdot)$ , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that $L^1(n+1,\cdot)$ again has a single sign change, which requires $V(n,\cdot) - J^1(n,\cdot;0)$ to be increasing beyond $x_n$ . One must also know that $H^2(n+1,\cdot)$ is positive up to $t^2_{n+1}$ and eventually negative, so that $z_{n+1}$ is finite, and that $z_n < z_{n+1}$ . These facts concern three different price pairs at once: $(p,p_1)$ , $(p,p_2)$ and $(p_1,p_2)$ . A direct comparison of $V$ with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on $V$ matters.

Formalization scope

Model. Demand at $p$ is the counting process of i.i.d. exponential interarrival times from the published definition QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and $N_i(t-s)$ enters only through its law: the sum $N(s) + N_i(t-s)$ is written through its Poisson $(\lambda s + \lambda_i(t-s))$ law. $\mathcal T$ is the class of real-valued stopping times $\tau$ of the σ-algebras generated by the counts $N(u)$ , $0 \le u \le s$ , with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.
Conventions. Time is time-to-go, $t \ge 0$ ; ODEs are imposed at every $t > 0$ through HasDerivAt. Threshold sequences are indexed from $n = 1$ . Every infimum is a real sInf paired with the nonemptiness of its set. $F$ , $H^1$ , $H^2$ , $V$ and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption $t^1_n < t_n < t^2_n$ is a hypothesis of the goal, as on the page.
Added hypotheses. Prices and intensities are positive, the paper's standing convention. Lemma 1 as printed is false. It is stated with the boundary condition $V(n,0) = J(n,0;0)$ , the zero-stock condition $V(0,t) = 0$ , the obstacle condition $V \ge J(\cdot;0)$ , and local Lipschitz continuity of $V$ in place of "continuous and almost everywhere differentiable". The page's proof uses all four. Lemma 2's printed "bounded" is corrected to "bounded away from zero", since $y_n \to \infty$ .
No trivialization. No statement assumes the optimality identity, the verification conditions, the derivative identity (16), or any sign-change fact as a hypothesis. A goal that defined $V$ and assumed $J = V$ , or that left the thresholds unrelated to $L^1$ and $H^2$ , would not be Theorem 3.
Infrastructure needed. Poisson tail calculus (differentiation of $E\min(n, N(t))$ in $t$ ), variation-diminishing properties of the kernel $e^{-\lambda(t-u)}$ , linear first-order ODEs, and a martingale decomposition for Poisson counting processes evaluated at bounded stopping times. Contributions of any of these, or of proofs of the milestones, are welcome.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8):1371–1391, 1995. https://doi.org/10.1287/mnsc.41.8.1371
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
S. Karlin, Total Positivity, Vol. 1, Stanford University Press, 1968.
G. Bitran and R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003. https://doi.org/10.1287/msom.5.3.203.16031

10 thms3 active usersReviewed

Optimization Probability Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 2: Markup Is Optimal Once Time-to-Go Exceeds an Increasing Threshold z_nResearch Paper

Why a promotional fare needs a switching rule

An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.

The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.

Demand, inventory, and admissible decisions

There are $n\ge1$ items and $t\ge0$ units of time-to-go. At price $p_i$ , sales requests follow a Poisson counting process $N_i$ with rate $\lambda_i$ . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has

0<p_1<p_2,\qquad 0<\lambda_2<\lambda_1,\qquad p_2\lambda_2<p_1\lambda_1.

The salvage value at the end of the horizon is zero. A fixed switch at time $s\in[0,t]$ charges $p_1$ first and $p_2$ afterwards. Its expected revenue, denoted $J(n,t;s)$ , is

J(n,t;s)=(p_1-p_2)\sum_{j=1}^n\Pr\{N_1(s)\ge j\} +p_2\sum_{j=1}^n\Pr\{N_1(s)+N_2(t-s)\ge j\}.

The two counts in the last term are independent, so their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . This is the expression in §3 of the paper. In particular, $J(n,t;0)$ is the revenue from increasing the price immediately.

An admissible switching time $\tau$ uses only the history of sales at $p_1$ ; it lies between zero and $t$ and cannot wait past stock exhaustion. The optimal value $J(n,t)$ is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.

Formalization targets

The goal is Theorem 2 on pp. 1382–1383. Define the switching function

G(n,t)=p_1\lambda_1-p_2\lambda_2 -p_2(\lambda_1-\lambda_2)\Pr\{N_2(t)\ge n\}, \qquad y_n=\inf\{u\ge0:G(n,u)=0\}.

There are thresholds $x_n,z_n$ with $y_n\le x_n<z_n$ , and $(z_n)_{n\ge1}$ is increasing. A continuation premium $F$ gives the value

J(n,t)=\begin{cases} J(n,t;0)+F(n,t),&t<z_n,\\ J(n,t;0),&t\ge z_n. \end{cases}

For $n\ge1$ , $F(n,t)=H(n,t)$ below $z_n$ and is zero at or above it; $F(0,t)=0$ . The function $H$ satisfies $H(n,0)=0$ and the differential equation $\partial_tH(n,t)=-\lambda_1H(n,t)+L(n,t)$ , where $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ . The remaining thresholds are the first nonnegative zero of $L(n,\cdot)$ and the first positive zero of $H(n,\cdot)$ :

x_n=\inf\{u\ge0:L(n,u)=0\},\qquad z_n=\inf\{u>0:H(n,u)=0\}.

The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of $G$ , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.

What the result supplies

The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for $z_n$ : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for $F$ and $H$ , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.

Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.

Where the difficulty lies

The immediate-switch comparison $G(n,t)$ has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For $n>1$ , the relevant forcing term is $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , so the sign of $G$ alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.

Formalization scope

The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as $\min(n,N_1(\tau))$ , equal almost surely to $N_1(\tau)$ for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.

Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for $y_n$ , $x_n$ , and $z_n$ is nonempty; it also keeps $u>0$ in the definition of $z_n$ , since $H(n,0)=0$ . Continuity of $H(n,\cdot)$ at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; $y_n$ is unbounded as stock grows. These choices are recorded for review in the moderation notes.

The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Optimization Theoretical Computer Science·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments IV: Uniform Pricing Earns OPT/(1 + ln(v_m/v_1)) in Unit-Demand Min-PricingResearch Paper

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ( $\mathrm{UDP}_{\min}$ ). There are items $[n]$ and consumers $[m]$ , $m\ge 1$ . Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$ . Given a price assignment $p:[n]\to\mathbb R_{>0}$ , consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$ , and nothing otherwise. The seller's revenue is

\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$ , and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$ . Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$ , $S\subseteq\mathcal C$ , with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$ , (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$ , and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$ . With revenues $r:\mathcal C\to\mathbb R_{>0}$ , an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$ . If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$ , revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$ .

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$ , $r((x,v))=m\,v$ , and $\mathcal P=\frac1m\sum_i\mathcal P_i$ , where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$ , $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$ .

Formalization targets

Goal: Corollary 4.7

\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$ , $\rho:=v_m/v_1$ ", stated in product form.

Milestones

Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
Prices to assortments: for valuation-valued $p$ , $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
Theorem 3.2 for an arbitrary regular model:

\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$ . More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$ . The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$ , which receive the paper's " $+\infty$ " price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$ ; the reduction to a regular model is what supplies it.

Formalization scope

Items and consumers are finite types X and M, with Nonempty M ( $m\ge1$ ). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ( $r=m\,v>0$ ) and its ratio $v_m/v_1$ need positivity.
A consumer with $B_i=\emptyset$ pays $0$ . Ties among cheapest items do not affect payments, so payments are defined directly.
$\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$ . Uniform pricing ranges over all $q>0$ , not only valuations.
The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ , and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$ , which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$ ; $\ln$ is Real.log applied to ratios $\ge1$ .
Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

Selected references

G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
A. Aouad, V. Farias, R. Levi and D. Segev, The approximability of assortment optimization under ranking preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1754

13 thms3 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Inventory Control and Price Theory 2: For Style Goods with Uniform Demand Linear in Unit Profit, Expected Profit Is Maximized at P* = ((P₀ − 3L) + √((3L − P₀)² + 16P₀L))/4Research Paper

Pricing and stocking a perishable good

A retailer of style goods — seasonal clothing, newspapers, anything that loses most of its value when the selling period ends — must decide before the season how many units to stock, knowing demand only as a probability distribution. Units left over are liquidated at a loss; units short are sales forgone. This single-period trade-off is the newsvendor problem, and its solution, the critical-fractile rule, is one of the first results of stochastic inventory theory.

In practice the retailer also sets the price, and the price moves the demand distribution. T. M. Whitin's 1955 paper Inventory Control and Price Theory (DOI 10.1287/mnsc.2.1.61) is one of the first to put the two decisions into one model. Its Section 3 restates the critical fractile for a given price, then lets the demand distribution depend on the unit profit and asks for the unit profit and stock that jointly maximize expected profit. For one explicit family of demand laws it solves the problem in closed form. This joint price-setting newsvendor problem later grew into a large literature (Mills 1959, Karlin and Carr 1962, and the survey of Petruzzi and Dada 1999), which cites Whitin's model as its starting point.

Setting

There is one selling period. Stock $x \ge 0$ is on hand at its start. Each unit sold earns the unit profit $P$ ; each unit left over at the close is liquidated at the unit liquidation loss $L > 0$ .

Demand depends on the unit profit through its mean. The mean demand is the linear function

\mu(P) = k\,(P - P_0),

where $P_0 > 0$ is the unit profit at which demand falls to zero and $k$ is the reciprocal of the slope of the line relating unit profit and amount demanded. Demand decreases in $P$ , so $k < 0$ , and the admissible unit profits are $0 < P < P_0$ . At unit profit $P$ , demand $X$ has the rectangular (uniform) distribution on $[0, 2\mu(P)]$ .

The expected marginal profit of the $x$ -th unit is $f(x) = P\,\Pr(X \ge x)$ , the probability that it sells weighted by the unit profit, and the expected marginal loss is $g(x) = L\,\Pr(X < x)$ , the probability that it does not sell weighted by the liquidation loss. The expected profit of stocking $x$ units at unit profit $P$ is the area between them,

E(P, x) = \int_0^x \big[f(t) - g(t)\big]\,dt,

which is the expected profit on sales minus the expected liquidation loss. The equilibrium stock is

x_M(P) = -\frac{2kP(P_0 - P)}{P + L}.

Formalization targets

Goal: the optimal unit profit (Eq. (16))

With

P^* = \frac{(P_0 - 3L) + \sqrt{(3L - P_0)^2 + 16P_0L}}{4},

one has $0 < P^* < P_0$ , and for all $0 < P < P_0$ and all $x \ge 0$

E(P, x) \le E\big(P^*, x_M(P^*)\big),

with equality only at $(P, x) = (P^*, x_M(P^*))$ . The formula for $P^*$ involves only $P_0$ and $L$ : the optimal unit profit is independent of the demand slope $k$ .

Milestones, in the order of the paper

Eq. (8) — for a general demand law, profit is maximized at the stock whose probability of being sold is $L/(G + P + L)$ ( $G$ a goodwill loss per unit short). This is already proved on the platform as SupplyChainTheory.chain_optimal_fractile and enters as a reference.
Eq. (11) — on $0 \le x \le 2\mu(P)$ , $f(x) = \frac{P}{2k(P_0 - P)}x + P$ and $g(x) = \frac{-L}{2k(P_0 - P)}x$ .
Eqs. (10), (13) — on the same range, $E(P, x) = \frac{P + L}{4k(P_0 - P)}x^2 + Px$ .
Eqs. (9), (12) — $x_M(P)$ lies in $(0, 2\mu(P))$ , is the only stock with $f = g$ , and is the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ .
Eq. (14) — $E(P, x_M(P)) = -kP^2(P_0 - P)/(P + L)$ .
Eq. (15) — the derivative of $P \mapsto E(P, x_M(P))$ vanishes exactly when $2P^2 + (3L - P_0)P - 2P_0L = 0$ .
Footnote 7 — the elasticity of mean demand at $P^*$ equals $P^*/(P_0 - P^*)$ , and it tends to $1$ as $P_0 \to \infty$ with $L$ fixed.

Significance

The goal is a complete closed-form solution of a joint pricing-and-stocking problem under uncertainty: one price and one stock level, explicitly, with a proof that no other pair does as well. The independence of the optimal unit profit from $k$ says that, in this family, the scale of the market does not affect the optimal margin; only the ratio of the zero-demand margin to the liquidation loss does. Footnote 7 relates the optimum to the classical monopoly rule (unit elasticity) in the limit of a negligible liquidation loss.

Whitin's derivation is calculus on closed forms and was never stated as a theorem with hypotheses. He calls the stationary point of (15) "the optimal $P$ " without checking that it is a maximum, that it is global, or that the stock beyond the support of demand cannot do better. The formalization fixes all three: the goal is a statement of global, unique optimality over the whole admissible region. No machine-checked proof of this result, of the price-setting newsvendor, or of the uniform-demand newsvendor exists on the platform; the general critical-fractile rule (8) is the only part of Section 3 already proved there.

Difficulty

The expected profit is defined from the demand law, so the closed forms (11) and (13) must be derived from the uniform distribution — probabilities of half-lines under a conditioned Lebesgue measure, and an interval integral of the resulting piecewise-linear functions. They hold only on the support of demand; beyond $2\mu(P)$ the marginal profit is $0$ and the marginal loss is $L$ , and the global statement must cover that region too.

The pricing step is where the paper is loose. Setting the derivative of (14) to zero gives a quadratic with two real roots, and a stationary point of a function on an open interval need not be its maximum. The goal asks for the global maximum over $0 < P < P_0$ and its uniqueness, and asks that it be the global maximum of the joint problem, not only of the reduced function $P \mapsto E(P, x_M(P))$ .

Formalization scope

All quantities are real numbers; stock is continuous, as in the paper's calculus. Mean demand is meanDemand k P₀ P = k * (P - P₀) and the paper's sign convention is kept: $k < 0$ is a hypothesis of every statement, as are $L > 0$ and $0 < P < P_0$ (or $P_0 > 0$ where $P$ is not fixed). The demand law is ProbabilityTheory.cond volume (Set.Icc 0 (2 * μ)); $f$ and $g$ use $\Pr(X \ge x)$ and $\Pr(X < x)$ ; $E$ is an interval integral defined for every $x$ .

The paper's loose phrases are read as follows. "Equation (9) may be solved for $x$ " becomes uniqueness of the root of $f - g$ on $x \ge 0$ ; "the equilibrium value of $x$ " becomes the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ ; "differentiating (14)" becomes a HasDerivAt statement with the explicit derivative for $P \mapsto E(P, x_M(P))$ , together with the equivalence with (15); "solving (15) gives the optimal $P$ " becomes the goal's joint global maximum with equality case; "independent of $k$ " is the shape of the formula for $P^*$ ; "as $P_0$ becomes large relative to $L$ , the optimal elasticity approaches unity" becomes a limit as $P_0 \to \infty$ with $L$ fixed.

Defining $E$ by the closed form (13) instead of from the demand law would make milestones (11) and (13) tautologies and would change the model beyond the support of demand; this formalization rules that out. The paper's goodwill loss $G$ belongs to the fixed-price model of (8) and does not appear in $E$ .

A complete development needs the uniform distribution's tail probabilities, interval integrals of piecewise-linear functions, and one-variable calculus for the quadratic and the cubic $P^2(P_0 - P)/(P + L)$ ; the uniform-law lemmas are reusable for any newsvendor problem with uniform demand. Proofs of the milestones, and alternative arguments for the goal, are welcome.

Selected references

T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 61–68, 1955. https://doi.org/10.1287/mnsc.2.1.61
E. S. Mills, Uncertainty and Price Theory, Quarterly Journal of Economics 73(1), 116–130, 1959. https://doi.org/10.2307/1883828
S. Karlin and C. R. Carr, Prices and Optimal Inventory Policy, in Arrow, Karlin and Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 159–172, 1962.
N. C. Petruzzi and M. Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Eq. (14.8) (the critical fractile, formalized on the platform as SupplyChainTheory.chain_optimal_fractile).

9 thms3 active usersReviewed

Completed

Analysis Optimization·Captain: mikedeng1

Inventory Control and Price Theory 1: With Linear Demand and Economic Lot Sizes, the Profit-Maximizing Price Satisfies the Cubic (7)Research Paper

Motivation

Inventory calculations often take the selling price as fixed, while price calculations often treat the cost of supplying demand as independent of the order policy. Whitin's 1955 model connects the two decisions in one annual-profit calculation. A merchant chooses both the price charged to customers and the size of each replenishment order. Changing the price changes annual demand; changing demand changes the number of orders, inventory carrying cost, and therefore the economic lot size. This makes the selling price and the inventory decision parts of the same optimization problem. Whitin's paper gives a compact example in which the connection can be written down explicitly.

The mission concentrates on Section 2, the stationary-demand model for a stable item. Section 3 of the paper studies style goods under uncertain sales and belongs to a separate mission. The result here concerns a deterministic annual demand curve and continuous order quantities, so a solver can focus on the interaction between a classical economic order quantity calculation and a price first-order condition.

Setting

The price is a real number $p$ . Annual demand is the linear function $D(p)=ap+b$ , where $a$ and $b$ are given real constants. A feasible price has $D(p)>0$ . The paper does not require $a<0$ in its displayed model, so the formal statements leave the slope unrestricted. Negative $a$ is the economically usual decreasing-demand case; in other regimes a joint maximum may simply fail to exist.

The merchant pays a fixed setup cost $S$ whenever an order is placed. The purchase cost per unit is $C$ , and the annual carrying charge for one unit kept in stock is $IC$ , where $I$ is a carrying-rate factor. If $Q>0$ units are ordered each time, average stock is $Q/2$ and the annual number of orders is $D/Q$ . A per-unit operating cost $k$ is incurred on annual demand, and $f$ is an annual fixed cost. The resulting total variable cost and two-variable annual profit are

\operatorname{TVC}(D,Q)=\frac Q2 IC+\frac DQ S+kD, \qquad \Pi(p,Q)=D(p)p-\operatorname{TVC}(D(p),Q)-f.

Only pairs with $D(p)>0$ and $Q>0$ are feasible. For a fixed demand level, the economic lot size is $Q^*(D)=\sqrt{2DS/(IC)}$ . Substituting it into profit gives Whitin's reduced profit

P(p)=ap^2+bp-\sqrt{2SIC(ap+b)}-k(ap+b)-f.

The paper uses $P$ for annual profit in this section. The Lean development calls the two-variable function profit and the function after optimizing $Q$ reducedProfit.

Formalization targets

The first target is the unique lot-size minimum in Eq. (3), followed by its value in Eq. (4):

\operatorname{TVC}(D,Q^*(D))\leq\operatorname{TVC}(D,Q) \quad(Q>0),\qquad \operatorname{TVC}(D,Q^*(D))=\sqrt{2DSIC}+kD.

Equality in the inequality holds only at $Q=Q^*(D)$ . The next target is the necessary stationarity condition in Eqs. (6)–(7): when $D(p)>0$ and the derivative of $P$ at $p$ is zero,

8a^3p^3+(16a^2b-8ka^3)p^2 +(10ab^2-12ka^2b+2k^2a^3)p +2b^3-4kab^2+2k^2a^2b-SICa^2=0.

The goal joins these steps at a global joint maximum. If a feasible pair $(p,Q)$ maximizes $\Pi$ over all feasible price and lot-size pairs, then $Q=Q^*(D(p))$ and $p$ satisfies the cubic. The goal is an implication about any joint maximizer; it does not assert that one exists for every demand curve. The cubic is a necessary condition only. Its algebraic roots may include prices that fail the original first-order equation or fail to maximize profit.

Significance

The result gives a concrete relation between a price chosen to maximize annual profit and the ordering cost and carrying charge of the inventory system. The lot-size formula alone optimizes cost at a fixed demand rate. The cubic makes the demand response to price and the resulting inventory cost visible in the price condition. It also specifies what can be inferred from the calculation: an optimal price must satisfy the equation, while selecting an optimum from candidate roots remains a separate question.

The paper already supplies the mathematical result. The formalization task is to represent the joint optimization and verify its necessary conditions in Lean, together with the cost identity on which the reduced-profit expression rests. The published Prove2Me definition InventoryControl_eoq already provides the classical EOQ cost and square-root quantity; this mission uses its cost function and adds Whitin's demand curve and profit. Related inventory results for backorders and multilevel systems describe different models and do not replace the targets here.

Difficulty

At a fixed price, choosing the lot size involves both a term proportional to $Q$ and one proportional to $1/Q$ . The optimality statement needs a global inequality and a unique equality case, not merely the observation that a derivative vanishes. After substituting that quantity, the reduced profit contains a square root of the demand curve. Its derivative is meaningful on positive demand, and turning its stationarity equation into the displayed cubic loses information when an equation is squared. A proof therefore has to preserve the implication from optimality to the cubic without promoting all cubic roots to optima.

Formalization scope

The model uses real prices, real demands, and real lot sizes; it does not round order quantities to integers. The hypotheses $S,I,C>0$ make explicit the positive cost and carrying-charge conventions of Section 2. Neither $k$ nor $f$ is assigned a sign, and no sign is imposed on $a$ or $b$ . The conditions $Q>0$ and $D(p)>0$ apply to every cost or profit comparison. They exclude Lean's total value for division by zero and the zero value assigned by Real.sqrt to a negative argument. The goal quantifies over every feasible pair in a joint maximum of the original profit, so optimizing $Q$ is part of its content. Defining profit only by the reduced formula would erase that claim.

The definitions comprise linear demand, total variable cost, two-variable profit, and reduced profit. The classical EOQ cost comes from the existing InventoryControl_eoq definition; the model-specific layer is small and can be reused in further work on pricing with inventory costs. The theorem targets welcome proofs of the global lot-size inequality, the minimized-cost identity, the stationary cubic, and their combination at a joint maximizer. The paper's quantity-discount footnote is outside this scope because it leaves the revised purchase and carrying-cost model unspecified.

Selected references

T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 1955, pp. 61–68. DOI: 10.1287/mnsc.2.1.61.

6 thms3 active usersReviewed

Combinatorics Graph Theory·Captain: mikedeng1

An Introduction to Timetabling 1: Every Class–Teacher Requirement Matrix Has a Timetable over Any p Days with Every Daily Load and Pair Count Between ⌊r/p⌋ and ⌈r/p⌉Research Paper

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.

The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.

Timeline (as cited in the review).

1916. D. König proves that a bipartite multigraph of maximum degree $\Delta$ can be edge-coloured with $\Delta$ colours. The review states it as Proposition 2.1, citing Berge's Graphes [1].
1975. D. de Werra, "A few remarks on chromatic scheduling" (reference [37] of the review), gives the balanced version: for every $p$ the edges of a bipartite multigraph can be $p$ -coloured so that every node and every bundle of parallel edges is balanced. This is Proposition 2.3.
1978. D. de Werra, "Some comments on a note about timetabling" (INFOR, reference [38]), gives the weekly version with daily load limits, Proposition 2.2.
1985. The review collects the three results in matrix form as problems CT1, CT2 and CT3 and sketches a network-flow construction for CT3, citing Krarup [19].

Setting

There are $m$ classes $c_1,\dots,c_m$ and $n$ teachers $t_1,\dots,t_n$ . The requirement matrix $R=(r_{ij})$ is an $m\times n$ matrix of nonnegative integers: $r_{ij}$ is the number of lectures class $c_i$ must have with teacher $t_j$ . Write $r_{i\cdot}=\sum_j r_{ij}$ for the total load of class $c_i$ and $r_{\cdot j}=\sum_i r_{ij}$ for that of teacher $t_j$ . For nonnegative integers $s$ and $p\ge1$ , $\lfloor s/p\rfloor$ and $\lceil s/p\rceil$ are the floor and ceiling of the rational $s/p$ .

A schedule over $p$ periods or days is an array $x=(x_{ijk})$ of nonnegative integers ( $i\le m$ , $j\le n$ , $k\le p$ ) that places every lecture exactly once:

\sum_{k=1}^p x_{ijk}=r_{ij}\quad\text{for all } i,j. \tag{1}

CT1 asks in addition that $x_{ijk}\in\{0,1\}$ and that $\sum_j x_{ijk}\le1$ , $\sum_i x_{ijk}\le1$ : no class and no teacher has two lectures in one period.
CT2, given positive integers $a_i$ , $b_j$ , asks that $\sum_j x_{ijk}\le a_i$ and $\sum_i x_{ijk}\le b_j$ on every day $k$ .
CT3 asks that on every day $k$

\Big\lfloor \tfrac{r_{i\cdot}}{p}\Big\rfloor\le\sum_j x_{ijk}\le\Big\lceil \tfrac{r_{i\cdot}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{\cdot j}}{p}\Big\rfloor\le\sum_i x_{ijk}\le\Big\lceil \tfrac{r_{\cdot j}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{ij}}{p}\Big\rfloor\le x_{ijk}\le\Big\lceil \tfrac{r_{ij}}{p}\Big\rceil. \tag{8–10}

In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.

Formalization targets

Goal: Proposition 2.3

\forall\,R\in\mathbb N^{m\times n},\ \forall\,p\ge1:\quad \exists\,x,\ \ x \text{ solves CT3 for } R \text{ over } p \text{ days}.

The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.

Milestones

One balanced day (flow sketch, p. 153): for $p\ge1$ there is a matrix $y$ satisfying the bounds (8), (9), (10) at once.
The remaining days stay balanced (same sketch): if $p\ge2$ and $\lfloor s/p\rfloor\le y\le\lceil s/p\rceil$ , then $\lfloor s/p\rfloor\le\lfloor (s-y)/(p-1)\rfloor$ and $\lceil (s-y)/(p-1)\rceil\le\lceil s/p\rceil$ .
Proposition 2.1 (König): CT1 is solvable iff $r_{\cdot j}\le p$ and $r_{i\cdot}\le p$ for all $i,j$ .
Proposition 2.2: CT2 is solvable iff $r_{\cdot j}\le p\,b_j$ and $r_{i\cdot}\le p\,a_i$ .
Minimum number of days: CT2 is solvable over $p$ days iff $p\ge\max\big(\max_j\lceil r_{\cdot j}/b_j\rceil,\max_i\lceil r_{i\cdot}/a_i\rceil\big)$ .
Figure 1: the printed timetable for $R=\begin{pmatrix}1&2&4\\3&0&2\end{pmatrix}$ , $p=3$ , solves CT3.

Significance

The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take $p$ at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.

Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.

Difficulty

Each family of constraints alone is easy: spreading a single number $r_{ij}$ evenly over $p$ days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average $r_{ij}/p$ satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.

Formalization scope

Classes, teachers and days are Fin m, Fin n, Fin p; $R$ and $x$ are natural-number valued, which is the paper's " $x_{ijk}\ge0$ integer". Constraint (4) of CT1 is written $x_{ijk}\le1$ . Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is $0$ , and is stated as an equivalence ("solvable over $p$ days iff $p\ge p_{\min}$ ") rather than as an infimum.

Disclosed choices:

The goal and the one-day milestone assume $p\ge1$ ; the paper's "for any $p$ " means any number of days, and for $p=0$ Lean's division returns $0$ .
The remaining-days milestone assumes $p\ge2$ so that $p-1$ days remain.
Propositions 2.1, 2.2 and the minimum-days statement hold for every $p$ , including $p=0$ , and assume nothing more than the page: $a_i,b_j$ positive.
The edge-colouring and network-flow readings of the paper are stated in prose only; the formal statements are in matrix form, which is how the propositions are stated.

The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for $R=(2)$ and $p=1$ .

Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.

Selected references

D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Mathematische Annalen 77 (1916) 453–465. https://doi.org/10.1007/BF01456961
C. Berge, Graphes, Gauthier-Villars, Paris, 1983 (reference [1] of the review).
D. de Werra, A few remarks on chromatic scheduling, in B. Roy (ed.), Combinatorial Programming: Methods and Applications, Reidel, Dordrecht, 1975, 337–342.
D. de Werra, Some comments on a note about timetabling, INFOR 16 (1978) 90–92.
J. Krarup, Chromatic optimisation: Limitations, objectives, uses, references, European Journal of Operational Research 11 (1982) 1–19.

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

An Introduction to Timetabling 2: When Every Teacher Is Available in at Most Two Periods, Limited Backtracking Finds a Timetable or Correctly Reports That None ExistsResearch Paper

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In the class–teacher model, classes and teachers must be brought together for a prescribed number of lectures, each lecture occupies one period, and nobody can be in two places at once. With no further side constraints the model reduces to edge colouring of a bipartite multigraph and is solved exactly by König's theorem. Real instances, however, come with preassignments (a class and a teacher must meet at a fixed period) and unavailabilities (a teacher or a class cannot be scheduled at some periods). With these, deciding whether a daily timetable exists is NP-complete, as the paper records citing Even, Itai and Shamir (1976).

D. de Werra's invited review An introduction to timetabling (European Journal of Operational Research 19, 1985) surveys this landscape. In its §2.2 it isolates one restricted case that is easy: when every teacher is available during at most two periods, a limited backtracking method finds a timetable or proves that none exists (Proposition 2.4, attributed to [9], Even–Itai–Shamir). The Remark that follows recasts the procedure as a decision method for stable sets of half the vertices in graphs with a perfect matching, which is the 2-satisfiability problem in graph form.

Setting

There are $m$ classes $c_1,\dots,c_m$ , $n$ teachers $t_1,\dots,t_n$ and $p$ periods of one day. After removing the preassigned lectures, $\bar r_{ij}\in\mathbb N$ lectures of class $c_i$ with teacher $t_j$ remain; $\bar b_{ik}\in\{0,1\}$ is $1$ exactly when class $c_i$ is available and not preassigned at period $k$ ; $\bar c_{jk}\in\{0,1\}$ is $1$ exactly when teacher $t_j$ is available and not preassigned at period $k$ . A timetable (a solution of CT4) is a $0/1$ array $\bar x_{ijk}$ with

\sum_{k}\bar x_{ijk}=\bar r_{ij},\qquad \sum_{j}\bar x_{ijk}\le\bar b_{ik},\qquad \sum_{i}\bar x_{ijk}\le\bar c_{jk}.

A possible schedule of $t_j$ is the slice $y_{ik}=\bar x_{ijk}$ of a candidate array that satisfies the constraints involving $t_j$ alone. The conflict graph $G$ has one node per pair (teacher, possible schedule); two nodes are linked when they are different schedules of the same teacher or put the same class in the same period. When each teacher has exactly two schedules, they are written $x_j$ and $\bar x_j$ , and in Lean the nodes are (j, true) and (j, false) of Fin n × Bool.

The limited backtracking works on such a graph. The implications $\mathrm{cl}(S)$ of a set $S$ of chosen nodes form the least set containing $S$ such that whenever $u$ is in it and $u$ is linked to a node $w$ of another teacher, the other node of $w$ 's teacher is in it. A state is either $\mathrm{run}(A)$ , with $A$ the nodes fixed so far, or $\mathrm{fail}$ . From $\mathrm{run}(A)$ , for any teacher not yet fixed and any first choice $b$ of its node:

if $\mathrm{cl}(A\cup\{(j,b)\})$ is independent, the procedure moves there;
otherwise, if $\mathrm{cl}(A\cup\{(j,\lnot b)\})$ is independent, it moves there;
otherwise it fails.

Formalization targets

Goal: correctness of the limited backtracking

For every $n$ and every graph $G$ on $\mathrm{Fin}\,n\times\mathrm{Bool}$ in which $x_j$ and $\bar x_j$ are linked for all $j$ :

\begin{aligned} &\text{(1) the move relation is well founded from } \mathrm{run}(\emptyset);\\ &\text{(2) every reachable } \mathrm{run}(A) \text{ with an unfixed teacher has a move};\\ &\text{(3) a reachable } \mathrm{run}(A) \text{ with all teachers fixed has } A \text{ a set of } n \text{ pairwise non-adjacent nodes};\\ &\text{(4) if } \mathrm{fail} \text{ is reachable, } G \text{ has no set of } n \text{ pairwise non-adjacent nodes.} \end{aligned}

All four clauses range over every run of the nondeterministic procedure.

Milestones

A teacher available in at most $2$ periods has at most $2$ possible schedules.
CT4 has a solution iff its conflict graph has $n$ pairwise non-adjacent nodes.
The implications of chosen nodes lie inside every timetable that contains those nodes.
If $A$ is independent and closed under implications, $G$ has a timetable iff it has one containing $A$ .
In a graph $G=(X,E)$ with a perfect matching $M$ , a stable set has at most $|X|/2$ nodes, and one of exactly $|X|/2$ nodes contains one endpoint of every edge of $M$ .

Significance

Proposition 2.4 identifies a polynomial special case inside a scheduling problem that the paper cites as NP-complete in general (Even–Itai–Shamir [9]). The correctness of the procedure is what makes that special case tractable. Milestones 1 and 2 reduce the timetabling instance to a graph question, and the goal settles the graph question. Milestone 4 is the reason the method needs to undo only the last decision. It is the graph form of the autarky principle of 2-SAT solving: a closed, consistent partial assignment can always be kept. Milestone 5 extends the method from timetables to any graph with a perfect matching.

On the formal side, no machine-checked treatment of this reduction or of the backtracking argument exists on the platform; 2-SAT, unit propagation and autarky have no items there either. The statements are proved in the paper only in prose, and the propagation and autarky arguments are compressed into a few sentences. A formal proof makes the invariants explicit: what is closed, what is independent, and why a contradiction after a reversed decision is global.

Difficulty

Soundness of a successful run is an invariant argument. Soundness of failure is the hard part. The naive argument "both choices for $t_j$ lead to a contradiction, hence no timetable" is wrong in general backtracking, because an earlier decision might be at fault, and full backtracking would revisit it. The proof has to show that an earlier permanent decision never needs revisiting. This requires that the set of fixed nodes is closed under implications and independent, so that no unscheduled teacher is linked to it. This invariant must be maintained through both the keep and the reverse moves. Termination and progress are routine but must be stated: without them the correctness clauses hold for a procedure that never moves. On the CT4 side, the reduction must check that the class constraint $(13)$ with $\bar b_{ik}\in\{0,1\}$ splits exactly into per-teacher availability and pairwise disjointness of schedules.

Formalization scope

Data. $\bar r,\bar b,\bar c$ are taken as data; the preassignments that produce them are not modelled. Indices are Fin m, Fin n, Fin p; $0/1$ variables are Bool.
Schedules. The page's "each teacher has exactly 2 possible schedules" holds only after its normalisation. The milestone states the faithful bound $\le 2$ . The CT4-to-graph equivalence is stated for every instance, so its graph has $\sum_j\#\{\text{schedules of }t_j\}$ nodes rather than $2n$ .
Procedure. The implications are an inductive predicate with no iteration bound. A contradiction is a non-independent set of implications, checked against previously fixed nodes as well. The move relation is an inductive Step with one constructor for each of keep, reverse and fail, so the choice of teacher and of first schedule stays arbitrary.
Not formalized. The $O(n^2)$ running time of Proposition 2.4 and of the Remark has no machine model or constant on the page; termination stands in for it.
Ruled out. A goal with only clauses (3)–(4) would be satisfied by a relation with no moves, and a fixed choice rule would prove a weaker statement. The goal therefore includes termination and progress and quantifies over every run.
Needed infrastructure. Mathlib's SimpleGraph, IsIndepSet, IsNIndepSet, Subgraph.IsPerfectMatching, Relation.ReflTransGen and Acc. The autarky lemma (Milestone 4) and the propagation lemma (Milestone 3) are reusable for any 2-SAT-type development. Proofs of the milestones, and a bridge from the CT4 instance to the abstract graph on Fin n × Bool in the exactly-two-schedules case, are welcome.

Selected references

D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
S. Even, A. Itai, A. Shamir, On the complexity of timetable and multicommodity flow problems, SIAM Journal on Computing 5 (1976) 691–703. https://doi.org/10.1137/0205048
B. Aspvall, M. F. Plass, R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters 8 (1979) 121–123. https://doi.org/10.1016/0020-0190(79)90002-4

8 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research IV: Optimum Phase Times of a Two-Phase Fixed-Time Signal — When the Minimum Cycle Minimizes Average Delay, and the Optimum OtherwiseResearch Paper

Motivation

A fixed-time traffic signal is set by two numbers per phase: how long the green lasts and, through the other phase's green, how long the red lasts. Traffic engineers in the early 1950s set signals by Adams' formula, the shortest cycle that can clear the arriving traffic, on the working assumption that the shortest feasible cycle also gives the least delay. J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259), the paper that also introduced the two Wardrop principles of route choice, tested that assumption analytically for a two-phase signal with uniform arrivals. Appendix IV shows that the shortest cycle is optimal only under an explicit condition on the flows, and gives the optimal cycle when the condition fails. Its numerical example (p. 339) lengthens the cycle by 75 per cent and reduces the overall mean delay by 11 per cent, a case that arises when one phase serves a minor road.

The question was taken up by F. V. Webster's 1958 delay formula and optimum-cycle rule for random arrivals, which became the standard practice; the deterministic two-phase analysis here is its uniform-flow precursor.

Setting

A two-phase signal serves two streams. For phase $k \in \{1,2\}$ :

$q_k$ is the arriving flow (vehicles per unit time);
$p_k$ is the saturation flow, the rate at which a queue discharges at minimum headway;
$a_k$ is the lost time, the delay of the first vehicle at the start of green;
$g_k$ is the green time and $r_k$ the red time, with $r_1 = g_2$ and $r_2 = g_1$ .

The totals are $Q = q_1 + q_2$ , $A = a_1 + a_2$ , and the cycle time $c = g_1 + g_2$ . Vehicles do not accumulate indefinitely on phase $k$ when the green, less its lost time, can clear one cycle's arrivals: $q_k c \le p_k(g_k - a_k)$ . Equality on both phases (both greens saturated) gives Adams' formula

c = \frac{A}{1 - q_1/p_1 - q_2/p_2}. \tag{12}

The flow-weighted average delay at the intersection is

T = \frac{1}{2Qc}\left\{\frac{q_1(r_1+a_1)^2}{1 - q_1/p_1} + \frac{q_2(r_2+a_2)^2}{1 - q_2/p_2}\right\}. \tag{16}

Appendix IV changes variables to the effective-red fractions $x = (r_1+a_1)/c$ and $y = (r_2+a_2)/c$ . With

\xi = 1 - \frac{q_1}{p_1},\quad \eta = 1 - \frac{q_2}{p_2},\quad \lambda = \frac{Aq_1}{2Q\xi},\quad \mu = \frac{Aq_2}{2Q\eta},

one has $c = A/(x+y-1)$ , the no-accumulation conditions become $x \le \xi$ and $y \le \eta$ , and

T(x,y) = \frac{\lambda x^2 + \mu y^2}{x + y - 1}.

The feasible region is $F = \{(x,y) : x \le \xi,\ y \le \eta,\ x + y > 1\}$ . Its corner $(\xi,\eta)$ is the minimum cycle (12). The phases are labelled so that $\lambda \ge \mu$ .

Formalization targets

Goal: the optimum phase times

Put

D = \frac{\mu}{\lambda}\eta^2 + 2\xi(1-\eta) - \xi^2, \qquad x_0 = 1 - \eta + \sqrt{(1-\eta)^2 + \frac{\mu}{\lambda}\eta^2}.

For $\lambda \ge \mu > 0$ , $0 < \xi, \eta < 1$ and $\xi + \eta > 1$ :

D > 0 \implies T(\xi,\eta) = \min_{F} T, \qquad D \le 0 \implies (x_0,\eta) \in F \text{ and } T(x_0,\eta) = \min_F T.

At $D = 0$ , $x_0 = \xi$ , so the second formula gives the minimum cycle. This boundary case belongs to the page's final “if this condition is not satisfied” clause.

Milestones (Appendix IV, in the order of the argument)

The partial derivatives at the corner:

\left[\frac{\partial T}{\partial x}\right]_{\xi,\eta} = \frac{\lambda\xi^2 - \mu\eta^2 - 2\lambda\xi(1-\eta)}{(\xi+\eta-1)^2},\qquad \left[\frac{\partial T}{\partial y}\right]_{\xi,\eta} = \frac{\mu\eta^2 - \lambda\xi^2 - 2\mu\eta(1-\xi)}{(\xi+\eta-1)^2}.

If both are negative, $(\xi,\eta)$ minimizes $T$ over $F$ .
When $\lambda \ge \mu$ , $(\xi+\eta-1)^2[\partial T/\partial y]_{\xi,\eta} = -\mu\{2\eta(1-\eta) + (\xi-\eta)^2\} - (\lambda-\mu)\xi^2 < 0$ .
$[\partial T/\partial x]_{\xi,\eta} < 0$ if and only if $D > 0$ .
If $D < 0$ , $x_0$ is the unique root of $\lambda x^2 - \mu\eta^2 - 2\lambda x(1-\eta) = 0$ in $0 < x < \xi$ .

Companions

Adams' formula (12) and the minimality of its cycle; the change of variables from (16) to $T(x,y)$ ; and the translation into the original quantities: $\lambda \ge \mu$ iff $1/q_1 - 1/p_1 \le 1/q_2 - 1/p_2$ , $D > 0$ iff $q_1(1 - q_1/p_1) - q_2(1 - q_2/p_2) < 2q_1q_2/p_2$ , and the delay-minimizing cycle $c = A/\sqrt{(q_2/p_2)^2 + (q_2/q_1)(1 - q_1/p_1)(1 - q_2/p_2)}$ when $D \le 0$ .

Significance

The result gives a closed-form test for whether the minimum cycle is the delay-optimal cycle of a two-phase fixed-time signal with uniform flows, and the optimal cycle when it is not. It shows that the common assumption, shortest cycle equals best cycle, can fail, and identifies when: the test depends on the flow ratios and on which phase is the heavier one in the sense of $1/q - 1/p$ . In the failing case the optimum keeps the minor phase saturated and lengthens only the major phase's green.

The result is proved on the page by a short calculus argument. It has not been machine-checked anywhere known to this mission. The formal work is to establish the global optimality claims behind the page's local reasoning, to pin down the hypotheses the page uses silently (positivity of flows and lost times, the capacity condition, the phase labelling), and to correct the printed slips listed under Formalization scope. The reparametrization and the original-quantity forms tie the abstract statement back to signal settings.

Difficulty

The page argues locally: at the corner both partial derivatives are negative, and "the only possible changes in $x$ and $y$ are reductions", so $T$ is a minimum. Negative partial derivatives at a corner of the region show that no small reduction helps; they do not by themselves exclude a better point far from the corner. The global claim needs a property of $T$ on the whole region $x + y > 1$ , not just at one point. The second case has the same issue: the page locates a critical point on the edge $y = \eta$ and needs, in addition, that no interior or other boundary point does better. The algebra of the corner criterion is routine; the global minimality is the step that carries the content.

Formalization scope

All quantities are real numbers. The objects are delayT lam mu x y $= T(x,y)$ , feasibleXY xi eta $= F$ , cornerD $= D$ , edgeRoot $= x_0$ , the maps xiOf, etaOf, lamOf, muOf from the flows to $\xi,\eta,\lambda,\mu$ , and avgDelay16, the right side of (16). Derivatives are stated with HasDerivAt on the one-variable sections of $T$ ; minimality is the explicit inequality $T(\cdot) \le T(z)$ for every $z \in F$ .

Conventions and added hypotheses, each presupposed by the page:

$x + y > 1$ is part of $F$ : it is $c > 0$ through $c = A/(x+y-1)$ . Without it, $T$ would take Lean's junk value $0$ on the line $x + y = 1$ and negative values beyond it, and the minimum would be meaningless.
$\xi + \eta > 1$ , i.e. $q_1/p_1 + q_2/p_2 < 1$ : the minimum cycle is positive and $F$ is nonempty. Without it both parts of the goal hold vacuously.
$0 < \xi$ , $0 < \eta$ ( $q_k < p_k$ ), $\lambda, \mu > 0$ , and the labelling $\lambda \ge \mu$ , which the page imposes by interchanging the phases. Case 1 of the goal is false without $\lambda \ge \mu$ .
In the companions: $0 < q_k < p_k$ , $Q = q_1 + q_2 > 0$ , and positive total lost time $A$ (or $A \ne 0$ for Adams' formula), which keeps the divisions in (12) and in $c = A/(x+y-1)$ from being junk.

The goal is stated in $\lambda,\mu,\xi,\eta$ alone, which is all Appendix IV uses; the companions connect them to the flows.

Printed slips, corrected in the Lean and named in each item: $(\xi+\eta)^2$ for $(\xi-\eta)^2$ in the expression for $\partial T/\partial y$ (p. 359); the range " $0 < x < \eta$ " for $0 < x < \xi$ (p. 359); " $\ge$ " for $\le$ in the original-quantity form of $\lambda \ge \mu$ (p. 359); and " $c + a$ ", " $a/(x+y-1)$ ", " $\eta = 1 - q_1/p_1$ " for $c + A$ , $A/(x+y-1)$ , $\eta = 1 - q_2/p_2$ (p. 358).

Stating the goal as "the partial derivatives at $(\xi,\eta)$ are negative" would replace the theorem by its mechanism; the goal is minimality over the whole feasible region. Not covered: the delay formula (13) and its heuristic derivation in Appendix III, the approximation (14), and the rounded numerical example of p. 339.

Contributions are welcome on every milestone and companion. General facts about functions of the form $(\lambda x^2 + \mu y^2)/(x+y-1)$ on the half-plane $x + y > 1$ are reusable beyond traffic signals.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II, 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
A. J. H. Clayton, Road traffic calculations, Journal of the Institution of Civil Engineers 16 (1941), p. 247. Cited by Wardrop (his ref. 7) as the source of Adams' formula and of the delay formulae.
F. V. Webster, Traffic signal settings, Road Research Technical Paper No. 39, HMSO, London, 1958.

7 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Revenue Management Under a General Discrete Choice Model of Consumer Behavior 3: The Multinomial Logit Model Has the Nesting-by-Fare-Order PropertyResearch Paper

Motivation

Airline and hotel revenue management sells one perishable resource (seats on a flight, rooms on a night) through several fare products at different prices. The classical models of Littlewood (1972), Belobaba (1989) and Lee and Hersh (1993) assume independent demand: a customer who wants fare class $j$ either buys class $j$ or leaves, whatever else is on offer. Under that assumption the optimal booking policy is nested by fare order: at any time the firm opens a top segment $\{1, \dots, k\}$ of the fare ladder, and closes classes from the cheapest upwards as capacity becomes scarce.

Real customers substitute. If the cheap fare is closed, some buy up; if a mid-priced fare is open, some buy down. Talluri and van Ryzin (working paper 2001; published as Management Science 50(1), 2004) model this with a general discrete choice model: the firm chooses which set $S$ of fares to offer, and a customer buys product $j$ with probability $P_j(S)$ . Their §3 asks when the fare-order nesting of the independent model survives under choice behaviour. They give a characterization (Theorem 2, the subject of mission 2 of this series) and verify it for two models: the independent demand model (Proposition 5) and the multinomial logit (MNL) model (Proposition 6). The MNL model is the standard choice model in travel demand forecasting and marketing (Ben-Akiva and Lerman, 1985), so Proposition 6 says that the fare-order structure airlines already implement remains optimal under the most widely used substitution model.

Setting

There are $n$ fare products $N = \{1, \dots, n\}$ with revenues $r_1 \ge r_2 \ge \dots \ge r_n \ge 0$ . A choice model assigns to each offer set $S \subseteq N$ numbers $P_j(S) \ge 0$ with $\sum_{j\in S} P_j(S) \le 1$ and $P_j(S) = 0$ for $j \notin S$ ; the remainder $P_0(S) = 1 - \sum_{j\in S} P_j(S)$ is the no-purchase probability. Write $Q(S) = \sum_{j\in S} P_j(S)$ for the purchase probability and $R(S) = \sum_{j \in S} r_j P_j(S)$ for the expected revenue.

The complete sets are $A_k = \{1, \dots, k\}$ , $k = 0, 1, \dots, n$ , with $A_0 = \emptyset$ . A choice model has the nesting-by-fare-order property (Definition 4) if

$Q$ is increasing: $Q(S) \le Q(T)$ whenever $S \subseteq T$ ; and
for every $x_1 \ge x_2 \ge \dots \ge x_n$ , the problem $\max_{S\subseteq N} \sum_j x_j P_j(S)$ has an optimal solution that is complete.

In the single-resource dynamic program, $x_j = r_j - \Delta V$ for the marginal value $\Delta V$ of capacity, so condition 2 says that the optimal offer set is always a top segment of the fare ladder.

The MNL model with preference weights $w_j = e^{u_j} > 0$ and no-purchase weight $w_0 = 1$ is

P_j(S) = \frac{w_j}{\sum_{i\in S} w_i + 1}, \qquad j \in S. \qquad (14)

The independent model is $P_j(S) = q_j$ for $j \in S$ . A set $T$ is dominated (Definition 1) if some randomization over offer sets has no larger expected purchase probability and strictly larger expected revenue, or strictly smaller purchase probability and no smaller revenue.

Formalization targets

Goal: Proposition 6, in the form its proof establishes

\forall\, w \in \mathbb{R}_{>0}^n:\quad P = \mathrm{MNL}(w) \text{ has the nesting-by-fare-order property.}

This leaves the fares unrestricted: condition 2 quantifies over all ordered value vectors $x$ , so the goal holds for every fare ladder at once.

Milestones

Lemma 5: if $\theta f(y_1) + (1-\theta) f(y_3) = f(y_2)$ for $f(y) = y/(y+1)$ , the same holds for $g(y) = 1/(y+1)$ .
The MNL purchase probability $Q(S) = W(S)/(W(S)+1)$ , $W(S) = \sum_{i\in S} w_i$ , is increasing.
For an incomplete $T$ : an index $k^*$ with $W(A_{k^*}) \le W(T) < W(A_{k^*+1})$ , and a weight $\theta \in [0,1]$ solving (15).
With the weights $\theta$ on $A_{k^*}$ and $1-\theta$ on $A_{k^*+1}$ : $\bar P_j(\alpha) \ge P_j(T)$ for $j \le k^*$ , and the prefix sums beyond $k^*$ equal $Q(T)$ .
Theorem 2, sufficiency direction: increasing $Q$ plus such majorizing mixtures for every incomplete $T$ give the nesting-by-fare-order property.

Companions

Proposition 6, first sentence, under strictly decreasing fares: every nondominated set is complete.
Proposition 5: the independent model has the nesting-by-fare-order property.

Significance

The result. Proposition 6 turns a structural question about an exponentially large dynamic program (the firm chooses among $2^n$ offer sets in every period) into the familiar one-dimensional policy of opening fares from the top. For MNL demand, the optimal control is described by $n$ protection levels, which is how airline reservation systems already operate; the paper's later remark (17) gives the opening condition for fare $k+1$ . Without it, a firm whose customers substitute according to MNL would have no guarantee that fare-ordered nesting is not leaving revenue on the table.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked proof of Proposition 6, a checked sufficiency direction of Theorem 2 that applies to any choice model, and the independent-demand case (Proposition 5). The literal wording of Proposition 6 ("the only nondominated sets are the complete sets") is false when fares tie; the mission records the corrected statement under strictly decreasing fares.

Difficulty

The obvious approach compares an incomplete set $T$ directly with a single complete set, and it fails: under MNL, adding a fare changes every other fare's probability through the common denominator, so no single complete set need match $T$ 's purchase probability while selling at least as much of every high fare. A comparison through randomizations over complete sets is needed, and a weight that matches $T$ 's total purchase probability does not, for a general choice model, match the individual product probabilities as well. The final comparison must also hold for every ordered value vector $x$ , including vectors with negative entries, for which the empty set can be the only optimum.

Formalization scope

Products are Fin n (index $j-1$ for fare $j$ ); a choice model is P : Finset (Fin n) → Fin n → ℝ with the published RevenueManagement.IsChoiceModel (nonnegativity, total at most one) plus SupportedOn P ( $P_j(S) = 0$ off $S$ , the model's convention on p. 5). $A_k$ is complete n k = {j | j.val < k} for $k \in \{0, \dots, n\}$ ; the empty set $A_0$ counts as complete, and the mixture weights $\alpha$ are indexed by $\{0, \dots, n\}$ . The page indexes complete sets as $k = 1, \dots, n$ ; without $A_0$ , condition 2 fails for every model when all $x_j < 0$ , where only $\emptyset$ is optimal. The order $x_1 \ge \dots \ge x_n$ is Antitone x. The paper's weight $\lambda$ is written $\theta$ , since λ is reserved in Lean.

Standing hypotheses and pins: MNL weights $w_j > 0$ ( $w_j = e^{u_j}$ ); for the independent model $q_j \ge 0$ and $\sum_j q_j \le 1$ , so that it is a probability function; strictly decreasing fares StrictAnti r for the nondominated-set companion only, because with $r_1 = r_2 > 0$ and $w_1 = w_2$ the incomplete set $\{2\}$ is nondominated.

The goal is the full Definition 4 with both conditions; it may not be weakened to condition 1 alone, to condition 2 for nonnegative $x$ , or to a statement that assumes condition (ii) of Theorem 2 or the existence of $k^*$ . The "Moreover" sentence of Propositions 5 and 6 (nested allocation policies, Definition 3) is not formalized. Theorem 2's sufficiency half is restated here because draft items cannot import the drafts of mission 2; the definitions of complete sets and the property are shared verbatim with that mission.

Contributions welcome: proofs of the milestones, a general summation-by-parts lemma for majorized vectors (reusable beyond this mission), and the converse of Theorem 2 via Farkas' lemma.

Selected references

K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, working paper, October 21, 2001 (UPF Economics Working Paper 533); published in Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
M. Ben-Akiva, S. Lerman, Discrete Choice Analysis: Theory and Application to Travel Demand, MIT Press, 1985. https://mitpress.mit.edu/9780262536400/
T. C. Lee, M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3):252–265, 1993. https://doi.org/10.1287/trsc.27.3.252
A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

On Cores and Indivisibility 2: Gale's Top Trading Cycles Give a Core Allocation Supported by Competitive PricesResearch Paper

Motivation

Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.

Timeline.

1967: Scarf proves that balanced games without side payments have nonempty cores (doi:10.2307/1909383).
1974: Shapley and Scarf define the housing market, prove that it has a nonempty core by both arguments, and give Gale's top-trading-cycle construction with competitive prices, allowing indifferences.
1977: Roth and Postlewaite show that with strict preferences the competitive allocation is unique and is the unique allocation in the strong core (doi:10.1016/0304-4068(77)90004-0).
1982: Roth shows the top-trading-cycles mechanism is strategy-proof under strict preferences (doi:10.1016/0165-1765(82)90003-9).
2003: Abdulkadiroğlu and Sönmez adapt top trading cycles to school choice (doi:10.1257/000282803322157061).

Setting

A finite set $N$ of traders each brings one indivisible good; "item $j$ " is the good of trader $j$ . Preferences are a real matrix $A = (a_{ij})_{i,j\in N}$ : trader $i$ prefers item $j$ to item $k$ when $a_{ij} > a_{ik}$ and is indifferent when $a_{ij} = a_{ik}$ . Ties are allowed, and only comparisons matter.

An allocation is a bijection $\sigma : N\to N$ ; trader $i$ receives item $\sigma(i)$ . For a coalition $S$ , an $S$ -permutation $\tau$ reshuffles the items of $S$ among the members of $S$ . The allocation $\sigma$ is a core allocation if there is no nonempty $S$ and $S$ -permutation $\tau$ with $a_{i\tau(i)} > a_{i\sigma(i)}$ for every $i \in S$ .

Prices $\mathrm{price}: N \to \mathbb R$ are competitive for $\sigma$ if each trader $i$ , selling his own item for $\mathrm{price}(i)$ , can afford $\sigma(i)$ , i.e. $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$ , and no item $k$ with $\mathrm{price}(k) \le \mathrm{price}(i)$ is better for him than $\sigma(i)$ .

For $R \subseteq N$ , a top trading cycle for $R$ is a nonempty $S \subseteq R$ whose members can be arranged in a cycle $i_1 \to i_2 \to \cdots \to i_s \to i_1$ so that each $i_r$ likes the good of $i_{r+1}$ at least as well as any other good in $R$ . A top-trading-cycle partition is

N = S^1 \cup S^2 \cup \cdots \cup S^p,

with $S^1$ a top trading cycle for $N$ and each $S^j$ a top trading cycle for $N - (S^1\cup\cdots\cup S^{j-1})$ . In Lean the partition carries stage : N → Fin p and the successor map next : N → N.

Formalization targets

Goal: Section 6, assertions (1) and (2), p. 114

For every market $A$ and every top-trading-cycle partition with successor map $\mathrm{next}$ , the allocation $i \mapsto \mathrm{next}(i)$ is a core allocation, and for every choice of prices

\pi^1 > \pi^2 > \cdots > \pi^p > 0

on the goods of $S^1,\dots,S^p$ it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.

Milestones (Section 6, p. 114)

Every nonempty $R\subseteq N$ has a top trading cycle.
A top-trading-cycle partition of $N$ exists (so the goal is not vacuous and every market has a competitive core allocation).
If $j$ is the first index with $S \cap S^j \ne \emptyset$ and $i \in S\cap S^j$ , then $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k \in S$ .
Under the prices $\pi^{\mathrm{stage}(k)}$ , the successor's item costs the same as one's own, and every affordable item lies in one's own cycle or a later one.

Example (Section 7, pp. 115–116)

For the matrix $\begin{pmatrix}0&1&2\\1&0&-1\\-1&1&0\end{pmatrix}$ the unique competitive payoff is $(2,1,1)$ at equal prices, while the allocation with payoff $(1,1,0)$ is a core allocation that is competitive at no prices.

Significance

The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.

The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.

Difficulty

Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of $N$ from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in $R$ , with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.

Formalization scope

Traders form an arbitrary finite type N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.
Allocations are bijections σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.
Blocking is strict for every member of the coalition, as on p. 107; the weak notion (all weakly, one strictly better off) makes assertion (1) false with ties.
The paper gives no displayed definition of competitive prices. The Lean notion is: $\sigma$ is a bijection, $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$ , and $\mathrm{price}(k)\le\mathrm{price}(i) \Rightarrow a_{ik}\le a_{i\sigma(i)}$ . This transcribes "can sell his own item for $\pi^j$ dollars", "cannot afford", and "his utility is maximized" (p. 114).
A top trading cycle is a single cycle of the successor map: nonempty, inside $R$ , closed under next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).
Explicit readings of loose phrases: "it is evident" (milestone 1) is an existence statement; "the highest possible payoff available to him in $S$ " (milestone 3) is $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k\in S$ ; "cannot afford any items from $S^1,\dots,S^{j-1}$ " (milestone 4) is: price at most $\pi^j$ implies stage at least $j$ ; "a set of competitive prices exists" (goal) is strengthened to every strictly decreasing positive $\pi$ , as the proof gives.
Trivializing formalizations are ruled out: the partition is quantified over all choices and its existence is a milestone, cycles are required to be nonempty and single, and the budget clause is part of the price notion, so competitiveness does not reduce to "everyone gets a best good".
Contributions welcome: proofs of the milestones, a computable top-trading-cycle algorithm with a proof that it produces a partition, and a proof of the paper's remark that no other competitive prices exist up to ties.

Selected references

L. Shapley and H. Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974) 23–37. https://doi.org/10.1016/0304-4068(74)90033-0
H. Scarf, The core of an N person game, Econometrica 35 (1967) 50–69. https://doi.org/10.2307/1909383
A. E. Roth and A. Postlewaite, Weak versus strong domination in a market with indivisible goods, Journal of Mathematical Economics 4 (1977) 131–137. https://doi.org/10.1016/0304-4068(77)90004-0
A. E. Roth, Incentive compatibility in a market with indivisible goods, Economics Letters 9 (1982) 127–132. https://doi.org/10.1016/0165-1765(82)90003-9
A. Abdulkadiroğlu and T. Sönmez, School choice: a mechanism design approach, American Economic Review 93 (2003) 729–747. https://doi.org/10.1257/000282803322157061

8 thms3 active usersReviewed

Computational Geometry Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XII: The Euclidean Traveling Salesman Problem — P(|L_N − M| ≥ t) ≤ K e^{−t²/K} for N Uniform Points in the SquareTextbook

Motivation

The Euclidean traveling salesman problem asks for the shortest closed route through a finite set of points in the plane. Even when the points are placed independently and uniformly in a square, finding an individual shortest route is computationally difficult. A separate probabilistic question is whether the optimal length varies much from one random sample to another. In Chapter 11 of Talagrand's 1995 paper, this question motivates a concentration theorem for the tour length and for other geometric functionals with the same local regularity property.

The result is useful because a bound on fluctuations can be applied without computing the distribution of the optimal tour length. It separates the typical size of the length, which may need other geometric estimates, from the chance of a substantial deviation. The paper develops a more general concentration method for product spaces; the geometric chapter shows how its estimates can control an optimization problem whose response to changing one sample point depends strongly on the local configuration.

Setting

Let $Q=[0,1]^2$ , and let $X_1,\ldots,X_N$ be independent points uniformly distributed in $Q$ , with $N\ge1$ . A configuration is the finite set $F=\{X_1,\ldots,X_N\}$ ; repeated sample locations are represented once in $F$ . For any finite $F\subseteq Q$ , write $T(F)$ for the length of a shortest closed tour visiting every point of $F$ . The tour length of the random sample is $T_N=T(F)$ . The empty set and a singleton have tour length zero.

The main theorem concerns a functional $L$ on all finite subsets of $Q$ . A level $k\ge1$ dyadic square $C$ has side $2^{-k}$ . Say that $L$ has regularity constant $K_0>0$ when, for every finite $F$ and every finite $G\subseteq C$ , if a point of $F$ lies within Euclidean distance $2^{-k+2}$ of $C$ , then

L(F)\le L(F\cup G)\le L(F)+K_0,2^{-k}\sqrt{|G|}.

The first inequality is monotonicity under adding points. The second limits the added cost when the new points lie in a small square near an existing point. Lemma 11.2.1 says that the shortest tour functional $T$ has this property with a universal constant. In particular, the functional in the main theorem is not an arbitrary real function on samples: it must obey this condition for every admissible square and pair of finite sets.

A median $M$ of $L(F)$ is any real number for which both $P(L(F)\le M)$ and $P(L(F)\ge M)$ are at least one half. The theorem applies to every median. This convention avoids selecting one median when the distribution has more than one.

For the intermediate geometric estimates, $k_0$ is the largest integer with $2^{2k_0}\le N$ . Given a deviation parameter $t$ , $k_1$ is the integer selected by the criterion (11.1.9) after the paper sets the auxiliary Poisson intensity to $N/8$ . The number $m_k$ counts level $k$ squares that contain at most $N2^{-2k-6}$ distinct sample points. An isolation weight $\alpha(x)$ records the largest scale between $k_1$ and $k_0$ at which the square containing $x$ contains at most $N2^{-2k-7}$ sample points, and equals $2^{-k_0}$ if no such scale exists.

Formalization targets

Gaussian concentration for regular geometric functionals

For each fixed $K_0>0$ , there is a constant $K>0$ , independent of $N$ and $L$ , such that every measurable $L$ with the regularity property above satisfies, for all $t\ge0$ ,

P\bigl(|L(F)-M|\ge t\bigr)\le K\exp(-t^2/K).

This is Theorem 11.2.2, the goal. Its constant may depend on the fixed regularity constant $K_0$ . Lemma 11.2.1 makes the tour length a direct instance. The milestone list also includes the quantitative sparse-square estimate of Proposition 11.1.4, the isolation-weight bound of Proposition 11.2.3, and the deterministic insertion estimate of Proposition 11.2.5. These retain the paper's specified thresholds and the dependency of their constants.

Significance

For $T_N$ , the result supplies a tail bound whose scale does not grow with the number of sample points. It says that the shortest tour length lies near a median with a Gaussian-form upper bound on the probability of a deviation. It does not identify the median or give an algorithm for finding the optimal tour. The abstract form also covers other finite-set functionals once their local regularity condition is established.

The paper proves these claims in ordinary mathematics. This mission asks for machine-checked proofs of the stated concentration, geometric occupancy, and tour-insertion results. The reusable outputs include a finite-set model of Euclidean tours and a precise interface for local regularity; the dyadic occupancy and isolation-weight definitions can support later sections on other geometric structures. No machine-checked proof of these specific chapter results is claimed here.

Difficulty

A naive bounded-differences estimate treats the effect of changing a sample point as if a single fixed worst-case insertion cost applied everywhere. That loses the paper's uniform fluctuation scale: a point can be unusually isolated, and its insertion cost can be much larger than the cost near a typical dense cluster. The central problem is to keep track of those irregular locations while retaining a bound uniform in $N$ . The chapter's dyadic-square counts and isolation weights make this difficulty explicit in the statements.

Formalization scope

Points are pairs of real coordinates constrained to $[0,1]$ , represented as functions on Fin 2. Their distance is the Euclidean $\ell^2$ distance, defined explicitly; the default norm on a Lean function space would give a different metric. The random sample is a product of coordinatewise uniform probability measures. $F$ is the set of distinct sampled locations, so ties have a defined value. Tour length is the minimum cyclic tour cost over the finite set, using the published generic metric-TSP tour model as its base.

Dyadic squares are closed in the local regularity condition. For the single square assigned to a point in the definition of $\alpha$ , the implementation uses half-open cells, with the right endpoint $1$ assigned to the final cell. This resolves only grid-line ties, which have probability zero under the stated sample law. Counts use distinct locations, as does the paper's set $F$ . All probability inequalities are compared in the extended nonnegative reals. The event bound is written with ENNReal.ofReal; a negative formal lower bound represents the paper's trivial probability lower bound. The main theorem explicitly assumes measurability of the sample functional, following the paper's convention that all relevant functions are measurable. Theorems in Section 11.1 retain $t\ge1$ and $t\le\sqrt N/K$ ; the main theorem covers every $t\ge0$ .

The formalization must not replace the square's uniform law by an arbitrary distribution, use a supremum-norm tour, or place the existential constant after $N$ or $L$ . Contributions toward the goal may develop measure-theoretic facts about the product law, finite Euclidean tours, dyadic occupancy bounds, or the insertion estimate. Those interfaces have uses beyond this chapter.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.

7 thms3 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VII: Bin Packing — P(|B_N − M| ≥ 1 + u) ≤ 8 exp(−u²/(64 N E X₁²))Textbook

Motivation

Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in $[0,1]$ can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.

A short history of that question, as Talagrand recounts it on p. 151 of the source:

Late 1980s. Martingale methods (Rhee–Talagrand; McDiarmid, On the method of bounded differences, 1989) give $P(|B_N - \mathbb E B_N| \ge t) \le 2\exp(-2t^2/N)$ for $N$ i.i.d. items. The exponent ignores the item sizes.
1994. Since $B_N$ behaves like $\sum_i X_i$ when the items are small, the right exponent should be of order $t^2/(N\operatorname{var} X_1)$ , or at least $t^2/(N\,\mathbb E X_1^2)$ . The second form was proved by W. Rhee (Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385) using non-trivial bin-packing theory.
1995. Talagrand (Publ. Math. IHÉS 81, Chapter 6) derives the $t^2/(N\,\mathbb E X_1^2)$ bound in a few lines from his convex hull distance inequality, using only trivial facts about bin packing.

This mission formalizes that chapter.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$ . A point $x = (x_1,\dots,x_N) \in \Omega^N$ is a list of item sizes. A packing into $k$ bins is a map $\sigma : \{1,\dots,N\} \to \{1,\dots,k\}$ with $\sum_{i:\sigma(i)=j} x_i \le 1$ for every bin $j$ . The bin packing number $B_N(x)$ is the least $k$ for which a packing exists ( $N$ bins always suffice; $B_N = 0$ when $N = 0$ ).

Further notation, as in Lean (TalagrandConc.BinPacking):

$\|x\|_2 = (\sum_{i \le N} x_i^2)^{1/2}$ (l2Norm);
for real $a$ , the level set $A(a) = \{y \in \Omega^N : B_N(y) \le a\}$ (levelSet);
for $A \subseteq \Omega^N$ and $x \in \Omega^N$ , $U_A(x) = \{s \in \{0,1\}^N : \exists y \in A,\ s_i = 0 \Rightarrow x_i = y_i\}$ , its convex hull $V_A(x) \subseteq \mathbb R^N$ , and the convex hull distance $f_c(A,x)$ , the Euclidean distance from $0$ to $V_A(x)$ , valued in $[0,+\infty]$ (U, V, convexDist);
$\mu$ a probability measure on $[0,1]$ , $P = \mu^{\otimes N}$ the product probability on $[0,1]^N$ , whose coordinates $X_1,\dots,X_N$ are i.i.d. items with law $\mu$ , and $\mathbb E X_1^2 = \int \omega^2\,d\mu(\omega)$ (secondMoment);
$M$ is a median of $B_N$ if $P(B_N \le M) \ge 1/2$ and $P(B_N \ge M) \ge 1/2$ (IsMedian).

Formalization targets

Goal: Theorem 6.5 (p. 152)

For every median $M$ of $B_N$ and every $u$ with $0 \le u \le 8\sqrt2\,N\,\mathbb E X_1^2$ ,

P\big(|B_N(X_1,\dots,X_N) - M| \ge 1 + u\big) \le 8\exp\Big(-\frac{u^2}{64\,N\,\mathbb E X_1^2}\Big).

Milestones

Lemma 6.1 (p. 151): $B_N(x_1,\dots,x_N) \le 2\sum_{i\le N} x_i + 1$ .
Lemma 6.2, Eq. (6.2) (p. 151): for $a > 0$ and all $x$ , $B_N(x) \le a + 2\|x\|_2\, f_c(A(a),x) + 1$ .
Lemma 6.3, Eq. (6.3) (p. 152): $P(\|x\|_2 \ge 2\sqrt N(\mathbb E X_1^2)^{1/2}) \le \exp(-2N\,\mathbb E X_1^2)$ .
Proposition 6.4, Eq. (6.4) (p. 152): for all $t > 0$ , $a > 0$ ,

P(B_N \le a)\,P\big(B_N \ge a + 4t\sqrt N(\mathbb E X_1^2)^{1/2} + 1\big) \le e^{-t^2/4} + e^{-2N\,\mathbb E X_1^2}.

The goal keeps the paper's explicit constants $8$ , $64$ and $8\sqrt2$ .

Significance

The result. Theorem 6.5 shows that the random optimum $B_N$ fluctuates on the scale $\sqrt{N\,\mathbb E X_1^2}$ rather than $\sqrt N$ . For small items ( $\mathbb E X_1^2 \to 0$ ) this is much sharper than the martingale bound, and it is the scale of the fluctuations of $\sum_i X_i$ , which is a lower bound on $B_N$ . Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to $f_c$ of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.

Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general- $\Omega$ form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.

Difficulty

The obvious route is a bounded-differences argument: changing one item changes $B_N$ by at most one. That route yields only the exponent $t^2/N$ , because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights $x_i$ depend on the point $x$ itself, so no fixed weighted Hamming distance works. The convex hull distance $f_c$ controls every weighting at once, and the resulting factor $\|x\|_2$ is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) $\Omega = [0,1]$ is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.

Formalization scope

$\Omega = [0,1]$ is Mathlib's unitInterval. Coordinates are Fin N (0-based). $P$ is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.
$B_N$ is sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.
$f_c$ is an infimum in ℝ≥0∞ with the Euclidean norm written out ( $+\infty$ for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.
Probabilities are ℝ≥0∞-valued. Every event in the statements ( $\{B_N \le a\}$ , $\{\|x\|_2 \ge c\}$ ) is Borel. The paper's measurability convention matters only inside the proofs.
Theorem 6.5 makes the paper's implicit $u \ge 0$ explicit, and it is stated for every median, not for a chosen one. Lean's $u^2/0 = 0$ matters only in the degenerate case $N\,\mathbb E X_1^2 = 0$ , which forces $u = 0$ . There the bound is $8$ .
Not admissible: weakening the range of $u$ (the bound fails for large $u$ when $\mathbb E X_1^2$ is small), replacing $\mathbb E X_1^2$ by $1$ , or defining $B_N$ through a heuristic or a real-valued sInf.
Infrastructure needed: Talagrand's inequality (4.1.2) on a general product probability space (posed on the platform only in a finite-alphabet form) and Lemma 4.1.2. Both are welcome as separate contributions. A Chebyshev/exponential-moment bound gives Lemma 6.3.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 6, pp. 151–152. https://doi.org/10.1007/BF02699376
W. Rhee, Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385.
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, Cambridge Univ. Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
E. G. Coffman Jr., G. S. Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, Wiley, 1991.

6 thms3 active usersReviewed

Bandit Algorithms Probability Statistics·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments II: Staying on Heads and Switching on Tails Loses at Most 3 − 2√2 per Toss in the Long RunResearch Paper

Motivation

In 1952 Herbert Robbins asked how a statistician should draw a sample sequentially from two populations when the goal is the largest possible expected total, not a test or an estimate after the fact (Robbins 1952). This is the problem now called the two-armed bandit, and Robbins' paper is the usual starting point of the multi-armed bandit literature that underlies clinical-trial allocation, adaptive experimentation and online recommendation (Lattimore and Szepesvári 2020).

Robbins illustrated the problem with two coins. His first concrete rule, "stay on heads, switch on tails" (later known as win-stay, lose-shift or play the winner), uses only the outcome of the last toss, yet its long-run loss relative to an observer who knows the better coin is at most $3-2^{3/2}\approx 0.172$ per toss, against $1/2$ for a rule that ignores the outcomes. The same rule was studied again in clinical-trial design as "play the winner" (Zelen 1969).

Timeline. 1952: Robbins computes the operating characteristics of the stay-or-switch rule $R_1$ and of the outcome-blind rule $R_0$ for two coins, and shows that a greedy rule with sparse forced sampling attains $\max(\alpha,\beta)$ for arbitrary populations with finite means (Section 2). 1969: Zelen proposes the play-the-winner rule for clinical trials. 1985: Lai and Robbins give the logarithmic lower bound on regret and rules that attain it (Lai and Robbins 1985).

Setting

Two coins $A$ and $B$ have unknown head probabilities $\alpha$ and $\beta$ , with $0\le\alpha,\beta\le1$ . A head pays $\$ 1 $, a tail pays nothing. If$ x_i\in{0,1} $is the payoff of the$ i $-th toss,$ S_n=x_1+\dots+x_n $is the total received after$ n $tosses. In the formal development the pair of coins is a **two-armed stochastic bandit**: arm$ 0 $is coin$ A $, with payoff law$ (1-\alpha)\delta_0+\alpha\delta_1 $, and arm$ 1 $is coin$ B $, with payoff law$ (1-\beta)\delta_0+\beta\delta_1$.

A sampling rule chooses the coin for each toss from the outcomes of the earlier tosses. Two rules are studied.

Rule $R_1$ . For the first toss choose $A$ or $B$ at random. Then, for $i=1,2,\dots$ , if the $i$ -th toss results in heads, use the same coin for the $(i+1)$ -th toss; if it results in tails, switch to the other coin.
Rule $R_0$ . Choose one of the two coins at random and then use it for every toss.

Write $p_i$ for the probability of heads on the $i$ -th toss under the rule in use, and $\mathrm E(S_n/n)$ for the expected average payoff of the first $n$ tosses. The paper's two parameters are

\gamma=\frac{\alpha+\beta}{2},\qquad \delta=\frac{|\alpha-\beta|}{2},

so that $\max(\alpha,\beta)=\gamma+\delta$ is the expected payoff per toss of an observer who knows the better coin. Following the paper, $\alpha$ and $\beta$ are assumed not both $0$ and not both $1$ ; then $|\alpha+\beta-1|<1$ .

Formalization targets

Goal: the asymptotic loss of $R_1$ and its maximum

Under $R_1$ ,

\lim_{n\to\infty}\mathrm E\!\left(\frac{S_n}{n}\right)=\gamma+\frac{\delta^2}{1-\gamma}, \qquad L(A,B,R_1)=\lim_{n\to\infty}\left[\max(\alpha,\beta)-\mathrm E\!\left(\frac{S_n}{n}\right)\right]=\delta\left[1-\frac{\delta}{1-\gamma}\right],

and for every admissible pair of coins

0\le L(A,B,R_1)\le M_1=3-2^{3/2},

with equality at $\alpha=0,\ \beta=2-2^{1/2}$ and at $\alpha=2-2^{1/2},\ \beta=0$ (Eqs. (6), (8) and the text after (8), p. 531).

Milestones, in the order of the argument

Eq. (2): $p_{i+1}=(\alpha+\beta-1)p_i+(\alpha+\beta-2\alpha\beta)$ for $i\ge1$ .
Eq. (3): the closed form $p_i=(\alpha+\beta-1)^{i-1}\bigl[p_1-c\bigr]+c$ with $c=(\alpha+\beta-2\alpha\beta)/(2-(\alpha+\beta))$ .
Eqs. (4)–(5): $\lim_i p_i=c=\gamma+\delta^2/(1-\gamma)$ .
Eq. (6): both $\mathrm E(S_n/n)$ and $(p_1+\dots+p_n)/n$ have the stated limit.
Eqs. (7)–(8) and $M_1$ : $\max(\alpha,\beta)=\gamma+\delta$ and $0\le\delta[1-\delta/(1-\gamma)]\le 3-2^{3/2}$ , with the two maximizers.
Rule $R_0$ : $L(A,B,R_0)=\delta$ , whose maximum over the admissible pairs is $M_0=1/2$ , at $(0,1)$ and $(1,0)$ .

Significance

The result. The goal quantifies how much an extremely simple adaptive rule recovers. A rule blind to outcomes loses up to half a dollar per toss; one bit of memory cuts the worst case to about $0.172$ . Robbins used this comparison to argue that the sequential design problem has nontrivial, computable answers, and to motivate the forced-sampling rule $\bar R$ of the same section, whose loss tends to $0$ . The closed forms (3)–(6) are the exact operating characteristics of the four-state Markov chain $(\text{coin},\text{outcome})$ that $R_1$ generates.

Formalizing it. The results are classical and elementary on paper, but none of them has a machine-checked proof. The mission produces a verified chain from the canonical bandit measure to an explicit long-run payoff: the head probability of a fixed toss is computed from the law of the whole trajectory, the recursion is derived from the rule's kernels, and the Cesàro limit closes the argument. The same pattern applies to any finite-memory bandit rule, and the coin bandit and the two rules are reusable test cases for the platform's bandit library. No platform theorem states $R_1$ , its recursion or its loss; other two-state models on the platform (a Markov-renewal gain rate, an MDP gadget) are different objects.

Difficulty

The recursion (2) is a statement about the trajectory law, not about a Markov chain given in advance: the chain $(\text{coin}_i,x_i)$ has to be extracted from the Ionescu–Tulcea construction of the bandit measure, where the coin of toss $i+1$ is a deterministic function of toss $i$ and the payoff is drawn from the chosen coin's law. The head probability alone is not a Markov chain: $p_{i+1}$ depends on the joint law of coin and outcome at toss $i$ , so a naive one-step argument on $p_i$ does not apply, and the affine form of (2) is a property of this particular rule. The maximization in (8) is over a two-dimensional region whose maximizers lie on the boundary $\alpha=0$ or $\beta=0$ , and the excluded corners are exactly where the formula $\delta/(1-\gamma)$ breaks down.

Formalization scope

The bandit is the published BanditAlgorithm.StochasticBandit 2; the rules are policies of the published type BanditPolicy 2, and probabilities and expectations are taken under the published infinite-horizon measure banditTrajMeasure, whose coordinate $t$ is toss $t+1$ . Head probabilities are elements of unitInterval. The conventions committed to are:

"At random" for the first coin of $R_1$ and $R_0$ is the fair choice, probability $1/2$ each.
Heads is the payoff value $1$ ; $p_i$ is defined for $i\ge1$ and every statement quantifies over $i\ge1$ or $n\ge1$ .
"Not both $0$ or both $1$ " is the hypothesis $\neg(\alpha=0\wedge\beta=0)\wedge\neg(\alpha=1\wedge\beta=1)$ , never $0<\alpha$ or $\alpha<1$ , which would remove the maximizer $\alpha=0$ . Robbins states it immediately before Eq. (2), and the Lean carries it through the probability and loss results.
The paper's " $\lim E(S_n/n)=\lim (p_1+\dots+p_n)/n$ " is stated as convergence of both sequences to the same value.
" $L(A,B,R_1)$ has its maximum value $M_1$ when …" is read as: $L\le M_1$ for every admissible $(\alpha,\beta)$ , and $L=M_1$ at both named points ("or vice versa").
$2^{3/2}$ is written $2\sqrt2$ . The numerical asides ( $\approx .172$ , $\approx .586$ , "17.2 cents") are not formalized, nor is the "tossing the two coins alternately" variant of $R_0$ .

The asymptotic loss is stated as the limit of $\max(\alpha,\beta)-\mathrm E(S_n/n)$ ; defining $L$ by its closed form would make the goal a tautology. Likewise, the head probabilities are computed from the law of the rule on the coins: positing a sequence that satisfies (2) would drop the probabilistic content.

A complete development needs: the one-dimensional marginals of banditTrajMeasure (the law of coordinate $t+1$ given the prefix), the joint law of (coin, payoff) at each toss, linearity of expectation for bounded payoffs, a Cesàro-mean lemma, and a short two-variable optimization. The trajectory-marginal lemmas are reusable for every bandit mission on the platform; contributions that prove them in general are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
M. Zelen, Play the winner rule and the controlled clinical trial, J. Amer. Statist. Assoc. 64 (1969), 131–146. https://doi.org/10.1080/01621459.1969.10500959
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

12 thms3 active usersReviewed

Completed

Complexity Theory Linear Optimization Optimization·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 1: The Predictor–Corrector Algorithm Between N₂(1/4) and N₂(1/2) Attains Precision t in O(√n·t) IterationsResearch Paper

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$ , and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$ . The primal problem minimizes $c^Tx$ over $Ax=b$ , $x\ge0$ . Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$ , $s\ge0$ . The dual slack is $s$ . The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$ , with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ , and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$ . For $0<\beta<1$ , the Euclidean central-path neighborhood is

N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$ , $Ad_x=0$ , and $A^Td_y+d_s=0$ . A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$ . Algorithm 1 begins in $N_2(1/4)$ . It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$ , then takes one full corrector direction with $\gamma=1$ . The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$ ; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$ , every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.

The paper states the iteration order as $O(\sqrt n\,t)$ . The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$ , rather than with $n$ , in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$ . The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$ : Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$ ; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$ , because its printed lower bound on the predictor length fails at $n=1$ .

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$ ; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

12 thms3 active usersReviewed

Completed

Stochastic Systems·Captain: mikedeng1

A Proof of the Optimality of the Shortest Remaining Processing Time Discipline: SRPT Minimizes the Number of Jobs in System at Every Time, for Every Arrival Stream and Every ScheduleResearch Paper

Motivation

A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).

Timeline:

1966. Schrage and Miller analyse the M/G/1 queue under SRPT and state, without proof, that SRPT minimizes the number in system at every time for every arrival sequence (Schrage–Miller, 1966).
1968. Schrage publishes a letter giving a proof by an interchange argument (Schrage, 1968). This mission formalizes that letter.
1978. D. R. Smith gives a new proof of the same statement (Smith, 1978) by a different argument.

Setting

An arrival stream is a sequence of pairs $(A(n), P(n))$ , $n = 0, 1, 2, \dots$ , of real numbers: $A(n)$ is the arrival time and $P(n)$ the processing time of job $n$ . A schedule is a family of measurable functions $\delta(n, \cdot) : \mathbb R \to \{0, 1\}$ , with $\delta(n, t) = 1$ meaning that the processor works on job $n$ at time $t$ . No job is processed before it arrives ( $\delta(n, t) = 0$ for $t < A(n)$ ), and the processor works on at most one job at a time.

The remaining processing time of job $n$ at time $t$ is

S(n, t) = P(n) - \int_{A(n)}^{t} \delta(n, x)\,dx,

and its completion time is

C(n) = \min\Big\{x \ge A(n) : \int_{A(n)}^{x} \delta(n, t)\,dt \ge P(n)\Big\},

or $+\infty$ if the job never receives its processing time. The set of jobs in system at time $t$ is $\theta(t) = \{n : A(n) \le t,\ S(n, t) > 0\}$ , and $N(t)$ is its cardinality.

A schedule follows SRPT if, at every time $t$ with $\theta(t) \ne \emptyset$ , the processor works on a job $k \in \theta(t)$ with $S(k, t) \le S(j, t)$ for all $j \in \theta(t)$ . Ties may be broken arbitrarily.

Formalization targets

Goal: SRPT minimizes the number in system at every time

For every locally finite arrival stream, every SRPT schedule $\delta_s$ and every schedule $\delta$ of the same stream,

N_s(t) \le N(t) \qquad \text{for all } t \in \mathbb R.

The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.

Milestones: the steps of the letter's interchange argument

All five come from the PROOF on p. 689. They compare an original schedule $\delta_o$ with a revised schedule $\delta_r$ .

Idle case (b1). If the processor is idle on $[t, t+v]$ while job $j$ waits, processing $j$ there gives $C_r(j) < C_o(j)$ and $C_r(i) = C_o(i)$ for $i \ne j$ .
Max identity. Reassigning the capacity that two jobs $j, k$ share after time $t$ , in any way, leaves $\max\{C(k), C(j)\}$ unchanged.
SRPT minimizes the minimum. Giving that capacity first to the job with the smaller remaining time minimizes $\min[C(k), C(j)]$ .
Relation (2). If $k$ is served on $[t, t+v]$ while $j$ with $S_o(j,t) < S_o(k,t)$ waits, the SRPT reassignment gives $\min[C_r(k), C_r(j)] < \min[C_o(k), C_o(j)]$ .
Counting. Relations (1)–(3) on completion times give $N_r(y) = N_o(y) - 1$ for $C_r(j) \le y < \min[C_o(k), C_o(j)]$ , and $N_r(y) = N_o(y)$ otherwise.

Significance

The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.

Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.

Difficulty

The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.

Formalization scope

All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from $0$ , and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in $\{0,1\}$ , each δ n measurable, $\delta(n,t) = 0$ before arrival, and at most one job served at a time. The letter's $\sum_n \delta(n,t) \le 1$ is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for $S(n,t)$ , which has no setup term. Completion times take values in WithTop ℝ, with $+\infty$ for a job that never completes. A job is in system on $[A(n), C(n))$ . $N(t)$ is Set.ncard, and the goal assumes local finiteness ( $\{n : A(n) \le t\}$ is finite for every $t$ ) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every $t$ .

Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 (" $S(k,t) > S(j,t)$ for $j \in \theta(t)$ implies $\delta(k,t)=0$ ") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.

The milestones add disclosed hypotheses that the letter uses silently:

finiteness of $C_o(j)$ in the idle case;
no service on a job after it completes in the max identity;
that one of the two jobs completes under $\delta_o$ in relation (2).

The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.

A complete development needs:

continuity and monotonicity of $x \mapsto \int_{A(n)}^x \delta(n,t)\,dt$ ;
the characterization $n \in \theta(t) \iff A(n) \le t < C(n)$ ;
interval integrals of schedules modified on sets.

All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.

Selected references

L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3):687–690, 1968. https://doi.org/10.1287/opre.16.3.687
L. E. Schrage and L. W. Miller, The queue M/G/1 with the shortest remaining processing time discipline, Operations Research 14(4):670–684, 1966. https://doi.org/10.1287/opre.14.4.670
D. R. Smith, A new proof of the optimality of the shortest remaining processing time discipline, Operations Research 26(1):197–199, 1978. https://doi.org/10.1287/opre.26.1.197
J. D. C. Little, A proof for the queuing formula L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
M. Harchol-Balter, B. Schroeder, N. Bansal and M. Agrawal, Size-based scheduling to improve web performance, ACM Transactions on Computer Systems 21(2):207–233, 2003. https://doi.org/10.1145/762483.762486

7 thms3 active usersReviewed

Complexity Theory Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 5: KNAPSACK Reduces to Two-Machine Flow Shop Makespan with a Release Date or Tree Precedence and to Two- and Three-Machine Job Shop MakespanResearch Paper

Motivation

In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.

This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines $M_1, \dots, M_m$ in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.

Setting

A general shop instance has jobs $J_1,\dots,J_n$ and machines $M_1,\dots,M_m$ . Job $J_j$ consists of $m_j$ operations; its $r$ -th operation runs on machine $\mu_{jr}$ for $p_{jr}\in\mathbb N$ time units, and the tuple $\mu_j$ is the job's machine order (a machine may occur more than once). Each job has a release date $r_j$ , and some pairs of jobs carry a precedence constraint $J_j<J_k$ .

A schedule gives every operation a start time. It is feasible if no operation of $J_j$ starts before $r_j$ ; the operations of each job run in the order $\mu_j$ , each after the previous one completes; two operations on the same machine never overlap; and $J_j<J_k$ implies $C_j\le B_k$ , where $C_j$ is the completion time of $J_j$ and $B_k$ the starting time of $J_k$ . The makespan is $C_{\max}=\max_j C_j$ .

In the report's notation $n|m|\ell,\lambda|C_{\max}$ , $\ell=F$ means a flow shop and $\ell=G$ a job shop; $\lambda$ may contain $r_n\ge 0$ (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and $m_j\le m_*$ (at most $m_*$ operations per job). The recognition version of a problem asks, for an instance and a number $y$ , whether a feasible schedule with $C_{\max}\le y$ exists.

KNAPSACK asks, for positive integers $a_1,\dots,a_t$ and $b$ , whether some $S\subseteq T=\{1,\dots,t\}$ has $\sum_{j\in S}a_j=b$ . A problem $P'$ is reducible to $P$ ( $P'\propto P$ ) if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 4(g)–(j)

\mathrm{KNAPSACK}\ \propto\ n|2|F,r_n{\ge}0|C_{\max},\quad n|2|F,\mathit{tree}|C_{\max},\quad n|2|G,m_j{\le}3|C_{\max},\quad n|3|G,m_j{\le}2|C_{\max}.

Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.

Milestones: the four equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A=\sum_{j\in T}a_j$ , and for each of the paper's four constructions with its threshold $y$ ,

\exists\,S\subseteq T:\ \sum_{j\in S}a_j=b\iff\text{the constructed instance has a feasible schedule with } C_{\max}\le y,

with $y=A+1$ for (i), $y=2A$ for (j), $y=t(A+1)$ for (g) and $y=t(A+1)+1$ for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.

Significance

With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop $n|m|G|C_{\max}$ NP-complete for every fixed $m\ge 2$ . Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).

The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.

Difficulty

Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for $A$ , $t a_j$ and $t(A-b)$ , and parsing of the KNAPSACK code.

The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on $M_1$ " and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case $c<0$ contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses $t a_j\ge t$ , so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).

Formalization scope

Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as $\mu_n=(M_2,M_1,M_2)$ in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. $C_{\max}\le y$ is stated as $C_j\le y$ for every $j$ ; no maximum over an empty set is formed. Precedence $J_j<J_k$ is between jobs: every operation of $J_k$ starts no earlier than $C_j$ . A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations $(M_1,M_2)$ , with times allowed to be zero.

The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that $0<b<A$ " becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value $C_{\max}=y$ " of the forward directions is read as " $\le y$ ", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.

The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.

Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.

Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
J. R. Jackson, An extension of Johnson's results on job lot scheduling, Naval Research Logistics Quarterly 3 (1956) 201–203. https://doi.org/10.1002/nav.3800030307
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1 (1976) 117–129. https://doi.org/10.1287/moor.1.2.117
S. A. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

11 thms3 active usersReviewed

Completed

Machine Learning Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 2: On Any Partition into Segments, WML Makes at Most Σ min(l_i, (log(n/(βγ)) + m_i log(1/β))/log(1/u)) MistakesResearch Paper

Motivation

Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of $n$ prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor $\beta<1$ after each of its own mistakes. Its mistake bound is of order $\log n + m$ , where $m$ is the number of mistakes of the best member on the whole sequence.

That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).

Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.

Setting

A run takes place over $T$ trials $t = 0, \dots, T-1$ . In trial $t$ each member $i \in \{1,\dots,n\}$ of the pool predicts $x_i^{(t)} \in \{0,1\}$ , the master predicts $\lambda^{(t)} \in \{0,1\}$ , and the label $\rho^{(t)} \in \{0,1\}$ is revealed. The predictions of the pool and the labels are arbitrary.

The master keeps weights $w_i^{(t)} > 0$ , the weights at the beginning of trial $t$ . Let $W^{(t)} = \sum_j w_j^{(t)}$ be the total weight and $q_b^{(t)}$ the total weight of the members predicting $b$ . WML has parameters $0 < \beta < 1$ and $0 \le \gamma < \tfrac12$ :

it predicts $0$ if $q_0^{(t)} > q_1^{(t)}$ , $1$ if $q_1^{(t)} > q_0^{(t)}$ , and either value on a tie;
if $\lambda^{(t)} \ne \rho^{(t)}$ , each member $i$ with $x_i^{(t)} \ne \rho^{(t)}$ and $w_i^{(t)} > \frac{\gamma}{n} W^{(t)}$ has its weight multiplied by $\beta$ ; all other weights stay;
if $\lambda^{(t)} = \rho^{(t)}$ , no weight changes.

With $\gamma = 0$ this is WM. Write $m$ for the number of mistakes of the master and

u = \frac{1+\beta}{2} + (1-\beta)\gamma ,

which lies in $[\tfrac12, 1)$ for the stated parameter ranges.

Formalization targets

Goal: Theorem 3.1 (p. 224)

Split the sequence into consecutive segments $\mathcal S_1, \dots, \mathcal S_k$ , with $l_i$ trials in $\mathcal S_i$ , and let $m_i$ be the smallest number of mistakes any single pool member makes on $\mathcal S_i$ . If $\gamma > 0$ and every initial weight is at least $\beta\gamma/n$ times the total initial weight, then

m \le \sum_{i=1}^{k} \min\left( l_i,\ \frac{\log\big(n/(\beta\gamma)\big) + m_i \log(1/\beta)}{\log(1/u)} \right).

The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.

Milestone: Lemma 3.1 (pp. 223–224)

The single-segment case, $k = 1$ , together with the statement that the weight floor survives the run: if every initial weight is at least $\beta\gamma/n$ times the total, then

m \le \frac{\log\big(n/(\beta\gamma)\big) + m_0 \log(1/\beta)}{\log(1/u)},

and every final weight is at least $\beta\gamma/n$ times the total final weight.

Milestone: the contraction step (p. 224, proof of Lemma 3.1)

On every mistake trial, $W^{(t+1)} \le u\, W^{(t)}$ .

Significance

The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of $O(\log(n/(\beta\gamma)))$ mistakes per segment. The $\min$ with $l_i$ says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.

Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.

Difficulty

The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by $\beta$ per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.

Formalization scope

The pool is Fin n with $n > 0$ ; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial $t$ , w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute $0$ .

The paper allows $\gamma = 0$ for the algorithm, but then the bounds read $\log(n/0) = +\infty$ . In Lean, n / 0 = 0, so the bounds assume $\gamma > 0$ ; the contraction milestone holds for $0 \le \gamma < \tfrac12$ and is stated so. The hypothesis $\gamma < \tfrac12$ is kept as stated in the paper, not replaced by $u < 1$ . A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.

Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
M. Herbster, M. K. Warmuth, Tracking the Best Expert, Machine Learning 32, 151–178, 1998. https://doi.org/10.1023/A:1007424614876

4 thms3 active usersReviewed

Complexity Theory Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 4: KNAPSACK Reduces to Single-Machine Total Completion Time with One Release DateResearch Paper

Motivation

Minimizing the total completion time $\sum_j C_j$ of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time $0$ , processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may not start, change the picture. In their 1975 report Complexity of Machine Scheduling Problems (Mathematisch Centrum Report BW 43/75; journal version in Annals of Discrete Mathematics 1, 1977), Brucker, Lenstra and Rinnooy Kan used the then-new theory of NP-completeness (Cook 1971, Karp 1972) to map which classical scheduling problems are polynomially solvable and which are NP-complete. Theorem 4 of that report lists ten problems to which KNAPSACK reduces. Part (a) shows that total completion time on one machine is already hard when a single job has a nonzero release date and all weights are equal.

The result is a sharp boundary. With all release dates zero the problem is easy; with one nonzero release date it is NP-complete. It is a standard entry in the complexity classification of single-machine problems that later surveys (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993) and the scheduling-complexity databases build on.

Setting

An instance of KNAPSACK consists of positive integers $a_1,\dots,a_t$ and $b$ ; with $T=\{1,\dots,t\}$ , it has a solution if $\sum_{j\in S}a_j=b$ for some $S\subseteq T$ .

In the scheduling problem there are $n$ jobs $J_1,\dots,J_n$ and one machine. Job $J_j$ has a processing time $p_j$ , a weight $w_j$ and a release date $r_j$ , all nonnegative integers. A schedule assigns each job a starting time $B_j\ge r_j$ ; the job completes at $C_j=B_j+p_j$ , and no two jobs are processed at the same time. The problem written $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ in the paper's notation is the class of instances in which every weight is $1$ and every job except the last one, $J_n$ , has release date $0$ . Its recognition version asks, given such an instance and an integer $y$ , whether some schedule has $\sum_jC_j\le y$ .

A problem $P'$ is reducible to $P$ (written $P'\propto P$ ) when every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. The paper's construction maps $a_1,\dots,a_t,b$ (with $0<b<A=\sum_ja_j$ and $a_*=\max_ja_j$ ) to an instance with $n=t+t'+u+1$ jobs in four groups $T$ , $T'$ , $U$ and $\{J_n\}$ , with processing times $\tau+a_j$ , $\tau$ , $\upsilon$ and $1$ , the release date $r_n=t\tau+b$ , and threshold $y=\upsilon+\tfrac12u(u+1)\upsilon$ , where $t'$ , $\tau$ , $u$ , $\sigma$ , $\upsilon$ are explicit polynomials in $t$ , $a_*$ , $b$ and $A$ .

Formalization targets

Goal: Theorem 4(a)

\text{KNAPSACK}\ \propto\ n|1|r_n\ge0,w_j=1|\textstyle\sum w_jC_j ,

stated as CookPvsNP.PolyReducible knapsackLang sumCLangMult: a polynomial-time computable map on binary strings that sends codes of solvable KNAPSACK instances, and only those, to codes of yes-instances of the scheduling problem.

Milestones

Forward direction (p. 22). If $\sum_{j\in S}a_j=b$ , the processing order $(S',S,J_n,T'-S',T-S,U)$ , with $S'=\{t+j\mid j\in T-S\}$ , gives a feasible schedule with $\sum_{j\notin U}C_j\le u$ , $\sum_{j\in U}C_j=u\sigma+\tfrac12u(u+1)\upsilon$ and $\sum_jC_j\le y$ .
Claim (A). In every schedule with $\sum_jC_j\le y$ , all jobs outside $U$ precede all jobs of $U$ .
Claim (B). In every such schedule some job of $U$ starts by time $\sigma$ ; consequently $\sum_{j\notin U}C_j\le u$ .
Claim (C). Exactly $t$ jobs precede $J_n$ .
Claim (D). $B_n=t\tau+b$ .
Equivalence (pp. 22–23). For $0<b<A$ , KNAPSACK has a solution iff the constructed instance has a schedule with $\sum_jC_j\le y$ .

Significance

Together with the NP-completeness of KNAPSACK (Theorem 2(b), quoted from Karp), Theorem 4(a) shows that $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ is NP-complete; with general release dates the problem $1|r_j|\sum C_j$ is then NP-hard as well. The hardness here is in the ordinary sense: the construction is polynomial only in the multiplicity encoding (see below), and the reduction is from KNAPSACK, which has a pseudo-polynomial algorithm.

The result is proved on paper. A formalization adds a machine-checked complexity reduction whose correctness proof is a sequence of delicate counting estimates with large explicit constants; the paper closes the converse with "as is easily seen", and the forward computation and claims (C), (D) contain displayed identities that a formal proof must verify exactly. The definitions (single-machine schedules with release dates, the schedule of a processing order, the multiplicity encoding) are reusable for the other single-machine reductions of the same paper and for later classification results.

Difficulty

The forward direction is a direct computation. The converse is where the difficulty lies: a schedule with $\sum_jC_j\le y$ is arbitrary, may contain idle time, and may interleave the groups. Such a schedule must be shown to be rigid (claims (A)–(D)), and the claims are statements about every schedule, not about a convenient one. Each step compares sums of the form $\sum jτ$ against $u$ with an additive slack smaller than $\tau$ , so the constants must be tracked exactly; an estimate that loses a single $\tau$ breaks the argument. Extracting the knapsack subset at the end requires recognizing which $t$ jobs fill $[0,t\tau+b)$ and why their extra lengths $a_j$ sum to exactly $b$ .

For the goal, the polynomiality of the reduction is not automatic: the constructed instance has $t'=t(t+1)a_*$ and $u$ jobs, which is exponential in the length of the binary KNAPSACK input. The paper's Remark (p. 23) resolves this by encoding groups of identical jobs by their cardinality and one copy of their data, and the formal statement adopts that encoding.

Formalization scope

Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (polynomial-time many-one reducibility in Cook's machine model). Numbers are coded in binary over the four-letter alphabet BSym with encNats from the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's formalization); its own subsetSumLang allows zero entries, so KNAPSACK over positive integers is defined here.
Jobs are indexed by Fin n, 0-based; the groups $T$ , $T'$ , $U$ and $J_n$ are index ranges. Starting times are natural numbers: the paper computes them from processing orders on integer data (Section 3), and claim (D) is false for real starting times.
A schedule is feasible when every job starts at or after its release date and the occupied half-open intervals $[B_j,B_j+p_j)$ are pairwise disjoint; idle time is allowed.
"Precedes" in claims (A) and (C) means "starts earlier on the machine"; there are no precedence constraints.
The claims are stated with exactly the hypotheses the proof uses: the schedule is feasible and $\sum_jC_j\le y$ , for positive $a_j$ , $b$ with $0<b<A$ (the paper's "We may assume that $0<b<A$ ", p. 16).
The halves in $u$ and $y$ are exact natural-number divisions, since the products are even. The letter $u$ is both the size of $U$ and the bound $\sum_{j\notin U}C_j\le u$ , as in the paper.
The goal's target language uses the multiplicity encoding: a list of job types (count, processing time, weight, release date) and $y$ ; the class conditions (unit weights, release date $0$ for every job but the last) are checked on the expanded job list. A one-entry-per-job encoding would make the paper's construction non-polynomial, and the statement would not be the paper's.
Trivializing formalizations are ruled out: the goal includes polynomial-time computability (not just an equivalence of yes-instances), the KNAPSACK language requires positive entries as in the paper, and the target language requires class membership, so mapping to an instance outside the class is not a way out.
Welcome contributions: the arithmetic identities of the construction, the schedule of a processing order and its feasibility, the counting lemmas behind (C) and (D), and polynomial-time computability of the multiplicity-encoded construction in the CookPvsNP model.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, D. B. Shmoys, Sequencing and scheduling: algorithms and complexity, Handbooks in OR & MS 4, 1993, 445–522. https://doi.org/10.1016/S0927-0507(05)80189-6

14 thms3 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

A Functional Equation and Its Application to Resource Allocation and Sequencing Problems 2: Under Precedence Constraints, All Deadlines Can Be Met iff They Are Met in Order of Modified DeadlinesResearch Paper

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$ . Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$ . A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$ , one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$ . Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$ .

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$ , job $i$ must precede job $j$ ; such a $j$ is a successor of $i$ , and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$ .

For a number $\varepsilon$ the modified deadline of job $j$ is

\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ .

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .

Milestones (from §2 and the proof of the Theorem, p. 78)

For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$ .
The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
If $\bar d_j < \bar d_i$ , then $j$ or some successor $k$ of $j$ has $d_k \le d_i$ .
In an on-time sequence consistent with $\rho$ , two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$ .

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$ , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( $\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$ .

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$ : one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$ . That step uses the smallness of $\varepsilon$ : with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$ , $d = (7,9,8)$ , $\varepsilon = 3$ ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$ , a bubble-sort argument over lists.

Formalization scope

Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$ , and the tie-break is $((j:\mathbb N)+1)\varepsilon$ . Processing times and deadlines are real.
Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$ , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
Explicit readings of the paper's phrases:
- " $\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ . A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
- "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$ ": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
- "iρj implies $\bar d_i < \bar d_j$ ": stated for $i \ne j$ , since $\rho$ is reflexive.
- The pair condition "a consecutive pair with $\bar d_i > \bar d_j$ " of milestone 3 is dropped, since the claim does not use it.
Added hypothesis: $a_j \ge 0$ . The paper uses it tacitly (" $j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$ ). The goal assumes the full partial order of the paper.
Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$ ; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

8 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Stochastic Processes Occurring in the Theory of Queues and their Analysis by the Method of the Imbedded Markov Chain: In GI/M/s, a Positive Wait Is Exponential and a Positive Queue GeometricResearch Paper

Motivation

A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).

Timeline:

Erlang (1908–1929) treated M/M/s, where the queue length is itself Markovian.
Kendall (1951) treated M/G/1 by a chain imbedded at departure epochs.
W. L. Smith (Kendall's ref. [19]) observed that for a single server, under restrictions on the input law, exponential service gives an exponential waiting time apart from an atom at zero.
Kendall (1953), this paper, treated GI/M/s for every input law and every number of servers $s$ , and showed that Smith's restrictions are unnecessary.
Foster (1953) gave the criterion for ergodicity of a denumerable chain through a summable invariant vector, which is the step Kendall's argument relies on.

Setting

Customers arrive with independent inter-arrival times of law $A$ on $[0,\infty)$ and mean $a$ , $0<a<\infty$ . There are $s\ge 1$ servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean $b$ , $0<b<\infty$ . The relative traffic intensity is $\rho=b/(sa)$ .

The state of the imbedded chain at an arrival epoch is the number $i\in\{0,1,2,\dots\}$ of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix $P=[p_{ij}]$ of eq. (8) is given in three blocks, written with the death-process probabilities $[n\mid m]=\int_0^\infty\binom{m}{n}(1-e^{-u/b})^n e^{-(m-n)u/b}\,dA(u)$ of (9)–(10), the probabilities $\{n\mid s;m\}$ of (11)–(12), and the Poisson probabilities $(n\mid s)=\int_0^\infty e^{-su/b}(su/b)^n/n!\,dA(u)$ of (13)–(14):

p_{ij}=\begin{cases}(i+1-j\mid s) & j\ge s,\ j\le i+1,\\ [\,i+1-j\mid i+1\,] & i<s,\ j<s,\ j\le i+1,\\ \{s-j\mid s;\,i-s+1\} & i\ge s,\ j<s,\\ 0 & j>i+1.\end{cases}

The key function is

F(\lambda)=\int_0^\infty e^{-(1-\lambda)su/b}\,dA(u).

The queue size met by an arrival is $Q=\max(i-s,0)$ . The waiting time $w$ is, given $i$ , the sum of $k=\max(i-s+1,0)$ independent exponential variables of mean $b/s$ .

Formalization targets

Goal: Theorem IV (p. 350)

When $\rho<1$ the chain has a limiting distribution $\pi$ , and with $\lambda$ the root of $F(\lambda)=\lambda$ in $(0,1)$ and $c=b/(s(1-\lambda))$ ,

\Pr(Q=n\mid Q>0)=(1-\lambda)\lambda^{n-1}\ (n\ge1),\qquad \Pr(w>t\mid w>0)=e^{-t/c}\ (t\ge0),

with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: $\lambda$ and $c$ are determined by $A$ , $b$ and $s$ .

Milestones

The matrix is stochastic (p. 349), and the chain is irreducible and aperiodic (p. 347).
The coefficients $(n\mid s)$ are positive, sum to one and have mean $1/\rho$ ; $F(\lambda)=\sum_n (n\mid s)\lambda^n$ ; for $\rho<1$ the equation $F(\lambda)=\lambda$ has a unique root in $(0,1)$ (p. 348–349).
For the trial vector $x=[\mu_0,\dots,\mu_{s-2},1,\lambda,\lambda^2,\dots]$ (15): the invariance equations for $j\ge s$ are equivalent to $F(\lambda)=\lambda$ ; those for $1\le j\le s-1$ determine the $\mu$ 's; the one for $j=0$ follows from the row sums (pp. 348–349).
A nonnull absolutely summable invariant vector makes the chain ergodic, and normalized it is the limiting distribution (p. 348).
Theorem I: for $\rho<1$ the chain is irreducible and ergodic, and $\pi_j=C\lambda^{j-(s-1)}$ for $j\ge s-1$ .
Theorem II: $\Pr(Q=0)=\alpha=\dfrac{\sum\mu+1+\lambda}{\sum\mu+1/(1-\lambda)}$ and $\Pr(w=0)=\beta=\dfrac{\sum\mu+1}{\sum\mu+1/(1-\lambda)}$ .
Theorem III: $E(Q)=(1-\alpha)/(1-\lambda)$ and $E(w)/b=(1-\beta)/(s(1-\lambda))$ .
Eq. (27): for M/M/s the root is $\lambda=\rho$ .

Significance

Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number $\lambda$ . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing $\lambda$ from a one-dimensional equation and the finitely many $\mu$ 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.

The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of $Q$ and $w$ from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover $s\ge2$ .

Difficulty

The obvious route is to guess the geometric tail and check it against the balance equations. For $j\ge s$ this works, but the rows $i\ge s$ of the block $\mathbf B$ involve the convolution integral (11), and the equations for $j<s$ couple the geometric tail to the boundary terms $\mu_0,\dots,\mu_{s-2}$ . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give $p^n_{ij}\to\pi_j$ . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.

Formalization scope

The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and $w$ by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are $0$ -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all $i,j$ , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by $[0,\infty)$ , integrable, mean $a$ ), and $(n\mid s)$ is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.

Trivializing formalizations are ruled out: $\lambda$ is tied to $F(\lambda)=\lambda$ on $(0,1)$ rather than free; $\pi$ is the limiting distribution of $P$ , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the $\mu$ 's of Theorems II–III are characterized by the invariance equations, never defined from $\pi$ .

A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block $\mathbf B$ , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.

Selected references

D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950, ch. 15.
W. L. Smith, On the distribution of queueing times, Proc. Cambridge Philos. Soc. 49, 449–461, 1953 (cited by Kendall as "to be published", ref. [19]).
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.

22 thms3 active usersReviewed

Analysis Probability·Captain: mikedeng1

The Data-Driven Newsvendor Problem: New Bounds and Insights II: Every Log-Concave Demand Has Weighted Mean Spread at Least min(b,h)/(b+h)Research Paper

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $q$ units before a random demand $D$ is observed, pays $b>0$ per unit of unmet demand and $h>0$ per unit left over, and minimizes the expected cost $C(q)=E[b(D-q)^+ + h(q-D)^+]$ . When the distribution of $D$ is known, the optimal order is the $b/(b+h)$ quantile of $D$ . In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the $b/(b+h)$ quantile of the empirical distribution.

R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is $\epsilon$ -optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in $\epsilon$ , the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by $\min(b,h)/(b+h)$ . That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.

This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.

Setting

Fix costs $b>0$ , $h>0$ and the critical ratio $\beta=b/(b+h)\in(0,1)$ . A demand law is given by a probability density $f:\mathbb R\to\mathbb R$ : measurable, nonnegative, with $\int f=1$ . Its cdf is $F(t)=\int_{(-\infty,t]}f$ , and its $\beta$ quantile is

q^*=\inf\{q : F(q)\ge \beta\}.

The absolute mean spread (AMS, Definition 1) at $t$ is the gap between the conditional means above and below $t$ ,

\Delta(t)=E(D\mid D\ge t)-E(D\mid D\le t)=\frac{\int_{[t,\infty)}x f(x)\,dx}{1-F(t)}-\frac{\int_{(-\infty,t]}x f(x)\,dx}{F(t)},

and the weighted mean spread (WMS, Definition 2) is $\Delta(q^*)f(q^*)$ .

A density is log-concave (Definition 3) if $\log f$ is concave on its support. Equivalently, $f(x)^a f(y)^{1-a}\le f(ax+(1-a)y)$ for all $x,y$ and $a\in[0,1]$ ; this form allows $f$ to vanish outside an interval.

For a log-concave $f$ and a point $t$ with $f(t)>0$ , the number $\gamma_1$ is a supergradient of $\log f$ at $t$ , written $\gamma_1\in\partial\log f(t)$ , if $\log f(x)\le\log f(t)+\gamma_1(x-t)$ for all $x$ with $f(x)>0$ . The paper splits the class $\mathbb L$ of log-concave densities into the subclasses $\mathbb L_{q^*,\gamma_0,\gamma_1}$ of densities with quantile $q^*$ , $f(q^*)=\gamma_0$ and $\gamma_1\in\partial\log f(q^*)$ , and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density

\tilde f(x)=\gamma_0e^{\gamma_1(x-q^*)}\ \text{ on }[\underline x,\overline x],\qquad \underline x=q^*+\tfrac1{\gamma_1}\log\!\big(1-\tfrac{\gamma_1}{\gamma_0}\beta\big),\quad \overline x=q^*+\tfrac1{\gamma_1}\log\!\big(1+\tfrac{\gamma_1}{\gamma_0}(1-\beta)\big),

and zero elsewhere (display (12)), with AMS $z^*_{q^*,\gamma_0,\gamma_1}$ in closed form.

The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.

Formalization targets

Goal: Proposition 2

For every log-concave density $f$ ,

\Delta(q^*)\,f(q^*)\ \ge\ \frac{\min(b,h)}{b+h}.

The statement has no further hypothesis: no moment condition, no continuity, no restriction on $\gamma_0,\gamma_1$ .

Milestones, in the order of the paper's proof

Lemma 1: at the quantile, $-\frac{b+h}{h}\le\frac{\gamma_1}{\gamma_0}\le\frac{b+h}{b}$ .
Lemma 2: $f(x)\le\gamma_0e^{\gamma_1(x-t)}$ for every $x$ .
Lemma 3 (Domination Lemma): a density dominated on the support of another, with the same mass left of $t$ , has the larger AMS at $t$ .
Proposition 1: $\tilde f$ belongs to $\mathbb L_{q,\gamma_0,\gamma_1}$ and minimizes the AMS there.
The closed form: $\Delta_{\tilde f}(q)=z^*_{q,\gamma_0,\gamma_1}=\frac{\gamma_0}{\gamma_1^2}\big[(\frac{b+h}{h}+\frac{\gamma_1}{\gamma_0})\log(1+\frac{\gamma_1}{\gamma_0}\frac{h}{b+h})+(\frac{b+h}{b}-\frac{\gamma_1}{\gamma_0})\log(1-\frac{\gamma_1}{\gamma_0}\frac{b}{b+h})\big]$ .
Lemma 4: three elementary inequalities in $\beta\in(0,1)$ and $\eta\in(-\frac1{1-\beta},\frac1\beta)$ .

Significance

The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is $\epsilon$ -optimal is, asymptotically, at least $1-2\exp(-\frac14N\epsilon\,\Delta(q^*)f(q^*))$ (Theorem 3), and Proposition 2 replaces the unknown $\Delta(q^*)f(q^*)$ by $\min(b,h)/(b+h)$ . A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.

The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.

Difficulty

The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of $\log f$ at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of $t$ is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around $t$ , which is how Proposition 1 uses it. The case $\gamma_1=0$ (uniform minimizer) and the two boundary values of $\gamma_1/\gamma_0$ (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate $f/(1-F)$ and the reversed hazard rate $f/F$ of log-concave laws, which must be proved from log-concavity.

Formalization scope

Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of $D$ is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat $\log f$ as $0$ off the support. The quantile is an sInf; for $\beta\in(0,1)$ its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of $xf(x)$ , since log-concave densities have exponential tails. The value $f(q^*)$ is taken pointwise; $q^*$ lies in the interior of the support, where a log-concave density is continuous.

Conventions and disclosed departures from the page:

" $\gamma_1\in\partial\log f$ , the set of all subgradients" is read as the superdifferential of the concave $\log f$ on $\{f>0\}$ .
Lemma 3 carries three added hypotheses: $f_2$ vanishes outside some $[l,u]\ni t$ and is positive on $(l,u)$ ; $0<F_1(t)<1$ ; and $xf_1(x)$ , $xf_2(x)$ are integrable. The first repairs the printed statement; the other two are the conditions under which Definition 1 makes sense for general densities.
Proposition 1 and the closed form of $z^*$ are stated for $\gamma_1\neq0$ and $\gamma_1/\gamma_0$ strictly inside the interval of Lemma 1, where (12) is a finite interval.
The goal has no such restriction.

Assumption 1 of the paper (monotonicity of $f$ beyond $q^*$ ) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which $f(q^*)$ or $\Delta(q^*)$ takes a junk value (a non-integrable $xf(x)$ , a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.

Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on $\mathbb R$ (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).

Selected references

R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. Authors' accepted manuscript, MIT DSpace. https://doi.org/10.1287/opre.2015.1422
R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272

9 thms3 active usersReviewed

Operations Research

Missions

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 2: Near the Optimal Ratio, a Maximum-Weight Initial Set Is ρ-MaximalResearch Paper

Motivation

Setting

Formalization targets

Goal: the last step of the binary search

Milestones

Significance

Difficulty

Formalization scope

Selected references

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 3: The Nonquadratic Method of Multipliers for Linear Equality Constraints ConvergesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (pp. 212–213)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Residual Life Time at Great Age 5: If |c − ((1 − F)/F′)′| ≤ ε for t ≥ t₀, the Residual Life Normed by (1 − F(t))/F′(t) Is Within ε of Π_{0,c} for t ≥ t₀Research Paper

Motivation

Setting

Formalization targets

Goal: the Corollary to Theorem 7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stable Function Approximation in Dynamic Programming II: In a Nondiscounted MDP with All Policies Proper, Value Iteration Through a Self-Weighted Averager ConvergesResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 4.1 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 3: With One Markdown or Markup Allowed, Thresholds x_n < z_n Give the Optimal PolicyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (pp. 1385–1386)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 2: Markup Is Optimal Once Time-to-Go Exceeds an Increasing Threshold z_nResearch Paper

Why a promotional fare needs a switching rule

Demand, inventory, and admissible decisions

Formalization targets

What the result supplies

Where the difficulty lies

Formalization scope

Selected references

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments IV: Uniform Pricing Earns OPT/(1 + ln(v_m/v_1)) in Unit-Demand Min-PricingResearch Paper

Pricing with unit-demand consumers

Setting

Formalization targets

Goal: Corollary 4.7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Inventory Control and Price Theory 2: For Style Goods with Uniform Demand Linear in Unit Profit, Expected Profit Is Maximized at P* = ((P₀ − 3L) + √((3L − P₀)² + 16P₀L))/4Research Paper

Pricing and stocking a perishable good

Setting

Formalization targets

Goal: the optimal unit profit (Eq. (16))

Milestones, in the order of the paper

Significance

Difficulty

Formalization scope

Selected references