Optimization

Motivation

Policy gradient methods search directly over parameterized policies of a Markov decision process (MDP) by gradient ascent on the expected discounted reward. They are among the most widely used methods in reinforcement learning, yet the value $V^{\pi_\theta}(\rho)$ is a nonconcave function of the parameters, and until recently little was known about whether, or how fast, such methods reach a globally optimal policy. Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) give a systematic answer for tabular and function-approximation settings.

This mission formalizes one of their central results. Under the softmax parameterization, plain gradient ascent converges to optimal values only asymptotically (their Theorem 5.1, rate unknown): parameters can diverge and policies become nearly deterministic early, which stalls progress. Adding a log barrier regularizer, equivalent to a relative-entropy penalty towards the uniform policy, keeps action probabilities away from zero, and the paper shows that this yields an iteration count polynomial in every problem quantity. The result is the "softmax + log barrier" row of the paper's Table 1 and a reference point for later analyses of entropy-regularized policy gradient (for example Mei et al., 2020; Cen et al., 2021).

Setting

A finite MDP consists of finite sets $\mathcal S$ (states) and $\mathcal A$ (actions, nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns a probability distribution $\pi(\cdot\mid s)$ over actions to every state. Its value is $V^\pi(s)=\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid\pi,s_0=s]$, and for a distribution $\rho$ over states $V^\pi(\rho)=\mathbb E_{s\sim\rho}V^\pi(s)$. The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$.

The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$. Given a start distribution $\mu$ used by the algorithm, the distribution mismatch coefficient is $\|d^{\pi^\star}_\rho/\mu\|_\infty=\max_s d^{\pi^\star}_\rho(s)/\mu(s)$.

The softmax policy with parameter $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is $\pi_\theta(a\mid s)=\exp(\theta_{s,a})/\sum_{a'}\exp(\theta_{s,a'})$. For $\lambda>0$ the log barrier regularized objective is

$$L_\lambda(\theta)=V^{\pi_\theta}(\mu)+\frac{\lambda}{|\mathcal S|\,|\mathcal A|}\sum_{s,a}\log\pi_\theta(a\mid s)+\lambda\log|\mathcal A| =V^{\pi_\theta}(\mu)-\lambda\,\mathbb E_{s\sim\mathrm{Unif}_{\mathcal S}}\mathrm{KL}(\mathrm{Unif}_{\mathcal A},\pi_\theta(\cdot\mid s)),$$

and gradient ascent with step size $\eta$ is $\theta^{(t+1)}=\theta^{(t)}+\eta\nabla_\theta L_\lambda(\theta^{(t)})$. Write $V^{(t)}=V^{\pi_{\theta^{(t)}}}$.

Formalization targets

Goal: Corollary 5.1 (iteration complexity)

Let $D\ge d^{\pi^\star}_\rho(s)/\mu(s)$ for all $s$ (for example the mismatch coefficient), $\epsilon>0$, $\lambda=\epsilon(1-\gamma)/(2D)$, $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$ and $\eta=1/\beta_\lambda$. Starting from a parameter whose softmax policy is uniform (e.g. $\theta^{(0)}=0$),

$$\min_{t<T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\quad\text{whenever}\quad T\ge\frac{320\,|\mathcal S|^2|\mathcal A|^2}{(1-\gamma)^6\epsilon^2}\,D^2 .$$

Milestones

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot|s)}A^{\pi'}(s,a)$.
2. Lemma C.1 (softmax gradient): $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a|s)A^{\pi_\theta}(s,a)$.
3. Display (14): the same plus $\frac{\lambda}{|\mathcal S|}(\frac1{|\mathcal A|}-\pi_\theta(a|s))$ for $\partial L_\lambda/\partial\theta_{s,a}$.
4. Opening claim of the proof of Theorem 5.2: at an $\epsilon_{\rm opt}$-stationary point with $\epsilon_{\rm opt}\le\lambda/(2|\mathcal S||\mathcal A|)$, $\max_a A^{\pi_\theta}(s,a)\le 2\lambda/(\mu(s)|\mathcal S|)$.
5. Theorem 5.2: under the same hypotheses, $V^{\pi_\theta}(\rho)\ge V^\star(\rho)-\frac{2\lambda}{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty$.
6. Lemma D.4: $L_\lambda$ has $\beta_\lambda$-Lipschitz gradient, $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$.
7. Theorem E.1(3) (Beck, Theorem 10.15), unconstrained ascent form: for $\beta$-smooth $f\le M$ and step $1/\beta$, $\min_{t<T}\|\nabla f(x_t)\|\le\sqrt{2\beta(M-f(x_0))}/\sqrt T$.

Significance

The corollary shows that a first-order method on a nonconcave objective reaches an $\epsilon$-optimal policy in a number of steps polynomial in $|\mathcal S|$, $|\mathcal A|$, $1/(1-\gamma)$, $1/\epsilon$ and the mismatch coefficient, with no dependence on the MDP's structure beyond these quantities. Theorem 5.2 is of independent use: it certifies any approximately stationary point of the regularized objective, however it was found, as approximately optimal for the original problem. The dependence on $\|d^{\pi^\star}_\rho/\mu\|_\infty$ makes precise why the exploratory start distribution $\mu$ matters.

The results are proved in the paper; none of them is machine-checked. A formal development adds a checked softmax policy gradient formula on an infinite-horizon discounted MDP, a checked smoothness bound for the regularized objective, the nonconvex gradient-method rate in Euclidean space, and a corrected statement of the corollary (see the next sections). Lemma 3.2 and Lemma C.1 are reused across the other missions of this series.

Difficulty

The value function is not concave in $\theta$ and its gradient vanishes where policies become deterministic, so the standard route "small gradient implies near-optimal" fails for the unregularized objective. With the regularizer, the link between stationarity and optimality has to hold with explicit constants that do not degrade as policies approach the boundary of the simplex, which is where the unregularized argument breaks down. The second obstacle is smoothness: $V^{\pi_\theta}(\mu)$ is an infinite discounted sum of products of transition probabilities, and its Hessian must be bounded uniformly in $\theta$ by $8/(1-\gamma)^3$, which in Lean means differentiating a tsum of matrix-power–like terms in $\theta$. The policy gradient formula itself requires the same interchange of differentiation and infinite summation.

Formalization scope

States and actions are finite types; $\mathcal A$ is nonempty. Parameters live in EuclideanSpace ℝ (S × A), so $\|\cdot\|$ is the $\ell_2$ norm and $\nabla_\theta$ is Mathlib's gradient. The MDP layer (transition kernel, policy, occupation probabilities, $V^\pi$, $Q^\pi$, optimal policy) is the published FoundationsML.ReinforcementLearning library, and $V^\pi(\rho)$, $A^\pi$, $d^\pi_\rho$ are defined on top of it. Standing assumptions are those of §3: $P$ a kernel, $r\in[0,1]$, $0\le\gamma<1$, $\mu,\rho$ probability distributions, $\pi^\star$ optimal at every state.

Conventions committed to:

• the mismatch coefficient is replaced by any $D$ with $d^{\pi^\star}_\rho\le D\mu$ componentwise; no division by $\mu(s)$ occurs, and the same $D$ sets $\lambda$;
• $\min_{t<T}$ is "there is $t<T$ with …";
• $\lambda>0$, implicit in the paper, is a hypothesis of Theorem 5.2 and its proof-step milestone; $\lambda\ge0$ in Lemma D.4;
• Theorem E.1 is posed for ascent on $\mathbb R^d$ with an upper bound $M$ in place of an attained optimum.

Two corrections of the printed corollary. The printed statement allows "any initial $\theta^{(0)}$", but its proof uses $L_\lambda(\theta^\star)-L_\lambda(\theta^{(0)})\le1/(1-\gamma)$, valid for a uniform initial policy and false in general; the formal goal assumes a uniform start. The printed $\beta_\lambda=8\gamma/(1-\gamma)^3+2\lambda/|\mathcal S|$ contradicts the proof, which takes $\beta_\lambda$ from Lemma D.4, $8/(1-\gamma)^3+2\lambda/|\mathcal S|$; the formal goal uses the latter, with the same iteration count.

The goal is not trivialized by its encoding: the hypotheses fix the run completely from $\theta^{(0)}$, $\lambda$ and $\eta$, they are jointly satisfiable (a sorry-free check exhibits a one-state, two-action MDP with an optimal policy and $D=1$), and the conclusion concerns the unregularized value of the iterates. Theorem 5.2, Lemma D.4 and Theorem E.1 are milestones, not hypotheses of the goal.

Infrastructure that a complete development needs, and that is reusable beyond this mission: differentiability of discounted values in the policy parameters and the policy gradient theorem for the softmax class; Hessian bounds for softmax; the descent lemma and the $O(1/\sqrt T)$ rate of gradient methods for smooth nonconvex functions on Euclidean space. Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261v5
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• A. Beck, First-Order Methods in Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
• J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
• S. Cen, C. Cheng, Y. Chen, Y. Wei, Y. Chi, Fast Global Convergence of Natural Policy Gradient Methods with Entropy Regularization, Operations Research 70(4), 2022. https://arxiv.org/abs/2007.06558

Motivation

Bound constrained minimization asks for a low value of a smooth objective while each variable stays between prescribed lower and upper limits. Such limits occur in nonlinear optimization models even when the objective itself has no special convexity. Coleman and Li's interior reflective method was designed to approach a solution from inside those limits while using curvature information from a Newton system. Its local convergence claim explains what the method does after an iterate reaches the neighborhood of a suitably regular solution. The source is Coleman and Li (1994), especially Section 6 and Theorem 13.

The local result is distinct from a claim about finding that neighborhood. An algorithm can have excellent behavior near a solution without being guaranteed to reach it from every starting point. This mission isolates the precise local claim for the method in Fig. 11, including its reflected motion at a bound. It also records a regularity correction: the paper's stated twice continuous differentiability assumption alone does not imply a quadratic rate.

Setting

Let $f:\mathbb R^n\to\mathbb R$ be the objective and let $l_i\le x_i\le u_i$ describe a box $\mathcal F$. A lower bound may be $-\infty$ and an upper bound may be $+\infty$. The strict interior consists of points satisfying $l_i<x_i<u_i$ for every coordinate. Write $g(x)=\nabla f(x)$ and $H(x)=\nabla^2f(x)$.

The method's scaling vector $v(x)$ selects a bound according to the sign of $g_i(x)$. If $g_i(x)<0$, it uses $x_i-u_i$ when $u_i$ is finite and $-1$ otherwise. If $g_i(x)\ge0$, it uses $x_i-l_i$ when $l_i$ is finite and $1$ otherwise. Put $D(x)=\operatorname{diag}(|v_i(x)|^{1/2})$. The first order equation is $D(x)^2g(x)=0$. At an interior point, Fig. 11 chooses a scaled Newton direction $\widehat d$ from $\widehat B(x)\widehat d=-D(x)g(x)$ and sets $d=D(x)\widehat d$, where $\widehat B(x)$ is the scaled Hessian plus the diagonal correction in (2.5).

A reflective path $p_{x,d}(\alpha)$ follows $x+\alpha d$ and folds a coordinate back into the box whenever it crosses a finite bound. For a bounded coordinate this folding repeats after later crossings. The accepted value $\alpha_k$ obeys $|\alpha_k-1|\le\chi_\alpha\|D(x_k)^2g(x_k)\|$ and produces another strict interior point. Fig. 11 prints the rule as $|\alpha_k-1|=O(\|D_kg_k\|)$; the squared scaling is a second disclosed correction, explained below. The iteration is $x_{k+1}=x_k+p_{x_k,d_k}(\alpha_k)$.

At a candidate limit point $x_*$, nondegeneracy says that any coordinate with $g_i(x_*)=0$ lies strictly between its bounds. The free coordinates are those strictly between bounds. The second order sufficient conditions used here require that $x_*$ is feasible, $D(x_*)^2g(x_*)=0$, and the Hessian quadratic form is positive on every nonzero direction supported on the free coordinates. Section 6 also defines a finite family $F_\nu(x)=\operatorname{diag}(\nu(x))g(x)$ whose allowed coordinate choices come from (6.4). Coleman and Li, pp. 193–194 and 211–213 give these definitions and the local algorithm.

Formalization targets

Finite family and local Newton estimates

The supporting targets establish that the family vanishes at $x_*$ and has regular Jacobians there, that a scaled Fig. 11 direction is a Newton step for one family member, and that the reflected displacement is close to that direction. Lemma 12 makes the closeness quantitative at the coordinates that are active at $x_*$. Theorem 11 states the corresponding abstract local Newton result for a finite family of maps. These are the five milestones of the mission, ordered from the model and abstract estimate through the step and path estimates.

Quadratic convergence

The goal is the corrected local form of Theorem 13. For a fixed bound $\chi_\alpha\ge0$ on the permitted step size deviation, a common neighborhood and constant work for every Fig. 11 run starting there:

$$x_k\in\operatorname{int}(\mathcal F),\qquad \|x_{k+1}-x_*\|\le C\|x_k-x_*\|^2\quad(k\ge1), \qquad x_k\longrightarrow x_*.$$

The radius and $C$ are chosen before the run. A companion statement asserts that, when $\chi_\alpha>0$, a nearby interior point begins at least one run satisfying the algorithm's conditions.

Significance

The theorem gives a local rate for a feasible Newton method that can meet and reflect from finite bounds. It connects the behavior of the actual reflected iterates to Newton systems whose Jacobians are regular near $x_*$. This matters when the solution is on the boundary: convergence of an unconstrained Newton step by itself says nothing about whether the iterates remain feasible. Theorem 13 is a known paper result, and this mission asks for a machine checked proof of its corrected statement. None of this mission's seven draft theorems has a proof in the proposal; the published box definition is reused as an existing platform object.

The correction is mathematically material. In the one dimensional problem with no finite bounds and $f(x)=x^2/2+(2/5)|x|^{5/2}$, the objective is $C^2$ and $x_*=0$ meets the paper's nondegeneracy and second order conditions. Fig. 11 with $\alpha_k=1$ reduces to ordinary Newton iteration, whose error is of order $|x_k|^{3/2}$ rather than $|x_k|^2$. The source's proof invokes the Lipschitz Jacobian condition (6.5) of Theorem 11; the goal therefore assumes the Hessian is locally Lipschitz at $x_*$. This changes the literal hypotheses of the printed Theorem 13 and is disclosed in each relevant item.

The step-size rule needs a second correction. The proof on p. 212 asserts $\|D_kg_k\|=O(\|x_k-x_*\|)$ and so $|\alpha_k-1|=O(\|x_k-x_*\|)$. On $[0,\infty)$ with $f(x)=x$ and $x_*=0$, however, $D(x)g(x)=\sqrt x$, the Newton step is $d=-x$, and $\alpha_k=1-\chi_\alpha\sqrt{x_k}$ obeys the printed rule while giving $x_{k+1}=\chi_\alpha x_k^{3/2}$. The run predicate therefore bounds $|\alpha_k-1|$ by $\chi_\alpha\|D(x_k)^2g(x_k)\|$, which is $O(\|x_k-x_*\|)$ as the proof needs and is still computable without knowing $x_*$. Coleman and Li, Theorems 11 and 13 are the source of the two compared claims.

Difficulty

The scaling changes its coordinate formula when a gradient component changes sign, while the reflective path changes direction at each finite bound. A direct Newton estimate for an unreflected step does not control the displacement taken by Fig. 11. The finite family $F_\nu$ and the active-coordinate breakpoint estimate make the local statement precise across those choices. The abstract rate also needs a uniform regularity estimate for every member of that family. Twice continuous differentiability gives continuity of the Hessian, but it does not supply the linear modulus of continuity needed for a quadratic error bound.

Formalization scope

The variables are Euclidean vectors indexed by $\mathrm{Fin}(n)$; the paper's first iterate $x_1$ is Lean's sequence index zero. Bounds use extended reals, while all distances, derivatives and norms use real Euclidean space. A published definition supplies $\mathcal F$; this mission defines the strict interior, scaling, diagonal Newton correction, reflective map, run, nondegeneracy and second order condition, and the family $F_\nu$. The bounded-interval reflection uses the paper's repeated folding, including steps beyond the first breakpoint. Division in Lemma 12 is accompanied by a nonzero Newton component, and Newton directions are solutions of linear equations rather than values of a possibly undefined inverse.

The paper's standing assumption says that the initial sublevel set is compact and that $f$ is $C^2$ on an open set containing $\mathcal F$. The local statements retain the smoothness clause and omit compactness because no local conclusion uses it. The sole added regularity hypothesis in the goal is local Lipschitz continuity of $H$ at $x_*$; the run predicate uses the corrected step-size rule $|\alpha_k-1|\le\chi_\alpha\|D(x_k)^2g(x_k)\|$. The existence companion requires $\chi_\alpha>0$: if it were zero, the only allowed step size could hit a bound exactly. Neither the goal nor the run predicate assumes the iterates are already close after the start, that they converge, or that the scaled step is a Newton step for a chosen $F_\nu$; those are the claims to establish. A feasible interior start is required, so a box with an empty strict interior has no run. Contributions on the general finite family Newton estimate, active-coordinate ratio, reflected path, and existence of interior runs are all directly useful to the goal.

Selected references

• T. F. Coleman and Y. Li, On the convergence of interior-reflective Newton methods for nonlinear minimization subject to bounds, Mathematical Programming 67 (1994), 189–224. doi:10.1007/BF01582221.

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$, order enough to bring it up to the order-up-to level $S$. Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$, $j\ge0$, and $p_0<1$. An order costs $K>0$. $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$. The paper assumes only:

• $-G$ is unimodal: for some integer $m$, $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$;
• $\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$.

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$. The renewal density $m$ and renewal function $M$ are

$$m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).$$

For integers $s<S$, the long-run average cost of the (s, S) policy is

$$c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.$$

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$. The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$, $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$.

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$.

• Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$. Set $S^0:=y^*$, $c^0:=c(s,S^0)$ and $S:=y^*+1$.
• Step 1. While $G(S)\le c^0$: if $c(s,S)<c^0$, set $S^0:=S$, increase $s$ while $c(s,S^0)\le G(s+1)$, and set $c^0:=c(s,S^0)$. In either case, $S:=S+1$.

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$, every $K>0$, every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$, the algorithm terminates. On termination, with final values $s,S^0,c^0$,

$$c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.$$

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

1. the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$, and Lemma 0 on the comparisons it implies;
2. Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$;
3. Corollary 1, the stopping rule of Step 0;
4. Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$, which give the stopping rule of Step 1;
5. Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$, an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$, the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$. Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

• Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$. All costs are real.
• The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$, and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$, so every quantifier over reorder levels carries $s<S$.
• $m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$.
• The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$. Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$.
• Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$, $c^*(S)$, $y_i^*$, $\bar S^*$, $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$-statements, or binders characterised as least or greatest elements.
• The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
• Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$; leaving $c(s,S)$ unguarded for $s\ge S$.
• Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$, $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$, $K=1$, $G(0)=5$, $G(y)=10-0.1\cdot2^{-|y|}$ ($y\neq0$), $S=1$, where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
• Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$.
• Welcome contributions: general facts about the discrete renewal density ($m\ge0$, $M>0$), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

• Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

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

Motivation

A convex minimization problem comes with a dual maximization problem, and the dual value never exceeds the primal value. When the two values differ, a duality gap occurs. Dual bounds, Lagrangian relaxations and optimality certificates are then weaker than hoped. Conditions that rule the gap out are constraint qualifications such as Slater's condition and Rockafellar's notion of a stably set problem. Such conditions say when the gap vanishes, but not what the dual value is when it does not.

R. T. Rockafellar's 1967 paper answers that question for the Fenchel-type pair of problems built from a convex function, a concave function and a continuous linear map between infinite-dimensional spaces. Its Theorem 6 (§6, "Weak duality theorems", pp. 179–180) "explains the exact way in which inf (P) and sup (P*) can fail to be equal", by expressing the dual value through the primal problem alone: the dual supremum is the lower limit of the optimal values of slightly perturbed primal problems. This perturbational view of duality was later developed in Rockafellar's Conjugate Duality and Optimization (1974). It underlies the modern treatment of value functions in convex optimization.

Setting

Two real vector spaces $E$ and $E^*$ are topologically paired when each carries a locally convex Hausdorff topology, they are in duality under a bilinear form $\langle x,x^*\rangle$ that is continuous in each variable, and every continuous linear functional on either space is the pairing with exactly one element of the other. Let $(E,E^*)$ and $(F,F^*)$ be two such pairs. Let $A:E\to F$ be continuous linear and $A^*:F^*\to E^*$ its adjoint, the continuous linear map with $\langle Ax,y^*\rangle=\langle x,A^*y^*\rangle$.

A function $f:E\to[-\infty,+\infty]$ is convex when its epigraph $\{(x,\mu)\mid\mu\in\mathbb R,\ \mu\ge f(x)\}$ is convex in $E\times\mathbb R$. It is proper when it never takes $-\infty$ and is finite somewhere. A function $g$ is proper concave when $-g$ is convex, $g$ never takes $+\infty$, and $g$ is finite somewhere. The standing hypotheses are that $f$ is lower semicontinuous proper convex on $E$ and $g$ is upper semicontinuous proper concave on $F$. Their conjugates are

$$f^*(x^*)=\sup_{x}\{\langle x,x^*\rangle-f(x)\},\qquad g^*(y^*)=\inf_{y}\{\langle y,y^*\rangle-g(y)\}.$$

The primal problem (P) is to minimize $f(x)-g(Ax)$ over $x\in E$. The dual problem (P*) is to maximize $g^*(y^*)-f^*(A^*y^*)$ over $y^*\in F^*$. For $z\in F$ the perturbed problem (P($z$)) is to minimize $f(x)-g(Ax-z)$. Its value defines the perturbation function

$$h(z)=\inf(\mathrm P(z))=\inf_{x\in E}\{f(x)-g(Ax-z)\},\qquad h(0)=\inf(\mathrm P).$$

The lower semicontinuous hull of $h$ is $\bar h(y)=\liminf_{z\to y}h(z)$, where $z=y$ is allowed, so that $\bar h\le h$. All infima and suprema are taken in $[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 6

$$\sup(\mathrm P^*)=\liminf_{z\to 0}\,[\inf(\mathrm P(z))],$$

valid except in the trivial case where the left side is $-\infty$ and the right side is $+\infty$. No consistency, constraint qualification or attainment is assumed, and neither side need be finite. The exception is exactly the stated conjunction. A version assuming (P) consistent would be weaker, since an inconsistent (P), with $h(0)=+\infty$, may still have a finite lower limit.

Milestones: the four claims of the proof (p. 180)

1. $\bar h$ is a lower semicontinuous convex function on $F$.
2. For every $y^*\in F^*$, with $\bar h^*(y^*)=\sup_y\{\langle y,y^*\rangle-\bar h(y)\}$,

$$-\bar h^*(y^*)=\inf_y\{\bar h(y)-\langle y,y^*\rangle\}=\inf_z\{h(z)-\langle z,y^*\rangle\}=g^*(y^*)-f^*(A^*y^*).$$

3. (6.2): if $\bar h$ is proper, then $\bar h(0)=\sup_{y^*}\{\langle 0,y^*\rangle-\bar h^*(y^*)\}$.
4. If $\bar h$ is not proper, the maximand $g^*(y^*)-f^*(A^*y^*)$ of (P*) is identically $-\infty$.

The paper's Lemma 2 (convexity of $h$) is used by the first claim. It is a milestone of the companion mission on Theorem 3 of the same paper and is not restated here.

Significance

Theorem 6 reduces every question about the dual value to a question about the primal value function near the origin. Strong duality $\inf(\mathrm P)=\sup(\mathrm P^*)$ holds exactly when $h$ is lower semicontinuous at $0$ (outside the trivial case). A duality gap is exactly a downward jump of $h$ at $0$. The dual of (P*) obeys the same formula, which the paper uses to derive Theorem 7 on normal problems. An integer-lattice analogue appears in discrete convex analysis (Murota, Theorem 8.53, whose duality relation is already stated on Prove2Me as DiscreteConvex.ConjugacyDualityD.general_duality_relations). That statement has no topology and is not the same theorem.

The result is classical and its proof is published. As far as the platform's index shows, no machine-checked statement of it exists in the paper's generality, nor a statement of extended-real biconjugation on general paired locally convex spaces. The value of the mission is a formal proof in the paper's setting: arbitrary topologically paired spaces, extended-real-valued functions, and both the proper and the improper case of the hull. The biconjugation milestone (6.2) and the hull lemma are reusable for other perturbational duality results.

Difficulty

The obvious argument compares $h(0)$ with the dual objective directly. It cannot give the theorem, because $h$ may jump at $0$, and the dual objective does not detect the value of $h$ at a single point: the target is a lower limit, not a value. In infinite dimensions, conjugacy recovers a function only when it is lower semicontinuous and convex for a topology compatible with the pairing, so the statement depends on the full compatibility of the pairing on $F$, not on a norm. The usual statements of biconjugation cover proper functions only, whereas here the lower limit may take both values $\pm\infty$, and both cases of the theorem must be covered. Finally, extended-real arithmetic must be tracked so that the dual objective, defined from $f^*$, $g^*$ and $A^*$, is matched in every infinite case.

Formalization scope

Values lie in EReal. Infima and suprema are complete-lattice ⨅ and ⨆, so an empty or unbounded family gives $\pm\infty$ as in the paper. The lower limit is Filter.liminf h (nhds y) over the full neighbourhood filter: a punctured limit would change the theorem. Convexity is epigraph convexity in $E\times\mathbb R$, and properness is the paper's two-sided condition. A topological pairing is a structure holding a bilinear map, separate continuity, and existence and uniqueness of representing elements in both directions. No norm, inner product or finite dimension is assumed. The adjoint $A^*$ is continuous linear data satisfying the adjoint identity. The conjugates $f^*$, $g^*$ are defined by the paper's formulas from $f$, $g$, so their regularity is a consequence, not a hypothesis. Properness of $f$ and $g$ excludes the form $(+\infty)-(+\infty)$ from $f(x)-g(Ax-z)$ and from $g^*(y^*)-f^*(A^*y^*)$. No statement is repaired relative to the page.

The dual value is the supremum of the maximand built from $f^*$, $g^*$ and $A^*$ as on p. 172. Defining $\sup(\mathrm P^*)$ through $\bar h$ (for instance as the biconjugate of $\bar h$ at $0$) would make Theorem 6 true by definition and is ruled out.

A complete development needs extended-real conjugates on paired spaces, the lower semicontinuous hull and the closure of a convex epigraph, and Fenchel–Moreau for proper lower semicontinuous convex functions on a locally convex space. All of these are reusable beyond this mission. Proofs of the milestones, and lemmas toward Fenchel–Moreau in this generality, are welcome contributions.

Selected references

• R. T. Rockafellar, Duality and Stability in Extremum Problems Involving Convex Functions, Pacific J. Math. 21 (1967), 167–187. https://doi.org/10.2140/pjm.1967.21.167
• W. Fenchel, On conjugate convex functions, Canad. J. Math. 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
• A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964) (reference [2] of the paper; no DOI).
• J.-J. Moreau, Fonctions convexes en dualité, multigraph, Séminaires de Mathématique, Faculté des Sciences, Université de Montpellier, 1962 (reference [12] of the paper; no DOI).
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• K. Murota, Discrete Convex Analysis, SIAM, 2003, Theorem 8.53. https://doi.org/10.1137/1.9780898718508