Operations Research

Motivation

A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.

The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.

Setting

Demand is a random variable with distribution function $F$ and density $f$. The paper assumes $F(0) = 0$, $F$ strictly increasing, and an increasing generalized failure rate (IGFR): $g(x) = x f(x)/(1 - F(x))$ has $g'(x) > 0$. Production costs $c$ per unit, the retail price is $p$, and leftover units are salvaged for $v$, with $v < c < p$. Expected sales with $q$ units available are

$$S(q) = q - \int_0^q F(x)\,dx,$$

and the integrated supply chain's expected profit is $\Pi(q) = (p - v)S(q) - (c - v)q$. It is maximized at $q^o$ with $F(q^o) = (p-c)/(p-v)$; write $\Pi^o = \Pi(q^o)$. The efficiency of a contract is $\Pi(q)/\Pi^o$, where $q$ is the quantity produced.

A contract is a pair of wholesale prices $\{w_1, w_2\}$ with $w_1 \le w_2$. The retailer first prebooks $y \ge 0$ units at $w_1$ each. The supplier, seeing $y$, produces $q \ge y$. During the season the retailer sells the prebook and, once it runs out, places at-once orders at $w_2$ per unit from the supplier's remaining stock, provided $w_2 \le p$. The supplier's and retailer's expected profits are

$$\pi_s(y, q) = (w_1 - v)y + (w_2 - v)(S(q) - S(y)) - (c - v)q,$$ $$\pi_r(y, q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)(S(q) - S(y)),$$

with the at-once terms absent when $w_2 > p$. An outcome of a contract is a pair $(y, q)$ where $q$ maximizes the supplier's profit given $y$, and $y$ maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push ($w_1 < p < w_2$), pull ($w_1 = w_2 \le p$) and advance-purchase discount ($w_1 < w_2 \le p$). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).

Formalization targets

Goal: Theorem 7

For every $w_1$ with $c \le w_1 \le p$, the contract $\{w_1, p\}$ has an outcome and is Pareto; every outcome $(y, q)$ of every Pareto contract satisfies

$$\Pi(q) = \Pi^o;$$

and for every $r \in [0, \Pi^o]$ some contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome with payoffs

$$\bigl(\pi_r, \pi_s\bigr) = \bigl(r,\ \Pi^o - r\bigr).$$

Milestones

1. Eq. (2): $\Pi$ is concave on $[0, \infty)$ and maximized exactly where $F(q^o) = (p-c)/(p-v)$.
2. Eqs. (20)–(21): for $c \le w_2 \le p$, the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - c)/(w_2 - v)$.
3. Eq. (22): for $c \le w_1 \le w_2 \le p$, $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$ is the unique maximizer of $\pi_r(\cdot, q)$.
4. Eq. (3): in push mode the retailer's optimal prebook solves $F(q) = (p - \hat w_1)/(p - v)$.

A further draft theorem states the step of the proof in which the retailer's outcome profit along $\{w_1, p\}$ falls strictly from $\Pi^o$ to $0$ as $w_1$ rises from $c$ to $p$.

Significance

The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces $q^o$; the prebook price then acts as a pure transfer. Every division of $\Pi^o$ is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.

The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.

Difficulty

The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when $w_2 = p$. Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook $y = 0$ always being available and on $w_1 \ge c$. Third, the division claim is surjectivity of the retailer's equilibrium payoff over $w_1 \in [c, p]$, which needs the solution of $F(y_r) = (p - w_1)/(p - v)$ to vary continuously with $w_1$, including at both ends ($y_r = q^o$ at $w_1 = c$, $y_r = 0$ at $w_1 = p$).

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The standing assumptions are a structure: $F(0) = 0$, $F$ strictly increasing on $[0, \infty)$, $F' = f$ on $(0, \infty)$, and $g' > 0$ on $(0, \infty)$. Differentiability is required only on $(0, \infty)$, so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over $[0, \infty)$. $q^o$ is a parameter with the hypothesis $F(q^o) = (p-c)/(p-v)$; its existence is part of milestone 1.

Readings of informal words: "includes all" means every contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the $w_2 = p$ family; "any division is achievable" is surjectivity onto $[0, \Pi^o]$; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is $\max\{y, q_s\}$" is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when $w_2 \le p$ (p. 226, "with push $w_2 > p$, so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires $w_1 \ge c$ (p. 228 sets aside $\hat w_1 < c$ as Pareto inferior); pull includes $w_1 = w_2 = p$ (the paper's remark in the proof) and advance-purchase discounts include $w_2 = p$ (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.

Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of $\{w_1, p\}$ as $(y_r, q^o)$ would turn the goal into algebra, and is ruled out.

Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of $S$, and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon and M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

Who bears the inventory risk

A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.

Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.

Setting

Demand has distribution function $F$ and density $f$. The paper's standing assumptions (§3, p. 225) are: $F(0) = 0$, $F$ strictly increasing, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost $c$ to produce, sell at the retail price $p > c$, and are salvaged at $v < c$.

Expected sales with $q$ units available are $S(q) = q - \int_0^q F(x)\,dx$, and the integrated chain earns $\Pi(q) = (p - v)S(q) - (c - v)q$. It is maximized at the newsvendor quantity $q^o$, $F(q^o) = (p - c)/(p - v)$, with $\Pi^o = \Pi(q^o)$; the efficiency of a contract is $\Pi(q)/\Pi^o$.

A contract is described by the quantity $q$ it induces.

• Push at wholesale price $\hat w_1$: the retailer prebooks $q$ and earns $\hat\pi_r = (p - v)S(q) - (\hat w_1 - v)q$; the supplier earns $\hat\pi_s = (\hat w_1 - c)q$. The price inducing $q$ is $\hat w_1(q) = p - (p - v)F(q)$, and $\hat\pi_r(q)$, $\hat\pi_s(q)$ are the payoffs at that price.
• Pull at wholesale price $w_1 = w_2$: the supplier produces $q$ and earns $\pi_s = (w_1 - v)S(q) - (c - v)q$; the retailer earns $\pi_r = (p - w_1)S(q)$. The inducing price is $w_1(q) = (c - vF(q))/(1 - F(q))$.

Write $j(q) = S(q)/(1 - F(q))$ and $h(q) = f(q)/(1 - F(q))$ (the hazard rate). The retailer's preferred pull contract is $q^* = \arg\max \pi_r$ and the supplier's preferred push contract is $\hat q^* = \arg\max \hat\pi_s$.

A contract $k'$ Pareto dominates $k$ if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.

A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks $y \ge 0$ and the supplier then chooses her production $Q \ge y$ to maximize $(w_1 - v)y + (w_2 - v)(S(Q) - S(y)) - (c - v)Q$. A pull contract survives the push challenge if the retailer's profit is strictly highest at $y = 0$.

Formalization targets

Goal: Theorem 6 with Lemma 5

There is a quantity $q^P$, $0 < q^P < q^o$, the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that

$$\text{Pareto set} = \{\text{push}, \text{pull}\} \times [q^P, q^o],$$

and every pull contract with $q \in [q^P, q^o]$ survives the push challenge.

Milestones, in the order the proof uses them

• Eqs. (1)–(2), (3), (7): the newsvendor quantity $q^o$; the prices $\hat w_1(q)$, $w_1(q)$ induce $q$.
• Eqs. (5), (9) and Lariviere–Porteus: $\hat\pi_r$ and $\pi_s$ are increasing, $\hat\pi_s$ is unimodal.
• Lemma 1: $j(q)h(q)$ is increasing for $q > 0$. Theorem 2: $\pi_r$ is concave.
• Theorem 3: $\pi_r(q^*) > \hat\pi_s(\hat q^*)$, $q^* > \hat q^*$, $\Pi(q^*) > \Pi(\hat q^*)$.
• Lemma 4: $q^P$ exists, is the unique positive root of $\pi_r = \hat\pi_r$ and of $\pi_s = \hat\pi_s$, the unique maximizer of $\pi_r - \hat\pi_s$, and $q^P > q^*$.
• Eqs. (20)–(21) and Lemma 5: the supplier's reply to a prebook $y$ is $\max\{y, q_s\}$; pull contracts with $q \ge q^P$ survive the push challenge.

Significance

The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ($\hat q^*$ for the supplier, $q^*$ for the retailer) is Pareto, and the least efficient Pareto contract, $q^P$, is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself. The results are proved in the paper, with the calculus informal, the unimodality of $\hat\pi_s$ cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).

Difficulty

The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of $j(q)h(q)$ (Lemma 1), and that fails to be routine at $q \to 0$, where $F$ need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records $F(0) = 0$, $F$ strictly increasing on $[0, \infty)$, $F' = f$ on $(0, \infty)$, and $g'(x) > 0$ for $x > 0$. Differentiability is not required at $0$: the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy $v < c < p$; no sign is imposed on $v$. Quantities range over $[0, \infty)$. The paper's $q^o$ is a parameter characterized by $F(q^o) = (p - c)/(p - v)$, and the first milestone proves it exists and is unique.

Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.

Readings of informal words, each named in the item concerned:

• "increasing" in Lemma 1 and in Eqs. (2), (5), (9) is strict, as the proofs show; "concave" in Theorem 2 is strict concavity, as the proof shows via Lemma 1.
• "unimodal" means strictly increasing on $[0, \hat q]$ and strictly decreasing on $[\hat q, \infty)$ for some $\hat q > 0$.
• Uniqueness in Lemma 4 (i)–(ii) is over $q > 0$, since all profits vanish at $0$. Theorem 3 and Lemma 4 (v) hold for every maximizer, and the maximizers' existence is stated.
• Theorem 6's "includes all" is set equality, which its proof establishes. The survival conjunct comes from Lemma 5, which the proof's last sentence invokes.
• "prefers to prebook zero … rather than any positive amount" is strict preference.
• The contract space is the admissible contracts, $q \ge 0$ with wholesale price in $[c, p]$ (equivalently $0 \le q \le q^o$ in both modes). This is an explicit addition. The paper restricts prices to $\hat w_1 < p$ and $w_1 = w_2 < p$ and states that contracts with $q > q^o$ are Pareto inferior; but $\hat w_1 < p$ admits push with $q > q^o$ ($\hat w_1 < c$), where the retailer earns over $\Pi^o$ and nothing dominates.
• Eqs. (20)–(21) are stated for $w_2 > c$, which is what makes (21) solvable.

The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. $q^o$, $q^P$, $q^*$ and $\hat q^*$ are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.

Welcome contributions: basic facts about $S$, $j$ and $jh$ under the demand assumptions, reusable across the series' other two missions.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

Motivation

In the predict-then-optimize framework, a machine-learning model predicts the cost vector $\hat c$ of a linear optimization problem $\min_{w\in S}\hat c^\top w$, and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by $\hat c$ when the true cost is $c$. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.

The SPO loss is discontinuous in $\hat c$: its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and $\ell_q$ balls with $q\in(1,2]$.

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$ (the paper's $\mathbb R^d$ with a generic norm). A cost vector is a linear functional $c$ on $E$; its value at $w$ is written $c^\top w$, and its dual norm is $\|c\|_*=\max_{\|w\|\le1}c^\top w$. The closed ball of radius $r$ around $\bar w$ is $B(\bar w,r)=\{w:\|w-\bar w\|\le r\}$.

The feasible region $S\subseteq E$ is nonempty, compact and convex. An optimization oracle is any map $w^*$ with $w^*(\hat c)\in S$ and $\hat c^\top w^*(\hat c)\le\hat c^\top w$ for all $w\in S$; no tie-breaking rule is fixed.

• The degenerate set $\mathcal C^\circ$ consists of the cost vectors $\hat c$ for which $\min_{w\in S}\hat c^\top w$ has more than one optimal solution.
• The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$.
• $S$ satisfies the strength property with parameter $\mu>0$ if, for all cost vectors $\hat c$ and all $w\in S$,

$$\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \Big(\frac{\mu\,\nu_S(\hat c)}{2}\Big)\|w-w^*(\hat c)\|^2 .$$

• The normal cone of $S$ at $\bar w\in S$ is $N_S(\bar w)=\{c: c^\top(w-\bar w)\le0 \text{ for all } w\in S\}$.
• For $\bar\mu\ge0$, a convex set $S$ is $\bar\mu$-strongly convex if for all $w_1,w_2\in S$ and $\lambda\in[0,1]$,

$$B\Big(\lambda w_1+(1-\lambda)w_2,\ \Big(\frac{\bar\mu}{2}\Big)\lambda(1-\lambda)\|w_1-w_2\|^2\Big)\subseteq S .$$

Formalization targets

Goal: Theorem 7, strength claim (p. 23)

If $S$ is compact, not a singleton, and $\bar\mu$-strongly convex for some $\bar\mu>0$, then for every oracle $w^*$,

$$\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \Big(\frac{\bar\mu\,\nu_S(\hat c)}{2}\Big)\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S,\ \hat c .$$

The strength parameter equals the strong convexity constant.

Milestones

1. Maximum over a ball (Appendix D.1, p. 35): for $r\ge0$, $\max_{\tilde w\in B(\hat w,r)}c^\top\tilde w=c^\top\hat w+r\|c\|_*$.
2. Proposition 1 (Vial 1983; p. 23): for a $\bar\mu$-strongly convex set with $\bar\mu\ge0$ and every $\bar w\in S$,

$$N_S(\bar w)=\Big\{c: c^\top(w-\bar w)\le-\Big(\frac{\bar\mu}{2}\Big)\|c\|_*\|w-\bar w\|^2\ \text{for all } w\in S\Big\}.$$

3. Degenerate set (proof of Theorem 7, p. 24): under the hypotheses of the goal, $\mathcal C^\circ=\{0\}$.
4. Theorem 7, first claim (p. 23): under the same hypotheses, $\nu_S(\hat c)=\|\hat c\|_*$ for every $\hat c$.

Significance

Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with $\mu=\bar\mu$, so the Lipschitz constants in the margin analysis are explicit; and $\nu_S(\hat c)=\|\hat c\|_*$, so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).

The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.

Difficulty

Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant $\bar\mu/2$. Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of $c^\top w$ over a ball to be attained and equal to $c^\top\hat w+r\|c\|_*$, a fact about dual norms whose attainment depends on finite dimensionality.

For $\nu_S(\hat c)=\|\hat c\|_*$, comparing $\hat c$ with $0\in\mathcal C^\circ$ gives only the inequality $\nu_S(\hat c)\le\|\hat c\|_*$; equality needs every nonzero cost vector to have a unique minimizer over $S$. The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.

Formalization scope

• $E$ is a finite-dimensional real normed space with an arbitrary norm. Cost vectors are continuous linear functionals (StrongDual ℝ E), so $c^\top w$ is c w and the operator norm is the dual norm; balls are Metric.closedBall.
• The feasible region carries the paper's standing assumptions (§2, p. 5): compact, and convex (as part of the strongly convex set predicate). Nonemptiness follows from the hypothesis that $S$ is not a singleton, stated as S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.
• The oracle is quantified over: the goal holds for every map selecting a minimizer.
• $\nu_S$ is Metric.infDist to the degenerate set; the parameter conditions $\mu>0$ and $\bar\mu\ge0$ are hypotheses of the theorems, not parts of the predicates.
• The strongly convex set predicate includes convexity and quantifies $\lambda$ over $[0,1]$ only. Without the non-singleton hypothesis the theorem is false: a singleton is strongly convex for every $\bar\mu$, has no degenerate cost vector, and has $\nu_S\equiv0\ne\|\hat c\|_*$. A formalization that drops that hypothesis, quantifies $\lambda$ over all reals (which empties the ball for $\lambda\notin[0,1]$), or fixes a specific oracle is not this theorem.
• Reusable beyond this mission: the strongly convex set predicate and the normal-cone characterization (relevant to Frank–Wolfe analyses over strongly convex sets), and the identity for the maximum of a linear functional over a ball. Proofs of any milestone, and lemmas giving examples of strongly convex sets (Euclidean balls), are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022 (Mathematics of Operations Research, 2023). https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• J.-P. Vial, Strong and weak convexity of sets and functions, Mathematics of Operations Research 8(2), 1983. https://doi.org/10.1287/moor.8.2.231
• D. Garber, E. Hazan, Faster rates for the Frank–Wolfe method over strongly-convex sets, ICML 2015. https://arxiv.org/abs/1406.1305
• M. Journée, Y. Nesterov, P. Richtárik, R. Sepulchre, Generalized power method for sparse principal component analysis, JMLR 11, 2010. https://www.jmlr.org/papers/v11/journee10a.html

Motivation

Facility location asks where to open service points (warehouses, plants, servers) and how to connect customers to them so that the total opening cost plus the total connection cost is minimum. In the capacitated version each facility can serve only a limited number of customers, which is the situation in most applications: a warehouse has a floor area, a server a bandwidth. The problem is NP-hard, and the algorithms used in practice for it are often simple local search heuristics: start from a solution and repeatedly apply a small change that lowers the cost, until no such change exists.

The quality of such a heuristic is measured by its locality gap: the largest possible ratio between the cost of a solution that no allowed change can improve and the cost of an optimum solution. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave locality-gap analyses for k-median, uncapacitated facility location, and the capacitated problem in which several copies of a facility may be opened. This mission formalizes their §5, the capacitated case.

Timeline (as surveyed on pp. 545–546 of the paper). For the variant 1-CFL, where at most one facility may be opened at each location, Korupolu, Plaxton and Rajaraman (1998) showed that local search with add, drop and swap moves has locality gap at most 8 when capacities are uniform; Chudak and Williamson (IPCO 1999) refined this to 6, and Pál, Tardos and Wexler gave a local search with gap 9 for nonuniform capacities. For ∞-CFL, the variant with copies studied here, the known algorithms were LP-based: a 3-approximation of Chudak and Shmoys (1999) for uniform capacities, a 4-approximation of Jain and Vazirani for nonuniform capacities, and a 2-approximation of Mahdian, Ye and Zhang. Arya et al. (2004) analysed local search for ∞-CFL with nonuniform capacities: with a new move that drops any set of open copies and opens several copies of one facility, the locality gap is at most 4 (Theorem 5.5), and scaling the facility costs gives $2 + \sqrt3 + \epsilon$ (p. 561). The tight example for uncapacitated facility location (§4.3) also shows a locally optimum solution of cost 3 times the optimum, so the locality gap of the procedure lies between 3 and 4; its exact value was left open (§6).

Setting

An instance consists of a finite set $C$ of clients, a set $F$ of facilities and a distance $c$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji}$ is the cost of serving client $j$ from facility $i$. Every facility $i$ has an opening cost $f_i \ge 0$ and an integer capacity $u_i > 0$. Any number of copies of a facility may be opened; each copy of $i$ costs $f_i$ and serves at most $u_i$ clients.

A solution $X$ opens a finite list of copies, copy $s$ being a copy of facility $\mathrm{loc}(s)$, and assigns every client $j$ to a copy $\sigma(j)$ so that each copy $s$ serves at most $u_{\mathrm{loc}(s)}$ clients. Write $N_X(s)$ for the set of clients served by copy $s$ and $N_X(T)$ for the clients served by a set $T$ of copies. Its costs are

$$\mathrm{cost}_f(X) = \sum_s f_{\mathrm{loc}(s)}, \qquad \mathrm{cost}_s(X) = \sum_{j\in C} c_{j\,\mathrm{loc}(\sigma(j))}, \qquad \mathrm{cost}(X) = \mathrm{cost}_f(X) + \mathrm{cost}_s(X).$$

The neighbourhood (9) of a solution whose multiset of open facilities is $S$ consists of

1. $S + s'$: one more copy of any facility $s'$;
2. $S - T + l\cdot\{s'\}$: close any set $T$ of open copies and open $l \ge 1$ copies of a facility $s'$, provided $l\,u_{s'} \ge |N_S(T)|$.

$X$ is locally optimum if no neighbour, with any feasible assignment of the clients, has smaller cost.

Formalization targets

Goal: Theorem 5.5

For every instance with at least one client, every locally optimum solution $X$ and every solution $O$,

$$\mathrm{cost}(X) \le 4\,\mathrm{cost}(O).$$

Milestones

In the order the paper's proof uses them:

1. Lemma 5.1 (service cost): $\mathrm{cost}_s(X) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. Lemma 5.2: for every set $U$ of copies of $X$ and every facility $s'$,

$$\left\lceil \frac{|N_X(U)|}{u_{s'}}\right\rceil f_{s'} + \sum_{s\in U} |N_X(s)|\, c_{ss'} \ge \sum_{s\in U} f_s .$$

3. Lemma 5.4: in the graph with arcs $v_s \to w_o$ of length $c_{so}$ and $w_o \to \mathrm{sink}$ of length $f_o/u_o$, $|N_X(s)|$ units can be routed from every $v_s$ at cost at most $\mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$.
4. Inequality (10): the shortest-path flow, with $T_o$ the copies routed through $w_o$, satisfies $\sum_o\sum_{s\in T_o}|N_X(s)|(c_{so} + f_o/u_o) \le \mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$.
5. Inequality (11): $\sum_o f_o + \sum_o \sum_{s\in T_o} |N_X(s)|(c_{so} + f_o/u_o) \ge \mathrm{cost}_f(X)$.
6. Lemma 5.3 (facility cost): $\mathrm{cost}_f(X) \le 3\,\mathrm{cost}_f(O) + 2\,\mathrm{cost}_s(O)$.

A companion item states the scaled bound of p. 561: a local optimum for facility costs $(\sqrt3 - 1) f$ has cost at most $(2 + \sqrt3)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 5.5 gives a constant locality gap for a local search procedure for capacitated facility location with copies and nonuniform capacities, a variant previously approached through LP-based algorithms; the drop-add move it analyses is the paper's new operation for this problem. The scaled bound $2 + \sqrt3 \approx 3.732$ gives an approximation algorithm once local search is run to approximate local optimality. The paper also shows (Figure 13, the procedure T-hunt) that the exponentially large neighbourhood can be searched with a knapsack oracle, so the analysis applies to an implementable algorithm.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a checked model of capacitated facility location with copies (solutions, costs, the multiset neighbourhood) and of the locality-gap argument. The per-copy model and the flow comparison of Lemma 5.4 are reusable for other capacitated location problems and for local search analyses that compare a local optimum with an optimum through a flow or a matching.

Difficulty

The obvious attempt imitates the uncapacitated analysis: close one copy of $X$ and send its clients to a nearby copy of $O$. With capacities this fails, since that copy of $O$ may be too small to absorb them, and single-copy moves do not certify a constant bound. With the drop-add move a single copy of $O$ must be charged for a whole group of copies of $X$, and the groups must be chosen so that the charges add up to a constant times $\mathrm{cost}(O)$; the rounding $\lceil |N_X(T)|/u_{s'}\rceil$ of the number of new copies costs an additional $\mathrm{cost}_f(O)$ that has to be absorbed as well.

Formalization scope

• Solutions. A solution is a structure CFLSol Cl Fa u: a number n of open copies, a map loc : Fin n → Fa giving the facility of each copy, and an assignment σ : Cl → Fin n with the capacity constraint for every copy. Copies are separate indices because $N_S(s)$ is per copy. Its multiset of facilities is the image multiset of loc.
• Costs. A solution's cost is computed under its own assignment. The paper's cost of a multiset is the minimum over feasible assignments. Because every neighbour is compared with every feasible assignment, and $O$ ranges over every assignment, the statements are equivalent to the paper's. The move with $T = \{s\}$, $s' = \mathrm{loc}(s)$, $l = 1$ makes every reassignment of $X$'s clients a neighbour, so a locally optimum $X$ carries a minimum-cost assignment.
• Neighbourhood. Local optimality ranges over the whole of (9): every $s'$, every set $T$ of copies (including $\emptyset$ and all copies) and every $l \ge 1$ with $l u_{s'} \ge |N_X(T)|$. It is not restricted to what the search procedure T-hunt examines.
• Standing assumptions. Distances are nonnegative, symmetric and satisfy the triangle inequality on $C \cup F$; $d(x,x) = 0$ is not assumed. Capacities are natural numbers with $u_i > 0$; costs are real with $f_i \ge 0$; every client has unit demand. Ratios $f_o/u_o$ and the ceiling of Lemma 5.2 are computed in $\mathbb R$.
• Added hypothesis. The goal, Lemmas 5.2 and 5.3 and the companion assume at least one client. Without clients a single idle copy of a facility with $f = 1$, $u = 1$ is locally optimum at cost 1 while the empty solution costs 0, so these statements fail. The paper's instances implicitly have clients.
• No trivialization. $O$ is any solution, not a fixed optimum, and the bounds are multiplied out ($\mathrm{cost}(X) \le 4\,\mathrm{cost}(O)$, never a ratio). The empty solution is excluded only by the presence of a client, not by a default cost.
• Out of scope. The procedure T-hunt and the knapsack oracle, running time, the $\epsilon$ of approximate local optimality, and arbitrary demands.

Contributions are welcome at every level: proofs of the milestones, alternative proofs of Lemma 5.4 or (10) (for instance through a matching argument instead of flows), and general infrastructure for multiset neighbourhoods and assignment problems.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100

Motivation

The k-median problem asks where to open $k$ facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.

Local search is among the most widely used heuristics for it: start from any $k$ facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with $k$ facilities. This mission formalizes that result.

Timeline of the relevant bounds:

• Korupolu, Plaxton and Rajaraman (SODA 1998) analysed a local search for k-median that opens $k(1+\epsilon)$ facilities and costs at most $3 + 5/\epsilon$ times the optimum with $k$ facilities.
• Charikar, Guha, Tardos and Shmoys (STOC 1999) gave the first constant-factor approximation for metric k-median, by LP rounding ($6\tfrac23$).
• Jain and Vazirani (J. ACM 2001) and Charikar and Guha (FOCS 1999) improved the constant with primal–dual methods to 6 and 4.
• Arya et al. (STOC 2001; SIAM J. Comput. 2004) proved the locality gap 5 for single swaps and $3 + 2/p$ for swaps of $p$ facilities at a time, with matching examples.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. Write $c_{ji} = d(j,i)$ for the cost of serving client $j$ by facility $i$.

For a nonempty set $S \subseteq F$ of open facilities every client is served by its nearest open facility, and the cost of $S$ is

$$\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.$$

The k-median problem asks for a set $S$ of at most $k$ facilities of minimum cost.

A swap $\langle s, s'\rangle$ closes a facility $s \in S$ and opens a facility $s' \notin S$, giving $S - s + s' = (S \setminus \{s\}) \cup \{s'\}$. The neighbourhood of $S$ is

$$\mathcal B(S) = \{ S - \{s\} + \{s'\} \mid s \in S,\ s' \notin S \},$$

and $S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The local search starts from an arbitrary set of $k$ facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly $k$ facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.

The analysis uses the following notation. For a solution $A$, let $\sigma_A$ assign each client to a nearest facility of $A$, let $A_j = c_{j\sigma_A(j)}$ be the service cost of client $j$, and let $N_A(a)$ be the set of clients served by $a \in A$. For two solutions $S$ and $O$ put $N^o_s = N_O(o) \cap N_S(s)$. A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$; $s$ is bad if it captures some $o \in O$ and good otherwise.

Formalization targets

Goal: Theorem 3.2

For every metric instance, every $k$, every locally optimum set $S$ of exactly $k$ facilities and every nonempty set $O$ of at most $k$ facilities,

$$\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O).$$

The comparison solution $O$ is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.

Milestones, in the order the proof uses them

1. A facility $o$ is captured by at most one facility of $S$ (remark after Definition 3.1).
2. Property 3.1: for each $o$ there is a bijection $\pi$ of $N_O(o)$ with $\pi(N^o_s) \cap N^o_s = \emptyset$ whenever $s$ does not capture $o$.
3. When $|S| = |O|$ there are $|O|$ swaps $\langle s, o\rangle$, one for each $o \in O$, such that no facility capturing two or more facilities of $O$ is used, every good facility is used at most twice, and a used $s$ captures no $o' \ne o$.
4. Inequality (2): for a locally optimum $S$ and such a swap $\langle s, o\rangle$,

$$\sum_{j \in N_O(o)} (O_j - S_j) + \sum_{\substack{j \in N_S(s)\\ j \notin N_O(o)}} \bigl(O_j + O_{\pi(j)} + S_{\pi(j)} - S_j\bigr) \ge 0.$$

Significance

Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of $p \ge 1$ facilities, where the bound $3 + 2/p$ is 5 for $p = 1$. Combined with the standard device of accepting only swaps that improve the cost by a factor $1 - \epsilon/Q$, it yields a polynomial-time $5/(1-\epsilon)$-approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping $\pi$) are the reusable part.

The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.

Difficulty

The obvious argument adds up the inequalities $\mathrm{cost}(S - s + o) \ge \mathrm{cost}(S)$ over a pairing of $S$ with $O$, rerouting the clients of the closed facility $s$ to the nearest remaining facility. This fails when a single facility of $S$ serves most clients of several facilities of $O$: closing it leaves those clients with no nearby open facility, and no bound in terms of $\mathrm{cost}(O)$ follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when $S$ and $O$ share facilities.

Formalization scope

Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and $d(x,x) = 0$ is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes $S$ nonempty with S.card = k, which is the paper's $k \ge 1$. Local optimality quantifies over every swap $\langle s, s'\rangle$ with $s \in S$ and $s' \notin S$, exactly the neighbourhood $\mathcal B(S)$ of Theorem 3.2, and not only over the swaps with $s' \in O$ that the proof uses. The inequality is stated multiplied out, $\mathrm{cost}(S) \le 5 \cdot \mathrm{cost}(O)$, so it is meaningful when $\mathrm{cost}(O) = 0$.

The milestones quantify over nearest-facility assignments $\sigma_S$, $\sigma_O$ with arbitrary ties. Capture is stated in integers as $|N_O(o)| < 2|N^o_s|$. The bijection $\pi$ of $N_O(o)$ is a permutation of all clients fixing every client outside $N_O(o)$; in inequality (2) it is a single permutation preserving every $N_O(o)$. Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.

A formalization in which local optimality ranges over the swaps $\langle s, o\rangle$, $o \in O$, only, or in which $|O| = |S|$ or $O$ optimal is assumed, or in which the cost of the empty set is $0$, is a different statement and is ruled out.

A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping $\pi$ are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently of the goal.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
• K. Jain, V. V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

A coherent risk measure assigns to a future financial position the smallest amount of capital that makes it acceptable to a supervisor. Artzner, Delbaen, Eber and Heath characterised the one-period version: every coherent risk measure has the form $\pi(X)=\inf_{\mathbb Q\in\mathcal P}\mathbb E_{\mathbb Q}[X]$ for a set $\mathcal P$ of test probabilities (ADEH 1999). Regulators, insurers and banks, however, assess positions that evolve over several periods and whose risk is re-evaluated as information arrives. A multiperiod measurement should then be time consistent: the value assigned today should agree with the values the same method assigns tomorrow, so that it can be computed by backward induction, as in dynamic programming.

Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) identify exactly which sets of test probabilities give time-consistent multiperiod risk-adjusted values. The condition, stability under pasting, also appears as "rectangularity" in the recursive multiple-priors model of decision theory (Epstein and Schneider 2003), and as m-stability in the theory of risk-neutral measures (Delbaen, The structure of m-stable sets, Séminaire de Probabilités XXXIX, 2006). Riedel treated dynamic coherent risk measures on finite state spaces (Riedel 2004); the continuous-time case is in Delbaen's m-stable paper and Cheridito, Delbaen and Kupper 2004.

Setting

Let $(\Omega,\mathcal F,\mathbb P_0)$ be a probability space with a filtration $(\mathcal F_n)_{n\ge0}$ and a horizon $N$. A value process is an adapted process $X=(X_n)_{0\le n\le N}$ with every $X_n$ essentially bounded; the class of value processes is $\mathcal G$. All stopping times take values in $\{0,\dots,N\}$, and $\mathcal F_\sigma$ is the σ-algebra of the stopping time $\sigma$.

A set $\mathcal P$ of test probabilities is a closed convex set of probabilities on $(\Omega,\mathcal F_N)$, each absolutely continuous with respect to $\mathbb P_0$. Its elements are identified with their densities $f=d\mathbb Q/d\mathbb P_0$, and "closed" refers to $L^1(\mathbb P_0)$. $\mathcal P^e$ denotes the elements equivalent to $\mathbb P_0$. Each $\mathbb Q\in\mathcal P$ has the density martingale $Z^{\mathbb Q}_n=\mathbb E_{\mathbb P_0}[d\mathbb Q/d\mathbb P_0\mid\mathcal F_n]$.

Pasting. For $\mathbb Q^0,\mathbb Q\in\mathcal P^e$ with density martingales $Z^0,Z$ and a stopping time $\tau$, the pasted martingale is $L_n=Z^0_n$ for $n\le\tau$ and $L_n=Z^0_\tau Z_n/Z_\tau$ for $n\ge\tau$: the pasted probability follows $\mathbb Q^0$ up to $\tau$ and $\mathbb Q$ afterwards. $\mathcal P$ is stable (Definition 3.1) if every such pasting is again in $\mathcal P$.

Two risk-adjusted values. For a value process $X$ and a stopping time $\sigma$,

$$\Psi_\sigma(X)=\operatorname*{ess.inf}\bigl\{\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]\ \bigm|\ \tau\ge\sigma\text{ a stopping time},\ \mathbb Q\in\mathcal P^e\bigr\},$$

the worst conditional expected value over all test probabilities and all later stopping times. The generalized Snell envelope is the backward recursion

$$\bar\Psi_N(X)=X_N,\qquad \bar\Psi_n(X)=X_n\wedge\operatorname*{ess.inf}_{\mathbb Q\in\mathcal P^e}\mathbb E_{\mathbb Q}\bigl[\bar\Psi_{n+1}(X)\mid\mathcal F_n\bigr].$$

For a stopping time $\tau$ let $X^{\tau-}_n=X_n$ for $n<\tau$ and $X_{\tau-1}$ for $n\ge\tau$, and ${}^\tau X_n=0$ for $n<\tau$ and $X_n-X_{\tau-1}$ for $n\ge\tau$.

Formalization targets

Goal: Theorem 4.2

Assume $\mathcal F_0$ is $\mathbb P_0$-trivial and $\mathcal P^e\neq\emptyset$. Then the following are equivalent:

1. $\mathcal P$ is stable.
2. For every $\mathbb Q\in\mathcal P$ and $X\in\mathcal G$, $\Psi(X)$ is a $\mathbb Q$-submartingale.
3. $\Psi(X)=\bar\Psi(X)$ for every $X\in\mathcal G$.
4. Bellman's principle holds: for every $X\in\mathcal G$ and all stopping times $\sigma\le\tau$,

$$\Psi_\sigma(X)=\Psi_\sigma\bigl(X^{\tau-}+\Psi_\tau({}^\tau X)\mathbf 1_{[\tau,N]}\bigr).$$

Milestones

In attack order, all stated for any set $\mathcal P$ with $\mathcal P^e\neq\emptyset$ unless stability is named:

• Theorem 4.1. $\bar\Psi(X)$ is the largest process in $\mathcal G$ that lies below $X$ and is a $\mathbb Q$-submartingale for every $\mathbb Q\in\mathcal P$.
• Step (1) of the proof of Theorem 4.2. $\Psi_n(X)\ge\bar\Psi_n(X)$.
• Theorem 4.2, first sentence. The family $(\Psi_\sigma(X))_\sigma$ is a process: $\Psi_\sigma(X)=\Psi_{\sigma(\omega)}(X)(\omega)$ a.s.
• Remark after Theorem 4.2. $\Psi_\tau(X)=\Psi_\tau({}^\tau X)+X_{\tau-1}$.
• Lemma 3.1 (stable $\mathcal P$). For $\tau\le\sigma\le\nu$, $\{(Z_\nu/Z_\sigma,Z_\sigma/Z_\tau)\mid Z\in\mathcal P^e\}=\{(Z'_\nu/Z'_\sigma,Z_\sigma/Z_\tau)\mid Z,Z'\in\mathcal P^e\}$.
• Lemma 4.1 (stable $\mathcal P$). The family defining $\Psi_\sigma(X)$ is closed under minima and maxima.
• Corollary of Lemma 4.1 (stable $\mathcal P$). $\mathbb E_\mu[\Psi_\sigma(X)]=\inf\{\mathbb E_\mu[\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]]\mid\mathbb Q\in\mathcal P^e,\ \tau\ge\sigma\}$ for every probability $\mu\ll\mathbb P_0$.

A supporting item states that the essential infimum defining $\Psi_\sigma(X)$ exists.

Significance

The result. Theorem 4.2 characterises the sets of test probabilities for which the natural worst-case risk-adjusted value is computable by dynamic programming. Stability is thereby the structural condition behind time-consistent coherent risk measurement, recursive multiple-priors utility and backward-induction pricing under ambiguity. Without it, the worst-case value computed today may disagree with the value obtained by first computing tomorrow's worst case and then today's. The equivalence with the submartingale property says that stability is also exactly what makes $\Psi(X)$ the largest submartingale minorant of Theorem 4.1. Theorem 4.3 and the recursivity results for final values in Section 5 are corollaries.

Formalizing it. The paper's proof is complete apart from Lemma 4.1 and its Corollary, whose proofs are left to the reader. No machine-checked version of this result, of the generalized Snell envelope or of essential infima of families of random variables is known to exist. A formal proof would provide a reusable development of discrete-time optimal stopping under a set of probabilities, the essential-infimum calculus of Neveu, and density-martingale pasting — infrastructure that many results on robust optimal stopping, dynamic risk measures and robust Markov decision processes need.

Difficulty

The direction from stability to Bellman's principle needs an essential infimum to be exchanged with a conditional expectation under another probability (step (3) of the proof). This is false for a general family: an essential infimum of conditional expectations is not the conditional expectation of an essential infimum. The exchange works only because stability makes the family closed under minima (Lemma 4.1), so that it is directed downward and its essential infimum is the limit of a decreasing sequence, and because Lemma 3.1 lets the test probabilities used before and after $\tau$ be chosen independently. The converse, from the submartingale property to stability, is not a computation: it uses the separation theorem in $L^1$ against a pasted density assumed outside $\mathcal P$, which is where convexity and $L^1$-closedness of $\mathcal P$ are used. Dropping either hypothesis breaks that direction.

Formalization scope

Lean represents $\mathcal P$ by its set of densities in $\mathbb P_0$: $\mathcal F_N$-measurable, a.s. nonnegative, integrable, of mass one, convex, sequentially closed in the $L^1(\mathbb P_0)$ seminorm and saturated under a.s. equality. Test probabilities are $\mathbb Q_f=f\cdot\mathbb P_0$, and $\mathbb E_{\mathbb Q}[\cdot\mid\mathcal F_\sigma]$ is Mathlib's conditional expectation under $\mathbb Q_f$. Time is $\mathbb N$, and every stopping time is bounded by $N$. A $\mathbb Q$-submartingale on $0,\dots,N$ is Mathlib's Submartingale of the process frozen after $N$. The essential infimum of a family is defined in the mission (Mathlib has only that of a single function); a supporting item shows that it exists, so its fallback value is never used. All identities between risk-adjusted values hold $\mathbb P_0$-almost surely.

Conventions made explicit:

• the goal assumes that $\mathcal F_0$ is $\mathbb P_0$-trivial, which the proof uses when it treats $\Psi_0(X)$ as a number (without it, stability is not implied by (2)–(3));
• $\mathcal P^e\neq\emptyset$ replaces the paper's convenience assumption $\mathbb P_0\in\mathcal P$;
• $X_{-1}=0$;
• the Corollary's printed essential infimum over $\mathbb Q$ alone is read over $\mathbb Q$ and $\tau\ge\sigma$, as its right-hand side and its use require.

Bellman's principle must be stated with $\Psi$ on both sides and for all stopping times $\sigma\le\tau$. Replacing $\Psi$ by $\bar\Psi$, or restricting to deterministic times, turns the goal into a property of the recursion and is not the theorem.

Needed infrastructure, reusable beyond this mission: existence and directedness of essential infima of families; conditional expectations under equivalent measures and the Bayes formula; optional sampling for bounded stopping times under each $\mathbb Q$; the $L^1$–$L^\infty$ separation theorem. Contributions of any of these, and proofs of the milestones in any order, are welcome.

Selected references

• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, H. Ku, Coherent multiperiod risk adjusted values and Bellman's principle, Annals of Operations Research 152 (2007) 5–22. https://doi.org/10.1007/s10479-006-0132-6
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• L. G. Epstein, M. Schneider, Recursive multiple-priors, Journal of Economic Theory 113 (2003) 1–31. https://doi.org/10.1016/S0022-0531(03)00097-8
• F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112 (2004) 185–200. https://doi.org/10.1016/j.spa.2004.03.004
• P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112 (2004) 1–22. https://doi.org/10.1016/j.spa.2004.01.009
• F. Delbaen, The structure of m-stable sets and in particular of the set of risk neutral measures, Séminaire de Probabilités XXXIX, Lecture Notes in Mathematics 1874 (2006) 215–258. https://doi.org/10.1007/978-3-540-35513-7_17
• J. Neveu, Discrete-Parameter Martingales, North-Holland, 1975 (French original: Martingales à temps discret, Masson, 1972).
• Y. S. Chow, H. Robbins, D. Siegmund, Great Expectations: The Theory of Optimal Stopping, Houghton Mifflin, 1971; Dover reprint, 1991.