Probability

Motivation

Mean field control asks a central planner to steer a large population of interacting agents. Each agent's state follows a stochastic differential equation whose coefficients depend on the agent's own state and on the empirical distribution of the population; as the population grows, the system is described by a single McKean–Vlasov equation whose coefficients depend on the law of the solution itself. The planner's value is then a function $V(t,\mu)$ of time and of a probability measure, and its dynamic programming equation, the HJB master equation, is a partial differential equation on the Wasserstein space of measures.

C. Wu and J. Zhang (Ann. Appl. Probab. 30(2), 2020) develop a viscosity theory for such master equations in a path-dependent setting and apply it to McKean–Vlasov control with closed-loop controls, i.e. controls that depend on the observed state path rather than on the driving Brownian motion. Closed-loop information is the natural one when the noise is not observable, and it is the information structure relevant for games; but the value function is then not known to be smooth, so classical solutions are out of reach. This mission formalizes the paper's §5: the value function of the closed-loop problem with piecewise constant controls is a viscosity solution of the HJB master equation.

Setting

Fix $d\ge1$ and a horizon $T$. The path space is $\Omega=C([0,T],\mathbb R^d)$ with the uniform norm, the canonical process is $X_s(\omega)=\omega_s$, and $\mathbb F=(\mathcal F_t)$ is its natural filtration. $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu[\|X\|^2]<\infty$; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$. On $\Theta=[0,T]\times\mathcal P_2$ the pseudometric is

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

with $\mathcal W_2$ the 2-Wasserstein distance on laws of paths.

The data are a control set $A$ and coefficients $b(t,\omega,\mu,a)\in\mathbb R^d$, $\sigma(t,\omega,\mu,a)\in\mathbb R^{d\times d}$, $f(t,\omega,\mu,a)\in\mathbb R$, $g(\omega,\mu)\in\mathbb R$ satisfying Assumption 5.1: measurability and adaptedness, boundedness of $b,\sigma$ by $C_0$, Lipschitz continuity of $b,\sigma$ and uniform continuity of $f,g$ in $(\omega,\mu)$, local uniform continuity in $t$, and positive definiteness of $\sigma\sigma^\top$.

An admissible control $\alpha\in\mathcal A_t$ (5.3) is piecewise constant: $\alpha_s=\sum_{i<n}h_i\mathbf 1_{[t_i,t_{i+1})}(s)$ for a partition $t=t_0<\dots<t_n=T$, with $h_i:\Omega\to A$ $\mathcal F_{t_i}$-measurable. The controlled law $\mathbb P^{t,\mu,\alpha}\in\mathcal P_2$ agrees with $\mu$ on $[0,t]$ and solves, for a Brownian motion $B^\alpha$,

$$X_s=X_t+\int_t^s b\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dr+\int_t^s\sigma\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dB^\alpha_r,\quad s\in[t,T].$$

The value function (3.20) is

$$V(t,\mu)=\sup_{\alpha\in\mathcal A_t}\mathbb E^{\mathbb P^{t,\mu,\alpha}}\Big[g(X,\mathbb P^{t,\mu,\alpha})+\int_t^Tf(s,X,\mathbb P^{t,\mu,\alpha},\alpha_s)\,ds\Big],$$

and $V_0$ is the same supremum over the controls $\mathcal A^0_t$ (5.12) whose pieces depend on the path before $t$ only through finitely many values $X_{s_1},\dots,X_{s_m}$.

The HJB master equation (3.22) is $\mathbb LV=0$ with $\mathbb LV(t,\mu)=\partial_tV(t,\mu)+G(t,\mu,\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot))$, where

$$G(t,\mu,Z,\Gamma)=\mathbb E^\mu\Big[\sup_{a\in A}\Big(\tfrac12\Gamma(X):\sigma\sigma^\top(t,X,\mu,a)+Z(X)\cdot b(t,X,\mu,a)+f(t,X,\mu,a)\Big)\Big].$$

Viscosity solutions (Definition 4.4) are defined by test functions $\varphi$ that satisfy a functional Itô formula on $[t,t+\delta]\times\mathcal P_L(t,\mu)$, where $\mathcal P_L(t,\mu)$ is the set of laws agreeing with $\mu$ on $[0,t]$ under which $X$ is a semimartingale on $[t,T]$ with drift and diffusion bounded by $L$, and touch $V$ from above or below at $(t,\mu)$ on that set.

Formalization targets

Goal: Theorem 5.8

Under Assumption 5.1, $V$ is finite on $\Theta$ and is a viscosity solution of (3.22).

Milestones

• $(4.1)$: $\sup_{\mathbb P\in\mathcal P_L(t,\mu)}\mathbb E^{\mathbb P}[\sup_{t\le s\le t+\delta}|X_{t,s}|^p]\le C_{p,L}\delta^{p/2}$.
• Remark 5.4(i): (3.18) has a unique solution, and it lies in $\mathcal P_L(t,\mu)$ for $L\ge C_0\vee\frac12C_0^2$.
• Remark 5.4(ii): the dynamic programming principle (3.21),

$$V(t_1,\mu)=\sup_{\alpha\in\mathcal A_{t_1}}\Big[V(t_2,\mathbb P^{t_1,\mu,\alpha})+\int_{t_1}^{t_2}\mathbb E^{\mathbb P^{t_1,\mu,\alpha}}[f(s,X,\mathbb P^{t_1,\mu,\alpha},\alpha_s)]ds\Big].$$

• Lemma 5.11: a coupling construction with an independent Brownian motion.
• Lemma 5.13: $|V_0(t,\mu)-V_0(t,\nu)|\le\rho(\mathcal W_2(\mu_{[0,t]},\nu_{[0,t]}))$ for a modulus $\rho$.
• Lemma 5.14: $V=V_0$.
• Theorem 5.7: $|V(t_1,\mu)-V(t_2,\nu)|\le C\rho(\mathcal W_2((t_1,\mu),(t_2,\nu)))+C[1+\mathcal W_2(\mu_{[0,t_1]},\delta_{\{0\}})][t_2-t_1]$, and uniform continuity when $f$ is bounded.

Significance

The result characterizes the closed-loop value function through a PDE on the space of path laws without assuming any smoothness of $V$. Combined with a comparison principle for (3.22), which the paper leaves open, it would identify the closed-loop and open-loop values (Remark 5.9). The regularity result (Theorem 5.7) is itself delicate: Example 5.6 shows that a natural restricted class of closed-loop controls produces a value function that is discontinuous in $\mu$, and the piecewise constant class (5.3) is chosen to avoid this.

The theorems are proved in the paper; none of them is formalized. A formalization would supply a machine-checked path from a path-dependent McKean–Vlasov control problem to its HJB master equation, together with reusable statements on weak solutions of path-dependent McKean–Vlasov equations, their uniform moment bounds, and the dynamic programming principle in the Wasserstein space.

Difficulty

Definition 4.4 requires $V\in C^0(\Theta)$, and the central difficulty is continuity in $\mu$. Closed-loop controls are functions of the observed path; changing the initial law from $\mu$ to $\nu$ changes the information available to the control, and when $\nu_{[0,t]}$ is degenerate a control adapted to $\mu$ cannot be written as a function of the $\nu$-path. The obvious argument, transporting an $\varepsilon$-optimal control for $\mu$ along an optimal coupling of $\mu$ and $\nu$, fails for exactly this reason (Example 5.6).

Formalization scope

Time is $\mathbb R_{\ge0}$ and every statement quantifies over $t\le T$ and $\mu\in\mathcal P_2$. Paths are continuous maps $[0,T]\to\mathbb R^d$ with the sup norm and Borel $\sigma$-algebra; $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance with $p=2$. Brownian motion and Itô integrals are the published EthierKurtz.IsStandardBrownian and EthierKurtz.HasBrownianItoIntegral.

Committed conventions:

• The control set $A$ is a nonempty Polish space with its Borel $\sigma$-algebra (the paper says "some appropriate set $A$"); this provides continuity in $a$, measurability of $h_i$ and of $\omega\mapsto\sup_aG_2$.
• "Progressively measurable in all variables" is joint measurability (Giry $\sigma$-algebra on laws) plus adaptedness in $\omega$ and $\mu$. The bound $|\sigma|\le C_0$ uses the Frobenius norm; the joint Lipschitz bound on $(b,\sigma)$ is two bounds with the same $L_0$. $\delta_{\{0\}}$ is the Dirac mass at the zero path.
• (3.18) is solved in the weak sense: a law with a semimartingale representation, carrying its own Brownian motion, whose characteristics are the controlled coefficients on $[t,T)$. $\mathcal P_L(t,\mu)$ is defined through the same representations.
• $V$ and $V_0$ are suprema in the extended reals over admissible pairs; statements that subtract values or use $V$ as a real function assert finiteness explicitly.
• Test functions carry their derivatives as witnesses; the Itô formula of Definition 4.2 is stated in drift form for every representation; "$\inf(\varphi-V)=0$" is read as $\varphi-V\ge0$ on the test set with equality at $(t,\mu)$, and the test function's data at $(t,\mu)$ are those at $(t,\mathbb P)$ for $\mathbb P\in\mathcal P_L(t,\mu)$.
• Statements are for general $d$; §5.3 of the paper argues for $d=1$ only.

The test classes are not vacuous: constant functions satisfy every clause of the test-function class, and Assumption 5.1 holds for $b\equiv0$, $\sigma\equiv I$, $f\equiv g\equiv0$. A formalization that makes $\mathcal P_L(t,\mu)$ or the admissible set empty, or that lets $V$ be $-\infty$, does not prove the theorem.

Needed infrastructure: weak existence and uniqueness for path-dependent McKean–Vlasov SDEs with Lipschitz coefficients; Burkholder–Davis–Gundy-type moment bounds; measurable selection on Polish spaces; couplings and gluing on $\mathcal P_2$ of a path space. The moment bound and the McKean–Vlasov well-posedness are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2), 936–986, 2020. https://doi.org/10.1214/19-AAP1521
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3), 2017. https://doi.org/10.1137/16M1095895
• I. Ekren, N. Touzi, J. Zhang, Viscosity solutions of fully nonlinear parabolic path dependent PDEs: Part I, Ann. Probab. 44(2), 2016. https://doi.org/10.1214/14-AOP999

Motivation

Master equations are partial differential equations whose state variable is a probability measure. They arise as the Hamilton–Jacobi–Bellman equations of mean field control problems, where a planner steers a large population through its distribution, and as the limit description of large games. Their basic computational tool is an Itô formula for functions of measures: if $X$ is a semimartingale with law $\mathbb P_{X_t}$ at time $t$, how does $f(\mathbb P_{X_t})$ evolve? For functions on the Wasserstein space $\mathcal P_2(\mathbb R^d)$ this formula is due to Buckdahn, Li, Peng and Rainer (Ann. Probab. 2017) and Chassagneux, Crisan and Delarue (arXiv:1411.3009), with the derivative in the measure introduced by Lions through the lifting to random variables.

Many models are path dependent: exotic options, rough volatility, and control problems with constant controls all lead to functions of the law of a whole path rather than of its time marginal. Wu and Zhang (Ann. Appl. Probab. 2020) extend the measure derivative and the Itô formula to this setting, following Dupire's functional Itô calculus (Dupire 2009). This mission formalizes §2 of their paper: the derivative of a function of a path law and the functional Itô formula of Theorem 2.7. It is the first of three missions on the paper; the other two treat viscosity solutions of master equations and McKean–Vlasov control.

Setting

Fix $d\ge1$ and $T>0$. Continuous paths form $\Omega=C([0,T],\mathbb R^d)$ with $\|\omega\|=\sup_t|\omega_t|$. Càdlàg paths form $\widehat\Omega=\mathbb D([0,T],\mathbb R^d)$ with the Skorokhod distance

$$d_{SK}(\hat\omega,\hat\omega')=\inf_\lambda\sup_{0\le t\le T}\big[|t-\lambda(t)|+|\hat\omega_t-\hat\omega'_{\lambda(t)}|\big],$$

the infimum over continuous strictly increasing bijections $\lambda$ of $[0,T]$. The canonical process is $\widehat X_t(\hat\omega)=\hat\omega_t$, with natural filtration $\widehat{\mathbb F}$; $\hat\omega_{t\wedge\cdot}$ is the path stopped at $t$.

$\widehat{\mathcal P}_2$ is the set of probability measures $\mu$ on $\widehat\Omega$ with $\mathbb E^\mu\|\widehat X\|^2<\infty$, with the Wasserstein distance $\mathcal W_2$ whose cost is $d_{SK}^2$. The state space is $\widehat\Theta=[0,T]\times\widehat{\mathcal P}_2$ with the pseudometric

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

where $\mu_{[0,t]}$ is the law of $\widehat X_{t\wedge\cdot}$.

For $f:\widehat\Theta\to\mathbb R$ the time derivative is the right derivative $\partial_tf(t,\mu)=\lim_{\delta\downarrow0}[f(t+\delta,\mu_{[0,t]})-f(t,\mu)]/\delta$. The spatial derivative $\partial_\mu f(t,\mu,\hat\omega)\in\mathbb R^d$ comes from lifting $f$ to $F(t,\tilde X)=f(t,\tilde{\mathbb P}_{\tilde X})$ on square-integrable path-valued random variables of an atomless Polish probability space: the Fréchet derivative of $F$ under the perturbation $\tilde X+\xi\mathbf 1_{[t,T]}$ has the form $DF(t,\tilde X)=\partial_\mu f(t,\tilde{\mathbb P}_{\tilde X_{t\wedge\cdot}},\tilde X_{t\wedge\cdot})$. The second derivative $\partial_\omega\partial_\mu f\in\mathbb R^{d\times d}$ is the pathwise (Dupire vertical) derivative of $\partial_\mu f$. $C^{1,1,1}_b(\widehat\Theta)$ consists of the continuous $f$ with continuous derivatives, bounded $\partial_tf$, and $|\partial_\mu f|+|\partial_\omega\partial_\mu f|\le C[1+\|\hat\omega\|]$.

$\widehat{\mathcal P}_L$ is the set of laws $\mu=\tilde{\mathbb P}\circ\tilde X^{-1}$ of Itô processes $\tilde X_t=\tilde X_0+\int_0^t\tilde b_s\,ds+\int_0^t\tilde\sigma_s\,d\tilde B_s$ with $|\tilde b|\le L$, $\tfrac12|\tilde\sigma|^2\le L$ and $\tilde X_0$ square integrable.

Formalization targets

Goal: the functional Itô formula (Theorem 2.7)

For $f\in C^{1,1,1}_b(\widehat\Theta)$, $\mu\in\widehat{\mathcal P}_L$ and $t\in[0,T]$,

$$f(t,\mu)=f(0,\mu)+\int_0^t\partial_tf(s,\mu)\,ds+\mathbb E^\mu\Big[\int_0^t\partial_\mu f(s,\mu,\widehat X)\cdot d\widehat X_s+\tfrac12\int_0^t\partial_\omega\partial_\mu f(s,\mu,\widehat X):d\langle\widehat X\rangle_s\Big].$$

Milestones

1. Theorem 2.2: the Fréchet derivative of the lift is $\psi(\tilde X_{t\wedge\cdot})$ for an $\widehat{\mathcal F}_t$-measurable $\psi$ determined by $f$ and the law of $\tilde X$.
2. Corollary 2.3: under uniform continuity of $DF$, a single jointly measurable $\partial_\mu f$ represents $DF$, unique if continuous.
3. (2.21): the discrete expansion $f(T,\mu^n)-f(0,\mu^n)=I_1^n+I_2^n+I_3^n$ along a uniform partition.
4. (2.22) and the $\mathcal W_2$ limit after it: the discretized paths and laws converge.
5. The four limits on p. 946, which turn (2.21) into (2.20) as $n\to\infty$.

Significance

The formula is the chain rule of calculus on path laws. It is what makes $C^{1,1,1}_b$ functions admissible test functions for viscosity solutions of path-dependent master equations, and what identifies the value function of a McKean–Vlasov control problem with a solution of its HJB master equation (§§4–5 of the paper, the other two missions of this series). Without it, the notion of viscosity solution in that paper has no link to the underlying dynamics.

The result is proved in the paper. It has no machine-checked proof: Lean's Mathlib has neither the Skorokhod space, nor Wasserstein spaces of path laws, nor a derivative with respect to a measure. Formalizing it would also produce a reusable Lean account of càdlàg path spaces and of the Lions derivative, both of which are absent today.

Difficulty

The obvious argument would expand $f$ along the time marginals of $\tilde X$. That fails for path-dependent $f$: the stopped laws $\mu_{[0,t]}$ do not change continuously when a path is perturbed after $t$, and the perturbation $\tilde X+\xi\mathbf 1_{[t,T]}$ of the derivative's definition leaves the space of continuous paths. This is why the paper passes to càdlàg paths and the Skorokhod distance. Any argument then has to control $f$ and its derivatives along laws of discontinuous paths, which is where the joint continuity of all derivatives in $(t,\mu,\hat\omega)$ under $\mathcal W_2+d_{SK}$ and convergence of laws in $\mathcal W_2$ become unavoidable. Separately, Theorem 2.2 must show that a derivative defined through one probability space is a deterministic function of the stopped path, and atomlessness of that space is essential to it.

Formalization scope

Paths are functions on $[0,\infty)$, constant after $T$; $\Omega$ is C(Set.Icc 0 T, ℝ^d) with the sup norm, embedded in $\widehat\Omega$. $\widehat\Omega$ carries the $\sigma$-algebra of the evaluations. Distances, sup norms and $\mathcal W_2$ are $[0,\infty]$-valued. A law in $\widehat{\mathcal P}_L$ is given with an explicit representation: a filtered probability space, a standard Brownian motion with independent increments, progressively measurable bounded coefficients, and the Itô integral of the published EthierKurtz.HasBrownianItoIntegral. The goal holds for every representation of $\mu$, and (2.20) is stated in drift form: $\mathbb E\int_0^t(\partial_\mu f\cdot\tilde b_s+\tfrac12\partial_\omega\partial_\mu f:\tilde\sigma_s\tilde\sigma_s^\top)\,ds$, the stochastic integral having mean zero.

The class $C^{1,1,1}(\widehat\Theta)$ fixes $f$ together with its derivatives and states that they are the derivatives (2.7), (2.16), (2.18). It also requires $\partial_\mu f(t,\mu,\cdot)$ and $\partial_\omega\partial_\mu f(t,\mu,\cdot)$ to be $\widehat{\mathcal F}_t$-adapted, a property the paper's $\partial_\mu f$ has by Theorem 2.2. Without these clauses every continuous function would qualify, and (2.20) would be false. The printed $\mathbb D([0,T),\mathbb R^d)$ is read as $\mathbb D([0,T],\mathbb R^d)$. The proof's $d=1$ computations are stated in dimension $d$. Limits indexed by $t_i\le t<t_{i+1}$ are stated for $t<T$.

A complete development needs: the Skorokhod space and the fact that its Borel $\sigma$-algebra is the evaluation $\sigma$-algebra; Wasserstein distances on it; dominated convergence for path laws; and Itô's formula for the drift–diffusion representation. These are reusable well beyond this mission. Contributions to any milestone, or to these foundations as separate lemmas, are welcome.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2) (2020), 936–986. https://doi.org/10.1214/19-AAP1521
• R. Buckdahn, J. Li, S. Peng, C. Rainer, Mean-field stochastic differential equations and associated PDEs, Ann. Probab. 45(2) (2017), 824–878. https://doi.org/10.1214/15-AOP1076
• J.-F. Chassagneux, D. Crisan, F. Delarue, A probabilistic approach to classical solutions of the master equation for large population equilibria, Mem. Amer. Math. Soc. (2022). https://arxiv.org/abs/1411.3009
• B. Dupire, Functional Itô calculus, Bloomberg Portfolio Research Paper 2009-04 (2009); Quant. Finance 19(5) (2019). https://doi.org/10.2139/ssrn.1435551
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer (2018). https://doi.org/10.1007/978-3-319-58920-6

Motivation

In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process $V$ is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.

Model uncertainty replaces the single model by a set $\mathcal P$ of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.

Timeline:

• 1995: El Karoui and Quenez, optional decomposition in diffusion models.
• 1996: Kramkov, for locally bounded semimartingales.
• 2014: Nutz, superreplication duality under model uncertainty in discrete time (Finance Stoch. 18 (2014)).
• 2015: Bouchard and Nutz, the fundamental theorem, superhedging duality and the optional decomposition in nondominated discrete time (Theorem 6.1).

Setting

Fix a Polish space $\Omega_1$, a horizon $T \in \mathbb N$ and $d \in \mathbb N$. Let $\Omega_t := \Omega_1^t$ for $t = 0, \dots, T$. Then $\Omega_0$ is a single point and $\Omega := \Omega_T$, and a point of $\Omega_t$ is read as the first $t$ coordinates of a path. The $\sigma$-field $\mathcal F_t$ is the universal completion of $\mathcal B(\Omega_t)$.

For each $t < T$ and each node $\omega \in \Omega_t$ a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ is given, and its graph is an analytic set. The set of possible models $\mathcal P$ consists of all products $P_0 \otimes P_1 \otimes \cdots \otimes P_{T-1}$ whose kernels take values in $\mathcal P_t(\cdot)$. A set is $\mathcal P$-polar if it is null under every $P \in \mathcal P$. A property holds $\mathcal P$-quasi surely (q.s.) if it holds outside a polar set.

Stock prices $S_t : \Omega_t \to \mathbb R^d$ are Borel. A strategy $H \in \mathcal H$ is predictable: $H_u$ is a function of the first $u-1$ coordinates. The wealth at time $t$ is

$$H \bullet S_t = \sum_{u=1}^t H_u \Delta S_u, \qquad \Delta S_u = S_u - S_{u-1}.$$

NA($\mathcal P$) holds if $H \bullet S_T \ge 0$ q.s. implies $H \bullet S_T = 0$ q.s. A martingale measure is a probability $Q$ under which $S$ is a martingale. The set

$$\mathcal Q = \{Q \lll \mathcal P : Q \text{ is a martingale measure}\}$$

contains those $Q$ that are absolutely continuous with respect to some $P \in \mathcal P$ (written $Q \lll \mathcal P$). A function $f$ with values in $[-\infty, \infty]$ is upper semianalytic if every set $\{f > c\}$ is analytic.

At one node $\omega \in \Omega_t$, the increment $\Delta S_{t+1}(\omega, \cdot)$ defines a one-period market under $\mathcal P_t(\omega)$, with its own no-arbitrage condition NA($\mathcal P_t(\omega)$) and one-period martingale measures $\mathcal Q_t(\omega)$. The conditional sublinear expectation is

$$\mathcal E_t(f)(\omega) = \sup_{Q \in \mathcal Q_t(\omega)} E_Q[f(\omega, \cdot)].$$

Formalization targets

Goal: Theorem 6.1 (nondominated optional decomposition)

Let NA($\mathcal P$) hold and let $V$ be an adapted process such that $V_t$ is upper semianalytic and in $L^1(Q)$ for all $Q \in \mathcal Q$ and $t \in \{1, \dots, T\}$. Then the following are equivalent:

1. $V$ is a supermartingale under each $Q \in \mathcal Q$;
2. there exist $H \in \mathcal H$ and an adapted increasing process $K$ with $K_0 = 0$ such that

$$V_t = V_0 + H \bullet S_t - K_t \quad \mathcal P\text{-q.s.}, \qquad t = 0, 1, \dots, T.$$

Milestones

• Lemma 4.6: the set $N_t$ of nodes where NA($\mathcal P_t(\omega)$) fails is universally measurable, and it is polar under NA($\mathcal P$).
• Theorem 4.5: NA($\mathcal P$) holds if and only if every $N_t$ is polar, if and only if every $P \in \mathcal P$ is absolutely continuous with respect to some $Q \in \mathcal Q$.
• Lemma 4.10: $\mathcal E_t(f)$ is upper semianalytic, and there is a universally measurable $y$ with

$$\mathcal E_t(f)(\omega) + y(\omega)\,\Delta S_{t+1}(\omega, \cdot) \ge f(\omega, \cdot) \quad \mathcal P_t(\omega)\text{-q.s.}$$

at every arbitrage-free node where $f(\omega,\cdot) > -\infty$ q.s.

• (6.1): under condition 1 of the goal, $\mathcal E_t(V_{t+1}) \le V_t$ $\mathcal P$-q.s. for every $t < T$.

Significance

The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price $\sup_{Q} E_Q[f]$. The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy $H$ that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every $Q \in \mathcal Q$: up to a polar set they are exactly the wealth processes of strategies that consume.

The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.

Difficulty

With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in $\mathcal P$ may be mutually singular, so conditional expectations under different $Q$ disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, $\omega \mapsto \mathcal P_t(\omega)$. Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in $\omega$. Borel measurability is not preserved by taking suprema over the random set $\mathcal Q_t(\omega)$. Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each $P \in \mathcal P$ separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.

Formalization scope

The Lean development uses the following conventions.

• Paths and measures. $\Omega_t$ is Fin t → Ω₁, and measures are Borel. $\mathcal F_t$-measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.
• Polar sets. A polar set is null in outer measure under every model. The exceptional sets in the statements are universally measurable, and for such sets this agrees with the paper's definition.
• The model set. $\mathcal P$ consists of the laws of Borel Markov kernels that lie in $\mathcal P_t$ almost surely, which is the paper's equivalent formulation on p. 4.
• Processes. A process is a family V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.
• Strategies. The Lean strategy H u is the paper's $H_{u+1}$.
• Expectations. Expectations of functions with values in $[-\infty, \infty]$ follow (1.1) in EReal, with $\infty - \infty = -\infty$. Suprema over $\mathcal Q_t(\omega)$ are taken in EReal.
• Options. The setting has no options ($e = 0$).
• Page numbers. Pages and indices are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal pagination 823–859.

The increasing process $K$ must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with $K := V_0 + H \bullet S - V$ for any $H$. Integrability and supermartingale properties are always stated with explicit $Q$-integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.

The development needs the following infrastructure:

• analytic sets and measurable selection (some of it exists for Bertsekas–Shreve on the platform);
• measurability of $(\omega, Q) \mapsto E_Q[f(\omega,\cdot)]$;
• products of kernels;
• the one-period fundamental theorem and superhedging duality.

These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.

Selected references

• B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2), 823–859, 2015. https://doi.org/10.1214/14-AAP1011, arXiv:1305.6008v3 https://arxiv.org/abs/1305.6008
• N. El Karoui, M.-C. Quenez, Dynamic programming and pricing of contingent claims in an incomplete market, SIAM J. Control Optim. 33, 29–66, 1995. MR1311659, https://mathscinet.ams.org/mathscinet-getitem?mr=1311659
• D. O. Kramkov, Optional decomposition of supermartingales and hedging contingent claims in incomplete security markets, Probab. Theory Related Fields 105, 459–479, 1996. MR1402653, https://mathscinet.ams.org/mathscinet-getitem?mr=1402653
• M. Nutz, Superreplication under model uncertainty in discrete time, Finance Stoch. 18, 791–803, 2014. MR3255751, https://mathscinet.ams.org/mathscinet-getitem?mr=3255751
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Mathematics in Science and Engineering 139, Academic Press, 1978. MR0511544, https://mathscinet.ams.org/mathscinet-getitem?mr=0511544

Motivation

Master equations are partial differential equations whose state variable is a probability measure. They arise as the dynamic programming equations of mean-field control problems, as the limits of large particle systems, and as the pricing equations of options on a whole population. Their coefficients and solutions are functions on a Wasserstein space, which is infinite dimensional, and classical (smooth) solutions are known only under strong regularity assumptions (Cardaliaguet–Delarue–Lasry–Lions 2019). A notion of weak solution for which existence, comparison and uniqueness can all be proved is therefore the basic missing tool.

C. Wu and J. Zhang (Ann. Appl. Probab. 2020) propose such a notion for parabolic master equations on the space of laws of continuous paths, in the spirit of the viscosity theory for path-dependent PDEs of Ekren, Keller, Touzi and Zhang (Ann. Probab. 2014). This mission formalizes its §4: the definition of viscosity solutions and the comparison principle that makes them unique.

Setting

Fix a horizon $T$ and a dimension $d$. The canonical space is $\Omega=C([0,T];\mathbb R^d)$ with the uniform norm $\|\omega\|$, the canonical process is $X_t(\omega)=\omega_t$, and $\mathcal F_t=\sigma(X_s:s\le t)$. $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu\|X\|^2<\infty$; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$. The state space is $\Theta=[0,T]\times\mathcal P_2$ with the pseudometric

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

where $\mathcal W_2$ on laws is the 2-Wasserstein distance. A function $V:\Theta\to\mathbb R$ has a time derivative $\partial_tV$, a path derivative $\partial_\mu V(t,\mu,\omega)\in\mathbb R^d$ and a second derivative $\partial_\omega\partial_\mu V(t,\mu,\omega)\in\mathbb R^{d\times d}$, defined through a functional Itô formula along semimartingale laws.

The master equation (3.1) is

$$\mathbb LV(t,\mu):=\partial_tV(t,\mu)+G\big(t,\mu,V(t,\mu),\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot)\big)=0,$$

with a generator $G$ that is continuous in $(t,\mu)$, Lipschitz in $y$, and Lipschitz in $(Z,\Gamma)$ in the averaged sense (3.2) of Assumption 3.1.

For $L>0$, $\mathcal P_L(t,\mu)$ is the set of laws $\mathbb P\in\mathcal P_2$ that agree with $\mu$ up to time $t$ and under which $X$ is a semimartingale on $[t,T]$ with drift bounded by $L$ and half squared diffusion bounded by $L$. Test functions at $(t,\mu)$ are $C^{1,1,1}$ functions on $[t,t+\delta]\times\mathcal P_L(t,\mu)$ touching $V$ from above or below there, (4.2). $V\in C^0(\Theta)$ is an $L$-viscosity subsolution (supersolution) if $\mathbb L\varphi(t,\mu)\ge0$ ($\le0$) for every such test function, and a viscosity solution if it is both for one $L>0$ (Definition 4.4). The Perron envelopes $\overline V$, $\underline V$ of (4.17) are the infimum of piecewise classical supersolutions above $g$ and the supremum of piecewise classical subsolutions below $g$.

Formalization targets

Goal: comparison and uniqueness (Theorem 4.13)

Under Assumption 3.1 and $g\in C^0(\mathcal P_2)$, if $V_1$ is a viscosity subsolution, $V_2$ a viscosity supersolution, $V_1(T,\cdot)\le g\le V_2(T,\cdot)$, the classes $\underline{\mathcal U}_g,\overline{\mathcal U}_g$ are nonempty, and

$$\overline V=\underline V=:V,\qquad(4.19)$$

then $V_1\le V\le V_2$ on $\Theta$, and $V$ is the unique viscosity solution with terminal condition $g$.

Milestones

1. the moment estimate (4.1) over $\mathcal P_L(t,\mu)$;
2. Lemma 4.1: $[t,T]\times\mathcal P_L(t,\mu)$ is compact under $\mathcal W_2$;
3. Theorem 4.7: viscosity solutions are characterized by semi-jets of paraboloids;
4. Theorem 4.9: the change of variable $\tilde V=e^{\lambda t}V$;
5. Theorem 4.6: consistency with classical solutions;
6. Theorem 4.11: partial comparison when one side is smooth;
7. Proposition 4.12: a continuous lower envelope $\underline V$ is a viscosity subsolution.

Significance

The comparison principle is what turns a definition into a theory: it gives uniqueness, it identifies value functions of mean-field control problems with the solution of their master equation, and it is the input of stability and convergence arguments for numerical schemes. Theorem 4.13 reduces well-posedness to condition (4.19), and the authors verify (4.19) in examples (§4.6) via Theorem 4.14. The compactness of $\mathcal P_L(t,\mu)$ (Lemma 4.1) is the device that replaces local compactness, which the Wasserstein space lacks; it is reusable for any viscosity theory over semimartingale laws.

These results are proved on paper. No machine-checked development of viscosity solutions on Wasserstein spaces, or of the path-dependent functional Itô calculus on laws, is known to exist. A formalization would produce a checked notion of viscosity solution for master equations, the compactness of bounded-characteristic semimartingale laws, and the comparison machinery, and would expose the points where the printed proofs are sketched (see below).

Difficulty

The obvious route, copying the finite-dimensional theory, fails at two places. First, the doubling-of-variables argument for comparison needs a penalization on the state space that is smooth and coercive; on $\mathcal P_2$ under $\mathcal W_2$ neither is available, which is why comparison is reached through partial comparison and Perron envelopes. Second, maxima of $\varphi-V$ need not be attained on Wasserstein balls, which are not compact; the theory therefore tests only on $[t,T]\times\mathcal P_L(t,\mu)$, and Lemma 4.1 (via Zheng's tightness criterion for semimartingale laws and uniform integrability of $\|X\|^2$) is what makes the extrema exist. The printed proof of Theorem 4.13 opens with "$\overline V$ is lower semicontinuous and $\underline V$ is upper semicontinuous"; as printed the directions are swapped (an infimum of functions continuous in $\mu$ is upper semicontinuous in $\mu$), and the members of $\mathcal U$ are only càdlàg in $t$, so the continuity of $V$ needed for the conclusion requires an argument of its own.

Formalization scope

Time is $\mathbb R_{\ge0}$, and every condition is imposed only at $t\le T$, $\mu\in\mathcal P_2$. $\mathbb R^d$ is the Euclidean space, matrices are $d\times d$ real matrices with the Frobenius norm, and $A:B=\sum_{ij}A_{ij}B_{ij}$. $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance on laws of paths; Brownian motion and the Itô integral are the published EthierKurtz definitions. Membership in $\mathcal P_L(t,\mu)$ is the existence of a representation of $\mathbb P$ as the law of an Itô process from time $t$ with $|b|\le L$, $\tfrac12|\sigma|^2\le L$ (§2.4). A $C^{1,1,1}$ object is a record of a function and three derivative functions, and the functional Itô formula (2.25) is required in drift form for every representation, which equals (2.25) because the stochastic integral has mean zero. Test sets encode "$\inf(\varphi-V)=0$" literally, and the data of a test function at $(t,\mu)$ are its values at $(t,\mathbb P)$, $\mathbb P\in\mathcal P_L(t,\mu)$. The Perron envelopes are extended-real infima and suprema over the classes (4.18); (4.19) is stated with a real-valued $V$.

Two readings are fixed. Assumption 3.1(i) is continuity of $(t,\mu)\mapsto G(t,\mu,y,Z(X_{t\wedge\cdot}),\Gamma(X_{t\wedge\cdot}))$ for fixed continuous $Z,\Gamma$ of linear growth. "$V\in C_b^{1,1,1}(\Theta)$" in Theorems 4.6 and 4.11 is replaced by the larger class it is used through (Remark 4.3(i)): data continuous on $\Theta$ lying in $C_b^{1,1,1}([t_1,t_2]\times\mathcal P_L(t_1,\mu))$ for all $t_1<t_2$, $L$, $\mu$, so those statements are at least as strong as printed.

The definitions cannot be satisfied vacuously: every test set requires a witness law in $\mathcal P_L(t,\mu)$, the class $C_b^{1,1,1}$ contains the constants (checked in Lean), and a viscosity solution uses one $L$ for both halves. The semi-jets range only over $\mathcal F_t$-measurable continuous arguments of linear growth, as printed.

Contributions are welcome at every level: the moment bound (4.1) and Lemma 4.1 need tightness and uniform-integrability results for semimartingale laws on path space that Mathlib does not have; Theorems 4.7 and 4.9 are self-contained manipulations of the definitions; Theorems 4.6 and 4.11 and Proposition 4.12 need the compactness lemma and the Itô identity of test functions.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2) (2020) 936–986. https://doi.org/10.1214/19-AAP1521
• I. Ekren, C. Keller, N. Touzi, J. Zhang, On viscosity solutions of path dependent PDEs, Ann. Probab. 42(1) (2014) 204–236. https://doi.org/10.1214/12-AOP788
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games, Annals of Mathematics Studies 201, Princeton University Press, 2019. https://doi.org/10.2307/j.ctvckq7qf
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• W. A. Zheng, Tightness results for laws of diffusion processes application to stochastic mechanics, Ann. Inst. H. Poincaré Probab. Statist. 21(2) (1985) 103–124. http://www.numdam.org/item/AIHPB_1985__21_2_103_0/

Motivation

Games with many interacting agents, such as traffic participants, users of a shared communication channel or firms in a market, are rarely solvable exactly: a Nash equilibrium of an $N$-player stochastic game requires each agent to track the whole population, and its computation grows with $N$. Mean-field game theory replaces the population by its limiting distribution. A single representative agent faces a deterministic flow of state distributions, and consistency requires that this flow is the one the agent's own optimal policy generates. The equilibrium of this limit problem is then used as an approximate equilibrium of the finite game, with each agent acting only on its own state.

Most of this theory concerns risk-neutral agents, who minimize an expected cost. Saldi, Başar and Raginsky (arXiv:1808.03929; Math. Oper. Res. 2020) treat discrete-time agents with an exponential utility of the discounted cost, the classical risk-sensitive criterion that penalizes the variance of the cost as well as its mean. The paper proves two results: a mean-field equilibrium exists (Theorem 1, the first mission of this series), and the equilibrium policy is an approximate Nash equilibrium of every large enough finite game (Theorem 3, this mission). The risk-neutral counterpart is Saldi, Başar and Raginsky, SIAM J. Control Optim. 2018 (arXiv:1612.07878).

Setting

States lie in a Polish metric space $\mathsf X$, actions in a compact Polish space $\mathsf A$, and $\mathcal P(\mathsf X)$ is the set of Borel probability measures with the weak topology. The model consists of a transition kernel $p(\cdot\mid x,a,\mu)$, a one-stage cost $c(x,a,\mu)\ge0$, an initial law $\mu_0$, a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$.

In the $N$-agent game, the states $x^N_i(0)$ are i.i.d. $\mu_0$. At each time $t$, agent $i$ draws $a^N_i(t)\sim\pi^i_t(\cdot\mid x^N_i(t))$ from its Markov policy $\pi^i$, and the next states are drawn independently from $p(\cdot\mid x^N_i(t),a^N_i(t),e^{(N)}_t)$, where $e^{(N)}_t=\frac1N\sum_{j}\delta_{x^N_j(t)}$ is the empirical distribution of the states. Agent $i$'s cost is

$$J^{(N)}_i(\boldsymbol\pi^{(N)})=E^{\boldsymbol\pi^{(N)}}\Big[e^{\lambda\sum_{t=0}^\infty\beta^tc(x^N_i(t),a^N_i(t),e^{(N)}_t)}\Big].$$

A profile is an $\varepsilon$-Markov-Nash equilibrium if no agent can lower its $J^{(N)}_i$ by more than $\varepsilon$ by switching to another Markov policy.

In the mean-field game, one agent faces a flow $\boldsymbol\mu=(\mu_t)$: $x(t+1)\sim p(\cdot\mid x(t),a(t),\mu_t)$, with cost $J_{\boldsymbol\mu}(\pi)=E^\pi[e^{\lambda\sum_t\beta^tc(x(t),a(t),\mu_t)}]$. A mean-field equilibrium is a pair $(\pi,\boldsymbol\mu)$ in which $\pi$ minimizes $J_{\boldsymbol\mu}$ and $\boldsymbol\mu=\Lambda(\pi)$ is the flow of state laws that $\pi$ generates.

The hypotheses are Assumption 1 (bounded continuous $c$ with $|c|\le K$, weakly continuous $p$, compact $\mathsf A$, and a moment function $w$ with $\int w\,dp\le\alpha w$ and $\int w\,d\mu_0<\infty$) and Assumption 2. Part (a) of Assumption 2 asks that the moduli

$$\omega_p(r)=\sup_{x,a}\sup_{d_{BL}(\mu,\nu)\le r}\|p(\cdot\mid x,a,\mu)-p(\cdot\mid x,a,\nu)\|_{TV},\qquad\omega_c(r)=\sup_{x,a}\sup_{d_{BL}(\mu,\nu)\le r}|c(x,a,\mu)-c(x,a,\nu)|$$

tend to $0$, where $d_{BL}$ is the bounded-Lipschitz metric. Part (b) asks that the equilibrium policy $\pi$ be weakly continuous in the state.

Formalization targets

Goal: Theorem 3 (p. 23)

For every $\varepsilon>0$ there is $N(\varepsilon)$ such that, for every $N\ge N(\varepsilon)$, the profile $(\pi,\dots,\pi)$ is an $\varepsilon$-Markov-Nash equilibrium:

$$J^{(N)}_i(\pi,\dots,\pi)\le\inf_{\sigma\in\mathsf M}J^{(N)}_i(\pi,\dots,\sigma,\dots,\pi)+\varepsilon\qquad\text{for all }i .$$

The statement fixes no rate. It is the paper's main approximation result.

Milestones

The milestones follow the paper's proof. The first seven work in an augmented model, whose state $s=(x,c)$ carries the accumulated discounted cost, so that the exponential criterion becomes a terminal cost $e^{\lambda c(n+1)}$. They are: Proposition 6 (the augmented model has the same finite-horizon costs); Lemma 5 (the augmented flow $\Delta_{t+1}=\Delta_tP^\pi_{t,\Delta_t}$); Proposition 7 (propagation of chaos, $\mathcal L(\Delta^{(N)}_t)\to\delta_{\Delta_t}$); Proposition 8 (convergence of the augmented cost); Proposition 9 (propagation of chaos with one deviating agent); Proposition 10 (the deviating agent's state law); Proposition 11 (the deviating agent's augmented cost). The last three are stated in the original model: Theorem 4 (the finite-horizon limits (14)–(15)), Corollary 1 (the infinite-horizon comparison), and the first display of the proof of Theorem 3 (deviations may be restricted to weakly continuous policies).

Significance

Theorem 3 justifies the use of a mean-field equilibrium as a decentralized policy in risk-sensitive games with many players. The equilibrium is computed once, from a single-agent problem, and each agent uses only its own state, yet no agent of a large enough population gains more than $\varepsilon$ by deviating. The result extends the risk-neutral approximation theorem to the multiplicative criterion. Because the exponential cost does not decompose over time, the risk-neutral argument cannot be applied directly: the proof first passes through the augmented model and a finite-horizon truncation.

The result is proved in the paper; none of it is formalized. The mission formalizes the statement and the proof's intermediate results. That requires the $N$-agent law, a product of $N$ kernels driven by the empirical measure, built from Mathlib's Ionescu-Tulcea construction, and propagation of chaos for an interacting Markov chain on a Polish space. Alternative proofs of any milestone are welcome, as are quantitative versions of the limits.

Difficulty

The cost is the expectation of a product of one-stage factors, not a sum, so the convergence of the empirical measure gives no direct control of it. The paper therefore enlarges the state with the accumulated cost, and the finite-horizon limits must then be transferred back to the infinite horizon through a uniform tail bound. The coupling between agents runs through the empirical measure, which enters both the transition and the cost. Propagation of chaos (Proposition 7) is an induction over time that needs continuity of $p$ and $c$ in the measure argument uniformly in $(x,a)$ (Assumption 2-(a)) and a conditional variance bound. The deviating agent is not exchangeable with the others: its state law must be compared with that of a mean-field chain under its own policy (Proposition 10), uniformly over arbitrary sequences of deviations. Finally, a best response may be only measurable. The reduction to weakly continuous deviations, which the paper takes from its risk-neutral predecessor, is needed before any weak-convergence argument applies.

Formalization scope

Lean namespace RiskSensMFG.Nash. The definitions are in four files: the model, policies, the single-agent law and the flow (Model); the mean-field equilibrium, $d_{BL}$, total variation and Assumption 2-(a) (Equilibrium); the $N$-agent game (Game); and the augmented model (Augmented). Conventions:

• $\mathsf X$ is a complete separable metric space with its Borel $\sigma$-field, and $\mathsf A$ is a compact Polish space. $\mathcal P(\mathsf X)$ is Mathlib's ProbabilityMeasure with the weak topology and its Borel $\sigma$-field (not the Giry one), and $p$ is a Markov Kernel. The standing assumptions $\beta\in(0,1)$, $\lambda>0$ and $c\ge0$ measurable are a predicate Model.Standing. Assumption 1 is stated in full, including the moment function, although the proof of Theorem 3 does not use parts (d)–(e).
• Time is 0-based. Agents are indexed by Fin N, and the paper's Agent 1 is index 0; limits in $N$ are taken along $N+1$ so that Agent 1 exists. The empirical measure of the empty configuration is set to $\mu_0$ and enters no statement.
• The equilibrium's optimality is required against Markov policies only, which is a weaker hypothesis than Definition 3's optimality over all policies, so the goal is at least as strong as printed. The $\varepsilon$ of Definition 2 is on the scale of $J=E[e^{\lambda\sum\beta^tc}]$. Equilibrium and optimality are stated in "for every deviation" form, with no infimum over a type.
• Assumption 2-(a) and the modulus $\omega_g$ of Proposition 10 are written as $\varepsilon$–$\delta$ statements, which is equivalent to "$\omega(r)\to0$" because the moduli are nondecreasing. Total variation is $\sup_{|g|\le1}|\int g\,d\mu-\int g\,d\nu|$.
• The augmented cost coordinate is the discounted sum $\sum_{k<t}\beta^kc(\cdot)$; the page prints it without $\beta^k$, which contradicts $P_t$. The coordinate lies in $\mathbb R$ rather than $[0,L]$, because $\mathsf X\times[0,L]$ is not invariant under $P_t$, and the terminal cost is $e^{\lambda\max(0,\min(c,L))}$, which equals $e^{\lambda c}$ on reachable states. Corollary 1's printed "$\lim\ge$" (the limit is not shown to exist) is stated as three limit and eventual-inequality claims.

No hypothesis is vacuous: a sorry-free check exhibits a model satisfying the standing assumptions, Assumptions 1 and 2 and the equilibrium condition simultaneously, with $J^{(N)}_i\ge1$. This rules out the trivial reading in which a non-integrable integrand makes every cost $0$ and every profile an $\varepsilon$-equilibrium. Theorem 1 (existence of the equilibrium) is the other mission of the series; here the equilibrium is a hypothesis.

Selected references

• N. Saldi, T. Başar, M. Raginsky, Discrete-time Risk-sensitive Mean-field Games, arXiv:1808.03929v2, 2018; published as Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games, Math. Oper. Res. 45(4), 2020. https://arxiv.org/abs/1808.03929, https://doi.org/10.1287/moor.2019.1044
• N. Saldi, T. Başar, M. Raginsky, Markov–Nash Equilibria in Mean-Field Games with Discounted Cost, SIAM J. Control Optim. 56(6), 2018. https://arxiv.org/abs/1612.07878
• N. Bäuerle, U. Rieder, More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014. https://doi.org/10.1287/moor.2013.0601
• O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
• R. M. Dudley, Real Analysis and Probability, Cambridge University Press, 2002 (§11.3, the bounded-Lipschitz metric). https://doi.org/10.1017/CBO9780511755347

Motivation

In online allocation, requests arrive one at a time and each must be accepted or rejected on arrival, using a limited budget of resources. Revenue management, ad allocation and hiring all fit this pattern. A natural benchmark for an online policy is the prophet, or Offline: the decision maker who sees the whole arrival sequence in advance and acts optimally on it. The regret of a policy is the expected gap between Offline's value and the policy's value. Policies that track a fixed solution of a fluid relaxation lose on the order of $\sqrt T$ (Proposition 1 of the paper), so the question is whether a simple adaptive policy can achieve regret bounded independently of $T$ and of the budget.

The simplest such problem is the multi-secretary problem: hire at most $B$ of $T$ sequentially arriving candidates, each drawn i.i.d. from finitely many ability classes. Arlotto and Gurvich (Stochastic Systems 2019) showed that a budget-ratio policy has regret bounded uniformly in $T$ and $B$, using a martingale argument. Vera and Banerjee (SSRN 3158062; Management Science 2021) introduced the compensated coupling, a sample-path identity that expresses the regret of any online policy as the compensation Offline must be paid to follow it. They used it to prove constant regret for a simple re-solve-and-threshold rule, the Fluid Bayes Selector, with the explicit constant $r_{\max}\sum_{j>1}2/p_j$. This mission formalizes that result together with the compensated coupling it rests on.

Setting

A finite-horizon online decision problem has states $S$, arrival types $\Theta$, actions $A$, a transition function $T(a,s,j)$, a reward function $R(a,s,j)$, and a set $\mathcal F(s)$ of feasible actions in each state. Time is counted as time to go: decisions are made at $t=T,T-1,\dots,1$, and $\theta^t$ is the type arriving at time-to-go $t$. A standing assumption requires the best feasible reward in every state to be attained and to lie in a fixed bounded interval.

Given the whole arrival sequence, Offline's value obeys the Bellman equation

$$V^{\mathrm{off}}(0,s)=0,\qquad V^{\mathrm{off}}(t,s)=\max_{a\in\mathcal F(s)}\{R(a,s,\theta^t)+V^{\mathrm{off}}(t-1,T(a,s,\theta^t))\}.$$

An online policy chooses a feasible action at each time from the arrivals observed so far. Starting from $S^T=s_0$ it produces a state process $S^t$ and a value $V^{\mathrm{on}}=\sum_{t}R(\pi^{\mathrm{on}}(t,S^t,\theta^t),S^t,\theta^t)$, and its regret on a path is $\mathrm{Reg}=V^{\mathrm{off}}(T,s_0)-V^{\mathrm{on}}$. An action is satisfying for Offline at $(t,s)$ when it attains the Bellman maximum. The disagreement set $Q(t,a,s)$ is the set of paths on which it does not, and the marginal compensation $\partial R(t,a,s)$ is the amount by which it falls short.

In the multi-secretary problem there are $n$ classes with rewards $r_1\ge r_2\ge\dots\ge r_n\ge0$ and arrival probabilities $p_j>0$, i.i.d. over time (multinomial arrivals). The state is the remaining budget $b$. Accepting needs $b\ge1$, earns $r_j$ and lowers the budget by one; rejecting earns nothing. With $\bar p_j=\sum_{i\le j}p_i$, the Fluid Bayes Selector (Algorithm 2, in the rounded form of Appendix B.3) behaves as follows at time-to-go $t$ with budget $b$. If $b=0$ it rejects. Otherwise it always accepts class $1$, and it accepts a class $j>1$ iff $b/t\ge\bar p_j-p_j/2$.

Formalization targets

Goal: Theorem 2 (p. 18)

For every horizon $T$ and every initial budget $B$,

$$\mathbb E[\mathrm{Reg}]\ \le\ r_{\max}\sum_{j>1}\frac{2}{p_j}\ \le\ \frac{2(n-1)\,r_{\max}}{p_{\min}},$$

where $r_{\max}=\max_jr_j$ and $p_{\min}=\min_jp_j$. The goal keeps the paper's explicit constant: neither $T$ nor $B$ appears in it.

Milestones

1. Lemma 1 (Compensated Coupling), pathwise: $\mathrm{Reg}=\sum_{t\in[T]}\partial R(t,\pi^{\mathrm{on}}(t,S^t,\theta^t),S^t)\,\mathbf 1_{Q(t,S^t)}$ for any online policy of any problem.
2. Lemma 1, in expectation: $\mathbb E[\mathrm{Reg}]\le\max_{a,j}\partial r(a,j)\sum_t\mathbb P[Q(t,S^t)]$.
3. Eq. (18): $\mathbb P[X-\mathbb E X\le-t\varepsilon]$ and $\mathbb P[X-\mathbb E X\ge t\varepsilon]$ are at most $e^{-2\varepsilon^2t}$ for $X\sim\mathrm{Bin}(t,\alpha)$.
4. Appendix B.3, conditions (1)–(2): when Offline is not satisfied rejecting or accepting the current arrival.
5. Appendix B.3, disagreement bound: $q_1(t,b)=0$ and $q_j(t,b)\le e^{-p_j^2t/2}$ for $j>1$, uniformly in the budget $b$.
6. Appendix B.3, total compensation: $\sum_{t\le T}q(t,B^t)\le\sum_{j>1}p_j\sum_{t\le T}e^{-p_j^2t/2}\le\sum_{j>1}2/p_j$.

Significance

The result. Theorem 2 gives the best known regret bound for the multi-secretary problem with an explicit, simple constant. The compensated coupling (Lemma 1) holds for any finite-horizon problem with exogenous arrivals. It turns a regret bound into a bound on disagreement probabilities, and the paper reuses it for online packing, online matching and general online allocation, and for Bayes Selectors whose disagreement probabilities are only estimated.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of the compensated coupling, is known to us. The mission produces a reusable formal model of finite-horizon online decision problems with an Offline benchmark. It also produces a formal compensated-coupling identity that applies to any policy, and a binomial Chernoff–Hoeffding bound in elementary finite-sum form. Each of these supports other missions on prophet benchmarks, resolving heuristics and network revenue management.

Difficulty

Comparing the online policy with one fixed offline solution does not work: Offline's optimal decisions change with every future arrival, and tracking a single offline plan only gives regret of order $\sqrt T$. The compensated coupling avoids this by re-coupling Offline to Online at every step. That shifts the difficulty to two places. The first is an exact description of when Offline's Bellman equation disagrees with the policy, which involves ties between equal rewards and the boundary budget $b=0$. The second is a bound on the conditional probability of disagreement that is uniform over all budgets. That conditional probability is a binomial tail evaluated at a budget that is itself random but independent of the remaining arrivals.

Formalization scope

Lean conventions:

• Types are Fin n with [NeZero n], and Lean index 0 is the paper's class $1$.
• The ordering $r_1\ge\dots\ge r_n$ is Antitone r, so ties are allowed.
• Rewards are real and non-negative. This is the paper's implicit assumption (rewards are abilities), made explicit.
• The probabilities satisfy $p_j>0$ and $\sum_jp_j=1$.
• Time is time-to-go. θ t is the arrival at time-to-go t, and the counts $Z(t)$ include the current arrival.
• Feasibility is an explicit set of actions rather than a reward of $-\infty$. Offline's value is a real supremum over feasible actions, which equals the Bellman maximum under the standing assumption.
• Offline is the integer full-information optimum of the Bellman equation (2). It is not defined through an LP relaxation.
• For the multi-secretary goal, the expectation is the explicit finite sum over the $n^T$ type sequences weighted by $\prod_tp_{\theta^t}$. Lemma 1's expectation bound is stated on an abstract probability space with integrable regret.
• $\mathbb E[\mathbb P[Q\mid S^t]]$ is written as $\mathbb P[Q]$ (tower property).
• The maximal compensation $\max_{a,j}\partial r(a,j)$ is replaced by any upper bound $C$ on the compensations of feasible actions.
• Conditions (1)–(2) of Appendix B.3 are stated through counts of future arrivals with a better (or equal) reward, which is the exact Bellman characterization. The paper phrases them through a solution $X^{\star t}$ of $(P^\star_t)$, which is not unique when rewards tie.
• The disagreement bounds are stated for every fixed budget $b$, and the total-compensation bound for every budget sequence. Since $B^t$ is independent of the last $t$ arrivals, these imply the paper's statements at the random budget $B^t$.

The policy is the rounded rule of Appendix B.3, which always accepts class $1$ when the budget is positive. Algorithm 2 read literally would reject class $1$ when $b<tp_1/2$, and the bound $\sum_{j>1}$, which excludes class $1$, is proved for the Appendix B.3 rule. The policy is defined by its explicit thresholds and not through an arbitrary optimal solution of the fluid LP, because with tied rewards that LP has several solutions.

A formalization that replaced the expectation by a Bochner integral of a non-measurable function, or Offline by a fluid relaxation, would make the bound trivial or a different theorem. Both are excluded by construction.

Contributions are welcome at every level: proofs of the milestones, a proof of Eq. (18) from Mathlib's sub-Gaussian machinery, and lemmas computing Offline's value in the multi-secretary problem (the top-$b$ rewards among the remaining arrivals), which are reusable beyond this mission.

Selected references

• A. Vera and S. Banerjee, The Bayesian Prophet: A Low-Regret Framework for Online Decision Making, SSRN 3158062 (Management Science 67(3), 2021). https://doi.org/10.2139/ssrn.3158062
• A. Arlotto and I. Gurvich, Uniformly bounded regret in the multisecretary problem, Stochastic Systems 9(3), 2019. https://doi.org/10.1287/stsy.2018.0028
• D. Dubhashi and A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274