Operations Research

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage recourse $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. The fully-adaptable problem, in which $y$ may be an arbitrary function of $b$, is intractable in general. The standard tractable restriction, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), requires $y$ to be an affine policy $y(b)=Pb+q$; it turns the problem into a single convex program and is used throughout robust inventory, network design and energy planning.

How much is lost by this restriction? Bertsimas and Goyal (Math. Program. 2012) answer the question for problems with a nonnegative constraint matrix. On one side, affine policies are optimal when $\mathcal U$ is a simplex, and are within a factor $O(\sqrt m)$ of the optimum on every instance of the class, where $m$ is the number of constraints. On the other side, the bound is nearly tight: Section 4 of the paper constructs an instance on which the best affine policy costs $\Omega(m^{1/2-\delta})$ times the fully-adaptable optimum, for any $\delta>0$. This mission formalizes that lower bound.

Timeline: Ben-Tal et al. (2004) propose affinely adjustable robust counterparts; Bertsimas, Iancu and Parrilo (2010) prove optimality of affine policies for one-dimensional multistage problems; Bertsimas and Goyal (2012) give the $O(\sqrt m)$ upper bound and the matching lower-bound example formalized here.

Setting

The two-stage problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ has data $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$ and $\mathcal U\subseteq\mathbb R^m_+$:

$$z_{\mathrm{Adapt}}(\mathcal U)=\min_{x,\,y(\cdot)}\ c^\top x+\max_{b\in\mathcal U}d^\top y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ x\ge0,\ y(b)\ge0\ \ \forall b\in\mathcal U .$$

The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum over policies of the form $y(b)=Pb+q$; such a policy must be nonnegative on all of $\mathcal U$.

The large-gap instance $\mathcal I$ of display (19) has $n_1=n_2=m$, a parameter $\delta>0$ with $m^\delta>200$ (condition (18)), and

$$\theta_0=\frac{1}{m^{(1-\delta)/2}},\qquad r=\lceil m^{1-\delta}\rceil,$$ $$c=0,\quad d=e=(1,\dots,1)^\top,\quad A=0,\quad B_{ij}=\begin{cases}1,&i=j,\\ \theta_0,&i\ne j,\end{cases}$$ $$\mathcal U=\operatorname{conv}\Bigl(\{0,\ e_1,\dots,e_m,\ \tfrac{1}{\sqrt m}e\}\cup\{\theta_0\mathbf 1_S:\ |S|=r\}\Bigr),$$

where $e_j$ are the unit vectors and $\mathbf 1_S$ is the indicator vector of a set $S$ of coordinates. A permutation $\sigma$ of the coordinates acts on vectors by $b^\sigma=(b_{\sigma(1)},\dots,b_{\sigma(m)})$ and on matrices by $P^\sigma_{ij}=P_{\sigma(i),\sigma(j)}$.

Formalization targets

Goal: Theorem 3, explicit form

$$z_{\mathrm{Aff}}(\mathcal U)>\frac{m^{1/2-\delta}}{4}\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for all }\delta>0\text{ and }m\text{ with }m^\delta>200 .$$

The paper writes $z_{\mathrm{Aff}}(\mathcal U)=\Omega(m^{1/2-\delta})\cdot z_{\mathrm{Adapt}}(\mathcal U)$; the constant $1/4$ is the one the proof establishes, so the explicit statement is the stronger one.

Milestones

1. Lemma 4: $z_{\mathrm{Adapt}}(\mathcal U)\le1$, with a feasible solution attaining cost at most $1$.
2. Lemma 5: $\mathcal U$ is permutation-invariant under every $\sigma\in S^m$.
3. Lemma 6: the permuted instance $\mathcal I(\sigma)$ of (22) equals $\mathcal I$.
4. Lemma 7: if $y(b)=Pb+q$ is an optimal affine solution, so is $y^\sigma(b)=P^\sigma b+q^\sigma$.
5. Lemma 8: some optimal affine solution has $\hat P_{ij}=\mu$ ($i\ne j$), $\hat P_{jj}=\theta$, $\hat q_j=\lambda$.
6. The three Claims of the proof of Theorem 3: for a symmetric feasible affine policy with worst-case cost at most $m^{1/2-\delta}/4$, one has $0\le\lambda\le m^{-1/2-\delta}$, $\theta\ge1/3$, and $-m^{-1-\delta/2}\le\mu<0$.

Significance

The result shows that the $O(\sqrt m)$ approximation guarantee for affine policies on problems with $A\ge0$ (Theorem 4 of the same paper) cannot be improved beyond a factor $m^{\delta}$, so the uncertainty set that looks like a portion of the unit sphere in the nonnegative orthant is essentially the worst case for affine recourse. It also explains why later work moved to piecewise-affine and finitely adaptable policies to close the gap. The example satisfies $c,d\ge0$, $A,B\ge0$ and $\mathcal U\subseteq\mathbb R^m_+$, so the lower bound applies to every larger problem class.

The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization adds checked statements of the symmetrization argument (an optimal affine policy may be taken invariant under the symmetry group of the instance), which applies to any symmetric robust linear program, and a checked derivation of the explicit constant.

Difficulty

The upper bound $z_{\mathrm{Adapt}}\le1$ is a direct construction. The difficulty lies in the lower bound on $z_{\mathrm{Aff}}$, which must hold for every affine policy, a family with $m^2+m$ free parameters. Bounding the cost of a policy at a few chosen points of $\mathcal U$ does not suffice without first reducing the parameters, and the reduction requires that an optimal affine solution exists (attainment of the minimum over an unbounded parameter set) and that averaging over the symmetric group preserves both feasibility and optimality. The remaining argument balances three different generators of $\mathcal U$ against each other, and the exponents of $m$ must be tracked exactly through ceilings and real powers.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order and 0-based indices; matrices are Matrix (Fin m) (Fin m) ℝ. The values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are infima of the sets of worst-case cost bounds achieved by feasible solutions (epigraph form), so they do not rely on a supremum of a possibly unbounded function. Affine policies must be nonnegative on $\mathcal U$. Optimal solutions are defined as feasible solutions whose worst-case cost is bounded by every achievable bound, so Lemma 8 asserts attainment. Powers $m^{a}$ are real powers; $\theta_0=1/m^{(1-\delta)/2}$ and $r=\lceil m^{1-\delta}\rceil$ exactly as on the page. $\mathcal U$ is the convex hull of its listed generators; the generator count $N$ printed in (19) plays no role.

The parameter $\delta$ is not restricted beyond $\delta>0$ and $m^\delta>200$, as in the paper. Lemma 4's proof on the page uses $\delta\le1$; the statement is kept for all $\delta>0$, where it remains true with a different witness. The Claims are stated for any symmetric feasible affine policy with cost at most $m^{1/2-\delta}/4$; their hypotheses are jointly unsatisfiable by Theorem 3, which is inherent in steps of a proof by contradiction.

A trivializing formalization is excluded: the goal mentions only the instance data and the two optimal values, not the symmetric parameters $\mu,\theta,\lambda$, and the nonemptiness of the feasible sets is established by Lemma 4 and by the existence of a feasible affine policy, so neither value is a junk infimum of an empty set.

A complete development needs: convex hulls of finite point sets in $\mathbb R^m$ and their extreme points; the action of $S^m$ by coordinate permutation; averaging over the finite group $S^m$; and existence of minimizers for linear programs over a polytope. The symmetrization lemmas (5–8) are reusable for other symmetric robust problems. Proofs of any milestone, including partial infrastructure for linear-programming attainment, are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A 134 (2012) 491–531. https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444

Motivation

Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.

Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.

Setting

Fix a horizon $T$ and an initial state $x_1\in\mathbb R$. For each stage $k=1,\dots,T$ there are a per-unit control cost $c_k\ge0$, control bounds $L_k\le U_k$, disturbance bounds $\underline w_k\le\overline w_k$, and a state cost $h_k:\mathbb R\to\mathbb R$ that is convex and coercive. The state evolves as

$$x_{k+1}=x_k+u_k+w_k,\qquad u_k\in[L_k,U_k],\qquad w_k\in\mathcal W_k=[\underline w_k,\overline w_k].$$

The controller chooses $u_k$ after seeing $x_k$; the adversary then chooses $w_k$. The min-max value $J_{mM}$ is the value of the nested problem $\min_{u_1}[c_1u_1+\max_{w_1}[h_1(x_2)+\min_{u_2}[\cdots]]]$, computed by the Bellman recursion with $J^*_{T+1}\equiv0$:

$$g_k(y)=\max_{w\in\mathcal W_k}\big[h_k(y+w)+J^*_{k+1}(y+w)\big],\qquad J^*_k(x)=\min_{L_k\le u\le U_k}\big[c_ku+g_k(x+u)\big],\qquad J_{mM}=J^*_1(x_1).$$

An affine control policy and an affine running cost at stage $k$ are

$$q_k(w)=q_{k,0}+\sum_{t=1}^{k-1}q_{k,t}w_t,\qquad z_k(w)=z_{k,0}+\sum_{t=1}^{k}z_{k,t}w_t,$$

so $q_k$ sees the disturbances before stage $k$ and $z_k$ those up to stage $k$. Under these policies the state after stage $k$ is $x_1+\sum_{t\le k}(q_t(w)+w_t)$.

Formalization targets

Goal: Theorem 3.1

There exist affine policies $q_k$ and affine costs $z_k$ such that, for every $k=1,\dots,T$,

$$L_k\le q_k(w)\le U_k\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_{k-1},$$ $$z_k(w)\ge h_k\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\quad\forall w\in\mathcal W_1\times\dots\times\mathcal W_k,$$ $$J_{mM}=\max_{w_1,\dots,w_k}\Big[\sum_{t=1}^k\big(c_tq_t(w)+z_t(w)\big)+J^*_{k+1}\Big(x_1+\sum_{t=1}^k(q_t(w)+w_t)\Big)\Big].$$

At $k=T$ this says that affine policies are robustly feasible and attain the min-max value.

Milestones

1. Lemma 7.1 (with (8)–(9), P2): $J^*_k$ and $g_k$ are convex, and the optimal control is the clamp $\max(L_k,\min(U_k,y^*-x))$ for a minimizer $y^*$ of $c_ky+g_k(y)$.
2. P3: the clamp is non-increasing and 1-Lipschitz.
3. Lemma 4.1: the maximum of $\theta_1+f(\theta_2)$, $f$ convex, over a planar zonogon $\Theta=\pi([0,1]^k)$ is attained at one of the $k+1$ vertices on its right side.
4. Corollary 4.1: the maximum of $\theta_1+f(\theta_2)$ is unchanged when a polygon is replaced by its convex hull, its vertex set, its right side, or the zonogon hull of its vertices.
5. Lemma 4.2: after the optimal control is applied, the worst case is reached on the right side of $\operatorname{conv}\{\tilde v_0,\dots,\tilde v_k\}$.
6. Lemma 4.4: the matching-and-alignment system (37) defining the affine controller is feasible, and its solutions satisfy $-b_i\le q_i\le0$ and $L\le q(w)\le U$.
7. Lemma 4.8 and Lemma 4.9: the affine cost defined by system (51)–(53) dominates the convex cost, first at the hypercube vertices, then on the whole hypercube.

Significance

The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the $h_k$ are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most $k+1$ vertices, matching the $k+1$ coefficients of an affine policy.

The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of $c_ky+g_k(y)$, and Lemma 4.3 is proved in one sub-case only.

Difficulty

Dynamic programming gives the optimal control as a function of the current state, $u^*_k(x_k)$, which is piecewise affine in $x_k$ with up to three pieces. Since $x_k$ is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost $z_k$ that still dominates $h_k$. Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all $2^k$ vertices of the disturbance box is overdetermined.

Formalization scope

Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 ($c_k\ge0$, $h_k$ convex and coercive) plus two disclosed additions, $L_k\le U_k$ and $\underline w_k\le\overline w_k$: the page writes both as intervals but does not say they are nonempty. $J^*_k$ is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.

The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by $b_i$, the hypothesis $b_i>0$. Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.

Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true $J^*_{k+1}$. The policies read only past disturbances (sums over $t<k$, resp. $t\le k$). $J_{mM}$ is the Bellman value over all state-feedback controls, not the value of the affine problem.

The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.

Selected references

• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of Affine Policies in Multi-stage Robust Optimization, arXiv:0904.3986v1, 2009; Mathematics of Operations Research 35(2):363–394, 2010. https://arxiv.org/abs/0904.3986, https://doi.org/10.1287/moor.1100.0444
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2):491–531, 2012. https://doi.org/10.1007/s10107-011-0444-4
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995 (Chapter 7, zonotopes). https://doi.org/10.1007/978-1-4613-8431-1

Motivation

A robust linear constraint $a'x \ge b$ for all $a \in \mathcal U$ protects a decision $x$ against every realization of the data $a$ in an uncertainty set $\mathcal U$. Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where $\mathcal U$ is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of $\mathcal U$ to the decision maker's attitude towards risk: on a finite sample $\mathcal A = \{a_1,\dots,a_N\}$, a coherent risk measure constraint $\mu(\tilde a'x - b) \le 0$ is equivalent to a robust constraint over a convex set built from $\mathcal A$, and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.

An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.

Setting

Fix $N \ge 1$ and data $a_1,\dots,a_N \in \mathbb R^n$, the columns of a matrix $A$. Let $e_N \in \mathbb R^N$ have $1/N$ at each entry, so the sample mean is $\hat a = Ae_N$.

• The restricted simplex $\hat\Delta^N$ is the set of probability vectors $q \in \mathbb R^N$ with $q_1 \ge \dots \ge q_N$. Under the uniform probability on $N$ points, the distortion risk measures are exactly the maps $\mu_q(X) = -\sum_i q_i x_{(i)}$, $q \in \hat\Delta^N$, with $x_{(1)} \le \dots \le x_{(N)}$ the ordered values of $X$ (Theorem 4.2 of the paper).
• For $q \in \mathbb R^N$, the $q$-permutohull is $\Pi_q(\mathcal A) = \operatorname{conv}\{\sum_i q_{\sigma(i)} a_i : \sigma \in S_N\}$. The robust constraint over $\Pi_q(\mathcal A)$ is the risk constraint for $\mu_q$.
• The symmetric restricted simplex $\hat\Delta^N_{\mathrm{sym}}$ is the set of $q \in \hat\Delta^N$ with $q = 2e_N - q_\sigma$ for some permutation $\sigma$, where $(q_\sigma)_i = q_{\sigma(i)}$. For these $q$ the permutohull is centrally symmetric about $\hat a$.
• With $\tilde\pi_q(\mathcal A) = \Pi_q(\mathcal A) - \hat a$, the Minkowski functional

$$\|w\|_{q,\mathcal A} = \inf\{\alpha > 0 : w/\alpha \in \tilde\pi_q(\mathcal A)\}$$

measures $w = a - \hat a$ against the shifted permutohull (12).

• The polyhedron is $\mathcal U = \{a \in \mathbb R^n : u_k'a \ge v_k,\ k = 1,\dots,m\}$ (14), with $\hat a \in \mathcal U$.

The family of candidate inner approximations is obtained by mixing a fixed $\hat q \in \hat\Delta^N_{\mathrm{sym}}$ with the uniform generator: $q = \lambda\hat q + (1-\lambda)e_N$, $\lambda \in \mathbb R$.

Formalization targets

Goal: Theorem 4.5

Let $\lambda^*$ be the optimal value of the linear program

$$\max\ \lambda\quad\text{s.t.}\quad q = \lambda\hat q + (1-\lambda)e/N,\quad e'(s_k + t_k) \ge v_k\ \forall k,\quad s_{k,i} + t_{k,j} \le (u_k'a_j)\,q_i\ \forall i,j,k, \tag{15}$$

in $s_k, t_k, q \in \mathbb R^N$ and $\lambda \in \mathbb R$, and $q^* = \lambda^*\hat q + (1-\lambda^*)e_N$. Then

$$\Pi_{q^*}(\mathcal A) \subseteq \mathcal U,\qquad \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \mathcal U \implies \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \Pi_{q^*}(\mathcal A),$$

and, when $\hat q \ne e_N$, $q^* \in \hat\Delta^N$ if and only if

$$\lambda^* \le \frac{1}{1 - N\hat q_{\min}}. \tag{16}$$

Milestones

1. Proposition 4.2: for $q \in \hat\Delta^N_{\mathrm{sym}}$ with $\Pi_q(\mathcal A)$ of nonempty interior, $\|\cdot\|_{q,\mathcal A}$ is a norm.
2. Scaling (proof of Lemma 4.2): $\Pi_{\lambda q + (1-\lambda)e_N}(\mathcal A) = \hat a + \lambda\,\tilde\pi_q(\mathcal A)$ for every $q \in \mathbb R^N$, $\lambda \in \mathbb R$.
3. Lemma 4.2: $\|a - \hat a\|_{\lambda q + (1-\lambda)e_N,\mathcal A} = \frac{1}{|\lambda|}\|a - \hat a\|_{q,\mathcal A}$ for $q \in \hat\Delta^N_{\mathrm{sym}}$, $\lambda \ne 0$.
4. Containment as linear constraints (proof of Theorem 4.5): $\Pi_q(\mathcal A) \subseteq \mathcal U$ iff vectors $s_k, t_k$ satisfying the constraints of (15) exist, for every $q \in \mathbb R^N$.
5. Nonnegativity (proof of Theorem 4.5): for $\lambda \ge 0$ and $N\hat q_{\min} < 1$, $\lambda\hat q + (1-\lambda)e_N \in \hat\Delta^N$ iff $\lambda \le 1/(1 - N\hat q_{\min})$.

Significance

The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with $N!$ potential vertices, that fits inside an arbitrary polyhedron — to a linear program with $O(mN)$ variables and $O(mN^2)$ constraints. Its solution identifies a distortion risk measure $\mu = \lambda^*\mu_{\hat q} + (1-\lambda^*)\mathbb E[-X]$, which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.

The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, $\lambda \ne 0$ in (13), $\hat q \ne e_N$ in (16)), and the containment equivalence for arbitrary real weight vectors $q$ is a reusable fact about permutohulls and assignment duality.

Difficulty

The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real $\lambda$, including the reflected case $\lambda < 0$; the maximality claim then needs the central symmetry of $\Pi_{\hat q}(\mathcal A)$ about $\hat a$, which is a property of $\hat\Delta^N_{\mathrm{sym}}$ (Proposition 4.1 of the paper) and not of a general $q$. The tempting shortcut — comparing gauges directly — fails at $\lambda = 0$, where the permutohull is the single point $\hat a$ and the gauge is degenerate.

Formalization scope

Vectors in $\mathbb R^N$ and $\mathbb R^n$ are Fin N → ℝ and Fin n → ℝ, with $0$-based indices; $a_i$ is a i, $u_k'a$ is a dot product. $\hat\Delta^N$ uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real $q$ because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value $0$ (not $+\infty$) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes $\Pi_q(\mathcal A)$ has nonempty interior and why the goal states "largest" as set containment. $\hat q_{\min}$ is $\min_i \hat q_i$. The optimal value $\lambda^*$ is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.

Standing assumptions and disclosed additions: $N \ge 1$; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of $q$, not $\tilde q$ as printed, and $\lambda \ne 0$; in (16), $N\hat q_{\min} < 1$; "corresponds to a distortion risk measure" is read, as the proof reads it, as $q^* \in \hat\Delta^N$. A formalization that assumes $\Pi_{q^*}(\mathcal A) \subseteq \mathcal U$ or the maximality of $\lambda^*$ trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.

A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.

Selected references

• D. Bertsimas and D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
• A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

Motivation

Airlines, hotels and cruise lines rarely change prices continuously. They sell a fixed product (seats on one flight, rooms on one night) over a finite selling season, and they sell it at a small set of fares, opening and closing fare classes as the season unfolds. Gallego and van Ryzin, in Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), model this as the sale of $n$ items over a horizon of length $t$, with Poisson demand whose rate depends on the current price. Section 4 of the paper restricts the price to a finite menu and asks how much is lost by using a simple rule that charges only two adjacent prices and switches once. The answer, Theorem 5, gives one explanation of fixed-fare-class yield management: with two fares and one well-timed switch, a seller earns asymptotically the best revenue any policy over the menu can earn. The source of this mission is the published 1994 article.

The paper is the starting point of a long line of work on fluid (deterministic) approximations in revenue management, including Feng and Gallego (1995) on optimal switching times between two prices and later re-solving and bid-price analyses, all of which compare stochastic policies to the value of a deterministic problem in the same way.

Setting

A menu consists of $K\ge2$ prices $p_1<p_2<\dots<p_K$ and Poisson demand rates $\lambda_1>\lambda_2>\dots>\lambda_K>0$; the firm may also charge the null price $p_\infty$, at which demand is $0$. The revenue rates $r_k=p_k\lambda_k$ satisfy $r_1>r_2>\dots>r_K$, and the points $(\lambda_k,r_k)$ lie on a concave function on $[0,\infty)$ vanishing at $0$.

The deterministic problem replaces random demand by its rate. If $t_k\ge0$ is the time spent at price $p_k$, the problem is the linear program

$$J^D(n,t)=\sup\Big\{\sum_k r_k t_k:\ \sum_k t_k\le t,\ \sum_k\lambda_k t_k\le n,\ t_k\ge0\Big\}.$$

Given $n\in\mathbb N$ and $t>0$, let $k=k^*$ be the index with $\lambda_k t\ge n>\lambda_{k+1}t$, and put

$$t_k=\frac{n-\lambda_{k+1}t}{\lambda_k-\lambda_{k+1}},\qquad m=\lceil\lambda_k t_k\rceil,\qquad t_m=\frac{m}{\lambda_k}.$$

The stopping-time (ST) heuristic starts at price $p_k$ and switches to $p_{k+1}$ at the random time $\tau=\min(T_m,t_m)$, where $T_m$ is the time of the $m$-th demand. Sales stop when the $n$ items are gone or at time $t$. $J^{ST}(n,t)$ is its expected revenue.

Formalization targets

Goal: Theorem 5

For a fixed index $k$ with $1\le k\le K-1$ and any sequences $n_j\in\mathbb N$, $t_j\to\infty$ with $\lambda_k t_j\ge n_j>\lambda_{k+1}t_j$,

$$\lim_{j\to\infty}\frac{J^{ST}(n_j,t_j)}{J^D(n_j,t_j)}=1.$$

No rate of convergence is fixed in the goal, and the ratio $n_j/t_j$ may vary along the sequence.

Milestones

1. Proposition 4. The LP is solved by pricing at $p_{k^*}$ for time $t_{k^*}$ and at $p_{k^*+1}$ for time $t_{k^*+1}=(\lambda_{k^*}t-n)/(\lambda_{k^*}-\lambda_{k^*+1})$, together with the edge cases $k^*=0$ and $k^*=K$.
2. The wasteful heuristic is a lower bound: $J^W(n,t)\le J^{ST}(n,t)$, where the wasteful heuristic offers $m$ units at $p_k$ during $[0,t_m]$ and $n-m$ units at $p_{k+1}$ afterwards.
3. Equation (28): the shrunk horizon $t'=t_m+(n-m)/\lambda_{k+1}$ satisfies $t-(\lambda_k-\lambda_{k+1})/(\lambda_k\lambda_{k+1})<t'\le t$.
4. The closed form of $J^D$ and $J^D(n,t)<J^D(n,t')+(p_{k+1}-p_k)$.
5. Equation (29): $J^{ST}(n,t)/J^D(n,t)\ge J^W(n,t)/J^D(n,t)\ge J^W(n,t')/(J^D(n,t')+(p_{k+1}-p_k))$.
6. The wasteful bound: $J^W(n,t')\ge p_k[m-\tfrac12\sqrt m]+p_{k+1}[(n-m)-\tfrac12\sqrt{n-m}]$ and $J^W(n,t')/J^D(n,t')\ge1-\tfrac12(1/\sqrt m+1/\sqrt{n-m})$.

Significance

Theorem 5 says that a policy with one price change, chosen from the deterministic solution, loses a vanishing fraction of the deterministic revenue. Since $J^D$ bounds the optimal expected revenue over all non-anticipating policies with prices in the menu (§4.0.1 of the paper), the ST heuristic is asymptotically optimal, and the optimal policy, which solves a Hamilton–Jacobi–Bellman system with no closed form, can be replaced by a rule that is computed by hand. The result also shows that a finite menu, together with dynamic allocation of capacity between two neighbouring prices, can realize the effective price of a continuous demand curve.

The theorem is proved in the paper. As far as the platform's index shows, neither this result nor the controlled Poisson sales process it needs has been formalized; Mathlib has the exponential and Poisson distributions but no counting process with a policy-dependent intensity. The mission produces a machine-checked version of the paper's proof chain: the LP solution, the coupling inequality between two heuristics, the deterministic horizon estimate (28), and the Poisson overflow estimate built on Gallego's bound (inequality (18) of the paper, already proved on the platform as PricingRM.DetHeuristic.gallego_bound).

Difficulty

The deterministic parts (Proposition 4, (28), the closed form of $J^D$) are finite-dimensional linear algebra. The difficulty sits in the stochastic comparison $J^W\le J^{ST}$. The ST heuristic's switching time depends on the sales process, and after the switch the remaining stock and the remaining time are both random. The obvious attempt, writing $J^{ST}$ as a sum of two independent Poisson terms, is wrong: the two phases are dependent through $\tau$. Any comparison has to handle a second phase whose starting stock and starting time are both random, which brings in the behaviour of the sales process after a random time determined by the process itself. The limit step then needs the overflow bound uniformly along sequences whose ratio $n/t$ is not fixed.

Formalization scope

All declarations live in the namespace GVRPricing.StoppingTime. The committed conventions are:

• Indices are 0-based (Fin K): Lean index $k$ is the paper's price number $k+1$, and lamN, pN, rN extend the sequences by $0$ beyond $K$, matching the paper's $\lambda_{K+1}=r_{K+1}=0$.
• The menu carries the printed conditions plus an added concavity condition: the points $(\lambda_k,r_k)$ lie on a concave function vanishing at $0$. This is the reading of §4's "corresponding to price $p_k$, we have a known demand rate $\lambda_k$" for a regular demand function with concave revenue rate. Without it Proposition 4 and Theorem 5 are false: the menu $\lambda=(3,2,1)$, $p=(1,1.01,1.5)$ meets every printed condition, but at $t=1$, $n=1.5$ Proposition 4's allocation earns $1.76$ while a feasible mix of $p_1$ and $p_3$ earns $1.875$, and the ST ratio tends to about $0.939$.
• $J^D$ is defined directly as the LP value; the reduction from the rate-path problem (11) is the paper's assertion and is not formalized.
• The sales process is built from $n$ i.i.d. standard exponential clocks by the time change of the ST policy's cumulative intensity, so at most $n$ items are sold. Time is elapsed time from $0$. $J^{ST}$ is the expectation of the sum of prices charged at sales in $[0,t]$, a lower Lebesgue integral of a bounded nonnegative function.
• $J^W$ is the paper's two-Poisson formula of p. 1018.
• $J^*$ is not defined, so the left ratio of (29) uses $J^D$ in place of $J^*$ (a stronger inequality, since $J^*\le J^D$), and the §4.0.1 upper bound $J^*\le J^D$ is not a milestone.
• Corrected slips: the page prints $t_{n-m}\doteq n-m/\lambda_{k+1}$ for $(n-m)/\lambda_{k+1}$; the wasteful bound is stated at the shrunk horizon $t'$, where its integrality assumptions hold exactly, instead of along the paper's subsequence; the ratio bound assumes $m<n$, since $1/\sqrt{n-m}$ is undefined otherwise. Proposition 4 is stated as optimality, without the uniqueness that fails when three menu points are collinear.
• Excluded: the edge cases $k^*=0$ and $k^*=K$ of Theorem 5, treated on the page only in an unproved remark.

A trivializing formalization would define $J^{ST}$ through the wasteful formula, or by a closed-form expression, which makes the goal the wasteful bound; here $J^{ST}$ is the expected revenue of the switching rule $\tau=\min(T_m,t_m)$ on the sales process. Likewise the limit is taken along sequences with $t_j\to\infty$, not at a single $(n,t)$.

Useful infrastructure, reusable beyond this mission: the exponential-clock construction of a Poisson process with piecewise-constant intensity, the strong Markov property at a stopping time of the clocks, and the expected Poisson overflow $\mathbb E(N_\mu-\mu)^+$. Contributions to any milestone, and alternative proofs of $J^W\le J^{ST}$, are welcome.

Selected references

• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. doi:10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11, 55–60, 1992 (the source of inequality (18)).
• Y. Feng, G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995.
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the source).

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

• 2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
• 2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
• 2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$, $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$, and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

1. $\mathcal P(x,S)\ge0$ for every $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ whenever $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$. The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$. Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$. The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$, $i=1,\dots,k$, and the heuristic earns

$$\mathrm{RO}=\max_{1\le i\le k}\operatorname{rev}(S_i).$$

Formalization targets

Goal: Theorem 3.2

$$\mathrm{OPT}\;\le\;\Big(\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\Big)\,\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\;\le\;1+\ln\frac{r_k}{r_1}.$$

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

• Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$.
• Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$.
• Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$, and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$.
• Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$.

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$, that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$, using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

• Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
• IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
• r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
• Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$, the number of distinct values. roSet r i is $S_i$; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
• Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$.
• Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$.

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$, and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Why the shape of the optimal pricing policy matters

A retailer holding a fixed stock of a perishable or seasonal good (fashion items, airline seats, hotel rooms, concert tickets) must sell it before a deadline, after which unsold units are worthless. Demand is random and depends on the posted price, and the firm may change its price at any time. Dynamic pricing asks how the price should depend on the remaining stock and the remaining time.

Gallego and van Ryzin (Management Science 40(8), 1994) posed this problem as a continuous-time intensity control problem and established its basic structure. Their Theorem 1 says that the optimal expected revenue is strictly increasing and strictly concave in both the stock and the time remaining, and that the optimal price falls as stock grows and rises with the time left to sell. The paper is a standard reference of revenue management; the structural result is the continuous-time counterpart of the monotonicity of marginal values in discrete-time models (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 5.2), and it is what makes the optimal policy computable by restricting attention to monotone policies. The paper credits a slightly weaker version to Kincaid and Darling (1963). The source formalized here is the published 1994 article.

The model and the Hamilton–Jacobi system

The firm chooses a demand rate $\lambda$ from a set $\Lambda \subseteq [0,\infty)$ of allowable rates, an interval containing $0$; the market then sets the price $p(\lambda)$, where $p$ is the inverse demand function, strictly decreasing and nonnegative on the positive rates. The rate $0$ corresponds to the null price at which nothing sells. The revenue rate is

$$r(\lambda) = \lambda\,p(\lambda), \qquad r(0) = 0.$$

The demand function is regular when $r$ is continuous, bounded and concave on $\Lambda$ and has a least maximizer $\lambda^* = \min\{\lambda : r(\lambda) = \max_{\mu\in\Lambda} r(\mu)\}$. The exponential demand $\lambda(p) = ae^{-p}$, with $\Lambda=[0,a]$, $p(\lambda)=\log(a/\lambda)$ and $\lambda^*=a/e$, is the running example.

With $n$ units in stock and time remaining $t$, write $J(n,t)$ for the optimal expected revenue. The paper derives the Hamilton–Jacobi system

$$\frac{\partial J(n,t)}{\partial t} = \sup_{\lambda\in\Lambda}\big[r(\lambda) - \lambda\big(J(n,t)-J(n-1,t)\big)\big], \qquad n\ge1,\ t>0, \tag{8}$$

with $J(n,0)=0$ and $J(0,t)=0$. The difference $J(n,t)-J(n-1,t)$ is the marginal value of an item; a rate attaining the supremum is an optimal intensity $\lambda^*(n,t)$, and $p(\lambda^*(n,t))$ is the optimal price $p^*(n,t)$.

Formalization targets

Goal: Theorem 1 (p. 1005)

For the solution $J$ of (8), with $r$ strictly concave, differentiable on the interior of $\Lambda$, and $\lambda^*$ interior:

$$J(n,t)\ \text{strictly increasing in } n\ (t>0)\ \text{and in } t\ (n\ge1);\qquad J(n+1,t)-J(n,t) < J(n,t)-J(n-1,t);$$ $$t\mapsto J(n,t)\ \text{strictly concave};\qquad \exists\,\lambda^*(n,t):\ \lambda^*\!\uparrow_n,\ \lambda^*\!\downarrow_t,\quad p^*\!\downarrow_n,\ p^*\!\uparrow_t\ \text{(strictly)}.$$

Milestones

1. The supremum in (8) is a maximum over $[0,\lambda^*]$ whenever the marginal value is nonnegative (proof of Proposition 1).
2. Proposition 1: (8) has a unique solution, and $\lambda^*(n,s)\le\lambda^*$.
3. Eq. (26): $J(n,t)-J(n-1,t) = r'(\lambda^*(n,t)) > 0$ for $t>0$.
4. The case $n=1$ of Theorem 1: $\lambda^*(1,t)$ strictly decreasing and $J(1,t)$ strictly concave in $t$.
5. $\lambda^*(n,0^+) = \lambda^*$.
6. Eqs. (9)–(10), exponential demand: $J(n,t) = \log\sum_{i=0}^n(\lambda^*t)^i/i!$ and $p^*(n,t) = J(n,t)-J(n-1,t)+1$.
7. Proposition 3, exponential demand: $\lambda^*(n,t)\le\lambda^D(n,t)=\min\{\lambda^*,n/t\}$ and $p^*(n,t)\ge p(\lambda^D(n,t))$.

Significance

Theorem 1 is the qualitative backbone of single-product dynamic pricing. Concavity of $J$ in $n$ means that each additional unit is worth less than the previous one, which is the basis of bid-price and marginal-value reasoning in revenue management; the monotone price path justifies markdown practice as the deadline approaches and reduces the policy search to monotone policies. Proposition 3 answers, for exponential demand, a question raised by Mills (1959): the stochastic optimal price is never below the deterministic one. The closed form (9)–(10) is one of the few exactly solvable intensity control problems in pricing.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires the comparison and monotonicity theory of a countable system of coupled ordinary differential equations whose right-hand side is a convex conjugate, a theory that Mathlib does not package. A complete development would also certify the corrected hypotheses of Theorem 1 described below.

Difficulty

The value functions are defined only implicitly by (8), a triangular infinite system of ODEs in which each $J(n,\cdot)$ is driven by $J(n-1,\cdot)$ through the nonsmooth map $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$. Monotonicity of the optimal intensity in $t$ is a statement about the time derivative of a marginal value, and the paper establishes it by an induction on $n$ combined with an argument by contradiction on the first interval where monotonicity could fail. The obvious approach of differentiating (8) twice in $t$ needs second derivatives of $r$ and of $J$ that the hypotheses do not provide, and the paper's own proof of Proposition 1 assumes that $J$ is nondecreasing in $n$, which is only established in Theorem 1; a rigorous development must break this circularity.

Formalization scope

A regular demand function is a Lean structure (GVRPricing.Structure.Model) holding $\Lambda$, $p$ and $\lambda^*$ with the paper's standing assumptions of §2.1: $0\in\Lambda\subseteq[0,\infty)$ an interval, $p$ strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$, $r(\lambda)=\lambda p(\lambda)$ continuous, concave and bounded on $\Lambda$, and $\lambda^*$ the least maximizer. The definition IsHJBSolution encodes (8) for $J:\mathbb N\to\mathbb R\to\mathbb R$, with the second argument the time remaining, the two-sided derivative at each $t>0$, continuity on $[0,\infty)$, the boundary conditions, and the requirement that the set inside the supremum be bounded above, so that the real supremum is never a default value. An optimal intensity at $(n,t)$ is any $\ell\in\Lambda$ maximizing $\lambda\mapsto r(\lambda)-\lambda(J(n,t)-J(n-1,t))$ over $\Lambda$.

All theorems are about solutions of (8), on which the paper's proofs operate. The identification of the solution of (8) with the supremum of expected revenue over non-anticipating pricing policies is Brémaud's verification theorem, which the paper cites and does not prove; it is not part of this mission.

Added hypotheses and corrected statements.

• As printed, Theorem 1 assumes only a regular demand function and is false: for $r(\lambda)=\sqrt\lambda$ on $[0,1]$ and $r=1$ beyond, $\lambda^*(1,t)=1$ for all $t\in(0,\ln2]$; for $r(\lambda)=\lambda-\lambda^2/4$ on $\Lambda=[0,1]$, $\lambda^*=1$ is on the boundary and $\lambda^*(1,t)=1$ for small $t$. The goal, eq. (26) and the case $n=1$ therefore assume that $r$ is strictly concave, differentiable on the interior of $\Lambda$, and that $\lambda^*$ is interior; the appendix proof uses all three. Proposition 1, the restriction lemma and $\lambda^*(n,0^+)=\lambda^*$ use only the printed assumptions.
• Strict claims in $n$ are made for $t>0$, since $J(n,0)=0$ for all $n$; optimal intensities are considered for $n\ge1$, $t>0$.
• Proposition 1's bound "$\lambda^*(n,s)\le\lambda^*$ for $0\le s$" is read at $s=0$ as "$\lambda^*$ is optimal", since every maximizer of $r$ is optimal there.
• Proposition 3 is stated for $n\ge1$, $t>0$ (the page says $n\ge0$, $t\ge0$, where $n/t$ or the optimal intensity is undefined).
• The exponential results use the paper's normalization $\alpha=1$ of $\lambda(p)=ae^{-\alpha p}$.
• The case $n=1$ omits the displayed identities involving $r''$ and $\lambda^{*\prime}$, which presuppose second derivatives; its conclusions are stated.

A formalization that defines $J$ by a formula, or postulates a monotone function as the optimal intensity, would trivialize the goal: the goal quantifies over every solution of (8), and the optimal intensity it asserts must maximize the right-hand side of (8) at every $(n,t)$.

A complete development needs comparison principles for scalar ODEs with Lipschitz right-hand sides, properties of the concave conjugate $\Delta\mapsto\sup_\lambda[r(\lambda)-\lambda\Delta]$ (monotonicity, Lipschitz continuity, envelope theorem), and monotone comparative statics of maximizers. These are reusable well beyond this mission; contributions of any of them, or of the milestones in any order, are welcome.

Selected references

• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
• W. M. Kincaid, D. A. Darling, An Inventory Pricing Problem, Journal of Mathematical Analysis and Applications 7, 183–208, 1963. https://doi.org/10.1016/0022-247X(63)90047-7
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000