Convex Optimization

Motivation

A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).

The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.

Setting

Let $m,n$ be positive integers and $(\Omega,P)$ a probability space. A fixed real $m\times n$ matrix $A$ has rows $a_i'$. Random vectors $b:\Omega\to\mathbb R^m$ and $c:\Omega\to\mathbb R^n$ give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule $x=Db$, where the real $n\times m$ matrix $D$ is chosen before $b$ is realized. Write $\mu_b=E[b]$ and $\mu_c=E[c]$. A number $z_0$ is the given aspiration value. For each row $i$, its reliability level $\alpha_i$ is strictly between $1/2$ and $1$, and $K_i=\Phi^{-1}(\alpha_i)>0$ is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.

The residual $a_i'Db-b_i$ has raw second moment $\sigma_i^2(D)=E[(a_i'Db-b_i)^2]$ and negative mean $\mu_i(D)=\mu_{b_i}-a_i'D\mu_b$. The aspiration error has raw second moment $V(D)=E[(c'Db-z_0)^2]$. These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is $\mu_c'D\mu_b$; the model records the paper's assumption that the components of $b$ and $c$ are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.

Program (38) chooses $(D,v,v_0,w_0)$ and maximizes $v_0/w_0$. Its inequalities bound the mean objective below by $z_0+v_0$, bound $w_0$ below by the root-mean-square aspiration error, and bound each nonnegative $v_i$ between the row's risk term and $\mu_i(D)$. The denominator satisfies $w_0>0$. Program (39) introduces a nonnegative scale $t$ and barred variables. It fixes $\bar w_0=1$ and maximizes the linear objective $\bar v_0$. The barred moments are calculated from $\bar D$ and $t$ by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.

Formalization targets

Convex transformed program

Let $F_{39}$ contain every point satisfying all of (39), including $t=0$. The paper's convex-programming claim becomes

$$F_{39}\text{ is convex}.$$

The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.

Equal optimal values

Let $F_{38}$ be the feasible set of (38). Provided $F_{38}$ is nonempty, the mission goal states that the normalized substitution sends each point of $F_{38}$ to a point of $F_{39}$ with the same objective, and that

$$\sup_{(D,v,v_0,w_0)\in F_{38}}\frac{v_0}{w_0} =\sup_{(\bar D,\bar v,\bar v_0,\bar w_0,t)\in F_{39}}\bar v_0.$$

The suprema may be infinite. The equality concerns the complete program (39), including $t=0$. Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.

Significance

The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at $t=0$ occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.

The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.

Difficulty

The pointwise substitution $t=1/w_0$ only reaches points of (39) with $t>0$, while (39) explicitly permits $t=0$. Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: $\bar\sigma_i^2$ is a raw second moment and $\bar\mu_i^2$ is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.

Formalization scope

Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure $P$, and Bochner integrals for the moments. Square integrability is stated for every component of $b$ and $c$ and every product $c_jb_k$; this keeps the expected squares meaningful. The paper assumes $b$ and $c$ are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile $K_i$ is imported from the published Cohen2019.Robust.PhiInvReal, with $1/2<\alpha_i<1$ excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.

The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization $\bar w_0=1$, strict $w_0>0$, and weak $t\ge0$ are separate conditions. The $t=0$ slice is included, and the main theorem assumes $F_{38}$ nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, pp. 18–39. DOI.
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4), 1962, pp. 181–186. DOI.
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 1962, pp. 16–24. DOI.
• J. Cohen, E. Rosenfeld, and Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML, 2019. arXiv.

Motivation

A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition $A$ of players is assigned the set $V(A)$ of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.

Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.

Setting

The players are $N = \{1,\dots,n\}$. A coalition $A \subseteq N$ is identified with its characteristic vector $\tau^A \in \{0,1\}^n$, and $\tau^N = (1,\dots,1)$. A fuzzy coalition is a vector $\tau \in [0,1]^n$ of participation rates with support $A_\tau = \{i : \tau_i > 0\}$. Write $(\tau\cdot c)_i = \tau_i c_i$, $\mathbb{R}^\tau = \tau\cdot\mathbb{R}^n$ for the vectors vanishing off $A_\tau$, $\mathbb{R}^\tau_+$ for its nonnegative part, and $\mathring{\mathbb{R}}^\tau_+$ for the vectors strictly positive on $A_\tau$.

A fuzzy game without side payments assigns to each $\tau \ge 0$ a nonempty, closed, convex set $V(\tau)\subseteq\mathbb{R}^\tau$. Each $V(\tau)$ is comprehensive, meaning $V(\tau) = V(\tau)-\mathbb{R}^\tau_+$, and bounded above, meaning $V(\tau)\subseteq C-\mathbb{R}^\tau_+$ for some $C$. The map is positively homogeneous: $V(t\tau) = tV(\tau)$ for every $t>0$. Its core is the set of $c\in V(\tau^N)$ such that $\tau\cdot c\notin V(\tau)-\mathring{\mathbb{R}}^\tau_+$ for every fuzzy coalition $\tau\neq 0$. With the support function $v(\tau,\lambda)=\sup_{c\in V(\tau)}\sum_i\lambda_i c_i$ and the simplex $M^n$, a weak (resp. strong) canonical cooperative equilibrium is a $c\in V(\tau^N)$ together with a $\bar\lambda\in M^n$ (resp. $\bar\lambda$ with all coordinates positive) satisfying $\sum_i\bar\lambda^i\tau_ic_i\ge v(\tau,\bar\lambda)$ for every $\tau\in[0,1]^n$.

A usual NTU game lives on a family $\mathcal{C}$ of coalitions that contains $N$ and every singleton. For each $A\in\mathcal{C}$, the set $V(A)\subseteq\mathbb{R}^A$ is nonempty, closed, convex, comprehensive and bounded above. A balance of $\tau$ is a vector of weights $m\ge 0$ on $\mathcal{C}$ with $\sum_{A\ni i}m(A)=\tau_i$ for every $i$, and $\mathcal{C}(\tau)$ is the set of balances of $\tau$. The fuzzy extension of the game is

$$\pi V(\tau)=\bigcup_{m\in\mathcal{C}(\tau)}\ \sum_{A\in\mathcal{C}} m(A)\,V(A),$$

and the game is balanced if $V(N)=\pi V(\tau^N)$.

Formalization targets

Goal: Theorem 7.1

For a balanced game without side payments,

$$\emptyset\neq\operatorname{core}(\pi V)\subseteq\operatorname{core}(V),\qquad \mathrm{CCE}_{\rm strong}(V)\subseteq\operatorname{core}(\pi V)\subseteq\mathrm{CCE}_{\rm weak}(V),$$

and in particular $\operatorname{core}(V)\neq\emptyset$.

Milestones

• Proposition 3.1: $c\in V(\tau^N)$ is in the core iff the maximum complaint $\alpha(c)=\sup_{\tau\neq0}\inf_{\lambda\in M^\tau}[v(\tau,\lambda)-\sum_i\lambda^i\tau_ic_i]$ is $\le 0$.
• Proof of Theorem 3.1(b): if $V$ is superadditive, $V(\tau)+V(\sigma)\subseteq V(\tau+\sigma)$, then $\tau\mapsto v(\tau,\lambda)$ is concave on $\mathbb{R}^n_+$.
• Theorem 3.1: strong equilibria lie in the core, and for a superadditive game the core lies in the set of weak equilibria.
• Theorem 5.1: a superadditive fuzzy game has a nonempty core.
• §7, (6), (7), (11): $\pi V$ is a superadditive fuzzy game that extends $V$, and its support function is $\pi v(\tau,\lambda)=\sup_{m\in\mathcal{C}(\tau)}\sum_A m(A)v(A,\lambda)$.
• §7 and the proof of Theorem 7.1: under balancedness, $\operatorname{core}(\pi V)\subseteq\operatorname{core}(V)$, and the equilibria of $V$ coincide with those of $\pi V$.

Significance

Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer $\bar\lambda$, that sandwiches the core.

The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.

Difficulty

Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each $\tau\in[0,1]^n$, so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map $\tau\mapsto v(\tau,\lambda)$ at $\tau^N$, Ky Fan's inequality on a truncated simplex where all $\lambda_i\ge\varepsilon$, and a limit as $\varepsilon\to0$. That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in $\tau$ and convex and lower semicontinuous in $\lambda$. Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.

Formalization scope

All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.

• Players are Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. $\mathbb{R}^\tau$ is encoded as "vanishes where $\tau_i=0$", which equals $\tau\cdot\mathbb{R}^n$ for $\tau\ge0$.
• Fuzzy games are defined directly on the orthant $\tau\ge0$, the paper's extension of $V$ from $[0,1]^n$ by homogeneity. Homogeneity holds for every $t>0$, and superadditivity holds on $\mathbb{R}^n_+$.
• Support functions, $\alpha$ and $\pi v$ take values in EReal, so an unbounded supremum is $+\infty$ and never a junk $0$.
• The supremum defining $\alpha(c)$ ranges over $\tau\neq0$. Since $M^0=\emptyset$, including $\tau=0$ would make $\alpha\equiv+\infty$ and Proposition 3.1 false. Blocking coalitions are likewise $\tau\neq0$, as in §3 (4).
• $\mathcal{C}$ is a finite family of nonempty coalitions that contains $N$ and every singleton. "$\forall A\neq\emptyset$" in §7 ranges over $\mathcal{C}$.
• The paper leaves $n\ge1$ implicit. Theorem 3.1(b) and Theorem 5.1 carry $0<n$: for $n=0$ the simplex is empty while the core is not.
• In §7 (11), $\pi v(\tau,\lambda)$, which the paper uses without defining it, is taken to be the extension §6 (2) applied to $A\mapsto v(A,\lambda)$, for $\lambda\ge0$.
• The §7 sentence after (5) is stated with two extra conclusions: $\pi V(\tau)$ is nonempty and contained in $\mathbb{R}^\tau$. These are the remaining requirements of §3 (3) that are needed to apply Theorem 5.1.
• Sums and scalings of sets are Mathlib's pointwise operations.

The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about $\pi V$ do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: $V(\tau)=\{c\in\mathbb{R}^\tau: c\le\tau\}$ is a superadditive fuzzy game, and $V(A)=\{c\in\mathbb{R}^A:c\le\tau^A\}$ is a balanced game on every admissible $\mathcal{C}$, with $(1,\dots,1)$ in both cores.

Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• H. E. Scarf, The Core of an N Person Game, Econometrica 35(1) (1967) 50–69. https://doi.org/10.2307/1909888
• L. J. Billera, Some Theorems on the Core of an n-Person Game without Side-Payments, SIAM Journal on Applied Mathematics 18(3) (1970) 567–579. https://doi.org/10.1137/0118053
• K. Fan, A Minimax Inequality and Applications, in O. Shisha (ed.), Inequalities III, Academic Press (1972) 103–113.

Motivation

In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.

The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor $3/2$. When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio $2n^{3/2}$.

Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on $K$. Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio $n$, but not by a polynomial algorithm for varying $n$; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$, and write $B(p, \rho) = \{x \in \mathbb R^n : |x - p| \le \rho\}$ for the closed ball. For points $w_0, \dots, w_n \in \mathbb R^n$, the simplex volume is

$$\mathrm{vol}(w_0, \dots, w_n) = \frac{|\det M|}{n!},$$

where $M$ has column vectors $w_1 - w_0, \dots, w_n - w_0$.

Let $K \subseteq \mathbb R^n$ be convex, and let $v_0, \dots, v_n \in K$ with $v_1 - v_0, \dots, v_n - v_0$ linearly independent. Choose linear functions $g_0, \dots, g_n : \mathbb R^n \to \mathbb R$ with

$$g_i \text{ constant on } \{v_j : j \ne i\}, \qquad g_i(v_i) \ne g_i(v_j) \ (j \ne i). \tag{15}$$

Thus $g_i$ measures the height above the facet opposite $v_i$. The stopping condition of the second stage is

$$|g_i(x - v_j)| \le \tfrac32\, |g_i(v_i - v_j)| \quad \text{for all } x \in K \text{ and all } i \ne j. \tag{16}$$

The ratio $|g_i(x - v_j)|/|g_i(v_i - v_j)|$ is the factor by which the volume changes when $v_i$ is replaced by $x$, so (16) says that no such swap enlarges the simplex by more than $3/2$.

Let $\tau$ be a nonsingular linear map of $\mathbb R^n$ such that $z_j = \tau(v_j)$ span a regular simplex, meaning that all distances $|z_i - z_j|$, $i \ne j$, are equal. Let $p = (n+1)^{-1}\sum_j z_j$ be its centroid and $S$ its convex hull. For $c \ge 1$, the paper defines

$$T_c = \{x \in \mathbb R^n : \mathrm{vol}(z_0, \dots, z_{i-1}, x, z_{i+1}, \dots, z_n) \le c\cdot \mathrm{vol}(z_0, \dots, z_n) \text{ for all } i\}.$$

The proof of the LEMMA works in model coordinates. There $\mathbb R^n$ is the hyperplane $\sum_{j=0}^n r_j = 1$ of $\mathbb R^{n+1}$, the $z_j$ are the standard basis vectors, $p = (\tfrac1{n+1}, \dots, \tfrac1{n+1})$, and $T_c = \{r : |r_j| \le c \text{ for all } j,\ \sum_j r_j = 1\}$.

Formalization targets

Goal (§2, p. 543)

Under (15) and (16), with $\tau$ making the simplex regular and $p$ its centroid, there are positive reals $r, R$ with

$$B(p, r) \subseteq \tau K \subseteq B(p, R), \qquad \frac{R}{r} \le 2n^{3/2}.$$

These are conditions (3)–(4) of §1 with $c_1 = 2n^{3/2}$.

Milestones, in the order the proof uses them

1. (16) is a statement about $T_{3/2}$ (p. 543). Condition (16), for all $x \in K$ and $i \ne j$, holds exactly when $\tau K \subseteq T_{3/2}$.
2. Vertices of $T_c$ (pp. 543–544). In the model, $T_c$ is the convex hull of the coordinate permutations of $e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m$), or of $(1-c)e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m+1$).
3. Outer radius (p. 544). $T_c \subseteq B(p, R)$ with $R^2 = nc^2 + \tfrac{n}{n+1}$ ($n$ even) or $(n+1)c^2 - 2c + \tfrac{n}{n+1}$ ($n$ odd).
4. Inner radius (p. 544). $B(p, r) \subseteq S$ inside the hyperplane, with $r^2 = \tfrac{1}{n(n+1)}$.
5. LEMMA (p. 543). For $c \ge 1$ and any regular simplex, $B(p, r) \subseteq S \subseteq T_c \subseteq B(p, R)$ for positive $r, R$ with

$$\Big(\frac Rr\Big)^2 = \begin{cases} c^2n^3 + (c^2+1)n^2 & n \text{ even},\\ c^2n^3 + (2c^2 - 2c + 1)n^2 + (c^2 - 2c)n & n \text{ odd}.\end{cases}$$

The paper's own proof derives the goal from milestone 1 and the LEMMA at $c = 3/2$. At $n = 1$ the constant $2n^{3/2}$ cannot be improved by this argument.

Significance

The result. The theorem is the only place in the paper where the roundness constant $c_1$ is computed, and $c_1$ enters the bound $1 + c_1c_2\sqrt n$ on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of $c$ to obtain $c_1 = ((1+\epsilon)(n^3 + 2n^2))^{1/2}$ ($n$ even) and $((1+\epsilon)(n^3+n^2-n))^{1/2}$ ($n$ odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume-$c$ neighbourhood" $T_c$ of a regular simplex extends.

The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor $n$, by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.

Difficulty

There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map $\tau$. The second is the transfer to the model. The paper's "similarity transformation" identifies $\mathbb R^n$ with a hyperplane of $\mathbb R^{n+1}$ and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and $T_c$ must all be carried across this isometry up to scaling. The LEMMA is stated in $\mathbb R^n$, not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and the model $\mathbb R^{n+1}$ is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching $0, \dots, n$.
• The volume keeps the paper's normalisation $|\det M|/n!$. $T_c$ is defined from volumes exactly as on p. 543, not from barycentric coordinates.
• Readings of loose phrases. "Nonsingular endomorphism" is a linear equivalence. "Span a regular $n$-simplex" means all pairwise distances are equal and positive. "Certain/two positive real numbers $r, R$" is an existential with $0 < r$ and $0 < R$ in the conclusion; without them, $R/r$ with $r = 0$ would be $0$ in Lean. The LEMMA keeps the printed equality for $(R/r)^2$. (15) is two hypotheses on $g$, and (16) is quantified over all $x \in K$ and all pairs $i \ne j$.
• Generalizations, all harmless. The paper's $K$ is a bounded polyhedron and the $v_j$ are vertices; the claim is stated for any convex $K$ and any points $v_j \in K$, and boundedness of $K$ follows from (16). Milestone 1 holds for any set $K$. The LEMMA is stated for any regular simplex, since $\tau$ plays no role in it.
• $n \ge 1$ throughout. In the model, the ball of milestone 4 is intersected with the hyperplane $\sum_j x_j = 1$, the paper's $\mathbb R^n$. The full ball of $\mathbb R^{n+1}$ is not inside $S$.
• No trivializing formalization is possible: the hypotheses are satisfiable (checked at $n = 1$, $K = [0,1]$), the radii are positive, and the sets are computed from the data rather than assumed.
• Useful infrastructure, reusable beyond this mission: the volume of a simplex with one vertex replaced, as a multiple of a barycentric coordinate; existence and properties of regular simplices in $\mathbb R^n$; the isometric embedding of a regular simplex onto the standard simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• H. W. Lenstra, Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
• A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979) 191–194.
• R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.

D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.

Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.

Setting

Fix $n, m \in \mathbb N$, a vector $a \in \mathbb R^n$, a symmetric positive definite $n\times n$ matrix $G$, an $n\times m$ matrix $C$ with columns $n_1,\dots,n_m$, and $b \in \mathbb R^m$. The quadratic program (1.1) is

$$\min_x\ f(x) = a^{\mathsf T}x + \tfrac12 x^{\mathsf T}Gx \quad\text{subject to}\quad s_i(x) = n_i^{\mathsf T}x - b_i \ge 0,\quad i \in K = \{1,\dots,m\}.$$

The gradient is $g(x) = Gx + a$. For $J \subseteq K$, the subproblem $P(J)$ keeps only the constraints indexed by $J$; $P(\emptyset)$ is solved by $x^0 = -G^{-1}a$. A set $A \subseteq K$ is linearly independent if the normals $n_i$, $i\in A$, are.

For an independent $A$, let $N$ be the matrix with columns $n_i$, $i\in A$, and define

$$N^* = (N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1},\qquad H = G^{-1} - G^{-1}N(N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1}.$$

The multipliers are $u(x) = N^*g(x)$; for a constraint $p \notin A$ with normal $n^+ = n_p$ the infeasibility multipliers are $r = N^*n^+$; a superscript $+$ denotes the same objects for $A^+ = A\cup\{p\}$.

An S-pair $(x, A)$ is an independent active set $A$ with $s_i(x) = 0$ for $i\in A$ and $x$ optimal for $P(A)$. A V-triple $(x, A, p)$ has $p\notin A$, $A^+$ independent, $s_p(x) < 0$, $s_i(x) = 0$ for $i \in A$, $H^+g(x) = 0$ and $u^+(x) = (N^+)^*g(x) \ge 0$.

The dual algorithm starts from $(x^0, \emptyset)$. In Step 1 it stops if $x$ is feasible; otherwise it picks any violated constraint $p$. In Step 2 it moves along the primal direction $z = Hn^+$ and the dual direction $(-r; 1)$ with step $t = \min\{t_1, t_2\}$, where $t_1$ is the largest step that keeps the multipliers nonnegative and $t_2 = -s_p(x)/z^{\mathsf T}n^+$ makes constraint $p$ active. If both are infinite it reports infeasibility. A full step ($t = t_2$) adds $p$ and returns to Step 1. A partial step ($t = t_1 < t_2$), or a dual step ($z = 0$), drops a constraint $k$ attaining $t_1$ and repeats Step 2.

Formalization targets

Goal: Theorem 3 (p. 11)

For every choice of the violated constraint $p$ and of the dropped constraint $k$:

$$\text{no run from } (x^0,\emptyset) \text{ is infinite, and every run that cannot continue ends in } \begin{cases}\text{STOP at an optimal } x \text{ of (1.1)}, \text{ or}\\ \text{STOP with } \{x : C^{\mathsf T}x \ge b\} = \emptyset.\end{cases}$$

Milestones, in attack order

1. Properties (2.6)–(2.9) (p. 5): $Hw = 0 \iff w \in \operatorname{range} N$; $H \succeq 0$; $HGH = H$; $N^*GH = 0$.
2. Optimality conditions (2.3)–(2.4) (p. 5): on the manifold of $A$, $x$ solves $P(A)$ iff $N^*g(x) \ge 0$ and $Hg(x) = 0$.
3. Lemma 1 (p. 8): along $\bar x = x + tHn^+$ from a V-triple, $H^+g(\bar x) = 0$, the constraints of $A$ stay active, $u^+(\bar x) = u^+(x) + t(-r;1)$ and $s_p(\bar x) = s_p(x) + t\,z^{\mathsf T}n^+$.
4. Theorem 1 (pp. 8–9): the step $t = \min\{t_1,t_2\}$ increases $s_p$ and $f$; a partial step yields a V-triple, a full step an S-pair.
5. Theorem 2 (p. 10): if $n_p = Nr$ and $s_p(x) < 0$ at an S-pair, then $r \le 0$ means $P(A\cup\{p\})$ is infeasible; otherwise dropping a minimizing $k$ gives a V-triple.
6. One round of Step 2 (p. 11): from an S-pair and a violated $p$, at most $|A|$ partial or dual steps and one final step end either in infeasibility of (1.1) or in a new S-pair $(\bar x, \bar A \cup\{p\})$ with $\bar A\subseteq A$ and $f(\bar x) > f(x)$.

Significance

Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for $N^*$ and $H$, a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.

Difficulty

The obvious termination argument is that $f$ increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave $x$ unchanged (the dual steps of Step 2(c)(ii)), so $f$ is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move $x$. Any such argument relies on invariants (independence of $A^+$, nonnegativity of the multipliers, $s_p < 0$ along partial steps) that hold only on reachable states, and the operators $N^*$ and $H$ are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.

Formalization scope

Vectors are Fin n → ℝ, $G$ is Matrix (Fin n) (Fin n) ℝ with G.PosDef, $C$ is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in $A$. Lean's matrix inverse returns $0$ for singular matrices, so every statement about $N^*$ and $H$ assumes $G \succ 0$ and an independent active set (directly, or through an S-pair or V-triple).

The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of $p$ and $k$. Infinite step lengths are separate transitions; a tie $t_1 = t_2$ takes the full step, as the paper tests $t = t_2$ first. The running value of $f$ and the factorizations of Section 4 are not part of the state.

Explicit readings of the paper's words:

• "solves the QPP or indicates infeasibility in a finite number of steps" is: no infinite sequence of Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);
• "S-pair" is: $A$ independent and active at $x$, with $x$ optimal for $P(A)$ (the reading every use in the paper needs);
• in Theorem 1 the partial-step clause carries $t < t_2$ (as in its proof), and the multiplier printed $u^+_{j+1}$ in (3.16) is $u^+_{q+1}$, the entry belonging to $p$;
• "an S-pair can never reoccur" is expressed as the strict increase $f(\bar x) > f(x)$ in milestone 6.

Property (2.10), printed $HH^+ = H^+$, is false unless $G = I$ and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.

A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.

Needed infrastructure: Schur-complement and projector identities for $N^*$ and $H$; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about $N^*$ and $H$, are welcome.

Selected references

• D. Goldfarb and A. Idnani, A numerically stable dual method for solving strictly convex quadratic programs, Mathematical Programming 27 (1983) 1–33. https://doi.org/10.1007/BF02591962
• C. E. Lemke, A method of solution for quadratic programs, Management Science 8 (1962) 442–453. https://doi.org/10.1287/mnsc.8.4.442
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006, Chapter 16. https://doi.org/10.1007/978-0-387-40065-5

Dual decomposition of dominance constraints

A stochastic dominance constraint asks a random outcome $X$ of a decision to be at least as good as a benchmark outcome $Y$ for every risk-averse decision maker: in the second-order version, $\mathbb E[u(X)] \ge \mathbb E[u(Y)]$ for every concave nondecreasing utility $u$. Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes $X_i = G_i(z)$ that depend nonlinearly on a decision $z$.

The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the $i$-th dominance constraint are a utility function $u_i$ and an almost-sure multiplier $\theta_i$ for the coupling $X_i = G_i(z)$. The dual functional splits into a part $D_0$ that involves only the decision $z$ and one part $D_i$ per dominance constraint. This mission is about the second kind of part: Theorem 4 computes $D_i$ in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.

The underlying shortfall function $F_2(X;\eta)=\int_{-\infty}^{\eta}P[X\le\alpha]\,d\alpha$ and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $\mathcal L_1$ the integrable and $\mathcal L_\infty$ the essentially bounded random variables. Fix a bounded interval $[a,b]$ ($a\le b$) and a reference outcome $Y\in\mathcal L_1$.

The utility class $\mathcal U_1([a,b])$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge 0$. For such $u$, the left derivative $u'_-(a)$ at $a$ is that slope $c$.

The concave conjugate of $v:\mathbb R\to\mathbb R$ is

$$v^*(\xi)=\inf_{t\in\mathbb R}\,[\xi t-v(t)]\in[-\infty,+\infty).$$

For a random variable $\zeta$, $v^*(\zeta)$ is the extended-real random variable $\omega\mapsto v^*(\zeta(\omega))$.

The dual functional of one dominance constraint, eq. (34), is

$$D(w,\zeta)=\sup_{X\in\mathcal L_1}\mathbb E\big[w(X)-w(Y)-\zeta X\big]\in\overline{\mathbb R},\qquad w\in\mathcal U_1([a,b]),\ \zeta\in\mathcal L_\infty .$$

The functional of eq. (35) is $f(v,\zeta)=-\mathbb E\,v^*(\zeta)$, considered on $\mathrm{Lip}(\mathbb R)\times\mathcal L_1$, where $\mathrm{Lip}(\mathbb R)$ is the space of Lipschitz functions with norm $\|v\|_{\mathrm{Lip}}=|v(0)|+\sup_{t\ne s}|v(t)-v(s)|/|t-s|$.

Formalization targets

Goal: Theorem 4

For every $v\in\mathcal U_1([a,b])$ and every $\zeta\in\mathcal L_\infty$,

$$D(v,\zeta)=-\mathbb E\big[v^*(\zeta)+v(Y)\big].$$

The formal statement has two cases. If $0\le\zeta\le v'_-(a)$ almost surely, then $v^*(\zeta)$ is a.s. finite and integrable and the identity holds between real numbers. Otherwise $D(v,\zeta)=+\infty$.

Milestones

1. Unbounded cases (proof of Theorem 4, p. 13): $P[\zeta<0]>0 \Rightarrow D(v,\zeta)=+\infty$; and $P[\zeta>v'_-(a)]>0 \Rightarrow D(v,\zeta)=+\infty$.
2. Pointwise maximizer (p. 13): for $0\le\xi\le v'_-(a)$, the function $t\mapsto v(t)-\xi t$ attains its maximum at some $t_0\in[a,b]$, so $v^*(\xi)=\xi t_0-v(t_0)$ is finite.
3. Measurable selection (p. 13): if $0\le\zeta\le v'_-(a)$ a.s., there is a measurable $X\in[a,b]$ a.s. with $X(\omega)\in\operatorname{argmax}_t[v(t)-\zeta(\omega)t]$ a.s.
4. Effective domain (p. 13): $D(v,\zeta)<+\infty \iff 0\le\zeta\le v'_-(a)$ a.s.
5. Theorem 5 (p. 14): for $\bar v\in\mathcal U_1([a,b])$, $\bar\zeta\in\mathcal L_1$ with $0\le\bar\zeta\le\bar v'_-(a)$ a.s., and a measurable maximizer selection $X$ with values in $[a,b]$, the pair $(P_X,-X)$ is a subgradient of $f$ at $(\bar v,\bar\zeta)$:

$$f(v,\zeta)\ge f(\bar v,\bar\zeta)+\int\big(v-\bar v\big)\,dP_X-\mathbb E\big[X(\zeta-\bar\zeta)\big]\quad\text{for all }(v,\zeta)\in\mathrm{Lip}(\mathbb R)\times\mathcal L_1.$$

Significance

Theorem 4 reduces an optimization over the infinite-dimensional space $\mathcal L_1$ to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier $\zeta$ (bounded between $0$ and the slope of the utility at the left end of the interval), and it makes evaluating $D$ as cheap as evaluating $v^*$. Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.

Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on $\mathbb R$ with values in $[-\infty,+\infty)$, no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.

Difficulty

The hard step is the interchange $\sup_{X\in\mathcal L_1}\mathbb E[\,\cdot\,]=\mathbb E\sup_t[\,\cdot\,]$. The inequality "$\le$" is pointwise, but "$\ge$" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where $\zeta(\omega)=0$ or $\zeta(\omega)=v'_-(a)$ the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because $\zeta$ is only essentially bounded and the test outcomes $M\mathbb 1_{\{\zeta<0\}}$ must be shown integrable.

Formalization scope

This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions $\Omega\to\mathbb R$ on a probability space with IsProbabilityMeasure P; $\mathcal L_1$ is Integrable, $\mathcal L_\infty$ is MemLp ζ ⊤ P. The conventions and explicit readings:

• $c\ge 0$ in $\mathcal U_1([a,b])$. The paper prints $c>0$. The page calls $\mathcal U_1([a,b])$ a convex cone, which must contain $0$, and the companion optimality theorem fails with $c>0$; the formalization uses $c\ge0$.
• Left derivative $v'_-(a)$ is derivWithin v (Set.Iic a) a, never deriv v a, which is $0$ at a kink.
• Extended values. $v^*$, $D$ and $f$ are EReal-valued, so an infimum equal to $-\infty$ and a supremum equal to $+\infty$ are represented, not replaced by $0$. The supremum in $D$ is over integrable $X$ only.
• Theorem 4 in two cases. The paper's right side is an expectation of an extended-real random variable, read as $+\infty$ off the domain. The statement separates the finite case (Bochner integral of the real part, with a.s. finiteness and integrability asserted) from the infinite case, which avoids extended-real subtraction.
• $f$ equals the Bochner integral of $-v^*(\zeta)$ when $v^*(\zeta)$ is a.s. finite with integrable real part, and $+\infty$ otherwise. This is exact because $-v^*(\zeta)\ge v(0)$.
• Theorem 5 adds the hypothesis that the selection lies in $[a,b]$ a.s. As printed ("for every measurable selection") it is false: with $a=-1$, $b=0$, $\bar v(t)=\min(t,0)$, $\bar\zeta=0$ on $[0,1]$ with Lebesgue measure, the selection $X(\omega)=1/\omega$ is not integrable. The continuity of $(P_X,-X)$ as a functional is stated as $X\in\mathcal L_\infty$ and the bound $\int|v|\,dP_X\le(|v(0)|+K)(1+\mathbb E|X|)$ for $K$-Lipschitz $v$.
• The paper's index $i$ and the standing data of §4 ($Y\in\mathcal L_1$, $a\le b$) are explicit binders.

A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk $0$ at $\mp\infty$), a supremum over all measurable $X$ (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited ($v=\min(t,0)$, $\zeta=1/2$ and $\zeta=2$).

Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on $\mathbb R$, and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program. 99 (2004). Author manuscript, rev. April 2003. https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003). https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 13 (2002). https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorems 14.37, 14.60). https://doi.org/10.1007/978-3-642-02431-3

Motivation

Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.

The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.

Setting

Fix a dimension $n\ge1$ and a continuously differentiable function $f:\mathbb R^n\to\mathbb R$. Problem (1) minimizes $f(x)$ over the nonnegative orthant $\mathbb R_+^n=\{x:x^i\ge0\text{ for every }i\}$. The positive part $[z]^+$ replaces each negative coordinate of $z$ by zero. A feasible $x$ is critical when every partial derivative $\partial_i f(x)$ is nonnegative and $\partial_i f(x)=0$ wherever $x^i>0$. This is the paper's componentwise first-order condition.

For a feasible iterate $x_k$, the binding set is $B(x_k)=\{i:x_k^i=0\}$. The paper selects a larger working set $I_k^+$ using a fixed $\varepsilon>0$ and the projected-gradient residual $w_k=\|x_k-[x_k-M\nabla f(x_k)]^+\|$, where $M$ is fixed, diagonal and positive definite. More precisely, $I_k^+$ contains the indices with $0\le x_k^i\le\min(\varepsilon,w_k)$ and $\partial_i f(x_k)>0$. The matrix $D_k$ is symmetric positive definite and has zero off-diagonal entries in the rows indexed by $I_k^+$. The projected arc and update are

$$p_k=D_k\nabla f(x_k),\qquad x_k(a)=[x_k-a p_k]^+,\qquad x_{k+1}=x_k(\beta^{m_k}).$$

Here $0<\beta<1$, and $m_k$ is the first nonnegative integer passing the paper's two-sum Armijo test (37), with $0<\sigma<1/2$. One sum uses the scaled gradient outside $I_k^+$; the other uses the actual projected displacement on $I_k^+$. These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.

Formalization targets

The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:

$$I_k^+=B(x_k)=B(x^*)\quad\text{for all sufficiently late }k.$$

The goal is Proposition 4. Let $f$ be convex and $C^2$, let $x^*$ be the unique minimizer on $\mathbb R_+^n$ satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is $D_k=H_k^{-1}$, where $H_k$ retains Hessian entries except for off-diagonal entries touching $I_k^+$. Then

$$x_k\longrightarrow x^*,\qquad \forall c>0\ \exists K\ \forall k\ge K:\ \|x_{k+1}-x^*\|\le c\|x_k-x^*\|.$$

If the Hessian is Lipschitz in a neighborhood of $x^*$, the same proposition states an at-least-quadratic error bound: $\|x_{k+1}-x^*\|\le C\|x_k-x^*\|^2$ eventually for some $C>0$. The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.

Significance

Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.

Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.

Difficulty

A positive definite matrix by itself does not make projection along $[x-aD\nabla f(x)]^+$ a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set $I^+(x)$ can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged $I_k^+$ and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's $M$ is diag μ with every $\mu^i>0$. The run predicate includes a feasible initial point and the first acceptable integer $m_k$, and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs $D_k$ from $H_k$ and does not assume its invertibility, admissibility, convergence or eventual active-set equality.

Assumption (C) includes local $C^2$ smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no $x\ge0$ restriction, so neither does the Lean hypothesis.

A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.

Selected references

• Dimitri P. Bertsekas, Projected Newton Methods for Optimization Problems with Simple Constraints, SIAM Journal on Control and Optimization 20(2), 221–246, 1982. DOI: 10.1137/0320018.