Dynamic Programming

Motivation

Chunk 07a built the general theory of infinite-horizon Markov Decision Processes and its sharpest special case, contracting models, where Banach's fixed point theorem delivers existence, uniqueness, and an explicit convergence rate all at once. That theory answers "does an optimal policy exist, and can I compute it by iterating a fixed point equation?" This mission answers the two questions a practitioner asks next: what happens when the reward's negative part, rather than its positive part, is the one that needs controlling (positive models, §7.4), and — more strikingly — can finding an optimal policy be reduced to solving a genuine linear program, the single most heavily-optimized computational primitive in all of operations research (§7.5)?

Setting

A positive Markov Decision Model is the mirror image of chunk 07a's general setup: instead of bounding the reward's positive part with an upper bounding function, the negative part is bounded by an integrability quantity $\varepsilon$, and the roles of "largest subharmonic" and "smallest superharmonic" swap accordingly. The computational sections build on chunk 07a's contracting theory directly: Howard's policy improvement algorithm iteratively replaces a decision rule with a strict pointwise improvement; the linear-programming approach recasts the entire optimization problem — the value function and the optimal policy — as a primal/dual pair of linear programs, not over finite vectors but over an infinite-dimensional space of measurable functions ($v \in IM$) and finitely-additive-in-spirit measures ($\mu \in M_b$); and state-space discretization approximates an infinite (Borel) state space by a finite grid, with an explicit, computable bound on the resulting numerical error.

Formalization targets

The goal, Theorem 7.5.8 (Strong Duality), is the section's deepest result: under chunk 07a's contracting Structure Theorem's own hypotheses, the primal linear program $(P)$ is solved exactly by the true optimal value function $J_\infty$, the dual program $(D)$ is solved by the occupation measure of any optimal stationary policy, and the two optimal values coincide. The milestones build up to it in three groups: the positive-model mirror theory (Lemmas 7.4.1-7.4.2, Theorems 7.4.3 and 7.4.5); Howard's policy improvement and its termination guarantee (Theorem 7.5.1, Corollary 7.5.3); and the linear-programming machinery itself (weak duality, complementary slackness, and the finite-state specialization that recovers an ordinary finite linear program, Theorems 7.5.6, 7.5.7, 7.5.9) together with the discretization error bounds that make the whole theory numerically usable (Proposition 7.5.11, Theorem 7.5.12).

Significance

The strong duality theorem is genuinely new content relative to what is already on the platform: the existing finite-dimensional LP duality missions (SmaleNinth.lp_strong_duality, LinearOptimization.lp_general_weak_duality, and others in the linear-optimization field) all operate over $\mathbb R^n$-valued vectors, while this theorem's primal and dual variables are a measurable function on a general Borel space and a measure on a general Borel space respectively — an infinite-dimensional linear program in the fullest sense. Theorem 7.5.9, the finite-state specialization, is the one point of genuine hypothesis-for-hypothesis contact with that prior art (checked directly; see STATUS.md for why it was drafted fresh rather than cited as a reference item), and it is exactly there that the reduction to an ordinary finite LP — with the platform's familiar vertex/extreme-point vocabulary — becomes visible.

Difficulty

Constructing the occupation measure $\mu^{f^\infty}_p$ without a canonical infinite-horizon path measure is the central technical challenge: it must be a genuine Measure (E × A), not merely a real-valued functional, since the dual program optimizes over a space of such measures. This mission builds it from iterated Measure.bind (pushing the initial law $p$ forward through the model's kernel under a fixed stationary decision rule) combined with a countable Measure.sum of $\beta^k$-scaled terms — a construction that stays entirely within Mathlib's existing measure-theoretic vocabulary without needing an Ionescu–Tulcea-style infinite product. A second, different difficulty is the state-space discretization section's grid interpolation, which presupposes a convex-combination structure ($x = \sum_k\lambda_kx_k$ for grid points $x_k$) on the state space that a general Borel space does not carry; this mission represents the grid operator and grid bounding function as data satisfying exactly the structural properties their two target theorems' own proofs use, rather than reconstructing the literal interpolation scheme — a deliberate, documented scope decision (see MODERATION_NOTES.md), not an approximation of either theorem's mathematical content.

Formalization scope

Every operator and value-function construction restates chunk 07a's own vocabulary (per this series' file-ownership convention, an independent copy in this chunk's own namespace), extended by the positive-model integrability bound $\varepsilon$, the occupation-measure/linear-program apparatus of §7.5.2, and the grid-approximation data of §7.5.3. The primal/dual optimal values $\mathrm{val}(P)$/$\mathrm{val}(D)$ are kept EReal-valued rather than real-valued specifically so that Theorem 7.5.6's own finiteness claims ($-\infty < \mathrm{val}(D)$, $\mathrm{val}(P) < \infty$) remain genuine, checkable content rather than being trivialized by a real-valued sInf/sSup's always-finite convention. Theorem 7.5.9's "optimal vertex" is stated via an explicit convex-combination (extreme-point) characterization using ENNReal weights, since Measure does not carry the module structure Mathlib's own Set.extremePoints requires.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (the policy improvement algorithm this section names after him).
• E. V. Denardo, "On linear programming in a Markov decision problem," Management Science, 1970 (the classical finite-state linear-programming formulation this section generalizes).
• W. J. Heilmann, "A note on the dual of a linear program with infinitely many constraints," cited by the book's own Remark 7.5.5 for the finitely-additive treatment the restricted dual $(D)$ over $M_b$ sidesteps.

Motivation

Two of the oldest simplifying assumptions in portfolio theory are that trading is frictionless and that risk means variance. Neither survives contact with practice: every real market charges a transaction cost proportional to the size of a trade, and variance penalizes upside deviations exactly as much as downside ones, which is not what an investor actually fears. Bäuerle and Rieder's §4.5 reopens the multiperiod terminal-wealth problem of chunk 04a with proportional transaction costs added to every trade, and finds that the qualitative shape of the solution survives — a buy/hold/sell rule with explicit thresholds, still obtained from the Structure Theorem of chunk 02a. Their §4.6 then leaves expected-utility maximization altogether and solves the classical Markowitz mean-variance problem in its genuinely dynamic, multiperiod form: choose a self-financing trading strategy that attains a target expected terminal wealth $\mu$ while minimizing the variance of that terminal wealth. This is Markowitz's one-period portfolio selection problem (H. Markowitz, Portfolio Selection, Journal of Finance, 1952) transplanted into a stage-by-stage trading horizon, and it earns its own solution technique: the objective is not linear in the underlying probability measure, so no direct Bellman equation applies, and the chapter instead builds a Lagrangian-embedding argument from scratch. Section §4.7 closes the chapter by replacing variance with the Average-Value-at-Risk, an axiomatically better-behaved risk measure (P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance, 1999), and solves the resulting mean-risk problem in the binomial model by the same Lagrangian route.

Setting

The transaction-cost model (§4.5): state $(x_0,x_1)\in E:=\mathbb{R}_{\ge0}^2$ (bond and stock holdings), action $a\in[0,x_1+x_0/(1+c)]$ (the stock holding chosen after the trade), bond holding after the trade $h(x_0,x_1,a) := x_0+(1-c)(x_1-a)$ if $a\le x_1$ and $x_0+(1+c)(x_1-a)$ if $a>x_1$, for a proportional cost rate $c\in[0,1)$; transition $T_n((x_0,x_1),a,z) := (h(x_0,x_1,a)(1+i_{n+1}),\,az)$; terminal reward $U(x_0+x_1)$ for a utility $U$ homogeneous of degree $\gamma$.

The mean-variance model (§4.6): state $E:=\mathbb{R}$ (wealth), action $A:=\mathbb{R}^d$ (amounts invested in $d$ risky assets, short-selling allowed), transition $T_n(x,a,z) := (1+i_{n+1})(x+a\cdot z)$. Writing $X_N$ for the terminal wealth reached from $x_0$ under a strategy $\pi$, the problem is

$$\mathrm{(MV)}\qquad \mathrm{Var}_{x_0}^\pi[X_N] \to \min \quad\text{subject to}\quad \mathbb{E}_{x_0}^\pi[X_N] \ge \mu, \ \ \pi \text{ admissible.}$$

Because $\mathrm{Var}$ is not linear in the law of $X_N$, (MV) is solved via the Lagrangian $L_{x_0}(\pi,\lambda) := \mathrm{Var}_{x_0}^\pi[X_N] + 2\lambda(\mu-\mathbb{E}_{x_0}^\pi[X_N])$, whose saddle points give (MV)'s value and optimizer, reduced in turn to the tractable auxiliary quadratic problem $QP(b)$: minimize $\mathbb{E}_{x_0}^\pi[(X_N-b)^2]$, a stochastic linear-quadratic control problem.

The mean-risk model (§4.7): the binomial (Cox–Ross–Rubinstein) market with one bond (interest rate $0$) and one stock with relative return $u-1$ w.p. $p$ or $d-1$ w.p. $1-p$; the Average-Value-at-Risk at level $\gamma$, $\mathrm{AVaR}_\gamma(X) := \inf_{b\in\mathbb{R}} [b+\frac{1}{1-\gamma}\mathbb{E}[(X+b)^-]]$; the problem $\mathrm{(MR)}: \mathrm{AVaR}_\gamma(X_N)\to\min$ subject to $\mathbb{E}_{x_0}^\pi[X_N]\ge\mu$, solved via the same Lagrangian route through an auxiliary problem $P(\lambda,b)$.

Formalization targets

Goal — Theorem 4.6.6 (the mean-variance problem)

$$\mathrm{Var}_{x_0}^{\pi^*}[X_N] = \frac{d_0}{1-d_0}\big(\mathbb{E}_{x_0}^{\pi^*}[X_N] - x_0S^0_N\big)^2, \qquad \mathbb{E}_{x_0}^{\pi^*}[X_N] = \mu,$$ $$f_n^*(x) = \Big(\frac{\mu-d_0x_0S^0_N}{1-d_0}\cdot\frac{S^0_n}{S^0_N} - x\Big)\, C_{n+1}^{-1}\,\mathbb{E}[R_{n+1}],$$

where $(d_n)$ is a recursively-defined sequence in $(0,1)$ (Lemma 4.6.4) built from the one-period return moments $C_n,\mathbb{E}[R_n]$. This closes the loop the chapter opens: it is the exact value and optimal strategy of the dynamic mean-variance problem, obtained by specializing the auxiliary problem $QP(b)$'s closed-form solution (Theorem 4.6.5) at the Lagrange multiplier that Lemma 4.6.2's saddle-point argument selects.

Supporting milestones

The Lagrangian route itself: the equivalence of (MV) and its equality-constrained form (Lemma 4.6.1), the saddle-point value identity (Lemma 4.6.2), the reduction of the Lagrange problem $P(\lambda)$ to $QP(b)$ (Lemma 4.6.3), the boundedness of $(d_n)$ (Lemma 4.6.4), and $QP(b)$'s own explicit solution (Theorem 4.6.5) — the four-step argument the goal theorem is the payoff of. Upstream of §4.6: the transaction-cost model's upper bounding function (Proposition 4.5.1), its Structure Assumption via buy/hold/sell decision rules (Proposition 4.5.2), and the resulting explicit three-region optimal policy (Theorem 4.5.4). Downstream: the Two-Fund Theorem (Corollary 4.6.7), and the parallel mean-risk development — the auxiliary problem $P(\lambda,b)$'s solution (Theorem 4.7.1), the binomial value of $P(\lambda)$ (Proposition 4.7.2), and the mean-risk problem's own explicit solution in both orderings of $p$ and $q$ (Theorems 4.7.3 and 4.7.4).

Significance

Theorem 4.6.6 is the multiperiod extension of the single most-used result in portfolio theory: the mean-variance efficient frontier, here derived stage by stage rather than assumed static, and it recovers the classical Two-Fund Theorem (every investor holds the same risky portfolio, scaled by wealth) as an immediate corollary rather than a separate argument. The transaction-cost results answer a standing objection to frictionless portfolio theory by showing that its qualitative conclusions — a threshold trading rule derived from a value function via the same abstract Structure Theorem — survive costs, with the thresholds now depending on the current value function rather than being fixed. The mean-risk results extend the whole technique to a risk measure that, unlike variance, is coherent in the sense of Artzner et al., showing the Lagrangian-embedding method is not an accident of the quadratic case.

None of this chapter's results have machine-checked proofs on Prove2Me at the time of writing (the platform's saddle-point sufficiency results, VectorSpaceOpt.lagrangian_saddle_sufficient_pointed and ConvexOptimization.lagrangian_saddle_iff_strong_duality, are stated over a closed convex cone in a normed vector space, not over the finite-horizon admissible-policy space $F^N$ that Lemma 4.6.2 needs, and were checked and ruled out as reusable for this mission). Formalizing this chapter means building the Lagrangian-embedding argument for a dynamic (rather than static) optimization problem from scratch: no existing platform infrastructure covers a saddle point of a Lagrangian defined over a sequence of Markov policies.

Difficulty

The obvious first attempt at (MV) is to apply the Structure Theorem of chunk 02a directly to the variance objective, exactly as chunk 04a does for expected utility. This fails outright: $\mathrm{Var}_{x_0}^\pi[X_N] = \mathbb{E}_{x_0}^\pi[X_N^2] - (\mathbb{E}_{x_0}^\pi[X_N])^2$ is not additive over time and has no Bellman recursion of the usual form, because the square of an expectation over the whole horizon cannot be decomposed into a sum of one-period rewards. The chapter's actual route — Lagrangian relaxation to $P(\lambda)$, then a further reduction to the quadratic (and hence tractable) $QP(b)$ — is not a shortcut around this obstacle but the only way the mean-variance problem admits a Markov Decision Process reformulation at all. A correct formalization of the goal theorem must go through this exact chain (saddle_point_value, plambda_implies_qp, qp_solution), not around it.

Formalization scope

The financial market and the four named optimization problems (MV), (MV=), $P(\lambda)$, $QP(b)$ are formalized as explicit structures and Prop-valued predicates in MDPFinance.MeanVariance (none of them is a numbered definition in the book — each is introduced only in prose — so each gets its own precise Lean definition rather than being left implicit). Wealth is real-valued, policies are sequences of measurable Markov maps $\mathbb{N}\to\mathbb{R}\to(\mathrm{Fin}\ d\to \mathbb{R})$, and values that can be $\pm\infty$ in the book (the value of $P(\lambda,b)$, of $P(\lambda)$, and of (MR) itself) are typed EReal rather than ℝ, matching the book's own use of infinite values as legitimate outcomes rather than failure states. A formalization that solved the goal theorem by first proving a Bellman equation for $\mathrm{Var}_{x_0}^\pi[X_N]$ directly would not be proving Theorem 4.6.6 — no such recursion exists — and the goal statement is phrased purely in terms of IsOptimalMV, varXN, and meanXN, independent of any intermediate value function, precisely so that only the actual saddle-point argument can discharge it. The transaction-cost model's buy/hold/sell threshold functions $q^-(V_{n+1}),q^+(V_{n+1})$ are represented by their defining maximizing property rather than a closed form, since the book itself only pins them down as an argmax. Reusable beyond this mission: the MVMarket/ MeanRiskMarket structures and the Lagrangian-saddle-point machinery are natural substrate for any later mission that needs a dynamic risk-constrained portfolio problem. Contributions completing any milestone's sorry are welcome, particularly a sorry-free proof of Lemma 4.6.2 (the saddle-point value identity), since it is the one genuinely general technique this mission introduces.

Selected references

• H. Markowitz, Portfolio Selection, The Journal of Finance 7(1), 1952, https://doi.org/10.2307/2975974
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999, https://doi.org/10.1111/1467-9965.00068
• N. Bäuerle, U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011, https://doi.org/10.1007/978-3-642-18324-9, Chapter 4, §§4.5-4.7

Motivation

Once a finite-horizon Markov Decision Model (MDM) is known to admit an optimal policy — the existence theory of continuity/compactness models — a natural next question is qualitative: does the optimal value function inherit structural properties (monotonicity, concavity, convexity) of the model's own data, and are the resulting optimal actions themselves monotone in the state? These questions matter beyond aesthetics. A value function known in advance to be concave in wealth, say, restricts the search for an optimizer to a much smaller, better-behaved class of candidates, simplifies numerical solution (dynamic programming over convex functions can exploit shape-preserving approximation schemes), and is often the only handle available for comparative-statics questions — e.g. "if the model's transition mechanism becomes riskier, does the decision-maker's value go down?" — the kind of question that drives applications in inventory theory, insurance, and portfolio choice. The general theory traces to Topkis's lattice-programming approach to comparative statics (Topkis, Supermodularity and Complementarity, Princeton University Press, 1998) and to the stochastic-orders literature (Müller and Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002); Bäuerle and Rieder's Chapter 2, §2.4.4-2.4.5 specializes both to the Borel-space finite-horizon Markov Decision Model of their own Definition 2.1.1.

Setting

Fix a (non-stationary) Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ as in Definition 2.1.1: $E$, $A$ measurable spaces, $D_n \subseteq E \times A$ the admissible state-action pairs, $Q_n(\cdot\mid x,a)$ the transition kernel, $r_n$ the one-stage reward, $g_N$ the terminal reward. Write $D_n(x) := \{a \in A : (x,a) \in D_n\}$. An upper bounding function $b : E \to \mathbb{R}_{\geq 0}$ (Definition 2.4.1) is a measurable function for which constants $c_r, c_g, \alpha_b \geq 0$ exist with $r_n^+(x,a) \leq c_r\, b(x)$, $g_N^+(x) \leq c_g\, b(x)$, and $\int b(x')\,Q_n(dx'\mid x,a) \leq \alpha_b\, b(x)$ for all admissible $(x,a)$ and all $n$; $\mathbb{I\!B}_b^+$ is the set of measurable $v : E \to [-\infty,\infty)$ with $v^+ \leq c\, b$ for some $c \geq 0$. The two central operators are $(L_n v)(x,a) := r_n(x,a) + \int v(x')\,Q_n(dx'\mid x,a)$ and $(T_n v)(x) := \sup_{a \in D_n(x)} (L_n v)(x,a)$; a decision rule $f_n$ is a maximizer of $v$ at time $n$ if $(L_n v)(x, f_n(x)) = (T_n v)(x)$ for every $x$. The Structure Assumption (SAN) on families $(\mathrm{I\!M}_n)_{n \leq N} \subseteq \mathrm{I\!M}(E)$ and $(\Delta_n)_{n<N}$ of decision rules says: $g_N \in \mathrm{I\!M}_N$; $v \in \mathrm{I\!M}_{n+1}$ implies $T_n v \in \mathrm{I\!M}_n$; and every $v \in \mathrm{I\!M}_{n+1}$ has a maximizer in $\Delta_n$. It is the single hypothesis from which the whole finite-horizon theory — a well-defined Bellman recursion, an optimal policy built rule-by-rule — follows (established elsewhere in this mission series).

For this section only, $E \subseteq \mathbb{R}^d$ and $A \subseteq \mathbb{R}^m$ carry the usual componentwise order, and the same spaces are given a real vector-space structure when convexity statements are in play; $\mathbb{I\!M}_n^{\diamond}$ denotes $\{v \in \mathbb{I\!B}_b^+ : v$ has property $\diamond\}$ for $\diamond \in \{\text{increasing}, \text{concave}, \text{convex}\}$. A set $D \subseteq E \times A$ is completely monotone (Definition 2.4.15) if $(x,a'), (x',a) \in D$ with $x \leq x'$, $a \leq a'$ forces $(x,a), (x',a') \in D$. A function $f$ on a lattice is supermodular (Definition A.3.1) if $f(x) + f(y) \leq f(x \wedge y) + f(x \vee y)$ for all $x,y$. The comparison theorem below additionally uses three orders between probability measures: the usual stochastic order $\mu \leq_{\mathrm{st}} \nu$ ($\int f\,d\mu \leq \int f\,d\nu$ for every bounded increasing $f$, Definition B.3.2/Theorem B.3.3(ii)), the convex order $\mu \leq_{\mathrm{cx}} \nu$ (same, for convex $f$, Definition B.3.9a), and its concave-function dual $\mu \leq_{\mathrm{cv}} \nu$ (matching $\mathrm{I\!M}_n^{\mathrm{cv}}$; see the Formalization scope section on how the book's own, non-monotone "cv" differs from the increasing-concave order $\leq_{\mathrm{icv}}$ it also uses elsewhere, e.g. in Definition B.3.9c).

Formalization targets

Goal — Theorem 2.4.22 (the convex structure theorem)

$$\begin{aligned} &\text{If } E \text{ is convex}, D_n = E \times A, \text{ and for every } n: \\ &\quad\text{(ii) } x \mapsto \textstyle\int v(x')\,Q_n(dx'\mid x,a) \text{ is convex for every convex } v \in \mathbb{I\!B}_b^+, a \in A,\\ &\quad\text{(iii) } x \mapsto r_n(x,a) \text{ is convex for every } a, \quad \text{(iv) } g_N \text{ convex},\\ &\quad\text{(v) every convex } v \in \mathbb{I\!B}_b^+ \text{ has a maximizer in } \Delta_n,\\ &\text{then } \bigl(\mathrm{I\!M}_n^{\mathrm{cx}}\bigr)_{n \leq N} \text{ and } (\Delta_n)_{n<N} \text{ satisfy (SAN).} \end{aligned}$$

This is the weakest stable statement: it names exactly the compatibility conditions between the kernel, reward, and terminal payoff that propagate convexity through $T_n$, without committing to any particular model beyond them.

Six further results of the same section are formalized as milestones on the way to, or alongside, the goal: the monotone (increasing) analogue (Theorem 2.4.14), the accompanying result that a largest maximizer under a supermodular $L_n v$ on a completely monotone $D_n$ is itself weakly increasing (Proposition 2.4.16), the concavity-preservation step for $T_n$ and its structure theorem (Proposition 2.4.18, Theorem 2.4.19), the convexity-preservation step together with the existence of a bang-bang maximizer when $A$ is a polytope (Proposition 2.4.21), and the comparison theorem for two models whose kernels are ordered (Theorem 2.4.23).

Significance

Theorems 2.4.14/2.4.19/2.4.22 give three parallel, reusable templates: once a modeler checks three or four structural conditions on $D_n$, $Q_n$, $r_n$, $g_N$ individually — never on the recursively-defined value function itself, which is usually inaccessible in closed form — the corresponding shape of the value function is guaranteed for every horizon, with no further induction needed by the modeler. This is what makes results like the concavity of the optimal consumption-investment value function (used in later chapters of this book) checkable from the market model alone. Proposition 2.4.16's comparative-statics conclusion (optimal actions inherit monotonicity in the state) is the Markov-decision-process incarnation of Topkis's monotone comparative statics, and Theorem 2.4.23 formalizes the intuitive but non-trivial fact that making the transition mechanism "worse" in a precise stochastic-order sense can only lower the optimal value — a comparison that requires the compatibility between the order and the very shape (monotonicity/concavity/convexity) the Structure Assumption already pins down.

All of these results, including the goal, are unformalized on the platform prior to this mission: no result matching "supermodular", "completely monotone", "comparative statics", or a Borel-space convex Markov decision model was found in a platform search at drafting time. The proofs themselves are short (Bäuerle and Rieder give complete, self-contained arguments for every result in this section), so what this mission contributes is the formal statement — getting the exact quantifiers and hypothesis set right in a general Borel/vector-space setting — rather than a technically deep proof; the sorry-free companion proofs are left as the formalization task.

Difficulty

The obvious first idea for the goal is to prove convexity of $T_n v$ by convexity of a supremum of convex functions — true only when $D_n(x)$ does not itself depend on $x$ in a way that mixes domains under a convex combination. The book's own hypothesis (i), $D_n := E \times A$ (constant), is exactly what rules out the general case and makes the argument work: for a genuinely $x$-dependent $D_n(x)$, a convex combination $\alpha(x,a) + (1-\alpha)(x',a')$ need not even have its action component available at the combined state, so "supremum of convex functions is convex" does not apply termwise. A second trap is treating $\mathrm{I\!M}_n^{\mathrm{cv}}$ (closed under concave, not-necessarily-increasing $v$) as if it required the stronger increasing-concave order $\leq_{\mathrm{icv}}$ that the appendix's Definition B.3.9c actually names — the two are different relations, and only the plain "concave-test-function" order is compatible with $\mathrm{I\!M}_n^{\mathrm{cv}}$ as stated (see Formalization scope).

Formalization scope

Because Mathlib's ConvexOn/ConcaveOn require a Module ℝ structure on the codomain, and EReal (needed for value functions that may equal $-\infty$) carries no such structure, this mission introduces ConvexOnEReal/ConcaveOnEReal: the same defining inequality with the real convex-combination coefficients cast into EReal and multiplied there (EReal does carry a Mul). Real-valued convexity/concavity of $r_n$ and $g_N$ uses Mathlib's own ConvexOn/ ConcaveOn directly. "Vertex of a polytope" (Proposition 2.4.21) is formalized via Mathlib's Set.extremePoints, and "$A$ is a polytope" as compact, convex, with finitely many extreme points. The comparison theorem's order $\leq_{\mathrm{cv}}$ has no verbatim numbered definition in the book: Appendix B.3 defines the stochastic order $\leq_{\mathrm{st}}$ (Definition B.3.2, via CDFs, with the increasing-test-function characterization given as an equivalent condition, Theorem B.3.3(ii)) and the convex order $\leq_{\mathrm{cx}}$ (Definition B.3.9a, directly via $\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for convex $f$), but never a bare "$\leq_{\mathrm{cv}}$" — only the increasing-concave order $\leq_{\mathrm{icv}}$ (Definition B.3.9c). This mission defines $\leq_{\mathrm{cv}}$ as the direct concave-test-function analogue of $\leq_{\mathrm{cx}}$ ($\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for every concave $f$), matching the book's own $\mathrm{I\!M}_n^{\mathrm{cv}}$ (plain concavity, not required to be increasing) and consistent with the standard "st/cv/cx" triple of Müller and Stoyan (2002), the reference the book cites for this whole appendix section. Likewise $\leq_{\mathrm{st}}$ is formalized directly via Theorem B.3.3(ii)'s functional characterization (bounded increasing test functions) rather than the CDF definition, since Theorem 2.4.23 compares kernels on a general $E \subseteq \mathbb{R}^d$ rather than real-valued random variables. The value function $V_n$ used only in the comparison theorem is given by its recursive characterization ($V_N = g_N$, $V_n = T_n V_{n+1}$, established as this series' Theorem 2.3.8) rather than by re-deriving the sup-over-policies primitive definition and its supporting history/policy machinery, which is not otherwise needed in this mission.

A trivializing formalization is ruled out: taking $E := \mathbb{R}$ throughout would make hypothesis (i) ("$E$ is convex") vacuously true and hide the genuinely restrictive role $D_n = E \times A$ plays in the proof; this mission keeps $E$ (and $A$) as general real vector spaces (with a Preorder added only where monotonicity, rather than convexity, is at stake), so the convexity hypotheses carry their full content. Reusable infrastructure: ConvexOnEReal/ConcaveOnEReal (any later chunk needing shape-preservation results for EReal-valued value functions can reuse the same pattern, restated per this series' convention), and the LEStochasticOrder/LEConcaveOrder/LEConvexOrder triple (reused, restated, by mission 04b's Theorems 4.4.4-4.4.5 and mission 05b's Definition 5.4.9, which need the same or a closely related order). sorry-free proofs of the milestones (all short in the book) are welcome contributions.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.
• A. Müller and D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.

Motivation

The finite-horizon theory of chunk 02a-model-bellman-equation (Bäuerle and Rieder's Theorem 2.3.8, the Structure Theorem) reduces the existence of an optimal policy and the validity of the Bellman equation to a single abstract hypothesis: the Structure Assumption (SAN), the existence of function classes $\mathrm{IM}_n$ and decision-rule classes $\Delta_n$ closed under the one-step optimality operator $T_n$. That theorem does not say when (SAN) actually holds for a given Markov Decision Model — checking it directly from the definition would require exhibiting, for every value function that could arise, both its regularity and a measurable action attaining its supremum, an infinite regress. This mission formalizes the classical resolution: sufficient conditions on the primitive data of the model (the admissible-action correspondence, the transition kernel, the one-stage reward) under which (SAN) is guaranteed, so that Theorem 2.3.8 becomes usable in practice rather than merely an existence statement.

Setting

Fix a Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ (chunk 02a's Definition 2.1.1), now with $E$, $A$ Borel spaces. A measurable $b : E \to \mathbb{R}_+$ is an upper bounding function (Definition 2.4.1) if $r_n^+(x,a) \le c_r b(x)$, $g_N^+(x) \le c_g b(x)$, and $\int b(x')\, Q_n(dx' \mid x,a) \le \alpha_b b(x)$ for constants $c_r, c_g, \alpha_b \ge 0$; write $\mathrm{IB}_b^+$ for the value functions of weighted growth at most $c\, b$ for some $c$. A set-valued map $x \mapsto D(x)$ is upper semicontinuous if $x_n \to x$ and $a_n \in D(x_n)$ force $(a_n)$ to have an accumulation point in $D(x)$ (Definition A.2.1); it is continuous if also every point of $D(x)$ is approximated by a sequence from the $D(x_n)$.

Formalization targets

Goal: Theorem 2.4.13

Suppose the model has an upper bounding function $b$, and for every $n < N$: (i) $D_n(x)$ is compact for every $x$; (ii) $a \mapsto \int v(x')\, Q_n(dx' \mid x,a)$ is upper semicontinuous on $D_n(x)$ for every $v \in \mathrm{IB}_b^+$ and every $x$; (iii) $a \mapsto r_n(x,a)$ is upper semicontinuous on $D_n(x)$ for every $x$. Then $\mathrm{IM}_n := \mathrm{IB}_b^+$, $\Delta_n := F_n$ satisfy (SAN). Unlike the two milestone theorems that precede it in the chapter (Theorem 2.4.6 and Theorem 2.4.10, both of which also assume the correspondence $x \mapsto D_n(x)$ varies semicontinuously or continuously with $x$), Theorem 2.4.13 assumes nothing about $D_n(\cdot)$ as a set-valued map beyond pointwise compactness of each fiber $D_n(x)$; correspondingly it needs semicontinuity of the objective only in the action variable, at each state separately, and it recovers all of $\mathrm{IB}_b^+$ as the regularity class rather than a semicontinuous or continuous sub-class of it.

Milestones

Proposition 2.4.3 and Proposition 2.4.8 show, respectively, that $T_n$ preserves upper semicontinuity (resp. continuity) of $v$ and that a maximizer exists, when $D_n(x)$ is compact and $x \mapsto D_n(x)$ is upper semicontinuous (resp. continuous); Theorem 2.4.6 and Theorem 2.4.10 package these into concrete instances of (SAN). Lemma 2.4.7 gives a checkable criterion — weak continuity of the kernel $Q_n$ — for Theorem 2.4.6's integral-semicontinuity hypothesis. Proposition 2.4.11 drops all topological structure on $D_n(\cdot)$ itself, keeping only pointwise compactness of $D_n(x)$ plus semicontinuity of the objective in the action alone, and is what the goal theorem invokes directly, via a projection theorem of Kunugui and Novikov in place of the sequential compactness argument used for Proposition 2.4.3.

Significance

Compactness of the action set together with semicontinuity of the reward is the textbook Weierstrass mechanism for the existence of a maximizer in ordinary optimization; the content of this chapter is doing the same thing correctly when the maximization varies measurably over an uncountable state space $E$, so that the resulting maximizer is not just pointwise-optimal but a genuine decision rule (a measurable function of the state). No formalized version of this theory exists on the platform: BertsekasDP's existence theorems are for finite state-and-action-space models, where $D(x)$ is automatically compact (in the discrete topology) and every real-valued function on it is automatically semicontinuous, so none of this chapter's actual content — choosing a measurable maximizing selection as the state varies continuously — has any analogue there. This chunk earns the generalization rather than restating that finite-state prior art.

Difficulty

The three "compactness implies (SAN)" theorems of this chapter (2.4.6, 2.4.10, 2.4.13) trade regularity of the action correspondence $x \mapsto D_n(x)$ against regularity of the resulting value-function class: assuming more about how $D_n(\cdot)$ varies (continuity, in Theorem 2.4.10) buys a stronger conclusion (continuous, not merely upper semicontinuous, value functions); assuming nothing about $D_n(\cdot)$ beyond pointwise compactness (Theorem 2.4.13, the goal) forces the weakest conclusion, that the whole class $\mathrm{IB}_b^+$ is preserved, via a genuinely different, measure-theoretic argument (a projection theorem) rather than the sequential compactness argument common to Propositions 2.4.3 and 2.4.8. Formalizing all three side by side, rather than only the goal in isolation, is what exposes this trade-off as three logically independent theorems rather than one theorem instantiated three times, and is why every one of the section's numbered results is kept as an item of this mission (per the CAPTAIN's budget instruction to include, not cut, results of genuine independent content) rather than only the smallest set literally required by the goal's own proof tree.

Formalization scope

State and action spaces carry MeasurableSpace, TopologicalSpace, BorelSpace instances throughout (the section's own standing assumption that $E$, $A$ are Borel spaces), but no metrizability or separability instance is required beyond what each statement's own topology needs — sequences suffice for every semicontinuity notion used here, matching the book's own Appendix A, which is stated for metric spaces. The Markov Decision Model, its operators ($L_n$, $T_n$, $T_n^f$), the notion of a maximizer, and the Structure Assumption are restated from chunk 02a-model-bellman-equation in this mission's own MDPFinance.Semicontinuous namespace (drafts in this series cannot import one another). Set-valued upper/lower semicontinuity (Appendix A.2.1) is formalized with the book's own sequential definition, not Mathlib's neighborhood-filter-based UpperHemicontinuous/LowerHemicontinuous for correspondences — the book explicitly remarks that its own definition is "slightly more restrictive than other definitions appearing in the literature" (p. 351), so identifying the two without proof would silently substitute a different notion. The classes $\mathrm{IB}_b$, $\mathrm{IB}_b^+$ are formalized via the book's own equivalent bound-by-a-constant characterization rather than through the weighted supremum norm $\|\cdot\|_b$ itself, avoiding EReal division and its 0/0 := 0 convention for no loss of content. Each of Theorem 2.4.6's and Theorem 2.4.10's closing "in particular" sentences — restating chunk 02a's Theorem 2.3.8 applied to the (SAN) instance just constructed — is not repeated in this mission's Lean, since it is a corollary of a different chunk's goal, not new content of this section; only the "(SAN) is satisfied" conclusion that is this section's own contribution is stated. A trivializing formalization of the goal would specialize $A$ to a finite type or fix $D_n(x)$ to a single compact set independent of $x$, making hypotheses (i)-(iii) vacuous; this mission states the theorem for arbitrary Borel $A$ and a genuinely state-dependent $D_n(x)$.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
• C. J. Himmelberg, T. Parthasarathy, and F. S. Van Vleck, "Optimal plans for dynamic programming problems", Mathematics of Operations Research 1 (1976), 390-394.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors", Bulletin de l'Académie Polonaise des Sciences 13 (1965), 397-403.

Motivation

A Markov Decision Model (MDM) formalizes sequential decision-making under uncertainty: a controller observes the current state of a system, chooses an action, receives a reward, and the system moves to a new (random) state whose law depends on the current state and action. This framework underlies dynamic programming across operations research, economics, and engineering — inventory control, sequential portfolio choice, queueing control, and reinforcement learning are all instances of it. The finite-horizon theory developed here is the foundation on which every later chapter of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds, including the infinite-horizon, partially observed, and optimal-stopping variants treated later in the book.

The classical treatment of dynamic programming for finite state and action spaces goes back to Bellman (1957) and is standard textbook material (see e.g. Puterman, Markov Decision Processes, 1994). The generalization to Borel state and action spaces — needed as soon as a state variable is continuous, as in almost every financial application — requires genuine measure-theoretic care: suprema over an infinite (even uncountable) action set need not be attained, and the resulting value function need not be measurable. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete Time Case (1978) is the classical reference for this general theory; Bäuerle and Rieder's treatment isolates the exact abstract hypothesis — the Structure Assumption (SAN) below — under which the finite-horizon theory goes through cleanly, separating the recursive (Bellman) machinery from the case-by-case verification of when it applies.

Setting

A Markov Decision Model with planning horizon $N \in \mathbb{N}$ consists of a state space $E$ and action space $A$ (measurable spaces), and, for each stage $n = 0,\dots,N-1$: a measurable set $D_n \subseteq E \times A$ of admissible state-action pairs (containing the graph of some measurable selection $E \to A$); a stochastic transition kernel $Q_n(\cdot \mid x,a)$ giving the law of the next state; a measurable one-stage reward $r_n : D_n \to \mathbb{R}$; and a terminal reward $g_N : E \to \mathbb{R}$.

A decision rule at time $n$ is a measurable $f_n : E \to A$ with $f_n(x) \in D_n(x) := \{a : (x,a) \in D_n\}$ for every $x$; an $N$-stage policy $\pi = (f_0,\dots,f_{N-1})$ is a sequence of such rules. Given $\pi$ and an initial state $x$ at time $n$, the process evolves as a (non-stationary) Markov chain, and the value of $\pi$ is the expected total reward

$$V_n^\pi(x) := \mathbb{E}^\pi_{n,x}\!\left[\sum_{k=n}^{N-1} r_k\bigl(X_k, f_k(X_k)\bigr) + g_N(X_N)\right],$$

with value function $V_n(x) := \sup_\pi V_n^\pi(x)$, the best attainable expected reward. A policy is optimal if $V_0^\pi = V_0$. Write $\mathrm{IM}(E)$ for the measurable functions $E \to [-\infty,\infty)$ (never $+\infty$), and define, for $v \in \mathrm{IM}(E)$, the one-step operators $L_n v(x,a) := r_n(x,a) + \int v(x')\, Q_n(dx' \mid x,a)$, $T_n^f v(x) := L_n v(x, f(x))$, and $T_n v(x) := \sup_{a \in D_n(x)} L_n v(x,a)$. A decision rule $f$ is a maximizer of $v$ at time $n$ if $T_n^f v = T_n v$.

Formalization targets

Goal: Theorem 2.3.8 (the Structure Theorem)

Under the Structure Assumption (SAN) — the existence of sets $\mathrm{IM}_n \subseteq \mathrm{IM}(E)$, $\Delta_n \subseteq F_n$ with $g_N \in \mathrm{IM}_N$, $T_n$ mapping $\mathrm{IM}_{n+1}$ into $\mathrm{IM}_n$, and every $v \in \mathrm{IM}_{n+1}$ admitting a maximizer in $\Delta_n$ — the value function satisfies the Bellman equation $V_n = T_n V_{n+1}$ (with $V_n \in \mathrm{IM}_n$), and every sequence of maximizers of $V_1,\dots,V_N$ defines an optimal policy. This is the weakest level at which the theorem holds: it names an abstract structural hypothesis rather than a specific sufficient condition (e.g. compactness plus semicontinuity, treated in a later mission), so any future refinement of sufficient conditions for (SAN) leaves this statement untouched.

Significance

Reducing an $N$-stage optimization over an infinite-dimensional policy space to $N$ one-stage optimizations — literally the content of the Bellman equation — is what makes dynamic programming computationally and theoretically tractable at all. For finite state and action spaces this reduction is elementary (a supremum over a finite set is always attained); the content of the Structure Theorem is doing this correctly when $E$, $A$ are general Borel spaces, where existence of the supremum and of a measurable maximizing selection are not automatic and must be assumed abstractly.

Formalizing this theorem produces machine-checked statements of the finite-horizon Bellman equation and verification theorem in the generality actually used throughout the book's finance applications (wealth is real-valued, portfolios are vector-valued — never finite sets). The statement, proof, and every hypothesis are original to this textbook chapter; no formalized version of this general-Borel-space theory exists on the platform. The closest prior art, finite state-and-action-space Bellman equations and verification theorems (e.g. discounted infinite-horizon and stochastic-shortest-path theorems for finite MDPs), is a strictly weaker special case in which the Structure Assumption's existence-of-maximizer clause is automatic; this mission's goal is not restated as a reference to that prior art; the generalization is exactly the mission's content.

Difficulty

The obvious first attempt — prove $V_n = T_n V_{n+1}$ directly from the definitions of $V_n$ and $V_n^\pi$ — runs into two separate obstructions that (SAN) is built to bypass simultaneously. First, $\sup_\pi V_n^\pi(x)$ and $\sup_{a \in D_n(x)} L_n V_{n+1}(x,a)$ are a priori different suprema (over policies versus over actions), and showing they agree requires that the pointwise supremum over decision rules $f \in F_n$ of $L_n V_{n+1}(x, f(x))$ equals the supremum over bare actions $a \in D_n(x)$ — which needs a measurable selection achieving (or approaching) the action-wise optimum, not just its existence pointwise. Second, $V_{n+1}$ itself must be shown measurable — an a priori supremum of measurable functions over an uncountable index set (all policies) need not be measurable — before the integral $\int V_{n+1}\, dQ_n$ even makes sense. (SAN)'s three clauses are exactly what supplies both a well-behaved measurability class $\mathrm{IM}_n$ closed under $T_n$ and a measurable maximizing selection at every stage, letting a backward induction on $n$ establish both facts together.

Formalization scope

State and action spaces are arbitrary measurable spaces (MeasurableSpace E, MeasurableSpace A type classes), not restricted to Borel subsets of Polish spaces, since none of this mission's statements use topology. Time is indexed by ℕ rather than Fin N, with n < N as an explicit side condition throughout (documented in MODERATION_NOTES.md); this changes no content but avoids Fin-cast noise in the several backward recursions the chapter's operators require. Extended-real values (EReal) are used throughout for value functions, restricted by hypothesis to never equal $+\infty$, matching $\mathrm{IM}(E) := \{v : E \to [-\infty,\infty)\}$ exactly; a formalization using plain ℝ-valued value functions would be a strictly stronger — and unfaithful — claim, since it silently assumes no policy can drive the expected reward to $-\infty$.

The mission does not construct the canonical path measure on the full trajectory space via the Ionescu–Tulcea theorem; the value of a policy is instead built as an explicit backward accumulator recursion over the model's one-step kernels, which computes the same quantity by the tower property of conditional expectation. Definitions 2.1.1, 2.1.5, 2.2.2, 2.3.1, and 2.3.6 — the Markov Decision Model, (Markov and history-dependent) policies, and the operators — are restated from scratch in this mission's own namespace, since drafts in this series cannot import one another; later missions in the same series restate the same vocabulary independently. A trivializing formalization of the goal would state $V_n$ as an unspecified object merely postulated to satisfy the Bellman equation (Theorem 2.3.7's weaker claim) rather than as the supremum-over-policies value function fixed before the theorem — this mission states the latter.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
• K. Hinderer, Foundations of Non-stationary Dynamical Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994.

Motivation

An inventory manager who stocks many products, faces random demand and pays ordering, holding and shortage costs must decide each period how much of each product to order. In general the optimal decision depends on the whole state and is found by solving a dynamic programme, which becomes impractical as the number of products grows. Myopic (or base stock) policies avoid this: in each period they aim at a target level computed from that period's data alone. Knowing when such a policy is optimal over an infinite horizon tells a practitioner when the multi-period problem decouples into a sequence of one-period problems.

Arthur F. Veinott, Jr. gave such conditions in Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem (Management Science 12(3):206–222, 1965). Earlier results of this type were for a single product (the paper cites Karlin, Management Science 6(3), 1960, Bellman–Glicksberg–Gross, Management Science 2(1), 1955, Iglehart–Karlin 1962, and the Arrow–Karlin–Scarf volume of 1958); Veinott's model allows several products, several demand classes, costs and demand distributions that change over time, general ordering constraints and general stock dynamics (backlogging, lost sales, and mixtures), and it does not use the functional equation of dynamic programming. Instead, the proofs analyse the inventory process directly.

Setting

There are $n$ products and $m$ demand classes. Vectors are compared componentwise: $u \le v$ means $u_j \le v_j$ for all $j$. In period $i = 1, 2, \dots$ the manager observes the inventory vector $x_i \in X_i \subseteq \mathbb{R}^n$ (negative coordinates are backlogs) and orders up to a vector $y_i \in Y_i \subseteq \mathbb{R}^n$, subject to $y_i \ge q_i(x_i)$, where $q_i$ is a vector of extended-real functions (for instance $q_i(x) = x$ forbids disposal). A random demand vector $D_i$ with law $\Phi_i$ and values in a Borel set $\mathfrak{D}_i \subseteq \mathbb{R}^m$ then occurs, and the next inventory vector is $x_{i+1} = s_i(y_i, D_i) \in X_{i+1}$. The demands $D_1, D_2, \dots$ are independent. Ordering $y_i - x_i$ costs $c_i \cdot (y_i - x_i)$, the holding and shortage cost is $g_i(y_i, D_i)$, and $\alpha_i \ge 0$ is the discount factor of period $i$.

Regrouping the ordering costs gives the one-period cost

$$W_i(y,t) = c_i\, y + g_i(y,t) - \alpha_i\, c_{i+1}\, s_i(y,t), \qquad G_i(y) = \int_{\mathfrak{D}_i} W_i(y,t)\, d\Phi_i(t),$$

with discount weights $\beta_1 = 1$ and $\beta_i = \alpha_1 \cdots \alpha_{i-1}$. The integrals are assumed finite, and $G_i \ge \gamma_i$ with $\sum_i |\beta_i \gamma_i| < \infty$. An ordering policy $\bar Y$ chooses $y_i$ as a Borel function of the past; it is feasible if $y_i \in Y_i$ and $y_i \ge q_i(x_i)$ for every possible history. Its cost is

$$f(x_1 \mid \bar Y) = \sum_{i=1}^\infty \beta_i\, E\, G_i(y_i) \in (-\infty, +\infty],$$

and a feasible policy of least cost is optimal.

Let $\bar y_i$ minimize $G_i$ over $Y_i$. When $\bar y_i$ is not attainable from $x$, the minimal feasible level $w_i(x)$ is the least element of $Y_i \cap \{y : y \ge q_i(x),\ y \ge \bar y_i\}$. The base stock ordering policy orders up to $\bar y_i$ if $q_i(x_i) \le \bar y_i$ and up to $w_i(x_i)$ otherwise.

Formalization targets

The hypotheses are: (3a) $\bar y_i \in Y_i$ minimizes $G_i$ over $Y_i$; (3b) $q_{i+1}(s_i(\bar y_i, t)) \le \bar y_{i+1}$ for $t \in \mathfrak{D}_i$; (3c) $Y_i$ is closed and linearly ordered by $\le$; (3d) $G_i$ and $s_i(\cdot, t)$ are nondecreasing on $\{y \in Y_i : y \ge \bar y_i\}$, and $q_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$.

Goal: Theorem 3.2

Under (3a)–(3d), the base stock ordering policy

$$\bar Y_i^*(H_i^*) = \begin{cases} \bar y_i, & q_i(x_i^*) \le \bar y_i, \\ w_i(x_i^*), & q_i(x_i^*) \not\le \bar y_i \end{cases}$$

is feasible and optimal: $f(x_1 \mid \bar Y^*) \le f(x_1 \mid \bar Y)$ for every feasible $\bar Y$.

Milestones

1. A nonempty, closed, linearly ordered, bounded-below subset of $\mathbb{R}^n$ has a least element (p. 212); hence $w_i(x)$ exists and equals $\bar y_i$ when $q_i(x) \le \bar y_i$.
2. $w_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$ (p. 214).
3. Once $q_k(x_k^*) \le \bar y_k$, the base stock policy orders up to $\bar y_i$ for all $i \ge k$.
4. Theorem 3.1: under (3a) and (3b), if $q_1(x_1) \le \bar y_1$, ordering up to $\bar y_i$ in every period is optimal, with cost $\sum_i \beta_i G_i(\bar y_i)$.
5. The coupling (3.1): before the first period $T$ with $q_T(x_T^*) \le \bar y_T$,

$$\bar y_i < y_i^* = w_i(x_i^*) \le w_i(x_i) \le y_i.$$

6. Pathwise dominance: $G_i(y_i^*) \le G_i(y_i)$ for every $i$ and every possible demand path.
7. The reduction behind (2.3): $E\, W_i(y_i, D_i) = E\, G_i(y_i)$, by independence of $y_i$ and $D_i$.

Significance

The theorem shows that under (3a)–(3d) the infinite-horizon, nonstationary, multi-product problem is solved by one-period optimization: compute $\bar y_i$ from $G_i$ alone, and when it is unreachable order the least feasible amount. No value function is computed. It covers backlogging and lost sales, products stocked in fixed proportions, and time-varying cost and demand data, and Theorem 3.1 alone settles the frequent case in which the initial stock is small.

The result is proved in the paper. To our knowledge it has not been machine-checked: this mission produces a Lean model of a general stochastic, infinite-horizon, multi-product inventory problem (feasible policies, the expected discounted cost with $+\infty$ allowed), and a checked proof that a myopic policy is optimal in it. The model and its cost are reusable for other base stock and myopic optimality results.

Difficulty

The obvious argument would compare the base stock policy with an arbitrary policy period by period using (3a) alone. That fails once $\bar y_i$ is unreachable. The base stock policy then holds less stock than $\bar y_i$ would require, and it has to be shown that no other policy can reach a lower-cost level later. The proof couples the two trajectories along every demand path, using the monotonicity in (3d) and the linear order of $Y_i$ from (3c), until the base stock level becomes attainable, after which (3b) keeps it attainable. The formal difficulties are:

• the existence and monotonicity of the least element $w_i(x)$ in a closed chain of $\mathbb{R}^n$;
• the measurability of the base stock policy, which is part of its feasibility;
• the passage from pathwise dominance to the expected discounted cost when the cost may be $+\infty$.

Formalization scope

Periods are 0-based in Lean (Lean period $k$ is the paper's period $k+1$). Vectors are Fin n → ℝ with the product order; $q_i$ takes values in Fin n → EReal. Policies are functions of the past demands. The paper shows on p. 219 that this loses no generality once $x_1$ is fixed. The cost is excess, a $[0,\infty]$-valued series of lower Lebesgue integrals of $\beta_i(G_i(y_i) - \gamma_i)$, plus the finite real $\sum_i \beta_i\gamma_i$, taken in EReal. A divergent series therefore gives $+\infty$ and never the junk value $0$. "Minimal element" is IsLeast. The $G_i$ in the statements is the integral of $W_i$ built from the data, and the policy in the goal is constructed from $\bar y$, $q$, $w$ and $s$. Neither is an arbitrary object satisfying the conclusion. The goal concludes optimality, which includes feasibility: a pathwise or conditional statement would not be the theorem.

Hypotheses added relative to the page, each used by the paper without being stated:

• Order feasibility: from every $x \in X_i$ some $y \in Y_i$ with $y \ge q_i(x)$ exists (p. 212 asserts the set defining $w_i(x)$ has a minimal element, which needs it nonempty). The least-element lemma likewise assumes $A$ nonempty.
• (3d)'s $q$-clause in one-sided form: if $x \le x'$ in $X_i$ and $q_i(x) \not\le \bar y_i$, then $q_i(x) \le q_i(x')$. This is the form the proof on p. 214 uses; monotonicity on the region $\{q_i(x) \not\le \bar y_i\}$ alone admits a counterexample to Theorem 3.2.
• Integrability of $W_i(y_i, D_i)$ in the milestone $E W_i = E G_i$.
• Borel measurability of $q_i$ on all of $\mathbb{R}^n$ rather than on $X_i$ (a harmless strengthening).

A complete development needs: least elements of closed chains in $\mathbb{R}^n$; measurability of the least-element selection $x \mapsto w_i(x)$; a Fubini/independence argument for $E\,W_i(y_i,D_i)=E\,G_i(y_i)$; and monotone summation of lower integrals. The least-element lemma and the cost encoding are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments.

Selected references

• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• R. Bellman, I. Glicksberg, O. Gross, On the Optimal Inventory Equation, Management Science 2(1):83–104, 1955. https://doi.org/10.1287/mnsc.2.1.83
• S. Karlin, Dynamic Inventory Policy with Varying Stochastic Demands, Management Science 6(3):231–258, 1960. https://doi.org/10.1287/mnsc.6.3.231

Motivation

Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds $C_0$ units of a perishable product (airline seats, hotel rooms, seasonal goods) and must choose prices over a finite selling horizon while demand is random and responds to price. The exactly optimal policy solves a stochastic dynamic program whose state is the remaining inventory, and it changes the price after every sale. In practice sellers often prefer a simpler rule, fixed in advance: solve the deterministic version of the problem, in which random demand is replaced by its mean, and charge the resulting prices whatever happens.

Gallego and van Ryzin (Management Science 1994) showed that in continuous time with Poisson demand this fixed-price heuristic is asymptotically optimal, and bounded its relative loss by the coefficient of variation of demand. Bitran and Caldentey's survey (MSOM 2003, §3.2.1) extends this bound to a discrete-time, periodic-review model with general demand distributions, as Proposition 8, proved in the paper's Appendix. The proof combines three ingredients: a Lagrangian duality argument showing that the deterministic problem is an upper bound on the optimal expected revenue, a sample-path comparison of lost sales, and a distribution-free moment bound of Gallego (1992) on $E[(X-C)^+]$.

Setting

A single product is sold over $N \ge 1$ periods $n = 1, \dots, N$ starting from inventory $C_0$. In period $n$ the seller charges a price $p \ge 0$, and the demand $D_n(p)$ is a nonnegative random variable with finite mean $E[D_n(p)]$, whose law may depend on $n$ and $p$ arbitrarily. With inventory $C$ the seller sells $\min\{D, C\}$ units; unmet demand is lost.

The optimal expected revenue $V_1(C_0)$ is defined by the Bellman recursion $V_{N+1} \equiv 0$,

$$V_n(C) = \sup_{p \ge 0} E\big[p\min\{D_n(p), C\} + V_{n+1}\big(C - \min\{D_n(p), C\}\big)\big].$$

The deterministic problem (32)–(33) is

$$V_1^{\det}(C_0) = \sup_{p \in [0,\infty)^N} \sum_{n=1}^N p_n E[D_n(p_n)] \quad \text{subject to} \quad \sum_{n=1}^N E[D_n(p_n)] \le C_0,$$

and $p^{\det}$ denotes an optimal solution. The deterministic-price heuristic charges $p^{\det}_n$ in period $n$ regardless of sales. Its period demands $D_n(p_n^{\det})$ are independent, $\mathscr{D}_n^{\det} = \sum_{i=1}^n D_i(p_i^{\det})$ is the cumulative demand, and its expected revenue is

$$V_1(p^{\det}, C_0) = \sum_{n=1}^N p_n^{\det} E\Big[D_n(p_n^{\det}) - \big(D_n(p_n^{\det}) - (C_0 - \mathscr{D}_{n-1}^{\det})^+\big)^+\Big].$$

With $\sigma_n^2 = \operatorname{Var}(\mathscr{D}_n^{\det})$, eq. (34) defines

$$\eta_n^{\det}(C_0) = \frac{\sqrt{\sigma_n^2 + (C_0 - E[\mathscr{D}_n^{\det}])^2} - (C_0 - E[\mathscr{D}_n^{\det}])}{2},$$

and $\nu(C_0) = \sigma_N / E[\mathscr{D}_N^{\det}]$ is the coefficient of variation of the total demand.

Formalization targets

Goal: Proposition 8, eq. (35)

Assume that $p \mapsto p\,E[D_n(p)]$ is concave and $p \mapsto E[D_n(p)]$ is convex on $[0,\infty)$ for each $n$, that some price $p^\infty \ge 0$ has $\sum_n E[D_n(p^\infty)] < C_0$, and that $p^{\det}$ is optimal for (32)–(33). Then

$$1 \ge \frac{V_1(p^{\det}, C_0)}{V_1(C_0)} \ge \frac{1}{V_1^{\det}(C_0)} \sum_{n=1}^N p_n^{\det} E[D_n(p_n^{\det})]\left(1 - \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}\right) \ge 1 - \max_n \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}.$$

The constants are the paper's, and the goal is the full chain.

Milestones

1. Gallego's bound (Appendix, (*)): for square-integrable $X$, $E[(X - C)^+] \le \frac12\big(\sqrt{\operatorname{Var}X + (C - EX)^2} - (C - EX)\big)$, which is at most $\frac12\sqrt{\operatorname{Var} X}$ when $EX \le C$.
2. Eq. (24): in one period, $E[p\min\{D(p), C\}] \le p\min\{E[D(p)], C\}$, so $V(C) \le V^{\det}(C)$.
3. Proposition 6, eq. (26): in one period, $V(C, p^{\det})/V(C) \ge 1 - \nu^{\det}/2$.
4. $V_1^{\det}$ is concave in the capacity (first sentence of the Appendix proof).
5. Proposition 8, first assertion: $V_1(C_0) \le V_1^{\det}(C_0)$.
6. The Appendix display bounding $V_1(p^{\det}, C_0)$ below by $\sum_n p_n^{\det}E[D_n](1 - E[(\mathscr{D}_n^{\det} - C_0)^+]/E[D_n])$.
7. Eq. (36), after the goal: if $E[D_n(p)] = T_n\lambda(p)$, one constant price solves (32)–(33) and $1 \ge V_1(p^{\det},C_0)/V_1(C_0) \ge 1 - \nu(C_0)/2$.

Significance

The result gives a guarantee for a pricing policy that needs no inventory tracking: its relative loss is controlled by the first two moments of cumulative demand, with no distributional assumption beyond finite variance. When demand grows while its coefficient of variation shrinks, as for sums of independent period demands, the guarantee tends to one, which is the discrete-time form of asymptotic optimality of fixed prices. The upper bound $V_1 \le V_1^{\det}$ is used throughout revenue management as the benchmark for heuristics (fluid or deterministic LP bounds).

The paper's proof is complete in the Appendix, and the mathematics is not in question beyond minor typos. None of it is machine-checked. A formal development adds a checked Bellman model of periodic-review pricing with general demand laws, a checked fluid upper bound for it, and a checked form of Gallego's moment bound, all reusable for other revenue-management statements. A related platform theorem, RevenueManagement.deterministic_upper_bound (mission The Theory and Practice of Revenue Management III), states the deterministic bound for a Bernoulli-arrival model with at most one sale per period; the model here is different (arbitrary demand laws, continuous inventory), and neither statement implies the other.

Difficulty

The upper bound $V_1(C_0) \le V_1^{\det}(C_0)$ is the hard part. The natural induction replaces $V_2$ by $V_2^{\det}$ and applies Jensen's inequality, but $V_2^{\det}(C)$ is $-\infty$ at capacities where the remaining deterministic problem is infeasible, while $V_2(C)$ stays nonnegative. The induction therefore fails as stated when mean demand never vanishes. The paper's argument also passes through the Lagrangian dual of (32)–(33), and strong duality for that program on $[0,\infty)^N$ under the Slater point $p^\infty$ is not available in Mathlib in this form.

The lower bound is less deep but technical: it needs the product law of the period demands, linearity of expectation for truncated sums, and variances of partial sums. Gallego's inequality is elementary once the right quadratic bound on $(x - C)^+$ is found, but it is not in Mathlib.

Formalization scope

• Periods are Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by $[0,\infty)$ with finite mean, required at every price (laws at negative prices never enter a statement).
• The Bellman value is computed in $[0,\infty]$ with the lower Lebesgue integral and ⨆ over $p \ge 0$, so no supremum takes a junk value; the paper's $V_n$ is valueToGo M (N - n + 1). Ratios use its real value.
• $V_1^{\det}$ is an EReal supremum over the feasible set ($-\infty$ if infeasible). In the goal $p^{\det}$ is an optimal solution, so $V_1^{\det}(C_0)$ is its objective value.
• The heuristic's demands are independent: the joint law is the product measure.
• Implicit hypotheses made explicit: "concave objective and convex feasible region" is read as concavity of $p\,E[D_n(p)]$ and convexity of $E[D_n(p)]$ on $[0,\infty)$, the latter making (33) convex for every capacity; existence of the optimal deterministic solution; finite variance and positive mean of each $D_n(p_n^{\det})$; and $V_1^{\det}(C_0) > 0$, without which the ratios are $0/0$.
• The typo $\mathscr{D}_n^{\det} := \sum_{i=1}^n D_n(p^{\det})$ on p. 221 is read as $\sum_{i=1}^n D_i(p_i^{\det})$.

Trivializing formalizations ruled out: $V_1$ is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; $\eta_n^{\det}$ is the expression (34), not a hypothesis-supplied bound on expected overflow; the goal does not assume strong duality or a Lagrange multiplier, since that is the proof's key step; independence is built into the joint law, not assumed as an inequality; variances are taken only under square integrability, since Mathlib's variance is $0$ for infinite variance.

Needed infrastructure: measurability of the Bellman integrand (monotonicity of $V_n$ in inventory), Jensen's inequality for $\min\{\cdot, C\}$ (ConcaveOn.le_map_integral), Lagrangian strong duality for a separable concave program with one convex constraint, marginals and variances of sums under Measure.pi, and Gallego's bound. The duality and moment results are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the upper bound, are welcome.

Selected references

• G. R. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–230, 2003. https://doi.org/10.1287/msom.5.3.203.16061
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11(1):55–60, 1992 (as cited in Bitran and Caldentey 2003).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993.