Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In a combinatorial auction a seller offers indivisible items to bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.
Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an ratio; Feige observed that the same algorithm achieves and that its ratio is at least (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio () for subadditive bidders by a different rounding.
Items are and bidders . Bidder has a valuation assigning a real value to each bundle . Every valuation is normalized, , and monotone, . A valuation is complement free if for all . An allocation is a tuple of pairwise disjoint bundles; its welfare is , and denotes the largest welfare.
The LP relaxation has a variable for each bidder and bundle, with for each item and for each bidder ; its objective is , with optimum . Randomized rounding lets each bidder independently draw bundle with probability and with the remaining probability. The result, a preallocation, has expected welfare but may give an item to several bidders.
The algorithm takes and:
For all sufficiently large , for normalized, monotone, complement-free valuations and an optimal LP solution with value :
Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor into a feasible allocation losing only a factor for subadditive objectives. The same argument applies to the -duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every load estimate.
The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant in place of , a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.
The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold grows with while the mean stays at most , and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event- bound needs the preallocation's welfare as a sum of independent variables in , which requires rescaling by and monotonicity.
Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.
Explicit constants and conventions that replace the paper's notation:
Printed slips resolved in the statements:
Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible , neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.
Submodularity — the diminishing-returns property on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.
Let be a finite ground set. A function with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): for all ( componentwise max/min), and (TRF[Z]): there is with for all , where is the all-ones vector. An L-convex function is one whose lift to the extended ground set is L-convex; equivalently (Theorem 7.1), satisfies the translation-submodularity axiom (SBF[Z]): for all and all nonnegative integers . Discrete midpoint convexity asks componentwise. For a positive integer, a point satisfies scaled local optimality if for every .
Assume is a positive integer and . (1) If is L-convex with for all , and satisfies for all , then and there is with the componentwise bound
(2) If is L-convex and satisfies the two-sided version, then there is with . The bound is a genuine vector (lattice-order) inequality, not an -norm bound — the form later chapters' applications need.
Theorem 7.1: L-convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L-APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors , mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition .
The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via . The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.
Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.
A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.
The ground set is a Fintype with DecidableEq; is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and
(SBF[Z]) are stated for all of , not restricted to , so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's
structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same
concern for dom f). L-convexity is represented via an explicit lift to Option V,
matching the book's own primary definition, with the direct axiom (SBF[Z]) kept as a
separate object related to it by Theorem 7.1.
A trivializing formalization of the goal would convert its componentwise vector bound into an
-norm bound (losing the direction-of-approach information the vector form carries)
or drop Part (1)'s periodicity hypothesis ; neither is done here.
Propositions establishing dom g as an L-convex set, the L/L relationship (Theorem
7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure
properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets
for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom
vocabulary, mirroring chunks 06→07.
An M-convex function is defined on the integer lattice, but chapter 6's earlier results
(companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions,
23-ch06c-mconvexfunctions) show it always extends to a genuine convex function on real space.
Once that extension exists, every tool of classical convex analysis — directional derivatives,
subdifferentials, positive homogeneity — becomes available, and the natural question is whether
these classical objects remain combinatorially special when applied to an M-convex function's
extension. This mission answers that question at its sharpest: the directional derivative of an
M-convex function at any point is again a positively homogeneous M-convex function, its
subdifferential is exactly the admissible-potential set of a distance function satisfying the
triangle inequality, and this correspondence between positively homogeneous M-convex functions
and triangle-inequality distance functions is itself a clean one-to-one correspondence. This
closes the loop between chapters 4-5 (M-convex and L-convex sets, distance functions) and the
continuous convex-analytic machinery chapter 8 needs for its duality theory.
Companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, and
23-ch06c-mconvexfunctions cover this chapter's optimality theory, algebraic toolkit, and
convex-extensibility characterization. This mission builds the vocabulary those results also
need (redeclared here, since sibling drafts cannot yet import one another) and proves the
chapter's real-variable capstones: the transfer of M-convexity's basic operations, optimality
criterion, and supermodularity to the polyhedral (real-variable) setting, the identification of
positively homogeneous M-convex functions with distance functions satisfying the triangle
inequality, and — this mission's goal — the full directional-derivative/subdifferential
correspondence.
Fix a finite ground set . A polyhedral convex function is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for and , some and make the exchange inequality hold on ; M♮-convex if its lift to one extra coordinate is M-convex. The directional derivative of at in direction is . A function is positively homogeneous if for all ; write for the positively homogeneous polyhedral M-convex functions. A distance function satisfying the triangle inequality and its set of admissible potentials were introduced in chapter 5; the subdifferential generalizes this to any function at a point in its domain.
For and , setting :
with the analogous statement for at an integer point , using (Theorem 6.61). This is the weakest stable form: it identifies the subdifferential exactly, as a set, rather than bounding its size or complexity, and holds at every point of the domain uniformly.
Ten further results build the real-variable toolkit and the positive-homogeneity correspondence this goal completes: the transfer of M♮-convexity, the basic operations, the optimality criterion, supermodularity, and weighted-minimizer polyhedrality to the real-variable setting (Theorems 6.48-6.52, Proposition 6.53), the identification of the classes and and the compatibility of convex extension with positive homogeneity (Proposition 6.56), the two directions of the correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions (Propositions 6.57-6.58, Theorem 6.59), and the fact that a directional derivative of an M-convex function is itself positively homogeneous and M-convex (Proposition 6.60).
Theorem 6.61 is the technical bridge that lets discrete convex analysis borrow the entire apparatus of classical convex duality: because the subdifferential of an M-convex function is always the admissible-potential set of a chapter-5 distance function, every fact already proved about (its polyhedral structure, its own L-convexity, its relationship to shortest paths) transfers immediately to subdifferentials of M-convex functions. This is exactly the mechanism the book calls out as essential for Chapter 8's separation theorem for M♮-convex functions. The correspondence (Theorem 6.59) is independently significant: it says the positively homogeneous special case of M-convex function theory — which is what directional derivatives of any M-convex function reduce to, by Proposition 6.60 — is exactly as rich as ordinary shortest-path distance function theory, no more and no less, so nothing new needs to be built to understand local behavior at a point.
None of these results are open — they are Murota's account of how the discrete exchange axiom
interacts with directional differentiation and subgradients, a bridge chapter between the purely
combinatorial theory of chapters 4-6 and the duality theory of chapter 8. What this mission
contributes is a faithful, machine-checked formal statement of each, extending the shared Lean
vocabulary (MExchangeAxiomR, DirDeriv, GammaHat) the Discrete Convex Analysis series
builds on; no comparable formalization exists on the platform (see Formalization scope).
The naive approach to Theorem 6.61 would try to compute directly from the definition of subgradient and separately verify it happens to equal some ; the book's actual proof instead derives the equality of sets from the M-optimality criterion (Theorem 6.52) applied pointwise: is shown, via a chain of logical equivalences, to be exactly the condition defining , so no separate verification of polyhedrality or nonemptiness is needed beyond what Theorem 6.52 and Proposition 6.60 already supply. The genuine difficulty is upstream, in Proposition 6.60 itself: showing a directional derivative is M-convex requires exploiting the local validity of the identity for small (Eq. (6.85)) and then extending the exchange property from that neighborhood to all of using positive homogeneity — a two-step argument with no single-step shortcut, since the exchange axiom's defining inequality is not obviously homogeneous-invariant on its own.
Ground-set elements are a Fintype V with DecidableEq; real-domain functions are
(V→ℝ)→WithTop ℝ. The directional derivative is built directly as an infimum of difference
quotients over , matching the book's own local characterization (Eq. (6.85)) without a
separate limit construction. Positive homogeneity and the classes 0M[R→R]/0M[Z→R] are stated
exactly as the book defines them (the latter via positive homogeneity of the convex extension,
not of f itself, since f is undefined off Zⱽ). Theorems 6.49-6.50 restate 4 of their 8
operations (matching the identical scope decision for chunk 22-ch06b-mconvexfunctions's
Theorem 6.13); Theorem 6.61 omits the dual-integral refinement clauses for the M[R→R|Z]/
M[Z→Z] sub-classes. Both reductions are documented, not trivializing omissions — see
Difficulty above and HARD.md/MODERATION_NOTES.md. No numeric constants are hard-coded
anywhere in this mission. This mission's definitions are redeclared from chunks
06-mconvex-functions-i, 21-ch05b-lconvexsets (for the distance-function/admissible-potential
vocabulary), 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions rather than imported,
since sibling drafts in this series cannot yet reference one another. Contributions completing
any of the twelve sorrys are welcome; the goal and Proposition 6.60 carry the most independent
proof content.
The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.
Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.
Timeline of the thread this mission belongs to:
Let be -dimensional Euclidean space and let be a nonempty, closed, bounded, convex set. Its dimension is the dimension of its affine span , the smallest flat containing .
For let be the point of nearest to ; it exists and is unique. The image of with respect to is
the reflexion of through . The reflexion process starts at and sets as long as (3.2). Either the process terminates with some , or it produces an infinite sequence of points outside .
The family of supporting half-spaces of consists of the closed half-spaces whose bounding hyperplane touches . The paper observes that the half-space through normal to is the member of farthest from , so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family .
A sequence of points outside is Fejér-monotone with respect to if and for all . Two points are symmetric with respect to a flat if their midpoint lies in and is orthogonal to .
For every nonempty closed bounded convex with affine span , every and every run of the reflexion process:
No number of steps is fixed: termination is finite but not uniformly bounded.
The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of , so a solution can be read off.
Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.
The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit lies on the boundary of ; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through , which keeps the iterates on a sphere around . For a convex body there are infinitely many supporting hyperplanes near , and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of at boundary points near are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.
Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of to alone can be expected.
EuclideanSpace ℝ (Fin n). is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension ", "the point of nearest to ").IsImage A p p₁ holds when for a nearest point of ; the nearest point is not chosen by a function. For closed convex nonempty this relation is a function on . A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering are unconstrained. Every statement quantifies over every run from every ; a formalization that only asserts the existence of some terminating run is ruled out.affineSpan ℝ A; is affineSpan ℝ A = ⊤, is affineSpan ℝ A ≠ ⊤. No separate natural number is introduced.IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires and strict alternation for (strict inequality, as printed).frontier A; distances to sets are Metric.infDist.exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.An American option may be exercised at any moment up to maturity, so pricing one is not an integration problem but a stopping problem: the holder must decide, at each date and in each state of the market, whether the payoff available now beats the option value of waiting. A perpetual American put pushes this to its limit — there is no maturity at all, so the horizon is unbounded and the problem has no terminal condition to induct backwards from. What replaces the terminal condition is a fixed point characterization, and the classical answer, going back to McKean (1965) and Merton (1973) in continuous time and to Cox, Ross and Rubinstein (1979) in the binomial model, is that the price is the smallest superharmonic majorant of the payoff.
Bäuerle and Rieder's Chapter 11 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own general unbounded-horizon stopping theory rather than from stochastic analysis, and in the same chapter applies the bounded-horizon version to a problem from banking rather than trading: when should a bank cancel a credit line? The two halves share one mathematical shape — a stopping problem whose optimal policy turns out to be of threshold type — and this mission formalizes both, with the perpetual put as the goal.
The binomial model (§11.1). A stock moves from price to with risk-neutral probability and to with , where , and the discount factor is . The defining relation of the risk-neutral measure,
is carried as a hypothesis of the model: it is what makes the discounted stock price a martingale, and the proofs use it directly.
The American put with strike pays when exercised. With periods to maturity its price satisfies the recursion and
the maximum being "exercise now" against "hold". Proposition 11.1.2 describes the price at time of an option maturing at : it is continuous in , decreasing in , and — the part that carries the argument — is increasing, even though itself decreases in . That single reformulation, obtained by adding to both sides of the recursion and using the risk-neutral relation, is what yields the threshold structure: there are exercise boundaries with optimal. Exercise when the stock falls far enough, and the boundary rises as maturity approaches.
The perpetual put (Theorem 11.1.3, the goal). With no expiration date the price at time zero is a supremum over all stopping times, included:
with the stopping reward set to zero on . The theorem says four things: is the limit of the finite-maturity prices ; solves and satisfies ; is the smallest superharmonic function majorizing ; and, if the value of the exercise-region policy dominates , then equals that value and , the hitting time of , is optimal.
The conditional in part d) is the book's own and is not decoration: without it the exercise region need not deliver an optimal stopping time, and the unconditional version is a different, false statement. The boundedness in b) is likewise a genuine claim rather than a side remark — the fixed point equation alone admits other solutions, and it is boundedness together with minimality that pins down among them.
Credit granting (§11.2). A bank holds a credit contract of maximal duration . Each period it observes a rating class evolving as a Markov process , and chooses to extend — earning — or to cancel, ending the contract. The value iteration is . Under two structural assumptions — increasing, and stochastically monotone, so that a better-rated borrower stays better-rated — Theorem 11.2.1 gives the same shape of answer as the option: cancel exactly when the rating falls below a threshold , and those thresholds rise as the remaining duration shortens, since a marginal borrower is no longer worth keeping when there is little time left to recover.
Theorem 11.2.2 repeats this when the borrower is not rated at all. The bank has only a prior on the repayment probability and one signal per period; the state records positive signals out of , and the expected repayment probability is the posterior mean . Monotonicity here is for the order of p. 342 — more positive signals and fewer negative ones — and not the coordinatewise order, under which the claim would be false: an extra signal that is negative makes the state worse.
Formalize Theorem 11.1.3 in full, all four parts: the limit identification, the fixed point equation with its bounds, the minimality among superharmonic majorants, and the conditional optimality of the exercise-region stopping time. The three milestones are Proposition 11.1.2, the finite-horizon put whose threshold structure the perpetual case specializes, and the two credit granting theorems, which run the same bounded-horizon argument on a different model.
The stopping-time apparatus is built rather than assumed: the stock path, the law pinned by its finite-dimensional distributions, stopping times valued in , and the reward vanishing at . Part a) of the goal is the identification of the supremum with , so carrying as an abstract function would make the theorem vacuous.
MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least literals, it satisfies at least a fraction of the optimum.
B2 is the ancestor of a line of work on MAX-SAT approximation:
A literal is a variable or its negation . A clause is a finite set of literals. A truth assignment is a set of literals containing no pair ; it satisfies a clause when . An input is a finite set of clauses, and is the largest over subsets satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least distinct literals.
Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight per clause, starting from , , . While some literal of LIT occurs in a clause of LEFT, it picks any such literal . Let YT be the clauses of LEFT containing and YF those containing . If , it makes true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with . Finally it removes from LIT. When no literal of LIT remains in LEFT it returns SUB.
The choice of is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio and its maximum over inputs of size at most .
For every , every in MS(k) and every SUB choosable by B2 on ,
and for every there are in MS(k) and a choosable SUB with and
The paper states equality "for all sufficiently large " for every . At this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for . A separate item states that at the ratio is never attained.
The bound is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds against rather than against , a feature the paper points out. For the constant was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.
Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at . The paper's proof is complete; to our knowledge no machine-checked version exists.
The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is times to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both and . Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.
Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. is a maximum over the finite, nonempty family of satisfiable subsets.The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the tightness family, and of the correction.
An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.
The dividend model is a stationary Markov Decision Model on the integers: the state is the current risk reserve, the action (for ; only is available once ruined) is the dividend paid, the reward is , and the reserve evolves by i.i.d. increments (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of and its largest-maximizing policy (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that 's shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability , making the effective one-period discount rather than .
The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity ; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold is finite (not merely well-defined) and that is a simple barrier above it; Proposition 9.2.8 proves the increment property below that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.
Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.
The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a
band-policy is specified by an alternating chain of thresholds with a positive-width gap condition on every wave, and the policy's four
piecewise branches case-split on which wave (if any) the current state falls into. This mission
renders it existentially over the witnessing rather than as one closed-form function, a
faithful but more verbose transcription that avoids conflating the different branch conditions.
A second difficulty is Proposition 9.2.6's own finiteness claim: is a supremum over a
subset of that could, in principle, be unbounded, and Mathlib's convention for
sSup over the naturals returns a finite junk value () even for an unbounded set — using it
directly would silently trivialize "" into a claim that is true regardless of the
proposition's actual mathematical content. This mission instead states the proposition by
exhibiting the finite value of directly, so that " is finite" survives as genuine
content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's
random-horizon consumption-investment model shares no state space, action space, or definitions
with the dividend model of the goal, despite both appearing in this chunk's assigned page range;
it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting
theory, but is excluded from the milestone list proper since it plays no role in the goal's own
proof.
The dividend model's transition law is built from Mathlib's PMF (probability mass function)
type on , which supplies the "probabilities sum to one" fact automatically rather than
as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout
this mission use this whole book series' Filter.limsup-of-truncations convention for
infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership
boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment
model of §9.1 is formalized with the number of risky assets as an explicit type parameter and
its admissible-portfolio and domain restrictions as separate, citable fields rather than folded
silently into the reward or transition definitions.
A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).
This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.
Two players choose strategies from finite sets with elements and with elements; player receives payoff and maximizes it. A game is a pair of real matrices, that is, a point of ; a set of games has measure zero if it is Lebesgue-null in .
A joint distribution on is a correlated equilibrium if for every map , , and symmetrically for player 2. is the set of correlated equilibria.
Play is repeated in rounds . Before each round, player 1 issues a forecast , a probability vector over , produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence and the opponent's plays , let be the number of the first rounds with forecast , and the fraction of those rounds in which the opponent played (zero if ). The forecasts are calibrated if for every
Each player then plays of its forecast, where the best-reply function picks a best response to every forecast and does not depend on the round. is the fraction of the first rounds in which was played.
, the set of limit points of calibrated forecasts, consists of the for which some best-reply functions and some calibrated forecasting rules make for all .
Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The example shows that the genericity hypothesis cannot be dropped.
The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.
The natural construction takes a correlated equilibrium , a play sequence realizing , and forecasts equal to the conditional distributions of . The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies can have the same conditional forecast , while a stationary maps to only one strategy. Separating them needs forecasts near at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.
Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on ), and "almost every" is ∀ᵐ.The theorems are stated from the mission's own definitions of the game, calibration and ; no statement is vacuous: at or both sides of the goal are empty, and the example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.
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).
A Piecewise Deterministic Markov Decision Model (Definition 8.1.1) consists of a Borel state space , a Borel control space , a deterministic drift governing the flow between jumps, a Poisson jump clock of rate , a kernel giving the distribution of the post-jump state, a reward rate , and a discount rate . A control is a whole measurable function 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 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 — measurable functions into probability measures on rather than itself — which is compact in a suitable topology where the space of literal control functions is not.
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).
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.
The central formalization challenge is representing the continuous-time expected reward (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 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.
The book's own topology on the control-function space (the coarsest making certain
integrals measurable) and the Young topology on the relaxed-control space (which the book
cites as making 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
(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 -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.
09b's Sections 9.3-9.4).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 — 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 sign patterns) sharpens to a much smaller, purely pairwise test: checking for every pair of coordinates . 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.
Let be a finite ground set. A function with nonempty effective domain is an M-convex function if it satisfies the exchange axiom (M-EXC[Z]): for and in the positive support of , there is in the negative support of with
An M-convex function is one whose lift to the extended ground set — defined by when , and otherwise — is M-convex; equivalently (Theorem 6.2, below) satisfies the axiom (M-EXC[Z]), a variant of (M-EXC[Z]) that additionally allows a single-coordinate move ( alone, with no compensating ). Every M-convex function is M-convex, but not conversely. For a positive integer, a point satisfies the scaled local optimality condition at scale if for all relevant — a check against neighbors steps away rather than adjacent ones.
Assume is a positive integer and .
Both bounds are exact and specific to their hypothesis class; replacing either with an unspecified function of and would discard exactly the content chapter 10's algorithms rely on.
Theorem 6.2: M-convexity (defined via the lift) is equivalent to the direct exchange axiom (M-EXC[Z]) — the chapter's central definitional theorem, needed to work with M-convex functions without repeatedly invoking the lift construction. Theorem 6.26 (the M-optimality criterion): global optimality of at is equivalent to a purely pairwise local check, for all (plus, in the M case, ). 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.
The result itself. Theorem 6.26 already sharpens chapter 3's local-to-global criterion (checking a full -point neighborhood) to an -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 : 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-, linear-in- 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.
The natural first attempt at Theorem 6.37 is to try a direct coordinatewise argument: since the scaled hypothesis holds for every pair , one might hope to bound coordinate by coordinate independently. This does not work, because a single application of the exchange axiom only ever improves 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 , constructs a chain of strictly decreasing function values by repeatedly applying (M-EXC[Z]) against a fixed near-optimal point (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 constant to recover the bound on . The chain construction, not a per-coordinate estimate, is what makes the linear-in- bound provable at all.
The ground set is a Fintype with DecidableEq; is (V → ℤ) → WithTop ℝ. M-convexity is represented via an explicit
lift to Option V (none standing for the extended ground set's new element ), 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, or
, 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 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.
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.
An infinite-horizon Markov Decision Model reuses the same data 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, , 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 — a function controlling both the size of the reward and how fast the transition kernel can grow itself — with , the manageable special case that covers both the classical bounded-reward discounted case and the case of a non-positive reward.
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 of finite-weighted-norm functions a Banach space) with , and one abstract structural hypothesis — a closed class containing , mapped into itself by the Bellman operator , 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).
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 : 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 (). 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.
The central formalization challenge is representing , 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 equals the
limit of the finite-horizon truncations . 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.
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 (, , , the weighted norm ) are kept separate from the general
theory's EReal-valued objects (, , ), matching the book's own distinction between
a value function that is a priori only known to avoid 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.
Training a statistical model by empirical risk minimization means minimizing an average of losses over a parameter vector , where both and 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 steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the 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).
Let be twice continuously differentiable losses and
For a sample of size , the minibatch gradient is . For a sample of size , the subsampled Hessian is .
Assumption 1 requires constants with for every and every Hessian sample. It also requires a bound on the second moment of the stochastic gradient. denotes the minimizer of .
Algorithm 2 turns correction pairs into a matrix . With , it starts from and applies the BFGS update
for .
Algorithm 1 (SQN) runs for . It draws a gradient sample and steps
where for and , , afterwards. Every iterations it forms the block average of the last iterates and a new pair
Samples are drawn independently and uniformly among the subsets of their size. The step length is .
There are , depending only on the problem data, such that every matrix Algorithm 1 applies satisfies . Moreover, for every ,
The constants are not fixed numerically. The goal asserts a rate of order with an explicit constant in terms of them.
The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the 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.
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 depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which 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 that is uniform over all runs and all . 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.
Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices start at as in the paper. In the corollary, 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. and are -measurable, the sample is -measurable, and unbiasedness is a conditional expectation. Integrability of 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:
Smaller conventions:
Trivializing encodings are ruled out: 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 .
Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of 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.
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?
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.
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).
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).
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.
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.
The classical separating hyperplane theorem says that any two disjoint convex sets in 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 , no matter how large or complicated the sets are.
Let be a finite ground set. A nonempty set is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — , where are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — , where is the all-ones vector. A distance function satisfies for every ; it satisfies the triangle inequality if for all . The admissible-potential polyhedron of is
The convex hull of a discrete set is written .
If are disjoint L-convex sets, there exists such that
Dropping the 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.
Theorem 5.2: an L-convex set is hole free () — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: is L-convex if and only if for some integer-valued distance function 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.
The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into (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 structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a -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.
The natural first attempt at Theorem 5.9 is to try to construct directly from the structure of — 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 via distance functions (Theorem 5.5), combines them into , 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 pattern around the cycle is exactly the vector — with the cycle's negativity translating directly into the required gap of at least . 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 pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.
The ground set is a Fintype with DecidableEq; 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
, 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 constraint on
(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
(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.
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.
A Bayesian Model is a Markov Decision Model whose unobservable component is a single, never-changing, unknown parameter , drawn once from a prior distribution on a parameter space . Concretely: an observable state space , an action space , a disturbance space with reference measure , a feasible set , a deterministic transition , a disturbance density , a reward , a terminal reward , and a discount .
Because is never observed directly, the decision maker's state of knowledge at stage is the posterior , the conditional law of given the full observable history . Bayes' rule updates this posterior one disturbance at a time; unrolling the update gives an explicit closed form as a product of likelihoods against the prior (Lemma 5.4.1), and the process , for any fixed event , is a martingale (Lemma 5.4.2) — it is, after all, a sequence of conditional expectations of the same random variable against a refining amount of information.
Often the whole posterior is not needed to act optimally: a sufficient statistic compresses into a value in some space from which can still be recovered, and it is sequential if updates from only . Given a sequential sufficient statistic, the information-based Markov Decision Model replaces the never-observed by the always-computable as the second state coordinate, giving an ordinary Markov Decision Model on whose reward, terminal reward, and transition law are the original ones averaged against the current posterior .
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.
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.
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 , and 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 alone. The crux is showing that the sequential-sufficient-statistic update 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 is what turns "a good disturbance is more likely under a good " into "an increasing information state produces an increasing posterior update," without which the hypotheses on , , , alone would not propagate to the enlarged state space at all.
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 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. "" and " independent of " (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 , 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.
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.
Let be a finite ground set. A set function with and is submodular (the class ) if
Its base polyhedron and submodular polyhedron are
where ; a supermodular function is one with submodular. A nonempty set is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for and in the positive support of , there is in the negative support of with both and , where is the characteristic vector of . A polyhedron is integral if .
For submodular set functions ,
with both sides attained. If are integer valued, 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.
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: is M-convex if and only if for some integer-valued submodular — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular dominates a supermodular pointwise, a single vector separates them ( pointwise on every subset), integrally when are integer valued — derived, in the book, as a direct corollary of the goal theorem.
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 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.
The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize over ) 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 '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 () 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.
The ground set is a Fintype with DecidableEq; subsets are Finset V, vectors are
V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly ); 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 realizes ) rather than
reifying the book's own named bijection explicitly — a deliberate, documented scope
reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions
building the explicit 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.
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.
A Partially Observable Markov Decision Model (Definition 5.1.1) has data : state with observable and unobservable; feasible actions depending only on ; a stochastic kernel giving the joint law of the next state; initial law of ; rewards ; discount . A policy (Definition 5.1.3) is a sequence of decision rules , each depending only on the observable history — never on any . The objective
(Equation (5.2)) carries an extra expectation over the unknown that Chapter 2's objective never had.
Assuming has a density against reference measures, the Bayes operator and the filter recursion , (Equations (5.3)-(5.4)) compute the posterior law of given everything observed, purely from the observable history. Theorem 5.2.1 confirms is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats as an ordinary, fully-observed state, with its own kernel (built from and the marginal ), reward , and terminal reward .
under the Structure Assumption of Theorem 2.3.8; and if maximizes for each , then defines a policy optimal for the original -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.
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, 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).
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.
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 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 — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: depends on the observable history only through , never on more of the past. Recognizing this, and giving 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 '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.
are abstract measurable spaces; the transition kernel 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 , rather than
dependent finite tuples, with a decision rule's dependence on only the first /
coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping
while remaining exactly equivalent to the book's own typing. The belief state
is MeasureTheory.ProbabilityMeasure E_Y, giving 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 and the filtered kernel 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.
Many first-order methods in optimization are fixed-point iterations of a nonexpansive map : 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 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):
Let satisfy for all (the Euclidean norm), and assume the solution set is nonempty. The residual is , , and the averaged operator is .
Powell's weight. For , if and otherwise, with .
Window matrices. For vectors and , let be their unnormalized Gram–Schmidt orthogonalization (3.2), , and
The matrix norm is the induced operator norm.
Algorithm 3.1 (AA-I-S-m). With parameters , and max-memory : start from , , , and . At iteration , set and , orthogonalize against the current window, and restart the window (memory back to , replaced by ) if the memory would exceed or . Then apply one Powell-regularized rank-one update to obtain and the trial point . The trial point is accepted if (and increases); otherwise .
The only hypotheses are nonexpansiveness of , and the parameter ranges. The limit is not specified: it depends on and the parameters.
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).
The accelerated step 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 , requires a bound on that holds uniformly along the run; without the Powell regularization can be singular, and without the restart rule 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.
is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; is rankOne ℝ u ŝ; 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 , the parameters and , and a sorry-free check that runs exist (for ) was built locally. The reset of in line 8 is local to its iteration. is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.
Line 9. The paper prints , derived from (3.3) through , which fails when the window starts afresh (). The mission uses (3.3) there: when , and the printed formula when .
Milestones of §4.1 and Corollary 3.5 carry the hypothesis for all , 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 , contractivity of , 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 , 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 ) and of the convergence steps are all welcome.
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.
Index tracking (§4.8): state (wealth, value of the non-traded index ), action (amounts in traded assets), transition . The objective is (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 , quadratic cost with fixed matrix — via a backward Riccati-type recursion , , so §4.8's content is identifying this problem's own .
Indifference pricing (§4.9): a one-period market with a traded asset and an untradeable asset , four states of the world with probabilities , relative returns , an exponential-utility investor , and a claim . The investor's value with the claim sold short is (Eq. (4.37)); Definition 4.9.1 sets the indifference price as the amount solving for every wealth . The multiperiod extension (unnumbered display, p. 138) replaces the one period by i.i.d. periods and defines at every time the same way, now for a genuine dynamic value function.
where (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 , 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 a claim whose payoff at is the already-computed time- price of recovers 's own time- price directly.
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.
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 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.
For index tracking, the obstacle is not mathematical but representational: recognizing that is a quadratic form 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 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.
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
cost matrix and random / 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 , 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 , 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.
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.
There are products with a common contribution margin . The random demand vector is , nonnegative, with an arbitrary joint distribution on a probability space. The firm has initial wealth .
The firm chooses its investment to maximize one of three objectives of terminal wealth , with profit :
SF is (weakly) preferred when its optimal objective value is at least that of SD. The flexibility premium is , where the indifference cost is a flexible cost at which the firm is indifferent between the networks; the firm prefers SF as long as .
With perfectly reliable resources and any demand distribution, for every , for the loss-averse objective and for the CVaR objective. In the formalization: for every ,
for each expected utility with nondecreasing, and the loss-averse objective; for CVaR the same with the threshold quantified jointly with the investment.
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.
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 , 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, "" 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.
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 () is built into the wealths (A-4)–(A-5), so the committed-cost fraction does not appear. Standing parameters: , , , , arbitrary. The requirements and nonnegative, measurable demand are made explicit; the page treats them as part of the model.
The premium and the indifference cost are not defined as real numbers, since the indifference cost need not be unique. "" is encoded as "SF is weakly preferred for every ", 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 , as (A-5) is printed.
A formalization in which the expected utility of a non-integrable wealth defaults to zero, or in which makes the CVaR bracket , would make the comparisons meaningless; the statements exclude both ( with nonnegative demand bounds the wealths; ). "" is also not trivially true: for a flexible cost above 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.
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 , 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 : the tour is less than twice the optimal (Theorem 4), and more precisely at most times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant 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.
A traveling salesman graph has a finite node set with and a distance that is symmetric, nonnegative and satisfies the triangle inequality . 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 is a tour on a subset of (a one-node subtour has no edges). For , inserts into where it is cheapest: if has at least two nodes, choose an edge of minimizing and replace it by ; if , form the two-node tour on . is the length of minus the length of .
An insertion method builds subtours with and for some , ; INSERT is the length of . With :
The start node and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of .
For every traveling salesman graph on nodes and every run of nearest insertion or of cheapest insertion,
Theorem 4 itself, when is not identically zero, is included as a companion statement.
The bound says that two simple and construction rules are never worse than a factor from optimal on any metric instance, a guarantee independent of , 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 , 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 (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant , 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.
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 to the tree edge joining to its nearest node of , but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds . 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 is sharper than the bound obtained from , so the weaker spanning-tree bound already in the library does not suffice.
Nodes are Fin n with (the paper's nodes shifted to ). The distance satisfies the paper's three axioms plus the normalization , 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. is encoded as insertion of at a list position whose resulting length is minimal over all positions, which is the minimization of (3.1) over the edges of ; COST is the corresponding minimum increase. The subtour index is 1-based as printed (, final). The distance is taken in , 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.
A firm that sells several products must decide, before demand is known, how much production capacity to build and of what kind. Dedicated capacity makes one product; flexible capacity makes any of them. The classic argument for flexibility is demand pooling: capacity that can follow demand to whichever product needs it wastes less than capacity locked to one product (Fine and Freund 1990; Van Mieghem 1998).
When capacity itself is unreliable, as with a supplier that may fail to deliver, a plant that may be disrupted, or a batch that may be rejected, flexibility has a second face. A single flexible resource concentrates the firm's supply in one place, so one failure removes all of it, whereas several dedicated resources rarely fail together. This resource-aggregation effect works against flexibility. Tomlin and Wang (2005) set up a newsvendor network in which both effects are present and ask when a firm should pay more for flexible capacity than for dedicated capacity. Their first answer (Proposition 1) is that a risk-neutral firm facing equal reliabilities and costs never loses by choosing flexibility, whatever the joint distribution of demand. This mission formalizes that answer.
There are products with a common unit contribution margin . The demand vector is random, nonnegative and integrable; its total is .
Two networks are compared. In the dedicated network SD, resource makes only product and has marginal total cost . In the flexible network SF, a single resource, labelled , makes every product and has marginal total cost .
Every resource is unreliable with a Bernoulli yield , . The common reliability is , the yields are mutually independent, and they are independent of demand. Investing in resource delivers capacity and costs : the firm pays the committed cost per unit ordered and a further per unit delivered, with .
The realized profits are
and a risk-neutral firm maximizes the expected profit or over nonnegative investments. Let and be the optimal values. SF is (weakly) preferred if .
The indifference cost is a value of at which , and the flexibility premium is . The firm prefers SF as long as .
The -expected shortfall of a random variable is, for and the lower quantile ,
For any demand random vector :
No distributional form of demand is fixed and no constant is hard-coded beyond the paper's threshold.
and the optimal values are times partial expectations of demand.
Proposition 1 separates the two effects of flexibility under unreliable supply. It shows that for a risk-neutral firm the demand-pooling benefit together with an upside effect of aggregation (one flexible resource succeeds more often than all dedicated ones together) always outweighs the downside aggregation risk. Even with no pooling benefit at all (perfectly correlated demand) the firm is indifferent, not averse. The later results of the paper (loss aversion, CVaR, dual sourcing) are measured against this baseline: a negative premium can appear only once the firm is risk-averse. The expected-shortfall form links newsvendor optimal values to a coherent risk measure, a connection that recurs in inventory risk analysis.
The result is proved in the paper, with a proof that cites Acerbi and Tasche (2002) for two properties of expected shortfall. No machine-checked version exists. A formalization adds three things: a proof for general demand distributions (the paper assumes a joint density and uses the continuous form of expected shortfall); a Lean development of Acerbi–Tasche expected shortfall for general integrable random variables, including subadditivity and affine equivariance; and a reusable model of newsvendor networks with Bernoulli yields and committed costs.
The newsvendor steps (9)–(13) are single-variable concave optimization, but they must be done without a density: the distribution function of total demand may have atoms and flat pieces, so the critical fractile need not be attained or may be attained on an interval, and optimal values must be expressed through lower quantiles. Subadditivity of expected shortfall is the heart of part 1 and is not elementary in the general (atomic) case, which is exactly why the correction term appears. Part 3 requires identifying correlation with almost-sure positive affine dependence, which rests on the equality case of the Cauchy–Schwarz inequality in , and then handling nonnegativity constraints on the investments that the affine change of variables may violate. The obvious shortcut of computing everything from densities is not available, because the goal is stated for every demand vector and part 3 is incompatible with a joint density when .
Randomness lives on one probability space ; demand is X : Ω → Fin N → ℝ and yields are Y : Ω → Fin (N + 1) → ℝ, where dedicated resource is Fin.castSucc n and the flexible resource is Fin.last N. Expectations are Bochner integrals and probabilities are μ.real. The standing assumptions are: , , ; demands measurable, almost surely nonnegative and integrable (integrability is needed for expected shortfall and makes every profit integrable); yields measurable, -valued almost surely with , mutually independent, and independent of demand (the paper states the last in Appendix E). The paper's joint density of demand is deliberately not assumed.
The premium and the indifference cost are not defined as real numbers, because Definition 1's indifference cost need not exist or be unique (for below the threshold both optimal values are for every near ). "" is encoded as "SF is weakly preferred for every ", and "" as "SF and SD are each weakly preferred to the other at ". Weak preference is stated as: every nonnegative SD investment is matched by some nonnegative SF investment; no real supremum is taken. Quantiles in (10) and (12) appear only as parameters with the hypothesis fractile. Part 3 adds square integrability and positive variances, the conditions under which correlation coefficients exist; the threshold milestone adds almost surely positive demand and for its "if" direction. When the Lean value of the threshold is , so part 2 then covers only , where it is true.
A formalization that assumed a joint density, took as a free real satisfying Definition 1, or defined optimal values as real suprema over all of would make parts of the goal vacuous or trivial; each is ruled out above.
Needed infrastructure: single-variable newsvendor optimality for general distributions; the Acerbi–Tasche expected shortfall with subadditivity and affine equivariance; the equality case of Cauchy–Schwarz for correlation. The expected-shortfall and correlation lemmas are reusable well beyond this mission, and contributions of them are especially welcome. Out of scope: the loss-averse and CVaR analyses (Propositions 2–3, §3.2–3.3), the perfect-reliability result (Proposition 4, a separate mission), the dual-sourcing networks (§4) and all numerical results.
For a convex function on , a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.
Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of -valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the neighbors obtained by independently nudging each coordinate by , , or (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.
Let be a function with nonempty effective domain . The convex closure of is
the pointwise supremum of every affine function minorizing on all of . If agrees with on integer points, is convex extensible. The integral neighborhood of is
and the local convex extension relaxes 's definition by requiring the affine minorant condition only on rather than on all of . Always pointwise, and the two agree on . A function is integrally convex if everywhere on — equivalently, if is a convex function on all of (it is automatically convex on every unit cube with , but need not be convex globally without this extra condition).
A discrete set is hole free if equals the set of integer points in its own real convex hull, and denotes the minimizer set, over , of the linearly perturbed function .
For integrally convex and :
where is the indicator vector of . The right-hand side is a check over at most points (each coordinate independently unchanged, incremented, or decremented), regardless of how large is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single or letting the right-hand side range over all of would trivialize or falsify the equivalence.
Proposition 3.18: convex extensible hole free for every (and conversely, when is bounded). Proposition 3.19: is integrally convex if and only if every restriction to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of one at a time.
The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension , not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M-convex, L-convex, and L-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.
Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on , and an LP-duality-based alternate formula for ) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.
The natural first attempt is to try to prove the "" direction of Theorem 3.21 by a direct induction on the -distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces to be a local minimizer of the local convex extension restricted to the unit ball around , then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on ) to conclude globally minimizes , and finally uses integral convexity () to transfer this back to on . The identification of 's local behavior with 's convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.
The ground set is , represented as Fin n → ℤ; 's codomain is WithTop ℝ
(exactly ), while the convex closure and local convex
extension take values in EReal (exactly , a complete
lattice, so their defining suprema are total functions with no side conditions). A trivializing
formalization of the goal would quantify the right-hand side over a single fixed pair,
or over all of instead of the sign-pattern neighbors; both are excluded by keeping
universally quantified Finset (Fin n) ranging over the full sign-pattern space
(minus the trivial case, which the equivalence still holds through vacuously).
Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's
Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary
convex-function local-to-global optimality, LP duality): these are broadly available in
Mathlib's convex-analysis library in some form, but none of them is imported here, since none
appears in the statement of any item this mission drafts — they belong to a proof this pass
does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer
are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex
functions and will need the same convex-closure/local-extension vocabulary.
A multiple objective program asks to maximize objectives simultaneously over a feasible set . There is usually no point that is best in every objective, so the object of interest is the set of nondominated criterion vectors: those that cannot be improved in one objective without being worsened in another. Interactive procedures for multiple criteria decision making work by computing nondominated vectors one at a time, by solving a single-objective scalarization, and presenting them to a decision maker.
A scalarization is useful for this purpose only if it is complete (every nondominated vector is the solution of some instance of it) and sound (every solution is nondominated). The weighted-sum scalarization is sound for positive weights but not complete when the feasible region is nonconvex. R. E. Steuer and E.-U. Choo (Math. Programming 26 (1983) 326–344) built their interactive procedure on weighted Tchebycheff distances to an ideal point, following Bowman (1976) and Choo and Atkins (1983). In §3 they treat finite feasible regions with an augmented metric, which requires choosing a small parameter . In §4 (pp. 334–336) they show that a lexicographic version of the weighted Tchebycheff program is complete and sound for any feasible region, including nonconvex continuous ones, with no parameter to estimate. This mission formalizes that result, Theorems 4.5 and 4.6.
Let , , be the set of feasible criterion vectors (the image of under ). A vector dominates if for all and for at least one . The nondominated set consists of the dominated by no .
An ideal criterion vector is a with
where , and is required whenever (i) more than one nondominated vector maximizes objective , or (ii) the only nondominated vector maximizing objective also maximizes another objective. So may touch in coordinate only in a controlled way.
The weight set is the simplex . For the weighted Tchebycheff program minimizes subject to for all and ; its value at a fixed is
The lexicographic weighted Tchebycheff program first minimizes over and then, among the first-stage minimizers, minimizes . The paper writes it as with pre-emptive priority factors. Finally, for the weights of eq. (4.3) are , normalized to sum to one, when for all . When some , is on the coordinates with and elsewhere.
For compact , an ideal vector and ,
The goal is the characterization; Theorem 4.5 is the stronger half with uniqueness and an explicit weight.
Theorem 4.6 says that, as ranges over the simplex, the lexicographic weighted Tchebycheff program returns exactly the nondominated set, for any feasible region: no convexity, no finiteness, no polyhedral structure. Theorem 4.5 adds that each nondominated vector is the unique output for a weight vector computable from the vector itself, which is what an interactive procedure needs to sample reliably. The price, as the paper notes, is two optimization stages instead of one; the gain is that no augmentation parameter must be estimated. The result is a standard entry in the textbook treatment of Tchebycheff scalarizations (Steuer, Multiple Criteria Optimization, 1986; Ehrgott, Multicriteria Optimization, 2005).
The result is proved on paper. To our knowledge no machine-checked version exists in Lean or Mathlib, which has no material on Tchebycheff scalarization of multiple objective programs. The formal statements below also pin down two points the printed text leaves loose: the direction of the priority factors, and a closedness assumption that the proof uses without stating it.
The ⇐ direction and the soundness remark are short: a dominating vector is at least as good in the first stage and strictly better in the second. The work is in Theorem 4.5. The obvious argument is that is the unique minimizer of the first stage with weights ; the paper says so. That is true when in every coordinate, but false when for some : then , and every with ties with , dominated vectors included. For example, with and , the vectors and tie. Only the second stage separates them. Showing that it always selects requires every tied vector to lie below a nondominated vector attaining , which by the ideal-vector rule must be . That existence step fails for sets that are not closed.
Criterion vectors are Fin k → ℝ with [NeZero k] (); objectives are indexed from . , the objectives and the program's variable are eliminated: is a Set (Fin k → ℝ) and the first-stage value is above (the paper's metric uses , which agrees with on ). is Mathlib's stdSimplex ℝ (Fin k). "Minimizes" is global minimization over ; "uniquely minimizes" means every lexicographic minimizer equals as a criterion vector.
Conventions and added hypotheses:
IsLexMin. The printed "" read literally gives the second stage priority; the paper's text on p. 336 and the goal-programming convention it cites give priority. The two-stage reading is encoded, and the program is not replaced by a weighted sum with fixed numbers, which would be the augmented program of §3.Infrastructure needed: dominance and nondominated sets, the ideal vector, the weighted Tchebycheff value, the weights (4.3), and the lexicographic minimizer, all provided as definitions. Proofs will need existence of minimizers of continuous functions on compact sets and a maximal-element argument in the product order on a compact set. Both are reusable for other multiobjective results. Proofs of any item, and faithful statements of Corollaries 4.1 and 4.4 (polyhedral ), are welcome.
Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.
An -period financial market with risky assets consists of a probability space with filtration , trivial; a riskless bond with deterministic interest rate on (so ); and risky assets with relative price changes , -measurable and a.s. strictly positive (). A portfolio (trading strategy) is an -adapted process , , ; is the money invested in asset on . Its value before/after trading at time is , ; is self-financing if a.s. for every interior . An arbitrage opportunity is a self-financing with , a.s., with positive probability. The relative risk process is the excess return of asset over the riskless rate.
This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.
No further milestone is formalized in this mission: this chapter's only other theorem, Theorem
3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the
space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the
Formalization scope section and HARD.md.
Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.
Formalizing it contributes the exact discrete-time, filtration-indexed statement of the
reduction — a result absent from the platform (searched "arbitrage", "self-financing",
"martingale measure", "utility function"; the one related hit,
LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming
duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix —
a different equivalence for a different, non-stochastic model, not reused here).
The direction "local no-free-lunch at every stage no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from ) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth , and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between " a.s." failing to imply " with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).
The market is represented via DiscreteFinancialMarket, bundling the probability space,
filtration, and the two primitives (, ) actually used; price processes
are not separately represented, since they would only be running products of these two
primitives with no further role once the relative risk process is derived. Filtration is
represented directly as a monotone family of sub--algebras with a trivial Fam 0, not
via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here.
Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's
own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition,
needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken
as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg
semimartingale (only specific constructions such as Itô integration against Brownian motion);
this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it,
not a hidden simplification of the definition's own content, which states the self-financing
equation exactly as the book writes it.
Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem
asserts weak convergence of the whole path of the binomial-tree price process to the
Black-Scholes-Merton stock price on the Skorokhod space of càdlàg functions with the
Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional
convergence in distribution, and the book explicitly names this topology (it is not left
implicit). Mathlib has no formalization of or the Skorokhod topology, and building
either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the
tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking
outside the scope of a single milestone; weakening the claim to convergence of
finite-dimensional distributions, or silently substituting an unnamed alternative topology
(e.g. uniform convergence, under which the claim would in fact be false, since the discretized
paths have jumps the limit does not), would misstate the theorem rather than state a smaller
piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in
Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock
this result.
No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios
(Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the
one-period condition of part b) quantifies over all -measurable — narrowing either quantifier (e.g. to strategies with bounded positions) would
state a weaker, easier claim than the book's own theorem.