Probability

Motivation

An American option may be exercised at any moment up to maturity, so pricing one is not an integration problem but a stopping problem: the holder must decide, at each date and in each state of the market, whether the payoff available now beats the option value of waiting. A perpetual American put pushes this to its limit — there is no maturity at all, so the horizon is unbounded and the problem has no terminal condition to induct backwards from. What replaces the terminal condition is a fixed point characterization, and the classical answer, going back to McKean (1965) and Merton (1973) in continuous time and to Cox, Ross and Rubinstein (1979) in the binomial model, is that the price is the smallest superharmonic majorant of the payoff.

Bäuerle and Rieder's Chapter 11 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own general unbounded-horizon stopping theory rather than from stochastic analysis, and in the same chapter applies the bounded-horizon version to a problem from banking rather than trading: when should a bank cancel a credit line? The two halves share one mathematical shape — a stopping problem whose optimal policy turns out to be of threshold type — and this mission formalizes both, with the perpetual put as the goal.

Setting

The binomial model (§11.1). A stock moves from price $x$ to $xu$ with risk-neutral probability $q$ and to $xd$ with $1-q$, where $0 < d < u$, and the discount factor is $\beta \in (0,1]$. The defining relation of the risk-neutral measure,

$$\beta q u + \beta(1-q)d = 1,$$

is carried as a hypothesis of the model: it is what makes the discounted stock price a martingale, and the proofs use it directly.

The American put with strike $K$ pays $(K-x)^+$ when exercised. With $n$ periods to maturity its price satisfies the recursion $J_0(x) = (K-x)^+$ and

$$J_n(x) = \max\Big\{(K-x)^+,\ \beta\big(q J_{n-1}(xu) + (1-q)J_{n-1}(xd)\big)\Big\} =: \mathcal{T}J_{n-1}(x),$$

the maximum being "exercise now" against "hold". Proposition 11.1.2 describes the price $\pi_n(x) := J_{N-n}(x)$ at time $n$ of an option maturing at $N$: it is continuous in $x$, decreasing in $n$, and — the part that carries the argument — $x \mapsto \pi_n(x) + x$ is increasing, even though $\pi_n$ itself decreases in $x$. That single reformulation, obtained by adding $x$ to both sides of the recursion and using the risk-neutral relation, is what yields the threshold structure: there are exercise boundaries $K =: x_N^* \ge x_{N-1}^* \ge \dots \ge x_0^* \ge 0$ with $\tau^* = \inf\{n \le N \mid X_n \le x_n^*\}$ optimal. Exercise when the stock falls far enough, and the boundary rises as maturity approaches.

The perpetual put (Theorem 11.1.3, the goal). With no expiration date the price at time zero is a supremum over all stopping times, $\tau \le \infty$ included:

$$P(x) := \sup_{\tau \le \infty} \mathbb{E}^{\mathbb{Q}}_x\big[\beta^\tau (K - S_\tau)\big],$$

with the stopping reward set to zero on $\{\tau = \infty\}$. The theorem says four things: $P$ is the limit of the finite-maturity prices $J_n$; $P$ solves $\mathcal{T}P = P$ and satisfies $0 \le P \le K$; $P$ is the smallest superharmonic function majorizing $(K-x)^+$; and, if the value $J_{f^*}$ of the exercise-region policy dominates $\mathcal{T}J_{f^*}$, then $P$ equals that value and $\tau^* = \inf\{n \mid X_n \in E^*\}$, the hitting time of $E^* = \{x \mid P(x) = (K-x)^+\}$, is optimal.

The conditional in part d) is the book's own and is not decoration: without it the exercise region need not deliver an optimal stopping time, and the unconditional version is a different, false statement. The boundedness $0 \le P \le K$ in b) is likewise a genuine claim rather than a side remark — the fixed point equation alone admits other solutions, and it is boundedness together with minimality that pins $P$ down among them.

Credit granting (§11.2). A bank holds a credit contract of maximal duration $N$. Each period it observes a rating class $x_n$ evolving as a Markov process $Q^X$, and chooses to extend — earning $c(x)$ — or to cancel, ending the contract. The value iteration is $J_n(x) = \max\{0,\ c(x) + \beta\int J_{n-1}\,dQ^X(\cdot|x)\}$. Under two structural assumptions — $c$ increasing, and $Q^X$ stochastically monotone, so that a better-rated borrower stays better-rated — Theorem 11.2.1 gives the same shape of answer as the option: cancel exactly when the rating falls below a threshold $x_n^*$, and those thresholds rise as the remaining duration shortens, since a marginal borrower is no longer worth keeping when there is little time left to recover.

Theorem 11.2.2 repeats this when the borrower is not rated at all. The bank has only a prior $\mu_0$ on the repayment probability and one signal per period; the state $(s,n)$ records $s$ positive signals out of $n$, and the expected repayment probability is the posterior mean $q(s,n)$. Monotonicity here is for the order of p. 342 — more positive signals and fewer negative ones — and not the coordinatewise order, under which the claim would be false: an extra signal that is negative makes the state worse.

What is being asked

Formalize Theorem 11.1.3 in full, all four parts: the limit identification, the fixed point equation with its bounds, the minimality among superharmonic majorants, and the conditional optimality of the exercise-region stopping time. The three milestones are Proposition 11.1.2, the finite-horizon put whose threshold structure the perpetual case specializes, and the two credit granting theorems, which run the same bounded-horizon argument on a different model.

The stopping-time apparatus is built rather than assumed: the stock path, the law $\mathbb{Q}$ pinned by its finite-dimensional distributions, stopping times valued in $\mathbb{N}\cup\{\infty\}$, and the reward vanishing at $\infty$. Part a) of the goal is the identification of the supremum with $\lim_n J_n$, so carrying $P$ as an abstract function would make the theorem vacuous.

Motivation

Every mission in this series so far has treated a control problem that already lives in discrete time: a decision maker observes a state, chooses an action, and the process moves to a new state at the next integer time step. Many real systems evolve in continuous time instead — a machine that runs deterministically until it randomly breaks down and is repaired into a new condition, an inventory that drains continuously until a random demand arrives, a population that grows deterministically between random catastrophic events. Chapter 8 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) shows that an entire class of such continuous-time control problems — Piecewise Deterministic Markov Decision Processes, where the state moves along a deterministic, controlled flow between randomly-timed jumps to a new state — can be solved by exactly the discrete-time machinery this book's series has already built, once the problem is re-expressed as a Markov Decision Model at the jump times themselves. This mission covers that embedding and its consequences (§8.2), and a simpler, discrete-state special case, the continuous-time Markov Decision Chain, treated with both an infinite and a finite time horizon (§8.3).

Setting

A Piecewise Deterministic Markov Decision Model (Definition 8.1.1) consists of a Borel state space $E$, a Borel control space $U$, a deterministic drift $\mu(x,u)$ governing the flow $\varphi^\alpha_t(x)$ between jumps, a Poisson jump clock of rate $\lambda$, a kernel $Q$ giving the distribution of the post-jump state, a reward rate $r$, and a discount rate $\beta$. A control is a whole measurable function $\alpha : \mathbb R_{\ge0} \to U$ fixed at each jump time and applied until the next one — so the "action space" of the embedded discrete-time problem is itself a function space, a genuinely new technical wrinkle this book's earlier chapters never face. Embedding at the jump times produces a discrete-time Markov Decision Model $(E,A,Q',r')$ whose reward and kernel are themselves integrals of the original data against the flow (Eqs. (8.4)-(8.5)); Chapter 7's infinite-horizon existence theory, already developed for a general Borel state space, applies directly to this embedded model once its own compactness and semicontinuity hypotheses are checked. Checking them forces a further enlargement of the control space to the relaxed controls $R$ — measurable functions into probability measures on $U$ rather than $U$ itself — which is compact in a suitable topology where the space of literal control functions is not.

Formalization targets

The goal, Theorem 8.2.6, is the chapter's central existence result: given a continuous upper bounding function with the discrete embedded model's own contraction-type condition and a package of continuity/compactness assumptions, the value function of the model embedded with relaxed controls is bounded, upper semicontinuous, and a genuine fixed point of the maximal- reward operator, and an optimal relaxed Markov policy exists. The milestones build up to it and extend past it: Theorem 8.2.1 establishes the foundational fact that the continuous-time expected reward of the original process equals the discrete-time embedded model's own value — the correspondence every other result in the chapter relies on; Lemma 8.2.5 is the technical semicontinuity-preservation step the goal's proof needs; Theorem 8.2.7 upgrades the goal's relaxed optimal policy to a genuine, nonrelaxed one under an uncontrolled-flow or convexity condition; Theorem 8.2.8 gives the classical Hamilton-Jacobi-Bellman verification technique as an alternative, differential route to the same value function. Section 8.3's continuous-time Markov Decision Chain — the same theory specialized to a countable state space, transition rates in place of a kernel, and an uncontrolled flow — is covered for both an infinite horizon (Theorem 8.3.1) and, the more finance-relevant case, a finite horizon with a terminal reward (Theorems 8.3.2-8.3.3).

Significance

Piecewise Deterministic Markov Processes have no substrate anywhere in Mathlib or on the platform, and this mission's content is a genuine method, not just a specialization of existing results: it shows how to reduce an entire continuous-time control problem to the discrete-time theory already available, at the cost of enlarging the state of the discrete embedded problem's own data (which becomes an integral against a whole flow, not a pointwise value) and enlarging the control space when compactness is needed for existence. This mission is careful to keep two distinctions the book itself insists on separate: relaxed versus nonrelaxed controls (Theorem 8.2.6 produces only the former; recovering the latter is Theorem 8.2.7's own, harder, conditional content), and the general Piecewise Deterministic model of §8.1-8.2 versus the simpler, discrete-state Markov Decision Chain of §8.3, which is a genuinely different structure (sums over a countable state space rather than integrals against a controlled flow), not an instance of the general model specialized after the fact.

Difficulty

The central formalization challenge is representing the continuous-time expected reward $V^\pi(x)$ (Eq. (8.2)) faithfully, since the book itself only asserts the existence of a probability space carrying the jump-time/post-jump-state process with a specified conditional law, citing general marked-point-process theory rather than constructing it. This mission builds that probability-space data directly — via Mathlib's conditional expectation, conditioning on the current post-jump state — rather than treating $V^\pi$ as a bare hypothesis-only quantity, so that Theorem 8.2.1's value-equality claim is a genuine, non-vacuous correspondence between two independently-defined objects (a continuous-time path functional and a discrete-time recursion) rather than true by definitional fiat. A second, compounding difficulty is that the same correspondence must be built twice — once for the general flow-driven process (§8.2) and again, independently, for the discrete-state jump process of the finite-horizon chain (§8.3) — since the two models share no state-space structure. A third difficulty specific to Theorem 8.2.8 is that its Hamilton-Jacobi-Bellman verification argument is genuinely differential (a process generator built from a gradient, a self-referential closed-loop control solving its own ODE), unlike every other result in this chapter, which works through the discrete-time embedding alone.

Formalization scope

The book's own topology on the control-function space $A$ (the coarsest making certain integrals measurable) and the Young topology on the relaxed-control space $R$ (which the book cites as making $R$ separable, metric and compact, without reconstructing it) are not rebuilt from scratch; continuity/compactness hypotheses that need a topology on these spaces are stated directly against the pointwise/product topology on the underlying function types, a faithful but representationally simpler stand-in documented in MODERATION_NOTES.md. The embedded kernel $Q'$ (Eqs. (8.4), (8.7)) is bundled as data satisfying its own defining integral identity rather than literally constructed as a mixture of pushforward measures — a routine but heavy argument that would add no mathematical content beyond the formula itself. This mission's own goal (Theorem 8.2.6) explicitly produces a relaxed-control optimal policy, not a nonrelaxed one: stating it with a $U$-valued policy instead would silently substitute Theorem 8.2.7's strictly harder, conditionally-true conclusion for Theorem 8.2.6's own unconditional one, exactly the trivializing formalization this chapter's own structure warns against.

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.
• M. H. A. Davis, Markov Models and Optimization, Chapman & Hall, 1993 (the standard reference for Piecewise Deterministic Markov Processes, cited by the book for extensions of this chapter's basic model).
• A. A. Yushkevich, "On reducing a jump controllable Markov model to a model with discrete time", Theory of Probability and its Applications, 1980 (the topology on the control-function space $A$ cited by Definition 8.1.1's own construction).
• H. J. Kushner and P. G. Dupuis, Numerical Methods for Stochastic Control Problems in Continuous Time, 2nd ed., Springer, 2001 (the Young topology and the Chattering Theorem, cited by Remark 8.2.3).
• N. Bäuerle and U. Rieder, "Optimal control of piecewise deterministic Markov processes with finite time horizon", in Modern Trends of Controlled Stochastic Processes: Theory and Applications, 2010 (cited for the finite-horizon extension of this chapter's model, applied in chunk 09b's Sections 9.3-9.4).

Motivation

Every mission in this series so far has treated a finite-horizon decision problem: an investor or planner with a fixed, known number of periods left. Many of the most important applications — perpetual investment, an infinitely-repeated inventory or maintenance problem, a firm that never stops operating — have no natural end date at all. Chapter 7 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds the theory needed to make sense of "the value of a decision problem that never ends," and does so on a general Borel state space rather than a finite one. This mission covers the chapter's first three sections: the general infinite-horizon setup, the semicontinuous existence theory that makes it usable, and the sharper contraction-based theory that is the chapter's, and arguably the whole book's, theoretical center.

Setting

An infinite-horizon Markov Decision Model reuses the same data $(E,A,D,Q,r,\beta)$ as the finite-horizon models of earlier chapters, but drops the terminal reward and applies a single (possibly randomized) decision rule at every one of infinitely many stages. Its performance criterion, $J_\infty(x) := \sup_\pi \mathbb E^\pi_x\big[\sum_{k=0}^\infty \beta^kr(X_k,f_k(X_k)) \big]$, is only meaningful once an integrability condition (Assumption (A)) and a convergence condition (Assumption (C)) rule out the sum diverging or the finite-horizon approximations failing to settle down. Both conditions follow automatically once the model has an upper bounding function $b$ — a function controlling both the size of the reward and how fast the transition kernel can grow $b$ itself — with $\beta\alpha_b < 1$, the manageable special case that covers both the classical bounded-reward discounted case and the case of a non-positive reward.

Formalization targets

The goal, Theorem 7.3.5 (Structure Theorem), is the chapter's capstone: under a genuine bounding function (a two-sided reward bound making the space $IB_b$ of finite-weighted-norm functions a Banach space) with $\beta\alpha_b < 1$, and one abstract structural hypothesis — a closed class $IM \subset IB_b$ containing $0$, mapped into itself by the Bellman operator $T$, on which a maximizing action always exists — Banach's fixed point theorem delivers existence, uniqueness, an explicit geometric convergence rate for value iteration, and existence of an optimal stationary policy, all at once. The milestones build up to it in three stages: the general infinite-horizon machinery (Lemmas 7.1.4-7.1.5, Theorems 7.1.6-7.1.8 — reward iteration, a verification theorem, and a structure theorem under an abstract structure assumption that is not yet tied to any checkable property of the model); the semicontinuous existence theory that gives primitive, checkable conditions implying that abstract assumption (Theorem 7.2.1 and its two corollaries, including a genuine policy iteration conclusion); and the contracting theory proper (Lemma 7.3.3's contraction estimate, Theorem 7.3.4's sharpened verification theorem, and Theorem 7.3.6's continuous specialization of the goal).

Significance

The goal is the direct, general-Borel-space generalization of what finite-state dynamic programming theorems already on the platform (BertsekasDP.discounted_main_theorem, BertsekasDP.ssp_main_theorem) establish only for a finite state and action space, where Banach's theorem is applied directly on $\mathbb R^n$: this mission's content is that the same conclusions — including the same explicit geometric convergence rate for value iteration — hold on an arbitrary Borel state space, the moment one abstract, structural condition is checked. That condition is not vacuous or automatic: Example 7.2.4 (cited but not itself formalized, being an unnumbered worked counterexample rather than a numbered result) shows that without compactness of the feasible-action correspondence, the naive Structure Assumption of Chapter 2 is not enough and value iteration can converge to the wrong limit ($J \ne J_\infty$). Theorems 7.1.8's Structure Assumption (SA) is built precisely to rule this out, and Theorem 7.2.1's semicontinuity/ compactness conditions are the practical, checkable sufficient conditions for it.

Difficulty

The central formalization challenge is representing $J_\infty^\pi$, the genuine infinite-horizon expected discounted reward, without constructing a canonical infinite-horizon path measure from the model's transition kernel — a substantial undertaking the book itself sidesteps by proving (via an appendix result, Theorem B.1.1, not itself reproved here) that $J_\infty^\pi$ equals the limit of the finite-horizon truncations $J_n^\pi$. This mission takes that limit characterization as its own definition, via Filter.limsup for the same total, junk-safe reasons this book's series has used throughout (no canonical path measure anywhere in chunks 02a, 05a, 05b, 06). A second, genuinely new difficulty is Ls, the "upper limit of a sequence of sets" that drives every policy-iteration conclusion: it is a statement about accumulation points of a sequence of points, one drawn from each set in the sequence, not the more familiar set-theoretic limsup of a sequence of sets — getting this distinction right is the entire content of what "policy iteration" asserts.

Formalization scope

Every operator, bounding-function class, and value function of §7.1-7.3 is restated (not imported) in this chunk's own namespace from the finite-horizon originals of chunks 02a/02b, adapted to drop the time index and bake the discount into the one-stage operator directly, per this chapter's own presentation. The contracting theory's genuinely real-valued Banach-space objects ($T_f'$, $T'$, $IB_b$, the weighted norm $\|\cdot\|_b$) are kept separate from the general theory's EReal-valued objects ($T_f$, $T$, $IM(E)$), matching the book's own distinction between a value function that is a priori only known to avoid $+\infty$ and one known to be genuinely finite everywhere. Part (d) of the goal — the explicit geometric convergence rate — is stated in full, not weakened to bare qualitative convergence, since a formalization that dropped it would lose exactly the fact (used again by this book's own Theorem 7.5.12, a different chunk) that makes value iteration a genuine numerical method with a computable error bound rather than merely an existence argument.

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, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012 (the finite-state discounted/SSP theorems this goal generalizes).
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (analytic measurability of $J_\infty$, $J$; cited by the book for this chapter's foundational measure-theoretic facts).
• K. Hinderer, Foundations of Non-stationary Dynamic Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970 (Theorem 18.4, cited for the fact that history-dependent policies do not improve on Markov ones).

Motivation

Every portfolio-choice model treated so far in this series assumes the investor knows the exact law governing the market's returns. Real investors do not: the drift of a stock, the regime a market is in, or the probability of an up-move in a simplified binomial model is itself uncertain and must be learned from the very prices being observed. Bäuerle and Rieder's Chapter 6 (Markov Decision Processes with Applications to Finance, Springer, 2011) is the book's synthesis of two threads developed separately earlier: Chapter 5's reduction of a partially observable decision problem to an ordinary one on an enlarged "belief" state space, and Chapter 4's classical solutions of terminal-wealth utility maximization and dynamic mean-variance portfolio choice. Combining them answers a natural question with no simple a priori answer: how does not knowing which market you are in change the qualitatively optimal way to invest, and can the closed-form solutions of the fully-observed theory be recovered, term for term, once the unknown factor is replaced by a belief about it?

Setting

The market has an unobservable factor Y (state space E_Y) driving the vector of relative risks Z ∈ ℝ^d of d risky assets: given Y_n = y, the next return Z_{n+1} has a density q_R(y,\cdot), and Y itself evolves via its own transition density q_Y(y,\cdot), jointly — crucially, this joint law depends only on y, never on wealth or the action taken. An investor observes only the stock prices (equivalently, the return history), never Y itself. Bayes' rule turns this into a filtering problem: the investor's belief ρ_n \in \mathbb P(E_Y) about the current factor is updated one return at a time by an operator Φ(ρ,z) that depends only on the current belief and the newly observed return — a genuine simplification of Chapter 5's general Bayes operator, forced by the market's own structure. The pair (x_n,ρ_n) — observable wealth and current belief — is then an ordinary, fully observed state for an ordinary Markov Decision Model, and every value function and optimal policy of this chapter lives on that enlarged state space.

Formalization targets

The goal, Theorem 6.2.3, solves the dynamic mean-variance problem (MV): minimize the variance of terminal wealth X_N subject to a target expectation \mathbb E[X_N] \ge \mu, under partial observation. It is reached by a Lagrangian embedding into an auxiliary quadratic-loss problem QP(b), solved explicitly in Theorem 6.2.2, whose value function factors as ((xS^0_N/S^0_n)-b)^2 d_n(\rho) for a belief-only sequence (d_n) satisfying the backward recursion (6.7); Lemma 6.2.1 shows this sequence always lies strictly between 0 and 1, which is exactly what makes the final variance formula and Lagrange multiplier well-posed. The remaining milestones develop the parallel terminal-wealth theory of §6.1: the general structure theorem (Theorem 6.1.1), its power- and logarithmic-utility closed forms (Theorems 6.1.2, 6.1.7), and — for the specific binomial market with an unknown up-probability — a likelihood-ratio monotonicity result for the filter update (Lemma 6.1.4) and a comparison between the partially and completely observed optimal investment fractions (Theorem 6.1.5).

Significance

The chapter's organizing insight is that partial observation does not require a new theory: once the belief is added as a state coordinate, every general result already proved for fully observed Markov Decision Models — the Bellman equation, the existence of optimal Markov policies, the Lagrangian embedding technique for mean-variance problems — applies unchanged. What is genuinely new, and genuinely non-trivial, is checking that the reduced model inherits the structural hypotheses (monotonicity, boundedness, positive-definiteness of covariance matrices) those general theorems require, expressed now as conditions on the belief-indexed quantities Φ(ρ,z), d_n(\rho), \ell_n(\rho), C_n(\rho) rather than on the original, unobserved factor. Theorem 6.1.5's comparison result is a genuinely new phenomenon with no fully-observed analogue at all: it quantifies, in the two opposite directions dictated by the sign of the risk-aversion parameter γ, how residual uncertainty about the market itself changes the qualitatively optimal amount to invest — the discrete-time analogue of a continuous-time result in the literature this book cites (Sass and Haussmann 2004).

Difficulty

The recurring difficulty across every result in this mission is that the reduced model's state space E_X \times \mathbb P(E_Y) includes a space of probability measures as one coordinate, and every quantity that must be shown well-defined, monotone, or bounded is a functional on that space, not a function on a concrete Euclidean set. Formalizing the mean-variance recursion (6.7) in particular is a three-way mutual computation — a scalar d_n(\rho), a vector \ell_n(\rho), and a matrix C_n(\rho), each an integral against the same belief-dependent predictive law of the next return, each feeding the next stage's version of all three — where Lemma 6.2.1's strict-inequality bound is not a bookkeeping detail but exactly the fact that keeps C_n(\rho) invertible and the whole construction from breaking down. Theorem 6.2.3 itself is the hardest single step: verifying that the specific constant b^* the Lagrangian method selects makes the mean constraint bind at exact equality, and that the resulting variance is the true constrained minimum (not merely a feasible value), is exactly the non-trivial content a superficial restatement of Theorem 6.2.2 at an unspecified b would silently discard.

Formalization scope

Every value function of this chapter — the terminal-wealth maximization of §6.1, the quadratic loss QP(b) and the mean-variance problem (MV) of §6.2 — is built from one shared history-dependent value-function scaffold, parametrized by its terminal payoff (the utility U, a quadratic loss, or the raw first/second moment), its rate sequence (constant in §6.1, non-stationary in §6.2), and its feasible-action correspondence, rather than four separately re-derived constructions. Optimal fractions in the binomial sub-model (Lemma 6.1.4, Theorem 6.1.5) are characterized as any maximizer of the relevant one-step concave problem rather than through the closed-form solution the book's own proof derives via machinery from a different, unavailable chunk (Lemma 4.2.9) — the comparison and monotonicity results proved here are facts about any such maximizer, not about that specific formula. A formalization that assumed the reduced model's filter update or covariance structure directly, rather than deriving it from the market's own return and factor densities via the Bayes operator Φ, would trivialize every result in this mission; none of the items here take that shortcut.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• R. Sass and U. G. Haussmann, "Optimizing trading strategies with respect to drawdown in the hidden Markov model," Statistics & Decisions, 2004.
• N. Bäuerle and U. Rieder, "Portfolio optimization with unobservable Markov-modulated drift process," Journal of Applied Probability, 2007.
• V. Runggaldier, W. Trivellato, and T. Vargiolu, "A Bayesian adaptive control approach to parameter estimation and optimal portfolio selection," in Mathematical Finance, Trends in Mathematics, Birkhäuser, 2002 (the binomial-market source this chapter's §6.1 example specializes).

Motivation

A decision maker who does not know the true parameters of the system they are controlling — the success probability of a slot machine, the drift of an asset, the failure rate of a machine — faces a genuinely different problem from one who knows them: every action taken has two effects, an immediate payoff and a change in what is known. Formalizing this "explore versus exploit" tension precisely is the subject of Bayesian sequential decision theory, whose best-known instance is the multi-armed bandit problem (Robbins, 1952; Gittins and Jones, 1974). Bäuerle and Rieder's treatment (Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5) gives the finite-horizon Bayesian theory its cleanest general form: rather than analyzing each bandit variant from scratch, it builds one reduction — from a Markov Decision Model with an unknown parameter to an ordinary, fully observed Markov Decision Model on an enlarged "information state" — and one structural theorem that turns primitive monotonicity hypotheses on the original ingredients into monotonicity of the optimal policy in the information state. Two classical finite-horizon bandit results (Theorems 5.5.1, 5.5.2) then follow as applications, not separate proofs.

Setting

A Bayesian Model is a Markov Decision Model whose unobservable component is a single, never-changing, unknown parameter $\theta$, drawn once from a prior distribution $Q_0$ on a parameter space $\Theta$. Concretely: an observable state space $E_X$, an action space $A$, a disturbance space $Z$ with reference measure $\nu$, a feasible set $D \subseteq E_X \times A$, a deterministic transition $T^X : E_X \times A \times Z \to E_X$, a disturbance density $q_Z(x,\theta,a,z)$, a reward $r(x,\theta,a)$, a terminal reward $g(x,\theta)$, and a discount $\beta \in (0,1]$.

Because $\theta$ is never observed directly, the decision maker's state of knowledge at stage $n$ is the posterior $\mu_n(\cdot \mid \tilde h_n)$, the conditional law of $\theta$ given the full observable history $\tilde h_n = (x_0,a_0,z_1,\dots,x_n)$. Bayes' rule updates this posterior one disturbance at a time; unrolling the update gives $\mu_n$ an explicit closed form as a product of likelihoods against the prior (Lemma 5.4.1), and the process $\mu_n(C\mid \cdot)$, for any fixed event $C$, is a martingale (Lemma 5.4.2) — it is, after all, a sequence of conditional expectations of the same random variable $\mathbf 1_{\theta \in C}$ against a refining amount of information.

Often the whole posterior is not needed to act optimally: a sufficient statistic $t_n$ compresses $\tilde h_n$ into a value in some space $I$ from which $\mu_n$ can still be recovered, and it is sequential if $t_{n+1}$ updates from only $(x_n, t_n, a_n, z_{n+1})$. Given a sequential sufficient statistic, the information-based Markov Decision Model replaces the never-observed $\theta$ by the always-computable $t_n$ as the second state coordinate, giving an ordinary Markov Decision Model on $E_X \times I$ whose reward, terminal reward, and transition law are the original ones averaged against the current posterior $\hat\mu(\cdot\mid i)$.

Formalization targets

$$\textbf{Theorem 5.4.10.} \quad \begin{aligned} &\text{Given: } D(\cdot) \text{ increasing; } q_Z(\cdot\mid\theta,a) \le_{lr} q_Z(\cdot\mid\theta',a) \text{ for } \theta \le \theta'\text{; } (x,z)\mapsto T^X(x,a,z),\\ &(\theta,x)\mapsto r(\theta,x,a),\ (\theta,x)\mapsto g(\theta,x) \text{ increasing; every increasing } v \in IB_b^+ \text{ has a maximizer in } \Delta.\\ &\text{Then: } IM := \{v \in IB_b^+ \mid v \text{ increasing}\} \text{ and } \Delta \text{ satisfy the Structure Assumption.} \end{aligned}$$

This is the weakest, most reusable form of the result: it names exactly the primitive hypotheses on the original model's ingredients under which the reduced model's Bellman equation holds and its value function and an optimal policy are monotone in the information state — without fixing which bandit or estimation problem those ingredients come from. Theorems 5.5.1 and 5.5.2 are downstream applications kept as milestones, not additional goals: proving the general theorem subsumes verifying its hypotheses in each concrete case.

Significance

Every one of the classical finite-horizon two-armed-bandit results — "switch to the arm with higher posterior mean once the advantage function is nonnegative," "never abandon a winning arm," "once you commit to the known arm, never leave it" — is, in this book's organization, a one-page corollary of Theorem 5.4.10 plus a routine (if occasionally fiddly) check of its five hypotheses on a two- or four-dimensional concrete state space. The theorem is what makes the qualitative behavior of an optimal bandit policy provable in general, rather than re-derived by induction for each new bandit variant.

Formalizing it also isolates, in one place, exactly which comparison of distributions (likelihood-ratio order, not the weaker stochastic order) makes the reduction go through, and exactly which practically checkable joint-density condition (MTP2) implies it (Lemma 5.4.9) — a genuinely reusable piece of probability theory beyond Markov decision theory.

Difficulty

The obvious first idea — "the information state's order is defined via the likelihood ratio order on posteriors, so just check the transition kernel is stochastically monotone and invoke the general increasing-model theorem of Chapter 2" — hides the actual difficulty: the state space of the reduced model is $E_X \times I$, and $I$ is itself a space of posterior distributions, so "the transition kernel is monotone" is a statement about how the whole posterior moves when a new observation arrives, not a fact about $E_X$ alone. The crux is showing that the sequential-sufficient-statistic update $\hat\Phi$ is jointly increasing in the current information state and the new disturbance — and this is exactly where Lemma 5.4.9's MTP2 characterization does the real work: MTP2 of the disturbance density in $(z,\theta)$ is what turns "a good disturbance is more likely under a good $\theta$" into "an increasing information state produces an increasing posterior update," without which the hypotheses on $D$, $T^X$, $r$, $g$ alone would not propagate to the enlarged state space at all.

Formalization scope

The Bayesian Model, its posterior, and the information-based model are formalized as they are introduced in the book: BayesModel bundles the primitive data (disturbance density, prior, reward, discount); Posterior bundles the filter $(\mu_n)$ as data satisfying its defining one-step Bayes update, rather than constructed from a canonical probability space, matching how MDPFinance.POMDP.FilterData (chunk 05a) treats the general Bayes operator; the Structure Assumption, Bellman operators, and bounding-function machinery of Chapter 2 are restated specialized to the stationary form the information-based model needs. "$\Theta, Z \subseteq \mathbb R$" and "$q_Z$ independent of $x$" (the "Monotonicity Results" subsection's own standing simplifications) are carried as explicit hypotheses of Lemma 5.4.9 and the goal, not silently dropped. A formalization that merely assumed the reduced model's disturbance kernel monotone, rather than deriving it via Lemma 5.4.9 from the checkable hypothesis on $q_Z$, would trivialize the theorem; this one keeps hypothesis (ii) exactly as the book states it. The two bandit applications (Theorems 5.5.1, 5.5.2) are formalized as self-contained concrete finite (countable-state, finite-action) Markov Decision Models, since the book itself reduces them to explicit recursions before stating the results — no general measure-theoretic machinery is needed there. Reusable beyond this mission: the likelihood-ratio order and MTP2 definitions (LikelihoodRatioOrder, IsMTP2), applicable to any Bayesian comparison result.

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.
• H. Robbins, "Some aspects of the sequential design of experiments," Bulletin of the American Mathematical Society, 58(5), 1952, 527-535.
• J. C. Gittins and D. M. Jones, "A dynamic allocation index for the sequential design of experiments," in Progress in Statistics, 1974.
• A. Müller and D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (the book's own reference for the likelihood-ratio order and MTP2 functions, Appendices A.3, B.3).

Motivation

Every model in Chapters 2-4 assumed the controller sees the whole state before acting. Real control problems rarely offer that: a machine's true wear level, a customer's private valuation, a hidden regime driving asset returns — these are exactly the situations a decision-maker must act on despite never observing them directly, learning about them only through their effect on what is observed. This is the subject of Partially Observable Markov Decision Processes (POMDPs), introduced independently in operations research (K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, 1965) and studied extensively since as the right model for sequential decisions under hidden state. The central difficulty such a process raises is structural, not just computational: the state includes a component the controller never sees, so the very theory built in Chapter 2 — which assumes the controller's policies can depend on the full current state — does not apply. Bäuerle and Rieder's Chapter 5 resolves this by an idea with a long pedigree in stochastic control (Bayesian filtering, going back to R. E. Kalman and R. S. Bucy's filtering theory, and D. Blackwell's 1965 discounted-dynamic-programming treatment of the "state of information"): replace the unobservable state by the controller's own belief about it — a probability distribution, updated at every step by Bayes' rule — and show the resulting belief-state process is once again an ordinary, fully observed Markov Decision Model.

Setting

A Partially Observable Markov Decision Model (Definition 5.1.1) has data $(E_X\times E_Y, A, D, Q, Q_0, r, g, \beta)$: state $(x,y)\in E_X\times E_Y$ with $x$ observable and $y$ unobservable; feasible actions $D(x)$ depending only on $x$; a stochastic kernel $Q$ giving the joint law of the next state; initial law $Q_0$ of $Y_0$; rewards $r,g$; discount $\beta$. A policy $\pi=(f_0,\dots,f_{N-1})\in\Pi_N$ (Definition 5.1.3) is a sequence of decision rules $f_n:H_n\to A$, each depending only on the observable history $H_n=(x_0,a_0,\dots,x_n)$ — never on any $y_k$. The objective

$$J_N^\pi(x) := \int \mathbb{E}_{xy}^\pi\Big[\sum_{n=0}^{N-1}\beta^n r(X_n,Y_n,A_n) + \beta^N g(X_N,Y_N)\Big] Q_0(dy), \qquad J_N(x):=\sup_{\pi\in\Pi_N} J_N^\pi(x)$$

(Equation (5.2)) carries an extra expectation over the unknown $Y_0$ that Chapter 2's objective never had.

Assuming $Q$ has a density $q$ against reference measures, the Bayes operator $\Phi$ and the filter recursion $\mu_0:=Q_0$, $\mu_{n+1}(\cdot\mid h_n,a_n,x_{n+1}):=\Phi(x_n,\mu_n(\cdot\mid h_n),a_n,x_{n+1})$ (Equations (5.3)-(5.4)) compute the posterior law of $Y_n$ given everything observed, purely from the observable history. Theorem 5.2.1 confirms $\mu_n$ is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats $(x,\mu_n)\in E:=E_X\times\mathbb{P}(E_Y)$ as an ordinary, fully-observed state, with its own kernel $Q'$ (built from $\Phi$ and the marginal $Q^X$), reward $r'(x,\rho,a):=\int r(x,y,a)\rho (dy)$, and terminal reward $g'(x,\rho):=\int g(x,y)\rho(dy)$.

Formalization targets

Goal — Theorem 5.3.3

$$J_0'(x,\rho) = g'(x,\rho), \qquad J_n'(x,\rho) = \sup_{a\in D(x)}\Big[r'(x,\rho,a) + \beta\int J_{n-1}'(x',\rho')\,Q'(d(x',\rho')\mid x,\rho,a)\Big] \quad (1\le n\le N),$$

under the Structure Assumption of Theorem 2.3.8; and if $f_n'$ maximizes $J_{n-1}'$ for each $n$, then $f_n^*(h_n):=f_{N-n}'(x_n,\mu_n(\cdot\mid h_n))$ defines a policy optimal for the original $N$-stage POMDP. This is where the reduction pays off: an ordinary Bellman equation, of exactly the form Chapter 2 already solves, for a problem that had no Bellman equation at all in its original, partially-observed form.

Milestones

Lemma 5.2.2 (the filter-recursion identity, the technical engine behind everything that follows), Theorem 5.2.1 (the filter is truly the conditional law — without this, $\mu_n$ would be merely a formula, not a meaningful belief), and Theorem 5.3.2 (the value of the filtered model exactly equals the value of the original POMDP, policy for policy — without this, solving the filtered model would solve a different problem).

Significance

Theorem 5.3.3 is the standard justification, made precise, for the single most common technique in applied sequential decision-making under uncertainty: replace an unknown parameter or hidden state by a running Bayesian estimate, and optimize as if that estimate were the true state. This technique underlies applications from inventory control with unknown demand to adaptive clinical trial design, and Chapter 5's own closing application (two-armed Bernoulli bandits, taken up in chunk 05b) is a direct instance. The reduction also has real content beyond convenience: it shows the value is unchanged (Theorem 5.3.2), not merely that a good heuristic policy exists — the filtered model's optimum is the true POMDP optimum, not an approximation to it.

No result of this chapter has a machine-checked proof on Prove2Me at the time of writing, and no substrate exists for POMDPs, filtering, or Bayes-operator constructions on the platform. Formalizing this mission means building, from Mathlib's general kernel and probability-measure infrastructure, the first POMDP/filtering vocabulary on the platform: a policy class restricted to observable histories, a recursively-computable posterior, and the value-equality between a partially and a fully observed reformulation.

Difficulty

The obstacle is not any single hard inequality but a representational one: an admissible policy for the original problem is a function of a growing observable history, not of a fixed-size state, so the value function $J_N^\pi$ cannot be written as a simple recursion over a Markov chain the way every earlier chapter's could. The chapter's insight is that the belief $\mu_n$ — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: $\mu_{n+1}$ depends on the observable history only through $(x_n,\mu_n)$, never on more of the past. Recognizing this, and giving $\mathbb{P}(E_Y)$ the right measurable structure to serve as a genuine Borel state space, is what makes Definition 5.3.1's reformulation a legitimate Markov Decision Model rather than an informal analogy. A formalization that let $\mu_n$'s type be an unstructured "distribution object" with no Borel structure, or that quietly assumed the value functions of the filtered model already satisfy the Bellman equation, would miss this content entirely.

Formalization scope

$E_X,E_Y,A$ are abstract measurable spaces; the transition kernel $Q$ is a genuine MeasureTheory.Kernel, not assumed to arise from an i.i.d.-noise-driven transition function (the form every earlier finance chapter's market used) — the chapter's own examples (Hidden Markov Models, Bayesian models) do not have that special form in general. Observable histories are represented as (junk-padded) sequences $\mathbb{N}\to E_X$, $\mathbb{N}\to A$ rather than dependent finite tuples, with a decision rule's dependence on only the first $n{+}1$/$n$ coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping while remaining exactly equivalent to the book's own $H_n\to A$ typing. The belief state $\rho$ is MeasureTheory.ProbabilityMeasure E_Y, giving $E_X\times\mathbb{P}(E_Y)$ a genuine measurable structure via its standard weak-topology Borel σ-algebra — the formalization scope this chunk's own pitfall demands, ruling out an ad hoc encoding of "the space of distributions." The Bayes operator $\Phi$ and the filtered kernel $Q'$ are carried as data (functions landing genuinely in ProbabilityMeasure/Kernel types) characterized by their defining ratio-of-integrals or pushforward formulas, rather than constructed by normalizing a raw measure inline — proving that normalization is a routine Fubini calculation the book itself does not spell out, and would be proof content misplaced in a definition. Theorem 5.2.1's conditional-probability statement is formalized via the book's own Equation (5.5) test-function identity rather than Mathlib's conditional-expectation-with-respect-to-a-sub-σ-algebra machinery, since the two are equivalent by the standard characterization of conditional expectation and the test-function form is what the book's own proofs actually use. The Structure Assumption of Theorem 2.3.8 is restated locally (existential value-function and decision-rule classes with its three defining clauses), per this project's rule against importing another chunk's copy of shared machinery. Reusable beyond this mission: the kernel-based expectation recursion (Ex/Vpi) is natural substrate for any later mission needing a Markov Decision Process driven by a genuinely abstract stochastic kernel rather than an i.i.d.-noise transition function. Contributions completing any milestone's sorry, or the goal's, are welcome.

Selected references

• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1), 1965, https://doi.org/10.1016/0022-247X(65)90154-X
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 1965, https://doi.org/10.1214/aoms/1177700285
• R. E. Kalman, R. S. Bucy, New Results in Linear Filtering and Prediction Theory, Journal of Basic Engineering 83(1), 1961, https://doi.org/10.1115/1.3658902
• 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 5, §§5.1-5.3

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

Motivation

A manufacturer that makes several products must decide, before demand is known, how much capacity to buy. It can buy dedicated capacity, one resource per product, or a single flexible resource that can make every product. Flexible capacity pools demand: a surplus of one product's demand can be served by capacity that would otherwise sit idle. A common intuition in the operations literature holds that a flexible strategy is preferable to a dedicated one when the unit costs are equal, and much of that literature therefore assumes the flexible resource costs more (for example Van Mieghem 1998).

Tomlin and Wang (2005) examine when this intuition is valid for firms that are not risk neutral and whose resources may fail. Their answer has two halves. A risk-neutral firm always values flexibility, whatever the reliability of its resources (their Proposition 1). A firm with perfectly reliable resources also always values flexibility, whatever its attitude to risk, as long as it prefers more wealth to less (their Proposition 4). When neither condition holds, dedicated capacity can be strictly preferred (their Remark 1 and numerical study). This mission formalizes the second half.

Setting

There are $N$ products with a common contribution margin $p>0$. The random demand vector is $\tilde X=(\tilde X_1,\dots,\tilde X_N)$, nonnegative, with an arbitrary joint distribution on a probability space. The firm has initial wealth $w_0$.

• In the dedicated network SD, the firm invests $K_n\ge 0$ in a resource that can make only product $n$, at marginal total cost $c>0$ per unit. With perfectly reliable resources the whole investment is delivered, and the terminal wealth is

$$w^{SD}(K)=w_0+p\sum_{n=1}^N\min\{\tilde X_n,K_n\}-c\sum_{n=1}^N K_n .$$

• In the flexible network SF, the firm invests $K_{N+1}\ge0$ in one resource that can make every product, at marginal total cost $c_{N+1}$, and the terminal wealth is

$$w^{SF}(K_{N+1})=w_0+p\min\Big\{\sum_{n=1}^N\tilde X_n,K_{N+1}\Big\}-c_{N+1}K_{N+1}.$$

The firm chooses its investment to maximize one of three objectives of terminal wealth $W$, with profit $\tilde W=W-w_0$:

1. an expected utility $E[u(W)]$, where $u$ ranges over $U_1$, the set of utility functions that are nondecreasing in wealth;
2. the loss-averse objective $V_{LA}=w_0+E[\tilde W^+-\beta\tilde W^-]$ with $\beta\ge 1$;
3. the CVaR objective $V_{CVaR_\eta}=w_0+\max_v\{v+\tfrac1\eta E[\min\{\tilde W-v,0\}]\}$ with $\eta\in(0,1]$, the mean of the left $\eta$-tail of wealth.

SF is (weakly) preferred when its optimal objective value is at least that of SD. The flexibility premium is $\Delta=(c^I_{N+1}-c)/c$, where the indifference cost $c^I_{N+1}$ is a flexible cost at which the firm is indifferent between the networks; the firm prefers SF as long as $c_{N+1}\le(1+\Delta)c$.

Formalization targets

Goal: Proposition 4

With perfectly reliable resources and any demand distribution, $\Delta\ge 0$ for every $u\in U_1$, for the loss-averse objective and for the CVaR objective. In the formalization: for every $c_{N+1}\le c$,

$$\forall K\ge 0\ \exists K_{N+1}\ge 0:\quad \mathcal V^{SD}(K)\le\mathcal V^{SF}(K_{N+1})$$

for $\mathcal V$ each expected utility with $u$ nondecreasing, and the loss-averse objective; for CVaR the same with the threshold $v$ quantified jointly with the investment.

Milestones

1. (A-4)–(A-6): at equal cost, investing $\sum_nK_n$ in the flexible resource gives a terminal wealth at least that of SD, for every demand realization.
2. The SF wealth first-order stochastically dominates the SD wealth: $F_{W^{SF}}\le F_{W^{SD}}$.
3. $E[u(w^{SD}(K))]\le E[u(w^{SF}(\sum_nK_n))]$ for every nondecreasing $u$.
4. The loss-averse objective is the expected utility of a nondecreasing piecewise-linear utility with breakpoint $w_0$.
5. The CVaR comparison $V^{SD}_{CVaR}(K)\le V^{SF}_{CVaR}(\sum_nK_n)$.

Significance

Proposition 4 shows that the intuition "flexibility is worth at least as much as dedicated capacity at the same price" survives any monotone risk attitude and any demand distribution, provided supply is reliable. Combined with Proposition 1 it isolates the interaction of risk aversion and unreliable supply as the only source of a negative flexibility premium, which is the paper's Remark 1 and the organizing message of its numerical study. The result requires no concavity, differentiability or distributional assumption, so it applies to the loss-averse and CVaR objectives used throughout the paper.

The result is proved in the paper (Appendix A); no machine-checked version is known. A formalization produces a reusable statement of the model, a pathwise pooling inequality, and the passage from a pathwise comparison of two random variables on one probability space to comparisons of expected utilities and of CVaR, which recurs in capacity-pooling and inventory-pooling arguments.

Difficulty

The pathwise inequality is elementary. The work lies in the passage from it to the objectives. The paper cites Levy (1992) for both the expected-utility and the CVaR comparison; the first holds for every nondecreasing $u$, including discontinuous ones, and the second concerns a maximum over a real threshold that is not a priori attained. A formal proof must also make sure every expectation involved is a genuine integral: the utility is arbitrary, so the expected utility is finite only because, for a fixed nonnegative investment and nonnegative demand, both wealths are confined to a bounded interval. Finally, "$\Delta\ge 0$" is a statement about optimal values, and the optimal SD investment need not exist; the argument has to be run for every SD investment, not for an optimal one.

Formalization scope

All declarations live in the namespace MixFlex.Reliable. The probability space is (Ω, μ) with IsProbabilityMeasure μ; demand is a measurable X : Ω → Fin N → ℝ with each coordinate almost surely nonnegative, and no density, independence or integrability is assumed. Expectations are Bochner integrals. Perfect reliability ($\theta=1$) is built into the wealths (A-4)–(A-5), so the committed-cost fraction $\lambda$ does not appear. Standing parameters: $p>0$, $c>0$, $\beta\ge 1$, $0<\eta\le1$, $w_0$ arbitrary. The requirements $p,c>0$ and nonnegative, measurable demand are made explicit; the page treats them as part of the model.

The premium $\Delta$ and the indifference cost are not defined as real numbers, since the indifference cost need not be unique. "$\Delta\ge0$" is encoded as "SF is weakly preferred for every $c_{N+1}\le c$", and "weakly preferred" as "every nonnegative SD investment is matched or beaten by a nonnegative SF investment", with no real suprema. For CVaR the maximum in (8) over the investment and the threshold is encoded in the same matching form. The milestones compare the objectives at the flexible cost $c$, as (A-5) is printed.

A formalization in which the expected utility of a non-integrable wealth defaults to zero, or in which $\eta=0$ makes the CVaR bracket $w_0+v$, would make the comparisons meaningless; the statements exclude both ($K\ge0$ with nonnegative demand bounds the wealths; $\eta>0$). "$\Delta\ge0$" is also not trivially true: for a flexible cost above $c$ SF can be strictly worse.

Out of scope: Propositions 1–3 and 5–8 (Proposition 1 is the companion mission on the risk-neutral premium), Remark 1's negative-premium claim and the numerical study. Welcome contributions: a general lemma that an almost-sure inequality between bounded random variables transfers to expected utilities of monotone functions, and a proof of the CVaR bracket comparison.

Selected references

• B. Tomlin, Y. Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing & Service Operations Management 7(1):37–57, 2005. https://doi.org/10.1287/msom.1040.0063
• H. Levy, Stochastic dominance and expected utility: survey and analysis, Management Science 38(4):555–593, 1992. https://doi.org/10.1287/mnsc.38.4.555
• R. T. Rockafellar, S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• J. A. Van Mieghem, Investment strategies for flexible resources, Management Science 44(8):1071–1078, 1998. https://doi.org/10.1287/mnsc.44.8.1071

Motivation

A firm that sells several products must decide, before demand is known, how much production capacity to build and of what kind. Dedicated capacity makes one product; flexible capacity makes any of them. The classic argument for flexibility is demand pooling: capacity that can follow demand to whichever product needs it wastes less than capacity locked to one product (Fine and Freund 1990; Van Mieghem 1998).

When capacity itself is unreliable, as with a supplier that may fail to deliver, a plant that may be disrupted, or a batch that may be rejected, flexibility has a second face. A single flexible resource concentrates the firm's supply in one place, so one failure removes all of it, whereas several dedicated resources rarely fail together. This resource-aggregation effect works against flexibility. Tomlin and Wang (2005) set up a newsvendor network in which both effects are present and ask when a firm should pay more for flexible capacity than for dedicated capacity. Their first answer (Proposition 1) is that a risk-neutral firm facing equal reliabilities and costs never loses by choosing flexibility, whatever the joint distribution of demand. This mission formalizes that answer.

Setting

There are $N$ products with a common unit contribution margin $p>0$. The demand vector $\tilde X=(\tilde X_1,\dots,\tilde X_N)$ is random, nonnegative and integrable; its total is $\tilde X_{N+1}=\tilde X_1+\dots+\tilde X_N$.

Two networks are compared. In the dedicated network SD, resource $n\in\{1,\dots,N\}$ makes only product $n$ and has marginal total cost $c>0$. In the flexible network SF, a single resource, labelled $N+1$, makes every product and has marginal total cost $c_{N+1}$.

Every resource $j$ is unreliable with a Bernoulli yield $\tilde Y_j\in\{0,1\}$, $\mathbb P(\tilde Y_j=1)=\theta$. The common reliability is $\theta\in[0,1]$, the yields are mutually independent, and they are independent of demand. Investing $K_j\ge 0$ in resource $j$ delivers capacity $\tilde Y_jK_j$ and costs $(\lambda+(1-\lambda)\tilde Y_j)c_jK_j$: the firm pays the committed cost $\lambda c_j$ per unit ordered and a further $(1-\lambda)c_j$ per unit delivered, with $\lambda\in[0,1]$.

The realized profits are

$$W^{SD}(K)=\sum_{n=1}^N\Big(-(\lambda+(1-\lambda)\tilde Y_n)cK_n+p\min\{\tilde X_n,\tilde Y_nK_n\}\Big),$$ $$W^{SF}(K_{N+1})=-(\lambda+(1-\lambda)\tilde Y_{N+1})c_{N+1}K_{N+1}+p\min\{\tilde X_{N+1},\tilde Y_{N+1}K_{N+1}\},$$

and a risk-neutral firm maximizes the expected profit $V^{SD}_{RN}(K)=\mathbb E[W^{SD}(K)]$ or $V^{SF}_{RN}(K_{N+1})=\mathbb E[W^{SF}(K_{N+1})]$ over nonnegative investments. Let $V^{SD,*}$ and $V^{SF,*}$ be the optimal values. SF is (weakly) preferred if $V^{SF,*}\ge V^{SD,*}$.

The indifference cost $c^I_{N+1}$ is a value of $c_{N+1}$ at which $V^{SF,*}=V^{SD,*}$, and the flexibility premium is $\Delta=(c^I_{N+1}-c)/c$. The firm prefers SF as long as $c_{N+1}\le(1+\Delta)c$.

The $\alpha$-expected shortfall of a random variable $Z$ is, for $\alpha\in(0,1)$ and the lower quantile $x_{(\alpha)}=\inf\{x:\mathbb P(Z\le x)\ge\alpha\}$,

$$ES_\alpha(Z)=-\frac1\alpha\Big(\mathbb E\big[Z\mathbf 1\{Z\le x_{(\alpha)}\}\big]+x_{(\alpha)}\big(\alpha-\mathbb P(Z\le x_{(\alpha)})\big)\Big).$$

Formalization targets

Goal: Proposition 1

For any demand random vector $\tilde X$:

1. $\Delta_{RN}\ge 0$ for all $0\le\theta\le 1$, that is, SF is preferred whenever $c_{N+1}\le c$;

$$0\le\theta\le\frac{\lambda c}{p-(1-\lambda)c}\ \Longrightarrow\ \Delta_{RN}=0;$$

3. $\Delta_{RN}=0$ if $\rho_X=\mathbf 1$, i.e. all pairwise demand correlations equal $1$.

No distributional form of demand is fixed and no constant is hard-coded beyond the paper's threshold.

Milestones

• (9): the closed form of $V^{SF}_{RN}$.
• (10)–(11), (12)–(13): the optimal investments are critical fractiles

$$F_{X_{N+1}}(K^*_{N+1})=1-\frac{(\lambda+(1-\lambda)\theta)c_{N+1}}{\theta p},\qquad F_{X_n}(K^*_n)=1-\frac{(\lambda+(1-\lambda)\theta)c}{\theta p},$$

and the optimal values are $\theta p$ times partial expectations of demand.

• (A-1) in expected-shortfall form: with $\alpha=1-(\lambda+(1-\lambda)\theta)c/(\theta p)\in(0,1)$,

$$V^{SF,*}\ge V^{SD,*}\ \text{at}\ c_{N+1}=c\iff \alpha\Big(\sum_n ES_\alpha(\tilde X_n)-ES_\alpha\Big(\sum_n\tilde X_n\Big)\Big)\ge 0 .$$

• Subadditivity of $ES_\alpha$ (Acerbi and Tasche 2002).
• The positivity threshold of part 2: investing is worthwhile iff $\theta>\lambda c/(p-(1-\lambda)c)$.
• Correlation $1$ implies $\tilde X_n=a\tilde X_1+b$ with $a>0$, and $ES_\alpha(aX+b)=aES_\alpha(X)-b$.

Significance

Proposition 1 separates the two effects of flexibility under unreliable supply. It shows that for a risk-neutral firm the demand-pooling benefit together with an upside effect of aggregation (one flexible resource succeeds more often than all dedicated ones together) always outweighs the downside aggregation risk. Even with no pooling benefit at all (perfectly correlated demand) the firm is indifferent, not averse. The later results of the paper (loss aversion, CVaR, dual sourcing) are measured against this baseline: a negative premium can appear only once the firm is risk-averse. The expected-shortfall form links newsvendor optimal values to a coherent risk measure, a connection that recurs in inventory risk analysis.

The result is proved in the paper, with a proof that cites Acerbi and Tasche (2002) for two properties of expected shortfall. No machine-checked version exists. A formalization adds three things: a proof for general demand distributions (the paper assumes a joint density and uses the continuous form of expected shortfall); a Lean development of Acerbi–Tasche expected shortfall for general integrable random variables, including subadditivity and affine equivariance; and a reusable model of newsvendor networks with Bernoulli yields and committed costs.

Difficulty

The newsvendor steps (9)–(13) are single-variable concave optimization, but they must be done without a density: the distribution function of total demand may have atoms and flat pieces, so the critical fractile need not be attained or may be attained on an interval, and optimal values must be expressed through lower quantiles. Subadditivity of expected shortfall is the heart of part 1 and is not elementary in the general (atomic) case, which is exactly why the correction term $x_{(\alpha)}(\alpha-\mathbb P(Z\le x_{(\alpha)}))$ appears. Part 3 requires identifying correlation $1$ with almost-sure positive affine dependence, which rests on the equality case of the Cauchy–Schwarz inequality in $L^2$, and then handling nonnegativity constraints on the investments that the affine change of variables may violate. The obvious shortcut of computing everything from densities is not available, because the goal is stated for every demand vector and part 3 is incompatible with a joint density when $N\ge 2$.

Formalization scope

Randomness lives on one probability space $(\Omega,\mu)$; demand is X : Ω → Fin N → ℝ and yields are Y : Ω → Fin (N + 1) → ℝ, where dedicated resource $n$ is Fin.castSucc n and the flexible resource $N+1$ is Fin.last N. Expectations are Bochner integrals and probabilities are μ.real. The standing assumptions are: $p>0$, $c>0$, $\lambda,\theta\in[0,1]$; demands measurable, almost surely nonnegative and integrable (integrability is needed for expected shortfall and makes every profit integrable); yields measurable, $\{0,1\}$-valued almost surely with $\mathbb P(\tilde Y_j=1)=\theta$, mutually independent, and independent of demand (the paper states the last in Appendix E). The paper's joint density of demand is deliberately not assumed.

The premium $\Delta$ and the indifference cost are not defined as real numbers, because Definition 1's indifference cost need not exist or be unique (for $\theta$ below the threshold both optimal values are $0$ for every $c_{N+1}$ near $c$). "$\Delta\ge 0$" is encoded as "SF is weakly preferred for every $c_{N+1}\le c$", and "$\Delta=0$" as "SF and SD are each weakly preferred to the other at $c_{N+1}=c$". Weak preference $V^{SF,*}\ge V^{SD,*}$ is stated as: every nonnegative SD investment is matched by some nonnegative SF investment; no real supremum is taken. Quantiles $F^{-1}$ in (10) and (12) appear only as parameters with the hypothesis $F(K^*)=$ fractile. Part 3 adds square integrability and positive variances, the conditions under which correlation coefficients exist; the threshold milestone adds almost surely positive demand and $N\ge 1$ for its "if" direction. When $p\le(1-\lambda)c$ the Lean value of the threshold is $\le 0$, so part 2 then covers only $\theta=0$, where it is true.

A formalization that assumed a joint density, took $\Delta$ as a free real satisfying Definition 1, or defined optimal values as real suprema over all of $\mathbb R^N$ would make parts of the goal vacuous or trivial; each is ruled out above.

Needed infrastructure: single-variable newsvendor optimality for general distributions; the Acerbi–Tasche expected shortfall with subadditivity and affine equivariance; the equality case of Cauchy–Schwarz for correlation. The expected-shortfall and correlation lemmas are reusable well beyond this mission, and contributions of them are especially welcome. Out of scope: the loss-averse and CVaR analyses (Propositions 2–3, §3.2–3.3), the perfect-reliability result (Proposition 4, a separate mission), the dual-sourcing networks (§4) and all numerical results.

Selected references

• B. Tomlin and Y. Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing & Service Operations Management 7(1):37–57, 2005. https://doi.org/10.1287/msom.1040.0063
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26(7):1487–1503, 2002. https://doi.org/10.1016/S0378-4266(02)00283-2
• C. H. Fine and R. M. Freund, Optimal investment in product-flexible manufacturing capacity, Management Science 36(4):449–466, 1990. https://doi.org/10.1287/mnsc.36.4.449
• J. A. Van Mieghem, Investment strategies for flexible resources, Management Science 44(8):1071–1078, 1998. https://doi.org/10.1287/mnsc.44.8.1071

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

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