Probability

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.

Why ask whether a Wasserstein distance is Hilbertian

Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance $d$ on a set $\mathcal Z$ is Hilbertian when $\mathcal Z$ can be mapped into a Hilbert space so that $d$ becomes the norm distance; for such a $d$, the kernel $e^{-d^p/t}$ is positive definite for $0\le p\le 2$ and $t>0$ (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for $\mathcal W_2$: the map sending a measure to its quantile function is an isometry into $L^2([0,1])$, and between univariate Gaussians $\mathcal W_2$ is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for $p=1,2$ and $d\ge2$ the $p$-Wasserstein distance on $\mathbb R^d$ is not Hilbertian (Proposition 8.2, p. 507).

The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar $\mathcal W_1$ does not even embed into $L^1$ with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.

Setting

Let $\mathcal Z$ be a set. A function $\varphi:\mathcal Z\times\mathcal Z\to\mathbb R$ is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every $n\ge0$, every $x_1,\dots,x_n\in\mathcal Z$ and every $r\in\mathbb R^n$ with $\sum_ir_i=0$,

$$\sum_{i,j=1}^n r_ir_j\,\varphi(x_i,x_j)\le0 .$$

A function $d:\mathcal Z\times\mathcal Z\to\mathbb R$ is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space $\mathcal H$ and a map $\phi:\mathcal Z\to\mathcal H$ with $d(z,z')=\|\phi(z)-\phi(z')\|_{\mathcal H}$ for all $z,z'$.

On $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$, let $\mathcal P_p(\mathbb R^d)$ be the Borel probability measures $\mu$ with $\int\|x\|_2^p\,d\mu<\infty$. A coupling of $\mu$ and $\nu$ is a measure $\pi$ on $\mathbb R^d\times\mathbb R^d$ whose two marginals are $\mu$ and $\nu$, and the $p$-Wasserstein distance (2.18) is

$$\mathcal W_p(\mu,\nu)=\Big(\inf_{\pi}\int\|x-y\|_2^p\,d\pi(x,y)\Big)^{1/p},$$

finite on $\mathcal P_p(\mathbb R^d)$. For points $x_1,\dots,x_n$ and a histogram $a\in\Sigma_n$ (nonnegative, summing to one) the discrete measure is $\sum_ia_i\delta_{x_i}$; for two histograms $a,b$, $U(a,b)$ is the set of nonnegative matrices with row sums $a$ and column sums $b$, and $L_C(a,b)=\min_{P\in U(a,b)}\sum_{i,j}C_{i,j}P_{i,j}$ (2.11).

The configuration of the book's proof consists of the corners $x^1=[0,0]$, $x^2=[1,0]$, $x^3=[0,1]$, $x^4=[1,1]$ of the unit square, the 35 histograms of $\Sigma_4$ with entries in $\{0,\tfrac14,\tfrac12,\tfrac34,1\}$, and the centering matrix $J=I_n-\tfrac1n\mathbb 1_{n,n}$.

Formalization targets

Goal: Proposition 8.2

For $d\ge2$ and $p\in\{1,2\}$,

$$\mathcal W_p \text{ on } \mathcal P_p(\mathbb R^d) \text{ is not Hilbertian.}$$

Milestones

1. Proposition 8.1, proved direction (pp. 506–507): if $d$ is Hilbertian then $d^2$ is negative definite.
2. Squared distance (p. 507): $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$ is not negative definite, $d\ge2$, $p=1,2$.
3. Reduction to the plane (proof of Prop. 8.2): if $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^d)$, $d\ge2$, were negative definite, so would be $\mathcal W_p^2$ on $\mathcal P_p(\mathbb R^2)$.
4. Discrete measures (Remark 2.13, p. 375): $\mathcal W_p\big(\sum_ia_i\delta_{x_i},\sum_jb_j\delta_{x_j}\big)^p=L_C(a,b)$ with $C_{i,j}=\|x_i-x_j\|_2^p$.
5. Centering criterion (proof of Prop. 8.2): a matrix $M$ admits a zero-sum $r$ with $r^\top Mr>0$ if and only if $JMJ$ has a positive eigenvalue.
6. The grid counterexample (proof of Prop. 8.2, Figure 8.6): for $p=1,2$ there are grid histograms $a^1,\dots,a^n$ and a zero-sum $r$ with

$$\sum_{i,j}r_ir_j\,\mathcal W_p^2\Big(\sum_k a^i_k\delta_{x^k},\sum_k a^j_k\delta_{x^k}\Big)>0.$$

Significance

A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for $\mathcal W_1$ or $\mathcal W_2$ on $\mathbb R^d$, $d\ge2$, by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.

The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.

Difficulty

The abstract part is short: expanding $\|\phi(z_i)-\phi(z_j)\|^2$ and using $\sum_ir_i=0$ gives milestone 1. The obstacle is the certificate. The book observes that $J\mathbf D_p^2J$ has a positive top eigenvalue (about $1.2$ for $p=1$ and $0.7$ for $p=2$), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector $r$ for which the quadratic form is provably positive. For $p=1$ the costs involve $\sqrt2$, the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic $\mathcal W_p$ to the discrete program (milestone 4) and transporting a counterexample from $\mathbb R^2$ into $\mathbb R^d$ (milestone 3), both of which require working with couplings as measures on a product space.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\mathcal W_p$ is the published definition WassersteinDRO.Duality.wassersteinDistance (an $[0,\infty]$-valued infimum over all measures with the two marginals, raised to $1/p$), converted to a real number. The distance is considered on $\mathcal P_p(\mathbb R^d)$, the set where it is finite; outside it the real conversion is a junk $0$. The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on $\mathcal P_p$ and on every smaller set containing those measures.
• Negative definiteness is conditional. Definition 8.3 as printed quantifies over all $r$; under that reading no nonzero squared distance is negative definite, so Proposition 8.1 would be false and "not negative definite" trivially true. The zero-sum condition, used by the book in the proof of Proposition 8.1, is part of the definition; this rules out the trivial formalization.
• Hilbert spaces are real, complete inner-product spaces in the universe of $\mathcal Z$. Indices are 0-based (Fin n). Histograms are real vectors; the reduction milestone is stated for every $p\ge1$.
• Discrete transport objects ($U(a,b)$, $L_C$) are redefined in this mission's namespace CompOT.NotHilbertian, duplicating chunk II of the series.

Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of $\mathcal W_p$, and exact certificates for the grid computation.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
• I. J. Schoenberg, Metric spaces and positive definite functions, Transactions of the AMS 44(3):522–536, 1938. https://doi.org/10.1090/S0002-9947-1938-1501980-0
• C. Berg, J. P. R. Christensen and P. Ressel, Harmonic Analysis on Semigroups, Graduate Texts in Mathematics 100, Springer, 1984. https://doi.org/10.1007/978-1-4612-1128-0
• A. Naor and G. Schechtman, Planar earthmover is not in $L_1$, SIAM Journal on Computing 37(3):804–826, 2007. https://doi.org/10.1137/05064206X
• A. Andoni, A. Naor and O. Neiman, Snowflake universality of Wasserstein spaces, Annales scientifiques de l'École normale supérieure 51(3):657–700, 2018. https://arxiv.org/abs/1509.08677

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

On a Riemannian manifold, a lower bound $\mathrm{Ric}\ge K$ together with a dimension bound $N$ can be read off from the heat flow alone. This is the Bakry–Émery curvature-dimension condition $BE(K,N)$: Bochner's inequality $\Gamma_2(f)\ge K\,\Gamma(f)+\tfrac1N(\Delta f)^2$ for the iterated carré du champ. The condition makes sense for any diffusion: weighted manifolds, infinite-dimensional Gaussian spaces, and limits of manifolds where no Ricci tensor exists. For this reason it is one of the two main routes to synthetic curvature bounds, the other being the optimal-transport conditions of Lott–Villani and Sturm. Bakry–Émery 1985; Bakry–Gentil–Ledoux 2014.

Ambrosio, Gigli and Savaré prove that, on metric measure spaces, $BE(K,\infty)$ for the Cheeger energy is equivalent to the transport condition $RCD(K,\infty)$. Their first step (§2.2) is to state $BE(K,N)$ for an abstract Dirichlet form, in a weak form and under minimal regularity, and to show that the usual ways of writing it are equivalent. That equivalence, Corollary 2.3, is the subject of this mission. Every later section of the paper and the remaining missions of this series use one of its forms. arXiv:1209.5786v4, §2.2, pp. 14–20.

Setting

Let $(X,\mathcal B)$ be a measurable space with a $\sigma$-additive measure $m$.

• A symmetric Dirichlet form is a functional $\mathcal E:L^2(X,m)\to[0,\infty]$ that is quadratic and $L^2$-lower semicontinuous, satisfies $\mathcal E(\eta\circ f)\le\mathcal E(f)$ for every 1-Lipschitz $\eta$ with $\eta(0)=0$, and has a dense domain $\mathbb V=\{f:\mathcal E(f)<\infty\}$.
• Write $\mathcal E(f,g)$ for its bilinear form and $\mathbb V_\infty=\mathbb V\cap L^\infty$.
• $\mathcal E$ is strongly local if $\mathcal E(f,g)=0$ whenever $(f+a)g=0$ a.e. for some constant $a$.
• The generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int_X g\,\Delta_{\mathcal E}f\,dm$ for all $g\in\mathbb V$, and the heat flow $\mathsf P_t$ solves $\partial_t\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$ with $\mathsf P_tf\to f$ in $L^2$. By contraction, $\mathsf P_t$ extends to $L^1(X,m)$.

For $f,g,\varphi\in\mathbb V_\infty$ set

$$\Gamma[f,g;\varphi]=\tfrac12\big(\mathcal E(f,g\varphi)+\mathcal E(g,f\varphi)-\mathcal E(fg,\varphi)\big),\qquad \Gamma[f;\varphi]=\Gamma[f,f;\varphi].$$

By continuity, this extends to $f,g\in\mathbb V$, $\varphi\in\mathbb V_\infty$. The set $\mathbb G$ consists of those $f\in\mathbb V$ for which $\varphi\mapsto\Gamma[f;\varphi]$ has a density $\Gamma(f)\in L^1_+(X,m)$, the carré du champ. The iterated form is

$$\Gamma_2[f;\varphi]=\tfrac12\Gamma[f;\Delta_{\mathcal E}\varphi]-\Gamma[f,\Delta_{\mathcal E}f;\varphi].$$

Along the heat flow, for $t>0$ and $s\in[0,t]$, set

$$\mathsf A_t[f;\varphi](s)=\tfrac12\!\int_X(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,\qquad \mathsf A^\Delta_t[f;\varphi](s)=\tfrac12\!\int_X(\Delta_{\mathcal E}\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,dm,$$

$\mathsf B_t[f;\varphi](s)=\Gamma[\mathsf P_{t-s}f;\mathsf P_s\varphi]$ and $\mathsf C_t[f;\varphi](s)=\Gamma_2[\mathsf P_{t-s}f;\mathsf P_s\varphi]$. Finally $I_K(t)=\int_0^te^{Ks}ds$, $I_{K,2}(t)=\int_0^tI_K(s)ds$, and $\nu=1/N\ge0$.

Formalization targets

Goal: Corollary 2.3

Let $K\in\mathbb R$ and $\nu\ge0$. The following are equivalent:

• (i) $\Gamma_2[f;\varphi]\ge K\Gamma[f;\varphi]+\nu\int_X(\Delta_{\mathcal E}f)^2\varphi\,dm$ for every $(f,\varphi)\in D(\Gamma_2)$ with $\varphi\ge0$;
• (ii) $\mathsf C_t[f;\varphi](s)\ge K\mathsf B_t[f;\varphi](s)+2\nu\mathsf A^\Delta_t[f;\varphi](s)$ for $0\le s<t$;
• (iii) the distributional inequality

$$\partial_s^2\mathsf A_t[f;\varphi]\ge2K\,\partial_s\mathsf A_t[f;\varphi]+4\nu\,\mathsf A^\Delta_t[f;\varphi]\quad\text{in }\mathscr D'(0,t);$$

• (iv) $\mathsf P_tf\in\mathbb G$ and $I_{2K}(t)\Gamma(\mathsf P_tf)+2\nu I_{2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2$ a.e.;
• (v) $\mathbb G=\mathbb V$ and, for $f\in\mathbb V$, $t>0$, $\tfrac12\mathsf P_t(f^2)-\tfrac12(\mathsf P_tf)^2+2\nu I_{-2K,2}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le I_{-2K}(t)\mathsf P_t\Gamma(f)$ a.e.;
• (vi) $\mathbb G$ is dense in $L^2$, and for $f\in\mathbb G$, $t>0$,

$$\Gamma(\mathsf P_tf)+2\nu I_{-2K}(t)(\Delta_{\mathcal E}\mathsf P_tf)^2\le e^{-2Kt}\mathsf P_t\Gamma(f)\quad\text{a.e.}$$

Any of them implies $\mathbb G=\mathbb V$. Condition (iii) is the paper's definition of $BE(K,N)$ (Definition 2.4).

Milestones

1. Lemma 2.1, in four parts:
   • $\mathsf A$ is continuous, $\mathsf A^\Delta$ is continuous, and $\partial_s\mathsf A=\mathsf B$ (2.25);
   • $\mathsf A$ and $\mathsf A^\Delta$ are monotone for $\varphi\ge0$;
   • $\partial_s\mathsf B=2\mathsf C$ (2.26).
2. Lemma 2.2: four equivalent forms of the scalar inequality $a''\ge2Ka'+\nu g$.
3. Its integrated consequences (2.30) and (2.31).

Significance

The result. Condition (i) is the classical Bochner inequality. (iii) is the form that survives limits and is used as a definition. (iv), (v) and (vi) are pointwise estimates for the heat flow: the reverse and the local Poincaré inequalities, and the Bakry–Émery gradient bound $\Gamma(\mathsf P_tf)\le e^{-2Kt}\mathsf P_t\Gamma(f)$. Section 3 of the paper uses (vi) to obtain Lipschitz regularization and to identify the intrinsic distance. Section 4 uses (iii) with $\nu=0$ to prove the $RCD(K,\infty)$ property. The conclusion $\mathbb G=\mathbb V$ means that a $BE$ form automatically admits a carré du champ on its whole domain, so $\Gamma$-calculus is available without extra assumptions.

Formalizing it. The equivalences are classical for smooth diffusions with an algebra of nice functions. The paper's contribution is to prove them for an arbitrary strongly local Dirichlet form, where no such algebra is assumed. The result is proved; it is not formalized. The mission produces a Lean interface for Dirichlet forms, their heat flows, the extended $\Gamma$ and $\Gamma_2$, and the six conditions. Proofs of the milestones and of the goal are open.

Difficulty

The obvious argument differentiates $s\mapsto\mathsf A_t[f;\varphi](s)$ twice and reads off $\mathsf A''=2\Gamma_2$. That requires $f$, $\varphi$ and $\Delta_{\mathcal E}\varphi$ to be smooth enough for every term to be defined. For a general $f\in L^2$ only the first derivative exists, as $\Gamma[\cdot;\cdot]$ on $\mathbb V\times\mathbb V_\infty$, and only through the continuity extension (2.20). The weak forms must therefore be reached by truncation and semigroup mollification.

The passage from the integrated inequality (iv) to the existence of the density $\Gamma(\mathsf P_tf)$ is not a computation either. It needs a Daniell-type construction of a measure from a positive functional on $\mathbb V_\infty$. The converse directions, from (iv) or (vi) back to (iii), require a second-order Taylor expansion in time of quantities whose regularity is only that of Lemma 2.1.

Formalization scope

• Representation. An element of $L^2$ is a function with MemLp f 2 m, and every predicate is invariant under a.e. equality. $\mathcal E$ takes values in $[0,\infty]$, with $\infty$ off $L^2$. The completion of $\mathcal B$ is not modelled.
• Binders. The heat flow and its $L^1$ extension are binders, pinned by characterizing predicates. Generator values and carré du champ densities are witnesses, which are unique a.e.
• Γ and Γ₂. They are predicates "the value is $c$": approximating sequences exist, and along each of them $\Gamma$ converges to $c$. The paper defines $\Gamma$ only on $\mathbb V\times\mathbb V\times\mathbb V_\infty$, so $\Gamma_2[f;\varphi]$ is undefined when $\Delta_{\mathcal E}\varphi\notin\mathbb V$, and (i)–(ii) are required wherever it is defined.
• Weak forms. Distributional inequalities are tested against nonnegative smooth functions compactly supported in $(0,t)$, after integration by parts. This avoids derivatives at points where none exists.
• Standing assumptions and constants. The strong locality and density assumptions of (2.1) are standing binders; there is no topology and no mass preservation. $K\in\mathbb R$ is free and $\nu\ge0$. $I_K$ is defined by its integral, so $K=0$ needs no separate case.
• Departures from the page.
  • In condition (v) the coefficient of $\mathsf P_t\Gamma(f)$ is $I_{-2K}(t)$. The page prints $I_{-2K,2}(t)$, which makes (v) false for small $t$ already for the heat flow on $\mathbb R$; the paper's derivation of (v) from (2.31) gives $I_{-2K}(t)$. (v) is stated for $t>0$; at $t=0$ both sides vanish.
  • In Lemma 2.2 (iii), test functions are required to be nonnegative, since (2.27) fails for $-\zeta$.
  • In Lemma 2.2 (iv), $s_2<t$ is required.
• Not a trivialization. The admissible test classes are nonempty, the conditions are not vacuous, and the hypotheses are satisfiable: the zero form with the identity flow satisfies them and $BE(K,\infty)$ for every $K$, verified in Lean.
• Shared layer. The setting module carries the paper's metric-measure definitions for the series and is reusable for any Dirichlet-form development, as is the interval lemma 2.2.

Proofs of any milestone are welcome. Each proved milestone is usable independently: Lemma 2.2, (2.30) and (2.31) are real-variable statements.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. Pinned preprint arXiv:1209.5786v4, §2, pp. 10–20.
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 1985. https://doi.org/10.1007/BFb0075847
• D. Bakry, I. Gentil, M. Ledoux, Analysis and Geometry of Markov Diffusion Operators, Springer, 2014. https://doi.org/10.1007/978-3-319-00227-9

Motivation

A McKean–Vlasov stochastic differential equation, or distribution dependent SDE, is an SDE whose coefficients depend on the law of the solution itself:

$$dX(t) = b\big(t, X(t), \mathcal L_{X(t)}\big)\,dt + \sigma\big(t, X(t), \mathcal L_{X(t)}\big)\,dW(t),$$

where $\mathcal L_{X(t)}$ is the law of $X(t)$. Such equations describe the limit of large systems of interacting particles (mean-field limits), and they are the probabilistic side of nonlinear Fokker–Planck equations: by Itô's formula the time marginals $\mu_t = \mathcal L_{X(t)}$ solve a Fokker–Planck equation whose coefficients depend on $\mu_t$.

Most existence theory for McKean–Vlasov SDEs assumes that the coefficients are continuous, often Lipschitz, in the measure argument for a Wasserstein distance. That excludes the Nemytskii-type dependence $b(X(t), u(t, X(t)))$, where $u(t,\cdot)$ is the density of $\mathcal L_{X(t)}$ evaluated at the current position. This dependence appears in models of nonlinear diffusion and porous media, where the diffusion speed depends on the local concentration. V. Barbu and M. Röckner (arXiv:1808.10706, Ann. Probab. 2020) reverse the usual direction: they first solve the nonlinear Fokker–Planck equation in $L^1$ by nonlinear semigroup theory and then construct the SDE from its solution.

Earlier results covered the case $a_{ij}(x,u) = \delta_{ij}\beta(u)$, as recorded in Remark 4.2 of the paper. Benachour, Chassaing, Roynette and Vallois (Ann. Sc. Norm. Sup. Pisa, 1996) treated $d = 1$, $b \equiv 0$, $\beta(r) = r|r|^{m-1}$. Blanchard, Röckner and Russo (Ann. Probab. 38, 2010) and Barbu, Röckner and Russo (Probab. Theory Relat. Fields, 2011) treated $d = 1$, $b \equiv 0$ with irregular $\beta$, the latter in the degenerate case. Barbu and Röckner (SIAM J. Math. Anal. 50, 2018) treated a maximal monotone $\beta$ with a drift $b(u)$ satisfying (H3)′.

Setting

Let $d \ge 1$, $x \in \mathbb R^d$, and let $a_{ij}, b_i : \mathbb R^d \times \mathbb R \to \mathbb R$, $1 \le i,j \le d$. The nonlinear Fokker–Planck equation (3.1) is

$$\frac{\partial u}{\partial t} - \sum_{i,j=1}^d D^2_{ij}\big(a_{ij}(x,u)u\big) + \operatorname{div}\big(b(x,u)u\big) = 0, \qquad u(0,\cdot) = u_0 .$$

Two sets of hypotheses are considered. (H1)–(H3) (nondegenerate): $a_{ij}$ is $C^2$, bounded, with bounded $x$-gradient, symmetric; $\sum_{i,j}(a_{ij} + u\,\partial_ua_{ij})\xi_i\xi_j \ge \gamma|\xi|^2$ for some $\gamma > 0$; $b_i$ is bounded, $C^1$, and $b_i(x,0) = 0$. (H1)′–(H3)′ (degenerate): the coefficients do not depend on $x$, and the quadratic form above is only nonnegative.

The equation is written as an evolution equation $u' + Au = 0$ in $L^1(\mathbb R^d)$, with the operator $Au = -\sum_{i,j}D^2_{ij}(a_{ij}(x,u)u) + \operatorname{div}(b(x,u)u)$ taken in the sense of distributions and domain $D(A) = \{u \in L^1 : Au \in L^1\}$. An operator is m-accretive if $I + \lambda A$ is onto with a contractive inverse for every $\lambda > 0$. A mild solution is the uniform limit of the implicit Euler scheme $u_h^i + hAu_h^i = u_h^{i-1}$. The paper calls a mild solution a weak solution of (3.1).

The SDE of the main theorem is

$$dX(t) = b\big(X(t), u(t,X(t))\big)\,dt + \sqrt2\,\sigma\big(X(t), u(t,X(t))\big)\,dW(t), \quad 0 \le t \le T, \qquad u(t,\cdot) = \frac{d\mathcal L_{X(t)}}{dx}, \tag{4.1}$$

with $\sigma : \mathbb R^d \times \mathbb R \to L(\mathbb R^d;\mathbb R^d)$ measurable and $a = \sigma\sigma^T$.

Formalization targets

Goal: Theorem 4.1

If $a = \sigma\sigma^T$ and $b$ satisfy (H1)–(H3) or (H1)′–(H3)′ and $u_0$ is a probability density, then (3.1) has a mild solution $u$ with $u(0) = u_0$, and for every $T > 0$ there is a weak solution $X$ of (4.1) on $[0,T]$ with

$$P \circ X(t)^{-1}(dx) = u(t,x)\,dx, \qquad 0 \le t \le T .$$

Milestones

• The PDE layer for (H1)–(H3): Lemmas 3.2 and 3.3 (approximate and $H^1$ solutions of the resolvent equation under the extra smoothness (K)), the $L^1$ contraction (3.22), Proposition 3.1 (the resolvent equation in $L^1$, with contraction, positivity and mass conservation), density of $D(A)$, m-accretivity of $A$, and Theorem 3.4 (existence and uniqueness of the mild solution, properties (3.36)–(3.39)), including preservation of probability densities.
• The cited Crandall–Liggett theorem: an m-accretive operator generates a contraction semigroup of mild solutions.
• The PDE layer for (H1)′–(H3)′: Lemma 3.6, the resolvent properties (3.52)–(3.54), Theorem 3.7.
• The general scheme of §2: a weakly continuous probability solution of a linear Fokker–Planck equation with bounded coefficients is the marginal flow of a weak solution of the corresponding SDE.

Significance

The theorem gives weak existence for a class of distribution dependent SDEs whose coefficients are not continuous in the measure for any weak or Wasserstein topology: they are defined only on measures with a density and read that density at one point. The same construction gives a probabilistic representation of the nonlinear Fokker–Planck equation, which identifies its solutions as one-dimensional time marginals of a stochastic process and is the starting point for particle approximations.

The proofs are written in the literature. This mission formalizes them: the $L^1$ theory of a quasilinear elliptic operator in divergence form, the Crandall–Liggett generation theorem, and the passage from a Fokker–Planck solution to an SDE through the superposition principle. None of these is in Mathlib. The m-accretive operator layer and the superposition step are reusable well beyond this paper.

Difficulty

The natural first idea, a fixed point on the measure argument as in the Lipschitz McKean–Vlasov theory, fails: the map $\mu \mapsto b(x, \frac{d\mu}{dx}(x))$ is not continuous in any topology for which the law map of an SDE is compact, and it is not even defined at measures without density. The paper therefore solves the PDE first. There the obstacle is that $A$ is nonlinear in the highest-order term and, under (H1)′–(H3)′, degenerate. Its resolvent has to be built from $H^1$ solutions on balls under extra smoothness. Its $L^1$ contraction comes from a sign-function argument that needs the monotonicity of $u \mapsto a_{ij}(x,u)u$. Approximation arguments then remove (K) and the nondegeneracy. On the SDE side, the superposition principle needs a solution of the linear equation that is weakly continuous and consists of probability measures. Mass conservation and positivity of the semigroup supply exactly that.

Formalization scope

$\mathbb R^d$ is EthierKurtz.SDEState d, with indices Fin d (0-based) and Lebesgue measure volume. $L^1$ is MeasureTheory.Lp ℝ 1 volume. Coefficients are functions $a_{ij}(x,r)$, $b_i(x,r)$ of the point and of a real number. The degenerate case uses coefficients constant in $x$, and the operator $A_1$ of (3.42) is then literally $A$. Operators are graphs X → X → Prop, and no resolvent is ever chosen. Mild solutions require that the Euler scheme can be run for all small steps, so the notion is not vacuous. Distributional derivatives are always moved onto smooth compactly supported test functions. $H^1$ uses the published weak derivative HunterPDE.Shared.HasWeakDeriv, and $H^1_0(B_N)$ means "in $H^1(\mathbb R^d)$ and zero outside $B_N$". The SDE is the published EthierKurtz.IsWeakSDESolution on $[0,\infty)$ with coefficients switched off after $T$. Its coefficients are evaluated on a jointly measurable version $\tilde u(t,x)$ of the density, which must equal the law of $X(t)$.

Deviations from the page, all disclosed in the statements:

• $a = \sigma\sigma^T$, not the printed $2\sigma\sigma^T$. With noise $\sqrt2\sigma$ the printed factor makes the theorem false (for $d = 1$, $\sigma \equiv 1/\sqrt2$, $b \equiv 0$ the PDE has variance $2t$ and the SDE variance $t$).
• In Lemmas 3.2 and 3.3 the explicit $\lambda_0 = \gamma(b_\infty^2 + c_\infty^2)^{-1}$ is replaced by the existence of some $\lambda_0 > 0$; (3.22) keeps the printed $\lambda_0$, read as $+\infty$ when $b_\infty = c_\infty = 0$.
• In §2 the coefficients are bounded instead of satisfying the integrability Hypothesis 2.1 (ii), and any measurable $\bar\sigma$ with $\bar\sigma\bar\sigma^T = \bar a$ is allowed.
• The typos "$C_b(\mathbb R^d\times\mathbb R^d)$" in (H1) and "$C^1(\mathbb R^d)$" in (H3)′ are read as $C_b(\mathbb R^d\times\mathbb R)$ and $C^1(\mathbb R)$.

A trivializing formalization is ruled out: the goal asserts the existence of the mild solution as well as the SDE for every mild solution, a mild solution must come from a run of the scheme, and the constant $C$ of Lemma 3.3 is fixed before the data. Contributions are welcome at every layer, especially general results on m-accretive operators and the Crandall–Liggett theorem, $L^1$ estimates for quasilinear elliptic equations, and the superposition principle.

Selected references

• V. Barbu, M. Röckner, From nonlinear Fokker–Planck equations to solutions of distribution dependent SDE, Ann. Probab. 48(4), 2020; arXiv:1808.10706v4. https://arxiv.org/abs/1808.10706
• V. Barbu, M. Röckner, Probabilistic representation for solutions to nonlinear Fokker–Planck equations, SIAM J. Math. Anal. 50, 2588–2607, 2018.
• Ph. Blanchard, M. Röckner, F. Russo, Probabilistic representation for solutions of an irregular porous media type equation, Ann. Probab. 38, 1870–1900, 2010.
• V. Barbu, Nonlinear Differential Equations of Monotone Type in Banach Spaces, Springer, 2010. https://doi.org/10.1007/978-1-4419-5542-5
• M. G. Crandall, T. M. Liggett, Generation of semi-groups of nonlinear transformations on general Banach spaces, Amer. J. Math. 93, 1971. https://doi.org/10.2307/2373376
• D. Trevisan, Well-posedness of multidimensional diffusion processes with weakly differentiable coefficients, Electron. J. Probab. 21, 2016. https://doi.org/10.1214/16-EJP4453
• D. W. Stroock, S. R. S. Varadhan, Multidimensional Diffusion Processes, Springer, 1979. https://doi.org/10.1007/3-540-28999-2

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