All missions

Motivation

Policy gradient methods optimize a parameterized policy by gradient descent on its expected total cost. They are a staple of reinforcement learning and of simulation-based optimization in operations research, but the objective is nonconvex in the policy parameters, and the standard theory guarantees convergence only to a stationary point. J. Bhandari and D. Russo (arXiv:1906.01786v3, Operations Research, 2024, DOI 10.1287/opre.2021.0014) identify structural conditions under which every stationary point is globally optimal.

Their first result (Theorem 1) requires the policy class to be closed under policy improvement. That excludes many classes used in practice, where it is known only that some member of the class is optimal: base-stock policies in finite-horizon inventory control are the standard example (Bertsekas, Dynamic Programming and Optimal Control, 1995). For stationary policy classes, containing an optimal policy is not enough: the paper's Example 1 has a policy class that contains the optimal policy, and policy gradient still gets stuck in a bad local minimum. Theorem 3 shows that for finite-horizon problems with a non-stationary policy class (separate parameters for each period), containing an optimal policy suffices, together with a single-period regularity condition imposed only at the optimal cost-to-go. This mission formalizes Theorem 3.

Setting

A Markov decision process consists of a state space $\mathcal S$, nonempty feasible action sets $\mathcal A_s$, 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 distribution $\rho$. A policy is a measurable map $\pi$ with $\pi(s)\in\mathcal A_s$; $\Pi$ is the set of all of them. The cost-to-go is $J_\pi(s)=\mathbb E^\pi_s[\sum_{t\ge0}\gamma^t g(s_t,\pi(s_t))]$, the loss 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^tP^\pi_\rho(s_t\in\cdot)$. An optimal policy $\pi^*$ has $J_{\pi^*}\le J_\pi$ pointwise for all $\pi\in\Pi$; $J^*=J_{\pi^*}$. With the Bellman operator $(T_\pi J)(s)=g(s,\pi(s))+\gamma\int J(s')P(ds'\mid s,\pi(s))$, the weighted policy-iteration objective is

$$\mathcal B(\bar\pi\mid\eta,J)=\int (T_{\bar\pi}J)(s)\,\eta(ds).$$

A parameterized policy class is $\Pi_\Theta=\{\pi_\theta:\theta\in\Theta\}$ for a convex $\Theta\subseteq\mathbb R^d$, and $\ell(\theta)=\ell(\pi_\theta)$. A point $\theta\in\Theta$ is stationary for $\min_\Theta f$ if $f$ is differentiable at $\theta$ and $\langle\nabla f(\theta),\theta'-\theta\rangle\ge0$ for all $\theta'\in\Theta$.

The finite-horizon structure (Condition 3) embeds a time-inhomogeneous problem in this discounted formulation: the states split into stages $\mathcal S_1,\dots,\mathcal S_H,\mathcal S_{H+1}$; from a state in $\mathcal S_h$, $h\le H$, every feasible action leads to $\mathcal S_{h+1}$; and $\mathcal S_{H+1}=\{\tau\}$ is a costless absorbing state. The parameter is a concatenation $\theta=(\theta_1,\dots,\theta_H)$, the parameter set is a product $\Theta=\Theta_1\times\cdots\times\Theta_H$, and on $\mathcal S_h$ the action $\pi_\theta(s)$ depends only on $\theta_h$. The stage objectives are $\mathcal B_h(\bar\theta_h\mid\eta,J)=\int_{\mathcal S_h}(T_{\pi_{\bar\theta}}J)\,d\eta$.

Condition 4 asks that for every $\eta\in\{\eta_\pi:\pi\in\Pi_\Theta\}$, the problem $\min_{\theta\in\Theta}\mathcal B(\theta\mid\eta,J^*)$ has no suboptimal stationary points. Assumption 3 asks that $\eta_\pi\ll\rho$ for every $\pi\in\Pi_\Theta$. Condition 0 asks that the policy-iteration objective be continuously differentiable in the parameters.

Formalization targets

Goal: Theorem 3 (p. 17)

Under Conditions 0, 3 and 4 and Assumption 3, if $\pi_{\theta^*}$ is an optimal policy for some $\theta^*\in\Theta$, then every stationary point $\theta$ of $\ell$ on $\Theta$ satisfies

$$\ell(\pi_\theta)=\ell(\pi^*).$$

Milestones

1. Lemma 6 (policy gradient theorem): $\nabla\ell(\theta)=\nabla_{\bar\theta}\mathcal B(\bar\theta\mid\eta_{\pi_\theta},J_{\pi_\theta})|_{\bar\theta=\theta}$.
2. Lemma 17 (balance equation): $\eta_\pi(\mathcal M)=\int[(1-\gamma)\rho(\mathcal M)+\gamma P(\mathcal M\mid s,\pi(s))]\,\eta_\pi(ds)$.
3. The stage-wise balance equation: for $\mathcal M\subseteq\mathcal S_{h+1}$, $\eta_\pi(\mathcal M)=(1-\gamma)\rho(\mathcal M)+\gamma\int_{\mathcal S_h}P(\mathcal M\mid s,\pi(s))\,\eta_\pi(ds)$.
4. Separability (30): $\theta$ minimizes $\mathcal B(\cdot\mid\eta,J)$ over $\Theta$ iff each $\theta_h$ minimizes $\mathcal B_h(\cdot\mid\eta,J)$ over $\Theta_h$.
5. Stage-wise stationarity (31): $\theta$ is stationary for $\ell$ iff each $\theta_h$ is stationary for $\mathcal B_h(\cdot\mid\eta_{\pi_\theta},J_{\pi_\theta})$ on $\Theta_h$.
6. Lemma 1: $\pi\in\arg\min_{\Pi}\ell$ iff $J_\pi=J^*$ $\rho$-almost surely.

Significance

Theorem 3 covers finite-horizon dynamic programs in which a structured class of time-varying policies is known to contain an optimal policy, but is not closed under policy improvement: the paper's Example 8, multi-period inventory control with base-stock policies, is the motivating case. Policy gradient on such a class has no suboptimal stationary points, so any method that finds a stationary point finds a globally optimal policy, optimal among all policies and not only within the class. Condition 4 involves only the Bellman objective of the optimal cost-to-go $J^*$, which often has regularity (for instance convexity) that the cost-to-go of an arbitrary policy lacks.

The result is proved in the paper. To our knowledge no part of it, nor the policy gradient theorem for deterministic policies on general state spaces, has a machine-checked proof. Formalizing it requires a measure-theoretic treatment of occupancy measures, the stage-wise decomposition of the weighted policy-iteration objective, and the backward induction of App. D.2.

Difficulty

The obvious approach reasons stage by stage directly on $\ell$, but $\ell$ couples the stages: changing $\theta_h$ changes the distribution of states visited after stage $h$. The paper's argument instead passes through the policy gradient theorem, which turns stationarity of $\ell$ into stationarity of single-period problems weighted by the occupancy measure of the current policy. These single-period problems involve $J_{\pi_\theta}$, while Condition 4 speaks about $J^*$; relating them requires a backward induction over stages in which almost-sure equality $J_{\pi_\theta}=J^*$ on stage $h+1$ is transported to stage $h$ through the balance equation. This step needs the occupancy measures of all policies in the class, including policies other than $\pi_\theta$, to be equivalent to $\rho$, which is where Assumption 3 enters. The naive variant with a stationary policy class fails (Example 1).

Formalization scope

The state and action spaces are arbitrary measurable spaces (the paper takes Borel subsets of Euclidean spaces; no argument uses that structure). Cost and kernel are given on all state-action pairs; the cost is bounded. Policies are deterministic, stationary and measurable; parameters live in EuclideanSpace ℝ (Fin d), so gradients and norms are Euclidean. $J^*$ is never defined as an infimum: an optimal policy $\pi^*$ is a hypothesis, with $J^*=J_{\pi^*}$. Stages and sub-vectors are numbered from $1$ by a measurable stage index and a block index on coordinates; the product structure of $\Theta$ is encoded as closure under exchanging one block.

Hypotheses beyond the printed sentence of Theorem 3, all disclosed in the item statements: Assumption 3 (announced on p. 17 as required, used in the proof); Condition 0 (needed for Lemma 6, which the proof invokes), in a joint form that the proof of Lemma 6 uses and that implies the printed partial-map form; the standing Assumptions 1 and 2 of §2; and, inside Condition 4, differentiability of $\theta\mapsto\mathcal B(\theta\mid\eta,J^*)$ on $\Theta$, the premise of Definition 1. The Bellman operators carry the factor $\gamma$ omitted in the printed (3)–(4). The stage-wise balance equation is stated for $h<H$; the printed range $h\le H$ fails at the absorbing state.

A formalization in which the goal assumes the stage-wise characterization (31), the balance equation, or $J_{\pi_\theta}=J^*$ on any stage is not Theorem 3; neither is one where "contains an optimal policy" means optimal only within $\Pi_\Theta$. Stationarity includes differentiability, so a junk zero gradient never makes a point stationary.

Needed infrastructure: occupancy measures as series of iterated kernels and their balance equation, the cost-to-go as a bounded measurable function, the performance difference identity, the policy gradient theorem, and the decomposition of integrals over the stage partition. The occupancy-measure and policy gradient results are reusable for every mission of this series; contributions of these general lemmas are welcome.

Selected references

• J. Bhandari, D. Russo, Global Optimality Guarantees for Policy Gradient Methods, arXiv:1906.01786v3, 2022; Operations Research, 2024. 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
• I. Osband, B. Van Roy, D. Russo, Z. Wen, Deep Exploration via Randomized Value Functions, JMLR 20, 2019. https://jmlr.org/papers/v20/18-339.html
• D. Silver, G. Lever, N. Heess, T. Degris, D. Wierstra, M. Riedmiller, Deterministic Policy Gradient Algorithms, ICML, 2014. https://proceedings.mlr.press/v32/silver14.html
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995. https://www.athenasc.com/dpbook.html

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

Mean field games describe the limit of symmetric stochastic differential games with $n$ players as $n\to\infty$. A basic question of the theory is which mean field equilibria are limits of Nash equilibria of the $n$-player games. For closed-loop equilibria, in which each player's control may depend on the states of all players, this question was open in general until D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745, Ann. Appl. Probab. 2020). That paper shows that limits of closed-loop $\varepsilon_n$-Nash equilibria are weak mean field equilibria, a class that can be strictly larger than the classical (strong) one.

Section 7.3 of the paper gives an explicit game in which the difference is visible. It has exactly three strong equilibria (Lacker, Probab. Theory Related Fields 165, 2016, Proposition 3.6, cited as [43] in the paper) and infinitely many weak ones. The weak equilibria form a family indexed by a switching time $t_0\in[0,T]$, and for $t_0\in(0,T)$ they are not mixtures of strong equilibria (Remark 7.1). Proposition 7.2, the subject of this mission, treats $t_0=0$: the natural symmetric feedback is an $n$-player approximate Nash equilibrium, and its population mean selects the equal mixture of the two strong equilibria $m^{\pm1}$ rather than the third one, $m^0$. The selection mechanism is regularization by noise: the mean of the population solves an ill-posed ODE, and the small noise of the $n$-player system picks out a particular random solution (Trevisan, Electron. Commun. Probab. 18, 2013, cited as [57] in the paper).

Setting

Fix a horizon $T>0$. In the mean-sign game each of $n$ players controls a real state

$$X^i_t = \int_0^t \alpha^i_s\,ds + W^i_t,\qquad X^i_0=0,$$

with controls $\alpha^i_s\in A=[-1,1]$ and independent standard Brownian motions $W^1,\dots,W^n$. The mean process is $\overline\mu^n_t=\frac1n\sum_{k=1}^n X^k_t$, the mean of the empirical measure $\mu^n_t=\frac1n\sum_k\delta_{X^k_t}$. Player $i$ maximizes the expected terminal reward

$$J^n_i=\mathbb E\big[X^i_T\,\overline\mu^n_T\big],$$

that is, $b(t,x,m,a)=a$, $f\equiv0$, $g(x,m)=x\,\overline m$ with $\overline m=\int y\,m(dy)$, and initial law $\lambda=\delta_0$.

A Markovian control of player $i$ is a Borel function $\beta:[0,T]\times\mathbb R^n\to[-1,1]$ of time and the current states of all players. A profile $(\alpha^1,\dots,\alpha^n)$ is a Markovian $\varepsilon$-Nash equilibrium if no player can raise their payoff by more than $\varepsilon$ by switching to another Markovian control while the others keep theirs (Definition 2.1).

With $\operatorname{sgn}(x)=1,-1,0$ for $x>0$, $x<0$, $x=0$, the sign feedback (7.13) with $t_0=0$ is

$$\alpha^{n,i}_0(t,x_1,\dots,x_n)=\operatorname{sgn}\Big(\frac1n\sum_{k=1}^n x_k\Big)\mathbf 1_{(0,T]}(t),$$

the same for every player. Finally $H^\pm_0(t)=\pm t$ on $[0,T]$ (7.11).

Formalization targets

Goal: Proposition 7.2

For the profile $\alpha^n=(\alpha^{n,1}_0,\dots,\alpha^{n,n}_0)$:

$$\exists\,\varepsilon_n\ge0,\ \varepsilon_n\to0:\quad \alpha^n\ \text{is a Markovian }\varepsilon_n\text{-Nash equilibrium for each }n,$$ $$\mathcal L\big((\overline\mu^n_t[\alpha^n])_{t\in[0,T]}\big)\ \Longrightarrow\ \tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}\quad\text{on }C([0,T];\mathbb R).$$

The goal also asserts that the $n$-player system under $\alpha^n$ has a solution, so that the equilibrium property cannot hold vacuously.

Milestones

1. The equilibrium payoff: $J^n_1(\alpha^n)=\mathbb E[|\overline\mu^n_T|^2]\to T^2$ (proof of Proposition 7.2, p. 49).
2. Lemma 7.4, the part about the mean $Y^n$ and player 1's noise $W^1$ when player 1 deviates to a $\frac1n$-optimal control (7.15): the laws of $(Y^n,W^1)$ are tight, and every limit $(Y,W)$ has $\mathcal L(Y)=\tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}$, solves $Y_t=\int_0^t\operatorname{sgn}(Y_s)\,ds$, and has $Y$ independent of $W$.
3. The upper bound (7.14): $\limsup_n\sup_{\beta}J^n_1(\beta,\alpha^{n,2}_0,\dots,\alpha^{n,n}_0)\le T^2$.

Significance

Proposition 7.2 is a concrete instance of the paper's main theme. Theorem 2.7 says that limits of closed-loop equilibria are weak equilibria; this example exhibits explicit, symmetric, Markovian approximate equilibria whose limit is a genuinely random equilibrium (the sign of the mean is a fair coin), selected by noise among infinitely many candidates, and it identifies the limiting law of the population mean exactly. The paper states that the analogous claim for $t_0\in(0,T)$, where the limit would be a weak equilibrium that is not a mixture of strong ones, is not resolved; a formal treatment of the $t_0=0$ case makes the structure of that question precise.

Nothing of this proposition is machine-checked. Formalizing it requires weak solutions of SDEs with discontinuous drift, Nash equilibria over Markovian feedback controls, and weak convergence of laws on path space, all stated so that the junk values of Lean's total functions never enter. The objects defined here (the $n$-player game with quantified weak solutions, its payoffs and Markovian $\varepsilon$-Nash equilibria) are shared with the other missions of this series.

Difficulty

The obvious argument for $\varepsilon_n\to0$ compares player 1's payoff under a deviation with $T^2$. A deviation changes the drift of the mean only by $O(1/n)$, but the dynamics of the mean, $dY_t=\operatorname{sgn}(Y_t)dt+n^{-1/2}d\overline W_t$, is ill-posed in the limit: the ODE $\dot y=\operatorname{sgn}(y)$, $y_0=0$, has infinitely many solutions $\pm(t-s)^+$. Continuity of the solution map, the usual tool, is unavailable, and one must instead identify the limit law, which comes from the vanishing noise, and show that it is unchanged by the deviation. The second difficulty is that the payoff $X^1_TY_T$ is unbounded, so convergence of laws does not give convergence of payoffs without a uniform integrability estimate. The proof in the paper is short, but relies on a cited result on the vanishing-noise limit and on a compactness argument in a weak $L^2$ topology for the deviating controls.

Formalization scope

• Dimension and state. $d=1$; $\mathbb R^1$ is EuclideanSpace ℝ (Fin 1) (the platform's EthierKurtz.SDEState 1) and its coordinate is y 0. Controls are real, $A=[-1,1]$.
• Pathwise equations. Volatility is the identity, so the SDE of each player is stated as $X^i_t=X^i_0+\int_0^t b\,ds+W^i_t$ almost surely for all $t\in[0,T]$, with a Lebesgue integral of a bounded measurable integrand.
• Solutions are quantified. A weak solution of the $n$-player system is a structure (probability space, filtration, independent $\mathbb F$-Brownian motions, i.i.d. initial states independent of the noise, adapted path-valued states, the empirical flow). Payoffs are functions of a solution; the Nash inequality and every limit statement are required for every solution. Solutions exist and are unique in law, so this matches the paper's definitions; the goal asserts existence explicitly.
• Index shift. Term $n$ of every sequence is the $(n+1)$-player game; the factor $\frac1n$ in the controls and the mean is then $\frac1{n+1}$.
• sgn and time. $\operatorname{sgn}$ is Real.sign ($\operatorname{sgn}0=0$), and the control vanishes at $t=0$, both as printed.
• Unbounded payoff. Assumption A fails ($g$ is unbounded) and is not assumed anywhere. Payoffs are Bochner integrals; $X^i_T\overline\mu^n_T$ is integrable on every solution (bounded drift, $X^i_0=0$), which is a fact to be proved rather than an assumption.
• Laws. Laws on $C([0,T];\mathbb R)$ carry the topology of weak convergence; the mean path is a continuous function of the state paths, so its law is a probability measure by construction.
• Lemma 7.4. Only the $(Y,W)$ coordinates are stated: tightness, (i), the equation for $Y$ in (ii), and (iv). The coordinates $X$ and $\beta$, which need the weak topology of $L^2([0,T];[-1,1])$, and item (iii) are not stated; the norm topology must not be substituted, because the deviating controls are not tight in it.
• Ruled out. A statement in which the profiles have no solutions would make the Nash clause vacuous; the existence clause of the goal excludes it.

Contributions welcome: the existence of weak solutions for bounded measurable Markovian drifts, the vanishing-noise limit of $dZ=\operatorname{sgn}(Z)dt+\epsilon\,dW$, and Girsanov-type change-of-measure estimates are all reusable beyond this mission.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, Ann. Appl. Probab. 30(4), 2020; arXiv:1808.02745v1, 2018. https://arxiv.org/abs/1808.02745
• D. Lacker, A general characterization of the mean field limit for stochastic differential games, Probab. Theory Related Fields 165(3–4), 581–648, 2016 (reference [43] of the paper).
• D. Trevisan, Zero noise limits using local times, Electron. Commun. Probab. 18, 2013 (reference [57] of the paper).
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://arxiv.org/abs/1307.1152

Motivation

A directed polymer in random environment is a random walk path reweighted by a random potential that is refreshed at every time step. It is a basic model of a one-dimensional object (a polymer, an interface, a flux line) pinned by impurities, and a discrete version of the KPZ universality class in dimension $1+1$. A central question is localization: whether the walk's endpoint at time $n$, under the random Gibbs measure, concentrates on a few sites or spreads out like a simple random walk.

For a fixed disorder law there is a critical inverse temperature $\beta_c$ (Comets–Yoshida, Ann. Probab. 2006). In the low-temperature phase $\beta>\beta_c$ the endpoint has atoms of positive mass, in the Cesàro sense, at a positive fraction of times (Carmona–Hu 2002, Comets–Shiga–Yoshida 2003); in the high-temperature phase it does not. Atoms alone say nothing about geometry: the mass could sit on a few sites that are far apart. Bates and Chatterjee (arXiv:1612.03443v5, Ann. Probab. 2020) prove that in the low-temperature phase the mass also sits on a region of bounded diameter at a positive fraction of times, in every dimension and for every disorder law with exponential moments. Before this, geometric localization was known only for the integrable log-gamma polymer in $1+1$ dimensions (Comets–Nguyen 2016).

Setting

Fix $d\ge1$. Let $(X_u)_{u\in\mathbb N\times\mathbb Z^d}$ be i.i.d. real random variables with law $\mathfrak L$, not supported on a single point, such that $\lambda(\alpha)=\log\mathbf E\,e^{\alpha X_u}<\infty$ for $\alpha\in[-2\beta,2\beta]$ (assumption (1.1)), where $\beta\ge0$ is the inverse temperature. For a nearest-neighbour path $\gamma$ of length $n$ from the origin, its weight is $\exp(\beta\sum_{i=1}^n X_{i,\gamma(i)})$. The endpoint distribution $f_n(x)=\rho_n(\omega_n=x)$ is the total weight of paths ending at $x$ divided by the total weight of all $(2d)^n$ paths. The partition function is $Z_n=(2d)^{-n}\sum_\gamma\exp(\beta\sum_{i=1}^nX_{i,\gamma(i)})$ and the free energy is $F_n=\frac1n\log Z_n$. The limit $p(\beta)=\lim\mathbf E F_n$ exists, and $\beta_c$ is characterised by $p(\beta)=\lambda(\beta)$ for $0\le\beta\le\beta_c$ and $p(\beta)<\lambda(\beta)$ for $\beta>\beta_c$.

For $\delta>0$ and $K\ge0$ let $\mathcal G_{\delta,K}$ be the set of probability mass functions on $\mathbb Z^d$ that give mass greater than $1-\delta$ to some set $D$ with $\operatorname{diam}(D)=\sup_{x,y\in D}\|x-y\|_1\le K$.

The proofs work on the space $\mathcal S$ of partitioned subprobability measures: functions $f\ge0$ on $\mathbb N\times\mathbb Z^d$ with $\sum f\le1$, modulo translations of each copy of $\mathbb Z^d$, with a metric $d$ that makes $\mathcal S$ compact. The update $f_n\mapsto f_{n+1}$ induces a Markov kernel $\mathcal T$ on $\mathcal S$; $\mathcal K$ is its set of invariant probability measures and $\mathcal M\subset\mathcal K$ the minimisers of a free-energy functional $\mathcal R$. On $\mathcal S$ the mission uses the functionals $\max(f)=\max_uf(u)$, the support number $N(f)$ (number of copies carrying mass), $W_\delta(f)$ (the least diameter of a region of one copy with mass $>1-\delta$), $m(f)=\max_nq_n(f)$ and $Q(f)=\sum_nq_n(f)/(1-q_n(f))$, where $q_n(f)$ is the mass of copy $n$.

Formalization targets

Goal: Theorem 1.2 (= Theorem 7.3(a),(c))

If $\beta>\beta_c$, then for every $\delta>0$ there are $K<\infty$ and $\theta>0$, depending only on $\delta,\mathfrak L,\beta,d$, such that

$$\liminf_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}\ge\theta\quad\text{a.s.}$$

If $0\le\beta\le\beta_c$, then for every $K$ and every $\delta\in(0,1)$,

$$\lim_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}=0\quad\text{a.s.}$$

The goal fixes no constants: $K$ and $\theta$ are only asserted to exist.

Milestones

1. Lemma 5.4: $\max$ is continuous on $\mathcal S$.
2. Theorem 5.3: the Cesàro average of $\max_xf_i(x)$ tends to $0$ a.s. at high temperature and has $\liminf\ge c>0$ a.s. at low temperature.
3. Lemma 7.1: $W_\delta$ is upper semicontinuous; $m$ and $Q$ are lower semicontinuous.
4. Lemma 7.2: at low temperature $\int Q\,d\nu=\infty$ for every $\nu\in\mathcal M$.
5. Theorem 7.3(b): under the single-copy condition $\nu(N=1)=1$ for all $\nu\in\mathcal M$ (7.4), localization holds with full density $\theta\ge1-\delta$.
6. Proposition 7.4: under (7.4), $\lim_{K\to\infty}\liminf_n\frac1n\sum_{i<n}\rho_i(\omega_i\in\mathcal C_i^K)=1$ a.s., where $\mathcal C_i^K$ is the set of sites within distance $K$ of every mode of $f_i$.

Significance

The theorem shows that the low-temperature phase is detected by the shape of the endpoint distribution, not only by its largest atom: positive-density geometric localization holds if and only if $\beta>\beta_c$. The determinism of $K$ and $\theta$ makes the statement uniform over all environments with the given law. The conditional results 5 and 6 reduce full-density and favourite-region localization to a single property of the limit set $\mathcal M$, which is open.

The result is proved on paper; nothing in it is machine-checked. A formalization would produce a checked development of the compact space $\mathcal S$, of the Markov kernel $\mathcal T$, and of the variational characterisation of the free energy, which also underlies the companion mission on asymptotic pure atomicity of the same paper.

Difficulty

The obvious approach, tracking $f_n$ in $\ell^1(\mathbb Z^d)$, fails because mass escapes to infinity: the sequence $(f_n)$ has no convergent subsequence in any space of probability measures on $\mathbb Z^d$. The paper's compactification keeps pieces of mass that drift apart as separate copies, so a limit point can split one copy's mass over several. The semicontinuity of $W_\delta$, $m$ and $Q$ (Lemma 7.1) only goes one way for this reason, and positivity of the localized fraction needs the separate identity of Lemma 7.2, which uses strict convexity and the non-degeneracy of $\mathfrak L$. Theorem 5.3 already requires the full variational machinery of §4 (convergence of empirical measures to $\mathcal M$), which is the companion mission's subject.

Formalization scope

Points are $\mathbb Z^d=$ Fin d → ℤ, cells are ℕ × (Fin d → ℤ), and paths are sequences of $n$ signed coordinate steps. The environment is a family of independent measurable random variables, each with law $\mathfrak L$, on an arbitrary probability space. The phases are encoded through Theorem A as $\lim\mathbf E F_n<\lambda(\beta)$ ($\beta>\beta_c$) and $\lim\mathbf EF_n=\lambda(\beta)$ ($0\le\beta\le\beta_c$), with $\mathbf EF_n$ computed under the canonical product environment. Elements of $\mathcal S$ are represented by their representatives, with the topology generated by $d$-balls (no quotient). In the goal, $K$ and $\theta$ are chosen before the probability space. Part (a) is stated for all $\delta>0$ and part (c) for $\delta\in(0,1)$, as printed.

Trivializing encodings are ruled out: $\mathcal G_{\delta,K}$ requires total mass exactly $1$; $W_\delta$ and $N$ take values in $\mathbb N\cup\{\infty\}$ so that an empty infimum is $\infty$; $Q$ is computed in $[0,\infty]$ so that $1/0=\infty$; the sum in $\widetilde F$ is taken in $[0,\infty]$; $\mathcal M$ avoids a real infimum over $\mathcal K$; $\mathfrak L$ is non-degenerate; and the phase hypotheses are limits that exist.

A complete development needs: the metric space $(\mathcal S,d)$ and its compactness, the measurability and continuity of $\mathcal T$, the Wasserstein space $\mathcal P(\mathcal S)$ (here through the published RWPI.SqrtLasso.transportCost), and the convergence $\mathcal W(\mu_n,\mathcal M)\to0$ (Theorem 4.9) together with $\mathcal M=\{\delta_0\}$ at high temperature (Theorem 5.2), both posed in the companion mission. Contributions to any milestone, and to the shared infrastructure of $\mathcal S$, are welcome.

Selected references

• E. Bates, S. Chatterjee, The endpoint distribution of directed polymers, Ann. Probab. 48 (2020); arXiv:1612.03443v5. https://arxiv.org/abs/1612.03443
• F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006). https://doi.org/10.1214/009117905000000828
• F. Comets, T. Shiga, N. Yoshida, Directed polymers in a random environment: path localization and strong disorder, Bernoulli 9 (2003). https://doi.org/10.3150/bj/1065444233
• P. Carmona, Y. Hu, On the partition function of a directed polymer in a Gaussian random environment, Probab. Theory Related Fields 124 (2002). https://doi.org/10.1007/s004400200213
• F. Comets, V.-L. Nguyen, Localization in log-gamma polymers with boundaries, Probab. Theory Related Fields 166 (2016). https://doi.org/10.1007/s00440-015-0662-4
• F. Comets, Directed Polymers in Random Environments, Lecture Notes in Math. 2175, Springer (2017). https://doi.org/10.1007/978-3-319-50487-2

Why relate heat flow and curvature?

Heat flow gives an analytic way to describe how functions spread on a space. Optimal transport gives a metric way to describe how probability measures move on the same space. On a smooth Riemannian manifold, a lower Ricci curvature bound constrains both motions. The problem addressed by Ambrosio, Gigli and Savaré is to identify the corresponding relationship when the underlying space need not be a manifold. A Dirichlet form can specify a heat flow even when there are no smooth coordinates, while a Wasserstein distance can measure transport between probability measures. Theorem 4.17 connects these two descriptions for Riemannian energy measure spaces.

The paper proves the implication from the Bakry–Émery condition $BE(K,\infty)$ to the Riemannian curvature-dimension condition $RCD(K,\infty)$. Its printed theorem is an equivalence; the paper cites the reverse implication from earlier work in the proof on p. 58. This mission targets the implication established here, with the source's exact assumptions.

Setting

Let $X$ be a complete, separable metric space with a Borel measure $m$. A Dirichlet form $\mathcal E$ assigns a nonnegative energy to square-integrable functions, is quadratic and lower semicontinuous, and decreases under normal contractions. Its associated heat flow $P_t$ evolves a function over time. The associated carré du champ $\Gamma(f)$ measures the energy density of a function. Functions with energy density at most one define an intrinsic distance

$$d_{\mathcal E}(x,y)=\sup\{|\psi(y)-\psi(x)|:\psi\text{ is continuous and }\Gamma(\psi)\le1\ m\text{-a.e.}\}.$$

For the Riemannian energy measure space in this mission, this intrinsic distance is the metric of $X$. The structure also requires the paper's upper regularity and continuous-representative properties. The growth condition $(MD.exp)$ controls the measure of large balls. In the $BE(K,\infty)$ condition, a weak second-derivative inequality for the heat flow has curvature parameter $K$ and no finite-dimensional correction term. These assumptions are stated at the start of §4 and govern the §4 milestones even when an individual theorem does not repeat them. See Definitions 3.6 and 3.16 and the opening of §4.

Write $\mathcal P_2(X)$ for the probability measures with finite second moment, $W_2$ for their quadratic Wasserstein distance, and $\operatorname{Ent}_m(\rho)$ for entropy relative to $m$. The heat flow has a dual action $H_t$ on measures. The target $RCD(K,\infty)$ asks for a curve $H_t\rho$ from every $\rho\in\mathcal P_2(X)$ that satisfies the following evolution variational inequality against every $\nu\in\mathcal P_2(X)$ of finite entropy, at every $t>0$:

$$\frac{d^+}{dt}\frac{W_2^2(H_t\rho,\nu)}2 +\frac K2W_2^2(H_t\rho,\nu) +\operatorname{Ent}_m(H_t\rho) \le\operatorname{Ent}_m(\nu).$$

The definition also includes full support, local finiteness, the exponential growth condition, and the length-space property. See Definition 3.1.

Formalization targets

The goal is the forward implication of Theorem 4.17:

$$\text{Riemannian energy measure space}+(MD.exp)+BE(K,\infty) \quad\Longrightarrow\quad RCD(K,\infty).$$

Three milestones supply central results from the paper. The final assertions of Theorem 3.17 give the dual measure flow and its absolute continuity after positive time. Corollary 3.18 identifies $BE(K,\infty)$ with the $W_2$ contraction $W_2((P_t f)m,(P_t g)m)\le e^{-Kt}W_2(fm,gm)$ on probability densities. A companion item, Theorem 4.8, gives an entropy bound for $H_t\mu$ when $\mu$ has finite second moment:

$$\operatorname{Ent}_m(H_t\mu) \le\frac{r^2+\int_X d^2(x,x_0)\,d\mu(x)}{2I_{2K}(t)} -\log m(B_r(x_0)),\qquad r,t>0.$$

The third milestone, Theorem 4.16, bounds the distance and entropy at the heat-evolved endpoint of a regular curve $\rho_s$:

$$W_2^2(\rho_0,H_t\rho_1)+2t\operatorname{Ent}_m(H_t\rho_1) \le R_K(t)^2\int_0^1|\dot\rho_s|^2\,ds +2t\operatorname{Ent}_m(\rho_0),\qquad R_K(t)=t/I_K(t).$$

The milestone list follows the source labels and constants in §4.

What the result provides

The conclusion turns an analytic curvature bound on a heat semigroup into a transport statement about entropy on probability measures. It therefore identifies a concrete set of Dirichlet-form hypotheses under which the heat evolution has the metric behavior demanded by $RCD(K,\infty)$. The result applies in the paper's metric measure setting, where the space may lack a smooth tensor calculus. The $RCD$ conclusion carries convergence from every initial measure in $\mathcal P_2(X)$ and the inequality for all finite-entropy comparison measures.

The mathematical implication is proved in the cited paper. The proposed Lean statements are open proof targets: their declarations compile with placeholders, and no machine-checked proof of this implication is asserted here. A complete development would connect Dirichlet-form calculus, probability measures, entropy, and Wasserstein geometry in reusable interfaces. The dual-flow and regular-curve definitions are especially useful beyond this theorem.

Main difficulty

The heat flow is initially specified on square-integrable functions, whereas the target is an inequality for probability measures, including measures without an initial density. A bound on $\Gamma(P_t f)$ by itself controls functions almost everywhere; it does not immediately produce the pointwise dual flow or the right derivative of $W_2^2$ required by Definition 3.1. The action estimate also begins with regular curves, while the target quantifies over every initial measure in $\mathcal P_2(X)$. These changes of domain and regularity are the central mathematical obstacles; simply renaming the heat semigroup as a measure flow leaves the target unjustified.

Formalization scope

Lean uses real-valued function representatives for $L^2(X,m)$, with almost-everywhere congruence in the Dirichlet form and heat flow. Measures use the Borel sigma algebra. The source uses its $m$-completion; the formalization treats quantities invariant under $m$-almost-everywhere equality, and this convention is explicit in the definition layer. The metric is complete and second countable, and its equality with $d_{\mathcal E}$ is part of the energy-measure-space predicate. A sigma-finiteness instance is carried where entropy or measure operations need it; it follows from the source's measure-growth setting. The dual flow and the $L^1$ extension are bound by predicates that specify their action on densities. The mollifier for a regular curve is bound by the conditions of (2.17), while the action is the infimum of squared admissible speeds, which equals the integral of the squared metric derivative.

Wasserstein costs use $\mathbb R_{\ge0}\cup\{\infty\}$, and entropy uses extended real values. Theorem 4.8 restricts $r,t$ to positive numbers, so the ball mass and $I_{2K}(t)$ used in its formula have the intended domain. Theorem 4.16 also uses $t>0$, making $R_K(t)=t/I_K(t)$ meaningful, including at $K=0$. The goal requires an EVI flow beginning at each $\rho\in\mathcal P_2(X)$ and the inequality at every positive time; allowing a vacuous flow or checking only almost every time would not express Definition 3.1. Contributions may establish the milestone statements and the companion Theorem 4.8, develop the omitted intermediate estimates from §4, or prove the goal from the source's full argument.

Selected references

• L. Ambrosio, N. Gigli and G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Annals of Probability 43(1), 2015, 339–404. arXiv:1209.5786v4.

Motivation

Mean field games (Lasry–Lions 2006, Huang–Malhamé–Caines 2006) describe Nash equilibria of stochastic differential games with very many symmetric players. In this description each player interacts with the others only through the empirical distribution of their states. The mean field game is meant to be the limit of the $n$-player games as $n\to\infty$. Making that link rigorous has two halves:

• a limit theorem: every limit of $n$-player equilibria is a mean field equilibrium;
• a converse: every mean field equilibrium is the limit of $n$-player approximate equilibria.

For closed-loop equilibria, where players react to the observed states of all others, both halves are harder than for open-loop equilibria. A single player's deviation changes the feedback of the whole system.

This mission covers the converse half of D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020).

Timeline.

• Carmona–Delarue (2013) and Huang–Malhamé–Caines constructed $\epsilon_n$-Nash equilibria from mean field equilibria, under Lipschitz or linear-quadratic structure, with continuous feedbacks.
• Cardaliaguet–Delarue–Lasry–Lions (2015, arXiv:1509.02505) obtained such a converse implicitly from a smooth master equation.
• Lacker (2018) proved the converse for every strong mean field equilibrium. His hypotheses are bounded continuous coefficients and a drift that is Lipschitz in total variation, and the feedback may be discontinuous. The key input is a propagation-of-chaos result in total variation (Lacker, On a strong form of propagation of chaos for McKean–Vlasov equations, arXiv:1805.04476).

Setting

Fix a horizon $T>0$, a compact convex action set $A$ in a real normed space, an initial law $\lambda\in\mathcal P(\mathbb R^d)$ and coefficients

$$b:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R^d,\quad f:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R,\quad g:\mathbb R^d\times\mathcal P(\mathbb R^d)\to\mathbb R .$$

The $n$-player game.

• A Markovian control is a Borel map $\alpha:[0,T]\times(\mathbb R^d)^n\to A$.
• Under a profile $\alpha=(\alpha^1,\dots,\alpha^n)$ the states solve

$$dX^i_t=b\big(t,X^i_t,\mu^n_t,\alpha^i(t,X_t)\big)dt+dW^i_t,\qquad \mu^n_t=\tfrac1n\textstyle\sum_{k}\delta_{X^k_t},$$

with independent Brownian motions $W^i$ and i.i.d. initial states of law $\lambda$.

• Player $i$ receives $J^n_i(\alpha)=\mathbb E\big[\int_0^Tf(t,X^i_t,\mu^n_t,\alpha^i(t,X_t))dt+g(X^i_T,\mu^n_T)\big]$.
• The profile is a Markovian $\epsilon$-Nash equilibrium if no player gains more than $\epsilon$ by switching to another Markovian control.
• Relaxed controls take values in $\mathcal P(A)$ and average $b$ and $f$ against them.

The mean field game. A flow $m\in C([0,T];\mathcal P(\mathbb R^d))$ is a strong MFE if some Borel feedback $\alpha^*:[0,T]\times\mathbb R^d\to A$ satisfies two conditions:

• the state $dX^*_t=b(t,X^*_t,m_t,\alpha^*(t,X^*_t))dt+dW_t$, $X^*_0\sim\lambda$, has law $m_t$ at every time;
• $\alpha^*$ maximizes $\mathbb E[\int_0^Tf(t,X_t,m_t,\alpha(t,X_t))dt+g(X_T,m_T)]$ among all Borel feedbacks $\alpha$.

A strong RMFE is the relaxed analogue.

The assumptions are:

• Assumption A: $A$ compact convex; $b,f,g$ bounded and jointly continuous.
• Assumption B: the sets $\{(b(t,x,m,a),z):a\in A,\ z\le f(t,x,m,a)\}$ are convex.
• Assumption C: $|b(t,x,m,a)-b(t,x,m',a)|\le c\,\|m-m'\|_{TV}$, with $\|m-m'\|_{TV}=\sup_{|\varphi|\le1}\int\varphi\,d(m-m')$.

Formalization targets

Goal: Theorem 2.11

Under Assumptions A, B and C, if $m$ is a strong MFE, there are two families of objects:

• numbers $\epsilon_n\ge0$ with $\epsilon_n\to0$;
• for each $n$, Markovian $\epsilon_n$-Nash equilibria $\alpha^n$;

such that

$$\mu^n[\alpha^n]\ \xrightarrow{\ \text{law}\ }\ m\quad\text{in }C([0,T];\mathcal P(\mathbb R^d)).$$

The goal asserts no rate, so any quantitative improvement still implies it.

Milestones

• Proposition 3.7 (strong part): under A and B, strong MFE and strong RMFE are the same flows.
• Theorem 2.14 (Markovian projection): a drift process can be replaced by a Markovian drift $\hat b(t,x)=\mathbb E[b_t\mid X_t=x]$ with the same one-dimensional marginals.
• (7.2): for the symmetric profile $\Lambda^{n,i}(t,x)=\Lambda^*(t,x^i)$, $\mu^n\to m$ in law and $\int\varphi\,d\mu^n_t\to\int\varphi\,dm_t$ in probability for bounded measurable $\varphi$.
• $\nu^n\to m$ (§7.1, p. 45): after one player deviates, the empirical flow still converges to $m$ in probability.
• Theorem 3.10: the relaxed converse, under A and C only.
• Proposition 3.4(a): under A and B, a relaxed Markovian $\epsilon$-Nash equilibrium can be replaced by a strict one with the same state law.

Significance

The result. Theorem 2.11 says that the strong MFE is a faithful idealization: every classical mean field equilibrium is approximately realized by Markovian feedback equilibria of large finite games. No continuity of the equilibrium feedback and no master equation are required. Together with the paper's main limit theorem (mission 1 of this series), it locates strong MFE inside the set of limits of closed-loop equilibria. The paper's Section 2.4 explains why the same converse is open for weak MFE.

Formalizing it. The result is proved on paper but has no machine-checked proof. A complete development would produce several reusable pieces:

• pathwise formulations of SDEs with bounded measurable drift;
• the Markovian projection theorem;
• total-variation propagation of chaos;
• relaxed-control purification by measurable selection.

None of these is in Mathlib.

Difficulty

The obvious argument has every player use $\alpha^*(t,X^i_t)$, invokes the McKean–Vlasov limit, and passes optimality to the limit. It fails at two places:

• Discontinuous feedback. $\alpha^*$ is only measurable, so weak convergence of $\mu^n$ does not give convergence of payoffs. Convergence in probability of $\int\varphi\,d\mu^n_t$ for discontinuous $\varphi$ is needed, and that is exactly what the total-variation Lipschitz Assumption C provides.
• Arbitrary deviations. A deviating player's control $\beta^n$ is arbitrary and depends on all $n$ states. Its limit is a relaxed, non-Markovian control. Comparing it with the mean field optimum requires a projection back onto Markovian feedbacks, without losing the marginal laws.

Formalization scope

Representation.

• States live in EuclideanSpace ℝ (Fin d).
• $\mathcal P(\cdot)$ is Mathlib's ProbabilityMeasure with the weak topology and the Borel $\sigma$-field.
• Paths and flows are continuous maps on Set.Icc 0 T with the compact-open (uniform) topology.
• Unit volatility makes every SDE a pathwise integral equation $X_t=X_0+\int_0^t(\text{drift})ds+W_t$ a.s., with no stochastic integral.
• Solutions are quantified, not chosen. Payoffs are functions of a solution, and every equilibrium inequality, consistency condition and convergence statement is required for every solution. This equals the paper's definitions because solutions exist and are unique in law (Girsanov; Veretennikov; Krylov–Röckner).
• The game with $n+1$ players is indexed by $n$.

Committed choices.

• The paper's consistency condition "$m_t=\mathcal L(X_t)$" is read as $\mathcal L(X^*_t)$.
• "Strong RFME" in Proposition 3.7 is read as strong RMFE.
• Theorem 2.14's "unique strong solution" is a strong solution adapted to the completed filtration of $(X_0,W)$; its existence is part of the conclusion.
• The $\nu^n$ milestone is stated for arbitrary relaxed Markovian deviations, which include the paper's near-optimal ones.
• Coefficients and controls are defined at all real times; only $[0,T]$ matters.

Ruled out. Because equilibria quantify over solutions, a profile whose state system has no solution would be an equilibrium vacuously. For this reason every existence conclusion (the goal, Theorem 3.10, Proposition 3.4(a)) also asserts that the chosen profiles have solutions, and strong (R)MFE requires the equilibrium SDE to have one.

Infrastructure. A complete proof needs Girsanov's theorem, strong existence for SDEs with bounded measurable drift, measurable selection, tightness on path space, and total-variation propagation of chaos. Each is reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.4(b), the weak half of Proposition 3.7, and Theorem 2.7 are outside this mission.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020. https://arxiv.org/abs/1808.02745
• D. Lacker, On a strong form of propagation of chaos for McKean–Vlasov equations, Electron. Commun. Probab. 23, 2018. https://arxiv.org/abs/1805.04476
• I. Gyöngy, Mimicking the one-dimensional marginal distributions of processes having an Itô differential, Probab. Theory Related Fields 71, 1986. https://doi.org/10.1007/BF00699039
• G. Brunick, S. Shreve, Mimicking an Itô process by a solution of a stochastic differential equation, Ann. Appl. Probab. 23(4), 2013. https://arxiv.org/abs/1011.0111
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://arxiv.org/abs/1210.5780
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The master equation and the convergence problem in mean field games, Annals of Math. Studies 201, 2019. https://arxiv.org/abs/1509.02505
• A. Yu. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR Sb. 39, 1981. https://doi.org/10.1070/SM1981v039n03ABEH001518

Why this phase transition matters

Sparse recovery asks when a vector with few nonzero coordinates can be reconstructed from fewer linear measurements than unknowns. A related geometric question asks how many faces of a high-dimensional cross-polytope survive a random linear projection. The two questions meet at the same threshold: uniqueness of a minimum-one-norm solution corresponds to a face of the projected cross-polytope. For Gaussian measurement matrices this threshold was known before the work of Bayati, Lelarge and Montanari, from Donoho's face-counting analysis (Donoho 2006); the same curve was later identified as the transition of approximate message passing (Donoho, Maleki and Montanari 2009). Their 2015 paper establishes the same weak-neighborliness curve for a broader class of independent sub-Gaussian entries with a nonzero Gaussian component. The result addresses the universality question posed for these projections: does the asymptotic transition depend on the full entry distribution or only on broad features of the matrix law?

The mathematical theorem is established in that paper. This mission records its statement in Lean and leaves the machine-checked proof open. The relevant statement is Theorem 2 on page 5 of the pinned arXiv version 2, rather than a claim about every random projection without a Gaussian component.

Polytopes, faces, and random matrices

The cross-polytope $C_n$ is the unit ball for the coordinate one-norm in $\mathbb R^n$:

$$C_n=\left\{x\in\mathbb R^n:\sum_{i=1}^n|x_i|\leq1\right\}.$$

For an $m\times n$ matrix $A$, the projected polytope $AC_n$ consists of all $Ax$ with $x\in C_n$. Write $F(Q;\ell)$ for the number of nonempty faces of $Q$ whose affine dimension is $\lfloor\ell\rfloor$. The weak neighborliness level $\rho\in(0,1)$ of a random sequence $Q_n\subseteq\mathbb R^{m(n)}$ means that, for every $\xi>0$, the ratio $F(Q_n;m(n)\rho(1-\xi))/F(C_n;m(n)\rho(1-\xi))$ converges in probability to one, while the analogous ratio with $1+\xi$ converges in probability to zero. Both limits belong to the definition; the first alone would record only survival below a candidate threshold.

The matrices have $m(n)=\lfloor n\delta\rfloor$ rows for a fixed sampling ratio $\delta\in(0,1)$. Within each matrix, the entries are independent, centered, unit-variance, and sub-Gaussian with one scale factor independent of $n$. They also admit a decomposition $A(n)=\widetilde A(n)+\nu_0G(n)$, where $\nu_0>0$ and the entries of $G(n)$ are independent standard normal variables, jointly independent of $\widetilde A(n)$. The theorem imposes no independence between matrices with different values of $n$ Bayati–Lelarge–Montanari, Theorem 2.

Formalization targets

Let $\phi$ and $\Phi$ be the density and distribution function of a standard normal random variable. The paper defines its phase boundary through a positive parameter $\alpha$:

$$f_\delta(\alpha)=\frac{2\phi(\alpha)}{\alpha+2\bigl(\phi(\alpha)-\alpha\Phi(-\alpha)\bigr)},\qquad f_\rho(\alpha)=1-\frac{\alpha\Phi(-\alpha)}{\phi(\alpha)}.$$

Footnote 3 states that $f_\delta$ decreases from one to zero on the nonnegative half-line, so each $\delta\in(0,1)$ has exactly one positive parameter. The goal, Theorem 2, says that whenever $f_\delta(\alpha)=\delta$, the sequence $A(n)C_n$ has weak neighborliness $f_\rho(\alpha)$ in probability. The Lean theorem spells out this parameter relation; it does not apply an inverse function at an argument outside a proved range.

The milestone list covers the two scalar results identifying the boundary, a deterministic condition for exact recovery, and the compressed-sensing transition. With $Z$ standard normal and $u_+=\max(u,0)$, the scalar function is

$$G_\varepsilon(\alpha)=\varepsilon(1+\alpha^2)+2(1-\varepsilon)\mathbb E[(Z-\alpha)_+^2].$$

Lemma 8 gives its unique positive minimizer and its minimum value. Lemma 9 relates that minimum to both sides of the boundary. The scalar state evolution $\sigma_{t+1}^2=\mathsf F(\sigma_t^2,\alpha\sigma_t)$, with $\mathsf F(\sigma^2,\theta)=\delta^{-1}\mathbb E\{[\eta(X+\sigma Z;\theta)-X]^2\}$ and $\eta(u;\theta)=\operatorname{sign}(u)(|u|-\theta)_+$ soft thresholding, has slope $G_\varepsilon(\alpha)/\delta$ at the origin and is concave (Lemma 7). Lemma 10 shows that a two-time correlation map $\mathcal F_{\alpha,\varepsilon}$ satisfies $\mathcal F_{\alpha,\varepsilon}(Q)>Q$ on $[0,1)$. Theorem 10, cited from Bürgisser and Cucker, bounds the probability that a Gaussian-perturbed rectangular matrix has a small least singular value:

$$\mathbb P\{\sigma_N(B+\nu G)\le\nu z\}\le(a_1z)^{M-N+1}.$$

Lemma 5 gives a recovery condition based on an approximate dual certificate and singular-value bounds. Theorem 8 states that minimum-one-norm recovery succeeds with probability tending to one below the boundary and fails with probability tending to one above it Bayati–Lelarge–Montanari, pp. 39–41, 60–61.

What a formal proof would establish

The goal would certify that the same face-count transition applies to every entry law in the stated class, including laws that are not identically distributed across the matrix. The conclusion is geometric: it counts faces of an actual projected one-norm ball. The recovery milestone provides a second way to state the threshold for sparse signals. Together they make the normalization and the two sides of the transition explicit, so future variants can compare their assumptions and conclusions with a fixed formal statement.

No machine-checked proof of Theorem 2 or of the selected milestones is known. The declarations are open Lean statements over explicit definitions. A complete development would formalize the known argument in the paper, including the probabilistic estimates and the bridge from recovery probabilities to face counts. Sharper results that remove the Gaussian component would be separate theorems with their own hypotheses.

Where the difficulty lies

The count of surviving faces depends on many supports and sign patterns simultaneously. Matching means and variances of matrix entries does not make their finite-dimensional face counts equal. Likewise, controlling recovery for one fixed signal does not immediately control the fraction of all faces. Near the boundary, exact recovery also requires uniform singular-value information for many column submatrices. These are the points where elementary concentration for a single entry or a single support is insufficient. The source paper treats the geometric statement and the recovery transition under a Gaussian-component condition; a proof that silently assumes full Gaussianity would miss its universality claim.

Formalization scope

Vectors are functions on Fin n, and every one-norm is an explicit sum of absolute values. The squared Euclidean norm is a sum of coordinate squares; the default norm on Fin n → ℝ is not used for it. Face counts reuse the published Grunbaum2003.faceCount definition, with dimension $\lfloor\ell\rfloor$ for nonnegative $\ell$; negative dimensions have zero nonempty faces. The two limits in weak neighborliness use convergence in measure, which expresses convergence in probability here. The printed lower ratio has a zero denominator for $\xi>1$, so that limit is stated for $0<\xi\leq1$. Ratios at small $n$ may involve zero denominators, but the asymptotic assertion concerns arbitrarily large $n$.

Theorem 2 uses variance one and an $N(0,1)$ Gaussian component. Theorem 8 instead uses variance $1/m(n)$ and an $N(0,1/m(n))$ component, exactly as printed. Sub-Gaussianity uses Mathlib's moment-generating-function predicate for all real parameters; this is the operative two-sided reading of the paper's stated scale condition. The scalar Gaussian expectation in $G_\varepsilon$ is accompanied by an explicit integrability conclusion in Lemma 8, excluding Lean's zero value for a nonintegrable integral. The restricted least singular value is the infimum of output norms on unit column vectors. This gives zero when a wide submatrix has a kernel and is the bound needed by Lemma 5. The state-evolution map is written as a function of $\sigma^2$, and its derivative at $0$ is a right derivative. In Lemma 10 the law of $X_\infty$ is the three-atom mixture on $\{0,+\infty,-\infty\}$, with the split of the mass $\varepsilon$ between the two infinite atoms left free. The page's clause $\mathcal F'_{\alpha,\varepsilon}(1)<1$ is stated for $\alpha>\alpha_*(\varepsilon)$, since the derivative equals $1$ at $\alpha=\alpha_*$. Theorem 10 quantifies $\nu>0$ and $z>0$, which the page leaves implicit.

The random-matrix predicates require measurability, independence within each $n$, the stated marginal laws, and independence of $G(n)$ from $\widetilde A(n)$. They leave the matrix law otherwise arbitrary. The weak-neighborliness predicate contains both face-ratio limits and $0<\rho<1$; neither the goal nor a milestone defines the threshold by assuming its conclusion. A full proof needs reusable facts about Gaussian integrals, independence of finite arrays, random face counts, restricted singular values, and the relation between projected faces and unique one-norm recovery. Contributions establishing those facts or closing any of the listed theorem statements are within scope.

Selected references

• Mohsen Bayati, Marc Lelarge and Andrea Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015. arXiv:1207.7321v2
• David L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete & Computational Geometry 35, 617–652, 2006. MR2225676
• David L. Donoho, Arian Maleki and Andrea Montanari, Message-passing algorithms for compressed sensing, Proceedings of the National Academy of Sciences 106, 18914–18919, 2009. doi:10.1073/pnas.0909892106
• Peter Bürgisser and Felipe Cucker, Smoothed analysis of Moore–Penrose inversion, SIAM Journal on Matrix Analysis and Applications 31, 2769–2783, 2010. MR2740632