Operations Research

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

$$\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,$$

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$, and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$. An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$. The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$.

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$, $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$. A basis is an $m$-element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$.

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$: $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$,

$$\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},$$ $$\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.$$

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

1. Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$.
2. Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$.
3. The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$, $c^{T}\tilde x\ge c^{T}x_0$.
4. Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$, solve $A_Bx_B=b$, and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$, extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$-element basis, which requires the rank-$m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

• vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
• $Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
• a subset $B$ of indices is a Finset (Fin n); "$A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$, together with B.card = m;
• the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
• "optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
• "vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
• Theorem 4.4.1 carries the extra hypothesis $n\ge 1$: for $n=0$ there is no nonzero vector in $\mathbb{R}^0$, the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$, and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$-person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$; and every splitting set is a union of blocks of $\Pi_\Gamma$. The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$). Write $-S = I - S$. From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

$$\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .$$

For $J \subseteq I$ with complement $K = I - J$, the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$-constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

$$v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .$$

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$, for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

$$J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .$$

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ($\ominus$, $I$), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ($K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$); and the two extreme cases (43:J) ($\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ($\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$. The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$, since a pair $S \subseteq J' \cup J''$, $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$.

Formalization scope

• Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$, and $v$ is a function Finset ι → ℝ.
• Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$); every other statement holds without it. (43:E) assumes $J \neq \ominus$, since the book's constituent is a game and has at least one player.
• Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$, $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$-constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
• Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$.
• No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$, or complements taken in an ambient type larger than $I$, would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
• Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
• C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$, and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$, which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$, through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$. Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$, valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$, sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$, and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$, write $F_T c = \sum_{j \in T} c_j v_j$. A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$; with this convention $F_T c$ is just the product $Fc$. Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$.

Definition 1.1. For an integer $S$, the $S$-restricted isometry constant $\delta_S$ is the smallest quantity such that

$$(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2$$

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$. The $S, S'$-restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

$$|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|$$

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$. The paper writes $\theta_S$ for $\theta_{S,S}$. These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

$$(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.$$

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$, and $F$ a real $p \times m$ matrix with $FA = 0$. Let $S \ge 1$ satisfy

$$\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}$$

If $y = Af + e$ where $e$ is supported on a set of size at most $S$, then $f$ is the unique minimizer of $(P_1')$.

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$, and let $c$ be supported on a set $T$ with $|T| \le S$. Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$.

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$), and the two dual sparse reconstruction properties, Lemma 2.1 ($\ell^2$ version) and Lemma 2.2 ($\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$, checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$, and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$. Given such a $w$, the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ($T_0 \cup T_n$) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$, are what Lemma 2.1 gives for a set of size $S$; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$; the mission states the lemma with $\theta_{S,S'}$, which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$, and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$. The definitions are total in $S, S'$, and each theorem carries the paper's domain conditions ($S \ge 1$, and $2S \le m$, $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$, so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$" is a positive function of the real number $\delta_S$, quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$, and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$) belong to a separate mission.

Selected references

• E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
• E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
• E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
• D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
• S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

Motivation

Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an $\ell_0$ or $\ell_{1/2}$ penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.

For a smooth part $h$ whose gradient is $L$-Lipschitz, the classical analysis allows any constant step size $\beta \in (0, 1/L)$, and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when $h + P$ has the Kurdyka–Łojasiewicz property. When $h$ is nonconvex, however, $L$ is governed by the most negative curvature of $h$ as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of $h$ alone would require.

Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of $h$ imposes no restriction on the step size: it suffices to bound the curvature of $h$ after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. The problem is

$$\min_{x \in \mathbb{R}^n}\; h(x) + P(x),$$

under the paper's standing assumptions: $h : \mathbb{R}^n \to \mathbb{R}$ is twice continuously differentiable with a bounded Hessian $\nabla^2 h$; $P : \mathbb{R}^n \to (-\infty, +\infty]$ is proper (never $-\infty$, finite somewhere) and closed (lower semicontinuous); and for every $\tau > 0$ and $u$ the proximal problem $\min_y \tau P(y) + \frac12\|y - u\|^2$ has a minimizer. Neither $h$ nor $P$ is assumed convex.

A vector $v$ is a regular subgradient of $P$ at $x$ (with $P(x) < \infty$) if $P(z) \ge P(x) + \langle v, z - x\rangle - \varepsilon\|z - x\|$ for all $z$ near $x$, for every $\varepsilon > 0$. The limiting subdifferential $\partial P(x)$ collects the limits $v = \lim v^t$ of regular subgradients $v^t$ at points $x^t \to x$ with $P(x^t) \to P(x)$. A point $x$ is stationary if

$$0 \in \nabla h(x) + \partial P(x).$$

Given a step size $\beta > 0$ and an arbitrary starting point $x^0$, the proximal gradient method generates $(x^t)_{t \ge 0}$ by

$$x^{t+1} \in \operatorname*{Arg\,min}_x \Bigl\{ \langle \nabla h(x^t), x - x^t\rangle + \frac{1}{2\beta}\|x - x^t\|^2 + P(x) \Bigr\}. \tag{43}$$

Any minimizer may be selected. A cluster point of $(x^t)$ is the limit of a subsequence $x^{t_i}$.

The step-size condition involves a convex function $q$ and a constant $\ell > 0$ with

$$-\ell I \preceq \nabla^2 h(x) + \nabla^2 q(x) \preceq \ell I \quad \text{for all } x, \tag{44}$$

where $\preceq$ is the Loewner order on symmetric linear maps.

Formalization targets

Goal: Theorem 4

Suppose $q$ is twice continuously differentiable and convex, $\ell > 0$, (44) holds, and $(x^t)$ is generated by (43) with $\beta \in (0, 1/\ell)$. Then

$$h(x^{t+1}) + P(x^{t+1}) \le h(x^t) + P(x^t) \quad \text{for all } t,$$

and every cluster point $x^*$ of $(x^t)$, if one exists, satisfies $0 \in \nabla h(x^*) + \partial P(x^*)$.

The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.

Milestones

In the order of the paper's proof:

1. Eq. (3): robustness of $\partial$ under $x^t \to x$, $f(x^t) \to f(x)$, $v^t \to v$.
2. Eq. (45): under (44), $(h+q)(v) \le (h+q)(u) + \langle \nabla h(u) + \nabla q(u), v - u\rangle + \frac{\ell}{2}\|v - u\|^2$.
3. Eq. (46): $h(x^{t+1}) + P(x^{t+1}) \le h(x^t) + P(x^t) + \bigl(\frac{\ell}{2} - \frac{1}{2\beta}\bigr)\|x^{t+1} - x^t\|^2$.
4. The summed bound after (46): $\bigl(\frac{1}{2\beta} - \frac{\ell}{2}\bigr)\sum_{t=0}^{N-1}\|x^{t+1} - x^t\|^2 + h(x^N) + P(x^N) \le h(x^0) + P(x^0)$.
5. Vanishing steps: if a cluster point exists, $\|x^{t+1} - x^t\| \to 0$.
6. Function-value convergence: if $x^{t_i} \to x^*$, then $P(x^{t_i+1}) \to P(x^*)$.
7. Eq. (47): $0 \in \nabla h(x^t) + \frac{1}{\beta}(x^{t+1} - x^t) + \partial P(x^{t+1})$ for every $t$.

Significance

The result. For $h = h_1 - h_2$ a difference of convex $C^2$ functions with $\nabla h_1$ being $L_1$-Lipschitz, (44) holds with $q = h_2$ and $\ell = L_1$, so the step size may be taken in $(0, 1/L_1)$ whatever the curvature of $h_2$. For an indefinite quadratic $h(x) = \frac12\langle x, Qx\rangle$ the admissible range becomes $(0, 1/\lambda_{\max}(Q))$ instead of $(0, 1/\max_i|\lambda_i(Q)|)$, and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of $h + P$, so the sequence is bounded whenever $h + P$ is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.

Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.

Difficulty

The descent part rests on (45), a descent inequality for $h + q$ whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for $h$ alone and does not apply, since $\nabla h$ may have a much larger Lipschitz constant than $\ell$.

The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only $x^{t_i+1} \to x^*$ but also $P(x^{t_i+1}) \to P(x^*)$, because the limiting subdifferential is closed only under $P$-attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against $x^*$. The objective may be $+\infty$ at $x^0$, so summability of the steps has to be extracted without assuming a finite starting value.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). $h$ and $q$ are real-valued; $P$ takes values in EReal, and every objective value $h(x) + P(x)$ is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its $\varepsilon$-neighbourhood form, and the limiting subdifferential requires all three convergences $x^t \to x$, $P(x^t) \to P(x)$, $v^t \to v$. Stationarity is $\exists w \in \partial P(x),\ \nabla h(x) + w = 0$. The update (43) is a relation on sequences: $x^{t+1}$ minimizes the bracket over all of $\mathbb{R}^n$, with no uniqueness and a free starting point. A cluster point is the limit of $x^{\varphi(i)}$ for a strictly increasing $\varphi$.

Trivializing formalizations are ruled out: (44) is not replaced by "$\nabla h$ is $\ell$-Lipschitz", which is the classical special case $q = 0$; $P(x^0) < \infty$, boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without $P(x^t) \to P(x)$ is not used, since that would make stationarity a weaker statement.

Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.

Selected references

• G. Li and T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4), 2015. Preprint arXiv:1407.0753v6. https://arxiv.org/abs/1407.0753 · https://doi.org/10.1137/140998135
• H. Attouch, J. Bolte and B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems: proximal algorithms, forward–backward splitting, and regularized Gauss–Seidel methods, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9
• K. Bredies and D. A. Lorenz, Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009 (reference [9] of Li–Pong; no stable link recorded there).
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

The alternating direction method of multipliers (ADMM) splits a problem of the form $\min_x h(x) + P(\mathcal M x)$ into a sequence of simpler subproblems, one in which the nonsmooth term $P$ enters only through its proximal map and one in which only the smooth term $h$ appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as $\ell_0$- or $\ell_{1/2}$-regularized least squares, where $P$ is nonconvex and possibly discontinuous and convex theory does not apply.

Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on $h$, $P$ and $\mathcal M$ under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.

Setting

Let $n, m \ge 0$. The data are:

• $h : \mathbb{R}^n \to \mathbb{R}$, twice continuously differentiable with bounded Hessian $\nabla^2 h$;
• $P : \mathbb{R}^m \to (-\infty, +\infty]$, proper (never $-\infty$, finite somewhere) and closed (lower semicontinuous);
• $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ linear, with adjoint $\mathcal M^*$;
• a penalty $\beta > 0$ and a convex, twice continuously differentiable $\phi : \mathbb{R}^n \to \mathbb{R}$.

The augmented Lagrangian is

$$L_\beta(x, y, z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac{\beta}{2}\|\mathcal M x - y\|^2 ,$$

and the Bregman distance of $\phi$ is $D_\phi(x_1, x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$. A sequence $(x^t, y^t, z^t)_{t\ge 0}$ is generated by the proximal ADMM if, from arbitrary $x^0, z^0$,

$$y^{t+1} \in \operatorname*{Arg\,min}_y L_\beta(x^t, y, z^t), \quad x^{t+1} \in \operatorname*{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\}, \quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).$$

For a linear self-map $\mathcal T$, write $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$, and write $\succeq$, $\succ$ for the semidefinite and definite order of symmetric maps. Assumption 1 asks for $\sigma > 0$ with $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ (so $\mathcal M$ is surjective), bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$, maps $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$ with $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$, $\delta > 0$ with $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$, a bound $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2\phi]^2$, and $\gamma \in (0,1)$ with

$$\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\Bigl(\frac1\gamma\mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\Bigr).$$

Formalization targets

Goal: Theorem 2 (p. 11)

Suppose Assumption 1 holds and, with the same $\sigma$ and $\gamma$, there is $0 < \zeta < 2\beta\gamma$ with

$$h_0 := \inf_x\Bigl\{h(x) - \frac{1}{\sigma\zeta}\|\nabla h(x)\|^2\Bigr\} > -\infty. \tag{29}$$

Suppose that either (i) $\mathcal M$ is invertible and $\liminf_{\|y\|\to\infty} P(y) = \infty$, or (ii) $\liminf_{\|x\|\to\infty} h(x) = \infty$ and $\inf_y P(y) > -\infty$. Then

$$\sup_{t \ge 0}\ \bigl(\|x^t\| + \|y^t\| + \|z^t\|\bigr) < \infty .$$

Milestones

The milestones are the numbered displays of the paper's proof:

• Eq. (13): $\mathcal M^* z^{t+1} = \nabla h(x^{t+1}) + \nabla\phi(x^{t+1}) - \nabla\phi(x^t)$.
• Eq. (20): the one-step estimate $L_\beta(w^{t+1}) \le L_\beta(w^t) + \tfrac12\|x^{t+1}-x^t\|^2_{\frac{2}{\sigma\beta\gamma}\mathcal Q_3 - \delta\mathcal I - \mathcal T_2} + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ for $t \ge 1$.
• Eq. (30): the merit quantity $L_\beta(w^t) + \tfrac12\|x^t - x^{t-1}\|^2_{\frac{2}{\sigma\beta(1-\gamma)}\mathcal T_1^2}$ stays below its value at $t = 1$.
• Eq. (31): $\sigma\|z^t\|^2 \le \frac1\gamma\|\nabla h(x^t)\|^2 + \frac1{1-\gamma}\|x^t - x^{t-1}\|^2_{\mathcal T_1^2}$ for $t \ge 1$.
• Eq. (32): a lower estimate of that value at $t = 1$ by $\mu h(x^t) + (1-\mu)h_0 + \frac{c}{\sigma}\|\nabla h(x^t)\|^2 + P(y^t) + \frac\beta2\|\mathcal M x^t - y^t - z^t/\beta\|^2 + \ldots$, where $c = \frac{1-\mu}{\zeta} - \frac{1}{2\beta\gamma} > 0$.

Significance

The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with $\mathcal M = \mathcal I$, and a strongly convex quadratic $h$ with a regularizer that is bounded below and a general surjective $\mathcal M$ falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.

Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.

Difficulty

The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves $L_\beta$, which contains $-\langle z, \mathcal M x - y\rangle$ and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through $\nabla h(x^t)$ and the last primal step, and the part involving $\|\nabla h(x^t)\|^2$ is then paid for out of $h$ itself. Condition (29) exists to make exactly this trade possible, which is why it couples $\zeta$ to the $\gamma$ of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from $y^t$ through $z^t$ to $x^t$ using invertibility of $\mathcal M$, and (ii) goes from $x^t$ through $z^t$ to $y^t$. In case (i) the lower bound on $P$ that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.

Formalization scope

• Spaces and values. Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and $\mathcal M$ is a continuous linear map with Mathlib's adjoint. $P$, $L_\beta$ and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.
• Assumption 1 is one definition with its witnesses $\sigma, \delta, \gamma, \mathcal Q_1, \mathcal Q_2, \mathcal T_1, \mathcal T_2, \mathcal Q_3$ as explicit parameters, and $\succeq$ is Mathlib's Loewner order on self-maps. $\|x\|^2_{\mathcal T}$ is $\langle x, \mathcal T x\rangle$ for every $\mathcal T$, including indefinite ones.
• Condition (29) takes $\zeta$ and a real lower bound $h_0$ as parameters, with the same $\sigma$ and $\gamma$ as Assumption 1.
• The algorithm is a relation on sequences. An argmin is a global minimizer, not necessarily unique. $x^0$ and $z^0$ are free, and $y^0$ is unconstrained. No existence of minimizers is asserted.
• Coercivity is stated in its $\forall r\,\exists R$ form, and "invertible" is bijectivity of $\mathcal M$.
• Boundedness means one radius for all three blocks and all $t \ge 0$.

Ruling out trivial versions. A formalization that bounds only $x^t$, fixes $\gamma$ or $\zeta$ to an example's values, lets (29) use a fresh $\gamma$, adds a lower bound on $P$ in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.

Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound $\|\nabla\phi(a) - \nabla\phi(b)\|^2 \le \|a-b\|^2_{\mathcal T_1^2}$ from the Hessian sandwich, and strong convexity of the $x$-subproblem. Proofs of individual milestones are welcome independently.

Selected references

• G. Li and T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015; preprint arXiv:1407.0753v6. https://arxiv.org/abs/1407.0753 (DOI 10.1137/140998135)
• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Found. Trends Mach. Learn. 3(1), 2011. https://doi.org/10.1561/2200000016
• H. Attouch, J. Bolte and B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137, 2013. https://doi.org/10.1007/s10107-011-0484-9

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$. Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$, which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$, a finite nonempty action set $A$, transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ is, for each state $s$, a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$.

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$. The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$. The discounted future state distribution from $\mu$ is

$$d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu),\qquad s_0\sim\mu,$$

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$.

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$: the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$. For nonnegative $f,g$ on $S$, $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

$$\eta_{\tilde\mu}(\pi^*)-\eta_{\tilde\mu}(\pi)\le\frac{\varepsilon}{1-\gamma}\left\|\frac{d_{\pi^*,\tilde\mu}}{d_{\pi,\mu}}\right\|_\infty\le\frac{\varepsilon}{(1-\gamma)^2}\left\|\frac{d_{\pi^*,\tilde\mu}}{\mu}\right\|_\infty.$$

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$; taking $\tilde\mu=D$, the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$, $\pi$ and any starting distribution $\mu$,

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi)=\frac{1}{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}\big[A_\pi(s,a)\big].$$

The states are weighted by the future state distribution of the new policy $\tilde\pi$, the advantage is that of the old policy $\pi$.

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$, which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$) and P s a s' (the paper's $P(s';s,a)$), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: "$X\le K\|f/g\|_\infty$" is "$X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$; no full-support assumption is made on $\mu$ or $\tilde\mu$. The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$, which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$, and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
• J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477