Dynamic Programming

Selling an asset bought with debt

Firms that hold a large, divisible asset (a commodity inventory, a block of shares, a stock of natural gas) often financed it with debt and must sell it over time to repay that debt. Without debt, the timing problem is classical: Karlin (1962) showed that a non-divisible asset facing independent prices should be sold the first time the price exceeds a reservation price. Debt changes the incentives in two opposite directions. Limited liability caps the shareholders' loss at zero, which rewards gambling on high future prices and delays selling. Bankruptcy also destroys the value of the unsold asset, an indirect bankruptcy cost, which rewards selling early to secure the debt payment. Ahn, Wang and Wu (SSRN 3472345, published in Operations Research 69(4), 2021, doi:10.1287/opre.2019.1961) solve the resulting dynamic program with Markov prices. This mission formalizes their central structural result: the optimal first sale under a single debt payment due before the end of the horizon.

Setting

A seller holds an amount $x_t \in [0,1]$ of a divisible asset at the beginning of period $t = 1, \dots, T$, with $x_1 = 1$. The selling price $P_t$ follows a Markov process: the law of $P_{t+1}$ given $P_t = p$ is a probability kernel $\kappa_t(p)$, with finite conditional mean. Write $E_t$ for the expectation given the current price. The discount factor is $\rho \in (0,1)$, the per-period selling capacity is $\ell \in (0,1]$, and unsold asset is worthless after period $T$.

The debt-free value $U_t(x,p)$ solves, with $U_{T+1} \equiv 0$,

$$U_t(x,p) = \max_{0 \le q \le \min(x,\ell)} \; p\,q + \rho\,E_t\,U_{t+1}(x-q, P_{t+1}).$$

The debt-free critical price is $R^o_t = \rho\,E[U_{t+1}(1,P_{t+1}) \mid P_t]$.

Debt. A schedule $d = (d_t)_{t \le m}$, $d_t \ge 0$, is due at the end of periods $t = 1, \dots, m$, with maturity $1 \le m \le T$. The seller's working capital $w_t$ starts at $w_1 = 0$ and grows at rate $1/\rho$. In period $t \le m$, a quantity $q$ is feasible if $0 \le q \le \min(x_t,\ell)$ and $w_t + p_t q \ge d_t$. If no quantity is feasible, the seller is bankrupt and the equity value $V_t(x,w,p;d)$ is $0$. Otherwise

$$V_m(x,w,p;d) = \max_{q \text{ feasible}} \; p\,q + w - d_m + \rho\,E_m\,U_{m+1}(x-q,P_{m+1}),$$ $$V_t(x,w,p;d) = \max_{q \text{ feasible}} \; \rho\,E_t\,V_{t+1}\big(x-q,\ \rho^{-1}(w + p\,q - d_t),\ P_{t+1}; d\big), \quad t < m.$$

For a single payment $d_m = D$ (and $d_t = 0$ otherwise), write $\delta_t = \rho^{m-t}D$ and $C_t = \rho\,E_t V_{t+1}(1,0,P_{t+1};d)$, with $V_{m+1} := 0$. The net effect of debt is

$$\Delta_t = V_t(1,0,P_t;d) - \big(U_t(1,P_t) - \rho^{m-t}D\big).$$

It is the value of limited liability net of the bankruptcy cost. The two critical prices are

$$R^{(1)}_t = \min\Big\{\frac{\delta_t R^o_t}{R^o_t - C_t},\ C_t + \delta_t\Big\}, \qquad R^{(2)}_t = \max\{R^o_t,\ C_t + \delta_t\}.$$

Formalization targets

Goal: Proposition 4 (p. 14)

Assume $\ell = 1$, a single payment $D > 0$ at $m < T$, a period $t \le m$ before any sale ($x = 1$, $w = 0$), and a price $p > 0$. Then $R^{(1)}_t \le R^{(2)}_t$, and:

$$p < R^{(1)}_t \Rightarrow \text{sell nothing } (t<m) \text{ or bankruptcy } (t=m), \qquad R^{(1)}_t \le p < R^{(2)}_t \Rightarrow q = \delta_t/p \text{ is optimal}, \qquad p \ge R^{(2)}_t \Rightarrow q = 1 \text{ is optimal}.$$

After the debt-securing sale, the optimal quantities coincide with the debt-free ones. Moreover:

$$E_t\Delta_{t+1} < 0 \Rightarrow R^{(1)}_t < R^{(2)}_t = R^o_t, \qquad E_t\Delta_{t+1} \ge 0 \Rightarrow R^{(1)}_t = R^{(2)}_t \ge R^o_t.$$

When $E_t\Delta_{t+1} = 0$, all three prices coincide.

Milestones

In attack order:

1. Lemma 1(i)–(ii) (p. 8). Enough working capital makes $V_t = U_t + w - \sum_{i\ge t}\rho^{i-t}d_i$. With no asset left, $V_t = (w - \sum_{i \ge t}\rho^{i-t}d_i)^+$.
2. Proposition 1 (p. 9) with (A.1). The debt-free rule is to sell everything once $P_t \ge R^o_t$; moreover $U_t(x,p) = \max\{p, R^o_t\}x$ and $R^o_t = \rho E_t\max\{P_{t+1}, R^o_{t+1}\}$.
3. (A.6). The closed form of $V_m$.
4. Lemma 3 (p. 13). Convexity, linearity and continuity of $V_t$ in $(x, w, d_m)$.
5. (A.8). $V_t$ is a three-term maximum.
6. (A.9). Its specialization at $x = 1$, $w = 0$.
7. Footnote 4. $0 \le C_t < R^o_t$.

Significance

Proposition 4 is the paper's headline. Under debt, the first sale follows a control band. Below $R^{(1)}_t$ the seller waits. Between the two critical prices, the seller sells exactly the quantity whose revenue covers the discounted debt; in that band a higher price means a smaller sale. Above $R^{(2)}_t$ the seller sells everything. Part (ii) separates the two economic forces by the sign of one number, $E_t\Delta_{t+1}$. When the bankruptcy cost dominates, part of the asset is sold earlier than without debt. When limited liability dominates, selling is delayed and done all at once. The same structure underlies the paper's later results on threshold debt levels and general installment schedules.

The result is proved on paper but has not been formalized; the platform has no asset-selling, reservation-price or debt-constrained selling model. The mission contributes three things. The first is a finite-horizon Markov-price dynamic program with an explicit bankruptcy branch and limited liability, built on Mathlib's probability kernels. The second is Karlin-type debt-free stopping results for a divisible asset. The third is the full convexity argument behind the control band.

Difficulty

Part (ii) is signed algebra once footnote 4 is known; the work is in part (i). Because of the bankruptcy branch, $V_t$ is neither convex nor concave in general (Lemma 1(iii)). So the first-order reasoning that settles the debt-free problem, a linear objective in $q$, does not carry over. Two facts reduce the optimum to three candidate quantities. The first is convexity of $V_t$ in $(x, w, d_m)$ below the debt-covering region, proved by backward induction together with the debt level. The second is linearity above that region. The induction must carry the debt level as a variable.

Every value function is integrated against a kernel. Before any identity between expectations can be used, $p' \mapsto U_{t+1}(x,p')$ and $p' \mapsto V_{t+1}(x,w,p')$ must be shown measurable and integrable, and both are suprema over a continuum of quantities. The strict inequality of footnote 4 is a separate induction: $V_{t+1}(1,0,\cdot) < U_{t+1}(1,\cdot)$ at every positive price.

Formalization scope

Everything lives in the namespace AssetDebt.ControlBand.

Representation.

• Periods are natural numbers and values are real numbers.
• κ t p is the law of $P_{t+1}$ given $P_t = p$, a Mathlib Kernel ℝ ℝ.
• $U$ and $V$ are defined by well-founded recursion as suprema of the objective over the feasible set. For $V$, the bankruptcy test comes first, so the supremum is only taken over a nonempty interval.
• $V_t := 0$ for $t > m$, which is the paper's convention $V_{m+1} := 0$.
• Feasibility is written $0 \le q \le \min(x,\ell)$, $d_t \le w + pq$. This avoids dividing by $p$.
• "Optimal" means feasible and attaining the maximum; uniqueness is not claimed.
• The critical prices $R^{(1)}_t, R^{(2)}_t$ are the explicit thresholds (A.10) from the paper's proof, not a free existential.
• $E_t\Delta_{t+1}$ is the integral of $\Delta_{t+1}$ as defined in (5).

Added hypotheses.

• Prices are almost surely strictly positive. The paper writes $P_t \ge 0$ but divides by $p_t$.
• The multi-step conditional means $E[P_s \mid p_t]$, $t < s \le T$, are finite. The paper treats $R^o_t$ as a real number, and the one-step assumption alone does not guarantee that.
• Section 3's standing assumption $\ell = 1$ is a hypothesis of every statement except Lemma 1.

Excluded trivializations. $V$ is never defined by its closed forms (A.6), (A.8) or (A.9), which would make the goal an unfolding exercise. The critical prices are not existentially quantified: a price-dependent existential could be witnessed by thresholds read off the optimal action itself.

Infrastructure. A complete development needs measurability of suprema of kernel integrals, sup-shift lemmas for bounded intervals, and the backward-induction convexity argument. The debt-free results (Proposition 1) and the sup and measurability lemmas apply to other finite-horizon selling and stopping models. Contributions are welcome on any milestone, in particular on the measurability layer.

Selected references

• H.-S. Ahn, D. D. Wang, O. Q. Wu, Asset Selling Under Debt Obligations, SSRN 3472345, version of May 7, 2019. https://ssrn.com/abstract=3472345 ; published in Operations Research 69(4), 2021. https://doi.org/10.1287/opre.2019.1961
• S. Karlin, Stochastic models and optimal policy for selling an asset, in K. J. Arrow, S. Karlin, H. Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 1962, pp. 148–158 (cited as in the paper’s reference list).
• O. Besbes, D. A. Iancu, N. Trichakis, Dynamic pricing under debt: spiraling distortions and efficiency losses, Management Science 64(10), 2018, pp. 4572–4589 (cited as in the paper's reference list).

Motivation

A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.

Setting

There is one buyer in tier 0 and two possible tier-1 firms, $a$ and $b$. The tier-2 suppliers are divided into three disjoint sets: $S_a$, whose members supply only $a$; $S_b$, whose members supply only $b$; and $S_{ab}$, whose members supply both. A network is $g=(S^{(1)},S_a,S_b,S_{ab})$, where $S^{(1)}\subseteq\{a,b\}$ is the set of tier-1 firms still present. Its supplier set $S_g$ contains those tier-1 firms and the members of the three tier-2 sets. The set $D_g(i)$ of dependents of supplier $i$ includes $i$ itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.

An auditing state $\gamma=(g,U_\gamma)$ records the current network and its finite set of unaudited suppliers, $U_\gamma\subseteq S_g$. The state is terminal when $U_\gamma=\varnothing$. The operator $\gamma\oplus i$ vets an unaudited supplier without changing the network. The operator $\gamma\ominus i$ drops $i$ and $D_g(i)$. If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.

At a state, the buyer can proceed to production ($pp$), audit and rectify an unaudited supplier ($ar(i)$), or audit and drop one if it fails ($ad(i)$). An auditing policy $\xi$ chooses an admissible action at every state. Let $a\geq0$ be the audit cost, $r\geq0$ the rectification cost, $u\in(0,1)$ the chance that a supplier is noncompliant, $w\in(0,1]$ the chance that an uncorrected violation is exposed, and $z\geq0$ the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit $\pi(g)$ less the expected penalty $\zeta(\gamma)=|U_\gamma|uwz$.

The optimal value $V^*(\gamma)$ is the maximum of the values of the admissible actions at $\gamma$, using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value $V(\xi,\gamma)$ of a fixed policy and the restricted value $V_{ar}(\gamma)$ when only $pp$ and $ar$ are available.

Formalization targets

The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison

$$a+ur\leq uwz\quad\text{(rectify all)},\qquad a+ur\geq uwz\quad\text{(proceed to production)}.$$

The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.

Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With $c_{rp}=\min\{uwz,a+ur\}$, its value formula is

$$V_{ar}(\gamma)=\pi(g)-c_{rp}|U_\gamma|.$$

Significance

Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.

The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.

Difficulty

An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever $a+ur\leq uwz$ ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.

Formalization scope

Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require $a,r,z\geq0$, $0<u<1$, and $0<w\leq1$. The paper derives $\zeta$ from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit $\pi$ is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.

The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.

Selected references

• H. Zhang, G. Aydin, and R. P. Parker, Social Responsibility Auditing in Supply Chain Networks, Management Science, 2021, authors' accepted manuscript dated 26 February 2021, pp. 8–11, 19, OA-11–OA-13. DOI: 10.1287/mnsc.2020.3950.

Motivation

Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).

The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.

Setting

Time is discrete and counted backward: $t$ is the number of periods to go and period $1$ is the last. Each order must be delivered at most $d \ge 1$ periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack $1$ means the order must leave now.

Shipping a package that must arrive within $p$ periods costs $F(p)$, the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes $F$ is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on $[1,\infty)$. In each period new orders arrive with probability $\alpha \in [0,1]$.

With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack $z$ among pending orders. The state is therefore $z \in \{1,\dots,d\}$, or $\infty$ when nothing is pending. The cost-to-go functions $V_t(z)$ and $V_t(\infty)$ satisfy the recursion (2)–(3): for $t > 1$ and $1 \le z \le d$,

$$V_t(z) = \min\{\,F(z) + V_t(\infty)\ \text{(ship)},\ \ V_{t-1}(z-1)\ \text{(do not ship)}\,\},$$ $$V_t(\infty) = \alpha V_{t-1}(d) + (1-\alpha) V_{t-1}(\infty),$$

with $V_1(z) = F(z)$ and $V_1(\infty) = 0$. Holding is infeasible at $z = 1$. Shipping is optimal at $(t,z)$ when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.

Formalization targets

Goal: Theorem 1 (p. 13)

For every period $t \ge 1$ there is an integer $\tau_t$ such that, for every slack $1 \le z \le d$,

$$z \le \tau_t \implies \text{shipping all pending orders is optimal}, \qquad z > \tau_t \implies \text{holding all pending orders is optimal}.$$

The threshold may depend on $t$, and no formula for it is asserted.

Milestones

1. Lemma E1 (Online Appendix, p. 1). For reals $a_1,\dots,a_n$ and $b_1 \ge \dots \ge b_n$,

$$\min_i (a_i + b_i) - \min_i a_i \ \ge\ b_n.$$

2. Unrolled cost-to-go (proof of Lemma 2, Online Appendix, p. 1). For $t \ge 1$ and $1 \le z \le d$,

$$V_t(z) = \min_{0 \le j \le k} \{F(z-j) + V_{t-j}(\infty)\}, \qquad k = \min\{t,z\} - 1.$$

3. Lemma 2 (p. 13). For $t \ge 1$ and $2 \le z \le d$,

$$V_t(z-1) - V_t(z) \ \ge\ F(z-1) - F(z).$$

4. The downward step (proof of Theorem 1, p. 13). For $t \ge 2$ and $3 \le z \le d$, if shipping is optimal at slack $z$, it is optimal at slack $z-1$.

Significance

Theorem 1 reduces the policy of a $T$-period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.

The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for $t \ge d$, and the case $t < d$ is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to argue that the cost-to-go $V_t(z)$ inherits convexity in $z$ from $F$ and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of $V_t$ and the slope of $F$ (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference $V_t(z-1) - V_t(z)$ can a priori be larger or smaller than $F(z-1) - F(z)$, because the optimal shipping periods for slacks $z-1$ and $z$ may differ. The recursion couples two indices, period and slack, through the no-order value $V_t(\infty)$, and its boundary cases ($z = 1$, where shipping is forced, and $t = 1$, the last period) behave differently from the interior. The paper's own argument covers only $t \ge d$; the regime $t < d$, in which the horizon ends before the most urgent order's deadline, is left to the reader.

Formalization scope

• Model. The model is the reduced recursion (2)–(3) itself, encoded as a recursive definition valuePair F α d t returning $(z \mapsto V_t(z), V_t(\infty))$. The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; $z$ stands for the smallest slack among pending orders. All objects are deterministic; $\alpha$ enters only through (3).
• Conventions. Periods are counted down, $t \ge 1$. $V_1(\infty) = 0$ (from (1): nothing pending costs nothing in the last period). The boundary condition $V_{t-1}(0) = \infty$ is encoded as a forced shipment at $z = 1$. Every statement is restricted to $1 \le z \le d$, the domain of (2); values outside it, and at $t = 0$, are placeholders. $F : \mathbb R \to \mathbb R$ is real-valued, assumed convex and non-increasing on $[1,\infty)$, and evaluated only at integers $z \ge 1$; the paper's $F(0) = \infty$ is never read and is not encoded.
• Optimality. A decision is optimal when its branch of (2) attains the minimum; ties make both decisions optimal. Holding is optimal only if it is feasible ($t \ge 2$, $z \ge 2$).
• Ruling out a trivial goal. Shipping is always optimal at $z = 1$, so "there is a threshold below which shipping is optimal" holds with $\tau = 1$ for free; the goal also requires holding to be optimal at every slack above the threshold.
• Not formalized. Lemma 1, Proposition 1, Theorem 2 and the results that rest on it (Proposition 2, Lemma 3), the two-warehouse results of §5, the variable-cost model of §6, and the heuristic bounds of §7.
• Infrastructure. Only Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.

Selected references

• L. Wei, R. Kapuscinski, S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2020.0903 — author's manuscript: https://ssrn.com/abstract=2920899

Motivation

An online allocator must commit to an action after each arrival, although later arrivals can change which actions would have been best. Revenue management and online resource allocation use regret to measure the expected reward lost against a benchmark. If the benchmark sees too much future information, this gap can grow with the horizon even when the online controller behaves optimally. Vera, Banerjee, and Gurvich use a benchmark whose extra information can be chosen for the application, and relate regret to two quantities that can be studied separately: how often the online action disagrees with an informed action, and how accurately a proposed value function satisfies a Bellman equation (Vera–Banerjee–Gurvich, 2020, §§2–3).

The paper proves constant-regret application results for online probing, dynamic pricing, and learning by combining this framework with estimates particular to each model. This mission isolates the framework's Theorem 5 and the displayed statements leading to it. Its result is known on paper; the work here is to give the model, the conditional expectations, and the regret bound machine-checkable statements.

Setting

There are $T$ decision periods, indexed by time to go $t=T,T-1,\ldots,1$. At the start of period $t$ the controller is in state $S^t\in\mathcal S$ and observes an input $\xi^t\in\Xi$. It selects an action $u$ from a nonempty feasible set $\mathcal U(S^t,\xi^t)$, collects real reward $R(S^t,\xi^t,u)$, and moves to $S^{t-1}=\mathcal T(S^t,\xi^t,u)$. The initial state is the fixed state $S^T=s_0$.

The observed filtration $\mathcal F_t$ is generated by the arrivals $\xi^t,\ldots,\xi^T$. A non-anticipative policy chooses an $\mathcal F_t$-measurable action from the current state. Offline has the augmented filtration $\mathcal G_t=\mathcal F_t\vee\mathcal H$, where $\mathcal H$ is a fixed sigma-algebra carrying extra information. Offline's value $V(t,s)$ is the feasible-action maximum in the conditional Bellman equation (2), with $V(0,s)=0$. Its expected initial value is the benchmark for the online policy's expected reward. Regret is their difference.

A relaxed value $\phi(t,s)$ and a Bellman loss $L_B(t,s)$ obey the Bellman inequalities if $\phi$ initially bounds the conditional Offline value, ends at zero, and at each state is at most one feasible action's immediate reward plus its expected relaxed continuation and $L_B$. An action meeting this inequality is satisfying. A maximum-loss bound $r$ controls the shortfall of every feasible action. For a policy with action $\widehat U^t$ on its actual trajectory, $Q_t$ is the event that $\widehat U^t$ is not satisfying under this same $\phi$ and $L_B$.

Formalization targets

Satisfying actions under augmented information

Proposition 1 concerns a feasible $\mathcal G_t$-adapted policy that always takes satisfying actions. It bounds its shortfall from Offline by the expected accumulated Bellman loss:

$$\mathbb E[V(T,s_0)]-\mathbb E\!\left[\sum_{t=1}^T R(S^t,\xi^t,U^t)\right]\le\mathbb E\!\left[\sum_{t=1}^T L_B(t,S^t)\right].$$

The proposal also states the one-step displayed inequality from its proof, where a conditional continuation at a fixed state and action becomes the conditional continuation of the policy's random trajectory.

Regret decomposition

Theorem 5 concerns a feasible non-anticipative policy. It states the pathwise-compensation expectation bound and, when $L_B$ is nonnegative, the paper's two-term bound:

$$\mathbb E[\mathrm{Regret}]\le\mathbb E\!\left[\sum_{t=1}^T\left(r\mathbf1_{Q_t}+\mathbf1_{Q_t^c}L_B(t,S^t)\right)\right]\le\sum_{t=1}^T\left(r\,\mathbb P(Q_t)+\mathbb E[L_B(t,S^t)]\right).$$

The milestones include the paper's maximum-loss, compensated one-step, and iterated displays on the route to this target. The first inequality is also stated for signed $L_B$; only the second requires $L_B\ge0$.

Significance

The theorem turns a regret analysis into two concrete estimates. An application can count or bound the periods when the online action fails the informed satisfying-action test, and can separately quantify the error in its chosen relaxed value. Neither quantity alone certifies small regret; the theorem supplies the inequality connecting both to the benchmark's actual reward gap. The paper's constant-regret claims use application-specific bounds on these terms (Vera–Banerjee–Gurvich, 2020, §§4–6).

A complete formalization would establish the conditional-expectation and measurability infrastructure needed to apply this template to other finite-horizon allocation models. The paper gives a proof of Theorem 5, but the theorem and its applications have no machine-checked proofs in this mission. The proposal records the open Lean statements and a statement-only non-vacuity check for the exact Bellman value with zero loss.

Difficulty

Definition 5 describes a satisfying action for a fixed state and action, while Theorem 5 evaluates it at a random state and a policy's random action. The conditional expectation in that definition cannot simply be substituted syntactically for the conditional expectation of the ensuing trajectory. Countable states and finite actions make the substitution meaningful, but measurability of the selected state and action still has to be established. The same issue appears in the maximum-loss display. Time runs backward, so the information at $t-1$ contains the information at $t$; a forward-indexed filtration would change the conditional expectation in the paper's formulas.

The second displayed inequality presents a separate statement issue: removing $\mathbf1_{Q_t^c}$ from $L_B$ is valid only for nonnegative $L_B$. The paper allows signed Bellman losses elsewhere, so nonnegativity is attached to that inequality rather than to the definition of Bellman inequalities.

Formalization scope

The Lean model uses a countable state type, a finite nonempty action type, real rewards, and an explicit nonempty feasible-action set. The probability space carries a probability measure, measurable arrivals, and an auxiliary sub-sigma-algebra $\mathcal H$. The observed and augmented information families are plain sigma-algebra families because their order decreases with time to go. The index $t=0$ is terminal; decision sums and hypotheses use exactly $t\in\{1,\ldots,T\}$. Offline's value is defined by the feasible-action Bellman recursion and is never a free benchmark variable.

The source bounds the maximum reward above. This formalization additionally bounds feasible rewards, $\phi$, and $L_B$ in absolute value over the finite horizon, and requires measurable reward, transition, and feasibility data. These assumptions ensure the real integrals and conditional expectations have their intended values. Definition 4 is an almost-sure real upper bound $r$ rather than a supremum that could take a default value. The feasible-action maximum in the Bellman inequality is represented by a feasible witness. The source's family $G_\Theta$ is represented by the single sigma-algebra it generates, $\mathcal H$.

The goal covers every feasible $\mathcal F_t$-adapted state-feedback policy; RABBI is in this class. Proposition 1 retains its distinct $\mathcal G_t$-adapted policy class. The disagreement event uses the same $L_B$ as the Bellman inequalities. The maximum-loss display follows Definition 4's parentheses and sign, correcting a printed slip on p. 14. The nonnegative-loss condition corrects the second inequality of the printed Theorem 5. A complete development needs reusable lemmas on finite feasible maxima, measurable state-feedback trajectories, conditional expectations under decreasing information, and integration of finite sums. Contributions to those lemmas and to the five stated milestones are in scope.

Selected references

• Alberto Vera, Siddhartha Banerjee, and Itai Gurvich, Online Allocation and Pricing: Constant Regret via Bellman Inequalities, arXiv preprint arXiv:1906.06361v2, 2020. arXiv.

Motivation

Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time $w$ (the work already in the queue) and a price rate $p$ per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.

The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at $w$ depends on the value at $w + \mathtt t(p) > w$. This mission formalizes the paper's existence theorem for that equation.

Setting

A model has a usage utility $U$, a waiting cost $c$, a Poisson arrival rate $\lambda > 0$ and a maximum service time $C > 0$, under Assumption 1 (p. 7):

1. $U(t) \ge 0$, $U(0) = 0$, $0 \le U'(t) \le U'(0)$ and $U''(t) < 0$ on $[0, C]$;
2. $\frac{d^2}{dt^2}[U'(t)t] < 0$ on $[0, C]$;
3. $c(0) = 0$, $c'(w) > 0$ and $c''(w) \ge 0$ for $w \ge 0$.

At price $p \in [0, U'(0)]$ a joining customer chooses the service time $\mathtt t(p) = \min\{(U')^{-1}(p), C\}$ (5). They join when $U(\mathtt t(p)) - p\,\mathtt t(p) - c(w) \ge 0$. Three thresholds follow:

• $\bar w$ solves $U(C) = c(\bar w)$; above it nobody joins.
• $\Gamma(w)$, for $w \in [0, \bar w]$, is the highest price at which a customer still joins (Proposition 2).
• $\hat w$ and $L(w)$ (Proposition 1) describe when the marginal price $U'(t)$ still attracts a customer.

The per-customer value is $\mathbf v(p) - \alpha c(w)$, with $\mathbf v(p) = p\,\mathtt t(p)$, $\alpha = 0$ for revenue and $\mathbf v(p) = U(\mathtt t(p))$, $\alpha = 1$ for welfare (Lemma 1).

The optimality equations (12)–(15) ask for a constant $\mathsf g$ (the average rate) and a relative value function $V$ with

$$\mathsf g = -V'(w) + \lambda \max\Big\{\max_{p \in [0, \Gamma(w)]} \big[\mathbf v(p) - \alpha c(w) + V(w + \mathtt t(p)) - V(w)\big],\ 0\Big\}, \quad w \in (0, \bar w],$$ $$\mathsf g = \lambda \max\Big\{\max_{p \in [0, \Gamma(0)]} \big[\mathbf v(p) + V(\mathtt t(p)) - V(0)\big],\ 0\Big\}, \qquad \mathsf g = -V'(w) \ (w > \bar w), \qquad V(\bar w) = 0.$$

Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess $g \ge 0$ and $N$ grid cells on $[0, \bar w]$, it starts from $V^g_N(w) = -(w - \bar w)g$ for $w \ge \bar w$. It then builds a piecewise-linear $V^g_N$ cell by cell from right to left. On the cell ending at $x$ the slope is $-g + K^g_N(x)$, where the slope adjustment $K^g_N(x)$ is $\lambda$ times the positive part of the inner maximum at $x$. The shooting value is $g_N = \min\{g \ge 0 : g \ge K^g_N(0)\}$ (23). Finally $\bar g = \lim_j g_{2^j}$ (24) and $V^{\bar g}(w) = \lim_j V^{\bar g}_{2^j}(w)$ (Proposition 6).

Formalization targets

Goal: Theorem 1 (p. 17)

$$\bar g = \lim_{j\to\infty} g_{2^j} \ \text{exists},\quad V^{\bar g}_{2^j}(w) \to V^{\bar g}(w)\ (w \ge 0),\quad (\bar g, V^{\bar g}) \text{ solves (12)–(15)},\quad V^{\bar g} \text{ is nonincreasing and concave on } [0, \bar w + C].$$

Milestones

The milestones follow the paper's proof in order:

• Thresholds and the value function (Propositions 1–3, pp. 8–11): uniqueness of $\hat w$ and $\bar w$, the characterization (8) of $\Gamma$, $\Gamma(0) = U'(0)$ with $\Gamma$ decreasing, and the bounds (V1)–(V2) on $\mathbf v$.
• The finite-$N$ scheme (Proposition 4, Lemmas 2, 3, 5): $V^g_N$ is concave and $K^g_N$ is nonincreasing; $K$ increases when the grid is refined and decreases in $g$; and $K^{U'(0)}_N \equiv 0$.
• The limits (Proposition 5, Lemma 6, Proposition 6): $g_{2^j}$ increases to $\bar g \le U'(0)$, the $V^{\bar g}_{2^j}$ are uniformly $\bar g$-Lipschitz, and they converge uniformly to a concave, nonincreasing, Lipschitz $V^{\bar g}$.
• The equations in the limit (Lemma 7, Propositions 7–8): $K^{\bar g}_{2^j}(0) \to \bar g$; the boundary condition (13); differentiability of $V^{\bar g}$ on $[0, \bar w]$ and the DDE (12).

Significance

Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed $\bar g$ equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off $V^{\bar g}$. Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.

The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.

Difficulty

The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. $V'(w)$ depends on $V$ on $[w, w + C]$, so the equation must be integrated backwards from $\bar w$, and then the value $\mathsf g$ is unknown. The shooting scheme fixes $g$, integrates backwards, and tunes $g$ so that the boundary condition (13) at $w = 0$ holds in the limit. For fixed $g$ the approximations need not converge as $N \to \infty$ (the slope at $0$ can diverge), so $g$ and $N$ must be coupled through $g_N$.

The hard step is Proposition 8. Each $V^{\bar g}_{2^j}$ has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a $w$-dependent price set to the limit.

Formalization scope

All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:

• $U, c : \mathbb R \to \mathbb R$ are $C^3$ and $C^2$ on $\mathbb R$, a disclosed strengthening of "three/two times differentiable". Assumption 1's inequalities are imposed exactly on $[0, C]$ and $[0, \infty)$. $\lambda > 0$ and $C > 0$ are added; the paper uses them without stating them.
• $\mathtt t(p) = \sup\{t \in [0, C] : p \le U'(t)\}$, meaningful for $p \in [0, U'(0)]$. $\hat w$, $L(w)$, $\bar w$ and $\Gamma(w)$ are defined by their characterizing sets, not by closed forms. Propositions 1–2 are theorems about these sets.
• The objective is one of Lemma 1's two cases. The paper's remark that any $\mathbf v$ satisfying (V1)–(V2) would do is not formalized, because it silently needs continuity of $\mathbf v$.
• Every "max" in (12), (13), (19) and (22) is a real supremum over $[0, \Gamma(w)]$. For the continuous $V$ used here this set is nonempty and bounded, and the supremum is attained.
• $V'$ is never a default-valued derivative. (12) and (14) assert that $V$ has the prescribed derivative, two-sided for $w \in (0, \bar w]$ and $w > \bar w$; Proposition 8 states the case $w = 0$ with a right derivative.
• Algorithm 1 is a recursion over the passes of its loop, with $N \ge 1$. The initialization (16) is extended from $[\bar w, \bar w + C]$ to $[\bar w, \infty)$ so that (14) can hold as printed on $(\bar w, \infty)$. Only values on $[0, \bar w + C]$ enter the loop, so the construction is unchanged.
• $\bar g$ and $V^{\bar g}$ are defined as limits that take a default value when the limit does not exist. Propositions 5–6 and the goal assert the convergence.
• "Decreasing" is nonincreasing everywhere (including $\Gamma$, Proposition 2(iii)), the reading the proofs establish.

Trivializations ruled out. The goal names the paper's $\bar g$ and $V^{\bar g}$ together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. $\Gamma$ and $\mathtt t$ are not closed forms that would make (8) true by definition. The weaker statement "some $(\mathsf g, V)$ solves (12)–(15)" is not the goal.

Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when $\bar g > U'(C)$.

Selected references

• C.-A. Lin, K. Shang, P. Sun, Wait Time Based Pricing for Queues with Customer-Chosen Service Times, SSRN 3709573, version of October 12, 2020. https://ssrn.com/abstract=3709573 (journal version: Management Science, https://doi.org/10.1287/mnsc.2022.4474)
• D. W. Low, Optimal dynamic pricing policies for an M/M/s queue, Operations Research 22(3), 1974. https://doi.org/10.1287/opre.22.3.545
• I. C. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842140
• J. Kim, R. S. Randhawa, The value of dynamic pricing in large queueing systems, Operations Research 66(2), 2018. https://doi.org/10.1287/opre.2017.1668
• D. P. Bertsekas, Dynamic Programming and Optimal Control, 2nd ed., Athena Scientific, 2000. http://www.athenasc.com/dpbook.html

Motivation

Value iteration (VI) is the standard method for computing the optimal value function of a discounted Markov decision process (MDP). It applies the Bellman operator repeatedly, and because that operator is a $\lambda$-contraction in the sup norm, the error after $s$ steps is at most $\lambda^s$ times the initial error. When the discount factor $\lambda$ is close to $1$, as in long-horizon planning, this rate is slow.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read value iteration as a gradient-type method and transfer momentum schemes from convex optimization (Nesterov acceleration, heavy-ball momentum) to the Bellman operator. On reversible policy chains these accelerated schemes provably converge faster than VI. On general MDPs, however, the accelerated iterates need not converge at all: the paper exhibits instances on which Accelerated Value Iteration (A-VI) oscillates or diverges. Section 7 of the paper resolves this tension with Safe Accelerated Value Iteration (S-AVI, Algorithm 1), which tries an accelerated step at every period and keeps it only when it makes enough progress on the Bellman equation $v = T(v)$. This mission formalizes the convergence guarantee of S-AVI, Theorem 7.1.

Setting

Let $\mathbb S$ be a finite set of states and $\mathbb A$ a nonempty finite set of actions. A discounted MDP is given by a transition kernel $P$, with $P_{iaj}\ge 0$ the probability of moving from state $i$ to state $j$ under action $a$ and $\sum_j P_{iaj} = 1$; a reward $r_{ia}\in\mathbb R$ for each state-action pair; and a discount factor $\lambda \in (0,1)$. The Bellman operator $T : \mathbb R^{\mathbb S} \to \mathbb R^{\mathbb S}$ is

$$T(v)_i = \max_{a\in\mathbb A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj}\, v_j \Big\}.$$

The sup norm is $\|v\|_\infty = \max_i |v_i|$. The optimal value function $v^*$ is the unique fixed point of $T$. For a vector $v$, the quantity $\|v - T(v)\|_\infty$ is its Bellman residual.

S-AVI (Algorithm 1) takes a scalar $\lambda' \in [\lambda, 1)$, step sizes $\alpha, \gamma > 0$ and any starting vector $v_0$. It sets $v_1 = T(v_0)$, and at each period $s \ge 1$ forms

$$h_s = v_s + \gamma\,(v_s - v_{s-1}), \qquad v_{s+1/2} = h_s - \alpha\,\big(h_s - T(h_s)\big).$$

If $\|v_{s+1/2} - T(v_{s+1/2})\|_\infty \le \lambda'^{\,s+1}\,\|v_0 - T(v_0)\|_\infty$, the accelerated candidate is accepted, $v_{s+1} = v_{s+1/2}$; otherwise the algorithm takes a value-iteration step, $v_{s+1} = T(v_s)$. In the Lean development the MDP is AccelVI.SafeAVI.MDP with validity predicate MDP.Valid, the operator is bellman M, and the iterates are savi M lam' α γ v0 : ℕ → (S → ℝ).

Formalization targets

Goal: Theorem 7.1

For a valid MDP, any $\lambda' \in [\lambda, 1)$, any $\alpha, \gamma > 0$ and any $v_0$, the S-AVI iterates converge to $v^*$, and

$$v_s = v^* + O(\lambda'^{\,s}), \quad \forall s \ge 0,$$

that is, there is a constant $C$ with $\|v_s - v^*\|_\infty \le C\,\lambda'^{\,s}$ for every $s \ge 0$. The constant is left unspecified, as in the paper.

Milestones

1. $T$ is a $\lambda$-contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
2. The first period: $\|v_1 - T(v_1)\|_\infty \le \lambda\|v_0 - T(v_0)\|_\infty \le \lambda'\|v_0 - T(v_0)\|_\infty$ (p. 13).
3. Geometric decay of the residual: $\|v_s - T(v_s)\|_\infty \le \lambda'^{\,s}\|v_0 - T(v_0)\|_\infty$ for all $s$ (p. 14).
4. The residual controls the error: $\|v - v^*\|_\infty \le (1-\lambda)^{-1}\|v - T(v)\|_\infty$ for every $v$ (p. 14).

Significance

The result. Theorem 7.1 says that the safeguard costs nothing in the worst case: S-AVI converges on every MDP at rate $\lambda'$, and with $\lambda' = \lambda$ it matches the rate of value iteration, which Theorem 6.3 of the same paper shows cannot be beaten by any first-order method uniformly over MDPs. At the same time it accepts accelerated steps whenever they reduce the residual fast enough, so it keeps the empirical speed-ups of A-VI. Remark 7.2 of the paper describes the role of $\lambda'$: values closer to $1$ admit more accelerated steps. The guarantee also gives a computable stopping rule, since the residual bounds the distance to $v^*$.

Formalizing it. The result is proved in the paper; to our knowledge it has not been machine-checked. This mission produces a Lean statement of the finite discounted MDP layer, the Bellman operator and Algorithm 1 itself (including its two-step recursion and its data-dependent branch), and a formal proof that the safeguarded iteration converges. The contraction property of $T$ and the residual-to-error bound are reusable for any later value-iteration development on the platform. Three sibling missions of this series pose the paper's other main results: the rate of Accelerated Value Computation on reversible chains (Theorem 5.1), the rate of Momentum Value Computation (Theorem 5.5), and the first-order lower bound (Theorem 6.3).

Difficulty

The accelerated candidate $v_{s+1/2}$ is built from two past iterates through a momentum step, and on a general MDP nothing controls it: A-VI is not a descent method, and its iterates may diverge. The natural first attempt, proving that A-VI steps contract the error, therefore fails. The difficulty in the formal setting lies elsewhere: the iterates are defined by a two-step recursion with a branch on a real inequality, so any argument must handle both branches at every period and keep the paper's indexing straight (the threshold at period $s$ is $\lambda'^{\,s+1}$ and it compares with the residual of $v_0$, not of $v_s$). Existence and uniqueness of $v^*$ and the contraction property of a max of affine maps also need to be established for the specific operator, from the stochasticity of $P$.

Formalization scope

States and actions are finite types, [Fintype S], [Fintype A], and [Nonempty A] so that the maximum in $T$ exists. Vectors are functions S → ℝ with Mathlib's sup norm, which is $\|\cdot\|_\infty$. Rewards are arbitrary reals. The discount factor is M.lam with $0 < \lambda < 1$ inside MDP.Valid; the initial distribution $p_0$ of the paper's tuple is omitted because no statement uses it. The optimal value function enters each statement as a vector vstar with bellman M vstar = vstar; this is not vacuous, since a valid MDP has exactly one such vector. The scalar $\lambda'$ ranges over the closed interval $[\lambda, 1)$, and $\alpha, \gamma > 0$ as in Algorithm 1, although the convergence argument does not need the step sizes to be positive. The sequence savi is indexed as the paper's $v_s$: its recursive case s + 2 is the paper's period $s+1$, with threshold lam' ^ (s + 2). "$v_s = v^* + O(\lambda'^s)$ for all $s \ge 0$" is encoded as a single constant valid for every $s$, which is stronger than an eventual big-O.

A formalization that replaced the test by the per-step condition (7.2) of Remark 7.3, used the residual of $v_s$ instead of $v_0$, fell back to $T(v_{s+1/2})$, or allowed $\lambda \ge 1$ would be a different theorem; none of these is posed. Remark 7.4's extension to arbitrary contractions is not posed either.

The development needs the contraction property of $T$, the Banach fixed-point bound relating error and residual, and an induction over the iterates. Proofs of the milestones as separate lemmas are welcome, as are general statements about safeguarded fixed-point iterations for $\lambda$-contractions that specialize to this one.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, reprinted 2014 (Chapter 6.3, value iteration). https://doi.org/10.1002/9780470316887
• Y. Nesterov, A method for solving the convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27, 1983.

Motivation

Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor $\lambda$ per step, so it needs on the order of $(1-\lambda)^{-1}\log(1/\epsilon)$ iterations, which is slow when $\lambda$ is close to $1$, the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map $v \mapsto v - T(v)$ and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate $\lambda$ of plain VI on every MDP? Theorem 6.3 of the paper answers no.

Setting

A finite MDP consists of a state set $S$ with $|S| = n$, a finite nonempty action set $A$, transition probabilities $P_{iaj} \ge 0$ with $\sum_j P_{iaj} = 1$, rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. Its Bellman operator $T : \mathbb{R}^n \to \mathbb{R}^n$ is

$$T(v)_i = \max_{a \in A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj} v_j \Big\}, \qquad i \in S,$$

a $\lambda$-contraction for the sup norm $\|\cdot\|_\infty$. Its unique fixed point $v^*$ is the optimal value function.

A sequence $(v_s)_{s \ge 0}$ in $\mathbb{R}^n$ is a first-order sequence for $T$ if

$$v_0 = 0, \qquad v_{s+1} \in \operatorname{span}\{v_0, \dots, v_s, T(v_0), \dots, T(v_s)\}, \quad s \ge 0 .$$

VI from $v_0 = 0$ ($v_{s+1} = T(v_s)$) and relaxed VI ($v_{s+1} = v_s - \alpha_s(v_s - T(v_s))$) from $0$ produce such sequences.

The chain MDP of Figure 1 has $n$ states and a single action. State $1$ is absorbing with reward $r_1 = 1$; every state $i \ge 2$ moves deterministically to $i - 1$ and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, $T$ is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.

Formalization targets

Goal: Theorem 6.3 (p. 12)

For every $n$, every $\lambda \in (0,1)$, the fixed point $v^*$ of the Bellman operator $T$ of the $n$-state chain, every first-order sequence $(v_s)$ for $T$, and every $s \in \{1, \dots, n-1\}$,

$$\|v_s - v^*\|_\infty \ge \frac{\lambda^s}{1+\lambda}.$$

Milestones

1. $T$ is a $\lambda$-contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
2. (3.5): $(1-\lambda)\|v - w\|_\infty \le \|(I-T)(v) - (I-T)(w)\|_\infty$ (p. 6).
3. (3.6): $\|(I-T)(v) - (I-T)(w)\|_\infty \le (1+\lambda)\|v - w\|_\infty$ (p. 6).
4. On the chain, the value function is $v^*_i = \lambda^{i-1}/(1-\lambda)$, and it is the only fixed point of $T$ (p. 12).
5. On the chain, every first-order sequence satisfies $v_{s,i} = 0$ for $i \ge s+1$ (p. 12).
6. (6.2)–(6.4): on the chain, $\|v_s - T(v_s)\|_\infty \ge \lambda^s$ for $1 \le s \le n-1$ (p. 12).

Significance

The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate $\lambda$ of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from $1 - \mu/L$ to $1 - \sqrt{\mu/L}$; with $\mu = 1-\lambda$, $L = 1+\lambda$, the analogue for MDPs would be a rate of about $1 - \sqrt{1-\lambda}$, and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.

Difficulty

The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with $s$ and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index $s$. The support claim has to be carried through the nonlinear max in $T$, which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of $v_s - v^*$ into a bound in sup norm with the exact constant $1/(1+\lambda)$, which requires the two-sided inequalities (3.5)–(3.6) for $I - T$ and the explicit value $v^*_{s+1} = \lambda^s/(1-\lambda)$.

Formalization scope

• States are Fin n and are 0-based: the paper's state $i$ is index $i - 1$, so $v^*_i = \lambda^{i-1}/(1-\lambda)$ is lam ^ k / (1 - lam) at index $k$ and "$i \ge s+1$" is $s \le k$. The action set of the chain is Unit.
• $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index $s$ inclusive.
• $v^*$ enters the goal through its defining equation $T(v^*) = v^*$; it is not replaced by the explicit vector. The initial distribution $p_0$ of the paper's MDP tuple is omitted, since no result here uses it.
• Pinned quantifiers. As printed, Theorem 6.3 asserts that there exists an MDP instance, with $n$ its own number of states; read literally, an instance with $n = 1$ has no admissible $s$. The proof fixes an arbitrary $n$ and $\lambda \in (0,1)$ and uses the chain. The goal states that claim for every $n$ and $\lambda$ on the explicit chain, which implies the printed form.
• $n - 1$ is natural-number subtraction, so the goal has content exactly when $n \ge 2$.
• The goal's constant is $\lambda^s/(1+\lambda)$ as printed; the sharper bound $\lambda^s/(1-\lambda)$, which the proof's chain also gives, is not the target.
• The Bellman operator and the kernel condition are the published platform definitions FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.
• A trivializing formalization would take an unsatisfiable fixed-point hypothesis or an empty first-order class. Both are satisfiable: the explicit vector is a fixed point (milestone 4), and VI from $0$ is first-order.

Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994/2014. https://doi.org/10.1002/9780470316887