Optimization

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

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

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

The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points $n$, when the distances satisfy the triangle inequality.

The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with $n$: the tour is less than twice the optimal (Theorem 4), and more precisely at most $2(1-1/n)$ times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant $2(1-1/n)$ is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.

Setting

A traveling salesman graph $(N,d)$ has a finite node set $N$ with $|N| = n$ and a distance $d : N\times N\to\mathbb R$ that is symmetric, nonnegative and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.

A subtour $T$ is a tour on a subset of $N$ (a one-node subtour has no edges). For $k\notin T$, $\mathrm{TOUR}(T,k)$ inserts $k$ into $T$ where it is cheapest: if $T$ has at least two nodes, choose an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and replace it by $(x,k),(k,y)$; if $T=\{i\}$, form the two-node tour on $i,k$. $\mathrm{COST}(T,k)$ is the length of $\mathrm{TOUR}(T,k)$ minus the length of $T$.

An insertion method builds subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some $a_i\notin T_i$, $1\le i<n$; INSERT is the length of $T_n$. With $d(T,p)=\min_{x\in T}d(x,p)$:

• nearest insertion chooses each $a_i$ with $d(T_i,a_i)=\min\{d(T_i,x): x\in N-T_i\}$;
• cheapest insertion chooses each $a_i$ with $\mathrm{COST}(T_i,a_i)=\min\{\mathrm{COST}(T_i,x): x\in N-T_i\}$.

The start node $a_0$ and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of $(N,d)$.

Formalization targets

Goal: Corollary to Theorem 4, eq. (4.12)

For every traveling salesman graph on $n\ge1$ nodes and every run of nearest insertion or of cheapest insertion,

$$\mathrm{INSERT}\;\le\;2\Bigl(1-\frac1n\Bigr)\cdot\mathrm{OPTIMAL}.$$

Milestones

1. Lemma 2, (3.3): $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for $k\notin T$, $j\in T$.
2. Eq. (3.7): for every insertion method, $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
3. Eqs. (4.9)–(4.10): nearest insertion satisfies $\mathrm{COST}(T_i,a_i)\le 2\,d(p,q)$ for all $p\in T_i$, $q\notin T_i$ (4.5).
4. Proof of Theorem 4: cheapest insertion satisfies (4.5) as well.
5. Lemma 3: every insertion run satisfying (4.5) has $\mathrm{INSERT}\le 2\cdot\mathrm{TREE}$ (4.6).
6. Eq. (4.11): $\mathrm{TREE}\le(1-1/n)\cdot\mathrm{OPTIMAL}$.

Theorem 4 itself, $\mathrm{INSERT}<2\cdot\mathrm{OPTIMAL}$ when $d$ is not identically zero, is included as a companion statement.

Significance

The bound says that two simple $O(n^2)$ and $O(n^2\log n)$ construction rules are never worse than a factor $2(1-1/n)$ from optimal on any metric instance, a guarantee independent of $n$, in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound $2\cdot\mathrm{TREE}$, and the paper notes that similar arguments apply to nearest addition and nearest merger.

The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant $2$ (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of $\mathrm{TREE}\le\mathrm{OPTIMAL}$ (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant $2(1-1/n)$, and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.

Difficulty

Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step $i$ to the tree edge joining $a_i$ to its nearest node of $T_i$, but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds $2\cdot\mathrm{TREE}$. Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant $2(1-1/n)$ is sharper than the bound $2\cdot\mathrm{OPTIMAL}$ obtained from $\mathrm{TREE}\le\mathrm{OPTIMAL}$, so the weaker spanning-tree bound already in the library does not suffice.

Formalization scope

Nodes are Fin n with $n\ge1$ (the paper's nodes $1,\dots,n$ shifted to $0,\dots,n-1$). The distance satisfies the paper's three axioms plus the normalization $d(i,i)=0$, which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. $\mathrm{TOUR}(T,k)$ is encoded as insertion of $k$ at a list position whose resulting length is minimal over all $|T|+1$ positions, which is the minimization of (3.1) over the edges of $T$; COST is the corresponding minimum increase. The subtour index is 1-based as printed ($T_1=\{a_0\}$, $T_n$ final). The distance $d(T,p)$ is taken in $\mathbb R\cup\{+\infty\}$, so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).

A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.

A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, GSIA, Carnegie Mellon University, 1976. https://doi.org/10.1007/s43069-021-00101-z (reprint in Operations Research Forum 3, 2022)
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10 (Theorem 10.7). https://doi.org/10.1002/9781119584445