Operations Research

Motivation

The reflected random walk $X_{n+1}=[X_n+U_{n+1}]^+$ is the waiting-time sequence of the single-server queue (Lindley's recursion). Additive functionals $\sum_{i\le n}X_i^p$ measure accumulated congestion. For $p=1$ this is the total waiting time, the area under the workload curve.

Existing general results on sample-path large deviations for additive functionals of Markov chains (in the Donsker–Varadhan line) assume the function to be bounded. They therefore do not cover the cumulative waiting time of a single-server queue. For $f(x)=x^p$ the relevant rare events are not produced by a small, uniform tilt of the whole trajectory but by a few busy periods of exceptional size, and the speed is sublinear.

Bazhba, Blanchet, Rhee and Zwart (arXiv:2003.14381, Mathematics of Operations Research, 2025) prove that the scaled partial-sum process satisfies a large deviation principle at the sublinear speed $n^{1/(1+p)}$. They also identify the rate function through a variational problem over paths of bounded variation.

Related work on large deviations of the area under a busy period either treats queue-length functionals (Blanchet–Glynn–Meyn, 2013) or assumes a moment generating function that is finite everywhere (Duffy–Meyn, 2014). Neither obtains a sample-path result. The present paper assumes only that the moment generating function of the increment is finite near the origin. It relies on the sample-path large deviations for light-tailed random walk trajectories of Borovkov and Mogulskii (II, III) and of Vysotsky (ALEA, 2021), and on the authors' earlier work in the $M_1'$ topology (Bazhba et al., 2020).

Setting

Let $U_1,U_2,\dots$ be i.i.d. copies of a real random variable $U$ with $\mu=\mathbf E(U)<0$. Let $\theta_+$ and $\theta_-$ be the supremum and infimum of $\{\theta:\mathbf E(e^{\theta U})<\infty\}$. The paper assumes:

1. $-\infty\le\theta_-<0<\theta_+\le\infty$ (Assumption 2.1);
2. $\log\mathbf P(U\ge n)/n\to-\theta_+$ and $\log\mathbf P(-U\ge n)/n\to\theta_-$ (Assumption 2.2);
3. $\mathbf P(U>0)>0$ (Assumption 2.3).

The chain is $X_0=0$, $X_{n+1}=[X_n+U_{n+1}]^+$. Fix $p>0$ and let $\alpha=1/(1+p)$. The object of study is

$$\bar Y_n(t)=\frac1n\sum_{i=1}^{\lfloor nt\rfloor}X_i^p,\qquad t\in[0,1].$$

The busy periods are delimited by the return times $T_0=0$, $T_i=\inf\{k>T_{i-1}:X_k=0\}$. The busy-period areas are $W_j=\sum_{i=T_{j-1}+1}^{T_j}X_i^p$, and the long-run mean of $X^p$ is $\lambda=\mathbf E(W_1)/\mathbf E(T_1)$.

$\bar Y_n$ lives in the Skorokhod space $\mathbb D[0,1]$ of càdlàg paths. This space carries the $M_1'$ metric $d_{M_1'}$ (Definitions 2.1–2.2). It compares parametrizations of the extended completed graph, which joins each jump by a vertical segment and also joins $0$ to $\xi(0)$ at the origin ($\xi(0-)=0$).

The rate function involves the variational problem

$$\mathcal B^*_y=\inf_{\xi\in B_y}I_y(\xi).$$

Here $B_y$ is the set of paths $\xi$ of bounded variation on compacts with $\xi(0)=y$ whose reflected area $\int_0^{\mathcal T(\xi)}\Psi(\xi)(s)^p\,ds$ up to the first return time $\mathcal T(\xi)$ of $\Psi(\xi)$ to zero is at least $1$. $\Psi(\xi)(t)=\xi(t)-\inf_{s\le t}(\xi(s)\wedge0)$ is the reflection map. The cost is

$$I_y(\xi)=\int_0^{\mathcal T(\xi)}\Lambda^*(\dot\xi^{(a)}(s))\,ds+\theta_+\xi^{(u)}(\mathcal T(\xi))+\theta_-\xi^{(d)}(\mathcal T(\xi)),$$

where $\Lambda^*$ is the Legendre transform of $\log\mathbf Ee^{\theta U}$ and $\xi^{(a)},\xi^{(u)},\xi^{(d)}$ are the absolutely continuous, upward singular and downward singular parts of $\xi$.

Formalization targets

Goal: Theorem 2.1

$\bar Y_n$ satisfies the large deviation principle in $(\mathbb D[0,1],\mathcal T_{M_1'})$ with speed $n^\alpha$ and rate function

$$I_Y(\zeta)=\begin{cases}\mathcal B^*_0\sum_{t:\zeta(t)\neq\zeta(t-)}(\zeta(t)-\zeta(t-))^\alpha & \zeta\in\mathbb D^{(\lambda)}[0,1],\\ \infty&\text{otherwise,}\end{cases}$$

where $\mathbb D^{(\lambda)}[0,1]$ is the set of paths $\lambda t+\zeta(t)$ with $\zeta$ a non-decreasing pure jump path, $\zeta(0)\ge0$.

Busy-period tails

• Theorem 2.2: $\lim_{t\to\infty}t^{-\alpha}\log\mathbf P(W_1\ge t)=-\mathcal B^*_0$.
• Theorem 2.3: $\lim_{n\to\infty}n^{-\alpha}\log\mathbf P(V_n\ge nb)=-\mathcal B^*_0b^\alpha$ for the last, incomplete busy period.

Milestones

1. The variational problem. Lemma 4.1 ($\mathcal B^*_y=0$ beyond $\bar y=(|\mu|(p+1))^\alpha$, and the restriction to absolutely continuous paths). Proposition 4.1 (monotonicity, Lipschitz continuity, $\mathcal B^*_y\in(0,\infty)$ on $[0,\bar y)$). Lemma 4.4 (finite horizon). Lemma 4.5 (uniform $M_1'$ continuity of the area on level sets).
2. Busy-period estimates. Lemma 4.6, Proposition 4.2, and Proposition 4.3(ii) ($\mathcal B^*_0=\mathcal B^*_\pi$).
3. The decomposition. Lemma 3.1 (LDP for the last busy period), Lemmas 3.2–3.3 (finite-dimensional LDP), Lemma 3.7 (LDP for completed busy periods in $M_1'$), and Lemma 3.8 (exponential equivalence).

Significance

The result. The theorem gives the full large deviation behaviour of $\sum X_i^p$, not only its one-dimensional tail. It identifies the mechanism of rare events: one or a few busy periods of area of order $n$, each contributing $\mathcal B^*_0$ times its area to the power $\alpha$. In the rate function, a busy period in progress at the end of the horizon is indistinguishable from a completed one; the paper's Theorem 2.3 and Proposition 4.3 make this precise. By contraction the theorem yields tail asymptotics for any $M_1'$-continuous functional of the cumulative cost process.

The formalization. The result is proved on paper. No part of it has been machine-checked, and the platform has no Skorokhod $M_1'$ metric and no large deviation principle at a sublinear speed. A complete development would supply the first formal $M_1'$ metric on $\mathbb D[0,T]$ and a sample-path LDP for a heavy-tailed regime. It would also provide a formal treatment of variational problems over paths of bounded variation with singular parts.

Difficulty

The obvious route is the contraction principle applied to the sample-path LDP for the scaled random walk $\bar K_n$, followed by the map that sends the walk to the area under its reflection up to its first return to zero. That map is not continuous: the first passage time is discontinuous in every Skorokhod topology. The paper replaces the random horizon by a large fixed horizon $T$, but then must show that the variational problems over $[0,T]$ and over $[0,\mathcal T(\xi)]$ have the same value (Lemma 4.4). It must also prove uniform continuity of the area functional on level sets of the rate function (Lemma 4.5).

A second difficulty is the class of admissible paths. Because $\theta_\pm$ may be finite, optimal paths could a priori contain jumps or singular parts. Lemma 4.1 rules this out. Finally, the passage from the finite-dimensional LDP to the $M_1'$ topology requires the busy period in progress at time $n$ to be handled separately. The mere existence of the limit in Theorem 2.3 relies on a time-reversal argument and on the decay rate of the stationary distribution.

Formalization scope

• Increments. A sequence U : ℕ → Ω → ℝ, measurable, independent and identically distributed, with U i the paper's $U_{i+1}$. Moments are lower Lebesgue integrals in $[0,\infty]$, never Mathlib's mgf. $\theta_\pm\in[-\infty,\infty]$.
• Logarithms and limits. All logarithms are ENNReal.log with $\log0=-\infty$; liminf and limsup are taken in EReal. Probabilities of possibly non-measurable events are outer measures.
• Path space. $\mathbb D[0,T]$ consists of functions $\mathbb R\to\mathbb R$, càdlàg on $[0,T]$ and constant outside. $\xi(0-)=0$. Parametrizations are on $[0,T]$, and "nondecreasing" uses the reflexive closure of the printed strict order. $d_{M_1'}$ takes values in $[0,\infty]$.
• Rate function ingredients. Costs, $\mathcal B^*_y$, $\mathcal B^*_\pi$, $\mathcal V^{T*}_y$, $\beta$ and all rate functions take values in $[0,\infty]$, with $\theta_+\cdot0=0$ when $\theta_+=\infty$. The exit time $\mathcal T(\xi)$ lies in $[0,\infty]$; the return times $T_i$ lie in $\mathbb N\cup\{\infty\}$. The cost of a bounded-variation path is the infimum over its representations $\xi(0)+\int g+\sigma_u-\sigma_d$ with singular non-decreasing $\sigma_u,\sigma_d$; this infimum is attained at the Hahn–Jordan decomposition. The downward singular cost is nonnegative (the sign on p. 22 is a typo).
• The goal. It is stated with $T=1$, as in the paper's proof. The LDP is given by bounds for open and closed sets, which is equivalent to (2.2).
• Ruling out trivial readings. $B_y$ and $V^T_y$ range over all paths, with jumps and singular parts, and $\mathcal B^*_0$ and $\lambda$ are defined from the data, not assumed. Restricting either problem to absolutely continuous paths would make Lemma 4.1(ii) a tautology. Taking $\theta_\pm$ infinite, $p=1$, or the $J_1$ topology would change the theorem.
• Infrastructure. A complete development needs sample-path LDPs for random walks in $M_1'$ (the cited Results B.1–B.3), the Dawson–Gärtner projective limit theorem, Lebesgue decompositions of BV functions, and regenerative structure of the reflected random walk. The $M_1'$ metric, the LDP vocabulary at general speed and the bounded-variation cost are reusable beyond this mission.

Contributions to any milestone, and formalizations of the cited Results B.1–B.3, are welcome.

Selected references

• M. Bazhba, J. Blanchet, C.-H. Rhee, B. Zwart, Sample-path large deviations for unbounded additive functionals of the reflected random walk, Mathematics of Operations Research, 2025; arXiv:2003.14381v3. https://arxiv.org/abs/2003.14381
• M. Bazhba, J. Blanchet, C.-H. Rhee, B. Zwart, Sample path large deviations for Lévy processes and random walks with Weibull increments, Annals of Applied Probability 30(6), 2020. https://doi.org/10.1214/20-AAP1570
• J. Blanchet, P. Glynn, S. Meyn, Large deviations for the empirical mean of an M/M/1 queue, Queueing Systems 73(4), 2013. https://doi.org/10.1007/s11134-013-9349-7
• A. A. Borovkov, A. A. Mogulskii, Large deviation principles for random walk trajectories. II, Theory of Probability and its Applications 57(1), 2013. https://doi.org/10.1137/S0040585X97985765
• A. A. Borovkov, A. A. Mogulskii, Large deviation principles for random walk trajectories. III, Theory of Probability and its Applications 58(1), 2014. https://doi.org/10.1137/S0040585X97986370
• K. R. Duffy, S. P. Meyn, Large deviation asymptotics for busy periods, Stochastic Systems 4(1), 2014. https://doi.org/10.1214/13-SSY098
• V. Vysotsky, Contraction principle for trajectories of random walks and Cramér's theorem for kernel-weighted sums, ALEA. Latin American Journal of Probability and Mathematical Statistics 18(2):1103–1125, 2021.
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, Springer, 2010 (corrected reprint of the 2nd ed.). https://doi.org/10.1007/978-3-642-03311-7
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479

Why the price of borrowing a stock matters

To sell a stock short, an investor must first borrow it, and the owner who lends it charges a lending fee. Securities lending is a large market, and the fee varies across stocks: D'Avolio (2002) documents that shorting costs are positively related to the dispersion of investors' beliefs. Short-sale constraints have a long history in asset pricing (Miller 1977; Harrison and Kreps 1978; Jones and Lamont 2002), but most models either forbid short sales outright or take the fee as an exogenous parameter. Neither explains where the fee comes from, nor when a lending market is active at all.

Evgeniou, Hugonnier and Prieto build a dynamic general equilibrium model in which the fee is endogenous: two investors with logarithmic utility disagree about the expected return of a risky asset, and a lending agent, acting for the asset owners, sets the fee charged to short sellers to maximize the owners' fee revenue. Their §3 derives the equilibrium shorting cost in closed form at every state of the economy. This mission formalizes that derivation.

Setting

The economy has a riskless asset and two risky assets with strictly positive volatilities $\sigma_1,\sigma_2$. Asset 1 can be shorted at a cost; asset 2 cannot be shorted at all. There are two investors, an optimist $o$ and a pessimist $p$, with wealths $W^{(o)},W^{(p)}>0$. Each investor $a$ perceives market prices of risk (Sharpe ratios) $\theta^{(a)}_1,\theta^{(a)}_2$, and the optimist is more optimistic about asset 1: $\theta^{(p)}_1\le\theta^{(o)}_1$, the disagreement $\Delta\ge0$.

A short position in asset 1 pays a shorting cost $\Phi$ per dollar shorted, and a long position earns a lending yield $\Gamma$. Both are measured per unit of volatility of asset 1: $\phi=\Phi/\sigma_1$ and $\gamma=\Gamma/\sigma_1$. A position $m$ in asset 1 earns fees at the rate

$$\Lambda(m;\Phi,\Gamma)=m^+\Gamma-m^-\Phi ,$$

with $m^+=\max\{m,0\}$ and $m^-=\max\{-m,0\}$. Investor $a$ chooses wealth fractions $p=(p_1,p_2)$ with $p_2\ge0$ to solve the mean-variance problem

$$\max_{p\in\mathbb R\times\mathbb R_+}\Big\{\Lambda(p_1;\Phi,\Gamma)+p_1\sigma_1\theta^{(a)}_1+p_2\sigma_2\theta^{(a)}_2-\tfrac12(p_1\sigma_1+p_2\sigma_2)^2\Big\},$$

which is what logarithmic utility reduces to at each instant. The lending agent's revenue per unit of volatility at fee $y$ is

$$R(y)=\sum_a y\,\big(\theta^{(a)}_1+y\big)^-\,W^{(a)} .$$

An equilibrium at a state consists of these quantities such that: the no-dominance condition $\theta^{(a)}_2=\theta^{(a)}_1+\gamma$ holds for both investors (equation (7)); each investor's portfolio is optimal; asset 1, in positive supply $S_1>0$, clears; the lending market clears (fees paid by short sellers equal fees received by long holders); and $\phi$ is the least maximizer of $R$ over $y\ge\gamma$. The inactive set is $\mathcal L=\{\gamma=0\}$ and the active set $\mathcal S$ is its complement.

Formalization targets

Goal: equations (15)–(17)

At every equilibrium state,

$$\gamma=0\iff\theta^{(p)}_2\ge0,\qquad \phi=-\tfrac12\,\theta^{(p)}_1\,\mathbb 1_{\{\theta^{(p)}_2<0\}} .$$

Lending is active exactly where the pessimist perceives a strictly negative net Sharpe ratio on long positions, and there the lending agent charges half the Sharpe ratio $-\theta^{(p)}_1$ the pessimist could earn by shorting absent frictions.

Milestones, in attack order

1. Proposition 1 (p. 17): the optimal portfolios of the mean-variance problem under (7) and $\phi\ge\gamma$.
2. (11) (p. 18): the optimist is long, $\theta^{(o)}_2=\theta^{(o)}_1+\gamma>0$.
3. (14) (p. 18): $\gamma\sigma_1S_1=(\phi-\gamma)(\theta^{(p)}_1+\phi)^-W^{(p)}$.
4. (12)–(13) (p. 18): the maximizers of the revenue over $y\ge\gamma$, and their least element $\max\{\gamma,-\tfrac12\theta^{(p)}_1\}$.

Two companion statements are also included: (18) (p. 20), that the pessimist is strictly short on $\mathcal S$, and the fee flow $(\pi^{(p)}_1)^-\Phi=\tfrac14(\theta^{(p)}_1)^2W^{(p)}\mathbb 1_{\mathcal S}$ (p. 19).

Significance

The goal is the paper's description of the short market. It identifies the active set by a condition on one observable-in-principle quantity, the pessimist's net Sharpe ratio, and it gives the fee as a fixed fraction of the pessimist's frictionless Sharpe ratio. The rest of the paper rests on it: the one-asset closed forms of §4.1, the trading regions of §3.3, and the pricing results of Proposition 2 all start from (15)–(16). The fee-flow identity shows that the optimist captures a quarter of the pessimist's frictionless excess return, which is the upper bound Remark 1 attributes to any alternative fee-setting mechanism.

The result is proved in the paper, partly in the text and partly in Appendix A. Some steps are argued informally: (11) rests on the sentence "agents cannot be short simultaneously in equilibrium", and (14) on "substituting the optimal portfolios of Proposition 1 into the market clearing conditions". As far as is known, none of it has been machine-checked. A formalization makes each step explicit, including the degenerate states the text passes over. In checking the statements against each other, three printed slips were found and are corrected here (see Formalization scope).

Difficulty

The goal combines optimality, clearing and revenue maximization, and the obvious argument fails at its degenerate edge. On the inactive set the shorting cost equals the lending yield ($\phi=\gamma=0$). There Proposition 1's characterization of optimal portfolios no longer holds: portfolios that short asset 1 to buy asset 2 are also optimal. So the step "substitute the optimal portfolios" is not available, and (14) must be obtained from the clearing conditions directly in that case. Similarly the revenue maximizer is not unique on the inactive set; the shorting cost is pinned down only by the paper's selection of the least maximizer, and (16) is false for any other selection. Finally, (11) requires an argument that the two investors cannot both be short while asset 1 is in positive supply. This uses optimality of both portfolios, not just of one.

Formalization scope

Everything is stated at one state $(\omega,t)$ of the paper's continuous-time economy, about real numbers. The continuous-time economy of §2 (Brownian filtrations, consumption streams, the dynamics of wealth) is the paper's motivation and is not formalized; the formalized statements are its instantaneous equilibrium conditions. The time index is dropped throughout, and the paper's "arbitrary process $x_t$" in Proposition 1 becomes an arbitrary real number.

Conventions:

• Rates are per unit of volatility; the dollar rates are $\Phi=\phi\sigma_1$ and $\Gamma=\gamma\sigma_1$, never obtained by division.
• $m^+$ and $m^-$ are written as $\max\{m,0\}$ and $\max\{-m,0\}$; indicators are if … then … else 0.
• Dollar positions are $\pi^{(a)}_1=W^{(a)}p^{(a)}_1$.
• The standing assumptions are hypotheses of every equilibrium statement: $\sigma_1,\sigma_2>0$ (the standing assumption of §3), $S_1>0$, $W^{(o)},W^{(p)}>0$, and $\theta^{(p)}_1\le\theta^{(o)}_1$.
• The shorting-cost condition (4) is stated in its per-volatility form (10), over $y\ge\gamma$, with the least maximizer selected as in (13). A single lending agent is built in.
• Consumption clearing and asset-2 clearing are not part of the equilibrium predicate; no statement uses them, so leaving them out makes every statement more general.

Corrected slips of the page, each disclosed in the item concerned:

1. Proposition 1's "the optimal portfolio satisfies (9)" fails when $\phi=\gamma$; the converse direction is stated under $\phi>\gamma$, and the constraint $0\le x\le\theta_2$ only where $\theta_2\ge0$.
2. The indicator in (12) should be $\mathbb 1_{\{\theta^{(p)}_1+\gamma\ge0\}}$, not $\mathbb 1_{\{\theta^{(p)}_1\ge0\}}$; the least maximizer (13) is unaffected.
3. (18) prints "$\neq\emptyset$"; its proof shows the set is empty, which is what is stated.

The results (11), (13) and (14) are not built into the equilibrium predicate. With them assumed, the goal would reduce to a four-line computation; they are separate items to be proved. The definitions are short and self-contained, needing only real arithmetic from Mathlib. Proofs of the milestones, and proofs of the goal that use the milestones, are welcome.

Selected references

• T. Evgeniou, J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Swiss Finance Institute Research Paper N°22-21, version of September 22, 2022 — the source of this mission. Published as J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Management Science (2024), https://doi.org/10.1287/mnsc.2023.01887, whose numbering is not used here.
• G. D'Avolio, The market for borrowing stock, Journal of Financial Economics 66 (2002), 271–306.
• C. Jones, O. Lamont, Short-sale constraints and stock returns, Journal of Financial Economics 66 (2002).
• R. Radner, Existence of equilibrium of plans, prices and price expectations in a sequence of markets, Econometrica 40 (2) (1972), 289–303.

Motivation

Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. Computing the optimal adjustable solution is intractable in general, and even for a single budget constraint it cannot be approximated within $\Omega(\log n/\log\log n)$ under a standard complexity assumption (Feige, Jain, Mahdian, Mirrokni, IPCO 2007), where $n$ is the number of decision variables.

Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by one linear program and are widely used in practice. The question is how much they lose in the worst case.

Uncertainty sets in applications are rarely a single budget: demand is usually grouped (by region, product family or time period) with a separate budget per group. When the groups are disjoint the set is a Cartesian product of budget sets, a class studied by Gupta et al. and by Feige et al. in the robust covering literature.

Timeline. Bertsimas and Goyal (2012) proved that affine policies are within $O(\sqrt m)$ of the adjustable optimum for general uncertainty sets and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved $O(\log n/\log\log n)$ for a single budget set (Theorem 3.1, the first mission of this series) and $O(\log^2 n/\log\log n)$ for disjoint constrained budgeted sets (Theorem 4.1, the goal of this mission).

Setting

Let $A\in\mathbb R^{m\times n}$, a non-negative recourse matrix $B\in\mathbb R^{m\times n}_+$, costs $c,d\in\mathbb R^n_+$ and a polyhedral set $\mathcal X\subseteq\mathbb R^n$ be given. For an uncertainty set $\mathcal U\subseteq\mathbb R^m$ of right-hand sides, problem (1.1) is

$$z_{AR}(\mathcal U)=\min_{x\in\mathcal X}\ c^Tx+\max_{h\in\mathcal U}\ \min_{y(h)\ge0}\big\{d^Ty(h)\ :\ Ax+By(h)\ge h\big\}.$$

A first-stage $x$ and a recourse rule $y(\cdot)$ form a feasible solution when $x\in\mathcal X$ and $y(h)\ge0$, $Ax+By(h)\ge h$ for every $h\in\mathcal U$. The affine problem (2.1) restricts the rule to $y(h)=Ph+q$ (still requiring $Ph+q\ge0$ on $\mathcal U$); its value is $z_{Aff}(\mathcal U)\ge z_{AR}(\mathcal U)$.

Let $S_1,\dots,S_L$ be a partition of $[m]$ and $w_{\ell i}\in[0,1]$ weights. The disjoint constrained budgeted set (4.1) is

$$\mathcal U=\Big\{h\in[0,1]^m\ :\ \sum_{i\in S_\ell}w_{\ell i}h_i\le1\ \ \forall\ell\in[L]\Big\}.$$

With $L=1$ it is the budget of uncertainty set of the first mission.

The fractional covering value (3.2) of a requirement $h$ is $z(h)=\min_{y\ge0}\{d^Ty: By\ge h\}$. In an online fractional covering problem the rows to be covered arrive in batches and a solution may only be increased; an online algorithm $\mathcal A$ is $\rho$-competitive when its cost on every sequence is at most $\rho$ times the offline optimum $\Theta$. Throughout, $\log$ is the natural logarithm and $\beta=8\log n/\log\log n$.

Formalization targets

Goal: Theorem 4.1

$$z_{Aff}(\mathcal U)=O\Big(\frac{\log^2n}{\log\log n}\Big)\cdot z_{AR}(\mathcal U)$$

for every instance with $\mathcal U$ a disjoint constrained budgeted set: there are $C>0$ and $N$ such that $z_{Aff}\le C\frac{\log^2n}{\log\log n}z_{AR}$ for all $n\ge N$, all $m$, every number $L$ of blocks and all data. The constant is unfixed, and the bound must not depend on $L$.

Milestones (the paper's proof, in order)

1. Lemma 3.3 (structural result), restated from the first mission: if covering each row $i\in\mathcal J$ costs more than $4\gamma\frac{\log n}{\log\log n}w_i$ while every scenario $\mathcal W\subseteq\mathcal J$ with $\sum_{\mathcal W}w_i\le1$ costs at most $\gamma$, then $z(\mathcal J)\le4\gamma\frac{\log n}{\log\log n}$ (for $n$ large).
2. Lemma 4.1 — for a greedy scenario $a_1,\dots,a_L$ chosen by Algorithm 1, the online cost $\nu_L$ is at most $\rho\cdot\mathrm{OPT}$.
3. Lemma 4.2 — the affine solution (4.7), a linear part on the thresholded components plus a static part, is feasible.
4. Lemma 4.3 — the linear part costs at most $\beta\rho\cdot\mathrm{OPT}$ for every $h\in\mathcal U$.
5. Lemma 4.4 — the static part costs at most $(1+2\rho+\beta\rho)\cdot\mathrm{OPT}$.

With $\rho=O(\log n)$, Lemmas 4.3 and 4.4 give the goal.

Significance

The result. For disjoint budgets the bound is within a $\log n$ factor of the hardness bound for a single budget, and it does not depend on the number of groups $L$. It shows that affine policies stay near-optimal beyond the single-budget case, for a class that models grouped demand. The paper notes that it is open whether the extra $\log n$ factor is necessary. Gupta et al. give an $O(\log n)$-approximation for a special case with 0/1 matrices and equal weights, but their algorithm is not an affine policy.

Formalizing it. The theorem is proved on paper; no machine-checked proof is known. The formal development makes explicit what the paper uses about the online covering algorithm (monotone, covering, competitive), handles the "without loss of generality" relabelling of the blocks in the greedy scenario, and records two gaps in the proof of Lemma 4.4 (zero weights, and a zero increment $\nu_\ell-\nu_{\ell-1}$, for which Lemma 3.3 is stated with $\gamma>0$).

Difficulty

The thresholds that split cheap from expensive components cannot use the single quantity $\mathrm{OPT}$ as in the single-budget case: a scenario may activate one budget in every block at once, and summing per-block bounds gives a factor $L$. That is the $O(L\log n/\log\log n)$ bound of the paper's Section 5. Removing the dependence on $L$ requires per-block thresholds that add up to $O(\log n)\cdot\mathrm{OPT}$, and the paper obtains them from the increments of an online covering algorithm along a greedily chosen worst sequence of scenarios. A proof of the goal therefore needs an $O(\log n)$-competitive online fractional covering algorithm, Buchbinder and Naor's Theorem 4.1, posed on this platform as BNCovPack.Covering.theorem_4_1 (b57de23d-5953-424f-a729-5a018aa74b37, open). That theorem requires positive costs, so zero-cost columns, which this paper allows, need separate handling. The static part also needs Lemma 3.3, the core of the first mission.

Formalization scope

• Data. Vectors are functions on Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean indices and blocks are 0-based. First stage and recourse share the dimension $n$, as on p. 1. The partition is S : Fin L → Finset (Fin m), pairwise disjoint and covering Fin m (empty blocks allowed).
• Values. $z_{AR}$, $z_{Aff}$, $z(h)$, $\Theta$ and $z_{Sta}$ are infima in the extended reals, $+\infty$ when infeasible. A formalization with real infima (equal to $0$ on infeasible problems) or without $Ph+q\ge0$ would trivialize the goal and is excluded, as is a constant $C$ that depends on the instance or on $L$.
• Standing assumptions of p. 1: $B\ge0$, $c,d\ge0$, $\mathcal X$ polyhedral, $w_{\ell i}\in[0,1]$, $S$ a partition. "$\mathcal U\subseteq[0,1]^m$ compact convex with $e_i\in\mathcal U$" holds for the set (4.1) and is not added.
• Added hypotheses and corrections. (i) $c^Tx\ge0$ for $x\in\mathcal X$: Theorem 4.1 is false without it (already for $L=1$), and it holds whenever $\mathcal X\subseteq\mathbb R^n_+$. (ii) $n\ge3$ where $\beta\ge0$ is needed, and a threshold $N_0$ in Lemma 3.3, which as printed fails at $n=2$. (iii) Covering solutions $v_i$ are required only for $i\in\mathcal I$.
• The online algorithm is an abstract structure OnlineCover with ratio $\rho$: starting at $0$, non-negative, monotone, covering every revealed coverable row, and $\rho$-competitive on disjoint batches. The milestones hold for every such algorithm, with the paper's $O(\log n)$ written as $\rho$. The goal does not mention the algorithm. Algorithm 1 is a predicate on a run (a bijection of blocks and the chosen scenarios) with its maximality clause, so ties are arbitrary.
• Thresholds are in multiplied form $\alpha_iz(e_i)\le w\beta(\nu_\ell-\nu_{\ell-1})$; no division by a weight that may be $0$.
• Infrastructure. Lemma 3.3 is shared with the first mission and needs LP duality and randomized rounding. Buchbinder–Naor's theorem, or any $O(\log n)$-competitive online fractional covering algorithm, is needed for the goal. Proofs of any milestone are welcome.

The source is arXiv:1807.00163v2; its printed page numbers equal the PDF page numbers.

Selected references

• O. El Housni, V. Goyal, On the Optimality of Affine Policies for Budgeted Uncertainty Sets, arXiv:1807.00163v2, 2019; Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1807.00163
• N. Buchbinder, J. Naor, Online primal-dual algorithms for covering and packing, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0363
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2), 2012. https://doi.org/10.1007/s10107-011-0444-4
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007, LNCS 4513.
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2), 2004. https://doi.org/10.1007/s10107-003-0454-y

Why bound the order-up-to level of a perishable product

Food, blood products, pharmaceuticals and many retail goods are perishable: a unit is usable for a fixed number of periods and is then discarded. A seller of such a product decides every period how much to order, what price to charge, and how much stock to deplete or dispose of. Because units of different ages coexist, the state of the system is a vector of inventory levels by remaining lifetime, and the exact dynamic program suffers from the curse of dimensionality in that vector. Nahmias's survey (Nahmias 1982) records this obstacle for the pure ordering problem; adding pricing makes it worse.

Chen, Pang and Pan (Operations Research 62(2), 2014) analyse the joint ordering, pricing and disposal problem with the tools of L♮-concavity (Murota's discrete convex analysis, extended to real vectors). Their §4 shows that the optimal profit-to-go is L♮-concave, which yields monotone policies with bounded sensitivity. Their §6.1 then shows that two one-dimensional, myopic problems bracket the optimal order-up-to level, which is the starting point of the heuristics of §6.2. This mission formalizes the backlogging case of that bracketing result, Theorem 3.

Setting

A single product has lifetime $l\ge 2$ periods; the replenishment lead time is zero, and unmet demand is backlogged. The unit costs are $c$ (ordering), $h^+$ (holding), $h^-$ (backlogging) and $\theta$ (disposal); $\gamma$ is the discount factor. The seller chooses the expected demand $d$ in an interval $\mathcal D=[\underline d,\bar d]$, which is equivalent to choosing the price $P(d)$, where $P$ is strictly decreasing. The expected revenue $P(d)\,d$ is continuous and concave on $\mathcal D$ (Assumption 1). Realized demand is $d_t=d+\varepsilon_t$, with independent, identically distributed, zero-mean noise supported in $[A,B]$, $A\le 0\le B$, and $\underline d+A\ge 0$.

The state $s=(s_1,\dots,s_{l-1})$ lies in $\mathcal S=\{s_1\le\dots\le s_{l-1}\}$: $s_i$ is the inventory with residual lifetime at most $i$ periods (negative values are backorders), and $s_{l-1}$ is the inventory position. Each period the seller picks an order-up-to level $s_l\ge s_{l-1}$, the demand level $d$, and, after demand is realized, a depletion $a$ with $s_1\vee d_t\le a\le s_l\vee d_t$. The next state is $\tilde s=(s_2-a,\dots,s_l-a)$. The one-period objective is

$$\varphi_t(s,s_l,d,a\mid\varepsilon_t)=\gamma c\,\tilde s_{l-1}-cs_l-\theta(a-d_t)-h^+(s_l-a)^+-h^-(a-s_l)^++\gamma f_{t+1}(\tilde s),$$

$g_t$ maximizes it over $a$, $G_t(s,s_l,d)=P(d)d+\mathbb E[g_t]$, and the profit-to-go is $f_t(s)=\max_{s_l\ge s_{l-1},\,d\in\mathcal D}G_t(s,s_l,d)$ with $f_{T+1}=0$.

Under $\theta\ge h^+/(1-\gamma)$ only expiring stock is disposed of (Proposition 1). With $\tilde\theta=\theta+\gamma c-h^+$ and $v_t(s_l,d_t)=-(1-\gamma)cs_l-\gamma cd_t-h^+(s_l-d_t)^+-h^-(d_t-s_l)^+$, the two myopic objectives are

$$\Pi_t(s_l,d)=P(d)d+\mathbb E[v_t(s_l,d_t)],\qquad \tilde\Pi_t(s_l,d)=\Pi_t(s_l,d)-\gamma cs_l-K\,\mathbb E[(s_l-d_t)^+],$$

with $K=\gamma h^++\dots+\gamma^{l-2}h^++\gamma^{l-1}\tilde\theta$. $\bar S_t(d)$ and $\underline S_t(d)$ are their largest maximizers over $s_l\ge0$.

Formalization targets

Goal: Theorem 3 (Bounds), backlogging case

For every period, every state $s\in\mathcal S$ and every $d\in\mathcal D$, the largest optimal order-up-to level $s_{lt}(s,d)$ satisfies

$$\underline S_t(d)\vee s_{l-1}\ \le\ s_{lt}(s,d)\ \le\ \bar S_t(d)\vee s_{l-1}.$$

Milestones, in attack order

1. Lemma 6 (p. 290): $f_t$ is nonincreasing in each coordinate of the state.
2. Proposition 1 (p. 292): if $\theta\ge h^+/(1-\gamma)$, depleting $d_t\vee s_1$ is optimal.
3. The p. 294 decomposition: $\varphi_t$ at $a=d_t\vee s_1$ equals $v_t(s_l,d_t)-\tilde\theta(s_1-d_t)^++\gamma f_{t+1}(\tilde s)$.
4. Theorem 1, first sentence (p. 291), at zero lead time: $f_t$, $g_t$, $\varphi_t$ are L♮-concave.
5. Concavity in $s_l$ (p. 295): $\Pi_t(\cdot,d)$ and $G_t(s,\cdot,d)$ are concave.
6. Upper step (p. 295): $G_t(s,s'_l,d)-G_t(s,s_l,d)\le\Pi_t(s'_l,d)-\Pi_t(s_l,d)$ for $s'_l>s_l\ge s_{l-1}$.

The proof's lower-bound display (p. 295) is not a milestone: as printed, for arbitrary $s'_l>s_l\ge s_{l-1}$, it is false when $h^+>\gamma c$ (see Formalization scope).

Significance

The result. The bounds reduce an $(l-1)$-dimensional optimization to two scalar newsvendor-type problems whose solutions do not depend on the period (Remark 6), and they give interpretable brackets: $\bar S_t(d)$ ignores the future cost of excess stock, while $\underline S_t(d)$ charges every excess unit holding until expiry and then disposal. They justify the one-dimensional heuristics of §6.2 and give a check on any computed policy.

Formalizing it. The paper's proof is short but compresses three steps that need care: the structural results of §4 at zero lead time, the minimal-disposal property, and a coupling argument for the lower bound whose printed display is not correct as stated (see below). A machine-checked development would make the whole chain from the recursion to the bounds explicit, including the existence conventions for optimal decisions. To the knowledge of this mission, none of these results has been formalized in any proof assistant.

Difficulty

The central obstacle is the concavity of $G_t(s,\cdot,d)$ in the order-up-to level. It is not visible from the one-period terms: it rests on L♮-concavity of the whole recursion (Theorem 1), and the depletion constraint $s_1\vee d_t\le a\le s_l\vee d_t$ is not an L♮-convex set, so the standard preservation lemma does not apply to (5) as written.

The lower bound needs a quantitative estimate of how much an extra unit of fresh stock can cost in the future. The printed estimate charges the expiring unit $\tilde\theta$ where an unused unit actually costs $\theta$, so it cannot hold for every pair of order-up-to levels; the lower bound must use that the comparison is only needed below $\underline S_t(d)$, where excess stock is not pushed past the next period's optimal order-up-to level.

Formalization scope

The Lean development lives in the namespace PerishablePricing.Bounds. Its conventions are:

• Carrier $\mathbb R$. The paper treats real and integer vectors at once; only the real case is formalized. L♮-convexity is defined on an explicit domain with real values, the paper's convention for "L♮-convex on a set".
• Indices. States are Fin L → ℝ with $L=l-1\ge1$, 0-based.
• Time. Time counts periods to go: f 0 = 0 is $f_{T+1}$, and $G_t$, $g_t$, $\varphi_t$ use the continuation f n.
• Maxima and expectations. The maxima in the recursion are suprema over nonempty sets whose values are bounded above, and expectations are Bochner integrals against the noise law.
• Optimal decisions. Every optimal decision is a largest maximizer, taken as a hypothesis at the points where it is used. With an arbitrary maximizer the upper bound fails when $\Pi_t(\cdot,d)$ is flat.

The standing assumptions are the hypotheses of every statement:

• nonnegative unit costs and $0\le\gamma\le1$;
• the noise conditions and the strictly decreasing inverse demand;
• Assumption 1;
• $(1-\gamma)c\le h^-$, the §4 assumption $c\le h^-/(1-\gamma)$;
• $h^+\le(1-\gamma)\theta$ with $\gamma<1$, the §6.1 assumption $\theta\ge h^+/(1-\gamma)$, which divides by $1-\gamma$.

Deviations from the page, all disclosed in the items:

• Only the backlogging case of Theorem 3 is stated. The lost-sales case rests on Theorem 2, which is not posed.
• The hypothesis "the starting inventory level of the planning horizon is zero" constrains no object of the statement, and the conclusion is stated for every state.
• $\tilde\Pi_t$'s printed term $-\gamma c\,\tilde s_{l-1}$ depends on the state and the noise. It is read as $-\gamma c\,s_l$, which leaves the maximizers unchanged.
• The objective missing from the printed definition of $\bar S_t(d)$ is $\Pi_t$.
• The upper step's "$G_t=\Pi_t+\gamma\mathbb E[f_{t+1}]$" omits a term constant in $s_l$.
• The lower-bound display of the proof of Theorem 3 is not stated. Its exponents $t+l-3$, $t+l-2$ should read $l-3$, $l-2$, and even then, for arbitrary $s'_l>s_l\ge s_{l-1}$, it fails when $h^+>\gamma c$. Example: $l=2$, deterministic demand, $c=1$, $\gamma=\tfrac12$, $h^+=h^-=1$, $\theta=2$, one period after the current one, $s_1=0$, $d=\tfrac12$, $s_l=100$, $s'_l=101$: the left side is $-3$ and the right side is $-2.75$. In that case an unused unit is disposed of at cost $\theta$, not $\tilde\theta$. Theorem 3 itself is stated as printed, with $\underline S_t(d)$ defined through $\tilde\Pi_t$.

The goal must not be trivialized. Its continuation, the concavity of $G_t$ and the monotonicity of $f_{t+1}$ are properties of the model's own recursion, never hypotheses on abstract functions. Likewise $s_{lt}(s,d)$ is defined through $G_t$, never through $\Pi_t$ or $\tilde\Pi_t$.

A complete development needs:

• L♮-concavity preservation under partial maximization over an L♮-convex set and under expectation;
• concavity of expectations of piecewise-linear functions of the noise;
• measurability and integrability of the stage value $g_t$ in the noise;
• the coupling arguments for Proposition 1 and the lower bound.

The L♮ preservation lemmas are reusable for other discrete-convexity models in inventory theory. Contributions toward any milestone, or toward that infrastructure, are welcome.

The source is the published Operations Research article. In the held scan, printed page = PDF page + 282.

Selected references

• X. Chen, Z. Pang, L. Pan, Coordinating Inventory Control and Pricing Strategies for Perishable Products, Operations Research 62(2):284–300, 2014. https://doi.org/10.1287/opre.2014.1261
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4):937–944, 2008. https://doi.org/10.1287/opre.1070.0482
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680

Motivation

Many businesses are run by an agent on behalf of an owner who cannot see everything the agent does. Two frictions arise together. The agent may shirk, saving the cost of the effort that brings customers in, and the agent may divert cash, pocketing the fee of a customer the owner never sees: a plumbing franchise whose offline jobs bypass the head office, or a home-services platform whose providers are paid off-platform by returning clients. Each friction alone is a classical object of dynamic contract theory: DeMarzo and Sannikov (2006) study cash diversion, and Sun and Tian (2018) study effort incentives with Poisson arrivals. Tian, Astashkina and Duenyas (SSRN 4249177; Management Science, 2024, doi:10.1287/mnsc.2022.01169) solve the problem with both frictions present, in a model where customers arrive by a Poisson process whose rate the agent controls. This mission formalizes the baseline model of their Section 2 and its main result, Theorem 1.

Setting

Customers arrive at rate $\mu$ while the agent exerts effort ($\nu_t=\mu$, at flow cost $c$) and do not arrive while the agent shirks ($\nu_t=0$). Each arriving customer independently uses the unobservable channel $u$ with probability $p$, paying the fee $R^u$, or the observable channel $o$ with probability $1-p$, paying $R^o$. The counting processes $N^u_t$ and $N^o_t$ count the arrivals by channel. The principal observes $N^o$ and the agent's reports $\hat N^u$ of the $u$-arrivals; an unreported $u$-arrival is cash the agent keeps. Both parties discount at rate $r$.

A contract $\gamma=(L,\tau)$ consists of a nondecreasing cumulative payment $L$ (limited liability: payments are never negative) and a termination time $\tau$, both functions of what the principal observes. The agent's utility (2.1) and the principal's utility (2.2) are

$$u(\gamma,\nu,\hat N^u)=\mathbb E\Big[\int_0^\tau e^{-rt}\big[R^u(dN^u_t-d\hat N^u_t)+dL_t+c(1-\mathbb 1[\nu_t=\mu])dt\big]\Big],$$ $$U(\gamma,\bar\nu,N^u)=\mathbb E\Big[\int_0^\tau e^{-rt}\big[R^u dN^u_t+R^o dN^o_t-dL_t-c\,dt\big]\Big].$$

A contract is incentive compatible, $\gamma\in\Gamma^{IC}$, if always working and always reporting truthfully ($\bar\nu$, $\hat N^u=N^u$) is optimal for the agent against every alternative effort process and reporting rule. Write $\bar V=(\mu(pR^u+(1-p)R^o)-c)/r$, $\beta=c/\mu$, $\beta^o=(\beta-pR^u)/(1-p)$, and assume the standing condition (2.5), $\bar V\ge0$.

The candidate optimal contracts $\gamma^i(w)$, $i=1,2,3$, track a promised utility $W_t$ that starts at $w$, drifts by $dW_t=r(W_t-\bar w^i)dt$, jumps up at rewarded arrivals, triggers termination when it reaches $0$, and is capped at a tenure threshold $\bar w^i$, with the excess paid out: $\bar w^1=\mu pR^u/r$ with jumps $R^u$ at reported $u$-arrivals only (Definition 1); $\bar w^2=c/r$ with jumps $R^u$ and $\beta^o$ (Definition 2); $\bar w^3=c/r$ with jump $\beta$ at every arrival (Definition 3). The principal's value function $F_i$ solves a differential equation with advanced arguments, for instance in the first scenario

$$rF(w)=r\bar V+\mu p\,[F(w+R^u)-F(w)]+r(w-\bar w^1)F'(w),\qquad F(0)=0,\qquad (2.9)$$

extended by $F(w)=F(\bar w^1)-(w-\bar w^1)$ beyond the threshold.

Formalization targets

Goal: Theorem 1 (p. 21)

With $w^i=\arg\max_{w\ge0}F_i(w)$ (2.14), the optimal contract in $\Gamma^{IC}$ is

$$\gamma^1(w^1)\ \text{if}\ c\le\mu pR^u,\qquad\gamma^2(w^2)\ \text{if}\ \mu pR^u<c<\mu R^u,\qquad\gamma^3(w^3)\ \text{if}\ c\ge\mu R^u,$$

meaning $\gamma^i(w^i)\in\Gamma^{IC}$ and $U(\gamma,\bar\nu,N^u)\le U(\gamma^i(w^i),\bar\nu,N^u)$ for every $\gamma\in\Gamma^{IC}$.

Milestones

1. Lemma 4 (three items, one per scenario): the scenario's equation with $F(0)=0$ has a unique solution $F_i$ on $[0,\infty)$, concave, with $F_i'\ge-1$.
2. Proposition 1: $U(\gamma^i(w),\bar\nu,N^u)=F_i(w)$ and $u(\gamma^i(w),\bar\nu,N^u)=w$ for $w\in[0,\bar w^i]$.
3. The bound (B.12)–(B.16): for $F=F_i$, the drift $\Phi$ of (B.7) is nonpositive at every jump pair satisfying $H^u\ge R^u$ and $pH^u+(1-p)H^o\ge\beta$.
4. Proposition 2: $F_i(u(\gamma,\bar\nu,N^u))\ge U(\gamma,\bar\nu,N^u)$ for every $\gamma\in\Gamma^{IC}$.

Significance

The theorem shows that three simple contracts, each a probation period followed by termination or tenure, solve a two-dimensional moral hazard problem, and it tells which incentive constraint binds: truth-telling alone when $c\le\mu pR^u$, both when $\mu pR^u<c<\mu R^u$, effort alone when $c\ge\mu R^u$. Section 2.4 of the paper extends optimality to contracts that may let the agent shirk, and Sections 3 to 5 build monitoring, dynamic pricing and continuous effort on the same baseline, so the definitions here are the substrate for those results.

The result is proved in the paper, with two of the three scenarios of Lemma 4 and Proposition 1 left to the reader. It has not been formalized. A complete development would give a machine-checked account of a continuous-time contracting model driven by a controlled point process, which no library currently provides.

Difficulty

Three steps resist a direct transcription of the paper's argument. First, the value-function equations are not ordinary differential equations: they evaluate $F$ at $w+R^u$, $w+\beta^o$, $w+\beta$, so existence, uniqueness and concavity come from a backward induction over intervals of length $R^u$ starting at the tenure threshold, and concavity holds only under (2.5). Second, the upper bound for an arbitrary incentive compatible contract needs the promise-keeping representation of the agent's continuation utility, a martingale representation for point-process filtrations, and a verification argument through Itô's formula for jump processes; the paper's proof uses the terminal condition $F(W_\tau)=F(0)$ and a martingale property without addressing $\tau=\infty$ or integrability. Third, the characterization of incentive compatibility by the jump conditions $H^u\ge R^u$ and $pH^u+(1-p)H^o\ge\beta$ is argued in the paper by a one-deviation heuristic, whereas (IC) quantifies over all joint deviations in effort and reporting.

Formalization scope

The arrival process is built from an i.i.d. sequence of standard exponential clocks and Bernoulli($p$) channel marks: the next arrival occurs when $\mu$ times the effort time accumulated since the last arrival reaches the next clock. Strategies (effort and reporting) and contracts (cumulative payment and termination rule) are functions of the relevant history: the agent's full arrival history for strategies, the principal's observed history for contracts, which is the general form of predictable and adapted processes for a marked point process. Effort at time $t$ depends only on arrivals strictly before $t$; reports can hide $u$-arrivals but never invent them. Utilities are expectations in $[0,\infty]$ of nonnegative pathwise terms, payments enter as a Lebesgue–Stieltjes integral over $[0,\tau]$, and $U$ is real-valued on contracts with finite expected payments, which $\Gamma^{IC}$ requires. (IC) quantifies over every measurable strategy.

The value functions are pinned by solution classes: continuity on $[0,\infty)$, the slope $-1$ extension beyond $\bar w^i$, differentiability and the equation on $[0,\bar w^i)$, and $F(0)=0$. The printed (2.11) has a stray $-rF(w)$ on its right-hand side; the formalization uses the equation obtained from the HJB equation (2.7), which is the one the proofs use. Proposition 2 is stated for every promised utility $w\ge0$ (the page says $w\in[0,\bar w^i]$), which is what the optimality argument (2.15) needs. The bound (B.12)–(B.16) adds the condition $w+H^o\ge0$, since $F$ is defined on $[0,\infty)$.

The formalization does not trivialize: $\Gamma^{IC}$ is not shrunk by restricting deviations, contracts react to reports so that hiding an arrival changes what the agent is paid, $U$ carries no junk value on $\Gamma^{IC}$, and the goal quantifies over solutions of the value-function equations rather than over arbitrary concave functions; Lemma 4 is what makes that quantification non-vacuous.

Out of scope: Theorem 2 (optimality in the larger space $\Gamma$, whose shirking payoffs are defined only inside its proof), Lemma 5, Sections 3 to 5, and as separate items Lemmas 1 to 3, Lemma 14 and the equivalence of (IC) with the two jump conditions, which need a promised-utility process with left limits built from conditional expectations. Contributions of that infrastructure (point-process martingale representation, Itô's formula for finite-variation jump processes, a verification theorem for discounted optimal control) are welcome and reusable beyond this mission.

Selected references

• F. Tian, E. Astashkina, I. Duenyas, Dynamic Contract Design in the Presence of Double Moral Hazard, SSRN 4249177 (preprint); Management Science, 2024. https://ssrn.com/abstract=4249177, https://doi.org/10.1287/mnsc.2022.01169
• P. M. DeMarzo, Y. Sannikov, Optimal Security Design and Dynamic Capital Structure in a Continuous-Time Agency Model, Journal of Finance 61(6), 2006. https://doi.org/10.1111/j.1540-6261.2006.01033.x
• P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 2018. https://doi.org/10.1287/mnsc.2017.2795
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8

Motivation

Approximate policy iteration is the template behind most practical reinforcement-learning systems for large state spaces: alternate between choosing a policy that looks good under the current value estimate and estimating the value of that policy, with errors in both steps. Game-playing systems such as AlphaZero add two ingredients to this template: a multi-step lookahead (tree search) when choosing the policy, and a linear or neural value-function approximation fitted from a few evaluated states. Classical error bounds for approximate policy iteration (Bertsekas and Tsitsiklis, 1996) assume that each evaluation error is bounded by a fixed $\delta$; Efroni, Dalal, Scherrer and Mannor (2019) extended them to $H$-step lookahead policies. Neither analysis asks whether a fitted value function actually meets such a bound.

Winnicki, Lubars, Livesay and Srikant (arXiv:2109.13419, Operations Research, 2025) show that it need not: with least-squares fitting on a subset of states, the iterates of approximate policy iteration can diverge (their Section 3.2). They then prove that sufficient lookahead $H$ and rollout length $m$ restore convergence, with an explicit finite-time error bound. This mission formalizes that bound.

Setting

A Markov decision process $(\mathcal S,\mathcal A,P,r,\alpha)$ has a finite set of states $\mathcal S$, a finite set of actions $\mathcal A$, transition probabilities $P_{ij}(a)$ of moving from state $i$ to state $j$ under action $a$, mean rewards $r(s,a)\in[0,1]$, and a discount factor $\alpha\in(0,1)$. A deterministic policy is a map $\mu:\mathcal S\to\mathcal A$. Its value is the expected discounted reward

$$J^\mu(s)=E\Big[\sum_{k\ge0}\alpha^k r(s_k,\mu(s_k))\,\Big|\,s_0=s\Big],$$

and the optimal reward-to-go is $J^*(s)=\max_\mu J^\mu(s)$. Vectors $J\in\mathbb R^{|\mathcal S|}$ are compared in the sup norm $\|\cdot\|_\infty$. The policy operator and the Bellman operator are

$$(T_\mu J)(s)=r(s,\mu(s))+\alpha\sum_jP_{sj}(\mu(s))J(j),\qquad (TJ)(s)=\max_{a}\Big\{r(s,a)+\alpha\sum_jP_{sj}(a)J(j)\Big\}.$$

Each state $i$ has a feature vector $\phi(i)\in\mathbb R^d$; $\Phi$ is the matrix with rows $\phi(i)$. For a set of states $\mathcal D$, $\Phi_{\mathcal D}$ keeps the rows indexed by $\mathcal D$ and $\mathcal P_{\mathcal D}$ selects the entries of a vector indexed by $\mathcal D$.

Algorithm 2 starts from an arbitrary $J_0$ and, at iteration $k$, (i) picks a policy $\mu_{k+1}$ with $\|T^HJ_k-T_{\mu_{k+1}}T^{H-1}J_k\|_\infty\le\varepsilon_{LA}$ (an inexact $H$-step lookahead); (ii) forms the noisy return $\hat J^{\mu_{k+1}}(i)=T^m_{\mu_{k+1}}T^{H-1}J_k(i)+w_{k+1}(i)$ on an evaluation set $\mathcal D_k$; (iii) fits $\theta_{k+1}$ by least squares on $\mathcal D_k$ and sets $J_{k+1}=\Phi\theta_{k+1}$. Assumption 1 asks that the features of $\mathcal D_k$ have rank $d$ for every $k$ and that $\|w_k\|_\infty\le\varepsilon_{PE}$. Under it the fit is linear, $J_{k+1}=\mathcal M_{k+1}\hat J^{\mu_{k+1}}$ with $\mathcal M=\Phi(\Phi_{\mathcal D}^\top\Phi_{\mathcal D})^{-1}\Phi_{\mathcal D}^\top\mathcal P_{\mathcal D}$, and the paper defines

$$\delta_{FV}=\sup_k\|\mathcal M_k\|_\infty,\qquad \delta_{app}=\sup_{k,\mu}\|\mathcal M_kJ^\mu-J^\mu\|_\infty,\qquad \beta=\alpha^{m+H-1}\delta_{FV},\qquad \tau=\frac{\alpha^m+\alpha^{m+H-1}}{1-\alpha}\delta_{FV}+\delta_{app}+\delta_{FV}\varepsilon_{PE}.$$

Formalization targets

Goal: Theorem 1 (p. 14, eq. (10))

If $m+H-1>\log(\delta_{FV})/\log(1/\alpha)$, then under Assumption 1 every run of Algorithm 2 satisfies, for every $k\ge0$,

$$\|J^{\mu_k}-J^*\|_\infty\le\frac{\alpha^{kH}}{1-\alpha}+\frac{2\alpha^H\|J^{\mu_0}-J_0\|_\infty}{1-\alpha}\,k\max(\alpha^H,\beta)^{k-1}+\frac{2\alpha^H\frac{\tau}{1-\beta}+\varepsilon_{LA}}{(1-\alpha^H)(1-\alpha)}.$$

Milestones

In the order the proof uses them:

1. Section 2: the Bellman equations $J^\mu=T_\mu J^\mu$ (unique solution) and $J^*=TJ^*$ (eq. (2)); the contraction $\|TJ-J^*\|_\infty\le\alpha\|J-J^*\|_\infty$; shift and monotonicity of $T$, $T_\mu$ (eqs. (3)–(4)).
2. Section 3.1, eq. (6): the closed form $J_{k+1}=\mathcal M_{k+1}\hat J^{\mu_{k+1}}$ of the least-squares step.
3. Appendix A, eq. (15): one lookahead step with evaluation error $\delta_k$,

$$\|J^{\mu_{k+1}}-J^*\|_\infty\le\alpha^H\|J^{\mu_k}-J^*\|_\infty+\frac{2\alpha^H\delta_k+\varepsilon_{LA}}{1-\alpha}.$$

4. Proposition 1 (p. 13): the bound for Algorithm 3, an abstract scheme whose evaluation error at step $k$ is at most $\delta_k$, in three displays: the general bound, the bound under $\delta_k\le\beta^k\delta_0+\mu$, and its limsup.
5. Appendix B, eq. (19): for Algorithm 2, $\delta_k=\|J_k-J^{\mu_k}\|_\infty$ satisfies $\delta_k\le\beta\delta_{k-1}+\tau$ and, if $\beta<1$, $\delta_k\le\beta^k\delta_0+\tau/(1-\beta)$.

Significance

Theorem 1 states a sufficient condition for convergence that does not depend on the size of the state space: lookahead plus rollout depth must exceed $\log\delta_{FV}/\log(1/\alpha)$, where $\delta_{FV}$ depends only on the features and the evaluation sets. Paired with the divergence example of Section 3.2, it shows that lookahead is not merely a heuristic improvement but can be what makes approximate policy iteration with linear function approximation stable. Proposition 1 is a reusable interface: any policy-evaluation scheme whose errors satisfy a geometric-plus-floor bound inherits the same convergence guarantee; the paper's gradient-descent variant is obtained this way.

The result is proved on paper; it has not been machine-checked. The Prove2Me platform has the finite-MDP layer used here (transition kernels, policy values as discounted series, the Bellman optimality operator), exact modified policy iteration, and a one-step bound for greedy approximate policy iteration with $Q$-functions ($H=1$, no lookahead error). It has no lookahead bound, no least-squares value-function fit, and no finite-time bound for approximate policy iteration with function approximation. A complete development would add the Bellman equations for deterministic policies, the lookahead step (15), the least-squares projection identity, and the error recursion, all of which are reusable for other analyses of approximate dynamic programming.

Difficulty

The obvious argument fails at the evaluation step. Classical analyses treat $\|J_k-J^{\mu_k}\|_\infty\le\delta$ as given; here the error is produced by the algorithm and fed back: the fitted $J_k$ is the input of the next lookahead, and the least-squares operator can amplify sup-norm errors by a factor $\delta_{FV}$, which is at least $1$ whenever $d\ge1$. The error recursion therefore contracts only when $\alpha^{m+H-1}\delta_{FV}<1$. A second point is the lookahead step (15), which must hold for an arbitrary previous policy and an inexact lookahead, and rests on the increase of $T^nJ^\mu$ in $n$ rather than on contraction alone. Finally, combining the geometric decay of the evaluation errors with the $\alpha^H$-contraction of (15) requires a convolution estimate that yields the factor $k\max(\alpha^H,\beta)^{k-1}$.

Formalization scope

States and actions are finite nonempty types; the transition kernel is the published IsTransitionKernel, $J^\mu$ is the published PolicyValue (a discounted series of expected rewards, not a fixed point of $T_\mu$) of the point-mass policy at $\mu$, $T$ is the published BellmanOperator, and $J^*$ is the maximum of $J^\mu$ over the finitely many deterministic policies. Rewards enter only through their means $r(s,a)\in[0,1]$. Vectors are functions $\mathcal S\to\mathbb R$ with the sup norm; matrix norms are Mathlib's $\ell^\infty$ operator norm (maximum absolute row sum). The rank condition of Assumption 1 is $\det(\Phi_{\mathcal D_k}^\top\Phi_{\mathcal D_k})\ne0$ for every $k$; Lean's matrix inverse is zero on singular matrices, so no statement relies on it without this hypothesis.

Conventions fixed where the page is loose: Algorithms 2 and 3 are predicates on whole runs, quantified over every admissible lookahead policy, noise and minimiser. $\mu_0$, which Algorithm 2 never produces, is free, so every bound holds for every deterministic $\mu_0$. $\mathcal M_k$ is the operator of $\mathcal D_k$ (eq. (6) calls it $\mathcal M_{k+1}$; the suprema agree). $\delta_{app}$ is the supremum over all $k$ and all deterministic policies. Algorithm 3 is stated with $\|J_k-J^{\mu_k}\|_\infty\le\delta_k$, the index of (15) and Appendix B, and without the representation $J_k=\Phi\theta_k$, which Proposition 1 does not use. Proposition 1's first display divides by $1-\alpha^{H-1}$ and is stated for $H\ge2$; the other results take $H\ge1$. The noise bound $\|w_k\|_\infty\le\varepsilon_{PE}$ is imposed on the whole vector instead of setting $w_k(i)=0$ off $\mathcal D_k$; off $\mathcal D_k$ it constrains only entries the run never reads. The limsup is stated as "for every $\varepsilon>0$, eventually $\le$ bound $+\varepsilon$". The hypothesis of Theorem 1 is kept with the real logarithm as printed; for $\delta_{FV}>0$ it is equivalent to $\beta<1$, and when $\delta_{FV}=0$ (possible only if $d=0$) it reads $m+H-1>0$.

A formalization that fixes the lookahead policy to an exact argmax, the noise to zero, or $\mu_0$ to a convenient policy proves a special case and is ruled out; so is defining $J^\mu$ or $J^*$ as a fixed point, which would make eq. (2) definitional.

Contributions welcome: proofs of the Section 2 milestones from the series definition of $J^\mu$, the least-squares identity (6), the lookahead step (15), and the recursions of Proposition 1 and Appendix B. Theorem 2 of the paper (gradient-descent fitting) is not part of this mission: its Assumption 2 places no lower bound on the step size, and the statement fails for negative step sizes.

Selected references

• A. Winnicki, J. Lubars, M. Livesay, R. Srikant, The Role of Lookahead and Approximate Policy Evaluation in Reinforcement Learning with Linear Value Function Approximation, Operations Research, 2025; arXiv:2109.13419v7. https://arxiv.org/abs/2109.13419
• Y. Efroni, G. Dalal, B. Scherrer, S. Mannor, How to Combine Tree-Search Methods in Reinforcement Learning, AAAI, 2019. https://arxiv.org/abs/1809.01843
• D. P. Bertsekas, J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.
• D. P. Bertsekas, Reinforcement Learning and Optimal Control, Athena Scientific, 2019.
• M. G. Lagoudakis, R. Parr, Least-Squares Policy Iteration, Journal of Machine Learning Research 4, 2003. https://www.jmlr.org/papers/v4/lagoudakis03a.html