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?
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.
Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.
For , the epigraph is , and is convex iff is a convex set; is proper if additionally its effective domain is nonempty, and closed if is topologically closed. A function is concave, proper, closed analogously via its hypograph. The convex conjugate is , and the concave conjugate . The relative interior of a set is the interior of relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an matrix , , , the primal and dual linear programs are and , with feasible regions , . A matrix is totally unimodular if every square submatrix has determinant , , or . A discrete set is hole free if , where is the convex hull of 's real embedding; the discrete Minkowski sum is .
Goal (Theorem 3.6, Fenchel duality). For proper convex and proper concave satisfying at least one of four alternative conditions — a relative-interior condition on , a polyhedrality condition on the same, or the analogous pair of conditions on together with closedness of , —
with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).
Supporting milestones. Theorem 3.2 (biconjugation: is always closed proper convex, and for closed proper convex ); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).
Fenchel duality is the single result from which the separation theorem, LP duality, and (via the
totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying
weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing
this chain in one mission exhibits that structure directly, rather than treating each result as
an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that
naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's
good closure properties under Minkowski sums, which is exactly the gap the book's later
M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is
therefore the motivating negative result for the rest of the book's positive theory, not a loose
end. So far as a platform search shows, no existing formalization matches this chunk's specific
combination of extended-valued (possibly ) functions, the four-alternative Fenchel
duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related
platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions
on general normed spaces under a single relative-interior-and-solidness hypothesis, a different
generality from the extended-valued, four-hypothesis statement here.
The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.
All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued
(Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions,
so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a
well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex
subset of the ordinary real vector space (Mathlib's Convex ℝ),
following the book's own equivalent characterization, rather than unfolding the direct
inequality definition, which would require a extended-arithmetic scalar-multiplication
convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior
is defined directly from the book's own metric-ball-intersected-with-affine-hull description,
since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite
intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection
between the two vertex sides restricted to the edge set — a faithful, not narrower,
representation since every perfect matching between equal-size parts arises this way. The
formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced
to the easiest single case), and no result is stated only for finite-valued (never )
functions, which would discard the entire point of the extended-value convex-analysis framework
this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex,
Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral
apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of
the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would
be a natural entry point.
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.
Real investors do not merely accumulate wealth for a single terminal payoff; they consume along
the way, and the market they invest in is rarely a single fixed statistical regime for years at
a time — bull and bear markets, business cycles, and volatility regimes shift the distribution
of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by
adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem),
and §4.4 extends it again by letting the return distribution itself depend on a hidden,
Markov-modulated environment state. Both extensions are shown to be genuine instances of the
same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint
consumption-investment choice and the extra regime coordinate change the state and action
spaces, but not the proof strategy, which is exactly the point.
The consumption-investment problem: state (wealth), action (consumption , amounts invested), transition , reward , terminal reward . Value functions . The one-period sub-problem: , , .
The regime-switching extension (§4.4): an environment process , a finite-state Markov chain with transition probabilities , modulates the risky-asset return law: given , the next relative risk has law , and has joint law given , . The augmented state is ; value functions are defined analogously, with the recursion incorporating a finite sum over the next regime.
with strictly increasing, strictly concave, continuous, and an optimal strategy realized
by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every
closed-form corollary below specializes it.
Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).
Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, , is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime 's returns dominate regime 's for every risk-averse (concave, monotone) preference," not merely "regime has a higher mean."
No result of this chunk was found on the platform (searched "consumption investment", "regime
switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says
so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise
joint-choice statement of each result and, for the comparative-statics theorems, the correct
increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order
(≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different
relations and must not be conflated.
The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction and an investment fraction optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ( interacts with the investable amount ), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of in directly from alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.
The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the
one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern
exactly, extended to a joint action. The regime-switching model
(RegimeSwitchingMarket) represents the finite regime set abstractly (a Fintype with a
row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on
the joint disturbance): the book's own formula for is already a finite sum over the
next regime of an integral against , so this is the direct, faithful representation and
needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator
recursing through this finite-sum-of-integrals at each step (the natural generalization of
chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate,
rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder
(Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx)
does not include the increasing-concave order this chunk's theorems actually use — reusing one
of those three would silently substitute a different hypothesis, exactly the trap the chunk
brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated
fresh for a finite chain given by its transition matrix.
No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two
independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the
comparative-statics pair) each state their own explicit recursion for — matching the
brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6
gives and recurses backward; Theorem 4.4.2 gives and recurses forward) — encoded
exactly as each theorem states it, not standardized to one direction.
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.
An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).
An investor with utility function (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth invests in a bond (interest rate on ) and risky assets with relative risk (Chapter 3). The one-period problem: admissible investments , , . The multiperiod problem is the -stage Markov Decision Model with state space (wealth), action space , transition , zero one-stage reward, terminal reward ; its value functions are over Markov portfolio strategies .
with strictly increasing, strictly concave and continuous, and an optimal portfolio strategy realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.
Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).
Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.
No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for , since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable (, , or a wealth-independent constant) each uses.
The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if [strictly increasing/concave/continuous with linear growth], then is a utility function on up to the growth bound, so Theorem 4.1.1 applies directly to ." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.
The multiperiod value function V is defined as an explicit supremum over admissible Markov
portfolio strategies (not the Bellman recursion itself, and not full history-dependent
strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov
strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than
restatements of the value function's own definition. The one-period vocabulary
(OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement
matching §4.1's own notation (a single , , no time index), independent of chunk 03's
full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period
reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the
book (a concave function is dominated by an affine function; no-arbitrage bounds admissible
actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather
than re-derived, since re-deriving them is not this proposition's own content. HARA and power
utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and
exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since
their admissibility sets and objective functions genuinely differ (a strict vs. non-strict
inequality; a fraction vs. an absolute amount).
No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for (a finite product or sum over of genuinely different per-stage terms) rather than a shared abstract "some sequence exists with " — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form (, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.
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.
Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).
A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.
A generator is : a state set , a finite alphabet of events, a partial transition function , an initial state and marker states . Extending to strings gives the generated language (strings along which is defined from ) and the marked language (those that end in ). The closure of a language is its set of prefixes. Throughout, is trim: . A recognizer for a language is an accessible generator whose marked language is .
A subset of events is controllable. A supervisor is where is an accessible deterministic automaton with possibly infinite state set and is a state feedback map; events outside are always enabled. The closed loop runs and in lockstep and allows from iff and are defined and . Its languages are , (marker set ) and .
is complete if never refuses an event that the plant can execute and enables: , and imply . It is proper if it is complete and .
A projection is a surjection with , , wherever is defined, and .
For a language , strings are -equivalent if for all . The automaton is -reduced if -equivalent strings of lead to the same state, and -trim if every state is reached by a string of .
Let be complete, , , with -reduced and -trim, and let be a trim recognizer for . Then there are and such that satisfies
Proposition 8.1 (p. 219): for complete and a projection , (i) is unique; (ii) ; (iii) is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.
The displayed steps of the proof of Theorem 10.1 (pp. 223–224): is well defined on ; it is a projection once and ; follows from two enablement conditions; is complete; and .
Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of . Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.
The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.
The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, for all , is not available: the page asks for it only where is defined, and Proposition 8.1 (ii) holds only because completeness of compensates for transitions that has and lacks. Likewise, the map of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that recognizes with all states marked and that is -reduced.
The alphabet is a Lean type α with [Fintype α] (the page's , which is Lean syntax); strings are List α, is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and " enabled at " means or ; the page's is the same object under this extension. The closed loop is run from without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.
Standing assumptions that are hypotheses of every theorem: finite; trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume complete, -reduced and -trim, and a trim recognizer for with all states marked, and is built on that given rather than on a recognizer chosen by the prover. The conclusion names and as the languages of , not as free variables. A projection predicate that drops , surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.
Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.
Most concrete applications of Markov Decision Theory — inventory control, cash management, linear-quadratic regulation, sequential games — have data that does not change from one period to the next: the same state space, action space, transition mechanism and reward apply at every stage, only discounted by a fixed factor per period. Bäuerle and Rieder's Chapter 2, §2.5 specializes the general finite-horizon theory of the previous sections to this stationary case, and §2.6 shows the specialization at work on three classical models: a card game with a famously boring answer, a firm's cash-management problem, and stochastic linear-quadratic control. Together they demonstrate the payoff of the abstract theory: once the Structure Assumption is checked for a stationary model, the general machinery (the Forward Induction Algorithm) produces the concrete optimal policy — a critical-level -type control for cash management, a linear feedback law for LQ control — with no further case-specific argument.
A stationary Markov Decision Model is a Markov Decision Model (Definition 2.1.1) whose data does not depend on the stage: the reward at absolute time is and the terminal reward at time is , for a fixed discount . For a policy sequence (each a decision rule with ), the reward-to-go is and the value function is . The operators , , are the stationary counterparts of §2.3's non-stationary operators. The (stationary) Structure Assumption (SAN) asks for sets , with , , and every having a maximizer in .
A firm's cash level moves under i.i.d. shocks; each period the firm transfers to a new level at linear cost , pays a convex, coercive holding cost (), and the level becomes . Modeled as a stationary MDM with , , :
with , and the optimal policy transfers up to below it, down to above it, and does nothing in between. This is the weakest stable statement: it asserts the existence of critical levels with the stated recursive characterization, not any closed form for itself (which depends on 's exact shape and is not computable in general).
Three milestones build toward and alongside it: the Reward Iteration theorem and stationary Structure Theorem (Theorems 2.5.3-2.5.4, the general machinery instantiated), the trivial-but- sharp red-and-black card game (Theorem 2.6.1), and the stochastic linear-quadratic problem (Theorem 2.6.3, a Riccati-type recursion with random coefficients).
Theorem 2.6.2 is the textbook derivation of -type control, the dominant policy structure in inventory theory and cash management: a firm should act only when its state leaves a band, and should act to bring it exactly to the band's edge, never further. Its proof pattern — verify (SAN) with the convex functions of at most linear growth, extract the critical levels from the derivative conditions of a one-stage minimization — is the template used across the inventory-control literature for essentially every variant of this problem. Theorem 2.6.1's answer ("no strategy beats stopping immediately") is a genuine, if minimal, comparative-statics fact: a positive-content instance of collapsing to functions constant on the game's absorbing set, forcing every action to be a maximizer. Theorem 2.6.3's Riccati-type recursion, with random transition coefficients, generalizes the classical deterministic-coefficient LQR (linear-quadratic regulator) of control theory; the recursion governs mean-variance and quadratic-hedging problems return to in later chapters of this book (Chapters 4 and 6).
None of the three examples' specific results were found on the platform (searched for
"comparative statics", "convex Markov decision", the exact model names, and "bang-bang"/"LQR"
adjacent terms). BertsekasDP.riccati_completion_of_square is the platform's one close relative
to Theorem 2.6.3: it solves the deterministic-coefficient LQR by a completion-of-squares
argument, not the random-coefficient recursion here, so it is cited as related work rather than
reused. The proofs themselves are complete and self-contained in the book (a few pages each,
using only single-variable convex analysis and elementary linear algebra); this mission
contributes the formal statement of each, in its full generality (general convex , general
random coefficient pairs), as the task for a sorry-free proof.
The cash-balance proof's central step is showing the minimizer of the one-stage problem is of critical-level form for every in the candidate class — not just for the particular sequence that eventually arises. The obvious shortcut, guessing the form of directly and verifying it solves the Bellman equation by substitution, fails because are themselves defined only implicitly, via one-sided derivative conditions on ; there is no closed form to substitute except in degenerate special cases (e.g. quadratic). The genuine content is the general argument (convexity of the one-stage objective forces a unique critical-level minimizer structure, and this structure is preserved under ) that lets the induction go through for an arbitrary convex, coercive . For Theorem 2.6.3, the natural first attempt — solve the deterministic LQR recursion and substitute expected coefficient matrices for the random ones — is not obviously valid, since in general; the correct recursion genuinely involves the joint second moments of , which is exactly what the standing positive-definiteness assumption on (not on itself) is there to make precise.
The stationary vocabulary (StationaryMarkovDecisionModel, its operators, J, (SAN)) is
restated independently of chunk 02a's non-stationary vocabulary — drafts in this series cannot
import one another, and the book itself keeps the two notationally separate ( vs. ,
related by , a relation this mission does not separately formalize
since no listed result needs it). Theorem 2.6.3's stochastic LQ problem is explicitly
non-stationary in the book's own text, so a second, NS-prefixed restatement of the non-
stationary model and value function (via the Bellman recursion established as Theorem 2.3.8,
not the sup-over-policies primitive — the same simplification chunk 02c makes for its own V)
is introduced solely for that one theorem. The card game (Theorem 2.6.1) is formalized on the
concrete state space and action space Bool, with the model's
exact transition density, reward and terminal reward given as hypotheses on an abstract
StationaryMarkovDecisionModel, matching the book's own discrete-density notation
(introduced in the text following Theorem 2.5.4) rather than
built from an explicit PMF/Kernel construction — a lighter-weight but equally precise
formalization, since the density equations pin the kernel exactly. The stochastic LQ problem
uses Matrix (Fin m) (Fin m) ℝ and needs a MeasurableSpace (Matrix m n α) instance Mathlib
does not provide (Matrix is a non-reducible def for m → n → α); this mission supplies it by
transport across the definitional equality. Random matrix moments are
computed entrywise as ordinary Bochner integrals against the joint law of .
A trivializing formalization is ruled out on two fronts: the cash-balance critical levels
are existentially quantified as functions of , not fixed constants (dropping
the index would silently claim a single band works for every horizon length, which is false in
general); and the card game's "every strategy is optimal" is stated as a universally-quantified
claim over all policy sequences, not weakened to mere existence of an optimal one. Reusable
infrastructure: the jointMatMean/xQx helpers and the MeasurableSpace (Matrix m n α)
instance are generic and available to any later chunk needing random-matrix moments (none of the
remaining chunks' briefs currently list one, but Chapter 4's mean-variance and LQ-flavored
missions may). sorry-free proofs of all five items are welcome contributions; Theorem 2.5.3's
short inductive proof (unwinding the accumulator definition against the operator-composition
recursion) is likely the easiest entry point.
BertsekasDP.riccati_completion_of_square
on the platform).Single-machine sequencing with deferral costs asks how to order jobs when the price of finishing a job depends on when it finishes. A job completed at time incurs the cost ; lateness penalties, holding costs and service-level penalties are special cases. Two objectives are standard: the sum of the costs, studied by McNaughton (Management Science 6(1), 1959) and Lawler (Management Science 11(2), 1964), and the maximum cost, the bottleneck objective, which asks that no single job be charged too much.
At the end of his 1968 paper on minimizing the number of late jobs (Moore, Management Science 15(1)), J. M. Moore added a short section, suggested by E. L. Lawler, showing that the maximum-cost problem reduces to a family of feasibility problems with due-dates. Each such problem is settled by one sort, by Jackson's earliest-due-date rule (J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, UCLA Research Report 43, 1955). This reduction is the unconstrained case of what later became Lawler's algorithm for (Lawler, Management Science 19(5), 1973).
Timeline:
A finite nonempty set of jobs is processed on one machine that starts at time and runs without idle time or preemption. Job has processing time . A schedule is an ordering of with each job appearing exactly once, and is the completion time of in : the sum of the processing times of and of every job before it.
Each job has a deferral cost , which is continuous, bounded and non-decreasing. The maximum deferral cost of is
For a cost level , the generalized inverse is the latest time at which job can be completed at cost at most . Following the paper's definition (p. 108), with times :
For each , is a schedule ordered by the "due-dates" , with ties broken arbitrarily. has no late jobs if for every .
In Lean these are IsSchedule, completionTime, Pstar, NoLateAt and maxCost in the namespace MooreLateJobs.MaxDeferral.
Let satisfy: (1) has no late jobs; (2) for every , has at least one late job. Then for every schedule of ,
This is the last sentence of the section (p. 109). The goal takes with its two properties as given, so it needs no hypothesis beyond the model.
The result. The theorem turns a min–max problem over all schedules into a monotone one-parameter feasibility question. Each value of is checked by a single sort, and the optimal level is the threshold where feasibility switches on. The same threshold structure underlies bottleneck scheduling and the backward rule for . Special cases include minimizing the maximum lateness, , clipped to be bounded, and minimizing the maximum weighted tardiness.
Formalizing it. The result is classical and proved on paper, but no machine-checked proof of it, or of Jackson's lemma, is known to exist. The mission would produce a checked Jackson lemma for extended-real due-dates, a verified generalized inverse of a monotone continuous function with the paper's case analysis, and the threshold argument connecting them. Jackson's lemma is shared with part I of this series (minimizing the number of late jobs).
The reduction is short on paper. The work is in the edge cases that the paper passes over:
Conventions committed to in Lean:
ι with decidable equality, and the job set is J : Finset ι, assumed nonempty in the goal. Processing times are t : ι → ℝ with 0 ≤ t i: this is added, because the page never states it but processing times are durations.P : ι → ℝ → ℝ, each continuous, bounded (∃ M, ∀ s, |P i s| ≤ M) and monotone, as on p. 108. The Introduction's assumption has no counterpart, since the problem has no given due-dates, and it is not assumed.Pstar f y : EReal, with every time in the definition ranging over . If the level set is unbounded, its "max" does not exist, and the value is fixed to . The final case is "otherwise", which for continuous monotone is the paper's case (c).SD : ℝ → List ι such that SD y is a due-date-ordered schedule for every . Theorems hold for every such family, so every tie-break is covered.The goal is not the trivializing statement "every on-time is optimal", which is false for large . It concerns exactly the threshold level . The minimum is over all schedules of , not over the only.
The needed infrastructure is list permutations, prefix sums and Finset.sup', plus basic facts about sSup of closed sets bounded above in ℝ, and the intermediate value theorem. The Jackson lemma and the generalized inverse are reusable beyond this mission. Contributions are welcome on any milestone, in any order. The goal depends only on the Jackson lemma and on properties of Pstar.
Not in scope: the remark that "can be found to whatever accuracy is desired by a binary search technique" (computational), and the sum-of-costs problem the section contrasts itself with.
Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.
Let be a finite ground set (identified with in the book) and let be a symmetric real matrix. has off-diagonal nonpositivity if for all , and diagonal dominance if for every row . The associated quadratic form is for . For write , for the componentwise maximum and minimum. A function is submodular if for all , and has translation submodularity if the stronger inequality holds for every , where is the all-ones vector (ordinary submodularity is the case ).
On the conjugate side, for write , , and let denote the -th unit vector ( denotes the zero vector). A function has the exchange property if for all and there exist and such that for every . The Legendre-Fenchel conjugate of is ; two functions are conjugate to each other when and . For positive-definite symmetric , the quadratic forms and are conjugate to each other exactly when and are matrix inverses of one another.
Goal (Theorem 2.11). For conjugate strictly convex quadratic forms and as above,
This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.
Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of ); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of ); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric , among membership in the matrix class , two sign-consistency inequalities on the columns of together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class is closed under taking principal submatrices).
The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.
Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.
The naive approach to Theorem 2.11 tries to derive the exchange property for directly from the defining supremum in the conjugate relation , differentiating under the sup; this fails because the exchange property compares along a specific combinatorial direction tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair without already knowing the sign pattern of . The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on itself (conditions (b)/(c)) via the identity , and closes the loop back to membership in using the Farkas lemma applied to the linear system — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.
Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V])
rather than a fixed Fin n, matching this project's convention elsewhere and letting
Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted
index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and
dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel
conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be
finite in general even though it is finite here. Every min(0, \dots)-based condition in
Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the
finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop
machinery — a faithful, checked-equivalent simplification, not a narrowing (see
MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs
instantiation anywhere in this mission. The formalization does not trivialize: the goal's
exchange property is stated for the specific combinatorial direction with , — not an arbitrary
direction, which would reduce the exchange property to a restatement of ordinary convexity and
discard the entire combinatorial content the mission is about.
Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib);
everything else (submodularity, translation submodularity, the exchange axioms, the
sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to
the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13)
as lemmas; contributions completing any of the seven milestones independently, or supplying the
Schur-complement induction behind Proposition 2.4, are welcome.
Monotone variational inequalities cover convex minimisation, convex–concave saddle-point problems, Nash equilibria of monotone games and complementarity problems, and they are the standard model for these in optimization and operations research. First-order methods for them (extragradient, forward–backward–forward, reflected and projected gradient methods) need a stepsize below , where is a global Lipschitz constant of the operator. That constant is often unknown, too pessimistic, or nonexistent: in composite minimisation with a locally smooth term, or in saddle-point problems with bilinear-plus-nonlinear couplings, the operator is only locally Lipschitz. The usual remedy is a linesearch, which costs extra operator or prox evaluations per iteration and complicates the complexity accounting.
Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities (preprint 2018, Optimization Online 6598; published in Mathematical Programming, 2020, doi:10.1007/s10107-019-01416-w) proposes the Explicit Golden Ratio Algorithm (EGRAAL): its stepsizes are computed in closed form from the last two iterates, it uses one evaluation of and one proximal step per iteration, and it needs neither a Lipschitz constant nor a linesearch. This mission formalizes its main convergence theorem, Theorem 2 of the preprint.
Let be a finite-dimensional real inner product space with norm . Let with domain , and . The variational inequality (1) asks for
Its solution set is . The standing assumptions are: (C1) ; (C2) is proper, convex and lower semicontinuous; (C3) is monotone on , for .
The proximal operator is . Write for the golden ratio. Algorithm 1 (EGRAAL) takes , , a parameter and a cap , sets , , , and for computes
with the convention in the middle term. The paper uses the bifunction .
If is locally Lipschitz continuous and (C1)–(C3) hold, then for every run of Algorithm 1 there is with
Nothing is fixed beyond the paper's parameter ranges: , , and the starting points are arbitrary. The two sequences share one limit.
The result. Theorem 2 shows that a monotone variational inequality with a locally Lipschitz operator can be solved by a method whose stepsizes adapt to the local curvature of at no extra cost: one evaluation and one prox step per iteration, and no global constant and no backtracking. Because is only ever evaluated at the prox outputs , the method also applies when is undefined or badly behaved outside the feasible set, where reflected-gradient methods can fail. The same analysis gives an ergodic rate and, under an error bound, an -linear rate (§2.2 of the preprint; not part of this mission). The paper also derives fixed-point algorithms for demi-contractive operators from it.
Formalizing it. The theorem has a published proof; to our knowledge no machine-checked version exists, and Mathlib has no proximal operator, no theory of monotone variational inequalities and no Fejér-monotonicity lemma. This mission produces a formal convergence proof for an adaptive first-order method with a nonsmooth convex term, together with reusable pieces: the prox-inequality for extended-real-valued convex functions, a finite-dimensional Fejér convergence lemma, and a formal model of an adaptive-step algorithm with the rule.
The usual convergence argument for projected or extragradient methods bounds the cross term using a global Lipschitz constant and a fixed stepsize. Here neither exists. The stepsize at iteration depends on the iterates, and the energy that decreases changes from step to step, since it involves . Local Lipschitz continuity gives a usable constant only once the iterates are known to be bounded, and boundedness has to come from the energy inequality. Stepsizes that tend to would also break the argument (Lemma 2 excludes this for bounded runs). The last step, identifying cluster points as solutions, needs lower semicontinuity of and a limit in the prox-inequality along a subsequence with convergent stepsizes.
is a real InnerProductSpace with FiniteDimensional ℝ E. is a map E → EReal; (C2) is a structure: never takes the value , is finite somewhere, has a convex epigraph in , and is LowerSemicontinuous on . is a total map E → E, and every hypothesis on it (monotonicity, Lipschitz bounds) is restricted to . The variational inequality is stored as , with , which avoids extended-real subtraction. is an argmin predicate, so it never produces a junk value. The algorithm is a predicate on the four sequences, written for index . The rule is a case split: if the step is . No condition such as or is imposed.
"Locally Lipschitz" is formalized as Lipschitz on every bounded subset of . This is the property the proof of Lemma 2 uses. It agrees with local Lipschitz continuity when is closed (for example for a closed convex , or finite everywhere) and is stronger otherwise. Eq. (27) is stated for , where and are defined. Lemma 1 carries the hypothesis of its cited source, without which it is false.
The statements are not vacuous: , satisfy (C1)–(C3) and the Lipschitz hypothesis, and admit a run of Algorithm 1 with . A proof of Theorem 2 must hold for every run with the paper's parameters, not only for such degenerate data.
Contributions welcome: the prox-inequality and the existence of the prox for proper convex lsc (both reusable beyond this mission), the Fejér lemma, the algebraic estimates (18) and (24), and the energy inequality (27). Once these are in place, Lemma 2 and the cluster-point argument complete Theorem 2.
Newton's method converges quadratically near a non-degenerate minimum, but on its own it has no global guarantee: far from a minimizer the Newton step may increase the objective, and at points where the Hessian is indefinite it may not even be a descent direction. For most of the method's history, the global behaviour of second-order methods was controlled by line searches or trust regions whose worst-case complexity was not quantified.
Nesterov and Polyak (Math. Program. Ser. A 108 (2006) 177–205) proposed regularizing the Newton model by a cubic term and proved global worst-case rates for the resulting method on several problem classes. This mission is the third in a series formalizing that paper. It concerns the class of gradient dominated functions of degree two, for which the gap to the optimal value is bounded by a multiple of the squared gradient norm. For this class the paper shows that the method first converges linearly and then superlinearly, with explicit constants and without convexity.
The class itself predates the paper by four decades. Polyak (USSR Comput. Math. Math. Phys. 3 (1963)) introduced the inequality to prove linear convergence of gradient descent without convexity; related inequalities are due to Łojasiewicz. Under the name Polyak–Łojasiewicz condition it has become a standard assumption in the analysis of first-order methods, for example in Karimi, Nutini and Schmidt (2016). Theorem 7 of Nesterov and Polyak is the corresponding result for a second-order method.
Let be a closed convex set, and let be twice differentiable on with gradient and Hessian . The Euclidean norm is , and on matrices it is the spectral norm. The standing assumptions of the paper are:
For the cubic model of at is
A cubic-regularized Newton step is any global minimizer of over . Write and .
Method (3.3). Fix . At iteration , choose such that , and set . The choice always passes this test.
Gradient domination of degree two (Definition 3 with ). The function attains its minimum over at some , and for a constant
The minimizer need not be unique. Two examples:
Two quantities appear in the targets. With , they are
For every run of method (3.3) on a gradient dominated function of degree two, both of the following hold.
The constants , , and are the paper's, and neither weakened nor improved.
In the order a proof would use them:
The result shows that on the Polyak–Łojasiewicz class, cubic regularization has two properties at once.
As the authors note, this is the only class in the paper where the initial gap enters the complexity of the first phase polynomially, through .
The result has been proved on paper since 2006. As far as the platform's catalog shows, none of the paper's statements has a machine-checked proof. This mission produces:
Once Lemma 7 and the recursion (4.17) are in hand, deriving the two rates is elementary scalar analysis. The difficulty sits upstream.
The second-order condition. Proposition 1 is a statement about the global minimizer of a nonconvex function of variables. The first-order condition (2.5) alone does not give it: a stationary point of the cubic model that is not a global minimizer can violate it. The inequality (2.11) on which every rate rests needs Proposition 1.
Lemma 7 needs two facts. First, the new iterate stays in , where the Lipschitz bound applies. Second, the monotonicity of on , which lets the unknown be replaced by .
The phases. Both need bookkeeping with nonnegative quantities under fractional powers. Along a run, the gap must be shown to be nonnegative and non-increasing before any power of it is taken.
The following conventions are fixed:
EuclideanSpace ℝ (Fin n) with arbitrary . The gradient and Hessian are maps g and H, with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every . At boundary points these are two-sided derivatives. The Lipschitz condition uses the operator norm on E →L[ℝ] E, which is the spectral norm.T is a global minimizer of the cubic model", and every lemma about is stated for every such T. The value is written as plus the model at that minimizer, with no infimum over an expression.Real.rpow of nonnegative numbers.Trivializing formalizations are ruled out. Using a stationary point in place of a global minimizer of the model, allowing , or requiring the domination inequality on all of rather than on would each change the theorem. None of these is done. A worked instance (, ) checks that the hypotheses are satisfiable.
A complete development needs Taylor estimates for a map with Lipschitz derivative on a convex set, the optimality conditions of the cubic subproblem (Section 5 of the paper characterizes its global minimizers through a one-dimensional dual problem), and some real-power arithmetic. The Section 2 lemmas are reusable for every other mission in the series and for any analysis of cubic-regularized or trust-region methods. Contributions are welcome at every level:
For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.
Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for . This mission formalizes that theorem.
Timeline:
For , is the set of permutations of , for , and . For and , counts the increasing -tuples in with , and the subpermutation density is for and for . A permutation sequence is convergent if converges for every fixed .
A limit permutation is a Lebesgue measurable such that is a cdf (non-decreasing, right-continuous, ) for every and for every ; the set of them is . Each has an associated random point with and conditional cdf , joint distribution function , and pattern densities (the probability that independent copies of form the pattern ).
For , the step limit permutation spreads the permutation matrix of uniformly over the corresponding grid cells. The rectangular distance of is
the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and . On permutations of possibly different lengths, . A sequence is Cauchy with respect to if for every there is with for all .
In the order the proof uses them:
Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of is modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.
The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.
The direction "convergent Cauchy" needs a limit permutation for the sequence and the equivalence of density and convergence on (Lemma 5.3), which is not formal: density convergence involves every pattern, a supremum over rectangles. For "Cauchy convergent", completeness of bounded functions under the sup norm gives a uniform limit of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.
The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume " covers only one direction.
unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every and every . is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.
Newton's method converges quadratically near a non-degenerate minimizer, but classical theory says little about its behaviour far from one: the pure Newton step can move uphill, diverge, or be undefined when the Hessian is singular. For decades the global analysis of Newton-type methods consisted of convergence statements without rates. Nesterov and Polyak (Math. Program. 108, 2006) replaced the quadratic model of Newton's method by a cubic-regularized model and proved, for the first time, global worst-case complexity bounds for a second-order method on several problem classes, including classes of non-convex functions.
This mission covers one of these results: on star-convex functions, the method reduces the optimality gap at the rate (Theorem 4 of the paper). Star-convexity is a weakening of convexity that only asks for convexity along segments towards the global minimizers. It includes non-convex functions such as on , and, as the paper notes, it arises in sum-of-squares problems such as .
Timeline.
Let be a closed convex set with nonempty interior, and let be twice differentiable on , with gradient and Hessian . A starting point is fixed, and is assumed large enough to contain the level set in its interior. Assumption 1 is that the Hessian is Lipschitz continuous on with constant :
where the matrix norm is the spectral norm.
For a parameter and a point , the cubic model is
The cubic step is any global minimizer of over (Eq. (2.4)), and is the model value.
Method (3.3) takes parameters . At iteration it finds such that , and sets . The choice always passes the test.
A function is star-convex (Definition 1) if its set of global minimizers is nonempty and, for every , every and every ,
Write for the optimal value, and when is bounded.
Assume is star-convex, is bounded with , and . Then every run of method (3.3) satisfies
The constants are those printed on p. 189. The bound depends on the problem only through and ; the lower parameter and the choice of within are free.
The result. Theorem 4 gives a global function-value rate for a second-order method on a class that contains non-convex functions, with no assumption on the Hessian at the minimizer. The method needs no knowledge of the class: the same iteration (3.3) that yields second-order stationarity rates on general functions yields on star-convex ones. This adaptivity is the paper's main message for Section 4. The analysis also serves as the template for Theorems 5, 8 and 9 of the paper (star-convex with a non-degenerate minimum, and the convex case).
Formalizing it. The theorem has been proved in the paper, and to our knowledge it has not been machine-checked. A complete formalization produces:
These are the pieces needed for the paper's other rates and for later variants (accelerated and adaptive cubic regularization).
The argument has three parts, and each needs some care.
The first is the Taylor bound (2.3) on a convex set , under a Hessian that is Lipschitz only on . The Hessian is given as the derivative of a gradient map, not as a smooth function on all of .
The second is keeping the iterates inside . Lemma 4 and the diameter bound apply only to points of . So the iterates must be shown to stay in the level set, and the points used in the estimate must also lie in .
The third is the passage from the one-step inequality to the explicit constant in (4.2). The one-step inequality is a minimum over of a cubic in . It has two regimes (the unconstrained minimizer lies inside or beyond it), and the recursion for must be carried through without losing the constant or the factor . A generic "sublinear recursion" lemma gives the rate only up to a constant, which is not the printed theorem.
EuclideanSpace ℝ (Fin n) with arbitrary. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every . These are two-sided derivatives, also at boundary points of ; the iterates lie in . The Hessian norm is the operator norm.IsCubicStep). Every statement about it holds for every such minimizer.IsCubicNewtonRun, with a 0-based index.IsStarConvexFn quantifies over , as in display (4.1). It requires and the inequality for every global minimizer.Metric.diam F, with Bornology.IsBounded F as a hypothesis. It is the diameter of itself, not of the level set.Ruling out trivial formalizations. Without the boundedness hypothesis, Metric.diam F is , and the goal would assert outright. The formalization keeps boundedness, the nonemptiness of and the global-minimizer reading of , so that the hypotheses describe the paper's class and not a degenerate one. The hypotheses are satisfiable: for example, on with the closed unit ball, and .
Contributions are welcome at every level: proofs of the milestones, and general-purpose lemmas on Taylor bounds with a Lipschitz Hessian on convex sets. Those lemmas are reusable for missions I, III and IV of this series, which formalize the paper's other rates.
The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements that turns one string into the other. It underlies spelling correction, sequence alignment in computational biology, and file comparison. Wagner and Fischer (J. ACM 21, 1974) computed it for strings of length in time by filling an matrix. Masek and Paterson (J. Comput. System Sci. 20, 1980) lowered this to with a "Four Russians" block method: the matrix is cut into blocks, and the effect of every possible block is tabulated in advance.
The tabulation only pays off if the number of possible blocks is small. The paper guarantees this under two hypotheses: the alphabet is finite, and the edit costs are discrete, that is, all integer multiples of one constant. Its §4 asks whether discreteness can be dropped, and answers no with an explicit example whose costs are , , and . This mission formalizes that example.
Timeline:
Let be an alphabet and the null string. An edit operation is a pair of strings of length at most one other than : a replacement when both are symbols, a deletion when , an insertion when . results from by if and . A cost function assigns a nonnegative real to each edit operation; , , . The edit distance is the minimum of over sequences of edit operations taking to . For fixed strings, , where ; this is the edit matrix. A step is the difference of two horizontally or vertically adjacent entries, or , and the possible steps of are the steps of all edit matrices of all pairs of strings. The cost set is discrete if some has every element of as an integer multiple.
An edit path is a sequence of matrix cells in which each cell increases , or both by one: a deletion of (cost ), an insertion of (cost ), or a replacement of by (cost ). The eccentricity of is .
The example. with
Let . The infinite strings and are and with a written into both, at each even position where , so that and each contain exactly letters . The first is at position . is the minimum cost of an edit path from to through points all of eccentricity at least .
For the example's , and ,
The first part gives at least distinct steps in the edit matrix of and ; the second is the negation of the conclusion of the paper's Lemma 4. The goal fixes no constants and no growth rate beyond "at least one new step per diagonal position".
A further item records that the example satisfies every other condition of the paper: its costs are nonnegative and normalized (), but is not discrete.
The block algorithm precomputes one table entry per block and per pair of initial step vectors, so its preprocessing is polynomial in only when the number of possible steps is bounded independently of the strings. The example shows that without discreteness the steps can grow with even over a three-letter alphabet with nonnegative normalized costs, so the table size becomes of order and the method gives no speedup. It explains why the finite-alphabet, non-discrete case is left open in the paper's conclusion.
The paper's result is proved on paper; no machine-checked version is known to exist, and Mathlib has no edit distance at the pinned revision. The formalization produces exact closed forms for three diagonals of a nontrivial edit matrix with irrational entries, a formal link between edit distance over arbitrary edit sequences and minimum-cost paths, and a verified counterexample to the naive generalization of the algorithm. The sibling mission of the series formalizes the algorithm and Lemma 4.
The central difficulty is Lemma 5: a lower bound on the cost of every path confined to a band of eccentricity, not only the straight diagonal. A path may leave its diagonal, pay for a deletion and an insertion, and travel along another diagonal whose 's may or may not line up. The bound must hold uniformly in , and , and it depends on the floor function and on precise inequalities between and . Checking that the straight diagonals are optimal for small does not suffice: the -densities are chosen so that even and odd diagonals cost almost exactly the same per step, and a periodic placement of 's would let one diagonal eventually undercut another.
Strings are Lists; the infinite strings , are functions read from index , and is the list of their first symbols. An edit operation is a pair of Option values other than . The edit distance and are real infima (sInf) of nonempty sets of nonnegative reals, so they coincide with the paper's minima. has indexing and indexing (the paper's Figure 4 prints across the columns). is . The constraint of applies to every point of the path, endpoints included. Costs use Real.pi itself.
Pinned statements: the paper states Theorem 5 about the running time of Algorithm Y ("Discreteness is a necessary condition for Algorithm Y to run in time on length strings and step sequences"); its proof establishes that the number of distinct steps grows linearly with the string length, which is what the goal states. Running time is not formalized. The §2.3 milestone is stated, as in the paper, for all strings and every nonnegative cost function satisfying the §1.1 normalization ; both standing assumptions are hypotheses. The paper's standing assumption is used only for running times and is omitted.
The example must be the paper's: replacing by a rational, or quantifying over "some" cost function or "some" strings, makes the goal false or empty, and the edit distance must be the minimum over edit sequences, not a recurrence.
Needed infrastructure: edit sequences and their costs, the reduction of edit sequences to edit paths, and bounds on with (Mathlib's irrational_pi and Real.pi_gt_d2). The edit-distance definitions are shared in shape with the sibling mission and are reusable. Proofs of any milestone are welcome.
A buyer and a seller negotiate over one indivisible good. Each knows the good's worth to themselves but not to the other side, so each shades their offer to exploit the other's uncertainty, and some mutually profitable trades fail. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game of simultaneous sealed offers and computed its equilibria in closed form for uniformly distributed values.
That closed-form equilibrium became the reference example of bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade in this setting and showed that, for uniform values, the equilibrium of the sealed-offer game with attains the largest expected gains from trade of any incentive-compatible, individually rational mechanism. The later literature on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the same game and uses the linear equilibrium as its benchmark.
A seller has reservation price and a buyer has reservation price , both in with . Each knows their own value. Each believes the other's value is uniformly distributed on : the distribution functions are on . In Lean this belief is the measure unif v̄, Lebesgue measure conditioned on .
Under the Bargaining Rule, the seller asks and the buyer offers simultaneously. If the good is sold at for a fixed ; if there is no sale. On a sale the seller earns and the buyer ; otherwise both earn zero. The case gives the buyer the right to make a take-it-or-leave-it offer, gives it to the seller, and splits the difference.
An offer strategy maps values to offers: for the seller, for the buyer. Against , a buyer with value who offers earns in expectation
and against a seller with value asking earns . These are buyerProfit and sellerProfit. The pair is an equilibrium (IsEquilibrium) if, for every value in , each player's prescribed offer maximises their expected profit over all real offers.
Write and . If and are measurable and
then is an equilibrium. The statement leaves the no-trade branches free, as the paper does: a seller whose value exceeds every serious bid may ask anything at least , and a buyer whose value is below every serious ask may bid anything at most .
The goal is the conjunction of milestones 2 and 3, by definition of equilibrium. Milestone 1 is the step the paper actually writes down; it records the necessary first-order conditions and does not by itself give the global best-response property.
The result. Example 1(a) is the explicit equilibrium from which the paper derives the probability of trade, , and each party's ex ante profit as a function of (Example 1(b)–(c)). It is the equilibrium shown by Myerson and Satterthwaite to be second-best efficient at , and it is the standard test case against which other double-auction equilibria and mechanisms for bilateral trade are compared.
Formalizing it. The result is proved in the literature but, to our knowledge, has not been machine-checked. The paper itself only observes that the linear branches satisfy the first-order conditions; the global statement (no deviation to any real offer is profitable, including deviations that reach the other side's no-trade types) is left to the reader. A formal proof closes that gap and yields reusable facts about expected profits under uniform beliefs. The two companion missions of this series formalize the paper's Theorem 2 (the linked differential equations in general) and Example 1(b)–(c) (trade probability and expected profits).
First-order conditions do not suffice. A seller can ask below the lowest serious ask and trade with buyers on the free lower branch, whose bids are only bounded above; a buyer can bid above and meet sellers on the free upper branch, whose asks are only bounded below. The best-response inequality must hold for every such deviation and for every admissible choice of the free branches, so it cannot be read off from the linear strategies alone. The expected profit is a piecewise function of the offer, with the pieces determined by where the offer meets the opponent's linear branch and the free branches, and the inequality must be shown on each piece and at the boundaries, uniformly in including the endpoints and , where one of the free ranges is empty.
Values and offers are real numbers; strategies are functions , and their values outside are irrelevant because the beliefs give that set measure zero. Beliefs are the probability measure unif v̄ = volume[|Icc 0 v̄]; expected profits are Bochner integrals against it, written over the opponent's value rather than against an offer density. The value intervals are closed; ties trade; deviations range over all of ; ranges over the closed interval .
The strategies and are assumed measurable. Without this a deviation's expected profit could be the junk value of a non-integrable Bochner integral; with it, all integrands are bounded on the trade event. The inline coefficient of the page is read as , the reading under which the buyer's lowest serious bid equals the seller's lowest serious ask, as in the paper's Figure 1.
The claim is the sufficiency direction only; the paper states that other equilibria exist, and a statement that every equilibrium has the linear form would be false. The canonical linear pair satisfies all hypotheses, so the goal is not vacuous.
Useful infrastructure includes integrals of piecewise-affine functions against the uniform measure on an interval and the distribution function of volume[|Icc 0 v̄]. Contributions welcome: proofs of the milestones, and lemmas computing and in closed form on each piece.
Many optimization problems ask for a subset of a finite ground set that maximizes a function with diminishing returns: the cut of a graph or a directed graph, the value of a facility-location configuration, the entropy of a set of random variables, or a welfare function in combinatorial auctions. These functions are submodular but typically non-monotone: adding elements can decrease the value. Max Cut and Max Directed Cut are the textbook special cases. Unconstrained maximization of a nonnegative non-monotone submodular function is NP-hard, and before Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) no constant-factor approximation was known for general such functions in the value-oracle model.
The paper gives several algorithms. A uniformly random set achieves of the optimum (a separate mission of this series). This mission concerns the paper's first deterministic algorithm: a local search that repeatedly adds or removes a single element while the value improves by a factor larger than , and returns the better of the final set and its complement. The key structural fact behind it, that a local optimum of a submodular function dominates all its subsets and supersets, goes back to Cherenin (1962) and Goldengorin, Tijssen and Tso (1999).
Timeline. Cherenin (1962) and Goldengorin–Tijssen–Tso (1999): local optima dominate comparable sets. Schäffer and Yannakakis (SIAM J. Comput. 1991): finding an exact local optimum of Max Cut is PLS-complete, which is why the algorithm here uses an approximate improvement threshold. Feige–Mirrokni–Vondrák (FOCS 2007; SIAM J. Comput. 2011): the and guarantees of this mission, and for a randomized "smooth" local search. Buchbinder, Feldman, Naor and Schwartz (SIAM J. Comput. 2015): a randomized double-greedy -approximation, which is optimal in the value-oracle model by the lower bound of the same 2011 paper.
Let be a finite ground set with elements. A set function assigns a real number to every . It is submodular (Definition 1.1) if
and symmetric if for all . Throughout the section of the paper formalized here, is nonnegative. The algorithm may query for any (a value oracle). The optimum is .
A set is a local optimum if for every and for every . It is a -approximate local optimum (Definition 3.2) if for and for .
Algorithm LS with parameter and :
In Lean these are Submodular, SymmetricSetFun, OPT, IsLocalOptimum, IsApproxLocalOptimum, lsStep, IsLSRun, IsLSTerminal and lsOutput in NonmonotoneSubmod.LocalSearch.
For nonnegative submodular on a nonempty and , every run of Algorithm LS, with any choice of starting singleton and of improving elements, satisfies:
The last line is the explicit content of the printed bound of oracle calls: it gives steps of at most queries each, and in particular termination.
The result. Theorem 3.4 is the deterministic constant-factor approximation of the paper that first gave guaranteed approximation factors for maximizing general nonnegative submodular functions ("Prior to our work, to the best of our knowledge, no guaranteed approximation factor was known", p. 1135), and the bound for symmetric functions matches the value-oracle lower bound proved in the same paper (so it is optimal for symmetric functions among algorithms using polynomially many queries). Local search with a multiplicative acceptance threshold was subsequently used for constrained non-monotone submodular maximization (matroid and knapsack constraints, Lee–Mirrokni–Nagarajan–Sviridenko 2010).
Formalizing it. The result is proved; to our knowledge neither the theorem nor Lemmas 3.1 and 3.3 has a machine-checked proof. The mission produces a reusable finite model of set functions and single-element local search over Finset, with the algorithm stated as a nondeterministic step relation, so that the guarantee is proved for every tie-breaking rule. The same model is the starting point for formalizing other local-search guarantees.
The natural first idea, to argue from an exact local optimum via Lemma 3.1, does not apply: LS stops at an approximate local optimum, and the error per element must be accumulated along a chain of up to single-element changes between and or . This accumulation is where the nonnegativity of enters (the lemma fails for negative-valued ), and where the factor in the final ratio comes from. The running-time bound requires relating to the best singleton, which uses submodularity on sets of all sizes and breaks down on a one-element ground set. A further bookkeeping difficulty is the algorithm itself: its steps are ordered (removals only when no addition applies), and the termination bridge must use that order.
X : Type with [Fintype X] [DecidableEq X]; subsets are Finset X; is Finset X → ℝ; complements are Sᶜ. is (Fintype.card X : ℝ).∀ S, 0 ≤ f S (standing assumption of §3); Lemma 3.1 and the termination bridge are stated without it, as they need none.Finset.sup'), never a supremum with a default value.S : ℕ → Finset X with S 0 = {v} for any maximum-value singleton v and consecutive sets related by an LS step; the theorems quantify over all runs. Steps use strict inequalities, termination their negation, exactly as printed.Contributions welcome: proofs of the milestones, general lemmas about chains of single-element changes in Finset, and the derivation of the goal from them.
A variational inequality asks for a point of a set at which a vector field points "into" : for every . It is the common form of the first-order optimality conditions of constrained optimization, of complementarity problems, and of equilibrium models in economics and traffic networks. In many of these models the feasible set itself depends on the decision: the admissible actions of one agent are restricted by the current state, as in the impulse-control problems of Bensoussan and Lions that motivated quasi-variational inequalities, where .
D. Chan and J. S. Pang, The generalized quasi-variational inequality problem (Math. Oper. Res. 7 (1982) 211–222), unify the quasi-variational inequality with the generalized (set-valued) variational inequality of Fang and Peterson (JOTA 1982). Their §§3–4 prove existence by fixed-point theorems for set-valued maps; §5 takes a different route and characterizes solutions as fixed points of a composite projection map. Theorem 5.3, the subject of this mission, gives conditions under which that map is a contraction, so that its fixed point exists, is unique, solves the problem, and is computed by plain fixed-point iteration from any starting point. It is the algorithmic result of the paper, and an early instance of the projection methods for strongly monotone quasi-variational inequalities studied since (e.g. Nesterov and Scrimali 2011).
Throughout, carries the Euclidean inner product and norm .
Given point-to-set mappings and of into itself, the generalized quasi-variational inequality problem is to find vectors and with
When is point-to-point, is read as the singleton .
For a set and a point , the projection is the point of nearest to , ; it exists and is unique when is nonempty, closed and convex.
Theorem 5.3 concerns the special structure in which the feasible set moves by translation: fix a nonempty closed convex set and a point-to-point mapping , and put
For a step length and a point-to-point , the projection map is
The mappings and are assumed Lipschitz continuous with constants , (, ) and strongly monotone with constants , (, ).
For each with
the map is a contraction (Lipschitz with a constant independent of the points), it has a fixed point , the point solves , and the iterates converge to from every initial vector . All four conclusions are stated together.
The result. Theorem 5.3 turns an existence question into a computation: under Lipschitz and strong monotonicity assumptions, a quasi-variational inequality with translated feasible sets has exactly one solution reachable by projection iterations, each of which is a projection on the fixed set (a convex quadratic program when is polyhedral). The step-size window it gives is explicit in , so it certifies a convergent method before any iteration is run. The closing remark of the paper (p. 222) reads each step as solving the GQVI under a zero-th order approximation of , the viewpoint behind later splitting methods.
Formalizing it. The result is proved in the paper; the proof is short, but its constants and the equivalence of the two contraction conditions are easy to get wrong. A machine-checked version fixes the exact hypotheses (no sign conditions on the constants, Euclidean geometry), and produces reusable pieces: the translation identity for projections, nonexpansiveness of the Euclidean projection on a closed convex set, and the projection characterization of quasi-variational inequalities (Theorem 5.1).
Banach's fixed-point theorem does the last step; the work is the estimate. The naive bound, projection nonexpansiveness applied directly to , fails because the sets and differ: two projections on different sets are not controlled by the distance of the projected points alone. The translation identity separates the moving part from a projection on the one set , at the cost of the additive term in the constant. The remaining square must be expanded with the inner-product cross terms bounded by the monotonicity constants in the right directions, including the cross term between and . Finally, the condition "bracket " is equivalent to the stated -condition only when , which must be derived from the hypotheses rather than assumed.
EuclideanSpace ℝ (Fin n), with Mathlib's Euclidean norm and inner product; Fin n → ℝ (sup norm) would change every constant. No assumption is made; at all statements hold trivially.proj that returns a junk value only when no nearest point exists; under the hypotheses of every statement using it, the nearest point exists and is unique, so proj is the paper's . Theorem 5.1 is stated relationally (nearest-point predicate IsProj) to avoid junk values altogether.ContractingWith c F with c : ℝ≥0: c < 1 and a Lipschitz bound with that single constant. A constant allowed to depend on the points, or a Lipschitz bound without c < 1, is not a contraction and would trivialize the goal; so would a projection whose junk value is reachable (e.g. with empty), which makes unrelated to the paper's map. The fixed point must be linked to the GQVI and to the iteration from every starting point.Real.sqrt; its radicand is nonnegative under the hypotheses when .ContractingWith.fixedPoint and ContractingWith.tendsto_iterate_fixedPoint (Banach), exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero (projection on convex sets), and the platform theorem VectorSpaceOpt.min_distance_convex_set. A general lemma that the Euclidean nearest-point map of a closed convex set is 1-Lipschitz is reusable well beyond this mission and is welcome as a separate contribution.Quadratic programming, the minimisation of a quadratic function subject to linear inequality constraints, is a basic subproblem of nonlinear optimisation (sequential quadratic programming, trust-region methods) and a model in its own right in portfolio selection, least-squares estimation and control. The classical solution methods are active-set methods: they keep a set of constraints treated as equalities, minimise over the resulting affine set, and then decide which constraint to drop or add (Gill, Murray and Wright, Practical Optimization, 1981; Fletcher, Practical Methods of Optimization, Vol. 2, 1981). Their finite-termination proofs need either a nondegeneracy assumption (linearly independent active constraints) or an anti-cycling rule, because under degeneracy the choice of the constraint to drop, made from Lagrange multiplier estimates, can cycle.
Calamai and Moré (Mathematical Programming 39, 1987) showed that the gradient projection method can take over the step that leaves a working set. Their Algorithm 6.1 alternates two kinds of step: an arbitrary non-increasing step that adds constraints to the working set until the equality-constrained subproblem is solved, and a single projected-gradient step once it is solved. Theorem 6.2 states that this algorithm terminates at a stationary point for every quadratic that is bounded below on the feasible polyhedron, with no nondegeneracy assumption and no anti-cycling rule. The same paper's Sections 2–4 (the subject of the first two missions of this series) supply the properties of the gradient projection step that the argument uses.
Timeline of the ingredients:
Let be a finite-dimensional real inner product space (the paper's with a general inner product). The feasible set is a polyhedron
with active set . The objective is a quadratic function with self-adjoint but not necessarily positive semidefinite, so may be nonconvex. Its gradient is taken with respect to the inner product of .
The projection into is , and a point is stationary if for every .
A gradient projection step from is with satisfying the sufficient decrease condition (2.1) with a constant , the condition (2.2) that or for some at which the decrease test (2.3) with constant fails, and the upper bound (3.2).
A working set is a set ; problem (6.2) is , over an affine set that ignores the inequality constraints outside .
Algorithm 6.1 produces iterates and working sets from :
For every quadratic bounded below on , all constants , , , and every run of Algorithm 6.1,
The theorem makes no assumption on the boundedness of the iterates and none on the linear independence of the constraints.
Theorem 6.2 separates the two roles an active-set method plays: solving equality-constrained subproblems, for which any method that does not increase may be used, and choosing the next working set, which the gradient projection step does. The consequence is a finitely terminating quadratic programming algorithm for nonconvex quadratics that needs neither nondegeneracy nor an anti-cycling rule, and a template for large-scale bound-constrained and linearly constrained solvers that combine projection steps with subspace minimisation.
The result is proved in the paper and is classical; no machine-checked version is known. A formalization produces a checked finite-termination theorem for an active-set method on degenerate problems, together with reusable pieces: the projection onto a polyhedron as a total function with its variational inequality, the descent estimate of a projected step, and a predicate describing active-set runs with working sets, which other active-set algorithms can reuse.
The obvious argument — each step decreases and there are finitely many working sets — fails on two counts. First, step (b) only guarantees , so values alone do not rule out infinitely many iterations; the nesting of working sets and the final clause of step (b) are what bound consecutive (b)-steps. Second, a gradient projection step taken at a solution of (6.2) can in principle leave unchanged, and nothing in the algorithm's rules says directly that it makes progress; that it does so at every non-stationary iterate is a property of the projection and of the step conditions (2.1)–(2.2), not of the algorithm. A further point is that the minimum of (6.2) is taken over an affine set, not over , and the link between the value at a step-(a) iterate and later iterates runs through the requirement .
The space is a finite-dimensional real inner product space E; is Mathlib's gradient. Constraints are indexed by Fin m, working and active sets are Finset (Fin m), and a run is a predicate IsAlgorithm61Run on three sequences , , indexed from . The run does not stop by itself; "the algorithm terminates at a stationary iterate" is rendered as the existence of an index with stationary. The projection is argmin made total by a junk value that is unreachable when is nonempty, closed and convex. The paper's "" between working sets is inclusion. A quadratic function is with symmetric and no definiteness assumption.
A trivializing formalization — a run predicate that forces to be stationary, or that no sequence satisfies — would make the goal empty; the step rules here are the paper's verbatim, and a run on with starting at the non-stationary point satisfies the predicate. Replacing step (a) by "any step that strictly decreases " would assume the central fact and is not acceptable.
A complete development needs: the variational inequality of the projection (Lemma 2.1(a)), the descent estimate (2.5), the characterisation of stationary points as fixed points of the projected step, and a finiteness argument over the finitely many subsets of Fin m. Proofs of the milestones, of these auxiliary facts, and of the goal are all welcome.
Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?
Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.
All graphs are finite, undirected and loopless. A stable set of a graph is a set of vertices no two of which are adjacent. Write for the set of incidence vectors of stable sets (the zero–one vectors with stable), and
for the stable set polytope. A finite system of linear inequalities in the variables is a defining linear system of when its set of solutions is exactly .
Let and be graphs with , and let . The graph obtained from by substituting for has vertex set . Its edges are the edges of , the edges of , and every edge joining a vertex of to a neighbour of in . In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.
For let
be a defining linear system of , with finite index sets and real coefficients, and put for . Then
is a defining linear system of . The statement fixes no particular system for or : any defining systems of the two pieces produce one for , with rows besides nonnegativity.
where and are the maxima of over with and respectively, and is the maximum of over .
Theorem 5.1 gives an explicit construction: from a polyhedral description of and it writes one of , row by row, with no loss. Specialized to it gives Corollary 5.2 of the paper, a defining linear system for the join ; applied repeatedly it gives defining systems for lexicographic products, and applied with it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of , so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.
The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of , and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.
That every point of satisfies (5.1) is a short case check on stable sets of . The difficulty is the reverse inclusion: that no point outside satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of and a point of , fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part in place of is what keeps the system valid when .
The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.
SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in .IsIndepSet); is convexHull ℝ (S G), never the solution set of an inequality system.a : J → V → ℝ, b : J → ℝ. The nonnegativity rows are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with .[Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of ; with , and , (5.1) is just and the theorem fails. The validity milestone does not need it.sSup over a finite set that always contains the zero vector or the incidence vector of , so no junk value of sSup can occur.Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.
Minimizing a smooth function subject to linear inequality constraints is the core subproblem of much of nonlinear optimization: bound-constrained problems, quadratic programs, and the subproblems of sequential quadratic programming and augmented Lagrangian methods all have this form. Methods for these problems are usually built from two parts, one that decides which constraints hold with equality at the solution and one that solves the resulting equality-constrained problem quickly. The first part only pays off if the decision stabilizes after finitely many iterations; otherwise the fast local method never gets to run.
Calamai and Moré (Math. Programming 39, 1987) proved that this stabilization is a property of the limit point, not of the algorithm. Any feasible sequence that converges and whose projected gradients tend to zero identifies the active constraints of a nondegenerate limit in finitely many steps. This is the result that later active-set and gradient-projection methods for bound-constrained and linearly constrained problems invoke to justify switching to a fast local phase.
Timeline.
Let be a finite-dimensional real inner product space (the paper's with a general inner product) and let be continuously differentiable on the feasible set, with gradient taken with respect to the inner product of .
The feasible set is a polyhedral set
for constraint normals and scalars . The active set at is .
A direction is feasible at if for all sufficiently small . The tangent cone is the closure of the set of feasible directions. The projected gradient is the point of closest to :
A point is stationary if for all . It is a Kuhn–Tucker point if with . It is nondegenerate if the active normals are linearly independent and the multipliers satisfy for every .
A Lagrange multiplier estimate is a map . It defines the binding set . The estimate is consistent if whenever , the point is a nondegenerate Kuhn–Tucker point, and for every .
Let be an arbitrary sequence in converging to . If and is nondegenerate, then
The sequence need not come from any particular algorithm. The goal asserts eventual equality of the index sets, not inclusion.
The result. Theorem 4.1 separates identification from convergence. Any method that keeps its iterates feasible and drives the projected gradient to zero inherits finite identification, whatever its step-size rule or search direction. After identification the constrained problem is locally an unconstrained problem on the affine subspace , so Newton-type or conjugate-gradient methods can take over. Theorem 4.2 carries the same conclusion to methods that drop constraints according to the signs of multiplier estimates. The companion missions of this series use the result: the gradient projection method drives the projected gradients to zero (mission I), and a gradient projection algorithm for quadratic programs terminates finitely (mission III).
Formalizing it. The theorems are proved in the paper. No machine-checked version of the projected gradient, of tangent cones of polyhedra with their active-set description, or of finite active-set identification is known to exist. Formalization adds a reusable account of tangent cones and polar cones of polyhedral sets and of the equivalence between stationarity and the Kuhn–Tucker conditions for linear constraints, together with a method-independent identification theorem stated at the level of generality of the paper.
Two different limits are involved. Convergence is enough to show that no inactive constraint of is active at for large . The hard direction is the converse: a constraint active at might be inactive at infinitely many , approached from the interior. Convergence of the points alone cannot rule this out. The projected gradient is also not continuous, because the tangent cone changes when a new constraint becomes active. So the hypothesis cannot be passed to the limit naively. Both nondegeneracy conditions matter: without linear independence, or with a zero multiplier, the statement fails.
The space is a real inner product space E with [FiniteDimensional ℝ E], and is Mathlib's gradient. "Continuously differentiable on " means DifferentiableAt ℝ f x for every together with ContinuousOn (gradient f) Ω. The constraints are indexed by Fin m. is polyhedron c δ, and is activeSet c δ x : Finset (Fin m).
The tangent cone is defined as the closure of the feasible directions, not by the polyhedral formula, which is a milestone. The projected gradient is the nearest point of to , chosen by a choice function that returns only when no nearest point exists. That never happens at a point of a polyhedral set.
Nondegeneracy is bundled as IsNondegenerate c δ f x*: , the family is linearly independent, and positive multipliers represent . "For all sufficiently large " is ∀ᶠ k in Filter.atTop.
In Theorem 4.2 the paper leaves one condition implicit: the estimate at must be the Kuhn–Tucker multiplier vector, . Without it the statement is false, so it is an explicit hypothesis. Consistency is required only along feasible sequences and only in the coordinates .
A formalization that assumes , assumes the active sets are eventually constant, weakens nondegeneracy to nonnegative multipliers, or concludes only inclusion is not the paper's theorem and does not satisfy this mission.
Needed infrastructure: tangent cones of convex sets, the Moreau decomposition into a closed convex cone and its polar, Farkas' lemma in a general inner product space, and orthogonal projections onto subspaces spanned by linearly independent vectors. The polyhedral tangent-cone and Kuhn–Tucker results are reusable beyond this mission. Proofs of any milestone are welcome, as are auxiliary lemmas on polyhedral cones.