Operations Research

Motivation

Many planning problems are made in two stages: a first decision $x$ (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision $y$ (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy $\omega\mapsto y(\omega)$, and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair $(x,y)$ that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).

The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.

Setting

Fix $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$ and nonnegative costs $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$. A set $\Omega$ of scenarios carries a probability measure $\mu$, and each scenario $\omega$ has a right-hand side $b(\omega)\in\mathbb R^m_+$. The uncertainty set is $\mathcal I_b(\Omega)=\{b(\omega):\omega\in\Omega\}$. First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ($p_2=0$).

The stochastic problem $\Pi_{\mathrm{Stoch}}(b)$, (1.1), chooses $x$ and a policy $y(\cdot)$:

$$z_{\mathrm{Stoch}}(b)=\inf\ c^Tx+\mathbb E_\mu[d^Ty(\omega)]\quad\text{s.t.}\quad Ax+By(\omega)\ge b(\omega)\ \ \forall\omega\in\Omega .$$

The robust problem $\Pi_{\mathrm{Rob}}(b)$, (1.2), chooses one $y$ for all scenarios:

$$z_{\mathrm{Rob}}(b)=\inf\ c^Tx+d^Ty\quad\text{s.t.}\quad Ax+By\ge b(\omega)\ \ \forall\omega\in\Omega .$$

A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for all $z$; $u^0$ is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection $\{2u^0-x\}$ the same mass.

Formalization targets

Goal: Theorem 2.1 (p. 10)

If $\mathcal I_b(\Omega)$ is symmetric with point of symmetry $b(\omega^0)$, $p_2=0$, and $\mu$ satisfies

$$\mathbb E_\mu[b(\omega)]\ \ge\ b(\omega^0)\qquad(2.1)$$

then

$$z_{\mathrm{Rob}}(b)\ \le\ 2\cdot z_{\mathrm{Stoch}}(b).$$

Milestones on the way

• Lemma 2.2 (p. 12): the coordinatewise bounding box $H$ of a symmetric set $S$ is the smallest hypercube containing $S$.
• Lemma 2.3 (p. 12): the centre $x^0$ of $H$ is the point of symmetry of $S$, and $x\le 2x^0$ on $S$ when $S\subseteq\mathbb R^n_+$.
• Eqs. (2.9)–(2.10) (p. 13): if $(x,y)$ covers $b(\omega^0)$ then $(2x,2y)$ covers every $b(\omega)$, so it is robust feasible.
• p. 14 display: under (2.1), the mean second-stage decision $\mathbb E_\mu[y(\omega)]$ covers $b(\omega^0)$.
• Lemma 2.1 (p. 11): a symmetric probability measure has mean $u^0$, so it satisfies (2.1).
• Theorem 2.7 (p. 21): the same bound $z_{\mathrm{Rob}}(b)\le 2\,z_{\mathrm{Stoch}}(b)$ when $\mathcal I_b(\Omega)$ is convex and positive (contained in a symmetric subset of $\mathbb R^m_+$ whose centre lies in $\mathcal I_b(\Omega)$).

Significance

The result. The robust problem is one mixed-integer program, independent of $\mu$; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution $(x,y)$ used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least $n+1$) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).

Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).

Difficulty

Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of $\Pi_{\mathrm{Stoch}}(b)$; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from "$Ax+By(\omega)\ge b(\omega)$ for all $\omega$" to "$Ax+B\,\mathbb E_\mu[y]\ge\mathbb E_\mu[b]$" needs integrability of the policy and of $b$ and linearity of the Bochner integral through a matrix. The bound $b(\omega)\le 2b(\omega^0)$ uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since $\mathbb E_\mu[y(\omega)]$ need not be integral.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set $I$ of coordinates", which is the paper's $\mathbb R^{n-p}_+\times\mathbb Z^p_+$ up to relabelling.
• $\Omega$ is an arbitrary measurable space with a probability measure; $\mathcal I_b(\Omega)$ is Set.range b. Constraints hold for every scenario, not almost surely.
• Second-stage policies are $\mu$-integrable, and $b$ is $\mu$-integrable in every statement that uses (2.1). Without these, Lean's integral of a non-integrable function is $0$ and (2.1) would degenerate.
• $z_{\mathrm{Stoch}}$ and $z_{\mathrm{Rob}}$ are infima in EReal, equal to $+\infty$ when infeasible; no attainment is assumed. A real-valued infimum would return $0$ on an infeasible robust problem and make the goal trivial; that formalization is ruled out.
• The bounding box of (2.5)–(2.7) uses suprema and infima, with boundedness assumed where needed.
• Corrections to the page: Lemma 2.3's inequality $x\le 2x^0$ is stated under $S\subseteq\mathbb R^n_+$, which its proof uses and which holds in every application; Lemma 2.1 assumes the measure has a mean; Theorem 2.7 carries the standing assumption $p_2=0$ of §2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace)
• A. Ben-Tal, A. Nemirovski, Robust optimization — methodology and applications, Mathematical Programming 92, 2002. https://doi.org/10.1007/s101070100286
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106, 2006. https://doi.org/10.1007/s10107-005-0578-0
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134, 2012. https://doi.org/10.1007/s10107-011-0444-4

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$. The stock at the beginning of the horizon is $x_0$. Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

$$x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).$$

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$, a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$. A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$. The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

Each period costs $C(u_k) + R(x_{k+1})$. The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$, with $c > 0$ and $K \ge 0$. The holding/shortage cost is $R(x) = \max(hx, -px)$, with $h \ge 0$ and $p > c$. The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$.

For each $k$, $A_k$ is the optimal value of the linear program

$$A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)$$

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$. Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$:

• $u_k \ge 0$, $q_k \ge 0$, and $r_{ik} \ge 0$, $q_k + r_{ik} \ge \hat w_i$ for $i \le k$;
• $y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$;
• $y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$.

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$.

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

$$w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)$$

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$. Then:

1. For every $u \ge 0$, the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

$$N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.$$

2. $u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$.
3. The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$.
4. If $K = 0$ and $w'_k \ge 0$, the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

• LP (13) and its dual are attained with the common value $A_k$.
• The constraints of (14) are the robust counterpart of the $k$-th holding/shortage pair (10)–(11).
• For fixed orders, the value of (14) is the sum (21).
• The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$.
• The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$.
• Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$.
• Remark 1: $A_{k-1} \le A_k$, so $w'_k \ge \bar w_k$ when $p \ge h$.
• Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$, which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$, upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

• the budgeted robust counterpart of a pair of piecewise-linear constraints;
• the duality of the fractional knapsack LP (13);
• the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$. The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$-period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$, the stock at the end of period $k$. The standing assumptions of §3.1 are fields of the model:

• $c > 0$, $K \ge 0$, $h \ge 0$, $p > c$;
• $\hat w_k \ge 0$;
• $\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

The conventions and corrections are:

• Fixed cost. The paper writes it with binary variables and a big-$M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
• "Optimal". It always means minimality over all feasible points.
• The policy. It is the order sequence chosen at time 0.
• $A_k$. It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
• The robust formulation. (14) is formalized as printed: the $k$-th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$.
• Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$. The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
• Part (b). It is stated under $w'_k \ge 0$. As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$, $\bar w = \hat w = (10, 0)$, $\Gamma = (0, 1)$, $c = 1$, $h = 4$, $p = 2$, $x_0 = 0$. Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
• Remark 3. It adds $\Gamma_0 \le 1$.
• Remark 1. Its inequalities are weak.
• Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$, and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

• D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.

Motivation

A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.

Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.

Setting

There are $n\ge1$ states. State $1$ is the destination. At state $i$, a control $u\in U(i)$ incurs a real cost $c_i(u)$ and moves the process to state $j$ with probability $p_{ij}(u)$. A selector $\mu$ chooses one control $\mu(i)$ at every state. A policy $\pi=(\mu_0,\mu_1,\ldots)$ may change selectors over time; a stationary policy repeats one selector. The matrix $P(\mu)$ has entries $p_{ij}(\mu(i))$, and $c(\mu)$ is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.

The cost vector $x(\pi)$ is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost $x_i^*$ is the infimum of $x_i(\pi)$ over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is $T_\mu(x)=c(\mu)+P(\mu)x$; the Bellman operator $T$ takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).

A stationary policy is proper when its probability of reaching state $1$ tends to one from every starting state. Assumption 1 says state $1$ is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to $+\infty$. Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in $X=\{x\in\mathbb R^n:x_1=0\}$. Bertsekas and Tsitsiklis (1991), pp. 583–584.

Formalization targets

Proposition 2: Bellman's equation and value iteration

Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of $T$ in $X$. Every initial $x\in X$ has

$$\lim_{t\to\infty}T^t(x)=x^*.$$

A stationary selector $\mu$ is optimal exactly when $T_\mu(x^*)=T(x^*)$; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.

Supporting results

The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of $T$. Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.

Significance

Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.

The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.

Difficulty

When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet $T(0,x_2)=(0,\min\{1+x_2,2\})$ is not a contraction in any norm on $X$. The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.

Formalization scope

States are Fin n, with the paper's state $1$ represented by 0; the model requires $n\ge1$. A control set $U(i)$ is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes $T:\mathbb R^n\to\mathbb R^n$; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.

Policy costs and their infimum use extended reals so that an improper policy's $+\infty$ cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that $x^*$ has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; $T^0$ is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.

Selected references

• Dimitri P. Bertsekas and John N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 580–595, 1991. DOI.

Motivation

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

• 1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
• 1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
• 1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
• 1959. Dijkstra gives a label-setting method for nonnegative lengths.
• 1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$. Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$.

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$, and its time is $\sum_{r<m} t_{c_r c_{r+1}}$. The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$, and $f_N = 0$.

The routing equation (3.2) is the system

$$F_i = \min_{j \ne i}\,[t_{ij} + F_j]\quad (i = 1, \dots, N-1), \qquad F_N = 0 .$$

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$, and iterates (5.1):

$$f_i^{(k+1)} = \min_{j \ne i}\,[t_{ij} + f_j^{(k)}]\quad (i \ne N), \qquad f_N^{(k+1)} = 0 .$$

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$, attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$:

$$k \ge N-1 \;\Longrightarrow\; f^{(k)} = f = \text{the unique solution of (3.2)}.$$

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

1. (3.2): the minimal times exist and satisfy the routing equation.
2. §4: (3.2) has at most one solution.
3. (5.4): $f^{(1)} \le f^{(0)}$.
4. §5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
5. (5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$.
6. §7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$. The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$, the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most-$k$-stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$.

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$, with standing hypothesis $n \ge 1$. City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$. Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$. Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$, the destination included.

The paper's loose phrases are made explicit as follows.

• "Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
• "Represents the minimum time for a path with at most one stop" becomes, for every $k$, a minimum over routes with at most $k + 1$ roads.
• "Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$.
• "Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$, $\underline f^{(k)} = f$.
• "The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$, which would set $f_N^{(0)} = t_{NN}$, and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$, the value the paper's own justification needs. (7.1) prints "$N = 1$" for $N - 1$. Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$.

Selected references

• R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$-space is $n$-tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

• 1927: Menger states the disjoint-paths theorem for separating sets.
• 1932: Whitney proves the characterization of $n$-connected graphs by $n$ disjoint paths between every pair of points.
• 1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
• 1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$, $p_{m+1} = p_k$ and $m \ge 1$. Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$-tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$, none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$.

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$. A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$, such that for every point $x$ and every line $e$

$$\sum_{C \ni x} f(C) \le c(x), \qquad \sum_{C \ni e} f(C) \le c(e).$$

Its value is $\operatorname{val}(f) = \sum_C f(C)$. A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$. Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$.

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$, and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$. In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$:

$$G \text{ is } n\text{-tuply connected} \iff \text{for all } p_s \ne p_k,\ G \text{ has } n \text{ disjoint paths from } p_s \text{ to } p_k.$$

Both directions are part of the goal.

Milestones, in the order of the proof

1. Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$.
2. Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
3. Min-cut in the unit network (p. 434). If $G$ is $n$-tuply connected and $p_s \ne p_k$, every disconnecting set of the unit network has value at least $n$.
4. Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$.
5. Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$-tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$-connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$-connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$-space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$, which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$) together with up to $n-2$ points, and the deletion hypothesis of $n$-tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

• "dropping out $n-1$ or fewer points" is $|X| < n$;
• "$n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$, $p_s b$, and $p_s p_k$, the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$-tuply connected. The theorem therefore uses its conventional simple-path reading;
• path flows live on simple paths (merging and shortcutting changes no maximum value);
• the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$;
• "the condition is sufficient is obvious" is the full statement that $n$-tuple connectedness follows;
• the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$-connected for all $n$. Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

Motivation

An airline sells the seats of one flight leg at several fares. Cheaper fares are booked earlier, so the airline must decide, while low-fare requests arrive, how many seats to hold back for later and more valuable passengers. In nested booking control a seat that could be sold at a low fare is always available to a higher fare. The airline therefore chooses protection levels: $p_k$ seats are reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain.

For two classes the optimal protection level was found by Littlewood (1972): protect $p_1$ seats, where $f_1 \Pr[X_1 > p_1] = f_2$. For more classes the industry used the EMSRa heuristic of Belobaba (1987, 1989), which applies Littlewood's rule to each pair of classes separately and adds the results. Brumelle and McGill (1993) gave the exact optimality conditions for any number of nested classes and showed that EMSRa is in general not optimal. Their conditions are part of the standard theory of single-leg revenue management, as presented in Talluri and van Ryzin (2004).

Setting

There are fare classes $k = 1, 2, \dots$, numbered from the highest fare. Class $k$ has fare $f_k$ and random demand $X_k \ge 0$. The standing assumptions (pp. 128–129) are: the demands are mutually independent random variables on a probability space $(\Omega, \mathcal F, P)$, and the fares are strictly decreasing, $f_1 > f_2 > \cdots$. Demands arrive in order of increasing fare: all of class $k+1$ before any of class $k$. There are no cancellations or no-shows, and the decision to close a class depends only on the number of current bookings.

A protection-level policy is a vector $p = (p_1, p_2, \dots)$ with $p_k \ge 0$; the dummy $p_0 = 0$. The revenue $R_k[s; p; x]$ of the $k$ highest classes with $s$ seats available and demand vector $x$ is defined recursively by (8)–(9), p. 130:

$$R_1[s; p; x] = f_1 \min(s, x_1),$$ $$R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k, \\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1}, \\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s. \end{cases}$$

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$. A policy $p$ is optimal if $ER_k[s; q; X] \le ER_k[s; p; X]$ for every policy $q$, every $k \ge 1$ and every $s \ge 0$.

For $g : \mathbb R \to \mathbb R$, $\delta_+ g[s]$ and $\delta_- g[s]$ denote the right and left derivatives, and the subdifferential $\delta g[s]$ is the interval $[\delta_+ g[s], \delta_- g[s]]$, with $\delta_- g[0] = +\infty$ (p. 131).

Formalization targets

Goal: Theorem 3 (p. 134)

If the protection levels satisfy

$$f_1 \Pr[X_1 > p_1 \cap X_1 + X_2 > p_2 \cap \dots \cap X_1 + \dots + X_k > p_k] = f_{k+1} \quad \text{for all } k \ge 1, \tag{31}$$

then $p$ is optimal.

Milestones

1. (27), p. 132: $ER_1$ is concave, and $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$.
2. Lemma 1, p. 131: if $ER_k[\,\cdot\,; p; X]$ is concave on $s \ge 0$ and $f_{k+1} \in \delta ER_k[p_k; p; X]$, then $E\{R_{k+1}[s; p; X] \mid X_{k+1}\}$ is concave in $s$.
3. Corollary 1, p. 131: under the same conditions $ER_{k+1}[\,\cdot\,; p; X]$ is concave on $s \ge 0$.
4. Theorem 1, p. 131: if $f_{k+1} \in \delta ER_k[p_k; p; X]$ for every $k$ (condition (20)), then $p$ is optimal.
5. Lemma 2, p. 134: under (31), for $s \ge p_k$,

$$\delta_+ E\{R_{k+1}[s; p; X] \mid X_{k+1}\} = f_1 \Pr[X_1 > p_1 \cap \dots \cap X_1 + \dots + X_k > p_k \cap X_1 + \dots + X_{k+1} > s \mid X_{k+1}].$$

6. Corollary 2, p. 134: the unconditional version (37) of Lemma 2 for $\delta_+ ER_{k+1}[s; p; X]$.

Significance

Theorem 3 turns the optimal nested protection levels into a sequence of equations in the joint distribution of the cumulative demands $X_1 + \dots + X_j$. For $k = 1$ it is Littlewood's rule. For $k \ge 2$ it identifies exactly what EMSRa approximates: EMSRa replaces the joint event in (31) by separate pairwise comparisons, and the paper shows (§4) that EMSRa can both over- and underestimate the optimal protection levels. The conditions are also the input of numerical methods: given demand forecasts, the levels $p_1, p_2, \dots$ are found one after another by solving (31), and §3.3 notes that a continuous joint demand distribution guarantees a solution exists.

The results are proved in the paper. As far as is known they have no machine-checked proof. Related platform items cover the two-class, integer-seat case from Belobaba (1987) (SeatInventory.Nested.emsr_protection_level_optimal) and the integer marginal-seat-revenue analogue of (27). They use a different model: two classes, natural-number seats and first differences. This mission formalizes the multi-class statement with real-valued seats and one-sided derivatives. A sister mission of the series proves the existence of optimal integer policies for integer-valued demand (Theorem 2).

Difficulty

The expected revenue is not differentiable: for discrete demand it is piecewise linear, so first-order conditions must be stated with one-sided derivatives and subdifferentials. The natural approach, to optimize each protection level separately with the others fixed, fails without concavity, and concavity of $ER_{k+1}$ in $s$ is not automatic. It holds only when the lower protection levels already satisfy the first-order conditions. Concavity and optimality must therefore be carried through one joint induction over the classes. Passing from (31) to (20) requires computing the right derivative of the expected revenue in closed form for every $s \ge p_k$. This involves exchanging differentiation with expectation and conditioning on one class's demand at a time.

Formalization scope

• Classes are indexed by $\mathbb N$ from $1$; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$, with no bound on the number of classes. Seats and protection levels are real numbers.
• Expectation is the Bochner integral on a probability space. The standing assumptions are a single predicate: probability measure, measurable nonnegative demands, mutual independence (iIndepFun), strictly decreasing fares.
• $E\{\cdot \mid X_k\}$ evaluated at $X_k = y$ is the integral with the $k$-th demand frozen at $y$. Because the demands are independent this is a version of the conditional expectation, and "with probability 1" becomes "for every $y \ge 0$", which is stronger.
• One-sided derivatives are HasDerivWithinAt on half-lines and must exist; derivWithin, which returns $0$ where no derivative exists, is not used. $\delta_- g[0] = +\infty$ is encoded as a disjunct.
• Optimality is global: $p$ beats every policy $q$ at every level $k$ and every $s \ge 0$. The page's proof of Theorem 1 shows coordinatewise optimality of $p_k$, and the global form follows by induction on $k$.
• Fares are not assumed positive in the model: under (20) or (31) with strictly decreasing fares, $f_1 > 0$ follows. The milestone (27), stated with only the hypotheses on $X_1$ that it needs, assumes $X_1 \ge 0$ and $f_1 \ge 0$, without which $ER_1$ is not concave.
• No continuity of the demand distribution is assumed. Theorem 3 is conditional on a solution of (31).
• The page's hypothesis of Lemma 1 has the misprint "$(p_0, \dots, p_{k+1})$" for $(p_0, \dots, p_{k-1})$. The formal statement uses the latter.

The goal assumes only the standing assumptions, $p \ge 0$, and (31). It does not assume concavity, condition (20) or any derivative formula: those are milestones. A formalization that quantified optimality over one level, one value of $s$, or policies differing from $p$ in one coordinate would be weaker than the paper and is excluded.

A complete development needs one-sided derivatives of integrals of piecewise-linear functions (dominated convergence for difference quotients), concavity of piecewise functions glued at points where the slopes decrease, and the independence calculus that turns $E[E\{\cdot \mid X_{k+1}\}]$ into an iterated integral. These pieces are reusable for other newsvendor-type and revenue-management models. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

• S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1), 127–137, 1993. https://doi.org/10.1287/opre.41.1.127
• K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12, 95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
• P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.

Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret $O\big((\log\log n)(\log n)^{1/2}/n^{1/2}\big)$. The paper's lower bound for parametric families (Proposition 4) is of order $n^{-1/2}$, so the rate is optimal up to logarithmic factors.

Setting

Market. Prices lie in $[\underline p,\overline p]\cup\{p_\infty\}$ with $0<\underline p<\overline p<p_\infty$. Posting the off price $p_\infty$ stops demand. The seller starts with inventory $x>0$ and sells over the horizon $[0,T]$, $T>0$.

Demand. A demand function $\lambda$ maps a price to a demand rate. The class $\mathcal L(M,\underline K,\overline K,m)$ consists of the functions that are non-increasing with an inverse $\gamma$ on $[\underline p,\overline p]$, have a concave revenue rate $r(l)=l\gamma(l)$, are bounded by $M$, are $\overline K$-Lipschitz with a $\underline K^{-1}$-Lipschitz inverse, and attain a revenue rate $\max_p p\lambda(p)\ge m$. The parametric family is $\lambda(p;\theta)$, $\theta\in\Theta=[\theta_{\mathrm{lo}},\theta_{\mathrm{hi}}]$, with every member in the class (Assumption 1). Assumption 2 adds a test price $p_1$, differentiability of $\sqrt{\lambda(p_1;\cdot)}$ and the Lipschitz bound $|\lambda(p;\theta)-\lambda(p;\theta')|\le\overline K_2|\theta-\theta'|$. Assumption 3 requires $\inf_{p,\theta}\lambda(p;\theta)>l_0>0$ and an $\alpha$-Lipschitz solution map $d\mapsto g(p,d)$ of the equation $\lambda(p;\cdot)=d$.

Demand process. Let $N$ be a unit-rate Poisson process. Under a price path $p(\cdot)$ and parameter $\theta^*$, the cumulative demand up to time $t$ is $N\big(\int_0^t\lambda(p(s);\theta^*)\,ds\big)$. Sales stop when the inventory runs out.

Benchmark and regret. The deterministic relaxation $J^D(x,T\mid\theta)$ is the supremum of $\int_0^T p(s)\lambda(p(s);\theta)\,ds$ over price paths with $\int_0^T\lambda(p(s);\theta)\,ds\le x$. In the market of size $n$ the inventory is $nx$ and the demand $n\lambda$. If $J^\pi_n(x,T;\theta)$ is the expected revenue of a policy $\pi$, its regret is $\mathcal R^\pi_n=1-J^\pi_n/J^D_n$.

Algorithm 3. Start from $\hat p_1=p_1$ and use stages of lengths $\Delta^{(1)}_n,\dots,\Delta^{(\ell_n)}_n$ summing to $T$. Stage $i$ applies $\hat p_i$, estimates the demand rate $\hat d_i$ from the stage's demand, solves for $\hat\theta_i=g(\hat p_i,\hat d_i)$, and sets $\hat p_{i+1}=\max\{p^u(\hat\theta_i),p^c(\hat\theta_i)\}$. Here $p^u(\theta)$ maximizes $p\lambda(p;\theta)$ and $p^c(\theta)$ minimizes $|\lambda(p;\theta)-x/T|$. The tuning (19)–(20) is $\ell_n=(\log2)^{-1}\log\log n$ stages with $\Delta^{(m)}_n=\beta_n n^{(a_{\ell_n}/a_m)-1}$ and $a_m=2^{m-1}/(2^m-1)$.

Formalization targets

Goal: Proposition 5

$$\exists\,C>0,\ \exists\,n_0,\quad \forall n\ge n_0,\ \forall\theta\in\Theta:\qquad \mathcal R^{\pi_n}_n(x,T;\theta)\le C\,\frac{(\log\log n)(\log n)^{1/2}}{n^{1/2}} .$$

The constants are uniform in $\theta$ and $n$. This is the paper's (21): $\sup_\theta\mathcal R^{\pi}_n=O(\cdot)$.

Milestones, in proof order

1. Fact 1: $J^D_n=nJ^D$ and $J^D\ge m\min\{T,x/M\}$ on the class.
2. Lemma 1: the deterministic relaxation is solved by the fixed price $p^D=\max\{p^u,p^c\}$.
3. Lemma 2: Poisson deviation bounds at scale $(\log n/r_n)^{1/2}$.
4. (A-27): a revenue lower bound that splits the loss into stage-wise terms and an overflow term.
5. The per-stage revenue gap $r(p^D)-\mathbb E\,r(\hat p_i)\le C_2(n\Delta^{(i-1)}_n)^{-1/2}$.
6. (A-30): the stage-$i$ demand rate rarely exceeds the run-out rate.
7. The overflow bound $\mathbb E[(Y_n-nx)^+]\le nC_8(\log n)^{1/2}n^{a_{\ell_n}-1}$.
8. (A-31): the revenue ratio before the exponents are evaluated.
9. The rate estimate $n^{a_{\ell_n}-1}\le e\,n^{-1/2}$.

Milestones 6–8 hold in the case $\lambda(\overline p;\theta^*)\le x/T$, the only case the paper's proof treats in detail.

Significance

Proposition 5 shows that with one unknown parameter, learning while earning reaches the $n^{-1/2}$ rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only $n^{-1/4}$ and $n^{-1/3}$. The paper leaves open whether the multi-parameter case attains the lower bound.

The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.

The result is proved in the paper, but parts of the proof are only sketched. The case $\lambda(\overline p;\theta^*)>x/T$ is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.

Difficulty

The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries $\Lambda_i=\sum_{j\le i}n\lambda(\hat p_j;\theta^*)\Delta^{(j)}_n$ depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses $\Delta^{(i)}_n/(n\Delta^{(i-1)}_n)^{1/2}$ are all of the same order. That balance has to be checked exactly, including the rounding of $\ell_n$ to an integer.

Formalization scope

• Poisson process. A structure on an arbitrary probability space: $N(0)=0$, monotone right-continuous paths, measurable marginals, Poisson increments, and independent increments over finite partitions. No process is published on the platform.
• Class and family. Conditions on $\lambda$ are imposed on $[\underline p,\overline p]\cup\{p_\infty\}$, the only prices a path uses. The inverse $\gamma$ is Function.invFunOn. $\Theta$ is a nonempty closed interval of $\mathbb R$.
• Assumption 3. As printed it cannot hold for $d>\sup_\theta\lambda(p;\theta)$. It is read as an $\alpha$-Lipschitz map $g(p,\cdot):[0,\infty)\to\Theta$ that inverts $\lambda(p;\cdot)$ on $\Theta$. $g$ is jointly measurable, so that estimates at random prices are random variables.
• Selections. $p^u,p^c$ are any measurable selections of the maximizer and minimizer; the statements hold for each.
• Inventory. The inventory is $\lfloor nx\rfloor$ units, and sales are capped cumulative counts.
• Time change. Eq. (1) is applied stage by stage with random stage boundaries.
• Typos. In Algorithm 3, "$\lambda(p_i,\theta)$" is read as $\lambda(\hat p_i;\theta)$ and "$x/t$" as $x/T$.
• Stages. $\ell_n=\lceil\log_2\log n\rceil$.
• Integrals. Expectations are lower Lebesgue integrals of nonnegative quantities, converted to reals. The relaxation is a real supremum over measurable paths.
• Asymptotics. The $O(\cdot)$ is rendered with an explicit $n_0$. The clause "asymptotically optimal" is omitted, since it needs the second half of Lemma 1.
• Ruled out. Each of the following would trivialize the statement: removing the inventory cap, replacing the random stage boundaries by deterministic ones, fixing $\theta$, letting $C$ depend on $\theta$, or using a non-measurable selection (whose expectation would be a junk value).

Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• 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
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000