Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$. The state space $S$, control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$. Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$, the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ($\{g<c\}$ is analytic for every real $c$), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$.

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$-stage cost and optimal cost are

$$J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).$$

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$, and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$, for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$-th pair. The DP operators are

$$T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.$$

Formalization targets

Goal: Proposition 8.2

$$J^*_K=T^K(J_0),\qquad K=1,\dots,N,$$

under (F⁺) or (F⁻), where $J_0\equiv0$. The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$), Lemma 8.4 (monotone and bounded convergence for $T_\mu$). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ($J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$.

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$, choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$-optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

• Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
• Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$. Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
• The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
• The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
• Stages are indexed $0,\dots,N-1$, and a history is $k$ state–control pairs plus the current state.
• $g$ is stored on $S\times C$, but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$, not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

• the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
• extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?

F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on $\{0,1,2,\dots\}$, stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.

Timeline:

• 1951–1953, Kendall. Introduces the imbedded chains of M/G/1 and GI/M/1 and obtains most of their classification by direct methods.
• 1953, Foster. Derives the classification from general criteria: Theorem 2 (ergodicity), Theorems 4–6 (transience and recurrence).
• 1950s onward. The criteria become the standard tools (Feller's text; later the drift conditions of Meyn and Tweedie).

Setting

A Markov chain on the states $\{0,1,2,\dots\}$ is given by a transition matrix $P=[p_{ij}]$: $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every row $i$. Write $f_{ij}^{(n)}$ for the probability that the chain started in $i$ first reaches $j$ (for $i=j$, first returns to $j$) at step $n\ge1$. The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor $1$. A state $j$ is recurrent if $f_{jj}=\sum_n f_{jj}^{(n)}=1$ and transient if $f_{jj}<1$; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time $\sum_n n f_{jj}^{(n)}$ is finite. The mean first-passage time from $i$ to $j$ is $\mu_{ij}=\sum_{n\ge1} n f_{ij}^{(n)}\in[0,\infty]$.

The M/G/1 matrix is built from a sequence $k_0,k_1,\dots$ of positive numbers summing to one ($k_n$ is the probability of $n$ arrivals during one service):

$$[p_{ij}] = \begin{bmatrix} k_0 & k_1 & k_2 & \cdots \\ k_0 & k_1 & k_2 & \cdots \\ 0 & k_0 & k_1 & \cdots \\ 0 & 0 & k_0 & \cdots \\ \vdots & \vdots & \vdots & \end{bmatrix},$$

that is, $p_{0j}=k_j$ and, for $i\ge1$, $p_{ij}=k_{j-i+1}$ when $j\ge i-1$ and $0$ otherwise. The traffic intensity is

$$\rho=\sum_{n=1}^{\infty}n\,k_n\in[0,\infty],$$

the mean number of arrivals per service.

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

$$\text{the chain is ergodic}\iff\rho<1,\qquad\text{the chain is recurrent}\iff\rho\le1 .$$

The goal leaves $k$ arbitrary apart from positivity and normalization; in particular $\rho=\infty$ is allowed and falls in the transient case.

Milestones (the paper's general theorems and the step of §3 they feed)

1. Theorem 2 (drift criterion): a nonnegative solution of $\sum_j p_{ij}y_j\le y_i-1$ ($i\ne0$) with $\sum_j p_{0j}y_j<\infty$ makes the system ergodic. Already posed on the platform and referenced here.
2. Theorem 3: in an ergodic system the mean first-passage times $d_j=\mu_{j0}$ are finite and satisfy $\sum_{j\ge1}p_{ij}d_j=d_i-1$ ($i\ne0$), $\sum_{j\ge1}p_{0j}d_j<\infty$.
3. §3 display: for the ergodic M/G/1 chain, $\mu_{i,i-1}=\mu_{10}$ and $\mu_{i0}=i\mu_{10}$ ($i\ne0$).
4. Theorem 5: a solution of $\sum_j p_{ij}y_j\le y_i$ ($i\ne0$) with $y_i\to\infty$ makes the system recurrent.
5. Theorem 7: for a probability distribution $\{p_n\}$ with $p_0>0$, $\sum_n z^np_n=z$ has a root in $(0,1)$ iff $\sum_{n\ge1}np_n>1$.
6. Theorem 4: the system is transient iff $\sum_j p_{ij}y_j=y_i$ ($i\ne0$) has a bounded nonconstant solution.

Significance

The result. The classification is the stability theorem for the M/G/1 queue: for $\rho<1$ the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for $\rho=1$ the queue empties infinitely often but has no steady state; for $\rho>1$ it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.

Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.

Difficulty

The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the $n$-step probabilities $p_{ij}^{(n)}$ and of hitting probabilities of state $0$, none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic $\Rightarrow\rho<1$, recurrent $\Rightarrow\rho\le1$) need exact identities for mean first-passage times, not just bounds, and these must be handled in $[0,\infty]$ because the means may be infinite. And the boundary case $\rho=1$ (null recurrence) separates the two equivalences: an argument that only compares the mean drift $\rho-1$ with $0$, such as a law of large numbers for the increments, cannot tell recurrence from transience there.

Formalization scope

• The chain is the published QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to $1$ as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.
• States are indexed from $0$, as in the paper; "$i\ne0$" is i ≠ 0.
• The M/G/1 matrix is a function mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for $k_i=2^{-(i+1)}$).
• $\sum_n k_n=1$ is added as the meaning of "stochastic matrix"; §3 writes only $k_i>0$.
• $\rho$ and all mean first-passage times are extended nonnegative reals ($[0,\infty]$), so divergent means are $\infty$, never $0$. Theorem 7's mean is also taken in $[0,\infty]$.
• Recurrent means $f_{jj}=1$ for every state $j$; transient means $f_{jj}<1$ for every state. For irreducible chains these are complementary, which is a theorem, not a definition.
• The general Theorems 3, 4 and 5 assume irreducibility and aperiodicity, the paper's standing assumption of §1. The goal does not assume them: they follow from $k_i>0$.
• Every series in a hypothesis carries its convergence (Summable or HasSum); Theorem 3's equation (6) is written as $d_i=1+\sum_{j\ge1}p_{ij}d_j$ in $[0,\infty]$ together with finiteness of the $d_j$, $j\ne0$.
• Theorem 7's distribution is renamed $q$ in Lean to avoid a clash with $p_{ij}$. Theorem 1 of the paper (§2) and Theorem 6 are not targets of this mission.

Ruled out: $\rho$ as a real tsum (which is $0$ for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix $P$ that need not exist.

Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem $p_{ij}^{(n)}\to\pi_j$ for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Some problems in the theory of queues, Journal of the Royal Statistical Society B 13(2), 151–185, 1951. https://doi.org/10.1111/j.2517-6161.1951.tb00093.x
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, The Annals of Mathematical Statistics 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, Wiley, 1950.
• S. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511626630

Motivation

Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.

Setting

The state is a real process. Without interventions it is $x+\sigma W_s$, where $W$ is a standard real Brownian motion and $\sigma>0$. Player 1 may shift it up by impulses $\delta\in Z_1=[0,\infty[$, player 2 down by impulses $\delta\in Z_2=]-\infty,0]$:

$$X_s=x+\sigma W_s+\sum_{k:\tau_{1,k}\le s}\delta_{1,k}+\sum_{k:\tau_{2,k}\le s}\delta_{2,k}.$$

Player 1 earns the running payoff $f_1(X_s)=X_s-s_1$, player 2 earns $f_2(X_s)=s_2-X_s$, with $s_1<s_2$. An impulse $\delta$ costs its author $c+\lambda|\delta|$ and pays the opponent $\tilde c+\tilde\lambda|\delta|$. Payoffs are discounted at rate $\rho>0$. The standing assumptions are $c\ge\tilde c\ge0$, $\lambda\ge\tilde\lambda\ge0$, $(c,\lambda)\ne(\tilde c,\tilde\lambda)$ and $1-\lambda\rho>0$.

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$: an open continuation region $\mathcal C_i\subseteq\mathbb R$ and a continuous impulse map $\xi_i:\mathbb R\to Z_i$. Player $i$ intervenes when the state leaves $\mathcal C_i$, applying the impulse $\xi_i(\text{state})$; player 1 has priority when both want to act. This rule defines the controlled process $X^{x;\varphi_1,\varphi_2}$ and the interventions $(\tau_{i,k},\delta_{i,k})$ inductively. Player $i$'s payoff is

$$J^i(x;\varphi_1,\varphi_2)=\mathbb E_x\Big[\int_0^\infty e^{-\rho s}f_i(X_s)\,ds-\sum_{k}e^{-\rho\tau_{i,k}}(c+\lambda|\delta_{i,k}|)+\sum_{k}e^{-\rho\tau_{j,k}}(\tilde c+\tilde\lambda|\delta_{j,k}|)\Big].$$

A pair is $x$-admissible, $(\varphi_1,\varphi_2)\in\Phi_x$, when these random variables are integrable, $\sup_t|X_t|$ has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.

The explicit objects are $\theta=\sqrt{2\rho/\sigma^2}$, $\eta=(1-\lambda\rho)/\rho$ and

$$F(y)=2y+\theta c-\eta\log\frac{\eta+y}{\eta-y},\qquad 0<y<\eta .$$

From the zero $\xi$ of $F$ and a free parameter $\tilde s\in\mathbb R$, the formulas (4.20)–(4.21) give thresholds $\bar x_1<\bar x_2$, targets $x_1^*,x_2^*\in]\bar x_1,\bar x_2[$, coefficients $A_{ij}$, the functions $\varphi_i(y)=A_{i1}e^{\theta y}+A_{i2}e^{-\theta y}\pm(y-s_i)/\rho$ and the piecewise candidates $\tilde V_1,\tilde V_2$ of (4.6). These are linear outside $]\bar x_1,\bar x_2[$ and equal $\varphi_i$ inside.

Formalization targets

Goal: Proposition 4.7

For every $\tilde s\in\mathbb R$ and every initial state $x\in\mathbb R$, the threshold strategies

$$\varphi_1^*=\big(]\bar x_1,+\infty[,\ y\mapsto\max(x_1^*-y,0)\big),\qquad \varphi_2^*=\big(]-\infty,\bar x_2[,\ y\mapsto\min(x_2^*-y,0)\big)$$

form an $x$-admissible Nash equilibrium, and

$$J^1(x;\varphi_1^*,\varphi_2^*)=\tilde V_1(x),\qquad J^2(x;\varphi_1^*,\varphi_2^*)=\tilde V_2(x).$$

Milestones

1. (4.17). $F$ has a unique zero $\xi\in(0,\eta)$.
2. Proposition 4.2. For every $\tilde s$, the explicit 8-uple (4.20) satisfies the order conditions (4.7) and the optimality and pasting conditions (4.8)–(4.9). Moreover, $\varphi_2''$ changes sign exactly once in $]x_2^*,\bar x_2[$.
3. Lemma 4.6. The impulses (4.23) maximise $\delta\mapsto\tilde V_i(x+\delta)-c-\lambda|\delta|$, and the intervention operators satisfy (4.24): $\{\mathcal M_1\tilde V_1-\tilde V_1<0\}=]\bar x_1,\infty[$ and $\{\mathcal M_2\tilde V_2-\tilde V_2<0\}=]-\infty,\bar x_2[$.
4. Condition (v). The equilibrium pair is $x$-admissible for every $x$. This includes the integrability (4.26) of the discounted intervention costs.

Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.

Significance

The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by $\tilde s$: equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.

Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to $\tilde V_1,\tilde V_2$. The admissibility estimate (4.26) is written out only for initial states $x\in\{x_1^*,x_2^*\}$; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.

Difficulty

The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of $\tilde V_i(y)\pm\lambda y$, which needs the sign pattern of $\varphi_2''$ from Proposition 4.2, not only local conditions at the thresholds.

The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is $C^2$ only piecewise and $C^1$ across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.

Formalization scope

The Lean development lives in the namespace ImpulseGames.LinearGame.

• The constants and standing assumptions are a structure Model with the proposition Model.Standing. The added hypothesis $c>0$ appears in every statement that uses $\xi$: with $c=0$, which the standing assumptions allow, $F$ has no zero in $(0,\eta)$ and the family (4.20) does not exist.
• The zero $\xi$ is a parameter, constrained by $\xi\in(0,\eta)$ and $F(\xi)=0$. Milestone 1 shows that exactly one such $\xi$ exists.
• The Brownian motion is Mathlib's IsBrownianReal W P on a probability space, with time in $\mathbb R_{\ge0}$. Definition 2.2 is formalized pathwise: exit times $\inf\{s>\tilde\tau_{k-1}:\tilde X^{k-1}_s\notin\mathcal C_i\}$ in $[0,\infty]$ with $\inf\emptyset=\infty$, the tie rule favouring player 1, and $e^{-\rho\cdot\infty}=0$ for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are $\zeta+\sigma(W_s-W_t)$.
• Payoffs are Bochner expectations. $\Phi_x$ requires every random variable of (2.7) to be integrable, so no deviation can obtain the default value $0$ of a non-integrable expectation. The moment condition (2.8) is stated with an extended-real supremum, and (2.9) is read almost surely.
• The Nash condition quantifies over all strategies of Definition 2.1. A formalization that restricts deviations to threshold strategies would be a different, weaker theorem and is excluded. Likewise, the equilibrium payoffs $\tilde V_i$ are the explicit formulas (4.6), never defined as "the equilibrium value".

Two slips of the page are corrected. First, the paper's impulse maps $\xi_i^*(y)=x_i^*-y$ are not $Z_i$-valued on all of $\mathbb R$; they are replaced by $\max(x_1^*-y,0)$ and $\min(x_2^*-y,0)$, which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when $\lambda=\tilde\lambda$, in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.

A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with $C^1$, piecewise-$C^2$ functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.

Selected references

• R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 (accepted manuscript: arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039)
• G. Bertola, W. J. Runggaldier, K. Yasuda, On classical and restricted impulse stochastic control for the exchange rate, Applied Mathematics and Optimization 74(2), 423–454, 2016.
• A. Cadenillas, F. Zapatero, Classical and impulse stochastic control of the exchange rate using interest rates and reserves, Mathematical Finance 10(2), 141–156, 2000.
• B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007.

Motivation

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of $T$ periods, decides whether to place an order, pays a fixed cost $K$ for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.

Timeline:

• Scarf (1960) proved that $(s,S)$ policies are optimal for independent demands with fixed costs; with correlated demand the optimal policy is a state-dependent $(s_t(f_t), S_t(f_t))$ rule that is hard to compute.
• Levi, Pál, Roundy and Shmoys (2007) gave the dual-balancing 2-approximation for the model without fixed costs (§4) and the triple-balancing 3-approximation for the stochastic lot-sizing problem (§6, Theorem 6.1), both for arbitrarily correlated demand.

Setting

There are periods $t=1,\dots,T$ on a probability space $(\Omega,\mathcal F,\mu)$ with a filtration $(\mathcal F_t)$: $\mathcal F_t$ is the information available at the beginning of period $t$. The data are a fixed ordering cost $K\ge0$, per-unit holding costs $h_t\ge0$, per-unit backlogging penalties $p_t\ge0$, an initial inventory level $x_1\in\mathbb R$, and nonnegative demands $D_t$. The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that $D_t$ is $\mathcal F_t$-measurable: the demand of a period is known when the period begins. For every period $s$ there is a conditional joint distribution $I_s$ of the demands given $\mathcal F_s$, under which every conditional mean $E[D_t\mid f_s]$ is finite.

A feasible policy is an order process $Q=(Q_t)$ with $Q_t\ge0$ and $Q_t$ determined by $\mathcal F_t$. Its inventory levels are $x_t=x_1+\sum_{j<t}(Q_j-D_j)$ before ordering and $y_t=x_t+Q_t$ after ordering, and its cost is

$$\mathcal C(Q)=\sum_{t=1}^T\Bigl(K\,\mathbb 1(Q_t>0)+h_t(y_t-D_t)^++p_t(D_t-y_t)^+\Bigr).$$

The triple-balancing policy TB uses two rules. Let $s^*$ be the last period before $s$ in which TB ordered ($s^*=0$ if none). Rule 1: TB orders in period $s$ if and only if, without an order in $s$, the accumulated backlogging cost over $(s^*,s]$ would exceed $K$. Rule 2: when it orders in $s<T$, it orders

$$q_s^B=\max\{q\ge0:\ E[H_s^B(q)\mid f_s]\le K\},\qquad H_s^B(q)=\sum_{j=s}^T h_j\bigl(q-(D_{[s,j]}-x_s)^+\bigr)^+,$$

the largest quantity whose expected marginal holding cost over $[s,T]$ is at most $K$. When it orders in period $T$, it orders exactly enough to clear the backorders and meet $D_T$. Let $N$ be the number of orders TB places.

Formalization targets

Goal: Theorem 6.1

For every instance, the triple-balancing policy TB and every feasible policy $P$ satisfy

$$E[\mathcal C(TB)]\le 3\,E[\mathcal C(P)].$$

The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.

Milestones

1. §6.1, Rule 2 observation. In a period where TB orders, $D_s\le y_s^{TB}$: no backorders remain at the end of the period.
2. Lemma 6.1. $K\cdot E[N]\le E[\mathcal C(P)]$ for every feasible $P$.
3. Lemma 6.2. $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\cdot E[N]$ for every feasible $P$.

Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when $h_T>0$.

Significance

The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).

The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event $N=0$. It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.

Difficulty

The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.

Formalization scope

• Periods are natural numbers $1,\dots,T$, demands and orders are real-valued, and data at indices outside $1,\dots,T$ are unused.
• Information is a MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and "$D_t$ known at the start of period $t$" means $D_t$ is $\mathcal F_t$-measurable.
• The conditional distributions $I_s$ are model data: Markov kernels to demand paths that are $\mathcal F_s$-measurable regular conditional distributions of the demand path. At every outcome they make $D_s$ deterministic, demands nonnegative and the conditional means $E[D_t\mid f_s]$ finite.
• Expected costs, $E[N]$ and the conditional expectation in Rule 2 are lower Lebesgue integrals in $[0,\infty]$. Lemma 6.2 is stated additively, $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\,E[N]$, which is the paper's inequality whenever the expectations are finite.
• The comparison policy is an arbitrary feasible policy, not an optimal one. The paper's proofs use only feasibility, and this form implies the paper's whenever an optimum exists, without any existence hypothesis.
• TB is the predicate "feasible and satisfies Rules 1 and 2 at every period and outcome". The rules determine the policy uniquely. Rule 1 uses a strict "exceeds $K$", and the period-$T$ order is $D_T-x_T$.

Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every $q$, because it uses kernel integrals in $[0,\infty]$. Infinite expected costs cannot be read as $0$. The policy class is not empty, because a separate theorem gives existence under $h_T>0$ (without some positive holding cost on $[s,T]$ the maximum in Rule 2 does not exist).

Contributions welcome: proofs of the existence theorems (measurable selection of $q_s^B$, versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.

Selected references

• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. https://doi.org/10.1287/moor.1060.0205
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

• Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
• Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
• Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

• Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ($k\in\mathcal J$), service times $v_k^i>0$, and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$. When the $i$th customer served at station $k$ finishes, it moves to station $\phi_k^i$, or leaves if $\phi_k^i=0$. The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$, the service-time variances $s_k=\operatorname{var} v_k^1$, the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$), and the interarrival variances $a_k=\operatorname{var} u_k^1$. The routing matrix $P=(p_{kj})$, $p_{kj}=P\{\phi_k^1=j\}$, has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$, and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$, with $e_0=0$. The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

$$Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .$$

A sequence of such networks, indexed by $n$, shares $K$, $\mathcal J$ and $P$. Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$. With $\nu(n)=\lambda(n)+\mu(n)P$, the heavy-traffic condition is

$$c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .$$

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$. The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$, $0\le t\le1$.

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$, where

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$. Then

$$Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.$$

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

• the existence and uniqueness claim for (1)–(3);
• the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
• the least-element map $f$ (Proposition 1);
• the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
• the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
• stochastic boundedness of $Z^n$ (Lemma 6);
• vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
• the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

• a formal statement of the network, of its Harrison representation, and of weak convergence in $D$;
• a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
• eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$, which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$. It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

• Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
• A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$.
• The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
• "Spectral radius $<1$" is stated as $P^m\to0$.
• $(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
• The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$, (22) and (26) over $k\in\mathcal J$, and $\mathcal J$ is the same for all $n$.
• Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$. It is defined by continuity, $\xi(0)=0$, independent increments, and the Gaussian characteristic function of increments.
• $Z$ is the reflection of $\xi$ in the sense of (14)–(17).
• Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J$_1$ convergence on $[0,1]$. This form accommodates a separate probability space for each $n$.

Added hypotheses, each implicit on the page:

1. The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
2. Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

• convergence of finite-dimensional distributions only;
• a single network without the index $n$;
• uniform convergence used in place of the Skorohod topology without the coupling;
• a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

• the deterministic reflection-map results;
• Donsker-type theorems for renewal counting processes in $D$;
• the random time-change lemma (Billingsley);
• the continuous mapping theorem in coupling form.

Selected references

• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
• J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
• J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
• D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
• P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$, $\lambda\in(0,\infty)^d$, nominal volatilities $\sigma\in(0,\infty)^d$, effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$, risk aversions $r,p>0$, a marginal volatility cost $h>0$, slopes $\kappa,\theta\in\mathbb R$, a horizon $T>0$, an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$.

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$, at cost

$$c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).$$

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$, in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$, and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$; write $\delta=\kappa-\theta$. For a payment $\xi$ made at time $T$, the consumer's and the producer's criteria are

$$J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].$$

A contract is an $\mathcal F_T$-measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

$$V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.$$

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$. Finally $\rho=\frac{rp}{r+p}$, $L_0=-\frac1r\log(-R_0)$, $U(x)=-e^{-px}$, $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$.

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$. Then

$$V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.$$

Milestones

1. Proposition 2.1. The best responses $\hat a(z)$, $\hat b(\gamma)$ attain the infima defining $H_m$, $H_v$, and these Hamiltonians have explicit closed forms.
2. (A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$.
3. Proposition A.3 (i), with the explicit solution of p. 28.

$$\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).$$

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$. It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$. Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$; a contract remains any $\mathcal F_T$-measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$, and every value is an extended-real supremum with $\sup\emptyset=-\infty$. $B$ is read as $[\varepsilon,1]^d$, with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$, without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$; the index range of $\hat b$ is $j=1,\dots,d$; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

• R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
• J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
• B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
• Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
• I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2