All missions

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

• Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
• Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
• Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$, and costs are discounted by a factor $\nu \in [0,1)$: the cost at stage $t$ is $\nu^t c(i,a)$.

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$. No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$, so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$, the state distribution evolves as $\mu_0 = e_{i_0}$, $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$. The discounted cost is

$$C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).$$

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$. The robust Bellman operator $g$ and, for a stationary policy $\pi$, the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

$$g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).$$

The two values of the game are

$$\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).$$

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$, i.e.

$$v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}$$

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

$$\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).$$

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$, where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

1. Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$, the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$, every feasible $v$ satisfies $v \le v_\infty$, and $v_\infty$ is the unique optimizer when $q > 0$.
2. The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$-Lipschitz in $\|\cdot\|_\infty$.
3. (26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$.
4. (28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$.
5. (27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$.

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$-contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

• $C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
• Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
• The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$.
• The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
• $\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
• $C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$, so the series is summable and the tsum is the limit of the $N$-stage costs, the paper's definition.
• $\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$.
• Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$, whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
• Corrected statements:
  • Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$.
  • In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$.
  • The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
• Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
• Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$). Both are needed by the other missions of this series.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$, and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$. The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$, of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$, and integrally convex if $\bar f(x)$ can always be computed using only points from $x$'s own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$.

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

$$f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),$$

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$: every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$, a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of-$\alpha$) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
• F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

Motivation

A closed set $F\subseteq\mathbb R^n$ is flow-invariant for a dynamical system when every trajectory that starts in $F$ stays in $F$. Invariance of sets underlies state constraints in optimal control, safety certificates for controlled systems, comparison and maximum principles for differential equations, and the positivity of solutions of kinetic and population models. The question is always the same: which infinitesimal condition at the points of $F$ is equivalent to the global statement that trajectories cannot leave $F$?

For a smooth vector field and a smooth boundary the answer is that the field must not point strictly outward. For a nonsmooth set, such as a polyhedron, the positive orthant or a set with inward cusps, "pointing inward" must be made precise through a notion of tangent vector that works at corners. Frank H. Clarke's 1975 paper introduces the generalized gradient of a Lipschitz function and derives from it a normal cone and a tangent cone for arbitrary closed sets. Its Theorem (4.4) shows that this tangent cone is exactly the right notion: for a Lipschitz differential inclusion $\dot x\in X(x)$, a closed set is flow-invariant if and only if $X(x)$ is contained in the tangent cone at each point of the set.

Timeline:

• 1942. Nagumo characterizes invariance for continuous ODEs with unique solutions by a condition on the distance function (Proc. Phys.-Math. Soc. Japan 24).
• 1969. Bony proves an invariance theorem for Lipschitz vector fields, stated through exterior normals, in the course of a maximum principle for degenerate elliptic operators (Bony 1969).
• 1970. Brezis characterizes flow-invariant closed sets of a locally Lipschitz vector field by $\lim_{\delta\downarrow0} d_F(y+\delta X(y))/\delta=0$ (Brezis 1970).
• 1972. Redheffer gives simplified proofs of the Bony and Brezis theorems under weaker "uniqueness function" hypotheses (Amer. Math. Monthly 79, 740–747).
• 1975. Clarke extends the characterization to Lipschitz multifunctions with nonempty compact values, with tangency in the sense of his new tangent cone, and recovers Bony and Brezis as corollaries (Clarke 1975, Theorem (4.4), Corollaries (4.10), (4.12)).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $\zeta\cdot v$ and norm $|\cdot|$.

Generalized gradient. For $f:\mathbb R^n\to\mathbb R$ Lipschitz on bounded sets, $\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$ (Definition (1.1)). The generalized directional derivative is $f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}[f(x+h+\delta v)-f(x+h)]/\delta$ (Definition (1.3)).

Distance function. For a nonempty closed $E\subseteq\mathbb R^n$, $d_E(x)=\min\{|x-e|:e\in E\}$. It is Lipschitz with constant $1$. A point $e\in E$ with $|x-e|=d_E(x)$ is a closest point to $x$; it exists but need not be unique.

Normal and tangent cones. For $e\in E$, the cone of normals is

$$N_E(e)=\operatorname{cl}\{p:\ s\,p\in\partial d_E(e)\text{ for some }s>0\}\qquad\text{(Definition (3.1))},$$

and the tangent cone is its dual,

$$T_E(e)=\{\zeta:\ \zeta\cdot v\le0\text{ for all }v\in N_E(e)\}\qquad\text{(Definition (3.6))}.$$

Differential inclusions. A multifunction $X$ assigns to each $x\in\mathbb R^n$ a set $X(x)\subseteq\mathbb R^n$; standing assumption of §4: every $X(x)$ is nonempty and compact. A trajectory is an absolutely continuous $x:[0,1]\to\mathbb R^n$ with $\dot x(t)\in X(x(t))$ for almost every $t$ ((4.1)). $X$ is Lipschitz if there is $K$ such that for all $x_1,x_2$ and $v_1\in X(x_1)$ some $v_2\in X(x_2)$ has $|v_1-v_2|\le K|x_1-x_2|$ ((4.2)). A closed set $F$ is flow-invariant for $X$ if every trajectory with $x(0)\in F$ has $x(t)\in F$ for all $t\in[0,1]$ ((4.3)).

Formalization targets

Goal: Theorem (4.4)

Let $X$ be a Lipschitz multifunction with nonempty compact values and $F$ a nonempty closed subset of $\mathbb R^n$. Then

$$F\text{ is flow-invariant for }X\iff X(x)\subseteq T_F(x)\ \text{ for every }x\in F.$$

Milestones, in the order the proof uses them

1. Proposition (1.4). $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$.
2. Proposition (2.4). If $\nabla d_E(x)$ exists and is nonzero, then $x\notin E$, $x$ has a unique closest point $e$, and $\nabla d_E(x)=(x-e)/|x-e|$.
3. Corollary (2.5). For $e\in E$, $\partial d_E(e)=\operatorname{co}\{0,\lim (x_i-e_i)/|x_i-e_i|\}$ over $x_i\notin E$, $x_i\to e$, $e_i$ closest to $x_i$.
4. Proposition (3.2). $N_E(e)=\operatorname{cl}\operatorname{co}\{\lim s_i(x_i-e_i)\}$ over $s_i\ge0$, $x_i\to e$, $e_i$ closest to $x_i$.
5. Inequality (4.8). If $X(y)\subseteq T_F(y)$ on $F$ and $x$ is a trajectory, then $f(t)=d_F(x(t))$ satisfies $f'(t)\le Kf(t)$ almost everywhere.
6. Limit (4.9). If $F$ is flow-invariant, then $d_F(y+\delta v)/\delta\to0$ as $\delta\downarrow0$ for every $y\in F$ and $v\in X(y)$.
7. Proposition (3.7). $v\in T_E(e_0)$ iff $\lim_{e\to e_0,\,e\in E}\liminf_{\delta\downarrow0} d_E(e+\delta v)/\delta=0$.

Significance

The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on $F$ that can be checked without solving anything. It is the prototype of the strong invariance theorems of nonsmooth control theory, later developed in viability theory and in the monograph of Clarke, Ledyaev, Stern and Wolenski, and it is the tool behind state-constrained optimal control and Lyapunov-type arguments for nonsmooth systems. Its corollaries recover the Bony and Brezis theorems for Lipschitz vector fields. The companion milestones (2.5), (3.2) and (3.7) are standalone facts of nonsmooth geometry: the Clarke normal cone is generated by limits of proximal normals, and Clarke tangency can be tested along rays from nearby points of the set.

Formalizing it. The result is proved in the paper and has been reproved in textbooks; to the best of our knowledge it has no machine-checked proof. Mathlib contains Rademacher's theorem, absolutely continuous functions on intervals and the Bouligand tangent cone, but no Clarke generalized gradient, no Clarke normal or tangent cone, and no theory of differential inclusions. A complete development supplies a first nonsmooth-analysis layer on top of Mathlib and a first existence theorem for Lipschitz differential inclusions.

Difficulty

The direction (2) $\Rightarrow$ (1) looks like a Gronwall argument for $f(t)=d_F(x(t))$, but $d_F$ is not differentiable, $x$ is only absolutely continuous, and the closest point to $x(t)$ can jump. The step that must be controlled is the comparison between $\dot x(t)$, a nearby admissible velocity at the closest point, and the normal $x(t)-y$; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.

The direction (1) $\Rightarrow$ (2) needs a trajectory through an arbitrary $y\in F$ whose initial velocity is a prescribed $v\in X(y)$. For a nonconvex multifunction this is Filippov's theorem [7, Theorem 5], which the paper cites and does not prove. A solver must prove it, or an equivalent existence result for Lipschitz inclusions with compact values, from scratch in Lean. The Clarke tangent cone and the more familiar Bouligand (contingent) cone differ pointwise at nonconvex corners, so a statement written with Mathlib's tangentConeAt is a different theorem from (4.4). That the two universal conditions "$X(x)\subseteq T_F(x)$ for all $x\in F$" are equivalent for Lipschitz $X$ is a later, separate result and cannot be assumed.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $d_E$ is Metric.infDist · E; "$e$ is a closest point to $x$" is e ∈ E ∧ dist x e = infDist x E.
• $\partial f$ and $f^\circ$ follow Definitions (1.1) and (1.3). The gradient limits carry DifferentiableAt, because Mathlib's gradient is $0$ off the differentiability set. $f^\circ$ is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.
• $N_E$ and $T_E$ are defined from $\partial d_E$ as in (3.1) and (3.6). The tangent cone is not Mathlib's tangentConeAt.
• A trajectory is x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every $t\in[0,1]$, ∃ w ∈ X (x t), HasDerivAt x w t. Values outside $[0,1]$ are irrelevant.
• Standing assumptions made explicit: $X(x)$ nonempty and compact for every $x$ (§4, p. 259); $E$, $F$ nonempty and closed and $e\in E$ (§3, p. 254); $f$ Lipschitz on bounded sets (§1, p. 247). The Lipschitz constant of (4.2) is global.
• Ruled out: dropping absolute continuity (Cantor-type curves would leave $F$), using deriv in (4.1), using a punctured filter in (3.7), which would make (3.7)(2) hold at isolated points, and assuming Filippov's theorem as a hypothesis of (4.9) or of the goal.
• Needed infrastructure: the Clarke calculus for $d_E$, a chain-rule-type estimate for $d_F\circ x$ along absolutely continuous curves, a Gronwall lemma for absolutely continuous functions (Mathlib has norm_le_gronwallBound_of_norm_deriv_right_le for the differentiable case), and Filippov's existence theorem. The generalized gradient, cones and trajectory notions are reusable by any nonsmooth-optimization or control mission. Contributions of any of these as separate lemmas are welcome.
• The §1 definitions duplicate those of the companion mission Generalized Gradients and Applications I; the two missions were drafted at the same time.

Selected references

• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
• A. F. Filippov, Classical solutions of differential equations with multivalued right-hand side, SIAM J. Control 5 (1967), 609–621. https://doi.org/10.1137/0305040
• H. Brezis, On a characterization of flow-invariant sets, Comm. Pure Appl. Math. 23 (1970), 261–263. https://doi.org/10.1002/cpa.3160230211
• J. M. Bony, Principe du maximum, inégalité de Harnack et unicité du problème de Cauchy pour les opérateurs elliptiques dégénérés, Ann. Inst. Fourier 19 (1969), 277–304. https://doi.org/10.5802/aif.319
• R. M. Redheffer, The theorems of Bony and Brezis on flow-invariant sets, Amer. Math. Monthly 79 (1972), 740–747. MR 46 #2166.
• F. H. Clarke, Yu. S. Ledyaev, R. J. Stern, P. R. Wolenski, Nonsmooth Analysis and Control Theory, Graduate Texts in Mathematics 178, Springer, 1998. https://doi.org/10.1007/b97650

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

• Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
• Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
• Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
• Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$. A point system is a finite set $S \subseteq \mathbb{R}^n$. It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$. A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$. A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$. A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$.

Read as inequalities $(a \xi) \ge 0$, $a \in S$, the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$, one for each extreme solution $\alpha$, and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$, identified with $\mathbb{R}^m$, $m = n-1$. A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$. Given a finite index set $J$, normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$, the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

$$H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.$$

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$, with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$.

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ($A_j \ne 0$ or $b_j \ne 0$). Then

$$H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).$$

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

1. Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$, every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$.
2. Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$.
3. Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$, then $p$ is a nonnegative combination of $S$. This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
4. Satz 6, p. 297: for non-degenerate $S$, $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$.
5. §3 II, p. 298: for non-degenerate $S$, every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
6. Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
7. §4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$: positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$. Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

• The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
• Non-degeneracy is the literal condition "$(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$", not span = ⊤.
• Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
• Extreme solutions are required to be nonzero and to lie in $(S)$. This is implicit in the paper.
• §4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$. Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
• A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
• Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$, p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
• Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
• A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$, $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
• Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$. Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
• H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
• J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$. In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$. The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

$$U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.$$

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$, and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$. The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$, $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

$$U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},$$

with $\min$ read, as in the paper, "in the wide sense of $\inf$", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$.

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$. Its expected utility is the two-point objective (8),

$$U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).$$

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$; the set of their coefficients is $\mathcal Q$. Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$, each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$.

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$.

(a) If $u'$ is convex, then

$$U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.$$

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$.

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$. When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$.

Milestones

1. Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$.
2. For convex $u'$ and $s>0$, $U(p)$ is nonincreasing on $(0,1)$.
3. Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$, including the value $-\infty$.
4. Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$.
5. The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
6. Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$, and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$.

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$.

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ($u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$. With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$, a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "$\lim_{y\to-\infty}u'(y)=\infty$" fails for affine $u$, where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$, gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$. Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$, a second-order asymptotic statement about $u$ at $-\infty$. The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$; showing that it lies below $u$ everywhere, not only near $m$, is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$. The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$. Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$. Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$, since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$. The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$, the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
• S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.