All missions

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$. It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$. The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$, the real random variables with $\mathbb E|X|^p<\infty$. An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$.

• The cdf of $X$ is $F_X(t)=P(X\le t)$. $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$.
• $\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$.
• $\rho$ is risk averse (Definition 5.1) if for every $\sigma$-algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$,

$$\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),$$

for every version of the conditional expectation.

• For random variables $X_1,X_2$, the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
• $\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$.

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$.

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$.

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$,

$$\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.$$

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

1. The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$.
2. The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$, and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
3. Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
4. Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$.
5. Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$, there are $\widehat X_1\overset{D}{\sim}X_1$, $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$, cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$, together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$, with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$, so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$, related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$, not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$. That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

• $\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
• The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
• "For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$, as in the published increasing convex order.
• Risk aversion quantifies over every sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$-measurable version of Mathlib's conditional expectation P[X|m].
• The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
• The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ($t\notin(0,1)$); milestone 2 is therefore stated almost surely.
• The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$, dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$-algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
• V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
• D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.

Setting

A finite game has a finite set of players $\mathcal M$; each player $m$ has a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements, and a utility $u^m : E \to \mathbb R$ on the set of strategy profiles $E = \prod_m E^m$. For a profile $p$, $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$.

A profile $p$ is an $\epsilon$-equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m}) - \epsilon$ for every player $m$ and strategy $q^m$ (equation (2) of the paper). A game is a potential game if there is $\varphi : E \to \mathbb R$ with $\varphi(p^m, p^{-m}) - \varphi(q^m, p^{-m}) = u^m(p^m, p^{-m}) - u^m(q^m, p^{-m})$ for all $m$, $p^m$, $q^m$, $p^{-m}$ (Definition 2.1).

A game is identified with its tuple of utilities, an element of $C_0^M$ where $C_0 = \{f : E \to \mathbb R\}$. The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator $D_m$ sends $u^m$ to its differences along the edges where player $m$ deviates, $D = \sum_m D_m$, $\delta_0$ is the gradient of the game graph, $\Pi_m = D_m^\dagger D_m$, and $\dagger$ is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces

$$\mathcal P = \{u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\qquad \mathcal H = \{u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D ,$$

and a harmonic game is a game in $\mathcal H \oplus \mathcal N$.

Section 6 introduces the weighted inner product and norm

$$\langle G, \hat G\rangle_{M,E} = \sum_{m} h_m \sum_{p \in E} u^m(p)\,\hat u^m(p), \qquad \|G\|_{M,E}^2 = \langle G, G\rangle_{M,E} .$$

A closest potential game to $G$ is a potential game $\hat G$ with $\|G - \hat G\|_{M,E} \le \|G - G'\|_{M,E}$ for every potential game $G'$; a closest harmonic game is defined in the same way.

Formalization targets

Goal: Theorem 6.3

Let $\hat G$ be the closest potential game to $G$ and $\alpha = \|G - \hat G\|_{M,E}$. Then for every $\epsilon_1$, every $\epsilon_1$-equilibrium of $\hat G$ is an $\epsilon$-equilibrium of $G$, and every $\epsilon_1$-equilibrium of $G$ is an $\epsilon$-equilibrium of $\hat G$, where

$$\epsilon = \max_{m \in \mathcal M} \frac{2\alpha}{\sqrt{h_m}} + \epsilon_1 .$$

Milestones

1. Lemma 2.1. If $|u^m(p) - \hat u^m(p)| \le \epsilon_0$ for all $m$ and $p$, every $\epsilon_1$-equilibrium of one game is a $(2\epsilon_0 + \epsilon_1)$-equilibrium of the other.
2. Theorem 5.1. The set of potential games is the subspace $\mathcal P \oplus \mathcal N$.
3. Theorem 6.1. Under $\langle\cdot,\cdot\rangle_{M,E}$ the subspaces $\mathcal P$, $\mathcal H$, $\mathcal N$ are pairwise orthogonal.
4. Theorem 6.2. With $\varphi = \delta_0^\dagger D u$, the closest potential game to $G$ has utilities $\Pi_m \varphi + (I - \Pi_m)u^m$, and the closest harmonic game has utilities $u^m - \Pi_m\varphi$.

Significance

The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.

Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections $\Pi_m$), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for $\epsilon$-equilibria.

Difficulty

Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into $\mathcal P$, $\mathcal H$, $\mathcal N$) and properties of pseudoinverses of the operators $D_m$ and $\delta_0$ that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality $\mathcal P \perp \mathcal H$ under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the $h_m$ differ, so the standard orthogonal-complement machinery cannot be applied to $C_0^M$ with its default inner product.

Formalization scope

Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product $\tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$ of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.

Hypotheses made explicit: every strategy set is nonempty (the paper's $E^m = \{1,\dots,h_m\}$), so $h_m \ge 1$; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an $\epsilon$-equilibrium for some $\epsilon \le B$" is stated as "a $B$-equilibrium", which is equivalent because (2) is monotone in $\epsilon$. Both directions of Lemma 2.1 and Theorem 6.3 are included.

The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance $\alpha$ would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.

Contributions welcome: the Penrose identities for the pseudoinverse, the identities $D^\dagger D = \Pi$ and $\Delta_{0,m} = h_m \Pi_m$, and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Math. Oper. Res. 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games Econ. Behav. 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044

Motivation

This mission asks for a formal proof that the matrix multiplication exponent is at most $2.25=9/4$ over every field. It is proposed for the Matrix multiplication exponent campaign, using the campaign's existing tensor-rank definition. The target is deliberately non-strict: equality with $9/4$ is allowed.

The starting point is OpenAI's October 2026 matrix-multiplication material, whose original arithmetic-exponent theorem is stated over the complex numbers. An all-fields adaptation has been checked separately in Lean. This mission asks for the corresponding result in the campaign's precise mathematical model; that connection still requires proof.

Setting

Let $K$ be any field, finite or infinite and in any characteristic. For a positive integer $n$, the square matrix multiplication tensor is the sum of $e_{ij}\otimes e_{jk}\otimes e_{ki}$ over all indices $i,j,k<n$. Each factor is the vector space of functions from pairs of indices to $K$. Its tensor rank is the least number of pure tensors in an exact decomposition over $K$.

The imported definition MME.matMulExp takes the infimum of the ratios $\log R_K(MM_n)/\log n$ for integer $n\ge2$, together with the value $3$ at sizes zero and one. The goal refers to this existing definition without modifying it. An upper bound on the infimum need not be attained at any one matrix size.

Target

For every field $K$, prove

$$\operatorname{MME.matMulExp}(K)\le 2.25=\frac94.$$

The Lean theorem is mme_omega_le_225, with the sole typeclass hypothesis [Field K]. The decimal is interpreted exactly as a real rational, not as a floating-point approximation. There is no restriction to characteristic zero, infinite fields, algebraically closed fields, or the complex numbers.

The campaign template currently uses a strict inequality. This proposal intentionally requests the non-strict bound $\le2.25$ and should be reviewed on that basis. It does not assert $\omega<2.25$. The proposed numeric campaign value is $2.25$.

Significance

A proof of this goal would place the nine-fourths bound in the same formal tensor-rank model used by other entries in this campaign. Reusing the foundation makes its assumptions and numeric value directly inspectable. Establishing the comparison between the arithmetic and tensor formulations would also produce reusable results for future matrix multiplication missions.

The all-fields quantifier matters: constructions that use interpolation or roots of unity must justify their applicability and any descent back to the original field. A result over the complex numbers alone does not establish this goal.

Difficulty

The available checked adaptation proves the nine-fourths bound for the OAI arithmetic exponent and its exact-rank exponent. A remaining task is to connect that exact-rank representation to the campaign's tensor product and rank definition. This requires checking the coordinate conventions, converting rank decompositions, and transporting the bound through the infimum and logarithms.

The proof must also compile in the campaign's pinned Lean environment. Success in a different Lean or Mathlib version is useful evidence for the source proof, but it does not verify this mission's theorem.

Formalization scope

This draft imports the campaign's published mme_omega definition and contains one open goal. It preserves the campaign environment, Mathlib 777aaa6 with Lean 4.29.0-rc3. The separate all-fields OAI adaptation was checked using Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; its proof is not yet an accepted Prove2me solution to this goal.

In particular, the bridge to MME.matMulExp and the environment port remain unproved here. The mission should remain open until Prove2me accepts a proof of this exact statement. An independent auditor read the Lean goal and imported definition without seeing the intended wording; that read-back is included verbatim in the goal's natural-language statement for review.

Selected references

• OpenAI matrix multiplication preprint, October 2, 2026.
• OpenAI ComparatorChallenges Lean source.
• Matrix multiplication exponent campaign.

The all-fields adaptation and the proposed connection to the campaign definition are additional formalization work; they are not attributed to the original complex-field statement.

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$-vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic $O(n^{2.99942})$ algorithm, the campaign's first entry. Later entries tightened the accounting to $2.9983$ and $2.99791$.

This entry records the deterministic exponent $2.996001$. It roughly doubles the saving below $3$ compared with $2.99791$, and it matches what was previously only known with randomized hashing.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$, indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$. Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$, and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.

Formalization target

The goal is the campaign template with the value $2.996001$:

$$\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 2.996001,$$

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.996001})$ steps.

How the bound arises

The algebraic core is the thin-product data structure of Alman and Vassilevska Williams: for an $N\times D$ by $D\times N$ integer product it answers requested entries $W$ in $\tilde O(N^2D^{-\Gamma} + N D^{a} + |W| D^{q})$. Two local refinements of that construction sharpen the exponents:

1. Pruned encodings. Encoding branches with more than $m$ copies of the distinguished symbol $P_0$ are never materialized, giving $a(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$.
2. Exact binomial tail. The box preprocessing is bounded by its actual binomial sum, giving $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$, with $q(\theta) = \bigl(H(\theta)+\theta\ln 9\bigr)/\ln 4$.

The main new step is a deterministic filtering reduction. Moduli are chosen one small prime factor at a time, using exact thin-product witness counts to certify positive answers and to eliminate whole blocks of unresolved queries. Repeated filtering removes the need to scan individual modular witnesses, which was the bottleneck of earlier deterministic reductions (the prime-by-prime idea is suggested in footnote 9 of the source paper, after Fischer, Kaliciak and Polak). With middle blocks of size $n^{\varepsilon/2}$ this yields all-edges Exact Triangle in $n^{3-\delta+o(1)}$, where

$$\delta = \min\{\varepsilon\Gamma,\ 1-\varepsilon a,\ \varepsilon(1/2-q)\},$$

and deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.

The exact rational parameters $c = 21.2733$, $\theta = 0.111731$ and $\varepsilon = 0.056846$ satisfy the thin regime $\varepsilon(a+\Gamma) < 1$ with margin $1.16\times10^{-6}$, and give $\delta > 0.00399928$. Hence APSP runs in $n^{2.99600072+o(1)}$, and the gap $2.996001 - 2.99600072 > 0$ absorbs the subpolynomial factor.

Significance

This is the first deterministic entry near $2.996$. Earlier analyses reached about $2.99601$ only by repeating random-prime hashing, which this word-RAM model cannot express. The deterministic filtering closes that gap.

Selected references

• J. Alman and V. Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs (2026). https://arxiv.org/abs/2610.06783
• Deterministic APSP in $O(n^{2.996001})$: an explicit refinement of the thin-product method, technical note, 6 October 2026. This is the source of $2.996001$ and has not been peer reviewed.

Motivation

The $\beta$-model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of $n$ nonlinear equations in $n$ unknowns, one per vertex, where $n$ can be in the thousands.

Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.

Setting

Let $n\ge 3$ and label the vertices $1,\dots,n$. For $\beta=(\beta_1,\dots,\beta_n)\in\mathbb R^n$, the $\beta$-model puts an edge between distinct vertices $i$ and $j$ independently with probability

$$p_{ij}(\beta)=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}}.$$

Given an observed graph with degrees $d_1,\dots,d_n$, the maximum likelihood estimate $\hat\beta$ must satisfy the ML equations

$$d_i=\sum_{j\ne i}\frac{e^{\hat\beta_i+\hat\beta_j}}{1+e^{\hat\beta_i+\hat\beta_j}},\qquad i=1,\dots,n.\tag{3}$$

The sup norm of $x\in\mathbb R^n$ is $|x|_\infty=\max_i|x_i|$. For $i\ne j$ put $r_{ij}(x)=1/(e^{-x_j}+e^{x_i})$, and define the map $\varphi:\mathbb R^n\to\mathbb R^n$ by

$$\varphi_i(x)=\log d_i-\log\sum_{j\ne i}r_{ij}(x).$$

Starting from any $x_0\in\mathbb R^n$, the fixed-point iteration is $x_{k+1}=\varphi(x_k)$. The fixed points of $\varphi$ are exactly the solutions of (3).

For an $n\times n$ matrix $A=(a_{ij})$, the $L^\infty$ operator norm is $|A|_\infty=\max_i\sum_j|a_{ij}|$. For $\delta>0$, the class $\mathcal L_n(\delta)$ consists of the matrices with $|A|_\infty\le 1$, $a_{ii}\ge\delta$ and $a_{ij}\le-\delta/(n-1)$ for $i\ne j$. For $x,y\in\mathbb R^n$, $J(x,y)$ is the matrix with entries $J_{ij}(x,y)=\int_0^1\frac{\partial\varphi_i}{\partial x_j}(tx+(1-t)y)\,dt$.

Formalization targets

Goal: Theorem 1.5

There are functions $\Theta(a,b)\in[0,1)$ and $C(a,b)$, $C$ continuous, independent of $n$ and $d$, such that for every $n\ge3$ and every $d\in(0,\infty)^n$: if (3) has a solution $\hat\beta$, then $\hat\beta=\varphi(\hat\beta)$, it is the unique solution of (3), and for all $x_0$ and $k$

$$|x_k-\hat\beta|_\infty\le\Theta(|\hat\beta|_\infty,|x_0|_\infty)^{\lfloor k/2\rfloor}|x_0-\hat\beta|_\infty,\qquad |x_0-\hat\beta|_\infty\le C(|\hat\beta|_\infty,|x_0|_\infty)\,|x_0-x_1|_\infty;$$

and if (3) has no solution, then every orbit $\{x_k\}$ is unbounded.

Milestones, in the order the proof uses them

1. p. 9: $\varphi(x)=x$ if and only if $x$ solves (3).
2. (6)–(7), p. 12: on $|x|_\infty\le K$, $-\frac{e^{2K}}{n-1}\le\frac{\partial\varphi_i}{\partial x_j}\le-\frac{e^{-4K}}{2(n-1)}$ for $i\ne j$, and $\frac12e^{-4K}\le\frac{\partial\varphi_i}{\partial x_i}\le e^{2K}$.
3. (8), pp. 12–13: $\varphi(x)-\varphi(y)=J(x,y)(x-y)$; off-diagonal partials are negative, diagonal ones positive, and every row of the Jacobian has absolute sum $1$.
4. Lemma 2.1, p. 11: for $A,B\in\mathcal L_n(\delta)$,

$$|AB|_\infty\le 1-\frac{2(n-2)\delta^2}{n-1}.$$

5. (9), p. 13: with $K$ the largest of $|x|_\infty,|y|_\infty,|\varphi(x)|_\infty,|\varphi(y)|_\infty$ and $\delta=\frac12e^{-4K}$,

$$|\varphi(\varphi(x))-\varphi(\varphi(y))|_\infty\le\Big(1-\frac{2(n-2)\delta^2}{n-1}\Big)|x-y|_\infty,$$

and $|\varphi(x)-\varphi(y)|_\infty\le|x-y|_\infty$. 6. (10), p. 13: a single $\theta=\Theta(|\hat\beta|_\infty,|x_0|_\infty)\in[0,1)$, continuous in its arguments, with $|x_{k+3}-x_{k+2}|_\infty\le\theta|x_{k+1}-x_k|_\infty$ and $|x_{k+2}-\hat\beta|_\infty\le\theta|x_k-\hat\beta|_\infty$.

Significance

The theorem turns an implicit statistical object, the MLE of an $n$-parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on $n$; an a posteriori error bound in terms of the computable step $|x_0-x_1|_\infty$; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound $|x_0-\hat\beta|_\infty\le C|x_0-x_1|_\infty$ is the device that proves consistency of the MLE (Theorem 1.3, applied with $x_0=\beta$), and the two-step contraction is reused in the proof of the graph-limit theorem.

The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.

Difficulty

The obvious approach is to show that $\varphi$ is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of $\varphi$ has absolute sum exactly $1$, so $\varphi$ is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map $\varphi\circ\varphi$, through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to $1$ as the norms grow. A second difficulty is uniformity: the factor must be bounded away from $1$ independently of $n$, which needs $(n-2)/(n-1)\ge\frac12$, hence $n\ge3$. For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.

Formalization scope

• Vertices are Fin n $=\{0,\dots,n-1\}$; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm $|x|_\infty$. Matrix norms are the explicit maximal absolute row sum.
• The degrees $d_i$ are arbitrary positive reals. This is a generalization of the page (degrees of a graph), and it is all the proof uses; positivity is required because $\log d_i$ is junk in Lean at $0$.
• $n\ge3$ is a hypothesis of the goal and of (10). It is not on the page but is necessary: for $n=2$, (3) reads $d_1=d_2=p_{12}$, whose solutions form a line, so uniqueness fails, and the factor in Lemma 2.1 equals $1$.
• Partial derivatives are Fréchet derivatives applied to unit vectors; $J(x,y)$ uses the interval integral over $[0,1]$.
• "Geometrically fast, with rate depending only on $(|\hat\beta|_\infty,|x_0|_\infty)$" is stated with the function $\Theta$ quantified before $n$, $d$, $\hat\beta$ and $x_0$, and "$C$ is a continuous function of the pair" likewise. A version that chooses the rate after fixing $n$, $d$ and $x_0$ is strictly weaker and nearly says only that a convergent sequence converges; it is not the target.
• "A divergent subsequence" is stated as unboundedness of $\{|x_k|_\infty\}$, which is equivalent for sequences in $\mathbb R^n$.
• The paper's remark that $\theta$ is "uniformly bounded away from 1 on subsets of $\mathbb R^n\times\mathbb R^n$" holds only on bounded subsets; it is not stated separately, and its quantitative content is (10).

Needed infrastructure: calculus of $\varphi$ (derivatives of $\log$ of a sum of exponentials), the integral form of the mean value theorem for maps $\mathbb R^n\to\mathbb R^n$, and elementary matrix-norm estimates. The class $\mathcal L_n(\delta)$ and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.

Selected references

• S. Chatterjee, P. Diaconis and A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. arXiv:1005.1136v5, DOI 10.1214/10-AAP728
• P. W. Holland and S. Leinhardt, An exponential family of probability distributions for directed graphs, J. Amer. Statist. Assoc. 76, 33–65, 1981. DOI 10.1080/01621459.1981.10477598
• J. Park and M. E. J. Newman, Statistical mechanics of networks, Phys. Rev. E 70, 066117, 2004. arXiv:cond-mat/0405566
• J. Blitzstein and P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Mathematics 6(4), 489–522, 2011. DOI 10.1080/15427951.2010.557277

Motivation

A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon $T$? Kakade calls this number the sample complexity of exploration.

The question builds on two algorithms. $E^3$ (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. $R_{max}$ (Brafman and Tennenholtz 2002) replaced $E^3$'s explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of $R_{max}$. For deterministic MDPs it shows that the number of non-optimal steps is at most $NAT$, which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on $N$, $A$ and $T$ made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.

Setting

An MDP $M$ has a finite set $S$ of $N$ states, a finite nonempty set of $A$ actions, a transition model $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A deterministic MDP has a next-state map $f$, with $P(s'\mid s,a)=1$ exactly when $s'=f(s,a)$.

Online model. An algorithm $\mathcal A$ is a deterministic function that maps the path observed so far, $(s_0,a_0,r_0,\dots,s_t)$, to the next action $a_t$. Started at $s_0$, it produces one path $c=(s_0,a_0,s_1,a_1,\dots)$; $c_t$ is the subpath up to $s_t$. The $T$-step end time $t'$ of $t$ is the smallest multiple of $T$ larger than $t$. The $T$-step value of the algorithm on $c_t$ is the normalized reward it collects until $t'$,

$$U_{\mathcal A}(c_t)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{t'-1}r(s_\tau,a_\tau)\Big],$$

and $U^*(c_t)$ is the supremum of this quantity over all algorithms continuing from $c_t$.

$T$-step policies. A $T$-step policy $\pi$ is a sequence of deterministic decision rules $\pi(\cdot,0),\dots,\pi(\cdot,T-1)$. Its $t$-value is $U_{\pi,t,M}(s)=\frac1T\mathbb E[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s]$, and $U^*_{t,M}(s)$ is the supremum over $T$-step policies. For a set of states $K$, the induced MDP $M_K$ agrees with $M$ on $K$ and makes every state outside $K$ absorbing with reward $1$. The escape probability $\Pr(\text{escape from }K\mid\pi,M,s_t=s)$ is the probability that the path $(s_t,\dots,s_{T-1})$ of $\pi$ in $M$ leaves $K$. A transition model $\hat P$ is an $\varepsilon$-approximation to $P$ if $\sum_{s'}|\hat P(s'\mid s,a)-P(s'\mid s,a)|<\varepsilon$ for every $(s,a)$.

Formalization targets

Goal: Theorem 8.3.5 (deterministic sample complexity)

For every $N$, $A$ and $T\ge1$ there is one algorithm $\mathcal A$ such that, for every deterministic MDP with rewards in $[0,1]$, every start state and every $L$,

$$\#\{\,t<L:\ U_{\mathcal A}(c_t)\neq U^*(c_t)\,\}\ \le\ NAT .$$

Milestones

• Lemma 8.4.4 (induced inequalities). For every $T$-step policy, every $t<T$ and every state $s$,

$$U_{\pi,t,M_K}(s)\ge U_{\pi,t,M}(s)\ge U_{\pi,t,M_K}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Corollary 8.4.5 (implicit explore or exploit). If $\pi$ is $T$-step optimal in $M_K$, then for every $t<T$ and every state $s$,

$$U_{\pi,t,M}(s)\ge U^*_{t,M}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Deterministic escapes (p. 114). In a deterministic MDP every escape probability is $0$ or $1$.
• Non-escaping steps are optimal (p. 114). In a deterministic MDP, an optimal policy of $M_K$ that does not escape from $(s,t)$ satisfies $U_{\pi,t,M}(s)=U^*_{t,M}(s)$.
• Lemma 8.5.4 ($\varepsilon$-approximation condition). If $\hat P$ is an $\varepsilon$-approximation to $P$ and the rewards agree, then $|U_{\pi,t,\hat M}(s)-U_{\pi,t,M}(s)|<\varepsilon T$ for all $\pi$, $s$ and $t<T$.
• Lemma 8.5.5, pinned. If $m\ge\frac{8N}{\varepsilon^2}\log\frac{2N}\delta$ with $\varepsilon>0$, $0<\delta<1$, then the empirical distribution of $m$ independent samples from a distribution $p$ on $N$ points satisfies $\sum_i|\hat p(i)-p(i)|\le\varepsilon$ with probability greater than $1-\delta$.

Significance

The result. The bound $NAT$ does not depend on $L$. However long the agent runs, only a fixed number of its steps fail to be $T$-step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has $\Omega(NAT)$ such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.

Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:

• a verified finite-horizon dynamic-programming layer (backward recursions, optimal $T$-step values as suprema);
• a simulation lemma in $\ell_1$;
• a concentration bound for empirical distributions whose sample size is linear in $N$;
• an explicit construction of an online exploration algorithm, with a counting argument about its run.

The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form $P(|\hat p_i-p_i|>\alpha p_i)\le2e^{-\alpha^2p_im/2}$. This form fails for the upper tail when $\alpha>1$, so the pinned statement needs a different argument.

Difficulty

The algorithm must be fixed before the MDP. It knows nothing about $f$ or $r$ beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full $T$-step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most $T$ steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that $U^*_{t,M}$ is a supremum over all $T$-step policies, so the comparison has to go through $M_K$ for every competing policy, not only the planner's.

Formalization scope

• Model. $S$ and $A$ are finite types, $A$ nonempty; $N=|S|$ and $A=|A|$. Rewards are deterministic, with $0\le r\le1$ a hypothesis of every statement. Transition models are IsTransitionKernel functions $P(s'\mid s,a)$.
• Normalization and time. Values carry the factor $1/T$, so they lie in $[0,1]$; epochs are 0-based. $T$-step policies are functions $\mathbb N\to S\to A$, entered into the canonical stochastic $T$-epoch layer as indicator policies. $U^*_{t,M}$ is the supremum over these policies, which is bounded under the hypotheses.
• Online model. In the online model the algorithm has type List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. $U_{\mathcal A}(c_t)$ is the realised normalized sum up to the end time, and $U^*(c_t)$ is the backward recursion $W_{t'-t}(s_t)$, which is the supremum over algorithms by the Markov property. The count runs over $t<L$ for every $L$.
• Corrections to the printed text. Corollary 8.4.5 is stated for $t<T$, where its quantities are defined; the printed range is $t\le T$. Lemma 8.5.5 carries an explicit sample size in place of $O(\cdot)$.

Four formalizations would make the goal trivial or false, and each is excluded:

• quantifying the algorithm after the MDP, which lets it read $f$ and $r$;
• giving the algorithm a type that takes $f$ or $r$ as an argument;
• defining $U^*$ as a junk real supremum;
• hiding rewards from the observed path, which makes the statement false.

Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the $\ell_1$ concentration bound. Contributions to any of these are useful independently of the goal.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• R. I. Brafman and M. Tennenholtz, R-max — a general polynomial time algorithm for near-optimal reinforcement learning, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/brafman02a.html
• M. Kearns and S. Singh, Near-optimal reinforcement learning in polynomial time, Machine Learning 49, 2002. https://doi.org/10.1023/A:1017984413808
• A. L. Strehl, L. Li and M. L. Littman, Reinforcement learning in finite MDPs: PAC analysis, Journal of Machine Learning Research 10, 2009. https://jmlr.org/papers/v10/strehl09a.html

Motivation

Planning in a Markov decision process with a large or infinite state space cannot visit every state. The trajectory tree method of Kearns, Mansour and Ng (2000) finds a near-best policy in a class $\Pi$ with a number of generative-model calls independent of the state space, but exponential in the horizon $T$. Chapter 6 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), trades that exponential factor for a weaker notion of optimality. The weaker notion is tied to a reset distribution $\mu$ that encodes prior knowledge of where good policies spend their time, such as a desired trajectory in robotic control or a known operating regime of a queueing network.

The resulting algorithm, μ-PolicySearch, chooses one decision rule per time step, backward in time, from a hypothesis class $\Pi_1$, optimizing each against states drawn from $\mu$. The same idea was later published as Policy Search by Dynamic Programming (Bagnell, Kakade, Ng and Schneider, NeurIPS 2003). Conservative policy iteration (Kakade and Langford, ICML 2002) carries the same reset-distribution idea into the discounted setting.

Timeline:

• 2000 — Kearns, Mansour and Ng: trajectory trees; uniform convergence over $\Pi$ with $O(2^T)$ dependence on the horizon.
• 2002 — Kakade and Langford: the performance difference lemma for discounted values and conservative policy iteration under a reset distribution.
• 2003 — Kakade's thesis, Chapter 6: μ-optimality (Theorem 6.3.1) and μ-PolicySearch, with sample complexity polynomial in $T$ (Theorem 6.3.3, an $O(\cdot)$ statement not part of this mission).

Setting

A T-epoch MDP has a finite state set $S$, a finite nonempty action set $A$, a transition kernel $P(s'\mid s,a)$, a deterministic reward $r(s,a)\in[0,1]$ and a horizon $T\ge1$. Decision epochs are $t=0,\dots,T-1$. A non-stationary policy $\pi$ gives a distribution $\pi(\cdot\mid s,t)$ over actions at each state and epoch. A decision rule is a map $h:S\to A$. A class $\Pi_1$ of decision rules induces the class $\Pi=\Pi_1^T$ of deterministic policies that use a rule of $\Pi_1$ at every epoch.

Values are normalized. The $t$-value $V_{\pi,t}(s)$ is $\frac1T$ times the expected reward collected from epoch $t$ to $T-1$ when starting in $s$ at epoch $t$, so $V_{\pi,t}(s)\in[0,1]$. The value is $V_\pi(s)=V_{\pi,0}(s)$. The state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_{\pi,t+1}(s')]$, and the advantage is $A_{\pi,t}(s,a)=Q_{\pi,t}(s,a)-V_{\pi,t}(s)$. The future state-time distribution of $\pi$ from $s_0$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$ on $S\times\{0,\dots,T-1\}$.

A μ-reset distribution $\mu$ is a family of distributions $\mu(\cdot\mid t)$ on $S$, one per epoch $t<T$. Its joint law, uniform over epochs, is $\mu(s,t)=\mu(s\mid t)/T$. For a decision rule $h$ the μ-advantage is

$$A_{\pi,t}(\mu,h)=\mathbb E_{s\sim\mu(\cdot\mid t)}\big[A_{\pi,t}(s,h(s))\big],$$

and $Q_{\pi,t}(\mu,h)$ is defined in the same way. The ℓ1 distance of two functions on $S\times\{0,\dots,T-1\}$ is $\|p-q\|_1=\sum_s\sum_{t<T}|p(s,t)-q(s,t)|$.

Formalization targets

Goal: μ-optimality (Theorem 6.3.1, p. 75)

If a policy $\pi$ satisfies $A_{\pi,t}(\mu,h)\le\varepsilon/T$ for all $h\in\Pi_1$ and $t<T$, then for all $\pi'\in\Pi$ and all start states $s_0$,

$$V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-T\,\|d_{\pi',s_0}-\mu\|_1 .$$

Milestones

• Lemma 5.2.1 (undiscounted), p. 59. $V_{\pi'}(s_0)-V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s,t)}[A_{\pi,t}(s,a)]$ for all policies $\pi,\pi'$.
• Change of measure, p. 76. $T\,\mathbb E_{d_{\pi',s_0}}\mathbb E_{\pi'}[A_{\pi,t}]\le T\,\mathbb E_{\mu}\mathbb E_{\pi'}[A_{\pi,t}]+T\|d_{\pi',s_0}-\mu\|_1$.
• Lemma 5.3.1, p. 63. The policy returned by non-stationary approximate policy iteration (NAPI) has the same $Q_{\pi,t}$ as the input policy of update $t$. Its advantages are bounded by the per-state errors $\varepsilon_t(s)$ of the PolicyChooser.
• Theorem 6.3.2, p. 76. Exact μ-PolicySearch returns $\tilde\pi$ with $A_{\tilde\pi,t}(\mu,h)\le0$ for all $h\in\Pi_1$, $t<T$.

Significance

Theorem 6.3.1 states what μ-PolicySearch buys. The guarantee holds at every start state, whereas the trajectory tree guarantee holds only at the root it was built for. The policy is guaranteed to compete with each policy of $\Pi$ whose future state-time distribution is close to $\mu$. The penalty $T\|d_{\pi',s_0}-\mu\|_1$ makes the role of the reset distribution precise: it is the price of the change from the "training" distribution $\mu$ to the "test" distribution $d_{\pi',s_0}$. With Theorem 6.3.2 at $\varepsilon=0$, the exact algorithm attains the bound with no slack. The sample-based analysis (Theorem 6.3.3) reduces to controlling the $\varepsilon/T$ condition.

The results are proved in the thesis, and no machine-checked version is known to exist. The mission produces a Lean development of the normalized T-epoch model (non-stationary policies, $t$-values, advantages, future state-time distributions) together with the undiscounted performance difference lemma. These pieces are the common substrate of Chapters 4–6 of the thesis and of later finite-horizon policy-search analyses.

Difficulty

The performance difference lemma relates two objects defined in opposite directions of time: the state distribution of $\pi'$ runs forward from $s_0$, while the $t$-values of $\pi$ are defined backward from the horizon. A formal statement must keep the epochs of the two aligned, including the boundary epochs $t=0$ and $t=T-1$. The change of measure needs the bound $|A_{\pi,t}(s,a)|\le1$, which holds only because values are normalized and rewards lie in $[0,1]$. With unnormalized rewards the constant $T$ in front of the ℓ1 term is wrong.

A first idea is to read the hypothesis as "the advantages are small under $d_{\pi',s_0}$". That reading is not available. The hypothesis controls averages under $\mu$ only, and the gap between the two distributions is exactly the penalty term.

Formalization scope

• The state space is finite (Fintype S), so expectations and the ℓ1 distance are finite sums. The thesis also allows infinite state spaces in this chapter, with integrals in place of sums.
• Epochs are 0-based, $t\in\{0,\dots,T-1\}$, with $T\ge1$.
• Values carry the factor $1/T$. $V_{\pi,t}$ is defined by backward recursion and is $0$ for $t\ge T$.
• Policies are real functions π t s a together with a validity predicate. Deterministic policies $h=(h_t)$ enter as indicator policies $\pi(a\mid s,t)=\mathbf 1[a=h_t(s)]$.
• $\Pi_1$ is an arbitrary set of deterministic decision rules, not assumed finite. Exact μ-PolicySearch is described as a run: the chosen rule at each update is an exact maximizer over $\Pi_1$ of $Q_{\pi,t}(\mu,\cdot)$ for the current policy $\pi$, and the run is stated by hypotheses rather than by a choice of argmax.
• The policy $\pi$ in the goal may be stochastic. The competitors $\pi'$ range over $\Pi_1^T$.
• The μ-mismatch term must stay in the goal. Dropping it, or replacing $d_{\pi',s_0}$ by $\mu$, gives a different and false statement. An empty class $\Pi_1$ makes the conclusion vacuous. That case is harmless, since the conclusion only quantifies over $\pi'\in\Pi_1^T$, and the source has it too.

The T-epoch layer (policies, state distributions, values, advantages, the future state-time distribution) is shared with the other missions of this series (namespaces SampleComplexityRL.PolicyGrad and SampleComplexityRL.Mismeasure); the μ-reset objects are defined in SampleComplexityRL.MuPolicySearch; IsTransitionKernel and IsPolicy are published definitions. Contributions of the performance difference lemma and of general facts about the T-epoch layer (values in $[0,1]$, $d_{\pi,s_0}$ sums to one) are welcome.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• M. Kearns, Y. Mansour, A. Y. Ng, Approximate planning in large POMDPs via reusable trajectories, NeurIPS 12, 2000. https://papers.nips.cc/paper_files/paper/1999
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. A. Bagnell, S. Kakade, A. Y. Ng, J. Schneider, Policy search by dynamic programming, NeurIPS 16, 2003. https://papers.nips.cc/paper_files/paper/2003