Operations Research

Motivation

The classical separating hyperplane theorem says that any two disjoint convex sets in $\mathbb R^n$ can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.

L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in $\{-1, 0, 1\}$, no matter how large or complicated the sets are.

Setting

Let $V$ be a finite ground set. A nonempty set $D \subseteq \mathbb Z^V$ is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — $p, q \in D \implies p \vee q,\ p \wedge q \in D$, where $\vee, \wedge$ are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — $p \in D \implies p \pm \mathbf 1 \in D$, where $\mathbf 1$ is the all-ones vector. A distance function $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ satisfies $\gamma(v,v) = 0$ for every $v$; it satisfies the triangle inequality if $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ for all $v_1, v_2, v_3$. The admissible-potential polyhedron of $\gamma$ is

$$D(\gamma) = \{p \in \mathbb R^V : p(v) - p(u) \le \gamma(u,v)\ (\forall u \ne v)\}.$$

The convex hull of a discrete set $D \subseteq \mathbb Z^V$ is written $\bar D \subseteq \mathbb R^V$.

Formalization targets

Goal: Theorem 5.9 (discrete separation for L-convex sets)

If $D_1, D_2 \subseteq \mathbb Z^V$ are disjoint L-convex sets, there exists $x^* \in \{-1,0,1\}^V$ such that

$$\inf\{\langle p, x^*\rangle : p \in D_1\} - \sup\{\langle p, x^*\rangle : p \in D_2\} \ge 1.$$

Dropping the $\{-1,0,1\}^V$ restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.

Milestones: Theorems 5.2, 5.5, 5.7

Theorem 5.2: an L-convex set is hole free ($D = \bar D \cap \mathbb Z^V$) — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: $D$ is L-convex if and only if $D = D(\gamma) \cap \mathbb Z^V$ for some integer-valued distance function $\gamma$ satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.

Significance

The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into $\{-1,0,1\}^V$ (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The $\{-1,0,1\}$ structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a $\{-1,0,1\}$-separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.

Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.

Difficulty

The natural first attempt at Theorem 5.9 is to try to construct $x^*$ directly from the structure of $D_1, D_2$ — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents $D_1, D_2$ via distance functions $\gamma_1, \gamma_2$ (Theorem 5.5), combines them into $\gamma_{12} = \min(\gamma_1, \gamma_2)$, and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating $\pm 1$ pattern around the cycle is exactly the $\{-1,0,1\}$ vector $x^*$ — with the cycle's negativity translating directly into the required gap of at least $1$. Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary $\{-1,0,1\}$ pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $D \subseteq \mathbb Z^V$ is a Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently return a junk value on an unbounded set. The conclusion is stated as $\sup_{D_2}\langle p,x^*\rangle + 1 \le \inf_{D_1}\langle p,x^*\rangle$, an addition-based reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while remaining equivalent whenever both sides are finite.

A trivializing formalization of the goal would drop the $\{-1,0,1\}^V$ constraint on $x^*$ (recovering the classical, L-convexity-independent separation theorem) or fix a single coordinate pattern rather than asserting existence over the full three-valued family; neither is done here. Theorem 5.5 is stated existentially rather than via the book's named bijection $\Phi, \Psi$ (a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15), and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and (4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible- potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

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

Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.

Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.

Setting

Let $V$ be a finite ground set. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$) if

$$\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y) \qquad (X, Y \subseteq V).$$

Its base polyhedron and submodular polyhedron are

$$B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V),\ x(V) = \rho(V)\}, \qquad P(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V)\},$$

where $x(X) = \sum_{v \in X} x(v)$; a supermodular function $\mu$ is one with $-\mu$ submodular. A nonempty set $B \subseteq \mathbb Z^V$ is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for $x, y \in B$ and $u$ in the positive support of $x-y$, there is $v$ in the negative support of $x-y$ with both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$, where $\chi_u$ is the characteristic vector of $u$. A polyhedron $P \subseteq \mathbb R^V$ is integral if $P = \operatorname{conv}(P \cap \mathbb Z^V)$.

Formalization targets

Goal: Theorem 4.18 (Edmonds's intersection theorem)

For submodular set functions $\rho_1, \rho_2 \in S[\mathbb R]$,

$$\max\{x(V) : x \in P(\rho_1) \cap P(\rho_2)\} = \min\{\rho_1(X) + \rho_2(V \setminus X) : X \subseteq V\},$$

with both sides attained. If $\rho_1, \rho_2$ are integer valued, $P(\rho_1) \cap P(\rho_2)$ is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.

Milestones: Theorems 4.3, 4.15, 4.17

Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: $B$ is M-convex if and only if $B = B(\rho) \cap \mathbb Z^V$ for some integer-valued submodular $\rho$ — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular $\rho$ dominates a supermodular $\mu$ pointwise, a single vector $x^*$ separates them ($\rho \ge x^* \ge \mu$ pointwise on every subset), integrally when $\rho, \mu$ are integer valued — derived, in the book, as a direct corollary of the goal theorem.

Significance

The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case $\rho_1, \rho_2$ both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.

Formalizing it. No matching item exists on the platform (searches for "submodular set function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general submodular set functions or their polyhedra). This mission gives the first formal statement of the theorem at its natural generality, together with the M-convex-set viewpoint that motivates the rest of the book, and Frank's separation theorem as an explicit worked corollary.

Difficulty

The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize $\langle p, x\rangle$ over $P(\rho_1) \cap P(\rho_2)$) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each $\rho_i$'s effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data ($\rho_1, \rho_2$) are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; subsets are Finset V, vectors are V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$); supermodular functions in WithBot ℝ; comparisons across the two use an explicit embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a common EReal witness, so that "both sides attained, at the same value" — not merely "sup equals inf" — is what the Lean statement asserts, which is essential since the integrality clause's whole content is about which point attains the maximum.

A trivializing formalization of the goal would drop the integrality clause (leaving unqualified LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the "is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is stated as the existential "iff" (some integer submodular $\rho$ realizes $B$) rather than reifying the book's own named bijection $\Phi, \Psi$ explicitly — a deliberate, documented scope reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions building the explicit $\Phi$ map, the Lovász extension (needed for Theorem 4.16, not drafted here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build on this chapter's vocabulary) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16, 1982, pp. 97–120.

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

Many first-order methods in optimization are fixed-point iterations $x^{k+1}=f(x^k)$ of a nonexpansive map $f:\mathbb R^n\to\mathbb R^n$: proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration $x^{k+1}=(1-\alpha)x^k+\alpha f(x^k)$ converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.

Timeline (as recounted in the paper's related-work section):

• 1965. Anderson introduces the method for nonlinear integral equations (J. ACM 12).
• 1978. Gay and Schnabel prove local Q-superlinear convergence of a full-memory AA-I-type method (Broyden with projected updates), assuming $f$ continuously differentiable near the solution.
• 2009. Fang and Saad connect AA with multisecant Broyden methods and distinguish the two types (Numer. Linear Algebra Appl. 16).
• 2011. Walker and Ni show the essential equivalence of full-memory AA with GMRES for affine $f$ (SIAM J. Numer. Anal. 49); Rohwedder and Schneider prove local Q-linear convergence of limited-memory AA-II for differentiable $f$.
• 2015. Toth and Kelley give local linear convergence of AA-II for contractive $f$ (SIAM J. Numer. Anal. 53).
• 2020. Zhang, O'Donoghue and Boyd introduce a stabilized AA-I method (Powell-type regularization, restart checking, safeguarding) and prove global convergence for every nonexpansive map with a fixed point, without differentiability (SIAM J. Optim. 30(4), 3170–3197; longer version arXiv:1808.03971).

Setting

Let $f:\mathbb R^n\to\mathbb R^n$ satisfy $\|f(x)-f(y)\|_2\le\|x-y\|_2$ for all $x,y$ (the Euclidean norm), and assume the solution set $X=\{x^\star\mid x^\star=f(x^\star)\}$ is nonempty. The residual is $g(x)=x-f(x)$, $g_k=g(x^k)$, and the averaged operator is $f_\alpha(x)=(1-\alpha)x+\alpha f(x)$.

Powell's weight. For $\bar\theta\in(0,1)$, $\phi_{\bar\theta}(\eta)=1$ if $|\eta|\ge\bar\theta$ and $\phi_{\bar\theta}(\eta)=(1-\operatorname{sign}(\eta)\bar\theta)/(1-\eta)$ otherwise, with $\operatorname{sign}(0)=1$.

Window matrices. For vectors $s_0,\dots,s_{m_k-1}$ and $y_0,\dots,y_{m_k-1}$, let $\hat s_i$ be their unnormalized Gram–Schmidt orthogonalization (3.2), $B^0=I$, and

$$B^{i+1}=B^i+\frac{(\tilde y_i-B^is_i)\hat s_i^T}{\hat s_i^Ts_i},\qquad \tilde y_i=\theta^iy_i+(1-\theta^i)B^is_i,\qquad \theta^i=\phi_{\bar\theta}\Bigl(\frac{\hat s_i^T(B^i)^{-1}y_i}{\|\hat s_i\|_2^2}\Bigr).$$

The matrix norm $\|\cdot\|_2$ is the induced $\ell_2$ operator norm.

Algorithm 3.1 (AA-I-S-m). With parameters $\bar\theta,\tau,\alpha\in(0,1)$, $D,\epsilon>0$ and max-memory $m\ge1$: start from $H_0=I$, $m_0=0$, $n_{AA}=0$, $\bar U=\|g_0\|_2$ and $x^1=\tilde x^1=f_\alpha(x^0)$. At iteration $k\ge1$, set $s_{k-1}=\tilde x^k-x^{k-1}$ and $y_{k-1}=g(\tilde x^k)-g(x^{k-1})$, orthogonalize $s_{k-1}$ against the current window, and restart the window (memory back to $1$, $H_{k-1}$ replaced by $I$) if the memory would exceed $m$ or $\|\hat s_{k-1}\|_2<\tau\|s_{k-1}\|_2$. Then apply one Powell-regularized rank-one update to obtain $H_k$ and the trial point $\tilde x^{k+1}=x^k-H_kg_k$. The trial point is accepted if $\|g_k\|_2\le D\bar U(n_{AA}+1)^{-(1+\epsilon)}$ (and $n_{AA}$ increases); otherwise $x^{k+1}=f_\alpha(x^k)$.

Formalization targets

Goal: Theorem 4.1

$$\text{for every run of Algorithm 3.1:}\qquad \lim_{k\to\infty}x^k=x^\star\quad\text{for some } x^\star=f(x^\star).$$

The only hypotheses are nonexpansiveness of $f$, $X\ne\emptyset$ and the parameter ranges. The limit is not specified: it depends on $x^0$ and the parameters.

Milestones

1. Lemma 3.2. Well-defined updates give $|\det B^{m_k}|\ge\bar\theta^{m_k}>0$.
2. Lemma 3.3. If $\|y_i\|_2\le2\|s_i\|_2$, $\|\hat s_i\|_2\ge\tau\|s_i\|_2$ and $m_k\le m$, then $\|B^{m_k}\|_2\le3((1+\bar\theta+\tau)/\tau)^m-2$.
3. Corollary 3.4. $\|H_k\|_2\le(3((1+\bar\theta+\tau)/\tau)^m-2)^{n-1}/\bar\theta^m$ (3.8).
4. Corollary 3.5. Along the algorithm, unless a solution is hit, (3.8) holds and $\mathrm{cond}(H_k)\le(3((1+\bar\theta+\tau)/\tau)^m-2)^n/\bar\theta^m$.
5. Eq. (4.3). $\|x^k-y\|_2\le\|x^0-y\|_2+CD\bar U\sum_{i\ge0}(i+1)^{-(1+\epsilon)}$ for every $y\in X$.
6. Eq. (4.6). $\lim_k\|g_k\|_2=0$.
7. Eq. (4.7). $\|x^{k+1}-y\|_2^2\le\|x^k-y\|_2^2+\epsilon_k$ with $\epsilon_k\ge0$ summable.
8. §4.1, Step 2. $\|x^k-y\|_2$ converges for every $y\in X$.

Significance

The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.

The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).

Difficulty

The accelerated step $\tilde x^{k+1}=x^k-H_kg_k$ need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding $\|H_kg_k\|_2$, requires a bound on $\|H_k\|_2$ that holds uniformly along the run; without the Powell regularization $B_k$ can be singular, and without the restart rule $\|B_k\|_2$ can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; $u\hat s^T$ is rankOne ℝ u ŝ; $\det$ is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by $f$, the parameters and $x^0$, and a sorry-free check that runs exist (for $f=\mathrm{id}$) was built locally. The reset of $H_{k-1}$ in line 8 is local to its iteration. $\mathrm{sign}(0)=1$ is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.

Line 9. The paper prints $\tilde y_{k-1}=\theta_{k-1}y_{k-1}-(1-\theta_{k-1})g_{k-1}$, derived from (3.3) through $B_{k-1}s_{k-1}=-g_{k-1}$, which fails when the window starts afresh ($m_k=1$). The mission uses (3.3) there: $\tilde y_{k-1}=\theta_{k-1}y_{k-1}+(1-\theta_{k-1})s_{k-1}$ when $m_k=1$, and the printed formula when $m_k\ge2$.

Milestones of §4.1 and Corollary 3.5 carry the hypothesis $f(x^k)\ne x^k$ for all $k$, as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on $\|H_k\|_2$, contractivity of $f$, or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.

Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality $\|f_\alpha(x)-y\|_2^2\le\|x-y\|_2^2-\alpha(1-\alpha)\|g(x)\|_2^2$, quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's $H_k^{-1}$) and of the convergence steps are all welcome.

Selected references

• J. Zhang, B. O'Donoghue, S. Boyd, Globally Convergent Type-I Anderson Acceleration for Nonsmooth Fixed-Point Iterations, SIAM J. Optim. 30(4), 3170–3197, 2020. https://doi.org/10.1137/18M1232772
• J. Zhang, B. O'Donoghue, S. Boyd, longer version, 2018. https://arxiv.org/abs/1808.03971
• D. M. Gay, R. B. Schnabel, Solving systems of nonlinear equations by Broyden's method with projected updates, in Nonlinear Programming 3, Academic Press, 245–281, 1978 (reference [20] of the paper). https://doi.org/10.1137/18M1232772
• D. G. Anderson, Iterative procedures for nonlinear integral equations, J. ACM 12(4), 547–560, 1965. https://doi.org/10.1145/321296.321305
• H. Fang, Y. Saad, Two classes of multisecant methods for nonlinear acceleration, Numer. Linear Algebra Appl. 16(3), 197–221, 2009. https://doi.org/10.1002/nla.617
• H. F. Walker, P. Ni, Anderson acceleration for fixed-point iterations, SIAM J. Numer. Anal. 49(4), 1715–1735, 2011. https://doi.org/10.1137/10078356X
• A. Toth, C. T. Kelley, Convergence analysis for Anderson acceleration, SIAM J. Numer. Anal. 53(2), 805–819, 2015. https://doi.org/10.1137/130919398
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7

Motivation

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

Setting

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

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

Formalization targets

Goal — Theorem 4.9.4

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

• R. E. Kalman, A New Approach to Linear Filtering and Prediction Problems, Journal of Basic Engineering 82(1), 1960, https://doi.org/10.1115/1.3662552
• M. H. A. Davis, Option Pricing in Incomplete Markets, in M. A. H. Dempster, S. R. Pliska (eds.), Mathematics of Derivative Securities, Cambridge University Press, 1997
• N. Bäuerle, U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011, https://doi.org/10.1007/978-3-642-18324-9, Chapter 4, §§4.8-4.9