Dynamic Programming

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

Motivation

Mean-field games describe large populations of identical agents who interact only through the distribution of their states. Each agent solves a stochastic control problem in which the population appears through a deterministic flow of distributions, and an equilibrium requires that this flow coincide with the distribution the agents generate themselves. The theory goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007) in continuous time. In discrete time, Saldi, Başar and Raginsky (SIAM J. Control Optim. 2018) proved existence of equilibria for risk-neutral agents with discounted costs on Polish state spaces.

Risk-neutral agents care only about expected cost. Many applications in engineering and finance call for agents that also penalize the variability of their cost. A standard way to model this is the exponential (risk-sensitive) criterion $E[\exp(\lambda\cdot\text{cost})]$ with risk factor $\lambda>0$. Its theory for single-agent Markov decision processes goes back to Howard and Matheson (1972) and Jacobson (1973), and Bäuerle and Rieder (Math. Oper. Res. 2014) treat general utilities. Saldi, Başar and Raginsky (arXiv:1808.03929, Math. Oper. Res. 2020) carry the discrete-time mean-field program over to this criterion. This mission covers its first main result: existence of a mean-field equilibrium (Theorem 1).

Setting

The state space $\mathsf X$ and the action space $\mathsf A$ are Polish, and $\mathsf A$ is compact. $\mathcal P(E)$ denotes the probability measures on $E$, with the topology of weak convergence and its Borel σ-field. The model consists of:

• a stochastic kernel $p(\cdot\,|\,x,a,\mu)$ on $\mathsf X$ given $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$;
• a one-stage cost $c(x,a,\mu)\in[0,K]$;
• an initial law $\mu_0$, a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$.

A Markov policy is a sequence $\pi=(\pi_t)_{t\ge0}$ of kernels $\pi_t(da\,|\,x)$. A policy in general is allowed to depend on the whole history $(x(0),a(0),\dots,x(t))$. Given a measure flow $\mu=(\mu_t)_{t\ge0}\subset\mathcal P(\mathsf X)$, a generic agent evolves as

$$x(0)\sim\mu_0,\qquad a(t)\sim\pi_t(\cdot\,|\,\text{history}),\qquad x(t+1)\sim p(\cdot\,|\,x(t),a(t),\mu_t),$$

and pays the risk-sensitive cost

$$J_\mu(\pi)=E^\pi\Big[\exp\Big(\lambda\sum_{t=0}^\infty\beta^tc(x(t),a(t),\mu_t)\Big)\Big].$$

For a Markov policy, $\Lambda(\pi)$ is the flow of state laws it generates: it starts at $\mu_0$ and satisfies $\mu_{t+1}(\cdot)=\int p(\cdot\,|\,x,a,\mu_t)\,\pi_t(da|x)\,\mu_t(dx)$. A pair $(\pi,\mu)$ is a mean-field equilibrium if $\mu=\Lambda(\pi)$ and $\pi$ minimizes $J_\mu$ over all policies.

Assumption 1 asks for the following:

• (a) $c$ is continuous with $\|c\|\le K$;
• (b) $p$ is weakly continuous in $(x,a,\mu)$;
• (c) $\mathsf A$ is compact;
• (d) there are $\alpha\ge0$ and a continuous moment function $w\ge1$ (compact sets $K_n\uparrow\mathsf X$ with $\inf_{x\notin K_n}w(x)\to\infty$) with $\int w(y)\,p(dy|x,a,\mu)\le\alpha w(x)$;
• (e) $\int w\,d\mu_0<\infty$.

Formalization targets

Goal: Theorem 1 (p. 10)

Under Assumption 1 there are a Markov policy $\pi$ and a flow $\mu$ with

$$\mu=\Lambda(\pi)\qquad\text{and}\qquad J_\mu(\pi)=\inf_{\sigma\in\Pi}J_\mu(\sigma).$$

Milestones

In the paper's order of proof:

1. Proposition 1: Markov policies achieve the optimal value.
2. Lemmas 1–3: the finite- and infinite-horizon optimal value functions $J^n_k(\cdot,\lambda\beta^k)$ and $J_k(\cdot,\lambda\beta^k)$ of the nonhomogeneous MDP of a fixed flow are bounded and continuous. They satisfy the dynamic programming equation $T_kJ_{k+1}(\cdot,\lambda\beta^{k+1})=J_k(\cdot,\lambda\beta^k)$, and

$$\big\|J^n_k(\cdot,\lambda\beta^k)-J_k(\cdot,\lambda\beta^k)\big\|\le\frac{\lambda K}{1-\beta}e^{\frac{\lambda\beta^kK}{1-\beta}}\beta^{n+1}.$$

3. Theorem 2: a Markov policy is optimal if and only if it almost surely selects minimizers in the dynamic programming equation.
4. Propositions 2–5 and Lemma 4: equilibria are fixed points of a set-valued map $\Gamma$ on state–action flows in $\Xi=\prod_t\{\nu:\nu_1(w)\le\alpha^tM\}$; the optimal value functions depend continuously on the flow; and the graph of $\Gamma$ is closed in $\Xi\times\Xi$.

Significance

The result. Theorem 1 is what makes the second main result of the paper meaningful. That result, Theorem 3 and the second mission of this series, states that the equilibrium policy is an $\varepsilon$-Markov–Nash equilibrium of every $N$-agent game with $N$ large enough. Equilibria of finite risk-sensitive games with many agents are rarely computable, so a mean-field equilibrium gives an approximately optimal decentralized policy that ignores the other agents' states. Along the way, the paper proves results on nonhomogeneous risk-sensitive MDPs that it describes as "mostly absent and dispersed in the literature": uniform finite-to-infinite horizon bounds and a characterization of optimal Markov policies. These results are useful outside game theory.

Formalizing it. The result is proved on paper. No part of it, nor of the risk-neutral precursor, has a machine-checked proof. Formalization produces a verified theory of nonhomogeneous risk-sensitive MDPs on Polish spaces, a verified closed-graph argument for the mean-field map, and an exact record of the hypotheses. The paper omits or cites several steps: Proposition 1, Proposition 2, Lemma 2, the conditional optimality (8) and the nonemptiness and convexity of $\Gamma(\nu)$. A formalization has to supply them.

Difficulty

The obvious route is Banach's fixed point theorem for the dynamic programming operator, as in risk-neutral discounted MDPs. It fails here: the cost is multiplicative, and the operator $T_k$ is not a contraction. Uniform convergence of value iteration has to come from the explicit tail bound of Lemma 3 instead.

The second obstacle is the fixed point itself. The natural map, from a flow to the flows of its optimal policies, is set-valued and lives on an infinite product of spaces of measures. Kakutani–Fan–Glicksberg applies only after three steps:

• re-encoding the problem on state–action flows (the map $\Gamma=C\cap B$);
• proving compactness of $\Xi$ through the moment function (tightness);
• proving that the graph of $\Gamma$ is closed (Proposition 4).

The last step requires the optimal value functions to vary continuously with the flow (Proposition 5) and a portmanteau argument for sets defined by optimality conditions. None of this machinery (the Kakutani–Fan–Glicksberg theorem in locally convex spaces, Prokhorov compactness via moment functions, continuous convergence) is in Mathlib in the required form.

Formalization scope

$\mathcal P(E)$ is a type synonym of Mathlib's ProbabilityMeasure E with the weak topology and its Borel σ-field. The kernel $p$ is a Mathlib Kernel on $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$. Policies are sequences of Markov kernels, and history-dependent policies take $(\mathsf X\times\mathsf A)^t\times\mathsf X$ as input. The law $P^\pi$ is built with the Ionescu–Tulcea kernel Kernel.trajMeasure, one coordinate $(x(t),a(t))$ per time step. Time is $0$-based.

Standing hypotheses on every statement:

• $\mathsf X$ and $\mathsf A$ are Polish and Borel;
• $\mathsf A$ is compact and nonempty (used tacitly by the paper);
• $\beta\in(0,1)$, $\lambda>0$, and $c\ge0$ is measurable;
• Assumption 1.

For §4.2 the pair $(\alpha,w)$ defining $\Xi$ is an explicit argument. In §4.1, "policy" means Markov policy, as the paper states on p. 11. The conditional expectations "given $x(k)=x$" are expectations for the chain started at time $k$ in $x$. Lemma 1 is stated with $\zeta_{k,n}=\sum_{t=k}^n\beta^t$, the quantity its proof uses; the page prints $\sum_{t=k}^n\beta^k$.

The goal asks for a Markov equilibrium policy that is optimal against all history-dependent policies, at least as strong as Definition 3. Optimality is "$\le$ the cost of every policy", not an infimum, so it has no junk case. The cost is a genuine integral: with $c\ge0$ bounded, the integrand lies in $[1,e^{\lambda K/(1-\beta)}]$, so no policy is trivially optimal. The moment-function predicate has no infimum, so compact $\mathsf X$ is admitted.

Contributions are welcome at every level:

• risk-sensitive dynamic programming on Borel spaces (reusable for any MDP);
• the Kakutani–Fan–Glicksberg theorem in locally convex spaces;
• Prokhorov compactness from moment functions;
• measurable selection and disintegration of state–action measures.

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
• 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://doi.org/10.1137/17M1112583
• 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
• C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis, 3rd ed., Springer, 2006. https://doi.org/10.1007/3-540-29587-9

Motivation

Many platforms match two sides of a market over time: ride-hailing platforms match riders with drivers, blood banks match donated units with patients, organ allocation matches donors with recipients, and retailers pool inventory across fulfilment centres to serve orders from several regions. Demand and supply arrive in several types (locations, blood groups, quality grades), the reward of a match depends on both types, and whatever is not matched today partly waits for tomorrow. A central operational question is which pairs to match first. Static versions of this question go back to the transportation problem and to Monge sequences: Hoffman (1963) characterized the cost matrices for which a fixed greedy order of the arcs solves a transportation problem.

Hu and Zhou (arXiv:1811.07048, published in Manufacturing & Service Operations Management 24(1), 2022) extend this to a stochastic, multi-period setting. They identify conditions on the rewards, the (weak) modified Monge conditions, under which an optimal dynamic policy matches a dominant pair before the neighbouring pairs it dominates. This mission formalizes their main structural result, Theorem 1, and the chain of results it rests on.

Setting

There are $m$ demand types $\mathcal D=\{1,\dots,m\}$, $n$ supply types $\mathcal S=\{1,\dots,n\}$, and $T$ periods $t=1,\dots,T$. In period $t$ the state is a pair of vectors $(\mathbf x,\mathbf y)\in\mathbb R^m_+\times\mathbb R^n_+$ of available demand and supply. The firm chooses a matching decision $\mathbf Q=(q_{ij})\in\mathbb R^{m\times n}$, collecting the reward

$$\mathbf R^t\circ\mathbf Q=\sum_{i=1}^m\sum_{j=1}^n r^t_{ij}q_{ij},$$

where the rewards $r^t_{ij}$ are arbitrary real numbers. The post-matching levels are $u_i=x_i-\sum_j q_{ij}$ and $v_j=y_j-\sum_i q_{ij}$, and $\mathbf Q$ is feasible if $\mathbf Q\ge0$, $\mathbf u\ge0$ and $\mathbf v\ge0$. A fraction $\alpha\in[0,1]$ of unmatched demand and $\beta\in[0,1]$ of unmatched supply carries over, and new random quantities $(\mathbf D^{t+1},\mathbf S^{t+1})\ge0$ arrive. The value function $V_t$ is defined by the dynamic program

$$V_t(\mathbf x,\mathbf y)=\max_{\mathbf Q\ \text{feasible}}H_t(\mathbf Q,\mathbf x,\mathbf y),\qquad H_t(\mathbf Q,\mathbf x,\mathbf y)=\mathbf R^t\circ\mathbf Q+\mathbb E\,V_{t+1}(\alpha\mathbf u+\mathbf D^{t+1},\beta\mathbf v+\mathbf S^{t+1}),$$

with $V_{T+1}\equiv0$. A matching policy assigns a feasible decision $\mathbf Q^t(\mathbf x,\mathbf y)$ to every period and state; it is optimal if each of these decisions maximizes $H_t$.

Two neighbouring pairs are compared by the relation $\succ_{\mathcal M}$. For $i'\ne i$, $(i,j)\succ_{\mathcal M}(i',j)$ means $r^t_{ij}>r^t_{i'j}$ for all $t$, and $r^t_{ij}-r^t_{i'j}\ge\alpha(r^{t+1}_{ij''}-r^{t+1}_{i'j''})$ for all $t\le T-1$ and all $j''$; the relation $(i,j)\succ_{\mathcal M}(i,j')$ is defined symmetrically with $\beta$. The modified Monge condition requires $r^t_{ij}+r^t_{i'j'}\ge r^t_{ij'}+r^t_{i'j}$ whenever $(i,j)$ dominates both $(i',j)$ and $(i,j')$; the paper then writes $\succ_{\mathcal M_s}$. For a pair $(i,j)$, let $a_i$ be the type-$i$ demand left after matching $i$ through all pairs that $(i,j)$ does not dominate, and $b_j$ the analogous supply residual. A decision respects $\succ_{\mathcal M_s}$ if $(i,j)\succ(i',j)$ implies $q_{i'j}=0$ or $a_i=0$, and $(i,j)\succ(i,j')$ implies $q_{ij'}=0$ or $b_j=0$.

Formalization targets

Goal: Theorem 1 (p. 12)

Under the modified Monge condition there is a single policy $P$ such that, for all $1\le t\le T$ and all $\mathbf x,\mathbf y\ge0$,

$$P_t(\mathbf x,\mathbf y)\ \text{is optimal}\quad\text{and}\quad P_t(\mathbf x,\mathbf y)\ \text{respects}\ \succ_{\mathcal M_s}.$$

Milestones

• Proposition 1 (p. 10): $V_t$ and $H_t$ are continuous and concave, and an optimal policy exists.
• Lemma A.1 (Online Appendix A, p. 1): shifting $\varepsilon$ units of demand from type $i$ to type $i'$ (or of supply from $j$ to $j'$) changes $V_t$ by at least $-\sum_\tau\sum_{j'}\lambda^\tau_{j'}(r^\tau_{ij'}-r^\tau_{i'j'})$ for some nonnegative multipliers with $\sum_\tau\alpha^{-(\tau-t)}\sum_{j'}\lambda^\tau_{j'}\le\varepsilon$.
• Lemma A.2 (p. 3): transferring matching quantity from a dominated pair to a dominant one weakly increases $H_t$.
• Theorem 2 (p. 28): without the Monge condition, some optimal policy weakly respects $\succ_{\mathcal M}$: $q_{i'j}=0$ or $u_i=0$, and $q_{ij'}=0$ or $v_j=0$.
• Monge exchange (proof of Theorem 1, p. 4): the transfer $\mathbf Q+\varepsilon(\mathbf e_{ij}+\mathbf e_{i'j'}-\mathbf e_{i'j}-\mathbf e_{ij'})$ stays feasible and weakly increases $H_t$.
• Properties (i)–(iii) imply compatibility (proof of Theorem 1, p. 5).

Significance

Theorem 1 replaces the search over all optimal policies, which are state-dependent and generally complex, by a priority structure: whenever $(i,j)$ dominates a neighbour, the neighbour is matched only once the residual capacity of $(i,j)$ is exhausted. The paper derives from it the optimality of greedy matching for "perfect" pairs (Proposition 2), the priority order for horizontal (distance-based) and vertical (quality-based) reward structures, and the match-down-to threshold structure of the optimal policy in those models. These results generalize inventory rationing and capacity allocation with upgrading.

The result is proved in the paper, but not completely: the limit argument in the printed proofs of Theorems 1 and 2 ("the quantity transferred converges to zero") is not justified, and Proposition 1 has no printed proof in this version. A machine-checked development would close these gaps and would provide a reusable finite-horizon model with continuous states, concave value functions and an exchange-argument toolkit. No part of this mission is known to be formalized.

Difficulty

The obvious argument starts from an optimal decision and repeatedly applies the transfers of Lemma A.2 and the Monge exchange. Each transfer preserves optimality, but nothing in the printed argument guarantees that the procedure terminates or that its limit has the required property: transfers of different kinds can undo each other's progress, and with equal rewards they can cycle forever. A complete proof has to select the right optimal decision without relying on such an iteration. Before that, the dynamic program itself needs care: the value function is a supremum of an expectation of the next value function, so continuity, concavity, measurability and integrability have to be established together by backward induction, and attainment of the maximum is needed for any optimal policy to exist. Lemma A.1 is a further backward induction in which the multipliers become random and must be averaged.

Formalization scope

The Lean development lives in the namespace DynTypeMatching.Priority. Types are Fin m and Fin n; states are Fin m → ℝ, Fin n → ℝ; decisions are Fin m → Fin n → ℝ. Periods are natural numbers with the paper's 1-based indexing, and $V_t=0$ for $t>T$. A model Model m n carries $T$, the rewards, $\alpha$, $\beta$ and one arrival law per period on $\mathbb R^m\times\mathbb R^n$. The paper permits exogenous correlation between periods; its recursion (1) uses per-period laws and does not specify a joint arrival process. The expectation in $H_t$ is over the law of the arrivals entering period $t+1$.

Every result assumes Model.WellPosed: each arrival law is a probability measure, supported on the nonnegative orthant and integrable, and $0\le\alpha,\beta\le1$. Integrability is not stated in the paper, but without it the expectation in (1) is undefined. The value function is a real supremum and the expectation a Bochner integral, so outside the nonnegative orthant, or for non-integrable integrands, Lean returns the junk value 0. All statements therefore quantify over nonnegative states and feasible decisions.

The following hypotheses are added relative to the page, and each is disclosed in the item where it occurs:

• Definition 1(i) is strict, $r^t_{ij}>r^t_{i'j}$, and the neighbours are distinct. With the printed weak inequality, Theorems 1 and 2 are false. Take $m=3$, $n=1$, $T=1$, all rewards equal to 2, $\mathbf x=(0,1,1)$, $\mathbf y=(1)$. Then types 2 and 3 dominate each other, every optimal decision matches one unit, and no such decision respects the relation.
• Definition 1(ii) is required only for $t+1\le T$, because $r^{T+1}$ is not part of the model.
• Lemma A.1 assumes $\alpha>0$ in part (i) and $\beta>0$ in part (ii), because $\alpha^{-(\tau-t)}$ is undefined at $\alpha=0$.
• Lemma A.2 assumes that $\mathbf Q$ itself is feasible.

Several printed index slips are corrected: the doubled $\varepsilon\mathbf e_{ij}$ in the Monge exchange, the index ranges in Lemma A.1, and "and" for "or" in the compatibility step.

An optimal decision is defined as a feasible maximizer of $H_t$ over feasible decisions, not through the equation $V_t=H_t$. This rules out a trivializing reading of the goal: a decision that respects the relation but is not optimal (for instance $\mathbf Q=0$) does not satisfy it. The goal asserts one policy that is optimal and compatible at the same time.

A complete development needs measurable-function and Bochner-integral calculus on finite-dimensional spaces, concavity and continuity of parametric suprema over polytopes, and compactness arguments for attainment. The model and the exchange lemmas are reusable for later missions on this paper (greedy matching, horizontal and vertical models). Proofs of any milestone are welcome, and so are alternative proofs of the goal.

Selected references

• Ming Hu, Yun Zhou, Dynamic Type Matching, arXiv:1811.07048v1, 2018; Manufacturing & Service Operations Management 24(1), 2022. https://arxiv.org/abs/1811.07048 · https://doi.org/10.1287/msom.2020.0952
• Alan J. Hoffman, On simple linear programming problems, Convexity, Proc. Symposia in Pure Mathematics 7, AMS, 1963, 317–327. https://doi.org/10.1090/pspum/007/0157783
• Rainer E. Burkard, Bettina Klinz, Rüdiger Rudolf, Perspectives of Monge properties in optimization, Discrete Applied Mathematics 70(2), 1996, 95–161. https://doi.org/10.1016/0166-218X(95)00103-X

Motivation

A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.

Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.

Setting

The hidden state space is $X=\{1,2\}$ and the observation space is $Y=[0,1]$ with Lebesgue probability measure $m$. The action space is $A=\{0\}\cup\{1/n:n=1,2,\ldots\}$, equipped with the topology inherited from $\mathbb R$. The state does not move: its transition law $P(\cdot\mid x,a)$ is the point mass at $x$ for every action. Its continuity in total variation is immediate from this fixed-state behavior.

At hidden state 1 the observation law is always $m$. At hidden state 2, action zero also produces $m$. Under action $1/n$, state 2 produces a law $m^{(n)}=f^{(n)}m$. The density $f^{(n)}$ equals zero on the open left half of each cell in the $2^n$-part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as $n$ grows, and the paper establishes $m^{(n)}(C)\to m(C)$ for every fixed Borel set $C$. Thus the observation kernel $Q(\cdot\mid a,x)$ is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.

A belief $z\in\mathcal P(X)$ assigns a probability to each hidden state. For a current belief $z$ and an action $a$, the joint law $R(\cdot\mid z,a)$ covers the next state and its observation, and $R'(\cdot\mid z,a)$ is the observation marginal. A filter $H(z,a,y)$ is a conditional law of the next state given observation $y$: it satisfies the disintegration identity (3.3). The belief transition $q_H(\cdot\mid z,a)$ is the law of the random posterior $H(z,a,y)$ when $y$ has law $R'(\cdot\mid z,a)$. These objects are defined in (3.1)–(3.5) of the paper. Different versions of $H$ agree only almost everywhere for each current belief and action, yet they yield the same belief transition.

Formalization targets

Example 4.1: failure of weak belief continuity

At the uniform belief $z=(1/2,1/2)$, action zero reveals nothing, while every positive-index action produces the same two-point posterior law:

$$q_H(\cdot\mid z,0)=\delta_z,\qquad q_H(\cdot\mid z,1/n)=\tfrac34\delta_{(1/3,2/3)}+\tfrac14\delta_{(1,0)} \quad(n\ge1).$$

The mission's goal asserts that $P$ is total-variation continuous, $Q$ is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as $1/n\to0$. It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of $Q$, the two posterior values almost everywhere, and the explicit laws of $q_H$.

Significance

The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.

A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.

Difficulty

Setwise continuity controls $Q(C\mid a,x)$ for each fixed Borel set $C$. A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with $n$, so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of $Q$ to weak convergence of $q_H$.

The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every $y$ would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of $H$.

Formalization scope

Lean represents $X$ by Fin 2, with 0 for the paper's state 1 and 1 for state 2; $Y$ by unitInterval; and $A$ by the specified subtype of $\mathbb R$. Positive integers are a subtype of $\mathbb N$, so the density and the action $1/n$ are never evaluated at $n=0$. The measure $m$ is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition $P$ and observation law $Q$ use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete $Q$ and existence of a valid $H$, guarding the universal filter clause against vacuity.

Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of $q_H$ carries the Borel σ-algebra of the weak topology on $\mathcal P(X)$, stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in $y$ for fixed $(z,a)$ in both structures. Joint measurability in $(z,a,y)$ is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.

No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on $A$, or a claim for only one version of $H$ would change the counterexample and is excluded by the definitions and goal.

Selected references

• E. A. Feinberg, P. O. Kasyanov, and M. Z. Zgurovsky, Partially Observable Total-Cost Markov Decision Processes with Weakly Continuous Transition Probabilities, Mathematics of Operations Research 41(2), 2016; arXiv:1401.2168v2. This mission follows the pinned preprint's numbering and pages.

Motivation

A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.

Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.

Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.

Setting

Fix a horizon $T>0$, dimensions $n,d,\ell\in\mathbb N$, a nonempty Polish space $(U,\rho)$ of control values, a point $u_0\in U$ and an exponent $p\ge0$. Let $\mathcal C^k:=C([0,T],\mathbb R^k)$ with the uniform norm, $\mathcal P(E)$ the Borel probability measures on $E$ with the weak topology, and $x_{t\wedge\cdot}$ the path $x$ stopped at time $t$. The coefficients $b,\sigma,\sigma_0,L$ are maps $[0,T]\times\mathcal C^n\times\mathcal P(\mathcal C^n\times U)\times U\to\mathbb R^n,\mathbb R^{n\times d},\mathbb R^{n\times\ell},\mathbb R$, and $g:\mathcal C^n\times\mathcal P(\mathcal C^n)\to\mathbb R$; all are Borel measurable, and $b,\sigma,\sigma_0,L$ depend on the path and the measure only through their restrictions to $[0,t]$ (non-anticipative).

A weak control $\gamma$ with initial condition $(t,\nu)\in[0,T]\times\mathcal P(\mathcal C^n)$ consists of a probability space carrying two filtrations $\mathbb F^\gamma\supseteq\mathbb G^\gamma$ (the second models the common noise), a state $X^\gamma$, Brownian motions $W^\gamma$ (idiosyncratic) and $B^\gamma$ (common) on $[t,T]$, a predictable $U$-valued control $\alpha^\gamma$, and measure-valued processes $\mu^\gamma_s=\mathcal L(X^\gamma_{s\wedge\cdot}\mid\mathcal G^\gamma_s)$ and $\bar\mu^\gamma_s=\mathcal L((X^\gamma_{s\wedge\cdot},\alpha^\gamma_s)\mid\mathcal G^\gamma_s)$, such that $X^\gamma_{t\wedge\cdot}\sim\nu(t)$, an integrability condition of order $p$ holds, a compatibility condition between the two filtrations holds, and

$$dX^\gamma_s=b(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+\sigma(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dW^\gamma_s+\sigma_0(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dB^\gamma_s,\qquad s\in[t,T].$$

The reward and the value function are

$$J(t,\gamma)=\mathbb E\Big[\int_t^TL(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+g(X^\gamma_{T\wedge\cdot},\mu^\gamma_T)\Big],\qquad V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}J(t,\gamma),$$

with $\infty-\infty:=-\infty$ and $\sup\emptyset=-\infty$. Each weak control also carries $A^\gamma_s=\int_t^{s\vee t}\pi(\alpha^\gamma_r)\,dr$, where $\pi$ is a Borel isomorphism of $U$ onto a subset of $[0,1]$, and the continuous conditional-law process $\hat\mu^\gamma$ of $(X^\gamma,A^\gamma,W^\gamma,B^\gamma)$ given $\mathbb G^\gamma$.

Formalization targets

Goal: Theorem 3.1

$V_W:[0,T]\times\mathcal P(\mathcal C^n)\to[-\infty,\infty]$ is upper semi-analytic (every superlevel set $\{V_W>c\}$ is analytic), and for every stopping time $\tau^\star$ of the canonical filtration of $\Omega^\star:=\mathcal C^\ell\times C([0,T],\mathcal P(\mathcal C^n\times\mathcal C\times\mathcal C^d\times\mathcal C^\ell))$ with values in $[t,T]$, setting $\tau^\gamma:=\tau^\star(B^{\gamma,t},\hat\mu^\gamma)$,

$$V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}\mathbb E\Big[\int_t^{\tau^\gamma}L(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})\Big].$$

Milestones

The canonical reformulation on $\bar\Omega:=\hat\Omega\times C([0,T],\mathcal P(\hat\Omega))$ with weak control rules $\bar{\mathcal P}_W(t,\nu)$ (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 ($V_W(t,\nu)=\sup_{\bar{\mathbb P}\in\bar{\mathcal P}_W(t,\nu)}J(t,\bar{\mathbb P})$), Lemma 4.7 (analytic graphs, $V_W$ u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through $\hat\nu(t)$), (4.10) (moment truncation $V^M_W\nearrow V_W$, analytic and u.s.a.) and Lemma 4.10 (universally measurable $\varepsilon$-optimal families and concatenation).

Significance

The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.

Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.

Difficulty

The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: $V_W$ is not known to be measurable, so $\mathbb E[V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})]$ is not obviously meaningful; conditioning a weak control on its information at $\tau^\gamma$ need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as $\mu^\gamma_{\tau^\gamma}$ need a continuous version.

Formalization scope

The Lean development lives in the namespace MKVDPP.Weak. Conventions:

• Times are in $\mathbb R_{\ge0}$; paths are elements of $C([0,T],\mathbb R^k)$ with $\mathbb R^k$ Euclidean; a path is read at times beyond $T$ as its value at $T$.
• Expectations and time integrals are $\mathbb E[\xi^+]-\mathbb E[\xi^-]$ in $[-\infty,\infty]$ with $\infty-\infty=-\infty$, computed as lower integrals.
• The supremum defining $V_W$ ranges over weak controls on probability spaces in Type (universe 0).
• "The integrals are implicitly assumed to be well-defined" is pinned to local Itô integrals (EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on $[t,T]$, taken against the shifted Brownian motions $W^{\gamma,t}$, $B^{\gamma,t}$; no $L^2(\mathbb P)$ condition, which would shrink $\Gamma_W$.
• The conditional-law requirement "for $d\mathbb P\otimes ds$-a.e. $(s,\omega)$" is read in Fubini form; $\mu^\gamma_T$ and $\mu^\gamma_{\tau^\gamma}$ are the $X$-marginals of the continuous process $\hat\mu^\gamma$.
• "Local martingale on $[t,T]$" in Definition 4.1 is pinned to: every localised process $S^{\varphi,m}$, $m\ge1$, is an $(\bar{\mathbb F},\bar{\mathbb P})$-martingale on $[t,T]$. The page integrates $|\bar S|$ and $\bar S^\varphi$ from $0$. Here they run from the initial time $t$, because before $t$ the canonical control may be $\partial$, where the coefficients are undefined, and a coefficient that is not integrable before $t$ would empty $\hat{\mathcal P}_W(t,\cdot)$.
• The cemetery value $\partial$ of the canonical control is read as $u_0$ inside the coefficients (a null set under Definition 4.1).
• In (3.2), $(+\infty)+(-\infty)$ inside the expectation is $-\infty$.
• Lemma 4.4(i)'s converse carries the hypothesis that the canonical $A$ is a.s. $\int_t^{\cdot\vee t}\pi(\bar\alpha_r)\,dr$; without it the converse is false, because Definition 4.1 leaves $A$ before $t$ unconstrained.

The goal does not mention the canonical space $\bar\Omega$, weak control rules or any selection; a formalization of $\Gamma_W$ that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case $n=d=\ell=0$ for every $t\le T$, so the structure is satisfiable.

Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable $\sigma$-algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.

Selected references

• M. F. Djete, D. Possamaï, X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, Ann. Probab. 50(2), 2022; cited as arXiv:1907.08860v2. https://arxiv.org/abs/1907.08860v2
• H. Pham, X. Wei, Dynamic programming for optimal control of stochastic McKean–Vlasov dynamics, SIAM J. Control Optim. 55(2):1069–1101, 2017. https://arxiv.org/abs/1604.04057
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3):1641–1672, 2017. https://arxiv.org/abs/1609.08064
• N. El Karoui, X. Tan, Capacities, measurable selection and dynamic programming part II: application in stochastic control problems, 2013. https://arxiv.org/abs/1310.3364
• E. Bayraktar, A. Cosso, H. Pham, Randomized dynamic programming principle and Feynman–Kac representation for optimal control of McKean–Vlasov dynamics, Trans. Amer. Math. Soc. 370(3):2115–2160, 2018. https://doi.org/10.1090/tran/7118
• M. Laurière, O. Pironneau, Dynamic programming for mean-field type control, C. R. Math. Acad. Sci. Paris 352(9):707–713, 2014. https://doi.org/10.1016/j.crma.2014.07.008
• A. Bensoussan, J. Frehse, S. Yam, Mean Field Games and Mean Field Type Control Theory, SpringerBriefs in Mathematics, Springer, 2013. https://doi.org/10.1007/978-1-4614-8508-7
• D. Bertsekas, S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/SOC_1978.pdf
• D. Stroock, S. Varadhan, Multidimensional Diffusion Processes, Springer, 1997. https://doi.org/10.1007/3-540-28999-2