Convex Optimization

Motivation

Convex programs with inequality constraints arise when a decision must meet capacity, resource, or performance limits. Their Lagrange multipliers assign a price to each constraint. Finding an optimal multiplier gives a dual certificate and can guide a primal optimization method. Classical quadratic multiplier methods update these prices through a particular penalty. Eckstein's 1993 paper places a broader family of multiplier updates inside the theory of Bregman proximal point algorithms, allowing a nonquadratic function to shape each step (Eckstein 1993, §4.2).

The result here concerns the inequality constrained case, where multiplier vectors must be componentwise nonnegative. Eckstein identifies a monotone conjugate that incorporates this restriction into the primal penalty and proves that the resulting multiplier sequence converges to an optimal multiplier when one exists. The paper also studies primal limit points and the behavior when no optimal multiplier exists (Eckstein 1993, Theorem 7 and proof, pp. 216–219).

Setting

Let $C\subseteq\mathbb R^n$ be closed, nonempty, and convex. Let $f,g_1,\ldots,g_m$ be proper lower semicontinuous convex functions, finite on $C$. The primal problem is to minimize $f(x)$ over $x\in C$ subject to $g_i(x)\le 0$ for every $i$. Write $g(x)=(g_1(x),\ldots,g_m(x))$. A point solves the problem only when it lies in $C$, satisfies every inequality, and has no larger objective value than any other feasible point.

For a nonnegative multiplier $p$, the dual functional is $d(p)=\inf_{x\in C}\{f(x)+\langle p,g(x)\rangle\}$; it equals $-\infty$ outside the nonnegative orthant. A multiplier $p^*$ is optimal when it maximizes $d$. The standing assumption that $d$ is not identically $-\infty$ makes this dual functional a meaningful proper concave object (Eckstein 1993, p. 215).

A Bregman function $h$ has an open zone $S$. It is continuously differentiable there, strictly convex and continuous on $\overline S$, and satisfies the boundedness and sequential conditions of Definition 1. Its Bregman distance is $D_h(u,v)=h(u)-h(v)-\langle\nabla h(v),u-v\rangle$, with $u\in\overline S$ and $v\in S$. The zone contains the strict positive orthant, and the image of its gradient contains that orthant. Its monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$. Lemma 3 establishes that this function is finite and differentiable everywhere under these assumptions (Eckstein 1993, pp. 205, 215–216).

Given positive step sizes $c_k$ bounded away from zero, recursion (11) chooses $x^{k+1}$ as a minimizer over $C$ of $f(x)+c_k^{-1}h^{*+}(\nabla h(p^k)+c_kg(x))$, then sets $p^{k+1}=\nabla h^{*+}(\nabla h(p^k)+c_kg(x^{k+1}))$. The theorem assumes an infinite sequence conforming to these recursions; it does not assert that each minimizer exists for arbitrary data.

Formalization targets

Multiplier convergence

The goal is Eckstein's Theorem 7. If the dual problem has an optimal multiplier, then the multiplier sequence converges to one:

When every $g_i$ is continuous on $C$ and $S$ contains the closed nonnegative orthant, each subsequential limit of the primal iterates solves the constrained problem. Under the same zone condition, the multiplier sequence is unbounded if the dual has no optimal multiplier. The printed theorem says “if (10) has no solution” in this last clause; its proof on p. 218 establishes the no-optimal-multiplier condition, which is the version formalized here.

Supporting targets

The milestones include the representations of $h^{*+}$ in Lemma 2, the appendix results governing recession directions and the monotone conjugate, Lemma 3's global finiteness and differentiability, the subdifferential chain rule, and the Bregman proximal point result of Theorem 1. They also capture the paper's claims that recursion (11) is a Bregman proximal point run for $\partial(-d)$ and that primal limit points meet the feasibility, complementarity, and Lagrangian conditions.

Significance

The theorem supplies a convergence guarantee for nonquadratic methods of multipliers with inequality constraints. It separates the dual conclusion, which uses the strict positive orthant condition, from the primal limit and unboundedness conclusions, which additionally require the closed orthant to lie in the zone. This distinction lets a Bregman function whose zone excludes boundary points still yield dual convergence when optimal multipliers exist (Eckstein 1993, Theorem 7, pp. 216–218).

Eckstein proved this theorem on paper. The mission asks for machine checked proofs of its precise statements and the supporting results; the draft statements compile but their proofs remain open. A completed development would also provide reusable finite dimensional infrastructure for extended-real convex functions, monotone conjugates, Bregman distances, and convex-analytic multiplier conditions.

Difficulty

A direct appeal to ordinary proximal point convergence does not identify the update in (11) as a proximal step: the primal minimization uses $h^{*+}$, whereas the operator of interest is the subdifferential of the negative dual functional. The nonnegative orthant also introduces boundary behavior absent from the equality constrained case. The link requires precise conjugacy and subdifferential statements, including a globally finite monotone conjugate, before Theorem 1 can apply (Eckstein 1993, pp. 215–218). For primal limit points, the issue is to pass from optimality of each primal subproblem to feasibility, complementarity, and minimization of the limiting Lagrangian.

Formalization scope

Lean uses finite dimensional real inner product spaces for the general proximal point theorem and EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) for the primal and multiplier spaces. Functions that the paper regards as extended-valued are represented by EReal; their properness excludes $-\infty$. The infimum defining $d$ and the supremum defining $h^{*+}$ remain extended-real operations, so an infinite value cannot silently become zero. Real values are extracted from $h^{*+}$ in recursion (11) only because Lemma 3 asserts finiteness everywhere.

The real function $h$ is total in Lean but constrained only on $\overline S$; its gradient is evaluated only at points in $S$. Every multiplier iterate is explicitly in $S$. The initial primal value $x^0$ is unused by recursion (11). The Bregman proximal point recursion is represented by its equivalent inclusion (4), and a “limit point” is a subsequential limit. The sequential condition (vi) of Definition 1 is stated for $x^k\in\overline S$, the natural first-argument domain of $D_h$. The Appendix's essential strict convexity means strict convexity on convex subsets of the subdifferential domain. Its recession direction uses the stated limit inferior condition.

Lemma A4's printed unconditional claim that its composite $G$ is proper lacks a finite-value witness. The formal statement keeps convexity of $G$ unconditional and states properness at a point $x_0$ where all inner functions and the outer function are finite; differentiability of the outer function there is expressed with local finiteness of its extended-real value. At a zero coefficient, its corresponding subgradient term contributes zero without requiring a subgradient to exist. These conditions expose rather than hide the domain issue. The formulation rules out an arbitrary multiplier sequence, an all-space supremum, or a minimization over infeasible points. Contributions proving the milestones, improving shared convex analysis libraries, and checking the boundary conventions are welcome.

Selected references

• Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI:10.1287/moor.18.1.202.

Motivation

The proximal point method seeks a zero of an operator by repeatedly solving an implicit equation. For a maximal monotone operator, the ordinary quadratic proximal step is available throughout a Hilbert space. Eckstein's 1993 paper replaces the quadratic penalty with a Bregman function, allowing a step to reflect the geometry of a constrained problem. Before convergence can be discussed, each implicit step must have a solution in the region where the Bregman gradient is defined. Eckstein, 1993, §§1–2 isolates that existence question in Theorem 4.

The theorem draws on the L-property and a range theorem attributed to Brézis and Haraux. Their results describe when the image of a sum of monotone operators is large enough to contain the inputs of a proximal step. The paper uses those results to obtain two practical sufficient conditions: a gradient whose image is the whole space, or an open gradient image together with a zero in the image of the operator. Eckstein, 1993, Theorems 2–4

Setting

Let $H$ be a finite-dimensional real inner product space, representing the paper's $\mathbb R^n$. An operator $T:H\to2^H$ assigns a set of vectors to each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ whenever $u\in Tx$ and $v\in Ty$, and maximal monotone when its graph cannot be enlarged while preserving monotonicity. Its domain and image are $\operatorname{dom}T=\{x:Tx\ne\varnothing\}$ and $\operatorname{im}T=\{u:\exists x,\ u\in Tx\}$.

Let $S\subseteq H$ be open. A Bregman function with zone $S$ is a real function $h$ on $\bar S$ satisfying the six conditions of Definition 1: continuous differentiability on $S$, strict convexity and continuity on $\bar S$, boundedness of two families of partial level sets, and two sequential conditions that relate convergence to its D-function

The gradient is an operator with domain $S$ and image $\nabla h(S)$. For positive step sizes $c_k$, a Bregman proximal point sequence is a sequence $x^k\in S$ satisfying

This is the inclusion form (4) of recursion (3). The expression $\nabla h+c_kT$ is a sum of set-valued operators, and each step asks for a preimage of $\nabla h(x^k)$ under that sum. Eckstein, 1993, pp. 205–207

Formalization targets

The goal is Theorem 4. If $T$ is maximal monotone, $h$ is Bregman with zone $S\supseteq\operatorname{dom}T$, and either

then every $x^0\in S$ and every positive sequence $(c_k)$ admit an infinite Bregman proximal point sequence starting at $x^0$. The theorem asserts existence for every starting point in the zone, at every step. Eckstein, 1993, p. 209, Theorem 4

The milestones follow the cited results and the paper's proof: trimonotone operators and subdifferentials have the L-property (Theorem 2); the interior and closure of the image of a sum agree with those of the sum of images under the hypotheses of Theorem 3; the subdifferential and gradient sums agree on the domain of $T$ and yield a maximal monotone sum; and the relevant gradient image lies in the image of $\nabla h+cT$ for every $c>0$. These targets provide the range statement needed for the infinite recursion. Eckstein, 1993, pp. 208–209

Significance

Theorem 4 certifies that the nonlinear proximal point recursion is well defined from any admissible starting point under either range condition. Without this existence statement, a convergence theorem for sequences satisfying the recursion leaves open whether a sequence can be generated. Its range conditions also distinguish Bregman geometries whose gradient covers the whole space from geometries with a smaller but open gradient image. Eckstein, 1993, p. 209

The mathematical result is proved in the paper; the work here is to formalize its definitions, the Brézis–Haraux statements cited there, and the existence theorem in Lean. The milestone statements are open proof obligations in the draft, not claims of completed machine-checked proofs. The operator vocabulary and range theorem can be reused for other implicit algorithms involving sums of monotone operators.

Difficulty

Knowing that $T$ and $\nabla h$ are monotone does not by itself show that a prescribed $\nabla h(x^k)$ belongs to $\operatorname{im}(\nabla h+c_kT)$. Even maximality of $T$ alone gives no direct description of that image. The hard point is the range of the sum on the zone of $h$, especially when $\nabla h(S)$ is a proper subset of $H$. Theorem 3 supplies an interior and closure comparison, but its domain, maximality, and L-property hypotheses must all be established for the particular operators in Theorem 4. Eckstein, 1993, pp. 208–209

Formalization scope

The Lean model uses a finite-dimensional real inner product space $H$, set-valued operators $H\to\operatorname{Set}H$, and Mathlib's gradient on the open zone $S$. The image of $\nabla h$ is precisely $\nabla h(S)$; values of the total Lean gradient outside $S$ do not enter it. The function $h:H\to\mathbb R$ is total for Lean's type system, but only values on $\bar S$ matter. Its extension by $+\infty$ outside $\bar S$ is EReal-valued, and the subdifferential uses the published convex-analysis predicate. The L-property uses boundedness below in $\mathbb R$, matching the paper's strict lower bound above $-\infty$.

Recursion (3) is represented by its equivalent inclusion (4), with every iterate explicitly in $S$. The paper leaves the positive step sizes implicit in Theorem 4; the goal quantifies over all such sequences and imposes no convergence-specific lower bound on them. Condition (vi) of Definition 1 is applied to first arguments in $\bar S$, the stated natural domain of $D_h$. Trimonotonicity is the three-point cyclic condition used by Brézis and Haraux. A one-step solution, a sequence with an arbitrary starting point chosen by the prover, or an image taken over all of $H$ would not establish this target.

The development needs convex subdifferentials, maximal monotonicity, maximality of appropriate sums, and the Brézis–Haraux range result. Contributions that prove these milestones or add reusable range lemmas are within scope; an optional formalization of the existence part of Theorem 5 is outside the core path.

Selected references

• J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI.
• H. Brézis and A. Haraux, Image d'une somme d'opérateurs monotones et applications, Israel Journal of Mathematics 23, 165–186, 1976. DOI.

Motivation

A linear program $\max c\cdot x$ subject to $Ax\le b$, $x\ge 0$ assumes that the constraint matrix $A$ is known exactly. In practice the columns of $A$ — the activity vectors, describing how much of each resource one unit of activity $j$ consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision $x$ should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.

The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.

Setting

Fix integers $m,n\ge0$. Vectors in $\mathbb R^m$ are compared componentwise. For a set $S\subseteq\mathbb R^m$ and a scalar $t$, $tS=\{ta: a\in S\}$, and the sum of sets is Minkowski addition, $S+T=\{s+t: s\in S,\ t\in T\}$.

Let $K_1,\dots,K_n\subseteq\mathbb R^m$ be nonempty convex activity sets and $K\subseteq\mathbb R^m$ a nonempty convex resource set. Problem (I) is

and $X\subseteq\mathbb R^n$ denotes its set of feasible $x$. Problem (Ib) is the special case $K=K(b)=\{y\in\mathbb R^m: y\le b\}$ for a right-hand side $b\in\mathbb R^m$.

The support functional of a set $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y\cdot a$, a value in $[-\infty,+\infty]$. With $e_i$ the $i$-th unit vector, the auxiliary matrix $\bar A$ is the $m\times n$ matrix with entries

defined when all of these are finite, and LP$(\bar A)$ is the linear program $\max c\cdot x$ subject to $\bar Ax\le b$, $x\ge0$. Finally $M$ is the set of $m\times n$ matrices $(a_1,\dots,a_n)$ whose $j$-th column lies in $K_j$.

In the application, the activity sets are Euclidean balls $K_j=\{a\in\mathbb R^m:\|a-a_j\|_2\le\rho_j\}$ around nominal columns $a_j$ of a matrix $A_0$, with radii $\rho_j\ge0$.

Formalization targets

Goal: the THEOREM (p. 1156)

Assume every $K_j$ is nonempty and convex and $\delta^*(e_i\mid K_j)<\infty$ for all $i,j$. Then

and for every objective $c$, the optimal solutions of (Ib) and of LP$(\bar A)$ coincide.

Milestones

1. Feasibility for (I) is equivalent to $x\ge0$ and $\sum_j x_ja_j\in K$ for every choice $a_j\in K_j$ (p. 1154).
2. LEMMA (p. 1155): $X$ is convex.
3. If $\delta^*(e_i\mid K_j)=\infty$ for some $i$, every feasible $x$ of (Ib) has $x_j=0$ (p. 1155).
4. Compact activity sets have $\delta^*(e_i\mid K_j)<\infty$ (p. 1156).
5. $x$ is feasible for (Ib) iff $Ax\le b$ for every $A\in M$ and $x\ge0$ (p. 1156).
6. Every $A\in M$ satisfies $A\le\bar A$ entrywise (proof of THEOREM).
7. Feasible for LP$(\bar A)$ implies feasible for (Ib) (proof of THEOREM).
8. Feasible for (Ib) implies $\sum_j x_j\sup_{a_j\in K_j}a_{ij}\le b_i$ for every $i$, i.e. feasible for LP$(\bar A)$ (proof of THEOREM).
9. For Euclidean balls, $\delta^*(e_i\mid K_j)=a_{ij}+\rho_j$, so $\bar a_j=a_j+\rho_je$ with $e$ the all-ones vector (p. 1157).
10. Inexact LP over balls: (Ib) has the same feasible and optimal solutions as $\max c\cdot x$ subject to $\sum_j x_j(a_j+\rho_je)\le b$, $x\ge0$ (p. 1157).

Significance

The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in $M$, of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column $j$ is inflated by the full radius $\rho_j$, which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.

The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.

Difficulty

The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every $A\in M$" to $\bar A$ uses that the supremum of a sum of independent terms is the sum of suprema, which needs every $K_j$ nonempty and the scalars $x_j$ nonnegative; with an empty activity set the Minkowski sum is empty and every $x\ge0$ becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.

Formalization scope

• Vectors are Fin m → ℝ and Fin n → ℝ, with indices $0,\dots,m-1$ in place of $1,\dots,m$; the order on vectors is componentwise.
• Feasibility of (I) is the Minkowski-sum inclusion (∑ j, x j • K j) ⊆ R (pointwise set operations) together with $x\ge0$. It is not defined as "for every choice $a_j\in K_j$", which would make milestones 1 and 5 trivial, and $\bar A$ is constructed from the $K_j$, not an arbitrary matrix dominating $M$, which would make the goal trivial.
• $\delta^*$ is valued in EReal. The entries of $\bar A$ are its real conversions, so every statement mentioning $\bar A$ assumes $K_j\neq\emptyset$ and $\delta^*(e_i\mid K_j)<\infty$, the paper's standing assumptions (pp. 1154–1156). Convexity of the $K_j$ is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of $K$).
• An optimal solution is a feasible point attaining the maximum of $c\cdot x$; the paper writes $\sup$ and does not discuss attainment. Because the goal identifies the feasible sets, the two problems also have equal suprema.
• Hyperspheres use the Euclidean norm (EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii $\rho_j\ge0$.
• The support functional restates the published FenchelRobust.Counterpart.supportFun with the same body.
• Not formalized: Magnanti's extension to $\ge$ and $=$ rows (p. 1156), and the remarks on (GLP) and stochastic programming. Contributions of proofs of any milestone, and of an EReal statement equating the optimal values, are welcome.

Selected references

• A. L. Soyster, Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming, Operations Research 21(5), 1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Mathematical Programming 88, 411–424, 2000. https://doi.org/10.1007/PL00011380
• D. Bertsimas and M. Sim, The Price of Robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.

The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.

Timeline.

• 1966–1967: Hartman–Stampacchia and Lions–Stampacchia prove existence of solutions for monotone, hemicontinuous variational inequalities on bounded closed convex sets (Lions–Stampacchia 1967). Minty's lemma characterizes the solution set by the inequality with the operator evaluated at the variable point.
• 1970: Martinet introduces the regularization iteration (2) and proves Théorème 1 below (Martinet 1970). In §IV of the same note he states the convex-minimization version.
• 1976: Rockafellar extends the method to maximal monotone operators, allowing inexact steps and variable step sizes, and proves weak convergence of the whole sequence when a zero exists (Rockafellar 1976).
• 1991: Güler constructs an example in which the iterates converge weakly but not strongly (Güler 1991).

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $H'$ be its dual, and write $(\varphi, y)$ for the value of a functional $\varphi\in H'$ at $y\in H$. Let $C\subseteq H$ be convex, closed and bounded, and let $T:H\to H'$ be

• monotone on $C$: $(Tx-Ty,\,x-y)\ge0$ for all $x,y\in C$;
• hemicontinuous on $C$: for all $x,y\in C$, the map $t\mapsto T((1-t)x+ty)$, $t\in[0,1]$, is continuous into $H'$ with its weak topology.

The variational inequality (1) asks for $\bar x\in C$ such that

Its solution set is denoted $M$ (solSet T C in Lean).

Martinet's regularization algorithm starts from $x^0\in C$. Given $x^n\in C$, it determines $x^{n+1}\in C$ such that

In words, $x^{n+1}$ solves the variational inequality for the operator $T+(\,\cdot\,-x^n)$, which is strongly monotone. A point $\tilde x$ is a weak cluster point of $(x^n)$ if every neighbourhood of $\tilde x$ in the weak topology contains $x^n$ for infinitely many $n$.

Formalization targets

Goal: Théorème 1

Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that $T$ is bounded on $C$.

Milestones, in the order the paper uses them

1. §2.1: (1) has at least one solution when $C\neq\emptyset$, so $M\neq\emptyset$.
2. §2.2: the step (2) has exactly one solution $x^{n+1}\in C$ for every $x^n\in C$.
3. §2.3, (5): Minty's characterization $M=\{\bar x\in C\mid (Tx,\,x-\bar x)\ge0\ \forall x\in C\}$.
4. §2.3, (7): for every $\bar x\in M$, $\|x^{n+1}-\bar x\|^2\le\|x^n-\bar x\|^2-\|x^{n+1}-x^n\|^2$.
5. Lemme 1: $\|x^{n+1}-x^n\|\to0$.
6. §2.3, (8): $\liminf_n (Tx^{n+1},\,x-x^{n+1})\ge0$ for every $x\in C$.
7. §2.3, (9): $\liminf_n (Tx,\,x-x^{n})\ge0$ for every $x\in C$.
8. Corollaire (stronger than the goal): if $M=\{\bar x\}$, then $x^n\rightharpoonup\bar x$.

Significance

The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.

Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.

Difficulty

Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.

First, the iterates satisfy the variational inequality only approximately, and only with $T$ evaluated at the iterate. A weak cluster point gives no control over $Tx^{n}$, because $T$ is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in $(Tx^{n+1},\,x-x^{n+1})\ge -\varepsilon_n$, fails for this reason. Passing to the limit requires the reformulation in which $T$ is evaluated at a fixed point of $C$. That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.

Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of $C$, and this is the heaviest item of the mission.

Formalization scope

• $H$ is a real Hilbert space: NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.
• $H'$ is StrongDual ℝ H, and $(\varphi,y)$ is φ y. $T$ is not replaced by a map $H\to H$ through the Riesz isomorphism.
• Hemicontinuity is weak-* continuity: for $x,y\in C$ and every $z\in H$, the map $t\mapsto (T((1-t)x+ty),z)$ is continuous on $[0,1]$. Since $H$ is reflexive, this is the paper's weak topology on $H'$. It is not strengthened to continuity of $T$.
• The algorithm is a relation (IsRegSeq): any sequence with $x^0\in C$ that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.
• A weak cluster point is MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.
• $\liminf_n a_n\ge0$ in (8) and (9) is stated as $\forall\varepsilon>0$, eventually $a_n\ge-\varepsilon$. Filter.liminf on $\mathbb R$ returns a junk value on sequences that are unbounded below.
• "C nonempty" is added to the existence milestone. The paper leaves it implicit, and the claim is false for $C=\emptyset$.
• In Lean the sequence is called $x$ and an arbitrary point of $C$ is called $y$. The paper uses the letter $x$ for both.

A trivializing formalization is ruled out. The goal does not assume $M\neq\emptyset$, boundedness of $T$, or strong cluster points. Its hypotheses are satisfiable: $H=\mathbb R$, $C=[-1,1]$, $(Tx,y)=xy$, $x^n=2^{-n}$ is an instance, checked locally.

Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of $C$ under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.

Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.

Selected references

• B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3) (1970), 154–158. https://doi.org/10.1051/m2an/197004R301541
• J.-L. Lions, G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20 (1967), 493–519. https://doi.org/10.1002/cpa.3160200302
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14 (1976), 877–898. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29 (1991), 403–419. https://doi.org/10.1137/0329022

Motivation

Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation

where $\partial\psi_C$ is the normal-cone operator of a closed convex set $C$. S. M. Robinson introduced strong regularity of such an inclusion at a solution $x_0$ in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).

Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set $C$ the paper's appendix does this by a reduction: locally around $x_0$ the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.

Setting

Work in $\mathbb R^n$ with the standard inner product, which identifies $\mathbb R^n$ with its dual. For $C\subseteq\mathbb R^n$ the normal cone at $x$ is

A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex $C$, an $n\times n$ real matrix $A$ and $a\in\mathbb R^n$, and consider

It is strongly regular at a solution $x_0$ with constant $\lambda$ if there are neighbourhoods $U$ of $0$ and $V$ of $x_0$ such that for each $y\in U$ the perturbed inclusion

has exactly one solution $x=s(y)$ in $V$, and $\|s(y_1)-s(y_2)\|\le\lambda\|y_1-y_2\|$ on $U$.

The reduction uses the following objects, all built from the data:

• $y_0:=Ax_0+a$;
• the face $F:=\partial\psi_C^*(-y_0)$, the set of maximisers of $\langle -y_0,\cdot\rangle$ over $C$ (it contains $x_0$);
• the tangent cone $T:=T_F(x_0)=\partial\psi_F(x_0)^\circ$, the polar of the normal cone of $F$ at $x_0$;
• the subspace $L$ parallel to $F$ (the direction of its affine hull) and the orthogonal projector $P_L$;
• the lineality space $M$ of $T$, the subspace $L\cap M^\perp$, and the cone $K:=T\cap M^\perp$.

The reduced form of (A.1) at $x_0$ is the inclusion $z\in P_LAw+\partial\psi_T(w)$ for $z\in L$; in an orthonormal basis adapted to $M$, $L\cap M^\perp$ and $L^\perp$ it is $z\in Bw+\partial\psi_{\mathbb R^r\times K}(w)$ with an $(r+s)\times(r+s)$ matrix $B$. It is vacuous when $L=\{0\}$.

Formalization targets

Goal: Theorem A.4 (p. 60)

If $x_0$ solves (A.1), then (A.1) is strongly regular at $x_0$ if and only if

No Lipschitz constant is fixed: the left side is "strongly regular for some $\lambda$".

Milestones

1. Proposition A.1 (p. 58): for $x_0\in C$, $(C-x_0)\cap U=T_C(x_0)\cap U$ for some neighbourhood $U$ of $0$.
2. Proposition A.2 (p. 58): on $F=\partial\psi_C^*(-y_0)$, $\partial\psi_F(x)=\partial\psi_C(x)+y_0\mathbb R_+$, and $\partial\psi_C^*(-y)\subset F$ for $y$ near $y_0$.
3. Proposition A.3 (p. 58): for $x_0\in F$, near the origin, $0\in(y_0+k)+\partial\psi_C(x_0+h)$ iff $0\in P_Lk+\partial\psi_T(h)$.
4. The correspondence (A.4) (p. 60): for $x$ near $x_0$ and small $y$, (A.2) holds iff $0\in P_L(Ah-y)+\partial\psi_T(h)$ with $h=x-x_0$.

Companions

• Corollary 3.2 (p. 53), in two items. Sufficiency: the reduced form is vacuous, or $B_{11}$ is nonsingular and the Schur complement $B/B_{11}$ is positive definite. Characterisation when $K=\mathbb R^s_+$: strongly regular iff vacuous, or $B_{11}$ nonsingular and $B/B_{11}$ a P-matrix.
• The 3 × 3 linear complementarity example of §4 (p. 53): strongly regular at $x_0=(1,0,0)$, and not strongly regular once the entry $5$ of $A$ becomes $4$.

Significance

Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where $A$ itself is neither positive definite nor a P-matrix.

The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.

Difficulty

The definition of strong regularity is local, while condition (ii) is global on $L$. The obvious argument, "linearise and read off the inverse", does not apply, because $\partial\psi_C$ is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of $y_0$ may move the solution off the face $F$, and only polyhedrality, through the finitely many values of $\partial\psi_C$ on $F$ and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near $0$ to uniqueness on all of $L$. The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is $y-(Ax+a)\in\partial\psi_C(x)$. A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause $x\in C$, so $\partial\psi_C(x)=\emptyset$ off $C$; without it every inclusion would be satisfiable at points outside $C$ and the statements would change meaning.
• $T_C(x_0)$ is the polar of the normal cone, as on p. 58, not the closure of the cone of feasible directions. $F$ is the set of maximisers of $\langle -y_0,\cdot\rangle$ (the sign matters: the opposite face would make the theorem false). $L$ is the direction of the affine span of $F$, and $P_L$ is Mathlib's Submodule.starProjection.
• The reduced form is stated basis-free on $L$; $\partial\psi_T$ is the normal cone of $T$ in all of $\mathbb R^n$. In Corollary 3.2, $B_{11}$ and $B/B_{11}$ are expressed through projectors onto $M$ and $L\cap M^\perp$. Only the case $K=\mathbb R^s_+$ is stated in a basis, an orthonormal basis of $L\cap M^\perp$ in which $K$ is the orthant.
• "Positive definite" does not require symmetry. "Strongly regular" without a constant is existential in $\lambda$, with $\lambda$ real.
• Corollary 3.2's second sentence refers on the page to "(3.8)", an evident slip for (3.9); it is formalized for (3.9).
• The standing assumption "C nonempty polyhedral convex" is a hypothesis of every item.
• A trivializing formalization is ruled out: strong regularity requires existence, uniqueness in $V$ and the Lipschitz bound together, and condition (ii) requires existence and uniqueness for every $z\in L$.
• Needed infrastructure: faces and tangent cones of polyhedra and their local structure (Minkowski–Weyl, finitely many faces), orthogonal decompositions, and Lipschitz continuity of single-valued polyhedral inverses. All of this is reusable beyond this mission. Proofs of the propositions, of the correspondence, and of the companions are welcome independently.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• S. M. Robinson, Generalized equations and their solutions, Part I: Basic theory, Mathematical Programming Study 10, 128–141, 1979. https://doi.org/10.1007/BFb0120850
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8, 189–211, 1974. https://doi.org/10.1016/0024-3795(74)90066-4