Stochastic Systems

Why boundary regularity matters

An optimal stopping rule chooses when to end a stochastic process in order to collect a terminal reward, possibly after earning or paying a running reward. The resulting value function often solves a free-boundary problem: the state space splits into a region where stopping is optimal and one where continuing is better. Smoothness inside either region does not by itself say what happens where the regions meet. This mission concerns the global first spatial derivative of that value function at the optimal stopping boundary.

De Angelis and Peskir proved that a probabilistic condition on the boundary, together with regularity of the process as a spatial flow and explicit integrability bounds, gives continuous differentiability of the value function across the boundary. Their result applies to standard Markov processes with right-continuous paths and left limits, including jump processes; it is not restricted to diffusions or to a constant discount rate. The source is De Angelis and Peskir, arXiv:1812.04564v2, Theorem 8.

The stopping problem and its boundary

Let $d\ge1$, let $E=\mathbb R^d$, and let $X_t^x$ be a stochastic flow: the same probability space carries a path starting from every state $x\in E$. Time is nonnegative. One right-continuous filtration makes every path adapted and is used for every stopping rule. The process is strong Markov, has right-continuous paths with left limits, is left continuous over stopping times, and starts from $X_0^x=x$. Expectations and probabilities written $E_x$ and $P_x$ in the paper are the expectation and probability of the flow $X^x$ under one measure $P$.

The continuous data are a nonnegative discount rate $\lambda:E\to[0,\infty)$, a terminal reward $G:E\to\mathbb R$, and a running reward $H:E\to\mathbb R$. The discount accumulated along the path from $x$ is $\Lambda_t^x=\int_0^t\lambda(X_s^x)\,ds$. For every finite-valued stopping time $\tau$ of the common filtration, define

$$J(x,\tau)=E\!\left[e^{-\Lambda_\tau^x}G(X_\tau^x)+\int_0^\tau e^{-\Lambda_t^x}H(X_t^x)\,dt\right], \qquad V(x)=\sup_\tau J(x,\tau).$$

This is the infinite-horizon problem (2.1). It is well posed here when all admissible payoffs are integrable and the first entry time into the stopping set is an almost surely finite optimal stopping time. These conditions ensure that $V$ is a real, attained supremum rather than a default value of Lean's real supremum or integral. Define the stopping set $D=\{x:V(x)=G(x)\}$, the continuation set $C=\{x:V(x)>G(x)\}$, and the boundary relevant to the theorem as $D\cap\overline C$. For a state set $A$, the first entry time is $\tau_A^x=\inf\{t\ge0:X_t^x\in A\}$ and the first strictly positive hitting time is $\sigma_A^x=\inf\{t>0:X_t^x\in A\}$. Both may be infinite.

A boundary point $z$ is probabilistically regular for $A$ if $P_z(\sigma_A=0)=1$. It is Green regular for $A$ when $P_x(\tau_A\ge\varepsilon)\to0$ as $x\to z$ through $C$, for every $\varepsilon>0$. The paper obtains Green regularity by either strong Feller continuity with probabilistic regularity for $D$, or spatial continuity of the flow with probabilistic regularity for $D^\circ$. Lemma 1 and Corollaries 2–3 give the first route; Lemma 4 and Corollaries 5–6 give the second. All six statements use an arbitrary closed $D$, as in Section 3 of the source. Source: §§2–3, pp. 3–11.

Formalization targets

The milestone results first establish the two boundary regularity routes. In particular, approaching $z$ through $C$, the first route gives $\tau_D^{x_n}\to0$ in probability; the second gives $\tau_{D^\circ}^{x_n}\to0$ and $\tau_D^{x_n}\to0$ almost surely. Equations (4.16) and (4.19) then bound, respectively, the lower and upper limits of each coordinate derivative $\partial_iV(x_n)$ by $\partial_iG(z)$. The pointwise part of Theorem 8 concludes

$$D V(z)=D G(z),\qquad \lim_{C\ni x\to z}D V(x)=D G(z).$$

The mission goal is the final sentence of Theorem 8. If the theorem's local hypotheses hold at every $z\in D\cap\overline C$, then

$$V\in C^1(\mathbb R^d).$$

The hypotheses include the discounted generator representation (2.14) from the problem setup, continuity and interior $C^1$ regularity of $V$, global $C^1$ regularity of $G$, one positive Lipschitz constant for both $H$ and $\lambda$, a $C^1$ spatial flow, the four local bounds (4.4)–(4.7) with one radius at each boundary point, and one of the two probabilistic regularity alternatives. The goal retains all dimensions $d\ge1$, all nonnegative continuous discount rates, and the source's full class of standard Markov flows. Source: §2.5 and Theorem 8, pp. 7, 11–12.

What the result gives

The conclusion identifies the derivative of the value function on both sides of the stopping boundary. It strengthens a derivative match along a single direction or a chosen sequence into continuous differentiability on the whole state space. This is relevant to free-boundary formulations of optimal stopping, where interior regularity can be available from a Dirichlet or Poisson problem while boundary regularity remains the missing step. The authors describe that distinction in their discussion of smooth fit and global differentiability. Source: §2.5, p. 8.

The mathematical theorem is proved in the 2020 paper. In this mission, the definitions and statements compile as Lean declarations, while the theorem proofs remain to be formalized. A complete development would supply reusable arguments about hitting times, semicontinuity of hitting probabilities, stochastic flows, and limits of derivatives near a stopping boundary. Those components would also support the paper's finite-horizon spatial and temporal results.

The central difficulty

The value is a supremum over stopping rules. Differentiating the reward for a fixed stopping time does not automatically differentiate that supremum, because the optimal time depends on the initial state. Near the boundary, even continuity of the value does not control the duration of the optimal rule from neighboring states. The paper's probabilistic regularity conditions address that duration, while (4.4)–(4.7) provide the integrability needed to pass to derivative limits. A direct appeal to interior differentiability leaves the boundary itself untreated. Source: §§3–4.1, pp. 9–15.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d) with $d\ge1$; Fin d indices are the paper's coordinates $1,\ldots,d$ shifted by one. Balls are open Euclidean balls. Time is $\mathbb R_{\ge0}$, and the entry and hitting times live in $\mathbb R_{\ge0}\cup\{+\infty\}$ so an unattained hit has its intended value. The flow is the process; no separate family of measures $P_x$ is introduced. One common filtration is used for all initial states and is right-continuous. Its finite stopping times are the full admissible class, not only hitting times.

The value uses Bochner expectations and real Lebesgue time integrals. Well-posedness records integrability for every admissible payoff and optimality and almost sure finiteness of $\tau_D^x$. The generator clause acts on smooth functions in the domain of the discounted transition semigroup; it retains the paper's diffusion, drift, killing, and jump terms. The boundary is $D\cap\overline C$, and approach through continuation points is expressed by the within-set neighborhood filter. Pointwise continuous differentiability means a Fréchet derivative at $z$ equal to $D G(z)$ and convergence of $D V$ along $C$; the goal uses global ContDiff. The local bounds retain all independently indexed starting states and coordinates. Their uncountable suprema are represented by integrable common majorants, with timewise measurable envelopes for the suprema inside time integrals. This convention excludes default integral values from nonmeasurable or nonintegrable expressions.

A formalization restricted to Brownian motion, one dimension, zero or constant discount, continuous paths, bounded rewards, or only one boundary regularity branch would state a different theorem. Contributions toward measurable hitting-time events, the two Section 3 regularity chains, the envelope bounds, and the derivative comparison are welcome.

Selected references

• De Angelis, T., and Peskir, G., Global C¹ Regularity of the Value Function in Optimal Stopping Problems, Annals of Applied Probability 30(3), 2020. arXiv:1812.04564v2; DOI:10.1214/19-AAP1517.

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

Motivation

Many quantities in stochastic control, mathematical finance and stochastic differential games depend on the whole past of a Brownian path rather than on its current position: the price of an Asian or lookback option, the value of a control problem with delay, the solution of a non-Markovian backward stochastic differential equation (BSDE). For Markovian problems the value is a function $v(t,x)$ and solves a parabolic PDE, and the theory of viscosity solutions (Crandall, Ishii and Lions) gives existence, uniqueness and stability without any smoothness. For path-dependent problems the value is a functional $u(t,\omega)$ of the path, and the corresponding equation is a path-dependent PDE (PPDE), written with the horizontal and vertical derivatives introduced by Dupire (SSRN 1435551) and developed into a functional Itô calculus by Cont and Fournié (arXiv:1002.2446). Classical solutions of PPDEs rarely exist, so a weak notion is needed.

Timeline:

• 1990. Pardoux and Peng prove well-posedness of BSDEs with Lipschitz generator (doi:10.1016/0167-6911(90)90082-6); the BSDE value is the natural candidate solution of a semilinear PPDE.
• 2009–2013. Dupire, and Cont and Fournié, define pathwise derivatives and prove a functional Itô formula; Peng asks for a viscosity theory of PPDEs (ICM 2010).
• 2011–2014. Ekren, Keller, Touzi and Zhang (arXiv:1109.5971, Ann. Probab. 42 (2014) 204–236) define viscosity solutions of semilinear PPDEs through an optimal stopping problem under a nonlinear expectation and prove existence, stability, comparison and uniqueness. Fully nonlinear PPDEs follow in Ekren, Touzi and Zhang (arXiv:1210.0006).

Setting

Fix $d \ge 1$ and $T>0$. Let $\Omega$ be the space of continuous paths $\omega:[0,T]\to\mathbb R^d$ with $\omega_0 = 0$, $B$ the canonical process, $\mathbb F$ the filtration it generates, $P_0$ the Wiener measure and $\Lambda = [0,T]\times\Omega$. On $\Lambda$ the pseudometric is $d_\infty((t,\omega),(t',\omega')) = |t-t'| + \sup_{s\le T}|\omega_{t\wedge s}-\omega'_{t'\wedge s}|$. For $t\le T$, $\Omega^t$ is the space of continuous paths on $[t,T]$ vanishing at $t$, with Wiener measure $P^t_0$, and $\hat\Omega^t$ the space of càdlàg paths on $[t,T]$. The concatenation $\omega\otimes_t\omega'$ follows $\omega$ up to $t$ and then $\omega_t + \omega'$, and $u^{t,\omega}(s,\omega') = u(s,\omega\otimes_t\omega')$.

A functional $\hat u$ on $[t,T]\times\hat\Omega^t$ has the Dupire derivatives $\partial_\omega\hat u$, the derivative under a bump $h\mathbf 1_{[s,T]}e_i$ of the path, and $\partial_t\hat u$, the right derivative in time along the stopped path. $C^{1,2}_b(\Lambda^t)$ is the class of functionals that agree on continuous paths with some $\hat u$ whose derivatives $\partial_t\hat u$, $\partial_\omega\hat u$, $\partial^2_{\omega\omega}\hat u$ exist and are bounded and $d_\infty$-continuous.

The equation is the semilinear PPDE

$$(\mathcal L u)(t,\omega) := -\partial_t u - \tfrac12\operatorname{tr}\big(\partial^2_{\omega\omega}u\big) - f\big(t,\omega,u,\partial_\omega u\big) = 0,\qquad 0\le t<T.$$

For $L\ge0$, $\underline{\mathcal E}^L_t$ and $\overline{\mathcal E}^L_t$ are the infimum and supremum of expectations under the Girsanov measures $P^{t,\beta}$, $|\beta^i|\le L$. A bounded $d_\infty$-continuous $u$ is a viscosity $L$-subsolution if $(\mathcal L^{t,\omega}\varphi)(t,\mathbf 0)\le0$ at every $(t,\omega)$ with $t<T$ for every test function $\varphi\in C^{1,2}_b(\Lambda^t)$ that touches $u^{t,\omega}$ from above in the sense

$$0 = \varphi(t,\mathbf 0)-u(t,\omega) = \min_{\tilde\tau\in\mathcal T^t}\underline{\mathcal E}^L_t\big[(\varphi-u^{t,\omega})_{\tilde\tau\wedge\tau}\big]\quad\text{for some }\tau\in\mathcal T^t_+ ,$$

where $\mathcal T^t$ is a class of stopping times with open level sets. Supersolutions use $\max$ and $\overline{\mathcal E}^L_t$. A viscosity subsolution is an $L$-subsolution for some $L$, the same $L$ at every point. The candidate solution is $u^0(t,\omega) = Y^{0,t,\omega}_t$, where $Y^{0,t,\omega}$ solves the BSDE with terminal value $g^{t,\omega}$ and generator $f^{t,\omega}$ under $P^t_0$.

Formalization targets

Goal: Theorem 4.6

Under Assumption 4.2 ($f$ bounded, progressively measurable, continuous in $t$, uniformly continuous in $\omega$, Lipschitz in $(y,z)$; $g$ bounded and uniformly continuous) and Assumption 4.4 (an extension $\hat f$ of $f$ to càdlàg paths, continuous and Lipschitz), for every viscosity subsolution $u^1$ and supersolution $u^2$,

$$u^1(T,\cdot)\le g\le u^2(T,\cdot)\ \Longrightarrow\ u^1\le u^2\ \text{ on }\Lambda,$$

and consequently $u^0$ is the unique viscosity solution with terminal condition $g$.

Milestones

In the order the proof uses them: Example 2.5 (hitting times lie in $\mathcal T$); Proposition 5.4 ($u^0$ is uniformly continuous); Theorem 4.3 ($u^0$ is a viscosity solution); Lemma 5.7 (partial comparison when one of $u^1,u^2$ is smooth) and its form under the weaker condition (5.11); the bound $\underline u\le u^0\le\bar u$ of (6.3) between the Perron envelopes

$$\bar u(t,\omega) = \inf\{\varphi(t,\mathbf 0):\varphi\in\overline{\mathcal D}(t,\omega)\},\qquad \underline u(t,\omega) = \sup\{\varphi(t,\mathbf 0):\varphi\in\underline{\mathcal D}(t,\omega)\};$$

Lemma 6.3 (classical solutions built from an ODE with random coefficients); and Theorem 6.1, $\underline u = \bar u$.

Significance

Theorem 4.6 makes the definition of the paper a well-posed one: existence (Theorem 4.3) without uniqueness would allow any number of solutions, and the comparison principle is what identifies the BSDE value as the solution. It gives a path-dependent nonlinear Feynman–Kac formula, characterising non-Markovian BSDEs analytically, and it is the template on which the fully nonlinear theory, path-dependent games and non-Markovian control were later built.

The result is proved, in this paper, and the proof is not known to have been machine-checked. The formalization contributes a precise Lean account of the definitions (Dupire derivatives through extensions to càdlàg paths, the stopping-time class $\mathcal T^t$, Girsanov measures, the piecewise class $\bar C^{1,2}$) and a checked proof of comparison. Pieces of independent value are a functional Itô formula for $C^{1,2}_b$ functionals, Girsanov's theorem on the canonical space, comparison for BSDEs, and optimal stopping under the nonlinear expectation $\underline{\mathcal E}^L$.

Difficulty

The classical proof of comparison doubles variables and uses the Crandall–Ishii lemma, which rests on local compactness of the state space; $\Omega$ is infinite-dimensional and not locally compact, so that route fails. The paper instead proves comparison when one side is smooth (Lemma 5.7), and then shows that the Perron envelopes $\underline u$ and $\bar u$, built from piecewise-smooth super- and subsolutions, coincide. That equality needs an approximation of an arbitrary square-integrable BSDE integrand $Z$ by processes that are piecewise differentiable in time with uniformly continuous derivative, so that the resulting functionals lie in $\bar C^{1,2}$ (Lemmas 6.3–6.5). The partial comparison relies on optimal stopping under $\underline{\mathcal E}^L$, which the paper treats with heuristic arguments in Remark 3.11 and references to later work, so that step will need its own development.

Formalization scope

Time is $[0,\infty)$ with a fixed horizon $T$; paths take values in Euclidean $\mathbb R^d$ and are constant after $T$. $\Omega^t$ is encoded as continuous paths vanishing on $[0,t]$ and $\hat\Omega^t$ as càdlàg paths constant on $[0,t]$, so $\Omega = \Omega^0$. Filtrations are the raw ones generated by the canonical process. The Wiener measure is a hypothesis on finite-dimensional laws, and $P^t_0$ is its image under the shift. The stochastic integral and BSDE solutions are those of the platform definition Peng1990.SMP.Stochastic.

Conventions and readings, all disclosed in the items:

• the standing assumptions are Assumptions 4.2 and 4.4 as printed; "continuous in $t$" is for each fixed $(\omega,y,z)$, "uniformly continuous in $\omega$" is one modulus uniform in $(t,y,z)$, and the Lipschitz bound uses $|y-y'|+|z-z'|$;
• $C^{1,2}_b$ membership is witnessed by an extension to càdlàg paths together with its derivatives, and every statement involving derivatives quantifies over all such extensions; by Theorem 2.4(i) of the paper they agree on $\Lambda$;
• the $\min$/$\max$ in the test sets is attained at $\tilde\tau\equiv t$, so the test condition is written as "every Girsanov expectation is $\ge0$" (resp. $\le0$), with integrability required; no real infimum or supremum is formed, and Theorem 6.1 is stated with greatest lower and least upper bounds;
• $u^0$ is characterised by the BSDE, not constructed: the statements quantify over every $u$ satisfying the characterisation, which by Pardoux–Peng holds for exactly one $u$;
• in (6.2) and (5.11) the sign of the operator is required $P^t_0$-a.s. for $s\in[t,T)$;
• Lemma 6.3 adds Assumption 4.4, which the page omits although (6.8) uses $\hat f$, and reads "$\theta=\hat\theta$ in $\Lambda$" as $\Lambda^t$.

No trivializing reading is available: the test functions are exactly the $C^{1,2}_b(\Lambda^t)$ functionals satisfying (3.6), the measures exactly the Girsanov measures with $|\beta^i|\le L$, and the stopping times exactly $\mathcal T^t$. A test set that is too large makes sub- and supersolutions scarce and the comparison principle weaker, a test set that is too small makes them abundant and the principle false, and neither is the case here.

The source is arXiv:1109.5971v2, the IMS electronic reprint of the Annals of Probability article; its printed page numbers equal the PDF's. Lemmas 6.4 and 6.5 (the approximation of $Z$) are part of the proof but not stated as items. Contributions welcome: the functional Itô formula, Girsanov on $\Omega^t$, BSDE comparison and stability, and the optimal stopping theory under $\underline{\mathcal E}^L$.

Selected references

• I. Ekren, C. Keller, N. Touzi, J. Zhang, On viscosity solutions of path dependent PDEs, Ann. Probab. 42(1) (2014) 204–236. arXiv:1109.5971, doi:10.1214/12-AOP788
• B. Dupire, Functional Itô calculus, Bloomberg Portfolio Research Paper 2009-04 (2009). SSRN 1435551
• R. Cont, D.-A. Fournié, Functional Itô calculus and stochastic integral representation of martingales, Ann. Probab. 41(1) (2013) 109–133. arXiv:1002.2446
• É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14 (1990) 55–61. doi:10.1016/0167-6911(90)90082-6
• I. Ekren, N. Touzi, J. Zhang, Viscosity solutions of fully nonlinear parabolic path dependent PDEs: Part I, Ann. Probab. 44(2) (2016) 1212–1253. arXiv:1210.0006

Motivation

A mean field game describes the Nash equilibria of $n$ symmetric players whose states interact only through their empirical distribution, in the limit $n\to\infty$. The law of large numbers for the equilibria — convergence of the empirical measure of the $n$-player equilibrium to the mean field equilibrium — was proved in the diffusion setting by Cardaliaguet, Delarue, Lasry and Lions through the master equation (arXiv:1509.02505), and refined by Delarue, Lacker and Ramanan into fluctuation estimates and a central limit theorem in a companion paper (Electron. J. Probab. 2019). The next question is the size of rare deviations: the probability that the $n$-player equilibrium empirical measure flow stays near a flow different from the mean field limit decays exponentially in $n$, and the exponent is a rate function. Delarue, Lacker and Ramanan (arXiv:1804.08550) prove such a large deviation principle (LDP), including the case of a common noise affecting all players, for which no LDP was previously known even for McKean–Vlasov particle systems.

Timeline. Dawson and Gärtner (1987) proved the LDP for the empirical measure flows of weakly interacting diffusions without common noise, with time-independent coefficients and deterministic initial states, using the action functional adopted here. Budhiraja, Dupuis and Fischer (Ann. Probab. 2012) gave a weak-convergence proof for the empirical measure of paths. For mean field games, master-equation methods gave limit theorems, including LDPs, for finite state spaces without common noise (Cecchin–Fischer, arXiv:1704.00984; Cecchin–Pelino, arXiv:1707.01819; Bayraktar–Cohen, arXiv:1707.02648), and Lacker and Ramanan proved an LDP for static games (arXiv:1702.02113). The present paper (arXiv v1, 2018; Ann. Probab. 2020) treats diffusion-based games, with common noise.

Setting

On a filtered probability space $(\Omega,\mathcal F,\mathbb F,\mathbb P)$ live a $d_0$-dimensional Brownian motion $W$ (the common noise), independent $d$-dimensional Brownian motions $B^1,B^2,\dots$, and i.i.d. initial states $X^1_0,X^2_0,\dots$ with law $\mu_0$. The whole initial-state family is independent of the joint noise family, as specified for (6.1). Player $i$ of $n$ controls

$$dX^i_t=b(X^i_t,m^n_{\boldsymbol X_t},\alpha^i_t)\,dt+\sigma\,dB^i_t+\sigma_0\,dW_t,\qquad m^n_{\boldsymbol x}=\frac1n\sum_{i=1}^n\delta_{x_i},$$

with running cost $f$ and terminal cost $g$. With the Hamiltonian $H(x,m,y)=\inf_a[b(x,m,a)\cdot y+f(x,m,a)]$, its minimizer $\hat\alpha$ and $\hat b(x,m,y)=b(x,m,\hat\alpha(x,m,y))$, a classical solution $(v^{n,i})_i$ of the Nash system (2.6) gives the equilibrium states

$$dX^i_t=\hat b\big(X^i_t,m^n_{\boldsymbol X_t},D_{x_i}v^{n,i}(t,\boldsymbol X_t)\big)dt+\sigma\,dB^i_t+\sigma_0\,dW_t. \qquad (2.7)$$

The master equation (2.8) is a PDE for $U(t,x,m)$ on $[0,T]\times\mathbb R^d\times\mathcal P^2(\mathbb R^d)$ involving derivatives in the measure argument. Assumption A asks for Lipschitz $\hat b$ (with exponent $p^*\in[1,2]$ for the Wasserstein metric), non-degenerate $\sigma$, $p'>4$ moments of $\mu_0$, classical solutions of the Nash systems, and a classical solution $U$ of the master equation with bounded derivatives; B or B′ controls $\hat f$.

The state space is $C([0,T];\mathcal P^1(\mathbb R^d))$: flows $\nu=(\nu_t)$ of probability measures with finite first moment, continuous for the 1-Wasserstein distance $\mathcal W_1$, with the uniform metric $\sup_t\mathcal W_1(\nu_t,\nu'_t)$. The rate function uses the drift $\tilde b(t,x,m)=\hat b(x,m,D_xU(t,x,m))$ and the Dawson–Gärtner action functional

$$I(\nu)=\frac12\int_0^T\big\|\dot\nu_t-\mathcal L^*_{t,\nu_t}\nu_t\big\|^2_{\nu_t}\,dt,\qquad \mathcal L_{t,m}\varphi=\tfrac12\mathrm{Tr}[\sigma\sigma^\top D^2\varphi]+D\varphi\cdot\tilde b(t,\cdot,m),$$

with $\|\gamma\|^2_m=\sup_\varphi\langle\gamma,\varphi\rangle^2/\langle m,|D\varphi|^2\rangle$ over test functions, and $I=\infty$ off absolutely continuous paths. With common noise, the drift is shifted along the mean path: $\tilde I^\phi$ is $I$ for the drift $\tilde b(t,x+\phi_t,m\circ\tau^{-1}_{-\phi_t})$, $\tau_x(z)=z-x$, and

$$J^{\sigma_0}(\nu)=\tilde I^{\mathbb M^{\tilde b,\nu}}\big((\nu_t\circ\tau^{-1}_{\mathbb M^{\tilde b,\nu}_t})_t\big),\quad \mathbb M^{\tilde b,\nu}_t=\sigma\Pi_{\sigma^{-1}\sigma_0}\sigma^{-1}\Big(\int x\,d(\nu_t-\nu_0)-\int_0^t\langle\nu_s,\tilde b(s,\cdot,\nu_s)\rangle ds\Big),$$

where $\Pi_{\sigma^{-1}\sigma_0}$ is the orthogonal projection onto the image of $\sigma^{-1}\sigma_0$. $\mathcal R$ is relative entropy.

Formalization targets

Goal: Theorem 3.10 (weak LDP, common noise allowed)

If $p^*=1$, A and B or B′ hold, and $\int e^{\lambda|x|}\mu_0(dx)<\infty$ for every $\lambda>0$, then for open $O$, compact $K$ and closed $F$,

$$\liminf_n\tfrac1n\log\mathbb P(m^n_{\boldsymbol X}\in O)\ge-\inf_O\big(J^{\sigma_0}+\mathcal R(\cdot_0|\mu_0)\big),\qquad \limsup_n\tfrac1n\log\mathbb P(m^n_{\boldsymbol X}\in K)\le-\inf_K\big(J^{\sigma_0}+\mathcal R(\cdot_0|\mu_0)\big),$$ $$\limsup_n\tfrac1n\log\mathbb P(m^n_{\boldsymbol X}\in F)\le-\lim_{\delta\searrow0}\inf_{F_\delta}\big(J^{\sigma_0}+\mathcal R(\cdot_0|\mu_0)\big).$$

Milestones

Exponential equivalence of the Nash flows and the McKean–Vlasov particle flows (Corollary 6.1); a weak LDP for the noises and initial states (Proposition 6.15); uniform continuity of the McKean–Vlasov solution map (Lemma 6.16); the shifted action (Lemma 6.4); identification of the contracted entropy (Lemma 6.17); the weak LDP for general weakly interacting systems with common noise (Theorem 6.8) and its transfer to the Nash flows (Theorem 6.13); compactness after centering (Proposition 6.11); removal of the $\delta$-relaxation on compacts, and the full LDP without common noise (Proposition 6.10); explicit forms of $J^{\sigma_0}$ (Proposition 6.5, Theorem 6.6). A companion item states Theorem 3.9: without common noise, a full LDP with the good rate function $I(\nu)+\mathcal R(\nu_0|\mu_0)$.

Significance

The result quantifies how unlikely atypical equilibrium behaviour is in large games: rare macroscopic deviations of the equilibrium empirical measure flow cost $\exp(-n\,\mathrm{rate})$, and the rate function makes explicit that the common noise moves the mean of the population for free in the directions of the image of $\sigma_0$. When $\sigma_0\ne0$ the rate function has non-compact level sets, which is why the principle is weak and why the closed-set bound carries the $\delta$-relaxation.

The proof transfers the LDP from the McKean–Vlasov particle system to the Nash system through the master equation, a method that applies beyond this model. Nothing in this paper is formalized: there is no large deviation principle, no Wasserstein space of measure flows, no derivative on Wasserstein space and no mean field game on the platform. A formal development produces reusable definitions (weak and full LDPs, the Dawson–Gärtner action functional, $C([0,T];\mathcal P^1)$) and checked proofs of the contraction and exponential-equivalence steps. The exponential estimate behind Corollary 6.1 (Theorem 4.3) is the companion mission's milestone and rests on estimates quoted from the companion central-limit-theorem paper.

Difficulty

The obvious route — exponential equivalence plus the Dawson–Gärtner LDP for the particle system — fails twice. The particle drift $\tilde b$ is time-dependent and the initial states are random, which the classical results do not cover; and with common noise there is no LDP to transfer. The proof instead freezes the noise: it proves a weak LDP for the pair (empirical measure of initial states and idiosyncratic paths, common noise path), which needs Sanov's theorem in the $\mathcal W_1$ topology and the Brownian support theorem, and contracts it through the McKean–Vlasov solution map. The contraction principle requires the rate function to be good, and it is not when $\sigma_0\ne0$; uniform continuity of the solution map and the $\delta$-enlargements replace goodness.

Formalization scope

Time is $[0,T]\subset\mathbb R_{\ge0}$ with $T>0$; paths are continuous maps on $[0,T]$, and solutions of the SDEs are path-valued, adapted, and satisfy the integral equations almost surely. Players are indexed from $0$. Probability measures with finite $p$-th moment are guarded by an explicit predicate, and $\mathcal W_p$ is the published WassersteinDRO.Duality.wassersteinDistance, kept in $[0,\infty]$. Derivatives in $x$, $v$, $t$ are genuine derivatives; derivatives in the measure are normalized flat-derivative witnesses. Relative entropy is Mathlib's klDiv. Logarithms of probabilities are in $[-\infty,\infty]$; open, closed and compact sets are those of the uniform $\mathcal W_1$ metric, and $\lim_{\delta\searrow0}$ is a supremum over $\delta>0$. The action functional is an infimum over all distributional time derivatives, with test functions and distributions from Mathlib. The common-noise paths are $d_0$-dimensional.

Standing assumptions are carried explicitly: the filtered space and noises of §2.3, joint independence of initial states and noises from §6.1, Assumption A (with the Borel measurability of $b,f,g$), B or B′, $p^*=1$ where the paper assumes it, and, for §6, Condition 6.3 and non-degenerate $\sigma$. Two disclosed additions: Theorems 3.9, 3.10 and 6.13 assume $\tilde b$ bounded (Condition 6.3(2) requires it; Assumption A does not imply it), and Theorem 6.13 assumes $p^*=1$. The solutions of the Nash systems, the master equation and the SDEs are hypotheses; existence is not posed.

A rate function identically $0$ or $\infty$, or bounds over a restricted family of sets, would trivialize the statements: the seminorm is a supremum over all test functions, $I=\infty$ exactly off absolutely continuous flows, and the bounds quantify over every open, compact or closed set. A complete development needs Sanov's theorem in $\mathcal W_1$, the Brownian support theorem, the contraction principle, Dawson–Gärtner's analysis of distribution-valued paths, and stochastic calculus for the particle systems; each of these is reusable, and contributions to any of them are welcome.

Selected references

• F. Delarue, D. Lacker, K. Ramanan, From the master equation to mean field game limit theory: large deviations and concentration of measure, Ann. Probab. 48(1), 2020; arXiv v1, 2018. https://arxiv.org/abs/1804.08550
• F. Delarue, D. Lacker, K. Ramanan, From the master equation to mean field game limit theory: a central limit theorem, Electron. J. Probab. 24, 2019 (reference [19] of the paper).
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The master equation and the convergence problem in mean field games, Ann. Math. Studies 201, 2019. https://arxiv.org/abs/1509.02505
• D. Dawson, J. Gärtner, Large deviations from the McKean–Vlasov limit for weakly interacting diffusions, Stochastics 20(4), 1987, 247–308.
• A. Budhiraja, P. Dupuis, M. Fischer, Large deviation properties of weakly interacting processes via weak convergence methods, Ann. Probab. 40(1), 2012, 74–102.
• R. Wang, X. Wang, L. Wu, Sanov's theorem in the Wasserstein distance: a necessary and sufficient condition, Statist. Probab. Lett. 80(5), 2010, 505–512.
• A. Cecchin, G. Pelino, Convergence, fluctuations and large deviations for finite state mean field games via the master equation, 2017. https://arxiv.org/abs/1707.01819
• D. Lacker, K. Ramanan, Rare Nash equilibria and the price of anarchy in large static games, 2017. https://arxiv.org/abs/1702.02113