Dynamic Programming

Markov Chain Operations Research Optimization·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 1: For a Reversible Policy Chain, Accelerated Value Computation Converges at Rate 1 − √((1−λ)/(1+λ)) + η for Every η > 0Research Paper

Motivation

Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate $\lambda$ , the discount factor. When $\lambda$ is close to one, as in long-horizon reinforcement-learning benchmarks ( $\lambda = 0.99$ or $0.999$ ), the number of iterations grows like $1/(1-\lambda)$ , and each iteration costs a full sweep over states and actions.

In convex optimization, gradient descent on a $\mu$ -strongly convex, $L$ -smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number $\kappa = L/\mu$ from $\kappa$ to $\sqrt\kappa$ . Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read $v - T(v)$ as a gradient with "strong convexity" $1-\lambda$ and "smoothness" $1+\lambda$ , transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order $1-\sqrt{1-\lambda}$ instead of $\lambda$ .

Setting

An MDP has a finite set of states $\mathbb S$ with $|\mathbb S| = n$ , a finite set of actions $\mathbb A$ , transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$ ; each $P_{ia\cdot}$ is a probability distribution), real rewards $r_{ia}$ , and a discount factor $\lambda \in (0,1)$ . A policy $\pi$ assigns to every state $i$ a probability distribution $\pi_{i\cdot}$ over actions. It induces the reward vector $r_{\pi,i} = \sum_a \pi_{ia} r_{ia}$ , the transition matrix $L_{\pi,ij} = \sum_a \pi_{ia}P_{iaj}$ , the policy operator $T_\pi(v) = r_\pi + \lambda L_\pi v$ , and the value function

v^\pi = \sum_{t\ge0}\lambda^t L_\pi^t r_\pi,

the expected discounted reward when actions are drawn from $\pi$ . VC iterates $v_{s+1} = T_\pi(v_s)$ .

Accelerated Value Computation (A-VC) starts from arbitrary $v_0, v_1 \in \mathbb R^n$ and sets, for $s \ge 1$ ,

h_s = v_s + \gamma\,(v_s - v_{s-1}),\qquad v_{s+1} = h_s - \alpha\,\big(h_s - T_\pi(h_s)\big),

with the constant step sizes $\alpha = 1/(1+\lambda)$ and $\gamma = (1-\sqrt{1-\lambda^2})/\lambda$ . Write $\kappa = (1+\lambda)/(1-\lambda)$ .

A transition matrix $L$ is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution $\nu$ satisfying detailed balance, $\nu_iL_{ij} = \nu_jL_{ji}$ for all $i, j$ .

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

B_\pi = \begin{bmatrix}(1-\sqrt{1/\kappa})(I+L_\pi) & -\tfrac12(1-\sqrt{1/\kappa})^2(I+L_\pi)\\ I & 0\end{bmatrix},

whose powers propagate the stacked error $x_s - x^\pi$ , where $x_s = (v_s, v_{s-1})$ and $x^\pi = (v^\pi, v^\pi)$ . Its spectral radius $\rho(B_\pi)$ is the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.1

If $L_\pi$ is irreducible and reversible, then $v_s \to v^\pi$ , and for every $\eta > 0$

v_s = v^\pi + o\Big(\big(1-\sqrt{1/\kappa}+\eta\big)^s\Big),\qquad 0 < 1-\sqrt{1/\kappa} < \lambda.

The goal is stated with the $\eta$ slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order $s\,(1-\sqrt{1/\kappa})^s$ in general, so a clean $O\big((1-\sqrt{1/\kappa})^s\big)$ bound is false.

Milestones

The step-size identities of the proof of Lemma 5.2: $1+1/\kappa-2\alpha=0$ , $(1-\alpha)(1+\gamma)=\alpha\lambda(1+\gamma)=1-\sqrt{1/\kappa}$ , $\alpha\gamma\lambda=(1-\alpha)\gamma=\alpha-\sqrt{1/\kappa}=\tfrac12(1-\sqrt{1/\kappa})^2$ .
Lemma 5.2: $x_s = x^\pi + B_\pi^{s-1}(x_1-x^\pi)$ for all $s\ge1$ .
The eigenvalues of a reversible transition matrix are real (§2, p. 4).
$\operatorname{Sp}(L_\pi)\subset[-1,1]$ for a reversible policy chain.
(5.3): each eigenvalue $\omega$ of $B_\pi$ solves $\omega^2-(\mu+1)(1-\sqrt{1/\kappa})\omega+\tfrac12(\mu+1)(1-\sqrt{1/\kappa})^2=0$ for some $\mu\in\operatorname{Sp}(L_\pi)$ .
For $\mu\in[-1,1]$ : $\tfrac12|\mu+1\pm\sqrt{\mu^2-1}|\le1$ .
Lemma 5.3: $\rho(B_\pi) = 1-\sqrt{1/\kappa}$ .
(5.6): $\lambda = 1-\sqrt{1/\kappa}+\sqrt{1-\lambda}\,(1-\sqrt{1-\lambda^2})/\sqrt{1+\lambda}$ , with a positive last term.

Significance

The result. Since $1-\sqrt{1/\kappa} = 1-\sqrt{(1-\lambda)/(1+\lambda)}$ , A-VC reaches an $\epsilon$ -approximation of $v^\pi$ in $O\big((1-\lambda)^{-1/2}\log(1/(\epsilon(1-\lambda)))\big)$ iterations against $O\big((1-\lambda)^{-1}\log(1/(\epsilon(1-\lambda)))\big)$ for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound $\lambda^s/(1+\lambda)$ for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.

Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts $\eta$ under the square root, $o\big((1-\sqrt{1/\kappa+\eta})^s\big)$ . That rate is faster than $\rho(B_\pi)$ and is false (a one-state chain is a counterexample). The mission poses the rate $(1-\sqrt{1/\kappa}+\eta)^s$ that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).

Difficulty

The obvious argument says " $\rho(B_\pi)<1$ , so $B_\pi^s\to0$ at rate $\rho(B_\pi)$ ". That argument breaks twice. First, computing $\rho(B_\pi)$ requires knowing where the eigenvalues of $L_\pi$ lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed $1-\sqrt{1/\kappa}$ in modulus. Reversibility is what confines them to $[-1,1]$ , and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue $1-\sqrt{1/\kappa}$ of $B_\pi$ (coming from $\mu=1$ ) is a double root of (5.3) with a single eigenvector, so $\|B_\pi^s\|$ is not $O(\rho^s)$ ; only the $\eta$ -relaxed little-o holds. The eigenvalues of $B_\pi$ are non-real for $\mu\in(-1,1)$ , so the whole computation must be done over $\mathbb C$ .

Formalization scope

Data. $\mathbb S$ and $\mathbb A$ are finite types. The MDP is the data $(P, r, \lambda)$ . Validity (stochastic $P_{ia\cdot}$ , $\lambda\in(0,1)$ ) and the policy property are hypotheses. Rewards are arbitrary reals. The initial-state distribution $p_0$ of the paper's tuple is omitted, since nothing here uses it.
Reused definitions. $r_\pi$ , $L_\pi$ , $v^\pi$ , policies and the kernel condition are the published FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. $v^\pi$ is the discounted reward series, not an arbitrary fixed point of $T_\pi$ .
Reversibility is irreducibility plus a stationary probability vector in detailed balance. Detailed balance alone would be satisfied by $\nu=0$ and is not used.
Norms and rates. Vectors are functions $\mathbb S\to\mathbb R$ with the sup norm $\|\cdot\|_\infty$ ; " $o(\cdot)$ " is Mathlib's little-o along $s\to\infty$ .
Spectra are complex: $\rho(B_\pi)$ is the spectral radius of the complexified matrix, valued in $[0,\infty]$ . Using the real spectrum would make Lemma 5.3 a different, weaker statement.
Indexing. A-VC is a sequence on $\mathbb N$ with $v_0, v_1$ given; $x_s = (v_s, v_{s-1})$ is used only for $s\ge1$ .
Pinned relative to the page. In the goal, $\eta$ is outside the square root, as in the proof. In milestone 6, $\sqrt{\mu^2-1}$ is written as $i\sqrt{1-\mu^2}$ , its value for $\mu\in[-1,1]$ .

Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with $P_{iaj}=1/2$ is valid, reversible and has a policy), the rate is stated with $\forall\eta>0$ rather than for some $\eta$ , and $v^\pi$ is a fixed object rather than a variable constrained by hypotheses.

Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of $2\times2$ block matrices with commuting blocks; and the bound $\|M^s\| = o((\rho(M)+\eta)^s)$ from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

V. Goyal, J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004 (reprint 2013). https://doi.org/10.1007/978-1-4419-8853-9
P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 1999 (reprint 2013), Ch. 6. https://doi.org/10.1007/978-1-4757-3124-8
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (reprint 2014). https://doi.org/10.1002/9780470316887

18 thms6 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case III: Monotone Increase Models — Accumulation Points of DP-Optimal Controls Give an Optimal Stationary PolicyTextbook

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

16 thms6 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

On the Optimal Dividend Problem for a Spectrally Negative Lévy Process I: Optimality of the Barrier Strategy at c* in the Classical Dividend ProblemResearch Paper

Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$ . They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$ . Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$ , finite for $\theta\ge0$ :

\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).

Increments after time $s$ are independent of $\mathcal F_s$ . Initial capital $x$ is added to $X$ . The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$ , and either $\sigma>0$ , $\int_{(-1,0)}|y|\,\nu(dy)=\infty$ , or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$ . The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$ . The strategy is admissible ( $L\in\Pi$ ) if no lump sum exceeds the current reserves. Its value is

v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),

with discount rate $q>0$ . For $C\in[0,\infty]$ , $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$ .

The $q$ -scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$ . It is extended by $W=0$ on $(-\infty,0)$ . The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$ , paying $(x-a)^+$ at time $0$ . The paper computes its value

v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$ , read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$ . The generator is

\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$ , or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$ . Then $c^*<\infty$ and:

\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);

\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$ , $x\in[0,a]$ .
Lemma 2(i) (p. 15): $c^*<\infty$ .
Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$ , $a\ge0$ .
Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$ .
Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$ .
Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$ .

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$ , and optimality over all strategies reduces to one inequality on $(c^*,\infty)$ . It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$ , Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$ . The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$ . Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$ . Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$ . The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$ . The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$ : it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

Admissibility. The paper requires $L_{t+}-L_t<U_t$ . The formalization uses $\le$ , because the paper's own strategy of paying out everything at once needs it.
Barrier level (5.2). Printed over $a>0$ and "all $x$ ", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$ ) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$ , and otherwise $c^*=\infty$ .
Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$ . In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$ , and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$ .
Proposition 4(i) is stated for initial capital $x\le C$ . Beyond $C$ , $w$ is unconstrained and the printed claim fails.
Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$ .

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

Lévy processes and their Laplace exponents;
scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$ ;
reflected processes;
Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

294 thms6 active usersReviewed

Completed

Markov Chain Operations Research Optimization·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 2: For a Reversible Policy Chain, Momentum Value Computation Converges at Rate (1 − √(1/κ))/(1 + √(1/κ)) + η for Every η > 0Research Paper

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

The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
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)$ .
The eigenvalues of an irreducible, reversible transition matrix are real (§2).
(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$ .
For $\mu \in [-1,1]$ , the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$ .
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}}$ .
Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$ .
$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

13 thms5 active usersReviewed

Completed

Markov Chain Operations Research Optimization·Captain: mikedeng1

Optimality of (s, S) Policies in Inventory Models with Markovian Demand I: With Markov-Modulated Demand and Fixed Ordering Costs, a State-Dependent (s, S) Policy Is Optimal over a Finite HorizonResearch Paper

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

Theorem 3.1: the DP functions lie in $C_1$ (nonnegative, linear growth, uniformly continuous), and a measurable minimizer exists.
Theorem 3.2: the verification theorem.
Proposition 4.1(i)–(iv): calculus of $K$ -convex functions.
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.
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:

Theorem 3.1's minimizer needs a coercivity condition.
Proposition 4.2(v) fails for a merely lower semicontinuous $g$ .
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:

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.
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.
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.

20 thms5 active usersReviewed

Completed

Machine Learning Operations Research Probability+1·Captain: mikedeng1

Stable Function Approximation in Dynamic Programming II: In a Nondiscounted MDP with All Policies Proper, Value Iteration Through a Self-Weighted Averager ConvergesResearch Paper

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

Theorem 4.1 (Derived MDP, p. 7): $T_{M'}=T_M\circ M_A$ , for every discount factor and for the nondiscounted backup.
Exhaustiveness (p. 10, after [BT89]): if all policies of $M$ are proper, every state lies in some layer $S_k$ .
$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.
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.)

8 thms5 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Revenue Management Under a General Discrete Choice Model of Consumer Behavior 1: The Optimal Policy Offers Only Nondominated Sets, a Larger One the More Capacity and the Less Time RemainResearch Paper

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.

10 thms5 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

A Probabilistic Production and Inventory Problem: The Optimal Discounted Cost Is the Greatest Point of the Constraint Set (9) and the Unique Optimum of the Linear Program (P2)Research Paper

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

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$ .
Eq. (4). $u - \lambda P u \ge 0$ implies $u \ge 0$ .
Eq. (5). If moreover $u - \lambda P u \ne 0$ and $P$ is indecomposable, then $u_i > 0$ for all $i$ .
Eq. (7). (7) has a unique solution, the cost of an optimal strategy (referenced, Proved).
Section 5. $u$ solves (7) iff $u \in A \cap B$ ; the points of $B$ are exactly the costs of strategies.
Section 5. Every point of $A$ lies below every point of $B$ .
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

10 thms5 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case 1: Additive Demand: k-Concave Profit-to-Go, Optimal (s, S, p) PolicyResearch Paper

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

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

11 thms5 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control IV: LQR and the Riccati EquationTextbook

Motivation

The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.

Setting

Matrices $A \in \mathbb{R}^{n\times n}$ , $B \in \mathbb{R}^{n\times m}$ , $Q = C^\top C \succeq 0$ , $R \succ 0$ . The Riccati operator (BertsekasRiccatiMap)

F(P) = A^\top\big(P - P B (B^\top P B + R)^{-1} B^\top P\big) A + Q.

$(A,B)$ is controllable if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (BertsekasControllablePair); $(A,C)$ is observable if $(A^\top, C^\top)$ is controllable (BertsekasObservablePair). Separately, $g : \mathbb{R} \to \mathbb{R}$ is $K$ -convex (BertsekasKConvex, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$ , $b > 0$ , $y$ .

Target

\exists\, P \succ 0:\quad F(P) = P,\quad P \text{ unique among } P' \succeq 0,\quad F^{k}(P_0) \to P \ \ \forall P_0 \succeq 0,\quad \rho\big(A + BL\big) < 1,

with $L = -(B^\top P B + R)^{-1} B^\top P A$ — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the $(s,S)$ structure theorem for continuous coercive $K$ -convex functions.

Significance

The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$ -policy optimality. All results are classical and proved in the book; the formal work is new.

Difficulty

The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$ . For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.

Formalization scope

Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$ ; note $K \ge 0$ is forced whenever it is satisfiable ( $z = 0$ ), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5 (1960), 102–119.
H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford Univ. Press, 1960.

9 thms5 active usersReviewed

Completed

Control Theory Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control III: The Minimum PrincipleTextbook

Motivation

The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.

Setting

Minimize, over admissible pairs, the cost

h(x(T)) + \int_0^T g(x(t), u(t))\,dt \quad\text{s.t.}\quad \dot x(t) = f(x(t), u(t)),\; x(0) = x_0,\; u(t) \in U \subseteq \mathbb{R}^m,

with $f, g, h$ continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on $[0,T]$ — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start $(t_0, \xi)$ ). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (BertsekasHamiltonian).

Target

For an optimal admissible pair $(u^*, x^*)$ : there exist an adjoint $p$ and a constant $c$ with

\dot p(t) = -\nabla_x H(x^*(t), u^*(t), p(t)), \quad p(T) = \nabla h(x^*(T)),

u^*(t) \in \arg\min_{u \in U} H(x^*(t), u, p(t)), \qquad H(x^*(t), u^*(t), p(t)) = c,

away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).

The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$ .

Significance

The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.

Difficulty

For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.

Formalization scope

States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set — no compactness or convexity is assumed in the goal.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7

18 thms5 active usersReviewed

Bandit Algorithms Linear Optimization Operations Research+2·Captain: Shuze Chen

Multi-armed Bandit Allocation Indices IX: Suboptimality Bounds for Branching Bandits and Index Policies on Parallel MachinesTextbook

Motivation

Gittins index policies are optimal for a single server choosing among alternative bandit processes, and the achievable region method of Bertsimas and Niño-Mora (Math. Oper. Res. 1996) explains why: when the performance vectors of a scheduling system satisfy generalized conservation laws, the region they fill is a polytope whose optimal vertex is an index priority. Most real systems have several servers working in parallel, and for them the conservation laws fail. Glazebrook and Wilkinson (Ann. Appl. Probab. 2000) observed that $M$ parallel machines are close to a single machine working at $M$ times the speed, where the laws do hold, and turned that closeness into explicit bounds on how much an index policy can lose. Section 5.7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), presents that analysis for the simple family of alternative bandit processes (SFABP). Its first quantitative output is an upper bound on the optimal return, Corollary 5.20. This bound is the reference point against which the index heuristics of the rest of the section are measured.

This mission continues the public series Multi-armed Bandit Allocation Indices I–VI. Mission IV of that series formalized the single-machine achievable region theory of Chapter 5: Lemma 5.1, Theorems 5.5 and 5.10, and the identity of the adaptive greedy indices with Gittins indices.

Setting

There are $n$ arms. Arm $b$ has a finite state space $E_b$ ; the $E_b$ are disjoint, and their union $E = \{1, \dots, N\}$ is the set of job types. One transition kernel $P$ on $E$ moves an arm when it is processed. Each $E_b$ is closed under $P$ , and $P$ is irreducible on each $E_b$ . Time is discrete, rewards are discounted by $a^t$ with $0 < a < 1$ , and processing a job of type $i$ earns $r_i$ . There are $M$ identical machines, $1 \le M \le n$ . At each time $t = 0, 1, 2, \dots$ a policy $\pi$ chooses, on the basis of the history, a set of exactly $M$ arms. Each chosen arm makes one transition and the others are frozen. From the initial state-vector $k$ , the performance $x_i^\pi(k)$ is the expected total discounted number of times a job of type $i$ is processed. The return is $R^\pi(k) = \sum_{i \in E} r_i x_i^\pi(k)$ , and $R^{\mathrm{opt}}(k) = \sup_\pi R^\pi(k)$ .

The matrix $A = (A_i^S)$ is the single-arm matrix of §5.3, published in the series as conservationCoeff: for $i \in S$ , $A_i^S = E[1 + a + \cdots + a^{T_i^S - 1}]$ , where $T_i^S \ge 1$ is the number of transitions the chain started at $i$ needs to return to $S$ , and $A_i^S = 0$ otherwise. Job types are numbered in ascending order $\nu_1 \le \cdots \le \nu_N$ of the indices produced by the adaptive greedy algorithm $\mathrm{AG}(A, r)$ (IsAdaptiveGreedy, greedyIndex), and $S_i = \{1, \dots, i\}$ . Write

A^\pi(S, k) = \sum_{i \in E} A_i^S x_i^\pi(k), \qquad A(S, k) = \inf_\pi A^\pi(S, k).

Let $\psi_i$ be the number of arms with no job type in $S_i$ , let $i_b = \min E_b$ , and number the arms so that $i_1 \le \cdots \le i_n$ . For each other arm, $T_{k_b}^{S_i}$ is the processing needed to bring it from $k_b$ into $S_i$ for the first time, and $T_k^{S_i}$ is the sum of these over the other arms, which evolve independently.

Formalization targets

Goal: Corollary 5.20 (p. 142)

R^{\mathrm{opt}}(k) \le \nu_N \Big(\frac{M}{1-a}\Big) - \Big(\frac{1}{1-a}\Big) \sum_{i = i_{n-M+1}}^{N-1} (\nu_{i+1} - \nu_i)(M - \psi_i)\, E\Big[a^{T_k^{S_i}/(M - \psi_i)}\Big].

Milestones

Eq. (5.21) in the form of p. 139: $r_j = \nu_N - \sum_{i=j}^{N-1} (\nu_{i+1} - \nu_i) A_j^{S_i}$ .
Eq. (5.25): for every policy, $R^\pi(k) = \nu_N \frac{M}{1-a} - \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i) A^\pi(S_i, k)$ .
Lemma 5.19(ii): if $\psi_i \ge M$ then $A(S_i, k) = 0$ .
Lemma 5.19(i): if $M - 1 \ge \psi_i$ then $A(S_i, k) \ge \frac{M - \psi_i}{1 - a} E\big[a^{T_k^{S_i}/(M - \psi_i)}\big]$ .
Eq. (5.27): $R^{\mathrm{opt}}(k) - R^\pi(k) \le \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i)\big[A^\pi(S_i, k) - A(S_i, k)\big]$ .

The goal keeps the book's constants. Eq. (5.27) is a companion bound from the same identity.

Significance

The bound is explicit and computable from single-arm quantities: the AG indices and the laws of first-entry times. Subtracting from it the exact return of a concrete policy gives a certified suboptimality gap without solving the parallel-machine dynamic program, which has no index solution. The book uses it in exactly this way. With the exact return (5.30)–(5.31) of the heuristic $\pi_G^*$ , it shows that $\pi_G^*$ loses $O(1-a)$ , and in the limit $a \to 1$ that $\pi_G^*$ is average-overtaking optimal (Theorem 5.25).

All of these results are proved in the book and in Glazebrook and Wilkinson (2000). None is machine-checked. The series so far covers only the single-machine theory, and there is no parallel-machine bandit model on Prove2Me. This mission supplies that model and states the first link of the chain: from conservation-law algebra to a bound for a system that does not satisfy the conservation laws.

Difficulty

The identity (5.25) is algebra once the policy processes exactly $M$ arms in every period. The difficulty is the lower bound on $A(S_i, k)$ . The obvious idea, which works for one machine, is to minimize $A^\pi(S_i, k)$ by giving priority to job types outside $S_i$ . On $M$ machines such a policy cannot keep every machine busy outside $S_i$ , and the minimizing policy is not known, so $A(S_i, k)$ has no closed form and must be bounded below over all history-dependent policies at once. The bound has to hold uniformly: it must account for each arm's processing both before and after its first visit to $S_i$ , with arms frozen for random lengths of time in between. The printed proof also contains a step whose last inequality goes the wrong way (finding F2). The lemma is true, but the printed chain of inequalities cannot be followed literally.

Formalization scope

Job types are Fin (N + 1), so the book's $N$ is Lean's N + 1 and the book's type $i$ is the Lean index i - 1. Sums over $i = 1, \dots, N - 1$ run over i : Fin N, with $\nu_{i+1}$ = ν i.succ, $\nu_i$ = ν i.castSucc and $S_i$ = Finset.Iic i.castSucc. The arms are Fin n, and arm : Fin (N + 1) → Fin n assigns job types to arms. One kernel on the disjoint union replaces the book's per-arm matrices $P^b$ , and IsArmFamily states closedness and irreducibility. A policy (ParallelPolicy n N M) is a sequence of Markov kernels from histories to Boolean selection vectors with exactly $M$ true entries. The law of the history is built by composition, and the performance is a discounted sum of expected per-period occupation counts. $R^{\mathrm{opt}}$ and $A(S, k)$ are a real supremum and infimum over all policies. The class is nonempty because $1 \le M \le n$ , and both families are bounded, so neither takes a junk value. $E[a^{T/m}]$ is an integral against the product of the single-arm chain laws, with a real exponent and $a^\infty = 0$ . The numbering by AG indices is two hypotheses: the identity permutation is an output of $\mathrm{AG}(A, r)$ , and $\nu$ is monotone. The arm numbering is a function lowest with lowest b $= i_b$ and lowest monotone.

Unit conversions: none. Section 5.7 is written in discrete time with discount factor $a$ , the convention of the series' published definitions, so every constant is the book's.

Correction of the setup: the book assumes "the number of parallel servers $M$ exceeds the number of arms $n$ " (p. 139). The rest of the section needs the opposite (finding F1): for instance, the arm index $n - M + 1$ in Corollary 5.20 is not positive when $M > n$ . Every item assumes $1 \le M \le n$ .

Trivializing formalizations ruled out: $A(S_i, k)$ is not a hypothesis or an abstract GCL quantity. It is the infimum over an explicitly constructed, nonempty class of parallel-machine policies, so the goal cannot be discharged by assuming the conservation laws for the $M$ -machine system (which fail). The theorems do not allow $M > n$ , where the policy class is empty and the supremum would take the junk value $0$ .

Out of scope: the branching-bandit bounds of §5.5 (Theorems 5.12 and 5.13). They need a continuous-time branching-bandit model whose GCL property the book only cites. Also out of scope are Theorem 5.11 (priority classes) and the $O(\cdot)$ results 5.21–5.23 and Theorem 5.25.

Reusable infrastructure: the parallel-machine SFABP model (Def_AllocationIndices_Branching_Parallel) serves the remaining results of §5.7. Lemmas on the law of a frozen arm's trajectory under an arbitrary policy are welcome contributions.

Selected references

J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, §5.3 and §5.7. https://doi.org/10.1002/9780470980033
K. D. Glazebrook, D. J. Wilkinson, Index-based policies for discounted multi-armed bandits on parallel machines, Annals of Applied Probability 10 (2000), 877–896. https://doi.org/10.1214/aoap/1019487512
D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21 (1996), 257–306. https://doi.org/10.1287/moor.21.2.257

11 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 1: Under Multinomial Logit Choice the Optimal Dynamic Prices Equalize Marginal RevenuesResearch Paper

Motivation

Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.

The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.

Setting

There are $n$ product variates, indexed by $i$ , with finite quality parameters $a_i$ . Time $t$ is the number of periods remaining, so it counts down to zero. The inventory state $x=(x_i)$ has nonnegative integer coordinates, and $S(x)=\{i:x_i>0\}$ is the set of variates still in stock. At most one customer arrives during a period, with probability $\lambda$ satisfying $0<\lambda\leq1$ . Inventory is not replenished. The retailer chooses a finite, nonnegative price $r_i$ for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.

An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility $a_i-r_i$ to variate $i$ and utility $u_0$ to no purchase, with positive scale $\mu$ . Its probabilities are

P_i(x,r)=\frac{\exp((a_i-r_i)/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)},\qquad P_0(x,r)=\frac{\exp(u_0/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)}.

Let $\pi_t(x)$ be the maximum expected revenue from state $x$ with $t$ periods remaining and zero terminal value $\pi_0(x)=0$ . A sale of variate $i$ moves the inventory to $x-e^i$ . Its marginal inventory value is $\Delta^i\pi_t(x)=\pi_t(x)-\pi_t(x-e^i)$ when $i\in S(x)$ . For a continuation value $V$ , the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as $\xi_V(x,r)+V(x)$ , where $\xi_V$ is the probability-weighted marginal revenue.

Formalization targets

Optimal dynamic prices

Theorem 1 asks for a unique common margin $m_t(x)$ satisfying

\left(\frac{m_t(x)}{\mu}-1\right)\exp\left(\frac{m_t(x)+u_0}{\mu}\right) =\sum_{i\in S(x)}\exp\left(\frac{a_i-\Delta^i\pi_{t-1}(x)}{\mu}\right).

For every in-stock variate, the price $r_i^*=\Delta^i\pi_{t-1}(x)+m_t(x)$ must be feasible and attain the Bellman maximum. The margin also satisfies $m_t(x)P_0(x,r^*)=\mu$ . These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).

Total expected revenue

For each $s=1,\ldots,t$ , let $m_s(x)$ be the unique margin equation root at the same inventory state $x$ , with $s$ periods remaining. The remaining clause of Theorem 1 states

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr].

The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.

Significance

The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).

The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.

Difficulty

The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.

Formalization scope

Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes $\mu>0$ and $0<\lambda\leq1$ . The set $S(x)$ filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.

Lean's natural-number subtraction in $x-e^i$ is used only for $i\in S(x)$ , where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for $s=1,\ldots,t$ at one fixed $x$ , not along a sample path. No assumption that $n>0$ or $S(x)$ is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume $S(x)$ nonempty where the paper's positive-simplex argument requires it.

A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.

Selected references

Lingxiu Dong, Panos Kouvelis, and Zhongjun Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. DOI: 10.1287/msom.1080.0221.

10 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Dynamic Pricing and Inventory Control of Substitute Products 2: The Optimal Unified Dynamic Price under Multinomial Logit ChoiceResearch Paper

Motivation

Retailers often sell several variates of one product (colours, sizes or flavours of an otherwise identical item) from a fixed stock over a short season, with no replenishment. Customers substitute among the variates and the no-purchase option, so the price of one variate changes the demand for all of them, and the stock of each variate changes the value of selling the others. Dong, Kouvelis and Tian (M&SOM 2009) model this joint pricing and inventory problem with multinomial logit (MNL) choice and characterize optimal dynamic prices in closed form up to a scalar equation.

Many sellers do not price variates individually: apparel, sporting goods and airline examples are cited in the paper (Liu and Milner 2006) of unified dynamic pricing, where one price is charged for all variates and changed over time. Proposition 1 of the paper gives the optimal unified price and the optimal revenue in the same form as the paper's main result for variate-specific prices. Comparing the two quantifies how much revenue is lost by restricting to a common price, which is the purpose of the paper's §5.

Setting

There are $n$ variates, $\mathfrak n=\{1,\dots,n\}$ . Variate $i$ has quality index $a_i\in\mathbb R$ , the no-purchase option has utility $u_0\in\mathbb R$ , $\mu>0$ is the MNL scale parameter, and in each period one customer arrives with probability $\lambda\in(0,1]$ . Time $t$ counts the remaining periods, so the season runs $t=T,T-1,\dots,1$ and ends at $t=0$ .

An inventory level is $x\in\mathbb N^n$ . The in-stock set is $S(x)=\{i:x^i>0\}$ , and $x-e^i$ is the inventory after one sale of variate $i\in S(x)$ . Out-of-stock variates are not offered. At the price vector $r$ , an arriving customer buys variate $i\in S(x)$ or nothing with the MNL probabilities

P^i(r)=\frac{e^{(a_i-r^i)/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}},\qquad P^0(r)=\frac{e^{u_0/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}}.

Under unified pricing the decision in each period is one price $r\ge0$ charged for every in-stock variate. The unified value function $\pi_t(x)$ , the maximal expected revenue from $t$ remaining periods, satisfies $\pi_0\equiv0$ and

\pi_t(x)=\max_{r\ge0}\Bigl\{\lambda\sum_{i\in S(x)}rP^i+\lambda\sum_{i\in S(x)}P^i\pi_{t-1}(x-e^i)+(\lambda P^0+1-\lambda)\pi_{t-1}(x)\Bigr\},

with $P^i,P^0$ evaluated at $(r,\dots,r)$ . Write $\Delta^i\pi_{t-1}(x)=\pi_{t-1}(x)-\pi_{t-1}(x-e^i)$ for the marginal value of a unit of variate $i$ , and

\Delta^w\pi_{t-1}(x)=\frac{\sum_{i\in S(x)}e^{a_i/\mu}\Delta^i\pi_{t-1}(x)}{\sum_{i\in S(x)}e^{a_i/\mu}},\qquad a_w=\mu\ln\sum_{i\in S(x)}e^{a_i/\mu}.

Formalization targets

Goal: Proposition 1

For $t\ge1$ and $S(x)\neq\emptyset$ , the equation

\Bigl(\frac{m}{\mu}-1\Bigr)\exp\Bigl(\frac{m+u_0}{\mu}\Bigr)=\exp\Bigl(\frac{a_w-\Delta^w\pi_{t-1}(x)}{\mu}\Bigr)

has a unique solution $m_t(x)$ ; the price

r^*_t(x)=\Delta^w\pi_{t-1}(x)+m_t(x)

is nonnegative and optimal, with $m_t(x)P^0(r^*_t)=\mu$ ; and

\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr],

where $m_s(x)$ solves the equation of period $s$ at the same inventory $x$ . The statement asserts attainment of the maximum, not only a value for $\pi_t$ .

Milestones

The proof in Appendix A proceeds through a one-variable problem. For marginal values $\delta_i$ let $\xi(r)=\sum_{i\in S(x)}\lambda P^i(r)(r-\delta_i)$ . The milestones are: the rewriting (23)–(24) of the optimality equation as an attained $\max_{r\ge0}\xi^u_t+\pi_{t-1}(x)$ ; the derivatives of $P^i$ , $P^0$ and $\xi$ in the common price; the first-order conditions (25)–(26) with $\xi>0$ and $0<P^0<1$ at a stationary point; the second-order condition, giving exactly one stationary point, which is the global maximizer of $\xi$ on $\mathbb R$ ; the formula $r=\delta_w+m$ with $m=\mu/P^0$ and the equation for $m$ ; uniqueness of the root of the margin equation, with root $>\mu$ ; and the displayed revenue sum $\pi_t(x)=\lambda\sum_{s=1}^{t}[m_s(x)-\mu]$ at the same inventory.

Significance

Proposition 1 reduces a dynamic program over a high-dimensional inventory state to a scalar root-finding problem per state and period, and gives the optimal revenue as a sum of margins. It shows that the full dynamic pricing result (Theorem 1 of the paper) survives the restriction to a common price, with the individual marginal values $\Delta^i\pi_{t-1}$ replaced by their quality-weighted average $\Delta^w\pi_{t-1}$ , and the qualities replaced by the aggregate $a_w$ . This is what makes the paper's numerical comparison of unified, static and full dynamic pricing in §5 computable.

The result is proved in the paper; it has not been formalized. A formalization produces a checked version of the MNL derivative calculus, of the quasiconcavity argument for the common-price objective, and of the backward induction, and it closes a step the printed proof leaves implicit: that the maximizer over all real prices is nonnegative, so that it is feasible for the constrained problem.

Difficulty

The one-period objective is not concave in the price, so neither a concavity argument nor a direct appeal to a compactness theorem gives a unique maximizer. Negativity of the second derivative at stationary points is a local statement; the existence of a stationary point and its being the global maximum on all of $\mathbb R$ do not follow from it alone.

The second difficulty is the constraint $r\ge0$ . The paper solves the unconstrained problem. Showing that $\Delta^w\pi_{t-1}(x)+m_t(x)\ge0$ needs a property of the unified value function, nonnegativity of the weighted marginal value, which the paper does not state. The obvious argument, $\pi_{t-1}$ increasing in inventory term by term, does not apply verbatim when a variate leaves the in-stock set, because the choice set itself changes.

Finally, a supremum in Lean is a real number even when not attained; the value identity is only meaningful together with attainment, which the goal states explicitly.

Formalization scope

The model is one definition file, SubstitutePricing.Unified.Model: a structure with $n$ , $a:\mathrm{Fin}\,n\to\mathbb R$ , $u_0$ , $\mu$ , $\lambda$ ; assumptions $\mu>0$ , $0<\lambda\le1$ ; inventories $x:\mathrm{Fin}\,n\to\mathbb N$ ; the in-stock set as a Finset; MNL probabilities with sums over $S(x)$ only (the paper's null price $r^i=\infty$ is modelled by removal from the choice set); and the unified value function by recursion on $t$ , as a real sSup over $r\in[0,\infty)$ . The equation (3) is read with the no-purchase term outside the sum over variates, as the paper's (5) and (22) use it.

Committed conventions and restrictions:

$t\ge1$ in Proposition 1 (the printed " $t=T,\dots,0$ " includes $t=0$ , where $\pi_{t-1}$ does not exist).
$S(x)\neq\emptyset$ in every statement of the dynamic program and in the static milestones that use it: for an empty in-stock set $a_w$ and $\Delta^w\pi$ involve $\ln0$ and $0/0$ , and the revenue formula fails.
The optimal margin is quantified as the unique root of its equation, and the revenue formula takes the roots of all periods $s\le t$ at the same inventory $x$ .
The goal asserts nonnegativity of $r^*_t$ ; the paper's proof uses but does not prove it.
The paper's intermediate display (27) is misprinted and is not formalized; its correct consequences are.
Milestones 2–6 concern a static objective with arbitrary marginal values $\delta$ ; only the goal and the recursion milestone refer to the value function.

A statement about $\pi_t$ alone, without the attainment and feasibility of $r^*_t$ , would be trivially satisfiable by a junk supremum and is ruled out by the goal's form.

Infrastructure needed: derivatives of MNL probabilities, a quasiconcavity or unique-critical-point lemma for one-variable functions, a root lemma for $(m/\mu-1)e^{(m+u_0)/\mu}$ , and a monotonicity property of the unified value function. The MNL derivative calculus and the root lemma are reusable for the companion missions on full dynamic pricing and mixed pricing from the same paper. Contributions on any milestone, and on the nonnegativity of $\Delta^w\pi_{t-1}$ , are welcome.

Selected references

L. Dong, P. Kouvelis, Z. Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. https://doi.org/10.1287/msom.1080.0221
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997. https://doi.org/10.1287/opre.45.1.24
Q. Liu, J. Milner, Multiple-item dynamic pricing under a common pricing constraint, working paper, University of Toronto, 2006 (cited in the source as the motivation for unified pricing).
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.

9 thms4 active usersReviewed

Completed

Linear Optimization Markov Chain Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems VI: Constrained Average Reward — the Limit Points of the Expected State-Action Frequencies Form the Linear Programming PolytopeTextbook

Motivation

A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.

Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.

Setting

A finite Markov decision model has a finite state set $E$ , for each state $i$ a finite nonempty set $A(i)$ of actions, rewards $r_{ia}$ and transition probabilities $p_{iaj}\ge0$ with $\sum_j p_{iaj}=1$ . A policy $R$ chooses, at each time $t=1,2,\dots$ , an action in $A(i_t)$ at random, with probabilities that may depend on the entire history $(i_1,a_1,\dots,a_{t-1},i_t)$ . Special classes are the Markov policies $C_M$ (the rule at time $t$ ignores the past), the stationary policies $C_S$ , written $\pi^\infty$ (one rule $\pi$ , with $\pi_{ia}\ge0$ and $\sum_a\pi_{ia}=1$ , at every time), and the pure stationary policies $C_D$ , written $f^\infty$ with $f(i)\in A(i)$ . All policies form the class $C$ .

Fix an initial distribution $\beta$ : $\beta_j\ge0$ and $\sum_j\beta_j=1$ , with zeros allowed. The expected state-action frequencies in the first $T$ periods are

x^T_{ja}(R)=\frac1T\sum_{t=1}^T\sum_i\beta_i\,\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i).

$X(R)$ is the set of limit points of $\{x^T(R)\}_{T\ge1}$ , and $C_1$ the class of policies with exactly one limit point $x(R)$ . For a class $C'$ , $L(C')$ collects the limit points of all $R\in C'$ , giving $L$ , $L(M)$ , $L(C)$ (for $C_1$ ), $L(S)$ and $L(D)$ . For a stationary $\pi$ , $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$ , $P^*(\pi)$ is its Cesàro limit, and $x_{ja}(\pi)=[\beta^TP^*(\pi)]_j\pi_{ja}$ .

The polytope $X$ is the set of $x$ for which some $y$ satisfies

\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad\sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\quad(j\in E),\qquad x,y\ge0.

Given constraint data $q_{iak}$ and $b_k$ , the constrained problem (4.7.5) is $\sup_{R\in C_1}\{\phi(\beta,R)\mid\sum_i\sum_aq_{iak}x_{ia}(R)\le b_k,\ k=1,\dots,m\}$ , with $\phi(\beta,R)$ the lim inf of the average expected reward, and the linear program (4.7.6) maximizes $\sum_i\sum_ar_{ia}x_{ia}$ over $X$ 's constraints together with $\sum_i\sum_aq_{iak}x_{ia}\le b_k$ .

Formalization targets

Goal: Theorem 4.7.2

L=X.

Every limit point of the expected state-action frequencies of any policy lies in the polytope $X$ , and every point of $X$ is such a limit point.

Milestones

Theorem 4.7.1. $\overline{L(D)}=\overline{L(S)}=L(C)=L(M)=L$ , the bar being the closed convex hull.
Lemma 4.7.1. For $R\in C_1$ , $x_{ja}(R)=\lim_{\alpha\uparrow1}(1-\alpha)\sum_{t\ge1}\alpha^{t-1}\sum_i\beta_i\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ .
Theorem 4.7.3. Problems (4.7.5) and (4.7.6) have the same feasibility and the same optimum; an optimal policy yields an optimal $x(R)$ ; a Markov policy reproducing a mixture of pure stationary policies with the optimal $x$ is optimal.
Theorems 4.7.4–4.7.5. If the stationary rule $\pi^*$ built from an optimal $(x^*,y^*)$ by (4.7.14) satisfies $x^*=x(\pi^*)$ , then $(\pi^*)^\infty$ is optimal; two sufficient conditions for $x^*=x(\pi^*)$ .
Theorem 4.7.9. If $\pi\mapsto x(\pi)$ is continuous, then $X=L(S)$ .
Lemma 4.6.1 and Theorem 4.7.10. If every pure stationary policy is unichain, so is every stationary one, and then $X=L(S)$ .

Significance

The goal identifies the set of achievable long-run behaviours of a multichain Markov decision process with a polytope given by $2|E|$ linear equations. Any objective and any constraints that are linear in the frequencies then become one linear program (Theorem 4.7.3), and optimal policies are recovered from its solution. This is the basis of the linear programming approach to constrained average-reward control, later developed by Altman (Constrained Markov Decision Processes, 1999) and others.

The results of this section are proved in the monograph; none has a machine-checked proof. The mission produces a formal account of state-action frequencies under history-dependent policies on a finite model, their limit points, and the multichain LP polytope. The unichain special case is related to Derman's statements posed on the platform (DermanSeqDecisions.LinProg.*, completely ergodic models); the multichain statements here are not posed elsewhere.

Difficulty

The inclusion $L\subseteq X$ needs a limit point of a history-dependent policy to satisfy the second family of equations, which involves the auxiliary vector $y$ ; for stationary policies $y$ comes from the deviation matrix, but a general policy has no such matrix. The reverse inclusion cannot be obtained by realizing each $x\in X$ with a stationary policy: Example 4.7.1 of the book exhibits a model where $L(S)\neq X$ , and a point of $L(D)$ that is not an extreme point of $X$ . The natural candidate, the stationary rule $x_{ia}/\sum_ax_{ia}$ , is not defined on states with $\sum_a x_{ia}=0$ , and filling in $y$ there does not in general reproduce $x$ (Theorem 4.7.5 gives conditions under which it does). In the converse direction, frequencies of general policies need not converge, so arguments must work with all limit points, not with a limit.

Formalization scope

The model is the platform definition MarkovDecisionProcesses_AverageReward (reference item): StationaryMDP S A with finite state type S, a common finite action type A, a nonempty admissible Finset per state, rewards, and transition rows that sum to one; policies are its AvgHRPolicy, history-dependent and randomized. Frequency vectors are indexed by the admissible pairs.
$\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ is a finite recursive sum over histories; no measure theory is used. Lean's time index starts at $0$ (the book's $t-1$ ).
$X(R)$ is the set of limits of convergent subsequences of $x^T(R)$ . Policy classes are predicates that constrain only the weights of admissible actions.
$P^*$ is the limUnder of the Cesàro means $\frac1n\sum_{k=1}^nP^k$ ; its existence is the book's Theorem 2.4.1(i) and is not assumed as a hypothesis.
$\beta$ is a probability vector with zeros allowed; $\beta\gg0$ is never assumed.
The optima in Theorem 4.7.3 are compared in the extended reals, so the infeasible case reads $-\infty=-\infty$ .
"One ergodic set" is the platform's IsUnichainMatrix (any two recurrent states communicate); Assumption 4.7.1 is IsUnichain.
Trivializing formalization ruled out: $L$ ranges over all history-dependent randomized policies. Restricting it to stationary policies would replace $L$ by $L(S)$ , for which $L(S)=X$ fails in general.

A complete development needs Cesàro limits of stochastic matrices (Theorem 2.4.1), the stationary-policy correspondence of §4.3, a separating hyperplane in finite dimension, and the Derman–Strauch construction of a Markov policy matching a mixture of policies (Theorem 2.5.1). The frequency and limit-point infrastructure is reusable for any average-reward model on a finite state space. Proofs of any milestone, and of the auxiliary facts above as separate theorems, are welcome.

Selected references

L.C.M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
C. Derman, Finite State Markovian Decision Processes, Academic Press, New York, 1970.
C. Derman and A.F. Veinott, Constrained Markov decision chains, Management Science 19 (1972), 389–390. https://doi.org/10.1287/mnsc.19.4.389
C. Derman and R.E. Strauch, A note on memoryless rules for controlling sequential control problems, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699617
E. Altman, Constrained Markov Decision Processes, Chapman & Hall/CRC, 1999. https://doi.org/10.1201/9781315140223

13 thms4 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Bandit Processes and Dynamic Allocation Indices: A Policy Is Optimal If and Only If It Almost Surely Continues a Bandit Process of Maximal Dynamic Allocation IndexResearch Paper

Motivation

The multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.

J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.

Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.

Setting

A bandit process $D$ is a Markov chain $x(0), x(1), \dots$ on a measurable state space $\Theta$ with transition kernel $P$ . Applying the continuation control at process time $t$ earns the discounted reward $a^t R(x(t))$ , with $0<a<1$ , and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time $\tau$ of the chain (possibly infinite) write

R_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^tR(x(t))\,\Big|\,x(0)=x\Big\},\qquad W_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^t\,\Big|\,x(0)=x\Big\}.

The dynamic allocation index of $D$ in state $x$ is the largest reward per unit of discounted time obtainable by continuing for at least one step:

\nu(D,x)=\sup_{\tau>0}\nu_\tau(D,x),\qquad \nu_\tau(D,x)=\frac{R_\tau(D,x)}{W_\tau(D,x)}. \tag{2}

A simple family of alternative bandit processes consists of $k$ bandit processes. At each stage $n=0,1,2,\dots$ a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.

The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x ( $\nu_\tau$ ), gittinsIndex P r α x ( $\nu$ ), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first $n$ stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with $a$ written α and $R$ written r.

Formalization targets

Goal: the DAI Theorem (Section 3, p. 154)

For every policy $\pi$ and initial state vector $x$ ,

V_\pi(x)=\sup_{\pi'}V_{\pi'}(x)\iff \forall n,\ \text{a.s. under the play of }\pi\text{ from }x:\ \ \pi_n\Big(\big\{i:\nu(x_i(n))=\max_j\nu(x_j(n))\big\}\Big)=1 .

Milestones

Section 4, Lemma (p. 154). For $\Theta_0=\{y:\nu(D,y)<\nu(D,x)\}$ and $\tau$ the first $t\ge1$ with $x(t)\in\Theta_0$ ,

\nu_\tau(D,x)=\nu(D,x).

The "if" half of the DAI Theorem. A policy that selects a process of maximal index on every history is optimal: the published BanditAlgorithm.gittins_index_theorem, already Proved.
Section 4, Corollary 1 (p. 155). For the $M$ -horizon index $\nu^M(D,x)=\sup_{0<\tau\le M}\nu_\tau(D,x)$ (5), the rule that stops at the first $t\in\{1,\dots,M-1\}$ with $\nu^{M-t}(D,x(t))<\nu^M(D,x)$ , and at $M$ otherwise, attains $\nu^M(D,x)$ .

Significance

The result. The DAI Theorem replaces a dynamic program on the product of $k$ state spaces by $k$ one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.

Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.

Difficulty

The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if $\{y:\nu(D,y)<\nu(D,x)\}$ is measurable; the arguments of the countable case, which treat each state separately, do not transfer.

Formalization scope

All objects are the published discounted $k$ -armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from $0$ , stopping times are $\mathbb N\cup\{\infty\}$ -valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times $\tau\ge1$ . The explicit readings committed to are:

"Optimal" means attaining $\sup_{\pi'}V_{\pi'}(x)$ from the given initial state vector, over all randomized history-dependent policies; this supremum is finite because the values are bounded uniformly in the policy under the integrability hypothesis.
"At each stage … almost always" means: for every stage $n$ , almost surely under the law of the first $n$ stages of $\pi$ from $x$ , the selection kernel puts mass one on the processes of maximal current index. Requiring the index rule on every history would make "only if" false.
"The supremum of the total expected reward is finite" (p. 151) is read as $E_x\sum_t a^t|R(x(t))|<\infty$ for every state $x$ .
" $\nu(D,\cdot)$ is an $\mathcal X$ -measurable function" (p. 151) is an explicit hypothesis of the Lemma and of the goal; the measurability of every $\nu^m(D,\cdot)$ is a hypothesis of Corollary 1.
"The supremum is attained by setting $\Theta_0$ " means that the first hitting time of $\Theta_0$ from time $1$ on is a positive stopping time whose ratio equals the index.
The state space is standard Borel (the paper asks only for measurable singletons), and all processes share one kernel and one reward function; a family of different processes is encoded on the disjoint union of their state spaces.

A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time $1$ , so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.

Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for $k$ -armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.

Selected references

J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
P. Whittle, Multi-armed bandits and the Gittins index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
R. Weber, On the Gittins index for multiarmed bandits, Ann. Appl. Probab. 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
J. N. Tsitsiklis, A short proof of the Gittins index theorem, Ann. Appl. Probab. 4(1), 194–199, 1994. https://doi.org/10.1214/aoap/1177005207
J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

7 thms4 active usersReviewed

Completed

Linear Optimization Markov Chain Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems V: Average Reward — an Extreme Optimal Solution of the Multichain Linear Program Yields a Pure Stationary Average Optimal PolicyTextbook

Motivation

A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.

Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.

Setting

Let $E$ be a finite set of states. Each state $i$ has a nonempty finite set $A(i)$ of actions, a reward $r_{ia}\in\mathbb R$ for each action, and transition probabilities $p_{iaj}\ge 0$ with $\sum_j p_{iaj}=1$ . A policy $R$ chooses, at each epoch $t=1,2,\dots$ , a probability distribution on $A(X_t)$ that may depend on the whole history. A stationary policy $\pi^\infty$ uses fixed weights $\pi_{ia}$ at every epoch. A pure stationary policy $f^\infty$ always plays $f(i)\in A(i)$ . Write $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$ , $r(\pi)_i=\sum_a r_{ia}\pi_{ia}$ , and $P(f)$ , $r(f)$ in the pure case.

The average reward of $R$ from state $i$ is

\phi_i(R)=\liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i)\,r_{ja},

and $\hat\phi_i(R)$ is the same expression with $\limsup$ . The AMD-value-vector is $\phi_i=\sup_R\phi_i(R)$ , where $R$ ranges over all policies, and $R^*$ is average optimal if $\phi(R^*)=\phi$ . A policy is Blackwell optimal if it maximises the discounted reward $v^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\mathbb E_R[r_{X_tY_t}]$ for all discount factors $\alpha$ in some interval $[\alpha_0,1)$ .

For a stochastic matrix $P$ , the stationary matrix $P^*$ is the Cesàro limit of $P^n$ , and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$ . For a pure policy, $\phi(f^\infty)=P^*(f)r(f)$ and $u(f^\infty)=D(f)r(f)$ .

A vector $\tilde\phi$ is AMD-superharmonic if some $\tilde u$ satisfies $\tilde\phi_i\ge\sum_jp_{iaj}\tilde\phi_j$ and $\tilde\phi_i+\tilde u_i\ge r_{ia}+\sum_jp_{iaj}\tilde u_j$ for all $a\in A(i)$ , $i\in E$ . For weights $\beta_j>0$ with $\sum_j\beta_j=1$ , the primal program (4.2.10) minimises $\sum_j\beta_j\tilde\phi_j$ over such pairs. Its dual is

\max\Big\{\sum_{i,a}r_{ia}x_{ia}\ \Big|\ \sum_{i,a}(\delta_{ij}-p_{iaj})x_{ia}=0,\ \ \sum_ax_{ja}+\sum_{i,a}(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\ \ (j\in E),\ \ x,y\ge0\Big\}.\tag{4.2.11}

Write $E_x=\{i\mid\sum_ax_{ia}>0\}$ .

Formalization targets

Goal: Theorem 4.2.4

If $(x^*,y^*)$ is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule $f_*$ with

x^*_{if_*(i)}>0\ \ (i\in E_{x^*}),\qquad y^*_{if_*(i)}>0\ \ (i\in E\setminus E_{x^*})

exists, and every such $f_*^\infty$ is average optimal.

The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming $f_*$ .

Milestones

Optimality equations (Theorem 4.2.1): a Blackwell optimal pure policy gives $(\phi^\circ,u^\circ)$ with $\phi^\circ_i=\max_{a\in A(i)}\sum_jp_{iaj}\phi^\circ_j$ and $\phi^\circ_i+u^\circ_i=\max_{a\in\bar A(i)}\{r_{ia}+\sum_jp_{iaj}u^\circ_j\}$ .
Superharmonic characterisation (Theorem 4.2.2): $\phi$ is the smallest AMD-superharmonic vector.
Lim sup optimality (Theorem 4.2.3): a pure stationary average optimal $f^\infty$ satisfies $\hat\phi(f^\infty)\ge\hat\phi(R)$ for every $R$ .
The three propositions inside the proof of Theorem 4.2.4: complementary slackness along $f_*$ (4.2.1), closedness of $E_{x^*}$ under $P(f_*)$ (4.2.2), and transience of $E\setminus E_{x^*}$ under $P(f_*)$ (4.2.3).
The policy–solution correspondence (§4.3): the representative $(x(\pi),y(\pi))$ is feasible (Theorem 4.3.1); the map is one-to-one with inverse (4.3.1) (Theorem 4.3.2); $E_x$ is closed under, and is exactly the recurrent set of, $P(\pi(x,y))$ (Propositions 4.3.2–4.3.3); the correspondence preserves optimality (Theorem 4.3.3); pure policies map to extreme points (Theorem 4.3.4).
Policy evaluation (Theorem 4.4.1): the system $(I-P(f))\tilde\phi=0$ , $\tilde\phi+(I-P(f))\tilde u=r(f)$ , $\tilde u+(I-P(f))\tilde z=0$ is solvable, and every solution has $\tilde\phi=\phi(f^\infty)$ and $\tilde u=u(f^\infty)$ .

Significance

Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.

The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.

Difficulty

Under a unichain assumption, the dual variables $x$ form a stationary distribution and the $y$ -variables are unnecessary, so the obvious argument reads a policy off $x$ alone. In the multichain case the $x$ -part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off $y$ . The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of $\phi(f_*^\infty)$ with $\phi$ must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, $\phi_i(R^*)=\sup_R\phi_i(R)$ for every $i$ . It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from $i$ leads back to $i$ . The ergodic set of a recurrent state is the set of states accessible from it.

A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights $\beta_j$ are strictly positive and sum to one, as in (4.2.10).

The proofs need finite Markov chain theory: the Cesàro limit, $P^*P=PP^*=P^*$ , $P^*D=0$ , transience versus $P^*_{\cdot j}=0$ , and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
E. V. Denardo and B. L. Fox, Multichain Markov renewal programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968.
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

17 thms4 active usersReviewed

Completed

Linear Optimization Markov Chain Operations Research·Captain: mikedeng1

Linear Programming and Markov Decision Chains 1: A Pure Policy Read Off a Simplex-Optimal Solution of One Dual LP Is Average Optimal in Every Finite Multichain MDPResearch Paper

Motivation

A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.

Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.

Timeline, following the paper's introduction:

1960: d'Epenoux introduces linear programming for the discounted case; De Ghellinck and Manne treat the unichain average case.
1962: Blackwell (DOI 10.1214/aoms/1177704593) proves that some pure stationary policy is discounted-optimal for all discount factors near 1, and expands the discounted value near $\alpha = 1$ .
1968–1970: Denardo and Fox (DOI 10.1137/0116038) and Denardo (DOI 10.1287/mnsc.16.5.281) give the first analysis of linear programs for the multichain case. Derman's 1970 monograph streamlines it: in the worst case two linear programs and one search problem must be solved. Denardo and Fox record Bruce Miller's conjecture that the policy of Theorem 7 below is optimal.
1979: Hordijk and Kallenberg prove the conjecture (Theorem 7), so one linear program suffices.

Setting

The state space is a finite nonempty set $E$ . In state $i$ a finite nonempty set $A(i)$ of actions is available; choosing $a \in A(i)$ earns the reward $r_{ia}$ and moves the system to state $j$ with probability $p_{iaj}$ ( $p_{iaj} \ge 0$ , $\sum_j p_{iaj} = 1$ ). A policy $R$ chooses actions at times $t = 1, 2, \dots$ , possibly at random and using the whole history. For a policy $R$ and an initial state $i$ ,

\varphi_i(R) = \liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a \mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}

is the average expected reward, and $\varphi_i = \sup_R \varphi_i(R)$ is the optimal one. A policy $R^*$ is average optimal if $\varphi_i(R^*) = \varphi_i$ for every $i \in E$ . A decision rule $f$ picks $f(i) \in A(i)$ in every state; $f^\infty$ is the pure stationary policy that always applies $f$ . Its transition matrix is $P(f) = (p_{if(i)j})$ and its reward vector $r(f) = (r_{if(i)})$ . The α-discounted value $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\sum_j\sum_a\mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$ enters through Theorems 1, 3, 4 and 5.

Fix weights $\beta_j > 0$ with $\sum_j \beta_j = 1$ . The dual program has a variable pair $x_{ia}, y_{ia}$ for every state $i$ and every $a \in A(i)$ :

\max \sum_i\sum_a r_{ia}x_{ia}\quad\text{s.t.}\quad \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\quad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j,\quad x,y\ge0,

for all $j \in E$ . Its linear programming dual, the primal program, minimizes $\sum_j\beta_j\tilde\varphi_j$ over superharmonic pairs $(\tilde\varphi,\tilde u)$ : $\tilde\varphi_i \ge \sum_j p_{iaj}\tilde\varphi_j$ and $\tilde\varphi_i + \tilde u_i \ge r_{ia} + \sum_j p_{iaj}\tilde u_j$ for all $a \in A(i)$ , $i \in E$ . For a dual solution $(x, y)$ put $E_x = \{i \mid \sum_a x_{ia} > 0\}$ .

Formalization targets

Goal: Theorem 7

Let $(x, y)$ be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let $f$ be any decision rule with

x_{if(i)} > 0 \ \ (i \in E_x), \qquad y_{if(i)} > 0 \ \ (i \notin E_x).

Then $f^\infty$ is average optimal: $\varphi_i(f^\infty) = \varphi_i$ for every $i \in E$ , the comparison running over all policies.

Milestones

In the order the proof uses them:

Theorem 1 (Blackwell): some pure stationary $f_0^\infty$ is α-discounted optimal for all α near 1.
Theorem 2a: $\varphi(f^\infty) = P^*(f)r(f)$ . The other clauses of Theorem 2 are Blackwell's Lemma 1(a), (d), referenced as published theorems.
Theorem 3 (Blackwell): $v_i^\alpha(f^\infty) - \varphi_i(f^\infty)/(1-\alpha) \to (D(f)r(f))_i$ as $\alpha \uparrow 1$ .
Theorem 4 (Derman): the policy of Theorem 1 is average optimal.
Theorem 5: $\varphi^0 = \varphi(f_0^\infty)$ and $u^0 = D(f_0)r(f_0)$ solve the two nested optimality equations.
Proof of Theorem 6: $(\varphi^0, u^0 + M\varphi^0)$ is superharmonic for some $M$ .
Theorem 6: $\varphi$ is the smallest function that admits $u$ with $(\varphi, u)$ superharmonic.
§3.2: $(\varphi(f_0^\infty), D(f_0)r(f_0) + M\varphi(f_0^\infty))$ is primal optimal for all large $M$ .
Proof of Theorem 7: $\sum_a x_{ja} + \sum_a y_{ja} \ge \beta_j > 0$ , so the rule always defines a policy; and every primal optimum has first component $\varphi$ .
Propositions 1–3: $\varphi$ is $P(f)$ -harmonic and the gain–bias equation holds on $E_x$ ; $E_x$ is closed under $P(f)$ ; at an extreme optimal dual solution, the states outside $E_x$ are transient under $P(f)$ .

Significance

Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive $x$ -variable, otherwise any action with a positive $y$ -variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.

The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.

Difficulty

The obvious argument reads $f$ off any optimal dual solution and uses complementary slackness to obtain $\varphi = P(f)\varphi$ and $\varphi + (I - P(f))u = r(f)$ . The second equation holds only on $E_x$ , and outside $E_x$ nothing controls the reward of $f$ . The argument closes only when $E \setminus E_x$ is transient under $P(f)$ , so that the stationary distribution of $f$ ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside $E\setminus E_x$ would make the corresponding $y$ -columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from $(x, y)$ (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.

Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near $\alpha = 1$ . Both compare against all history-dependent policies and need the full limit theory of $P^*$ and $D$ .

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. $\varphi_i(R)$ is gainInf (the lim inf of the average of the first $T$ expected rewards) and $\varphi_i$ is optGainInf, a real supremum that is finite because rewards are bounded. $P^*$ and $D$ are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:

Average optimality is Hordijk and Kallenberg's $\varphi(R^*) = \varphi$ , not the stronger Puterman criterion IsAverageOptimal in the published file.
The discounted value is the limit of the $N$ -epoch discounted reward, defined by the same backward recursion as totalReward. "α near enough to 1" means some $\alpha_0 \in [0,1)$ such that the property holds on $[\alpha_0, 1)$ .
Dual variables are indexed by the admissible pairs only (Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.
"The simplex method is used" is encoded as " $(x, y)$ is an extreme point of the feasible set" (Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some $f$ instead of every $f$ obeying the rule is weaker than the paper's. Both are ruled out.
"Transient" is the negation of the published IsRecurrent. Maxima over $A(i)$ and $A^0(i)$ are stated as an upper bound plus attainment, so that $A^0(i) \ne \emptyset$ is part of Theorem 5.

A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of $\{z \ge 0 : Az = b\}$ by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with $P^*r$ . Contributions to any of them, including proofs of individual milestones, are welcome.

Selected references

A. Hordijk, L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
E. V. Denardo, B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
J. G. Kemeny, J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
C. Derman, Finite State Markovian Decision Processes, Academic Press, 1970.

17 thms4 active usersReviewed

Completed

Machine Learning Operations Research Reinforcement Learning·Captain: mikedeng1

Stable Function Approximation in Dynamic Programming I: In a Discounted Finite MDP, Value Iteration Through an Averager Converges to V₀ with ‖V₀ − V*‖ ≤ 2γε/(1 − γ)Research Paper

Motivation

Value iteration computes the optimal value function of a Markov decision process by applying the dynamic programming backup to every state until the values stop changing. When the state space is too large for a lookup table, practitioners replace the table by a function approximator: after each backup, the new values are computed only at a sample of states and an approximator (a neural net, a spline, a nearest-neighbour rule) is fitted to them. This approximate value iteration is the basis of much of reinforcement learning, and in the early 1990s it was known to work well in some experiments and to diverge in others, with no theory separating the two. Boyan and Moore (NIPS 7, 1995) exhibited divergence with linear regression and neural nets, and Tsitsiklis and Van Roy (1996) later studied the same question for feature-based architectures.

Gordon's technical report (CMU-CS-95-103, 1995; a shorter, differently numbered version appeared at ICML 1995) isolated a property of the approximator that guarantees convergence: the approximator must not exaggerate differences between target value functions in max norm. It identified a broad class with this property, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a mesh), and proved that in a discounted problem approximate value iteration through an averager always converges, with an explicit error bound. This mission formalizes that discounted theory: the report's §2–§3 and its error bound of §6.1.

Setting

A finite Markov decision process $M$ has states $1,\dots,n$ , a finite nonempty set $U(i)$ of actions at each state $i$ , an expected one-step cost $c_{ia}$ for action $a$ at state $i$ , and transition probabilities $p_{aij}\ge0$ with $\sum_j p_{aij}=1$ . It is discounted with factor $0\le\gamma<1$ . A value function is a vector $V\in\mathbb R^n$ , measured in the max norm $\|V\|=\max_i|V(i)|$ .

The parallel value backup operator $T_M$ updates every state at once:

(T_MV)(i)=\min_{a\in U(i)}\Big(c_{ia}+\gamma\sum_{j=1}^n p_{aij}V(j)\Big).

Its fixed point $V^*$ is the optimal value function, the minimal expected discounted cost from each state.

A function approximator is studied through its mapping $M_F$ : the function sending a vector of target values to the vector of fitted values. Two operators $M_F$ and $T$ are compatible if the iterates $(M_F\circ T)^k(x_0)$ converge from every initial guess $x_0$ .

An averager $A$ is given by constants $k_i$ and nonnegative weights $\beta_i,\beta_{ij}$ with $\beta_i+\sum_j\beta_{ij}=1$ for every $i$ ; its mapping is

M_A(Y)_i=\beta_ik_i+\sum_{j=1}^n\beta_{ij}Y_j .

The weights are fixed in advance and do not depend on the targets $Y$ .

Formalization targets

Goal: Theorem 6.2 (p. 12)

Let $V^A$ be any fixed point of $M_A$ and $\varepsilon=\|V^A-V^*\|$ . Then there is $V_0$ such that $(T_M\circ M_A)^k(V)\to V_0$ from every initial guess $V$ , and

\|V_0-V^*\|\le\frac{2\gamma\varepsilon}{1-\gamma}.

The goal has two parts: convergence from every start to a common limit $V_0$ , and the error bound on that limit.

Milestones

Theorem 2.2, first clause (p. 4). $\|T_MV-T_MW\|\le\gamma\|V-W\|$ .
Theorem 3.2 (p. 7). $M_A$ is a max-norm nonexpansion, $\|M_A(Y)-M_A(Z)\|\le\|Y-Z\|$ , and is compatible with $T_M$ for every discounted MDP.
Theorem 3.1 (p. 5). If $M_F$ is any max-norm nonexpansion, then $M_F$ is compatible with $T_M$ and $\|M_F(T_MV)-M_F(T_MW)\|\le\gamma\|V-W\|$ .
Corollary 3.1 (p. 6). There is $V_\infty$ with $\|(M_F\circ T_M)^k(V)-V_\infty\|\le\gamma^k\|V-V_\infty\|$ for all $V$ and $k$ .

A further item, not a milestone, is the display after the proof of Theorem 6.2 (p. 13), the bound on the fitted output: $\|V^*-M_A(V_0)\|\le2\varepsilon+2\gamma\varepsilon/(1-\gamma)$ .

Significance

Theorem 6.2 gives a guarantee that depends only on how well the approximator can represent $V^*$ , not on how the iteration is started: if some fixed point of the averager lies within $\varepsilon$ of $V^*$ , approximate value iteration finds a function within $2\gamma\varepsilon/(1-\gamma)$ of $V^*$ . Theorems 3.1 and 3.2 explain why: an averager is a max-norm nonexpansion, and composing a nonexpansion with a $\gamma$ -contraction leaves a $\gamma$ -contraction. Together they separate the approximators that are safe to use with value iteration from those that are not (linear regression is not a nonexpansion: the report's Figure 2 shows it can expand max-norm distances).

All results of this mission are proved in the report; none is open. The contraction of the discounted Bellman operator and the identification of its fixed point with the optimal value function are proved on Prove2Me (BertsekasDP.discounted_main_theorem, used here as a reference item). No machine-checked proof of Gordon's averager results or of the $2\gamma\varepsilon/(1-\gamma)$ bound is known to exist; this mission produces one, on top of the published finite MDP model.

Difficulty

Each step is short on paper; the difficulty is in the bookkeeping that a formal proof cannot skip. The nonexpansion of an averager rests on nonnegative weights summing to at most one, which must be extracted from the row constraint $\beta_i+\sum_j\beta_{ij}=1$ in the max norm on $\mathbb R^n$ . The goal's convergence clause asks for one limit $V_0$ shared by all initial guesses, which needs completeness of $\mathbb R^n$ and the contraction-mapping theorem applied to $T_M\circ M_A$ , not to $T_M$ . The error bound compares three different fixed points ( $V^*$ of $T_M$ , $V^A$ of $M_A$ , $V_0$ of $T_M\circ M_A$ ) in a chain of triangle inequalities. The order of composition matters throughout: the compatibility results iterate $M_F\circ T_M$ (fit after the backup), while the goal iterates $T_M\circ M_A$ (back up after the fit), and the two may not be interchanged.

Formalization scope

The MDP is the published BertsekasSSPModel (Fin n states, a finite action type, nonempty admissible action sets $U(i)$ , costs g, transition probabilities p), and $T_M$ is its BertsekasDiscountedBellmanOp M γ. That model allows substochastic rows; every statement adds the hypothesis $\sum_j p_{aij}=1$ for admissible $a$ , which makes it the report's MDP. Action sets may depend on the state, a harmless generalization of the report's single action set. The initial-state distribution $S_0$ never enters a statement and is omitted.
The discount satisfies $0\le\gamma<1$ in every item. Theorem 6.2's page says only "with discount factor $\gamma$ "; it belongs to the report's discounted discussion and its proof uses that $T_M$ is a $\gamma$ -contraction.
$\|\cdot\|$ on Fin n → ℝ is Mathlib's sup norm, i.e. the max norm.
$V^*$ is a hypothesis: a fixed point of $T_M$ . Theorem 2.2's last clause, proved on the platform as BertsekasDP.discounted_main_theorem, identifies it with the optimal value function.
The averager acts on whole value functions $\mathbb R^n\to\mathbb R^n$ , indexed by the states. The report's approximator fits a sample $X_0$ of states; ignoring the value at a state $j$ outside the sample is the special case $\beta_{ij}=0$ .
Theorem 3.1 is printed with " $X=S\times A$ " and $M_F\in\mathbb R^{|X|}\mapsto\mathbb R^{|X|}$ ; since $T_M$ acts on value functions of the state, $M_F$ is stated on $\mathbb R^n$ .
"Converges at the rate $\gamma$ " (Corollary 3.1) is the geometric rate of the contraction-mapping theorem, $\gamma^k$ times the initial distance to the limit.
Theorem 6.2 keeps $\varepsilon=\|V^A-V^*\|$ as an equality, as printed, and its conclusion keeps the convergence clause. A statement asserting only the existence of some $V_0$ with $\|V_0-V^*\|\le2\gamma\varepsilon/(1-\gamma)$ would be trivial ( $V_0=V^*$ ) and is not the theorem.
Lemma 2.1 and the Contraction Mapping theorem (Theorem 2.1) are in Mathlib (LipschitzWith.comp, ContractingWith) and are not posed.

Proofs of any item are welcome, as are reusable lemmas on max-norm nonexpansions of row-stochastic linear maps, which also serve the nondiscounted companion mission (Stable Function Approximation in Dynamic Programming II).

Selected references

G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995; shorter version in Machine Learning Proceedings 1995 (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 (the report's [BT89]; no DOI).
J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, MIT Press, 1995 (the report's [BM95]).
J. N. Tsitsiklis and B. Van Roy, Feature-Based Methods for Large Scale Dynamic Programming, Machine Learning 22, 1996, pp. 59–94. https://doi.org/10.1007/BF00114724

8 thms4 active usersReviewed

Completed

Complexity Theory Operations Research Optimization·Captain: mikedeng1

The Complexity of Markov Decision Processes I: A Boolean Circuit Is True Iff Its Finite-Horizon Markov Decision Process Has Optimal Expected Cost ZeroResearch Paper

Motivation

Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.

The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).

Setting

A circuit is a finite sequence of triples $C=((a_i,b_i,c_i),\ i=1,\dots,k)$ with $k\ge1$ . Each $a_i$ is one of the operations false, true, and, or. A triple with $a_i\in\{\text{false},\text{true}\}$ is an input; a triple with $a_i\in\{\text{and},\text{or}\}$ is a gate, and a gate reads two earlier triples, $1\le b_i,c_i<i$ . The value of an input is its constant; the value of a gate is the Boolean operation $a_i$ applied to the values of triples $b_i$ and $c_i$ . The value of $C$ is the value of triple $k$ .

A finite Markov decision process has a finite state set $S$ , an initial state $s_0$ , and at each state $s$ a nonempty finite set $D_s$ of decisions. Taking decision $i$ at state $s$ at time $t$ costs $c(s,i,t)$ and moves to $s'$ with probability $p(s,s',i,t)$ . A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state and time. For a horizon $T$ the expected cost of $\delta$ is

J_T(\delta)=\mathbb E_\delta\Bigl[\sum_{t=0}^{T}c\bigl(s_t,\delta(s_t,t),t\bigr)\Bigr],

and the optimal expected cost is $J_T^\ast=\inf_\delta J_T(\delta)$ over all policies.

From a circuit $C$ the proof of Theorem 1 builds a stationary process $M_C$ : one state per triple plus an absorbing state $q$ . An input state has one decision, moving to $q$ , at cost $1$ if the input is false and $0$ if it is true. An or gate has two free decisions, $0$ moving to $b_i$ and $1$ moving to $c_i$ . An and gate has one decision, moving to $b_i$ or $c_i$ with probability $1/2$ each. All other costs are zero. The initial state is triple $k$ and the horizon is $T=k$ .

In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.

Formalization targets

Goal: correctness of the reduction

J_k^\ast(M_C)\le 0\quad\Longleftrightarrow\quad \text{the value of } C \text{ is true},

for every circuit $C$ with $k\ge1$ triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of $C$ was true" on p. 445.

Milestones

Every policy has $J_k(\delta)\ge0$ ("it cannot be less").
For any finite process with nonnegative costs, $J_T(\delta)=0$ iff no positive cost is incurred on any trajectory of positive probability ("the states with positive costs are impossible to reach").
If some policy has $J_k(\delta)=0$ , then $C$ is true.
If $C$ is true, some policy has $J_k(\delta)=0$ .

Further statement

The discounted analogue, which the paper asserts in one sentence: for $\beta\in(0,1)$ , the optimal expected discounted cost $\inf_\delta\sum_{t\ge0}\beta^t\,\mathbb E_\delta[c(s_t,\delta(s_t,t))]$ of $M_C$ is at most $0$ iff $C$ is true (discounted_reduction).

Significance

Combined with the log-space computability of $M_C$ from $C$ , the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.

The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.

Difficulty

The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.

Formalization scope

Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.

Conventions committed to:

Triples are indexed by Fin k (paper index $i$ is Lean index $i-1$ ); $k\ge1$ via [NeZero k]. The fields $b_i,c_i$ of an input are unused (the paper sets them to $0$ , not a triple index). Triple $k$ need not be a gate.
States of $M_C$ are Option (Fin k), with none the state $q$ ; decisions are Fin 2 at or gates and Fin 1 elsewhere.
The and-gate row is $\tfrac12\mathbf 1[s'=b_i]+\tfrac12\mathbf 1[s'=c_i]$ , so that $b_i=c_i$ (allowed by the paper) gives a probability vector.
Rows of the transition kernel are probability vectors and every $D_s$ is nonempty (implicit in the paper, explicit here).
The expected cost is a finite sum over trajectories, with the §2 horizon convention $\sum_{t=0}^{T}$ and $T=k$ . The optimum is a real infimum over all policies $\delta(s,t)$ , not over stationary ones.
The discounted cost is $\sum_t\beta^t$ times the expected time- $t$ cost, which equals the expectation of the discounted series for bounded nonnegative costs.

A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.

Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time $T$ ) that are reusable for any finite-horizon process.

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3) (1987) 441–450. https://doi.org/10.1287/moor.12.3.441
R. E. Ladner, The Circuit Value Problem is Log Space Complete for P, SIGACT News 7(1) (1975) 18–20. https://doi.org/10.1145/990518.990519
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

8 thms4 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

The Complexity of Markov Decision Processes III: The Optimal Discounted Cost of a Deterministic Process Is the Least Discounted Cost of a SigmaResearch Paper

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$ -th arc with weight $\beta^t$ . The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$ , and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$ . Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$ ; it is stationary if $\delta(s,t)$ does not depend on $t$ . From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$ , the infimum over all policies $\delta(s,t)$ .

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$ : the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$ , multiplication is $+$ , zero is $+\infty$ ), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ( $+\infty$ if none), let $rA$ multiply every finite entry by $r$ , and let

B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$ -arc walk from $u$ to $v$ .

Formalization targets

Goal

For $0<\beta<1$ ,

J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$ .
A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
The products $B_j$ are the cheapest discounted $j$ -arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$ , and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$ -arc walks and closed $l$ -walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$ . Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$ "; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
Policies are maps $\delta(s,t)$ , time is $\mathbb N$ from $0$ , and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
Costs are tsums, which are junk ( $0$ ) for non-summable series; every statement that sums costs assumes $0<\beta<1$ , under which the series converge absolutely.
A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$ . This includes $j=0$ , a sigma whose cycle passes through $s_0$ , which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$ .
Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$ , not $\beta^j$ , for its $j$ -th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$ , not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$ , which the printed form misses); (iii) $B_0$ , used but not defined, is the min-plus identity.
Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$ , the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887

7 thms4 active usersReviewed

Completed

Linear Optimization Markov Chain Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 2: Under Irreducibility, an Optimal Solution of a Linear Program over State-Action Frequencies Yields an Optimal Stationary ProcedureResearch Paper

Linear programming for Markov decision problems

A Markov decision problem asks how to control a system that moves at random between finitely many states, where each decision changes the probabilities of the next move and incurs a cost. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) treats two criteria: the long-run average cost per period, and the total cost of driving the system into an absorbing state. Its Theorem 2 shows that, once attention is restricted to stationary procedures, each problem can be solved as a linear program over the state-action frequencies of the procedure. This mission formalizes that theorem, its supporting displays (3)–(10) and its Lemma on linear-fractional programs.

The linear programming formulation is now the standard computational and theoretical tool for constrained Markov decision processes, and its variables, the occupation measures, are the objects of most later work on that topic. Derman's paper is among the first to state it for the average-cost criterion. Manne (Linear Programming and Sequential Decisions, Management Science, 1960) gave an earlier average-cost formulation for an inventory model. The reduction of a ratio of linear functions to a linear program in Derman's Lemma is the transformation published in the same year by Charnes and Cooper (Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly, 1962).

Setting

There are finitely many states $0, \dots, L$ and decisions $d_1, \dots, d_K$ , all available in every state. Making decision $d_k$ in state $i$ sends the system to state $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ , and costs $w_{ik}$ .

A procedure of class $C'$ is stationary randomized: in state $i$ it makes decision $d_k$ with probability $D_{ik}$ , where $D_{ik} \ge 0$ and $\sum_k D_{ik} = 1$ , independently of the past and of the time. Under such a procedure the states form a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ . Write $W_t$ for the expected cost at time $t$ when $X_0 = i$ .

Problem 1 (average cost): minimize $Q_R(i) = \limsup_{T\to\infty} \frac{1}{T}\sum_{t=0}^{T} W_t$ . Here $w_{ik} > 0$ , and Assumption A says that under every procedure of $C'$ all states belong to one class.
Problem 2 (total cost): the state $L$ is absorbing under every decision and $w_{Lk} = 0$ . Minimize $S_R(i) = \sum_{t=0}^{\infty} W_t$ , the expected cost of reaching $L$ . Assumption B says that under every procedure of $C'$ , $L$ is reached from every state with probability one.

The state-action frequencies of a procedure $D \in C'$ with stationary distribution $\pi$ are $x_{jk} = \pi_j D_{jk}$ . They satisfy the linear constraints

\text{(10)}\qquad x_{jk} \ge 0,\qquad \sum_k x_{jk} - \sum_{i}\sum_k x_{ik}\, q_{ij}(k) = 0 \ \ (j),\qquad \sum_j\sum_k x_{jk} = 1 .

For Problem 2, Derman adjoins a state $-1$ that restarts the chain uniformly on $0, \dots, L$ and is entered from $L$ . The expected total cost then becomes a ratio of two linear functions of the frequencies of this augmented chain, (9).

Formalization targets

Goal: Theorem 2, pinned-down reading

The printed statement, "If Assumption A (B) holds, then problem 1 (2) can be formulated as a linear programming problem", is not a mathematical statement as it stands. The goal is the reading established by its proof (pp. 20–23).

Under Assumption A with $w > 0$ , the program

\min \ \sum_{j,k} x_{jk} w_{jk} \quad \text{subject to (10)}

has an optimal solution. For every optimal $x^*$ , every row sum $\sum_k x^*_{jk}$ is positive, and $D^*_{jk} = x^*_{jk}/\sum_k x^*_{jk}$ satisfies $Q_{D^*}(i) \le Q_D(i)$ for all $D \in C'$ and all $i$ .

Under Assumption B with the Problem 2 costs, the linear program obtained from (9) by the Lemma's transformation, $\min \sum w_{jk} z_{jk}$ subject to (12), has an optimal solution. For every optimal $(z^*, z^*_{n+1})$ one has $z^*_{n+1} > 0$ , and the procedure decoded from $x^* = z^*/z^*_{n+1}$ satisfies $S_{D^*}(i) \le S_D(i)$ for all $D \in C'$ and all $i$ .

Milestones

In the order the proof uses them: the Cesàro limit and the unique positive stationary distribution of a one-class chain ((3), (5)); the taboo-probability identity (4); the formula (6) for $Q_R$ ; the cycle formula (7) for the averaged total cost; the remark that minimizing the average of the $S_R(i)$ minimizes each one; the correspondence between $C'$ and the solutions of (10); and the Lemma reducing a linear-fractional program under conditions (i) and (ii) to the linear program (12).

Significance

The theorem replaces a search over infinitely many randomized procedures by a single finite linear program. It also yields the structural fact that an optimal stationary procedure can be read off from any optimal solution. The variables $x_{jk}$ make constraints on long-run frequencies of actions expressible as linear constraints. That is the origin of the theory of constrained Markov decision processes, and of the dual linear programs whose variables are value functions. The Lemma is the classical linear-fractional reduction, used well beyond this setting.

All of these results are proved in the paper and in later textbooks (for example Puterman, Markov Decision Processes, 1994, §8.8 and §9.5). None of them has been formalized: Mathlib has Perron–Frobenius-type facts for irreducible matrices but no linear programming theory, no taboo probabilities and no Markov decision model. The mission produces machine-checked versions of the proof's chain of equalities and of the decoding step, written so that they can be reused for occupation-measure arguments.

Difficulty

Several steps fail in the naive argument. The correspondence between procedures and solutions of (10) needs every row sum $\sum_k x_{jk}$ to be positive. That uses Assumption A for a procedure obtained by completing the decoded rows arbitrarily, together with the uniqueness and positivity of the stationary distribution. Positivity of the stationary vector of an irreducible but possibly periodic chain, and the Cesàro (not ordinary) convergence of $P^t$ , have no ready-made form in Mathlib. The total-cost identity (7) needs the regenerative identity (4), whose sums must first be shown to converge, and needs the augmented chain to be irreducible, which follows from Assumption B but is not assumed. Problem 2 needs one more step: a minimizer of the averaged total cost is optimal from every starting state, which uses the finiteness of all $S_R(i)$ .

Formalization scope

States and decisions are finite Lean types S and Act. Probabilities and costs are real numbers, a procedure of $C'$ is a nonnegative real matrix with unit row sums, and the chain is chainMatrix q D. Assumption A is irreducibility (Matrix.IsIrreducible) of every such chain matrix. Assumption B is reachability of $L$ from every state; for a finite chain in which $L$ is absorbing, this is equivalent to absorption with probability one. $Q_R(i)$ is a real limsup of a bounded sequence, with the paper's sum over $t = 0, \dots, T$ . $S_R(i)$ takes values in $[0, \infty]$ . The paper requires $w_{ik} > 0$ on p. 17 and $w_{Lk} = 0$ in Problem 2. The formalization uses $w_{ik} > 0$ for $i \ne L$ in Problem 2, and keeps the two problems as separate implications. The adjoined state $-1$ is none : Option S, with the transition law that produces Derman's $p_{-1,i} = 1/(L+1)$ , $p_{L,-1} = 1$ for every procedure. The published JewellMRP.InfiniteStep definitions of an ergodic matrix and of a stationary vector are reused.

The goal states optimality of the decoded procedure against every competitor in $C'$ , for every optimal solution of the linear program, with existence of an optimal solution as a separate clause. A statement that only identifies feasible sets, or that only asserts that some optimal procedure exists, does not count as Theorem 2. Optimality over all history-dependent procedures is Theorem 1, a separate mission of this series.

Welcome contributions: the stationary-distribution facts for irreducible finite stochastic matrices (reusable across Markov chain work), a small linear-programming existence lemma (a linear function attains its minimum on a nonempty compact polytope), and the Lemma's transformation, which is self-contained.

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4):181–186, 1962. https://doi.org/10.1002/nav.3800090303
K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Markov Chain Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 1: Deterministic Stationary Procedures Are Optimal for the Long-Run Average Cost and for the Total Cost to AbsorptionResearch Paper

Why restrict to stationary procedures

A Markov decision process with finitely many states and decisions is the basic model of sequential decision making under uncertainty: inventory replacement, machine maintenance, queue control and pursuit problems all fit it. Its computational methods (Howard's policy iteration, 1960; Manne's linear programming formulation, 1960) search only over stationary procedures, which use the same decision every time the system is in the same state. A controller, however, may also remember the whole past and randomize. Whether such procedures can do better is a genuine question: as Derman puts it, "a proof is required before a procedure optimal over $C'$ can be considered as the optimal procedure."

Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) answers it for two criteria, the long-run average cost and the total cost until absorption, by showing that a deterministic stationary procedure is optimal against all procedures. This mission formalizes that theorem, Theorem 1, together with the steps of its proof.

Timeline. Karlin (1955) gives the existence of a discount-optimal procedure used here; Howard (1960) and Manne (1960) solve the average-cost problem over stationary procedures; Wagner (1960) shows by linear programming that an optimal average-cost procedure can be taken deterministic and stationary; Derman (1962) proves the reduction for both criteria by the functional equation approach; Blackwell (1962) strengthens the discounted side to procedures optimal for all discount factors close to $1$ .

Setting

The system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of $K$ decisions $d_1, \dots, d_K$ is made; every decision is available in every state. If the system is in state $i$ and decision $d_k$ is made, it moves to state $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ , and a cost $w_{ik}$ is incurred.

A procedure $R$ chooses decision $d_k$ at time $t$ with probability $D_k(X_0, \Delta_0, \dots, X_t)$ , which may depend on the whole history of states $X_s$ and decisions $\Delta_s$ . The class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which this probability is a number $D_{ik}$ depending only on the current state $i$ . The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with $D_{ik} \in \{0, 1\}$ , that is, maps $f$ from states to decisions; $C''$ is finite.

Started from $X_0 = i$ , a procedure $R$ incurs the expected cost $W_t$ at time $t$ . The criteria are

Q_R(i) = \limsup_{T \to \infty} \frac1T \sum_{t=0}^{T} W_t \quad\text{(Problem 1)}, \qquad S_R(i) = \sum_{t=0}^{\infty} W_t \in [0, \infty] \quad\text{(Problem 2)},

and, for a discount factor $0 < \alpha < 1$ , the auxiliary discounted cost $V_R(i, \alpha) = \sum_{t \ge 0} \alpha^t W_t$ . Problem 1 assumes $w_{ik} > 0$ . Problem 2 assumes that state $L$ is absorbing under every decision and that $w_{Lk} = 0$ , so $S_R(i)$ is the expected cost of driving the system from $i$ into $L$ .

Formalization targets

Goal: Theorem 1

There are procedures $R_1, R_2 \in C''$ such that, for every state $i$ ,

Q_{R_1}(i) = \min_{R \in C} Q_R(i) \quad\text{(Problem 1)}, \qquad S_{R_2}(i) = \min_{R \in C} S_R(i) \ \ (\text{possibly } \infty) \quad\text{(Problem 2)}.

One procedure serves every initial state, and the minimum is over all of $C$ .

Milestones, in the order of the proof

The functional equation: $V_i = \min_{R \in C} V_R(i, \alpha)$ satisfies $V_i = \min_{D_i} \sum_k D_{ik}\,(w_{ik} + \alpha \sum_j q_{ij}(k) V_j)$ , the minimum over randomizations $D_i$ being attained.
For each $\alpha \in (0,1)$ some $R_\alpha \in C''$ minimizes $V_R(i, \alpha)$ over $C$ .
One $R^* \in C''$ is $\alpha_v$ -discount optimal along a sequence $\alpha_v \to 1$ .
$\lim_{v} (1 - \alpha_v) V_{R^*}(i, \alpha_v) = Q_{R^*}(i)$ for a stationary $R^*$ (published).
The Abelian inequality $Q_R(i) \ge \limsup_{\alpha \to 1^-} (1 - \alpha) V_R(i, \alpha)$ for every $R \in C$ (published).
Theorem 1 (1) itself (published, as part of Sennott's Proposition 6.2.3).
$S_R(i) = \lim_{\alpha \to 1^-} V_R(i, \alpha)$ for every $R \in C$ , finite or not.

Significance

Theorem 1 is what makes finite optimization possible for these problems: once $C''$ is known to contain an optimal procedure, the search runs over finitely many maps, and the linear programs of the paper's §3 (the next mission of this series) and of Manne describe the whole problem rather than a restriction of it. Part (2) is a total-cost result without any assumption that the absorbing state is reached; it holds even when every procedure has infinite cost from some state, which separates it from the stochastic shortest path theory that assumes properness.

Part (1) is available on the platform as part of Sennott's Proposition 6.2.3 (stated there, not yet proved), and it is referenced here rather than restated. Part (2), the functional equation for history-dependent procedures and the Abel-limit identity for the total cost have no statement on the platform; to our knowledge none has a machine-checked proof.

Difficulty

The obvious argument compares an arbitrary procedure with stationary ones state by state, but a history-dependent randomized procedure does not induce a Markov chain, so no transition matrix is available for it. The comparison has to pass through the discounted problem, where an optimal stationary procedure exists for each $\alpha$ , and then let $\alpha \to 1$ . Two limit exchanges are needed: for the average cost, an Abelian inequality valid for every procedure plus a Markov chain limit theorem for the stationary one; for the total cost, monotone convergence in $[0, \infty]$ , which must work when the limit is infinite. The discount-optimal procedure depends on $\alpha$ , and the finiteness of $C''$ is what yields a single procedure along a sequence $\alpha_v \to 1$ .

Formalization scope

The model is the published SennottDP.AvgFinite.Model (a Markov decision chain with finite action sets, nonnegative costs in $\mathbb R_{\ge 0}$ and transition probabilities in $[0, \infty]$ ) with finite nonempty types of states and decisions and every action set equal to the whole decision type. Derman's class $C$ is its Policy (history-dependent, randomized); $C''$ is StationaryPolicy. $W_t$ is expCost, $V_R(i, \alpha)$ is discCost, and $Q_R(i)$ is avgCost $= \limsup_n \frac1n \sum_{t<n} W_t$ , which has the same value as Derman's normalization because $W_t$ is bounded. $S_R(i)$ is a new definition, a sum in $[0, \infty]$ . Every discount factor is restricted to $(0, 1)$ explicitly. "Minimum over $C$ " is stated as an inequality against every policy, with the optimal procedure chosen before the initial state.

Problems 1 and 2 enter as separate implications with their own cost hypotheses; the page's " $w_{ik} > 0$ " is read as $w_{ik} > 0$ for $i \ne L$ in Problem 2, since $w_{Lk} = 0$ there. A formalization that compares only against stationary procedures, or that states the total cost as a real series (whose divergent values default to $0$ ), is ruled out: the competitors are all policies and $S_R(i)$ lives in $[0, \infty]$ .

A complete development needs the discounted Bellman equation for history-dependent policies, the selection of a deterministic minimizer, and Abelian theorems for nonnegative series. These are reusable across the platform's dynamic programming missions, and proofs of the referenced Sennott propositions are welcome contributions in their own right.

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
S. Karlin, The Structure of Dynamic Programming Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
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, 1960.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3):268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Propositions 6.1.1, 6.2.2, 6.2.3. https://doi.org/10.1002/9780470317037

11 thms4 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems III: Approximating Sequences for the Discounted Cost CriterionTextbook

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC( $\alpha$ ), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$ . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; nonnegative finite costs $C(i,a)$ ; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$ . A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$ . A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$ . Fix a discount factor $\alpha\in(0,1)$ . The discounted cost of $\theta$ and the discounted value function are

V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),

both in $[0,\infty]$ , the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$ , probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$ . The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$ , $r\notin S_N$ , according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$ : $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$ .

Assumption DC( $\alpha$ ): for every $i\in S$ , $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$ .

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$ ) is discount optimal for $\Delta$ .

Milestones

Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
Proposition 4.7.1: bounded costs imply DC( $\alpha$ ).
Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$ -step transition probabilities.
Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$ .
Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC( $\alpha$ ) holds.
Corollary 4.7.5: the case of a single distinguished state $z$ , with the relative form of the optimality equation for $\Delta_N$ .
Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$ , then $V^N_\alpha\le V_\alpha$ on $S_N$ .

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$ -valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$ , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$ -valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$ . The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$ ; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$ , a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$ . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$ ) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC( $\alpha$ ) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$ .

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Control Theory Operations Research Optimization·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 2: The Robust Bellman Recursion for Discounted Infinite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$ , and costs are discounted by a factor $\nu \in [0,1)$ : the cost at stage $t$ is $\nu^t c(i,a)$ .

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$ . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$ , so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$ , the state distribution evolves as $\mu_0 = e_{i_0}$ , $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$ . The discounted cost is

C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$ . The robust Bellman operator $g$ and, for a stationary policy $\pi$ , the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).

The two values of the game are

\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$ , i.e.

v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$ , where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$ , the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$ , every feasible $v$ satisfies $v \le v_\infty$ , and $v_\infty$ is the unique optimizer when $q > 0$ .
The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$ -Lipschitz in $\|\cdot\|_\infty$ .
(26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$ .
(28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$ .
(27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$ .

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$ -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

$C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$ .
The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$ ) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
$\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
$C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$ , so the series is summable and the tsum is the limit of the $N$ -stage costs, the paper's definition.
$\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$ .
Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$ , whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
Corrected statements:
- Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$ .
- In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$ .
- The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$ ). Both are needed by the other missions of this series.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms4 active usersReviewed

Dynamic Programming

Missions

A First-Order Approach to Accelerated Value Iteration 1: For a Reversible Policy Chain, Accelerated Value Computation Converges at Rate 1 − √((1−λ)/(1+λ)) + η for Every η > 0Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case III: Monotone Increase Models — Accumulation Points of DP-Optimal Controls Give an Optimal Stationary PolicyTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 5.11

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Optimal Dividend Problem for a Spectrally Negative Lévy Process I: Optimality of the Barrier Strategy at c* in the Classical Dividend ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 14)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A First-Order Approach to Accelerated Value Iteration 2: For a Reversible Policy Chain, Momentum Value Computation Converges at Rate (1 − √(1/κ))/(1 + √(1/κ)) + η for Every η > 0Research Paper

Why accelerate value computation

Setting

Formalization targets

Goal: Theorem 5.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimality of (s, S) Policies in Inventory Models with Markovian Demand I: With Markov-Modulated Demand and Fixed Ordering Costs, a State-Dependent (s, S) Policy Is Optimal over a Finite HorizonResearch Paper

Inventory control when demand follows the state of the world

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stable Function Approximation in Dynamic Programming II: In a Nondiscounted MDP with All Policies Proper, Value Iteration Through a Self-Weighted Averager ConvergesResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 4.1 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Revenue Management Under a General Discrete Choice Model of Consumer Behavior 1: The Optimal Policy Offers Only Nondominated Sets, a Larger One the More Capacity and the Less Time RemainResearch Paper

Why offer sets matter

Model and notation

Formalization targets

Nondominated frontier

Largest optimal index

What the result gives

Main difficulty

Formalization scope

Selected references

A Probabilistic Production and Inventory Problem: The Optimal Discounted Cost Is the Greatest Point of the Constraint Set (9) and the Unique Optimum of the Linear Program (P2)Research Paper

Motivation

Setting

Formalization targets

Goal: u∗=max⁡(u∈A)u^* = \max(u \in A)u∗=max(u∈A), and (P2)(P_2)(P2​)

Milestones

Significance

Difficulty

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