Probability

Motivation

Food, blood and pharmaceuticals are perishable: a unit not sold within its lifetime is thrown away. A seller decides each period how much to order, which price to charge, and whether to dispose of stock early. A large stock of old units argues for a lower price and a smaller order.

Optimal policies for fixed-lifetime inventory are hard to characterize: the state is a vector of inventory levels by remaining lifetime (Fries 1975; Nahmias 1982), and later work turned largely to heuristics.

Chen, Pang and Pan (Oper. Res. 62(2), 2014) obtained structural results for the joint ordering, pricing and disposal problem with a positive replenishment lead time. They used L♮-concavity, a notion from discrete convex analysis (Murota 2003) that Zipkin (2008) used to analyze lost-sales inventory systems with lead times. This mission formalizes the paper's result for the case where unmet demand is backlogged.

Setting

A product with a lifetime of exactly $l \ge 2$ periods is reviewed periodically over a finite horizon of $T$ periods. Orders arrive after a lead time of $k$ periods, $0 \le k < l$. Write $L = l - 1$.

Vectors and L♮-convexity. For vectors $u, v \in \mathbb{R}^n$, $u \wedge v$ and $u \vee v$ are the componentwise minimum and maximum, and $e$ is the all-ones vector. A set $\mathcal{V}$ is L♮-convex if $(u + \alpha e) \wedge v$ and $u \vee (v - \alpha e)$ lie in $\mathcal{V}$ for all $u, v \in \mathcal{V}$ and $\alpha \ge 0$. A function $f$ is L♮-convex on $\mathcal{V}$ if moreover

$$f(u) + f(v) \ge f\big((u + \alpha e) \wedge v\big) + f\big(u \vee (v - \alpha e)\big),$$

and L♮-concave if $-f$ is L♮-convex. The ordered sets are $\mathcal{V}_{n,k} = \{s \in \mathbb{R}^n : s_1 \le \dots \le s_k\}$.

Data. The unit costs are $c$ (ordering), $h^+$ (holding), $h^-$ (backlogging) and $\theta$ (disposal), all nonnegative, and $\gamma \in [0, 1]$ is the discount factor. The seller chooses the expected demand $d \in \mathcal{D} = [\underline d, \bar d]$ in place of the price. The price is $P(d)$, strictly decreasing, and the expected revenue $P(d)d$ is continuous and concave on $\mathcal{D}$. The realized demand is $d_t = d + \varepsilon_t$, where the noise terms are i.i.d. with mean zero and support in $[A, B]$, $A \le 0 \le B$, and $\underline d + A \ge 0$.

State and decisions. The state $s = (s_1, \dots, s_{l-1})$ satisfies $s_1 \le \dots \le s_{l-1}$, so the state space is $\mathcal{S} = \mathcal{V}_{l-1,l-1}$. The coordinate $s_i$ is the inventory, net of backorders, with residual lifetime at most $i$, including orders in transit. Each period the seller chooses:

• an order-up-to level $s_l \ge s_{l-1}$;
• a demand level $d \in \mathcal{D}$;
• after demand is realized, a depletion $a$ with $s_1 \vee d_t \le a \le s_{l-k} \vee d_t$, so $a - d_t$ units are disposed of.

The next state is $\tilde s = (s_2 - a, \dots, s_l - a)$.

Recursion. The modified profit-to-go satisfies $f_{T+1} = 0$ and

$$f_t(s) = \max_{s_l \ge s_{l-1},\ d \in \mathcal{D}} \Big\{ P(d)d + \mathbb{E}\big[g_t(s, s_l, d \mid \varepsilon_t)\big] \Big\}, \qquad g_t = \max_{s_1 \vee d_t \le a \le s_{l-k} \vee d_t} \phi_t,$$ $$\phi_t(s, s_l, d, a \mid \varepsilon_t) = \gamma c\,\tilde s_{l-1} - c s_l - \theta(a - d_t) - h^+(s_{l-k} - a)^+ - h^-(a - s_{l-k})^+ + \gamma f_{t+1}(\tilde s).$$

In §4 the paper also assumes $c \le h^-/(1 - \gamma)$.

Formalization targets

Goal: Theorem 1 (p. 291)

For $t = 1, \dots, T+1$, $f_t$, $g_t$ and $\phi_t$ are L♮-concave in $s$, $(s, s_l, d)$ and $(s, s_l, d, a)$. The largest optimal order-up-to level $s_{lt}(s)$ and demand level $d_t(s)$ are nondecreasing in $s$, the optimal price is nonincreasing, and

$$s_{lt}(s + \omega e) \le s_{lt}(s) + \omega, \qquad d_t(s + \omega e) \le d_t(s) + \omega \qquad (\omega \ge 0).$$

The largest optimal depletion $a_t(s, s_l, d \mid \varepsilon)$ is nondecreasing, and $a_t(s + \omega e, s_l + \omega, d + \omega \mid \varepsilon) \le a_t(s, s_l, d \mid \varepsilon) + \omega$.

Milestones

• The ordered sets $\mathcal{V}_{n,k}$, $\mathcal{V}^+_{n,k}$ are L♮-convex (p. 287).
• Lemma 1: $g(x, \xi) = f(x - \xi e)$ is L♮-convex when $f$ is (p. 287).
• Lemma 2: partial minimization over an L♮-convex set preserves L♮-convexity (p. 287).
• The set $\{a \ge s_1 \vee d_t\}$ is L♮-convex (p. 291).
• The bound $f_{t+1}(\tilde s') - f_{t+1}(\tilde s) \le (\theta + c)\delta$ for the next states generated by $a' > a \ge s_{l-k}\vee d_t$ (p. 291).
• (9): $\phi_t$ is nonincreasing in $a$ beyond $s_{l-k} \vee d_t$, so the upper bound on $a$ can be dropped (p. 291).
• Lemma 3: the largest minimizer of an L♮-convex function is monotone, with $\xi(x + \omega e) \le \xi(x) + \omega$ (p. 287).
• The first sentence of Theorem 1, the L♮-concavity of $f_t$, $g_t$, $\phi_t$.
• Corollary 1: monotone sensitivity of the order quantity and the demand level in each age class (p. 292).
• Proposition 1: if $\theta \ge h^+/(1-\gamma)$, depleting only $d_t \vee s_1$ is optimal (p. 292).

Significance

The result. Theorem 1 gives a qualitative description of the optimal policy in a model where no closed form is available. Fresher inventory leads to ordering less and charging more. One more unit of inventory of any age raises the order-up-to level and the demand level by at most one unit. Corollary 1 refines this by age: the order quantity is most sensitive to young inventory, and the price discount is most sensitive to inventory close to expiry. These properties underlie the bounds and heuristics of §6 of the paper.

The formalization. The result is proved in the paper, but parts of the argument are informal: the $(\theta + c)\delta$ bound is a coupling argument, existence of optimal solutions is "straightforward to check and thus omitted", and Lemmas 1–3 are stated without proof. A formalization makes the induction checkable and yields a reusable library of L♮-convexity on real vectors with domains, used by the wider family of inventory models built on the same technique. None of these results is known to be machine-checked.

Difficulty

The obvious induction, that each step of the recursion preserves L♮-concavity, fails at the depletion problem (5): its constraint set is not L♮-convex, because of the upper bound $a \le s_{l-k} \vee d_t$, so Lemma 2 does not apply. The bound must first be shown inactive, which needs a quantitative estimate of how the profit-to-go changes when backorders are added, a property of the value function itself.

Lemma 3 handles a scalar decision, while Theorem 1 has a pair $(s_l, d)$ and needs the componentwise-largest maximizer; every supremum and expectation must also be shown to be finite.

Formalization scope

• Carrier. The paper treats $\mathbb{F} \in \{\mathbb{R}, \mathbb{Z}\}$ at once. The mission formalizes the real case only.

• L♮-convexity. Functions are real-valued on an explicit domain set, which is the paper's own convention for "L♮-convex on a set". The submodularity characterization is not used as the definition.

• Indexing. States are Fin L → ℝ with $L = l - 1 \ge 1$, indexed from 0, and the lead time satisfies $k \le L$. The paper's $s_{l-k}$ is coordinate $L - k$ of $(s_1, \dots, s_l)$: at $k = 0$ it is the decision $s_l$, and at $k = L$ it is $s_1$.

• Time. Time is counted in periods to go, which is faithful because the data are stationary. f 0 = 0 is $f_{T+1}$. The parts of Theorem 1 about $g_t$, $\phi_t$ and decisions cover the decision periods $t \le T$.

• Suprema and expectations. Every maximum is sSup of the image of a nonempty feasible set that is bounded above. Expectations are Bochner integrals against the noise law $\mu$.

• Optimal decisions. Largest optimal decisions are hypotheses at the points compared; at $\gamma = 1$, $k \ge 1$ no largest order-up-to level exists in the last period.

• Standing assumptions. All the §3 assumptions (nonnegative costs, $\gamma \in [0,1]$, strictly decreasing $P$, continuous concave revenue, zero-mean noise with support in $[A, B]$, $\underline d + A \ge 0$) are fields of the model structure. The §4 assumption $c \le h^-/(1-\gamma)$ is a hypothesis $(1-\gamma)c \le h^-$ of every §4 statement.

• Corrected slips.

  • The paper sets $f_t = +\infty$ off $\mathcal{S}$, a slip for $-\infty$. The Lean evaluates $f_t$ on $\mathcal{S}$ only.
  • In Lemma 3, "$\xi(x) + \omega \in \mathrm{dom}(f)$" reads $x + \omega e \in \mathrm{dom}(f)$.
  • The final "$< 0$" of (9) is stated as "$\le 0$". It is an equality when $h^- = 0$ and either $\gamma = 1$ or $\theta = 0$.
  • Proposition 1 needs $\gamma < 1$ for its quotient, and it asserts that $d_t \vee s_1$ is optimal, not that it is unique.

• Ruled-out formalizations. Any of the following would trivialize the mission:

  • defining $f_t$ as an arbitrary L♮-concave function, or taking the continuation in $\phi_t$ as a hypothesis-bound function;
  • dropping the upper bound $a \le s_{l-k} \vee d_t$ from the depletion interval;
  • restricting to $l = 2$.

  The value functions here are the model's own recursion, for every $l \ge 2$.

• What is needed. L♮-convexity on $\mathbb{R}^n$ with domains (shifts, sums, expectations, partial maximization, comparative statics for largest maximizers) and integrability of $g_t$ in the noise; all reusable. Proofs of single milestones are welcome.

• Source. The source is the published Operations Research article; in the copy held, printed page = PDF page + 282.

Selected references

• X. Chen, Z. Pang, L. Pan, Coordinating Inventory Control and Pricing Strategies for Perishable Products, Operations Research 62(2):284–300, 2014. https://doi.org/10.1287/opre.2014.1261
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4):937–944, 2008. https://doi.org/10.1287/opre.1070.0482
• K. Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508
• B. Fries, Optimal Ordering Policy for a Perishable Commodity with Fixed Lifetime, Operations Research 23(1):46–61, 1975. https://doi.org/10.1287/opre.23.1.46
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680

Motivation

Optimization under uncertainty usually fixes one probability distribution $\mathbb P$ for the uncertain data and optimizes an expected payoff, or fixes a set $\mathcal Q$ of distributions and protects against the worst one (robust optimization). The first is sensitive to a misspecified $\mathbb P$; the second can be very conservative, because it treats a barely plausible distribution exactly like the nominal one. Ben-Tal, Bertsimas and Brown (Oper. Res. 58(4), 2010) propose a graded alternative, the soft robust model: the decision maker accepts a loss of at most $\varepsilon$ in expected payoff under every distribution of a set $\mathcal Q(\varepsilon)$, simultaneously for all levels $\varepsilon$ up to a budget $\delta$. Larger sets of distributions are allowed a larger shortfall.

The paper's central result, Theorem 2.1, shows that this model is exactly a constraint on a convex risk measure in the sense of Föllmer and Schied (Finance Stoch. 6, 2002), and that every normalized convex risk measure arises from some soft robust model. This connects distributionally robust optimization with the theory of monetary risk measures, and gives a tractable convex reformulation of soft robust constraints. Related earlier work connected coherent risk measures with standard robust optimization (Bertsimas and Brown, Oper. Res. 57(6), 2009).

Setting

Let $(\Omega,\mathcal F)$ be a measurable space and $\mathcal P$ the set of all probability measures on it. A decision $x$ ranges over a nonempty, closed, convex set $X\subseteq\mathbb R^n$; a random variable $u:\Omega\to\mathbb R^m$ carries the uncertain parameters, and $f(x,u(\omega))$ is the payoff, concave in $x\in X$ for every $\omega$. For each $x\in X$ the random variable $f(x)=f(x,u(\cdot))$ is assumed bounded and measurable.

A family of measures is $\mathbf Q=\{\mathcal Q(\varepsilon)\subseteq\mathcal P:\varepsilon\ge0\}$. It is nondecreasing if $\mathcal Q(\varepsilon_1)\subseteq\mathcal Q(\varepsilon_2)$ for $\varepsilon_1\le\varepsilon_2$, and convex if $\mathbb Q_i\in\mathcal Q(\varepsilon_i)$ implies $\lambda\mathbb Q_1+(1-\lambda)\mathbb Q_2\in\mathcal Q(\lambda\varepsilon_1+(1-\lambda)\varepsilon_2)$ for $\lambda\in[0,1]$. The standing assumptions are that $\mathbf Q$ is nondecreasing and convex and that $\mathcal Q(0)\neq\emptyset$. The soft robust feasible set at level $\delta\ge0$ is

$$X^Q(\delta)=\Big\{x\in X:\ \inf_{\mathbb Q\in\mathcal Q(\varepsilon)}\mathbb E_{\mathbb Q}[f(x)]\ \ge\ -\varepsilon\quad\forall\,\varepsilon\in[0,\delta]\Big\}.\tag{5}$$

A risk measure, on the space $\mathcal Y$ of bounded payoffs, is a map $\rho:\mathcal Y\to\mathbb R$ with $Y_1\ge Y_2\Rightarrow\rho(Y_1)\le\rho(Y_2)$ and $\rho(Y+c)=\rho(Y)-c$ for $c\in\mathbb R$; it is convex if $\rho(\lambda Y_1+(1-\lambda)Y_2)\le\lambda\rho(Y_1)+(1-\lambda)\rho(Y_2)$. It is generated by a convex penalty $\alpha:\mathcal P\to[0,\infty]$ if $\rho(Y)=\sup_{\mathbb Q\in\mathcal P}\{-\mathbb E_{\mathbb Q}[Y]-\alpha(\mathbb Q)\}$, and normalized if in addition $\alpha(\mathbb Q)=0$ for some $\mathbb Q$. A family and a penalty determine each other:

$$\alpha^Q(\mathbb Q)=\inf\{\varepsilon\ge0:\mathbb Q\in\mathcal Q(\varepsilon)\},\qquad \mathcal Q^\alpha(\varepsilon)=\{\mathbb Q\in\mathcal P:\alpha(\mathbb Q)\le\varepsilon\},$$

and $\rho^Q$ denotes the risk measure generated by $\alpha^Q$.

Formalization targets

Goal: Theorem 2.1 for $\delta>0$

For every nondecreasing, convex family $\mathbf Q$ with $\mathcal Q(0)\ne\emptyset$, $\rho^Q$ is a convex risk measure generated by the normalized convex penalty $\alpha^Q$, the minimum below is attained for every $x\in X$, and

$$X^Q(\delta)=\Big\{x\in X:\ \min_{\lambda\ge0}\Big\{\lambda\delta+(\lambda+1)\,\rho^Q\Big(\frac{f(x)}{\lambda+1}\Big)\Big\}\le0\Big\}.\tag{6}$$

Conversely, for every convex risk measure $\rho$ generated by a normalized convex penalty $\alpha$, the family $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$, and (6) holds with $\rho$ on the right and $\mathbf Q^\alpha$ on the left.

Milestones: the steps of the proof (p. 1224)

1. The soft robust infimum $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\varepsilon:\varepsilon\in[0,\delta],\ \mathbb Q\in\mathcal Q(\varepsilon)\}$ equals $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\alpha^Q(\mathbb Q):\alpha^Q(\mathbb Q)\le\delta\}$.
2. Strong duality with an attained multiplier: that infimum equals $\max_{\lambda\ge0}\{-\lambda\delta+\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[f(x)]+(\lambda+1)\alpha^Q(\mathbb Q)\}\}$.
3. The scaling identity $\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[Y]+(\lambda+1)\alpha^Q(\mathbb Q)\}=-(\lambda+1)\rho^Q(Y/(\lambda+1))$.
4. $\rho^Q$ is a convex risk measure generated by the convex, normalized penalty $\alpha^Q$.
5. For a convex normalized $\alpha$, $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$.
6. $\alpha^{Q^\alpha}=\alpha$.

Significance

Theorem 2.1 makes the soft robust constraint usable: the right side of (6) is a single constraint in $(\lambda,x)$, and the function $(\lambda+1)\rho(f(x)/(\lambda+1))$ is jointly convex in $(\lambda,x)$ for $\lambda\ge0$, so soft robust problems are convex programs whenever the risk measure can be evaluated. Read in the other direction, it gives every normalized convex risk measure an interpretation as a graded robustness requirement over the level sets of its penalty, which is how the paper derives soft robust counterparts of optimized certainty equivalents, CVaR and entropic risk, and its later bounds on the probability of a loss.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a Lean development of convex risk measures generated by penalties on an arbitrary measurable space, with extended-valued penalties and mixtures of probability measures, and a one-constraint Lagrange duality theorem over a convex set of probability measures. Mathlib does not currently provide Lagrange duality in this form.

Difficulty

The equalities of the proof read as routine, and two of them are not. The first equality is described as "the definition of $\alpha^Q$", but a measure with $\alpha^Q(\mathbb Q)=\delta$ need not belong to $\mathcal Q(\delta)$, because the infimum defining $\alpha^Q$ need not be attained; the equality relies on the convexity of the family, the nonemptiness of $\mathcal Q(0)$ and the boundedness of $f(x)$. The second equality is Lagrange duality with dual attainment for a convex program whose variable is a probability measure and whose objective and constraint are extended-valued; the classical theorem applies to convex subsets of vector spaces, and transferring it to mixtures of probability measures with $[0,\infty]$-valued penalties is the main formal work. Attainment of the minimum in (6), which the paper asserts by writing "min", is exactly dual attainment and does not follow from the inequality alone.

Formalization scope

The probability measures are ProbabilityMeasure Ω on a measurable space; a family is a map from levels $\varepsilon\in\mathbb R_{\ge0}$ to sets of probability measures, and mixtures are built from the measures $t\,\mathbb Q_1+(1-t)\,\mathbb Q_2$. Penalties, including $\alpha^Q$, take values in $[0,\infty]$, so that a measure in no $\mathcal Q(\varepsilon)$ has penalty $+\infty$; a real-valued $\alpha^Q$ would give such measures penalty $0$ through the junk value of an empty infimum, and is excluded. Risk measures are real functions whose axioms are imposed on bounded measurable payoffs, "generated by" includes the least-upper-bound property of the supremum, and "min" in (6) is attainment on $[0,\infty)$ together with a nonpositive minimum. The decision set and payoff carry the paper's assumptions; concavity of the payoff and closedness and convexity of $X$ are kept although Theorem 2.1 does not use them. Infima over measures in the milestones are taken in the extended reals.

The case $\delta=0$ is excluded. The paper states Theorem 2.1 for $\delta\ge0$, but at $\delta=0$ its proof interchanges a limit in $\lambda$ with a supremum over measures without justification, and (6) fails: on $\Omega=\{a,b\}$ with $\mathcal Q(0)$ the measures giving $a$ mass at most $1/4$ and $\mathcal Q(\varepsilon)$ those giving it mass at most $1/2$ for $\varepsilon>0$, the payoff $f(a)=-2$, $f(b)=1$ is soft robust at level $0$ while the right side of (6) is empty. The goal and the milestones therefore fix $\delta>0$, the case the paper's main argument treats.

A complete development needs: convex risk measures and their generation by penalties, mixtures of probability measures, Lagrange duality with Slater's condition over convex sets of measures, and the scaling identity for $\rho^Q$. The duality theorem and the risk-measure layer are reusable beyond this mission. Contributions of any milestone are welcome, as are general convex-duality lemmas that the strong-duality step can import.

Selected references

• A. Ben-Tal, D. Bertsimas, D. B. Brown, A Soft Robust Model for Optimization Under Ambiguity, Operations Research 58(4, Part 2):1220–1234, 2010. https://doi.org/10.1287/opre.1100.0821
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 8.
• D. Bertsimas, D. B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0695

Motivation

Many engineering and operations problems must guarantee that a system operates safely with high probability, when the uncertain parameters $\tilde z$ are only partially known. A chance constraint asks that the safety condition $S\tilde z \le t$ hold with probability at least $1-\epsilon$ for a tolerance $\epsilon \in (0,1)$. When the distribution of $\tilde z$ is itself uncertain, the distributionally robust version asks this for every distribution in an ambiguity set $\mathcal P$ built from what is known: moments, supports, confidence regions. Two problems then arise: computing the worst-case probability $\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t]$ (uncertainty quantification), and optimizing a design $x$ under the constraint $\inf_{\mathbb P \in \mathcal P}\mathbb P[S(x)\tilde z \le t(x)] \ge 1-\epsilon$ (chance constrained programming).

Hanasusanto, Roitch, Kuhn and Wiesemann (Math. Program. 151, 2015) chart which combinations of ambiguity sets and constraint structures admit exact finite reformulations and which are strongly NP-hard. This mission takes the positive core of that chart: for Markov ambiguity sets (first-order moment information plus a conic support), the worst-case probability is the value of a finite conic program, and an individual chance constraint is equivalent to a finite system of linear conic inequalities.

Timeline. Chebyshev-type bounds for worst-case probabilities under moment information go back to the generalized Chebyshev inequalities of Vandenberghe, Boyd and Comanor (2007), and to the duality theory of moment problems summarized by Shapiro (2001). Wiesemann, Kuhn and Sim (2014) introduced the nested conic ambiguity sets used here to evaluate worst-case expectations. Hanasusanto et al. (2015) applied them to worst-case probabilities of polytopes and to chance constraints, proving Theorem 3 (moment problem reformulation) and Theorem 7 (individual chance constraints over Markov sets), together with strong NP-hardness results, such as Theorem 8, showing that the restrictions cannot be dropped.

Setting

Let $\tilde z \in \mathbb R^P$ be the uncertain parameters and $\tilde u \in \mathbb R^Q$ an auxiliary random vector. Fix $A \in \mathbb R^{K\times P}$, $B \in \mathbb R^{K\times Q}$, $b \in \mathbb R^K$, and a confidence set

$$\mathcal C_1 = \{(z,u) : C_1 z + D_1 u \preccurlyeq_{\mathcal K_1} d_1\},$$

where $C_1 \in \mathbb R^{L_1\times P}$, $D_1 \in \mathbb R^{L_1\times Q}$, $d_1 \in \mathbb R^{L_1}$ and $\mathcal K_1$ is a proper cone (closed, convex, pointed, with nonempty interior); $x \preccurlyeq_{\mathcal K} y$ means $y - x \in \mathcal K$, and $\mathcal K_1^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K_1\}$ is the dual cone. The Markov ambiguity set is

$$\mathcal P = \{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_1] = 1\},$$

the case $I = 1$, $\underline p_1 = \overline p_1 = 1$ of the paper's nested set (4).

Two regularity notions enter. $\mathcal C_1$ is essentially strictly feasible if it contains a point satisfying all non-polyhedral constraints of its description strictly. The Slater condition (S) for $I = 1$ requires $b$ to lie in the interior of $\{Az + Bu : (z,u) \in \mathcal C_1\}$.

For the safety system $S\tilde z \le t$ with rows $s_j^\top$, $j \in \mathcal J = \{1,\dots,J\}$, let $\mathcal L = \{j : \exists (z,u) \in \mathcal C_1,\ s_j^\top z > t_j\}$ be the rows that can be violated on $\mathcal C_1$. Problem (17) at $I = 1$ maximizes $b^\top\gamma + \underline p_1\lambda - \overline p_1\kappa$ over $\gamma \in \mathbb R^K$, $\lambda,\kappa \ge 0$, $\phi \in \mathcal K_1^\star$ and, for $j \in \mathcal L$, $\tau_j \ge 0$, $\psi_j \in \mathcal K_1^\star$, subject to $\lambda - \kappa + d_1^\top\phi \le 1$, $A^\top\gamma = C_1^\top\phi$, $B^\top\gamma = D_1^\top\phi$ and, for $j \in \mathcal L$, $\lambda - \kappa + d_1^\top\psi_j - \tau_j t_j \le 0$, $A^\top\gamma + \tau_j s_j = C_1^\top\psi_j$, $B^\top\gamma = D_1^\top\psi_j$.

For an individual constraint ($J = 1$) write $s^\top\tilde z \le t$. System (26) asks for $\beta \in \mathbb R$, $\gamma \in \mathbb R^K$, $\phi,\psi \in \mathcal K_1^\star$, $\tau \ge 0$ with

$$\beta + b^\top\gamma \ge (1-\epsilon)\tau,\ \ \beta + d_1^\top\phi \le \tau,\ \ \beta + d_1^\top\psi \le t,\ \ A^\top\gamma = C_1^\top\phi,\ \ B^\top\gamma = D_1^\top\phi,\ \ A^\top\gamma + s = C_1^\top\psi,\ \ B^\top\gamma = D_1^\top\psi.$$

Formalization targets

Goal: Theorem 7 (p. 18)

Under essential strict feasibility of $\mathcal C_1$, (S), and $\epsilon \in (0,1)$,

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon \iff \text{(26) is solvable}.$$

Milestones

1. Theorem 3 (case $I = 1$), sufficiency. Every feasible point of (17) has objective value at most $\mathbb P[S\tilde z \le t]$ for every $\mathbb P \in \mathcal P$.
2. Theorem 3 (case $I = 1$). Under essential strict feasibility and (S),

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t] = \sup\,(17).$$

3. §5 feasibility claim (with (17), case $I = 1$). Under the same hypotheses and $\epsilon \in (0,1)$, the chance constraint holds iff (17) has a feasible point of value at least $1-\epsilon$.
4. Theorem 7, sufficiency. Any solution of (26) certifies $\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon$ for all $\mathbb P \in \mathcal P$.

Significance

Theorem 7 turns an individual distributionally robust chance constraint over a Markov ambiguity set into finitely many linear conic constraints whose size is polynomial in the data. Since $s(x)$ and $t(x)$ are affine in the design $x$, the chance constrained program becomes a single conic program, solvable with standard software. The paper notes (p. 18) that, apart from the Wasserstein set, all ambiguity sets of its Section 2.3 are Markov sets or intersections of Markov sets with structural ambiguity sets, and Theorem 8 shows that adding a second confidence set already makes the problem strongly NP-hard, so the theorem marks a precise tractability boundary. Theorem 3 underlies the paper's later results and its §5 heuristic for intractable cases.

All five statements are proved in the literature: the paper defers its proofs to an accompanying technical report. None is machine-checked. A formal proof would supply a verified duality theory for moment problems with conic supports, a reusable bridge between semi-infinite constraints and conic certificates, and a verified basis for the paper's hardness results to be stated against.

Difficulty

The sufficiency halves are weak-duality arguments. The converse directions are not: the worst-case probability is an infimum over an infinite-dimensional set of measures, and the conclusion of Theorem 7 requires the dual certificate to be attained, not just approached. Two separate duality steps must both close without a gap and with attainment: the moment problem against its semi-infinite dual, which is where (S) enters, and each semi-infinite constraint against its conic dual over $\mathcal C_1$, which is where essential strict feasibility enters. The event $\{s^\top z > t\}$ is open, so the semi-infinite constraint must also be passed to its closure. Mathlib has neither a duality theorem for moment problems nor conic strong duality with attainment.

Formalization scope

The mission covers Markov ambiguity sets only ($I = 1$, $\underline p_1 = \overline p_1 = 1$). The general nested case of Theorem 3 is not stated, because the paper does not make (S) explicit for $I > 1$. Symmetry and unimodality information, joint chance constraints and the hardness results are out of scope. The paper's proofs are in a technical report that the mission does not use.

Conventions committed to in Lean:

• Vectors are Fin n → ℝ, the single confidence set is index 0 : Fin 1 of the published DRConvexOpt.Reform.AmbData, and its field c 0 is $d_1$.
• Probabilities are μ.real. The local paperAmbiguitySet reuses the published data and confidence-set definitions and requires integrability only of $A\tilde z+B\tilde u$. This makes the expectation condition void when $K=0$, as the paper states.
• "$\inf_{\mathbb P}\mathbb P[E] \ge 1-\epsilon$" is stated as "$1-\epsilon \le \mathbb P[E]$ for every $\mathbb P \in \mathcal P$", so an empty $\mathcal P$ is not mishandled by sInf ∅ = 0.
• "Coincides with the optimal value" is one real number that is both the greatest lower bound of the probabilities and the least upper bound of the objective values of (17).
• Essential strict feasibility is read as: $\mathcal K_1 = \mathcal K_p \cap \mathcal K_n$ for some polyhedral cone $\mathcal K_p$ and closed convex cone $\mathcal K_n$, with a point of $\mathcal C_1$ whose slack lies in $\mathcal K_p \cap \operatorname{int}\mathcal K_n$.
• The decision $x$ is fixed: $s, t$ stand for $s(x), t(x)$, and the program (2) and the set $\mathcal X$ are not formalized.
• $\epsilon \in (0,1)$, proper $\mathcal K_1$, essential strict feasibility and (S) are explicit hypotheses. The sufficiency halves drop (S) and essential strict feasibility, which they do not need.

Replacing essential strict feasibility by full strict feasibility, adding $\tau > 0$ to (26), or imposing the $\psi_j$-constraints for $j \notin \mathcal L$ would each change the theorem and is ruled out. The hypotheses are jointly satisfiable: $\mathcal C_1 = [-1,1]$, $A = 1$, $b = 0$, $\mathcal K_1 = \mathbb R^2_+$ satisfies all of them, with a nonempty ambiguity set.

A complete development needs conic duality with attainment under partial Slater conditions, Lagrangian duality for moment problems, and the reduction of a measure-valued infimum to finitely supported measures. All three are reusable well beyond this mission, and contributions to any of them are welcome.

Selected references

• G. A. Hanasusanto, V. Roitch, D. Kuhn, W. Wiesemann, A distributionally robust perspective on uncertainty quantification and chance constrained programming, Mathematical Programming 151(1), 35–62, 2015. https://doi.org/10.1007/s10107-015-0896-z
• W. Wiesemann, D. Kuhn, M. Sim, Distributionally robust convex optimization, Operations Research 62(6), 1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in: Semi-Infinite Programming, Kluwer, 135–165, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
• L. Vandenberghe, S. Boyd, K. Comanor, Generalized Chebyshev bounds via semidefinite programming, SIAM Review 49(1), 52–64, 2007. https://doi.org/10.1137/S0036144504440543
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

Why adaptive decisions matter

A planner often chooses a first action before uncertain inputs are known and a corrective action afterward. If the uncertain input has no trusted probability law, a distributionally robust model tests the first action against all laws consistent with known support and moment information. The corrective action may depend on the realized input. This combination produces a difficult optimization problem: the adversary chooses a probability law, while the planner chooses a function of the input. Bertsimas, Sim, and Zhang study a class in which the support and moment bounds have second-order-cone representations. Their particular question is whether a tractable affine corrective rule can recover the exact worst-case cost.

Earlier work on moment-based distributionally robust optimization developed other ambiguity sets and reformulations. The related Prove2Me drafts MinimaxSLP and TractableDRO address mean and second-moment equality classes or bounds on positive parts of affine functions. Their model conventions differ from this paper's lifted SOC support, so this mission develops its own definitions. The affine-policy result of Bertsimas, Iancu, and Parrilo concerns a different multistage robust model. The paper places these contributions in its account of robust and distributionally robust decision rules (pp. 604–605).

Two-stage model and lifted ambiguity set

Write $x\in\mathbb R^{N_1}$ for the first-stage decision and $z\in\mathbb R^{I_1}$ for the observed uncertainty. After observing $z$, the planner chooses a free second-stage vector $y\in\mathbb R^{N_2}$. The constraint data depend affinely on $z$: $A(z)=A^0+\sum_i A^i z_i$ and $b(z)=b^0+\sum_i b^i z_i$. The fixed recourse matrix is $B$, and $d$ gives the second-stage cost. The recourse value is

$$Q(x,z)=\min\{d^\top y:A(z)x+By\ge b(z),\ y\in\mathbb R^{N_2}\}.$$

The support set $W$ restricts possible realizations. An SOC ambiguity set $F$ contains probability laws $P$ on $z$ for which $P(W)=1$, $\mathbb E_P[Gz]=\mu$, and $\mathbb E_P[g_i(z)]\le\sigma_i$ for each auxiliary function $g_i$. The paper assumes that $W$ and each epigraph $\{(z,u_i):g_i(z)\le u_i\}$ can be represented using products of second-order cones (Definition 3). Its exact worst-case expected recourse cost is $\beta(x)=\sup_{P\in F}\mathbb E_P[Q(x,z)]$.

The model introduces an auxiliary vector $u\in\mathbb R^{I_2}$ with lifted support $\bar W=\{(z,u):z\in W,\ g(z)\le u\}$. The lifted ambiguity set $\mathcal G$ consists of joint laws on $(z,u)$ supported on $\bar W$ with $\mathbb E[Gz]=\mu$ and $\mathbb E[u]\le\sigma$. Proposition 1 states that the primary marginals of these joint laws are exactly $F$. A regular linear decision rule has $y(z)=y^0+Y^1z$. An extended linear decision rule has $y(z,u)=y^0+Y^1z+Y^2u$. Their best worst-case costs are $\beta_L(x)$ and $\beta_E(x)$, with feasibility enforced at every point of $W$ or $\bar W$ respectively (§3.1).

Formalization targets

Theorem 2 gives the comparison that holds for the two rule classes:

$$\beta(x)\le\beta_E(x)\le\beta_L(x).$$

Theorem 1 identifies $\beta(x)$ with the robust program (9). Its variables are $r\in\mathbb R$, $s\in\mathbb R^{L_1}$, and $t\in\mathbb R^{I_2}_+$, constrained by $r+s^\top Gz+t^\top u\ge Q(x,z)$ at every $(z,u)\in\bar W$; its objective is $r+s^\top\mu+t^\top\sigma$. This result assumes relative complete recourse and Assumption 1, which represents the actual lifted support by a product of second-order cones and supplies a strict Slater point.

The mission's goal is Theorem 4. Under complete recourse and one second-stage decision variable, the extended affine class gives the exact value for every first-stage vector:

$$\forall x\in\mathbb R^{N_1},\qquad \beta(x)=\beta_E(x).$$

The equality is stronger than the bounds alone: it says that optimizing over this finite-parameter decision-rule class loses no worst-case value in the stated regime (Theorems 1, 2, and 4).

What the result supplies

Theorem 4 gives a precise case where the lifted affine approximation is exact. This matters because the unrestricted corrective decision is a function, while the affine class is described by finitely many coefficients. The paper observes that, with one recourse variable, the associated dual polyhedron has only $M$ extreme points; the robust reformulation can therefore be handled using a finite collection of constraints in this regime (p. 610). Proposition 3 marks a boundary: relative complete recourse by itself does not ensure that any extended affine rule is feasible.

The results are proved mathematically in the published paper and its electronic companion; the proofs of Theorems 1 and 4 are located in the companion, which is not held with this mission's source PDF. The Lean statements here are open proof obligations. A completed development would add reusable interfaces for free-variable linear recourse, SOC-supported moment ambiguity sets, lifted joint laws, and extended-real optimization values. It would also make the assumptions behind the paper's real-valued expectations and recourse costs explicit.

The hard point

Replacing the adaptive function $y(z)$ by an affine function of $z$ alone can fail even when the recourse LP is feasible for every realization: a single affine rule must satisfy every pointwise constraint simultaneously. Adding $u$ enlarges the rule class, but the lifted support contains all $u\ge g(z)$, not just $u=g(z)$. Thus its feasibility condition is stronger than feasibility on a convenient graph. Theorem 4 asserts exactness despite that universal lifted-support constraint. The direct comparison $\beta\le\beta_E$ does not by itself give the reverse inequality; the robust moment reformulation must describe the same worst-case value under its Slater and recourse hypotheses (§§2.2–3.1).

Formalization scope

Finite vectors are functions on Fin n, so the paper's indices $1,\ldots,n$ become zero-based. Laws are probability measures on finite real-vector spaces. The original and lifted ambiguity sets include integrability of all primary coordinates; the lifted set also includes integrability of all auxiliary coordinates, and the original set includes integrability of each $g_i$. This is a finite-first-moment reading of the paper's expectations. It excludes laws whose constrained linear moments exist while an unconstrained coordinate has infinite absolute moment. These conditions ensure that expected affine rule costs are genuine. The paper's Theorem 3 itself explicitly asks for finite coordinate first moments.

The recourse LP is represented as a separate reusable definition with free $y$, constraints $By\ge t$, and dual feasibility $p\ge0$, $B^\top p=d$. Statements using its real value require primal and dual feasibility. Theorem 2 states primal feasibility on the support at its chosen $x$; Theorem 1 uses relative complete recourse on $X\times W$; Theorem 4 uses complete recourse for every right-hand side. Theorems 1 and 4 also state dual feasibility explicitly because primal feasibility alone does not ensure it. Assumption 1 is explicit in both, including equality between its cone representation and the previously defined $\bar W$. Its bound $u^\dagger<\sigma$ means strict inequality in every auxiliary coordinate, and strict cone feasibility means membership in the interior of the product cone.

The values $\beta$, $\beta_L$, $\beta_E$, and (9) lie in the extended reals. Each printed “min” is an infimum, and no optimizer is presumed. A value is never formed by subtracting infinities. The SOC support, the epigraphs, and all rule feasibility conditions retain their pointwise meanings. Neither an empty ambiguity set nor an impossible rule class is silently replaced by a favorable real default. Contributions to LP value regularity, integrability, moment duality, and SOC geometry are all useful beyond this mission. The goal must continue to compare the original $\beta$ with the actual lifted-rule value $\beta_E$; replacing either by an easier surrogate would remove its content.

Selected references

• Dimitris Bertsimas, Melvyn Sim, and Meixia Zhang, Adaptive Distributionally Robust Optimization, Management Science 65(2):604–618, 2019. DOI.

Motivation

A large family of random growth models, interacting particle systems and directed polymers in one space dimension share a common, non-Gaussian fluctuation theory: observables of size $t$ fluctuate on the scale $t^{1/3}$ (instead of the central-limit scale $t^{1/2}$), with spatial correlations on the scale $t^{2/3}$. This family is the Kardar–Parisi–Zhang (KPZ) universality class, named after the 1986 physics paper of Kardar, Parisi and Zhang. The KPZ universality conjecture (Open Problem Garden, posted 2020, importance "High") asks for a central limit theorem for this class: any one-dimensional growth model with a smoothing mechanism, short-range noise and slope-dependent ("lateral") growth should exhibit KPZ fluctuations.

KPZ fluctuations have been proved only for models with exact algebraic structure, such as the corner growth model / totally asymmetric exclusion process (Johansson, 2000) and the polynuclear growth model (Prähofer–Spohn, 2002). The Open Problem Garden entry describes ballistic deposition (Vold, 1959) as a concrete growth model with the KPZ features. Corwin's survey states the prediction that its column heights fluctuate like $t^{1/3}$ and notes that "this prediction has not been proved" (Corwin 2012, §1.1.1). Ballistic deposition has no known exact solvability, so it tests universality itself rather than one integrable instance of it.

Timeline.

• 1959 — Vold introduces ballistic deposition as a sediment model.
• 1986 — Kardar–Parisi–Zhang predict the exponents $1/3$ and $2/3$.
• 2000 — Seppäläinen proves a strong law of large numbers (hydrodynamic limit) for the ballistic deposition interface (arXiv:math/9906193).
• 2008 — Penrose proves linear growth of the mean height, $L^p$ laws of large numbers, polynomial moment bounds, a duality with a seed-grown process, and the only known lower bound on fluctuations: $\operatorname{Var}\xi_t(0)\gtrsim\log t$ in $d=1$ (arXiv:math/0608540).
• 2021 — Chatterjee proves existence of a stationary measure for the gradient process (arXiv:2110.10294).
• 2026 — Sudijono proves exponential concentration and the upper bound $\operatorname{Var}\xi_t(0)\le Ct$ (arXiv:2609.24056).

The gap between $\log t$ and $t$ is open; the predicted order is $t^{2/3}$.

Setting

Columns are indexed by $x\in\mathbb Z$. Each column carries an independent rate-one Poisson clock: on a probability space $(\Omega,P)$ the inter-arrival times $\tau_{x,k}$, $(x,k)\in\mathbb Z\times\mathbb N$, are independent and $\mathrm{Exp}(1)$-distributed, and the $n$-th ring of column $x$ (counting from $n=0$) is at time $T_{x,n}=\tau_{x,0}+\dots+\tau_{x,n}$.

Random deposition. The height $N_t(x)$ of column $x$ at time $t$ is the number of rings of its clock in $[0,t]$. Columns are independent and $N_t(x)$ is Poisson with mean $t$.

Ballistic deposition (nearest-neighbour model, flat initial surface). Write $\xi_t(x)\in\mathbb N$ for the height of column $x$ at time $t$, with $\xi_0\equiv0$. When the clock of column $x$ rings at time $t$, a unit block falls in column $x$ and sticks at the first point of contact, so

$$\xi_t(x)=\max\{\xi_{t-}(x)+1,\ \xi_{t-}(x-1),\ \xi_{t-}(x+1)\},$$

and all other columns are unchanged. On the finite substrate $Q_L=[-L,L]$ only clocks in $Q_L$ ring and columns outside $Q_L$ stay at height $0$; the finitely many rings in $[0,t]$ are applied in time order. The height on $\mathbb Z$ is the monotone limit $\xi_t(x)=\lim_{L\to\infty}\xi^{Q_L}_t(x)=\sup_L\xi^{Q_L}_t(x)$. The next-arrival height is $\eta_t(x)=\max\{\xi_t(x)+1,\xi_t(x-1),\xi_t(x+1)\}$. This is the model of Penrose (2008) with $d=1$ and the nearest-neighbour displacement function, and the model (1) of Sudijono (2026) with $d=1$.

Formalization targets

Goal: the KPZ fluctuation exponent

$$\exists\,c,C>0,\ T:\qquad c\,t^{2/3}\ \le\ \operatorname{Var}\xi_t(0)\ \le\ C\,t^{2/3}\qquad(t\ge T).$$

This is the statement "the column height fluctuates around its mean like $t^{1/3}$" (Corwin 2012, §1.1.1; Sudijono 2026, §1). The constants are left unspecified because they are model-dependent.

Stronger (not formalized here)

The predicted scaling limit: $(\xi_t(0)-\rho t)/(\sigma t^{1/3})$ converges in law to the Tracy–Widom GOE distribution for some model-dependent $\rho,\sigma>0$.

Milestones (known results)

1. Random deposition CLT: $(N_t(0)-t)/\sqrt t\Rightarrow\mathcal N(0,1)$, the Gaussian class, for contrast.
2. Penrose, Prop. 2.1: $\xi_t(0),\eta_t(0)<\infty$ a.s. and $E[\xi_t(0)^k],E[\eta_t(0)^k]=O(t^k)$.
3. Penrose, Thm. 2.1: $E\xi_t(0)/t\to\rho_1\in(0,\infty)$ and $\xi_t(0)/t\to\rho_1$ in every $L^p$, $p\ge1$.
4. Seppäläinen, Thm. 1 (as noted in Penrose, p. 5): $\xi_t(0)/t\to\rho_1$ almost surely.
5. Penrose, Thm. 2.2: $\liminf_t\operatorname{Var}\xi_t(0)>0$ and $\liminf_t\operatorname{Var}\xi_t(0)/\log t>0$.
6. Sudijono, Thm. 1.1 (2): $P(|\xi_t(0)-E\xi_t(0)|\ge r)\le C\exp(-c\,r^2/(t+r))$ for $t\ge1$, $r\ge0$.
7. Sudijono, Thm. 1.1 (3): $\operatorname{Var}\xi_t(0)\le Ct$ for $t\ge1$.

Significance

A proof of the goal would establish the KPZ exponent for a growth model without exact solvability, which is the content of the universality conjecture as opposed to its integrable special cases. For ballistic deposition only $\log t\lesssim\operatorname{Var}\xi_t(0)\lesssim t$ is currently known.

On the formal side, the milestones are known results with published proofs; formalizing them requires a library for continuous-time interacting particle systems on $\mathbb Z$ (graphical constructions, monotone couplings, finite speed of propagation), subadditive ergodic theory, and concentration inequalities for Poisson-driven processes. These pieces are reusable for first-passage percolation and other growth models. The goal itself is open.

Difficulty

The standard tools give the wrong exponents. Bounded-difference concentration applied to a last-passage representation fails because adding one clock ring can change future heights by an unbounded amount (Sudijono 2026, §1); martingale hitting-time arguments reach only the diffusive bound $O(t)$. Lower bounds of Pemantle–Peres type reach only $\log t$, as in first-passage percolation, where the analogous gap is also open. The exact formulas (determinantal structure, Bethe ansatz) behind the proved instances of KPZ fluctuations are not available for ballistic deposition.

Formalization scope

The model is encoded on a general probability space $(\Omega,P)$ with inter-arrival times τ : ℤ → ℕ → Ω → ℝ satisfying IsPoissonClocks P τ (measurability, mutual independence over ℤ × ℕ, each law expMeasure 1). The finite-substrate process boxHeight τ L t ω sorts the rings in $[-L,L]\times[0,t]$ lexicographically by (time, column) and folds the update rule bdStep; bdHeight τ t x ω : ℕ∞ is the supremum over $L$. Real-valued statements use bdHeightReal, which is bdHeight cast to ℝ with the value $0$ on the event $\{\xi_t(x)=\infty\}$; this event is null (Milestone 2), so the convention does not affect any distributional statement. Ties between rings and non-divergent arrival times are null events and receive junk values. Variances are Mathlib's variance, which returns $0$ for non-square-integrable variables; the lower bound in the goal therefore also forces square-integrability, so the goal cannot hold vacuously. Moments in Milestone 2 are lower Lebesgue integrals in $[0,\infty]$, so they are not trivialised by non-integrability.

Contributions welcome: the graphical construction and its basic properties (monotonicity in $L$ and $t$, a.s. finiteness), the duality with seed-grown deposition, subadditivity of hitting times, and the Poisson CLT.

Selected references

• I. Corwin, The Kardar–Parisi–Zhang equation and universality class, Random Matrices Theory Appl. 1 (2012). https://arxiv.org/abs/1106.1596
• M. Kardar, G. Parisi, Y.-C. Zhang, Dynamic scaling of growing interfaces, Phys. Rev. Lett. 56 (1986). https://doi.org/10.1103/PhysRevLett.56.889
• T. Kojar (poster), KPZ Universality Conjecture, Open Problem Garden (2020). http://www.openproblemgarden.org/op/kpz_universality_conjecture
• M. D. Penrose, Growth and roughness of the interface for ballistic deposition, J. Stat. Phys. 131 (2008). https://arxiv.org/abs/math/0608540
• T. Seppäläinen, Strong law of large numbers for the interface in ballistic deposition, Ann. Inst. H. Poincaré Probab. Statist. 36 (2000). https://arxiv.org/abs/math/9906193
• T. Sudijono, A linear variance bound for ballistic deposition, preprint (2026). https://arxiv.org/abs/2609.24056
• S. Chatterjee, Existence of stationary ballistic deposition on the infinite lattice, preprint (2021). https://arxiv.org/abs/2110.10294
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000).
• M. J. Vold, A numerical approach to the problem of sediment volume, J. Colloid Sci. 14 (1959).

Motivation

Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, portfolio management and capacity planning are standard examples. Their dynamic programming equations involve recourse functions (cost-to-go functions) of the decision history, which cannot be computed exactly. Stochastic Dual Dynamic Programming (SDDP), introduced by Pereira and Pinto in 1991, approximates each recourse function from below by a maximum of affine cuts, built at trial points generated by simulating sampled scenarios. SDDP is the method of choice in the energy industry for long-horizon stochastic planning.

Two extensions motivate this mission. Risk-averse planning replaces the expectation at each stage by a coherent risk measure (for instance the Conditional Value-at-Risk), and many applications have convex but nonlinear stage problems. Guigues (2016) proves that the risk-averse sampling algorithm for convex stage problems converges almost surely.

Timeline.

• 1991: Pereira and Pinto introduce SDDP for linear multistage problems.
• 2008: Philpott and Guan prove almost sure finite convergence of SDDP-type methods for linear problems with finitely many scenarios.
• 2011: Shapiro analyses the sample-average SDDP method and formulates its risk-averse variant with nested conditional risk measures; 2013: Philpott, de Matos and Finardi treat SDDP with coherent risk measures in dual form.
• 2015: Girardeau, Leclère and Philpott prove almost sure (asymptotic) convergence of sampling-based decomposition methods for risk-neutral multistage stochastic convex programs.
• 2016: Guigues extends that analysis to risk-averse problems in dual form, with nonlinear constraints and interstage independent processes (arXiv:1408.4439, SIAM J. Optim.); the convergence theorem is Theorem 4.1.

Setting

There are $T$ stages with decisions $x_t\in\mathbb R^n$ and a given $x_0$. A history $x_{1:t}=(x_1,\dots,x_t)$ is identified with the vector $[x_1;\dots;x_t]\in\mathbb R^{nt}$ with its Euclidean norm. The random data $\xi_t$ are interstage independent (H1). For $t\ge2$, $\xi_t$ takes $M$ values $\xi_{t,1},\dots,\xi_{t,M}$ with probabilities $\Phi_{t,j}>0$, and $\xi_1$ is deterministic. A realization $\xi_{t,j}$ consists of a cost $f_t(\cdot,\Psi_{t,j})$ with values in $\mathbb R\cup\{+\infty\}$, convex constraints $g_t(x_0,\cdot,\Psi_{t,j})\le0$ and linear constraints $\sum_{\tau=0}^tA_{t,\tau,j}x_\tau=b_{t,j}$. Together with a compact set $\mathcal X_t$, they define the feasible set $X_t(x_{0:t-1},\xi_{t,j})$.

The risk measure of stage $t$ is given in dual form,

$$\rho_t(Z)=\sup_{p\in\mathcal P_t}\sum_{j=1}^Mp_j\Phi_{t,j}Z_j,\qquad \mathcal P_t\subseteq\mathcal D_t=\Big\{p\ge0:\sum_jp_j\Phi_{t,j}=1\Big\}.$$

The recourse functions satisfy $\mathcal Q_{T+1}\equiv0$ and, for $t=T,\dots,2$,

$$\mathfrak Q_t(x_{1:t-1},\xi_{t,j})=\inf_{x_t\in X_t(x_{0:t-1},\xi_{t,j})}f_t(x_{1:t},\Psi_{t,j})+\mathcal Q_{t+1}(x_{1:t}),\qquad \mathcal Q_t(x_{1:t-1})=\rho_t\big(\mathfrak Q_t(x_{1:t-1},\xi_t)\big).$$

The first-stage value is $\mathcal Q_1(x_0)=\mathfrak Q_1(x_0,\xi_1)$. Assumption (H2) requires convexity, lower semicontinuity and properness of the data, and fixes an $\varepsilon>0$ such that the costs are finite and the feasible sets nonempty on the $\varepsilon$-fattening $[\mathcal X_1\times\dots\times\mathcal X_{t-1}]^\varepsilon$. It also asks for a relative-interior point of the nonlinear constraints.

Algorithm 1 keeps cutting-plane models $\mathcal Q^k_t$, starting from $\mathcal Q^0_t\equiv-\infty$. At iteration $k$ it computes decisions $x^k_m$ at every node $m$ of the scenario tree, by solving the stage problems with $\mathcal Q^{k-1}_{t+1}$ in place of $\mathcal Q_{t+1}$. It then samples one scenario $n^k_1,\dots,n^k_T$, with indices $\xi^k_t$ satisfying the independence assumption (H3), and adds at each sampled node one cut

$$\theta^k_t+\langle\beta^k_t,\,\cdot-x^k_{[n^k_{t-1}]}\rangle,\qquad \theta^k_t=\sum_mp_{k,m}\Phi_m\mathfrak Q^{k-1}_t(x^k_{[n]},\xi_m),\quad\beta^k_t=\sum_mp_{k,m}\Phi_m\pi_{k,m}.$$

Here $p^k$ attains the supremum in $\rho_t$, and $\pi_{k,m}$ is a subgradient of $\mathfrak Q^{k-1}_t(\cdot,\xi_m)$.

Formalization targets

Goal: Theorem 4.1 (p. 12)

Almost surely, for $t=2,\dots,T+1$ and every node $n$ of stage $t-1$,

$$\lim_{k\to\infty}\mathcal Q_t(x^k_{[n]})-\mathcal Q^k_t(x^k_{[n]})=0.$$

Almost surely, moreover, $\mathfrak Q^k_1(x_0,\xi_1)\to\mathcal Q_1(x_0)$, and every accumulation point of the first-stage decisions $(x^k_1)$ is an optimal solution of the first-stage problem.

Milestones

• Proposition 2.2: subgradient bound $\|s\|\le(M_0-m_0)/\varepsilon$ for the value function of a convex program.
• Proposition 3.1: $\mathcal Q_t$ is convex, finite and continuous on $[\mathcal X_1\times\dots\times\mathcal X_{t-1}]^{\hat\varepsilon}$, $0<\hat\varepsilon<\varepsilon$.
• Lemma 3.2: valid cuts $\mathcal Q^k_t\le\mathcal Q_t$, bounded cut coefficients and slopes, and Lipschitz models for $k\ge T-t+1$.
• Lemma 3.4: $\mathcal Q^k_t(x^k_{[n^k_{t-1}]})=\theta^k_t$.
• Lemma 3.5: a uniform Lipschitz constant $L$ for the models.
• (4.26), (4.28), (4.29), (4.31): the steps of the proof of Theorem 4.1. These are the error propagation along the tree, the limit along the iterations through a node, the almost sure limit along the other iterations, and the first-stage bound.

Significance

Theorem 4.1 guarantees that the algorithm's lower bound $\mathfrak Q^k_1(x_0,\xi_1)$ converges to the true risk-averse optimal value, and that its first-stage decisions approach optimal ones. It covers nonlinear convex stages, where finite convergence arguments for polyhedral problems do not apply. It also covers every risk measure with a dual representation, including CV@R and its combinations with expectation. Practitioners rely on this to justify stopping rules based on the lower bound.

The result is proved on paper. To our knowledge neither Theorem 4.1 nor its risk-neutral counterpart (Girardeau–Leclère–Philpott, Theorem 3.1) has been machine-checked; the risk-neutral statements are posed, unproved, on this platform. A formalization would check a proof that combines convex analysis (value functions of convex programs, subgradient bounds, Lipschitz continuity on fattenings), cutting-plane bookkeeping and a probabilistic argument (strong law of large numbers along a predictable subsequence).

Difficulty

The cuts are built only along sampled scenarios, so at a given node the approximation is refined only at the iterations whose scenario passes through it. The obvious induction argument controls the error $\mathcal Q_t-\mathcal Q^k_t$ only along those iterations. Extending it to all iterations is the probabilistic core (4.29). It needs the samples to be independent of everything the algorithm has computed so far, and it needs a strong law of large numbers along the subsequence of iterations at which the error is still large. A second difficulty is passing from the current model $\mathcal Q^k_{t+1}$ to the previous one $\mathcal Q^{k-1}_{t+1}$. This needs uniform Lipschitz bounds on the models (Lemmas 3.2, 3.5), which in turn rest on the fattening in (H2) and on the subgradient bound of Proposition 2.2.

Formalization scope

• Histories and norms. Histories are $L^2$ products of copies of $\mathbb R^n$ (PiLp 2), so fattenings, inner products and Lipschitz constants use the Euclidean norm on $\mathbb R^{n(t-1)}$. Fattenings are closed thickenings.
• Extended reals. Values are in EReal, infima are $+\infty$ on empty feasible sets, and weights $p_j\Phi_{t,j}$ are real numbers (with $0\cdot(\pm\infty)=0$). Limits of gaps are taken in EReal, so that convergence to $0$ forces the gaps to become finite.
• Data and indices. The recourse functions are constructed by the backward recursion from the data. The scenario tree is the product tree indexed by histories of realization indices, so (H1) is built into the model. Stage 1 uses the data of the first realization index.
• Runs. A run is pinned to fixed deterministic choice rules (minimizers, maximizing $p^k$, subgradients), so it uses only present and past samples. The goal holds for every choice of rules.
• Departures from the printed text, disclosed in the items.
  • The cut slope $\pi_{k,m}$ is any subgradient of $\mathfrak Q^{k-1}_t(\cdot,\xi_m)$. The printed formula on p. 9 uses a partial subgradient of $f_t$, which is not a subgradient when $f_t$ is nonsmooth, and the proof only uses the subgradient property.
  • $\mathcal P_t\ne\emptyset$ is assumed; it is implicit, because $\rho_t$ is a real-valued coherent risk measure.
  • In Proposition 2.2, $M_0$ is an extended-real supremum. The proof's claim that $M_0$ is finite does not follow from lower semicontinuity.
  • Lemma 3.2's vacuous "almost surely" is dropped.
  • One $\varepsilon$ serves all stages in (H2).
• Ruled out. A formalization in which the decisions or cuts ignore the models, or in which $\mathcal P_t=\emptyset$ or every stage value is $+\infty$, would make the limits trivial. The decisions must minimize against $\mathcal Q^{k-1}_{t+1}$, the cut must use the attained supremum, and the companion item run_exists shows that under (H2), with closed $\mathcal P_t$, rules producing a run exist for every sample path.
• Infrastructure and contributions. A complete development needs value functions of parametric convex programs, subgradient bounds for convex functions on fattenings, Lipschitz continuity of finite maxima of affine functions, and a strong law of large numbers along predictably selected subsequences (Lemma A.3 of Girardeau–Leclère–Philpott). The last two are reusable well beyond this mission. Contributions to any milestone, or to these general lemmas, are welcome.

Selected references

• V. Guigues, Convergence analysis of sampling-based decomposition methods for risk-averse multistage stochastic convex programs, SIAM J. Optim. 26(4), 2016; preprint arXiv:1408.4439v4. https://arxiv.org/abs/1408.4439
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1), 2015. https://doi.org/10.1287/moor.2014.0664
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• A. B. Philpott, V. L. de Matos, E. Finardi, On solving multistage stochastic programs with coherent risk measures, Oper. Res. 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007