Optimization

Motivation

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

Timeline:

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

Setting

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones, in the order the proof uses them

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$, a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$-self-concordant ($\kappa\ge0$) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

$$\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},$$

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$-th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$. Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

$$\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},$$

and its logarithmic barrier (35) is

$$\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y$$

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$, with $h_1$ along $s$ and $h_2$ along $y$, and $h\in\mathbb R^3$ for $\varphi_B$.

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$,

$$|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}$$

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$-self-concordant on $F_f$.

Milestones (the displayed steps of the proof)

1. Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$.
2. The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$.
3. Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$:

$$\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.$$

4. Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$, then $\varphi_B$ is $(1+\beta/3)$-self-concordant on $F_f$.

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$. A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$.

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$, which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$, together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$. The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$, fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$. A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$. Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$, but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

• "$f:\mathbb R^+\to\mathbb R$" is read as $f$ convex on the open half-line $(0,\infty)$; the Burg case $f=-\log$ is undefined at $0$, and $f$ is only evaluated at $s/y$ with $s,y>0$.
• $f$ is assumed $C^3$ on $(0,\infty)$. The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$.
• The printed third-differential display ends in $s^3h_x^3/y^5$; the correct term is $s^3h_2^3/y^5$, and the Lean statement uses it. The milestone text keeps the printed version.
• Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$", which is false for $\beta<0$: with $f\equiv0$, (36) holds for every $\beta$ and $\beta=-3$ would give a $0$-self-concordant $-\ln z-\ln s-\ln y$. The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$, the domain is exactly $F_f$ (not a subset such as $\emptyset$), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
• Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$, finite on $(0,\infty)$, and satisfies $\phi(1)=0$; the value $\phi(0)$ may be $+\infty$. Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

$$I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),$$

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$, a function with values in $\mathbb R\cup\{+\infty\}$.

Fix $a\in\mathbb R^n$, $B\in\mathbb R^{n\times m}$ with columns $b_i$, $\beta\in\mathbb R$, $C\in\mathbb R^{k\times m}$ with columns $c_i$, $d\in\mathbb R^k$, a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$. The uncertainty region is

$$U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},$$

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$. A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

$$(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}$$

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$. Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

$$a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}$$

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$. The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$:

1. Closing identity. For $\lambda\ge0$, $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$, with the convention above at $\lambda=0$.
2. Eq. (15). For $q>0$ and $\lambda\ge0$,

$$g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).$$

3. Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$, $\eta\ge0$. This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$, where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$. The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$, and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$, the conjugate may be $+\infty$, and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

• Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
• $\phi$ is ℝ → EReal, never $-\infty$, finite on $(0,\infty)$, with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
• $I_\phi(p,q)$, $\phi^*$, $(\lambda\phi)^*$, $L$, $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$. The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$, and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
• The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$.
• $m$ and $k$ may be $0$.

Corrected slip. The paper's standing assumption is $q\ge0$. The third equality of (15) substitutes $p_i=q_it$, which needs $q_i>0$, and Theorem 1 is false for $q\ge0$: with $m=k=2$, $n=1$, $\phi(t)=|t-1|$, $q=(1,0)$, both columns of $C$ equal to $(1,-1)^\top$, $d=(1,-1)$, $a=0$, $B=(0\ \ 1)$, $x=1$, $\rho=1$, $\beta=0$, the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$, $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$. The hypothesis $q\in U$ (the paper's "such that $q\in U$") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the optimization problem is difficult; the planar restriction gives a concrete geometric promise under which approximation is possible. Williamson and Shmoys state a polynomial-time approximation scheme for planar maximum independent set as Theorem 10.11 of The Design of Approximation Algorithms, in the author electronic manuscript at PDF/manuscript page 271.

Setting

The instance has vertices labeled by Fin n, an adjacency table edge : Fin n → Fin n → Bool, and a real weight weight i for each vertex. SimpleGraph.fromRel turns the table into an undirected simple graph G. The theorem requires every weight to be nonnegative. A finite set S is feasible when G.IsIndepSet (S : Set (Fin n)) holds. Its value is ∑ i ∈ S, weight i.

Planarity is expressed by HasPlanarDrawing G: vertices are placed at distinct points of the real plane, and every edge is represented by a continuous simple arc. An arc has no vertex in its interior, and distinct edges can meet only at endpoints. This is a concrete local drawing convention for the planar graph promise. The drawing witnesses the hypothesis; it is not passed as part of the algorithm's input.

The computational model is a fixed finite unit-cost RAM program. Its input includes the vertex count, an integer accuracy parameter, a complete adjacency table, and the real weights in named memory cells. Its instructions include natural-number and real addition and subtraction, exact comparisons, random-access loads and stores, branches, jumps, and halt. The machine starts with the instance preloaded and produces a bitmap after the adjacency table. This precise instruction set is a formalization convention: the book states an arithmetic-operation running time but does not specify a machine language.

Formalization targets

For every real $\varepsilon>0$, let $k=\max(1,\lceil1/\varepsilon\rceil)$. The goal asserts that a single finite program and fixed positive natural constants $C,d$ work for every planar instance and every vector of nonnegative real weights. The program must halt after a number $t$ of operations satisfying

$$t+1\le C\,2^{dk}(n+1)^2.$$

Its bitmap must represent an independent set $A$, and for every independent set $S$,

$$(1-\varepsilon)\sum_{i\in S}w_i\le\sum_{i\in A}w_i.$$

Comparison with every feasible $S$ includes an optimal solution. The same program and constants precede all accuracy and instance quantifiers. The $(n+1)^2$ form includes the empty graph without imposing zero running time. The result corresponds to the $O(2^{O(1/\varepsilon)}n^2)$ bound in Theorem 10.11; the formal statement makes the constants and accuracy parameter explicit.

Significance

The result supplies an accuracy-time tradeoff for planar weighted independent set: any fixed positive accuracy has a quadratic dependence on graph size in this operation model, while the accuracy dependence is exponential. It separates the planar setting from the general graph problem. The finite instruction set and input layout make the computational claim inspectable, including what information the program receives and what counts as an operation.

The cited result is known in the textbook. This mission asks for a Lean proof of the packaged statement; the theorem currently has sorry, and no machine construction or correctness proof is claimed. The original local statement was compiled and source reviewed before packaging. That prior result establishes statement validity in its source workspace, while the upload payload is checked separately.

Difficulty

A high-quality independent set in each planar region does not immediately give a high-quality global set: edges across regions can create conflicts, and discarding boundary vertices can lose weight. A proof must coordinate the approximation inequality with a uniform operation bound for one program across all graph sizes, accuracies, and real weight vectors. It must also show the computed bitmap is always independent and that execution reaches an explicit halt instruction within the bound. These requirements rule out treating an optimizer, an embedding, or a best solution as preloaded input.

Formalization scope

The goal uses finite labeled graphs, nonnegative arbitrary real weights, exact real arithmetic, and the concrete drawing predicate above. It does not claim a bit-complexity bound for encoded reals. The RAM starts from a complete adjacency table and weight vector, with no supplied drawing or optimum. Its step function is deterministic; an invalid program counter is stuck, so the theorem explicitly requires a halt instruction. Outputs are bits in designated natural memory cells and are checked for validity before their weighted value is compared.

The packaged definitions are the drawing predicate, instruction type, state, transition, iteration, input layout, and output decoder. They contain no proof axioms or optimization oracle. The rational-input polynomial bit-time fragment in the source workspace is a separate statement and is outside this goal. A complete contribution would construct the finite program and prove its running time and approximation guarantee in the specified model.

Selected references

• David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Theorem 10.11, PDF/manuscript p. 271; weighted independent-set setting p. 269 and context pp. 270–272. DOI.

Motivation

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

• The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
• W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
• zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
• The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
• Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
• Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

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

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