Convex Optimization

Motivation

Many decision problems under uncertainty take the form of minimizing an expected cost $\varphi(x) = \mathbb E_\xi f(x, \xi)$ over a convex feasible set, where $\xi$ is a random parameter whose distribution can be sampled but not integrated in closed form. Evaluating $\varphi$ even approximately can cost exponentially many evaluations of $f$ in the dimension of $\xi$, so the classical deterministic notion of an approximate solution is unusable. A practical alternative, going back to Nemirovski and Yudin, asks for a random output $x$ whose expected objective value is close to the optimum: $\mathbb E\,\varphi(x) - \varphi^* \le \epsilon$. Stochastic subgradient methods achieve this; Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009)) shows that the same guarantee holds for a stochastic version of his method of simple dual averages, a scheme that aggregates all past subgradients in the dual space instead of taking projected steps with decreasing step sizes.

Dual averaging has since become a standard tool in stochastic and online convex optimization (regularized dual averaging, AdaGrad's primal-dual variant, distributed dual averaging). Section 6 of Nesterov's paper is the original statement of its expected-accuracy guarantee.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ and dual space $E^*$ with dual norm $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$. Let $Q \subseteq E$ be closed and convex, and let $d$ be a prox-function of $Q$: continuous on $Q$ and strongly convex on $Q$ with convexity parameter $\sigma > 0$,

$$d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x-y\|^2,$$

with prox-center $x_0 = \arg\min_{x\in Q} d(x)$ and $d(x_0) = 0$. For $\beta > 0$ and $s \in E^*$ the point $\pi_\beta(s) = \arg\min_{x \in Q}\{-\langle s, x\rangle + \beta d(x)\}$ is well defined. The scalar sequence $\hat\beta$ is given by $\hat\beta_0 = \hat\beta_1 = 1$ and $\hat\beta_{i+1} = \hat\beta_i + 1/\hat\beta_i$ for $i \ge 1$.

The stochastic problem is given by a probability space $(\Xi, \mu)$ and a cost $f : Q \times \Xi \to \mathbb R$ with $\varphi(x) = \mathbb E_\xi f(x,\xi)$ well defined on $Q$, and a minimizer $x^*$ of $\varphi$ over $Q$ with $\varphi^* = \varphi(x^*)$. Assumption 1: each $f(\cdot, \xi)$ is convex on $Q$. Assumption 2: a stochastic oracle returns a subgradient $f'(x, \xi)$ of $f(\cdot, \xi)$ at $x$, and $\|f'(x,\xi)\|_* \le L$ for all $x \in Q$, $\xi \in \Xi$.

The method of stochastic simple averages (SSA, (6.3)) fixes $\gamma > 0$, starts from $x_0$ and $s_0 = 0$, and for $k \ge 0$ draws a fresh independent sample $\xi_k \sim \mu$ and sets

$$s_{k+1} = s_k + f'(x_k, \xi_k), \qquad x_{k+1} = \pi_{\gamma\hat\beta_{k+1}}(-s_{k+1}).$$

Its deterministic counterpart, the method of simple dual averages (SDA, (2.21)), is the same recursion with arbitrary answers $g_k$ in place of $f'(x_k, \xi_k)$. The quality of the points $x_0,\dots,x_k$ is measured by the gap $\delta_k(D) = \max\{\sum_{i=0}^k\langle g_i, x_i - x\rangle : x \in Q,\ d(x)\le D\}$. Write $\boldsymbol\xi_k = (\xi_0, \dots, \xi_k)$ and $\mathbb E_{\boldsymbol\xi_k}$ for the expectation over these $k+1$ independent samples.

Formalization targets

Goal: Theorem 7 (p. 27)

For every $k \ge 0$,

$$\mathbb E_{\boldsymbol\xi_k}\Big(\varphi\Big(\frac{1}{k+1}\sum_{i=0}^k x_i\Big)\Big) - \varphi^* \le \frac{\hat\beta_{k+1}}{k+1}\Big(\gamma\, d(x^*) + \frac{L^2}{2\sigma\gamma}\Big).$$

Milestones

1. Theorem 2 (p. 11): for SDA with any answers $g_i$ and $L_k = \max_{i\le k}\|g_i\|_*$, $\delta_k(D) \le \hat\beta_{k+1}(\gamma D + L_k^2/(2\sigma\gamma))$ for $D \ge 0$, and, if some $x^* \in Q$ satisfies $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$, $\|x_k - x^*\|^2 \le \frac2\sigma d(x^*) + L_k^2/(\sigma^2\gamma^2)$.
2. (6.5) (p. 26): along every sample path, $\frac{1}{k+1}\tilde\delta_k(D) \le \frac{\hat\beta_{k+1}}{k+1}(\gamma D + \frac{L^2}{2\sigma\gamma})$.
3. Display after (6.5) (p. 26): for $D \ge d(x^*)$, the gap of a run dominates $\frac1{k+1}\sum_i\langle f'(x_i,\xi_i), x_i - x^*\rangle$, which dominates $\frac1{k+1}\sum_i[f(x_i,\xi_i) - f(x^*,\xi_i)]$.
4. (6.6) (p. 26): $\mathbb E_{\boldsymbol\xi_k}(\frac1{k+1}\delta_k(D)) \ge \frac1{k+1}\sum_i\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) - \varphi^*$.
5. p. 27, first display: $\mathbb E_{\boldsymbol\xi_k} f(x_i,\xi_i) = \mathbb E_{\boldsymbol\xi_k}\varphi(x_i)$ for $i \le k$.
6. p. 27, display before Theorem 7: $\frac1{k+1}\sum_i\mathbb E\varphi(x_i) \ge \mathbb E\varphi(\frac1{k+1}\sum_i x_i)$, together with the averaged identity.

Significance

Theorem 7 gives an explicit, non-asymptotic bound on the expected optimality gap of the averaged SSA point. Since $\hat\beta_{k+1} \approx \sqrt{2k}$, the bound is $O(1/\sqrt k)$, the optimal rate for nonsmooth stochastic convex optimization with bounded subgradients. Two features distinguish it from the classical stochastic subgradient bound: it holds in an arbitrary norm with a non-Euclidean prox-function (for example the entropy on the simplex with the $\ell_1$ norm), and the feasible set $Q$ need not be bounded, since only $d(x^*)$ enters. The constant is explicit and $\gamma$ can be tuned to $\gamma = L/\sqrt{2\sigma d(x^*)}$.

The result is proved in the paper; to our knowledge no machine-checked proof of Theorem 7 or of the dual averaging bounds of the paper exists. A formalization yields a reusable verified analysis of dual averaging in a general normed space, a template for expectation bounds over i.i.d. sample paths of an adaptive algorithm, and checked constants.

Difficulty

The pathwise part is a consequence of the deterministic Theorem 2, which itself rests on the general Dual Averaging bound (the companion mission's Theorem 1) and on the strong convexity estimates for $\pi_\beta$. The probabilistic part looks routine on paper but is where formal arguments break: the iterate $x_i$ is a function of $\xi_0, \dots, \xi_{i-1}$, and the identity $\mathbb E f(x_i, \xi_i) = \mathbb E\varphi(x_i)$ requires measurability of the whole run and a Fubini argument on the product space. Measurability of the run in turn depends on continuity of the argmin map $\pi_\beta$, and integrability of $\varphi(\bar x_k)$ and of the gap is not assumed but must be derived from the uniform bound $L$ and the boundedness of the iterates. Pathwise bounds alone do not suffice: (6.5) controls the gap on each sample, not $\varphi(\bar x_k)$.

Formalization scope

Theorem numbers and page numbers refer to source.pdf, the author's revised CORE discussion-paper version (September 2005) of the Math. Program. article; printed pages equal PDF pages.

• $E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, and $\langle s, x\rangle$ is s x. Strong convexity is Mathlib's StrongConvexOn Q σ d, which is exactly (1.8); $\sigma > 0$.
• $\pi$ is a map ℝ → StrongDual ℝ E → E with the hypothesis that $\pi_\beta(s)$ lies in $Q$ and minimizes $-\langle s, x\rangle + \beta d(x)$ for every $\beta > 0$; no choice function is used.
• $\hat\beta$ is defined by recursion with $\hat\beta_0 = \hat\beta_1 = 1$. The gap is a real supremum over $\mathcal F_D = \{x\in Q : d(x)\le D\}$, used only for $D \ge 0$, where the set is nonempty and bounded.
• Indices start at 0; $x_0$ is the prox-center. The run is a function of a sample path $\omega : \mathbb N \to \Xi$; $\mathbb E_{\boldsymbol\xi_k}$ is the integral against the product measure $\mu^{\otimes(k+1)}$ on $\Xi^{k+1}$ (the law of $k+1$ i.i.d. copies of $\xi$), with the finite sample padded to a sequence that the iterates never read.
• $f$ and $f'$ are functions on $E \times \Xi$ whose values off $Q$ are irrelevant; the subgradient inequality is relative to $Q$. Integrability of $f(x, \cdot)$ for $x \in Q$, and joint measurability of $f$ and $f'$, are explicit hypotheses. The paper uses measurability tacitly; without it a Lean integral of a non-measurable function is $0$ and the goal could become false.
• A statement for a fixed sample path, or with $\mathbb E\varphi(\bar x_k)$ replaced by a pathwise quantity, is a different and weaker theorem and does not count. Integrability of the run is not assumed: it is part of what must be proved.

A complete development needs the deterministic dual averaging analysis (Lemma 1, Lemma 2, Theorem 1 of the paper, restated here only through Theorem 2), measurability and continuity of $\pi_\beta$, and Fubini on finite products of probability spaces. The dual averaging lemmas and the product-measure lemmas for adaptive sample paths are reusable beyond this mission. Proofs of any milestone, and supporting lemmas on measurability of the SSA run, are welcome.

Selected references

• Yu. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009), 221–259. https://doi.org/10.1007/s10107-007-0149-x
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009), 1574–1609. https://doi.org/10.1137/070704277
• L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010), 2543–2596. https://jmlr.org/papers/v11/xiao10a.html

Motivation

Two-stage stochastic programming with recourse models a decision taken in two steps: a first-stage decision $x_1$ is fixed before a random outcome $s$ is observed, and a recourse decision $x_2(s)$ is taken afterwards, once $s$ is known. The model goes back to Dantzig (1955) and Beale (1955) and is the basic template of stochastic optimization in operations research: capacity planning before demand is known, production before prices are revealed, reservoir management before inflows are observed.

When the outcome space is not finite, the recourse is a function $x_2(\cdot)$, and the problem must specify the class of functions it ranges over. Rockafellar and Wets (Pacific J. Math. 62 (1976) 173–195) develop the duality theory of the convex case with recourse functions that are measurable and essentially bounded ($\mathcal L^\infty$), the setting in which the dual multipliers and their interpretation as prices become available. Their §3 asks whether that restriction loses anything: whether minimizing over $\mathcal L^\infty$ recourses gives the same first-stage problem as minimizing, scenario by scenario, the best attainable second-stage cost.

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. The data are closed convex nonempty sets $C_1\subseteq\mathbb R^{n_1}$, $C_2\subseteq\mathbb R^{n_2}$, finite convex functions $f_{10},f_{1i}$ on $\mathbb R^{n_1}$ ($i=1,\dots,m_1$), and functions $f_{20}(s,x_1,x_2)$, $f_{2i}(s,x_1,x_2)$ ($i=1,\dots,m_2$), finite and jointly convex in $(x_1,x_2)$ for each $s$, and measurable in $s$ for each $(x_1,x_2)$, summable for $i=0$ and bounded for $i\ge1$. These are the paper's standing assumptions.

With $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$, the essential objective of the problem $\mathbf P$ is

$$f(x_1,x_2)=F_1(x_1,0)+\int_S F_2\big(s,x_1,x_2(s),0\big)\,\sigma(ds),$$

where $F_1(x_1,u_1)=f_{10}(x_1)$ if $x_1\in C_1$ and $f_{1i}(x_1)\le u_{1i}$ for all $i$, and $+\infty$ otherwise, and $F_2(s,x_1,x_2,u_2)=f_{20}(s,x_1,x_2)$ if $x_2\in C_2$ and $f_{2i}(s,x_1,x_2)\le u_{2i}$ for all $i$, and $+\infty$ otherwise. Integrals of extended-real functions follow the paper's convention (2.4): the ordinary integral (real or $-\infty$) when the integrand is majorized by a summable function, and $+\infty$ otherwise.

Two first-stage problems are compared:

• the first-stage problem induced by $\mathbf P$ minimizes $J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2)$;
• the intrinsic first-stage problem $\mathbf Q$ minimizes $j(x_1)=F_1(x_1,0)+\int_S q(s,x_1)\,\sigma(ds)$, where $q(s,x_1)=\inf_{x_2\in\mathbb R^{n_2}}F_2(s,x_1,x_2,0)$ is the optimal recourse cost in scenario $s$.

The hypothesis of the general result uses $\rho(s,x_1)=\inf\{|x_2|\mid F_2(s,x_1,x_2,0)<+\infty\}$, the Euclidean distance from the origin to the feasible recourses ($+\infty$ if there are none), and calls $x_1$ intrinsically feasible when $j(x_1)<+\infty$. A normal convex integrand $h$ on $S\times\mathbb R^n$ is lower semicontinuous, convex and proper in $z$ for each $s$, with a measurability condition given by a sequence of measurable functions dense in each $\operatorname{dom}h(s,\cdot)$.

Formalization targets

Goal: Theorem 2 (p. 187)

If $C_2$ is bounded, then for every $x_1\in\mathbb R^{n_1}$

$$j(x_1)=J(x_1)=\inf_{x_2\in\mathcal L^\infty_{n_2}}f(x_1,x_2),\qquad \inf\mathbf Q=\inf\mathbf P,$$

the two first-stage problems have the same minimizers, and the infimum over $x_2\in\mathcal L^\infty_{n_2}$ is attained for each $x_1$.

Theorem 1 (p. 186)

If $\rho(\cdot,x_1)$ is essentially bounded for every intrinsically feasible $x_1$, then $j(x_1)=J(x_1)$ for all $x_1$, $\inf\mathbf Q=\inf\mathbf P$, and the minimizers coincide. Boundedness of $C_2$ is a special case of this hypothesis.

Milestones

• (2.1): $F(x,u)=F_1(x_1,u_1)+\int_S F_2(s,x_1,x_2(s),u_2(s))\,\sigma(ds)$ (p. 180);
• Proposition 1: for a normal convex integrand, $\inf_{z\in\mathcal L^p_n}\int_S h(s,z(s))\,\sigma(ds)=\int_S\inf_z h(s,z)\,\sigma(ds)$ whenever the left side is not $+\infty$ (p. 181);
• Proposition 2: $F_2$ is a normal convex integrand (p. 182);
• Proposition 4: $q(\cdot,x_1)$ is measurable (p. 185);
• (3.5)–(3.6): $j\le f$, hence $\inf\mathbf Q\le\inf\mathbf P$ (p. 186);
• the feasible-recourse multifunction (3.10) is measurable, $\rho$ is measurable, and the nearest feasible point is a measurable selection (p. 187);
• Theorem 1 (p. 186);
• with $C_2$ bounded, the argmin multifunction of $F_2(s,x_1,\cdot,0)$ is nonempty, compact, measurable and has a measurable selection (p. 188).

The Corollary of Theorem 2 (p. 188), that $x_1$ minimizes $\mathbf Q$ iff some $(x_1,x_2)$ minimizes $\mathbf P$, is included as a further statement.

Significance

The theorem justifies the modelling choice behind the paper's duality theory: when the second-stage constraint set is bounded, restricting recourse to essentially bounded measurable functions changes neither the optimal value nor the optimal first-stage decisions, and an optimal recourse function exists for every first stage. The duality theory of the companion mission (Theorem 3 of the same paper) is developed in that $\mathcal L^\infty$ setting, so the two results together describe the problem completely in the bounded case. Proposition 1, the interchange of infimum and integral for normal integrands, is a basic tool of stochastic programming and of the calculus of variations, used well beyond this paper.

The results are proved in the 1976 paper, relying on Rockafellar's earlier work on normal integrands and measurable selections. None of them has a machine-checked proof. Mathlib has the Lebesgue and Bochner integrals, $\mathcal L^p$ spaces and the measurable-selection prerequisites in partial form; it has no normal integrands, no extended-real integral convention of this kind, and no interchange theorem. A formal development produces those as reusable components.

Difficulty

The inequality $j\le J$ is immediate. The reverse inequality requires, from the pointwise infima $q(s,x_1)$, a single recourse function $x_2(\cdot)$ that is measurable, essentially bounded and nearly optimal in almost every scenario. Choosing a near-minimizer separately for each $s$ gives no measurability at all: the content is a measurable choice, and that needs the normality of $F_2$ and the measurability of the multifunctions of feasible and of optimal recourses. Essential boundedness is a second, independent obstacle: without a bound on $\rho$ every feasible recourse may be unbounded, and the infimum over $\mathcal L^\infty$ can then exceed $j$. Attainment in Theorem 2 needs, in addition, compactness of the argmin sets, which comes from the boundedness of $C_2$ and lower semicontinuity.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; indices $i=1,\dots,m$ are Fin m; $\mathcal L^\infty_n$ and $\mathcal L^p_n$ are Mathlib's Lp (Fin n → ℝ) p σ, so recourse functions are almost-everywhere classes and the second-stage constraints hold almost surely. $\sigma$ is a probability measure in every theorem. All extended-real quantities ($F$, $F_1$, $F_2$, $f$, $J$, $q$, $j$, $\rho$, $\inf\mathbf P$, $\inf\mathbf Q$) take values in EReal, and every infimum is the complete-lattice infimum, so an empty infimum is $+\infty$. The integral convention (2.4) is the published definition DupacovaWets.Consistency.expect: $+\infty$ when the positive part has infinite integral (for a measurable function, exactly when it has no summable majorant), and otherwise the difference of the lower Lebesgue integrals of the positive and negative parts. $|\cdot|$ in $\rho$ is the Euclidean length, not the sup norm. "Gives the minimum" is "has value $\le$ the value at every point". Measurability of a multifunction is the published definition DupacovaWets.Consistency.IsMeasurableMultifunction ($\{s\mid\Gamma(s)\cap K\ne\emptyset\}$ measurable for every closed $K$). The standing assumptions are fields of the structure Problem.

The integral of an extended-real function must not be replaced by a Bochner integral of its real part, which would turn $\pm\infty$ values into $0$ and make $j$ meaningless; and the infima must not be real sInf, which returns $0$ on unbounded sets.

Reusable beyond this mission: the notion of a normal convex integrand on a finite-dimensional space, and Proposition 1. Contributions of measurable-selection infrastructure (Kuratowski–Ryll-Nardzewski type theorems, measurability of distance functions of closed-valued multifunctions) are welcome as supporting lemmas. The mission "Stochastic Convex Programming: Basic Duality 1" formalizes the duality theorem of the same paper on the same model.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Measurable dependence of convex sets and functions on parameters, Journal of Mathematical Analysis and Applications 28 (1969) 4–25. https://doi.org/10.1016/0022-247X(69)90104-8
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• G. B. Dantzig, Linear programming under uncertainty, Management Science 1(3–4) (1955) 197–206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

Portfolio decisions in continuous time must respect both market uncertainty and investment restrictions. A ban on short sales, for example, restricts the vector of wealth fractions a trader may hold at every instant. The corresponding optimal consumption and investment problem is harder than its unrestricted counterpart because a candidate portfolio obtained from the usual pricing equations may violate the constraint. Cvitanić and Karatzas introduced auxiliary markets indexed by a process and used a dual optimization problem to establish existence of an optimal constrained policy in their 1992 paper. This mission formalizes the paper's existence theorem, Theorem 13.1, together with the results in Sections 12–13 that specify its dual target.

Setting

Fix a finite horizon $T>0$ and a complete probability space carrying a standard $d$-dimensional Brownian motion $W$. Information at time $t$ is the probability augmentation of the filtration generated by $W$ up to $t$. A bond earns short rate $r_t$; $d$ stocks have appreciation vector $b_t$ and volatility matrix $\sigma_t$. The market assumptions require progressively measurable coefficients, a uniform lower bound on $r$, uniform nondegeneracy of $\sigma\sigma^{\mathsf T}$, finite expected interest-rate integral, and finite energy of the market price of risk $\theta=\sigma^{-1}(b-r\mathbf1)$ §2.

A portfolio $\pi_t$ specifies fractions of wealth held in the stocks, while $c_t\geq0$ is consumption and $X_t$ is wealth. The feasible portfolios lie in a fixed nonempty closed convex set $K\subseteq\mathbb R^d$. Its support function is $\delta_K(v)=\sup_{\pi\in K}(-\pi\cdot v)$, which may equal $+\infty$. The process $\nu$ indexing an auxiliary market belongs to $\mathcal D$ when it has finite expected quadratic energy and finite expected integrated support value. Its deflator $H_\nu$ combines an interest-rate discount with a Brownian exponential. The class $\mathcal D'$ consists of those $\nu\in\mathcal D$ for which the budget map $\mathcal X_\nu(y)$ is finite for every $y>0$ §§4, 8.

The running utility $U_1(t,c)$ and terminal utility $U_2(X_T)$ are strictly increasing and strictly concave for positive arguments. An admissible constrained policy has nonnegative wealth, finite expected negative utility, and $\pi_t\in K$ for Lebesgue-time times probability almost every $(t,\omega)$. The primal value $V(x)$ is the supremum of its expected utility over all such policies with initial capital $x>0$. The dual value $\widetilde V(y)$ is the infimum, over $\nu\in\mathcal D$, of expected conjugate utility evaluated at $yH_\nu$ §§5–6, 12.

Formalization targets

Dual attainment

The first conclusion of Theorem 13.1 is the paper's condition (12.9):

$$\forall y>0\quad\exists\lambda_y\in\mathcal D'\quad\widetilde V(y)=\widetilde J(y;\lambda_y).$$

Thus the infimum is attained by a drift with a finite budget map. It is a conclusion of this mission, even though earlier Section 12 results assume it. The milestones include weak duality (12.8), the dual representation of Proposition 12.1, the capital-matching result of Proposition 12.2, and the analytic properties of the extended dual functional in Proposition 13.2 pp. 792–795.

An optimal constrained policy for every capital

The theorem's second conclusion is

$$\forall x>0\quad\exists (\widehat\pi,\widehat c,\widehat X)\in\mathcal A'(x)\quad\forall(\pi,c,X)\in\mathcal A'(x),\quad J(\pi,c,X)\leq J(\widehat\pi,\widehat c,\widehat X).$$

Here $\mathcal A'(x)$ is the constrained admissible class. Theorem 12.4 establishes this conclusion when dual attainment is assumed; Theorem 13.1 provides that assumption under the paper's stated utility and dual-finiteness conditions p. 794.

Significance

The result supplies an optimizer, rather than only a bound on the best attainable utility. It also identifies a minimizing auxiliary market for every positive dual parameter, making the dual description usable at a specified initial capital. The dual representation links the primal value to a convex function that can be studied without choosing a constrained policy first §§12–13.

The theorem is proved in the paper; the remaining work here is a machine-checked development of its definitions, hypotheses, and existence argument. The mission also produces reusable definitions of an almost-surely square-integrable Brownian integral relation, extended-real utility expectations, an extended support function, and constrained wealth classes. The Brownian state space and predictable step-sum substrate credit the published Ethier–Kurtz formalizations. The paper refers some analytic steps to earlier works instead of reproducing full proofs, including Lemma 12.3 and a final finiteness argument pp. 793–796.

Difficulty

Weak duality alone only bounds the constrained value from above. It does not supply a minimizer of $\widetilde J(y;\nu)$, and an arbitrary minimizing auxiliary process need not belong to $\mathcal D'$. The dual functional must retain meaningful infinite values on the full finite-energy process space $\mathcal H$; replacing them with total-operation defaults can turn the needed coercivity and lower-semicontinuity statements into different claims. Even after dual attainment, the minimizing parameter for a prescribed capital must match the budget map $\mathcal X_{\lambda_y}(y)$ §§12–13. These are the precise gaps between a numerical bound and the asserted optimal policy.

Formalization scope

Lean uses $\mathbb R^d$ with its Euclidean norm, a finite positive horizon, a complete probability measure, and the augmented Brownian filtration. Processes are functions of time and sample point; $\ell\otimes P$ almost-everywhere restrictions on portfolios and auxiliary drifts are distinct from pathwise $P$-almost-sure statements. A policy is represented by a triple $(\pi,c,X)$ whose wealth process satisfies the integral equation, matching the paper's pair together with its unique wealth solution. The integral operator is bound to the local Itô construction by predictable step approximations; it is not a free function. Integrands must be in its almost-sure square-integrable domain.

Support values, utility at zero, expected utility, and value functions use extended reals. The extension $U(0)$ is the right limit $U(0+)$; an extended-real supremum defines conjugate utility where zero arguments arise. The inverse marginal is a positive-argument inverse of $U'$. The minimization in $\widetilde V$ ranges over $\mathcal D$, while (12.9) asks for a minimizer in $\mathcal D'$. Its witnesses $\lambda_y$ remain explicit choices in statements involving $\mathcal X_{\lambda_y}$; no default-valued inverse $\mathcal Y_\nu$ is introduced. The functional $\widetilde J_y$ of (13.3) is defined on $\mathcal H$, uses the paper's formula on $\mathcal G$, and is $+\infty$ off $\mathcal G$. On $\mathcal D$ it agrees almost everywhere with the original dual objective, an equality requiring a formal lemma. Assumption 6.2 and conditions (5.8), (8.25), (12.2), (12.3), and (12.11) are explicit. Their quantifiers cover both utilities and every time in $[0,T]$ where stated. The mission rules out a vacuous dual-attainment hypothesis, a zero default for an unbounded support supremum, and an unconstrained stochastic-integral operator. Contributions proving the source milestones and the analytic lemmas they need are in scope.

Selected references

• Jakša Cvitanić and Ioannis Karatzas, Convex Duality in Constrained Portfolio Optimization, The Annals of Applied Probability 2(4), 1992, 767–818. DOI: 10.1214/aoap/1177005576.

Why cores of games with side payments

A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.

The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.

Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition $A\subseteq N$ is identified with its characteristic vector $\tau^A\in\{0,1\}^n$, and $\tau^N=(1,\dots,1)$. A fuzzy coalition is a vector $\tau\in[0,1]^n$, where $\tau_i$ is the rate at which player $i$ participates.

A fuzzy game with side payments is a worth function $v$ with $v(0)=0$ that is positively homogeneous, $v(t\tau)=t\,v(\tau)$ for $t>0$. Homogeneity extends $v$ from $[0,1]^n$ to the orthant $\mathbb R^n_+$. Its core is

$$\operatorname{core}(v)=\Big\{c\in\mathbb R^n:\ \sum_{i\in N}c_i=v(\tau^N),\ \ \sum_{i\in N}\tau_ic_i\ge v(\tau)\ \text{for all }\tau\in[0,1]^n\Big\},$$

the allocations that no fuzzy coalition blocks. The superdifferential of $v$ at $\tau$ is $\partial v(\tau)=\{c:\ v(\tau)-v(\sigma)\ge\sum_i c_i(\tau_i-\sigma_i)\ \text{for all }\sigma\in\mathbb R^n_+\}$.

A usual game with side payments is given by a family $\mathscr C$ of nonempty coalitions that contains $N$ and every singleton $\{i\}$, and by a worth $v(A)\in\mathbb R$ for each $A\in\mathscr C$. Its core is the set of $c\in\mathbb R^n$ with $\sum_{i\in N}c_i=v(N)$ and $\sum_{i\in A}c_i\ge v(A)$ for every $A\in\mathscr C$. For $\tau\in\mathbb R^n_+$, $\mathscr C(\tau)$ is the set of nonnegative weights $m(A)$, $A\in\mathscr C$, with $\sum_{A\ni i}m(A)=\tau_i$ for each player $i$, and

$$\pi v(\tau)=\sup_{m\in\mathscr C(\tau)}\ \sum_{A\in\mathscr C}m(A)\,v(A).$$

The game is balanced if $\pi v(\tau^N)=v(N)$.

Formalization targets

Goal: Proposition 6.1

$$\operatorname{core}(v)\neq\emptyset\iff \pi v(\tau^N)=v(N),\qquad\text{and then}\qquad \operatorname{core}(v)=\operatorname{core}(\pi v).$$

The first half is the Bondareva–Shapley theorem for an arbitrary family $\mathscr C$. The second identifies the core of the discrete game with the core of the fuzzy game $\pi v$.

Milestones

1. §2 (4)–(5). For a positively homogeneous $v$ with $v(0)=0$, $\operatorname{core}(v)=\partial v(\tau^N)$.
2. Remark 2.1. Such a $v$ is concave on $\mathbb R^n_+$ if and only if it is superadditive, $v(\tau+\sigma)\ge v(\tau)+v(\sigma)$.
3. Proposition 2.1. If $v$ is moreover concave, its core is convex, compact and nonempty; if $v$ is differentiable at $\tau^N$, the core is $\{Dv(\tau^N)\}$.
4. §6 (5). If $m\in\mathscr C(\tau)$ and $m(A)>0$, then $A\subseteq A_\tau=\{i:\tau_i>0\}$.
5. §6 (2). $\pi v$ is the smallest concave positively homogeneous function on $\mathbb R^n_+$ with $\pi v(\tau^A)\ge v(A)$ for every $A\in\mathscr C$.
6. §6, after (6). The core of the fuzzy game $\pi v$ is nonempty, convex and compact, whether or not $v$ is balanced.

Significance

Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when $\pi v$ is smooth at $\tau^N$, reduces to a single point given by the gradient.

The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family $\mathscr C$ of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension $\pi v$. The definitions (fuzzy coalitions, balances, $\pi v$) are reusable by later missions on games without side payments and on values of fuzzy games.

Difficulty

The inclusion $\operatorname{core}(v)\subseteq\operatorname{core}(\pi v)$ and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from $\pi v(\tau^N)=v(N)$, a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because $\pi v$ is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.

Formalization scope

Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:

• A fuzzy game is a function on $\mathbb R^n$ whose values off the orthant are never used; $v(0)=0$ and homogeneity for every $t>0$ and $\tau\ge0$ are hypotheses of every §2 statement, because §2 states them once for the whole section. Concavity is concavity on $\mathbb R^n_+$.
• In the superdifferential (5), $\sigma$ ranges over $\mathbb R^n_+$, the domain of the extended $v$; the paper leaves this implicit.
• "Differentiable at $\tau^N$" is DifferentiableAt at the interior point $(1,\dots,1)$, and $Dv(\tau^N)$ is the vector of partial derivatives.
• The family $\mathscr C$ contains $N$ and all singletons and excludes $\emptyset$; the core and $\pi v$ use only coalitions in $\mathscr C$, so $v(\emptyset)=0$ plays no role. Because $N\in\mathscr C$ and $\emptyset\notin\mathscr C$, the family exists only for $n\ge1$.
• $\pi v$ is a real supremum. For $\tau\ge0$ the set of values is nonempty and bounded above, so the value is the paper's; off the orthant the set is empty and the value is never used.
• The printed $v(\mathscr C)$ and $\tau^{\mathscr C}$ in §6 (2)–(3) are read as $v(A)$ and $\tau^A$, as §6 (4) settles.

Balancedness is the equation $\pi v(\tau^N)=v(N)$ with $\pi v$ built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes $\pi v$ to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1), 1981, 1–13. https://doi.org/10.1287/moor.6.1.1
• O. N. Bondareva, Some applications of linear programming methods to the theory of cooperative games, Problemy Kibernetiki 10, 1963, 119–139 (in Russian; no stable online copy).
• L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14(4), 1967, 453–460. https://doi.org/10.1002/nav.3800140404
• H. E. Scarf, The core of an N person game, Econometrica 35(1), 1967, 50–69. https://doi.org/10.2307/1909703
• L. J. Billera, Some theorems on the core of an n-person game without side-payments, SIAM Journal on Applied Mathematics 18(3), 1970, 567–579. https://doi.org/10.1137/0118007
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Why marginal allocation needs a convex hull

Service organizations keep repairable spare parts at a depot and at operating bases. Stock has a purchase or holding cost, while insufficient stock leaves backorders. Craig Sherbrooke's METRIC study describes how to evaluate such a system and distribute additional units among item types. Its fifth computational stage compares the reduction in expected backorders from the next unit with the cost of that unit. The comparison is delicate because the backorder function after optimizing the depot–base split can fail to be convex as a function of total item stock, even though a fixed depot-stock version is convex. Sherbrooke therefore introduces a convex extension before applying marginal analysis (Sherbrooke 1968, pp. 134–135).

This mission isolates the theorem in the paper's Appendix. It concerns abstract item functions with the properties needed for the allocation rule, so the result can be studied independently of the queueing assumptions and the FORTRAN procedure that produced those functions in METRIC. The paper supplies a proof of the Appendix theorem; the mission seeks a machine-checked formalization of its precise mathematical content (Sherbrooke 1968, pp. 140–141).

Setting: stock levels, costs, and the lower boundary

There is a finite collection of items indexed by $i$. A decision assigns each item a stock level $m_i\in\mathbb N$, where $0$ is permitted. Item $i$ has a unit cost $c_i$ and a real-valued function $\Xi_i(m)$ representing the backorder contribution associated with stock level $m$. In the METRIC application, $\Xi_i$ is obtained after choosing the best allocation of $m$ units between depot and bases. The Appendix theorem uses only that $\Xi_i$ is nonincreasing and has a finite lower bound. “Decreasing” is read weakly: the paper's justification says that adding a unit “cannot exceed” the backorders at the previous level (Sherbrooke 1968, p. 136).

For a function $g:\mathbb N\to\mathbb R$, write $\Delta g(m)=g(m+1)-g(m)$. The function is discretely convex when $\Delta g(m+1)\ge\Delta g(m)$ at every level. The lower convex hull $H_i$, written $\Xi_i'$ in the paper, is the greatest discretely convex function at or below $\Xi_i$. It follows the lower boundary of the convex hull of the points $(m,\Xi_i(m))$; a point above that boundary is lowered, while a contact point keeps its original value (Sherbrooke 1968, pp. 135–136, 140). The existing ServiceParts.StockLevels.Basic definition supplies $\Delta$ and $\Delta^2$ for real stock-level functions; this mission reuses it.

The original objective is the separable sum

$$J(m)=\sum_i\bigl(c_i m_i+\Xi_i(m_i)\bigr).$$

For each item, conditions (12) select the first level $\bar m_i$ where adding another unit no longer lowers the convexified cost:

$$c_i+H_i(\bar m_i+1)-H_i(\bar m_i)\ge0,\qquad \bar m_i>0\Longrightarrow c_i+H_i(\bar m_i)-H_i(\bar m_i-1)<0.$$

The second condition is automatic at $\bar m_i=0$, following the paper's convention $H_i(-1)=+\infty$ (Sherbrooke 1968, p. 140, Eqs. (11)–(12)).

Formalization targets

The Appendix goal is that each item's conditions (12) have exactly one solution and that the vector formed from those solutions minimizes the original, possibly nonconvex objective:

$$\forall i\;\exists!\bar m_i\in\mathbb N\text{ satisfying (12)}, \qquad J(\bar m)\le J(m)\quad\text{for every }m\in\mathbb N^I.$$

The milestone list follows the Appendix's claims: the lower boundary is a convex minorant; its marginal changes approach zero; (12) has a solution and that solution is unique; it minimizes the convexified single-item cost; and the selected level is a contact point where $H_i(\bar m_i)=\Xi_i(\bar m_i)$. The final comparison is with $J$, not just with the objective formed from $H_i$ (Sherbrooke 1968, pp. 140–141).

What the result establishes

The theorem licenses the paper's marginal allocation rule even when an item's original backorder function has nonconvex points. The rule can use a convex lower boundary to identify a level, yet the resulting allocation is optimal for the original function. Without the contact-point conclusion, optimality of the modified objective alone would not give that guarantee. The theorem is stated for any finite number of independent items with the listed properties, so it is reusable beyond the specific depot–base model (Sherbrooke 1968, pp. 134–136, 140–141).

The paper proves the result informally. This mission's definitions and theorem statements compile locally as open Lean goals; they do not yet constitute a machine-checked proof. A related published Prove2Me result, ServiceParts.Allocation.allocOpt_correct, proves correctness of an allocation algorithm for piecewise-linear functions assumed convex. It does not address the convexification or contact claim here. The platform's posed ServiceParts.StockLevels.optimal_stock_criterion and greedy_fill_rate_optimal concern other marginal criteria and likewise do not settle this Appendix theorem. A successful development would provide reusable Lean infrastructure for lower convex envelopes of integer sequences, their forward differences, and separable finite allocations.

Difficulty

A one-step marginal comparison on the raw $\Xi_i$ is insufficient when its forward differences can fall and then rise: an apparent local stopping point need not minimize the full sequence. Replacing $\Xi_i$ by a convex minorant restores ordered marginal changes, but a minimizer of a smaller function need not minimize the original function. The central burden is therefore the exact relation between the lower boundary and the original points at a level selected by the strict condition in (12). Ties in the objective add a second precision issue: the selected level is unique under the rule even when the objective has more than one minimizer (Sherbrooke 1968, pp. 135, 140–141).

Formalization scope and conventions

Stock levels are natural numbers, item contributions and costs are real, and the item type is finite; the empty item type is allowed, making both the sum and the coordinatewise statement trivial. The functions $\Xi_i$ are nonincreasing and bounded below, as in the Appendix. The lower hull is a pointwise real supremum over all discretely convex minorants. Its defining family is nonempty and bounded at each point under the lower-bound hypothesis, which every hull theorem carries. The hull is therefore fixed by the input function rather than supplied as an arbitrary minorant. The goal compares every vector in $\mathbb N^I$, without a budget restriction. The formalization does not use a default value for $H_i(-1)$: the predecessor condition applies only to positive stock levels.

The paper prints $c_i\ge0$ with at least one positive cost. Its existence assertion fails when a particular $c_i=0$: for $\Xi_i(m)=1/(m+1)$, a bounded, decreasing, convex sequence, the first inequality of (12) never holds. The goal and existence milestone therefore require $c_i>0$ for every present item. The paper's phrase “unique optimizing” is interpreted as uniqueness of the stock vector determined by (12), together with its optimality. It cannot assert uniqueness among all minimizers: with $c=1$, $\Xi(0)=1$, and $\Xi(m)=0$ for $m\ge1$, levels $0$ and $1$ tie. The proof's own wording identifies (12) as the unique selection rule (Sherbrooke 1968, p. 140).

The formalization contains separate definitions for discrete convexity, the greatest lower hull, conditions (12), and objective (11). It welcomes proofs and general lemmas about convex integer sequences and finite separable sums. The METRIC computation, empirical Air Force data, equations (7)–(9), and the discussion of Lagrangian versus combinatorial solutions are context rather than goals of this mission. A definition that simply sets $H_i=\Xi_i$, or a conclusion that minimizes only the hull objective, would omit the theorem's content.

Selected references

• Craig C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1), 122–141, 1968. DOI: 10.1287/opre.16.1.122.

Motivation

The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian $L_r$ and reinterpreted it as unconstrained maximization of a smooth concave dual function $g_r$. Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.

Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through $L_r$ and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.

Setting

Let $X \subset \mathbb R^n$ be convex and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex. The problem is

$$\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \text{ subject to } f_i(x) \le 0,\ i = 1, \dots, m.$$

With $\theta(t) = \max\{0, t\}$ and a parameter $r > 0$, the penalty Lagrangian is

$$L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big], \qquad x \in X,\ y \in \mathbb R^m,$$

and the dual problem $(D_r)$ maximizes $g_r(y) = \inf_{x \in X} L_r(x, y)$ over all $y \in \mathbb R^m$; $\sup g_r$ is its supremum. A maximizing sequence is a sequence $\{y^k\}$ with $g_r(y^k) \to \sup g_r$. The dual method of Theorem 4.1 takes a bounded maximizing sequence $\{y^k\}$ and, for each $k$, a point $x^k \in X$ that minimizes $L_r(\cdot, y^k)$ to within a tolerance $\alpha_k$:

$$L_r(x^k, y^k) - g_r(y^k) \le \alpha_k, \qquad \alpha_k \to 0. \qquad (4.7)$$

The standing assumptions of §5 concern a point $\bar x \in \operatorname{int} X$ that is an optimal solution of (P), near which $f_0, \dots, f_m$ are twice continuously differentiable, and a multiplier vector $\bar y$ satisfying with $\bar x$ the Kuhn–Tucker conditions ($\bar y_i \ge 0$, $f_i(\bar x) \le 0$, $\bar y_i f_i(\bar x) = 0$, and $\bar x$ minimizes $f_0 + \sum_i \bar y_i f_i$ over $X$). With $I = \{i : f_i(\bar x) = 0\}$ the active set and $H(x, y) = \nabla^2 f_0(x) + \sum_{i \in I} y_i \nabla^2 f_i(x)$, they are: (i) $\bar y_i \ne 0$ for $i \in I$; (ii) the $\nabla f_i(\bar x)$, $i \in I$, are linearly independent; (iii) $z \cdot H(\bar x, \bar y) z > 0$ for every nonzero $z$ with $z \cdot \nabla f_i(\bar x) = 0$ for all $i \in I$.

Formalization targets

Goal: Corollary 5.3

Under the standing assumptions, with $\{y^k\}, \{x^k\}, \{\alpha_k\}$ as in (4.7), if for some $q > 0$

$$\alpha_k \le q\,[\sup g_r - g_r(y^k)] \quad \text{for all sufficiently large } k, \qquad (5.18)$$

then there is a constant $s > 0$ with

$$|x^k - \bar x| \le s\,|y^k - \bar y| \quad \text{for all sufficiently large } k. \qquad (5.19)$$

No rate for $\{y^k\}$ is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.

Milestones

1. $\bar x$ is the unique optimal solution to (P) and $\bar y$ the unique optimal solution to the ordinary dual $(D_0)$ and every $(D_r)$ for $r > 0$ (§5, after (5.1)).
2. Theorem 5.1 (i)–(iii): for every $r, \beta > 0$ there are $\varepsilon, \alpha > 0$ such that $\sup g_r - g_r(y) \le \varepsilon$ and $L_r(x, y) - g_r(y) \le \alpha$ force $(x, y)$ into a $\beta$-neighborhood of $(\bar x, \bar y)$ with $x \in \operatorname{int} X$, where $L_r$ is $C^2$, given locally by (5.4), and $\nabla_x^2 L_r(x, y)$ is positive definite.
3. Theorem 5.1 (iv): the unique minimizer $\xi(y)$ of $L_r(\cdot, y)$ over $X$ is $C^1$ in $y$ with derivative (5.5).
4. Theorem 5.1 (v): $g_r$ is $C^2$ with negative definite Hessian (5.6)–(5.7).
5. Corollary 5.2 (5.14): $x^k \to \bar x$ and $y^k \to \bar y$.
6. Corollary 5.2 (5.15)–(5.17): $a|x^k - \xi(y^k)|^2 \le \alpha_k$, $b_1|y^k - \bar y|_I \le |\xi(y^k) - \bar x| \le b_2|y^k - \bar y|_I$, and $c_1|y^k - \bar y|^2 \le g_r(\bar y) - g_r(y^k) \le c_2|y^k - \bar y|^2$.

Significance

Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since $g_r$ is $C^2$ with a negative definite Hessian near $\bar y$ (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to $g_r$ yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.

The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of $L_r$ and $g_r$, the implicit minimizer map $\xi$, and the rate comparison. Complete formal proofs of each milestone are the remaining work.

Difficulty

The obvious argument linearizes everything at $(\bar x, \bar y)$, but $L_r$ is only $C^1$ globally: $\theta^2$ has a kink in its second derivative, so smoothness of $L_r$ must first be established on a neighborhood of $(\bar x, \bar y)$, using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence $\{(x^k, y^k)\}$ is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with $\varepsilon, \alpha$ chosen after $r, \beta$) and the uniqueness of $\bar x$ and $\bar y$. The minimizer map $\xi$ then comes from the implicit function theorem applied to $\nabla_x L_r(x, y) = 0$, and the formula for $\nabla^2 g_r$ needs the derivative of the envelope $g_r(y) = L_r(\xi(y), y)$.

Formalization scope

• Spaces. Primal points lie in EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and $f_0$ is a separate argument.
• Functions. The $f_i$ are total functions on $\mathbb R^n$; convexity is assumed on $X$ only (ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of $\bar x$. Smoothness of $L_r$ and $g_r$ is always a conclusion, never a hypothesis.
• Extended values. $g_0$, $g_r$, $\sup g_r$ and the infimum in (P) are computed in EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in $[-\infty, +\infty]$; $r > 0$ is explicit for the penalty Lagrangian, while $L_0$ is defined separately.
• Derivatives. Hessians are quadratic forms $z \cdot D(\nabla\varphi)(x) z$; every inverse matrix appears together with positive definiteness of the same matrix, so Lean's convention that a non-invertible map has inverse $0$ never applies. Local identities such as (5.4) are stated as equality on a neighborhood, not globally.
• Choices. The assumption of Theorem 4.1 that the asymptotic optimal value is finite is omitted because it holds under the §5 assumptions. "Generated as in Theorem 4.1" is spelled out as its hypotheses. In (5.15)–(5.17), $\xi$ is any function that picks a minimizer of $L_r(\cdot, y)$ over $X$ whenever one exists; along $y^k$ it eventually coincides with the paper's unique minimizer. In (iv) and (v), the conclusions are stated for every $y$ with $\sup g_r - g_r(y) \le \varepsilon$, since they do not depend on $x$.
• Ruled out. The goal does not assume that $x^k$ or $y^k$ converge, nor that $y^k \ne \bar y$, and $s > 0$ is one constant valid for all large $k$; a formalization assuming convergence, or one with an unsatisfiable second-order hypothesis, would be trivial. The standing assumptions and all sequence hypotheses are satisfiable (checked on $f_0(x) = |x|^2$, $f_1(x) = 1 - e\cdot x$ in $\mathbb R^1$).
• Infrastructure. The proofs need the implicit function theorem (Mathlib's Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a $C^2$ function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
• M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
• R. T. Rockafellar, The multiplier method of Hestenes and Powell applied to convex programming, Journal of Optimization Theory and Applications 12 (1973) 555–562. https://doi.org/10.1007/BF00934777
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1 (1976) 97–116. https://doi.org/10.1287/moor.1.2.97