Operations Research

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$: a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$. Time is discrete, $t=0,1,2,\dots$. The iterate $x(t)\in\mathbb R^n$ evolves by

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),$$

where $\alpha_i(t)\in[0,1]$ is a stepsize ($\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$, the history up to the choice of the stepsizes at time $t$.

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

• Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
• Assumption 2: $x(0)$, $\alpha_i(t)$, $\tau^i_j(t)$ are $\mathcal F(t)$-measurable and $w_i(t)$ is $\mathcal F(t+1)$-measurable; $E[w_i(t)\mid\mathcal F(t)]=0$; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$.
• Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$.
• Assumption 4: $F$ is monotone ($x\le y\Rightarrow F(x)\le F(y)$), continuous, has a unique fixed point $x^*$, and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$.

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

$$\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}$$

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

1. Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$, and stepsizes with $\sum\alpha=\infty$, $\sum\alpha^2\le C$, $W(t)\to0$ with probability 1.
2. Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$, $U^0=x^*+re$, and $L^{k+1}=(L^k+F(L^k))/2$, $L^0=x^*-re$, satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$.
3. Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$.
4. Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$, where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$.
5. Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$.

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

• Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
• The update is stated in the paper's unified form for every $t$, with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
• Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$-set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$. Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
• Series conditions use partial sums (divergence to $+\infty$; every partial sum at most $C$), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
• The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
• Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$. Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ($k$, $t_k$, $t'_k$, $t''_k$, $X$, $\delta_k$) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
• A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$, or a second unrelated $x^*$) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$), and lemmas on monotone maps satisfying (7).

Selected references

• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
• C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
• B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.

Setting

There are items $1,\ldots,N$ in a tree rooted at end item $1$. Every item $i>1$ has one immediate successor $s(i)<i$; one unit of each component is needed for an end unit. Let $l_i$ be the production or delivery lead time of item $i$. The total lead time $M_i$ is the sum of lead times on the path from $i$ to the end item, with $M_0=0$, and the equivalent lead time is $L_i=M_i-M_{i-1}$. Items are indexed so that $M_i$ is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.

At the beginning of each period $t$, outstanding orders arrive, the controller chooses the post-order echelon position $Y_{it}$, and then demand $\xi_t$ for the end item occurs. The pre-order position is $X_{it}$, while $X^l_{kt}$ is the position of predecessor $k$ from orders old enough to arrive after its lead time. A decision is feasible when $X_{it}\le Y_{it}\le X^l_{kt}$ for every immediate predecessor $k$ of $i$. Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.

The discounted Problem P charges echelon holding cost $h_i$ for item $i$ and a shortage coefficient $p+H_1$ for the end item. Its discount factor is $\alpha$. The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over $l_1+1$ demands, with a constant independent of the policy. The paper's Assumption requires every $h_i>0$ and $\sum_i h_i\alpha^{-M_{s(i)}}<p+H_1$. The system is in long-run balance in period $t$ when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):

$$X^{M_i-\mu}_{it}\le X^{M_{i+1}-\mu}_{i+1,t} \quad(1\le i<N,\ 0\le\mu<M_i).$$

Formalization targets

Equivalent series optimal policies

The equivalent series system has successor $i-1$, lead time $L_i$, the same demand law and shortage coefficient, and holding coefficient $h_i\alpha^{l_i-L_i}$. Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:

$$\operatorname{Opt}(P)\subseteq\operatorname{Opt}(P_{\mathrm{series}}), \qquad \operatorname{Opt}(P)\ne\varnothing \Longrightarrow \operatorname{Opt}(P_{\mathrm{series}})\subseteq\operatorname{Opt}(P).$$

The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.

Significance

Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.

The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.

Difficulty

The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with $M_i=0$. The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.

Formalization scope

Items use the paper's indices $1,\ldots,N$, with $N\ge1$ and $s(1)=0$. Lean period $k$ is paper period $t=k+1$; the policy sees exactly $k$ earlier demands. The common demand law $\nu$ is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over $l_1+1$ periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.

Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when $M_i=0$. Discounting is restricted to $0<\alpha<1$: at $\alpha=1$ the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.

The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.

Selected references

• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. DOI: 10.1287/opre.37.4.565.

Motivation

A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.

For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis $\|P(f)\|<1$.

Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.

Setting

There are $S\ge 1$ states $1,\dots,S$. In state $s$ a finite nonempty set $A_s$ of actions is available; taking action $a$ earns the real reward $r(s,a)$ and assigns the transition weight $p(t\mid s,a)\ge 0$ to each state $t$. No bound on $\sum_t p(t\mid s,a)$ is assumed. The set of decision rules is $F=\times_{s=1}^S A_s$; for $f\in F$, $r(f)$ is the vector $(r(s,f(s)))_s$ and $P(f)$ the matrix $(p(t\mid s,f(s)))_{s,t}$.

A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules. The policy $f^\infty=(f,f,\dots)$ is stationary; $(g,\pi)=(g,f_1,f_2,\dots)$ uses $g$ first and then follows $\pi$; ${}^N\pi$ repeats the first $N$ rules of $\pi$ forever and is called periodic. Let $P^0(\pi)=I$ and $P^N(\pi)=P(f_1)\cdots P(f_N)$. The policy $\pi$ is transient if $\sum_{N\ge0}P^N(\pi)$ converges, and then its vector of total returns is

$$V(\pi)=\sum_{N=0}^\infty P^N(\pi)\,r(f_{N+1}).$$

The one-step comparison $v(g,\pi^*)=V(g,\pi^*)-V(\pi^*)$ measures the gain from deviating to $g$ for one step. Vectors are compared coordinatewise, and $x>y$ means $x\ge y$, $x\ne y$. For a matrix $B$, $\|B\|=\max_i\sum_j|b_{ij}|$ and $|\sigma(B)|$ is its spectral radius. Finally $V^*=\max_f V(f^\infty)$ and $\Re V=\max_g[r(g)+P(g)V]$, both coordinatewise.

Formalization targets

Goal: Corollary 6

If every stationary policy is transient, there is $f\in F$ with

$$V(\pi)\le V(f^\infty)\qquad\text{for every policy }\pi.$$

The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.

Milestones

1. Lemma 1. For transient $\pi=(g_i)$ and $\pi^*$: $V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*)$, and $V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*)$.
2. Lemma 2. If every stationary policy is transient and $f\in F$: either $v(g,f^\infty)>0$ for some $g$, and then $V(g^\infty)>V(f^\infty)$, or $v(g,f^\infty)\le0$ for all $g$, which holds iff $f^\infty$ is best among stationary policies.
3. Corollary 1. If every stationary policy is transient, some stationary policy maximizes $V$ over the stationary policies.
4. Corollary 2. Under the same hypothesis, $V^*$ is the unique fixed point of $\Re$.
5. Lemma 3 (Hoffman). For every $\varepsilon>0$ and every program there is a positively similar program with $\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon$.
6. Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to $\|P^N(\pi)\|<1$ for some $N\ge1$; with $\|P(g)\|\le1$ also to $\|P^S(\pi)\|<1$.
7. Theorem 1. If every stationary policy is transient and $\pi^*$ is any policy: $v(g,\pi^*)>0$ implies $V(g^\infty)>V(\pi^*)$, and $v(\cdot,\pi^*)\le0$ iff $V(\pi)\le V(\pi^*)$ for all $\pi$.

Significance

Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation $\Re V=V$ and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes $V(\pi)$ well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).

On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.

Difficulty

Without a contraction, the standard argument — $\Re$ is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: $\|P(g)\|$ may exceed one for every $g$, and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers $P(g)^N$, whereas the goal concerns infinite products of different matrices $P(f_1)P(f_2)\cdots$, whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.

Formalization scope

The Lean development fixes these conventions.

• States are a nonempty finite type St; actions are a family of nonempty finite types A : St → Type, so $F$ is the dependent function type (s : St) → A s, not a common action set.
• A program is a structure Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes $\|P(g)\|\le1$.
• Policies are deterministic Markov sequences ℕ → F, indexed from $0$: π 0 is $f_1$. "All policies" means all such sequences.
• Transience is Summable of $N\mapsto P^N(\pi)$ in the entrywise topology. $V$ is a tsum; it is the genuine series exactly for transient policies.
• $>$ on vectors is written out as $\ge$ and $\ne$; $\|\cdot\|$ is the maximum absolute row sum, defined explicitly; $|\sigma(\cdot)|$ is Mathlib's spectralRadius ℂ of the complexified matrix, valued in $[0,\infty]$.
• $V^*$ and $\Re$ are coordinatewise Finset.sup' over the finite set $F$.

A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is $0$, no statement compares $V$ of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.

A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative $(I-B)^{-1}=\sum B^N$, and finite-dimensional spectral theory relating $|\sigma(B)|<1$ to $B^N\to0$. These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.

Selected references

• A. F. Veinott, Jr., Discrete dynamic programming with sensitive discount optimality criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• D. Blackwell, Discrete dynamic programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• L. S. Shapley, Stochastic games, Proc. Nat. Acad. Sci. 39(10):1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2):165–177, 1967. https://doi.org/10.1137/1009030
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16

Motivation

Axiomatic bargaining theory asks which rule should divide a set of feasible utility vectors among a group of agents, and answers by listing properties a reasonable rule must have and determining the rules that have them. Nash's solution (Nash 1950) and the Kalai–Smorodinsky solution (Kalai and Smorodinsky 1975) are the two classical answers for a fixed set of two agents. Both characterizations take the number of agents as given.

In many division problems the group is not fixed: a supply of goods that was to be shared among some agents must later be shared among more. Thomson (1983) (Math. Oper. Res. 8:319–326) introduced a framework in which the population varies and a solution is a family of rules, one for each finite group. He proposed an axiom tying the rules for different groups together: when new agents arrive and the resources stay fixed, none of the original agents should gain (population monotonicity). The paper shows that this axiom, combined with four standard ones, singles out the Kalai–Smorodinsky solution.

Timeline.

• 1950: Nash characterizes the Nash solution for two agents.
• 1975: Kalai and Smorodinsky replace Nash's independence axiom by individual monotonicity and characterize their solution for two agents.
• 1980: Roth (Internat. J. Game Theory 8, 129–132, cited as [5] in Thomson 1983) discusses the $n$-agent extension; Thomson notes that without comprehensiveness the $n$-agent solution can fail weak Pareto-optimality once $n \ge 3$.
• 1983: Thomson characterizes the Kalai–Smorodinsky solution for a variable population by WPO, anonymity, scale invariance, continuity and population monotonicity. This is the result of this mission.

Setting

The agents are the natural numbers, and a group $P$ is a nonempty finite set of agents. For a group $P$, $\mathbb R^P$ is the space of real vectors indexed by $P$, and $\mathbb R^P_+$ its nonnegative orthant. For vectors, $x > y$ means $x_i > y_i$ for every $i$, $x \geqq y$ means $x_i \ge y_i$ for every $i$, and $x \geqslant y$ means $x \geqq y$ with $x \ne y$.

A division problem for $P$ is a set $S \subseteq \mathbb R^P_+$ that is compact, convex, contains a strictly positive vector, and is comprehensive: if $x \in S$ and $0 \leqq y \leqq x$, then $y \in S$. The class of these problems is $\Sigma^P$. The subclass $\tilde\Sigma^P$ also requires that whenever $x, y \in S$ and $y \geqslant x$, some $z \in S$ satisfies $z > x$.

A solution $F$ chooses a point $F^P(S) \in S$ for every group $P$ and every $S \in \Sigma^P$. The ideal point of $S$ is $a(S)$, with $a_i(S) = \max_{x \in S} x_i$. The Kalai–Smorodinsky solution $K$ selects the largest point of $S$ on the segment from the origin to $a(S)$:

$$K^P(S) = t^*\,a(S), \qquad t^* = \max\{t \ge 0 : t\,a(S) \in S\}.$$

The axioms on a solution $F$ are:

• WPO: no $y \in S$ has $y > F^P(S)$.
• PO: no $y \in S$ has $y \geqslant F^P(S)$.
• An: relabelling the agents along a bijection $\gamma : P \to P'$ relabels the outcome.
• S. Inv: rescaling each agent's utility by a positive factor rescales the outcome the same way.
• Cont: $F^P(S^k) \to F^P(S)$ whenever $S^k \to S$ in the Hausdorff metric.
• Mon: if $P \subseteq Q$, $S \in \Sigma^P$, $T \in \Sigma^Q$, and $S = T \cap \mathbb R^P$ (the points of $T$ that give zero to everyone outside $P$), then $F^P_i(S) \ge F^Q_i(T)$ for every $i \in P$.

Formalization targets

Goal: the characterization (Theorems 1 and 3)

For every solution $F$,

$$F \text{ satisfies WPO, An, S. Inv, Cont, Mon} \iff F^P(S) = K^P(S)\ \text{ for all finite } P \text{ and all } S \in \Sigma^P.$$

Milestones

1. Theorem 1. $K$ is a solution and satisfies WPO, An, S. Inv, Cont and Mon.
2. Theorem 2, $|P| = 2$. Under WPO, An, S. Inv and Mon, $F^P(S) \geqq K^P(S)$ for every two-agent group.
3. The replica problem (appendix). If $a(S) = e^P$, $a e^P \in S$ and $i_0 \in P$, there are $Q \supseteq P$ with $|Q| = 3|P| - 2$ and $T \in \Sigma^Q$ such that $T \cap \mathbb R^P = S$ and $a e^Q \in T$. In addition, every agent $j \in Q$ faces, in some slice of $T$, a relabelled copy of $S$ in which $j$ holds agent $i_0$'s position.
4. Theorem 2. Under WPO, An, S. Inv and Mon, $F^P(S) \geqq K^P(S)$ for every $P$ and every $S \in \Sigma^P$.
5. Corollary 1. Under the same four axioms, $F = K$ on every $\tilde\Sigma^P$.
6. Density. Every $S \in \Sigma^P$ is a Hausdorff limit of problems in $\tilde\Sigma^P$.
7. Theorem 3. WPO, An, S. Inv, Cont and Mon imply $F = K$ on every $\Sigma^P$.

Two further statements accompany the goal. Corollary 2 says that no solution satisfies PO, An, S. Inv and Mon. Lemma 1 says that some solution other than $K$ satisfies WPO, An, S. Inv and Mon.

Significance

The theorem identifies the Kalai–Smorodinsky solution as the only rule, among those treating agents symmetrically and ignoring utility units, under which an arrival of new claimants never benefits existing ones. Corollary 2 shows that weak Pareto-optimality cannot be strengthened to Pareto-optimality. Lemma 1 shows that continuity cannot be dropped. Together they fix the logical boundary of the result. The replica construction of the appendix is a reusable device: a problem in which every agent of a larger group faces an exact copy of one agent's situation.

The result has been proved since 1983. It has not been machine-checked, and to our knowledge no proof assistant library contains bargaining problems, solutions or the Kalai–Smorodinsky solution. The mission produces these definitions and checks the full argument, including two steps the paper asserts without proof. One is that the replica problem has the required slices. The other is that problems satisfying condition (c) are dense in the Hausdorff metric. Formalizing the paper also exposes a printed slip: Theorem 2 is stated as an equivalence, but only one direction is true and proved, and only that direction is stated here.

Difficulty

Theorem 1 asks for routine but real convex analysis. Continuity of $K$ requires the ideal point and the maximal scalar $t^*$ to move continuously with $S$ in the Hausdorff metric. Comprehensiveness and the strictly positive vector are what make this work.

The substance is in Theorem 2. The first thought is to compare $F^P(S)$ with $K^P(S)$ inside $S$ alone, using only WPO, An and S. Inv. That cannot work: Lemma 1 exhibits a solution satisfying all four axioms that differs from $K$, so the argument must leave the group $P$. The proof builds a larger problem $T$ in which every member of an enlarged group faces a copy of the worst-treated agent's position. Mon then caps each agent's payoff in $T$, and WPO fails at the diagonal point $a e^Q$. Choosing the groups and bijections, and verifying that each slice of the convex comprehensive hull is exactly the intended copy, is the delicate part. The paper dismisses it as "clear".

Theorem 3 needs the density of $\tilde\Sigma^P$ in $\Sigma^P$. An approximating problem must lose every flat face on its weak Pareto boundary while staying compact, convex and comprehensive.

Formalization scope

Agents are ℕ, where the paper uses $\{1, 2, \dots\}$; this relabelling is harmless. Groups are nonempty: for the empty group, $\mathbb R^\emptyset$ is a point and WPO would hold for no solution, so the page's "finite subsets" is read as nonempty finite subsets. A group is a Finset ℕ, and $\mathbb R^P$ is the function type P → ℝ, whose metric is the sup metric. Hausdorff convergence uses Mathlib's extended Hausdorff distance Metric.hausdorffEDist. Convergence in it is equivalent to Euclidean Hausdorff convergence, because the norms are equivalent.

A solution is a total function on all sets, together with the hypothesis IsSolution F that $F^P(S) \in S$ for $S \in \Sigma^P$. Every axiom quantifies over problems in $\Sigma^P$ only, and "$F$ is the Kalai–Smorodinsky solution" means agreement on every $\Sigma^P$. Two formalizations of the goal would be trivial or false, and the statements here rule out both: one that equates $F$ and $K$ as functions, and one that drops IsSolution.

The remaining conventions are these.

• $K$ and the ideal point use sSup. Both suprema are attained on $\Sigma^P$.
• $T \cap \mathbb R^P$ is the set of $x$ whose zero-extension lies in $T$.
• An quantifies over bijections P ≃ P'.
• Scalings have strictly positive factors.

Deviation from the page. Theorem 2's printed "if" direction is false, so only "only if" is stated. For example, choosing $(2,1,1)$ on $\mathrm{cch}\{(2,1,1),(0,2,0),(0,0,2)\}$ and $K$ elsewhere gives a solution with $F \geqq K$ that violates S. Inv. The replica milestone states the appendix construction existentially, for a generic agent $i_0$ instead of agent 1.

Out of scope: Theorem 4 (solutions defined on $\tilde\Sigma^P$ only, whose necessity proof is a sketch), and the remarks of §4.2–§4.4.

A complete development needs Hausdorff-metric continuity of maxima over compact sets and the convex comprehensive hull. It also needs elementary facts about slices and relabellings of comprehensive sets. All of these are reusable for other bargaining and fair-division formalizations. Contributions are welcome on any milestone, and on lemmas about $\Sigma^P$ that several milestones share.

Selected references

• W. Thomson, The fair division of a fixed supply among a growing population, Mathematics of Operations Research 8(3):319–326, 1983. https://doi.org/10.1287/moor.8.3.319
• E. Kalai and M. Smorodinsky, Other solutions to Nash's bargaining problem, Econometrica 43(3):513–518, 1975. https://doi.org/10.2307/1914280
• J. F. Nash, The bargaining problem, Econometrica 18(2):155–162, 1950. https://doi.org/10.2307/1907266
• A. E. Roth, An impossibility result for n-person games, International Journal of Game Theory 8:129–132, 1980 (as cited in Thomson 1983, reference [5]); see the reference list of https://doi.org/10.1287/moor.8.3.319

Motivation

The logarithm of a share price is commonly modelled as a Brownian motion with drift, $X_t=\sigma B_t+ct$. The Black–Scholes option pricing formula needs the volatility $\sigma$ but not the drift $c$, so a practitioner must estimate $\sigma^2$ from data. Observing the whole path would give $\sigma^2$ exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.

Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, $c=0$, and the Garman–Klass estimator is biased when $c\neq0$. Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator

$$\hat\sigma^2\equiv S_1(S_1-X_1)+I_1(I_1-X_1),$$

which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying a standard Brownian motion $B=(B_t)_{t\ge0}$: $B_0=0$, its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path $t\mapsto B_t(\omega)$ is continuous. Fix a drift $c\in\mathbb R$ and a volatility $\sigma\ge0$. The log-price is

$$X_t=\sigma B_t+ct,\qquad t\ge0,$$

and, for a trading period $[0,t]$, the running maximum and running minimum are

$$S_t=\sup_{0\le u\le t}X_u,\qquad I_t=\inf_{0\le u\le t}X_u.$$

Thus $S_t$, $I_t$ and $X_t$ are the high, the low and the close of the log-price (with the open normalized to $X_0=0$). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.

The proof in the paper passes through an exponential time: a random variable $T$ with $P(T>x)=e^{-\lambda x}$ (rate $\lambda>0$, mean $\lambda^{-1}$), independent of the whole path $B$. For $\sigma>0$ the rates

$$\alpha=\frac{\sqrt{c^2+2\lambda\sigma^2}-c}{\sigma^2},\qquad \beta=\frac{\sqrt{c^2+2\lambda\sigma^2}+c}{\sigma^2}$$

appear, in Lean alpha σ c lam and beta σ c lam.

Formalization targets

Goal: display (3)

For every $c\in\mathbb R$, every $\sigma\ge0$ and every $t\ge0$, $S_t(S_t-X_t)+I_t(I_t-X_t)$ is integrable and

$$E\big[S_t(S_t-X_t)+I_t(I_t-X_t)\big]=\sigma^2t.$$

At $t=1$ this is the unbiasedness of $\hat\sigma^2$ of display (2). The statement quantifies over all drifts; the absence of $c$ on the right-hand side is the content.

Milestones (Section 2, pp. 505–506)

1. At an independent exponential time $T$ of rate $\lambda$: $S_T\sim\operatorname{Exp}(\alpha)$ and $-I_T\sim\operatorname{Exp}(\beta)$.
2. The Wiener–Hopf splitting: $S_T$ and $S_T-X_T$ are independent, and $S_T-X_T$ has the law of $-I_T$.
3. $E[S_T(S_T-X_T)]=1/(\alpha\beta)=\sigma^2/2\lambda$.
4. $E[S_T(S_T-X_T)]=\int_0^\infty\lambda e^{-\lambda t}\,E[S_t(S_t-X_t)]\,dt$.
5. $E[S_t(S_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
6. $E[I_t(I_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
7. (off the goal's path) With $Y_1=S_1(S_1-X_1)$, $Y_2=I_1(I_1-X_1)$: $E Y_1^2=EY_2^2=\sigma^4/2$, $E(Y_1+Y_2)^2\le2\sigma^4$ and $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, for every drift $c$.

Significance

The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only $\sigma^2$ enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter $c$ is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, while the exact value $0.331\sigma^4$ quoted in the paper is only available at $c=0$.

On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.

Difficulty

The obvious approach, computing $E[S_t(S_t-X_t)]$ directly from the joint density of $(S_t,X_t)$ for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of $c$. The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to $c=0$ (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.

Formalization scope

• Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.
• $S_t$ and $I_t$ are the real sSup/sInf of the path over the interval $[0,t]$; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.
• "$E$" is the Bochner integral, and every expectation identity also asserts integrability, so no identity can hold through Lean's convention that a non-integrable function integrates to $0$.
• "$T$ exponential with mean $\lambda^{-1}$" is HasLaw T (expMeasure λ) P; "parameter $\alpha$" is read as rate $\alpha$. "Independent of $B$" is independence from the path-valued random variable with the product σ-algebra. $S_T$ is evaluated at $T$ truncated to $[0,\infty)$.
• "Has the same law as" is equality of image measures, together with the almost-everywhere measurability of both maps.
• "Inversion of the Laplace transform gives" becomes the fixed-time identity for every $t\ge0$ (milestones 5 and 6), separate from the Laplace identity (milestone 4).
• Milestones 1 and 3 assume $\sigma>0$ because $\alpha,\beta$ divide by $\sigma^2$; the Wiener–Hopf splitting, the goal, and milestones 4–7 allow $\sigma\ge0$.

A formalization that specializes to $c=0$, takes the supremum over all of $[0,\infty)$, or omits the integrability conjuncts is not the statement of this mission.

Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4), 1991, 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1), 1980, 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1), 1980, 61–65. https://doi.org/10.1086/296071
• P. Greenwood and J. Pitman, Fluctuation identities for Lévy processes and splitting at the maximum, Advances in Applied Probability 12(4), 1980, 893–902. https://doi.org/10.2307/1426747

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