The OR Formalization Drive

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk $\delta$. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity $\mathbb E_{\boldsymbol\mu}[\tau_\delta]$, the expected number of samples a strategy takes before stopping.

Timeline of the question this mission formalizes:

• Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
• Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every $\delta$-PAC strategy (arXiv:1407.4443).
• Garivier and Kaufmann (COLT 2016) identified the exact constant $T^*(\boldsymbol\mu)$ in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as $\delta\to0$ (arXiv:1602.04589). This mission covers the upper-bound half of that paper.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$; $b$ is twice differentiable and strictly convex, and $\nu_\theta$ has mean $\dot b(\theta)$. Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence $d(\mu,\mu')$ is the Kullback–Leibler divergence between the members with means $\mu$ and $\mu'$.

A bandit model $\boldsymbol\mu=(\mu_1,\dots,\mu_K)$ assigns a member of the family to each arm. The class $\mathcal S$ consists of models with a unique optimal arm $a^*(\boldsymbol\mu)$. At each round $t=1,2,\dots$ the learner picks an arm $A_t$ as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time $\tau_\delta$ recommends an arm. $N_a(t)$ is the number of draws of arm $a$ in the first $t$ rounds and $\hat\mu_a(t)$ its empirical mean.

With $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S: a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ and $\Sigma_K$ the probability simplex, the characteristic time is

$$T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}\ \inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\ \sum_{a=1}^K w_a\,d(\mu_a,\lambda_a),$$

and the maximizer $w^*(\boldsymbol\mu)$ are the optimal proportions of arm draws.

Track-and-Stop combines two ingredients:

• a sampling rule that tracks the plug-in proportions $w^*(\hat{\boldsymbol\mu}(t))$ while forcing each arm to be drawn about $\sqrt t$ times: C-Tracking tracks the cumulated sum of projections of $w^*(\hat{\boldsymbol\mu}(s))$ onto $\Sigma^{\epsilon_s}_K=\{w\in\Sigma_K: w_a\ge\epsilon_s\}$, $\epsilon_s=(K^2+s)^{-1/2}/2$; D-Tracking draws an under-sampled arm when some $N_a(t)<\sqrt t-K/2$, and otherwise the arm maximizing $t\,w^*_a(\hat{\boldsymbol\mu}(t))-N_a(t)$;
• Chernoff's stopping rule, which stops at the first $t$ at which some arm $a$ beats every other arm $b$ in a generalized likelihood ratio test, $Z_{a,b}(t)>\beta(t,\delta)$, here with $\beta(t,\delta)=\log(r(t)/\delta)$.

Formalization targets

Goal: Theorem 14 (p. 13)

For $\alpha\in[1,e/2]$ and $r(t)=O(t^\alpha)$, Chernoff's stopping rule with $\beta(t,\delta)=\log(r(t)/\delta)$ combined with C-Tracking or D-Tracking satisfies

$$\limsup_{\delta\to0}\frac{\mathbb E_{\boldsymbol\mu}[\tau_\delta]}{\log(1/\delta)}\le\alpha\,T^*(\boldsymbol\mu)$$

for every $\boldsymbol\mu\in\mathcal S$.

Milestones

• Lemma 15 (p. 20): greedy tracking of cumulated proportions $P(k)$ keeps $\max_i|N_i(n)-P_i(n)|\le K-1$.
• Lemma 7 (p. 7): C-Tracking ensures $N_a(t)\ge\sqrt{t+K^2}-2K$ and $\max_a|N_a(t)-\sum_{s<t}w^*_a(\hat{\boldsymbol\mu}(s))|\le K(1+\sqrt t)$.
• Lemma 8 (p. 7): D-Tracking ensures $N_a(t)\ge(\sqrt t-K/2)_+-1$, and proportions within $3(K-1)\epsilon$ of $w^*(\boldsymbol\mu)$ after a time $t_\epsilon$ that does not depend on the trajectory, once the plug-in targets are within $\epsilon$.
• Proposition 9 (p. 8): under either rule, $N_a(t)/t\to w^*_a(\boldsymbol\mu)$ almost surely.
• Lemma 18 (p. 27): an explicit $x$ with $c_1x\ge\log(c_2x^\alpha)$ for $\alpha\in[1,e/2]$.
• Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to $w^*$, $\tau_\delta<\infty$ almost surely and $\limsup_{\delta\to0}\tau_\delta/\log(1/\delta)\le\alpha T^*(\boldsymbol\mu)$ almost surely.

Significance

Theorem 1 of the same paper shows $\mathbb E_{\boldsymbol\mu}[\tau_\delta]\ge T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ for every $\delta$-PAC strategy, and $\mathrm{kl}(\delta,1-\delta)\sim\log(1/\delta)$. Theorem 14 with $\alpha=1$ therefore shows that the lower bound is attained: $T^*(\boldsymbol\mu)$ is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.

The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.

Difficulty

The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of $\tau_\delta/\log(1/\delta)$ does not control $\mathbb E[\tau_\delta]$, because on the rare events where the empirical means are far from $\boldsymbol\mu$ the stopping time may be very large. Theorem 14 needs a quantitative concentration of $\hat{\boldsymbol\mu}(t)$ on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the $\sqrt t$ lower bounds on $N_a(t)$ (the concentration step of App. D, Lemmas 19–20).

A second obstacle is the regularity of $w^*$: the tracking lemmas only transfer convergence of $\hat{\boldsymbol\mu}(t)$ to convergence of $N_a(t)/t$ through the continuity of $\boldsymbol\mu\mapsto w^*(\boldsymbol\mu)$ on $\mathcal S$, proved from the characterization of $w^*$ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near $\boldsymbol\mu$, which requires the empirical means to lie in the interior of the mean space.

Formalization scope

• Model. The exponential family is a structure $(\xi,\Theta,b)$ with $\Theta$ a nonempty open interval, each $\nu_\theta$ normalized, $b$ twice continuously differentiable and $\ddot b>0$ on $\Theta$. Openness and $\ddot b>0$ are added to the paper's "convex, twice differentiable"; strict convexity is what makes $\nu^\mu$ unique. Bandit models are parameter vectors $\theta\in\Theta^K$ with $K\ge2$; arms are indexed $0,\dots,K-1$. $\mathcal S$ is the set of parameter vectors with a unique arm of largest mean $\dot b(\theta_a)$.
• Protocol. Policies, the trajectory law $\mathbb P_{\boldsymbol\mu}$, pull counts, empirical means and $T^*(\boldsymbol\mu)$ are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). $T^*$ uses Kullback–Leibler divergences of the arm laws over the class $\mathcal S$ and takes values in $[0,\infty]$. Trajectory coordinate $t$ is round $t+1$. An arm never drawn has empirical mean $0$.
• Target map. $w^*(\hat{\boldsymbol\mu}(t))$ is undefined in the paper when $\hat{\boldsymbol\mu}(t)\notin\mathcal S$ (an unsampled arm, ties, a mean outside $\dot b(\Theta)$). Every tracking statement quantifies over every target map with values in $\Sigma_K$ that returns optimal proportions on $\mathcal S$, over every choice of $L^\infty$ projections, and over every tie-breaking, including randomized ones.
• Stopping rule. The two maxima in $Z_{a,b}(t)$ are suprema over $\Theta$ in the extended reals. $Z_{a,b}(t)>\beta$ is written without subtracting infinities. The stopping time is the first $t\ge1$ at which the test succeeds, $+\infty$ if none. "$r(t)=O(t^\alpha)$" is $r(t)\le Dt^\alpha$ for $t\ge1$; $r>0$ is added so that $\log(r(t)/\delta)$ is defined.
• Values in $[0,\infty]$. Expectations of $\tau_\delta$, the ratios and $T^*$ live in $[0,\infty]$. No statement converts them to reals, so an infinite expected stopping time is never read as $0$.
• Corrections, disclosed. Proposition 9's printed $\mathbb P_w$ is $\mathbb P_{\boldsymbol\mu}$. Lemma 18 adds $c_2/c_1^\alpha>1$ and $x>0$, without which its expressions are undefined.
• Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
• Welcome contributions. Exponential-family facts ($\dot b$ is the mean, the KL formula, concentration of empirical means); the continuity of $w^*$ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
• H. Chernoff, Sequential Design of Experiments, Ann. Math. Statist. 30(3), 1959. doi:10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 33. doi:10.1017/9781108571401

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$. Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$, each of capacity $Q>0$. Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$. A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$.

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP($\mathcal P$) minimizes $c(\mathbf R)$ over route sets such that

$$\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .$$

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$, the demand estimator of the paper's Eq. (2) is

$$d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .$$

The problem 2VF($\mathcal P$) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

$$\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .$$

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$.

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$-a.s. for all $\mathbb P\in\mathcal P$, and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

$$\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}$$

Milestones

1. The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
2. Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$.
3. Example 1: an instance with two customers where a route set is RVRP($\mathcal P$)-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$, since $d_{\mathcal P}(\{1,2\})\ge3$.
4. Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
5. Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$, must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$.

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

• $Q>0$, because (2) divides by $Q$;
• boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$.

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$. 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$. A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$, is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

• S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
• F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

Motivation

The capacitated vehicle routing problem (CVRP) asks for a set of minimum-cost routes by which a fleet of identical vehicles of capacity $Q$, based at a depot, serves every customer exactly once without any vehicle carrying more than its capacity. In practice customer demands are not known when routes are planned. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust CVRP: the demand vector $\tilde{\boldsymbol q}$ is random, its distribution is known only to lie in an ambiguity set $\mathcal P$, and every route must respect its capacity with probability at least $1-\epsilon$ under every distribution in $\mathcal P$.

Exact CVRP solvers rely on compact two-index vehicle flow formulations strengthened by rounded capacity inequalities, which bound from below the number of vehicles entering any customer subset $S$ by a demand estimator $d(S)$. The paper shows (its Theorem 1) that the robust two-index formulation is exact whenever the demand estimator is subadditive and demands are nonnegative, and that this fails for some natural ambiguity sets: sets that fix the marginal distribution of each customer's demand violate it (Example 1). This mission formalizes the paper's positive result for the most widely used class of ambiguity sets, the moment ambiguity sets of distributionally robust optimization (see El Ghaoui et al. 2003, Delage and Ye 2010, Wiesemann et al. 2014).

Setting

There are $n$ customers, indexed $i=1,\dots,n$; the demand vector is $\tilde{\boldsymbol q}\in\mathbb R^n$. Fix

• a rectangular support $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$;
• a mean vector $\boldsymbol\mu\in\mathbb R^n$;
• a dispersion measure $\boldsymbol\varphi=(\varphi_1,\dots,\varphi_p):\mathbb R^n\to\mathbb R^p$ (for example mean absolute deviations $|q_i-\mu_i|$, variances $(q_i-\mu_i)^2$ or Huber losses) and bounds $\boldsymbol\sigma\in\mathbb R^p$.

The moment ambiguity set is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P(\tilde{\boldsymbol q}\in\mathcal Q)=1,\ \ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \ \mathbb E_{\mathbb P}[\boldsymbol\varphi(\tilde{\boldsymbol q})]\le\boldsymbol\sigma\Big\},$$

where $\mathcal P_0(\mathbb R^n)$ denotes all probability distributions on $\mathbb R^n$. The paper's standing assumptions are $\boldsymbol\mu\in\operatorname{int}\mathcal Q$, each $\varphi_l$ closed and convex, and $\boldsymbol\varphi(\boldsymbol\mu)<\boldsymbol\sigma$.

For a distribution $\mathbb P$ the value-at-risk of a random variable is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$, with risk level $\epsilon\in(0,1)$. The worst-case value-at-risk of a customer subset $S$ is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$, and the demand estimator (2) is

$$d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .$$

The Lean development names these momentAmbiguitySet qlo qhi μ φ σ, worstCaseVaR, demandEstimator and twoPointMeasure in the namespace DRCVRP.Moment.

Formalization targets

Goal: Theorem 2 (p. 723)

For every moment ambiguity set satisfying the standing assumptions, every $\epsilon\in(0,1)$ and every $Q>0$,

$$d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)\qquad\text{for all customer subsets } S,T .$$

This is condition (S) of the paper, stated for the rounded estimator (2) and for all pairs of subsets, overlapping or empty ones included.

Milestone: Proposition 1 (p. 723)

For every customer subset $S$ there are two-point distributions $\mathbb P^t=p_1^t\delta_{\boldsymbol q_1^t}+p_2^t\delta_{\boldsymbol q_2^t}\in\mathcal P$ with $p_1^t,p_2^t\ge0$ and $\boldsymbol q_1^t,\boldsymbol q_2^t\in\mathcal Q$ such that

$$\mathbb P^t\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\longrightarrow\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\qquad(t\to\infty).$$

Significance

Combined with the paper's Theorem 1, Theorem 2 says that for every moment ambiguity set with nonnegative demands the robust CVRP can be solved through the compact two-index formulation with robust rounded capacity inequalities, i.e. by the branch-and-cut machinery of the deterministic CVRP. It also separates moment ambiguity sets from ambiguity sets built from marginal histograms, hypothesis tests, $\phi$-divergences or Wasserstein balls, whose estimators can violate subadditivity. Proposition 1 describes the worst case: however many moment constraints the set contains, two demand scenarios suffice to approach the worst-case value-at-risk, strengthening the Richter–Rogosinski theorem for this functional.

Both results are proved in the paper's online supplement. They have not, to the best of current knowledge, been machine checked. This mission produces a checked statement and proof of both, together with a reusable encoding of moment ambiguity sets and of the worst-case value-at-risk over them. The companion missions of the series formalize the equivalence theorem (I) and the explicit worst-case VaR formulas for marginalized (III), first-order (IV) and covariance (V) ambiguity sets.

Difficulty

Value-at-risk is not subadditive for a single distribution, so the obvious route, subadditivity of the worst-case VaR followed by $\lceil a+b\rceil\le\lceil a\rceil+\lceil b\rceil$, needs an argument specific to the moment set; for the marginal-histogram set of Example 1 the worst-case VaR itself fails to be subadditive. The supremum over $\mathcal P$ ranges over an infinite-dimensional set of distributions and is in general not attained, so an argument that picks a maximizer does not apply, and the classical finite-support reduction (Richter–Rogosinski) yields a number of support points that grows with the number of moment constraints, not two. The integer rounding and the $\max\{\cdot,1\}$ must also be handled for all pairs of subsets, including overlapping ones.

Formalization scope

Customers are Fin n (0-based) and customer subsets are Finset (Fin n). Distributions are measures on Fin n → ℝ; membership in the moment set requires a probability measure giving mass one to the closed box Set.Icc qlo qhi, integrable coordinates with ∫ q, q i ∂P = μ i (an equality), and integrable φ l with ∫ q, φ l q ∂P ≤ σ l. The integrability clauses hold automatically under the standing assumptions and do not shrink the set. The dispersion measure is an arbitrary real-valued function whose components are convex (convex real functions on $\mathbb R^n$ are continuous, which covers "closed"); $p=0$ is allowed. The value-at-risk is the published platform definition MultistageStochastic.valueAtRisk at level $1-\epsilon$. The worst-case VaR is a real sSup; over a moment set satisfying the standing assumptions the set of VaRs is nonempty (the Dirac measure at $\boldsymbol\mu$ belongs to $\mathcal P$) and bounded by the box, so this is the true supremum. The estimator is integer valued. Every standing assumption is a hypothesis of both theorems.

Neither statement can be satisfied trivially: the goal is about the rounded estimator of the true supremum over a nonempty set, not about subadditivity of an arbitrary set function, and the milestone requires the two-point laws to lie in $\mathcal P$ and their VaRs to converge to the supremum, not to be attained. Extended-valued dispersion measures, such as the one expressing the covariance set of §5.2 as an instance of (4), are outside the scope of the real-valued encoding.

A complete development needs basic facts about quantiles of finitely supported measures, the structure of the moment set, and a duality or construction argument for the worst-case VaR. Lemmas about value-at-risk of two-point laws and about moment sets are reusable across the series. Proofs of the milestone, of the goal, and of intermediate lemmas are welcome.

Selected references

• S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• 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, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973433

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

Motivation

The capacitated vehicle routing problem (CVRP) assigns customers to a fleet of $m$ identical vehicles of capacity $Q$ and orders each vehicle's visits so as to minimize transportation cost, subject to each vehicle's total load not exceeding $Q$. In practice the customers' demands are not known when the routes are planned. Two classical responses are the robust CVRP, which requires feasibility for every demand vector in an uncertainty set, and the chance-constrained CVRP, which requires each capacity constraint to hold with probability at least $1-\epsilon$ under a known demand distribution. The first ignores all distributional information; the second assumes a distribution that is rarely known and usually requires independent demands.

Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP, RVRP($\mathcal P$), in which each capacity constraint must hold with probability at least $1-\epsilon$ under every distribution of an ambiguity set $\mathcal P$. Whether this problem can be solved with existing CVRP technology depends on how the worst-case value-at-risk of a customer set's total demand behaves as a set function. This mission formalizes §4 of the paper, which treats ambiguity sets that only constrain each customer's demand separately.

Setting

There are $n$ customers $V_C=\{1,\dots,n\}$ with random demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ and a risk level $\epsilon\in(0,1)$. For a probability distribution $\mathbb P$ and a real random variable $\tilde X$, the value-at-risk is

$$\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\ \mathbb P[\tilde X\le x]\ge1-\epsilon\}.$$

For an ambiguity set $\mathcal P$ and a customer subset $S$, the worst-case value-at-risk of $S$ is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$.

Fix a support box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, and for each customer $i$ a componentwise convex dispersion measure $\boldsymbol\varphi_i:\mathbb R\to\mathbb R^{p_i}$ with bound $\boldsymbol\sigma_i>\boldsymbol\varphi_i(\mu_i)$. The marginalized moment ambiguity set (5) is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P(\tilde{\boldsymbol q}\in\mathcal Q)=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}[\boldsymbol\varphi_i(\tilde q_i)]\le\boldsymbol\sigma_i\ \forall i\in V_C\Big\}.$$

It constrains marginal moments only, and so contains joint distributions of every dependence structure, from independent to perfectly correlated demands. Three special cases have their own closed forms: the first-order set (6), where $\sigma_i>0$ bounds the mean absolute deviation $\mathbb E|\tilde q_i-\mu_i|$; the variance set (8), where $\sigma_i>0$ bounds $\mathbb E(\tilde q_i-\mu_i)^2$; and the semivariance set (10), where $\sigma_i^+,\sigma_i^->0$ bound $\mathbb E[\tilde q_i-\mu_i]_+^2$ and $\mathbb E[\mu_i-\tilde q_i]_+^2$.

A route set $\mathbf R=(R_1,\dots,R_m)\in\mathfrak P(V_C,m)$ partitions the customers into $m$ nonempty ordered routes. It is feasible in RVRP($\mathcal P$) if $\mathbb P[\sum_{i\in R_k}\tilde q_i\le Q]\ge1-\epsilon$ for all $\mathbb P\in\mathcal P$ and all $k$, and feasible in the deterministic CVRP with demands $\boldsymbol q$ if $\sum_{i\in R_k}q_i\le Q$ for all $k$.

Formalization targets

Goal: Theorem 3 (p. 723)

For every marginalized moment ambiguity set (5) and every nonempty $S\subseteq V_C$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]=\sum_{i\in S}\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i].$$

The dispersion measures are left arbitrary (convex, componentwise, any number of components), so the goal covers every set of the form (5).

Milestones

• Proposition 2 (p. 724, Eq. (7)), first-order sets: $\sup_{\mathbb P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i]=\mu_i+\min\{\overline q_i-\mu_i,\frac{1-\epsilon}{\epsilon}(\mu_i-\underline q_i),\frac1{2\epsilon}\sigma_i\}$.
• Proposition 3 (p. 725, Eq. (9)), variance sets: the same with last term $\sqrt{\frac{1-\epsilon}{\epsilon}\sigma_i}$.
• Proposition 4 (p. 725, Eq. (11)), semivariance sets: the four-term minimum with $\sqrt{\sigma_i^+/\epsilon}$ and $\sqrt{(1-\epsilon)\sigma_i^-}/\epsilon$.
• Corollary 1 (p. 723): a route set is feasible in RVRP($\mathcal P$) over (5) if and only if it is feasible in the deterministic CVRP with demands $q_i=\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i]$.

Significance

Theorem 3 says that over (5) the worst case of a sum is the sum of the worst cases. Because the value-at-risk is not additive for a fixed distribution, and the online supplement exhibits distributions in such a set for which the individual values-at-risk are not additive, the statement is about the ambiguity set, not about any of its members. Its consequence, Corollary 1, is that RVRP($\mathcal P$) over (5) is a deterministic CVRP with inflated demands, so existing branch-and-cut and branch-and-cut-and-price codes solve it unchanged. Propositions 2–4 make those inflated demands explicit for three standard dispersion measures, so that the whole reduction is in closed form. The corollary also exposes a limitation: under (5) the worst-case distribution does not depend on the route set, and the model cannot represent known dependencies between customers.

The results are proved in the paper's online supplement; none has a machine-checked proof. A formalization produces a checked worst-case value-at-risk calculus over moment sets with support constraints, including sharp one-sided Chebyshev-type bounds under mean-absolute-deviation, variance and semivariance constraints, which are reusable in distributionally robust optimization beyond vehicle routing.

Difficulty

The value-at-risk is neither subadditive nor superadditive in general, so neither inequality of Theorem 3 follows from properties of a single distribution. The inequality "$\ge$" requires combining near-worst-case distributions of the individual customers into one joint distribution in $\mathcal P$ that is simultaneously near-worst for the sum; the inequality "$\le$" requires bounding the value-at-risk of the sum for an arbitrary joint law using only marginal information. In Propositions 2–4 the supremum is typically not attained: the distribution concentrating mass at the claimed worst-case value violates the mean constraint, and the value is reached only as a limit of distributions in $\mathcal P$. An argument that exhibits a single maximizer therefore fails, and the statements must be proved as equalities of suprema.

Formalization scope

Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. An ambiguity set is a set of measures on Fin n → ℝ, each required to be a probability measure; the support condition is P (Set.Icc qlo qhi) = 1 and expectations are Bochner integrals. The sets are sets of joint laws on $\mathbb R^n$, never products of marginals. In (5) each expectation $\mathbb E_{\mathbb P}[\varphi_{i,l}(\tilde q_i)]$ is required to exist; this is automatic for convex $\varphi_{i,l}$ on the bounded support. The value-at-risk is the published definition MultistageStochastic.valueAtRisk P Y (1 - ε), and the worst-case value-at-risk is the real supremum of its values over the ambiguity set; under the standing assumptions that set of values is nonempty (the Dirac law at $\boldsymbol\mu$ belongs to $\mathcal P$) and bounded (by the support), so the supremum is not a default value. The single-customer quantity is the case $S=\{i\}$. The standing assumptions ($\underline{\boldsymbol q}\ge\mathbf 0$, $\underline{\boldsymbol q}<\boldsymbol\mu<\overline{\boldsymbol q}$, convexity of $\varphi_{i,l}$, $\varphi_{i,l}(\mu_i)<\sigma_{i,l}$, $\boldsymbol\sigma,\boldsymbol\sigma^\pm>\mathbf 0$, $0<\epsilon<1$) are explicit hypotheses. Routes are lists of customers; a route set has nonempty routes whose concatenation is a permutation of all customers. Costs are not formalized, since both routing problems minimize the same cost over their feasible route sets.

All targets are equalities or equivalences; a one-sided inequality, a statement asserting that some distribution attains the value, or a formulation over product measures is a different theorem and does not count.

Contributions welcome: the reduction of the chance constraint to a value-at-risk bound, the right-continuity lemmas for the value-at-risk of a measure on $\mathbb R^n$, two-point constructions in the ambiguity sets, and one-sided Chebyshev-type bounds with support constraints.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Laporte, Y. Nobert and M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
• G. Casella and R. L. Berger, Statistical Inference, 2nd ed., Duxbury, 2002.

Motivation

Mission 32-ch09b-networkflows established the potential and negative-cycle optimality criteria for M-convex submodular flow problems. This mission finishes chapter 9 with the two topics that close it out: the constructive engine behind the negative-cycle criterion — cycle cancellation, which actually improves a nonoptimal flow rather than merely detecting suboptimality, resting on a delicate "unique-min condition" for bipartite matchings — and network duality, the chapter's capstone structural theorem showing that M-convexity and L-convexity are preserved (and their conjugacy is preserved) under transformation by an arbitrary network.

Setting

For a feasible integer flow ξ in the M-convex submodular flow problem MSFP2, a negative cycle in the auxiliary network (Gξ,ℓξ) witnesses suboptimality (mission 32's Theorem 9.20); cycle cancellation modifies ξ along a smallest such cycle to produce a strictly better flow ξ̄ (Eq. (9.75)). The unique-min condition for a pair (x,y) of integer vectors with ‖x-y‖∞=1 asks whether the bipartite graph G(x,y) — vertices the positive/negative supports of x-y, weights the M-convex exchange values Δf(x;v,u) — has a unique minimum-weight perfect matching; when it does, the M-convex exchange inequality of Proposition 6.25 becomes an equality. Separately, a network G=(V,A;S,T) with entrance set S and exit set T transforms a pair of functions f,g on Zˢ into induced functions f̃,g̃ on Zᵀ (Eqs. (9.81)-(9.82)), the minimum cost to meet a boundary specification at the exit given a production cost at the entrance and a transportation cost along arcs.

Formalization targets

Goal: Network duality for Z→Z functions (Theorem 9.26)

M-(resp. M$^\natural$-)convexity and integer-valuedness of f transfer to the induced f̃; L-(resp. L$^\natural$-)convexity and integer-valuedness of g transfer to g̃; and if f is M$^\natural$-convex, g is its L$^\natural$-conjugate, and each arc cost ga is the conjugate of fa, then g̃ is the conjugate of f̃. Chosen as goal: the book calls this "the harmonious relationship between network flow and M-/L-convexity", its own proof runs roughly six pages (the longest argument in this chunk), and it is the general fact from which Theorems 9.27-9.28 (analogues for other type combinations) and Notes 9.29-9.30 (the aggregation and infimal- convolution closure properties of M-convex functions, already placed in mission 22-ch06b-mconvexfunctions's own Theorem 6.13) all descend.

Supporting structural targets

Theorem 9.22 shows cycle cancellation strictly improves the objective; Propositions 9.23-9.25 are "the key ingredient" behind it: Proposition 9.23 shows the unique-min condition upgrades the M-convex exchange inequality to an equality, Proposition 9.24 gives a checkable characterization of when a bipartite weighted graph has a unique minimum-weight perfect matching, and Proposition 9.25 is the fact that makes the machine run — the specific pair (∂ξ,∂ξ̄) arising from cycle cancellation always satisfies the unique-min condition. Theorems 9.27 and 9.28 are the network duality theorem's own analogues for Z→R and R→R functions, the second restoring the conjugacy assertion (missing for Z→R) via the ordinary real Legendre-Fenchel transform.

Significance

Cycle cancellation is this book's constructive answer to the negative-cycle criterion: not just a certificate of suboptimality, but an actual improvement step, the combinatorial core of the cycle-canceling algorithm explained in section 10.4.3 (mission 35-ch10c-algorithms). Its correctness proof is one of the most intricate combinatorial arguments in the entire book — a proof by contradiction using a multiset-union identity (Eq. (9.80)) to derive a smaller negative cycle from an assumed non-uniqueness, itself resting on Proposition 9.24's Monge-like characterization of unique bipartite matchings. Network duality, meanwhile, is the theorem that explains why discrete convex analysis and network flow theory are so tightly intertwined throughout this book: it is the general mechanism (matroid induction, min-max relations, the M-convex aggregation and infimal-convolution closure properties) underlying nearly every construction chapter 2 introduced informally and chapter 6 proved piecemeal.

None of these results are open — they are Murota's own account of cycle cancellation (section 9.5.2) and network duality (section 9.6). What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 9 begun in missions 12-network-flows and 32-ch09b-networkflows; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Theorem 9.26's own proof needs the full weight of everything chapter 9 has built (Theorem 9.16's potential criterion for integer flows, the conjugacy theorem of chapter 8), which this mission does not re-prove (proofs are sorry throughout, per this pass's scope) but whose statement still needs the induced-function machinery built faithfully: since the general framework's optimal-value-type quantities can genuinely be -∞ (the book's own blanket hypothesis f̃ > -∞ acknowledges this), InducedFTilde/InducedGTilde are EReal-valued, following the same soundness discipline established in mission 31-ch08d-conjugacyduality for Lagrangian duality's derived quantities.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions. Functions "on Zˢ" for S a proper subset of the ground set are represented as ordinary V→Z functions required to vanish outside S (SupportedOn), rather than as functions on a dependent subset type — a padding-with-zero encoding consistent with this whole series' preference for a single ambient ground-set domain. C[R→R] (univariate real polyhedral convex functions, needed only for Theorem 9.28's arc costs) is formalized as ordinary midpoint-style convexity (IsConvexUnivariateR) rather than the book's own polyhedral characterization, since polyhedrality plays no role in Theorem 9.28's conclusion beyond ensuring the induced functions are well-behaved. All seven numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 9.25 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Valuated matroid intersection," SIAM Journal on Discrete Mathematics, 9 (1996), pp. 545-561 [135] (the unique-max lemma Proposition 9.23 reformulates, and the proof technique behind Proposition 9.25).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (network duality and cycle cancellation for the M-convex submodular flow problem).

Motivation

In the capacitated vehicle routing problem (CVRP) a depot serves customers $V_C=\{1,\dots,n\}$ with $m$ vehicles of capacity $Q$, and every route must respect the capacity. When customer demands are uncertain, the distributionally robust chance-constrained CVRP of Ghosal and Wiesemann (Oper. Res. 68(3), 2020) requires every route to meet its capacity with probability at least $1-\epsilon$ under every distribution in an ambiguity set $\mathcal P$, a family of distributions consistent with what is known about the demands. Such constraints are handled in a branch-and-cut scheme through rounded capacity inequalities, whose right-hand sides require one quantity for each customer subset $S$: the worst-case value-at-risk of the cumulative demand of $S$.

For ambiguity sets that describe each customer separately (marginal moment sets), this quantity is additive over customers and the problem reduces to a deterministic CVRP. Such sets cannot express that the demands of customers in the same municipality, county or state vary jointly within limits. The first-order generic moment ambiguity set does express this: it bounds the mean absolute deviation of the cumulative demand of prescribed customer groups. The mean absolute deviation is a standard robust dispersion measure, less sensitive to outliers than the standard deviation (see Casella and Berger, Statistical Inference, 2002). This mission formalizes the paper's description of the worst-case value-at-risk over such sets.

Setting

Demands form a random vector $\tilde{\boldsymbol q}$ on $\mathbb R^n$. The data are a support box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, customer subsets $S_1,\dots,S_p\subseteq V_C$ and bounds $\boldsymbol\nu>\mathbf 0$. For $A\subseteq V_C$, $\mathbf 1_A\in\{0,1\}^n$ is its indicator vector. The first-order generic moment ambiguity set, Eq. (12) of the paper, is

$$\mathcal P=\Bigl\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P[\tilde{\boldsymbol q}\in\mathcal Q]=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}\bigl[\mathbf 1_{S_i}^\top|\tilde{\boldsymbol q}-\boldsymbol\mu|\bigr]\le\nu_i\ \ \forall i=1,\dots,p\Bigr\},$$

where $\mathcal P_0(\mathbb R^n)$ is the set of probability distributions on $\mathbb R^n$ and $|\cdot|$ acts componentwise. The subsets are arbitrary: they may overlap and need not cover $V_C$.

For a risk level $\epsilon\in(0,1)$ and a random variable $\tilde X$, the value-at-risk is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$. For a customer subset $S$ the quantity of interest is

$$\sup_{\mathbb P\in\mathcal P}\ \mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr].$$

Write $\hat{\boldsymbol q}=\min\{\overline{\boldsymbol q}-\boldsymbol\mu,\ \frac{1-\epsilon}{\epsilon}(\boldsymbol\mu-\underline{\boldsymbol q})\}$ (componentwise) and $[\cdot]_+$ for the componentwise positive part. A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)$ partitions $V_C$ into $m$ nonempty ordered routes. It is feasible in the deterministic CVRP with demands $\boldsymbol q$ if $\sum_{i\in\mathbf R_k}q_i\le Q$ for all $k$, and feasible in the distributionally robust CVRP if $\mathbb P[\sum_{i\in\mathbf R_k}\tilde q_i\le Q]\ge1-\epsilon$ for all $\mathbb P\in\mathcal P$ and all $k$.

Formalization targets

Goal: Theorem 5 (p. 726)

For every customer subset $S$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\inf_{\boldsymbol\gamma\in\mathbb R^p_+}\ \mathbf 1_S^\top\boldsymbol\mu+\hat{\boldsymbol q}^\top\Bigl[\mathbf 1_S-2\sum_{i=1}^p\gamma_i\mathbf 1_{S_i}\Bigr]_+ +\frac1\epsilon\boldsymbol\nu^\top\boldsymbol\gamma .$$

The right-hand side is the optimal value of the paper's problem (13). The statement holds for every family of subsets and all data satisfying the standing assumptions, so it is the general form of which the milestones are special cases.

Corollary 2 (p. 726, Eq. (14))

If $S_1,\dots,S_{p-1}$ are pairwise disjoint and cover $V_C$ and $S_p=V_C$, then

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\mathbf 1_S^\top\boldsymbol\mu+\min\Bigl\{\frac{\nu_p}{2\epsilon},\ \sum_{i=1}^{p-1}\min\Bigl\{\mathbf 1_{S\cap S_i}^\top\hat{\boldsymbol q},\ \frac{\nu_i}{2\epsilon}\Bigr\}\Bigr\}.$$

Corollary 3 (pp. 726–727, Eq. (15))

If $p=n+1$, $S_i=\{i\}$ for $i\le n$ and $S_{n+1}=V_C$, then

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\mathbf 1_S^\top\boldsymbol\mu+\min\Bigl\{\frac{\nu_{n+1}}{2\epsilon},\ \sum_{i\in S}\min\Bigl\{\hat q_i,\ \frac{\nu_i}{2\epsilon}\Bigr\}\Bigr\}.$$

Theorem 4 (p. 726)

For some instance with an ambiguity set of the form (12), no deterministic CVRP instance on the same customers and vehicles (capacity $Q'\ge0$, demands $\boldsymbol q'\ge\mathbf 0$) has the same set of feasible route sets.

Significance

Theorem 5 makes the worst-case value-at-risk over (12) computable in polynomial time as the value of a nonsmooth convex problem over the nonnegative orthant, which the paper notes can be written as a linear program. This gives the right-hand sides of the rounded capacity inequalities in a branch-and-cut scheme for the distributionally robust CVRP. Corollaries 2 and 3 give closed forms for two structured families of groups, evaluable in time linear in $|S|$. Theorem 4 shows the gain in modelling power has a cost: unlike the marginal case, the problem cannot in general be replaced by a deterministic CVRP with altered demands. With a single customer and $S_1=\{1\}$, Theorem 5 reduces to the closed form $\mu+\min\{\hat q,\nu/(2\epsilon)\}$ for marginalized first-order sets, so it extends that single-customer formula to joint dispersion constraints.

All four results are proved in the paper's online supplement. As far as a platform search shows, none has been machine-checked. The mission produces checked proofs of the equality in Theorem 5, the two closed forms, and an explicit instance for Theorem 4.

Difficulty

The supremum ranges over an infinite-dimensional set of joint distributions, and the value-at-risk is neither convex nor concave in the distribution. Bounding the value-at-risk of each group separately and adding the bounds does not work when groups overlap, and it ignores the total-dispersion constraint. It gives only an upper bound, and in the setting of Corollary 2 that bound is strict whenever the total bound $\nu_p/(2\epsilon)$ is the binding term. Showing that the infimum in (13) is attained in the limit needs distributions that saturate several overlapping dispersion constraints at once while keeping the mean fixed and the support inside the box. For Theorem 4, the witness must separate the feasible-route-set family of the robust instance from every family defined by a single linear capacity inequality with nonnegative weights.

Formalization scope

Customers are Fin n (0-based), subsets are Sfam : Fin p → Finset (Fin n), and a distribution is a Measure (Fin n → ℝ) that is required to be a probability measure. Support is P (Set.Icc qlo qhi) = 1, the mean condition is ∫ q, q j ∂P = μ j, and the dispersion condition is ∫ q, ∑ j ∈ Sfam l, |q j - μ j| ∂P ≤ ν l. The integrability clauses stated alongside are automatic for measures carried by the box. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is the real sSup of its image over the set; under the standing assumptions this image is nonempty (the Dirac at $\boldsymbol\mu$ lies in the set) and bounded (bounded support), so the real supremum is the paper's. The optimal value of (13) is the real sInf of the objective over $\{\boldsymbol\gamma\ge\mathbf 0\}$, a nonempty set on which the objective is bounded below by $\mathbf 1_S^\top\boldsymbol\mu$. Attainment is not claimed. All statements carry the standing assumptions $\underline{\boldsymbol q}\ge\mathbf 0$, $\underline{\boldsymbol q}<\boldsymbol\mu<\overline{\boldsymbol q}$, $\boldsymbol\nu>\mathbf 0$ and $0<\epsilon<1$. Corollary 2 writes $p=r+1$ with the last subset Sfam (Fin.last r). Corollary 3 indexes the singleton of customer $i$ by Fin.castSucc i. In Theorem 4 route sets are Fin m → List (Fin n) and only feasibility is modelled; costs play no role.

The theorems are not trivialized by an empty ambiguity set or a junk supremum: membership of the Dirac distribution at $\boldsymbol\mu$ is checked locally with a sorry-free proof. Theorem 4 needs a genuinely separating instance: an instance in which no route set is robustly feasible, for example, is matched by a deterministic instance in which none is feasible either.

Needed infrastructure: two-point and finitely supported distributions on $\mathbb R^n$ and their value-at-risk; weak duality for moment problems over the box; the positive-part calculus of (13). The value-at-risk lemmas for finitely supported measures are reusable in the sibling missions on this paper. Contributions of any of the milestones, of lemmas for these building blocks, or of either inequality of Theorem 5 on its own are welcome.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Casella and R. L. Berger, Statistical Inference, 2nd ed., Duxbury, 2002.
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• G. Laporte, Y. Nobert and M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050

Motivation

Chapters 6 through 9 characterized minimality for M-convex functions structurally (the M-optimality criterion, Theorem 6.26: a point is a global minimizer iff no local swap improves it) without saying how to find one. Chapter 10 turns that structural fact into an algorithm: the local characterization is the termination test of the simplest possible minimization procedure, steepest descent by coordinate swaps. This mission formalizes that algorithm and its two complexity bounds, plus a structural min-max identity for submodular base polyhedra that the chapter's heavier submodular-minimization algorithms build on. It is the first mission in this series whose goal names a method, not just a property of a class of functions — formalizing it faithfully means giving the algorithm itself a Lean representation that the complexity theorem then quantifies over, not just describing its output.

Setting

Let $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ be an M-convex function (MExchangeAxiom, chunk 06), $n = |V|$. The steepest descent algorithm repeatedly replaces the current point $x$ by $x - \chi_u + \chi_v$ for a pair $u \ne v$ minimizing $f(x - \chi_u + \chi_v)$, stopping when no such swap improves on $f(x)$ — at which point, by the M-optimality criterion, $x$ is a global minimizer. This mission represents a run of the algorithm as a sequence $x : \mathbb N \to \mathbb Z^V$ satisfying these step and termination relations directly, so that "the number of iterations" is a genuine property of any such run, not an informal gloss. Separately, for a submodular set function $\rho : 2^V \to \mathbb R$ (chunk 04's SubmodularSetFunction), the base polyhedron $B(\rho)$ (chunk 04's BasePolyhedron) is the polytope $\{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$.

Formalization targets

Goal: Proposition 10.2 (iteration bound with tie-breaking)

For an M-convex function $f$ with finite $\ell^1$-diameter $K_1 = \max\{\|x-y\|_1 : x,y \in \operatorname{dom} f\}$ (Eq. (10.1)), the number of iterations in the steepest descent algorithm using the tie-breaking rule (10.2) — a fixed lexicographic rule for choosing among tied steepest pairs, based on an arbitrary but fixed ordering $\varphi$ of $V$ — is bounded by $K_1/2$.

Milestones: Proposition 10.1, Proposition 10.8

Proposition 10.1: an unconditional warm-up — if $f$ has a unique minimizer $x^*$, any run of the plain (untied) algorithm from $x^0$ terminates within $\|x^0 - x^*\|_1/2$ iterations, with no tie-breaking rule needed. Proposition 10.8: a structural min-max identity, $\max\{x^-(V) : x \in B(\rho)\} = \min\{\rho(X) : X \subseteq V\}$, for a submodular set function $\rho$ — chosen deliberately as a milestone that names no algorithm at all, in contrast to this mission's other two items.

Significance

The result itself. Proposition 10.2 is the complexity backbone of §10.1: it is what turns "steepest descent terminates" (an easy monotonicity observation) into a genuine polynomial bound, and it is the base case the chapter's more elaborate scaling and domain-reduction algorithms (not drafted here) improve on. Proposition 10.8, though algorithm-free, is the structural fact ("verifying membership in $B(\rho)$ seems to need a submodular minimization procedure — but demonstrating optimality of a cut $X$ only needs a base with $x^-(V) = \rho(X)$") that makes Schrijver's and the IFF algorithms' correctness proofs possible, and specializes chunk 04's Edmonds's intersection theorem to the two-function case $\rho_1 = \rho, \rho_2 = 0$.

Formalizing it. A prior-art search (q=steepest descent, q=submodular minimization, q=base polyhedron) found no existing platform items for any of this chapter's results. This mission gives the first formal statement of an M-convex minimization algorithm's complexity, and directly reuses chunk 06's MExchangeAxiom/ArgMin/CharVec/DomZ and chunk 04's SubmodularSetFunction/BasePolyhedron — genuine cross-chunk substrate reuse spanning two different chapters' worth of prior missions.

Difficulty

The chapter's own framing (quoted in BRIEF.md) is that every other chapter's theorems state a property of a class of functions or sets, while this chapter's theorems state properties of a named algorithm run on such an object. Formalizing "the number of iterations in the steepest descent algorithm is bounded by ..." faithfully means giving the algorithm's steps (S0-S3) and termination test a Lean representation that the bound then quantifies over — stating the bound about "the minimizer" alone, with the algorithm silently dropped, would misrepresent the theorem as a fact about minimizers rather than about a procedure that finds one. This mission represents a run of the algorithm as an abstract sequence satisfying the book's own step-transition relations (documented in full in MODERATION_NOTES.md), letting the complexity theorems quantify over any valid run rather than committing to one executable implementation.

A second difficulty is scope: the chapter's recommended primary goal, Proposition 10.18 (Schrijver's algorithm's complexity), needs a scaling procedure with several auxiliary data structures — a materially larger definitional undertaking than steepest descent's simple greedy-swap loop. Per BRIEF.md's own explicit fallback authorization, this mission takes Proposition 10.2 as its goal instead; see HARD.md and MODERATION_NOTES.md for the full reasoning.

Formalization scope

Runs of the algorithm are represented as x : ℕ → V → ℤ satisfying IsSteepestDescentRun (plain) or IsSteepestDescentRunTieBreak (with the tie-breaking rule) — a step relation plus a termination test, with an explicit iteration count N the theorems bound. The tie-breaking key $\Phi(u,v)$ (Eq. (10.2)) and its lexicographic order are formalized directly (a manual three-way comparison, not Mathlib's default componentwise Prod order). Both iteration bounds are stated as 2 * N ≤ k rather than N ≤ k / 2, avoiding natural-number division. Not drafted: the derived "hence ... in $O(F \cdot n^2 K_1)$ time" corollary of Proposition 10.2 (needs a cost-model primitive for "time" and "$F$" this mission does not otherwise use — the iteration-count bound itself, this proposition's genuine combinatorial content, is drafted in full); Schrijver's algorithm and everything in §10.2.2 onward; the steepest descent scaling algorithm, the domain reduction algorithm and its scaling variant (§10.1.2-10.1.3, structurally different algorithms); the quasi-M-convex extension mentioned immediately after Proposition 10.2. A trivializing formalization would state the iteration bound as an unconditional fact about "a" minimizer-finding procedure, or would drop the tie-breaking rule from Proposition 10.2 and thereby understate what the bound actually requires; neither is done.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

In the capacitated vehicle routing problem (CVRP) a fleet of $m$ vehicles of capacity $Q$ leaves a depot and serves $n$ customers; every customer is visited once, and the load of each route must not exceed $Q$. In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least $1-\epsilon$, but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set $\mathcal P$ built from the information that can actually be estimated: support, means and dispersion bounds.

Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set $S$. This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.

Setting

Customers are indexed by $i\in\{1,\dots,n\}$ and their random demand vector is $\tilde{\boldsymbol q}\in\mathbb R^n$. Fix a box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, and a symmetric positive definite matrix $\Sigma\succ0$. The covariance ambiguity set is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P[\tilde{\boldsymbol q}\in\mathcal Q]=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}\big[(\tilde{\boldsymbol q}-\boldsymbol\mu)(\tilde{\boldsymbol q}-\boldsymbol\mu)^\top\big]\preceq\Sigma\Big\},\tag{16}$$

where $\mathcal P_0(\mathbb R^n)$ is the set of all probability distributions on $\mathbb R^n$ and $A\preceq\Sigma$ means that $\Sigma-A$ is positive semidefinite.

For a distribution $\mathbb P$ and a real random variable $\tilde X$, the value-at-risk at level $1-\epsilon$, $\epsilon\in(0,1)$, is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$. For a customer set $S$, the worst-case value-at-risk is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$. A route serving $S$ satisfies the chance constraint for every $\mathbb P\in\mathcal P$ exactly when this number is at most $Q$.

Two componentwise bounds appear in the answer:

$$\boldsymbol q^\ell=\max\Big\{-\tfrac{1-\epsilon}{\epsilon}(\overline{\boldsymbol q}-\boldsymbol\mu),\ \underline{\boldsymbol q}-\boldsymbol\mu\Big\},\qquad\boldsymbol q^u=\min\Big\{\tfrac{1-\epsilon}{\epsilon}(\boldsymbol\mu-\underline{\boldsymbol q}),\ \overline{\boldsymbol q}-\boldsymbol\mu\Big\}.$$

A route set is an ordered partition of the customers into $m$ nonempty ordered routes. It is feasible in the distributionally robust problem RVRP($\mathcal P$) if every route satisfies the chance constraint for every $\mathbb P\in\mathcal P$, and feasible in a deterministic instance with capacity $Q'$ and demands $\boldsymbol q$ if every route's total demand is at most $Q'$.

Formalization targets

Goal: Theorem 7

For every customer set $S$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]=\max\Big\{\mathbf 1_S^\top\boldsymbol\mu+\mathbf 1_S^\top\boldsymbol q:\ \boldsymbol q^\top\Sigma^{-1}\boldsymbol q\le\tfrac{1-\epsilon}{\epsilon},\ \boldsymbol q\in[\boldsymbol q^\ell,\boldsymbol q^u]\Big\}.\tag{17}$$

The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.

Milestone: Corollary 4 (corrected)

For a diagonal bound $\Sigma=\operatorname{diag}(\sigma_1^2,\dots,\sigma_n^2)$, program (17) collapses to a search over one parameter $\theta\ge0$ with $S(\theta)=\{i\in S:\sigma_i^2>\theta q^u_i\}$:

$$\sup_{\theta}\ \mathbf 1_S^\top\boldsymbol\mu+\sum_{i\in S(\theta)}q^u_i+\sqrt{\Big[\tfrac{1-\epsilon}{\epsilon}-\sum_{i\in S(\theta)}\big(\tfrac{q^u_i}{\sigma_i}\big)^2\Big]\Big[\sum_{i\in S\setminus S(\theta)}\sigma_i^2\Big]},\tag{18}$$

over the $\theta$ for which the first bracket is nonnegative and the point of (17) that $\theta$ induces respects $\boldsymbol q^u$ (see Formalization scope).

Milestone: Theorem 6

For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.

Significance

Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in $|S|$ after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.

The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.

Difficulty

The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "$\ge$" requires, for every feasible $\boldsymbol q$ of (17), a sequence of distributions in (16) whose value-at-risk approaches $\mathbf 1_S^\top(\boldsymbol\mu+\boldsymbol q)$. The value-at-risk is a lower quantile, so a distribution placing mass exactly $\epsilon$ on a high point does not attain the value: the construction has to be a limit. The inequality "$\le$" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for $\sum_{i\in S}\tilde q_i$ alone ignores the box: it yields $\sqrt{\frac{1-\epsilon}{\epsilon}\mathbf 1_S^\top\Sigma\mathbf 1_S}$, which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound $\boldsymbol q^\ell$, is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.

Formalization scope

Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals $\int(q_i-\mu_i)(q_j-\mu_j)\,d\mathbb P$. The covariance bound is called Sig because Σ is Lean syntax. The side conditions $\underline{\boldsymbol q}\ge\mathbf 0$, $\boldsymbol\mu\in\operatorname{int}\mathcal Q$, $\Sigma\succ0$ (Sig.PosDef) and $0<\epsilon<1$ are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at $\boldsymbol\mu$ lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. $\Sigma^{-1}$ is Mathlib's matrix inverse.

The paper states Theorem 7 and Corollary 4 with "$\mathbb P$-VaR" without a level; the level $1-\epsilon$, used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every $\theta\ge0$ with a nonnegative bracket. For $n=1$, every large $\theta$ then gives the value $\mu_1+\sigma_1\sqrt{(1-\epsilon)/\epsilon}$, which can exceed $\overline q_1$ and hence every value-at-risk. The formal statement adds the condition that makes each $\theta$ a feasible point of (17): $\sigma_i^2\sqrt{s(\theta)}\le q^u_i\sqrt{\sum_{k\in S\setminus S(\theta)}\sigma_k^2}$ for $i\in S\setminus S(\theta)$, where $s(\theta)$ is the first bracket. With this condition the statement is the diagonal case of Theorem 7.

A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on $\sum_{i\in S}\tilde q_i$ would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives $\mathbf 1_S$, and it has no multiplier for $\boldsymbol q\ge\boldsymbol q^\ell$.

Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• E. Delage and Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• G. Laporte, Y. Nobert and M. Desrochers, Optimal Routing under Capacity and Distance Restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050