All missions

Motivation

Fictitious play is the oldest model of learning in games: players repeatedly play a fixed normal form game, and each round every player best-responds to the empirical frequencies of the opponents' past play. Brown (1951) proposed it as an algorithm for computing the value of a zero-sum game, and Robinson (1951) proved that the empirical frequencies converge to the set of equilibria in that case. In stochastic fictitious play (Fudenberg and Kreps 1993) each player's payoffs are perturbed by fresh random shocks before every choice. The shocks make best responses single-valued and smooth in beliefs, which puts the process within reach of stochastic approximation theory: its long-run behaviour is governed by a deterministic perturbed best response dynamic.

Before Hofbauer and Sandholm (2002), convergence of stochastic fictitious play was known only for 2×2 games (Fudenberg and Kreps 1993; Kaniovski and Young 1995) and for certain games with two strategies per player (Benaïm and Hirsch 1999). The difficulty was the perturbed dynamic itself, whose vector field involves choice probabilities with no closed form for general noise distributions. Hofbauer and Sandholm showed that every such dynamic can be rewritten with a deterministic payoff perturbation (their Theorem 2.1), and used that to carry Lyapunov functions over to arbitrary noise distributions. This mission covers the first two classes of games in their main convergence theorem: symmetric games with an interior evolutionarily stable strategy, and two player zero-sum games.

Setting

A two player normal form game has strategy sets $S^1 = \{1,\dots,n^1\}$ and $S^2 = \{1,\dots,n^2\}$ and utilities $u^\alpha : S^1 \times S^2 \to \mathbb R$. Player $\alpha$'s mixed strategies form the simplex $\Delta S^\alpha$, and $\Sigma = \Delta S^1 \times \Delta S^2$. The payoff vector $U^\alpha(x^{-\alpha}) \in \mathbb R^{n^\alpha}$ lists the expected payoff of each pure strategy of $\alpha$ against the opponent's mixed strategy. The game is zero-sum if $u^1(s) = -u^2(s)$ for every profile $s$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function $C^\alpha(\pi)_i = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$, for $\varepsilon$ with density $f^\alpha$, gives the perturbed best response $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$. The densities are required to be strictly positive with continuously differentiable choice functions ("the conditions of Theorem 2.1").

Standard stochastic fictitious play. Pure strategies are identified with basis vectors $e_i$. Choices $\zeta_1$ are arbitrary. At every time $t \ge 1$ each player $\alpha$ draws a shock $\varepsilon^\alpha_t$ with density $f^\alpha$ and plays at time $t+1$ the pure strategy maximizing $U^\alpha_k(Z^{-\alpha}_t) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t \sum_{u=1}^t \zeta_u \in \Sigma .$$

The shocks are independent over time and across players. The expected motion of $Z_t$ is the perturbed best response dynamic

$$\text{(P)}\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha \quad\text{on } \Sigma .$$

Symmetric games. A two player game is symmetric if $S^1 = S^2 = \{1,\dots,m\}$ and $u^1(i,j) = u^2(j,i)$; it is described by the matrix $A_{ij} = u^1(i,j)$, and $U^1(z) = Az$. In symmetric stochastic fictitious play two players in roles 1 and 2 play at every time, their shocks are independent and identically distributed with one density $f$, and the state is the average of all past plays in both roles,

$$\hat Z_t = \frac1{2t}\sum_{u=1}^t \big(\hat\zeta^1_u + \hat\zeta^2_u\big) \in \Delta S^1 .$$

Its mean dynamic is $\text{(SP)}\ \dot x = C(Ax) - x$ on $\Delta S^1$. A mixed strategy $x^*$ in the interior of $\Delta S^1$ is an interior evolutionarily stable strategy (ESS) if $x^*\cdot Ax > x\cdot Ax$ for all mixed $x \ne x^*$ near $x^*$.

Rest points and chain recurrence. For a dynamic $\dot x = F(x)$ on a compact set $X$, the rest points are the zeros of $F$ in $X$. A point $x$ is chain recurrent if for every $\varepsilon > 0$ one can return from $x$ to $x$ by following solution segments of length at least $1$, with jumps of size less than $\varepsilon$ between segments.

Formalization targets

Goal: Theorem 6.1 (i) and (ii)

(i) If $A$ has an interior ESS, then (SP) has a unique rest point $\hat x$ and

$$P\Big(\lim_{t\to\infty} \hat Z_t = \hat x\Big) = 1 .$$

(ii) If the two player game is zero-sum, then (P) has a unique rest point $x^*$ and

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1 .$$

Both hold for all shock densities meeting the conditions of Theorem 2.1, all probability spaces carrying the shocks, and all initial choices.

Milestones

1. Theorem 2.1: for such a density, the choice function $C$ is the unique maximizer $C(\pi) = \operatorname{argmax}_{y \in \operatorname{int}\Delta}(y\cdot\pi - V(y))$ for one admissible deterministic perturbation $V$.
2. With an interior ESS, $\hat\Lambda(x) = x\cdot Ax - V(x) - W(Ax)$, where $W(\pi) = \max_y (y\cdot\pi - V(y))$, is strictly concave and a strict Lyapunov function for the deterministically perturbed dynamic (SPV).
3. Its maximizer is the unique chain recurrent point of (SPV).
4. In zero-sum games, $\Lambda(x^1,x^2) = -V^1(x^1) - W^1(U^1(x^2)) - V^2(x^2) - W^2(U^2(x^1))$ is strictly concave and a strict Lyapunov function for (PV).
5. Its maximizer is the unique chain recurrent point of (P).
6. The maximizer of $\hat\Lambda$ is the unique chain recurrent point of (SP).

Significance

The theorem gives global, almost sure convergence of a learning process for arbitrary noise distributions, not only for the logit (Gumbel) noise under which the perturbed dynamic has a closed form. For zero-sum games it is the stochastic counterpart of Robinson's theorem. For symmetric games with an interior ESS it shows that a population learning by stochastic fictitious play settles at a single mixed state. Since the choice functions are continuous, the players' choice probabilities converge as well. The limit is the rest point of the perturbed dynamic, which approximates a Nash equilibrium (in case (i), the ESS) as the noise vanishes.

On the formal side, the paper's results are proved, but no part of them is machine-checked, and the platform has no model of learning in games, of chain recurrence, or of stochastic approximation. The mission produces a formal model of stochastic fictitious play as a random process, formal statements of the Hofbauer and Hofbauer–Hopkins Lyapunov functions, and the chain recurrence characterizations that connect them to the process.

Difficulty

The obvious route replaces the process $Z_t$ by the ODE (P) and argues that (P) converges. That step is where the argument is incomplete: convergence of every solution of (P) does not give convergence of the stochastic process, because a stochastic approximation can in principle circulate near a set of orbits the ODE never follows. The right invariant is the chain recurrent set, and the limit sets of the process lie in a connected component of it (Benaïm and Hirsch 1999; Benaïm 1999). The characterization therefore has to be of chain recurrence, which is strictly weaker than asymptotic stability of individual orbits.

The second obstacle is that (P) itself is defined through the noise distribution and admits no useful Lyapunov function in general. The Lyapunov functions exist for the deterministic form (PV)/(SPV), and moving between the two forms requires the representation of Theorem 2.1, whose perturbation $V$ has no closed form either.

Formalization scope

Players and strategies are indexed from $0$. Mixed profiles live in $\prod_\alpha \mathbb R^{n^\alpha}$ and every vector field is defined on that ambient space. The processes are defined pathwise from a family of shock vectors on an arbitrary probability space. Ties in the argmax are broken by the smallest index, an event of probability zero because the shocks have densities. The shock drawn at time $t$ produces the choice at time $t+1$. Shock densities are arbitrary strictly positive densities with continuously differentiable choice functions; no noise law is fixed, and the two players' densities in (ii) may differ. Independence is joint over times and players (and roles in (i)). The symmetric process has its own state in one simplex and is not the standard process applied to a symmetric game.

Deterministic perturbations are functions defined on the whole space whose values off the open simplex are ignored; derivatives are taken of their composition with the projection onto the affine plane $\{\sum_i y_i = 1\}$. Perturbed best responses in (PV) and (SPV) are supplied as maps together with the hypothesis that they are the unique maximizers. A strict Lyapunov function must increase strictly along every non-constant solution on $(0,\infty)$. The ESS definition includes $x \ne x^*$, which the source omits.

The conclusions assert existence and uniqueness of the rest point; they are not hypotheses. A statement for the ODE (P) in place of the process $Z_t$, for one fixed noise law, or with the ESS as the limit point would be a different theorem.

A complete development needs Theorem 2.1 (convex duality and the Legendre transform on the simplex), existence and uniqueness of solutions of (P), basic chain recurrence theory, and the stochastic approximation results of Benaïm and Hirsch, which are not restated here and are welcome as independent contributions. The model layer (games, payoff vectors, choice functions, stochastic fictitious play) is shared with the other missions of this series.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• Y. M. Kaniovski and H. P. Young, Learning Dynamics in Games with Stochastic Perturbations, Games and Economic Behavior 11, 330–363, 1995. https://doi.org/10.1006/game.1995.1054
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54, 296–301, 1951. https://doi.org/10.2307/1969530
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

Models of learning in games, and discrete choice models in econometrics, describe an agent who does not always pick the best alternative. Two descriptions of such an agent are standard. In the additive random utility model (McFadden 1981; Anderson, de Palma and Thisse 1992) the agent maximizes payoffs perturbed by random shocks. In the deterministic perturbation model (Fudenberg and Levine 1998) the agent chooses a probability vector and pays a deterministic, strictly convex cost for it. The logit choice rule arises from both: from i.i.d. extreme-value shocks, and from the entropy cost $V(y) = \eta \sum_j y_j \ln y_j$.

Hofbauer and Sandholm (Econometrica 70 (2002)) show that the second description is general enough to cover the first for every shock distribution with a strictly positive density, not only for logit. Their analysis of stochastic fictitious play rests on this: the deterministic representation provides the perturbed payoff functions from which Lyapunov functions for the learning dynamics are built, for arbitrary noise. This mission formalizes that discrete choice theorem, Theorem 2.1 of the paper, together with the steps of its proof.

Setting

Fix $n \ge 1$ alternatives $A = \{1, \dots, n\}$ with base payoffs $\pi = (\pi_1, \dots, \pi_n) \in \mathbb{R}^n$. A random vector $\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)$ has a strictly positive density $f : \mathbb{R}^n \to \mathbb{R}$, whose law does not depend on $\pi$. The agent chooses the alternative whose total payoff $\pi_j + \varepsilon_j$ is largest, which gives the choice probability function $C : \mathbb{R}^n \to \mathbb{R}^n$,

$$C_i(\pi) = P\big(\operatorname{argmax}_j\, \pi_j + \varepsilon_j = i\big).$$

The probability simplex is $\Delta A = \{x \in \mathbb{R}^n_+ : \sum_j x_j = 1\}$, with relative interior $\operatorname{int}(\Delta A)$ (all coordinates positive) and tangent space $\mathbb{R}^n_0 = \{z \in \mathbb{R}^n : \sum_j z_j = 0\}$.

A deterministic perturbation is a function $V : \operatorname{int}(\Delta A) \to \mathbb{R}$. Because $V$ lives on the relative interior, its gradient $\nabla V(y)$ is the vector of $\mathbb{R}^n_0$ with $V(y + hz) = V(y) + (\nabla V(y) \cdot z) h + o(h)$ for all $z \in \mathbb{R}^n_0$, and its second derivative $D^2 V(y)$ is a quadratic form on $\mathbb{R}^n_0$. The perturbation is admissible if $V$ is twice continuously differentiable along the simplex, $D^2V(y)$ is positive definite on $\mathbb{R}^n_0$ for every $y$, and $\|\nabla V(y)\| \to \infty$ as $y$ approaches the boundary of $\Delta A$.

Formalization targets

Goal: Theorem 2.1

If $\varepsilon$ has a strictly positive density and $C$ is continuously differentiable, then there is an admissible $V$ such that, for every $\pi \in \mathbb{R}^n$,

$$C(\pi) = \operatorname*{argmax}_{y \in \operatorname{int}(\Delta A)} \big( y \cdot \pi - V(y) \big),$$

with a unique maximizer. The perturbation $V$ is one function serving all payoff vectors at once.

Milestones

The milestones are the steps of the paper's proof (pp. 5–7), in order:

1. Eq. (4). $DC(\pi)$ is symmetric, $\partial C_i/\partial \pi_j = \partial C_j / \partial \pi_i$, and its off-diagonal terms are strictly negative.
2. Eq. (5). $\partial C_i/\partial \pi_i = -\sum_{j \ne i} \partial C_j/\partial \pi_i$, and $DC(\pi)\mathbf{1} = 0$.
3. Eq. (6). $z \cdot DC(\pi) z > 0$ whenever $z$ is not proportional to $\mathbf{1}$.
4. Shift invariance and injectivity. $C(\pi + c\mathbf{1}) = C(\pi)$, and $C$ is one-to-one on $\mathbb{R}^n_0$.
5. Range observation. If the payoffs $\pi_j$, $j \in J$, stay bounded while the others tend to $+\infty$, then $C_j(\pi) \to 0$ for $j \in J$.
6. Convex potential. There is $W : \mathbb{R}^n \to \mathbb{R}$ with $\nabla W \equiv C$, strictly convex on $\mathbb{R}^n_0$.
7. Range. $C$ takes values in $\operatorname{int}(\Delta A)$, and $C(\mathbb{R}^n_0) = \operatorname{int}(\Delta A)$.

Significance

The result. Theorem 2.1 lets any smooth additive random utility model be replaced by an optimizing agent with a strictly convex, boundary-repelling cost. In the paper this is the bridge from the perturbed best response dynamic to a deterministic perturbed-payoff formulation, which yields Lyapunov functions for zero-sum games, games with an interior evolutionarily stable strategy, and potential games (§4 of the paper), and so the almost sure convergence of stochastic fictitious play under general noise (Theorem 6.1). Without it those convergence results would be restricted to noise distributions whose choice rule has a known deterministic representation, essentially logit. The paper also shows (Proposition 2.2) that the converse fails when $n \ge 4$: deterministic perturbations generate strictly more choice rules than random utility.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. The mission asks for a formal proof of Theorem 2.1 and the seven steps above. Along the way it requires symmetric Jacobians of probability integrals, a gradient-field potential on $\mathbb{R}^n$, and the Legendre transform of a strictly convex function restricted to a hyperplane. None of these is currently packaged in Mathlib in the needed form.

Difficulty

The obvious argument is to take $V$ to be the Legendre transform of the potential $W(\pi) = \mathbb{E}\max_j(\pi_j + \varepsilon_j)$ and read off the first-order conditions. Three steps of that argument are not routine. First, the derivative identity (4) is a change of variables inside an $(n-1)$-fold integral over a moving region, and its strict sign needs the density to be positive on the relevant hyperplane sections. Second, the Legendre transform is well defined on all of $\operatorname{int}(\Delta A)$ only if $C$ maps $\mathbb{R}^n_0$ onto the whole open simplex. The paper takes this from Theorem 26.5 of Rockafellar (1970), whose hypotheses (essential smoothness, strict convexity, identification of the conjugate's domain) must be checked here. Third, positive definiteness of $D^2V$ and the gradient blow-up at the boundary are statements about the inverse of $C$ on $\mathbb{R}^n_0$. They need an inverse function argument on a subspace and a properness argument, not only pointwise convexity.

Verifying that $C(\pi)$ satisfies the first-order condition for one fixed $\pi$ does not suffice: the goal requires a single $V$ for all $\pi$, and a unique maximizer.

Formalization scope

Alternatives are indexed by Fin n with $n \ge 1$; vectors are Fin n → ℝ with its sup norm. The density is a real function $f$ that is continuous, strictly positive at every point, and has $\int f = 1$; the law of $\varepsilon$ is Lebesgue measure weighted by $f$. The paper's formula (4) evaluates $f$ on hyperplanes, which is meaningful for a continuous $f$. Without continuity the theorem can fail: a density that is positive everywhere but tends to zero near a hyperplane can make $C$ continuously differentiable with a vanishing off-diagonal derivative, and then no twice differentiable $V$ represents $C$. Continuous differentiability of $C$ is a hypothesis, as in the paper, stated as ContDiff ℝ 1 of the map $\pi \mapsto C(\pi)$. The event "$i$ is the argmax" uses strict inequalities; ties have probability zero.

$V$ is a function on $\mathbb{R}^n$ of which only the values on $\operatorname{int}(\Delta A)$ enter. Its smoothness and second derivative are taken in the chart $z \mapsto V(y + z)$ on the subspace $\mathbb{R}^n_0$. $\nabla V(y)$ is the tangent gradient of the paper's footnote 3, not an ambient gradient of an extension. The boundary blow-up is stated uniformly: for every $M$ there is $\delta > 0$ such that every tangent gradient at an interior point with some coordinate below $\delta$ has norm above $M$.

The goal cannot be satisfied trivially. $V$ must be chosen before $\pi$, all three admissibility conditions are part of the definition, and the maximizer must be unique. Weakening any of these (a $V$ depending on $\pi$, a $V$ without second derivatives, a non-strict maximum) changes the theorem.

Reusable infrastructure: differentiation of choice probabilities under a density, potentials of symmetric $C^1$ vector fields on $\mathbb{R}^n$, and Legendre duality for strictly convex functions on a subspace. Contributions of any of these as separate lemmas are welcome, as are alternative proofs of the milestones, for instance obtaining the potential directly as $\mathbb{E}\max_j(\pi_j + \varepsilon_j)$.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press, 1998.
• S. P. Anderson, A. de Palma and J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• D. McFadden, Econometric Models of Probabilistic Choice, in C. F. Manski and D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the $\pm 1$ entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.

Setting

Fix two fields $K \subseteq F$: typically $K = \mathbb{Q}$ and $F$ a field large enough to hold every number in the problem. A family $t_1, \dots, t_m \in F$ is algebraically independent over $K$ if no nonzero polynomial with coefficients in $K$ vanishes at $(t_1, \dots, t_m)$ — informally, the $t_i$ behave as free, unconstrained parameters relative to $K$. Fix finite row and column index sets $R$ and $C$. A matrix $A = (A_{ij})_{i \in R, j \in C}$ over $F$ is a mixed matrix with respect to $(K, F)$ if it decomposes as

$$A = Q + T$$

where $Q = (Q_{ij})$ has every entry in $K$, and $T = (T_{ij})$ has entries in $F$ whose nonzero values, taken together as one family, are algebraically independent over $K$. $Q$ models the exact, structural part of the system; $T$ models the independent physical parameters. For $I \subseteq R$ and $J \subseteq C$, write $A[I,J]$ for the submatrix with rows $I$ and columns $J$. The rank of $A$ is its rank over $F$ — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write $\rho(I,J) = \operatorname{rank} Q[I,J]$, $\tau(I,J) = \operatorname{rank} T[I,J]$, and $\gamma(I,J)$ for the number of rows of $I$ that contain a nonzero entry of $T$ in some column of $J$. A mixed polynomial matrix $A(s) = Q(s) + T(s)$ is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate $s$ (used to model the Laplace- or $z$-transform variable of a linear time-invariant system): $Q(s)$ has every coefficient of every entry in $K$, and the coefficients of $T(s)$'s entries, taken together, are algebraically independent over $K$.

Formalization targets

$$\textbf{Theorem 12.9 (goal).}\quad \text{For a mixed matrix } A=Q+T,\ \exists\, I \subseteq R,\ J \subseteq C:\quad |I|+|J|-\operatorname{rank} Q[I,J] = |R|+|C|-\operatorname{rank} A \ \ \text{and}\ \ \operatorname{rank} T[I,J] = 0.$$

This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of $A$'s rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of $A$ reduces to nonsingularity of a $Q$-part and a $T$-part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.

Significance

The result itself. Theorem 12.9 gives a certificate, not just a number: a pair $(I,J)$ that simultaneously proves the exact numeric rank contribution of $Q$ and exhibits a submatrix of $T$ that vanishes identically. Because $\rho$ (via Gaussian elimination on $Q$) and $\gamma$, $\tau$ (via maximum bipartite matching on $T$'s nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.

Formalizing it. All five results in this mission are proved in the source text (this is textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that the genericity hypothesis — "the nonzero entries of $T$ are algebraically independent" — is precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent rather than an informal paraphrase such as "generic" or "random" values, which would be either meaningless or a different (probabilistic) condition.

Difficulty

The naive approach to testing whether $A = Q+T$ is nonsingular is to expand $\det A$ directly and check whether the resulting expression, as a polynomial in $T$'s free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion $\det A = \sum_{|I|=|J|} \pm \det Q[I,J] \cdot \det T[R\setminus I, C\setminus J]$ has no cancellation between distinct terms, precisely because the nonzero entries of $T$ are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for $Q$, a nonzero-pattern-only matching argument for $T$). Missing this point — e.g. by treating $T$'s entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.

Formalization scope

Row and column index sets $R$, $C$ are general finite types (Fintype, with DecidableEq where needed for Finset operations), not fixed to $\mathrm{Fin}\ n$. No constant appears in any statement in this mission — every quantity (ranks, cardinalities, $\gamma$) is instance-dependent, so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly rectangular, cross-type-indexed) submatrix $M[I,J]$ is formalized as I.card = J.card together with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13 is computed the same way, via an arbitrary reindexing bijection between the row- and column-index subtypes — a choice that changes the determinant by at most a sign and hence never changes its degree. A formalization that replaced the genericity hypothesis on $T$ with mere distinctness of its nonzero entries would admit spurious cancellations in the determinant expansion and would not prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise, non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank, IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to mixed-matrix decompositions.

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 12.)
• Murota, K. Matrices and Matroids for Systems Analysis. Springer, 2000.
• Murota, K. "Systems Analysis by Graphs and Matroids: Structural Solvability and Controllability." Springer, 1987.
• König, D. "Gráfok és mátrixok" (Graphs and matrices). Matematikai és Fizikai Lapok 38, 1931, 116–119.
• Egerváry, J. "Matrixok kombinatorius tulajdonságairól" (On combinatorial properties of matrices). Matematikai és Fizikai Lapok 38, 1931, 16–28.

Motivation

This mission continues chapter 10's algorithmic account across its remaining two sections: finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity bounds; this mission places the results that are ordinary mathematical propositions.

Setting

The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F) and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq. (10.26)); this mission places the case-independent inequality its own legitimacy rests on, and restates its correctness conclusion. The steepest descent algorithm for an L-convex function g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the resulting monotonicity fact and a domain-size bound for the L$^\natural$-convex adaptation. Conjugate scaling replaces a dual-integral M-convex function's conjugate g with g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.

Formalization targets

Goal: Conjugate scaling preserves M-convexity (Proposition 10.41)

For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/ integer-dual conjugate of an L$^\natural$-convex g), the conjugate scaling f⟨α⟩ is again dual-integral M-convex, witnessed by g_α itself being L$^\natural$-convex, provided f⟨α⟩>-∞. Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work where a naive approach provably does not.

Supporting structural targets

Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission 34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct reading) bounds the L$^\natural$-convex adaptation's domain-size parameter in terms of the original function's.

Significance

Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own structure — completing the book's account of the M-convex submodular flow problem with an algorithm whose polynomial running time depends on exactly this compatibility. Propositions 10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular- minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32 are the analogous structural facts for L-convex function minimization, chapter 10's third major algorithmic thread.

None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR extraction demonstrably cannot distinguish the two visually different capacity-bound symbols (c* overlined vs. underlined) central to their shared defining formula, confirmed directly against the raw extracted bytes, making faithful reconstruction of that formula impossible from the available text; see HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions 10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type where the original was V-specific, since this draft cannot import that sibling. Proposition 10.26 is placed as the case-independent core inequality its own proof establishes, rather than by replicating the three-case verification against Proposition 10.24's own internal proof objects (Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25, 10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys are welcome; the goal carries the most independent proof content (via the conjugacy theorem and Theorem 7.10(2), both established elsewhere in this series).

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• S. Iwata, "A faster scaling algorithm for minimizing submodular functions," SIAM Journal on Computing, 32 (2003), pp. 833-840 [99] (conjugate scaling's origin).
• A. Frank, "A weighted matroid intersection algorithm," Journal of Algorithms, 2 (1981), pp. 328-336 [55] (the primal-dual framework this mission's Proposition 10.28 continues, via mission 34-ch10b-algorithms's own Proposition 10.24).

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

In one complex variable the Riemann mapping theorem classifies a whole class of domains by topology alone: every nonempty simply connected proper subdomain of $\mathbb{C}$ is biholomorphic to the unit disc. Nothing of the kind holds in several variables. The two most obvious generalizations of the disc to $\mathbb{C}^n$, the unit ball and the unit polydisc, are homeomorphic, yet no biholomorphic map carries one onto the other. This is the first result a student of several complex variables meets that has no one-variable shadow, and it is the standard illustration that the geometry of the boundary, not the topology of the domain, governs holomorphic equivalence.

As recounted in the source, Poincaré (1907) observed the inequivalence by computing the automorphism groups of $\mathbb{D}^2$ and $\mathbb{B}_2$, assuming the maps extend past the boundary; H. Cartan gave the first complete proof in 1931; and Rothstein (1935) proved that there is not even a proper holomorphic map from the bidisc to the ball. This mission follows the presentation in §1.4–1.6 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026), where the inequivalence is derived from a general theorem on proper maps out of product domains, followed by Cartan's uniqueness theorem and the basic structure theory of zero sets and injective maps.

Setting

Write $\mathbb{C}^n$ for $n$-tuples $z = (z_1, \dots, z_n)$ of complex numbers, $\mathbb{D} = \{\zeta \in \mathbb{C} : |\zeta| < 1\}$ for the unit disc, and $\|z\| = (|z_1|^2 + \cdots + |z_n|^2)^{1/2}$ for the Euclidean norm. The unit ball and unit polydisc are

$$\mathbb{B}_n = \{ z \in \mathbb{C}^n : |z_1|^2 + \cdots + |z_n|^2 < 1 \}, \qquad \mathbb{D}^n = \{ z \in \mathbb{C}^n : |z_k| < 1 \text{ for } k = 1, \dots, n \},$$

and the unit sphere is $S^{2n-1} = \partial\mathbb{B}_n = \{ z : |z_1|^2 + \cdots + |z_n|^2 = 1 \}$. A domain is a nonempty connected open set. A map between open subsets of complex spaces is holomorphic if it is complex differentiable at every point.

A continuous map $f : U \to V$ is proper if $f^{-1}(K)$ is compact for every compact $K \subset V$. A biholomorphic map $f : U \to V$ is a holomorphic bijection whose inverse is holomorphic; every biholomorphism is proper. An analytic disc is a nonconstant holomorphic map $\varphi : \mathbb{D} \to \mathbb{C}^n$, and a set $S$ contains no analytic discs if no analytic disc has $\varphi(\mathbb{D}) \subset S$. A circular domain is a domain $U$ with $e^{i\theta} z \in U$ whenever $z \in U$ and $\theta \in \mathbb{R}$.

Formalization targets

Goal: Rothstein's theorem (Theorem 1.4.4)

$$\text{there is no proper holomorphic map } f : \mathbb{D}^2 \to \mathbb{B}_2 .$$

The path to the goal

• Proposition 1.4.6. $S^{2n-1}$ contains no analytic discs.
• Lemma 1.4.7. For bounded domains $U \subset \mathbb{R}^n$, $V \subset \mathbb{R}^m$ and continuous $f : U \to V$: $f$ is proper if and only if, whenever $p_k \in U$ and $p_k \to p \in \partial U$, every limit point of $\{f(p_k)\}$ lies in $\partial V$.
• Theorem 1.4.8. If $U = U' \times U'' \subset \mathbb{C}^n \times \mathbb{C}^k$ ($n, k \ge 1$) and $V \subset \mathbb{C}^m$ are bounded domains and $\partial V$ contains no analytic discs, there is no proper holomorphic map $U \to V$.

Further results on the same definitions

• Theorem 1.5.1 (Cartan). If $U \subset \mathbb{C}^n$ is a bounded domain, $a \in U$, $f : U \to U$ holomorphic, $f(a) = a$ and $Df(a) = I$, then $f(z) = z$ on $U$.
• Corollary 1.5.2. A biholomorphism $f : U \to V$ of bounded circular domains with $f(0) = 0$ is the restriction of a linear map.
• Theorem 1.6.1 (Riemann extension). If $g \in \mathcal{O}(U)$ is not identically zero on a domain $U$ and $f \in \mathcal{O}(U \setminus g^{-1}(0))$ is locally bounded in $U$, then $f$ extends uniquely to some $F \in \mathcal{O}(U)$.
• Theorem 1.6.2. The zero set of a holomorphic function that is not identically zero on a domain is, on an open dense subset of itself, locally a graph $z_n = g(z_1, \dots, z_{n-1})$ after reordering the variables.
• Theorem 1.6.6. An injective holomorphic map $U \to \mathbb{C}^n$ on an open $U \subset \mathbb{C}^n$ has nowhere vanishing Jacobian determinant; a holomorphic bijection between open sets of $\mathbb{C}^n$ is biholomorphic.

The goal is chosen as the textbook's headline result of §1.4. Theorem 1.4.8 is strictly more general; it is a milestone, so a solver may prove the goal as its special case.

Significance

Rothstein's theorem implies the biholomorphic inequivalence of $\mathbb{B}_2$ and $\mathbb{D}^2$, the basic example that the Riemann mapping theorem has no analogue in several variables. Theorem 1.4.8 isolates the reason: a boundary that contains analytic discs cannot be mapped properly into a boundary that contains none. Cartan's uniqueness theorem and its corollary are the standard tools for computing automorphism groups of the ball and the polydisc. The Riemann extension theorem, the local graph structure of zero sets and the Jacobian criterion for injective maps are used throughout the theory of analytic varieties and of holomorphic mappings.

All of these results are classical and proved in the source. None of them is formalized in Mathlib or on the platform for $\mathbb{C}^n$ with $n \ge 2$: Mathlib has one-variable Riemann removable singularities and the maximum modulus principle, and the platform has one-variable results on injective holomorphic maps. This mission produces machine-checked statements of the several-variable versions, and infrastructure (proper maps between subsets, analytic discs, holomorphic families) that later chapters of the series reuse.

Difficulty

The goal cannot be reached through topology: $\mathbb{D}^2$ and $\mathbb{B}_2$ are homeomorphic, so any argument must use holomorphy essentially and must see the boundary. The step that needs genuine analysis is passing from properness, a statement about compact sets, to a statement about boundary values of holomorphic functions of one variable along slices of the product domain; this requires normal families (Montel's theorem) in several variables, which Mathlib does not provide in the needed form. Cartan's theorem rests on power-series expansions in homogeneous parts and vector-valued Cauchy estimates on polydiscs. Theorem 1.6.2 needs the holomorphic implicit function theorem and Rouché's theorem, and Theorem 1.6.6 an induction on dimension that runs through Theorem 1.6.2. The Riemann extension theorem needs holomorphy of parameter-dependent Cauchy integrals.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ. Mathlib's norm on this type is the sup norm, so Metric.ball 0 1 is the polydisc, not the ball. The ball and the sphere are therefore defined with the explicit Euclidean condition, unitBall n = {z | ∑ k, ‖z k‖ ^ 2 < 1} and unitSphere n = {z | ∑ k, ‖z k‖ ^ 2 = 1}. The polydisc is written coordinatewise as unitPolydisc n. Reading the ball as the sup-norm ball would trivialize the goal (the identity of the bidisc is a proper holomorphic self-map); the definitions exclude that reading. Boundedness is Bornology.IsBounded, and boundaries are Mathlib's frontier; neither depends on the norm. A domain is IsOpen U ∧ IsConnected U, so it is nonempty.

Holomorphic means DifferentiableOn ℂ on an open set. On open sets this is equivalent to the book's Definition 1.1.2 (Proposition 1.1.3 and Theorem 1.2.1). Maps into $\mathbb{C}^m$ are Fin m → ℂ-valued. $Df(a)$ is fderiv ℂ f a, and the Jacobian determinant is LinearMap.det of it. Maps are ambient functions whose values off the relevant set are irrelevant. Consequently:

• Proper is IsProperMapOn f U V: f maps U into V, is continuous on U, and U ∩ f ⁻¹' K is compact for every compact K ⊆ V. This is Definition 1.4.3 for the restricted map. It is not IsProperMap of the ambient map.
• Uniqueness in Theorem 1.6.1 is uniqueness on $U$.
• The inverse of a biholomorphism is a function g holomorphic on $V$ with Set.InvOn g f U V.

Lemma 1.4.7 works in Fin n → ℝ and reads "limit point of the sequence $\{f(p_k)\}$" as a cluster point of the sequence (MapClusterPt). Theorem 1.4.8 uses the product type (Fin n → ℂ) × (Fin k → ℂ) for $\mathbb{C}^n \times \mathbb{C}^k$. In Theorem 1.6.2, "after reordering the variables" means choosing the index j of the solved-for coordinate. The remaining coordinates are indexed by {i // i ≠ j}. Only the open-disc part of Definition 1.4.5 (analytic discs) is formalized, because closed analytic discs are not used here.

A complete development needs Montel's theorem for maps into bounded subsets of $\mathbb{C}^m$, homogeneous expansions and Cauchy estimates on polydiscs, the holomorphic implicit function theorem, Rouché's theorem, and holomorphic parameter-dependent Cauchy integrals. All of it is reusable beyond this mission, and contributions of it are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, §1.4–1.6 (pp. 32–46). https://www.jirka.org/scv/scv.pdf
• H. Poincaré, Les fonctions analytiques de deux variables et la représentation conforme, Rend. Circ. Mat. Palermo 23 (1907), 185–220. https://doi.org/10.1007/BF03013518
• S. G. Krantz, Function Theory of Several Complex Variables, 2nd ed., AMS Chelsea, 2001 (cited by Lebl as [K]). https://doi.org/10.1090/chel/340