Operations Research

Motivation

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

Setting

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

Formalization targets

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Scaling algorithms are one of the standard techniques for solving discrete optimization problems efficiently: instead of searching a huge integer domain directly, an algorithm first solves a coarsened version of the problem — checking optimality only against neighbors reached by a large step size $\alpha$ — and then refines the resulting approximate solution down to the true optimum. This strategy is only as good as the guarantee that a coarse-scale local optimum is provably close to a true, fine-scale global optimum; without such a guarantee, refinement could require an unbounded number of steps. Results providing this guarantee are called proximity theorems, and they are a standard tool across combinatorial optimization, from network flow scaling algorithms to submodular function minimization.

M-convex functions, the subject of this chapter, are exactly the class of discrete convex functions for which the classical local-optimality test of chapter 3 (checking a full neighborhood of up to $3^n-1$ sign patterns) sharpens to a much smaller, purely pairwise test: checking $f(x) \le f(x - \chi_u + \chi_v)$ for every pair of coordinates $u, v$. This mission formalizes the chapter's central definitional equivalence (Theorem 6.2), this pairwise optimality criterion (Theorem 6.26), a structural minimizer-cut lemma (Theorem 6.28), and the chapter's capstone, the M-proximity theorem (Theorem 6.37) — the result that makes M-convex scaling algorithms provably correct, with an explicit, dimension-and-scale-only distance bound between a coarse-scale local optimum and a true global minimizer.

Setting

Let $V$ be a finite ground set. A function $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom} f$ is an M-convex function if it satisfies the exchange axiom (M-EXC[Z]): for $x, y \in \operatorname{dom} f$ and $u$ in the positive support of $x - y$, there is $v$ in the negative support of $x-y$ with

$$f(x) + f(y) \ge f(x - \chi_u + \chi_v) + f(y + \chi_u - \chi_v).$$

An M$^\natural$-convex function is one whose lift $\tilde f$ to the extended ground set $\tilde V = \{0\} \cup V$ — defined by $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$, and $+\infty$ otherwise — is M-convex; equivalently (Theorem 6.2, below) $f$ satisfies the axiom (M$^\natural$-EXC[Z]), a variant of (M-EXC[Z]) that additionally allows a single-coordinate move ($u$ alone, with no compensating $v$). Every M-convex function is M$^\natural$-convex, but not conversely. For $\alpha$ a positive integer, a point satisfies the scaled local optimality condition at scale $\alpha$ if $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all relevant $u, v$ — a check against neighbors $\alpha$ steps away rather than adjacent ones.

Formalization targets

Goal: Theorem 6.37 (the M-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$.

$$\text{(1) } f \text{ M-convex, } f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v-\chi_u))\ \forall u,v \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le (n-1)(\alpha-1),$$ $$\text{(2) } f \text{ M}^\natural\text{-convex, same hypothesis over } u,v \in V \cup \{0\} \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le n(\alpha-1).$$

Both bounds are exact and specific to their hypothesis class; replacing either with an unspecified function of $n$ and $\alpha$ would discard exactly the content chapter 10's algorithms rely on.

Milestones: Theorems 6.2, 6.26, 6.28

Theorem 6.2: M$^\natural$-convexity (defined via the lift) is equivalent to the direct exchange axiom (M$^\natural$-EXC[Z]) — the chapter's central definitional theorem, needed to work with M$^\natural$-convex functions without repeatedly invoking the lift construction. Theorem 6.26 (the M-optimality criterion): global optimality of $f$ at $x$ is equivalent to a purely pairwise local check, $f(x) \le f(x-\chi_u+\chi_v)$ for all $u,v$ (plus, in the M$^\natural$ case, $f(x) \le f(x\pm\chi_v)$). Theorem 6.28 (the M-minimizer cut): from any point and any coordinate pair minimizing a one-step exchange, one can certify a coordinate-wise bound that some global minimizer must satisfy — the structural fact underlying both the domain-reduction algorithm and, via the same proof technique, the proximity theorem itself.

Significance

The result itself. Theorem 6.26 already sharpens chapter 3's local-to-global criterion (checking a full $3^n-1$-point neighborhood) to an $O(n^2)$-size pairwise check — the minimum spanning tree optimality criterion is a direct special case. The proximity theorem builds on this to control what happens when the local check is only performed at a coarse scale $\alpha$: it guarantees that scaling-based algorithms, which alternate between coarse-scale local search and scale reduction, terminate with a guaranteed-close approximation at every stage, with an explicit linear-in-$n$, linear-in-$\alpha$ error bound rather than a qualitative "eventually converges" guarantee.

Formalizing it. No matching item exists on the platform for M-convex functions, the exchange axiom, or a discrete proximity theorem of this kind. This mission gives the first formal statement of the M-optimality criterion and the M-proximity theorem, together with the exchange-axiom / lift-based-definition equivalence (Theorem 6.2) that the rest of the M-convex function theory (chunks 07, and indirectly 10–14) is built on.

Difficulty

The natural first attempt at Theorem 6.37 is to try a direct coordinatewise argument: since the scaled hypothesis holds for every pair $u, v$, one might hope to bound $|x_\alpha(v) - x^*(v)|$ coordinate by coordinate independently. This does not work, because a single application of the exchange axiom only ever improves $f$ by trading one coordinate down and one other coordinate up simultaneously — there is no way to move a single coordinate toward a minimizer in isolation without accounting for where the compensating mass goes. The actual proof instead fixes a target coordinate $v$, constructs a chain of strictly decreasing function values $y_0 = x_\alpha, y_1, \ldots, y_k$ by repeatedly applying (M-EXC[Z]) against a fixed near-optimal point $x^*$ (exactly the technique of Theorem 6.28's proof), and then bounds how far each other coordinate can move along this chain using the scaled hypothesis itself, before summing those bounds via the M-convex domain's hyperplane constraint $x(V) =$ constant to recover the bound on $v$. The chain construction, not a per-coordinate estimate, is what makes the linear-in-$n$ bound provable at all.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. M$^\natural$-convexity is represented via an explicit lift to Option V (none standing for the extended ground set's new element $0$), matching the book's own primary definition; the direct exchange-axiom form is a separate predicate related to it by Theorem 6.2, not conflated with it. `‖x_\alpha - x^*|_\infty \le c$ is stated pointwise.

A trivializing formalization of the goal would replace either exact bound, $(n-1)(\alpha-1)$ or $n(\alpha-1)$, with an unspecified asymptotic bound, or merge the two hypothesis classes into a single weaker statement; neither is done here. Propositions establishing dom f as an M-convex set, the M/M$^\natural$ relationship (Theorem 6.3), and several structural closure properties are cut from this mission's scope (not needed by the chosen items' statements — see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 07, which builds directly on this chunk's exchange-axiom vocabulary. Contributions building the arg min f M-convexity corollary (Proposition 6.29) or the scaled minimizer cut (Theorem 6.39, the direct generalization of Theorem 6.28 drafted here) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• D. S. Hochbaum, "Lower and upper bounds for the allocation problem and other nonlinear optimization problems," Mathematics of Operations Research, 19(2), 1994, pp. 390–409.

Motivation

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

Setting

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

Formalization targets

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012 (the finite-state discounted/SSP theorems this goal generalizes).
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (analytic measurability of $J_\infty$, $J$; cited by the book for this chapter's foundational measure-theoretic facts).
• K. Hinderer, Foundations of Non-stationary Dynamic Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970 (Theorem 18.4, cited for the fact that history-dependent policies do not improve on Markov ones).

Motivation

Training a statistical model by empirical risk minimization means minimizing an average of $N$ losses over a parameter vector $w\in\mathbb R^n$, where both $N$ and $n$ can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.

Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every $L$ steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the $O(1/k)$ expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).

Setting

Let $f_1,\dots,f_N:\mathbb R^n\to\mathbb R$ be twice continuously differentiable losses and

$$F(w)=\frac1N\sum_{i=1}^N f_i(w).$$

For a sample $\mathcal S\subseteq\{1,\dots,N\}$ of size $b$, the minibatch gradient is $\nabla F_{\mathcal S}(w)=\frac1b\sum_{i\in\mathcal S}\nabla f_i(w)$. For a sample $\mathcal S_H$ of size $b_H$, the subsampled Hessian is $\nabla^2F_{\mathcal S_H}(w)=\frac1{b_H}\sum_{i\in\mathcal S_H}\nabla^2 f_i(w)$.

Assumption 1 requires constants $0<\lambda,\Lambda$ with $\lambda I\prec\nabla^2F_{\mathcal S_H}(w)\prec\Lambda I$ for every $w$ and every Hessian sample. It also requires a bound $\gamma^2$ on the second moment of the stochastic gradient. $w^*$ denotes the minimizer of $F$.

Algorithm 2 turns correction pairs $(s_j,y_j)$ into a matrix $H_t$. With $\tilde m=\min\{t,M\}$, it starts from $\frac{s_t^Ty_t}{y_t^Ty_t}I$ and applies the BFGS update

$$H\leftarrow(I-\rho_js_jy_j^T)H(I-\rho_jy_js_j^T)+\rho_js_js_j^T,\qquad\rho_j=\frac1{y_j^Ts_j},$$

for $j=t-\tilde m+1,\dots,t$.

Algorithm 1 (SQN) runs for $k=1,2,\dots$. It draws a gradient sample $\mathcal S_k$ and steps

$$w^{k+1}=w^k-\alpha^kH\nabla F_{\mathcal S_k}(w^k),$$

where $H=I$ for $k\le2L$ and $H=H_t$, $t=\lfloor(k-1)/L\rfloor-1$, afterwards. Every $L$ iterations it forms the block average $\bar w_t$ of the last $L$ iterates and a new pair

$$s_t=\bar w_t-\bar w_{t-1},\qquad y_t=\nabla^2F_{\mathcal S_{H,t}}(\bar w_t)\,s_t .$$

Samples are drawn independently and uniformly among the subsets of their size. The step length is $\alpha^k=\beta/k$.

Formalization targets

Goal: Corollary 3.3, with a corrected constant

There are $0<\mu_1\le\mu_2$, depending only on the problem data, such that every matrix Algorithm 1 applies satisfies $\mu_1I\prec H\prec\mu_2I$. Moreover, for every $\beta>1/(2\mu_1\lambda)$,

$$E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k\qquad(k\ge1),$$ $$Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.$$

The constants $\mu_1,\mu_2$ are not fixed numerically. The goal asserts a rate of order $1/k$ with an explicit constant in terms of them.

Milestones

• (3.8)–(3.10): the curvature bounds $\lambda\|s\|^2\le y^Ts\le\Lambda\|s\|^2$ and $\lambda\le\|y\|^2/y^Ts\le\Lambda$ for Hessian-product pairs.
• (3.11) and (3.12): the trace bound and Powell's determinant formula for the direct L-BFGS matrices.
• Lemma 3.1: $\mu_1I\prec H_t\prec\mu_2I$ uniformly along every run.
• (3.18): expected descent for the general Newton-like iteration $w^{k+1}=w^k-\alpha^kH_k\nabla f(w^k,\xi^k)$.
• (3.19): $2\lambda[F(w)-F(w^*)]\le\|\nabla F(w)\|^2$.
• (3.22): the recursion $\phi_{k+1}\le(1-2\alpha^k\mu_1\lambda)\phi_k+\frac\Lambda2(\alpha^k\mu_2)^2\gamma^2$.
• Theorem 3.2: the $Q_c(\beta)/k$ rate for the Newton-like iteration.

Significance

The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the $\beta/k$ schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.

The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner $H_t$ depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which $H_t$ is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.

On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of $H_t$ that is uniform over all runs and all $t$. The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and $A\prec B$ is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices $k,t$ start at $1$ as in the paper. In the corollary, $E$ is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. $H_k$ and $w^k$ are $\mathcal F_k$-measurable, the sample $\xi^k$ is $\mathcal F_{k+1}$-measurable, and unbiasedness is a conditional expectation. Integrability of $F(w^k)$ is part of each conclusion, so a junk-zero integral cannot satisfy it.

Two corrections to the paper, each labelled in the item titles and notes:

• Iterate-wise $\gamma$. Assumption 1(3) says $E_\xi\|\nabla f(w,\xi)\|^2\le\gamma^2$ for all $w$. Together with unbiasedness and $\lambda$-strong convexity on $\mathbb R^n$, this forces $\lambda\|w-w^*\|\le\|\nabla F(w)\|\le\gamma$ for every $w$, which is impossible. The mission imposes the bound at the iterates, conditionally on the past, which is how the proof uses it.
• Constant $Q_c(\beta)$. The induction after (3.22) multiplies by $1-2\beta\mu_1\lambda/k$, which is negative for $k<2\beta\mu_1\lambda$. Counterexample: $n=1$, $f_{1,2}(w)=(w\mp1)^2/2$, $H_k=I$, $w^1=0$, $\beta=2$, $\gamma^2=5$. Then $F(w^2)-F(w^*)=2>Q(2)/2=5/3$, and the example survives perturbing the constants so that every strict inequality holds. The middle entry of $Q_c$ repairs it, and $Q_c=Q$ whenever $2\mu_1\lambda\beta\le3/2$.

Smaller conventions:

• The pairs must satisfy $s_t\neq0$, since Algorithm 2 is undefined otherwise.
• Hessian samples have size $b_H\ge1$; the empty sample makes (2.3) a $0/0$.
• The corollary's undefined $\mu_2$ is Lemma 3.1's constant, enlarged together with $\mu_1$ to cover the initial $H=I$ steps.
• The block average of Algorithm 1 is used, not Eq. (2.1).

Trivializing encodings are ruled out: $H_t$ is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all $w$.

Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of $C^2$ functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.

Selected references

• R. H. Byrd, S. L. Hansen, J. Nocedal, Y. Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2):1008–1031, 2016. https://doi.org/10.1137/140954362
• A. Mokhtari, A. Ribeiro, Global Convergence of Online Limited Memory BFGS, J. Mach. Learn. Res. 16:3151–3181, 2015. https://jmlr.org/papers/v16/mokhtari15a.html
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2):223–311, 2018. https://doi.org/10.1137/16M1080173
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277
• M. J. D. Powell, Some global convergence properties of a variable metric algorithm for minimization without exact line searches, in Nonlinear Programming, SIAM-AMS Proc. IX, 1976, pp. 53–72.

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