Control Theory

Motivation

Optimal portfolio liquidation asks how a trader should unwind a position of $\mathcal X$ shares over a horizon $[0,T]$ when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost $\eta_t\xi_t^2$ for trading at rate $\xi_t$ (temporary impact) and a risk penalty $\lambda_tX_t^2$ on the open position, and imposes the liquidation constraint $X_T=0$. When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate $\mu_t$ through a permanent impact term $\kappa_t\mu_tX_t$. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.

The liquidation constraint makes the problem singular: the value function blows up at $T$, and the equilibrium is described by a forward-backward system whose decoupling field $A$ satisfies a Riccati BSDE with terminal value $A_T=+\infty$. A natural question is whether the constraint can be replaced by a finite penalty $nX_T^2$ on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as $n\to\infty$. Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.

Setting

Fix $T>0$, an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$ whose first coordinate $W^0$ is common noise, and an initial position $\mathcal X\in L^2$ independent of $\widetilde W$. Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,\widetilde W)$, both augmented. The coefficients $\kappa,\lambda,\eta$ are bounded, nonnegative, $\mathbb F$-progressive processes, with $\lambda$ and $\eta$ bounded below by positive constants. Write $\kappa_{\max}$, $\eta_\star$, $\lambda_\star$ for the essential supremum of $\kappa$ and the essential infima of $\eta$ and $\lambda$, $\|\eta\|$ for the essential supremum of $|\eta|$, and $\alpha=\eta_\star/\|\eta\|\in(0,1]$. Assumption 2.3 adds the weak-interaction condition: some $\theta>0$ satisfies $\kappa_{\max}<4\eta_\star\theta$ and $\theta\kappa_{\max}<4\lambda_\star$.

Given an aggregate rate $\mu$, a trading rate $\xi\in L^2_{\mathbb F}$ yields the position $X^\xi_t=\mathcal X-\int_0^t\xi_s\,ds$. The constrained problem minimizes

$$J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_s\mu_sX^\xi_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\,\Big|\,\mathcal X\Big]$$

over $\xi$ with $\int_0^T\xi_s\,ds=\mathcal X$; its value is $V(\mathcal X;\mu)$. The penalized problem (4.1) drops the constraint and minimizes

$$J^n(\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_t\mu_tX^\xi_t+\eta_t\xi_t^2+\lambda_t(X^\xi_t)^2\big)dt+n(X^\xi_T)^2\,\Big|\,\mathcal X\Big]$$

over all $\xi\in L^2_{\mathbb F}$, with value $V^n(\mathcal X;\mu)$. An equilibrium is a fixed point $\mu_t=\mathbb E[\xi^*_t|\mathcal F^0_t]$.

The constrained equilibrium is given by the FBSDE (2.3), $dX_t=-\frac{Y_t}{2\eta_t}dt$, $-dY_t=\big(\kappa_t\mathbb E[\frac{Y_t}{2\eta_t}|\mathcal F^0_t]+2\lambda_tX_t\big)dt-Z_t\,d\widetilde W_t$, $X_0=\mathcal X$, $X_T=0$, decoupled as $Y=AX+B$ where

$$-dA_t=\Big(2\lambda_t-\frac{A_t^2}{2\eta_t}\Big)dt-Z^A_t\,d\widetilde W_t,\qquad A_T=+\infty .$$

The penalized equilibria are given by the FBSDE (4.2) with $Y^n_T=2nX^n_T$, decoupled by $A^n$, the solution of the same Riccati BSDE with $A^n_T=2n$. The solutions live in weighted spaces: $\mathcal H_l$ with norm $\big(\mathbb E\sup_t|Y_t/(T-t)^l|^2\big)^{1/2}$, and the penalized analogue $\mathcal H^n_l$ with weight $(T-t+\eta_\star/n)^{-l}$. Assumption 4.1 requires a constant $C$ with $\exp\big(-\int_r^s\frac{A_u}{2\eta_u}du\big)\le C\frac{T-s}{T-r}$ for all $0\le r\le s<T$, almost surely.

Formalization targets

Goal: Theorem 4.6

Under Assumptions 2.3 and 4.1, with $\mu^*=\mathbb E[Y/(2\eta)|\mathcal F^0]$ the constrained equilibrium and $\mu^n=\mathbb E[Y^n/(2\eta)|\mathcal F^0]$ the penalized ones,

$$\lim_{n\to\infty}\mathbb E\big|V^n(\mathcal X;\mu^n)-V(\mathcal X;\mu^*)\big|=0 .$$

Milestones

1. Lemma 4.2 (first condition). If $\eta$ is deterministic, Assumption 4.1 holds.
2. Lemma A.3. $A^n$ exists uniquely, $A^n_t\ge\big(\frac1{2n}+\mathbb E[\int_t^T\frac{ds}{2\eta_s}|\mathcal F_t]\big)^{-1}$, $A^n\uparrow A$, and $\|A^n\|_{\mathcal M_{-1}}+\|A^n\|_{\mathcal M^n_{-1}}\le\mathfrak C$ uniformly in $n$.
3. Theorem 4.3. The FBSDE (4.4), with parameter $\mathfrak p\in[0,1]$ and data $f\in L^2$, has a unique solution in $\mathcal H^n_\alpha\times\mathcal H^n_\gamma\times S^2\times L^2\times L^2$.
4. Lemma 4.4. $\|X^n\|_{n,\alpha}+\|B^n\|_{n,\gamma}+\mathbb E\int_0^T|Y^n_t|^2dt\le\overline{\mathfrak C}$ uniformly in $n$.
5. (4.8). Under Assumption 4.1 the constrained equilibrium position satisfies $\|X^*\|_1<\infty$.
6. Lemma 4.5. $(X^n,B^n,Y^n)\to(X,B,Y)$ in $L^2(dt\otimes d\mathbb P)$.

Significance

The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.

The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in $n$-dependent weighted spaces (Lemma 4.4).

Difficulty

The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so $V^n\le V$ up to the change of $\mu$. The reverse inequality is where it fails. The penalized optimizer leaves a residual position $X^n_T\neq0$, and its cost has to be compared with the singular one, whose weight $(T-t)^{-1}$ explodes at $T$. Controlling this requires estimates uniform in $n$ in spaces whose weights $(T-t+\eta_\star/n)^{-l}$ degenerate as $n\to\infty$, and the bare exponent $\alpha=\eta_\star/\|\eta\|<1$ of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to $\mathcal H_1$, is what closes the gap. In addition, the aggregate rate $\mu^n$ changes with $n$, so both the controls and the cost functional move at once.

Formalization scope

Time is $\mathbb R_{\ge0}$; processes are real-valued functions of $(t,\omega)$; $W$ is the $m=k+1$-dimensional $\widetilde W$ with coordinate $0$ the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$; $A_T=+\infty$ is $\lim_{t\uparrow T}A_t=+\infty$ a.s. Conditional expectations inside drivers are $\mathbb F^0$-progressive versions of integrable processes. Weighted norms are computed in $[0,\infty]$. The explicit readings are:

• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$; (2.4) is stated without division; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• Assumption 2.3 is a hypothesis of every statement, including Lemma A.3 (the appendix assumes only its boundedness part).
• Assumption 4.1 holds almost surely with the constant chosen before $\omega$ (as restated on p. 32).
• The penalty index is an integer $n\ge1$; constants in Lemma A.3 and Lemma 4.4 are chosen before $n$.
• The class of $A^n$ is $S^2\times L^2$ on $[0,T]$ (not printed in Lemma A.3).
• The penalized control set is $L^2_{\mathbb F}$, with no terminal constraint.
• Values are conditional essential infima given $\sigma(\mathcal X)$.
• The equilibria $\mu^n,\mu^*$ of Theorem 4.6 are defined through the FBSDE solutions, as in the proof; uniqueness of penalized equilibria is not claimed.
• The solution of Proposition 2.8 includes the relation $Y=AX+B$ on $[0,T)$; "Theorem 2.8" on pp. 25–29 means Proposition 2.8.
• $L^1$ convergence means $\int|V^n-V|\,d\mathbb P\to0$, not convergence of expectations.

A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define $V$ by a pointwise infimum over all controls (which is $-\infty$ or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, Math. Oper. Res. 46(4), 2021; preprint arXiv:1804.04911v3. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, Journal of Risk 3, 2001. https://doi.org/10.21314/JOR.2001.041
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2):893–913, 2014 (reference [3] of the paper).
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stochastic Process. Appl. 128(3):979–1006, 2018 (reference [28] of the paper).
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Motivation

Large traders who must unwind a position by a deadline face a trade-off between trading fast, which moves prices against them, and trading slowly, which exposes them to price risk. When many traders liquidate at once, each one's execution price also depends on the aggregate selling rate of the others. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and a hard liquidation constraint: every position must be zero at the terminal time $T$. Single-player liquidation with this constraint leads to backward equations with singular terminal values (Ankirchner, Jeanblanc and Kruse, SIAM J. Control Optim. 2014; Graewe, Horst and Séré, Stoch. Proc. Appl. 2018). Earlier MFG models of execution (Cardaliaguet and Lehalle, Math. Financ. Econ. 2018; Carmona and Lacker, Ann. Appl. Probab. 2015) allow no liquidation constraint. This mission formalizes the paper's first main result: the constrained game has a unique equilibrium under a weak-interaction condition.

Setting

Fix $T>0$ and a probability space carrying an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$, where $W^0$ is the one-dimensional common noise, and an initial portfolio $\mathcal X\in L^2$ independent of $\widetilde W$. Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,W^0,W)$, both augmented by null sets. The cost coefficients are bounded nonnegative $\mathbb F$-progressive processes $\kappa$ (interaction), $\lambda$ (risk aversion) and $\eta$ (temporary impact), with $\lambda,\eta$ bounded away from zero.

A player's trading rate $\xi$ produces the position $X^\xi_t=\mathcal X-\int_0^t\xi_sds$. The admissible strategies are $\mathcal A_{\mathbb F}(\mathcal X)=\{\xi\in L^2_{\mathbb F}:\int_0^T\xi_sds=\mathcal X\}$. Given an $\mathbb F^0$-progressive aggregate rate $\mu$, the cost is

$$J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_sX^\xi_s\mu_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\ \Big|\ \mathcal X\Big],$$

and $V(\mathcal X;\mu)$ is its essential infimum over $\mathcal A_{\mathbb F}(\mathcal X)$. A process $\mu$ solves the MFG (1.7) if some optimal strategy $\xi^*$ given $\mu$ satisfies $\mu_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for a.e. $t$.

The equilibrium is described by the conditional mean-field FBSDE (2.3):

$$X_t=\mathcal X-\int_0^t\frac{Y_s}{2\eta_s}ds,\quad X_T=0,\quad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t\ \ \text{on }[0,T).$$

Solutions are sought in weighted spaces: $Y\in\mathcal H_l$ if $\mathbb E\sup_{t\le T}|Y_t/(T-t)^l|^2<\infty$, and $Y\in\mathcal M_l$ if $(T-t)^{-l}|Y_t|$ is essentially bounded. The weak-interaction condition (Assumption 2.3) asks for $\theta>0$ with $\kappa_{\max}/(4\eta_\star)<\theta<4\lambda_\star/\kappa_{\max}$, and $\alpha:=\eta_\star/\|\eta\|\in(0,1]$. The decoupling $Y=AX+B$ uses the solution $A$ of the singular Riccati BSDE $-dA_t=(2\lambda_t-A_t^2/(2\eta_t))dt-Z^A_td\widetilde W_t$, $A_T=+\infty$.

Formalization targets

Goal: Theorem 2.4

Under Assumption 2.3 the FBSDE (2.3) has a unique solution

$$(X,Y,Z)\in\mathcal H_\alpha\times L^2_{\mathbb F}([0,T])\times L^2_{\mathbb F}([0,T-];\mathbb R^m);$$

$\xi^*=Y/(2\eta)$ is optimal, $X$ is the optimal position, $\mu^*_t=\mathbb E[Y_t/(2\eta_t)\mid\mathcal F^0_t]$ is the unique solution of the MFG (1.7), and

$$V(\mathcal X;\mu^*)=\tfrac12A_0\mathcal X^2+\tfrac12B_0\mathcal X+\tfrac12\mathbb E\Big[\int_0^T\kappa_sX^*_s\mu^*_sds\ \Big|\ \mathcal X\Big].$$

Milestones

The milestones follow the paper's proof: Fact 2.2 on the weighted spaces; Lemma A.1, existence and uniqueness of $A$ with the bounds (A.1), and $A\in\mathcal M_{-1}$; the decay estimate (2.9), $\exp(-\int_r^sA_u/(2\eta_u)du)\le((T-s)/(T-r))^\alpha$; Lemma 2.5, an a priori estimate for the decoupled system (2.11) with homotopy parameter $\mathfrak p\in[0,1]$; Lemma 2.6, explicit unique solvability at $\mathfrak p=0$; Lemma 2.7, the continuation step $\mathfrak p\to\mathfrak p+\mathfrak d$; Proposition 2.8, unique solvability of (2.3) with (2.10) and a norm bound; the boundary limit (2.15); and Proposition 2.9, optimality, the equilibrium property and the value formula.

Significance

The theorem gives a complete equilibrium description for constrained liquidation with many players and stochastic, partially common market data: the equilibrium rate is the conditional expectation of the decoupled feedback rate given the common noise, and its value is explicit in terms of the Riccati solution. It is the basis of the paper's other two results, the $O(N^{-1/2})$-Nash property of the equilibrium in the $N$-player game (Theorem 3.3) and the approximation by penalized games (Theorem 4.6), which are separate missions in this series.

The result is proved in the paper; none of it is machine-checked. A formal development would contain the first formal treatment of BSDEs with singular terminal value and of a conditional (common-noise) mean-field FBSDE. Shorter proofs of individual steps, in particular of the a priori estimate and the continuation step, are welcome.

Difficulty

The obvious approach fails at the terminal time. Standard FBSDE theory requires a terminal condition for $Y$; here only $X_T=0$ is known, and $Y_T$ is undetermined. The decoupling coefficient $A$ blows up like $(T-t)^{-1}$, so the driver of the equation for $B$ is singular, and the classical monotonicity method of Hu–Peng and Peng–Wu, applied to $(X,B)$ in unweighted spaces, does not close. The paper works instead with weighted norms that encode the rate at which $X$ and $B$ vanish at $T$, and runs the continuation on the triple $(X,B,Y)$. The mean-field term is a conditional expectation given the common-noise filtration, not an expectation, so it remains random and has to be controlled pathwise in the weighted norms.

Formalization scope

Time is ℝ≥0; processes are real valued and $\widetilde W$ has $m=k+1$ coordinates, coordinate $0$ being $W^0$. The Itô calculus is the published definition Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs in integrated form). The explicit choices:

• Filtrations are augmented by the measurable null sets, and $\mathbb F$ contains $\sigma(\mathcal X)$.
• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$. Condition (2.4) is written without division, and "$1/\lambda,1/\eta$ bounded" as positive essential lower bounds.
• Assumption 2.3 is a hypothesis of every statement of §2, as the paper's standing assumption. Lemma A.1 (appendix) assumes only what §A assumes: $\lambda,\eta$ progressive, nonnegative and bounded, and $1/\eta$ bounded.
• Backward equations on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$. $A_T=\infty$ means $A_t\to+\infty$ as $t\uparrow T$ a.s.
• Weighted norms are computed in $[0,\infty]$, with the weight $(T-t)^{-l}$ in ℝ≥0∞.
• Every conditional expectation $\mathbb E[\cdot\mid\mathcal F^0_t]$ in an equation is evaluated through a progressive version, and its argument is required to be integrable.
• The value is an essential infimum of conditional costs.
• The relation $Y=AX+B$ is part of the solution concept of (2.11): without it, $Y$ is determined only up to an additive $\mathcal F_0$-measurable constant.
• The constant of Proposition 2.8 is uniform over initial portfolios in an $L^2$ ball, for fixed coefficients.
• Fact 2.2's product rule assumes paths of $K_1$ continuous on $[0,T)$, and its claim that $K_T=0$ for $K\in\mathcal M_l$ is not stated. Both printed versions fail under the essential-supremum norm.

The interaction term must stay conditioned on $\mathcal F^0_t$: conditioning on $\mathcal F_t$ makes it $Y_t/(2\eta_t)$ itself and collapses the game. The constraint $X_T=0$ and the admissibility condition $\int_0^T\xi=\mathcal X$ cannot be dropped either. The degenerate instance $\kappa\equiv0$ satisfies all hypotheses but decouples the game.

A complete development needs the following, all reusable beyond this mission: martingale representation for the augmented filtration $\mathbb F$; existence of progressive versions of conditional expectation processes; Doob's inequality on $[0,\tau]$; and linear BSDE solution formulas.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2), 2014. https://doi.org/10.1137/130913411
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stoch. Proc. Appl. 128(3), 2018. https://doi.org/10.1016/j.spa.2017.07.002
• P. Cardaliaguet, C.-A. Lehalle, Mean field game of controls and an application to trade crowding, Math. Financ. Econ. 12, 2018. https://doi.org/10.1007/s11579-017-0206-z
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://doi.org/10.1214/14-AAP1020
• Y. Hu, S. Peng, Solution of forward-backward stochastic differential equations, Probab. Theory Related Fields 103, 1995. https://doi.org/10.1007/BF01204214

Motivation

A trader who must sell a large position within a fixed horizon faces a trade-off: selling fast moves the price against her (temporary price impact), selling slowly exposes her to price risk. Since Almgren and Chriss, this optimal liquidation problem has been studied as a stochastic control problem with a terminal state constraint: the remaining position must be zero at the horizon $T$. When many traders liquidate at the same time, each trader's sales also depress the price that the others receive (permanent price impact), and the problem becomes a game.

Fu, Graewe, Horst and Popier (arXiv:1804.04911v3) study this game in the mean-field limit. Their §2 constructs a mean-field equilibrium through a singular conditional mean-field FBSDE. Their §3, the subject of this mission, justifies the limit: the strategies computed from the mean field game are an approximate Nash equilibrium of the finite game with $N$ traders, with an error of order $1/\sqrt N$. Without such a result, the mean-field equilibrium describes a model nobody plays; with it, the equilibrium is a usable approximation for large but finite markets.

The approximation of $N$-player games by mean field games goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007); Carmona and Delarue (SIAM J. Control Optim. 51, 2013) proved an $\varepsilon_N$-Nash property for a McKean–Vlasov class with state interaction and a rate $N^{-1/(d+4)}$. The present game differs in three respects: players interact through their controls (the average trading rate), there is a common noise observed by all, and each player's state must reach zero at time $T$.

Setting

A single probability space carries a one-dimensional Brownian motion $W^0$ (the common noise, which drives the benchmark price and is observed by every player), for each player $i$ a $k$-dimensional Brownian motion $W^i$ (the private noise), and i.i.d. initial portfolios $\mathcal X^i$ with law $\nu$; all of these are mutually independent. Player $i$ observes $\mathbb F^i$, $\mathcal F^i_t=\sigma(\mathcal X^i,W^0_s,W^i_s,\ s\le t)$, and chooses a trading rate $\xi^i$; her position is $X^i_t=\mathcal X^i-\int_0^t\xi^i_s\,ds$ and must satisfy $X^i_T=0$. Given the profile $\vec\xi=(\xi^1,\dots,\xi^N)$, her conditional cost is

$$J^{N,i}(\vec\xi)=\mathbb E\Big[\int_0^T\Big(\frac{\kappa^i_t}{N}\sum_{j=1}^N\xi^j_tX^i_t+\eta^i_t(\xi^i_t)^2+\lambda^i_t(X^i_t)^2\Big)dt\ \Big|\ \mathcal X^i\Big],$$

where $\kappa^i$ (permanent impact), $\eta^i$ (temporary impact) and $\lambda^i$ (risk aversion) are nonnegative bounded processes. Under Assumption 3.1 they are the same deterministic measurable functionals $\kappa,\eta,\lambda$ of $(t,\mathcal X^i,W^i_{\cdot\wedge t},W^0_{\cdot\wedge t})$ for every player, so the players are statistically identical.

In the mean field game, the average $\frac1N\sum_j\xi^j$ is replaced by a process $\mu$ adapted to the common-noise filtration $\mathbb F^0$, and an equilibrium is a $\mu^*$ with $\mu^*_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for the representative player's best response $\xi^*$. The paper characterizes it through the FBSDE (2.3),

$$dX_t=-\frac{Y_t}{2\eta_t}dt,\qquad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t,\qquad X_0=\mathcal X,\ X_T=0,$$

with $\widetilde W=(W^0,W)$; the optimal rate is $\xi^*=Y/(2\eta)$. Player $i$'s mean-field strategy $\xi^{*,i}=Y^i/(2\eta^i)$ comes from the same FBSDE with her own data.

Formalization targets

Goal: Theorem 3.3

For a positive function $M$ with $\psi\le M$, where $\psi(\mathcal X^i)=\mathbb E[\int_0^T|\xi^{*,i}_t|^2dt\mid\mathcal X^i]$, and admissible sets $\mathcal A^i=\{\xi\in\mathcal A_{\mathbb F^i}(\mathcal X^i):\mathbb E[\int_0^T|\xi_t|^2dt\mid\mathcal X^i]\le M(\mathcal X^i)\}$, there is a function $g$, independent of $i$ and $N$, with

$$J^{N,i}(\vec\xi^*)\le J^{N,i}(\xi^i,\xi^{*,-i})+\frac{g(\mathcal X^i)}{\sqrt N}\qquad\text{for all }N\ge1,\ 1\le i\le N,\ \xi^i\in\mathcal A^i .$$

The goal asserts only the shape of the bound, not its constant.

Milestones

1. Lemma 3.2: one measurable map $\Phi$ gives $(X^i,Y^i,\int_0^\cdot Z^i)=\Phi(\mathcal X^i,W^i,W^0)$ for every player, and $\xi^{*,i}=\phi(\mathcal X^i,W^0,W^i)$ (3.1).
2. (3.2): a single $\mu^*$ with $\mu^*_t=\mathbb E[\xi^{*,i}_t\mid\mathcal F^0_t]$ for every $i$.
3. (3.3): $\mathbb E\int_0^T|\xi^{*,i}_t|^2dt\le C$ uniformly in $i$.
4. (3.5): $\mathbb E[\int_0^T(\mu^*_t-\frac1N\sum_j\xi^{*,j}_t)^2dt\mid\mathcal X^i]\le 2(M(\mathcal X^i)+(2N-1)C)/N^2$.
5. The bounds on $I_1$ and $I_2$ (p. 24): the two differences of conditional costs into which the proof splits $J^{N,i}(\xi,\xi^{*,-i})-J^{N,i}(\vec\xi^*)$ are $O(1/\sqrt N)$.

Significance

The result turns the mean-field equilibrium of §2 into a statement about the finite market: when all $N$ traders use their mean-field strategies, a trader who deviates can save at most $g(\mathcal X^i)/\sqrt N$ in conditional expected cost. The error bound depends on the trader's own initial position only through $M(\mathcal X^i)$, and the rate $1/\sqrt N$ is dimension-free, in contrast with the $N^{-1/(d+4)}$ rates of state-interaction games, because the interaction runs through the empirical mean of the controls rather than through an empirical measure.

The paper's proof of Theorem 3.3 is short but rests on several facts it states without proof: the Yamada–Watanabe-type Lemma 3.2 (whose proof is referred to other papers), the identification (3.2) of a common conditional mean, and the moment bound (3.3) attributed to Proposition 2.8. This mission makes each of these a separate machine-checkable statement. As far as we know, none of these results, nor any optimal-liquidation mean field game, has a machine-checked proof.

Difficulty

The estimate (3.5) is a law-of-large-numbers bound for the average of $N$ processes that are not independent: all of them depend on the common noise $W^0$. The obvious argument, expanding the square and using independence, fails as stated; the cross terms vanish only conditionally on $W^0$, and only once one knows that every $\xi^{*,j}$ is the same measurable functional of $(\mathcal X^j,W^0,W^j)$. That is Lemma 3.2, a Yamada–Watanabe-type statement for a singular FBSDE with a conditional mean-field term, which needs strong uniqueness of the FBSDE in the class $\mathcal H_\alpha\times L^2\times L^2([0,T-])$ and is the main technical step. The terminal constraint $X_T=0$ makes the backward component singular at $T$ ($Y$ blows up like $X/(T-t)$), so standard Lipschitz FBSDE theory does not apply. Finally, the deviation $\xi$ is constrained only through a conditional second-moment bound $M$, and the comparison with the mean-field cost uses the optimality of $\xi^{*,i}$ (Proposition 2.9) against $\mu^*$.

Formalization scope

Everything is stated on one probability space carrying all players, with players indexed by $\mathbb N$; the $N$-player game uses players $i<N$ (the paper's $1,\dots,N$, shifted by one). Time is $\mathbb R_{\ge0}$ and the processes are real valued. Choices made explicit:

• Assumption 2.3 for every player is a hypothesis of every theorem: the paper states it "throughout" (p. 8), and the proof of Theorem 3.3 uses Propositions 2.8 and 2.9, which need it. Its constants $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $[0,T]\times\Omega$; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• The equilibrium processes $(X^i,Y^i,Z^i)$ are hypotheses: solutions of (2.3) for player $i$'s data in the class of Theorem 2.4. $\xi^{*,i}$ is defined as $Y^i/(2\eta^i)$, never through $\phi$.
• Conditioning on $\mathcal X^i=x^i$ is conditioning on $\sigma(\mathcal X^i)$; every conclusion holds almost surely, i.e. for $\nu$-a.e. $x^i$. "$\psi\le M$" is the a.s. inequality of conditional second moments, and $M$ is assumed measurable.
• $g$ is quantified before $N$ and $i$. A statement in which $g$ may depend on $N$ is trivially true and is ruled out.
• Filtrations are augmented by null sets. Each conditional expectation $\mathbb E[\,\cdot\mid\mathcal F^0_t]$ is evaluated through a progressive version of an integrable argument. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$.
• Lemma 3.2's path spaces carry the product σ-algebra; its identities hold for each $t$ almost surely.
• The paper's bound on $I_2$ is stated for $|I_2|$, which is what its Cauchy–Schwarz step gives and what the proof needs.

The development reuses the Itô-calculus definitions of Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs). Contributions useful beyond this mission: conditional independence given a common noise for functionals of independent inputs, a Yamada–Watanabe argument for FBSDEs, and conditional Cauchy–Schwarz bounds for time integrals. Proofs of any milestone, and of the facts from §2 they rely on, are welcome.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, J. Risk 3(2), 2001. https://doi.org/10.21314/JOR.2001.041
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2, 2007. https://doi.org/10.1007/s11537-007-0657-8
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://doi.org/10.1137/120883499
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Why approximate Nash equilibria of finite games

Mean field games (MFGs) were introduced by Lasry and Lions (Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (Commun. Inf. Syst. 2006) as limits of stochastic differential games with many symmetric players whose interaction runs through the empirical distribution of their states. An MFG is a fixed point problem for one representative player facing a flow of measures, and it is much easier to analyse than an $n$-player game. The justification for studying it is a converse statement: a solution of the MFG should yield strategies that are nearly optimal for every player of the finite game when $n$ is large. Results of this type were proved by Huang, Malhamé and Caines for linear-quadratic models and by Carmona and Delarue (SIAM J. Control Optim. 2013) in the strong formulation with Lipschitz data.

Carmona and Lacker (arXiv:1307.1152v2; Ann. Appl. Probab. 25(3), 2015) set up MFGs in a weak formulation: controls change the law of the state through a Girsanov density instead of entering the state equation. This allows measurable, path-dependent data and controls that need only be progressively measurable. Their Theorem 4.2 is the finite-player approximation in this generality. This mission formalizes it.

Setting

Let $\mathcal C=C([0,T];\mathbb R^d)$ with the sup norm, and fix a measurable weight $\psi:\mathcal C\to[1,\infty)$. $\mathcal P_\psi(\mathcal C)$ is the set of probability measures $\mu$ on $\mathcal C$ with $\int\psi\,d\mu<\infty$, carrying the topology $\tau_\psi$: the weakest topology making $\mu\mapsto\int f\,d\mu$ continuous for every measurable $f$ with $|f|\le c\,\psi$. The control set $A$ is a compact convex subset of a normed space, and $\mathcal P(A)$ carries the weak topology.

The data are a volatility $\sigma(t,x)$, a drift $b(t,x,\mu,a)$, a running reward $f(t,x,\mu,q,a)$ and a terminal reward $g(x,\mu)$, where $x\in\mathcal C$ is a whole path, $\mu\in\mathcal P_\psi(\mathcal C)$ and $q\in\mathcal P(A)$. On a probability space with an initial value $\xi\sim\lambda_0$ and an independent Wiener process $W$, let $X$ solve $dX_t=\sigma(t,X)\,dW_t$, $X_0=\xi$. A control $\alpha$ (an $A$-valued progressive process) and a measure $\mu$ define a new probability $P^{\mu,\alpha}$ with density

$$\frac{dP^{\mu,\alpha}}{dP}=\mathcal E\Big(\int_0^\cdot\sigma^{-1}b(t,X,\mu,\alpha_t)\,dW_t\Big)_T,$$

under which $X$ has drift $b(t,X,\mu,\alpha_t)$. The reward is $J^{\mu,q}(\alpha)=\mathbb E^{\mu,\alpha}[\int_0^Tf(t,X,\mu,q_t,\alpha_t)\,dt+g(X,\mu)]$. A pair $(\hat\mu,\hat q)$ is a solution of the MFG (Definition 3.4) if some $\hat\alpha$ maximizes $J^{\hat\mu,\hat q}$ and reproduces the input: $P^{\hat\mu,\hat\alpha}\circ X^{-1}=\hat\mu$ and $P^{\hat\mu,\hat\alpha}\circ\hat\alpha_t^{-1}=\hat q_t$ for a.e. $t$. Under the standing assumptions the optimal control is a function $\hat\alpha(t,X)$ of the path, the closed-loop control.

The $n$-player game. On a probability space with independent Wiener processes $W^i$ and i.i.d. initial values $\xi^i\sim\lambda_0$, let $X^i$ solve $dX^i_t=b(t,X^i,\hat\alpha(t,X^i))\,dt+\sigma(t,X^i)\,dW^i_t$ (the drift has no mean field term under (F.1)). The distributed controls are $\alpha^i_t=\hat\alpha(t,X^i)$: each player uses only their own state. A deviation $\beta\in\mathbb A_n$ is any process that is progressively measurable for the filtration $\mathbb F^n$ of all $n$ states (full information). A profile $\beta=(\beta^1,\dots,\beta^n)$ changes the probability to $P_n(\beta)$, with density the Doléans exponential of $\sum_i\int(\sigma^{-1}b(t,X^i,\beta^i_t)-\sigma^{-1}b(t,X^i,\alpha^i_t))\,dW^i_t$. Player $i$ then receives

$$J_{n,i}(\beta)=\mathbb E^{P_n(\beta)}\Big[\int_0^Tf\big(t,X^i,\mu^n,q^n(\beta_t),\beta^i_t\big)\,dt+g(X^i,\mu^n)\Big],$$

with $\mu^n=\frac1n\sum_j\delta_{X^j}$ and $q^n(\beta_t)=\frac1n\sum_j\delta_{\beta^j_t}$.

Formalization targets

Goal: Theorem 4.2 (p. 13)

Under (S), (C) and (F), there is a sequence $\epsilon_n\ge0$, $\epsilon_n\to0$, such that for all $n\ge1$, $1\le i\le n$ and $\beta\in\mathbb A_n$,

$$J_{n,i}(\alpha^1,\dots,\alpha^{i-1},\beta,\alpha^{i+1},\dots,\alpha^n)\le J_{n,i}(\alpha^1,\dots,\alpha^n)+\epsilon_n.$$

No rate is claimed; the theorem asserts only that the gain from deviating vanishes uniformly over players and deviations.

Milestones

1. Lemma 5.6 (p. 16): for compact $K$, joint continuity of $G:E\times K\to\mathbb R$ at $\{x_0\}\times K$ is equivalent to continuity of $G(x_0,\cdot)$ together with continuity at $x_0$ of $x\mapsto\sup_{y\in K}|G(x,y)-G(x_0,y)|$.
2. Lemma 8.1 (p. 32): for empirically measurable $F$ with $|F(x,\mu)|\le c(\psi(x)+\int\psi\,d\mu)$ and $F(x,\cdot)$ continuous at $\hat\mu$, $\mathbb E|F(X^i,\mu^n)-F(X^i,\hat\mu)|^p\to0$ for $p\in[1,2)$.
3. The $L^p$ bound (p. 33): $\{dP_n(\beta^\alpha)/dP:\beta\in\mathbb A_n,\ n\ge1\}$ is bounded in $L^p$ for each $p\ge1$, where $\beta^\alpha=(\beta,\alpha^2,\dots,\alpha^n)$.
4. Lemma 8.2 (p. 32): $\sup_{\beta\in\mathbb A_n}|J_{n,1}(\beta^\alpha)-J'_n(\beta)|\to0$, where $J'_n(\beta)=\mathbb E^{P_n(\beta^\alpha)}[\int_0^Tf(t,X^1,\hat\mu,\hat q_t,\beta_t)\,dt+g(X^1,\hat\mu)]$.
5. Lemma 8.3 (p. 33): $J'_n(\alpha^1)\ge J'_n(\beta)$ for every $\beta\in\mathbb A_n$.

Significance

Theorem 4.2 states the sense in which an MFG solution solves the finite game. It covers path-dependent and merely measurable coefficients, interaction through the law of the controls, and full-information deviations against distributed strategies. In the paper it underlies the applications of §6: the price impact model, where Proposition 6.1 adds the rate $C/\sqrt n$, and the flocking model. The result is qualitative: it gives no rate in general.

The result is proved in the paper. No machine-checked proof of it or of its lemmas exists on the platform. The mission produces a formal statement layer for weak-formulation MFGs: path space, $\mathcal P_\psi$ with $\tau_\psi$, Girsanov densities over Itô versions, Definition 3.4, and the $n$-player game. It then asks for the formal proof of the theorem. Missions 1 and 2 of this series (existence and uniqueness of MFG solutions) use the same model encoding. The strong-formulation result of Carmona and Delarue is a separate statement with a separate model and is not part of this mission.

Difficulty

The obvious route replaces $\mu^n$ by $\hat\mu$ and $q^n(\beta_t)$ by $\hat q_t$ in $J_{n,i}$ and appeals to the law of large numbers. This fails for two reasons. First, the expectation is taken under $P_n(\beta)$, which depends on the deviation $\beta$, and $\beta$ may depend on all players' states. The convergence therefore has to be uniform over a class of measures and requires uniform integrability of the densities. Second, $\tau_\psi$ is neither metrizable nor separable. Continuity in $\mu$ does not reduce to sequences, and dominated convergence does not hold for nets, so the almost sure convergence of empirical measures does not by itself transfer to the rewards. The remaining step asks whether full information helps the deviating player against the limiting environment. It is not a direct consequence of the optimality of $\hat\alpha$ in the mean field problem, which is posed over a smaller filtration.

Formalization scope

• Paths and time. States are Fin d → ℝ. $\mathcal C$ is C(Set.Icc 0 T, Fin d → ℝ) with its Borel σ-field. Time is ℝ≥0; only $[0,T]$ matters.
• Measures and topologies. $\mathcal P_\psi(\mathcal C)$ is a structure carrying $\tau_\psi$ as its only topology. $\mathcal P(A)$ is Mathlib's ProbabilityMeasure A with the weak topology and its Borel σ-field. Progressive measurability uses the canonical filtration on $\mathcal C$.
• Base space. It is abstract: any probability space with $\xi$ and an independent Brownian motion $W$. The canonical space is an instance. Filtrations are augmented by the measurable null sets.
• Stochastic integrals. All stochastic integrals come from the published Peng1990.SMP.Stochastic $L^2$ Itô layer. "Strong solution" therefore includes square integrability, $\mathbb E\int_0^T\|\sigma(t,X)\|^2dt<\infty$ and $\sup_t\mathbb E|X_t-\xi|^2<\infty$.
• Assumptions (S). Nonsingularity of $\sigma$ is encoded as invertibility of $\det\sigma$. The "increasing" $\rho$ of (S.4) is encoded as monotone.
• Densities and values. A density is a relation over versions of the Itô integrals. Every statement asserts that a version exists and holds for every version, so no statement holds because the set of versions is empty. $J_{n,i}$ and $J'_n$ are computed as $\mathbb E^P[D(\cdots)]$ for a version $D$. Suprema over $\mathbb A_n$ are unfolded into $\forall\varepsilon\,\exists N$ form, never written as real ⨆.
• Players. Players are indexed from $0$, so player 1 is index $0$.
• Hypotheses. (S), (C), (F), the fixed solution with its closed-loop control and the game space are bundled into one structure.

Two readings of the goal would make it trivial, and the statement excludes both. If $\epsilon$ were allowed to depend on $i$ or $\beta$, the bound would carry no content. If the deviation were evaluated under the undeviated measure $P$ instead of $P_n(\beta)$, the game would be a different one. (F.4) is genuine continuity, not the sequential continuity of (E).

A complete development needs:

• the strong law of large numbers for i.i.d. path-valued variables tested against $B_\psi$ functions;
• $L^p$ bounds for Doléans exponentials of bounded integrands;
• Girsanov's theorem for the $L^2$ Itô layer;
• comparison for BSDEs (Pardoux–Peng).

The Girsanov and BSDE comparison results are reusable well beyond this mission and are welcome as separate contributions, as are proofs of Lemma 5.6 and of the $L^p$ bound.

Selected references

• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, arXiv:1307.1152v2, 2014; Ann. Appl. Probab. 25(3), 2015. https://arxiv.org/abs/1307.1152v2, https://doi.org/10.1214/14-AAP1020
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2, 2007. https://doi.org/10.1007/s11537-007-0657-8
• M. Huang, R. Malhamé, P. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://doi.org/10.1137/120883499
• É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14, 1990. https://doi.org/10.1016/0167-6911(90)90082-6

Motivation

Mean field games, introduced independently by Lasry and Lions (Mean field games, Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (2006), describe the Nash equilibria of games with a very large number of symmetric players, each of whom reacts only to the empirical distribution of the others. In the limit, an equilibrium is a fixed point: a flow of population laws such that the optimal response of a single representative player to that flow reproduces it.

Existence of such fixed points is typically obtained by compactness, and says nothing about whether the equilibrium is determined by the data. Uniqueness matters for the use of the model: a unique equilibrium can be computed, approximated, and compared across parameters, while multiple equilibria raise a selection problem. Lasry and Lions showed by counterexamples that uniqueness fails in general, and identified a monotonicity condition on the population-dependent part of the reward under which it holds; outside that condition, uniqueness is typically available only for short horizons and Lipschitz coefficients.

Carmona and Lacker (arXiv:1307.1152v2, 2014; Ann. Appl. Probab. 25(3), 2015) set up a weak formulation of mean field games in which the controlled state is obtained from a fixed driftless diffusion by a Girsanov change of measure, so that the coefficients may be merely measurable in the state and path dependent. This mission formalizes their uniqueness theorem (Theorem 3.8): the Lasry–Lions argument carried out in the weak formulation, through backward stochastic differential equations.

Setting

Fix a horizon $T$, a dimension $d$, the path space $\mathcal C = C([0,T];\mathbb R^d)$ with the sup norm, and a measurable $\psi:\mathcal C\to[1,\infty)$. Write $\mathcal P_\psi(\mathcal C)$ for the probability measures $\mu$ on $\mathcal C$ with $\int\psi\,d\mu<\infty$. A control set $A$ is a compact convex subset of a normed space, and $\mathcal P(A)$ is the set of probability measures on $A$ with the weak topology.

On a probability space $(\Omega,P)$ carrying an initial state $\xi$ and an independent $d$-dimensional Brownian motion $W$, filtered by the augmented filtration of $(\xi,W)$, let $X$ solve the driftless state equation $dX_t=\sigma(t,X)\,dW_t$, $X_0=\xi$. The admissible controls $\mathbb A$ are the progressively measurable $A$-valued processes. For $\mu\in\mathcal P_\psi(\mathcal C)$ and $\alpha\in\mathbb A$ the measure $P^{\mu,\alpha}$ has density

$$\frac{dP^{\mu,\alpha}}{dP}=\mathcal E\Big(\int_0^\cdot\sigma^{-1}b(t,X,\mu,\alpha_t)\,dW_t\Big)_T,$$

under which $X$ has drift $b(t,X,\mu,\alpha_t)$. For a flow $q:[0,T]\to\mathcal P(A)$ the reward is

$$J^{\mu,q}(\alpha)=E^{\mu,\alpha}\Big[\int_0^T f(t,X,\mu,q_t,\alpha_t)\,dt+g(X,\mu)\Big].$$

A pair $(\mu,q)$ is a solution of the MFG (Definition 3.4) if some $\alpha\in\mathbb A$ maximizes $J^{\mu,q}$ over $\mathbb A$, $P^{\mu,\alpha}\circ X^{-1}=\mu$, and $P^{\mu,\alpha}\circ\alpha_t^{-1}=q_t$ for almost every $t$.

The Hamiltonian is $h(t,x,\mu,q,z,a)=f(t,x,\mu,q,a)+z\cdot\sigma^{-1}b(t,x,\mu,a)$, with maximum $H$ over $a\in A$ and maximizer set $A(t,x,\mu,q,z)$. Assumption (U) asks that (U.1) the maximizer is unique; (U.2) $b=b(t,x,a)$ does not depend on $\mu$; (U.3) $f=f_1(t,x,\mu)+f_2(t,\mu,q)+f_3(t,x,a)$; and (U.4) the Lasry–Lions monotonicity condition

$$\int_{\mathcal C}\Big[g(x,\mu)-g(x,\mu')+\int_0^T\big(f_1(t,x,\mu)-f_1(t,x,\mu')\big)dt\Big](\mu-\mu')(dx)\le0\qquad\text{for all }\mu,\mu'.$$

The standing assumptions (S) of the paper (measurability, continuity in $a$, nonsingular $\sigma$, bounded $\sigma^{-1}b$, a $\psi$-growth bound on $f,g$, and a separation of $f$) are in force throughout.

Formalization targets

Goal: Theorem 3.8

Under (S) and (U), if $(\mu^1,q^1)$ and $(\mu^2,q^2)$ are solutions of the MFG, then

$$\mu^1=\mu^2\qquad\text{and}\qquad q^1_t=q^2_t\ \text{for almost every }t\in[0,T].$$

Definition 3.4 constrains $q_t$ only for almost every $t$, so this is the strongest identification possible.

Milestones

1. §7.3, p. 30. For a solution $(\mu,q)$ with optimal control $\alpha$ and a solution $(Y,Z)$ of the BSDE $Y_t=g(X,\mu)+\int_t^TH(s,X,\mu,q_s,Z_s)ds-\int_t^TZ_sdW_s$ (7.1), $\alpha_t$ maximizes the Hamiltonian at $Z_t$, $dt\times dP$-a.e.; under (U.1) every such maximizing control agrees with $\alpha$ a.e.
2. (7.9)–(7.10). $E[Y^1_0-Y^2_0]$ written as an expectation under $P^{\mu^1,\alpha^1}$ and under $P^{\mu^2,\alpha^2}$.
3. (7.11)–(7.12). Pointwise bounds from maximization of the Hamiltonian, strict when the controls differ.
4. (7.13). $\big[E^{\mu^1,\alpha^1}-E^{\mu^2,\alpha^2}\big]\big[\Delta g(X)+\int_0^T\Delta f_1(t,X)dt\big]=0$.
5. §7.3, p. 31. $\alpha^1=\alpha^2$, $\mathcal L\times P$-a.e.

Significance

Theorem 3.8, combined with the existence theorem of the same paper (Theorem 3.5, the first mission of this series), gives existence and uniqueness of the equilibrium (Corollary 3.9) for coefficients that are only measurable and path dependent in the state, under a monotonicity condition and no Lipschitz or small-horizon requirement. Uniqueness is also what makes the approximation result of the paper (Theorem 4.2, the third mission) refer to the equilibrium.

The result is proved in the paper. It has not been machine-checked; no mean field game uniqueness theorem in a weak or Girsanov formulation is formalized in Lean or Mathlib. The formal development would contain, as reusable parts, the Doléans exponential of a bounded Itô integrand as a probability density, the change of Brownian motion under it, the comparison principle for BSDEs with Lipschitz drivers, and the Lasry–Lions monotonicity argument.

Difficulty

The argument compares two equilibria through two different measures $P^{\mu^1,\alpha^1}$ and $P^{\mu^2,\alpha^2}$. The direct Lasry–Lions computation, which differentiates a pairing of a Hamilton–Jacobi–Bellman solution with a Fokker–Planck solution, is not available: there is no PDE, and the value functions are only known through BSDEs. The proof needs (a) that an optimal control maximizes the Hamiltonian along the adjoint process $Z$ — the necessity half of the BSDE optimality criterion, which the paper uses without a displayed proof; (b) the representation of $E[Y^1_0-Y^2_0]$ under each of the two measures, which requires that the stochastic integrals $\int(Z^1-Z^2)\,dW^{\mu^i,\alpha^i}$ be true martingales under the changed measures; and (c) turning a strict pointwise inequality on a set of positive $dt\times dP$-measure into a strict inequality of expectations, which uses the equivalence $P\sim P^{\mu^i,\alpha^i}$.

Formalization scope

The Lean development lives in the namespace WeakMFG.Uniqueness and builds on the published definition Peng1990.SMP.Stochastic (Brownian motion, $L^2$ Itô integrals, Itô processes, BSDEs). Conventions:

• Base space. Any probability space carrying $\xi$ and an independent standard Brownian motion $W$, with the filtration $\sigma(\xi)\vee\sigma(W_s:s\le t)$ completed by the measurable null sets; the canonical space of the paper is an instance.
• State. "Strong solution" of $dX=\sigma(t,X)dW$ is read in the $L^2$ Itô theory (square-integrable solutions); $\sigma(t,X)>0$ is matrix invertibility; states are vectors of $\mathbb R^d$ with the sup norm, Euclidean squares written as sums of squares.
• Measures. $\mathcal P_\psi(\mathcal C)$ is a structure carrying the topology $\tau_\psi$; $\mathcal P(A)$ has the weak topology and its Borel $\sigma$-field; time is $\mathbb R_{\ge0}$, of which only $[0,T]$ enters.
• Densities. Itô integrals are determined up to versions, so $dP^{\mu,\alpha}/dP$ is a predicate on a random variable; statements assert that a version exists and hold for every version. Optimality is stated against every admissible competitor, never through a real supremum.
• Added hypotheses, disclosed. Joint measurability of $(t,x,q,a)\mapsto f(t,x,\mu,q,a)$, which the reward presupposes; in (U.4), integrability of the integrals the page writes; the slip in (U.3), which omits $q$ from the arguments of $f$, is corrected.

A formalization whose hypotheses contain the conclusion is ruled out: the goal assumes only that the two pairs are solutions in the sense of Definition 3.4 — no BSDE solution, no Hamiltonian maximization, no equality of densities is assumed. Uniqueness of $q$ is stated almost everywhere in time, and nowhere is equality of the two optimal controls as functions asked for.

Contributions welcome: the Doléans exponential and Girsanov's theorem for bounded drifts in the $L^2$ Itô layer, existence and comparison for Lipschitz BSDEs on a filtration enlarged by an independent initial condition, and the measurable maximum theorem for the Hamiltonian. These are reusable beyond this mission, in particular by the other two missions of the series.

Selected references

• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, arXiv:1307.1152v2, 2014; Ann. Appl. Probab. 25(3), 2015. https://arxiv.org/abs/1307.1152
• J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2(1), 2007. https://doi.org/10.1007/s11537-007-0657-8
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems & Control Letters 14(1), 1990. https://doi.org/10.1016/0167-6911(90)90082-6