Operations Research

Motivation

Bilinear programs, which minimize an objective containing a term $x^\top y$ over constraints on $x$ and $y$, model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term $x^\top y$ is not convex, so such problems can have local minima that are not global. For example, $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$. When $x$ and $y$ are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple $x$ and $y$, this property is lost.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.

Timeline:

• 1969, Falk and Soland: a branch-and-bound scheme for separable nonconvex programs using convex envelopes, the pattern this algorithm follows.
• 1976, McCormick: convex underestimators of factorable functions, including the envelope of $xy$ on a rectangle.
• 1983, Al-Khayyal and Falk: the envelope of $xy$ over a rectangle (Theorem 2), the branch-and-bound algorithm for jointly constrained biconvex programs, and a proof of its convergence.

Setting

Fix $n \ge 1$ and a box $\Omega = \{(x,y) \in \mathbb{R}^n \times \mathbb{R}^n : l \le x \le L,\ m \le y \le M\}$ with coordinate rectangles $\Omega_i = [l_i, L_i] \times [m_i, M_i]$. Problem $\mathcal P$ is

$$\min\ \varphi(x,y) = f(x) + x^\top y + g(y) \quad \text{subject to } (x,y) \in S \cap \Omega,$$

with $f$, $g$ convex (and continuous) on their boxes, $S$ closed and convex, and $S \cap \Omega \neq \emptyset$. Its optimal value is $v^*$.

The convex envelope $\mathrm{Vex}_B\, h$ of a function $h$ over a set $B$ is the pointwise supremum of all convex functions that underestimate $h$ on $B$. For a box $B$, the node function $\psi^B(x,y) = f(x) + \mathrm{Vex}_B\, x^\top y + g(y)$ is convex and lies below $\varphi$ on $B$. The subproblem at node $B$, minimizing $\psi^B$ over $S \cap B$, is a convex program.

A run of the algorithm is a sequence of stages. Stage $0$ has the single open node $\Omega$. At stage $k$ the Best Bound Rule selects an open node $B_k$ whose subproblem value is least, and the stage point $(x^k, y^k)$ is its subproblem solution. The best lower bound is $v_b^k = \psi^{B_k}(x^k, y^k)$ and the best upper bound is $V_b^k = \min_{l \le k} \varphi(x^l, y^l)$. The selected node is then split. The algorithm picks the coordinate $I$ with the largest gap $x^k_i y^k_i - \mathrm{Vex}_{(B_k)_i}\, x_i y_i$ and replaces the rectangle $(B_k)_I$ by the four subrectangles cut out by the point $(x^k_I, y^k_I)$ (Figure 1 of the paper). All other rectangles are kept. The stage function $\psi^k$ assigns to each point of $\Omega$ the least node value $\psi^B$ among the open boxes containing it.

Formalization targets

Goal: convergence to a global solution

For every run,

$$\text{every accumulation point } (\bar x, \bar y) \text{ of } (x^k, y^k) \text{ solves } \mathcal P, \qquad \lim_k v_b^k = v^* = \lim_k V_b^k .$$

Milestones

In attack order:

• Theorem 2: $\mathrm{Vex}_\Omega\, xy = \max\{mx + ly - lm,\ Mx + Ly - LM\}$ on a rectangle.
• Theorem 3: the envelope is exact on the rectangle's boundary.
• The Corollary, in two parts:
  • separability, $\mathrm{Vex}_\Omega\, x^\top y = \sum_i \mathrm{Vex}_{\Omega_i}\, x_i y_i$;
  • exactness at points whose every coordinate pair lies on $\partial\Omega_i$.
• Along runs: $\psi^k \le \psi^{k+1} \le \varphi$ on $\Omega$.
• The bound chain $v_b^1 \le v_b^2 \le \cdots \le v^* \le \cdots \le V_b^2 \le V_b^1$.
• Termination when $v_b^k = V_b^k$.
• The gradient bound $\gamma_i$.
• The equicontinuity estimate $\|z - w\| < \varepsilon/(n\gamma) \Rightarrow |\mathrm{Vex}_B\, x^\top y(z) - \mathrm{Vex}_B\, x^\top y(w)| < \varepsilon$ within every sub-box $B$.
• The limit identity: along a convergent subsequence of stage points, $v_b^{k_t} \to \varphi(\bar x, \bar y)$.

Theorem 4 of the paper, on the envelope of $\sum f_i(x_i) + x^\top y + \sum g_i(y_i)$ with concave $f_i, g_i$, is included as a further target.

Significance

The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.

As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.

Difficulty

The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.

Formalization scope

Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from $0$ and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on $\mathbb{R}^{2n}$ is written out explicitly.

Hypotheses and corrections relative to the page:

• Continuity of $f$ and $g$ on their boxes is added; the paper uses it without stating it. $n > 0$ is assumed. The box form of convexity (p. 276) is used.
• Corollary, second clause (p. 276): "for all $(x,y) \in \partial\Omega$" is false for $n \ge 2$ (take $\Omega_1 = \Omega_2 = [0,2]^2$, $x = y = (0,1)$). It is stated for points with every $(x_i, y_i) \in \partial\Omega_i$.
• Well-definedness of the stage function (p. 277) is false from stage 3 on. Two open boxes can share a point at which their node functions differ, and the stage function then jumps. It is not a target. The stage function takes the minimum over the open boxes containing a point, and the continuity asserted on p. 279 is not formalized. The piecewise convexity asserted there is formalized as convexity of each open node function on its box.
• Equicontinuity (p. 282): the display $|H_i^{kj}(x_i,y_i) - H_i^{kj}(u_i,v_i)| \le |x_i y_i - u_i v_i|$ is false, and so is equicontinuity of the stage functions on all of $\Omega$. The estimate is stated within each sub-box, with the paper's $\delta = \varepsilon/(n\gamma)$.

Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.

Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.

Selected references

• F. A. Al-Khayyal and J. E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• J. E. Falk and R. M. Soland, An Algorithm for Separable Nonconvex Programming Problems, Management Science 15(9):550–569, 1969. https://doi.org/10.1287/mnsc.15.9.550
• G. P. McCormick, Computability of Global Solutions to Factorable Nonconvex Programs: Part I — Convex Underestimating Problems, Mathematical Programming 10:147–175, 1976. https://doi.org/10.1007/BF01580665
• H. Konno, Bilinear Programming: Part II. Applications of Bilinear Programming, Technical Report 71-10, Operations Research House, Stanford University, 1971 (reference [10] of Al-Khayyal and Falk; no online copy known). https://doi.org/10.1287/moor.8.2.273

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 5.9

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

The Lean development uses the following representation and conventions.

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

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

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

Selected references

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

Why price without knowing demand

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

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

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

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

Setting

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

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

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

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

Assumption 1 requires:

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 1

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

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

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

Milestones

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

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

Significance

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

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

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

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

Difficulty

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

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

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

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

Formalization scope

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

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

Selected references

• O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$. A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$, its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$, and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$. The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$, Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$. The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$. The authors construct the set

$$\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.$$

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

$$\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).$$

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$, while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$. Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$, $\Gamma_1,\Gamma_2\ge0$, $0<\varepsilon<1$, and $C^\top C=\hat\Sigma+\Gamma_2I$. This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$. The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$. The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$, yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

• D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
• J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
• G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$. The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$.

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$, observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$. Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$.

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

$$\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},$$

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$. A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$, $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$.

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$, $1\le j\le N$, be the $j$-th order statistic (the $j$-th smallest value) of coordinate $i$, and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

$$s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}$$

and the uncertainty set is the box

$$\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}$$

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$.

Formalization targets

Goal: Theorem 7

If $N-s+1<s$, then with probability at least $1-\alpha$ over the sample ($N$ samples of each marginal of $\mathbb P^*$, each marginal's samples i.i.d., arbitrary dependence across marginals),

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,$$

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}$$

Milestones

1. Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
2. Each one-sided order-statistic test is valid at level $\alpha/(2d)$: $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$, and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
3. Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
4. The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
5. If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
6. (EC.8): for $\mathbb P\in\mathcal P^M$, $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
7. (29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$, so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$, where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$, where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$, and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$, a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$.

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$-th sample of marginal $i$, under any probability law Q such that, for each $i$, the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$-th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$, together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$. Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$. A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$, $0<\epsilon<1$, $0<\alpha<1$, $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$, $\mathbb P^*$ a probability measure with $\mathbb P^*$-null complement of the box, and Theorem 7's hypothesis $N-s+1<s$. The page prints the second condition of $\mathcal P^M$ as "$\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$"; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with "$\le$" for each $\mathbb P\in\mathcal P^M$; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
• P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$.

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$, the Value at Risk is

$$\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.$$

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$, the forward deviation and the backward deviation are

$$\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.$$

From a sample, a bootstrap produces thresholds $t_i$, $\bar\sigma_{fi}$, $\bar\sigma_{bi}$. With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$. The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$, each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$, $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$.

The uncertainty set is

$$\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.$$

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$, $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$, the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

$$\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)$$

for every $v$, and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$.

Milestones

1. The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$.
2. The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$.
3. Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$.
4. The three one-dimensional sub-subproblems and their optimal values.
5. The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$.
6. $\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$, attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$.

Companions

• Remark 9: when (24) exceeds $t$, an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$.
• Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$.

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$, which should be $v_i^2\bar\sigma^2/(2\lambda)$, and the bound $m_b\le y_1\le m_b$). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$. The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$, and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$, so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

• $\bar\sigma_{fi},\bar\sigma_{bi}>0$, so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$.
• $m_b\le m_f$, which holds because $t_i\ge0$.
• The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
• "$\sigma_f(\mathbb P_i)\le\bar\sigma$" is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$", which is equivalent and avoids an unbounded supremum.
• Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$, stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$.

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441