Optimization

Motivation

In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.

The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.

A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.

Setting

A product passes through three successive stages $A\to B\to C$ before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost $V_a,V_b,V_c$ (marginal cost equal to average variable cost at every relevant output).

Final demand is a function $D:\mathbb R\to\mathbb R$: $D(p)$ units of $C$ are bought at price $p$. A firm with constant unit cost $c$ that sells at price $p$ earns the profit (return above variable outlay)

$$\pi_c(p)=(p-c)\,D(p),$$

and $p$ is a profit-maximizing price at cost $c$ when $\pi_c(x)\le\pi_c(p)$ for every $x$.

Unintegrated chain. Stage A sells to B at a transfer price $P_a$, B sells to C at $P_b$. Their per-unit profits are $R_a=P_a-V_a$ and $R_b=P_b-(V_b+P_a)$; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is $C_c=V_c+P_b$; it charges a profit-maximizing price $P_c$ at that cost and sells $Q=D(P_c)$. The chain's aggregate profit is $R_aQ+R_bQ+R_cQ$ with $R_c=P_c-(V_c+P_b)$.

Integrated firm. One firm owns all three stages. Its unit cost is $C'_c=V_a+V_b+V_c$; it charges a profit-maximizing price $P'_c$ at that cost and sells $Q'=D(P'_c)$, earning $(P'_c-C'_c)\,Q'$.

The price elasticity of demand at $p$ is $e(p)=-p\,D'(p)/D(p)$ (positive for a downward-sloping curve) and the marginal revenue is $r(p)=p+D(p)/D'(p)$. The consumers' surplus gained when the price falls from $P_c$ to $P'_c$ is $\int_{P'_c}^{P_c}D(x)\,dx$.

Formalization targets

Goal: vertical integration benefits producer and consumer

For every non-increasing demand curve $D$, all unit costs $V_a,V_b,V_c$, and all transfer prices with $R_a>0$, $R_b>0$, if $P_c$ is profit-maximizing at cost $V_c+P_b$, $P'_c$ is profit-maximizing at cost $V_a+V_b+V_c$, $D$ is differentiable at $P_c$ and $Q=D(P_c)>0$, then

$$P'_c<P_c,\qquad D(P_c)<D(P'_c),\qquad R_aQ+R_bQ+R_cQ<(P'_c-C'_c)\,Q',$$ $$0<\int_{P'_c}^{P_c}D(x)\,dx,\qquad Q\,(P_c-P'_c)\le\int_{P'_c}^{P_c}D(x)\,dx.$$

The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".

Milestones

1. Footnote 6, equilibrium identities. At a profit-maximizing price, $r=c$, $e=p/(p-r)=p/(p-c)$, and $p=c\,e/(e-1)$ when $c\ne0$.
2. Section III, unitary elasticity. At zero cost, $e=1$; at positive cost, $p>c$ and $e>1$.
3. Section III, cost raises price. For $c_1<c_2$, profit-maximizing prices satisfy $D(p_2)\le D(p_1)$, and $p_1<p_2$ under the goal's regularity hypotheses.
4. Footnote 6, straight-line demand. For $D(p)=b(a-p)$: $p^*(c)=(a+c)/2$, $\Delta r=2\Delta p$, $e(p^*(c))=(a+c)/(a-c)$, the elasticity rises relatively more than the price, and the relative rise grows with $c$.
5. Figure 1. With $D_c(p)=\tfrac85(140-p)$ and $V_a=V_b=V_c=20$: $P_c=115$, $Q=40$, aggregate profit $2{,}200$; $P'_c=100$, $Q'=64$, profit $2{,}560$; consumers' surplus rises by $780$.

Significance

The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.

Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.

Difficulty

The weak inequalities ($P'_c\le P_c$, $Q\le Q'$, profit $\le$) follow from comparing the two maximization problems (the price comparison also uses $Q>0$: if $D\equiv 0$, every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at $P_c$, and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.

Formalization scope

• Prices, costs and quantities are real numbers; maximization is over all prices $p\in\mathbb R$. Demand is a function $D:\mathbb R\to\mathbb R$; the goal assumes only that it is non-increasing (Antitone D).
• Profit-maximizing prices are hypotheses (IsProfitMax D c p), never closed forms; the closed form $(a+c)/2$ appears only for straight-line demand.
• The transfer prices $P_a,P_b$ are arbitrary data with positive markups; they need not be profit-maximizing for $D_a,D_b$, which the paper draws only in its figure.
• Explicit readings of the paper's prose. "Benefits both producer and consumer" and "will lower the price" become the four strict inequalities of the goal. "Aggregate profit" is the sum over the three stages, $Q[P_c-(V_a+V_b+V_c)]$, not stage C's profit alone. Consumers' surplus "in the Marshallian sense" is the interval integral of $D$ between the two prices; footnote 5's trapezoid formula is used only for the straight line of Figure 1. Elasticity is a positive number $-pD'(p)/D(p)$. "Relatively greater increment in the elasticity" is made exact for straight-line demand as $e(p^*(c'))/e(p^*(c))>p^*(c')/p^*(c)$; the literal $\Delta e/e>\Delta c/c$ is false for small $c$. Footnote 6's $e'=(p+\Delta p)/(p-2\Delta p)$ and "approximating $3\Delta p/p$" are a printed slip; the exact $e(p^*(c))=(a+c)/(a-c)$ is stated instead, and no approximation is formalized. Figure 1's demand line $D_c(p)=\tfrac85(140-p)$ is the line through the three points the text gives.
• Added hypotheses. Differentiability of $D$ at $P_c$ and $D(P_c)>0$, which the paper's marginal-revenue reasoning presupposes. Every statement involving elasticity or marginal revenue carries differentiability and positive demand, because Lean's deriv and division return $0$ on bad input.
• Ruled out. Formalizations that hard-code linear demand in the goal, compare the integrated profit with stage C's profit alone, or prove only the weak ($\le$) inequalities do not capture the result.
• Sections IV and the policy remarks of Section III (rent evasion, taxes, co-operatives) are not formalized.
• Only Mathlib is needed: Fermat's rule (IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.

Selected references

• J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256964
• A. A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, 1838, Chapter IX.
• J. Tirole, The Theory of Industrial Organization, MIT Press, 1988, §4.2.
• G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

Motivation

Planning a road improvement requires an estimate of how traffic will redistribute over the routes affected. Because speed falls as flow rises, sending every vehicle along the route that is quickest today changes which route is quickest. J. G. Wardrop posed the question in its simplest setting in 1952: a given flow $Q$ chooses among $D$ alternative routes between one origin and one destination, and the journey time on each route rises with the flow on it. He proposed two criteria for the resulting distribution. The first, equal journey times, became known as Wardrop's first principle or user equilibrium: "the journey times on all the routes actually used are equal, and less than those which would be experienced by a single vehicle on any unused route." It describes the state in which no driver can shorten their trip by switching routes, and it is the equilibrium notion behind traffic-assignment models and the theory of selfish routing.

Timeline:

• 1952. Wardrop states both criteria and, for parallel routes with journey times of the form (22), derives the closed-form equal-times split (23)–(24) (Wardrop 1952, p. 345).
• 1956. Beckmann, McGuire and Winsten show that, on general networks with increasing link costs, the equal-times conditions are the optimality conditions of a convex program, which gives existence and uniqueness of link flows (Beckmann et al. 1956).
• 2014. Kelly and Yudovina give a textbook treatment of the network case (Kelly–Yudovina 2014, ch. 4); its existence theorem is on Prove2Me for total, continuous, increasing delay functions.

Setting

There are $D$ routes, $i = 1, \dots, D$. Route $i$ has two positive constants: $b_i$, its journey time when no additional traffic uses it, and $p_i$, the additional flow at which its speed would drop to zero. When an additional flow $x$ uses route $i$, its journey time is

$$t_i(x) = \frac{b_i}{1 - x/p_i}, \qquad 0 \le x < p_i. \tag{22}$$

This form comes from a linear speed/flow relation on each route. A feasible split of the total flow $Q$ is a vector $q = (q_1, \dots, q_D)$ with $0 \le q_i < p_i$ and $\sum_i q_i = Q$. A feasible split $q$ satisfies the equal-times criterion with common time $t$ when

• every used route ($q_i > 0$) has $t_i(q_i) = t$, and
• every unused route ($q_i = 0$) has $t \le b_i$, so a single vehicle could not do better than $t$ by moving to it.

Write $U(t) = \{ i : b_i < t \}$ for the routes whose empty-route time is below $t$. In Lean these objects are routeTime b p i x, IsFeasible p Q q, IsEqualTimes b p Q q t and usedSet b t, all in the namespace WardropTraffic.EqualTimes.

Formalization targets

Goal: the closed form (23)–(24)

For every $Q$, $t$ and $q$, the split $q$ is feasible and satisfies the equal-times criterion with common time $t$ if and only if

$$q_i = \begin{cases} p_i\left(1 - \dfrac{b_i}{t}\right) & b_i < t,\\[4pt] 0 & \text{otherwise,}\end{cases} \qquad Q = \sum_{i \in U(t)} p_i - \frac{1}{t}\sum_{i \in U(t)} p_i b_i .$$

This states which routes are used, the flow on each, and the relation between the total flow and the common journey time. The milestones are the steps of Wardrop's derivation:

1. $t_i(x) \ge b_i$ for $0 \le x < p_i$, with equality exactly when $x = 0$;
2. a route in use has $b_i < t$;
3. every route with $b_i < t$ is in use;
4. on a route in use, $q_i = p_i(1 - b_i/t)$, equation (23).

Companion: the equal-times split exists and is unique

If $0 < Q < \sum_i p_i$, there is exactly one pair $(q, t)$ satisfying the criterion. This formalizes the paper's closing sentence, that the solution is found "by picking out the value of $t$ which corresponds to the given $Q$".

Significance

The result. For parallel routes with journey times (22), the equilibrium is explicit. The common time $t$ is the root of a single scalar equation (24), and the flows follow from $t$ by (23). The derivation also shows a threshold structure: a route is used if and only if its empty-route time is below the equilibrium time. Adding flow raises $t$, and the routes enter the set in use one at a time, in increasing order of $b_i$. This structure is what the paper's second criterion (minimum average time, the next mission of this series) is compared with.

Formalizing it. The result is classical and its proof is elementary; it has not been machine-checked. The platform has the existence of a Wardrop equilibrium on general networks for delay functions that are total, continuous and increasing on $\mathbb R$, with no closed form. That model excludes the vertical asymptote of (22) at $q_i = p_i$ and has no empty-route time $b_i$. This mission adds the closed-form characterization for Wardrop's own model, both directions of it, and the existence and uniqueness of the split, including the corner cases that the printed criterion leaves open.

Difficulty

Each step is short. The difficulty is in the boundaries. The paper labels the routes so that $b_1 < \dots < b_D$ and speaks of "the first $j$ routes", with $b_j < t \not> b_{j+1}$. A faithful formal version has to say what happens at $t = b_{j+1}$, at ties among the $b_i$, at $t \le \min_i b_i$ (no route is used), and at a route used near capacity. The printed criterion says "less than" for unused routes, yet the derivation's own case split allows equality. With the strict comparison, an equal-times split fails to exist at the values of $Q$ where $t$ coincides with some $b_k$. The companion's uniqueness requires $Q > 0$: at $Q = 0$ every $t \le \min_i b_i$ is a common time of the zero split. Existence requires a continuity and monotonicity argument for the right-hand side of (24) as a function of $t$.

Formalization scope

• Routes are indexed by Fin D, and all quantities are real.
• The standing hypotheses are $b_i > 0$ and $p_i > 0$ for every $i$. Feasibility includes $q_i < p_i$, the range in which (22) is a positive finite journey time. Without it, Lean's $b_i/0 = 0$ would give a route at capacity journey time $0$.
• The criterion is formalized in the weak form $t \le b_i$ on unused routes, as the paper's derivation uses it. Every split satisfying the printed strict form satisfies it, and the definitions file records the implication. The goal under the weak form is therefore stronger than under the strict one.
• The ordering $b_1 < \dots < b_D$ is not assumed. "The first $j$ routes" becomes the set $U(t) = \{i : b_i < t\}$. This generalisation also covers ties.
• No sign condition on $t$ or $Q$ is assumed in the goal. For $t \le \min_i b_i$ the term $1/t$ multiplies an empty sum, and both sides of the equivalence force $q = 0$ and $Q = 0$.
• The goal is a two-sided equivalence for arbitrary $(Q, q, t)$. The companion requires $0 < Q < \sum_i p_i$ and asserts existence and uniqueness. Together they rule out a vacuous reading in which no split satisfies the criterion.

The development needs only the definitions above and basic real analysis (the intermediate value theorem for the companion). The model of a finite family of parallel routes with hyperbolic journey times is reusable for the minimum-average-time criterion. Proofs of the milestones, of the goal and of the companion are welcome.

Selected references

• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956 (RAND RM-1488, 1955). https://www.rand.org/pubs/research_memoranda/RM1488.html
• F. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, ch. 4. https://doi.org/10.1017/CBO9781139565363

Motivation

A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).

The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.

Timeline.

• 1949–1951: Brown proposes the method and conjectures convergence for zero-sum games.
• 1951: Robinson proves it for every vector system of every zero-sum matrix game; the statement contains no rate.
• 1958: Shapiro extracts from Robinson's argument a rate: the gap $(\max V(t) - \min U(t))/t$ is $O(t^{-1/(m+n-2)})$ (doi:10.1002/cpa.3160110408).
• 1964: Shapley gives a 3 × 3 bimatrix (non-zero-sum) game in which fictitious play does not converge (doi:10.1515/9781400882014-002).
• 1996: Monderer and Shapley prove convergence for games with identical interests (doi:10.1006/jeth.1996.0014).
• 2014: Daskalakis and Pan show that with adversarial tie-breaking the convergence can be much slower than the rate $t^{-1/2}$ conjectured by Karlin (arXiv:1412.4840).

Setting

Let $A = (a_{ij})$ be a real $m \times n$ matrix, $m, n \ge 1$. The first player chooses a row $i$, the second a column $j$, and the second pays the first $a_{ij}$. A mixed strategy is a probability vector $x = (x_1, \dots, x_m)$ for the first player, or $y = (y_1, \dots, y_n)$ for the second. For all mixed strategies,

$$\min_j \sum_i a_{ij} x_i \le \max_i \sum_j a_{ij} y_j. \tag{1}$$

A pair $(X, Y)$ for which equality holds is a solution, and the common number $v$ is the value of the game. The minimax theorem says that a solution exists.

Write $A_{i\cdot}$ for the $i$-th row, $A_{\cdot j}$ for the $j$-th column, and $\max W$, $\min W$ for the largest and smallest component of a vector $W$. A vector system for $A$ is a pair of sequences $U(0), U(1), \dots$ of $n$-vectors and $V(0), V(1), \dots$ of $m$-vectors with $\min U(0) = \max V(0)$ and

$$U(t+1) = U(t) + A_{i\cdot}, \qquad V(t+1) = V(t) + A_{\cdot j},$$

where $v_i(t) = \max V(t)$ and $u_j(t) = \min U(t)$. In the alternate vector system the column satisfies $u_j(t+1) = \min U(t+1)$ instead. A row $i$ is eligible in the interval $(t, t')$ if $v_i(t_1) = \max V(t_1)$ for some $t \le t_1 \le t'$, and similarly a column $j$ if $u_j(t_2) = \min U(t_2)$ for some $t \le t_2 \le t'$.

With $U(0) = V(0) = 0$, $U(t)/t$ is the payoff vector of the first player's empirical mixed strategy against each column, and $V(t)/t$ that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.

Formalization targets

Goal: the Theorem (p. 297)

For every vector system $(U, V)$ for $A$, and $v$ the value of the game,

$$\lim_{t\to\infty} \frac{\min U(t)}{t} = \lim_{t\to\infty} \frac{\max V(t)}{t} = v.$$

The statement holds for arbitrary initial vectors with $\min U(0) = \max V(0)$ and for every way of breaking ties.

Milestones, in the order of the proof

1. Inequality (1).
2. Lemma 1: $\liminf_{t\to\infty} (\max V(t) - \min U(t))/t \ge 0$.
3. Lemma 2: if every row and column is eligible in $(s, s+t)$, then $\max U(s+t) - \min U(s+t) \le 2at$ and $\max V(s+t) - \min V(s+t) \le 2at$, where $a = \max_{i,j}|a_{ij}|$.
4. Lemma 3: under the same hypothesis, $\max V(s+t) - \min U(s+t) \le 4at$.
5. Display (3) of the proof of Lemma 4: if some row or column is not eligible in $(s, s+t^*)$, the gap $\max V - \min U$ grows by less than $\tfrac12 \varepsilon t^*$ over that window, given the bound $\tfrac12\varepsilon t$ for the vector systems of the submatrices.
6. Lemma 4: for every $\varepsilon > 0$ there is $t_0$, uniform over all vector systems for $A$, with $\max V(t) - \min U(t) < \varepsilon t$ for $t \ge t_0$.
7. $(\max V(t) - \min U(t))/t \to 0$.
8. $\limsup \min U(t)/t \le v$ and $\liminf \max V(t)/t \ge v$.

Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing $\min U(t)/t \le v \le \max V(t')/t'$ when $U(0) = V(0) = 0$ (p. 297).

Significance

The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, $2\times n$ games, and continuous-time best-response dynamics.

The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.

Difficulty

Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap $\max V(t) - \min U(t)$ grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why $t_0$ in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.

Formalization scope

• Rows and columns are indexed by finite nonempty types ι, κ (the paper's $m, n \ge 1$); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.
• $\max W$, $\min W$ are Finset.sup' and Finset.inf' over all indices, hence attained.
• A vector system allows any maximizing row and minimizing column at each step (an existential per step). No tie-breaking rule is fixed, and the initial vectors are arbitrary subject to $\min U(0) = \max V(0)$. The case $U(0) = V(0) = 0$ is not imposed.
• Time is a natural number. Limits are Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in $\varepsilon$-form (for every $\varepsilon > 0$, eventually), with no boundedness side conditions.
• The value $v$ is given by a solution: every statement about $v$ assumes IsSolution A x y v, i.e. probability vectors $x$, $y$ with $\min_j \sum_i a_{ij} x_i = v = \max_i \sum_j a_{ij} y_j$. Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with $v$ free, or with "there exists $v$", would be false or would lose the identification with the value; neither is used.
• In Lemmas 2 and 3, $a$ is any upper bound on the $|a_{ij}|$. This is equivalent to the paper's $a = \max_{i,j}|a_{ij}|$.
• In display (3), the bound for submatrices is assumed only for the submatrices that delete one row or one column, which makes the statement at least as strong as the paper's.
• The paper's closing display on p. 301 prints $\lim \min V(t)/t$ for $\lim \min U(t)/t$. The goal follows the statement of the Theorem on p. 297.

A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.

Selected references

• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54(2), 296–301, 1951. https://doi.org/10.2307/1969530
• G. W. Brown, Some notes on computation of games solutions, RAND Report P-78, 1949. https://www.rand.org/pubs/papers/P78.html
• H. N. Shapiro, Note on a computation method in the theory of games, Communications on Pure and Applied Mathematics 11(4), 587–593, 1958. https://doi.org/10.1002/cpa.3160110408
• L. S. Shapley, Some topics in two-person games, Advances in Game Theory, Annals of Mathematics Studies 52, 1964. https://doi.org/10.1515/9781400882014-002
• D. Monderer, L. S. Shapley, Fictitious play property for games with identical interests, Journal of Economic Theory 68, 258–265, 1996. https://doi.org/10.1006/jeth.1996.0014
• C. Daskalakis, Q. Pan, A counter-example to Karlin's strong conjecture for fictitious play, FOCS 2014. https://arxiv.org/abs/1412.4840

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

$$\sup\ c\cdot x\quad\text{subject to}\quad x_1K_1+x_2K_2+\cdots+x_nK_n\subseteq K,\quad x_j\ge0,$$

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

$$\bar a_{ij}=\delta^*(e_i\mid K_j)=\sup_{a_j\in K_j}a_{ij},$$

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

$$\{x : x\ \text{feasible for (Ib)}\}=\{x : \bar Ax\le b,\ x\ge 0\},$$

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

$$(T\bar x,\, x-\bar x)\ge 0\qquad\forall x\in C .$$

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

$$(Tx^{n+1},\, x-x^{n+1})+\langle x^{n+1}-x^n,\, x-x^{n+1}\rangle\ge 0\qquad\forall x\in C. \tag{2}$$

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

$$\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in M .$$

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

$$0\in f(x)+\partial\psi_C(x),$$

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

$$\partial\psi_C(x)=\{y:\langle y,c-x\rangle\le 0\ \text{for all } c\in C\}\ \text{if } x\in C,\qquad \partial\psi_C(x)=\emptyset\ \text{if } x\notin C.$$

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

$$0\in Ax+a+\partial\psi_C(x).\qquad\text{(A.1)}$$

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

$$y\in Ax+a+\partial\psi_C(x)\qquad\text{(A.2)}$$

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

$$L=\{0\}\quad\text{or}\quad\forall z\in L\ \exists!\,w\in\mathbb R^n:\ z\in P_LAw+\partial\psi_T(w).$$

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