Stochastic Systems

Motivation

Large service systems (call centers, hospital wards, cloud server pools) run with many servers, and for many of them no exact formula describes how the number of busy servers moves over time. Heavy-traffic limits replace such a system by a diffusion process that is easier to analyze. The many-server regime, in which the number of servers and the arrival rate grow together, goes back to Halfin and Whitt (1981) and is the basis of square-root staffing rules in call-center practice.

The simplest many-server model is the $M/M/\infty$ queue. Its stationary number in system is Poisson with mean $\lambda/\mu$, so the centered and $\sqrt n$-scaled stationary count is asymptotically normal when $\lambda_n = n\mu$. The question here is about the whole process: does the scaled number in system converge, as a random path, to a diffusion? The classical answer, the Ornstein–Uhlenbeck limit, was first established by Iglehart (1965) with Stone's theorem for birth-and-death processes, and was revisited by strong approximation (Mandelbaum, Massey and Reiman 1998) and, for general service times, by Krichagina and Puhalskii (1997).

Pang, Talreja and Whitt (2007) is a tutorial survey that proves this limit, and its finite-waiting-room extension, with martingale methods. The authors present the argument as a template for non-Markovian and network models (Reed 2009; Dai and Tezcan; Gurvich and Whitt). This mission formalizes the $M/M/\infty$ result and the steps of the paper's proof.

Setting

Fix a service rate $\mu > 0$. For each $n \ge 1$, the $n$-th system has arrival rate $\lambda_n = n\mu$. Let $A_n$ and $S_n$ be independent Poisson processes of rate $1$, and let $Q_n(0)$ be a random initial number of customers, independent of $A_n$ and $S_n$. The number in system $Q_n(t)$ is the $\mathbb N$-valued process with right-continuous paths having left limits that satisfies, almost surely,

$$Q_n(t) = Q_n(0) + A_n(\lambda_n t) - S_n\Big(\mu \int_0^t Q_n(s)\,ds\Big), \qquad t \ge 0. \qquad (12)$$

The departure term is a random time change: each of the $Q_n(s)$ customers in service completes service at rate $\mu$. The diffusion-scaled process is $X_n(t) = (Q_n(t) - n)/\sqrt n$, the paper's (3). The space $D$ consists of paths on $[0,\infty)$ that are right-continuous with left limits, and $\Rightarrow$ denotes convergence in distribution.

The limit is the Ornstein–Uhlenbeck (OU) process $X$, driven by a standard Brownian motion $B$, with $X(0)$ independent of $B$:

$$X(t) = X(0) + \sqrt{2\mu}\,B(t) - \mu \int_0^t X(s)\,ds, \qquad t \ge 0. \qquad (5)$$

The proof also uses the scaled martingales $M_{n,1}(t) = (A_n(\lambda_n t) - \lambda_n t)/\sqrt n$ and $M_{n,2}(t) = \big(S_n(\mu\int_0^t Q_n) - \mu\int_0^t Q_n\big)/\sqrt n$, the fluid processes $\Psi_{S,n} = Q_n/n$ and $\Phi_{S,n}(t) = \frac{\mu}{n}\int_0^t Q_n(s)\,ds$, and stochastic boundedness. A sequence of real random variables is stochastically bounded if it is tight, and a sequence of processes is stochastically bounded in $D$ if $\sup_{0\le t\le T}|X_n(t)|$ is, for every $T > 0$.

Formalization targets

Goal: Theorem 1.1

If $X_n(0) \Rightarrow X(0)$ in $\mathbb R$, with an arbitrary limit law $\nu$, then

$$X_n \Rightarrow X \quad \text{in } D \text{ as } n \to \infty,$$

where $X$ is the OU process (5) with $X(0) \sim \nu$. The goal fixes no initial distribution and assumes no moment condition on $Q_n(0)$.

Milestones, in the order of the proof

1. Lemma 2.1, that (12) defines $Q$, and Lemma 3.3, the crude bound $Q(t) \le Q(0) + A(\lambda t)$.
2. Lemmas 3.1 and 3.2, which identify $\langle M \rangle$ for compensated counting processes and for random time changes of a Poisson process. Then Theorem 3.4, the martingale representation $X_n = X_n(0) + M_{n,1} - M_{n,2} - \mu\int_0^\cdot X_n$, with $\langle M_{n,1}\rangle(t) = \mu t$ and $\langle M_{n,2}\rangle = \Phi_{S,n}$.
3. Theorem 4.1(i), the continuity of the integral representation; Lemma 4.1, Gronwall's inequality; and Theorem 4.2, the Poisson FCLT.
4. Lemmas 5.9, 5.5, 5.8 and 6.2, the stochastic-boundedness route to the fluid limit.
5. Lemmas 4.3 and 4.2, the fluid limits $Q_n/n \Rightarrow 1$ and $\Phi_{S,n} \Rightarrow \mu e$; then Lemma 4.4, $(M_{n,1}, M_{n,2}) \Rightarrow (\sqrt\mu B_1, \sqrt\mu B_2)$.

Significance

Theorem 1.1 describes the transient behavior of a large infinite-server system, not only its stationary law: fluctuations of order $\sqrt n$ around the offered load $n$ form a Gaussian Markov process that relaxes at rate $\mu$. It is the reference case for the Halfin–Whitt regime, whose finite-server version, Theorem 1.2 of the same paper (the $M/M/n/m_n+M$ queue), is the subject of the companion mission. The milestones are general tools reused well beyond queueing: Gronwall's inequality, the Lipschitz integral map, the Poisson FCLT, stochastic boundedness via Lenglart's inequality, and the fluid limit from stochastic boundedness.

The theorem is proved and classical; no machine-checked proof of it, or of the milestones below, is known. No formal library currently has the Poisson functional central limit theorem in $D$, compensators of counting processes, or random time changes of martingales. Formalizing the paper's proof would produce these, plus a template for the martingale method of heavy-traffic analysis. Alternative proofs, such as the paper's §4.3 route without martingales, are equally welcome as solutions.

Difficulty

Equation (12) is a fixed-point equation: $Q_n$ appears inside the argument of $S_n$. The integral map of Theorem 4.1 is continuous, so the obvious argument is to apply the continuous-mapping theorem to the martingale representation. That reduces the goal to the joint convergence of $(M_{n,1}, M_{n,2})$. But $M_{n,2}$ is a Poisson martingale evaluated at the random time $\Phi_{S,n}(t)$, and its limit is identified only after the fluid limit $\Phi_{S,n} \Rightarrow \mu e$ is known. The fluid limit is itself a statement about the whole sequence $Q_n$, and it needs a separate argument, either Gronwall at fluid scale or stochastic boundedness. Lemma 3.2 requires optional stopping at the continuum of stopping times $I(t)$, and the moment conditions (22) must be checked through the crude bound. Removing $E[Q_n(0)] < \infty$ needs a truncation of the initial conditions (§6.3).

Formalization scope

• Time. Paths are functions $\mathbb R \to \mathbb R$ and every condition is for $t \ge 0$. Brownian motions and filtrations are indexed by $\mathbb R_{\ge 0}$.
• Probability space. All systems live on one probability space. Each $n$ has its own pair of Poisson processes; the paper's single pair is a special case, and weak convergence depends only on laws. Sequences start at $n = 1$.
• Weak convergence in $D$ to a continuous limit is stated in coupling form (CouplingConverges): a Skorokhod representation with almost-sure uniform convergence on compact intervals. Convergence to a deterministic path is uniform convergence on compacts in probability (UocInProb). $X_n(0) \Rightarrow \nu$ is stated with bounded continuous test functions.
• The OU process is the published Erlang-A diffusion with $\beta = 0$ and $\theta = \mu$, whose drift is $-\mu x$. A solution has $X(0) \sim \nu$ independent of $B$ and is adapted to $\sigma(X(0)) \vee \sigma(B(s) : s \le t)$. The goal asserts existence and that every solution is a limit, which carries uniqueness in law. The limit space is in universe Type.
• Predictable quadratic variation is a property, since Mathlib has no Doob–Meyer theorem: $M$ is square integrable, $V$ is adapted, continuous (the paper's "predictable", p. 208), nondecreasing and integrable, and $M^2 - V$ is a martingale. Optional quadratic variations $[M]$ are not stated.
• Filtrations. The filtration of Theorem 3.4 is the generated history augmented by the measurable null sets.
• Norms and suprema. The norm on $\mathbb R^k$ is $\ell^1$, and suprema of paths are taken in $[0, \infty]$.
• Added hypotheses. The statements add three things the printed versions need: $M_n(0) = 0$ in Lemma 5.8 (without it the lemma is false), $S$ an $\mathbf F$-Poisson process and $I(0) = 0$ in Lemma 3.2, and integrability of $g$ in Lemma 4.1.
• Not formalized. Theorem 4.1(ii) ($J_1$ continuity) and the birth-and-death clause of Lemma 2.1.

A formalization that fixes $Q_n(0) = n$, assumes $X_n(0)$ converges almost surely, adds $E[Q_n(0)] < \infty$ to the goal, or replaces convergence in $D$ by convergence of finite-dimensional distributions proves a weaker theorem and does not close the goal.

Contributions are welcome at every level. The Poisson FCLT, Lenglart's inequality and the composition map are reusable library results, independent of queueing.

Selected references

• G. Pang, R. Talreja, W. Whitt, Martingale Proofs of Many-Server Heavy-Traffic Limits for Markovian Queues, Probability Surveys 4 (2007) 193–267. https://arxiv.org/abs/0712.4211 (doi:10.1214/06-PS091)
• D. L. Iglehart, Limit diffusion approximations for the many server queue and the repairman problem, J. Appl. Prob. 2 (1965) 429–441. https://mathscinet.ams.org/mathscinet-getitem?mr=0184302
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29 (1981) 567–588. https://mathscinet.ams.org/mathscinet-getitem?mr=0629195
• A. Mandelbaum, W. A. Massey, M. I. Reiman, Strong approximations for Markovian service networks, Queueing Systems 30 (1998) 149–201. https://mathscinet.ams.org/mathscinet-getitem?mr=1663767
• E. V. Krichagina, A. A. Puhalskii, A heavy-traffic analysis of a closed queueing system with a GI/∞ service center, Queueing Systems 25 (1997) 235–280. https://mathscinet.ams.org/mathscinet-getitem?mr=1458591
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://mathscinet.ams.org/mathscinet-getitem?mr=0838085

Motivation

Large service systems such as call centers, hospital wards and cloud server pools have many parallel servers, finite buffers and customers who leave when they wait too long. Their performance is usually analysed through heavy-traffic diffusion limits: the number of customers in the system, centred and rescaled, converges as the system grows to a diffusion process whose law is computable. The quality-and-efficiency-driven (QED) regime of Halfin and Whitt (Oper. Res. 29, 1981) is the scaling in which the number of servers $n$ and the arrival rate grow together so that the probability of delay stays strictly between $0$ and $1$. Garnett, Mandelbaum and Reiman (M&SOM 4, 2002) proved the QED limit for the Erlang-A model with unlimited waiting room. Whitt (Math. Oper. Res. 30, 2005) added finite waiting rooms of size of order $\sqrt n$, which produce a reflecting upper barrier in the limit.

Pang, Talreja and Whitt (Probab. Surveys 4, 2007) give a self-contained martingale proof of these limits. Theorem 1.2 of that paper, the target of this mission, covers the $M/M/n/m_n+M$ model with finite waiting room and abandonment. It contains the Erlang-B (loss) model ($m_n=0$) and finite-buffer Erlang-C models ($\theta=0$) as special cases.

Setting

Fix a service rate $\mu>0$, an abandonment rate $\theta\ge 0$, a constant $\beta\in\mathbb R$ and a barrier $\kappa\ge 0$. For $n\ge 1$, model $n$ is an $M/M/n/m_n+M$ queue: $n$ servers, a waiting room of $m_n\in\{0,1,2,\dots\}$ places, Poisson arrivals of rate $\lambda_n$, exponential services of rate $\mu$, first-come first-served service, and an exponential patience of rate $\theta$ for each waiting customer. An arrival that finds all $n+m_n$ places occupied is blocked and lost.

The number in system $Q_n(t)$ is constructed from independent rate-1 Poisson processes $A$, $S$, $R$ and an independent initial value $Q_n(0)\le n+m_n$ by

$$Q_n(t)=Q_n(0)+A(\lambda_n t)-S\Big(\mu\!\int_0^t (Q_n(s)\wedge n)\,ds\Big)-R\Big(\theta\!\int_0^t (Q_n(s)-n)^+ds\Big)-U_n(t),$$

where $U_n(t)=\int_{(0,t]}\mathbf 1\{Q_n(s-)=n+m_n\}\,dA(\lambda_n s)$ counts blocked arrivals. The QED scaling is

$$\frac{n\mu-\lambda_n}{\sqrt n}\to\beta\mu,\qquad \frac{m_n}{\sqrt n}\to\kappa,$$

and the scaled process is $X_n(t)=(Q_n(t)-n)/\sqrt n$.

The limit is a reflected diffusion: a pair $(X,U)$ of processes with right-continuous paths with left limits, $X\le\kappa$, $U$ nondecreasing and nonnegative, a standard Brownian motion $B$ independent of $X(0)$, and

$$X(t)=X(0)-\beta\mu t+\sqrt{2\mu}\,B(t)-\int_0^t\big[\mu(X(s)\wedge0)+\theta(X(s)\vee0)\big]ds-U(t),\qquad \int_0^\infty\mathbf 1\{X(t)<\kappa\}\,dU(t)=0 .$$

The regulator $U$ increases only when $X$ sits at $\kappa$.

Formalization targets

Goal: Theorem 1.2

If $X_n(0)\Rightarrow\nu$ in $\mathbb R$, then $X_n\Rightarrow X$ in $D$, where $X$ solves the reflected equation above with $X(0)\sim\nu$, and every solution with initial law $\nu$ has the same law:

$$X_n\Rightarrow X\quad\text{in } D[0,\infty)\qquad (n\to\infty).$$

The goal fixes no rate of convergence and no stationary quantity; it asserts the process limit and its characterization by (9)–(10).

Milestones

1. Theorem 7.4: the martingale representation of $X_n$ as $X_n(0)$ plus scaled Poisson martingales $M_{n,i}$, a drift term, a Lipschitz feedback term and the scaled blocking process $V_n=U_n/\sqrt n$, with the predictable quadratic variations of the $M_{n,i}$.
2. (110): the limit noise $B_1(\mu t)-B_2(\mu t)-B_3(0)$ of three independent Brownian motions has the law of $\sqrt{2\mu}\,B$.
3. Theorem 7.3 (i): the deterministic reflected integral equation $x=b+y+\int_0^\cdot h(x)\,ds-u$ with barrier $\kappa$ and Lipschitz $h$ has a unique solution, depending continuously on $(y,b)$ for uniform convergence on bounded intervals, and continuous when $y$ is.

Significance

The theorem supplies the diffusion approximation behind square-root staffing rules for systems with finite buffers: it says that buffers of order $\sqrt n$ are visible in the limit as a barrier at $\kappa$, and that the limit for $\kappa=0$ (Erlang-B with or without abandonment) is a reflected Ornstein–Uhlenbeck-type process. Stationary blocking and delay probabilities of the limit then approximate those of the large finite system.

The result is proved in the literature (Whitt 2005; Pang, Talreja and Whitt 2007, whose proof of Theorem 1.2 is a sketch built on §7.1). It is not formalized anywhere. A formal proof would supply a checked martingale representation for a birth–death queue with blocking, a checked reflection map with state-dependent drift, and the continuous-mapping step through it. The unlimited-waiting-room case is posed separately on the platform as the Erlang-A limit of Garnett, Mandelbaum and Reiman and is not part of this mission.

Difficulty

The obvious route is the one used for the Erlang-A model: write $X_n$ as a continuous function of the scaled Poisson noise and apply the continuous-mapping theorem. With a finite waiting room this fails as stated, because the blocking process $U_n$ is not a function of the noise alone. It depends on the path of $Q_n$ through the times the system is full. The proof must instead identify $(X_n,V_n)$ as the image of the noise under a reflection map with a drift inside it, prove that this map is well defined and continuous, and control the martingale terms through random time changes whose limits are deterministic. The barrier in model $n$ is $m_n/\sqrt n$, not $\kappa$, so the continuous-mapping step has to handle a moving barrier as well.

Formalization scope

• Paths. Time is real; every path is a function on $\mathbb R$ of which only the values at $t\ge0$ are used. "In $D$" is BellWilliams2001.ThresholdPolicy.IsCadlag. Brownian motion is ErlangA.Diffusion.IsStandardBM, indexed by $\mathbb R_{\ge0}$; martingales are Mathlib Martingales indexed by $\mathbb R_{\ge0}$.
• Model. All systems live on one probability space with their own primitives $A_n,S_n,R_n$; Poisson processes are ManyServerQED.Scheduling.IsPoissonProcess. $Q_n(0)$ is independent of the primitives and $Q_n(t)\le n+m_n$ for all $t\ge0$. Blocked arrivals are counted with the left limit $Q_n(s-)$, correcting (114) as printed. $\theta=0$ and $\kappa=0$ are allowed.
• Weak convergence. $X_n(0)\Rightarrow\nu$ is convergence of expectations of bounded continuous functions. $X_n\Rightarrow X$ in $D$ is BellWilliams2001.ThresholdPolicy.CouplingConverges (Skorohod coupling with almost sure uniform convergence on compacts), equivalent to $J_1$ weak convergence for a continuous limit. Uniform distances use supDist on $\mathbb R^1$.
• Limit. The drift is ErlangA.Diffusion.drift; $X(0)$ is independent of $B$; $X$ and $U$ are adapted to the filtration of $X(0)$ and $B$; condition (10) is "the Lebesgue–Stieltjes measure of $U$, extended by $0$ to negative times, gives zero mass to $\{t\ge0: X(t)<\kappa\}$". Uniqueness is uniqueness in law of $X$. The limit space lives in Type.
• Martingales. "Predictable quadratic variation $V$" means: $V$ adapted with continuous, nondecreasing, nonnegative paths and $M^2-V$ a martingale. The filtration (118) is augmented by the measurable null sets, as the paper states.
• Ruled out. Convergence of finite-dimensional distributions, a deterministic or almost surely convergent initial condition, a fixed barrier $\kappa$ inside the prelimit model, or a solution concept that drops $X\le\kappa$ or the barrier condition (10) would each make the statement weaker or vacuous; none is used.
• Not in scope. The Skorohod $J_1$ continuity in Theorem 7.3 (ii), the Erlang-A Theorem 7.1, and the non-Markovian arrivals of §7.3.

Contributions welcome: Stieltjes-integral and counting-process lemmas for $U_n$, a reflection map with Lipschitz drift on $D[0,\infty)$, the Poisson functional central limit theorem, and martingale facts for randomly time-changed Poisson processes. The last three are reusable well beyond this mission.

Selected references

• G. Pang, R. Talreja, W. Whitt, Martingale proofs of many-server heavy-traffic limits for Markovian queues, Probability Surveys 4 (2007) 193–267. https://arxiv.org/abs/0712.4211 (v1), https://doi.org/10.1214/06-PS091
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29 (1981) 567–588. https://doi.org/10.1287/opre.29.3.567
• O. Garnett, A. Mandelbaum, M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4 (2002) 208–227. https://doi.org/10.1287/msom.4.3.208.7753
• W. Whitt, Heavy-traffic limits for the $G/H_2^*/n/m$ queue, Mathematics of Operations Research 30 (2005) 1–27. https://mathscinet.ams.org/mathscinet-getitem?mr=2125135
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479

Motivation

An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility $U_\gamma(x)=\frac1\gamma x^\gamma$, $\gamma\in(0,1)$, this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.

For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in $z$. The existence theory for such equations is due to Kobylanski (2000).

This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.

Setting

Fix a horizon $T>0$ and a probability space $(\Omega,\mathcal F,P)$ carrying an $m$-dimensional Brownian motion $W$; $\mathbb F$ is the augmentation of its natural filtration. $|\cdot|$ is the Euclidean norm, and $\lambda$ is Lebesgue measure on $[0,T]$.

Market. There is a bond with zero interest and $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$. The rates $b_t\in\mathbb R^d$ and the volatility $\sigma_t\in\mathbb R^{d\times m}$ are predictable and uniformly bounded, and $KI_d\ge\sigma_t\sigma_t^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma_t^{\mathrm{tr}}(\sigma_t\sigma_t^{\mathrm{tr}})^{-1}b_t\in\mathbb R^m$.

Constraints. A closed set $\tilde C\subseteq\mathbb R^{1\times d}$ of row vectors constrains the proportions $\tilde\rho_t$ of wealth held in the stocks. In the variable $\rho_t=\tilde\rho_t\sigma_t\in\mathbb R^{1\times m}$ the constraint reads $\rho_t\in C_t(\omega)=\tilde C\sigma_t(\omega)$. For a closed $C\subseteq\mathbb R^m$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$, and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the (possibly multi-valued) projection.

Wealth and admissible strategies. From initial capital $x>0$ the wealth (11) is

$$X^{(\rho)}_t=x\exp\Big(\int_0^t\rho_s\,dW_s+\int_0^t\rho_s\theta_s\,ds-\tfrac12\int_0^t|\rho_s|^2\,ds\Big).$$

The admissible class $\tilde{\mathcal A}$ (Definition 13) consists of predictable $\rho$ with $\rho_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$ and $\int_0^T|\rho_s|^2\,ds<\infty$ a.s. The value is (12), $\bar V(x)=\sup_{\rho\in\tilde{\mathcal A}}E[U_\gamma(X^{(\rho)}_T)]$.

The BSDE. $\mathcal H^\infty(\mathbb R)$ is the class of predictable, $\lambda\otimes P$-a.e. bounded processes and $\mathcal H^2(\mathbb R^m)$ that of predictable $Z$ with $E\int_0^T|Z_t|^2\,dt<\infty$. The BSDE (15) is

$$Y_t=0-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad f(t,z)=\frac{\gamma(1-\gamma)}2\operatorname{dist}^2\Big(\frac{z+\theta_t}{1-\gamma},C_t\Big)-\frac{\gamma|z+\theta_t|^2}{2(1-\gamma)}-\frac12|z|^2 .$$

A BMO martingale $\int_0^\cdot\xi\,dW$ is one with $\sup_\tau\|E[\int_\tau^T|\xi_s|^2ds\mid\mathcal F_\tau]\|_\infty<\infty$ over stopping times $\tau\le T$ (equation (2)).

Formalization targets

Goal: Theorem 14

(15) has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, and for $x>0$

$$\bar V(x)=\frac1\gamma\,x^\gamma\exp(Y_0),$$

attained by some $\rho^*\in\tilde{\mathcal A}$ with

$$\rho^*_t\in\Pi_{C_t(\omega)}\Big(\frac1{1-\gamma}(Z_t+\theta_t)\Big).\qquad(16)$$

The page prints $V(x)=x^\gamma\exp(Y_0)$; its proof measures utility by $x^\gamma$, so the value of (12) with $U_\gamma=\frac1\gamma x^\gamma$ carries the factor $\frac1\gamma$ (see Formalization scope).

Milestones

1. (14), p. 17: for $\rho\in C$, $\gamma\rho\theta-\frac12\gamma|\rho|^2+f(z)\le-\frac12|\gamma\rho+z|^2$, with equality on $\Pi_C\big(\frac{z+\theta}{1-\gamma}\big)$.
2. (H1), p. 18: $|f(t,z)|\le c_0+c_1|z|^2$.
3. Existence and 4. uniqueness for (15), p. 18.
4. Lemma 17, p. 20: $\int Z\,dW$ and $\int\rho^*dW$ are BMO martingales.
5. Optimality of $\rho^*$, p. 18: $\rho^*\in\tilde{\mathcal A}$ and $E[(X^{(\rho^*)}_T)^\gamma]=x^\gamma\exp(Y_0)$.
6. Comparison, p. 18: $E[(X^{(\rho)}_T)^\gamma]\le x^\gamma\exp(Y_0)$ for every $\rho\in\tilde{\mathcal A}$.

Significance

The theorem gives the value of a constrained power-utility problem in closed form through one scalar, $Y_0$, of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when $\tilde C$ is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.

The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.

Difficulty

The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like $|z|^2$. Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of $\tilde R^{(\rho^*)}$ need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats $\tilde R^{(\rho)}$ as a martingale for every admissible $\rho$ fails: for a general $\rho\in\tilde{\mathcal A}$, which is only locally square integrable, it is merely a local supermartingale.

Formalization scope

All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m), with products $z\theta$ as inner products; $\tilde C$ is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure $\lambda\otimes P$ and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, $\rho$ and $\theta$; $\theta$ is computed from $b$ and $\sigma$.

Conventions and disclosed readings:

• The factor $\frac1\gamma$. The goal states $\bar V(x)=\frac1\gamma x^\gamma\exp(Y_0)$ for (12) with $U_\gamma$; milestones 6–7 state $E[(X_T)^\gamma]$ against $x^\gamma\exp(Y_0)$, as the proof does.
• Added hypothesis $\tilde C\neq\emptyset$ (needed for (4) and for $\Pi_{C_t}\neq\emptyset$).
• Strategies are written in $\rho=\tilde\rho\sigma\in\mathbb R^m$ (Definition 13 says "$d$-dimensional"); §3's "$\bar C_2\subseteq\mathbb R^d$" and $\tilde C$ are one closed set.
• (16) and the constraint hold $\lambda\otimes P$-a.e.; "$\rho^*$ given by (16)" means any predictable selection.
• $Y_0$ is a.s. constant; the value identity holds for $P$-a.e. $\omega$.
• Uniqueness means $Y^1_t=Y^2_t$ a.s. for every $t$ and $Z^1=Z^2$ $\lambda\otimes P$-a.e.
• Expectations of nonnegative quantities are lower integrals in $[0,\infty]$; the value is a supremum in $[0,\infty]$.
• Ellipticity holds for $P$-a.e. $\omega$ and every $t\le T$; boundedness of $b$, $\sigma$ holds everywhere.

The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable $U_\gamma(X_T)$ is $0$ and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.

Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 2005, 1691–1712. https://doi.org/10.1214/105051605000000188 (arXiv:math/0508448v1, https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 2000, 558–602. https://doi.org/10.1214/aop/1019160253
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 1992, 767–818. https://doi.org/10.1214/aoap/1177005576
• D. Kramkov, W. Schachermayer, The asymptotic elasticity of utility functions and optimal investment in incomplete markets, Ann. Appl. Probab. 9(3), 1999, 904–950. https://doi.org/10.1214/aoap/1029962818
• R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, J. Econom. Theory 3, 1971, 373–413. https://doi.org/10.1016/0022-0531(71)90038-X

Motivation

An investor who trades in a market with fewer stocks than sources of randomness cannot hedge every risk: the market is incomplete. If the investor also faces a liability $F$ due at the horizon $T$ and has to respect trading constraints (no short sales, limits on positions in certain stocks, a ban on trading some assets altogether), the question of how to trade optimally becomes a constrained stochastic control problem. With exponential utility $U(x)=-\exp(-\alpha x)$, its value function gives the investor's utility indifference price of $F$, a standard pricing rule in incomplete markets.

Earlier treatments needed convexity. Cvitanić and Karatzas (Ann. Appl. Probab. 2 (1992)) proved existence and uniqueness for utility maximization in a Brownian filtration with convex constraints, by convex duality. Delbaen, Grandits, Rheinländer, Samperi, Schweizer and Stricker (Math. Finance 12 (2002)) related exponential utility maximization to the martingale measure of minimal relative entropy. El Karoui and Rouge (Math. Finance 10 (2000)) computed the value function and optimal strategy for exponential utility by backward stochastic differential equations (BSDEs), for strategies confined to a convex cone; Sekine (preprint, 2002) obtained the same BSDE from the Cvitanić–Karatzas duality. Hu, Imkeller and Müller (Ann. Appl. Probab. 15 (2005)) gave a direct BSDE solution that works for closed, possibly nonconvex constraint sets, with a bounded liability. The tool is a BSDE whose driver grows quadratically in the control variable, whose solvability rests on Kobylanski's existence theorem for quadratic BSDEs (Ann. Probab. 28 (2000)).

Setting

Fix $T>0$ and an $m$-dimensional Brownian motion $W$ on a probability space $(\Omega,\mathcal F,P)$, and let $\mathbb F=(\mathcal F_t)$ be the $P$-augmentation of the filtration generated by $W$. There are $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$; the drift $b$ and the $d\times m$ volatility matrix $\sigma$ are predictable and uniformly bounded, and $KI_d\ge\sigma\sigma^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma^{\mathrm{tr}}_t(\sigma_t\sigma^{\mathrm{tr}}_t)^{-1}b_t\in\mathbb R^m$.

A strategy is an $\mathbb R^{1\times m}$-valued predictable process $p_t=\pi_t\sigma_t$, where $\pi_t$ is the vector of amounts held in the stocks. Its wealth from initial capital $x$ is

$$X^{(p)}_t=x+\int_0^tp_u\,(dW_u+\theta_u\,du).$$

The constraint is a closed set $\tilde C\subseteq\mathbb R^{1\times d}$, not necessarily convex; in terms of $p$ it reads $p_t\in C_t:=\tilde C\sigma_t$. A strategy is admissible, $p\in\mathcal A$, when $E\int_0^T|p_t|^2dt<\infty$, $p_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$, and $\{\exp(-\alpha X^{(p)}_\tau):\tau\le T\text{ a stopping time}\}$ is uniformly integrable. The value function is

$$V(x)=\sup_{p\in\mathcal A}E\Big[-\exp\Big(-\alpha\big(X^{(p)}_T-F\big)\Big)\Big],$$

with $\alpha>0$ and a bounded $\mathcal F_T$-measurable liability $F$. For a closed set $C$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$ and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the set of nearest points.

Formalization targets

Goal: Theorem 7

Let $f(t,z)=-\frac\alpha2\operatorname{dist}^2\big(z+\frac1\alpha\theta_t,C_t\big)+z\theta_t+\frac1{2\alpha}|\theta_t|^2$. The BSDE

$$Y_t=F-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad t\in[0,T],$$

has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, the value function is

$$V(x)=-\exp\big(-\alpha(x-Y_0)\big),$$

and there is an optimal strategy $p^*\in\mathcal A$ with $p^*_t\in\Pi_{C_t}\big(Z_t+\frac1\alpha\theta_t\big)$.

Milestones

In the order of the proof: the bound (4) on $C_t$ and its closedness; the measurable selection Lemma 11 (a), (b); the identity on p. 8 that dictates $f$; the growth bound (9) and the local Lipschitz estimate of $f$; existence and uniqueness for (7); the BMO property of Lemma 12; admissibility and optimality of any predictable selection $p^*$; and the comparison $E[-\exp(-\alpha(X^{(p)}_T-F))]\le-\exp(-\alpha(x-Y_0))$ for every $p\in\mathcal A$.

Significance

The theorem reduces a constrained, nonconvex control problem to a single quadratic BSDE: the value is read off the initial value $Y_0$, and the optimal strategy is a pointwise nearest-point selection from the constraint set. It requires neither convexity nor duality, and it exhibits non-uniqueness of the optimal strategy when $\Pi_{C_t}$ has several points. It is the starting point of the quadratic-BSDE approach to utility maximization, indifference pricing and related equilibrium problems.

The result is proved in the paper; nothing in it is open. As far as is known, none of it is formalized: Mathlib has no stochastic integral against Brownian motion, no BSDE theory and no BMO martingales. A complete development would be the first machine-checked solution of a continuous-time portfolio optimization problem by BSDE methods, and its intermediate results (measurable selection of nearest points, the BMO bound for quadratic BSDEs, the verification argument) are reusable.

Difficulty

The deterministic steps (the identity behind the choice of $f$, the growth and Lipschitz bounds) are short. The hard steps are elsewhere. Existence rests on Kobylanski's theorem for BSDEs with quadratic growth, whose proof is a monotone approximation argument with exponential transforms; the Lipschitz theory of Pardoux–Peng does not apply. Uniqueness and the optimality of $p^*$ need the BMO property of $\int Z\,dW$ and a Girsanov change of measure with a stochastic exponential of a BMO martingale. The selection Lemma 11 (b) cannot use a projection map because $\tilde C$ is not convex; a measurable choice from a possibly multivalued nearest-point set is required. Finally the verification argument is a localization: $R^{(p)}$ is only a local supermartingale, and passing to the limit uses the uniform integrability built into admissibility.

Formalization scope

Time is $\mathbb R_{\ge0}$ with $T>0$; row vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m) (so $|\cdot|$ is Euclidean) and products such as $z\theta$ are inner products. The Brownian motion is the published EthierKurtz.IsStandardBrownian; the filtration and the stochastic integral come from the published module CvitanicKaratzas92_Optimality_Market (IsAugmentedBrownianFiltration, lebP for $\lambda\otimes P$, and an Itô-integral operator I). Predictability is measurability for Mathlib's Filtration.predictable. The market price of risk $\theta$ and the wealth $X^{(p)}$ are computed from the data, not assumed.

Expectations of $-\exp(\cdot)$ are minus lower integrals in $[0,\infty]$, and $V(x)$ is an extended real: a Bochner expectation would assign the junk value $0$ to non-integrable strategies and make them optimal, which is the trivializing formalization to avoid. Existence and uniqueness of the BSDE solution are part of the goal, not hypotheses, and the optimal strategy is a predictable selection of the nearest-point set, not of a choice function.

Disclosed readings: $\tilde C\neq\emptyset$ is assumed (otherwise $\mathcal A=\emptyset$); constraints and (8) are read $\lambda\otimes P$-a.e.; ellipticity holds for $P$-a.e. $\omega$ and all $t\le T$; $Y_0$ is a.s. constant and the value identity holds a.s.; uniqueness is in $Y_t$ a.s. for each $t$ and $Z$ $\lambda\otimes P$-a.e.; "$p^*$ given by Lemma 11" is read as any predictable selection; Lemma 11 (b) assumes full rank of $\sigma_t(\omega)$. The equivalence of the $\pi$- and $p$-formulations (Remark 5), the dynamic principle (Proposition 9) and Remarks 2–10 are out of scope.

Needed infrastructure: Itô calculus for continuous semimartingales, stochastic exponentials, BMO martingales and Kazamaki's criterion, Girsanov's theorem, quadratic BSDEs, and measurable selection. Contributions to any of these are welcome; they serve the companion power-utility mission (Theorem 14) as well.

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 1691–1712, 2005. https://doi.org/10.1214/105051605000000188 (arXiv: https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 558–602, 2000. https://doi.org/10.1214/aop/1019160253
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 767–818, 1992. https://doi.org/10.1214/aoap/1177005576
• E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• N. El Karoui, R. Rouge, Pricing via utility maximization and entropy, Math. Finance 10(2), 259–276, 2000. https://doi.org/10.1111/1467-9965.00093
• F. Delbaen, P. Grandits, T. Rheinländer, D. Samperi, M. Schweizer, C. Stricker, Exponential hedging and entropic penalties, Math. Finance 12(2), 99–123, 2002. https://doi.org/10.1111/1467-9965.02001
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585

Motivation

Stochastic models of covariance matrices need processes that stay in the cone of positive semidefinite matrices. Wishart processes (Bru, 1991) and their extensions underlie multivariate stochastic-volatility and term-structure models in finance (see §1 of Cuchiero et al. for the literature). They are used because their Laplace transforms are explicit: they are exponential-affine in the initial state, and their exponents solve matrix Riccati equations. Cuchiero, Filipović, Mayerhofer and Teichmann (arXiv:0910.0137, Ann. Appl. Probab. 2011) classify all such affine processes on the cone. Theorem 2.4 of that paper says that affine processes on $S_d^+$ correspond one-to-one to admissible parameter sets. This mission formalizes the converse direction of that correspondence: every admissible parameter set is realized by exactly one affine process.

Timeline:

• Bru (1991, MR1132135) constructs Wishart processes for specific parameters.
• Duffie, Filipović and Schachermayer (Ann. Appl. Probab. 2003, MR1994043) characterize affine processes on the canonical state space $\mathbb R_+^m\times\mathbb R^n$, with existence through the martingale problem.
• Cuchiero et al. (2011) give the full characterization on $S_d^+$. The necessity of admissibility and the existence-and-uniqueness converse are proved in separate sections (§4 and §5).

Setting

Let $S_d$ be the real symmetric $d\times d$ matrices with $\langle x,y\rangle=\operatorname{Tr}(xy)$, let $S_d^+$ be the positive semidefinite cone, and let $S_d^{++}$ be its interior. Write $x\preceq y$ when $y-x\in S_d^+$. A time-homogeneous, possibly killed Markov process on $S_d^+$ with transition kernels $p_t(x,d\xi)$ is affine if it is stochastically continuous and

$$\int_{S_d^+}e^{-\langle u,\xi\rangle}p_t(x,d\xi)=e^{-\varphi(t,u)-\langle\psi(t,u),x\rangle},\qquad t\ge0,\ u,x\in S_d^+,$$

for functions $\varphi\ge0$ and $\psi\in S_d^+$.

An admissible parameter set $(\alpha,b,\beta^{ij},c,\gamma,m,\mu)$ (Definition 2.3) consists of the following:

• a diffusion matrix $\alpha\in S_d^+$;
• a drift $b\succeq(d-1)\alpha$;
• killing rates $c\ge0$ and $\gamma\in S_d^+$;
• a jump measure $m$ with $\int(\|\xi\|\wedge1)\,m(d\xi)<\infty$;
• a matrix of finite measures $\mu$, which gives the state-dependent jump kernel $M(x,d\xi)=\langle x,\mu(d\xi)\rangle/(\|\xi\|^2\wedge1)$;
• linear drift coefficients $\beta^{ij}$, with the inward-pointing conditions (2.9) and (2.11) on $\partial S_d^+$.

These data define the operator (2.12),

$$\mathcal Af(x)=\tfrac12\sum A_{ijkl}(x)\partial^2_{ij,kl}f+\sum(b_{ij}+B_{ij}(x))\partial_{ij}f-(c+\langle\gamma,x\rangle)f+\int(f(x+\xi)-f(x))m(d\xi)+\int(f(x+\xi)-f(x)-\langle\chi(\xi),\nabla f\rangle)M(x,d\xi),$$

with $A_{ijkl}(x)=x_{ik}\alpha_{jl}+x_{il}\alpha_{jk}+x_{jk}\alpha_{il}+x_{jl}\alpha_{ik}$. They also define the functions $F(u)$ and $R(u)$ of (2.16)–(2.17), which drive the generalized Riccati equations $\partial_t\varphi=F(\psi)$, $\varphi(0,u)=0$ and $\partial_t\psi=R(\psi)$, $\psi(0,u)=u$.

Formalization targets

Goal: Theorem 2.4, second part (= Proposition 5.9)

For every admissible parameter set there is a transition family $(p_t)$ and there are exponents $(\varphi,\psi)$ such that:

$$\text{(i) } p \text{ is affine with exponents } (\varphi,\psi);\quad\text{(ii) } \mathcal S_+\subset D(\mathcal A_p),\ \mathcal A_pf=\text{(2.12)};\quad\text{(iii) } (\varphi,\psi) \text{ solves (2.14)–(2.15)};$$ $$\text{(iv) every affine } p' \text{ whose generator equals (2.12) on } \mathcal S_+ \text{ satisfies } p'_t=p_t \text{ for } t\ge0.$$

Milestones, in attack order

1. Theorem 4.8: a comparison theorem for matrix ODEs whose vector field is quasi-monotone increasing (Volkmann).
2. Lemma 5.1: $R$ is analytic on $S_d^{++}$ and quasi-monotone increasing on $S_d^+$.
3. Lemma 5.2: the growth bound $\langle u,R(u)\rangle\le\frac K2(\|u\|^2+1)$.
4. Proposition 5.3: unique global $\mathbb R_+\times S_d^{++}$-valued Riccati solutions, analytic in $(t,u)$.
5. Lemma 5.5: the regularized operators $\mathcal A^{\varepsilon,\delta,n}$ converge to $\mathcal A$ uniformly on $\mathcal S_+$.
6. Lemma 5.7 (second part): the boundary condition $\langle b-\frac12\sum D\sigma^{kl}\sigma^{kl},u\rangle\ge0$ on $\partial S_d^+$.
7. Lemma 5.6: the regularized martingale problems have $S_d^+$-valued càdlàg solutions.
8. Lemma 5.8: the martingale problem for $\mathcal A$ has an $S_d^+\cup\{\Delta\}$-valued càdlàg solution.

Significance

Together with the necessity direction (companion mission I in this series), the goal makes admissibility an exact characterization. Every admissible parameter set, including those with jumps of infinite activity and state-dependent killing, defines a well-posed Markov model on $S_d^+$. Its Laplace transform is then given by the Riccati flow, which is what makes the model computationally tractable. The intermediate results are reusable on their own:

• the matrix comparison theorem applies to any ODE on symmetric matrices;
• the Riccati well-posedness on $S_d^{++}$ holds for vector fields that need not be Lipschitz at $\partial S_d^+$;
• the martingale-problem framework on a one-point compactification is used beyond this paper.

The theorem is proved in the paper; it is not formalized anywhere. No formal library contains affine processes, generalized Riccati equations on matrix cones, quasi-monotone comparison theorems or martingale problems with jumps. Formalizing them requires all of that infrastructure.

Difficulty

The obvious route is to solve the Riccati equation (2.15) on $S_d^+$ by Picard iteration and to show invariance of the cone from the inward-pointing condition. That route fails because $R$ need not be Lipschitz at $\partial S_d^+$: the integral term can have unbounded derivative there (Remark 5.4). Standard invariance theorems therefore do not apply. Instead, quasi-monotonicity keeps the solution away from the boundary.

The obvious construction of the process is also blocked. Stroock's existence and uniqueness theory for martingale problems needs $\mathbb R^n$ and a uniformly elliptic diffusion part, and neither holds on the cone, where the diffusion degenerates at the boundary. Existence must go through regularized operators with bounded smooth coefficients, then tightness in the Skorokhod space of $S_d^+\cup\{\Delta\}$ and a limit. Uniqueness in law comes from the Riccati solutions. The killing terms $c$ and $\gamma$ are added last.

Formalization scope

Conventions committed to in Lean:

• $M_d$ is the function type Fin d → Fin d → ℝ, with $\langle x,y\rangle=\sum_{ij}x_{ij}y_{ji}$ and its norm.
• $S_d^+$ is the subtype of positive semidefinite matrices, with the subspace topology and Borel structure.
• Partial derivatives $\partial/\partial x_{ij}$ are taken in the symmetrized directions $\tfrac12(E^{ij}+E^{ji})$.
• The matrix measure $\mu$ is encoded as $H\,d\nu$ with a finite measure $\nu$ and a positive semidefinite density $H$. This encoding is equivalent; take $\nu=\sum_i\mu_{ii}$.
• The test space $\mathcal S_+$ is represented by Schwartz functions on $M_d$, restricted to the cone. The generator is the uniform limit of $(P_tf-f)/t$.
• Transition families are indexed by $t\in\mathbb R$, and only $t\ge0$ enters. Uniqueness is equality for $t\ge0$, never ∃!.
• Analyticity on $S_d^{++}$ is analyticity of $y\mapsto G((y+y^\top)/2)$ on an open subset of $M_d$.
• Martingale problems carry an existentially quantified probability space, the natural filtration and càdlàg paths (the platform predicate EthierKurtz.HasCadlagPaths).
• The cut-offs $\phi_n$ and $\eta_\varepsilon$ of §5.2 are arbitrary functions with the properties the paper lists. The paper fixes some and uses only those properties.
• The case condition of (5.7) is tested on $\phi_n(x)x$, the argument of $\eta_\varepsilon$, rather than on $x$ as printed. The printed reading makes $s_{\varepsilon,n}$ discontinuous off $S_d^+$, which contradicts the paper's claim $s_{\varepsilon,n}\in C_b^\infty(S_d,S_d)$. The two readings agree on $S_d^+$.
• In Theorem 4.8, "locally Lipschitz" is read as Lipschitz in the state variable, locally uniformly in time. This is weaker than joint local Lipschitz continuity in $(t,x)$.
• Every statement that contains one of the integrals of (2.12), (2.16), (2.17) or (5.10) also asserts that its integrand is integrable.
• Hypotheses not present on the page: none. Lemmas 5.1 and 5.2 assume less than the section's standing assumptions (not the drift condition (2.4)).

Trivializing formalizations are excluded:

• Lean's value $0$ for a non-integrable integral is ruled out by the integrability conclusions.
• A pointwise generator would be weaker than the paper's notion, so the generator is the uniform limit.
• An ∃! over transition families would be false at negative times, so uniqueness is stated for $t\ge0$.
• A martingale problem is not posed for a fixed probability space, and $X_0=x$ is required almost surely.

Needed infrastructure, reusable beyond this mission: matrix calculus on $S_d$ (square roots, spectral derivatives), comparison theorems for quasi-monotone ODEs, analytic dependence of ODE solutions, tightness in Skorokhod space, and martingale problems on locally compact spaces. Contributions are welcome at any of these levels, as are alternative proofs of the milestones.

Selected references

• C. Cuchiero, D. Filipović, E. Mayerhofer, J. Teichmann, Affine processes on positive semidefinite matrices, Ann. Appl. Probab. 21 (2011) 397–463; cited from arXiv:0910.0137v3. https://arxiv.org/abs/0910.0137v3
• D. Duffie, D. Filipović, W. Schachermayer, Affine processes and applications in finance, Ann. Appl. Probab. 13 (2003) 984–1053. https://mathscinet.ams.org/mathscinet-getitem?mr=1994043
• M.-F. Bru, Wishart processes, J. Theoret. Probab. 4 (1991) 725–751. https://mathscinet.ams.org/mathscinet-getitem?mr=1132135
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, New York, 1986. https://mathscinet.ams.org/mathscinet-getitem?mr=0838085
• P. Volkmann, Über die Invarianz konvexer Mengen und Differentialungleichungen in einem normierten Raume, Math. Ann. 203 (1973) 201–210. https://mathscinet.ams.org/mathscinet-getitem?mr=0322305

Motivation

Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.

The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.

Timeline.

• 1984. Reiman proved the process-level heavy-traffic limit for open queueing networks started empty (doi:10.1287/moor.9.3.441).
• 1987. Harrison and Williams characterised when an orthant RBM has a stationary distribution and showed it is unique (doi:10.1080/17442508708833469).
• 1995. Dai related fluid-model stability to positive Harris recurrence of multiclass networks (doi:10.1214/aoap/1177004828).
• 2006. Gamarnik and Zeevi proved the interchange of limits for GJNs whose primitives have exponential moments (arXiv:math/0410066). This mission formalizes that result.

Setting

There are $J$ stations. Station $j$ receives external arrivals with i.i.d. interarrival times of law $F_{A,j}$ (rate $\alpha_j$, or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law $F_{S,j}$ (mean $m_j$, rate $\mu_j = 1/m_j$). A job finishing at $j$ moves to $k$ with probability $p_{jk}$ or leaves. The routing matrix $P$ is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation $\lambda = \alpha + P'\lambda$ gives the effective rates $\lambda = [I-P']^{-1}\alpha$ and the traffic intensities $\rho_j = \lambda_j m_j$.

The queue lengths $Q(t)$ are not Markov. The state $\bar Q(t) = (Q(t),\hat a(t),\hat v(t))$, which adds the elapsed interarrival and service times, is a Markov process on $\mathcal X = \mathbb Z_+^J\times\mathbb R_+^{2J}$. A law $\pi$ on $\mathcal X$ is stationary if $\bar Q(0)\sim\pi$ implies $\bar Q(t)\sim\pi$ for all $t\ge0$.

Heavy traffic. Fix a critically loaded network $\Xi$ ($\rho_j=1$ for all $j$) and a vector $\kappa^0>0$. The network $\Xi^n$ slows the arrivals of $\Xi$ at station $j$ by the factor $1-\kappa^0_j/\sqrt n$, so that $\rho^n_j = 1-\kappa_j/\sqrt n<1$ for an explicit $\kappa>0$ (display (17)). Let $\pi^n$ be any stationary distribution of $\Xi^n$, and let $\hat\pi^n$ be the law of $Q^n(0)/\sqrt n$ under $\pi^n$.

The RBM. For a Brownian motion $W$ with drift $\beta$ and covariance $\Gamma$, the RBM $Z$ with parameters $(\beta,\Gamma,I-P')$ solves the Skorohod problem $Z = W + [I-P']Y\ge0$, with $Y$ nondecreasing and increasing only when $Z$ is on the boundary. Here $\beta = -(I-P')M^{-1}\kappa$ and $\Gamma$ is the explicit covariance matrix of Reiman's theorem, built from $\mu$, $\alpha$, $P$ and the squared coefficients of variation $c^2_{a,j}$, $c^2_{s,j}$ of $\Xi$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\hat\pi^n\ \Rightarrow\ \pi_{\mathrm{RBM}}\qquad(n\to\infty),$$

where $\pi_{\mathrm{RBM}}$ is the unique stationary distribution of the $(\beta,\Gamma,I-P')$-RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and $\hat\pi^n$ converges weakly to it, for every choice of stationary distributions $\pi^n$.

Milestones

1. Theorems 5 and 6 (pp. 15–16). For a general Markov process, a geometric Lyapunov function $\Phi$ gives $\mathbb E_\pi\Phi\le\phi(t_0)K/(1-\gamma)$. A Lyapunov function with control of $L_2$ gives an exponential tail $\mathbb P_\pi(\Phi>s)\lesssim e^{-\theta s}$.
2. Proposition 1 (p. 11). The fluid model drains in time at most $w'z/\min_j\mu_j(1-\rho_j)$, where $w=e'[I-P']^{-1}$.
3. Lemma A.1 and Propositions 2–3 (pp. 17, 25). The net input deviates from its fluid path by $O(\sqrt n)$ uniformly over initial states. As a result, $\Phi(z,a,v)=w'z$ is a Lyapunov function for $\Xi^n$ with drift $-\sqrt n$ over time $nt_0$.
4. Theorem 7 and Corollary 1 (pp. 17–18). $\mathbb P_{\pi^n}(n^{-1/2}w'Q^n(0)>s)\le C_1e^{-c_1s}$ uniformly in $n$. Hence $\{\hat\pi^n\}$ is tight.
5. Theorems 4, 3 and 2 (cited). Reiman's process limit from a general initial law; Harrison and Williams's existence and uniqueness theorem for the RBM's stationary distribution; existence of $\pi^n$.

Significance

The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order $(1-\rho^{*n})^{-1}$ uniformly in $n$. Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.

Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.

Difficulty

Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of $\hat\pi^n$ to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.

The tightness step is the technical core. Moment bounds must be uniform in $n$ and in the initial residual times. A Lyapunov argument on the workload $w'Q$ over a time horizon of order $n$ requires deviation bounds of order $\sqrt n$ for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of $w'Q$ per unit time is only of order $n^{-1/2}$.

Formalization scope

• Stations are Fin J, vectors Fin J → ℝ, $P'$ is Pᵀ, and the norm $\|\cdot\|$ is the $\ell^1$ norm, written as an explicit sum. The spectral-radius condition is $P^m\to0$.
• A network is its data $(\mathcal J, F_A, F_S, P)$ plus the predicate IsGJN (positive times, conditions (1)–(2), substochastic $P$). $A_j$ and $S_j$ count renewal epochs in $[0,t]$. The initial times $a_j(0)$, $v_j(0)$ are residual lives given the elapsed ages $\hat a_j(0)$, $\hat v_j(0)$. States carry their elapsed times as reals; the predicate InStateSpace cuts out $\mathcal X=\mathbb Z_+^J\times\mathbb R_+^{2J}$, and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over $\mathcal X$ only.
• A realization from an initial law is a probability space carrying the primitives with their joint law and processes $Q, B$ satisfying the dynamics (4)–(5) almost surely. $\mathbb E[\cdot\mid\bar Q(0)=x]$ is the expectation under a realization from $\delta_x$. Stationarity of $\pi$ means: a realization from $\pi$ exists, and every realization from $\pi$ has $\bar Q(t)\sim\pi$ for all $t\ge0$.
• The heavy-traffic scaling is read as $a^n_j = a_j/(1-\kappa^0_j/\sqrt n)$. The printed $a_j(1-\kappa^0_j/\sqrt n)$ would overload every $\Xi^n$, so no $\pi^n$ would exist. $\kappa$ is defined so that (17) holds exactly, and every statement about $\Xi^n$ is for all large $n$.
• The RBM is built on the published Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by $\mathbb R^J_+$. Weak convergence of laws on $\mathbb R^J$ uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on $[0,T]$.
• Quantities $\limsup_n(\cdot)<\infty$ are rendered as one finite bound valid for all large $n$. Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$. Constants "depending only on $\Xi$" are quantified before $n$ and before the stationary distributions.
• Disclosed departures from the page:
  • $\phi(t_0)<\infty$ is assumed in Theorem 5.
  • $\{\Phi>K\}\neq\emptyset$ is assumed in Theorem 6. Its tail constant (29) is stated as $(\gamma\theta/2)^{-1}$, which is what the paper's proof yields, instead of the printed $(1-\gamma\theta/2)^{-1}$.
  • $\Gamma$ is positive definite in Theorem 3, the hypothesis of Harrison and Williams.
  • The derivative bound $w'\dot q(t)\le-\min_j\mu_j(1-\rho_j)$ of Proposition 1 is stated for $\rho_j\le1$ at every station; the page states it unconditionally, and it fails when two stations are overloaded.
  • Theorems 5 and 6 are stated for the time-$t_0$ transition kernel of the Markov process.
• A trivializing formalization is ruled out explicitly. The goal keeps the existence and uniqueness of $\pi_{\mathrm{RBM}}$ as conjuncts, stationarity requires a realization to exist, and the RBM's stationary law must live on the orthant. Hence neither an impossible network nor an empty RBM notion makes the goal vacuous.
• Contributions are welcome on any milestone. The cited Theorems 2–4 are substantial on their own, and Theorems 5–6 are independent of queueing.

Selected references

• D. Gamarnik and A. Zeevi, Validity of heavy traffic steady-state approximations in generalized Jackson networks, Ann. Appl. Probab. 16(1), 2006, 56–90. arXiv:math/0410066, doi:10.1214/105051605000000638
• M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9(3), 1984, 441–458. doi:10.1287/moor.9.3.441
• J. M. Harrison and R. J. Williams, Brownian models of open queueing networks with homogeneous customer populations, Stochastics 22, 1987, 77–115. doi:10.1080/17442508708833469
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5(1), 1995, 49–77. doi:10.1214/aoap/1177004828
• H. Chen and D. D. Yao, Fundamentals of Queueing Networks: Performance, Asymptotics, and Optimization, Springer, 2001 (reference [11] of the paper; Chapter 7).