Stochastic Systems

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

The bullwhip effect is the observation that the variability of orders increases as one moves up a supply chain, from the retailer towards the manufacturer and its suppliers. It was documented in industry and in classroom experiments such as the Beer Game (Sterman 1989), and analysed by Lee, Padmanabhan and Whang (1997), who named demand forecasting, lead times, batch ordering, rationing and price variations as its main causes. A remedy often proposed is to centralize demand information: give every stage of the chain the customer demand data, so that no stage forecasts from the distorted orders of its downstream neighbour.

Chen, Drezner, Ryan and Simchi-Levi (2000) quantified the effect for a retailer that forecasts with a moving average and orders with an order-up-to policy. They gave an explicit lower bound on the ratio of the order variance to the demand variance in terms of the lead time, the forecasting window and the demand autocorrelation. They then showed that in a multistage chain with fully centralized demand information this ratio still grows with the total lead time upstream of each stage. This mission formalizes that result, Theorem 3.1 of the paper, together with the single-stage analysis it rests on.

Setting

Time is indexed by the integers. The customer demands $D_t$ seen by the retailer follow the AR(1) model

$$D_t = \mu + \rho D_{t-1} + \epsilon_t, \tag{1}$$

where $\mu \ge 0$, $|\rho| < 1$, and the errors $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2$. The demand is in steady state, so that $E(D_t) = \mu/(1-\rho)$ and $\mathrm{Var}(D) = \mathrm{Var}(D_t) = \sigma^2/(1-\rho^2)$ for every $t$.

The retailer does not know the demand process. With a window of $p \ge 1$ past observations it forms the moving-average estimates

$$\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad e_t = D_t - \hat D^1_t, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}},$$

where $L$ is the lead-time parameter ($L = 1$ means an order placed at the end of period $t$ arrives at the start of period $t+1$) and $C_{L,\rho}$ is a constant the paper leaves unspecified. The order-up-to point is $y_t = \hat D^L_t + z\,\hat\sigma^L_{et}$ for a safety factor $z$, and the order placed in period $t$ is $q_t = y_t - y_{t-1} + D_{t-1}$. It may be negative: excess inventory is returned without cost.

In the multistage chain with centralized information, stages $k = 1, 2, \dots$ (stage $1$ is the retailer) all observe $D_t$ and use the same estimate $\hat D_t = \sum_{i=1}^p D_{t-i}/p$. Stage $k$ has lead time $L_k$ and safety factor $z_k$ and uses the order-up-to point $y^k_t = L_k\hat D_t + z_k\hat\sigma^{L_k}_{et}$. Following the paper's sequence of events, stage $1$ orders $q^1_t = y^1_t - y^1_{t-1} + D_{t-1}$, and stage $k \ge 2$, receiving $q^{k-1}_t$, orders $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$.

Formalization targets

Goal: Theorem 3.1 (p. 441)

For every stage $k \ge 1$ and every period $t$,

$$\frac{\mathrm{Var}(q^k_t)}{\mathrm{Var}(D)} \ge 1 + \left(\frac{2\sum_{i=1}^k L_i}{p} + \frac{2\left(\sum_{i=1}^k L_i\right)^2}{p^2}\right)(1-\rho^p),$$

with equality when $z_1 = \dots = z_k = 0$. The bound holds for every choice of the constants $C_{L_k,\rho}$ and of the safety factors.

Milestones (p. 438)

1. The AR(1) moments $\mathrm{Var}(D_t) = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}(D_{t-1}, D_{t-p-1}) = \rho^p\sigma^2/(1-\rho^2)$.
2. Eq. (4): $q_t = (1 + L/p)D_{t-1} - (L/p)D_{t-p-1} + z(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$ for every outcome.
3. Lemma 2.1: $\mathrm{Cov}(D_{t-i}, \hat\sigma^L_{et}) = 0$ for $i = 1, \dots, p$.
4. The variance identity after Eq. (4):

$$\mathrm{Var}(q_t) = \left[1 + \left(\tfrac{2L}{p} + \tfrac{2L^2}{p^2}\right)(1-\rho^p)\right]\mathrm{Var}(D) + 2z\left(1+\tfrac{2L}{p}\right)\mathrm{Cov}(D_{t-1}, \hat\sigma^L_{et}) + z^2\,\mathrm{Var}(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1}).$$

5. Theorem 2.2, the single-stage case:

$$\frac{\mathrm{Var}(q)}{\mathrm{Var}(D)} \ge 1 + \left(\frac{2L}{p} + \frac{2L^2}{p^2}\right)(1-\rho^p), \tag{5}$$

with equality when $z = 0$.

Significance

Theorem 2.2 shows that forecasting with a positive lead time is enough to make orders more variable than demand, even for independent demands ($\rho = 0$). It also says how the effect depends on each parameter: the bound decreases in the window $p$ and increases in the lead time $L$. Theorem 3.1 is the paper's answer to the centralization remedy. When every stage sees the true customer demand and uses the same forecast and the same policy, the variability of orders at stage $k$ is still bounded below by the single-stage expression with the cumulative lead time $\sum_{i\le k}L_i$. Centralization reduces the bullwhip effect but does not remove it. The decentralized comparison (Theorem 3.2, where the bound becomes multiplicative across stages) is a separate mission in this series.

On the formalization side, the Gaussian special case of the single-stage results is on the platform. Snyder and Shen's Fundamentals of Supply Chain Theory states Theorem 2.2, Lemma 2.1, Eq. (4) and the AR(1) moments for normally distributed errors, as the items SupplyChainTheory.bullwhip_signal_processing, bullwhip_lemma_13_1, bullwhip_order_identity and ar1_moments. This mission states them under the paper's weaker hypothesis of a symmetric error distribution. The multistage Theorem 3.1 has no machine-checked counterpart. The paper proves only Theorem 2.2 in print. For the proofs of Lemma 2.1 and Theorem 3.1 it refers to Ryan (1997) and to a working paper, so a formalization supplies arguments the published article does not contain.

Difficulty

Most of the algebra is routine. The difficulty is Lemma 2.1 and the covariances like it. The estimate $\hat\sigma^L_{et}$ is a square root of a quadratic form in past demands, so its covariance with a demand cannot be computed from second moments. Under Gaussian errors one can appeal to properties of Gaussian vectors. With only a symmetric error law, every distributional fact has to come from the symmetry of the errors and from the representation of the steady-state demand as an infinite series in past errors.

The printed derivation also moves faster than a proof. Expanding $\mathrm{Var}(q_t)$ from Eq. (4) produces the cross terms $\mathrm{Cov}(D_{t-1}, \hat\sigma^L_{e,t-1})$ and $\mathrm{Cov}(D_{t-p-1}, \hat\sigma^L_{et})$, which lie outside the lags $1, \dots, p$ of Lemma 2.1. The display after Eq. (4) does not account for them. A complete proof of milestone 4 must show that these terms vanish too. For the chain, the stage orders are defined by a recursion across stages, and the variance of $q^k_t$ involves the estimates $\hat\sigma^{L_i}_{et}$ of all stages $i \le k$.

Formalization scope

Random variables are real functions on a probability space $(\Omega, P)$, and time is $\mathbb Z$, so that $D_{t-p-1}$ exists for every $t$. Variance and covariance are Mathlib's ProbabilityTheory.variance and ProbabilityTheory.covariance. The demand structure ChenBullwhip.Centralized.AR1Demand records (1) for every outcome and the paper's error hypotheses: independence, identical distribution, symmetry, mean $0$ and variance $\sigma^2$. It adds four disclosed conditions:

1. $\sigma > 0$, since the results divide by $\mathrm{Var}(D)$;
2. square integrability of errors and demands, since Mathlib's variance of a non-square-integrable function is $0$;
3. a steady-state condition: every $D_t$ is square integrable with the law of $D_0$, which is the stationary solution the paper's moment formulas presuppose;
4. $p \ge 1$ in every result.

The published Gaussian structure SupplyChainTheory.AR1Demand satisfies these conditions, so this mission generalizes the Snyder–Shen items rather than referencing them. The constants $C_{L,\rho}$ are free real parameters, and in the chain $C_{L_k,\rho}$ is $C(L_k)$ for an arbitrary function $C$. Lead times are natural numbers, $L = 0$ included. Sums $\sum_{i=1}^p$ and $\sum_{i=1}^k$ run over $\{1,\dots,p\}$ and $\{1,\dots,k\}$, and stages are numbered from $1$. The order recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is read from the paper's sequence of events, because the paper prints no formula for $q^k_t$.

The orders are computed from the demands through the definitions above. They are never arbitrary random variables with assumed moments. "Tight" is formalized as equality, and orders are never truncated at zero. Without the steady-state condition, a process started from an arbitrary $D_0$ satisfies (1) but has time-dependent moments, and the results fail; with $\sigma = 0$ the ratio form would be false. Both cases are excluded by the structure, not by vacuous hypotheses. The structure is satisfiable: i.i.d. standard Gaussian demands on $\mathbb Z \to \mathbb R$ form an instance.

A complete development needs: the $L^2$ series representation of a stationary AR(1) process; distributional symmetry facts for i.i.d. sequences with a symmetric law; and covariance bookkeeping for finite linear combinations. The first two are reusable for any linear time-series model with symmetric innovations. Contributions to any milestone, and to general lemmas about stationary AR(1) processes, are welcome.

Selected references

• F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
• J. D. Sterman, Modeling Managerial Behavior: Misperceptions of Feedback in a Dynamic Decision Making Experiment, Management Science 35(3):321–339, 1989. https://doi.org/10.1287/mnsc.35.3.321
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
• J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Northwestern University, 1997 (cited by the paper for the proofs of Lemma 2.1 and Theorem 3.1).

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$, an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$. It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$. In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$, has the form

$$C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}$$

The paper's standing assumptions on $G$ are:

1. $-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
2. $\lim_{|y|\to\infty}G(y)=\infty$.

The sequence $y_Q$. Let $y_1$ be an integer minimizing $G$. Given $y_1,\dots,y_Q$, let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$, and set

$$y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}$$

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$, and

$$C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .$$

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$, $Q=1$, $C^*=S$, $r=y_1-1$, $R=y_1+1$. Each pass compares $G(r)$ and $G(R)$; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$. The output is the final $(r,Q)$.

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$, stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

$$C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .$$

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

• §2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$.
• Figure 1 (p. 809): $y_{Q+1}$ has the least $G$-value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$.
• Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$.
• Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$.
• Display before (6): $\min_r C(r,Q)=C^*(Q)$.
• (6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$, and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$.
• Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
• Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$.

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$, an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$. Because it uses only the form (1) and the unimodality of $-G$, it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$.

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$.

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$, and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$: "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$, not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$, and fails for constant $G$.

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$, $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

• Types. $G:\mathbb Z\to\mathbb R$, $\kappa\in\mathbb R$ with $\kappa>0$, reorder points in $\mathbb Z$, order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$, so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$.
• Assumptions. "$-G$ unimodal" is NegUnimodal G: $\exists m$, $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$. "$\lim_{|y|\to\infty}G=\infty$" is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$-weights it holds for every function.
• The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$, as the paper defines them, is the first milestone.
• The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$, $C^*\le G(R)$; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
• Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$, under the paper's simplification $y_1>0$; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$, which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
• Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
• Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$. Lemma 2's "$Q^*$" is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise "$r^*(Q)=L(Q)-1$" means $L(Q)-1$ is an optimal reorder point.
• Ruled out. Defining the algorithm's output as an argmin of $C$, or by searching for Lemma 2's $q$, would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
• H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
• I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$, where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

• 1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
• 1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$, the quality-and-efficiency-driven regime.
• 2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$, defined on $(0,\infty)$, is convex and strictly increasing; it does not depend on $\lambda$. For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$, is strictly increasing on $[0,\infty)$, and makes

$$G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt$$

finite for every $N > \lambda/\mu$. With the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},$$

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$, and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

$$H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},$$

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

$$S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}$$

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$, with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$, $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$. Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

• Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$.
• Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$.
• Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$, then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
• Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$-separation of ratios.
• Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$.

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$, with $y^*(r)$ the minimizer of $y + rP(y)/y$, a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$, which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$. A further obstacle is bounding $x^*_\lambda$: the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$, and so are these. Committed conventions:

1. The standing assumptions are a structure WaitModel ($\mu>0$; $D_\lambda(0)=0$; $D_\lambda$ strictly increasing on $[0,\infty)$; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$, which is the paper's finiteness of $G$). $F$ is convex and strictly increasing on $(0,\infty)$.
2. Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$.
3. Argmins ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are hypotheses that a given function is a minimizer, for every $\lambda>0$; ties are allowed and the theorems hold for every choice.
4. In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, where $C$ is undefined.
5. $\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$.
6. Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$. The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ($F(N)=cN$, $D_\lambda(t)=at$), for which (18) holds with $\gamma = c\kappa^2/a$, so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$, and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$, differentiation under the integral sign for $G$, and convexity of $\pi_\lambda$. All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

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

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