The OR Formalization Drive

Motivation

Many economic and engineering systems are steered by agents who act at discrete instants rather than continuously: a central bank intervenes on an exchange rate, two energy producers adjust a shared stock, a firm rebalances inventory. Each action has a fixed cost, so continuous control is not realistic. The mathematical model is impulse control: the state follows a diffusion, and a controller may shift it at chosen stopping times by paying a cost. The single-controller theory is classical (Øksendal and Sulem, Applied Stochastic Control of Jump Diffusions, 2007). When two controllers with different objectives act on the same state, the result is a nonzero-sum stochastic differential game with impulse controls.

Before Aïd, Basei, Callegaro, Campi and Vargiolu, the literature on games with impulse controls was almost entirely zero-sum: Cosso (SIAM J. Control Optim., 2013) characterised the value of zero-sum impulse games through a double-obstacle quasi-variational inequality in the viscosity sense. Their paper (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) gives the first general formulation of the nonzero-sum case together with a verification theorem: a system of quasi-variational inequalities (QVIs) whose sufficiently regular solutions are the equilibrium payoffs. Its Section 4 then computes Nash equilibria in closed form for a one-dimensional game.

Setting

A $k$-dimensional Brownian motion $W$ on a filtered probability space satisfying the usual conditions drives the state equation

$$dY_s=b(Y_s)\,ds+\sigma(Y_s)\,dW_s ,\qquad Y_s\in\mathbb R^d,$$

with globally Lipschitz $b$ and $\sigma$. The game takes place in an open set $S\subseteq\mathbb R^d$ and ends at the exit time $\tau_S$ of the state from $S$. Each of two players $i\in\{1,2\}$ has a nonempty impulse set $Z_i\subseteq\mathbb R^{l_i}$ and a continuous impulse map $\Gamma^i:S\times Z_i\to S$: an intervention with impulse $\delta$ moves the state from $y$ to $\Gamma^i(y,\delta)$.

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$ with $\mathcal C_i\subseteq S$ open and $\xi_i:S\to Z_i$ continuous. Player $i$ intervenes as soon as the state leaves $\mathcal C_i$, with impulse $\xi_i(y)$ at the current state $y$. Player 1 has priority on ties, and several interventions may happen at the same instant. This defines the controlled process $X$, the intervention times $\tau_{i,n}$ and impulses $\delta_{i,n}$ of each player, and the states $X_{(\tau_{i,n})^-}$ just before each intervention. The payoff of player $i$ is

$$J^i(x;\varphi_1,\varphi_2)=\mathbb E\Big[\int_0^{\tau_S}e^{-\rho_is}f_i(X_s)ds+\sum_{\tau_{i,n}<\tau_S}e^{-\rho_i\tau_{i,n}}\phi_i(X_{(\tau_{i,n})^-},\delta_{i,n})+\sum_{\tau_{j,n}<\tau_S}e^{-\rho_i\tau_{j,n}}\psi_i(X_{(\tau_{j,n})^-},\delta_{j,n})+e^{-\rho_i\tau_S}h_i(X_{\tau_S})\mathbf 1_{\{\tau_S<\infty\}}\Big],$$

where $j\ne i$, $\rho_i>0$, $f_i$ is a running payoff, $\phi_i$ the cost of one's own interventions, $\psi_i$ the gain from the opponent's, and $h_i$ a terminal payoff on $\partial S$. A pair of strategies is $x$-admissible, $(\varphi_1,\varphi_2)\in\Phi_x$, when these four terms are integrable, $\sup_{s\le\tau_S}|X_s|$ has all moments, and the interventions do not accumulate before $\tau_S$. A Nash equilibrium is a pair in $\Phi_x$ from which no player gains by a unilateral admissible deviation.

Given candidate payoff functions $V_1,V_2$ on $\bar S$, let $\delta_i(x)$ be the unique maximiser of $V_i(\Gamma^i(x,\delta))+\phi_i(x,\delta)$ over $Z_i$. Define $\mathcal M_iV_i(x)=V_i(\Gamma^i(x,\delta_i(x)))+\phi_i(x,\delta_i(x))$, $\mathcal H_iV_i(x)=V_i(\Gamma^j(x,\delta_j(x)))+\psi_i(x,\delta_j(x))$, the continuation region $\mathcal D_i=\{\mathcal M_iV_i-V_i<0\}$ and the generator $\mathcal AV=b\cdot\nabla V+\tfrac12\operatorname{tr}(\sigma\sigma^tD^2V)$. The QVI system is

$$V_i=h_i\ \text{on }\partial S,\quad \mathcal M_jV_j-V_j\le0\ \text{on }S,\quad \mathcal H_iV_i-V_i=0\ \text{on }\{\mathcal M_jV_j=V_j\},\quad \max\{\mathcal AV_i-\rho_iV_i+f_i,\ \mathcal M_iV_i-V_i\}=0\ \text{on }\mathcal D_j .$$

Formalization targets

Goal: Theorem 3.3 (verification theorem)

Suppose $V_1,V_2$ solve the QVI system, $V_i\in C^2(\mathcal D_j\setminus\partial\mathcal D_i)\cap C^1(\mathcal D_j)\cap C(\bar S)$ with polynomial growth, $\partial\mathcal D_i$ is a Lipschitz surface near which $V_i$ has locally bounded first and second derivatives, $x\in S$, and the threshold pair $\varphi_i^*=(\mathcal D_i,\delta_i)$ is $x$-admissible. Then

$$(\varphi_1^*,\varphi_2^*)\ \text{is a Nash equilibrium and}\quad V_i(x)=J^i(x;\varphi_1^*,\varphi_2^*),\qquad i=1,2 .$$

Milestones

• Lemma 2.3: the controlled process is the concatenation of diffusion pieces, it jumps only at interventions, and between interventions it stays in $\mathcal C_1\cap\mathcal C_2$.
• Remark 3.6, (3.8b), (3.8d), (3.8f): against $\varphi_2^*$, the state stays in $\mathcal D_2$, and player 2 intervenes only on $\{\mathcal M_2V_2=V_2\}$ with impulse $\delta_2$.
• Step 1 of the proof: $V_1(x)\ge J^1(x;\varphi_1,\varphi_2^*)$ for every admissible deviation $\varphi_1$.
• Step 2 of the proof: $V_1(x)=J^1(x;\varphi_1^*,\varphi_2^*)$.

The goal follows from Steps 1 and 2 and their mirror images for player 2.

Significance

The theorem turns the search for Nash equilibria of nonzero-sum impulse games, an infinite-dimensional fixed-point problem over strategy pairs, into a deterministic problem: find functions satisfying a system of coupled QVIs with prescribed regularity. The regularity conditions become smooth-pasting conditions, hence a system of algebraic equations; Section 4 of the paper solves it explicitly for a one-dimensional game with linear payoffs. A further consequence is structural: equilibrium payoffs need only be $C^2$ on the opponent's continuation region, which is what lets non-smooth, piecewise-defined candidates qualify.

The result is proved in the paper; no machine-checked version exists. A complete formalization would be the first verified verification theorem for impulse control, single-player or game, and would expose every convention of the model: priority on ties, simultaneous interventions, the treatment of exit, and the integrability of the payoff. Several of these conventions need correction on the page, as listed below.

Difficulty

The heuristic argument applies Itô's formula to $e^{-\rho_1t}V_1(X_t)$ and uses the QVIs term by term. This fails on two counts. First, $V_1$ is only $C^1$ across the free boundary $\partial\mathcal D_1$, so Itô's formula does not apply directly. The paper mollifies $V_1$ (following Øksendal's proof of his verification theorem for optimal stopping) and must control the second derivatives near a Lipschitz boundary. Second, the sums over interventions may be infinite and the horizon unbounded, so expectations and limits do not commute. The passage to the limit needs the integrability built into $\Phi_x$ and the polynomial growth of $V_i$. The stochastic-calculus infrastructure itself (Itô's formula for continuous semimartingales stopped at random times, strong solutions of Lipschitz SDEs restarted at stopping times) is largely missing from Mathlib.

Formalization scope

The Lean model is pathwise. A realization is a sequence of diffusion pieces, each solving the state equation from the random restart time with the restart value. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and the stochastic basis uses the published You2015.Shared.UsualConditions and IsFBrownian. Times take values in $[0,\infty]$ with $e^{-\rho\cdot\infty}=0$, and the state space is EuclideanSpace ℝ (Fin d). $\Phi_x$ asks for one admissible realization, while the Nash inequalities and the payoff identity hold on every admissible realization; strong uniqueness makes these readings equivalent.

The following deviate from the page and are disclosed in the items:

1. $\delta_i$ is assumed continuous, so that $\varphi_i^*$ is a strategy.
2. The fourth QVI is imposed on $\mathcal D_j\setminus\partial\mathcal D_i$, where $\mathcal AV_i$ exists.
3. The exit time is $\alpha^S_{\bar k+1}$, not the printed $\alpha^S_{\bar k}$.
4. The gain term of (2.7) is read with the opponent's interventions.
5. The supremum in (2.8) is taken over $[0,\tau_S]$.
6. Interventions accumulating at a finite $\tau_S$ are excluded from $\Phi_x$, since the page leaves $X_{\tau_S}$ undefined there.
7. Lemma 2.3 is stated in corrected form for simultaneous and boundary interventions.

The payoff is a Bochner expectation only inside $\Phi_x$, which requires the $L^1$ conditions of (2.7) and the integrability of each payoff. A non-integrable deviation therefore never receives the junk payoff $0$, and the Nash inequality cannot hold vacuously.

Contributions are welcome on the stochastic-calculus layer this needs (Itô's formula, strong existence and uniqueness for Lipschitz SDEs, optional stopping for stochastic integrals) and on the mollification lemma for functions that are $C^1$ with piecewise bounded second derivatives across a Lipschitz surface. These are reusable well beyond this mission.

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, Math. Oper. Res. 45(1), 2020 (accepted manuscript, arXiv:1605.00039v4). https://arxiv.org/abs/1605.00039
• A. Cosso, Stochastic differential games involving impulse controls and double-obstacle quasi-variational inequalities, SIAM J. Control Optim. 51(3), 2102–2131, 2013.
• B. Øksendal, Stochastic Differential Equations, 6th ed., Springer, 2003. https://doi.org/10.1007/978-3-642-14394-6
• B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69826-5

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$-armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$. Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$, with mean $\mu_i$. Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$, and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a success count $S_i$ and a failure count $F_i$, both starting at $0$. In each round $t=1,2,\dots$ it

1. samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$;
2. plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$;
3. performs a Bernoulli trial with success probability $\tilde r_t$, with outcome $r_t\in\{0,1\}$;
4. increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$. The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],$$

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$, the binomial cdf $F^B_{n,p}$, and the random variable $X(j,s,y)$: the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$.

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$, and every $T\ge 2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).$$

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$, is not the formal claim.

Milestones

• Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$.
• Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$.
• Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
• Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$.
• Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$, where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$.
• Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$.
• Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$.

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$-valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

• Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$. Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$.
• Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$, rewards $X(i,t)\sim D_i$, and uniforms $V(i,t)$. Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$, $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$. Ties in the arg max go to the smaller index (a null event).
• Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$. $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$-valued, so Lemma 1 at $y=1$ reads $\infty=\infty$, as in the paper.
• O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$) is stated with one universal constant $C>0$, quantified before the instance, the means and the horizon, for all $T\ge 2$. Eq. (1) is stated the same way, without its printed numerals.
• Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$, the reward laws or $T$, would not be Theorem 1.
• Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
• Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
• K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
• R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

Motivation

In an impulse control problem a controller does not steer a process continuously: at times of its choosing it shifts the state by a finite jump, paying a fixed cost plus a cost proportional to the jump. Such models describe central-bank interventions on an exchange rate, inventory replenishment and cash management. Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) study nonzero-sum games in which two players control the same diffusion by impulses. They prove a verification theorem for such games and apply it to a linear game whose Nash equilibria are explicit.

The paper's interpretation of the linear game is two central banks with different targets for an exchange rate. An explicit equilibrium gives explicit intervention thresholds, and Section 4.4 of the paper asks how these thresholds respond to the fixed cost of intervening. This mission formalizes that comparative-statics question: when intervening becomes more expensive, do the players intervene less?

Setting

The game of Section 4.1 has a discount rate $\rho > 0$, a volatility $\sigma > 0$, running payoffs $f_1(x) = x - s_1$ and $f_2(x) = s_2 - x$ with $s_1 < s_2$, and intervention costs: a player who shifts the state by $\delta$ pays $c + \lambda|\delta|$ and the opponent receives $\tilde c + \tilde\lambda|\delta|$. The standing assumptions of the section are

$$c \ge \tilde c \ge 0,\qquad \lambda \ge \tilde\lambda \ge 0,\qquad (c,\lambda) \ne (\tilde c,\tilde\lambda),\qquad 1 - \lambda\rho > 0 .$$

All parameters except the fixed cost $c$ are held fixed. Set $\theta = \sqrt{2\rho/\sigma^2}$ and $\eta = (1-\lambda\rho)/\rho$, both positive. For $c > 0$ the function

$$F_c(y) = 2y + \theta c - \eta\log\frac{\eta + y}{\eta - y},\qquad y \in (0,\eta),$$

has a unique zero $\xi(c) \in (0,\eta)$. With

$$\Gamma(c) = \frac{\theta(c-\tilde c)}{4\xi(c)} + \frac{\theta c(\lambda-\tilde\lambda)}{4\eta\,\xi(c)} + \frac{\lambda-\tilde\lambda}{2\eta}$$

and a parameter $\tilde s \in \mathbb R$, the paper's formulas (4.20) are

$$\bar x_i(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta+\xi}{\eta-\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],\qquad x_i^*(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta-\xi}{\eta+\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],$$

for $i \in \{1,2\}$, with $\xi = \xi(c)$ and $\Gamma = \Gamma(c)$. In the Nash equilibrium of the paper's Proposition 4.7, player 1 intervenes when the state falls below $\bar x_1$ and moves it to $x_1^*$; player 2 intervenes above $\bar x_2$ and moves it to $x_2^*$. The interval $]\bar x_1(c), \bar x_2(c)[$ is the continuation region, where nobody intervenes. The equilibrium payoffs $V_1^c$, $V_2^c$ are explicit as well (4.27).

Formalization targets

Goal: Proposition 4.13

$$c \mapsto \bar x_2(c)\ \text{is strictly increasing and}\ c \mapsto \bar x_1(c)\ \text{is strictly decreasing on}\ ]\tilde c, +\infty[ .$$

The continuation region therefore widens strictly as the fixed cost grows. The statement concerns the explicit functions (4.20); that they are equilibrium thresholds is mission 2 of this series.

Milestones

1. (4.17). For $c > 0$, $\xi(c)$ is the unique zero of $F_c$ in $(0,\eta)$.
2. (4.28). $\xi \in C^\infty(]0,\infty[)$ with $\xi' = \frac\theta2\frac{\eta^2-\xi^2}{\xi^2}$ and $\xi'' = -\theta\eta^2\frac{\xi'}{\xi^3} = -\frac{\theta^2\eta^2}{2}\frac{\eta^2-\xi^2}{\xi^5}$.
3. (4.29). $\xi$, $c/\xi$ and $c\,\xi'$ tend to $0$ as $c \to 0^+$; $c(\eta-\xi) \to 0$ and $\xi \to \eta$ as $c \to +\infty$.
4. Proposition 4.12. As $c \to +\infty$, $\bar x_2, x_1^* \to +\infty$, $\bar x_1, x_2^* \to -\infty$, and pointwise $V_1^c(x) \to (x-s_1)/\rho$, $V_2^c(x) \to (s_2-x)/\rho$.
5. Proposition 4.14 (with a corrected hypothesis, below). If $\tilde c = 0$, then $x_2^*$ is strictly decreasing and $x_1^*$ strictly increasing on $]0,\infty[$; if moreover $\lambda = \tilde\lambda$, then $x_2^*(c) < \tilde s < x_1^*(c)$ for all $c > 0$.

Significance

Proposition 4.13 is the rigorous form of the economic intuition that costlier intervention makes players more patient. Together with Proposition 4.12 it describes the whole range of costs: the region of inaction grows strictly and invades the real line as $c \to \infty$, where the payoffs converge to those of the uncontrolled Brownian motion. Proposition 4.14 adds that, when the fixed gain vanishes, the targets $x_i^*$ move away from the centre $\tilde s$. The paper's numerical section shows that without $\tilde c = 0$ the targets need not be monotone.

The results are proved in the paper, in a few lines each, by differentiating the implicit function $\xi(c)$. None of them is formalized. The mission produces a machine-checked treatment of a parametrised implicit function, $c \mapsto \xi(c)$ defined by a transcendental equation: smoothness, explicit derivatives, and the asymptotics at both ends. On top of it, it gives a fully verified comparative-statics result for an explicit game equilibrium.

Difficulty

The thresholds depend on $c$ only through $\xi(c)$, which has no closed form, and through $\Gamma(c)$, a sum of terms in $c/\xi(c)$ and $1/\xi(c)$. Monotonicity of $\xi$ alone does not settle the goal: $c/\xi(c)$ is a ratio of two increasing functions, and its direction is decided by how fast $\xi$ grows compared with $c$, uniformly on $]\tilde c,\infty[$, including near $c = 0$, where $F_0$ has no zero and $\xi$ degenerates. The limits as $c \to +\infty$ need more than $\xi(c) \to \eta$: $\Gamma(c)$ grows linearly in $c$, so the rate at which $\eta - \xi(c)$ decays decides whether the targets $x_i^*$ diverge and whether the payoff coefficients vanish.

Formalization scope

The parameters $\rho, \sigma, \lambda, \tilde\lambda, \tilde c, \tilde s, s_1, s_2$ are bundled in a structure, and the standing assumptions not involving $c$ in a predicate $\rho > 0$, $\sigma > 0$, $s_1 < s_2$, $\tilde c \ge 0$, $\lambda \ge \tilde\lambda \ge 0$, $1 - \lambda\rho > 0$. $\theta$ and $\eta$ are computed from $\rho, \sigma, \lambda$ as in (4.21), not taken as free parameters. All quantities are real numbers.

$\xi(c)$ is defined as $\sup\{y \in (0,\eta) : F_c(y) \ge 0\}$. Milestone 1 proves that this is the paper's unique zero for every $c > 0$. For $c \le 0$ the set is empty and the definition returns the placeholder $0$. Every statement therefore restricts $c$ to $c > 0$, to $c > \tilde c$, or to $c \to +\infty$, and no statement can be satisfied through a junk value. On $]\tilde c, \infty[$ one has $\Gamma > 0$, so the square roots in (4.20) are the paper's. "Increasing" and "decreasing" are read strictly, as the proofs give. $C^\infty$ is ContDiffOn ℝ ∞, and $\xi'$ is deriv ξ. Limits at $0^+$ use the right neighbourhood filter.

Two departures from the page are disclosed in the items:

• $c > 0$ in (4.17). The standing assumptions allow $c = 0$ when $\tilde c = 0$ and $\lambda > \tilde\lambda$, but then $F_0$ has no zero; the paper's argument uses $F(0^+) = \theta c > 0$.
• $\lambda = \tilde\lambda$ in the last sentence of Proposition 4.14. For $\lambda > \tilde\lambda$, Proposition 4.11 gives $x_2^*(0^+) > \tilde s$ and the inequality $x_2^* < \tilde s$ fails for small $c$. The monotonicity claims keep the hypothesis $\tilde c = 0$ alone.

A complete development needs the intermediate value theorem and strict monotonicity on an interval, a differentiable implicit (or inverse) function theorem in one variable, and asymptotic estimates of $\log\frac{\eta+y}{\eta-y}$ near $0$ and near $\eta$. These one-variable lemmas about implicitly defined functions are reusable beyond this mission. Proofs of the milestones in any order are welcome.

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

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$, cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$, nominal volatilities $\sigma\in(0,\infty)^d$, effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$, risk aversions $r,p>0$, a marginal cost of volatility $h>0$, marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$, a horizon $T>0$, an initial consumption $X_0$ and a reservation utility $R_0<0$. Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$.

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$. A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

$$X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .$$

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$.

Criteria. For a payment $\xi$ at time $T$, the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$. Contracts $\mathcal C$ are the $\mathcal F_T$-measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$, and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$, the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$:

$$V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .$$

Hamiltonians. $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\}$.

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$. With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$, $L_0=-\frac1r\log(-R_0)$,

$$m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},$$ $$V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .$$

Milestones

1. Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$, and

$$H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).$$

2. Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$, $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$, and $F_0$ is non-decreasing.
3. Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$, and lies in $[y,\frac p{r+p}y]$ when $y\le0$.

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$.

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$-measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$, an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

• Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $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 $\mathbb F$-martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$.
• Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$.
• Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$; all suprema are in the extended reals, so the empty supremum is $-\infty$, as on p. 9.
• Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
• Indices are Fin N, Fin d; $N=0$, $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$).
• Added hypotheses. $\varepsilon\le1$ ($B\neq\emptyset$), $R_0<0$ ($\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$. The paper's closed form is computed with the effort cap removed ("$\eta_A\to0$ as $A\nearrow\infty$", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
• Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$; with $H_m$ the infimum is $-\infty$. The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. "$j=1,\dots,N$" for $\hat b$ means $j=1,\dots,d$. In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$" is read as $\eta_A\equiv0$.

The goal is an equality of extended reals between $V^{SB}$, defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

• R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
• J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
• B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
• Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
• I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

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