Optimization

Motivation

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$, and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

• 2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
• 2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$, with equality for fully-supported problems.
• 2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$. A problem consists of a cost vector $c\in\mathbb R^d$, a convex domain $\mathcal X\subseteq\mathbb R^d$, convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$, and convex tie-break functions $t_1,\dots,t_p$. Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$, the scenario program is

$$\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.$$

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$, and so on; the resulting solution is $x^*_N$.

• The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$.
• A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
• Assumption 1: for every $m$ and every sample of size $m$, the program with those $m$ constraints has a unique tie-broken solution.
• Assumption 2 (non-degeneracy): for every $m$, with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$,

$$\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.$$

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$-valued $\epsilon(k)$, under Assumptions 1 and 2,

$$\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.$$

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$, which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

1. $s^*_m\le d$ for every sample (quoted from [7]).
2. (14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$, where $A$ adds "the first $k$ constraints are of support".
3. $A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
4. (16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$, with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$.
5. (17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$.
6. (18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$.
7. Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
8. (23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$, and $0$ otherwise.
9. (24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$.

Companions

• Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$, with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$, the probability is at most $\beta$.
• The root lemma of Sect. 5.3, including its sign and divergence claims.
• $\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
• Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$, a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$-dimensional problem, which is far below the a-priori level for dimension $d$. The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

• a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
• the exchangeability argument (14) on product measures;
• the representation (17) of a tail probability through generalized distribution functions;
• a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$-tuple $(F_0,\dots,F_d)$. It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$, which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$. The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

• Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$. $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
• Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
• Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
• Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
• $F_k$. $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$; it is not normalised.
• Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$, with derivatives taken within $[0,1]$. $\gamma^*$ is a real infimum over a set that is nonempty ($\xi(t)=t^N$) and bounded below by $0$.
• Probabilities are compared with real quantities through ENNReal.ofReal.
• Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$, which by its first part is the paper's $\epsilon$.
• Added hypothesis. The constant-$\epsilon$ companion assumes $d\ge1$: at $d=0$, $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

• The solution is never a free function of the sample.
• The goal does not mention $F_k$, moments or polynomials.
• Assumption 1 is not weakened to almost surely.
• $N>d$ is kept on Theorems 1, 2 and Corollary 1.
• The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

• the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
• the exchangeability lemma on Measure.pi;
• the duality and density lemmas, which are pure analysis.

Selected references

• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X

Why minimum-concave-cost flows

Many network design and production–distribution problems have economies of scale: shipping twice as much along an arc costs less than twice as much, because of fixed charges, set-up costs or volume discounts. Modelled as network flows, such problems ask for a flow of least cost when each arc cost is a concave function of the flow on the arc. Classical instances include the uncapacitated lot-sizing problem, the fixed-charge transportation problem, and the Steiner tree problem in graphs. Unlike linear costs, concave costs make the problem NP-hard in general, and the usual linear-programming arguments do not apply directly.

Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987) 634–664) give the send-and-split method, a dynamic program that solves such problems in time exponential only in the number of demand nodes. Before the method can run, two questions must be settled: when does a minimum-cost flow exist at all, and can the arc costs be shifted so that they are nonnegative on flows? Theorem 1 of the paper answers both. This mission formalizes Theorem 1.

Timeline. Hirsch and Hoffman (1961) showed that a concave function bounded below on a polyhedron's extreme rays attains its minimum at a vertex; Rockafellar's Convex Analysis (1970, pp. 61, 343) gives the polyhedral form. Edmonds and Karp (1972) showed how to choose node potentials making linear arc costs nonnegative. Theorem 1 (1987) extends both to additive concave costs on uncapacitated networks.

Setting

A graph $G = (N, A)$ has $n$ nodes and a set $A$ of ordered pairs of distinct nodes, the arcs. A demand vector $r \in \mathbb{R}^n$ assigns a demand $r_i$ to each node (negative demands are supplies). A preflow is a nonnegative matrix $x = (x_{ij})$ carried by the arcs, and a flow for $r$ is a preflow with

$$\sum_{(j,i)\in A} x_{ji} - \sum_{(i,k)\in A} x_{ik} = r_i \qquad (i \in N),$$

inflow minus outflow equal to demand. A circulation is a flow for $r = 0$.

The flow cost is $c(x) = \sum_{(i,j)\in A} c_{ij}(x_{ij})$, where each $c_{ij}$ is concave on $[0,\infty)$ and $c_{ij}(0) = 0$. A minimum-cost flow for $r$ is a flow whose cost is at most that of every flow for $r$.

A preflow induces the subgraph of arcs with nonzero flow. An extreme flow is a flow whose induced subgraph is a forest (in the undirected sense; two antiparallel arcs form a cycle). A simple circuit is a directed cycle through at least two distinct nodes, with arc set $C$; a simple circulation is a circulation whose induced subgraph is a simple circuit. The slope at infinity $\dot c_{ij}(\infty) \in [-\infty, \infty)$ is the limit of the right derivative of $c_{ij}$.

Two nodes are in the same strong component if chains (directed walks) join them both ways; a component is a sink if no chain leaves it. The augmented graph $\underline{G}$ appends a node $\nu$ and an arc $(i,\nu)$ for exactly one node $i$ of each sink component. Its arc costs $\underline{c}$ are $\dot c_{ij}(\infty)$ on arcs inside strong components and arbitrary real numbers elsewhere; $\underline{\pi}_i$ is the infimum of the costs of chains from $i$ to $\nu$. For $\pi \in \mathbb{R}^n$, the altered costs are $c^\pi_{ij}(y) = c_{ij}(y) - (\pi_i - \pi_j) y$.

Formalization targets

Goal: Theorem 1

The following are equivalent:

$$\begin{aligned} &1^\circ\ \text{there is a minimum-cost flow for some demand vector;}\\ &2^\circ\ \text{the null circulation is a minimum-cost circulation;}\\ &3^\circ\ \text{for every } r \text{ with a flow, some minimum-cost flow for } r \text{ is extreme;}\\ &4^\circ\ c(y) \ge 0 \text{ for every simple circulation } y;\\ &5^\circ\ \textstyle\sum_{(i,j)\in C} \dot c_{ij}(\infty) \ge 0 \text{ for every simple circuit with arc set } C;\\ &6^\circ\ \text{there is a minimum-cost chain from each node of } \underline{G} \text{ to } \nu \text{ under } \underline{c}. \end{aligned}$$

If moreover $r$ admits a flow and $\underline{c}_{ij} z \le c_{ij}(z)$ on arcs joining distinct strong components, where $z = \sum_i r_i^+$, they are equivalent to

$$7^\circ\quad \exists \pi\ \ c^\pi_{ij}(x_{ij}) \ge 0 \text{ for all arcs } (i,j) \text{ and all flows } x \text{ for } r,$$

and $\pi = \underline{\pi}$ is real and satisfies $7^\circ$.

Milestones

The milestones are the statements the paper's proof rests on: the Hirsch–Hoffman extension (p. 638), $c^\pi(x) = c(x) + \sum_i \pi_i r_i$, the bounds $\tfrac12 c(2x) + \tfrac12 c(2\theta y) \le c(x+\theta y) \le c(x) + c(\theta y)$, the circuit-wise form of 4° ⇔ 5°, uniqueness of the extreme circulation, $x_{ij} \le z$ between strong components, and the two inequalities giving $7^\circ$ (all p. 639).

Significance

Theorem 1 decides existence of an optimum from the costs alone: conditions 4° and 5° do not mention the demand vector, so one test settles every demand pattern at once, and 3° guarantees the optimum may be sought among extreme (forest) flows, which is what the send-and-split recursion enumerates. Condition 6° is checkable by a shortest-chain computation, and 7° supplies node potentials that convert the instance into an equivalent one with nonnegative arc costs, the standing assumption of the paper's Theorem 2 and of its running-time analysis. For linear costs the theorem reduces to the familiar statement that a minimum-cost flow exists iff no simple circuit has negative cost.

The result is proved in the paper; it has not been machine-checked. The formalization adds a precise model of extreme flows over arcs (so that antiparallel arcs form a cycle), a treatment of slopes that may equal $-\infty$, and the Hirsch–Hoffman extension specialized to network polyhedra, which the paper cites rather than proves. Related platform items cover the linear, capacitated case: CycleCanceling.MinMean.minCost_iff_no_negative_cycle and CycleCanceling.MinMean.minCost_iff_exists_price (Goldberg–Tarjan), and LinearOptimization.positive_directed_cycle_of_circulation and LinearOptimization.network_basic_iff_tree on a different arc encoding.

Difficulty

The first idea, to argue as for linear costs by cancelling negative cycles, fails because concave costs are not additive along cycle decompositions: the cost of a flow is not the sum of the costs of its cycle and path components, and a circuit can be harmless at small flow and arbitrarily negative at large flow. Existence therefore depends on the asymptotic slopes $\dot c_{ij}(\infty)$, which may be $-\infty$, rather than on any finite cost evaluation. The implication from bounded rays to an attained minimum (Hirsch–Hoffman) requires identifying the vertices of the flow polyhedron with forest flows and its extreme rays with simple circulations. The potential step 6° ⇒ 7° needs a cost bound on arcs between strong components, where the concave cost is only controlled up to the total positive demand $z$.

Formalization scope

Nodes are Fin n; a graph is ArcGraph n, a Finset (Fin n × Fin n) of arcs without loops. Preflows are real matrices vanishing off the arcs; arc costs are functions $\mathbb{R} \to \mathbb{R}$, concave on Set.Ici 0 with value $0$ at $0$ (the paper's "without further mention" assumption, made a hypothesis). The augmented graph has nodes Option (Fin n), with none the node $\nu$; chain costs, $\dot c_{ij}(\infty)$ and $\underline{\pi}$ are EReal-valued.

The explicit readings of loose phrases are:

• "minimum-cost flow" is a flow whose cost is at most that of every flow for the same demands (attained, never an infimum);
• "bounded below on each half-line" is $\exists M\ \forall \theta \ge 0,\ M \le c(x+\theta y)$;
• $\dot c_{ij}(\infty)$ is the infimum over $t > 0$ of the right derivative at $t$, equal to the limit by concavity;
• "chain" is a directed walk; "minimum-cost chain" is a chain of real cost at most every chain's cost;
• 6° quantifies over every admissible choice of the appended arcs and of the finite costs $\underline{c}$;
• in the 7° part, "flows $x$" are flows for the given $r$, and the existence of such a flow is an added hypothesis: without it 7° is vacuous while 4° can fail;
• "$\underline{\pi}$ satisfies 7°" uses the real values of $\underline{\pi}$, which the theorem asserts are real.

A formalization in which extreme flows are forests of a simple graph built from the support, in which chains are simple paths, or in which a chain of cost $-\infty$ counts as a minimum would make 3°, 6° or the equivalence trivially or falsely true; all three are ruled out by the definitions. The running-time remarks, the computation paragraph and the linear-cost remark after the proof are not formalized. Contributions are welcome on the polyhedral side (vertices and extreme rays of $\{x \ge 0 : \text{conservation}\}$), on right derivatives of concave functions at infinity, and on walk costs with negative cycles; all are reusable beyond this mission.

Selected references

• R. E. Erickson, C. L. Monma, A. F. Veinott, Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4), 1987, 634–664. https://doi.org/10.1287/moor.12.4.634
• W. M. Hirsch, A. J. Hoffman, Extreme varieties, concave functions, and the fixed charge problem, Communications on Pure and Applied Mathematics 14, 1961, 355–369. https://doi.org/10.1002/cpa.3160140312
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2), 1972, 248–264. https://doi.org/10.1145/321694.321699

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective $\theta \mapsto V^{\pi_\theta}(\mu)$ is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an $O(1/t)$ rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.

Setting

A finite MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions ($\mathcal A$ nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$. Its value $V^\pi(s)$ is the expected discounted sum of rewards $\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid s_0=s]$ when actions are drawn from $\pi$; its state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and its advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. For a distribution $\mu$ on states, $V^\pi(\mu)=\sum_s\mu(s)V^\pi(s)$, and the discounted state visitation distribution is $d^\pi_\mu(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\mu)$. A policy $\pi^\star$ is optimal if $V^{\pi}(s)\le V^{\pi^\star}(s)$ for every policy $\pi$ and every state $s$; $V^\star=V^{\pi^\star}$.

The softmax policy with parameters $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is

$$\pi_\theta(a\mid s)=\frac{\exp(\theta_{s,a})}{\sum_{a'\in\mathcal A}\exp(\theta_{s,a'})}.$$

Softmax policy gradient ascent with step size $\eta$ produces, from an arbitrary $\theta^{(0)}$, the iterates

$$\theta^{(t+1)}=\theta^{(t)}+\eta\,\nabla_\theta V^{(t)}(\mu),\qquad V^{(t)}=V^{\pi_{\theta^{(t)}}} .$$

The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ $=V^{\pi_\theta}(\mu)$, and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.

Formalization targets

Goal: Theorem 5.1

If $\mu(s)>0$ for every state and $0<\eta\le(1-\gamma)^3/8$, then for every state $s$

$$V^{(t)}(s)\longrightarrow V^\star(s)\qquad(t\to\infty).$$

Milestones (Appendices C.1 and D)

1. Lemma C.1, the gradient formula $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a\mid s)A^{\pi_\theta}(s,a)$.
2. Lemma D.1, smoothness $5\|c\|_\infty$ of $\theta_s\mapsto\sum_a\pi_\theta(a\mid s)c_a$.
3. Lemma D.4 at $\lambda=0$, smoothness $8/(1-\gamma)^3$ of $\theta\mapsto V^{\pi_\theta}(\mu)$.
4. Lemma C.2, pointwise monotone improvement of $V^{(t)}(s)$ and $Q^{(t)}(s,a)$ for $\eta\le(1-\gamma)^2/5$.
5. Lemma C.3, existence of the limits $V^{(\infty)}$, $Q^{(\infty)}$ and the bound (40).
6. Lemma C.4, eventual sign separation (41) of the advantages on $I^s_+=\{a:Q^{(\infty)}(s,a)>V^{(\infty)}(s)\}$ and $I^s_-=\{a:Q^{(\infty)}(s,a)<V^{(\infty)}(s)\}$.
7. Lemma C.5, vanishing gradients, $\pi^{(t)}(a\mid s)\to0$ off $I^s_0=\{a:Q^{(\infty)}(s,a)=V^{(\infty)}(s)\}$, and $\sum_{a\in I^s_0}\pi^{(t)}(a\mid s)\to1$.
8. Lemma C.6, eventual strict monotonicity of $\theta^{(t)}_{s,a}$ on $I^s_\pm$.
9. Lemma C.7, divergence of $\max_{a\in I^s_0}\theta^{(t)}_{s,a}$ and $\min_a\theta^{(t)}_{s,a}$ when $I^s_+\neq\emptyset$.
10. Lemma C.11, lower boundedness of $\theta^{(t)}_{s,a}$ on $I^s_+$ and $\theta^{(t)}_{s,a}\to-\infty$ on $I^s_-$.

The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.

Significance

The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to $V^\star$ at every state, not only on average under $\mu$. It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether $\mu>0$ can be dropped.

The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.

Difficulty

The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from $\nabla_\pi V^\pi(\mu)\to0$, but under softmax $\partial V/\partial\theta_{s,a}=\pi_\theta(a\mid s)\,\partial V/\partial\pi_\theta(a\mid s)$, so a vanishing $\theta$-gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters $\theta^{(t)}_{s,a}$ move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets $I^s_0, I^s_\pm$ and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.

Formalization scope

Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in $[0,1]$, $0\le\gamma<1$); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\theta$; the coordinate $(s,a)$ of the gradient is $\partial/\partial\theta_{s,a}$. Logarithms do not appear. Conventions committed to:

• $V^\star(s)$ is PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.
• The step size satisfies $0<\eta$, which "gradient ascent" presupposes and the page does not write; at $\eta=0$ the theorem is false.
• $\mu(s)>0$ for every $s$ is a hypothesis of the goal and of Lemmas C.5–C.11; Lemmas C.1–C.4 are stated without it, and Lemma C.1 for an arbitrary real weighting $\mu$.
• In Lemmas C.4–C.11 the limits $V^{(\infty)}$, $Q^{(\infty)}$ are parameters with the hypotheses that they are the limits of $V^{(t)}$, $Q^{(t)}$. The paper's $\Delta=\min_{A^{(\infty)}(s,a)\neq0}|A^{(\infty)}(s,a)|$ is replaced by any $\Delta>0$ bounded by every nonzero $|A^{(\infty)}(s,a)|$, which avoids an undefined minimum over an empty set.
• "$\to\pm\infty$" is Tendsto … atTop atTop / atBot; "strictly increasing for $t\ge T_1$" is StrictMonoOn on Set.Ici T1, with $T_1$ existentially quantified.

The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets $I^s_0, I^s_\pm$; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis $I^s_+\neq\emptyset$ of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.

A full development needs: differentiability of $\theta\mapsto V^{\pi_\theta}$ and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for $L$-smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation

Assortment planning with nested choice

A retailer that groups its products into categories (brands, store sections, flight classes) and decides which products to display in each faces the assortment problem: offering more products attracts more customers but also diverts sales away from the most profitable products. The nested logit model is the standard description of customer choice in this setting. A customer first selects a category (a nest), then a product within it. Choice-based models of this kind are the basis of revenue management under customer choice (Talluri and van Ryzin 2004).

Davis, Gallego and Topaloglu (DGT 2014) study the assortment problem under the nested logit model with two features that earlier work excluded: dissimilarity parameters larger than one, under which products in a nest act as complements rather than substitutes, and a no-purchase option inside each nest, under which a customer may enter a nest and still leave without buying. They show that the problem is NP-hard once either feature is present. For each regime they give a small linear program whose solution yields an assortment with a provable performance guarantee. This mission formalizes the guarantee for the most general instances, where both features occur together (§6.1, Theorem 11).

Timeline. Rusmevichientong, Shmoys and Topaloglu (2010) bound nested-by-revenue assortments under a multinomial logit mixture. [DGT 2014] prove that nested-by-revenue assortments are optimal for dissimilarity parameters at most one without within-nest no-purchase options (Theorem 4). They give factor-(6) guarantees with synergistic products, a factor-two guarantee via knapsack relaxations for partially-captured nests (Theorem 10), and the general factor (12) of Theorem 11. Li, Rusmevichientong and Topaloglu (2015) extend the nested-by-revenue result to $d$-level nested logit models.

The model

There are nests $i\in M=\{1,\dots,m\}$ and, in each nest, products $j\in N=\{1,\dots,n\}$. Product $j$ of nest $i$ has revenue $r_{ij}\ge0$ and preference weight $v_{ij}>0$, with $r_{i1}\ge r_{i2}\ge\dots\ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0}\ge0$ and a dissimilarity parameter $\gamma_i>0$, and $v_0\ge0$ is the weight of choosing no nest at all. For an assortment $S_i\subseteq N$,

$$V_i(S_i)=v_{i0}+\sum_{j\in S_i}v_{ij},\qquad R_i(S_i)=\frac{\sum_{j\in S_i}r_{ij}v_{ij}}{V_i(S_i)} .$$

A customer chooses nest $i$ with probability $V_i(S_i)^{\gamma_i}/(v_0+\sum_l V_l(S_l)^{\gamma_l})$, and the expected revenue is

$$\Pi(S_1,\dots,S_m)=\frac{\sum_{i}V_i(S_i)^{\gamma_i}R_i(S_i)}{v_0+\sum_{i}V_i(S_i)^{\gamma_i}} .$$

The optimal value $Z^*$ of $\max\Pi$ equals the optimal value of the linear program

$$\text{(3)}\qquad \min\ x\quad\text{s.t.}\quad v_0x\ge\sum_i y_i,\qquad y_i\ge V_i(S_i)^{\gamma_i}\big(R_i(S_i)-x\big)\ \ \forall S_i\subseteq N,\ i\in M,$$

which has $2^n$ constraints per nest. Problem (4) keeps only the constraints for a chosen candidate collection of assortments in each nest.

A nest is fully captured if $v_{i0}=0$ ($i\in M^f$) and partially captured if $v_{i0}>0$ ($i\in M^p$). $N_{ij}=\{1,\dots,j\}$ is the nested-by-revenue assortment. $N^k_{ij}$ is the set of the $j$ highest-revenue products among the $k$ products of nest $i$ with the smallest preference weights, with $N^k_{i0}=\emptyset$ and $N^n_{ij}=N_{ij}$.

Formalization targets

Goal: Theorem 11

Let $(\hat x,\hat y)$ be an optimal solution of (4) when the candidate collection of every nest is $\{N^k_{ij}:k\in N,\ j=0,\dots,k\}\cup\{\{j\}:j\in N\}$, and let

$$\beta=\max_{i\in M^f,\ j=2,\dots,n}\left\{\frac{V_i(N_{ij})}{V_i(N_{i,j-1})}\right\}\vee\max_{i\in M^p,\ j=1,\dots,n}\left\{\frac{V_i(N_{ij})}{V_i(N_{i,j-1})}\right\}\vee2 \qquad (12).$$

Then $(\beta\hat x,\beta\hat y)$ is feasible for problem (3).

The theorem assumes $\bar\gamma=\max_i\gamma_i>1$, as all of §6 does. Otherwise it places no restriction on the $\gamma_i$ or the $v_{i0}$.

Milestones

1. $\hat x\ge0$ (A.4, p. 46).
2. Every greedy knapsack assortment $\hat S_i(\epsilon_i)$ of §5 is one of the $N^k_{ij}$ (pp. 24–25).
3. The relaxed nest problem over $[0,1]^n$ has an optimal solution of fractional-prefix form (A.4 Case 1, p. 47).
4. Inequality (30): for a nest with $\gamma_i>1$ and $\hat y_i\ge0$, $\beta\hat y_i$ bounds the relaxed objective at every fractional prefix (p. 47).
5. Case 1: $\gamma_i>1$, $\hat y_i\ge0$ gives the constraints of (3) for nest $i$ (pp. 47–48).
6. Problem (31) has a nested-by-revenue optimal solution when $\gamma_i>1$ and its coefficient $b=\beta\hat y_i$ is negative (p. 48).
7. Case 2: $\gamma_i>1$, $\hat y_i<0$ (p. 48).
8. Case 3: $\gamma_i\le1$, through the factor-two argument of Theorem 10 (pp. 48–49).

Two companions follow the goal. One is the resulting guarantee $\beta\,\Pi(\hat S)\ge Z^*\ge\Pi(\hat S)$, through Theorem 1. The other is the bound $\beta\le2\kappa$ when the preference weights within a nest differ by at most a factor $\kappa$ (p. 26).

Significance

Theorem 11, combined with Theorem 1 of the paper, gives a polynomial-size method for an NP-hard problem. The method solves one linear program with $1+m$ variables and $1+m(1+n+n^2)$ constraints, then reads off an assortment whose expected revenue is within the factor $\beta$ of the optimum. This holds for every nested logit instance, including nests where customers may walk away and nests whose products are complements. When the weights inside each nest are within a factor $\kappa$ of each other, the guarantee is at most $2\kappa$.

The theorem is proved in the paper's appendix. No part of it is machine-checked. Formalizing it checks a case analysis that reuses, by reference, arguments from two other theorems: Theorem 7 (synergistic, fully-captured nests) and Theorem 10 (competitive, partially-captured nests). It makes precise what these arguments need when the two regimes are mixed in one instance. The formalization also fixes the boundary conventions the printed proof leaves implicit: fully-captured nests with $k=1$, zero-weight denominators, and the sign of $\hat y_i$.

Difficulty

Each nest falls into one of three regimes, and a different argument controls each. With $\gamma_i\le1$ the nest behaves like a knapsack problem. Its guarantee of two needs the knapsack collection of §5 to sit inside $\{N^k_{ij}\}$. With $\gamma_i>1$ and $\hat y_i\ge0$, the constraint must be extended from nested-by-revenue sets to every subset. This goes through a continuous relaxation whose optimum has a fractional coordinate, and it costs the ratio $V_i(N_{ik})/V_i(N_{i,k-1})$, which is where (12) comes from. With $\gamma_i>1$ and $\hat y_i<0$, the scaling argument of Case 1 fails because multiplying by a factor at most one no longer preserves the inequality. The proof switches to the different objective (31), whose convexity in one coordinate forces an integral optimum.

The first idea, bounding every assortment by a nested-by-revenue one, is false here. With $\gamma_i>1$ or $v_{i0}>0$, nested-by-revenue assortments are not optimal, and the loss is exactly the factor $\beta$.

Formalization scope

Products are Fin n; $N_{ij}$ is nbr n j. Powers are Real.rpow, and $x/0=0$, so $R_i(\emptyset)=0$. Problems (3) and (4) are stated in constraint form: LP4Optimal means feasible and with $x$ minimal among feasible points. $\beta$ is the greatest element of the finite set betaSet I, which contains $2$ and the ratios of (12). Fully-captured nests skip $j=1$, as on the page. The collection is constructed: nestedPR breaks weight ties by index and revenue ties by index.

Standing assumptions, all disclosed:

• $v_{ij}>0$, $r_{ij}\ge0$ and $\gamma_i>0$. The page allows zero-weight padding products and $\gamma_i=0$, but its arguments do not cover them.
• $\bar\gamma>1$ on every statement set in Theorem 11's context.
• $n\ge1$ for the collection claim and the prefix claim.
• $v_{i0}>0$ for the statement about (31). That is the only kind of nest where Case 2 arises. For $v_{i0}=0$, Lean's $0^{1-\gamma_i}=0$ would remove the page's $+\infty$.
• $v_0>0$ for the guarantee, where Theorem 1 fails otherwise.
• $\kappa\ge1$, and $v_{i0}$ counted among the weights of a partially-captured nest ($v_{ij}\le\kappa v_{i0}$, $v_{i0}\le\kappa v_{ij}$), for the $2\kappa$ bound.

A trivializing formalization is ruled out. The goal states only feasibility for (3), with $\beta$ the maximum of (12), not any upper bound. The collection is the page's, not an arbitrary family containing it. The goal mentions none of the cases or the relaxations.

A complete development needs continuous knapsack solutions (greedy optimality, fractional prefixes), convexity of $t\mapsto t^{1-\gamma}$ on $(0,\infty)$, and the factor-two argument of Theorem 10. The knapsack and fractional-prefix lemmas are reusable for the companion missions of this series. Proofs of individual cases, and proofs of milestones in greater generality, are welcome.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013). https://doi.org/10.1287/opre.2014.1256
• P. Rusmevichientong, D. B. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, technical report, Cornell University, 2010. http://legacy.orie.cornell.edu/~huseyin/publications/publications.html
• G. Li, P. Rusmevichientong, H. Topaloglu, The d-level nested logit model: assortment and price optimization problems, Operations Research 63(2), 2015.
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Scheduling precedence-constrained jobs on machines of different speeds

Graham (1966) showed that list scheduling finds a schedule within a factor $2$ of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem $Q|prec|C_{\max}$ resisted a guarantee independent of the speeds better than $O(\sqrt m)$.

Timeline:

• 1974, Liu and Liu: list scheduling on machines of different speeds, with a guarantee that depends on the speeds and can be arbitrarily large even for a fixed number of machines.
• 1980, Jaffe: list scheduling on the machines whose speed is within a factor $\sqrt m$ of the fastest gives an $O(\sqrt m)$-approximation.
• 1978, Lenstra and Rinnooy Kan: with precedence constraints, no $\rho$-approximation with $\rho < 4/3$ exists unless P = NP. This bound already holds for identical machines.
• 1997–1999, Chudak and Shmoys: an LP-guided variant of list scheduling achieves $O(\log m)$, and $K + 2\sqrt K + 1$ when there are only $K$ distinct speeds (J. Algorithms 30 (1999) 323–343; conference version SODA 1997).

The mission formalizes the makespan half of that paper, up to its Theorem 3.7.

Setting

An instance has $n$ jobs and $m \ge 1$ machines. Job $j$ requires $p_j > 0$ units of processing, and machine $i$ runs at speed $s_i > 0$, so job $j$ takes $p_j/s_i$ time units on machine $i$. A strict partial order $\prec$ on the jobs gives precedence constraints: $j \prec k$ means that job $k$ may not start until job $j$ has completed.

A schedule runs each job $j$ without interruption on one machine $\mu(j)$, from a start time $S_j \ge 0$ to its completion time $C_j = S_j + p_j/s_{\mu(j)}$. A machine processes at most one job at a time, and $j \prec k$ forces $C_j \le S_k$. Its length is $C_{\max} = \max_j C_j$. $C^*_{\max}$ is the length of an optimal schedule.

Let $\bar s_1 > \bar s_2 > \cdots > \bar s_K$ be the distinct speeds and $m_k$ the number of machines of speed $\bar s_k$. An assignment $k(j)$ names the speed class at which job $j$ is to run. Its loads are $D_k = \frac{1}{m_k}\sum_{j:k(j)=k} p_j/\bar s_k$, and its chain bound $C$ is the largest value of $\sum_{j\in\mathcal C} p_j/\bar s_{k(j)}$ over chains $\mathcal C$ of $\prec$. Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed $\bar s_k$ is idle, it starts the first available job $j$ on the list with $k(j) = k$.

The linear program LP has variables $x_{kj} \ge 0$, $C_j$ and $D$. It minimizes $D$ subject to the following constraints:

• $\sum_k x_{kj} = 1$;
• $\frac{1}{m_k\bar s_k}\sum_j p_j x_{kj} \le D$;
• $\sum_k (p_j/\bar s_k)x_{kj} \le C_j$, and $\sum_k (p_j/\bar s_k)x_{kj} \le C_j - C_{j'}$ whenever $j' \prec j$;
• $C_j \le D$.

From a solution, with $\bar p_j = \sum_k (p_j/\bar s_k)x_{kj}$, the assignment algorithm gives each job $j$ the speed class $k \notin B_j = \{k : p_j/\bar s_k > \gamma\bar p_j\}$ of largest capacity $\bar s_k m_k$.

Formalization targets

Goal: Theorem 3.7 (p. 10)

There is an absolute constant $c$ such that for every instance with $m \ge 2$ machines and $K$ distinct speeds, the better of the two schedules below has length at most

$$\min\bigl\{K + 2\sqrt K + 1,\ 1.89\log_2 m + c\sqrt{\log_2 m}\bigr\}\cdot C^*_{\max}.$$

• (A) An optimal LP solution, the assignment algorithm with $\gamma = \sqrt K + 1$, and speed-based list scheduling.
• (B) The same algorithm run on speeds rounded down to powers of $e$, with machines slower than $\bar s_1/(m\log_2 m)$ dropped, and read back on the original machines.

Milestones, in proof order

• Existence of speed-based list schedules (p. 4).
• Theorem 2.1: $C_{\max} \le C + \sum_k D_k$.
• The LP lower bound $\bar D \le C^*_{\max}$ (p. 6).
• Lemmas 3.1–3.4: chain bounds $2\bar D$ and $(\sqrt K + 1)\bar D$, and load bounds $2K\bar D$ and $(K + \sqrt K)\bar D$.
• Theorem 3.5 and Corollary 3.6: the factor $K + 2\sqrt K + 1$ against $C^*_{\max}$ and against $\bar D$.
• Rounded schedules serve the original instance (p. 9).
• The speed rounding: at most $\lfloor\log_\beta(\alpha m)\rfloor + 1$ speeds, and the LP value grows by a factor of at most $\beta(1 + 1/\alpha)$ (p. 10).
• The "In fact" form of the guarantee, relative to any feasible LP solution (p. 10).

Significance

The result gives the first $O(\log m)$ guarantee for $Q|prec|C_{\max}$, independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an $O(\log m)$ bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's $\sum w_jC_j$ algorithm in §4.

The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:

• the continuous-time list-scheduling argument for different speeds;
• the filtering argument of Lin and Vitter;
• the reduction to logarithmically many speeds, including the off-by-one count of rounded speeds that the page leaves implicit.

Later work gave a combinatorial $O(\log m)$-approximation (Chekuri and Bender, 2001) and an $O(\log m/\log\log m)$-approximation (Li, 2017). These are not part of this mission.

Difficulty

Graham's argument has two lower bounds:

1. the total processing along a chain;
2. the time during which every machine is busy.

With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about $C^*_{\max}$. Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.

Formalization scope

• Representation. Jobs are Fin n and machines Fin m with $m \ge 1$. $p_j > 0$ and $s_i > 0$. $\prec$ is a strict partial order, and a chain is a finite set of pairwise comparable jobs. $C_{\max}$ is the maximum completion time, or $0$ with no jobs.
• Speed classes. The classes are computed from the speeds, so $m_k \ge 1$ and $\bar s_k > 0$ by construction. The Lean index $0$ is the paper's fastest class $\bar s_1$.
• The algorithm as predicates. Speed-based list scheduling is the predicate the proof of Theorem 2.1 uses: jobs run at their assigned speed, and no machine of a job's speed idles while that job is available and unstarted. Every list order and every order of idle machines satisfies it. The assignment algorithm is a predicate allowing every maximizer, since the page does not break ties. Theorems 3.5 and 3.7 quantify over all optimal LP solutions, all such assignments and all such schedules. Existence is supplied by the milestones.
• Comparator. The bound is stated against every feasible schedule of the same instance, never against the LP value or a best schedule of the rounded instance. A statement asserting only that some good schedule exists would be trivially true (the optimum witnesses it); the goal bounds the schedule the algorithm returns.
• Constants and logarithms. $\log m$ is $\log_2 m$, as the paper specifies. $m \ge 2$ is assumed in Theorem 3.7 and in the "In fact" remark, which are asymptotic in $m$. The $O(\sqrt{\log m})$ term is one absolute constant $c$, quantified before the instance, and $1.89$ is the page's number.
• Generalizations and corrections. Lemmas 3.1–3.4 are stated for every feasible LP solution, since their proofs use only feasibility. The speed rounding is relative to $\bar s_1$, with no normalization. The count of rounded speeds is $\lfloor\log_\beta(\alpha m)\rfloor + 1$; the page writes $\log_\beta(\alpha m)$.
• Not formalized. Polynomial running time is not formalized.
• Out of scope. Corollaries 3.8–3.10, Theorem 3.11 and §4 are excluded.

Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.

Selected references

• F. A. Chudak and D. B. Shmoys, Approximation algorithms for precedence-constrained scheduling problems on parallel machines that run at different speeds, J. Algorithms 30 (1999) 323–343 (authors' manuscript used here). https://doi.org/10.1006/jagm.1998.0987
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45 (1966) 1563–1581. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• J. M. Jaffe, Efficient scheduling of tasks without full use of processor resources, Theoretical Computer Science 12 (1980) 1–17. https://doi.org/10.1016/0304-3975(80)90002-4
• J.-H. Lin and J. S. Vitter, ε-approximations with minimum packing constraint violation, STOC 1992, 771–782. https://doi.org/10.1145/129712.129787
• D. B. Shmoys, J. Wein and D. P. Williamson, Scheduling parallel machines on-line, SIAM J. Computing 24 (1995) 1313–1331. https://doi.org/10.1137/S0097539793248317
• C. Chekuri and M. A. Bender, An efficient approximation algorithm for minimizing makespan on uniformly related machines, J. Algorithms 41 (2001) 212–224. https://doi.org/10.1006/jagm.2001.1184
• S. Li, Scheduling to minimize total weighted completion time via time-indexed linear programming relaxations, SIAM J. Computing 46 (2017) 409–440. https://doi.org/10.1137/15M1053163

Motivation

A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?

Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor $1-1/(2\sqrt{\min\{n,\lambda^*t\}})$ of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.

Setting

Demand. The firm chooses a demand intensity $\lambda$ from an interval $\Lambda\ni 0$ of allowable rates, and the market charges the inverse-demand price $p(\lambda)$. On nonzero rates, $p$ is strictly decreasing and nonnegative; rate $0$ corresponds to the null price $p_\infty$, at which nothing sells. The revenue rate is $r(\lambda)=\lambda p(\lambda)$. It has $r(0)=0$, and it is continuous, concave and bounded on $\Lambda$. $\lambda^*$ denotes its least maximizer, and $p^*=p(\lambda^*)$, $r^*=r(\lambda^*)$. Such data form a regular demand function (§2.1).

The stochastic problem. At time $0$ the firm holds $n$ items and has a horizon $[0,t]$. A non-anticipating pricing policy $u$ chooses the intensity $\lambda_s\in\Lambda$ at each elapsed time $s$ as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most $n$ items can be sold. A sale at time $s$ earns the current price $p_s$. The expected revenue is $J_u(n,t)=E_u[\int_0^t p_s\,dN_s]$, where $N_s$ counts the sales, and the optimal expected revenue is $J^*(n,t)=\sup_u J_u(n,t)$.

The deterministic problem. Replacing random sales by their rates gives

$$J^D(x,t)=\sup\Big\{\int_0^t r(\lambda(s))\,ds:\ \lambda(s)\in\Lambda,\ \int_0^t\lambda(s)\,ds\le x\Big\}.$$

It is solved by the constant rate $\lambda^D=\min\{\lambda^*,x/t\}$ (Proposition 2).

Fixed-price heuristics. $J^{FP}(n,t)$ is the expected revenue of charging $p^D=p(\lambda^D)$ for the whole horizon. $J^{OFP}(n,t)$ is the expected revenue of the best constant price.

Formalization targets

Goal: Theorem 3

For $\lambda^*>0$, $n\ge1$ and $t>0$, $J^*(n,t)$ is finite and positive, and

$$\frac{J^{OFP}(n,t)}{J^*(n,t)}\ \ge\ \frac{J^{FP}(n,t)}{J^*(n,t)}\ \ge\ 1-\frac{1}{2\sqrt{\min\{n,\lambda^*t\}}}.$$

Milestones

1. Proposition 2: $\lambda^D$ solves (11), and $J^D(x,t)=t\,r(\lambda^D)$.
2. Eqs. (13)–(14): $E_u[N_t]=E_u[\int_0^t\lambda_s ds]\le n$ and $J_u(n,t)=E_u[\int_0^t r(\lambda_s)ds]$ for every policy.
3. Eq. (15) and Lemma 1: $J_u(n,t)\le J_u(n,t,\mu)\le J^D(n,t,\mu)$ for all $\mu\ge0$.
4. The zero duality gap: $J^D(n,t)=\min_{\mu\ge0}J^D(n,t,\mu)$.
5. Theorem 2: $J^*(n,t)\le J^D(n,t)$ for all $n\ge 0$, $t\ge0$.
6. Eq. (17): a fixed price $p$ earns $p\,E[\min\{n,N_{\lambda(p)t}\}]$, with $N$ Poisson.
7. Inequality (18), Gallego's bound $E[(N-n)^+]\le(\sqrt{\sigma^2+(n-\mu)^2}-(n-\mu))/2$, already on the platform.
8. The two case bounds of the proof of Theorem 3, including (19), and the exact fixed-price revenue of the Remark.

Significance

The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.

Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.

Difficulty

The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity $E_u[\int p_s\,dN_s]=E_u[\int r(\lambda_s)\,ds]$ for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to $J_u$ directly. It fails because the stock constraint holds only pathwise, through $N_t\le n$, and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.

Formalization scope

• Model. Rates are real numbers, and $\Lambda\subseteq[0,\infty)$ is an interval containing $0$. $p$ is a real function, strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$. $r(\lambda)=\lambda p(\lambda)$ is continuous, concave and bounded above on $\Lambda$, and $\lambda^*$ is its least maximizer. $p(0)$ is never used, since the null price may be $+\infty$.
• Policies depend on elapsed time and the past sale times (the internal history); randomized policies are not included. Intensities are jointly measurable and locally integrable.
• The sales process is built from i.i.d. $\mathrm{Exp}(1)$ clocks, one per item. A sale occurs when the intensity integrated since the last sale reaches the next clock, so at most $n$ items are sold. Constraint (2) is part of the construction, not a hypothesis.
• Values. Expected revenues and $J^*$ are in $[0,\infty]$, as lower Lebesgue integrals and suprema. $J^D$ is a real supremum over measurable, integrable rate paths, nonempty and bounded for $x,t\ge0$. $J^{FP}$ and $J^{OFP}$ are expected revenues of constant-price policies of this process, and the goal also asserts $0<J^*<\infty$. Defining $J_u$ by the right side of (14), $J^*$ by the HJB equation, or $J^{FP}$ by formula (17) would trivialize the mission, and is ruled out.
• Added hypotheses. Theorem 3 assumes $n\ge1$, $t>0$ and $\lambda^*>0$, which the page leaves implicit: the ratios divide by $J^*$, which vanishes otherwise. Eqs. (13)–(14) are stated for every policy, without Proposition 1's bound $\lambda_s\le\lambda^*$, and without the reduction to Markovian policies.
• Corrected slips. (12) prints $J^D(x,t)=t\min\{r^*,r^0\}$, which is false for $x>\lambda^*t$ (exponential demand with $x=at$ gives $r^0=0$). The statement uses $t\,r(\lambda^D)$, and the printed form where $x\le\lambda^*t$. The Remark's "$E(N_n-n)^+=n(1-P\{N_n=n\})$" should read $E[\min\{N_n,n\}]$; its displayed $J^{FP}$ formula is right. Proposition 2's "the optimal solution" is stated as optimality, since uniqueness fails without strict concavity.
• Welcome contributions. Infrastructure for counting processes with stochastic intensity (the clock construction, the compensator identity), Jensen and Lagrangian duality for concave integral functionals on rate paths, and Poisson truncated-mean computations.

Selected references

• G. Gallego, 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
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11:55–60, 1992 (cited in the paper's references, p. 1019).
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the paper).
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004 (Chapter 5; on the platform as RevenueManagement.*).
• G. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003 (on the platform as PricingRM.DetHeuristic.*).