All missions

Why approximate closure matters

Policy gradient methods search for a policy by changing a finite vector of parameters. The method can reach a stationary point of its objective without finding an optimal policy: a small change in the available parameters might not represent the policy improvement that the underlying control problem calls for. Bhandari and Russo identify a condition on the policy class that limits this obstruction. Their exact-closure result rules out suboptimal stationary points; their approximate-closure result measures the residual cost when the class can represent policy improvements only approximately. This mission formalizes the latter statement, Theorem 5 of Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods, using the arXiv v3 text and numbering.

The result concerns the optimization landscape rather than a particular gradient algorithm or convergence rate. It applies to structured policy classes in discounted control problems, including settings with general state spaces. The paper also discusses state aggregation as a source of small approximation error in Lemma 15; that example motivates the error condition, while the target here is the general guarantee of Theorem 5. The error is measured in the states visited by each current policy, so the condition describes what the restricted class can do where improvement affects that policy's performance.

The discounted control setting

A Markov decision process has a measurable state space $S$, a measurable action space $A$, and a nonempty feasible action set $A_s$ at each state $s$. Choosing $a\in A_s$ incurs a bounded cost $g(s,a)$ and changes the state according to a probability kernel $P(\cdot\mid s,a)$. A discount factor $\gamma\in(0,1)$ reduces future costs, and an initial probability measure $\rho$ specifies where evaluation begins. A stationary policy is a measurable choice $\pi(s)\in A_s$.

The cost-to-go $J_\pi(s)$ is the expected sum of discounted costs when starting at $s$ and following $\pi$. The discounted occupancy measure $\eta_\pi$ is the normalized, discounted distribution of visited states when the initial state has law $\rho$. The policy's objective is $\ell(\pi)=(1-\gamma)\int J_\pi\,d\rho$. The factor $1-\gamma$ puts $\ell$ on the scale of a per-period cost. An optimal policy $\pi^*$ minimizes cost-to-go at every state. Section 2, pp. 5–8 supplies these objects and Assumptions 1 and 2: absolute continuity of $\eta_{\pi^*}$ with respect to $\rho$, and measurable selection of a Bellman-minimizing action for bounded measurable value functions.

A parameter $\theta$ belongs to a convex set $\Theta\subseteq\mathbb R^d$ and determines a feasible policy $\pi_\theta$. The policy gradient objective is $\ell(\theta)=\ell(\pi_\theta)$. A stationary point is a feasible parameter with $\langle\theta'-\theta,\nabla\ell(\theta)\rangle\ge0$ for every $\theta'\in\Theta$. The Bellman optimality operator $T$ selects the smallest one-step cost plus discounted future value among feasible actions. The weighted policy improvement objective $B(\bar\theta\mid\eta_{\pi_\theta},J_{\pi_\theta})$ evaluates the one-step Bellman update from a candidate policy $\pi_{\bar\theta}$, averaged under the current policy's occupancy measure. Section 5.1, pp. 12–14 introduces its smoothness and stationary-point conditions.

Formalization targets

The target is Theorem 5, p. 26. Condition 5 says the restricted class has inherent Bellman error $\varepsilon\ge0$: for each current policy in the class, a class member gets within $\varepsilon$ of the best one-step weighted Bellman objective over all feasible policies. Condition 2.A says stationary points of that weighted one-step objective are global minima over $\Theta$. Condition 0 supplies differentiability. For a nonnegative coefficient $\kappa$ satisfying the effective concentrability inequality (13), the goal is continuous differentiability of $\ell$ and, at every stationary point,

$$\ell(\pi_\theta)-\ell(\pi^*)\le\frac{\kappa}{1-\gamma}\,\varepsilon.$$

The paper defines $\kappa_\rho$ as the least coefficient satisfying (13). The Lean statement quantifies over an admissible $\kappa$; its conclusion therefore includes the bound at $\kappa_\rho$ when that coefficient is finite. The milestone list follows the paper's supporting statements: occupancy domination after (2), Bellman inequalities (5), the performance difference identity (29), the policy gradient formula in Lemma 6, the stationary policy-improvement identity in Lemma 7, and the Bellman-error bound displayed in the proof of Theorem 5.

What the result establishes

The bound turns a property of the policy class into a quantitative guarantee about every stationary parameter. If $\varepsilon=0$ and a finite concentrability bound applies, the stated cost gap is zero. For positive error, it separates the approximation error from the factor $\kappa/(1-\gamma)$ that reflects evaluation under the exploratory start distribution and the effective planning horizon. Thus a small gradient alone is not the claim; the structural conditions on the one-step objective and the policy class determine what stationarity means for long-run cost. Theorem 5 and its discussion, §8 make this interpretation explicit.

The paper proves Theorem 5. The declarations in this mission currently compile as open theorem statements; they are not machine-checked proofs. A complete development would formalize the links among discounted kernels, occupancy integrals, Bellman operators, and gradients on the parameter space. The general measurable-state MDP definitions would be reusable for other discounted control results, while the stationary-point and approximate-closure predicates provide a vocabulary for further policy-gradient theorems.

Where the difficulty lies

A stationary point of $\ell$ need not be a minimum of the one-step Bellman objective by definition. Condition 0 and Lemma 6 connect their gradients, and Condition 2.A then links stationary points to minima of the restricted one-step objective. Approximate closure only compares that restricted minimum with the unrestricted one up to $\varepsilon$. The final result also requires moving an error measured under $\eta_{\pi_\theta}$ to one under $\rho$ and relating Bellman residual to the optimality gap. Each comparison has a distinct measure or operator, and losing a discount factor changes the constant in the theorem.

Formalization scope

The Lean model uses arbitrary measurable spaces for $S$ and $A$ and measurable stationary policies, extending the paper's Borel-subset setting. The cost and kernel are defined on all $S\times A$ and are uniformly bounded there; feasibility still restricts every policy and Bellman minimization to $A_s$. These extensions let Condition 0 evaluate nearby parameter values even when their policies need not be feasible. The representation uses Mathlib kernels, measures, Bochner integrals, and Euclidean parameter vectors. It fixes $0<\gamma<1$, a probability initial distribution, nonempty feasible action sets, an optimal policy, and the paper's Assumptions 1 and 2. The goal carries a nonnegative concentrability coefficient and Conditions 0, 2.A, and 5; it does not assume exact closure or the Bellman-error conclusion it is meant to establish.

Two corrections to the printed assumptions are explicit. The Bellman operators contain $\gamma$, consistently with equations (6) and (7), although displays (3) and (4) omit it. Condition 0 asks for joint continuous differentiability near the current parameter pair, the form used by the proof of Lemma 6; the printed condition lists two partial maps. The theorem's $\kappa$ is constrained to be nonnegative to represent the paper's effective concentrability coefficient. Definitions use pointwise optimality rather than a real-valued infimum over policies, and Bellman minimization uses the nonempty feasible-action subtype. These choices prevent default values of ill-bounded infima or non-integrable functions from turning the target into an empty claim. The needed contributions are proofs of the six milestones and the final bound, plus supporting measurable-kernel and gradient facts.

Selected references

• J. Bhandari and D. Russo, Global Optimality Guarantees for Policy Gradient Methods, Operations Research 72 (2024); preprint arXiv:1906.01786v3 (2022), arXiv, DOI.

Motivation

Sequential decisions often have costs whose timing matters. A controller may choose an action now, observe a random next state, and choose again. Ordinary expected-cost minimization averages the sum of the costs. A risk-sensitive criterion first applies an increasing function $U$ to the total cost and then takes its expectation. The curvature of $U$ changes how uncertain costs affect the ranking of policies: convex utility penalizes variability in a cost-minimization problem, while concave utility has the opposite tendency. Bäuerle and Rieder study this criterion for controlled Markov processes with general continuous increasing utility, rather than fixing an exponential function. Their finite-horizon discounted result is Theorem 3.6, pp. 10–12 of the authors' manuscript.

Discounting gives early and late costs different weights. For linear $U$, the remaining expected cost can be described using only the current physical state. For general $U$, the effect of a future cost also depends on what has already been paid and on the discount weight currently attached to the next cost. The mission targets the paper's finite-horizon treatment of these two additional quantities. The infinite-horizon problem is a separate part of the paper.

Setting

The state space $E$ and action space $A$ are Borel spaces. At state $x$, the nonempty set $D(x)$ contains the actions that may be chosen. If action $a\in D(x)$ is selected, the next state has distribution $Q(\cdot\mid x,a)$ and the stage cost is $c(x,a)$. The cost is measurable and bounded between positive constants $\underline c$ and $\overline c$. The discount factor satisfies $0<\beta<1$, and $U:[0,\infty)\to\mathbb R$ is continuous and strictly increasing. The paper imposes its compactness and continuity conditions (CC) on $U$, $D$, $c$, and $Q$; these are stated in the model item and correspond to §2, pp. 3–4.

A history policy $\sigma=(g_0,g_1,\ldots)$ chooses $A_n$ measurably from the states and actions observed through time $n$. Starting from $x$, it induces a law for the state-action trajectory. The first $n$ stages incur the discounted cost $C^n_\beta=\sum_{k=0}^{n-1}\beta^k c(X_k,A_k)$, with $C^0_\beta=0$. The paper minimizes $E_x^\sigma[U(C^N_\beta)]$ over every admissible history policy. The inverse utility appearing in the paper's original certainty-equivalent criterion can be omitted when selecting a minimizer because $U$ is strictly increasing §2, p. 3; §3.3, p. 10.

The extended state is $\hat E=E\times[0,\infty)\times(0,1]$. Its coordinates $(x,y,z)$ record the current physical state, accumulated cost, and current discount weight. Define $V_{n\sigma}(x,y,z)=E_x^\sigma[U(y+zC^n_\beta)]$ and $V_n=\inf_{\sigma\in\Pi}V_{n\sigma}$. A measurable extended-state decision rule $f$ chooses an action in $D(x)$. The paper's operator $T_f$ integrates a continuation value at $(x',y+zc(x,f(x,y,z)),z\beta)$; $T$ takes the infimum of the same integral over $D(x)$ equations (3.8)–(3.9), pp. 10–11.

Formalization targets

The first target identifies the cost iteration of any sequence of extended-state rules $\pi=(f_0,f_1,\ldots)$:

$$V_{n\pi}=T_{f_0}\cdots T_{f_{n-1}}U,\qquad 1\le n\le N.$$

The second target is the paper's value iteration for the infimum over all history policies, together with membership of every $V_n$ in its regularity class $C(\hat E)$:

$$V_0(x,y,z)=U(y),\qquad V_n=TV_{n-1},\qquad V_n\in C(\hat E).$$

The goal is Theorem 3.6(c): minimizers $f_k^*$ of $V_{k-1}$ exist, and their stage-dependent history rules attain the original objective $J_N(x)=V_N(x,0,1)$ for every $x$. At stage $n<N$, the rule uses $f_{N-n}^*$ at the current state, the observed sum $\sum_{j<n}\beta^jc(X_j,A_j)$, and $\beta^n$. “Optimal” compares against all admissible history policies, including those that use more of the history than these three quantities.

Significance

Theorem 3.6 gives a finite sequence of minimum-operator evaluations for a problem whose utility of total cost is not additively separable in the physical state alone. Its policy statement also identifies which observable quantities an optimal controller needs to retain. Together, these results relate the original history-dependent problem to an extended-state Markov decision problem §3.3, pp. 10–12.

The paper proves these statements. This mission asks for machine-checked definitions and proofs of the finite-horizon discounted theorem, including the comparison with all admissible history policies. The model layer and the finite-dimensional expectation construction can support later formalizations of other risk-sensitive objectives. The mission itself has no completed proof at the drafting stage.

Difficulty

The extra discount coordinate is essential: after one action, the next cost enters utility with weight $z\beta$, not $z$. Keeping only accumulated cost would describe a different process. The other demanding point is the policy comparison. An iteration over extended-state decision rules has to establish the value of an infimum over arbitrary measurable history policies. Regularity and measurable selection must also be maintained at each step under (CC). The proof of Theorem 3.6 invokes the corresponding total-cost argument from Theorem 3.1, pp. 5–6; the formal development must supply the precise discounted version.

Formalization scope

Lean represents $E$ and $A$ as Borel subsets of Polish spaces, with standard Borel measurable structures. The controlled process is a separate reusable definition containing $D$, $Q$, and history policies; the risk-sensitive model adds $c$, $\beta$, and $U$. The admissible graph is Borel and every section $D(x)$ is nonempty. A history is a chronological finite list of earlier state-action pairs and a current state. Each rule is defined on all lists, but only admissible lists of the matching length are visited. The transition kernel is total as a Lean object, and its values outside $D$ are irrelevant.

Policy values use nested kernel integrals representing the finite-dimensional marginals of the path law. They are defined from the cost and utility, so the Bellman recursion remains a theorem. The optimized value is an infimum over the subtype of measurable, admissible infinite history policies. The real infimum is meaningful here because this policy class is nonempty under (CC) and finite-horizon costs keep utility bounded on the relevant interval. The extended state uses real coordinates restricted to $y\ge0$ and $0<z\le1$; its transition stays in that domain. “Increasing” in $C(\hat E)$ means componentwise nondecreasing in $(y,z)$. A minimizer is an admissible measurable rule satisfying $T_fv=Tv$ on the entire extended domain.

The source's proof sentence that $T$ preserves $C(\hat E)$ is recorded with explicit integrability of each one-step continuation. For an arbitrary real-valued member of $C(\hat E)$ on an unbounded state space, the source's conditions alone do not ensure a finite real expectation. This domain condition prevents Lean's zero value for a nonintegrable real integral from turning the assertion into a different one. It does not narrow the finite-horizon values appearing in the goal. Contributions toward finite-dimensional expectation identities, kernel integrability, the regularity of $V_n$, and measurable minimizer selection are within scope.

Selected references

• N. Bäuerle and U. Rieder, More Risk-Sensitive Markov Decision Processes, authors' manuscript, KIT repository 1000039663; published in Mathematics of Operations Research 39(1):105–120, 2014. Manuscript; DOI.

Motivation

Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.

The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).

Setting

For each size $N$, let $A(N)$ be a random symmetric $N\times N$ matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale $C/N$. Each coordinate $i$ carries a polynomial map $f^i(\cdot;t):\mathbb R^q\to\mathbb R^q$ at iteration $t$ and an initial vector $x_i^0$. Their coefficients have degree at most $d$ and a uniform bound $C$. The AMP orbit is

$$x_i^{t+1}=\sum_j A_{ij}f^j(x_j^t;t) -\sum_j A_{ij}^{2}Jf^j(x_j^t;t)f^i(x_i^{t-1};t-1).$$

The second sum is the Onsager memory term; it is absent at $t=0$. Here $Jf^j$ is the Jacobian, so its product with the preceding $q$-vector is another $q$-vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's $(C,d)$-regularity condition (Definitions 2–4, pp. 6–7).

A converging sequence has a fixed finite set of classes $a\in[k]$. Coordinate $i$ belongs to $C_a^N$ for one class $a$, whose proportion approaches $c_a\in(0,1)$. A symmetric nonnegative matrix $W$ specifies entry variances: if $i\in C_a^N$ and $j\in C_b^N$, then $\mathbb E A_{ij}^2=W_{ab}/N$. Independent labels $Y(i)$ have class-dependent laws $P_a$, each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form $f^i(x;t)=g(x,Y(i),a,t)$ for $i\in C_a^N$ (Definition 5, pp. 8–9).

The empirical second moments of $g(x_i^0,Y(i),a,0)$ converge in probability to a prescribed positive semidefinite matrix $\widehat\Sigma_a^0$. For $t\ge1$, state evolution defines

$$\Sigma_a^t=\sum_b c_bW_{ab}\widehat\Sigma_b^{t-1},\qquad \widehat\Sigma_a^t=\mathbb E\big[g(Z_a^t,Y_a,a,t)g(Z_a^t,Y_a,a,t)^{\mathsf T}\big],$$

where $Z_a^t\sim\mathcal N(0,\Sigma_a^t)$ is independent of $Y_a\sim P_a$. The index $t-1$ in the first formula and $t$ in the second are essential (equations (1.9)–(1.11), p. 9).

Formalization targets

Coordinate moments and concentration

For a nonnegative multi-index $m$ and a coordinate sequence eventually in class $a$, Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:

$$\mathbb E[(x_{i(N)}^t)^m]\longrightarrow\mathbb E[(Z_a^t)^m],\qquad \operatorname{Var}\!\left(\frac1{|C_a^N|}\sum_{i\in C_a^N}(x_i^t)^m\right)\longrightarrow0.$$

The diagonal two-time identity (4.4) is another milestone: $\Sigma_a^{t,t}$ has four blocks, each equal to $\Sigma_a^t$. These are the paper's stated intermediate targets (pp. 15, 30, 32).

Main goal: Theorem 4

For $t\ge1$, class $a$, and every locally Lipschitz function $\psi$ with $|\psi(x,y)|\le K(1+\|x\|_2^2+\|y\|_2^2)^K$ for some $K$, prove convergence in probability:

$$\frac1{|C_a^N|}\sum_{j\in C_a^N}\psi(x_j^t,Y(j)) \longrightarrow \mathbb E[\psi(Z_a^t,Y_a)].$$

The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).

Significance

The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled $N$-dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).

The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.

Difficulty

The matrix $A(N)$ is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).

Formalization scope

Vectors in $\mathbb R^q$ are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at $t=0$. A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.

The paper's displayed sub-Gaussian formula conflicts with its stated $C/N$ scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when $g$ ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small $N$. Positive limiting class fractions make those finite exceptions irrelevant.

Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's $Y(i)$ in (1.12) is read as $Y(j)$, its summation index, and its final covariance as $\Sigma_a^t$. The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.

Selected references

• M. Bayati, M. Lelarge and A. Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015, 753–822. arXiv:1207.7321v2; DOI:10.1214/14-AAP1010.

Why the landscape of policy gradient matters

Policy gradient methods optimize a parameterized policy for a Markov decision process by running gradient descent on its expected cost. They underlie most large-scale reinforcement learning, from robotics to game playing, and are also natural in operations research, where structured policy classes (linear feedback, base-stock levels, thresholds) are standard. The objective, however, is almost never convex in the parameters, and classical theory only promises convergence to stationary points. Whether such methods find optimal policies therefore depends on the landscape: whether stationary points can be suboptimal.

J. Bhandari and D. Russo (arXiv:1906.01786v3, published in Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which the answer is no, connecting policy gradient to classical policy iteration. Fazel et al. (2018) established a landscape result for linear-quadratic control; Kakade and Langford (2002) developed a performance-difference identity for conservative policy iteration on finite MDPs. Bhandari and Russo's Theorem 1 gives a general sufficient condition on a general state space; Agarwal et al. (2021) developed the tabular case in detail.

Setting

A Markov decision process is a tuple $(\mathcal S,(\mathcal A_s)_{s\in\mathcal S},g,P,\gamma,\rho)$: a measurable state space $\mathcal S$, nonempty feasible action sets $\mathcal A_s\subseteq\mathcal A$, a bounded measurable cost $g(s,a)$, a transition kernel $P(\cdot\mid s,a)$, a discount factor $\gamma\in(0,1)$ and an initial probability distribution $\rho$. A policy is a measurable map $\pi:\mathcal S\to\mathcal A$; it is feasible, $\pi\in\Pi$, if $\pi(s)\in\mathcal A_s$ for every $s$.

For a policy $\pi$, the cost-to-go $J_\pi(s)$ is the expected discounted sum of costs started from $s$. The discounted average cost is $\ell(\pi) = (1-\gamma)\int J_\pi\,d\rho$, and the discounted state-occupancy measure is $\eta_\pi = (1-\gamma)\sum_{t\ge0}\gamma^t P^\pi_\rho(s_t\in\cdot)$. The Bellman operators are

$$(T_\pi J)(s) = g(s,\pi(s))+\gamma\!\int\! J\,dP(\cdot\mid s,\pi(s)),\qquad (TJ)(s) = \min_{a\in\mathcal A_s}\Big[g(s,a)+\gamma\!\int\! J\,dP(\cdot\mid s,a)\Big].$$

An optimal policy $\pi^*$ satisfies $J_{\pi^*}\le J_\pi$ pointwise for every $\pi\in\Pi$. Two standing assumptions hold throughout: Assumption 1, $\eta_{\pi^*}\ll\rho$ (the initial distribution is exploratory), and Assumption 2, measurable selection of a minimizing action in $T$.

A parameterized policy class is $\Pi_\Theta = \{\pi_\theta:\theta\in\Theta\}\subseteq\Pi$ with $\Theta\subseteq\mathbb R^d$ convex, and $\ell(\theta) = \ell(\pi_\theta)$ is the policy gradient objective. A point $\theta\in\Theta$ is stationary if $\langle\theta'-\theta,\nabla\ell(\theta)\rangle\ge0$ for all $\theta'\in\Theta$. The weighted policy-iteration objective is

$$\mathcal B(\bar\theta\mid\eta,J) = \int (T_{\pi_{\bar\theta}}J)\,d\eta ,$$

the cost of following $\pi_{\bar\theta}$ for one period and then incurring $J$, averaged over $\eta$.

The three conditions of the main theorem are:

• Condition 0 (differentiability): the policy parameter and the parameter that generates the occupancy measure vary jointly, with the resulting $\mathcal B$ continuously differentiable near each $(\theta,\theta)$;
• Condition 1 (closure under policy improvement): for each $\pi\in\Pi_\Theta$ some $\pi^+\in\Pi_\Theta$ attains $\min_{\pi'\in\Pi}\mathcal B(\pi'\mid\eta_\pi,J_\pi)$;
• Condition 2.A: for each $\pi\in\Pi_\Theta$, $\bar\theta\mapsto\mathcal B(\bar\theta\mid\eta_\pi,J_\pi)$ has no suboptimal stationary points on $\Theta$.

Formalization targets

Goal: Theorem 1 (p. 14)

Under Conditions 0, 1 and 2.A, $\ell$ is continuously differentiable, and for every $\theta\in\Theta$

$$\theta\ \text{is a stationary point of }\ell\quad\Longleftrightarrow\quad \ell(\pi_\theta) = \ell(\pi^*).$$

The right side compares with the optimum over all feasible policies, not only the class.

Milestones

1. $\eta_\pi\succeq(1-\gamma)\rho$ (p. 7) and the element-wise inequalities (5), $TJ\preceq T_\pi J$ and $TJ_\pi\preceq J_\pi$ (p. 7).
2. The performance difference identity (29), $\ell(\pi)-\ell(\bar\pi) = \int[T_\pi J_{\bar\pi}-J_{\bar\pi}]\,d\eta_\pi$ (p. 39).
3. Lemma 6, the policy gradient theorem: $\nabla\ell(\theta) = \nabla_{\bar\theta}\mathcal B(\bar\theta\mid\eta_{\pi_\theta},J_{\pi_\theta})|_{\bar\theta=\theta}$ (p. 13).
4. Lemma 7: at a stationary point, $\int J_{\pi_\theta}\,d\eta_{\pi_\theta} = \min_{\pi\in\Pi_\Theta}\int(T_\pi J_{\pi_\theta})\,d\eta_{\pi_\theta}$ (p. 14).
5. Lemma 8, the on-average Bellman equation: $\ell(\pi) = \ell(\pi^*)\iff\int(J_\pi-TJ_\pi)\,d\rho = 0$ (p. 15).

Significance

Theorem 1 converts a question about a nonconvex, multi-period objective into checks on single-period problems. Any algorithm that provably reaches stationary points (projected gradient descent, for instance) then reaches globally optimal policies whenever the policy class is closed under improvement and the one-step problems are benign. The paper verifies the conditions for LQ control, finite MDPs with softmax policies, optimal stopping with threshold policies and inventory control with base-stock policies; the quantitative refinements (gradient dominance, approximate closure, finite horizons) are the subject of the later missions of this series.

The result is proved in the paper; nothing in it has been machine-checked. A formalization would produce a measure-theoretic library for discounted MDPs on general spaces (cost-to-go via kernels, occupancy measures, Bellman operators, the performance difference identity) that is reusable well beyond this paper, and would pin down the exact differentiability hypothesis the argument needs.

Difficulty

The obvious route, differentiating $\ell(\theta) = (1-\gamma)\int J_{\pi_\theta}\,d\rho$ directly, requires differentiating an infinite discounted sum of $t$-step kernels in the parameter, and on a general state space that derivative is not available without regularity of the transition law. The performance difference identity demands an exchange of an infinite series with integrals against composed kernels, and measurability of every object involved, including $TJ_\pi$, which is measurable only through the selection assumption. The stationary-implies-optimal direction must pass from an inequality weighted by $\eta_{\pi_\theta}$ to one weighted by $\rho$, and then to $\eta_{\pi^*}$, where Assumption 1 enters.

Formalization scope

$\mathcal S$ and $\mathcal A$ are arbitrary measurable spaces; the paper takes Borel subsets of Euclidean spaces, a structure no argument uses. The cost $g$ is bounded and, with the kernel $P$, defined on all of $\mathcal S\times\mathcal A$: Condition 0 differentiates at parameters near $\Theta$, where $\pi_\theta$ need not be feasible. Policies are deterministic, stationary and measurable; randomized policies are covered by taking actions to be probability vectors. $\Theta\subseteq\mathbb R^d$ is the Euclidean space, gradients are Euclidean, and $\Theta$ is convex (not assumed closed).

Conventions committed to in Lean:

• a stationary point includes differentiability of the function at that point;
• $J^*$ is never an infimum over policies: an optimal policy $\pi^*$ is a hypothesis, and $J^* = J_{\pi^*}$;
• $T$ is an infimum over $\mathcal A_s$, equal to the minimum on bounded functions;
• the Bellman operators carry the factor $\gamma$, which the printed (3)–(4) omit but every other display and proof uses;
• Condition 0 is the joint form: $(\bar\theta,\theta')\mapsto\mathcal B(\bar\theta\mid\eta_{\pi_{\theta'}},J_{\pi_\theta})$ is $C^1$ near $(\theta,\theta)$. The printed condition asks only for its two partial maps; the paper's proof of Lemma 6 expands a total derivative into partials, which needs the joint form, and the joint form implies the printed one;
• Assumptions 1 and 2 are hypotheses of the goal (standing assumptions of §2);
• Lemma 7 also carries Condition 0, which its proof uses through Lemma 6.

The goal does not assume that $\Pi_\Theta$ contains $\pi^*$, the equation of Lemma 7 or the conclusion of Lemma 8; a formalization that takes any of these as a hypothesis trivializes the theorem.

A complete development needs the composition of kernels, interchange of series and integrals for bounded functions, the fixed-point identity $T_\pi J_\pi = J_\pi$, the performance difference identity, the first-order optimality condition on a convex set, and the chain rule for a jointly $C^1$ function along the diagonal. The MDP layer, the identity (29) and the element-wise inequalities are reused by the other missions of the series. Proofs of the milestones, and proofs of the identity (29) in isolation, are welcome.

Selected references

• J. Bhandari, D. Russo, Global Optimality Guarantees for Policy Gradient Methods, Operations Research, 2024 (arXiv:1906.01786v3, 2022). https://arxiv.org/abs/1906.01786, https://doi.org/10.1287/opre.2021.0014
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML, 2002. https://dl.acm.org/doi/10.5555/645531.656005
• M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML, 2018. https://arxiv.org/abs/1801.05039
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR, 2021. https://arxiv.org/abs/1908.00261
• O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0

Motivation

An online decision maker repeatedly chooses an action, observes an outcome, and receives a reward. In a Bayesian model, an unknown parameter controls the outcomes, and the decision maker begins with a prior distribution for that parameter. Thompson sampling acts by drawing a parameter from its current posterior distribution and choosing an action that would be best if that draw were correct. This makes it applicable when an agent can simulate a plausible model and optimize an action for that model. Russo, Van Roy, Kazerouni, Osband, and Wen explain this rule for general online decision problems in Section 4 of their tutorial.

The tutorial's Section 8.1.2 asks how to analyze the rule's expected regret. An upper confidence bound method chooses an action using an optimistic score and can analyze regret through the score's optimism and its uncertainty width. Thompson sampling does not choose its actions by maximizing such a score. Yet the tutorial shows that any score computed from the observed past can be used to split Thompson sampling's expected regret into the same two types of terms. The result is stated on pp. 72–73, equation (8.4) and the display that follows.

Setting

Let $\mathcal X$ be a finite, nonempty set of actions, $Y$ a finite set of outcomes, and $\Theta$ a measurable parameter space. A prior probability measure $P$ is placed on the unknown parameter $\theta\in\Theta$. If action $x\in\mathcal X$ is selected, the outcome is sampled from a probability kernel $q_\theta(\cdot\mid x)$ on $Y$. A known function $r:Y\to\mathbb R$ turns an outcome into a reward. The mean reward of action $x$ under parameter $\theta$ is

$$\mu(x,\theta)=\sum_{y\in Y}q_\theta(y\mid x)r(y).$$

For each $\theta$, choose an action $x^*(\theta)$ maximizing $\mu(\cdot,\theta)$. This choice uses a fixed tie-break and is measurable. The same selector is used throughout the mission. A length-$t$ history $H_t$ records the first $t$ action–outcome pairs. A policy $\pi$ assigns an action distribution to every such history. The prior, the policy, and the outcome kernel together determine the law of all histories: first draw $\theta$ from $P$, then choose each action from $\pi$ using the past history, and finally generate its outcome using $q_\theta$.

After history $h$, the posterior law of $x^*$ is obtained by reweighting the prior by the likelihood of the observed outcomes. Thompson sampling draws a parameter from this posterior and plays the selected optimum for that parameter. Thus the law of its next action, given $h$, is the posterior law of $x^*$ given $h$. The policy remains defined even for a history with zero likelihood; choices there do not affect expectations.

For a period $t$, let $U_t(x)$ be any real score that uses the action $x$ and the observed history $H_{t-1}$. The score is fixed before the period's outcome or the unknown parameter can be inspected. The period regret is $\mu(x^*,\theta)-\mu(x_t,\theta)$, with expectation taken over the prior, the policy's randomization, and the outcome process.

Formalization targets

Probability matching and equation (8.4)

The first target makes posterior sampling precise. For every feasible history $h$ and action $a$, the probability that Thompson sampling next plays $a$, together with observing $h$, equals the joint probability that the selected optimum is $a$ and the history is $h$. Consequently, for every history-determined $U_t$,

$$\mathbb E_\pi[U_t(x_t)] =\mathbb E_\pi[U_t(x^*)].$$

This is equation (8.4) on p. 72. It asserts equality of unconditional expectations while preserving the fact that $U_t$ may depend on the past. It does not assert that $x_t$ and $x^*$ have the same joint law with $\theta$.

Per-period regret decomposition

The goal is the full chain of equalities displayed on p. 73:

$$\begin{aligned} \mathbb E_\pi[\mu(x^*,\theta)-\mu(x_t,\theta)] &=\mathbb E_\pi[\mu(x^*,\theta)-U_t(x_t)] +\mathbb E_\pi[U_t(x_t)-\mu(x_t,\theta)]\\ &=\underbrace{\mathbb E_\pi[\mu(x^*,\theta)-U_t(x^*)]}_{\text{pessimism}} +\underbrace{\mathbb E_\pi[U_t(x_t)-\mu(x_t,\theta)]}_{\text{width}}. \end{aligned}$$

The theorem holds for every score $U_t$ determined by the past history. In particular, $U_t$ need not be a confidence bound for the identity to hold. Being a useful upper confidence bound matters when one later estimates the two terms.

Significance

The equality permits analyses built around optimistic scores to be transferred to Thompson sampling. It separates expected regret into a term measuring whether the score falls below the true optimal mean and another measuring the gap between the score and the true mean at the sampled action. The tutorial cites Russo and Van Roy for the surrounding regret bounds; the identity here is the precise bridge used in that discussion.

The result is already proved in the tutorial. This mission seeks a machine-checked proof of its finite-action, finite-outcome form, including the posterior-sampling law, the policy-dependent history distribution, and the conditioning behind equation (8.4). The goal and milestones are open Lean statements, not completed machine-checked proofs. Their definitions can be reused in later finite Bayesian decision models with a general measurable parameter.

Difficulty

The central issue is that $x_t$ and $x^*$ are not interchangeable inside an expression that depends on $\theta$. The sampled action and the selected optimum have the same distribution after conditioning on the observed past, but generally have different dependence on the true parameter. For example, replacing $U_t$ by $\mu(\cdot,\theta)$ would make the claimed equality false. A formal proof therefore has to respect the boundary between history-derived scores and parameter-dependent quantities, and it must use the same history law to interpret every expectation. Histories of zero probability also require a consistent posterior convention.

Formalization scope

The Lean model uses finite action and outcome types and a general measurable parameter type. This is a disclosed specialization of the tutorial, which also allows infinite actions and more general outcome spaces. The kernel $q_\theta$ is nonnegative, sums to one over outcomes, and is measurable in $\theta$. The prior is a probability measure. The reward function is real valued and bounded because its domain is finite. The optimal-action selector has measurable fibers and maximizes the mean reward for every parameter. These conditions make the integrands measurable and bounded, avoiding default values of nonintegrable Lean integrals.

Histories are functions from a finite period index to action–outcome pairs. Policies are normalized, nonnegative behavioural action probabilities. The likelihood of a history multiplies both its policy action factors and its kernel outcome factors. The posterior uses only outcome likelihood factors, which give the Bayes update on every positive-evidence history. The Thompson-sampling predicate enforces the posterior action probabilities on those histories and permits any normalized policy on impossible ones. Lean period $s$ denotes the tutorial's period $t=s+1$.

The shared tie-break is essential: Thompson sampling and $x^*$ use the same selected maximizer. The score has type $H_{t-1}\to\mathcal X\to\mathbb R$, so it cannot inspect $\theta$ or the current outcome. No definition is allowed to supply regret or the decomposition as a predetermined constant; the expectation is built from the prior, policy and outcome kernel. The development needs reusable definitions for the Bayesian model, finite histories, behavioural policies, likelihoods, posterior masses, and the two regret terms. Contributions proving probability matching, equation (8.4), and the final identity are welcome.

Selected references

• Daniel J. Russo, Benjamin Van Roy, Abbas Kazerouni, Ian Osband, and Zheng Wen, A Tutorial on Thompson Sampling, Foundations and Trends in Machine Learning 11(1), 2018. DOI: 10.1561/2200000070.