Operations Research

Motivation

Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number $p_k$ of seats is 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. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with $f_{k+1}$ in the subdifferential of the expected revenue of the $k$ highest classes at $p_k$, for every $k$, is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.

Timeline.

• Littlewood (1972): two fare classes, rule $f_2 = f_1 \Pr[X_1 > p_1]$.
• Belobaba (1987, 1989): EMSR heuristic for many classes.
• Curry (1990) and Wollmer (1992): multiple nested classes, continuous and discrete demand respectively.
• Brumelle and McGill (1993): subdifferential optimality conditions for any number of classes (Theorem 1), existence of an optimal integer policy for integer demand (Theorem 2), and the probability conditions (31) (Theorem 3).

Setting

Classes are numbered $k = 1, 2, \dots$, class $1$ paying the highest fare. Class $k$ has a random demand $X_k \ge 0$ and fare $f_k$, with $f_1 > f_2 > \cdots$. The demands are mutually independent on a probability space $(\Omega, \mathcal F, P)$. A protection-level policy is a sequence $p = (p_1, p_2, \dots)$ with $p_k \ge 0$; the dummy level $p_0 = 0$ is never used.

For a demand vector $x$ and $s$ available seats, the revenue of the $k$ highest classes is defined recursively (Eqs. (8)–(9), p. 130):

$$R_1[s; p; x] = \begin{cases} f_1 s & 0 \le s < x_1,\\ f_1 x_1 & x_1 \le s,\end{cases}$$ $$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 is optimal if it maximizes $ER_k[s; \cdot\,; X]$ for every $k$ and every $s \ge 0$ (p. 130).

For a function $g$ and $t \ge 0$, $\delta_+ g(t)$ and $\delta_- g(t)$ are the right and left derivatives, with $\delta_- g(0) = +\infty$, and the subdifferential is $\delta g(t) = [\delta_+ g(t), \delta_- g(t)]$ (p. 131). Condition (20) is

$$f_{k+1} \in \delta ER_k[p_k; (p_0, \dots, p_{k-1}); X], \qquad k = 1, 2, \dots$$

A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on $s \ge 0$ and linear on each interval $[m, m+1]$, $m = 0, 1, 2, \dots$

Formalization targets

Goal: Theorem 2 (p. 132)

If every $X_k$ is integer valued and the fares are positive, there is a policy $p^*$ with $p^*_k \in \{0, 1, 2, \dots\}$ such that

$$ER_k[s; q; X] \le ER_k[s; p^*; X] \qquad \text{for every policy } q,\ k \ge 1,\ s \ge 0,$$

and $p^*$ satisfies (20). The competitor $q$ ranges over all real protection levels.

Milestones (in proof order)

1. (27): $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$, and $ER_1$ is CLBI.
2. Covering property (p. 132): if $g$ is CLBI and $\delta_+ g(s_2) < c < \delta_- g(s_1)$ with $s_1 < s_2$, then $c \in \delta g(n)$ for an integer $n \in [s_1, s_2]$.
3. (28)–(29): for $s \ge p_k$,

$$\delta_+ ER_{k+1}[s] = f_{k+1}\Pr[X_{k+1} > s - p_k] + \sum_{i=0}^{\lfloor s - p_k\rfloor} \delta_+ ER_k[s - i]\Pr[X_{k+1} = i],$$

and the analogous formula for $\delta_-$ at $s > p_k$. 4. Corollary 1 (p. 131): concavity of $ER_k$ and $f_{k+1} \in \delta ER_k[p_k]$ give concavity of $ER_{k+1}$. 5. CLBI propagation (p. 133): if $ER_k[\cdot; p^*; X]$ is CLBI and integer $p^*_1, \dots, p^*_k$ satisfy (20), then $ER_{k+1}[\cdot; p^*; X]$ is CLBI. 6. (30): for $s$ large enough, $\delta_+ ER_{k+1}[s; p; X] < f_{k+2}$. 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.

Significance

The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.

Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of $s$ on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.

Difficulty

Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level $k$ satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of $ER_{k+1}$ are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer $s$, is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy $p^*$ is an infinite sequence built by recursion.

Formalization scope

• Model. Classes are indexed by $\mathbb N$ from $1$; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$. Seats, demands and protection levels are real; an integer policy is a sequence of natural numbers read as reals. Integer-valued demand means each $X_k(\omega)$ is a natural number. Expectations are Bochner integrals.
• Standing assumptions (§1). $P$ is a probability measure. The demands are measurable, nonnegative and mutually independent, and the fares are strictly decreasing.
• Added hypotheses. The goal assumes positive fares, $f_k > 0$ for $k \ge 1$. The page leaves this implicit (fares are average revenues), and without it the theorem is false. The same assumption appears in (30), and (27) assumes $f_1 \ge 0$, without which $ER_1$ is convex rather than concave.
• Derivatives. One-sided derivatives are required to exist, with their value asserted; no default value of an undefined derivative is used. The convention $\delta_- g(0) = +\infty$ is built into the subdifferential.
• Optimality. Optimality is global: against every real protection-level policy, at every level $k \ge 1$ and every $s \ge 0$.
• Paper's slips corrected. (28)–(29) are stated on their range $s \ge p_k$ (resp. $s > p_k$). (30) is stated for every $k \ge 1$, as the induction uses it, rather than the printed $k = 2, 3, \dots$
• Not a trivialization. The goal assumes only the model, integer demand and positive fares. It does not assume concavity, CLBI, (20) or any derivative formula, and optimality is not restricted to integer competitors or to one $k$.
• Duplication. Corollary 1 and Theorem 1 are restated from the companion mission in this series.
• Contributions. Proofs of the measure-theoretic derivative lemmas, of the covering property (a statement about real functions), and of the induction are all 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
• R. E. Curry, Optimal Airline Seat Allocation with Fare Classes Nested by Origins and Destinations, Transportation Science 24(3):193–203, 1990. https://doi.org/10.1287/trsc.24.3.193
• R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1):26–37, 1992. https://doi.org/10.1287/opre.40.1.26

Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the $k = 1$ case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$. In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$, and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

• 1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
• 1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
• 1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$, so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$. A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$. The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$.

For a set $\mathcal S$ of finite positive volume, its center of gravity is

$$c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .$$

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$, computes $c_t=c(\mathcal S_t)$, queries the first order oracle at $c_t$ to obtain a subgradient $w_t$, and sets

$$\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.$$

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$, found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

For every run of the method and every $t\ge1$,

$$f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.$$

Milestones (proof of Theorem 2.1, pp. 246–247)

1. Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$, then for every $w\ne0$,

$$\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).$$

2. (2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$, hence $x^*\in\mathcal S_t$ for every $t$.
3. Volume decay. If $w_s\ne0$ for $s\le t$, then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$.
4. Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$, $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$.
5. Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$.

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$, $O(n\log(2B/\varepsilon))$, depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ($O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$, so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$, continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$.

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$, which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$, which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
• B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
• A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
• D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Motivation

Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.

When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.

Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.

Setting

The state space is $S=\{0,1,2,\dots\}$. For each state $i$ the set $U(i)$ of admissible actions is a nonempty compact subset of a metric space $A$. Choosing $a\in U(i)$ in state $i$ costs $c(i,a)\ge0$, and the next state is $j$ with probability $P(j\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$.

An admissible policy $\pi\in\Pi$ chooses the action at time $t$ according to a probability distribution $\pi_t(\cdot\mid h_t)$ concentrated on $U(x_t)$, where $h_t=(x_0,a_0,\dots,x_t)$ is the history; it may use the whole history and may randomize. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$, applied at every step. Given an initial state $i$ and a policy $\pi$, the states and actions $(X_t,A_t)$ form a stochastic process with law $P^\pi_i$ and expectation $E^\pi_i$.

For $\beta\in(0,1)$, the discounted cost and the average cost of $\pi$ from $i$ are

$$J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N\,E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),$$

both in $[0,\infty]$. The optimal values are $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ and $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$, and the differential discounted value is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$. A policy $f\in\Pi_{SD}$ is AC-optimal if $J(i,f)=J^*(i)$ for every $i$.

Sennott's conditions (Assumptions 5.14–5.16) are:

1. $J^*_\beta(i)<\infty$ for all $i\in S$ and $\beta\in(0,1)$;
2. there is a nonnegative integer $L$ with $h_\beta(i)\ge-L$ for all $i$ and $\beta$;
3. there is $M:S\to\mathbb R_+$ with $h_\beta(i)\le M(i)$ for all $i$ and $\beta$, and for each $i$ some $a(i)\in U(i)$ with $\sum_jP(j\mid i,a(i))M(j)<\infty$.

Formalization targets

Goal: Theorem 5.9

$$\text{Under Assumptions 5.14–5.16, there is } f\in\Pi_{SD}\text{ with } J(i,f)=\inf_{\pi\in\Pi}J(i,\pi)\ \text{ for every } i\in S.$$

The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.

Milestones

1. Theorem 2.1 (i), (iii), countable form: the discounted cost optimality equation $J^*_\beta(i)=\inf_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)J^*_\beta(j)\}$ and a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$.
2. Display (5.15): $(1-\beta)J^*_\beta(0)+h_\beta(i)=c(i,f_\beta(i))+\beta\sum_jP(j\mid i,f_\beta(i))h_\beta(j)$.
3. The limit objects: along a subsequence $\beta_n\to1$, $f_{\beta_n}\to f$, $h_{\beta_n}\to h\ge-L$ pointwise, and $(1-\beta_n)J^*_{\beta_n}(i)\to\rho^*$, a constant.
4. The average cost optimality inequality (ACOI) $\rho^*+h(i)\ge c(i,f(i))+\sum_jP(j\mid i,f(i))h(j)$.
5. An ACOI along $f$ with $h$ bounded below gives $J(i,f)\le\rho$.
6. Theorem A.2: the Abelian inequalities between Cesàro and Abel means (already on the platform).
7. $J(i,\pi)\ge\rho^*$ for every $\pi\in\Pi$.

Significance

The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.

Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.

Difficulty

The obvious argument lets $\beta\to1$ in the discounted optimality equation (5.6). Two steps fail without more structure. First, $h_\beta$ need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum $\sum_jP(j\mid i,a)h_\beta(j)$ by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of $\Pi$, which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.

Formalization scope

The Lean development uses the following representation and conventions.

• States, actions, model. The state space is ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and $c(i,\cdot)$, $P(j\mid i,\cdot)$ are continuous on $U(i)$.
• Policies. $\Pi$ consists of all history-dependent randomized policies, with admissibility required almost surely. $J^*$ and $J^*_\beta$ are infima over all of $\Pi$, never over stationary policies only. Restricting the infimum to $\Pi_{SD}$ would drop the Tauberian half of the theorem and is not the paper's statement.
• Costs. Costs are lower Lebesgue integrals in $[0,\infty]$ against the Ionescu-Tulcea path measure, and the average cost is a limsup in $[0,\infty]$.
• Explicit hypotheses. $h_\beta$ is a difference of real parts and is used only under Assumption 5.14, so it is never read off an infinite $J^*_\beta$. The quantifiers over $i$ and $\beta$ in Assumption 5.15, implicit on the page, are universal, and $L$ is a natural number as printed. Every series $\sum_jP(j\mid i,a)h(j)$ carries a summability hypothesis or conclusion.
• Corrected claim. Remark 5.8(a) as printed claims that any scalar $\rho$ satisfying the ACOI with $h$ bounded below is the optimal average cost. That is false ($h\equiv0$, $\rho=\sup c$), so only the inequality $J(i,f)\le\rho$, which the proof uses, is stated.
• Sequences. The milestones about limits are stated for any sequence $\beta_n\in(0,1)$ with $\beta_n\to1$, not only increasing ones.

A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.

Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact $U(i)$; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37(4) (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
• L. I. Sennott, A new condition for the existence of optimal stationary policies in average cost Markov decision processes, Oper. Res. Lett. 5 (1986) 17–23 (reference [155] of the survey; no stable link checked).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150] of the survey).
• A. Federgruen, A. Hordijk, H. C. Tijms, Denumerable state semi-Markov decision processes with unbounded costs, average cost criterion, Stochastic Process. Appl. 9 (1979) 223–235 (reference [53] of the survey).
• R. Sznajder, J. A. Filar, Some comments on a theorem of Hardy and Littlewood, J. Optim. Theory Appl. 75 (1992) (reference [176] of the survey, cited for Theorem A.2).

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function $\lambda(p)$, the rate of purchase requests at price $p$, is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing $\lambda$. They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

• the problem is constrained by an initial inventory;
• the set of prices is a continuum;
• the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order $(\log n)^{1/2}n^{-1/4}$ in a market of size $n$.

Setting

Prices. Fix $0<\underline p<\overline p<\infty$ and an off price $p_\infty>0$ outside $[\underline p,\overline p]$. The seller may charge any price in $[\underline p,\overline p]\cup\{p_\infty\}$; charging $p_\infty$ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time $t$ is $\lambda(p(t))$. Let $N$ be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time $t$ under a price path $p(\cdot)$ are $N\big(\int_0^t\lambda(p(s))\,ds\big)$. The seller starts with inventory $x$ and sells until either the horizon $T$ ends or the stock runs out. The expected revenue of a policy $\pi$ is $J^\pi(x,T;\lambda)$.

Demand class. $\mathcal L=\mathcal L(M,\underline K,\overline K,m)$ is the set of regular demand functions satisfying Assumption 1. Regular means:

• $\lambda\ge0$ and $\lambda(p_\infty)=0$;
• $\lambda$ is non-increasing on $[\underline p,\overline p]$, with inverse $\gamma$;
• the revenue rate $r(l)=l\gamma(l)$ is concave.

Assumption 1 requires:

• (i) $\lambda\le M$ on $[\underline p,\overline p]$;
• (ii) $\lambda$ is $\overline K$-Lipschitz and $\gamma$ is $\underline K^{-1}$-Lipschitz;
• (iii) $\max_p p\lambda(p)\ge m$.

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

$$J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.$$

The regret of a policy is $\mathcal R^\pi=1-J^\pi/J^D$.

Scaling. In a market of size $n$ the inventory is $nx$ and the demand function is $n\lambda$, as in (11). The corresponding quantities are $J^\pi_n$, $J^D_n=nJ^D$ and $\mathcal R^\pi_n$.

Algorithm 1, $\pi(\tau,\kappa)$. The policy has three phases.

1. Learning. On $[0,\tau]$ it tests $\kappa$ equally spaced prices $p_i=\underline p+(i-1)(\overline p-\underline p)/\kappa$, each for $\Delta=\tau/\kappa$ time units. It estimates $\lambda(p_i)$ by the normalized request counts $\hat\lambda(p_i)$.
2. Optimization. It chooses $\hat p^u=\arg\max_i p_i\hat\lambda(p_i)$ and $\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|$, and sets $\hat p=\max\{\hat p^u,\hat p^c\}$.
3. Pricing. It charges $\hat p$ on $(\tau,T]$ until the stock runs out.

Formalization targets

Goal: Proposition 1

Let $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$, and let $\pi_n=\pi(\tau_n,\kappa_n)$. Then there is a finite constant $C$, independent of $\lambda$ and $n$, such that

$$\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).$$

The constant is left unspecified, as in the paper. Its dependence on the class parameters, $x$ and $T$ is "somewhat complex" (p. 12), and the order $(\log n)^{1/2}n^{-1/4}$ is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

• the scaling $J^D_n=nJ^D$ (p. 12);
• Fact 1, $J^D\ge m\min\{T,x/M\}$ on $\mathcal L$;
• Lemma 1, the solution of (5): charge $p^D=\max\{p^u,p^c\}$ until the stock runs out;
• Lemma 2, a Poisson deviation bound;
• the revenue lower bound (A-2);
• Lemma 3, the learned price is near $p^D$ with high probability;
• Lemma 4 and the Case 1 bound (A-11), for $\lambda(\overline p)\le x/T$;
• Lemma 5 and the Case 2 bound (A-15), for $\lambda(\overline p)>x/T$;
• the Step 4 bound $\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)$, where $u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}$.

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order $n^{-1/2}$ for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

• a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
• the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
• uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that $\hat p$ is close to the optimal price. It breaks in two places.

First, $p^D$ is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at $\hat p$ is not controlled by the error in $\hat p$ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on $\gamma$.

Second, when demand at the highest price exceeds the inventory rate ($\lambda(\overline p)>x/T$), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

• Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space $(\Omega,\mathbb P)$, a published platform definition: ℕ-valued, $N(0)=0$, monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating $N$ at cumulative intensities.
• Inventory. The inventory of the market of size $n$ is $\lfloor nx\rfloor$ units, and sales are $\min\{N(\cdot),\lfloor nx\rfloor\}$. The cap is never dropped.
• Revenue. $J^\pi_n$ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
• Demand functions. A demand function is a map $\mathbb R\to\mathbb R$, nonnegative, with $\lambda(p_\infty)=0$. Regularity and Assumption 1 are imposed on $[\underline p,\overline p]$, and the inverse $\gamma$ is Function.invFunOn.
• Benchmark. $J^D$ is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
• Algorithm. The grid excludes $\overline p$, as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare $\hat\lambda(p_i)$ with $x/T$.
• Tuning. $\tau_n\asymp n^{-1/4}$ and $\kappa_n\asymp n^{1/4}$ are encoded with explicit constants $0<c\le c'$, with $\tau_n\in(0,T]$ and $\kappa_n\ge1$. Constants may depend on $c,c'$, the class parameters, the prices, $x$ and $T$, but never on $\lambda$ or $n$.
• Range of $n$. Bounds whose right side vanishes at $n=1$ because $\log1=0$ are stated for $n\ge2$: the goal and (A-15).
• Typo correction. Lemma 5's event uses $nx-C_9nu_n$, as in its proof, not the printed $nx-C_9u_n$.
• Ruled out. A specific demand curve, a fixed $n$, deterministic demand, a finite price set, a known $\lambda$, constants depending on $\lambda$, or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
• Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 ($J^\pi\le J^D$ for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

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

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).