Optimization

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

$$\phi_v(t)=|t-1|,\qquad \phi_h(t)=(\sqrt t-1)^2,\qquad \phi_{\mathrm{kl}}(t)=t\log t-t+1,\qquad \phi_j(t)=(t-1)\log t.$$

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

$$\mathcal P^\phi(P_0;\varepsilon) =\{P\in\mathfrak M(\Xi,\mathcal F):\mathfrak D^\phi(P,P_0)\le\varepsilon\}.$$

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

$$\frac14\bigl(\mathfrak D^{\phi_v}(P,P_0)\bigr)^2 \le\mathfrak D^{\phi_h}(P,P_0) \le\mathfrak D^{\phi_{\mathrm{kl}}}(P,P_0) \le\mathfrak D^{\phi_j}(P,P_0).$$

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

$$\mathcal P^{\phi_j}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_{\mathrm{kl}}}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_h}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_v}(P_0;2\sqrt\varepsilon).$$

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

Why accelerate value computation

Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a $\lambda$-contraction, so they converge at the geometric rate $\lambda$, the discount factor. When $\lambda$ is close to $1$, which is the regime of long effective horizons in reinforcement learning ($\lambda = 0.99$ or $0.999$) and in healthcare and operations applications, the number of iterations grows like $1/(1-\lambda)$.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that $v \mapsto v - T(v)$ behaves like the gradient of a function with smoothness constant $1+\lambda$ and strong-convexity constant $1-\lambda$. This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator $T_\pi$ of a fixed policy, they prove that both schemes converge at a rate governed by $\sqrt{\kappa}$ rather than $\kappa$, with $\kappa = (1+\lambda)/(1-\lambda)$, provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.

Setting

A finite MDP has a state set $S$ with $|S| = n$, a finite action set $A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia}$ is a probability vector), rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi = (\pi_{ia})$ is a matrix with nonnegative rows summing to $1$; it induces

$$r_{\pi,i} = \sum_a \pi_{ia} r_{ia}, \qquad L_{\pi,ij} = \sum_a \pi_{ia} P_{iaj}, \qquad T_\pi(v) = r_\pi + \lambda L_\pi v .$$

The value function of $\pi$ is $v^\pi = \sum_{t \ge 0} \lambda^t L_\pi^t r_\pi$, the expected discounted reward from each starting state; it is the unique fixed point of $T_\pi$.

Reversibility (Definition 2.1): the chain with transition matrix $L$ is irreducible, and it has a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i,j$.

Momentum Value Computation (M-VC) starts from arbitrary $v_0, v_1 \in \mathbb{R}^n$ and iterates

$$v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,$$

with the constant step sizes (4.2)

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

The analysis runs through the $2n \times 2n$ matrix

$$B_\pi = \begin{pmatrix} \lambda(\beta+1)L_\pi & -\beta I \\ I & 0 \end{pmatrix},$$

which propagates the error of the pair $x_s = (v_s, v_{s-1})$, and its spectral radius $\rho(B_\pi)$, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.5

For a valid MDP and a policy $\pi$ whose chain $L_\pi$ is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to $v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\!\left(\left(\frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} + \eta\right)^{s}\right), \qquad 0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda .$$

The goal states the paper's three clauses as printed: convergence, the little-o rate for every $\eta > 0$, and the comparison with $\lambda$.

Milestones

1. The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
2. Lemma B.1: $x_s = x^\pi + B_\pi^{s-1}(x_1 - x^\pi)$ for all $s \ge 1$, with $x^\pi = (v^\pi, v^\pi)$.
3. The eigenvalues of an irreducible, reversible transition matrix are real (§2).
4. (B.1): every eigenvalue $\omega$ of $B_\pi$ satisfies $\omega^2 - \frac{2\lambda\mu}{1+\sqrt{1-\lambda^2}}\omega + \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} = 0$ for an eigenvalue $\mu$ of $L_\pi$.
5. For $\mu \in [-1,1]$, the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$.
6. The identity $\frac{\lambda}{1+\sqrt{1-\lambda^2}} = \frac{\sqrt{1+\lambda}-\sqrt{1-\lambda}}{\sqrt{1+\lambda}+\sqrt{1-\lambda}} = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
7. Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
8. $0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda$ for $\lambda \in (0,1)$.

Significance

The rate $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$ is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number $\kappa$. Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over $\lambda$, so that an $\epsilon$-approximation of $v^\pi$ needs a number of iterations scaling like $1/\sqrt{1-\lambda}$ rather than $1/(1-\lambda)$. The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in $[-1,1]$.

The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of $B_\pi$, and the passage from spectral radius to a little-o rate.

Difficulty

The obvious argument bounds $\|B_\pi\|$ in some norm and iterates. No such bound by the rate holds in general: $B_\pi$ is not normal, and for eigenvalues $\mu = \pm 1$ of $L_\pi$ the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between $\rho(B_\pi)$ and $\|B_\pi^s\|^{1/s}$ is exactly what the $+\eta$ absorbs. Computing $\rho(B_\pi)$ needs two separate facts: the eigenvalues of $B_\pi$ are tied to those of $L_\pi$ through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of $L_\pi$ are real and lie in $[-1,1]$, which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real $\mu$ the modulus computation fails, which is why the hypothesis cannot be dropped.

Formalization scope

States and actions are finite types. The MDP data $(P, r, \lambda)$ is a plain structure, with validity (stochastic $P_{ia}$, $0 < \lambda < 1$) a separate hypothesis; the paper's initial distribution $p_0$ plays no role and is omitted. The value function is the Neumann series $\sum_t \lambda^t L_\pi^t r_\pi$. The norm on $\mathbb{R}^n$ is the sup norm, and $o(\cdot)$ is with respect to it as $s \to \infty$. Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of $B_\pi$ are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by $\nu = 0$ and is not used.

Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with $x_0 - x^\pi$, but $x_0 = (v_0, v_{-1})$ is undefined; the statement uses $x_1 = (v_1, v_0)$. Lemma B.2 prints $\rho(B_\pi) = (1-\sqrt\kappa)/(1+\sqrt\kappa)$, a negative number; its proof computes $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$, the rate of Theorem 5.5, which is stated. On p. 22 the constant $\lambda/(1+\sqrt{1-\lambda^2})$ is printed as $\lambda/(1+\sqrt{1-\lambda})^2$. The second step size, printed $\gamma$ in (4.2), is the $\beta$ of (M-VC) and App. B.

A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which $\lambda$ is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.

A complete development needs the determinant of a $2\times 2$ block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• E. Ghadimi, H. R. Feyzmahdavian, M. Johansson, Global convergence of the Heavy-ball method for convex optimization, European Control Conference, 2015. https://arxiv.org/abs/1412.7457
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 2nd ed. 2020 (cited in the paper as 2013), Chapter 6. https://doi.org/10.1007/978-3-030-45982-6
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014. https://doi.org/10.1002/9780470316887

Motivation

Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate $\lambda$, the discount factor. When $\lambda$ is close to one, as in long-horizon reinforcement-learning benchmarks ($\lambda = 0.99$ or $0.999$), the number of iterations grows like $1/(1-\lambda)$, and each iteration costs a full sweep over states and actions.

In convex optimization, gradient descent on a $\mu$-strongly convex, $L$-smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number $\kappa = L/\mu$ from $\kappa$ to $\sqrt\kappa$. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read $v - T(v)$ as a gradient with "strong convexity" $1-\lambda$ and "smoothness" $1+\lambda$, transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order $1-\sqrt{1-\lambda}$ instead of $\lambda$.

Setting

An MDP has a finite set of states $\mathbb S$ with $|\mathbb S| = n$, a finite set of actions $\mathbb A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia\cdot}$ is a probability distribution), real rewards $r_{ia}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi$ assigns to every state $i$ a probability distribution $\pi_{i\cdot}$ over actions. It induces the reward vector $r_{\pi,i} = \sum_a \pi_{ia} r_{ia}$, the transition matrix $L_{\pi,ij} = \sum_a \pi_{ia}P_{iaj}$, the policy operator $T_\pi(v) = r_\pi + \lambda L_\pi v$, and the value function

$$v^\pi = \sum_{t\ge0}\lambda^t L_\pi^t r_\pi,$$

the expected discounted reward when actions are drawn from $\pi$. VC iterates $v_{s+1} = T_\pi(v_s)$.

Accelerated Value Computation (A-VC) starts from arbitrary $v_0, v_1 \in \mathbb R^n$ and sets, for $s \ge 1$,

$$h_s = v_s + \gamma\,(v_s - v_{s-1}),\qquad v_{s+1} = h_s - \alpha\,\big(h_s - T_\pi(h_s)\big),$$

with the constant step sizes $\alpha = 1/(1+\lambda)$ and $\gamma = (1-\sqrt{1-\lambda^2})/\lambda$. Write $\kappa = (1+\lambda)/(1-\lambda)$.

A transition matrix $L$ is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution $\nu$ satisfying detailed balance, $\nu_iL_{ij} = \nu_jL_{ji}$ for all $i, j$.

The analysis runs through the $2n\times2n$ matrix

$$B_\pi = \begin{bmatrix}(1-\sqrt{1/\kappa})(I+L_\pi) & -\tfrac12(1-\sqrt{1/\kappa})^2(I+L_\pi)\\ I & 0\end{bmatrix},$$

whose powers propagate the stacked error $x_s - x^\pi$, where $x_s = (v_s, v_{s-1})$ and $x^\pi = (v^\pi, v^\pi)$. Its spectral radius $\rho(B_\pi)$ is the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.1

If $L_\pi$ is irreducible and reversible, then $v_s \to v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\Big(\big(1-\sqrt{1/\kappa}+\eta\big)^s\Big),\qquad 0 < 1-\sqrt{1/\kappa} < \lambda.$$

The goal is stated with the $\eta$ slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order $s\,(1-\sqrt{1/\kappa})^s$ in general, so a clean $O\big((1-\sqrt{1/\kappa})^s\big)$ bound is false.

Milestones

1. The step-size identities of the proof of Lemma 5.2: $1+1/\kappa-2\alpha=0$, $(1-\alpha)(1+\gamma)=\alpha\lambda(1+\gamma)=1-\sqrt{1/\kappa}$, $\alpha\gamma\lambda=(1-\alpha)\gamma=\alpha-\sqrt{1/\kappa}=\tfrac12(1-\sqrt{1/\kappa})^2$.
2. Lemma 5.2: $x_s = x^\pi + B_\pi^{s-1}(x_1-x^\pi)$ for all $s\ge1$.
3. The eigenvalues of a reversible transition matrix are real (§2, p. 4).
4. $\operatorname{Sp}(L_\pi)\subset[-1,1]$ for a reversible policy chain.
5. (5.3): each eigenvalue $\omega$ of $B_\pi$ solves $\omega^2-(\mu+1)(1-\sqrt{1/\kappa})\omega+\tfrac12(\mu+1)(1-\sqrt{1/\kappa})^2=0$ for some $\mu\in\operatorname{Sp}(L_\pi)$.
6. For $\mu\in[-1,1]$: $\tfrac12|\mu+1\pm\sqrt{\mu^2-1}|\le1$.
7. Lemma 5.3: $\rho(B_\pi) = 1-\sqrt{1/\kappa}$.
8. (5.6): $\lambda = 1-\sqrt{1/\kappa}+\sqrt{1-\lambda}\,(1-\sqrt{1-\lambda^2})/\sqrt{1+\lambda}$, with a positive last term.

Significance

The result. Since $1-\sqrt{1/\kappa} = 1-\sqrt{(1-\lambda)/(1+\lambda)}$, A-VC reaches an $\epsilon$-approximation of $v^\pi$ in $O\big((1-\lambda)^{-1/2}\log(1/(\epsilon(1-\lambda)))\big)$ iterations against $O\big((1-\lambda)^{-1}\log(1/(\epsilon(1-\lambda)))\big)$ for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound $\lambda^s/(1+\lambda)$ for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.

Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts $\eta$ under the square root, $o\big((1-\sqrt{1/\kappa+\eta})^s\big)$. That rate is faster than $\rho(B_\pi)$ and is false (a one-state chain is a counterexample). The mission poses the rate $(1-\sqrt{1/\kappa}+\eta)^s$ that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).

Difficulty

The obvious argument says "$\rho(B_\pi)<1$, so $B_\pi^s\to0$ at rate $\rho(B_\pi)$". That argument breaks twice. First, computing $\rho(B_\pi)$ requires knowing where the eigenvalues of $L_\pi$ lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed $1-\sqrt{1/\kappa}$ in modulus. Reversibility is what confines them to $[-1,1]$, and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue $1-\sqrt{1/\kappa}$ of $B_\pi$ (coming from $\mu=1$) is a double root of (5.3) with a single eigenvector, so $\|B_\pi^s\|$ is not $O(\rho^s)$; only the $\eta$-relaxed little-o holds. The eigenvalues of $B_\pi$ are non-real for $\mu\in(-1,1)$, so the whole computation must be done over $\mathbb C$.

Formalization scope

• Data. $\mathbb S$ and $\mathbb A$ are finite types. The MDP is the data $(P, r, \lambda)$. Validity (stochastic $P_{ia\cdot}$, $\lambda\in(0,1)$) and the policy property are hypotheses. Rewards are arbitrary reals. The initial-state distribution $p_0$ of the paper's tuple is omitted, since nothing here uses it.
• Reused definitions. $r_\pi$, $L_\pi$, $v^\pi$, policies and the kernel condition are the published FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. $v^\pi$ is the discounted reward series, not an arbitrary fixed point of $T_\pi$.
• Reversibility is irreducibility plus a stationary probability vector in detailed balance. Detailed balance alone would be satisfied by $\nu=0$ and is not used.
• Norms and rates. Vectors are functions $\mathbb S\to\mathbb R$ with the sup norm $\|\cdot\|_\infty$; "$o(\cdot)$" is Mathlib's little-o along $s\to\infty$.
• Spectra are complex: $\rho(B_\pi)$ is the spectral radius of the complexified matrix, valued in $[0,\infty]$. Using the real spectrum would make Lemma 5.3 a different, weaker statement.
• Indexing. A-VC is a sequence on $\mathbb N$ with $v_0, v_1$ given; $x_s = (v_s, v_{s-1})$ is used only for $s\ge1$.
• Pinned relative to the page. In the goal, $\eta$ is outside the square root, as in the proof. In milestone 6, $\sqrt{\mu^2-1}$ is written as $i\sqrt{1-\mu^2}$, its value for $\mu\in[-1,1]$.

Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with $P_{iaj}=1/2$ is valid, reversible and has a policy), the rate is stated with $\forall\eta>0$ rather than for some $\eta$, and $v^\pi$ is a fixed object rather than a variable constrained by hypotheses.

Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of $2\times2$ block matrices with commuting blocks; and the bound $\|M^s\| = o((\rho(M)+\eta)^s)$ from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• V. Goyal, J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004 (reprint 2013). https://doi.org/10.1007/978-1-4419-8853-9
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 1999 (reprint 2013), Ch. 6. https://doi.org/10.1007/978-1-4757-3124-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (reprint 2014). https://doi.org/10.1002/9780470316887

Motivation

Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.

The potential carries a parameter $\rho > n$. The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give $O(\sqrt n\,t)$ iterations with $\rho = n + \Theta(\sqrt n)$. Practical codes, however, performed better with much larger $\rho$ (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With $\rho = n + \Theta(n^2)$ and the step chosen to minimise the potential inside the wide neighbourhood $\mathcal N_\infty^-(\beta)$, the method needs $O(nt)$ iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).

Timeline:

• 1990: Todd and Ye introduce the primal–dual potential function.
• 1989–1991: Kojima–Mizuno–Yoshise, Ye, Freund and others prove $O(\sqrt n\,t)$ bounds for $\rho = n + \Theta(\sqrt n)$.
• 1990–1991: Mizuno, Todd and Ye prove the $O(nt)$ bound for $\rho = n + \Theta(n^2)$ (Theorem 3 of the report formalized here).

Setting

Fix $m \ge 0$, $n \ge 1$, $A \in \mathbb R^{m\times n}$, $b \in \mathbb R^m$, $c \in \mathbb R^n$. The primal problem is $\min c^Tx$ subject to $Ax = b$, $x \ge 0$. The dual is $\max b^Ty$ subject to $A^Ty + s = c$, $s \ge 0$. The strictly feasible set $\mathcal F^0$ is the set of pairs $(x, s)$ with $x > 0$, $s > 0$, $Ax = b$ and $A^Ty + s = c$ for some $y$. The duality measure is $\mu = x^Ts/n$.

For $z \in \mathbb R^n$ put $(z^-)_j = \min\{z_j, 0\}$ and $\|z\|_\infty^- = \|z^-\|_\infty$. For $\beta \in (0,1)$, the wide neighbourhood is

$$\mathcal N_\infty^-(\beta) = \{(x,s) \in \mathcal F^0 : \|Xs - \mu e\|_\infty^- \le \beta\mu\},$$

i.e. $x_js_j \ge (1-\beta)\mu$ for all $j$, where $X = \mathrm{diag}(x)$ and $e$ is the all-ones vector.

The potential is

$$\psi(x,s) = \rho\log(x^Ts) - \sum_{j=1}^n \log(x_js_j), \qquad \rho > n,$$

with the natural logarithm. At $(x,s)$ and for $\gamma \in (0,1)$, a search direction $d = (d_x, d_y, d_s)$ solves

$$S d_x + X d_s = \gamma\mu e - Xs,\qquad A d_x = 0,\qquad A^Td_y + d_s = 0,$$

and the iterates move along $x(\theta) = x + \theta d_x$, $s(\theta) = s + \theta d_s$. The scaled vectors are $p_j = \sqrt{s_j/x_j}\,(d_x)_j$ and $q_j = \sqrt{x_j/s_j}\,(d_s)_j$, $Pq = (p_jq_j)_j$, and $\theta_2^- = \min\{1, \beta\gamma\mu/\|Pq\|_\infty^-\}$.

Algorithm 3. Start from $(x^0,s^0) \in \mathcal N_\infty^-(\beta)$ with $(x^0)^Ts^0 \le 2^t$ and $\psi(x^0,s^0) \le (\rho-n)t + n\log n$. While $(x^k)^Ts^k > 2^{-t}$, compute $d$ at $(x^k, s^k)$, choose $\bar\theta$ with $(x(\bar\theta), s(\bar\theta)) \in \mathcal N_\infty^-(\beta)$ and $\psi(x(\bar\theta), s(\bar\theta)) \le \psi(x(\theta), s(\theta))$ for every $\theta$ with $(x(\theta), s(\theta)) \in \mathcal N_\infty^-(\beta)$, and move to $(x(\bar\theta), s(\bar\theta))$.

Formalization targets

Goal: Theorem 3 (p. 11)

Let $\beta,\gamma \in (0,1)$ with $\gamma \le 2(1-\beta)$ and

$$\rho = n + \Bigl(\frac{3}{\beta\gamma(1-\gamma)}\log\frac{1}{1-\beta}\Bigr)n^2.$$

For every $t > 0$ and every run of Algorithm 3,

$$\exists\, k \le \Bigl\lceil \frac{6nt}{11\beta\gamma(1-\gamma)} \Bigr\rceil:\quad (x^k)^Ts^k \le 2^{-t}.$$

The paper states "$O(nt)$ iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.

Milestones

1. §5, p. 11. $\psi(x,s) = (\rho-n)\log(x^Ts) - \sum_j\log\frac{x_js_j}{x^Ts/n} + n\log n \ge (\rho-n)\log(x^Ts) + n\log n$. Hence reducing $\psi$ to $-(\rho-n)t + n\log n$ gives $x^Ts \le 2^{-t}$.
2. (16), p. 12. One step of Algorithm 3 satisfies $\psi(x(\bar\theta),s(\bar\theta)) - \psi(x,s) \le -\bigl(\frac{3n^2\theta_2^-}{\beta\gamma} - n\bigr)\log\frac{1}{1-\beta}$.
3. Proof of Theorem 3, p. 12. For $n \ge 1$, every step decreases $\psi$ by at least $11n\log\frac{1}{1-\beta}$.

Significance

The result shows that a potential-reduction method with $\rho - n$ of order $n^2$ keeps a polynomial worst-case bound. The earlier analyses cited by the report used $\rho - n$ of order $\sqrt n$. It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term $Pq$ decrease the potential far more.

The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step $\theta_2^-$ in $\mathcal N_\infty^-(\beta)$, the potential decrease (16), and the complexity bound.

Difficulty

The step $\bar\theta$ is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term $Pq$ of the Newton direction in the one-sided norm $\|\cdot\|_\infty^-$, together with the centrality of the current iterate. A fixed decrease of order $n$ arises only because $\rho - n$ is of order $n^2$. Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.

A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real $\theta$ whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.

Formalization scope

Vectors are Fin n → ℝ, with index $j = 1,\dots,n$ mapped to Fin n; $\|\cdot\|_\infty$ is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. $\psi$ is the published definition LinearOptimization.interiorPointPotential with $q := \rho$. It equals (1) at every strictly positive pair, and it is evaluated only at points of $\mathcal N_\infty^-(\beta)$. All logarithms are natural, and $2^{\pm t}$ are real powers with real $t > 0$. A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds $2^{-t}$, the step relation of Algorithm 3. Iterates after termination are unconstrained.

Conventions and repairs:

• $\theta_2^- := 1$ when $\|Pq\|_\infty^- = 0$, reading $\beta\gamma\mu/0$ as $+\infty$.
• The per-iteration milestone keeps the page's $n \ge 1$. The paper's step $\theta_2^- \ge 4\beta\gamma/n$ needs $4\beta\gamma \le n$, which can fail for $n = 1$; but for $n = 1$ the potential is unbounded below along the line inside the neighbourhood, so no step exists and the statement holds vacuously there. The goal keeps $n \ge 1$ as well.
• The minimisation in Algorithm 3 ranges over all real $\theta$, as printed. It does not range over a segment, and the step is not the largest admissible step of Algorithm 2.
• Both start conditions are kept: $(x^0)^Ts^0 \le 2^t$ from Algorithm 2 and the potential bound of §5.

A formalization in which no run can exist for any instance, or in which $\rho$ or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for $n \ge 2$ whenever the potential attains its minimum along the line, and the count is the explicit expression above.

Needed infrastructure: the algebra of system (2), namely $d_x^Td_s = 0$, the identity $\mu(\theta) = (1-(1-\gamma)\theta)\mu$, and $X(\theta)s(\theta) - \mu(\theta)e = (1-\theta)(Xs - \mu e) + \theta^2 Pq$. Also needed are the bounds $\|Pq\|_\infty \le \|r\|^2/4$ and $\|r\|^2 \le n\mu$ on $\mathcal N_\infty^-(\beta)$ when $\gamma \le 2(1-\beta)$, and the arithmetic–geometric mean inequality for $\psi$. These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.

Selected references

• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944, 1990, rev. 1991; Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• M. J. Todd, Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15(3):508–529, 1990. https://doi.org/10.1287/moor.15.3.508