Dynamic Programming

Motivation

Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping $H$, so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).

The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?

Setting

The abstract monotone model consists of a state space $S$, a control space $C$, nonempty constraint sets $U(x)\subseteq C$, a terminal function $J_0 : S\to(-\infty,\infty]$, and a mapping $H(x,u,J)\in[-\infty,\infty]$ defined for $x\in S$, $u\in C$ and $J : S\to[-\infty,\infty]$, which is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu : S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors, and it is stationary if all $\mu_k$ are equal. The operators are

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

the cost of a policy is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0)(x)$, $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$, and the optimal cost is $J^*(x)=\inf_\pi J_\pi(x)$. A policy is optimal if $J_\pi=J^*$.

Assumption I (uniform increase) is $J_0(x)\le H(x,u,J_0)$ for all $x$, $u\in U(x)$; under it the sequence defining $J_\pi$ is nondecreasing, so the limit exists in $[-\infty,\infty]$. Assumption I.1 says $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $J_0$, and I.2 says that for some $\alpha>0$, $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ and $J\ge J_0$. Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below $J_0$, and a lower shift bound).

The DP algorithm (value iteration) generates $T(J_0), T^2(J_0),\dots$; for $k\ge0$ and $\lambda\in\mathbb R$ the level sets

$$U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$$

collect the controls that keep the stage-$k$ cost below $\lambda$.

Formalization targets

Goal: Proposition 5.11

Let I, I.1 and I.2 hold, let $C$ be a Hausdorff space, and let $U_k(x,\lambda)$ be compact for all $x\in S$, $\lambda\in\mathbb R$ and $k\ge\bar k$. Then (a) some policy $\pi^*=(\mu_0^*,\mu_1^*,\dots)$ satisfies

$$(T_{\mu_k^*}T^k)(J_0)=T^{k+1}(J_0)\qquad\forall k\ge\bar k;$$

(b) for every such policy, $\{\mu_k^*(x)\}$ has an accumulation point whenever $J^*(x)<\infty$; and (c) any $\mu^*$ that picks such an accumulation point at those states, and any admissible control where $J^*(x)=\infty$, defines an optimal stationary policy:

$$J_{\mu^*}=J^*.$$

Milestones

In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation $J^*=T(J^*)$ under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff $T_{\mu^*}(J^*)=T(J^*)$), Proposition 5.10 (under the compactness hypothesis, $J_\infty=T(J_\infty)=T(J^*)=J^*$ and a stationary optimal policy exists), Proposition 5.6 ($\varepsilon$-optimal policies from approximate attainment, with explicit constants $\sum_k\alpha^k\varepsilon_k=\varepsilon$ and $\varepsilon(1-\alpha)$), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and $\varepsilon$-optimal policies under D, D.2 with finite $S$ and $J^*>-\infty$), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).

Significance

Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.

Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.

Difficulty

The obvious route to (c) is to pass to the limit in $H[x,\mu_k^*(x),T^k(J_0)]=T^{k+1}(J_0)(x)$. That fails twice. First, $\{\mu_k^*(x)\}$ need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, $H$ is not assumed continuous in $u$ at all: the only regularity in $u$ is compactness of the level sets $U_k(x,\lambda)$, and the only regularity in $J$ is I.1 along monotone sequences. States with $J^*(x)=\infty$ need separate treatment, because there the level sets give no control on $\mu_k^*(x)$.

For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of $S$ and $J^*>-\infty$ essentially, and both hypotheses are needed.

Formalization scope

Functions $J$ are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them $J_\pi$ is the limit (limUnder) of the policy compositions, which exists under I or D; $T^k$ is the iterate T^[k]; the composition $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first; the model requires $S$ nonempty and $J_0>-\infty$; "I.2 holds" is the existence of a scalar $\alpha$, and results that name the scalar take it as a parameter. An accumulation point of a sequence in $C$ is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that $\mu^*$ is admissible. $J^*+\varepsilon$ is computed pointwise in $[-\infty,\infty]$ and equals $+\infty$ where $J^*$ does.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$. Mathlib's EReal gives $\top+\bot=\bot$, so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable $W$ (expect, positive and negative parts summed in $[0,\infty]$, $+\infty$ when the positive part diverges) and the sum inside the minimax supremum (badd, $+\infty$ when either summand is $+\infty$), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose $H$ and $J_0$ are these mappings; such models exist because the mappings are monotone.

A formalization in which $J_\pi$ or $J^*$ is introduced as an arbitrary fixed point of $T$, or in which (c) assumes that $\mu^*$ is a limit of $\mu_k^*$, would make the goal trivial or different; both are ruled out by the definitions above.

Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; reprinted Athena Scientific, 1996. Chapter 5, pp. 70–90. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• D. Blackwell, "Positive dynamic programming", Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• R. E. Strauch, "Negative dynamic programming", Ann. Math. Statist. 37 (1966) 871–890. https://doi.org/10.1214/aoms/1177699369

Why accelerate value computation

Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a $\lambda$-contraction, so they converge at the geometric rate $\lambda$, the discount factor. When $\lambda$ is close to $1$, which is the regime of long effective horizons in reinforcement learning ($\lambda = 0.99$ or $0.999$) and in healthcare and operations applications, the number of iterations grows like $1/(1-\lambda)$.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that $v \mapsto v - T(v)$ behaves like the gradient of a function with smoothness constant $1+\lambda$ and strong-convexity constant $1-\lambda$. This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator $T_\pi$ of a fixed policy, they prove that both schemes converge at a rate governed by $\sqrt{\kappa}$ rather than $\kappa$, with $\kappa = (1+\lambda)/(1-\lambda)$, provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.

Setting

A finite MDP has a state set $S$ with $|S| = n$, a finite action set $A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia}$ is a probability vector), rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi = (\pi_{ia})$ is a matrix with nonnegative rows summing to $1$; it induces

$$r_{\pi,i} = \sum_a \pi_{ia} r_{ia}, \qquad L_{\pi,ij} = \sum_a \pi_{ia} P_{iaj}, \qquad T_\pi(v) = r_\pi + \lambda L_\pi v .$$

The value function of $\pi$ is $v^\pi = \sum_{t \ge 0} \lambda^t L_\pi^t r_\pi$, the expected discounted reward from each starting state; it is the unique fixed point of $T_\pi$.

Reversibility (Definition 2.1): the chain with transition matrix $L$ is irreducible, and it has a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i,j$.

Momentum Value Computation (M-VC) starts from arbitrary $v_0, v_1 \in \mathbb{R}^n$ and iterates

$$v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,$$

with the constant step sizes (4.2)

$$\alpha = \frac{2}{1+\sqrt{1-\lambda^2}}, \qquad \beta = \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} .$$

The analysis runs through the $2n \times 2n$ matrix

$$B_\pi = \begin{pmatrix} \lambda(\beta+1)L_\pi & -\beta I \\ I & 0 \end{pmatrix},$$

which propagates the error of the pair $x_s = (v_s, v_{s-1})$, and its spectral radius $\rho(B_\pi)$, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.5

For a valid MDP and a policy $\pi$ whose chain $L_\pi$ is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to $v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\!\left(\left(\frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} + \eta\right)^{s}\right), \qquad 0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda .$$

The goal states the paper's three clauses as printed: convergence, the little-o rate for every $\eta > 0$, and the comparison with $\lambda$.

Milestones

1. The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
2. Lemma B.1: $x_s = x^\pi + B_\pi^{s-1}(x_1 - x^\pi)$ for all $s \ge 1$, with $x^\pi = (v^\pi, v^\pi)$.
3. The eigenvalues of an irreducible, reversible transition matrix are real (§2).
4. (B.1): every eigenvalue $\omega$ of $B_\pi$ satisfies $\omega^2 - \frac{2\lambda\mu}{1+\sqrt{1-\lambda^2}}\omega + \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} = 0$ for an eigenvalue $\mu$ of $L_\pi$.
5. For $\mu \in [-1,1]$, the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$.
6. The identity $\frac{\lambda}{1+\sqrt{1-\lambda^2}} = \frac{\sqrt{1+\lambda}-\sqrt{1-\lambda}}{\sqrt{1+\lambda}+\sqrt{1-\lambda}} = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
7. Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
8. $0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda$ for $\lambda \in (0,1)$.

Significance

The rate $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$ is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number $\kappa$. Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over $\lambda$, so that an $\epsilon$-approximation of $v^\pi$ needs a number of iterations scaling like $1/\sqrt{1-\lambda}$ rather than $1/(1-\lambda)$. The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in $[-1,1]$.

The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of $B_\pi$, and the passage from spectral radius to a little-o rate.

Difficulty

The obvious argument bounds $\|B_\pi\|$ in some norm and iterates. No such bound by the rate holds in general: $B_\pi$ is not normal, and for eigenvalues $\mu = \pm 1$ of $L_\pi$ the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between $\rho(B_\pi)$ and $\|B_\pi^s\|^{1/s}$ is exactly what the $+\eta$ absorbs. Computing $\rho(B_\pi)$ needs two separate facts: the eigenvalues of $B_\pi$ are tied to those of $L_\pi$ through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of $L_\pi$ are real and lie in $[-1,1]$, which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real $\mu$ the modulus computation fails, which is why the hypothesis cannot be dropped.

Formalization scope

States and actions are finite types. The MDP data $(P, r, \lambda)$ is a plain structure, with validity (stochastic $P_{ia}$, $0 < \lambda < 1$) a separate hypothesis; the paper's initial distribution $p_0$ plays no role and is omitted. The value function is the Neumann series $\sum_t \lambda^t L_\pi^t r_\pi$. The norm on $\mathbb{R}^n$ is the sup norm, and $o(\cdot)$ is with respect to it as $s \to \infty$. Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of $B_\pi$ are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by $\nu = 0$ and is not used.

Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with $x_0 - x^\pi$, but $x_0 = (v_0, v_{-1})$ is undefined; the statement uses $x_1 = (v_1, v_0)$. Lemma B.2 prints $\rho(B_\pi) = (1-\sqrt\kappa)/(1+\sqrt\kappa)$, a negative number; its proof computes $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$, the rate of Theorem 5.5, which is stated. On p. 22 the constant $\lambda/(1+\sqrt{1-\lambda^2})$ is printed as $\lambda/(1+\sqrt{1-\lambda})^2$. The second step size, printed $\gamma$ in (4.2), is the $\beta$ of (M-VC) and App. B.

A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which $\lambda$ is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.

A complete development needs the determinant of a $2\times 2$ block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• E. Ghadimi, H. R. Feyzmahdavian, M. Johansson, Global convergence of the Heavy-ball method for convex optimization, European Control Conference, 2015. https://arxiv.org/abs/1412.7457
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 2nd ed. 2020 (cited in the paper as 2013), Chapter 6. https://doi.org/10.1007/978-3-030-45982-6
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014. https://doi.org/10.1002/9780470316887

Inventory control when demand follows the state of the world

Single-item inventory theory asks how much stock to order each period when the order carries a fixed cost $K$ on top of a per-unit cost and demand is random. With independent, identically distributed demand, Scarf (1960) showed that the optimal finite-horizon policy has the $(s,S)$ form: when the stock falls below the reorder point $s$, order up to the level $S$; otherwise order nothing. His proof introduced $K$-convexity.

In practice demand is rarely i.i.d. It depends on economic conditions, seasons, or the stage of a product's life cycle, which change over time and carry over from one period to the next. Song and Zipkin (1993) modeled this by letting a Markov chain of "world states" modulate the demand distribution. Sethi and Cheng (1997) treat a general discrete-time model of this kind. The demand density, the cost parameters and the surplus cost all depend on the period and on the current demand state. They prove that a state-dependent $(s,S)$ policy is optimal over a finite horizon. They require no growth condition on the backlog cost, and they allow $s$ and $S$ to be $-\infty$.

Timeline:

• 1960: Scarf proves $(s,S)$ optimality for i.i.d. demand using $K$-convexity, assuming a backlog cost that grows faster than the unit ordering cost.
• 1966: Veinott gives an alternative proof under different assumptions.
• 1993: Song and Zipkin treat a continuous-time model with Markov-modulated Poisson demand and linear costs, assuming $p > \alpha c^i$.
• 1997: Sethi and Cheng prove the discrete-time result studied here, with general convex surplus costs.

Setting

There are $L$ demand states $I$ and periods $0, 1, \dots, N$. The state $i_k$ in period $k$ follows a Markov chain with transition matrix $P = (p_{ij})$. Given $i_k = i$, the demand $\xi_k \ge 0$ has density $\varphi_{i,k}$, with mean at most $M$. At the start of period $k$ an order $u_k \ge 0$ is placed and arrives at once. Then demand is subtracted, and unmet demand is backlogged:

$$x_{k+1} = x_k + u_k - \xi_k .$$

Ordering costs $c_k(i,u) = K^i_k\delta(u) + c^i_k u$, with $\delta(u) = 1$ for $u > 0$ and $0$ otherwise, and $K^i_k, c^i_k \ge 0$. A surplus $x$ costs $f_k(i,x)$, a convex, nonnegative function with $f_k(i,0) = 0$ and $f_k(i,x) \le C(1+|x|)$.

A decision $U = (u_n, \dots, u_{N-1})$ may depend on the whole observed history: the states up to the current one and the past demands. The objective and the value function are

$$J_n(i,x;U) = E\Big\{\sum_{k=n}^{N} \big[c_k(i_k,u_k) + f_k(i_k,x_k)\big]\Big\}, \qquad v_n(i,x) = \inf_U J_n(i,x;U).$$

With

$$F_{n+1}(b)(i,y) = \sum_j p_{ij}\int_0^\infty b(j,y-z)\varphi_{i,n}(z)\,dz,$$

the dynamic programming equations are $v_N = f_N$ and

$$v_n(i,x) = f_n(i,x) + \inf_{u\ge 0}\big\{c_n(i,u) + F_{n+1}(v_{n+1})(i,x+u)\big\}.$$

A function $g$ is $K$-convex if $K + g(z+y) \ge g(y) + z\,(g(y)-g(y-b))/b$ for all $z \ge 0$, $b > 0$.

Formalization targets

Goal: Theorem 4.1

Assume, for $n \in \langle 0, N-1\rangle$ and all $i$,

$$K^i_n \ge \sum_j p_{ij}K^j_{n+1} \ge 0 \quad (4.1), \qquad c^i_n x + F_{n+1}(f_{n+1})(i,x) \to +\infty \ (x\to\infty) \quad (4.2).$$

Then there are extended reals $s^i_n \le S^i_n < +\infty$ such that the rule

$$\hat u_n(i,x) = (S^i_n - x)\,\delta(s^i_n - x)$$

(a) attains the infimum in the dynamic programming equation at every $n$, $i$, $x$, and (b) generates a policy whose expected cost equals $v_0(i,x)$, the infimum over all admissible history-dependent policies.

Milestones

1. Theorem 3.1: the DP functions lie in $C_1$ (nonnegative, linear growth, uniformly continuous), and a measurable minimizer exists.
2. Theorem 3.2: the verification theorem.
3. Proposition 4.1(i)–(iv): calculus of $K$-convex functions.
4. Proposition 4.2(i)–(vi): the one-period $(s,S)$ structure of a $K$-convex, lower semicontinuous function on an interval $[A,B]$ with extended-real endpoints.
5. From the proof of Theorem 4.1: $v_n \ge f_n$; $z_n(i,y) = c^i_n y + F_{n+1}(v_{n+1})(i,y)$ is coercive at $+\infty$ and uniformly continuous; $v_n(i,\cdot)$ and $z_n(i,\cdot)$ are $K^i_n$-convex.

Significance

The theorem shows that the $(s,S)$ form survives when demand is driven by a Markov environment, with fixed costs that may vary by state and period. The only coupling condition is (4.1), under which today's fixed cost is at least the expected fixed cost of the next period. It needs no assumption on the backlog side, such as $p > c$. When ordering never pays, the levels are $-\infty$. The result is the base case of the paper's later extensions: no-ordering periods, capacity limits, and the discounted infinite horizon (a separate mission in this series). Policies of this kind are what practitioners compute.

The result is proved in print. The paper delegates Theorems 3.1–3.2 to Beyer, Sethi and Taksar (1998). It contains gaps, which this mission records and repairs:

1. Theorem 3.1's minimizer needs a coercivity condition.
2. Proposition 4.2(v) fails for a merely lower semicontinuous $g$.
3. Proposition 4.2's hypothesis $g^* > -\infty$ is not checked for $z_n$, which can be unbounded below.

A machine-checked proof settles these points. No formalization of the theorem or of its verification step exists. Published platform results cover the narrower Lemma 4.2.1 of Bertsekas, for continuous functions coercive at both ends.

Difficulty

The $K$-convexity calculus is elementary. The difficulty lies elsewhere:

1. Verification. Theorem 3.2 compares a feedback rule against every history-dependent, measurable policy. This needs a measurable-selection and dynamic-programming argument with integrals over paths of a Markov-modulated process. The natural induction must also control integrability at every step.
2. Proposition 4.2 at its generality. $g$ is only lower semicontinuous, $[A,B]$ may be unbounded, and $S$ or $s$ may equal $-\infty$. The case analysis behind (ii)–(iv) is delicate at the boundary.
3. The unbounded-below case. When $z_n$ is unbounded below, Proposition 4.2 does not apply. One must show directly that never ordering is optimal, using $K$-convexity at a "record low" far to the left.

Formalization scope

Conventions committed to in Lean, namespace SethiChengSS.Finite:

• Demand states are Fin L; periods are natural numbers with the paper's base.
• A policy is a function of (t, states i_n…i_{n+t}, demands ξ_n…ξ_{n+t−1}). It is admissible if it is nonnegative and measurable in the demands. So it cannot see the current or future demand, and nothing restricts it to Markov rules.
• Expectations use the joint density $\prod p_{i_t i_{t+1}}\varphi_{i_t,t}(\xi_t)$ with respect to counting measure times Lebesgue measure. This is the conditional-independence reading of "ξ_k dependent on i_k" under which (3.1) is the conditional expectation in (3.2).
• $J$ and $v$ are lintegral/⨅ in $[0,\infty]$.
• No order is placed in period $N$ ($u_N = 0$; (2.3) prints $c_N$).
• The DP is real-valued, with Bochner integrals and real infima. Theorem 3.1 shows they are genuine.
• $s, S$ are EReal, with $S \ne +\infty$ and $S = -\infty$ only if $s = -\infty$.
• Pins: (4.2) is added to the minimizer part of Theorem 3.1; continuity of $g$ is added to Proposition 4.2(v).

Trivializations excluded:

• The value is the infimum over all history-dependent measurable policies, never the DP solution itself.
• Policies are neither restricted to Markov rules nor allowed to be non-measurable.
• The densities are genuine probability densities and $P$ is stochastic.
• Real-valued $s, S$, which would make the goal false, are not required. Unbounded $S = +\infty$, which would make the rule meaningless, is excluded.

K-convexity is the published definition BertsekasKConvex. The published Bertsekas lemmas (BertsekasDP.kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure) are included as references. Each is narrower than its counterpart here: positive coefficients only, finite support only, continuity and coercivity at both ends. The posed SongZipkinFluct.FixedCost.theorem3 concerns a different, continuous-time model with integer levels and linear costs and is not used.

Welcome contributions: reusable infrastructure for path-space expectations of Markov-modulated processes; verification theorems for finite-horizon DPs with history-dependent policies; the extended-real $K$-convexity lemmas of Proposition 4.2.

Selected references

• S. P. Sethi and F. Cheng, Optimality of (s, S) policies in inventory models with Markovian demand, Operations Research 45(6), 931–939, 1997. https://doi.org/10.1287/opre.45.6.931
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott, On the optimality of (s, S) inventory policies: new conditions and a new proof, SIAM J. Appl. Math. 14(5), 1067–1083, 1966. https://doi.org/10.1137/0114086
• J.-S. Song and P. Zipkin, Inventory control in a fluctuating demand environment, Operations Research 41(2), 351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press, New York (cited by Sethi and Cheng as 1978; Lemma (d), p. 85).
• D. Beyer, S. P. Sethi and M. Taksar, Inventory models with Markovian demands and cost functions of polynomial growth, J. Optim. Theory Appl. 98(2), 281–323, 1998.

Motivation

Value iteration solves a Markov decision process by repeatedly applying the Bellman backup to a table of state values. When the state space is too large for a table, the values are stored in a function approximator instead: each backup is followed by a fit, and the fitted function is backed up again. This approximate value iteration is the basis of fitted dynamic programming and of much of reinforcement learning, and it was known in the early 1990s to diverge for common approximators such as linear regression and neural networks (Boyan and Moore, 1995, cited in the report as [BM95]).

Gordon's technical report (Stable Function Approximation in Dynamic Programming, CMU-CS-95-103, 1995; conference version at ICML 1995) identified a class of approximators, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a grid), for which the combination is stable. For discounted problems stability follows from a norm argument. For nondiscounted problems, where the backup contracts only in a weighted norm, that argument fails, and the report proves convergence by a different route: approximate value iteration is exact value iteration on a derived MDP. This mission formalizes that route and its conclusion, Corollary 4.1 (p. 11).

Setting

A finite nondiscounted Markov decision process $M$ has non-goal states $x=1,\dots,n$, a finite nonempty action set $U(x)$ at each state, an expected one-step cost $c_{xa}$, and transition probabilities $p_{axy}\ge 0$ with $\sum_y p_{axy}\le 1$. The missing mass $1-\sum_y p_{axy}$ is the probability of moving to a cost-free absorbing goal state, which the paper calls state $1$. A value function is a vector $V\in\mathbb R^n$; the goal's value is $0$. The parallel value backup is

$$(T_M V)(x)=\min_{a\in U(x)}\Bigl[c_{xa}+\sum_y p_{axy}V(y)\Bigr],$$

and with a discount factor $\gamma$ the sum is multiplied by $\gamma$. A policy $\mu$ chooses an admissible action at each state; it is proper if, from every starting state, the probability of having reached the goal after $t$ steps tends to $1$.

An averager $A$ consists of constants $k_y$, nonnegative weights $\beta_y$ and nonnegative weights $\beta_{yz}$ ($z$ ranging over all states, the goal included) with $\beta_y+\sum_z\beta_{yz}=1$. Its mapping is $M_A(V)(y)=\beta_yk_y+\sum_z\beta_{yz}V(z)$. Two operators $M_F$ and $T$ are compatible if $(M_F\circ T)^k(V_0)$ converges from every initial guess $V_0$.

The derived MDP $M'$ has the same states and actions, transition probabilities $p'_{axz}=\sum_y p_{axy}\beta_{yz}$ to non-goal states $z$, the rest of the mass going to the goal, and costs $c'_{xa}=c_{xa}+\gamma\sum_{y}p_{axy}\beta_yk_y$.

The states are layered by distance from the goal: $S_1=\{1\}$, $U_k=\bigcup_{j<k}S_j$, and $S_k$ is the set of states outside $U_k$ from which every action reaches $U_k$ with positive probability. Write $k(x)$ for the index of the layer containing $x$. The averager is self-weighted for $M$ if for every state $y$ either $\beta_y>0$ or $\beta_{yx}>0$ for some state $x$ with $k(x)\le k(y)$.

Formalization targets

Goal: Corollary 4.1 (p. 11)

If every policy of $M$ is proper and $A$ is self-weighted for $M$, then for every initial guess $V_0$ both

$$(M_A\circ T_M)^k(V_0)\quad\text{and}\quad(T_M\circ M_A)^k(V_0)$$

converge as $k\to\infty$. The first is the page's "$T_M$ and $M_A$ are compatible", the second its "approximate value iteration … will converge".

Milestones

1. Theorem 4.1 (Derived MDP, p. 7): $T_{M'}=T_M\circ M_A$, for every discount factor and for the nondiscounted backup.
2. Exhaustiveness (p. 10, after [BT89]): if all policies of $M$ are proper, every state lies in some layer $S_k$.
3. $M'$ terminates (p. 10): if all policies of $M$ are proper and $A$ is self-weighted, there is $m>0$ such that under every policy of $M'$ and from every state the goal is reached within $m$ steps with positive probability; in particular every policy of $M'$ is proper.
4. Theorem 2.3 (p. 4), in its all-policies-terminate case: value iteration converges from any initial guess. This is the published, proved item BertsekasDP.ssp_main_theorem.

A further item, Theorem 6.1 (p. 12), says the limit is $V^*$ when the optimal value function is a fixed point of $M_A$, under self-weighting or under positive costs with $k\ge 0$.

Significance

The corollary gives a checkable, purely combinatorial condition on the approximator and the transition graph under which fitted value iteration on a stochastic shortest path problem cannot diverge. Weight decay ($\beta_y>0$ everywhere) and any averager that only ever averages a state's value with values no farther from the goal satisfy it. The derived-MDP identity, Theorem 4.1, is the tool the rest of the report builds on (§5, §6.1, Appendix A): it reduces questions about approximate dynamic programming with averagers (convergence, the limit's error, the online Q-learning variant) to questions about an ordinary MDP.

The results are proved in the report, in prose. They have no machine-checked version. The formal development needed here is a finite stochastic shortest path theory (proper policies, the layer partition, termination bounds) on top of the published model BertsekasSSPModel and the proved BertsekasDP.ssp_main_theorem.

Difficulty

The obvious argument fails. If all policies of $M$ are proper, $T_M$ contracts in some weighted max norm, and $M_A$ is a nonexpansion in the unweighted max norm, but $M_A$ can expand the weighted norm, so the composition need not contract. Figure 4 of the report gives a three-state chain and an averager, replacing $V(2)$ by $V(3)$, for which approximate value iteration diverges. The proof therefore has to go through $M'$ and show that self-weighting makes $M'$ terminate under every policy. That is a probabilistic statement about all, possibly nonstationary, policies of a new process, derived from a layer structure of the old one. Exhaustiveness of the layers itself needs a policy-construction argument.

Formalization scope

The MDP is the published BertsekasSSPModel n C: non-goal states Fin n, a finite action type C with admissible sets M.U i, costs M.g, and transition probabilities M.p whose deficit is the probability of termination. Gordon's state 1 is this implicit termination state: its value is $0$ by construction, and where the partition and the averager's goal weight need to name it, it is none : Option (Fin n). This realises the page's two "without loss of generality" steps (state 1 cost-free and absorbing; $\beta_1=1$, $k_1=0$). The nondiscounted backup is BertsekasSSPBellmanOp M, the discounted one BertsekasDiscountedBellmanOp M γ.

The averager acts on whole value functions over the state set. An approximator that fits only a sample $X_0$ of states is the special case $\beta_{yx}=0$ for $x\notin X_0$. "All policies proper" quantifies over stationary policies μ : Fin n → C with admissible actions, as on p. 3. Self-weightedness is stated through layer membership, which agrees with the page's $k(x)$ whenever the partition is exhaustive (milestone 2). Theorem 6.1 takes $V^*$ as a real fixed point of the backup; under either of its cases such a fixed point is unique and optimal. Convergence is in $\mathbb R^n$, which is the same as convergence in max norm.

The goal's hypotheses concern $M$ and $A$ only. A formalization that assumed properness of the derived MDP, dropped the "every action" quantifier in the layers (making the partition and self-weighting weaker notions), or dropped $k(x)\le k(y)$ (making every averager with a positive weight self-weighted) would be a different theorem.

Reusable beyond this mission: the layer partition and its exhaustiveness, and the termination bound for the derived model, are general finite stochastic shortest path facts. Contributions to any milestone are welcome, and so are proofs of the definitions-level lemmas they rely on.

Selected references

• G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995. Conference version in Proceedings of the 12th International Conference on Machine Learning (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. ([BT89] in the report.)
• D. P. Bertsekas and J. N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
• J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, Morgan Kaufmann, 1995. ([BM95] in the report.)

Why offer sets matter

A seller with one limited inventory pool can choose which fare products to show in each selling period. When customers choose among the displayed products, showing another fare can both add sales and divert buyers from a more expensive fare. A fixed ranking of fares therefore does not by itself tell the seller which products to offer. Talluri and van Ryzin's working paper studies the optimal offer decision under a general discrete choice model, without specifying a logit or independent-demand formula for customer choice (working paper, 2001, pp. 5–8; published article, 2004). The present mission concerns the paper's first main result: how to reduce the collection of possible offer sets and how the best choice changes with inventory and time.

Model and notation

There are $n$ fare products, indexed by $N=\{1,\ldots,n\}$. Product $j$ earns a nonnegative revenue $r_j$. In each period, a customer arrives with probability $\lambda\in[0,1]$, independent of the remaining time. The seller offers a set $S\subseteq N$. Conditional on arrival, the customer buys product $j\in S$ with probability $P_j(S)$ or buys nothing with the remaining probability. Thus $P_j(S)\ge0$ and $Q(S)=\sum_{j\in S}P_j(S)\le1$. The purchase probability is $Q(S)$, while the expected revenue conditional on arrival is $R(S)=\sum_{j\in S}P_j(S)r_j$. The empty set is a possible offer; it has $Q=R=0$.

Time is counted backward: $t$ is the number of periods still available, and $x$ is the number of inventory units left. Let $V_t(x)$ be the maximum expected revenue from that state, with $V_0(x)=V_t(0)=0$. For $t,x\ge1$, the marginal value of capacity is $\Delta V_{t-1}(x)=V_{t-1}(x)-V_{t-1}(x-1)$. The Bellman equation is

$$V_t(x)=V_{t-1}(x)+\max_{S\subseteq N}\lambda\bigl(R(S)-Q(S)\Delta V_{t-1}(x)\bigr).$$

The paper calls a set $T$ dominated if a randomization over offer sets achieves either strictly more expected revenue with no greater purchase probability, or no less expected revenue with strictly lower purchase probability. A set is nondominated if neither comparison applies. This two-clause definition is specific to the paper. It differs from the one-clause “efficient set” used for a related model in Talluri and van Ryzin's book; the published formalization of that book's optimal policy theorem is therefore related work rather than a replacement for this goal.

Formalization targets

Nondominated frontier

Proposition 1 characterizes the nondominated sets by a positive tradeoff value $v$: a set $T$ lies on the relevant frontier exactly when it maximizes $R(S)-vQ(S)$ for some $v>0$. Proposition 2 says that dominated sets can be excluded from the Bellman maximization when $\Delta V_{t-1}(x)>0$, and that a nondominated optimum exists when the marginal value is zero. Proposition 3 orders the nondominated sets $S_1,\ldots,S_m$ so that both $Q_k=Q(S_k)$ and $R_k=R(S_k)$ are nondecreasing (working paper, pp. 8–12).

Largest optimal index

Among indices maximizing $R_k-Q_kv$, let $k^*(v)$ be the greatest one when there are ties. Lemmas 1 and 2 say that $k^*(v)$ is nonincreasing in $v$. The paper's Lemmas 3 and 4 say that marginal capacity values decrease as inventory increases and increase as the number of remaining periods increases. For the admissible states $t,x\ge1$, the goal is Theorem 1:

$$V_t(x)=V_{t-1}(x)+\lambda\bigl(R_{k^*}-Q_{k^*}\Delta V_{t-1}(x)\bigr),$$

where $S_{k^*}$ is an optimal offer, and the greatest optimal index $k^*$ is nondecreasing in $x$ and nonincreasing in $t$ (working paper, pp. 12–15, Theorem 1). These are claims about the index in the nondominated ordering; the offer sets themselves need not be nested by inclusion.

What the result gives

Theorem 1 replaces a search over all $2^n$ offer sets at each state with a search over the nondominated sets. It also tells an operator how the preferred position in that ordered list changes as seats are sold or as the selling horizon shortens. The later sections of the paper add conditions under which this ordering corresponds to fare-order nesting; those conditions are treated in separate missions (working paper, §3).

The model's value recursion and the marginal-value inequalities already have published Prove2Me formalizations in the Talluri–van Ryzin book setting. The book's marginal-value theorem is proved and serves here as a referenced milestone after reindexing its forward time convention. The paper's two-clause dominance concept, its ordered frontier, and Theorem 1 itself remain the formalization work of this mission. Keeping those distinctions explicit makes the resulting definitions reusable for other choice models with the same purchase and revenue coordinates.

Main difficulty

A set with high expected revenue need not be attractive when capacity is scarce: it may also consume inventory more often. Ranking sets by revenue alone therefore fails. Conversely, an offer set can tie another at a single marginal value, so selecting an arbitrary maximizer does not give a monotone index across states. The paper resolves ties by taking the greatest optimal index. Formalization must also retain the full randomized dominance relation: using only strict revenue improvement would leave sets on the wrong frontier. These issues arise even with finitely many products and without a specialized formula for $P_j(S)$.

Formalization scope

Products are Fin n, and offers are finite subsets of them. The published RevenueManagement_singleResource definition supplies the choice-model predicate, $Q$, $R$, and the backward value recursion. This mission defines the paper's own dominance relation, stage objective, exhaustive ordered list of nondominated sets, and greatest-maximizer predicate. Every possible offer set, including the empty set, participates in the Bellman maximum. The list must contain all nondominated sets exactly once; otherwise choosing from it would weaken Theorem 1.

The assumptions $0\le\lambda\le1$ and $r_j\ge0$ are the model's arrival-probability and nonnegative-fare conventions. The paper indexes fares in decreasing order, but Section 2's claims do not use that order, so the Lean targets omit it. Proposition 2's assertion that a dominated set is never optimal requires $\lambda>0$; that condition is placed on that clause alone. Decisions and marginal values are stated for $t,x\ge1$. The paper prints Lemma 3 also at $x=1$, where its right side $\Delta V_t(0)$ is undefined; the referenced formalization states the meaningful range $x\ge2$. The imported book theorem uses forward time, reindexed here as the number of periods remaining. The goal does not assume the dominance reduction or the marginal-value monotonicities that its milestones supply.

A complete development uses finite sums and maxima, the choice-value recursion, a finite frontier argument for Proposition 1, and order properties of the stage objective. The dominance and ordered-frontier definitions can support later results on nested policies. Contributions that establish the stated milestones under the same conventions are within scope.

Selected references

• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, UPF Economics Working Paper 533, October 21, 2001, pp. 5–15. Working paper.
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004, pp. 15–33. DOI: 10.1287/mnsc.1030.0147.

Motivation

A Markov decision process with finitely many states and actions and a discounted cost criterion can be solved in three classical ways: policy iteration, value iteration, and linear programming. The third goes back to F. d'Epenoux's paper A Probabilistic Production and Inventory Problem (Management Science 10(1), 1963, partly redrafted from a translation of d'Epenoux's 1960 article in the Revue Française de Recherche Opérationnelle), which showed that the optimal discounted cost of a stochastic production and inventory model is the solution of a single linear program. Together with Manne's linear program for the average-cost case (1960), it is the origin of the linear programming approach to dynamic programming, which underlies occupation-measure methods, constrained Markov decision processes, and approximate linear programming for large models.

Timeline:

• 1957–1960. Bellman's Dynamic Programming (value iteration, the principle of optimality); Howard's policy iteration for average costs (1960); Manne's linear program for average costs (Linear programming and sequential decisions, Management Sci., 1960).
• 1960/1963. d'Epenoux treats the discounted case: policy iteration and value iteration (Sections 2–4), then the linear program $(P_2)$ and its dual (Sections 5–6). Footnote 2 credits Guilbaud (1957) with an earlier observation of an equivalent linear program in another context.
• 1967. Denardo, Contraction mappings in the theory underlying dynamic programming, places the linear programs in an abstract contraction framework.

Setting

The stock at the beginning of a period is $i \in \{0, 1, \dots, \sigma\}$, where $\sigma$ is the stock capacity. The decision is the potential $j$, the quantity available for the period (output plus initial stock), with $i \le j \le \sigma$. Given the potential $j$, the stock at the end of the period is $s$ with probability $p_{js}$; each row $(p_{js})_s$ is a probability vector. The expected cost of a period with initial stock $i$ and potential $j$ is a real number $d_{ij}$. Costs one period ahead are discounted by $\lambda$, $0 < \lambda < 1$.

A strategy is a map $J$ with $i \le J(i)$ for every $i$: the potential depends only on the current stock. It has the transition matrix $(P_J)_{is} = p_{J(i)s}$ and the cost vector $(d_J)_i = d_{iJ(i)}$. The cost of following $J$ forever is the solution $u$ of (2), $u = d_J + \lambda P_J u$. The optimal cost $u^*$ solves the fundamental equation (7),

$$u^*_i = \min_{j \ge i}\Big( d_{ij} + \lambda \sum_{s=0}^{\sigma} p_{js} u^*_s \Big), \qquad i = 0, \dots, \sigma .$$

For a vector $u$ put $U_{ij} = u_i - \lambda \sum_s p_{js} u_s - d_{ij}$. The set $A$ consists of the vectors satisfying the linear constraints (9), $U_{ij} \le 0$ for all admissible pairs $i \le j$. The set $B$ consists of the vectors with $\prod_{j \ge i} U_{ij} = 0$ for every $i$.

Formalization targets

Goal: $u^* = \max(u \in A)$, and $(P_2)$

The system (7) has a solution, and every solution $u^*$ is the greatest element of $A$:

$$u^* \in A, \qquad u \le u^* \ \text{componentwise for every } u \in A .$$

Moreover, for every weight vector $c$ with all $c_i > 0$ and $\sum_i c_i = 1$, $u^*$ is the unique optimal solution of

$$(P_2) \qquad \text{maximize } (1-\lambda) \sum_i c_i u_i \quad \text{subject to } U_{ij} \le 0 \ \ (i \le j).$$

Milestones

1. Eq. (3). For a stochastic matrix $P$ and $0<\lambda<1$, $I - \lambda P$ is invertible and $(I-\lambda P)^{-1} = \sum_{k \ge 0} \lambda^k P^k$.
2. Eq. (4). $u - \lambda P u \ge 0$ implies $u \ge 0$.
3. Eq. (5). If moreover $u - \lambda P u \ne 0$ and $P$ is indecomposable, then $u_i > 0$ for all $i$.
4. Eq. (7). (7) has a unique solution, the cost of an optimal strategy (referenced, Proved).
5. Section 5. $u$ solves (7) iff $u \in A \cap B$; the points of $B$ are exactly the costs of strategies.
6. Section 5. Every point of $A$ lies below every point of $B$.
7. Section 5. If every $P_J$ is indecomposable, $u^*$ is a strict vectorial maximum of $A$: $u \in A$, $u \ne u^*$ imply $u_i < u^*_i$ for all $i$.

Significance

The result turns a fixed-point equation with a minimum in it into a linear program with $\tfrac12(\sigma+1)(\sigma+2)$ linear constraints. Its consequences are the ones the paper draws in Section 6: the dual of $(P_2)$ has a probabilistic interpretation (discounted state–action frequencies), its optimal basic solutions are optimal strategies, and every linear programming algorithm becomes an algorithm for discounted dynamic programs. The uniqueness clause is what makes the weighted objective recover the whole cost vector; with a single objective $u_e$, as the paper notes, the optimum need not determine the complete optimal strategy when the states decompose into several groups.

The dynamic programming half of the paper (Sections 2–4: policy evaluation, policy iteration, value iteration) is already formalized and proved on the platform for the general finite discounted model, as Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.3.1 (BertsekasDP.discounted_main_theorem); it enters this mission as a reference item, and the mission's model is an instance of the same published structure BertsekasSSPModel. The linear programming half is not formalized. Related items in other models are posed elsewhere: Bäuerle and Rieder's Theorem 7.5.9 (finite-state linear program in a measure-theoretic reward model, open) and Denardo's Programs I–II in an abstract contraction model; neither states the componentwise maximality of $u^*$ in $A$ in this model.

Difficulty

The individual steps are short, but the goal combines several facts that are easy to state wrongly. The paper calls the invertibility of $I-\lambda P$ and the positivity of its inverse "known and obvious"; in Lean they are statements about an arbitrary stochastic matrix over Fin m, for which Mathlib provides no default matrix norm, and the comparison of $A$ with $B$ depends on them. Uniqueness of the optimum of $(P_2)$ needs both strict positivity of the weights and the componentwise maximality; with a zero weight it fails. The obvious first idea for the strict maximum, that indecomposability of the optimal strategy's matrix alone suffices, is not the formalized statement: only the sufficient condition over all strategies is posed.

Formalization scope

Stock levels and potentials are Fin (σ + 1), $0$-based. The kernel $p_{js}$ is an arbitrary stochastic kernel indexed by the potential, and the costs $d_{ij}$ are arbitrary reals; the paper's demand-driven kernel and its cost decomposition $d_{ij} = d'(j-i) + \sum_n p_n d''(i,j,n)$ are an instance and are not built in, because the arguments of Sections 2–5 use only stochasticity (the paper itself remarks on p. 101 that its methods apply far beyond the inventory problem). Only admissible pairs $i \le j$ enter $A$, $B$, the minimum in (7), and strategies. The discount is called lam in Lean. Equation (7) is the fixed-point equation of the Bellman operator BertsekasDiscountedBellmanOp of the model.

Explicit readings of the paper's phrases:

• "$u^* = \max(u \in A)$" is IsGreatest in the componentwise order.
• "the complete solution" of $(P_2)$ is uniqueness of its optimal solution, for every admissible weight vector.
• "$u > 0$" in (5) and "strict vectorial maximum" mean every component strictly positive, respectively strictly smaller.
• "indecomposable" means irreducible: for all $i,k$ some power $P^n$ has $(P^n)_{ik} > 0$. The weaker reading (one closed class plus transient states) makes (5) false.
• "the points of the set $B$ correspond to the costs associated with every possible strategy" is the equivalence between membership in $B$ and solving (2) for some strategy.

Ruled out: defining $u^*$ as the optimum of the linear program, as a supremum of $A$, or as a limit (which would make the goal circular); assuming a solution of (7) without the existence conjunct; constraining also the inadmissible pairs $j < i$ (which can exclude $u^*$ from $A$); and weakening the weights to $c_i \ge 0$.

Not formalized: the demand-driven kernel, the finite-horizon recursion of Section 2, the monotone convergence remark of Section 4 (c), the count of strategies, the reformulations $(P_1)$ and $(P_3)$, and all of Section 6 (duality). Contributions welcome: proofs of the milestones and of the goal, and, as a follow-up mission, the dual programs of Section 6. The matrix facts (3)–(5) are stated for arbitrary stochastic matrices and are reusable beyond this mission.

Selected references

• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963. https://doi.org/10.1287/mnsc.10.1.98
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press and John Wiley, 1960.
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Prop. 7.3.1.
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Section 7.5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

A retailer that sets both its replenishment quantities and its prices over a finite selling season faces a coupled decision: the price shapes the demand that the inventory must serve, and the inventory position shapes which price is worth charging. With a fixed cost per order, the classical inventory answer is the (s, S) policy of Scarf (1960): when the stock falls below a reorder point $s$, order up to the level $S$. Thomas (1974) asked what happens when the price is also a decision, and conjectured that an (s, S, p) policy — an (s, S) ordering rule together with a price that depends on the stock level — is optimal "under fairly general conditions". He also gave a counterexample when prices are restricted to a discrete set.

Chen and Simchi-Levi (Operations Research 52(6), 2004) settled the conjecture for the finite horizon. When demand is additive in a random shock, $w_t = D_t(p_t) + \beta_t$, the conjecture holds (§3, Theorem 3.1). When the shock is not additive, it fails, and a weaker policy class is optimal (§4, the second mission of this series). This mission formalizes the additive case.

Timeline:

• Scarf (1960): (s, S) policies are optimal for the fixed-cost inventory problem, through k-convexity.
• Thomas (1974): conjectures (s, S, p) optimality with a continuous price range.
• Federgruen and Heching (1999): joint pricing and inventory without a fixed cost; base-stock list-price policies are optimal.
• Polatoglu and Sahin (2000): the lost-sales variant; sufficient conditions for (s, S, p) optimality.
• Chen and Simchi-Levi (2004): (s, S, p) optimality for additive demand with backlogging, and its failure in general.

Setting

There are $T$ periods $t = 1, \dots, T$. In period $t$ the firm starts with inventory $x$, orders up to a level $y \ge x$ at cost $k\,\delta(y - x) + c_t(y - x)$, where $k \ge 0$ is a fixed cost, $c_t$ a unit cost and $\delta(u) = 1$ if $u > 0$ and $0$ otherwise, and sets a price. Demand is $w_t = \alpha_t D_t(p_t) + \beta_t$ for a random pair $\epsilon_t = (\alpha_t, \beta_t)$ with $\mathbb E\alpha_t = 1$, $\mathbb E\beta_t = 0$; in the additive case $\alpha_t = 1$. Unmet demand is backlogged, and an end-of-period inventory $x$ costs $h_t(x)$, a convex function.

Since price and expected demand determine each other, the decision is an expected demand $d \in [\underline d_t, \bar d_t]$, with price $P_t(d) = D_t^{-1}(d)$ and expected revenue $R_t(d) = d\,P_t(d)$, assumed concave. With $G_t(y, d) = \mathbb E\,h_t(y - \alpha_t d - \beta_t)$, the profit-to-go functions satisfy $v_{T+1} \equiv 0$ and, for $t = T, \dots, 1$,

$$v_t(x) = c_t x + \max_{y \ge x}\Big[-k\,\delta(y - x) + g_t\big(y, d_t(y)\big)\Big], \qquad (2)$$ $$g_t(y, d) = R_t(d) - c_t y + \mathbb E\big\{-h_t(y - \alpha_t d - \beta_t) + v_{t+1}(y - \alpha_t d - \beta_t)\big\}, \qquad (3)$$

where $d_t(y)$ maximizes $g_t(y, \cdot)$ over $[\underline d_t, \bar d_t]$. A function $f$ is k-convex if $k + f(z + y) \ge f(y) + \frac{z}{b}\big(f(y) - f(y - b)\big)$ for all $z \ge 0$, $b > 0$, $y$ (Definition 2.1), and k-concave if $-f$ is k-convex. Assumptions 3–5 of the paper give $G_t$ the stated one-sided growth limits and polynomial growth $O(|y|^\rho)$, and give demand a finite $\rho$-th moment.

Formalization targets

Goal: Theorem 3.1(c)–(d)

For additive demand and every period $t$: $g_t(y, \cdot)$ attains its maximum at some $d_t(y)$, the functions $y \mapsto g_t(y, d_t(y))$ and $x \mapsto v_t(x)$ are k-concave, and there exist $s_t \le S_t$ such that

$$y^*(x) = \begin{cases} S_t, & x < s_t,\\ x, & x \ge s_t,\end{cases}$$

maximizes $-k\,\delta(y - x) + g_t(y, d_t(y))$ over $y \ge x$, $v_t(x) = c_t x - k\,\delta(y^*(x) - x) + g_t(y^*(x), d_t(y^*(x)))$, and a best expected demand exists at $y^*(x)$; the price is $D_t^{-1}$ of it.

Milestones

1. Definitions 2.1 and 2.2 of k-convexity are equivalent.
2. Lemma 1(d): a continuous coercive k-convex function has the (s, S) shape (already proved on the platform).
3. Lemma 2: a maximizer $d_t(y)$ can be chosen with $y - d_t(y)$ nondecreasing.
4. Theorem 3.1(a): $g_t(y, d) = O(|y|^\rho)$ and $v_t(x) = O(|x|^\rho)$.
5. Theorem 3.1(b): $g_t$ is continuous, $g_t(y, d) \to -\infty$ as $|y| \to \infty$, and $d_t(y)$ exists.
6. Inequality (7): $g_t(y, d_t(y))$ is k-concave when the continuation value is.
7. The display of $v_t$: its (s, S) form and the transfer of k-concavity from $g_t(y, d_t(y))$ to $v_t$.

Significance

The theorem identifies the structure of an optimal policy for a basic model of coordinated pricing and replenishment: two numbers per period determine the ordering decision, and the price is a function of the post-order stock. It confirms Thomas's conjecture in the additive case and tells a computation or an approximation scheme which policy class it may restrict to; §5 of the paper extends it to a nonincreasing fixed cost, the infinite horizon and Markovian demand.

The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization adds checked versions of the k-convexity toolkit (the equivalence of the two standard definitions; the (s, S) structure lemma), a checked monotone-selection argument for a parametric maximization, and a checked finite-horizon induction in which an expectation, a maximization over a continuous action and a fixed cost interact. The proof of part (a) is omitted in the paper ("similar to that of Theorem 1 in Federgruen and Heching (1999)"), so formalizing it supplies a missing argument.

Difficulty

The obvious argument fails at the expectation. A k-concave function composed with a shift $y \mapsto y - d - \beta$ is k-concave for a fixed $d$, but here the demand decision depends on $y$, and k-concavity, unlike concavity, is not preserved under an arbitrary reparametrization: Definition 2.2 is asymmetric in its two points. The inequality needed for the continuation value requires the post-demand levels $y - d_t(y) - \beta_t$ to be ordered like the inventory levels $y$. That is the content of Lemma 2, and it uses additivity; for multiplicative demand the ordering fails, and so does the theorem (§4).

The second difficulty is analytic: each step of the induction needs a continuous continuation value of polynomial growth, so that the expectation in (3) is finite and continuous, the maximum over $d$ is attained, and $g_t$ is coercive.

Formalization scope

The model is a structure of real data indexed by $t \in \mathbb N$, with periods $1, \dots, T$; the law of $(\alpha_t, \beta_t)$ is a probability measure on $\mathbb R^2$ and expectations are Bochner integrals. The formalization works in expected-demand space $d \in [\underline d_t, \bar d_t]$, equivalent to price space because $D_t$ is a continuous strictly decreasing bijection. Additivity is "$\alpha_t = 1$ almost surely". The profit-to-go is defined by recursion on the number of periods to go, with $v_{T+1} = 0$. Maxima are written as real suprema; every target that uses them asserts that they are attained, so the convention that an unbounded supremum is $0$ never enters. k-convexity is the platform's BertsekasKConvex (Definition 2.1); k-concavity of $f$ is k-convexity of $-f$.

Conventions and restrictions relative to the printed page:

• $O(|y|^\rho)$ is an explicit bound $C(1 + |y|^\rho)$ with $\rho \in \mathbb N$, uniform in $d$.
• Assumption 5, printed $E\{D_t(p, \epsilon_t)\}^\rho < \infty$, is read as $\mathbb E|\alpha_t d + \beta_t|^\rho < \infty$.
• Integrability of $h_t(y - \alpha_t d - \beta_t)$ is part of Assumption 4, and Theorem 3.1(a) also asserts that the expectation of $v_{t+1}$ in (3) is finite.
• Added hypotheses: $c_{T+1} = 0$ (the paper uses $c_{T+1}$ without defining it), $c_t \ge 0$ (used in the proof of part (b); without it $g_t$ need not tend to $-\infty$), and $k \ge 0$.
• Independence across periods is not stated; the dynamic program uses only each period's marginal law.
• The paper writes $s_t < S_t$ in the proof; for $k = 0$ equality is possible, so the targets use $s_t \le S_t$.

A trivializing formalization is ruled out: the targets assert attainment of every maximum they mention and the identity between $v_t(x)$ and the maximized objective, so a supremum that defaults to $0$, or an integral of a non-integrable function, cannot make them hold vacuously; and the assumptions are satisfiable (a one-period instance with $h(x) = |x|$ meets all of them).

A complete development needs: continuity of parametric integrals under polynomial domination; attainment of maxima over compact intervals; Topkis-style monotone selection for functions with increasing differences; the (s, S) structure lemma for k-convex functions (proved on the platform); and the closure of k-concavity under the operations above. The k-convexity results and the monotone-selection lemma are reusable for the general-demand mission of this series and for other fixed-cost inventory models. Contributions to any milestone are welcome, including proofs that rely on platform results by Topkis (Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences).

Selected references

• X. Chen, D. Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. https://doi.org/10.1287/opre.1040.0127
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• L. J. Thomas, Price and Production Decisions with Random Demand, Operations Research 22, 513–518, 1974.
• E. L. Porteus, On the Optimality of Generalized (s, S) Policies, Management Science 17, 411–426, 1971.
• A. Federgruen, A. Heching, Combined Pricing and Inventory Control Under Uncertainty, Operations Research 47(3), 454–475, 1999. https://doi.org/10.1287/opre.47.3.454
• H. Polatoglu, I. Sahin, Optimal Procurement Policies under Price-Dependent Demand, International Journal of Production Economics 65, 141–171, 2000.
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, Athena Scientific, 1995.