Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$-stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$, ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$, $u\in U(x)$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$. A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

$$T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

and let $T^k$ be the $k$-fold composition of $T$. A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$-stage cost of $\pi$ and the $N$-stage optimal cost are

$$J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).$$

A policy is uniformly $N$-stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$-stage optimal, and $N$-stage $\varepsilon$-optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$.

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$), and F.3 (a quantitative selection property with a constant $\beta>0$).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$:

$$J^*_N=T^N(J_0),$$

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$.

Milestones

• Proposition 3.3: $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$. Needs monotonicity only.
• Corollary 3.3.1: a uniformly $N$-stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$.
• Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy exists.
• Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$.
• Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$.
• Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$, $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$, policies with $\{\varepsilon_n\}$-dominated convergence to optimality exist.
• Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$, the DP algorithm gives $J^*_N$ and $N$-stage $\varepsilon$-optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$. Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$. The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$-optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$, which is why F.3 and the definition of $\varepsilon$-optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$. Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$.

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$, so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

Iterative methods for optimization and equation solving on a smooth constraint set $\mathcal M$ (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector $u$ in the tangent space at the current iterate $x$ and then have to return to $\mathcal M$. The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, $R(x,0)=x$, and first-order agreement with the exponential.

Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from $x$ to $x+u$, then come back to $\mathcal M$ along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.

Setting

Let $\mathcal E$ be a Euclidean space of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a $C^k$ submanifold of dimension $d$ if around every $\bar x\in\mathcal M$ it is a coordinate slice: there are an open neighbourhood $\mathcal U$ of $\bar x$ and a $C^k$ diffeomorphism $\phi$ of $\mathcal U$ onto an open subset of $\mathbb R^n$ with $\mathcal M\cap\mathcal U=\{x\in\mathcal U:\phi_{d+1}(x)=\dots=\phi_n(x)=0\}$. Throughout, $k\ge2$.

The tangent space $\mathrm T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ of tangent directions of $\mathcal M$ at $x$, the normal space $\mathrm N_{\mathcal M}(x)$ is its orthogonal complement, and the tangent bundle is $\mathrm T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in\mathrm T_{\mathcal M}(x)\}$.

A map $R$ from $\mathrm T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if, on a neighbourhood $\mathcal U$ of $(\bar x,0)$ in $\mathrm T\mathcal M$, it is of class $C^{k-1}$, satisfies $R(x,0)=x$, and $u\mapsto R(x,u)$ has derivative $\mathrm{id}_{\mathrm T_{\mathcal M}(x)}$ at $u=0$. It is a retraction on $\mathcal M$ if this holds around every point.

A retractor (Definition 4.1) is a $C^{k-1}$ map $D$, defined on a neighbourhood of the zero section of $\mathrm T\mathcal M$, with values in the Grassmann manifold $\mathrm{Gr}(n-d,\mathcal E)$ of $(n-d)$-dimensional linear subspaces, such that $D(x,0)\cap\mathrm T_{\mathcal M}(x)=\{0\}$ for every $x\in\mathcal M$. Given $D$, set $\mathcal D(x,u)=x+u+D(x,u)$ and let

$$R(x,u)=\{\text{points of }\mathcal M\cap\mathcal D(x,u)\text{ nearest to }x+u\}.$$

Formalization targets

Goal: Theorem 4.2 (retractors give retractions)

$$\forall\bar x\in\mathcal M\ \ \exists r:\quad R(x,u)=\{r(x,u)\}\ \text{ for }(x,u)\in\mathrm T\mathcal M\text{ near }(\bar x,0),\quad\text{and } r \text{ is a retraction around } \bar x.$$

The theorem asserts both that the point-to-set map $R$ is single-valued near the zero section and that it is a retraction there.

Milestone: Lemma 4.7 (the normal case $D(x,u)=\mathrm N_{\mathcal M}(x)$)

Near $(\bar x,0)$ there is one and only one smallest $v(x,u)\in\mathrm N_{\mathcal M}(x)$ with $x+u+v(x,u)\in\mathcal M$; $\mathrm D_u v(x,0)=0$; and $R(x,u)=x+u+v(x,u)$ is a retraction around $\bar x$, hence on $\mathcal M$.

Milestone: Lemma 4.8 (straightening up)

On a neighbourhood of the zero section, $D(x,u)=\{v+A(x,u)v:\ v\in\mathrm N_{\mathcal M}(x)\}$ for a unique linear $A(x,u):\mathrm N_{\mathcal M}(x)\to\mathrm T_{\mathcal M}(x)$ depending $C^{k-1}$ on $(x,u)$.

Further: Theorem 4.9 (second order)

If $k\ge3$ and $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$, then $\frac{\mathrm d^2}{\mathrm dt^2}R(x,tu)|_{t=0}\in\mathrm N_{\mathcal M}(x)$ for all $(x,u)\in\mathrm T\mathcal M$.

Significance

Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at $u=0$. The orthographic retraction ($D=\mathrm N_{\mathcal M}(x)$) and the projective retraction $R(x,u)=P_{\mathcal M}(x+u)$ ($D=\mathrm N_{\mathcal M}(P_{\mathcal M}(x+u))$) are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at $u=0$ only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving $C^{k-1}$ regularity jointly in $(x,u)$, not only in $u$ (Remark 4.4 of the paper).

The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.

Difficulty

The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown $v$ lives in the normal space $\mathrm N_{\mathcal M}(x)$, which moves with $x$, and $(x,u)$ ranges over the tangent bundle, a $C^{k-1}$ submanifold of $\mathcal E\times\mathcal E$ rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in $(x,u,v)$, and turning it into "the smallest $v$", or "the nearest point of $\mathcal M\cap\mathcal D(x,u)$", requires excluding far-away intersection points. For a general retractor, the subspace $D(x,u)$ also moves, and has to be written as a graph over the normal space with a $C^{k-1}$ dependence before a second implicit-function argument applies.

Formalization scope

$\mathcal E$ is a finite-dimensional real inner product space E, $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $2\le k$ and $d\le n$ (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. $\mathrm T_{\mathcal M}(x)$ is the span of Mathlib's tangent cone (chart-free), $\mathrm N_{\mathcal M}(x)$ its orthogonal complement. Retractions and retractors are total maps on $\mathcal E\times\mathcal E$ constrained only on $O\cap\mathrm T\mathcal M$ with $O$ open; "of class $C^{k-1}$ on a subset of $\mathrm T\mathcal M$" is ContDiffOn on that set. A Grassmannian-valued map is $C^{k-1}$ when its orthogonal projector $P_{D(x,u)}$ is, and the dimension $n-d$ of $D(x,u)$ is part of the definition. The set-valued $R$ uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, $A(x,u)$ is extended by $0$ on $\mathrm T_{\mathcal M}(x)$ so that it is an operator on $\mathcal E$. Theorem 4.9 assumes $k\ge3$, the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's "$D(\bar x,0)=\mathrm N_{\mathcal M}(x)$" as $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$.

The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set $R(x,u)$ to equal a singleton $\{r(x,u)\}$ (so it is nonempty) and that very $r$ to be a retraction. Theorem 4.9 requires the curve $t\mapsto R(x,tu)$ to be twice differentiable, so a junk second derivative of $0$ does not satisfy it.

A complete development needs: finite-rank facts for tangent spaces of slices ($\dim\mathrm T_{\mathcal M}(x)=d$), smoothness of $x\mapsto P_{\mathrm N_{\mathcal M}(x)}$, charts of $\mathrm T\mathcal M$ and of the Whitney sum $\mathrm T\mathcal M\oplus\mathrm N\mathcal M$, ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.

Selected references

• P.-A. Absil, J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version: https://hal.science/hal-00651608)
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
• R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens, M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22(3):359–390, 2002. https://doi.org/10.1093/imanum/22.3.359

Motivation

Many large convex programs have the form "minimize a strictly convex function $f$ subject to linear equations $Ax=b$". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When $A$ is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of $A$.

L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets $A_i$, in which each step replaces the current point by its $D$-projection onto one set: the minimizer of a distance-like function $D(\cdot,y)$ over that set. §2 chooses $D$ from the objective $f$ itself, $D(x,y)=f(x)-f(y)-(g(y),x-y)$ with $g$ the gradient of $f$; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes $f$ over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.

Setting

Work in the Euclidean space $E^p$ with inner product $(\cdot,\cdot)$. Let $S\subset E^p$ be a convex set with closure $\bar S$ and interior $\operatorname{int}S$. Let $f$ be strictly convex and continuously differentiable over $S$, with gradient $g(x)$ at $x\in S$, and continuous over $\bar S$. Let $A$ be an $m\times p$ matrix with nonzero rows $A_1,\dots,A_m$ and $b\in E^m$. The problem (2.1)–(2.3) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax=b,\ x\in\bar S,$$

with feasible set $R=\{x\in E^p\mid Ax=b,\ x\in\bar S\}$, assumed nonempty. A point of $R$ minimizing $f$ over $R$ is a solution.

The function (1.4) is

$$D(x,y)=f(x)-f(y)-\bigl(g(y),x-y\bigr),$$

and $A_i$ also denotes the hyperplane $\{x\mid (A_i,x)=b_i\}$. The paper assumes that $D$ satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every $y\in S$, a $D$-projection $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$. It also assumes condition (2): if $y^n\in S$ and $y^n\to y^*\in\bar S$, then $D(y^*,y^n)\to 0$.

A relaxation sequence with control $(i_n)_{n\ge0}$ starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. The control is any sequence of row indices. Finally,

$$Z=\{x\in S\mid g(x)=uA=\textstyle\sum_i u_iA_i\ \text{for some } u\in E^m\}$$

is the set of points of $S$ at which the gradient lies in the row space of $A$.

Formalization targets

Goal: Theorem 3

Assume that the $D$-projection of every point of $\operatorname{int}S$ onto every $A_i$ lies in $\operatorname{int}S$. For every control and every relaxation sequence with $x^0\in Z\cap\operatorname{int}S$ that converges to a point $x^*\in R$,

$$f(x^*)\le f(y)\qquad\text{for every } y\in R .$$

Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.

Milestones

1. Lemma 3. If $y^*\in R\cap\bar Z$, then $y^*$ is a solution of (2.1)–(2.3).
2. (2.7)–(2.8). For $x\in\operatorname{int}S$ there is $\lambda\in\mathbb R$ with $g(P_ix)=g(x)+\lambda A_i$ and $(A_i,P_ix)=b_i$.
3. Invariance of $Z$. $P_i$ maps $Z\cap\operatorname{int}S$ into $Z\cap\operatorname{int}S$.

An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.

Significance

Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier $\lambda$ of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for $f(x)=\tfrac12\|x\|^2$.

The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.

Difficulty

The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of $A$, so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on $S$, the limit may lie on the boundary of $S$ (or outside $S$, in $\bar S$), and $g$ need not extend continuously there, so the multipliers $u^n$ need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at $y^*$. Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that $P_i$ preserves $\operatorname{int}S$; on the boundary of $S$ a minimizer over $A_i\cap S$ need not satisfy (2.7).

Formalization scope

The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and $(A_i,x)$ is the real inner product. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt f (g x) S x for $x\in S$ and continuous on $S$; $S$ is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:

• The $D$-projection is a fixed map $P$; condition II says $P_iy$ minimizes $D(\cdot,y)$ over $A_i\cap S$, and condition III is stated for that map.
• Condition IV is assumed in its one-sided directional form (implied by the paper's), so theorems under it are at least as strong as the paper's.
• "Compact" in conditions V and VI is sequential compactness. Condition V is assumed for the points of $R\cap S$.
• Condition (2) is assumed for limits $y^*\in\bar S$; the page prints $y^*\in S$, but its use at a feasible point needs $\bar S$.
• Translation slips are corrected in the statements and recorded: condition II's "$D(z,x)$" and "$i\in T$", (2.7)'s "$g(x^{n-1})$" (read $g(x^{n+1})$), and "Theorems 1 − 3" (read Theorems 1–2).
• The control is an arbitrary sequence of indices in $\{0,\dots,m-1\}$; λ is named lam.
• Note 2 is stated for candidate points $y,z\in S$, where $g$ is meaningful.

The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open $S$, or to a limit assumed to lie in $Z$: any of these would trivialize the passage to the limit that the theorem is about.

A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality $f(x)\ge f(y)+(g(y),x-y)$ for $x\in\bar S$, $y\in S$, and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. doi:10.1016/0041-5553(67)90040-7
• Y. Censor, S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997. doi:10.1093/oso/9780195100624.001.0001
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. doi:10.1007/BF00934676

Motivation

A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function $K(x,y)$ that represents evaluation at $y$ is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.

Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.

Setting

Let $X$ be an arbitrary set and $E_1\subset E_2\subset\cdots$ subsets with union $E = E_1+E_2+\cdots = X$. For each $n$ let $F_n$ be a complex Hilbert space of functions on $E_n$, with norm $\|\cdot\|_n$, in which point evaluations are continuous; $K_n(x,y)$, for $x,y\in E_n$, is its reproducing kernel, characterized by $K_n(\cdot,y)\in F_n$ and

$$f(y) = (f, K_n(\cdot,y))_n \qquad (f\in F_n,\ y\in E_n),$$

with the scalar product $(f,g)_n$ linear in $f$. For $f_n\in F_n$ and $m\le n$, $f_{nm}$ denotes the restriction of $f_n$ to $E_m$. The standing assumptions of §9 A (p. 362) are:

1. $E_1\subset E_2\subset\cdots$ and $E = \bigcup_n E_n$;
2. the classes decrease: $f_{nm}\in F_m$ for every $f_n\in F_n$ and $m\le n$;
3. the norms increase: $\|f_{nm}\|_m\le\|f_n\|_n$ for every $f_n\in F_n$ and $m\le n$;

together with the existence of every kernel $K_n$. For two kernels on a set $Y$, $K_1\ll K$ means that $K-K_1$ is a positive matrix: $\sum_{i,j}(K-K_1)(y_i,y_j)\,\bar\xi_i\xi_j\ge 0$ for all finite families $y_i\in Y$, $\xi_i\in\mathbb C$. $K_{nm}$ is the restriction of $K_n$ to $E_m\times E_m$.

The limit class $F_0$ is the set of functions $f_0$ on $E$ such that (1°) every restriction $f_{0n}$ belongs to $F_n$ and (2°) $\lim_n\|f_{0n}\|_n<\infty$.

Formalization targets

Goal: §9, Theorem I (pp. 362–363)

Under the standing assumptions there is $K_0 : E\times E\to\mathbb C$ such that, whenever $x,y\in E_N$,

$$\lim_{n\to\infty}K_n(x,y)=K_0(x,y),$$

and $K_0$ is the reproducing kernel of $F_0$ with the norm

$$\|f_0\|_0=\lim_{n\to\infty}\|f_{0n}\|_n .$$

Milestones (in the order the proof uses them)

1. §9, Eq. (4): $K_{nm}\ll K_m$ for $m<n$.
2. §9, proof of Theorem I, p. 363: for $y\in E_k$, $\{K_m(y,y)\}_{m\ge k}$ is a decreasing sequence of non-negative numbers.
3. §9, Eq. (5): for $y\in E_k$, $k\le m\le n$, $\|K_{mk}(\cdot,y)-K_{nk}(\cdot,y)\|_k^2\le K_m(y,y)-K_n(y,y)$.
4. §9, Eq. (6): with $K_0$ the pointwise limit, $K_{0k}(\cdot,y)\in F_k$ and $\|K_{mk}(\cdot,y)-K_{0k}(\cdot,y)\|_k^2\le K_m(y,y)-K_0(y,y)$.
5. §9, Remark after Theorem I: under 1°, $\|f_{0n}\|_n$ is non-decreasing, so its limit exists, possibly infinite.
6. §9, Eq. (7): if $F_0$ carries the limit norm, then $(f_0,g_0)_0=\lim_n(f_{0n},g_{0n})_n$.

Significance

The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With $E_n=E$ for all $n$ (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels $K_1\gg K_2\gg\cdots$ on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of $K_m(\cdot,y)$ in every $F_k$.

Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order $\ll$ between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over $\mathbb C$, with kernels on varying domains.

Difficulty

The kernels $K_n$ live on different sets $E_n\times E_n$, so convergence is not convergence of a sequence of functions on one set: a pair $x,y$ enters the sequence only from the first $E_N$ containing both. The identification of the limit class needs three separate facts: that $F_0$ with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that $K_0(\cdot,y)\in F_0$, and that $K_0$ reproduces. The natural first idea, to embed all $F_n$ in one space and take an intersection, fails: the $F_n$ are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.

Formalization scope

• Scalars and spaces. Complex scalars throughout (Aronszajn works with complex Hilbert spaces from §1 on). Each $F_n$ is a type H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set $E$ is a type X with no topology, measure or nonemptiness assumption.
• Kernel. The scalar kernel kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's $(f,g)$ is ⟪g, f⟫_ℂ.
• Standing assumptions. (1)–(3) are the structure IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on $E_m$. Indexing starts at $0$.
• Order. $K_1\ll K$ is KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).
• Comparisons of kernel values ($K_m(y,y)\ge 0$, the right-hand sides of (5), (6)) are in Mathlib's ComplexOrder, which also asserts that these values are real.
• Convergence of kernels is stated only where the terms are defined: for $x,y\in E_N$, the sequence $j\mapsto K_{N+j}(x,y)$ converges to $K_0(x,y)$. Kernels are never extended by $0$ outside $E_n$.
• Condition 2° is convergence of $\|f_{0n}\|_n$ to a real number, not a supremum, and the norm of $F_0$ is stated as a limit (Tendsto).
• The goal asserts (a) the convergence, (b) the existence of an RKHS on $X$ with kernel $K_0$, and (c) that every RKHS on $X$ with kernel $K_0$ has exactly the functions of $F_0$ as its elements and the limit norm. A formalization that defines $F_0$ as RKHS.OfKernel K₀ and then asserts that its kernel is $K_0$ would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.
• Eq. (7) is stated for an inner product space of functions whose norm is assumed to be the limit norm; the paper's derivation that the limit norm is a quadratic form is the content of the goal.
• Non-vacuity. The constant sequence $E_n=E$, $F_n=F$ satisfies the standing assumptions (checked in Lean), and the one-point example $F_n=\mathbb C$ with norms $c_n|f|$, $c_n$ increasing, satisfies them with $K_n=c_n^{-2}$.

Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part I, Memoirs of the American Philosophical Society 1 (1935). (Positive matrices.)
• Mathlib, Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4

Motivation

Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.

Setting

Let $E$ be an arbitrary set and let $F$ be a class of complex-valued functions on $E$ that forms a complex Hilbert space with scalar product $(f, g)$, linear in $f$ and conjugate-linear in $g$. A reproducing kernel of $F$ is a function $K : E \times E \to \mathbb{C}$ such that, for every $y \in E$, the function $K(\cdot, y)$ belongs to $F$ and

$$f(y) = (f, K(\cdot, y)) \qquad \text{for every } f \in F.$$

Such a kernel exists exactly when every point evaluation $f \mapsto f(y)$ is continuous.

For a bounded linear operator $L$ on $F$, with adjoint $L^*$ defined by $(Lf, g) = (f, L^* g)$, the kernel of $L$ is

$$\Lambda(x, y) = L^*_x K(x, y),$$

the value at $x$ of the element $L^*(K(\cdot, y))$ of $F$. By the reproducing property, $Lf(y) = (f, \Lambda(\cdot, y))$ for every $f \in F$ and $y \in E$, so $L$ is determined by $\Lambda$.

A function $P : E \times E \to \mathbb{C}$ is a positive matrix if $\sum_{i,j} \overline{\xi_i}\, P(y_i, y_j)\, \xi_j \ge 0$ for every finite family of points $y_i \in E$ and complex numbers $\xi_i$. For two arbitrary functions $\Lambda_1, \Lambda_2$ on $E \times E$, one writes $\Lambda_1 \ll \Lambda_2$ if $\Lambda_2 - \Lambda_1$ is a positive matrix. A bounded operator $L$ is symmetric if $L = L^*$, and positive if $(Lf, f) \ge 0$ for every $f$. A symmetric $L$ has lower bound $\ge m$ and upper bound $\le M$ if

$$m\,(f, f) \le (Lf, f) \le M\,(f, f) \qquad \text{for every } f \in F.$$

A kernel $\Lambda$ is hermitian symmetric if $\Lambda(x, y) = \overline{\Lambda(y, x)}$.

Formalization targets

Goal: §11, Theorem I (p. 373)

For an arbitrary hermitian symmetric function $\Lambda : E \times E \to \mathbb{C}$ and real numbers $m, M$:

$$\exists\, L \text{ bounded, symmetric, with } \Lambda = L^*_x K(x,y) \text{ and } m(f,f) \le (Lf,f) \le M(f,f)\ \ \forall f \quad\Longleftrightarrow\quad mK \ll \Lambda \ll MK .$$

The function $\Lambda$ is not assumed to have $\Lambda(\cdot, y) \in F$; that membership is part of what the condition yields.

Milestones

1. §11, (3): the kernel of the adjoint, $\Lambda^*(y, z) = \overline{\Lambda(z, y)}$.
2. §11, (6): $L$ is symmetric if and only if $\Lambda$ is hermitian symmetric.
3. §11, (7): $L$ is positive if and only if $\Lambda$ is a positive matrix.
4. §11, (4): the kernel of a composition, $\Lambda(y, z) = (\Lambda_1(x, z), \overline{\Lambda_2(y, x)})_x$ for $L = L_1 L_2$.
5. §11, Theorem II: if $L_n u \to L u$ weakly for every $u$, then $\Lambda_n \to \Lambda$ pointwise; if $\|L_n - L\| \to 0$, then $\Lambda_n \to \Lambda$ uniformly on every set of couples $(x, y)$ on which $K(x, x)$ and $K(y, y)$ are uniformly bounded.
6. §11, Theorem III, first sentence: for complete orthonormal systems $\{g'_m\}$, $\{g''_n\}$ and $\alpha_{mn} = (g''_n, L g'_m)$,

$$\Lambda(x, y) = \lim_{p, q \to \infty} \sum_{m=1}^{p} \sum_{n=1}^{q} \alpha_{mn}\, g'_m(x)\, \overline{g''_n(y)} .$$

Significance

Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities $mI \le L \le MI$) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence $L \mapsto \Lambda$ a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.

All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.

Difficulty

The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: $\Lambda$ is an arbitrary function, and the hypothesis $mK \ll \Lambda \ll MK$ is only about finite families of points. One has to produce an operator on all of $F$. The obvious attempt, defining $L$ on the dense span of the functions $K(\cdot, y)$ by the kernel and extending by continuity, needs the bound $|(\,L f, g)| \le C\|f\|\|g\|$ on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of $\Lambda - mK$ and $MK - \Lambda$ does not by itself give the membership $\Lambda(\cdot, y) \in F$, which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of $F$, while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.

Formalization scope

• The space is Mathlib's RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function $K(\cdot, y)$ is the element RKHS.kerFun H y 1.
• The kernel of L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's $(f, g)$ is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point $E$ with $F = \mathbb{C}$, $K = 1$ and $L = cI$, the kernel is $\bar c$.
• Positive matrices and $\ll$ are Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.
• Symmetric is IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume $m \le M$ and neither does the statement: for $m > M$ both sides hold exactly when $F = \{0\}$ and $\Lambda = 0$.
• In (4) the statement asserts that the functions $x \mapsto \Lambda_1(x, z)$ and $x \mapsto \overline{\Lambda_2(y, x)}$ are elements of H, and that the kernel of L₁ ∘L L₂ is their scalar product.
• Weak convergence in Theorem II is ⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.
• In Theorem III the orthonormal systems are HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by $\mathbb{N}$ this contains the paper's $\lim_{p,q}$ over $\{1..p\}\times\{1..q\}$; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in $F \otimes \overline{F}$ correspond to operators of finite norm) needs the direct product $F \otimes \overline F$ and is not stated.
• A trivializing formalization is ruled out: Theorem I quantifies over every hermitian function $\Lambda$, not over functions already known to be kernels of operators, and the right-hand side is the finite-matrix condition, not a statement about an operator built from $\Lambda$.
• Not stated: the decomposition (8)–(9) into hermitian parts and the remark on general bounded operators (p. 374), and formula (5). Available substrate: RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function $\Lambda$ with $0 \ll \Lambda \ll K$ is the kernel of an operator $0 \le L \le I$, and the inclusion theorem $K_1 \ll K \Rightarrow F_1 \subset F$, both reusable beyond this mission.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part II, Mem. Amer. Philos. Soc. 1 (1939).
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316219232

Motivation

In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.

Section 6 of the same paper turns to weighted players: player $i$ has a weight $w_i \ge 1$ (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.

Setting

A finite directed multigraph $D$ has a finite set $E$ of arcs; each arc $e$ has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source $s$ and a sink $t$. A simple $s$–$t$ path is a sequence of arcs $e_1,\dots,e_m$ ($m\ge1$), each starting where the previous one ends, beginning at $s$, ending at $t$, and visiting no vertex twice; it is identified with its arc set $P\subseteq E$. Write $\mathcal S_{st}$ for the finite set of these paths.

The weighted single-commodity game has a finite set of players; player $i$ has a weight $w_i\ge1$, arc $e$ has a fixed cost $c_e\ge0$, and every player's strategy set is $\mathcal S_{st}$. In a profile $S=(S_i)_i$ let

$$W_e=\sum_{i\,:\,e\in S_i} w_i$$

be the total weight on arc $e$. Player $i$ pays

$$\mathrm{pay}_i(S)=\sum_{e\in S_i}\frac{w_i}{W_e}\,c_e .$$

A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.

A best-response move of player $i$ replaces $S_i$ by a path $T$ that minimises $i$'s payment given the other players' paths, provided this strictly lowers $i$'s payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.

Formalization targets

Goal: Theorem 6.3 (p. 1620)

For every such game with $w_i\ge1$ and $c_e\ge0$:

$$\text{there is no infinite sequence } S^0,S^1,\dots \text{ with } S^{n+1} \text{ a best-response move from } S^n;$$ $$\text{a profile admitting no best-response move is a Nash equilibrium;}$$ $$\mathcal S_{st}\neq\emptyset \;\Longrightarrow\; \text{a pure Nash equilibrium exists.}$$

The goal asserts only termination and existence; it fixes no bound on the length of a run.

Milestones (proof of Theorem 6.3, p. 1620)

For a profile $S$ define the marginal cost of a path, $c_S(P)=\sum_{e\in P}c_e/W_e\in[0,+\infty]$, and the tuple $P(S)$ of all values $c_S(P)$, $P\in\mathcal S_{st}$, sorted increasingly. With strictly positive arc costs:

1. a player on path $P$ pays $w_i\,c_S(P)$ (this one needs only $c_e\ge0$);
2. inequality (6.1): if player $i$ makes a best-response move from $P_1$ to $P_2$ and $\mathcal P$ is the set of paths sharing an arc with $P_1\cup P_2$, then $\min_{P\in\mathcal P}c_{S'}(P)<\min_{P\in\mathcal P}c_S(P)$;
3. every best-response move strictly decreases $P(S)$ in the lexicographic order.

Significance

The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.

The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.

Difficulty

The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential $\Phi$ is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.

The argument also depends on the shape of the strategy sets. Two distinct simple $s$–$t$ paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: $c_e/W_e$ is $0/0$ on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.

Formalization scope

• Players form a finite type; arcs form a finite type with tail and head maps into a vertex type. Parallel arcs are kept.
• A strategy is a Finset of arcs; the strategy family of every player is the finite set of arc sets of simple $s$–$t$ paths (a list of consecutive arcs with distinct visited vertices). There are no paths when $s=t$.
• Weights and costs are real numbers with $w_i\ge1$, $c_e\ge0$ (the predicate IsStandard); the milestones (6.1) and the lexicographic decrease assume $c_e>0$.
• Payments are real; on every used arc $W_e\ge w_i\ge1$, so the division is never by zero.
• The marginal cost $c_S(P)$ is valued in $[0,+\infty]$ (ℝ≥0∞): an unused arc of positive cost contributes $+\infty$. Computing it in the reals, where $x/0=0$, would make unused paths free and the milestones false.
• Termination is the well-foundedness of the relation "$S'$ is reached from $S$ by one best-response move" with $S'$ below $S$; the reverse orientation is a different statement.
• A best-response move requires a strict improvement and an exact minimiser; dropping either makes termination trivially true or false, and the second clause of the goal (no move possible implies Nash) guards against a move relation that is too narrow.

Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14:124–143, 1996. https://doi.org/10.1006/game.1996.0044
• H. Chen, T. Roughgarden, Network design with weighted players, Proceedings of the 18th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), 2006, pp. 28–37.