Markov Decision Processes

Motivation

When a system is controlled indefinitely and decisions are frequent — a router admitting packets, a queue accepting jobs, a machine being maintained — discounting future rewards is often unjustified, and what matters is the long-run average reward per period. Puterman's Chapter 8 (doi:10.1002/9780470316887) develops the theory of this criterion, and its central object is a single equation, the average reward optimality equation $0=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, whose unknowns are a scalar gain $g$ and a bias function $h$. For unichain models, in which every stationary policy generates a Markov chain with one recurrent class, this equation determines the optimal gain and an optimal stationary policy. The results go back to Howard (Dynamic Programming and Markov Processes, MIT Press, 1960) for the recurrent case and to Blackwell (Discrete dynamic programming, Annals of Mathematical Statistics 33, 1962, doi:10.1214/aoms/1177704593) and Derman for the general finite case; Puterman's Section 8.4 proves them through the discounted theory of mission II, by letting the discount factor tend to one.

Setting

The model is stationary (Assumption 8.0.1): a finite set $S$ of states, for each $s$ a finite nonempty set $A_s$ of actions, a reward $r(s,a)$ and transition probabilities $p(j\mid s,a)$, none depending on the decision epoch. A policy $\pi\in\Pi^{HR}$ may randomize and may depend on the whole history; the deterministic stationary policy $d^\infty$ applies the decision rule $d:S\to A$ at every epoch. Its transition matrix is $P_d(i,j)=p(j\mid i,d(i))$.

For a policy $\pi$, $v^\pi_{N+1}(s)=\mathbb E^\pi_s[\sum_{t=1}^Nr(X_t,Y_t)]$ is the expected reward over $N$ epochs. Since the limit of $N^{-1}v^\pi_{N+1}(s)$ need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards $g^\pi_+(s)$ and $g^\pi_-(s)$, and with $g^*_\pm(s)=\sup_{\pi}g^\pi_\pm(s)$. A policy $\pi^*$ is average optimal when $g^{\pi^*}_-(s)\ge g^\pi_+(s)$ for all $s$ and $\pi$, the strongest of the three criteria of Section 8.1.2.

The optimality residual is $B(g,h)(s)=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, and the optimality equation is $B(g,h)=0$. A decision rule is $h$-improving when it attains $\max_{a\in A_s}\{r(s,a)+\sum_jp(j\mid s,a)h(j)\}$ at every state. A transition matrix is unichain when it consists of a single recurrent class plus a possibly empty set of transient states, and the MDP is unichain when $P_d$ is unichain for every deterministic decision rule.

Formalization targets

Goal — Theorem 8.4.5 (printed p. 361)

For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation $B(g^*,h^*)=0$ has a solution, and (d) its scalar satisfies $g^*_+(s)=g^*_-(s)=g^*$ for every $s$; (c) for every solution, every $h^*$-improving decision rule gives an average optimal stationary policy.

Theorem 8.4.1 (printed p. 356)

If $B(g,h)\le 0$ then $g\ge g^*_+$; if $B(g,h)\ge 0$ then $g\le\sup_{d}g^{d^\infty}_-\le g^*_-$; if $B(g,h)=0$ then $g^*_+=g^*_-=g$.

Theorem 8.4.3 (printed p. 358)

In a finite unichain model $B(g,h)=0$ has a solution, and every solution has the same $g$.

Theorem 8.4.4 (printed p. 361)

If $B(g^*,h^*)=0$ and $d^*$ is $h^*$-improving, then $(d^*)^\infty$ is average optimal.

Significance

Theorem 8.4.1(c) is what the source calls "one of the most important results for average reward models": a solution of the optimality equation with constant $g$ pins down the optimal gain under every criterion at once, so that in finite unichain models the three optimality criteria of Section 8.1.2 coincide. Theorem 8.4.3 guarantees such a solution exists, and Theorem 8.4.4 reads an optimal policy off it. Together, Theorem 8.4.5 reduces the infinite-horizon average reward problem over all history-dependent randomized policies to a finite system of equations in $(g,h)$, which is what policy iteration, value iteration and linear programming solve in Sections 8.5 to 8.8.

The results are classical and proved. Formalizing them fixes the chain-structure hypothesis in a checkable form and pins down which criterion "average optimal" means, two places where the literature is loose. The platform's MarkovDecisionProcesses series has the finite-horizon (mission I) and discounted (mission II) models; this mission adds the undiscounted stationary model, the gains, and the unichain classification, on which Chapter 9's multichain optimality equations and Chapter 10's sensitive discount optimality can be built.

Difficulty

The obvious argument for Theorem 8.4.3 is to take the discounted optimal value $v^*_\lambda$ of mission II and let $\lambda\uparrow 1$. It fails as stated because $v^*_\lambda$ blows up like $(1-\lambda)^{-1}$; what converges is the Laurent expansion $v^{d^\infty}_\lambda=(1-\lambda)^{-1}ge+h+o(1)$ of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix $P_d^*$ and the deviation matrix $H_{P_d}$ of a unichain chain. So the proof must first develop the Markov chain theory of Section 8.2 and Appendix A, choose a subsequence of discount factors along which one policy is discount optimal (possible because $D^{MD}$ is finite), and only then pass to the limit in the discounted optimality equation.

Theorem 8.4.1 looks elementary and hides the analytic step: iterating $ge\ge r_d+(P_d-I)h$ along an arbitrary history-dependent policy and dividing by $N$ requires the telescoping term $N^{-1}(P^\pi_N-I)h$ to vanish, which uses boundedness of $h$, and requires the reduction from history-dependent randomized to Markov randomized policies (Theorem 8.1.2). For Theorem 8.4.4 the step is Corollary 8.2.7, that $r_d-ge+(P_d-I)h=0$ forces the gain of $d^\infty$ to be $g$, which is the multiplication by $P_d^*$ that annihilates $(P_d-I)$.

The traps are in the definitions. Recurrence and the unichain property must be stated so that the source's Example 8.4.3 comes out as the book says — the policy using $a_{1,1}$ has the absorbing state $s_2$ as its single recurrent class — and the optimality residual must use the lim sup / lim inf gains, since a definition through a limit that need not exist would be a junk value on the policies of Example 8.1.1.

Formalization scope

State and action spaces are Fintypes and admissible actions are nonempty Finsets, as in missions I and II; the stationary model is a new structure because mission II's DiscountedMDP bundles a discount factor, and carries the same data otherwise. Policies are history-dependent and randomized, so "average optimal" has its full strength; a stationary policy is the deterministic one built from a decision rule. Expected total reward is defined by the policy evaluation recursion, as in the earlier missions, rather than through a measure on trajectories.

Gains are Filter.limsup and Filter.liminf of $N^{-1}v^\pi_{N+1}(s)$ on $\mathbb R$; these are the source's because the sequence is bounded by $\max|r|$, and the suprema $g^*_\pm$ over the nonempty family of policies are genuine real suprema for the same reason. The residual $B(g,h)$ is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from $i$ reaches $i$" and unichain is "any two recurrent states communicate", the definitions of Appendix A for finite chains, applied to $P_d$ for every admissible deterministic decision rule.

Restrictions relative to the printed text, all noted in the items: Theorem 8.4.1 is stated for finite $S$ where the source says countable, since the chapter's standing assumption and the model are finite; the gain $g^{d^\infty}$ of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain $ge=g^*=g^*_+=g^*_-$ of (8.4.6) is stated through $g^*_+$ and $g^*_-$, since $g^*$ presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and $B(g,h)=0$ with a junk maximum is impossible since every $A_s$ is nonempty. Welcome contributions beyond the milestones: Theorem 8.1.2 (reduction to Markov policies), Corollary 8.2.7 (the gain of a stationary policy from the evaluation equations), and the equivalence of the three optimality criteria in finite models.

Selected references

• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Chapter 8. doi:10.1002/9780470316887
• Ronald A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• David Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962). doi:10.1214/aoms/1177704593
• Cyrus Derman, Finite State Markovian Decision Processes, Academic Press, 1970.
• Paul J. Schweitzer and Awi Federgruen, The functional equations of undiscounted Markov renewal programming, Mathematics of Operations Research 3 (1978). doi:10.1287/moor.3.4.308

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

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

Most concrete applications of Markov Decision Theory — inventory control, cash management, linear-quadratic regulation, sequential games — have data that does not change from one period to the next: the same state space, action space, transition mechanism and reward apply at every stage, only discounted by a fixed factor $\beta$ per period. Bäuerle and Rieder's Chapter 2, §2.5 specializes the general finite-horizon theory of the previous sections to this stationary case, and §2.6 shows the specialization at work on three classical models: a card game with a famously boring answer, a firm's cash-management problem, and stochastic linear-quadratic control. Together they demonstrate the payoff of the abstract theory: once the Structure Assumption is checked for a stationary model, the general machinery (the Forward Induction Algorithm) produces the concrete optimal policy — a critical-level $(s,S)$-type control for cash management, a linear feedback law for LQ control — with no further case-specific argument.

Setting

A stationary Markov Decision Model is a Markov Decision Model $(E,A,D,Q,r,g)$ (Definition 2.1.1) whose data does not depend on the stage: the reward at absolute time $n$ is $\beta^n r$ and the terminal reward at time $N$ is $\beta^N g$, for a fixed discount $\beta \in (0,1]$. For a policy sequence $\pi = (f_0,\dots,f_{n-1}) \in F^n$ (each $f_k$ a decision rule $E \to A$ with $f_k(x) \in D(x)$), the reward-to-go is $J_n^\pi(x) := \mathbb{E}^\pi_x\bigl[\sum_{k=0}^{n-1} \beta^k r(X_k,f_k(X_k)) + \beta^n g(X_n)\bigr]$ and the value function is $J_n(x) := \sup_{\pi \in F^n} J_n^\pi(x)$. The operators $(Lv)(x,a) := r(x,a) + \beta\int v(x')\,Q(dx'\mid x,a)$, $(Tv)(x) := \sup_{a \in D(x)} (Lv)(x,a)$, $(T^f v)(x) := (Lv)(x,f(x))$ are the stationary counterparts of §2.3's non-stationary operators. The (stationary) Structure Assumption (SAN) asks for sets $\mathrm{I\!M} \subseteq \mathrm{I\!M}(E)$, $\Delta \subseteq F$ with $g \in \mathrm{I\!M}$, $v \in \mathrm{I\!M} \Rightarrow Tv \in \mathrm{I\!M}$, and every $v \in \mathrm{I\!M}$ having a maximizer in $\Delta$.

Formalization targets

Goal — Theorem 2.6.2 (the cash balance problem)

A firm's cash level $x \in \mathbb{R}$ moves under i.i.d. shocks; each period the firm transfers to a new level $a$ at linear cost $c(a-x) = c_u(a-x)^+ + c_d(a-x)^-$, pays a convex, coercive holding cost $L(a)$ ($L(0)=0$), and the level becomes $a - Z_{n+1}$. Modeled as a stationary MDM with $E=A=\mathbb{R}$, $r(x,a) = -c(a-x) - L(a)$, $g \equiv 0$:

$$\exists\, S_n^- \le S_n^+ \ \text{(depending on $n$)}: \quad J_n(x) = \begin{cases} (S_n^- - x)c_u + L(S_n^-) + \beta\,\mathbb{E}[J_{n-1}(S_n^- - Z)] & x < S_n^- \\ L(x) + \beta\,\mathbb{E}[J_{n-1}(x-Z)] & S_n^- \le x \le S_n^+ \\ (x-S_n^+)c_d + L(S_n^+) + \beta\,\mathbb{E}[J_{n-1}(S_n^+ - Z)] & x > S_n^+, \end{cases}$$

with $J_0 \equiv 0$, and the optimal policy transfers up to $S_n^-$ below it, down to $S_n^+$ above it, and does nothing in between. This is the weakest stable statement: it asserts the existence of critical levels with the stated recursive characterization, not any closed form for $S_n^\pm$ itself (which depends on $L$'s exact shape and is not computable in general).

Three milestones build toward and alongside it: the Reward Iteration theorem and stationary Structure Theorem (Theorems 2.5.3-2.5.4, the general machinery instantiated), the trivial-but- sharp red-and-black card game (Theorem 2.6.1), and the stochastic linear-quadratic problem (Theorem 2.6.3, a Riccati-type recursion with random coefficients).

Significance

Theorem 2.6.2 is the textbook derivation of $(s,S)$-type control, the dominant policy structure in inventory theory and cash management: a firm should act only when its state leaves a band, and should act to bring it exactly to the band's edge, never further. Its proof pattern — verify (SAN) with $\mathrm{I\!M}$ the convex functions of at most linear growth, extract the critical levels from the derivative conditions of a one-stage minimization — is the template used across the inventory-control literature for essentially every variant of this problem. Theorem 2.6.1's answer ("no strategy beats stopping immediately") is a genuine, if minimal, comparative-statics fact: a positive-content instance of $\mathrm{I\!M}$ collapsing to functions constant on the game's absorbing set, forcing every action to be a maximizer. Theorem 2.6.3's Riccati-type recursion, with random transition coefficients, generalizes the classical deterministic-coefficient LQR (linear-quadratic regulator) of control theory; the recursion governs mean-variance and quadratic-hedging problems return to in later chapters of this book (Chapters 4 and 6).

None of the three examples' specific results were found on the platform (searched for "comparative statics", "convex Markov decision", the exact model names, and "bang-bang"/"LQR" adjacent terms). BertsekasDP.riccati_completion_of_square is the platform's one close relative to Theorem 2.6.3: it solves the deterministic-coefficient LQR by a completion-of-squares argument, not the random-coefficient recursion here, so it is cited as related work rather than reused. The proofs themselves are complete and self-contained in the book (a few pages each, using only single-variable convex analysis and elementary linear algebra); this mission contributes the formal statement of each, in its full generality (general convex $L$, general random $(A,B)$ coefficient pairs), as the task for a sorry-free proof.

Difficulty

The cash-balance proof's central step is showing the minimizer of the one-stage problem is of critical-level form for every $v$ in the candidate class $\mathrm{I\!M}$ — not just for the particular sequence $J_0, J_1, \dots$ that eventually arises. The obvious shortcut, guessing the form of $J_n$ directly and verifying it solves the Bellman equation by substitution, fails because $S_n^-, S_n^+$ are themselves defined only implicitly, via one-sided derivative conditions on $L(x) + \beta\mathbb{E}[v(x-Z)]$; there is no closed form to substitute except in degenerate special cases (e.g. $L$ quadratic). The genuine content is the general argument (convexity of the one-stage objective forces a unique critical-level minimizer structure, and this structure is preserved under $T$) that lets the induction go through for an arbitrary convex, coercive $L$. For Theorem 2.6.3, the natural first attempt — solve the deterministic LQR recursion and substitute expected coefficient matrices for the random ones — is not obviously valid, since $\mathbb{E}[B^\top Q B] \ne (\mathbb{E}[B])^\top Q\,\mathbb{E}[B]$ in general; the correct recursion genuinely involves the joint second moments of $(A,B)$, which is exactly what the standing positive-definiteness assumption on $\mathbb{E}[B^\top Q B]$ (not on $\mathbb{E}[B]$ itself) is there to make precise.

Formalization scope

The stationary vocabulary (StationaryMarkovDecisionModel, its operators, J, (SAN)) is restated independently of chunk 02a's non-stationary vocabulary — drafts in this series cannot import one another, and the book itself keeps the two notationally separate ($J_n$ vs. $V_n$, related by $V_n(x) = \beta^n J_{N-n}(x)$, a relation this mission does not separately formalize since no listed result needs it). Theorem 2.6.3's stochastic LQ problem is explicitly non-stationary in the book's own text, so a second, NS-prefixed restatement of the non- stationary model and value function (via the Bellman recursion established as Theorem 2.3.8, not the sup-over-policies primitive — the same simplification chunk 02c makes for its own V) is introduced solely for that one theorem. The card game (Theorem 2.6.1) is formalized on the concrete state space $\mathbb{N} \times \mathbb{N}$ and action space Bool, with the model's exact transition density, reward and terminal reward given as hypotheses on an abstract StationaryMarkovDecisionModel, matching the book's own discrete-density notation $q(x'\mid x,a) := Q(\{x'\}\mid x,a)$ (introduced in the text following Theorem 2.5.4) rather than built from an explicit PMF/Kernel construction — a lighter-weight but equally precise formalization, since the density equations pin the kernel exactly. The stochastic LQ problem uses Matrix (Fin m) (Fin m) ℝ and needs a MeasurableSpace (Matrix m n α) instance Mathlib does not provide (Matrix is a non-reducible def for m → n → α); this mission supplies it by transport across the definitional equality. Random matrix moments $\mathbb{E}[F(A,B)]$ are computed entrywise as ordinary Bochner integrals against the joint law of $(A,B)$.

A trivializing formalization is ruled out on two fronts: the cash-balance critical levels $S_n^-, S_n^+$ are existentially quantified as functions of $n$, not fixed constants (dropping the index would silently claim a single band works for every horizon length, which is false in general); and the card game's "every strategy is optimal" is stated as a universally-quantified claim over all policy sequences, not weakened to mere existence of an optimal one. Reusable infrastructure: the jointMatMean/xQx helpers and the MeasurableSpace (Matrix m n α) instance are generic and available to any later chunk needing random-matrix moments (none of the remaining chunks' briefs currently list one, but Chapter 4's mean-variance and LQ-flavored missions may). sorry-free proofs of all five items are welcome contributions; Theorem 2.5.3's short inductive proof (unwinding the accumulator definition against the operator-composition recursion) is likely the easiest entry point.

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. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005 (the classical deterministic-coefficient LQR, BertsekasDP.riccati_completion_of_square on the platform).

Motivation

Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.

Setting

An $N$-period financial market with $d$ risky assets consists of a probability space $(\Omega,\mathcal{F},\mathbb{P})$ with filtration $(\mathcal{F}_n)_{n=0}^N$, $\mathcal{F}_0$ trivial; a riskless bond with deterministic interest rate $i_n$ on $[n-1,n)$ (so $S^0_n = S^0_{n-1}(1+i_n)$); and $d$ risky assets with relative price changes $\tilde R_n = (\tilde R^1_n,\dots,\tilde R^d_n)$, $\mathcal{F}_n$-measurable and a.s. strictly positive ($S^k_n = S^k_{n-1}\tilde R^k_n$). A portfolio (trading strategy) is an $(\mathcal{F}_n)$-adapted process $\varphi = (\varphi^0_n,\varphi_n)$, $\varphi^0_n \in \mathbb{R}$, $\varphi_n \in \mathbb{R}^d$; $\varphi^k_n$ is the money invested in asset $k$ on $[n,n+1)$. Its value before/after trading at time $n$ is $X_n^- := \varphi^0_{n-1}(1+i_n) + \varphi_{n-1}\cdot\tilde R_n$, $X_n^+ := \varphi^0_n + \varphi_n\cdot e$; $\varphi$ is self-financing if $X_n^- = X_n^+$ a.s. for every interior $n$. An arbitrage opportunity is a self-financing $\varphi$ with $X_0^\varphi = 0$, $X_N^\varphi \geq 0$ a.s., $X_N^\varphi > 0$ with positive probability. The relative risk process $R_n^k := \tilde R_n^k/(1+i_n) - 1$ is the excess return of asset $k$ over the riskless rate.

Formalization targets

Goal — Theorem 3.1.5

$$\text{No arbitrage} \iff \forall\, n < N,\ \forall\, \mathcal{F}_n\text{-measurable } \varphi_n \in \mathbb{R}^d: \quad \varphi_n \cdot R_{n+1} \geq 0 \text{ a.s.} \implies \varphi_n \cdot R_{n+1} = 0 \text{ a.s.}$$

This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.

No further milestone is formalized in this mission: this chapter's only other theorem, Theorem 3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the Formalization scope section and HARD.md.

Significance

Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage $\iff$ existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.

Formalizing it contributes the exact discrete-time, filtration-indexed statement of the reduction — a result absent from the platform (searched "arbitrage", "self-financing", "martingale measure", "utility function"; the one related hit, LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix — a different equivalence for a different, non-stochastic model, not reused here).

Difficulty

The direction "local no-free-lunch at every stage $\Rightarrow$ no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from $n=0$) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth $X_N$, and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between "$X \geq 0$ a.s." failing to imply "$X < 0$ with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).

Formalization scope

The market is represented via DiscreteFinancialMarket, bundling the probability space, filtration, and the two primitives ($i$, $\tilde R$) actually used; price processes $S^0, S^k$ are not separately represented, since they would only be running products of these two primitives with no further role once the relative risk process $R$ is derived. Filtration is represented directly as a monotone family of sub-$\sigma$-algebras with a trivial Fam 0, not via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here. Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition, needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg semimartingale (only specific constructions such as Itô integration against Brownian motion); this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it, not a hidden simplification of the definition's own content, which states the self-financing equation exactly as the book writes it.

Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem asserts weak convergence of the whole path of the binomial-tree price process to the Black-Scholes-Merton stock price on the Skorokhod space $D[0,T]$ of càdlàg functions with the Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional convergence in distribution, and the book explicitly names this topology (it is not left implicit). Mathlib has no formalization of $D[0,T]$ or the Skorokhod topology, and building either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking outside the scope of a single milestone; weakening the claim to convergence of finite-dimensional distributions, or silently substituting an unnamed alternative topology (e.g. uniform convergence, under which the claim would in fact be false, since the discretized paths have jumps the limit does not), would misstate the theorem rather than state a smaller piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock this result.

No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios (Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the one-period condition of part b) quantifies over all $\mathcal{F}_n$-measurable $\varphi_n \in \mathbb{R}^d$ — narrowing either quantifier (e.g. to strategies with bounded positions) would state a weaker, easier claim than the book's own theorem.

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. M. Harrison and D. M. Kreps, "Martingales and arbitrage in multiperiod securities markets", Journal of Economic Theory, 1979 (the discrete-time fundamental theorem of asset pricing this chapter's Theorem 3.1.5 is a structural lemma toward, not itself proved in this section).

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

Two more portfolio problems round out Bäuerle and Rieder's finance chapter, each raising a question the earlier sections do not. First: a fund manager is mandated to track an index — replicate its value as closely as possible — but the index itself is often built from assets the fund cannot trade directly (a broad benchmark, a proprietary basket). This is the multiperiod, statistical analogue of index-fund management, and it turns out to be a classical linear-quadratic control problem (R. E. Kalman, A New Approach to Linear Filtering and Prediction Problems, 1960, for the deterministic-coefficient case that Bäuerle and Rieder's §2.6.3 first generalizes to random coefficients) rather than requiring a new dynamic-programming argument at all. Second: how should a contingent claim be priced when it depends on an asset that cannot be traded, so that perfect replication is simply impossible? This is the market-incompleteness question at the heart of mathematical finance since the 1970s options-pricing literature, and §4.9 develops the utility indifference pricing approach (M. H. A. Davis, Option Pricing in Incomplete Markets, in Mathematics of Derivative Securities, 1997; also traceable to the zero-utility premium principle of classical insurance mathematics): price a claim at the amount that leaves an expected-utility-maximizing investor indifferent between holding it and not.

Setting

Index tracking (§4.8): state $(x,\hat s)\in E:=\mathbb{R}\times\mathbb{R}$ (wealth, value of the non-traded index $\hat S$), action $a\in A:=\mathbb{R}^d$ (amounts in $d$ traded assets), transition $T_n((x,\hat s),a,(z_1,z_2)) := ((1+i_{n+1})(x+a\cdot z_1),\ \hat s\,z_2)$. The objective is $V_n(x,\hat s) := \inf_\pi \mathbb{E}[\sum_{k=n}^N (X_k-\hat S_k)^2]$ (Eq. (4.36)): minimize the expected sum of squared tracking errors. Chapter 2's stochastic linear-quadratic theory (§2.6.3, Theorem 2.6.3) already solves any problem of this shape — linear dynamics with random coefficient matrices $A_{n+1},B_{n+1}$, quadratic cost with fixed matrix $Q$ — via a backward Riccati-type recursion $\tilde Q_N:=Q_N$, $\tilde Q_n := Q_n + \mathbb{E}[A_{n+1}^\top \tilde Q_{n+1}A_{n+1}] - \mathbb{E}[A_{n+1}^\top\tilde Q_{n+1}B_{n+1}](\mathbb{E}[B_{n+1}^\top \tilde Q_{n+1}B_{n+1}])^{-1}\mathbb{E}[B_{n+1}^\top\tilde Q_{n+1}A_{n+1}]$, so §4.8's content is identifying this problem's own $A_{n+1},B_{n+1},Q$.

Indifference pricing (§4.9): a one-period market with a traded asset $S$ and an untradeable asset $\hat S$, four states of the world with probabilities $p_1,\dots,p_4$, relative returns $(\tilde R,\hat R)\in\{(u,\hat u),(u,\hat d),(d,\hat u),(d,\hat d)\}$, an exponential-utility investor $U(x)=-e^{-\gamma x}$, and a claim $H=h(S_1,\hat S_1)$. The investor's value with the claim sold short is $V_0^H(x,s,\hat s) := \sup_a \mathbb{E}[-e^{-\gamma x-\gamma a(\tilde R-1)+\gamma H}]$ (Eq. (4.37)); Definition 4.9.1 sets the indifference price $v_0(H,s,\hat s)$ as the amount solving $V_0^0(x,s,\hat s) = V_0^H(x+v_0,s,\hat s)$ for every wealth $x$. The multiperiod extension (unnumbered display, p. 138) replaces the one period by $N$ i.i.d. periods and defines $v_n(H,s,\hat s)$ at every time $n$ the same way, now for $V_n^H$ a genuine dynamic value function.

Formalization targets

Goal — Theorem 4.9.4

$$V_n^H(x,s,\hat s) = -e^{-\gamma x}d_n(s,\hat s), \qquad d_N(s,\hat s):=e^{\gamma h(s,\hat s)}, \qquad d_n(s,\hat s) := \inf_{a} \mathbb{E}\big[e^{-\gamma a(\tilde R_{n+1}-1)}\,d_{n+1}(s\tilde R_{n+1},\hat s\hat R_{n+1})\big],$$ $$v_n(H,s,\hat s) = \frac{1}{\gamma}\log\Big(\frac{d_n(s,\hat s)}{v^{N-n}}\Big), \qquad v_n\big(v_{n+1}(H,s\tilde R_{n+1},\hat s\hat R_{n+1}),s,\hat s\big) = v_n(H,s,\hat s),$$

where $v:=\inf_a\mathbb{E}[e^{-\gamma a(\tilde R_1-1)}]$ (Eq. (4.39)). This is the genuine multiperiod solution: no closed form is available in general (unlike the one-period case), only this explicit backward recursion for $d_n$, obtained by folding the claim's payoff into the terminal reward of the exponential-utility Bellman recursion (Theorem 4.2.15). The consistency condition (part c) says the indifference-pricing operator is itself "time-consistent": pricing at time $n$ a claim whose payoff at $n+1$ is the already-computed time-$(n+1)$ price of $H$ recovers $H$'s own time-$n$ price directly.

Milestones

Theorem 4.8.1 (index-tracking's explicit LQ solution: quadratic value functions via the Riccati recursion, linear optimal policy) and Theorem 4.9.2 (the one-period special case of the goal, with a genuinely closed-form price, obtained by directly minimizing a convex one-variable objective). Definition 4.9.1 (the indifference price's defining equation) is needed by both and is a formalization target in its own right, but — being a definition, not a numbered theorem — is never a milestone.

Significance

Theorem 4.8.1 shows that a statistically-motivated portfolio criterion (tracking error, the industry-standard measure of an index fund's fidelity) reduces exactly to a textbook control problem, so every qualitative feature of LQ control — the value function's quadratic form, the policy's linearity in the state, off-line computability of the feedback gain — transfers immediately; the content is the reduction, not a new proof technique. The indifference-pricing results answer a question ordinary arbitrage-free pricing cannot: when a claim's payoff depends on an asset that literally cannot be traded, no replicating portfolio exists, so the no-arbitrage pricing theory of Chapter 3 gives no unique price at all. Theorem 4.9.4 shows the utility-based alternative is nonetheless computable to the same degree of explicitness as ordinary dynamic programming allows: a backward recursion, not a closed form, but a genuine algorithm.

None of these results have machine-checked proofs on Prove2Me at the time of writing. The platform's BertsekasDP.riccati_completion_of_square and related Riccati-family theorems were checked and are not reusable for Theorem 4.8.1: their system matrices are deterministic, with no expectation anywhere in the statement, while this chapter's $A_{n+1},B_{n+1}$ are random and every term of the recursion is an expectation — a genuinely more general result that happens to specialize to the deterministic case, not an instance of it. No substrate at all exists for utility indifference pricing.

Difficulty

For index tracking, the obstacle is not mathematical but representational: recognizing that $(x-\hat s)^2$ is a quadratic form $(x,\hat s)Q(x,\hat s)^\top$ in the augmented state that includes the untradeable index's own value, and that the transition is linear in this augmented state with coefficient matrices that are random only through next period's returns — once this identification is made, Theorem 2.6.3 is already proved and there is nothing further to argue. For indifference pricing, the obstacle is conceptual: Definition 4.9.1 characterizes $v_0$ implicitly, by an equation relating two suprema, not by a formula, so nothing prevents a formalization from simply asserting the closed-form answer as the definition and making the theorem vacuous. A faithful formalization must keep the two apart, proving that the printed formula is a solution of the defining equation rather than building the formula into what "indifference price" means.

Formalization scope

The index-tracking Riccati recursion is restated locally in this chunk's namespace (per the project's rule against importing another chunk's machinery), instantiated to this problem's own $2\times2$ cost matrix and random $2\times2$/$2\times d$ system matrices, using Mathlib's general Matrix inverse (Bᵀ Q B is inverted directly; positive-definiteness making the inverse genuine is not separately hypothesized in the Riccati recursion's own statement, matching how the book treats it as automatic under Assumption (FM)). The one-period and multiperiod indifference-pricing markets are formalized as separate structures (the one-period model's four-atom probability space is pinned down by explicit measure equations on the pair $(\tilde R,\hat R)$, not by an assumed Fin 4 state space, matching the pattern used for the binomial model in chunk 04c). The multiperiod value function VHAt carries an explicit maturity argument distinct from the model's own horizon $N$, needed only to state the goal's consistency condition (part c), which prices a claim maturing one period early. A formalization that defines the indifference price directly as a closed-form expression, rather than as the solution of Definition 4.9.1's equation, would be a trivializing formalization of Theorem 4.9.2 and 4.9.4(b) and is explicitly ruled out. Reusable beyond this mission: the local Riccati-recursion definitions are natural substrate for any later mission needing a stochastic LQ argument with random coefficients (the book's own §2.6.3 general theorem is a natural target for a future chunk). Contributions completing either milestone's sorry, or the goal's, are welcome.

Selected references

• R. E. Kalman, A New Approach to Linear Filtering and Prediction Problems, Journal of Basic Engineering 82(1), 1960, https://doi.org/10.1115/1.3662552
• M. H. A. Davis, Option Pricing in Incomplete Markets, in M. A. H. Dempster, S. R. Pliska (eds.), Mathematics of Derivative Securities, Cambridge University Press, 1997
• 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.8-4.9