Operations Research

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

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

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

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

Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.

This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.

Setting

A network consists of a finite vertex set $V$, a set of directed edges $(x, y)$, a source $S$ and a sink $T$ with $S \ne T$, and a capacity $c(x, y) \ge 0$ (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices $x, y$ at most one of $(x, y)$, $(y, x)$ is an edge. Every edge at $S$ points away from $S$ and every edge at $T$ points into $T$.

A flow is a function $\phi$ on the edges with $0 \le \phi(x, y) \le c(x, y)$, extended by $\phi(x, y) = 0$ on pairs that are not edges, satisfying the conservation laws

$$\sum_x \phi(S, x) = \sum_x \phi(x, T), \qquad \sum_x \phi(x, y) = \sum_x \phi(y, x)\quad (y \ne S, T).$$

The value of $\phi$ is $\operatorname{value}(\phi) = \sum_x \phi(S, x)$.

A cut is a partition $V = L \cup U$ with $S \in L$, $T \in U$. Its capacity is

$$c(L, U) = \sum_{x \in L,\ y \in U} c(x, y),$$

summed over the edges directed from $L$ to $U$ only.

Given a flow $\phi$, an edge $(x, y)$ is used if $\phi(x, y) > 0$ and has spare capacity if $\phi(x, y) < c(x, y)$. An augmenting path is a sequence $P = (x_0, \dots, x_m)$ of distinct vertices from $x_0 = S$ to $x_m = T$ such that each step either follows an edge $(x_{i-1}, x_i)$ with spare capacity (a forward edge) or traverses a used edge $(x_i, x_{i-1})$ backwards (a backward edge). Its augmentation amount is $\delta = \min\{\delta_1, \delta_2\}$, where $\delta_1$ is the least spare capacity of a forward edge and $\delta_2$ the least flow on a backward edge ($\delta = \delta_1$ when there is no backward edge).

For Chapter 14: in a finite simple graph with bipartition $V = V_1 \cup V_2$, a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and $N(A)$ is the set of neighbors of the vertices in $A$.

Formalization targets

Goal: the Max Flow–Min Cut Theorem (Theorem 13.10)

For every network there is a real number $v_0$ with

$$v_0 = \max\{\operatorname{value}(\phi) : \phi \text{ a flow}\} = \min\{c(L, U) : V = L \cup U \text{ a cut}\},$$

that is, $v_0$ is attained by some flow and bounds every flow value from above, and $v_0$ is attained by some cut and bounds every cut capacity from below.

Milestones

• Theorem 13.4. For every flow $\phi$ and every cut, $\operatorname{value}(\phi) \le c(L, U)$.
• Proposition 13.7. If $P$ is an augmenting path for a flow $\phi$ of value $v$ and $\delta$ is its augmentation amount, the function obtained by adding $\delta$ on the forward edges of $P$ and subtracting $\delta$ on its backward edges is a flow of value $v + \delta$.
• Theorem 14.1. If every capacity is an integer, some maximum flow has $\phi(x, y) \in \mathbb Z$ on every edge.
• Theorem 14.7 (Hall). In a finite bipartite graph with bipartition $V_1 \cup V_2$ there is a matching saturating every vertex of $V_1$ if and only if $|N(A)| \ge |A|$ for every $A \subseteq V_1$.

Significance

The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.

Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in $(0, \infty]$, value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.

Difficulty

Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.

Formalization scope

The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes $\phi = 0$ off the edges and keeps the first conservation law as part of the definition, as on the page. The value is $\sum_x \phi(S, x)$. A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and $\delta_1, \delta_2, \delta$ are computed in WithTop ℝ so that an empty minimum is $\top$ and $\delta = \delta_1$ when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.

No explicit constants arise: the chapter has no asymptotic or approximate statements.

The book's sentence of Theorem 13.10 reads "if $v_0$ is the maximum value of a flow and $c_0$ the minimum capacity of a cut, then $v_0 = c_0$". A formalization that takes $v_0$ and $c_0$ as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.

Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapters 13–14. https://www.appliedcombinatorics.org/book/
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• U. Zwick, The smallest networks on which the Ford–Fulkerson maximum flow procedure may fail to terminate, Theoretical Computer Science 148 (1995), 165–170. https://doi.org/10.1016/0304-3975(95)00022-O

Motivation

Chunk 10 formalized the discrete conjugacy theorem — the Legendre-Fenchel transform's bijection between the classes of M-convex and L-convex functions — and, along the way, a function-level generalization of Edmonds's intersection theorem. Section 8.4 turns that machinery toward a different question: not "how are two convexity classes related," but "when does a discrete optimization problem have a dual that meets it with equality." The classical route to such strong-duality results in continuous convex programming — Lagrangian relaxation, an embedding of the problem in a family of perturbed problems, and a saddle-point characterization of when primal and dual values coincide — has a discrete analogue that needs no continuity, no differentiability, and no convexity in the classical sense at all: only the elementary fact that the Legendre-Fenchel transform, once discretized, is still an involution on the right class of functions. This mission formalizes that discrete Lagrangian duality framework and its central saddle-point theorem, in full generality — before the book specializes it, in the section that follows, to the specific M-convex perturbation that gives the chapter's headline strong-duality result for M-convex programs.

Setting

Let $V$ and $U$ be finite ground sets. A perturbation of an optimization problem $\min\{f(x) : x \in \mathbb Z^V\}$ is a function $F : \mathbb Z^V \times \mathbb Z^U \to \mathbb Z \cup \{+\infty\}$ such that $F(x,0) = f(x)$ for all $x$ (Eq. (8.54)) and, for each fixed $x$, $F(x,\cdot)$ is self-biconjugate: $F(x,\cdot)^{\bullet\bullet} = F(x,\cdot)$ under the discrete Legendre-Fenchel transform of chunk 10 (Eq. (8.55)). The Lagrangian function is $K(x,y) = \inf\{F(x,u) + \langle u,y\rangle : u \in \mathbb Z^U\}$ (Eq. (8.58)), valued in $\mathbb Z \cup \{\pm\infty\}$ (formalized in EReal, since both the infimum and the supremum below can be genuinely unbounded). The dual objective is $g(y) = \inf\{K(x,y) : x \in \mathbb Z^V\}$ (Eq. (8.60)). Writing $\inf(P) = \inf_x f(x)$, $\sup(D) = \sup_y g(y)$, $\operatorname{opt}(P) = \{x : f(x) = \inf(P)\}$, $\operatorname{opt}(D) = \{y : g(y) = \sup(D)\}$, the primal problem $P$ is to minimize $f$ over $\mathbb Z^V$ and the dual problem $D$ is to maximize $g$ over $\mathbb Z^U$.

Formalization targets

Goal: Theorem 8.54 (the saddle-point theorem)

Assuming $F$ is self-biconjugate (Eq. (8.55)): both $\inf(P)$ and $\sup(D)$ are finite and $\min(P) = \max(D)$ if and only if there exist $\bar x \in \mathbb Z^V$, $\bar y \in \mathbb Z^U$ with $K(\bar x,\bar y)$ finite and $K(x,\bar y) \le K(\bar x,\bar y) \le K(\bar x,y)$ for all $x,y$ — a saddle point of the Lagrangian kernel. When this holds, $\bar x \in \operatorname{opt}(P)$ and $\bar y \in \operatorname{opt}(D)$.

Milestones: Theorem 8.52, Proposition 8.51(1)-(2)

Theorem 8.52 (weak duality): $\inf(P) \ge \sup(D)$ always, with no biconjugacy hypothesis on $F$ at all — the baseline the saddle-point theorem sharpens to equality. Proposition 8.51(1)-(2): under self-biconjugacy, the perturbation $F$ (and hence the primal objective $f$) is itself recoverable from the Lagrangian kernel $K$ by a supremum, $F(x,u) = \sup_y\{K(x,y) - \langle u,y\rangle\}$ and $f(x) = \sup_y K(x,y)$ — the algebraic identity the saddle-point theorem's proof turns on directly.

Significance

The result itself. The saddle-point theorem is the general-purpose engine behind every strong-duality result the book proves for specific classes of discrete optimization problems: the book's own next section specializes it (via a particular choice of $F$ built from an M-convex regularizer $r$) to obtain strong duality for M-convex programs, but the theorem itself needs no M-convexity, no submodularity, and no exchange axiom — only the elementary self-biconjugacy of a perturbation under the discrete Legendre-Fenchel transform. It is, in that sense, the most general and most reusable strong-duality statement in the book: any future mission proving strong duality for a specific class of discrete programs (M-convex, M2-convex, network flow, or otherwise) by exhibiting a self-biconjugate perturbation can cite this theorem directly rather than reproving the saddle-point argument from scratch.

Formalizing it. No matching item exists on the platform for a discrete Lagrangian saddle- point theorem, discrete weak duality, or this perturbation-based duality framework. (A prior-art search turned up an unrelated continuous Lagrangian saddle-point theorem for convex cones, Luenberger's Chapter 8 §8.4, formalized as VectorSpaceOpt.lagrangian_saddle_sufficient_pointed — a genuinely different setting: no discreteness, no biconjugacy hypothesis, and a one-directional sufficiency statement rather than this mission's iff. Not reused.) This mission gives the first formal statement of discrete Lagrangian duality, and directly reuses chunk 10's ConvexConjugate apparatus (self-biconjugacy is stated using chunk 10's own conjugate-of-conjugate composition), demonstrating exactly the kind of shared-substrate payoff the discrete conjugacy theorem was built to provide.

Difficulty

The saddle-point theorem's "only if" direction is not a routine unwinding of definitions: given $\min(P) = \max(D)$ at finite common value, one must construct the saddle point $(\bar x,\bar y)$ — the book's proof takes $\bar x \in \operatorname{opt}(P)$, $\bar y \in \operatorname{opt}(D)$ (which exist because the infimum/supremum are attained at a finite optimum) and verifies the sandwiching inequality using Proposition 8.51(2)'s identity $f(x) = \sup_y K(x,y)$ together with weak duality, rather than by any direct algebraic manipulation of $K$ alone. Skipping straight to a "trivial" biconditional that never invokes Proposition 8.51 would misrepresent the actual proof structure the book relies on for exactly this direction.

Formalization scope

$V, U$ are Fintype ground types; LagrangianKernel, DualObjective, InfP, SupD are EReal-valued to keep both the defining infima/suprema total (a complete lattice) without an artificial finiteness side-condition; OptP, OptD compare PrimalValue/DualObjective against InfP/SupD after casting through chunk 10's ToEReal, mirroring that chunk's own round-trip convention. "Finite" throughout is formalized as ≠ ⊤ ∧ ≠ ⊥ in EReal. The perturbation $F$ itself is left fully abstract (an arbitrary function satisfying the self-biconjugacy hypothesis where needed) — this mission does not draft the specific M-convex perturbation $F_r$ (Eq. (8.61)) that the book's next subsection (§8.4.3) uses to specialize this framework to M-convex programs, nor Theorem 8.59 (the resulting M-convex strong-duality theorem) itself, which needs that specific perturbation plus its own regularity conditions (REG)/(OBJ) and a chain of M-convex-specific propositions (8.55–8.58) beyond what the general framework built here provides. A trivializing formalization would state the saddle-point theorem's sandwiching inequality with a weaker order (e.g., only one of the two directions) or would omit the "$\bar x \in \operatorname{opt}(P), \bar y \in \operatorname{opt}(D)$" consequence clause; neither is done — both inequalities and the full consequence clause are included exactly as the book states them.

Selected references

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

Motivation

This mission completes chapter 7's L-convex function theory and closes the book on it. It first finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly with the classical Lovász extensions of submodular set functions, a one-to-one correspondence that recognizes forty years of submodular-optimization machinery as a special case of L-convex function theory. It then proves the L-side capstone this series has been building toward since mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex functions, ending exactly where chapter 7 itself ends.

Setting

Fix a finite ground set $V$. The class $0L[\mathbb R \to \mathbb R]$ consists of polyhedral L-convex functions that are positively homogeneous; $0L[\mathbb Z \to \mathbb Z]$, its integer-valued integer-domain analogue. A positively homogeneous L-convex function $g$ induces a submodular set function $\rho_g(X) = g(\chi_X)$; conversely the Lovász extension $\hat\rho$ of a submodular set function is positively homogeneous L-convex. The base polyhedron $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ of a submodular $\rho$ is always an M-convex polyhedron. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is quasi submodular (QSB) if $g(p\wedge q) \le g(p)$ or $g(p\vee q) \le g(q)$ for all $p,q$; the weaker (QSBw) requires only $\max\{g(p),g(q)\} \ge \min\{g(p\wedge q), g(p\vee q)\}$.

Formalization targets

Goal: the four characterizations of polyhedral L-convexity (Theorem 7.45)

For a polyhedral convex function $g$ with $\operatorname{dom}_{\mathbb R} g \ne \emptyset$: $g$ is L-convex if and only if every directional derivative $g'(p;\cdot)$ is $0L[\mathbb R \to \mathbb R]$, if and only if every subdifferential $\partial_{\mathbb R} g(p)$ is an M-convex polyhedron, if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct reading and chosen as goal because it is the exact L-side mirror of mission 24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).

Supporting structural targets

Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions 7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional- derivative/subdifferential correspondence via the induced submodular set function's base polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems 7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54 (both missed by the extractor, the latter's full statement requiring one page beyond this chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi L-proximity theorems.

Significance

The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to $\{0,1\}^V$ of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.

None of these results are open — they are Murota's account of how far L-convex function theory extends beyond the polyhedral case (to positive homogeneity and its submodular-function incarnation) and how far its exchange-style inequality can be relaxed while preserving optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for M-convex functions. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete, since chapter 7 ends there and this is the last mission covering it — extending the shared Lean vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove all six pairwise implications among its four conditions independently; the book's own proof instead chains through results already established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34, (b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring Proposition 7.41 applied to the directional derivative itself (showing $\arg\min(g'(p;\cdot)[-x])$ is an L-convex cone by an explicit description via the admissible-potential set of the distance function underlying $\arg\min g[-x]$). The remaining combinatorial difficulty in this block is in Theorem 7.43's proof: identifying $\partial_{\mathbb R} g(p)$ with the base polyhedron $B(\rho_{g,p})$ requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex functions are (V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented, content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made), and Proposition 7.50 states the general inequalities without restating their "In particular" specializations, which add no independent content — see HARD.md. "$\inf g[-x]>-\infty$" is replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission 25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the sixteen sorrys are welcome; the goal and Theorem 7.43 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral theory Theorems 7.26-7.46 are drawn from).
• P. Milgrom and C. Shannon, "Monotone comparative statics," Econometrica, 62 (1994), pp. 157-180 [129] (the origin of the quasi-submodularity condition (SSQSB)).

Motivation

L-convex functions were defined purely combinatorially, on the integer lattice. Chapter 6's M-convex theory showed that combinatorial definition always extends to a genuine convex function on real space (missions 23-ch06c-mconvexfunctions/24-ch06d-mconvexfunctions); this mission carries out the identical program for the L side. It first shows L$^\natural$-convexity is exactly integral convexity plus ordinary submodularity — a clean synonym that also explains why submodular set functions are a natural special case — then builds the entire polyhedral (real-variable) theory of L-convex functions: the axioms (SBF[R])/(TRF[R]), two practical local criteria for verifying submodularity without checking every pair of points, the fact that the classical Lovász extension of a submodular set function is itself a polyhedral L-convex function, the six-operation closure toolkit, and — this mission's goal — the L-optimality criterion in its full polyhedral generality, characterizing global optimality by finitely many directional derivatives.

Setting

Fix a finite ground set $V$. A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is polyhedral L-convex, $g \in L[\mathbb R \to \mathbb R]$, if it satisfies (SBF[R]): $g(p)+g(q) \ge g(p\vee q)+g(p\wedge q)$, and (TRF[R]): $\exists r \in \mathbb R$, $g(p+\alpha\mathbf 1) = g(p)+\alpha r$ for all $p \in \mathbb R^V$, $\alpha \in \mathbb R$; it is polyhedral L$^\natural$-convex if its lift to one extra real coordinate is polyhedral L-convex. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is integrally convex if its convex closure agrees, at every real point, with the closure taken using only that point's integral neighborhood. The Lovász extension $\hat\rho$ of a submodular set function $\rho$ is the piecewise-linear interpolation built from the sorted distinct components of $p \in \mathbb R^V$. The directional derivative $g'(p;d)$ is $\inf_{t>0}(g(p+td)-g(p))/t$.

Formalization targets

Goal: the polyhedral L-optimality criterion (Theorem 7.33)

For a polyhedral L-convex function $g$ and $p \in \operatorname{dom}_{\mathbb R} g$: $g(p) \le g(q)$ for all $q$ if and only if $g'(p;\chi_Y) \ge 0$ for every $Y \subseteq V$ and $g'(p;\mathbf 1)=0$; for polyhedral L$^\natural$-convex $g$, the criterion simplifies to $g'(p;\pm\chi_Y) \ge 0$ for every $Y$. This is the direct L-side mirror of mission 24-ch06d-mconvexfunctions's M-optimality criterion (Theorem 6.52) and the polyhedral generalization of mission 08-lconvex-functions-i's integer-domain L-optimality criterion (Theorem 7.14): checking global optimality against exponentially many points reduces to $|V|+1$ (or $2|V|$) directional-derivative inequalities.

Supporting structural targets

Twelve further results build the polyhedral theory from the ground up. Theorems 7.20-7.21 identify L$^\natural$-convexity with the conjunction of ordinary submodularity and integral convexity — a genuinely different, function-analytic characterization from the exchange-axiom- style definitions used so far. Propositions 7.23-7.24 give two practical sufficient conditions for verifying (SBF[R]) locally, at a single scale, rather than globally. Proposition 7.25 shows the Lovász extension of any submodular set function is automatically polyhedral L-convex — not in this chunk's own extraction table (its label is preceded by an unlabeled restatement of the same fact, which evidently confused the extractor), found and placed by direct reading. Theorem 7.26 shows an L-convex function's convex extension, when polyhedral, inherits polyhedral L-convexity, continuing mission 26-ch07b-lconvexfunctions's Theorem 7.19. Theorems 7.28-7.32 restate the discrete theory's core equivalences (translation submodularity, the L/L$^\natural$ correspondence, the six basic operations, restrictions) in the polyhedral setting, and Proposition 7.34 shows minimizer sets of linearly-perturbed polyhedral L-convex functions are themselves L-convex polyhedra — flagged by the book itself as a partial result whose full converse characterization (Theorem 7.45) lies beyond this chunk's range.

Significance

Theorems 7.20-7.21's synonym is structurally important: it means every algorithm and theorem already known for submodular-function minimization over $\{0,1\}^V$-type domains applies, after a midpoint-convexity check, to the vastly larger class of integer-lattice L$^\natural$-convex functions, with no new proof technique required. Proposition 7.25 is the bridge that lets the combinatorial Lovász extension — the workhorse of submodular optimization for forty years — be recognized as a special case of the polyhedral L-convex function theory this mission builds, explaining why algorithms for one transfer so readily to the other. The goal, Theorem 7.33, is the precise tool chapter 10's continuous-relaxation algorithms for L-convex-function minimization actually verify against: a scaling algorithm's claimed optimum is confirmed correct exactly by checking the criterion's finitely many directional-derivative inequalities.

None of these results are open — they are Murota's account of how the integer-lattice theory of L-convexity survives, result by result, the passage to polyhedral convex functions on $\mathbb R^V$, mirroring chapter 6's identical program for M-convexity. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 7.25) the platform's own automated extractor missed, extending the shared Lean vocabulary (SBFR, TRFR, LovaszExtension, DirDeriv) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify $g(p) \le g(q)$ directly against every $q \in \mathbb R^V$; the book's actual proof instead reduces this to the finite family of directional derivatives via Theorem 7.20's integral-convexity fact (an L$^\natural$-convex function's local behavior determines its global behavior) applied to the polyhedral setting through Theorem 3.21's general optimality criterion for integrally convex functions — a two-layer reduction (polyhedral $\to$ integral-convexity $\to$ finite local check) with no direct one-step argument. The genuine combinatorial content in this block is in Proposition 7.25's proof: showing the Lovász extension is submodular requires the finite-valued case (a direct calculation split on whether the two perturbed coordinates land in the same or different threshold sets) and then a limiting argument over a sequence of finite-valued truncations $\rho_k \to \rho$ for the general, possibly-infinite case — a genuine two-step argument, not a single inequality chase.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; polyhedral L-(natural-)convex functions are (V→ℝ)→WithTop ℝ. All thirteen numbered results found in this chunk's page range are placed, with one documented scope reduction: Proposition 7.24 states only part (1) (the unconditional-on-magnitude sufficient condition), not part (2)'s sharper, sorted-index-restricted version, which needs the same SortedValues apparatus a second time for no other result's benefit — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomR ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution. "Domain is closed"/"domain is an interval" (Propositions 7.23-7.24) are stated via Mathlib's IsClosed and Set.OrdConnected respectively, the latter being the precise order-theoretic notion of "interval" in a pointwise-ordered space. This mission's base vocabulary is redeclared from missions 08-lconvex-functions-i, 20-ch04b-mconvexsets (for the Lovász extension machinery), 21-ch05b-lconvexsets, 23-ch06c-mconvexfunctions/ 24-ch06d-mconvexfunctions, and 26-ch07b-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 7.25 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [152] (the polyhedral L-convex function theory this mission's real-variable results are drawn from).

Motivation

Chapter 5 characterized L-convex sets — sublattice-closed, translation-periodic subsets of $\mathbb Z^V$ — and showed they interact cleanly with integral convexity. Chapter 7 asks the functional analogue: which functions on the integer lattice deserve to be called convex in the "L" sense, and how do they relate back to L-convex sets? This mission (continuing mission 08-lconvex-functions-i, which built the axioms (SBF[Z])/(TRF[Z])/(SBF$^\natural$[Z]) and proved the L-optimality and L-proximity theorems) answers the second question at its sharpest: an L-convex function is exactly a function whose every weighted-minimizer set is an L-convex polyhedron — the discrete analogue of the fact that a convex function is determined by the convex geometry of its sublevel sets. Along the way it settles the chapter's basic toolkit: operations that preserve L-convexity, the local nature of submodularity, the correspondence with ordinary submodular set functions, and the first two structural facts about the convex extension every L-convex function admits.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is L-convex, $g \in L[\mathbb Z \to \mathbb R]$, if it satisfies submodularity (SBF[Z]): $g(p)+g(q) \ge g(p\vee q) + g(p\wedge q)$, and translation invariance (TRF[Z]): $\exists r \in \mathbb R$, $g(p+\mathbf 1) = g(p) + r$ for all $p$. It is L$^\natural$-convex if its lift to one extra coordinate (Eq. (7.2)) is L-convex. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ is submodular if $\rho(X)+\rho(Y) \ge \rho(X\cup Y) + \rho(X\cap Y)$; it corresponds to an L$^\natural$-convex function supported on $\{0,1\}^V$ via $g(\chi_X) = \rho(X)$ (Eq. (7.5)). The convex closure $\bar g$ of $g$ is its extension to $\mathbb R^V$ by finite convex combinations.

Formalization targets

Goal: L-convexity via minimizer polyhedra (Theorem 7.17)

For $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with bounded nonempty effective domain: $g$ is L-convex if and only if $\arg\min g[-x]$ is an L-convex set for every $x \in \mathbb R^V$; the L$^\natural$ analogue holds with L$^\natural$-convex sets. This is the direct mirror of mission 23-ch06c-mconvexfunctions's own goal (Theorem 6.43, characterizing M-convex functions via M-convex weighted-minimizer polyhedra) — the book's text calls it exactly "how the concept of L-convex functions can be defined from that of L-convex sets."

Supporting structural targets

Eleven further results build the chapter's basic vocabulary. Theorem 7.2 strengthens translation submodularity to allow negative shifts; Theorem 7.3 places L-convexity inside L$^\natural$- convexity; Proposition 7.4 identifies submodular set functions with a subclass of L$^\natural$-convex functions via the indicator embedding, and Theorem 7.15 derives the classical submodular-minimizer local-optimality criterion as its corollary; Proposition 7.5 shows submodularity is a local property, needing only unit-distance pairs; Proposition 7.8 transfers L-(natural-)convexity from functions to their effective domains; Proposition 7.9 and Theorem 7.10–7.11 give the chapter's basic examples (univariate and pairwise-difference functions) and its six-operation closure toolkit (scaling, affine reparametrization, linear perturbation, projection, infimal convolution with a separable function, and sums), both for L-convex and L$^\natural$- convex functions, the latter also admitting interval and coordinate restrictions; Proposition 7.16 shows minimizer sets of L-convex functions are themselves L-convex, the special case ($x=0$) the goal generalizes to every linear perturbation; Theorem 7.19 begins the convex-extension program this chapter's next chunk completes, establishing that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant.

Significance

The goal is significant for the same structural reason as its M-side counterpart: it says L-convexity is not merely a combinatorial condition on lattice differences but is equivalent to a purely polyhedral-geometric one, closing the loop between chapters 5 and 7 the way Theorem 6.43 closes the loop between chapters 4 and 6. Theorem 7.15's corollary status is itself instructive: the well-known fact that a submodular set function's global minimizer needs only local verification against comparable sets — the theoretical basis of every submodular-minimization algorithm in chapter 10 — falls out of the L-optimality criterion (mission 08-lconvex-functions-i's Theorem 7.14) applied to the indicator embedding, rather than needing an independent proof. Theorem 7.10–7.11's six operations are the toolkit every later construction in this chapter and chapter 9's network transformations builds new L-convex functions from old.

None of these results are open — they are Murota's account of the basic function-level theory of L-convexity, mirroring chapter 6's M-convex function theory chunk-by-chunk. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (SBF, TRF, LNaturalConvex, LConvexSet) that missions 08-lconvex-functions-i and 21-ch05b-lconvexsets began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify L-convexity's submodularity inequality directly against the definition of an L-convex set applied to each minimizer family; the book's actual proof instead routes through Theorem 7.10 (3)'s closure of L-convexity under linear perturbation and Proposition 7.16's minimizer-is-L-convex-set fact for the forward direction, and defers the converse entirely to a later note (Note 7.47, outside this chunk and mission 08's combined range) proved via the integral-convexity machinery of section 7.7 onward. The genuine combinatorial difficulty in this block is upstream, in Theorem 7.10 (5)'s infimal-convolution operation: proving L-convexity of the perturbed function requires a four-term submodularity inequality assembled from the separable function's own convexity and $g$'s submodularity applied at the optimal $q_1,q_2$ simultaneously — a genuine two-hypothesis combination with no single-inequality shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-(natural-)convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with one documented scope reduction: Theorem 7.19 states only parts (3)-(4) (that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant), not the explicit Lovász-extension-formula construction of parts (1)-(2) and (5), which needs a sorted-distinct- component apparatus no other result in this chunk requires — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomZ ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution (WithTop ℝ has no $-\infty$ element). This mission's base vocabulary (SBF, TRF, LNaturalConvex, etc.) is redeclared verbatim from mission 08-lconvex-functions-i rather than imported, since sibling drafts in this series cannot yet reference one another; LConvexSet is likewise redeclared from mission 21-ch05b-lconvexsets. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 7.10 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313–371 (the original account of L-convex functions this chapter's basic theory is drawn from).

Motivation

Milgrom and Shannon's theory of quasi-supermodularity, developed for monotone comparative statics in economics, showed that many of the consequences of lattice submodularity survive under a much weaker, purely ordinal relaxation of the defining inequality. Chapter 7's final section imports this idea into discrete convex analysis: does L-convexity's optimality and proximity theory survive when the additive submodularity inequality is relaxed to an ordinal condition on the sign pattern of the two relevant differences, rather than their sum? This mission formalizes the chapter's answer for the strongest of the relevant relaxations, (SSQSB) (semistrict quasi submodularity): yes, and the class is large enough to include every strictly increasing rescaling of an L-convex function — exactly mirroring chunk 07's result for the M-convex side, and completing the "quasi" theory on both halves of the exchange-axiom framework before chapter 8 unifies them under conjugacy.

Setting

Let $V$ be a finite ground set and $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Building on chunk 08's submodularity axiom (SBF[Z]), this section introduces four ordinal relaxations. $g$ is quasi submodular, satisfying (QSB), if for every $p, q \in \mathbb Z^V$, $g(p \wedge q) \le g(p)$ or $g(p \vee q) \le g(q)$. $g$ is semistrictly quasi submodular, satisfying (SSQSB), if additionally $g(p \vee q) \ge g(q) \implies g(p \wedge q) \le g(p)$ and symmetrically. The weak variants (QSBw) and (SSQSBw) restrict attention to points of the effective domain and compare $\max(g(p), g(q))$ against $\min(g(p \wedge q), g(p \vee q))$ directly, with (SSQSBw) additionally allowing the four-way tie $g(p) = g(q) = g(p\wedge q) = g(p \vee q)$. The linear perturbation of $g$ by $x : V \to \mathbb R$ is $g[x](p) = g(p) + \langle p, x \rangle$.

Formalization targets

Goal: Theorem 7.54 (the quasi L-proximity theorem)

Let $g$ satisfy (SSQSB) and $g(p) = g(p + \mathbf 1)$ for all $p$, $n = |V|$, $\alpha$ a positive integer. If $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha \chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound $p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1) \mathbf 1$ — verbatim the same conclusion, and the same exact bound, as chunk 08's Theorem 7.18(1), now established for the strictly larger class satisfying (SSQSB) rather than (SBF[Z]).

Milestones: Theorems 7.49, 7.53

Theorem 7.49: the full nesting chain (SBF[Z]) $\Rightarrow$ (SSQSB) $\Rightarrow$ (QSB), (SSQSB) $\Rightarrow$ (SSQSBw) $\Rightarrow$ (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of $g$ satisfies (QSBw) — precisely quantifying how weak (QSBw) is pointwise and how the classes reunite under universal perturbation. Theorem 7.53 (the quasi L-optimality criterion): the direct analogue of chunk 08's Theorem 7.14, showing that global (or, for the weaker (QSBw) case, unique-up-to-translation) optimality still reduces to a purely local check against the $2^n - 2$ nontrivial sign-pattern neighbors $p + \chi_X$.

Significance

The result itself. As with the M-convex case (chunk 07), the proximity theorem is what algorithms actually need: an L-convex-flavored objective transformed by any strictly increasing scalar rescaling (a common device — expressing a network-flow cost in a different currency, or applying a monotone risk adjustment) retains a scaling algorithm's correctness guarantee with exactly the same distance bound, even though the rescaled function is generally no longer L-convex itself.

Formalizing it. No matching item exists on the platform for quasi submodularity or quasi L-convexity in any form. Together with chunk 07 (the M-side quasi-convexity theory), this mission completes the "quasi" relaxation on both halves of the exchange-axiom framework the book develops, immediately before chapter 8 unifies M-convexity and L-convexity under a single conjugacy relationship.

Difficulty

As with chunk 07's quasi M-proximity theorem, the temptation is to imitate chunk 08's L-proximity proof line by line. The overall architecture does survive — translate so $p_\alpha = 0$, find a lattice-minimal sufficiently-good point, and bound the gap using submodularity — but chunk 08's proof uses (SBF[Z])'s additive inequality directly to compare four function values at once, while this proof must instead route every such comparison through (SSQSB)'s two one-directional implications (Proposition 7.50's quasi-version of the same two-sided inequality), which only ever license moving in one direction at a time depending on which side of a comparison is tight. The book's proof handles this by working with the specific implications (7.43)–(7.44) in place of the L♮-approach property used in chunk 08's proof — an ordinal substitute for the same additive step, at the cost of a case analysis chunk 08's proof did not need.

Formalization scope

This mission builds directly on chunk 08's published items (SBF, DomZ, ArgMin, IndicatorVec), per the platform's textbook convention that a later chapter section of the same book imports an earlier one's definitions; its own namespace DiscreteConvex.LConvexFunctions.Quasi nests under chunk 08's DiscreteConvex.LConvexFunctions accordingly. Note the sign convention of the linear perturbation here, $g[x](p) = g(p) + \langle p,x\rangle$, is the opposite of the M-side's $f[p](x) = f(x) - \langle p,x\rangle$ (chunks 06–07) — verified against the book's own formula rather than assumed by analogy.

A trivializing formalization of the goal would silently strengthen (SSQSB) back to plain (SBF[Z]) (making this mission redundant with chunk 08's Theorem 7.18) or loosen the exact bound $(n-1)(\alpha-1)$; neither is done. Only (QSB), (SSQSB), (QSBw), (SSQSBw) are drafted, matching exactly what the chosen three items need; the polyhedral L-convex-function bridge (§7.8–7.9, Theorems 7.40–7.46) and the level-set characterizations (Theorems 7.51–7.52) are left for a follow-on mission. Contributions building the 0L ↔ S correspondence (Theorem 7.40, a bridge back to chunk 04's submodular-set-function vocabulary) or the scaled quasi L-minimizer-cut analogue are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Milgrom, C. Shannon, "Monotone comparative statics," Econometrica, 62(1), 1994, pp. 157–180.