Markov Decision Processes

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

An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of $N$ periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).

Setting

An investor with utility function $U : \mathrm{dom}\,U \to \mathbb{R}$ (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth $x$ invests in a bond (interest rate $i_{n+1}$ on $[n,n+1)$) and $d$ risky assets with relative risk $R_{n+1}$ (Chapter 3). The one-period problem: admissible investments $D(x) := \{a \in \mathbb{R}^d : (1+i)(x+a\cdot R) \in \mathrm{dom}\,U \text{ a.s.}\}$, $u(x,a) := \mathbb{E}[U((1+i)(x+a\cdot R))]$, $v(x) := \sup_{a \in D(x)} u(x,a)$. The multiperiod problem is the $N$-stage Markov Decision Model with state space $E := \mathrm{dom}\,U$ (wealth), action space $\mathbb{R}^d$, transition $T_n(x,a,z) = (1+i_{n+1})(x+a\cdot z)$, zero one-stage reward, terminal reward $g_N := U$; its value functions are $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[U(X_N)]$ over Markov portfolio strategies $\pi$.

Formalization targets

Goal — Theorem 4.2.2

$$V_N = U, \qquad V_n(x) = \sup_{a \in D_n(x)} \mathbb{E}\bigl[V_{n+1}\bigl((1+i_{n+1})(x+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave and continuous, and an optimal portfolio strategy $(f_0^*,\dots,f_{N-1}^*)$ realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.

Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).

Significance

Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.

No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for $d_n$, since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable ($x$, $x+bS^0_n/S^0_N$, or a wealth-independent constant) each uses.

Difficulty

The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if $v \in \mathrm{I\!M}_{n+1}$ [strictly increasing/concave/continuous with linear growth], then $v$ is a utility function on $E$ up to the growth bound, so Theorem 4.1.1 applies directly to $T_n v$." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.

Formalization scope

The multiperiod value function V is defined as an explicit supremum over admissible Markov portfolio strategies (not the Bellman recursion itself, and not full history-dependent strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than restatements of the value function's own definition. The one-period vocabulary (OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement matching §4.1's own notation (a single $i$, $R$, no time index), independent of chunk 03's full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the book (a concave function is dominated by an affine function; no-arbitrage bounds admissible actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather than re-derived, since re-deriving them is not this proposition's own content. HARA and power utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since their admissibility sets and objective functions genuinely differ (a strict vs. non-strict inequality; a fraction vs. an absolute amount).

No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for $d_n$ (a finite product or sum over $k=n,\dots,N-1$ of genuinely different per-stage terms) rather than a shared abstract "some sequence $d_n$ exists with $V_n = d_n \cdot (\text{shape})$" — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form ($f_n^*(x) = \alpha_n^* x$, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.

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
• R. C. Merton, "Lifetime portfolio selection under uncertainty: the continuous-time case", Review of Economics and Statistics, 1969 (the continuous-time analogue this discrete-time theory approximates, per Chapter 3's binomial-to-Black-Scholes convergence result).

Motivation

Real investors do not merely accumulate wealth for a single terminal payoff; they consume along the way, and the market they invest in is rarely a single fixed statistical regime for years at a time — bull and bear markets, business cycles, and volatility regimes shift the distribution of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem), and §4.4 extends it again by letting the return distribution itself depend on a hidden, Markov-modulated environment state. Both extensions are shown to be genuine instances of the same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint consumption-investment choice and the extra regime coordinate change the state and action spaces, but not the proof strategy, which is exactly the point.

Setting

The consumption-investment problem: state $E := \mathrm{dom}\,U_p$ (wealth), action $\mathbb{R}_{\ge0}\times\mathbb{R}^d$ (consumption $c$, amounts $a$ invested), transition $T_n(x,c,a,z) = (1+i_{n+1})(x-c+a\cdot z)$, reward $r_n(x,c,a) := U_c(c)$, terminal reward $g_N := U_p$. Value functions $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[\sum_{k=n}^{N-1} U_c(c_k(X_k)) + U_p(X_N)]$. The one-period sub-problem: $D(x) := \{(c,a) : 0\le c\le x,\ (1+i)(x-c+a\cdot R)\in\mathrm{dom}\,U_p \text{ a.s.}\}$, $u(x,c,a) := U_c(c) + \mathbb{E}[U_p((1+i)(x-c+a\cdot R))]$, $v(x) := \sup_{(c,a)\in D(x)} u(x,c,a)$.

The regime-switching extension (§4.4): an environment process $(Y_n)$, a finite-state Markov chain with transition probabilities $p_{jk}$, modulates the risky-asset return law: given $Y_n=j$, the next relative risk $R_{n+1}$ has law $Q_j$, and $(R_{n+1},Y_{n+1})$ has joint law $Q_j(dz)p_{jk}$ given $Y_n=j$, $Y_{n+1}=k$. The augmented state is $(x,j) \in [0,\infty)\times E_Y$; value functions $J_n(x,j)$ are defined analogously, with the recursion incorporating a finite sum over the next regime.

Formalization targets

Goal — Theorem 4.3.3

$$V_N = U_p, \qquad V_n(x) = \sup_{(c,a)\in D_n(x)} \bigl[U_c(c) + \mathbb{E}\,V_{n+1}\bigl((1+ i_{n+1})(x-c+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave, continuous, and an optimal strategy realized by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every closed-form corollary below specializes it.

Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).

Significance

Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, $1/(N-n+1)$, is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime $k$'s returns dominate regime $j$'s for every risk-averse (concave, monotone) preference," not merely "regime $k$ has a higher mean."

No result of this chunk was found on the platform (searched "consumption investment", "regime switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise joint-choice statement of each result and, for the comparative-statics theorems, the correct increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order (≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different relations and must not be conflated.

Difficulty

The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction $\zeta$ and an investment fraction $\alpha$ optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ($0\le c\le x$ interacts with the investable amount $x-c$), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of $d_n(j)$ in $j$ directly from $Q_j\le_{\mathrm{icv}}Q_k$ alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of $\alpha^*(j)$ handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.

Formalization scope

The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern exactly, extended to a joint $(c,a)$ action. The regime-switching model (RegimeSwitchingMarket) represents the finite regime set $E_Y$ abstractly (a Fintype with a row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on the joint disturbance): the book's own formula for $J_n^\pi$ is already a finite sum over the next regime of an integral against $Q_j$, so this is the direct, faithful representation and needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator recursing through this finite-sum-of-integrals at each step (the natural generalization of chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate, rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder (Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx) does not include the increasing-concave order this chunk's theorems actually use — reusing one of those three would silently substitute a different hypothesis, exactly the trap the chunk brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated fresh for a finite chain given by its transition matrix.

No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the comparative-statics pair) each state their own explicit recursion for $d_n$ — matching the brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6 gives $d_N$ and recurses backward; Theorem 4.4.2 gives $d_0(j)$ and recurses forward) — encoded exactly as each theorem states it, not standardized to one direction.

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
• J. D. Hamilton, "A new approach to the economic analysis of nonstationary time series and the business cycle", Econometrica, 1989 (the regime-switching framework §4.4 specializes to a portfolio-choice setting).

Motivation

Chapter 7's abstract machinery — contracting Markov Decision Models, the Structure Theorem, value iteration with an explicit convergence rate — earns its keep by solving concrete problems. Section 7.6 works through four kinds of application: a return to the classical cash-balance inventory problem, now over an infinite horizon; the "red-and-black" gambling problem, where a player tries to reach a target fortune before going bankrupt; and, most substantially, the infinite-horizon two-armed bandit, where the general theory reveals something genuinely surprising — the qualitatively optimal policy can be computed one arm at a time.

Setting

Every application here specializes the general infinite-horizon, contracting-model machinery of chunks 07a/07b to a concrete transition structure. The cash-balance model orders inventory up to a level $a$ at linear cost, incurs a holding/shortage cost, then absorbs a random demand. The red-and-black model bets a fraction of a bounded fortune on a biased coin, absorbing at bankruptcy or at the target. The bandit model reconsiders the Beta-Bernoulli two-armed bandit of chunk 05b, now over an infinite horizon with a genuine discount $\beta<1$: the key new tool is the K-stopping problem, a fictitious single-arm decision problem where, at every stage, the decision maker may either pull the arm or retire with a fixed payment $K$. The Gittins index $I(m,n)$ is the smallest such payment at which retiring immediately is already as good as continuing.

Formalization targets

The goal, Theorem 7.6.10, is the Gittins index theorem for this book's two-armed bandit: always pulling the arm with the higher index is optimal for the full infinite-horizon problem. The milestones build the machinery it needs — the index's definition (Definition 7.6.5) and its equivalent representation as a supremum over stopping times (Theorem 7.6.6), the K-stopping value function's monotonicity/convexity/differentiability properties (Proposition 7.6.7), the index's optimal-stopping-set and indifference characterizations (Corollary 7.6.8), the two-arm joint stopping value's parallel structure (Proposition 7.6.9), and a fixed-point recasting useful for computation (Proposition 7.6.11) — plus, independently, the cash-balance and casino-game applications (Theorems 7.6.1-7.6.4), which use the general theory but not the bandit-specific machinery.

Significance

The Gittins index theorem's real content, emphasized by the book's own remark, is not merely that an optimal policy exists but how little computation it needs: instead of solving one optimization problem over the bandit's full four-dimensional joint state space $\mathbb N_0^2 \times \mathbb N_0^2$, the decision maker solves two independent two-dimensional single-arm problems and compares two numbers. This mission's formalization of the goal is built specifically to keep that separation visible — each arm's index is computed from a single, shared KStoppingValue structure applied to that arm's own state alone, never from a function that happens to take the whole joint state as an argument. The proof route here (via the K-stopping problem's explicit fixed-point characterization, Definition 7.6.5 and Proposition 7.6.11) is a genuinely different construction from the platform's existing Gittins-index theorems (BanditAlgorithm.gittins_index_theorem and related), which are built via Whittle's retirement/charge-accounting argument — checked directly and found to define the index differently enough that this mission drafts its own theorems rather than treat that construction as prior art.

Difficulty

The K-stopping value function $J(m,n;K)$ and the two-arm joint value $\tilde J(x;K)$ are both genuine fixed points of an infinite-horizon Bellman equation with no finite backward recursion to fall back on (the "stopping" option, rather than a terminal condition, is what makes the horizon infinite); this mission bundles them as data satisfying their own defining fixed-point equations, the same convention this series uses throughout for such objects. A second difficulty is Theorem 7.6.6's supremum over stopping times: without a canonical path measure for the underlying Markov chain (not built anywhere in this series), the two expectations the theorem compares are represented as data satisfying the positivity a genuine expectation must have, over an explicit, elementary notion of stopping time (a function of the whole observed path, adapted in the sense that whether it has fired by time $n$ depends only on the path up to $n$) — a faithful, if representational, rendering of the theorem's genuinely path-dependent content.

Formalization scope

The cash-balance model (Theorem 7.6.1) explicitly cites chunk 02d's finite-horizon critical-level sequences as a hypothesis rather than re-deriving them, since this mission's own content is the infinite-horizon extension, not a second proof of the finite-horizon theory those sequences come from. The casino-game theorems (7.6.2-7.6.4) state optimality for the specific, named timid and bold strategies, not for an unnamed "some optimal policy" — the theorems' entire content is that these particular policies, not merely some optimal one, are best in their regime. The bandit model's posterior mean and Bayes-update operator are kept identical in substance to chunk 05b's finite-horizon Beta-Bernoulli model (restated, since chunks cannot import each other's Lean), so a reader can see this section is solving the same underlying statistical model, now over an infinite horizon.

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.
• J. C. Gittins, "Bandit processes and dynamic allocation indices," Journal of the Royal Statistical Society, Series B, 1979 (the original index construction this section's K-stopping-problem approach reformulates).
• P. Whittle, "Multi-armed bandits and the Gittins index," Journal of the Royal Statistical Society, Series B, 1980 (the retirement-option construction the platform's existing Gittins theorems use, a different proof route from this chunk's own).
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965 (the classical red-and-black problem, Theorems 7.6.2-7.6.4).

Motivation

Two problems in this mission, both about markets that do not behave the way the textbook Black–Scholes market does, and both solved by the same technique.

The first is portfolio choice in a pure jump market. Prices move by jumps at the epochs of a Poisson process, not by continuous Brownian fluctuation. This is not a technical variation: the market is incomplete, there is no replicating portfolio, and the machinery of stochastic analysis that makes the diffusion case tractable is unavailable. What is available instead is that the wealth process is piecewise deterministic — between jumps it follows an ODE, and all the randomness is in when the jumps happen and how big they are. Chapter 8's technique embeds such a process in its jump chain and turns the continuous-time control problem into a discrete-time Markov Decision Model with infinite horizon; Chapter 7's contracting theory then solves that.

The second is trade execution in an illiquid market. An agent must sell a large block of shares by a deadline. Placing the whole order at once moves the price against them, and in a traditional order book other participants can see the intention and trade against it — so the order goes to a dark pool, where there is no order book and matches arrive at random. The agent can only sell when a counterparty happens to appear, and whatever is unsold at the deadline must be dumped on the traditional market at once. The question is how much to offer at each opportunity.

The two problems have opposite curvature — the first is a concave maximisation of utility, the second a convex minimisation of cost — and the section is a good demonstration that the same embedding technique handles both, with each problem's structure entering only through which set of functions the value function is sought in.

Setting

The jump market (§9.3). The bond is S⁰_t = e^{ρt}; the risky assets follow dS^k_t = S^k_{t-}(μ_k dt + dC^k_t) where C_t = Σ_{n≤N_t} Y_n is a compound Poisson process of intensity λ whose jumps Y_n are supported in (-1,∞)^d, which keeps prices positive. Short-sellings are prohibited, so the admissible fractions of wealth form the compact set 𝒰 = {u ≥ 0, u·e ≤ 1}, and the wealth follows

$$dX_t = X_{t-}\big((\rho + \pi_t\cdot(\mu-\rho e))dt + \pi_t dC_t\big). \tag{9.10}$$

The investor maximises E^π_{tx}[U(X_T)] for a strictly increasing, strictly concave U.

The embedded model's state is (t,x) — a jump time and the wealth just after it — and its action is a whole control path α : [0,T] → 𝒰, followed until the next jump. Between jumps the wealth is φ^α_t(x) = x exp(∫₀^t (ρ + α_s·(μ-ρe))ds) (9.13), and the transition kernel is substochastic: with probability e^{-λ(T-t)} no further jump arrives before the horizon, and the reward r(t,x,α) = e^{-λ(T-t)}U(φ^α_{T-t}(x)) is collected instead.

The trade execution model (§9.4). A Poisson process of intensity λ delivers the trading epochs; selling a shares costs C(a) with C strictly increasing and strictly convex (the discrete form (9.19)), C(0) = 0; the inventory X_t = x₀ - ∫₀^t π_s dN_s is what remains, and C(X_T) is the terminal dump. Here the flow is uncontrolled — the inventory does not move between epochs — which makes the embedded model simpler.

What is being asked

The goal is Theorem 9.3.4, the main result for the terminal wealth problem, in all six of its parts: the value function is the limit of the value iteration and lies in IM_cv; it is the unique fixed point of the dynamic programming operator there; value iteration converges at the explicit geometric rate α_b^n/(1-α_b); there exists an optimal Markov portfolio strategy given by a single decision rule; policy iteration holds; and Howard's policy improvement algorithm holds. Parts a)–c) describe the value; parts d)–f) produce the strategy, and a formalization of the first three alone would omit the entire control half of the theorem.

The seven milestones are the rest of §9.3–9.4: the reduction from continuous to discrete time, the bounding function and its explicit contraction modulus, the invocation of Chapter 7's Structure Theorem, the iff-characterization of when holding only the bond is optimal, the stability of the value and of the optimal policies under perturbation of the utility, and then the trade execution problem's own bounding function and its monotone, unit-Lipschitz optimal execution rate.

Two formalization conventions run through everything here. The operator of §9.3 is a supremum over a space of control paths, and since Mathlib's sSup of a set unbounded above is 0 — with an unbounded reward that is a live risk, not a formality — it is carried as a relation defined by least upper bounds against explicit sets of achievable values, with its iterates a chain of such relations. And the continuous-time side is built, not assumed: Theorem 9.3.1 is the identification of the continuous-time value with the discrete-time one, so the law of the embedded jump chain is pinned by the one-step conditional law the book displays, and the terminal wealth is read off that chain.

Motivation

A gambler watching a sequence unfold has to decide, at each moment and knowing only the past, whether to take what is on the table or wait for something better. That is the whole of optimal stopping, and it is one of the few problems in stochastic control with a clean and completely general answer: the value of the problem is the smallest superharmonic function dominating the immediate payoff. Snell (1952) proved the martingale form; the dynamic-programming form is due to Chow, Robbins and Siegmund. It is the structure behind the pricing of American options, the secretary problem, sequential hypothesis testing, and the bandit problems of Chapter 5.

Bäuerle and Rieder's Chapter 10 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own Markov-decision machinery rather than from martingale theory, which makes the whole development elementary and self-contained: a stopping problem is a Markov Decision Problem whose action space is {continue, stop}, so Chapter 2's finite-horizon theory and Chapter 7's unbounded-horizon theory apply to it verbatim. The chapter then runs the resulting theory on three classical problems and solves each one in closed form.

Setting

The problem. A Markov process (X_n) on a Borel space E is observed. A stopping time is a random time τ with {τ ≤ n} ∈ F_n — "upon observing the process until time n we can decide whether or not τ has already occurred". Stopping at τ collects

$$R_\tau := \sum_{k=0}^{\tau-1} c_k(X_k) + g_\tau(X_\tau),$$

a running reward c_k while continuing and a stopping reward g_τ at the end, and the problem is to find V_N^*(x) := sup_{τ ≤ N} E_x[R_τ] (10.1). Assumption (B_N) — finiteness of the supremum of the positive parts — is what makes this well posed.

The reduction (Theorem 10.1.2). Take A = {0,1}, let a = 0 mean continue and a = 1 mean stop, and make the transition law uncontrollable on continuation and absorbing on stopping. A policy π = (f_0,…,f_{N-1}) induces the stopping time τ_π = inf{n | f_n(X_n) = 1} ∧ N, and conversely every stopping time is a history-dependent policy. The theorem says the two suprema agree: the extra history buys nothing.

The recursion (Theorems 10.1.3, 10.1.5). The Bellman operator becomes a two-branch maximum,

$$\mathcal{T}v(x) = \max\Big\{g(x),\ c(x) + \beta\int v(x')Q^X(dx'|x)\Big\},$$

with no action variable left in it. In the stationary case J_0 = g, J_n = \mathcal{T}J_{n-1}; the J_n increase, the sets S_n^* = {J_n = g} shrink — "the tendency to stop is non-decreasing as time goes by" — and the optimal rule is "stop on first entry into S_{N-n}^*".

The unbounded horizon (§10.2). Now the reward is discounted, R_τ = Σ β^k c(X_k) + β^τ g(X_τ) for τ < ∞, the value is V_∞^*(x) = sup_{τ<∞} E_x[R_τ], and there is no terminal condition to induct from. Three candidate values present themselves: V_∞^*; G = sup_π liminf_n J_{nπ}, a supremum over policies of limits of finite-horizon values; and J = lim_n J_n, which exists by monotonicity. Theorem 10.2.2, the goal, says all three coincide, that the common value solves J = \mathcal{T}J and satisfies 0-free bounds, and — the characterization — that it is the smallest c-superharmonic function majorizing g.

Turning the value into a rule (Theorems 10.2.3, 10.2.7, Corollaries 10.2.6, 10.2.8). Knowing the value is not knowing when to stop. Theorem 10.2.3 produces the stopping region as S^* = {J = g} = {d ≥ 0} where d = lim_n d_n, under two conditions that Corollary 10.2.6 then gives three checkable sufficient conditions for. Theorem 10.2.7 is the practical one, the One-Step-Look-Ahead Rule: if the set where stopping now beats stopping one step later is closed under the transition law, then the myopic rule is globally optimal. Corollary 10.2.8 adds monotonicity and gets a threshold.

Three applications (§10.3). The house seller who receives i.i.d. offers and pays maintenance on each rejection should accept the first offer above an explicit threshold, obtained as the maximiser of a one-dimensional function (Theorem 10.3.1). The secretary problem's value function is computed exactly (Proposition 10.3.2), giving the classical rule — reject the first k^*, then take the first leader — with success probability (k^*/N)h(k^*) and k^*(N)/N → 1/e (Theorem 10.3.3). And when the offers' distribution has an unknown parameter, MTP_2 of the likelihood propagates into monotonicity of the value in the information state (Theorem 10.3.4), with a fully explicit solution for the exponential/Inverse-Gamma conjugate pair (Theorem 10.3.6).

What is being asked

Formalize Theorem 10.2.2 in full: the three-way equality of V_∞^*, G and J, the fixed point equation, and — the part that carries the theorem — minimality among all functions that are both c-superharmonic and above g. Asserting only that J is such a function, or only one of the two conditions, is a strictly weaker and different claim.

The twelve milestones are the rest of the chapter, in attack order: the reduction and the two recursions, then the unbounded-horizon apparatus, then the three worked problems.

The stopping-time apparatus is built rather than assumed — the chain's law pinned by its finite-dimensional distributions, stopping times valued in ℕ ∪ {∞}, rewards vanishing at ∞ — because every theorem here is the identification of a supremum over stopping times with something computable, and carrying the value as an abstract function would make them vacuous. Every supremum is taken as a least upper bound against an explicit set of achievable values rather than by sSup, so that a set unbounded above is not silently given the value 0.