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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
Ride-hailing, car-sharing and bike-sharing platforms price trips whose execution moves the resource itself: a car that takes a passenger from the suburbs to the airport is no longer available in the suburbs. Each price therefore sets both the revenue of the current request and the future spatial distribution of the fleet. Choosing prices to maximise long-run revenue is a Markov decision problem whose state, the number of resources at each location, has a number of configurations exponential in the number of locations. Exact dynamic programming is impossible at the scale of a city.
Balseiro, Brown and Chen (SSRN 3313737, version of May 23, 2020; published in Management Science, doi:10.1287/mnsc.2020.3735) study hub-and-spoke networks and propose a Lagrangian policy. The capacity constraint coupling the locations is relaxed with a dual variable, the relaxation separates into one small problem per spoke, and the per-spoke solutions are implemented in the real system. Earlier work on this model (Waserhole and Jost, 2016; Banerjee, Freund and Lykouris, 2016) uses fluid relaxations that lead to static prices, depending on the origin and destination but not on the resource levels. These are within a factor of the fluid bound, hence asymptotically optimal when the number of resources grows faster than the number of locations . When and grow at the same rate, which is the regime of a large city with few vehicles per area, no static policy is asymptotically optimal (the paper's Example 5.1). The Lagrangian policy is a dynamic, state-dependent policy that is computable and asymptotically optimal in that regime.
A hub (location ) and spokes share resources. In each period one request arrives: it asks to relocate a resource from spoke to the hub, type , with probability , or from the hub to spoke , type , with probability ; these probabilities sum to one and are independent across periods. The provider picks a demand level , equivalently a price. The request is fulfilled with probability if its origin holds a resource and is lost otherwise; the expected revenue is . Assumption 2.1: each is strictly concave on , , , , and the maximiser is interior.
The state is the vector of spoke levels , the hub holding . The optimal average revenue (problem (1)) is the supremum, over non-anticipative feasible policies, of the long-run average expected revenue.
Penalising the spoke resources with a dual variable yields, for each spoke, the spoke problem (6): maximise over a distribution on and controls satisfying the birth–death balance equations . Its value is . The relaxation value is (4), the Lagrangian bound is (9), and the perturbed dual is (11), with optimal solution . The Lagrangian policy (Definition 3.1) applies the controls of optimal solutions of (6) at , spoke by spoke, and drops a hub request when the hub is empty. is its average revenue and the stationary probability that the hub is empty. In the relaxed system the hub may go negative; there the spokes are independent with laws .
Under Assumption 4.1 ( for every spoke, independent of ) and with , for ,
and with ,
The milestones follow the paper's proof. The spoke problem solves the spoke Bellman equation (Proposition 3.2), the relaxation's value is independent of the initial state, equals and bounds (Proposition 3.1), and the controls are monotone (Proposition 3.3). The relaxed and original chains have stationary laws and a unique (Corollaries B.10, B.11). The perturbation costs at most (Lemma 4.2), continuation-value differences are at most (Lemma A.10), and the relaxed–original gap is controlled by hub depletion (Lemma 4.3), giving Theorem 4.1,
Stochastic dominance between the two systems (Lemma 4.4) gives (Corollary 4.5). The spoke laws are log-concave (Proposition B.9), log-concave generating functions are dominated by geometric ones (Lemma A.14), a concentration bound for sums of log-concave variables follows (Lemma A.12), and the relaxed depletion probability is at most (Proposition 4.6).
The result. A policy computed from independent problems of size loses only per period against the optimal policy of a problem with exponentially many states. No static policy achieves a vanishing gap. Theorem 4.1 also yields a practical certificate: is a computable upper bound, and the gap is governed by one observable quantity, the hub-depletion probability. The same structure extends to several hubs (the paper's Theorem 6.1).
Formalizing it. The result is proved in the paper; nothing here is open, and no part of it has been machine-checked. A formal proof would check a chain that combines average-reward dynamic programming, convex duality and sensitivity analysis, a coupling argument between two Markov chains, and a concentration inequality for log-concave variables. Several of these steps are stated in the paper with brief or cited arguments (the Bellman equation of the spoke problem, the class structure of the chains, Keilson's factorial-moment inequality behind Lemma A.14).
The natural first idea is to use the Lagrangian policy at the optimal dual of (9). At the relaxation keeps zero resources in the hub in expectation, so the real hub is empty a constant fraction of the time and every hub request lost there costs a constant. The perturbation is what makes the argument work. The key step is then to compare the relaxed system, where spokes are independent and the hub may go negative, with the original system, where the hub constraint couples all spokes. This needs both a loss bound per depletion event (Lemma A.10, which rests on the monotonicity of Proposition 3.3) and a pathwise coupling (Lemma 4.4). A Chebyshev bound on the hub level gives only a polynomial rate. The exponential rate requires the log-concavity of every spoke law and a geometric domination of its generating function.
limsup of its time average. Stationary distributions are finite probability vectors, via the published definition MarkovChain.IsStationary. Sums of independent ℕ-valued variables are iterated convolutions.Fin n ⊕ Fin n, spoke levels Fin (m+1), the hub level is , and the original chain lives on .Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first positions, with random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position also sees positions ) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.
The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.
There are items. Item has a price and an MNL preference weight ; write and, for an assortment ,
the expected revenue of offering to an MNL customer with a no-purchase option of weight . An assignment is a bijection from positions to items; is the set of items in positions , , and with position weights the objective is
The algorithm fixes an accuracy and a guessed position . A sequence of dynamic-programming actions consists of events and pairs of item sets (a sub-assortment and a super-assortment), starting from , and ending at , . Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness , the accuracy bounds and the same for , a cardinality constraint linking sets to events, and three growth conditions on the proxies
depending on the position of relative to . With the last index whose event is at most , the actions are rounded into blocks of new items (from before , from after), and the rounded assignment lists the blocks in order, each by non-increasing price. The block boundaries are , and are the position intervals between consecutive boundaries, split at .
For every , every feasible action sequence and every rounded assignment ,
with . This is inequality (15) of the paper combined with (16), in the proof of Lemma 5.4.
The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.
The remaining half of the paper's argument is not true as printed. Lemma 5.4, , and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with , , , and , no feasible action sequence can place item 2 first, and every rounded assignment earns at most against an optimum of . A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.
The rounding discards items. Before , block keeps only the part of the sub-assortment that is new with respect to , so the prefix of can carry less -mass than . A loss bounded by the per-step accuracy would accumulate over up to steps; Lemma 5.2's constant is independent of , and holds only because the growth constraint forces to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.
Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position to the item at position . A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention , and . Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by , non-increasing prices within a block, ties in any order.
Conventions and additions relative to the page:
Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance (, ) satisfying all hypotheses at once.
The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.
Assortment optimization asks a retailer which subset of products to offer so as to maximize expected revenue, given a model of how customers choose among what is offered. A widely used class of choice models in operations management describes customers by ranked preference lists: each customer type buys the highest-ranked product on offer, or nothing (Farias, Jagabathula & Shah 2013). These nonparametric models fit sales data well, but optimizing over them is hard: even when all customer types share one ranking and differ only in which products they are willing to consider, the problem is NP-hard to approximate within a factor (Aouad, Farias, Levi & Segev 2018).
Aouad, Farias and Levi (Management Science 2021) study consider-then-choose models, a behavioural refinement from marketing in which a customer first screens products into a consideration set and then picks her favourite among the offered products in that set. Their main algorithmic device is a dynamic program whose number of subproblems they bound by structural properties of the consideration sets. This mission formalizes the first and most general such bound, for a single common ranking, together with the lemmas it rests on. Earlier exact algorithms for special cases of ranking-based models are due to Honhon, Jonnalagedda & Pan (2012).
There are products with prices , and customer types . Type has a consideration set and occurs with probability , where is a probability vector. All types rank products by the same permutation, and products are numbered in that order: product is the most preferred. If assortment is offered, type buys the smallest-index product of , giving revenue
For and the subproblem value is
and is the original problem. The bipartite graph has the products and types as vertices and an edge when ; is its subgraph induced on , and is a connected component of when induces a connected subgraph and no edge of leaves it. For a product , .
The dynamic program processes products in preference order. Its state space is generated as follows: the components of are states; from a state with , the components of (product stocked) and of (product not stocked) are states. Only components with at least one product and at least one type are states. Finally,
together with its state-space consequence: if then . The bound holds for every family of consideration sets; prices and type probabilities do not enter.
over the components of the two residual graphs. 3. Claim 1 (p. 15): if two states have equal and , then . 4. Lemma 2 (Central Lemma) (p. 15): is injective on , so .
The result. A naive dynamic program over all pairs has states. Theorem 1 shows that the states actually generated are at most , so the algorithm, which spends operations per state, runs in time quadratic in when the number of customer types is constant and polynomial when . This identifies a tractable regime for a problem that is inapproximable in general. Lemma 2 is the paper's main counting tool: the same injection yields its later polynomial bounds for structured consideration sets (consideration sets of bounded diameter, induced intervals, laminar and -disjunctive families), which are natural follow-up missions on top of this one.
Formalizing it. The results are proved in the paper; none is formalized. The mission produces a machine-checked model of the consider-then-choose problem under a unique ranking, of its graph decomposition, and of the inductively generated state space, plus proofs of the decomposition lemma, the recursion, and the counting bound. The proof of Lemma 2 in the paper is short and relies on invariants of the generated states stated in passing; a formal proof has to establish them for every state the recursion produces.
The upper bound is not a count of subsets of products: the map is not injective on , and different states can share their product sets. The bound likewise is not a count of pairs for arbitrary connected subgraphs: for the family of all connected pairs the count exceeds both bounds (when every , all nonempty pairs are connected). The bounds hold only because of how the recursion generates states, processing products in the common preference order, and the injectivity of has to be derived from properties of that generation process (which types survive, which products remain) rather than from the definition of a state alone. Claim 1, proved in the paper's appendix, is where this history argument happens.
Fin N and types Fin K. The order on Fin N is the common ranking, so the paper's product is 0 : Fin N, and is the set of indices ≤ S.min' h, including itself. Prices and type probabilities are real; the standing assumption that is a probability vector is defined but not needed by any statement, since Lemma 1 and recursion (1) hold for all real data and the state space depends on the consideration sets only.SimpleGraph.Connected of the subgraph of the bipartite graph induced on ; a component is a connected, closed vertex set. In Lemma 1 and recursion (1) the sums run over all components, including isolated products and isolated types, which contribute .Set.ncard of a subset of a finite type. States are nontrivial components (at least one product and one type). This is the paper's own setting: the proof of Lemma 2 uses that every state has an edge, and on isolated products is not injective.Page numbers are those of the accepted manuscript: page of the body is PDF page of the deposited file, and page ec of the e-companion is PDF page .
Large-scale learning problems, such as empirical risk minimization over millions of samples, are solved in practice by stochastic gradient descent (SGD) run on many processors at once. In a master–worker system, or in a multi-processor system with shared memory, a worker reads the current parameter, computes a stochastic gradient and writes its update back. Other workers update the parameter in the meantime, so by the time a gradient is applied it is stale: it was evaluated at an older iterate. In heterogeneous clusters these delays are not bounded in any useful sense, and they can grow with the run.
The classical analyses of asynchronous gradient methods (Bertsekas and Tsitsiklis, Parallel and Distributed Computation, Prentice Hall 1989, reprinted by Athena Scientific 1997) and of asynchronous SGD for machine learning (Agarwal and Duchi, NeurIPS 2011; Recht et al., Hogwild!, NeurIPS 2011; Lian et al., NeurIPS 2015) assume bounded delays. Zhou, Mertikopoulos, Bambos, Glynn and Ye (arXiv:2107.02919, Mathematics of Operations Research, 2022) show that the delays may grow without bound, polynomially in the iteration count, as long as the step size shrinks to match. This mission formalizes their first main result, Theorem 1, on general nonconvex objectives.
Let be a probability space and a random function. The objective is
to be minimized over . Write for the gradient of in .
Assumption 1 asks that be differentiable for -almost every , that the stochastic gradient have bounded second moment, , and that its mean be -Lipschitz.
Distributed asynchronous SGD (DASGD, Algorithm 3 of the paper) starts at and updates
where are step sizes, is an i.i.d. sequence with law , and is the iteration at which the gradient applied at step was requested. Its delay is .
Assumption 2 couples delays and step sizes. It requires one of four regimes:
If Assumptions 1 and 2 hold and , then
The goal covers all four regimes at once, through the disjunction in Assumption 2. It fixes no constant: , and the regime's parameters are arbitrary.
The result. For a general nonconvex smooth objective, convergence to a minimizer cannot be expected. The standard guarantee is that the gradient vanishes, and Theorem 1 gives it in mean square, which also implies convergence in probability of to zero. The theorem shows that asynchronous SGD stays stable under delays that grow without bound, and it identifies the price: each step up in delay growth costs a logarithmic factor in the step size. A step size of order is, up to a factor, sufficient for every polynomial delay process. The guarantee does not depend on whether the architecture is master–worker or shared-memory, since only enters.
Formalizing it. The paper proves the result, but no machine-checked version of any asynchronous or delayed SGD guarantee exists on Prove2Me or in Mathlib. A formal proof would check the step most prone to error in such analyses: the conditioning that makes a stale stochastic gradient unbiased given the past. The page's own chain before (B.5) has a constant slip ( where belongs), which the printed (B.5) absorbs. The delay-sum estimates (B.8)–(B.10) are asymptotic computations with logarithms, and the paper states them with "". The reusable parts are the differentiation-under-the-integral lemma (Remark 1) and the series lemma A.4.
Without delays, the descent inequality telescopes directly: the cross term has zero conditional mean. With delays, the gradient is unbiased for , not for . The discrepancy has to be paid for out of the step sizes accumulated over the delay window. When the window grows polynomially, it is a sum over polynomially many past steps, and finiteness of the total penalty depends on the precise step-size law. A cruder bound that ignores the logarithmic factors fails in regimes 3 and 4.
A second obstacle is that a finite weighted sum gives only a . The paper's own counterexamples (p. 10) show that it does not imply convergence. The increment bound of Lemma 2 is what closes the gap.
EuclideanSpace ℝ (Fin d), and is Mathlib's gradient. gradient returns at points of non-differentiability, so the goal also asserts that is differentiable.A Lean integral of a non-integrable function is , and gradient is where is not differentiable. Those conjuncts are there so that the goal cannot be proved through either junk value. The goal is also stated for all four regimes, with the delay inside the recursion, so it is not the classical bounded-delay theorem.
A complete development needs:
Contributions of the real-analysis milestones (Lemma A.4, the delay sums) are welcome independently of the probabilistic ones.
In quantum mechanics an observable is a self-adjoint operator, not just a symmetric one. A differential expression such as on an interval or a half-line first defines a symmetric operator on smooth functions with compact support, and this operator usually has many self-adjoint extensions or none. Each extension is a different physical theory, with its own spectrum and dynamics, and choosing one amounts to choosing boundary conditions. Voronov, Gitman and Tyutin (arXiv:quant-ph/0603187) give a self-contained account of this problem written for physicists. Its abstract result is a description of all self-adjoint extensions that does not require computing the deficient subspaces.
Timeline. von Neumann (1929–30) classified the self-adjoint extensions of a closed symmetric operator through isometries between its deficient subspaces. The classical treatments are Akhiezer–Glazman and Naimark (Linear Differential Operators), and the Cayley-transform form is in Teschl's Mathematical Methods in Quantum Mechanics (2009), Theorem 2.26. Voronov, Gitman and Tyutin (2006) restate the finite-index case as a restriction of the adjoint by asymmetry-form conditions (their Theorem 3, (35)). They then remove the deficient subspaces from the description altogether (Theorem 15). For differential operators this gives self-adjoint boundary conditions in terms of boundary forms (Theorem 16).
Let be a complex Hilbert space whose inner product is linear in the second argument. Let be a linear operator with domain . It is symmetric if is dense and for all . It then has an adjoint extending it and a closure with domain , and . An operator is self-adjoint if , domains included.
The deficient subspaces are and . The deficiency indices are .
The asymmetry form of the adjoint is the sesquilinear form on
It vanishes identically exactly when is symmetric.
Vectors are linearly independent modulo if forces . Given such vectors, denotes the restriction of to their joint -annihilator:
Assume with . Then
Both inclusions are part of the goal: every self-adjoint extension arises from such a family, and every such family gives a self-adjoint extension.
The result. Theorem 15 lists all self-adjoint extensions of as solutions of linear conditions on . The vectors can be any vectors of the adjoint's domain satisfying two checkable conditions. For a differential operator, reduces to a boundary form , and Theorem 16 of the paper turns Theorem 15 into a recipe for self-adjoint boundary conditions that never solves . In von Neumann's parametrization that equation must be solved, and doing so is often the hardest part of a concrete calculation. The price is redundancy: families related by a nonsingular matrix give the same extension.
Formalizing it. The mathematics is known: von Neumann's theory is classical and Theorem 15 is proved on pp. 65–68. The Prove2Me platform has Teschl's Cayley-transform version of the existence criterion as a machine-checked proof. To our knowledge, the first von Neumann formula for LinearPMap, the asymmetry-form description of the closure, and the unitary-matrix parametrization are not formalized in Mathlib or on the platform. This mission produces those statements, together with Theorem 15 itself.
The forward direction rests on the unitary parametrization of Theorem 3, which in turn rests on the direct-sum decomposition of . Each of these steps requires working with rather than , because need not be closed. The converse is the substantial part. Linear independence modulo and isotropy are conditions on the as whole vectors. They say nothing directly about the deficient components, and relating an arbitrary admissible family to the deficient-subspace description of Theorem 3 is where the work lies. A count of dimensions alone does not give self-adjointness. Showing that a restriction of is symmetric is easy; showing that its adjoint is no larger than itself is not.
InnerProductSpace ℂ H, CompleteSpace H), and operators are LinearPMaps H →ₗ.[ℂ] H. The adjoint, closure, extension order and self-adjointness are Mathlib's f.adjoint, f.closure, f ≤ g and IsSelfAdjoint g (g† = g). Mathlib's inner product is conjugate-linear in the first slot, as in the paper.TeschlQM.Shared.IsSymmetric, which includes density. The initial operator is not assumed closed.kerAdd f.adjoint (-I) and kerAdd f.adjoint I , from the published TeschlQM.SelfAdjoint.addScalar. The index hypotheses are Module.finrank … = m with 0 < m, which forces both indices to be finite. Theorem 1 and (18)–(19) keep a general with , as the paper does.asymForm) is defined only on f.adjoint.domain. Families are indexed by Fin m. Linear independence is modulo f.closure.domain. The operator (144) is cutOut f w, which is f.adjoint restricted to the annihilator.finrank = 0, so that hypothesis is kept.LinearPMaps; closures of symmetric operators; the identity ; and the unitary-matrix parametrization. These are reusable beyond this mission, for example for Sturm–Liouville realizations and Theorem 16 of the paper. Contributions of any of them are welcome, as are proofs routed through the published Cayley-transform results.Double auctions match buy and sell orders at a common price. Stock exchanges, commodity markets and electricity markets use them at their opening and closing auctions and to trade multi-asset portfolios. Economists have long asked how efficient the resulting allocations are. Laboratory work starting with Smith (1962) found that repeated double auctions with few traders reach competitive outcomes quickly (Smith 1962). Since then the phenomenon has been documented in many experimental studies, but it had remained largely unexplained by theory (Pennanen, §1).
Pennanen (arXiv:2001.02071v2, Mathematics of Operations Research 2022) takes agents who bid their indifference prices in a multi-asset double auction, and shows that repeating the auction drives the economy to an efficient allocation. The total surplus left on the table decays like .
A finite nonempty set of agents trades a finite set of assets. Agent holds a portfolio , and an allocation is . Short positions are allowed and there is no free disposal. Agent has a utility with effective domain . All prices are quoted in a numeraire portfolio , for example cash.
Assumption 1 holds throughout: each is upper semicontinuous and concave (its hypograph is convex), and for and .
At the endowment , agent bids the indifference price
the most the agent would pay for without losing utility. The auctioneer solves the market clearing problem
whose optimum value is the total consumer surplus available at . A market clearing price is a vector that is a supergradient of every at a solution . Agent then receives and pays units of . An allocation with is a double auction equilibrium.
In the repeated auction the agents re-bid from their new positions:
where and clear the -th auction, whose indifference prices are built from .
Two further conditions are used. Assumption 3: no nonzero with has every a direction of recession of . Assumption 5: for every there is with on the ball . Assumption 4, which is needed only for Pareto efficiency, says that an agent who is not at the lowest possible utility can give away a little of and stay in .
Under Assumptions 1, 3 and 5:
The constants are those of Assumption 5 at one radius that is large enough for the whole sequence. The statement holds for every admissible choice of them.
The milestones are the results that the proof of Theorem 16 uses, in attack order:
Theorem 16 is a welfare theorem for a mechanism that is actually used. Agents bid myopically, nobody computes a Walrasian equilibrium, and the allocation still becomes efficient. The result also gives a convergence rate. Together with Theorem 11 it identifies the limits of the mechanism with the Pareto allocations, so studying where repeated auctions end up comes down to studying Pareto efficiency.
The theorem is proved in the paper. No part of it, and none of its model, has a machine-checked proof. The formalization would check an argument that runs entirely in extended-real convex analysis, with utilities that may take the value , such as Cobb–Douglas utilities on the positive orthant. It would also settle points the printed proof leaves implicit. One is the radius at which Assumption 5 is applied. Another is that the endowments must lie in the utility domains, which some lemmas need explicitly.
The obvious route bounds each agent's gain per auction by times the agent's surplus and then telescopes. That route needs a single constant valid along the whole sequence, which in turn needs the iterates and the surpluses to be bounded in advance. Boundedness is the step a newcomer cannot get from compactness or from Lipschitz estimates. It comes from recession analysis of the superlevel sets of upper semicontinuous concave extended-real functions, through Rockafellar's characterization of bounded closed convex sets. Mathlib has none of this.
A second difficulty is attainment. Several steps use , so the supremum defining must be attained. Attainment comes from upper semicontinuity, not from the definition. The cluster-point claims also need upper semicontinuity, in order to pass the monotone utilities to the limit.
Utilities are functions (J → ℝ) → EReal, with I, J finite types and I nonempty. Concavity is convexity of the real hypograph, which is Rockafellar's definition. Mathlib's ConcaveOn does not apply because EReal is not a module. The indifference price and are EReal suprema. A supergradient requires to be finite, which is Rockafellar's convention. Without that requirement a bid of would satisfy (4) vacuously and the goal would be trivial.
is encoded as the property that is nondecreasing for every , which the paper quotes from Rockafellar's Theorem 8.6. is the closed sup-norm ball. The paper fixes no norm, and Assumptions 2 and 5 are unaffected by the choice.
The sequence in Theorem 16 is any sequence the mechanism generates: purchases and prices satisfying the market clearing conditions at the current allocation. Existence of solutions and prices is not part of the goal. The rate is stated with the real values of and . Proving these values finite is part of the proof, and nothing in the statement assumes it.
The goal must not be trivialized. Bounded iterates, finite utilities along the sequence and are conclusions, not hypotheses. The constants are universally quantified at a radius whose existence is claimed, not chosen existentially.
The following additions are disclosed on the items concerned. Lemma 2, the boundedness milestone and the first half of Theorem 11 assume , without which they fail. Lemma 9's solution correspondence assumes a finite optimum value.
The development needs extended-real concave analysis: upper semicontinuous concave functions, their recession cones, and attainment of suprema. This layer is reusable beyond this mission. Contributions are welcome on any milestone. The recession-cone boundedness and Lemma 9 are good entry points.
A trader who quotes an exotic option written on several underlying assets (a basket call, a spread option, a best-of option) needs a price range that does not rest on a particular stochastic model. What is observed in the market is a finite set of liquid derivatives (vanilla calls and puts on each asset, and possibly some traded basket options), each with a bid price and an ask price. A model-free price bound for the exotic payoff is the range of prices consistent with these quotes and with the absence of arbitrage. Its upper end can be computed in two ways: as the cheapest static portfolio in the traded derivatives that dominates the payoff in every state of the world, or as the largest expected payoff over all probability measures that price the traded derivatives inside their bid–ask spreads.
The equality of these two numbers is a superhedging duality. For a single asset with exact (zero-spread) prices it goes back to the model-independent pricing literature of Hobson and others; Bouchard and Nutz (2015) proved a one-period duality and a fundamental theorem in a nondominated framework without spreads. Neufeld, Papapantoleon and Xiang (arXiv:2006.14288, Management Science 2023) extend the one-period result to a market where the derivatives are traded with bid–ask spreads and the payoffs are arbitrary Borel functions on a Polish state space, and then use the minimisation side to compute bounds exactly by cutting-plane algorithms.
Let be a Polish space with its Borel -algebra, and let be the set of all Borel probability measures on ; there is no reference measure. Fix traded derivatives with Borel payoffs , collected in , with bid prices and ask prices , .
A static position pays and costs
since long positions are bought at the ask and short positions sold at the bid. The cost is sublinear, not linear.
No-arbitrage (Assumption 2.1): for every , if for every , then for every .
For a Borel payoff , the superhedging price is
and the set of pricing measures is
The proofs also use the box and the set of payoffs super-replicable at zero cost, where is the set of nonnegative Borel functions.
Under Assumption 2.1, for every Borel ,
The identity is stated in and covers the case of payoffs that no static portfolio dominates.
In the order of the proof in Appendix EC.4:
The duality turns a maximisation over an infinite-dimensional set of probability measures into a minimisation over , a finite-dimensional problem with infinitely many constraints. This is what makes the exact computation of model-free bounds in the paper possible: for continuous piecewise affine payoffs, the minimisation side is solved by cutting-plane algorithms whose subproblems are linear and mixed-integer programs. Parts (i) and (ii) say that the upper bound is never under no-arbitrage and that it is realised by an actual static hedge. Lemma EC.4.2 also yields the paper's fundamental theorem (Theorem 2.3), which characterises no-arbitrage by the existence of pricing measures dominating any given probability measure.
The result is proved in the paper; it has no machine-checked proof. A formalization would also give a checked version of the closedness lemma for cones of super-replicable payoffs, which is the step most often adapted from Bouchard–Nutz in later work on one-period robust pricing, and a reusable statement of the extended-valued duality with an explicit convention for non-integrable payoffs.
The obvious route is finite-dimensional linear programming duality. It fails because the constraint is indexed by every in an uncountable Polish space and the dual variables are measures; the paper uses a semi-infinite Fenchel duality theorem (Borwein–Lewis), whose constraint qualification is exactly the relative-interior condition of Lemma EC.4.2. Proving that condition requires constructing, from any , an equivalent-type measure with finite moments, and separating a polyhedron from a convex set properly. A second difficulty is the passage to unbounded : it rests on the closedness of under pointwise limits (Lemma EC.4.1), proved by an induction on the number of coordinates along which the hedge positions diverge; compactness of the unit sphere alone does not suffice because the bid–ask cost is not linear.
The Lean development lives in the namespace ModelFreeBounds.Duality, with one definition file Market. Conventions:
[TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]. Indices are Fin m and vectors in are functions Fin m → ℝ; is intrinsicInterior ℝ.Market.Standing.EReal with ; the right-hand side of (2.3) is a supremum in EReal over the subset of measures, equal to when .The following formalizations would trivialise the statement and are excluded: a real-valued (where an unbounded infimum becomes ), the Bochner integral for (which is on non-integrable ), without the integrability of the , no-arbitrage stated almost surely under a fixed measure, over sub-probability or arbitrary measures, and a finite .
A complete development needs: semi-infinite or infinite-dimensional Fenchel duality for linear maps into (Mathlib has finite-dimensional separation theorems but not this duality), proper separation of a polyhedron from a convex set in , and the measure-theoretic construction of measures with prescribed null sets and finite moments on a Polish space. The closedness lemma and the support-function identity are independent of the duality and are natural first contributions. Contributions of any milestone, of alternative proofs of the goal, or of reusable infrastructure (extended-valued integrals, relative-interior constraint qualifications) are welcome.
Many decisions under uncertainty share one structure: a choice scales the exposure to a random quantity . A portfolio share scales the excess return of a risky asset, a coinsurance rate scales an uninsured loss, an output level scales a random price or a random cost. The linear-payoff model of Dionne, Eeckhoudt and Gollier (1993) covers all of these, and the comparative-statics question it poses is old: when the risk in increases, does the decision maker take less of it?
For second-degree risk (a mean-preserving spread, Rothschild and Stiglitz 1970) the answer is classical and depends on the decision problem. Menegatti and Peter (2022, doi:10.1287/mnsc.2021.4081) ask the question for risk increases of every order in the sense of Ekern (1980): downside risk (), outer risk () and beyond. Their finding is that the answer depends on whether is a risky benefit or a risky cost, and, for a risky cost, on the parity of .
Timeline:
The payoff of decision at realization is
where is compact, is continuous on , and are constants. The random variable takes values in . A decision maker with increasing, sufficiently smooth utility solves , with maximizer set .
Problem classes. The problem is risk taking if is increasing and risk mitigation if is decreasing; is a risky benefit if on and a risky cost if on .
th-degree risk increase. For a distribution function on put and . If have distribution functions , then is an th-degree risk increase over when for and on .
Risk attitudes. The decision maker is th-degree risk averse if . Where , the relative th-degree risk aversion is .
Strong set order. For , if for all , : and .
Assume the decision maker is th- and th-degree risk averse with on the relevant domain, and let be an th-degree risk increase over , with maximizer sets . Then
and for a risky cost with odd both orderings are reversed.
The result. Proposition 2 shows that the familiar statement "more risk, less risk taking" is a statement about risky benefits. For a risky cost, such as an uninsured loss or a random input price, an odd-order risk increase (for example, more downside risk) leads a prudent decision maker to take more risk. The paper uses this to explain apparently conflicting results in the portfolio, coinsurance, output-choice and hedging literatures, and to show that stochastic-dominance assumptions must be chosen differently for benefits and costs (its §5–§6).
Formalizing it. The result is proved in the paper; none of it is machine-checked. A complete development produces a reusable Lean account of Ekern's th-degree risk order through iterated distribution functions, the integration-by-parts identity behind Lemma 1, and a template for transferring a distributional order through Topkis's monotonicity theorem to argmax sets in the strong set order. Topkis's theorem is already proved on the platform and is included as a reference item.
The calculus steps (7)–(8) are short; the weight sits elsewhere. Lemma 1 is an -fold integration by parts of a Lebesgue–Stieltjes integral against a distribution function with possible atoms, with boundary terms that vanish only by Definition 2(i). Lemma 3 must turn a pointwise monotonicity of (5) into increasing differences of in , and then into a strong-set-order comparison of possibly set-valued maximizers. A tempting shortcut, differentiating (5) in , is unavailable: is only continuous. The sign conditions are then needed at payoffs lying between those of two decisions, not only at the payoffs themselves, which is why the relevant domain must be an interval.
cdf. The iterated CDF is indexed from : iterCDF μ xl k is the page's .Even/Odd.Supermodularity.Lattices.InducedSetOrder; is InducedSetOrder B₂ B₁.Contributions are welcome on any milestone; a proof of Lemma 1 is reusable well beyond this mission, for any statement about Ekern's risk orders.
Many models in decision theory, insurance and risk management do not act on random outcomes directly but on their distributions. A distributional transform is a map that sends a probability distribution on to another distribution . The most important class is that of probability distortions, for an increasing function on . They are the core of the rank-dependent utility theory of Quiggin (1982), the dual theory of choice under risk of Yaari (1987), the distortion premium principles of insurance pricing (Wang, Young and Panjer, 1997) and the probability weighting of cumulative prospect theory. Spectral risk measures such as Expected Shortfall are expectations under a distorted distribution.
In each of these theories is postulated. Liu, Schied and Wang (SSRN 3419388; Mathematics of Operations Research, 2021, doi:10.1287/moor.2020.1090) ask the converse question: which transforms of distributions are probability distortions? Their Theorem 1 answers it with three order-theoretic properties and no functional form. This mission formalizes that theorem and the steps of its proof.
A distribution is a Borel probability measure on , identified with its cdf . Write for the set of all distributions and for those with bounded support. The left quantile and the right quantile of are
is smaller than in stochastic order, , if for all . For a strictly increasing continuous with , the shape transform is the law of for .
is the class of functions that are increasing and right-continuous with , . A transform on a set of distributions is a probability distortion if for all , for some .
For the paper's Definition 2 introduces three properties:
The proof also uses (support unbounded below, bounded above) and (bounded below, unbounded above), and, for , the functional .
For or and ,
Both domains are part of the goal.
The theorem identifies probability distortions as the transforms that respect three structural features of a distribution: its order, its behaviour under weak limits, and its invariance under monotone reparametrisation of the outcome scale. It explains why distortion-based preferences and risk measures are the natural ones on distributions, and it is the base of the paper's further results on risk measures (§5) and on the sensitivity of distributional transforms (§6). Example 9 of the paper shows that lower-semicontinuity cannot be dropped.
The result is proved in the paper; to our knowledge no part of it has been formalized. The mission produces a machine-checked proof of Theorem 1, a formal account of how monotonicity and shape covariance force quantile representations, and reusable infrastructure: quantiles of probability measures on , stochastic order, shape transforms and probability distortions on Mathlib's ProbabilityMeasure ℝ. Formalizing Chambers' axiomatization of quantiles (milestone 3) is a contribution in its own right; the paper cites it and does not prove it.
The "if" direction is routine. The "only if" direction has two hard steps. The first is Chambers' axiomatization: showing that a monotone, shape-covariant functional on must be a quantile at a level independent of the distribution, which requires controlling the functional on distributions with flat stretches of the cdf, where the left and right quantiles differ. The second is the passage from to : monotonicity alone yields only one-sided inequalities for distributions with unbounded support, and the other inequality requires lower-semicontinuity along sequences produced by shape transforms that compress or stretch a tail. The obvious attempt, approximating by truncations and passing to the limit, gives only one of the two inequalities in each case.
Distributions are MeasureTheory.ProbabilityMeasure ℝ; is Set.univ and is the set of measures with for some . The paper's atomless probability space is not needed: every Borel probability measure on is the law of a random variable on such a space, so these are the same sets. The hypothesis is Set.MapsTo T M M. Cdfs are Mathlib's ProbabilityTheory.cdf. Quantiles are real-valued sInfs and are evaluated only at levels where the paper's quantile is finite: for , on and on . The stochastic order reuses the published StochasticOrders.Usual.UsualOrder (the survival-function form, which the paper notes on p. 5 is equivalent to its definition). Shape transforms are the order isomorphisms ℝ ≃o ℝ, acting by pushforward. Weak convergence is convergence in Mathlib's topology on ProbabilityMeasure ℝ. Lower-semicontinuity is the paper's closure property, not Mathlib's LowerSemicontinuous. A function is a real function constrained on , and "probability distortion" is the cdf identity on .
Shape transforms range over all increasing homeomorphisms of , not only affine maps; restricted to affine maps the "only if" direction is false (the super-quantile transform of Example 4 is a counterexample). No continuity, constant-preservation or support hypothesis is added to Theorem 1.
A complete development needs: elementary quantile calculus for measures on (Galois connection with the cdf, behaviour under pushforward), the portmanteau theorem for weak convergence (in Mathlib), Chambers' theorem, and the explicit approximating sequences of pp. 7–9. The quantile and stochastic-order lemmas are reusable well beyond this mission. Proofs of individual milestones, in particular Chambers' theorem, are welcome independently.
Markowitz's mean-variance problem trades off the expected terminal wealth of a portfolio against its risk. Over several periods the scalarized form of this problem is time inconsistent: a strategy that is optimal today for a fixed risk-aversion parameter is generally no longer optimal tomorrow for the same parameter, so the investor would deviate from her own plan (Björk & Murgoci 2014; Björk, Murgoci & Zhou 2014). The literature has responded by redefining optimality (equilibrium strategies) or by searching for a time- and state-dependent risk aversion that restores consistency (Karnam, Ma & Zhang, Annals of Applied Probability 27, 2017). Dynamic convex risk measures and their time consistency are developed in Detlefsen & Scandolo 2005 and Riedel 2004.
Kováčová and Rudloff (arXiv:1806.10981, Operations Research 2021) take a different route. They keep both objectives, measure risk by a time consistent dynamic convex risk measure, and treat the dynamic mean-risk problem as a family of vector optimization problems. They show that this family is time consistent with respect to weak minimizers and that its value functions, the upper images, satisfy a set-valued Bellman principle. This mission formalizes that Bellman principle.
Fix a horizon and a finite probability space with a filtration , trivial, , and for every nonempty event . denotes the -measurable random vectors with values in ; orders between random vectors are pointwise and componentwise.
A market has assets with adapted discounted prices . An investor holds positions on , subject to closed, conditionally convex constraint sets . With wealth at time , the feasible portfolios are
that is, self-financing strategies with initial value that respect the constraints. The terminal wealth is and .
Risk is measured by a dynamic convex risk measure : each is normalized, conditionally translation invariant, monotone (decreasing) and conditionally convex. It is time consistent: implies . The mean-risk function is
and the mean-risk problem minimizes over with respect to the cone . Its upper image is
and at the terminal time (5.2).
For every and every -measurable ,
The right side has a closure and no ordering cone.
The upper image is the infimum of in the complete lattice of closed upper sets, so it is the natural value function of a vector optimization problem. Theorem 5.1 expresses the value function at time through the value functions at time by a one-period problem, exactly as a scalar Bellman equation does. Computationally this is what makes the problem tractable: one solves a convex one-period vector optimization problem per node, backwards in time, and recovers the whole efficient frontier at every node and an efficient strategy forward along the realized path (Sections 6 and 7 of the paper do this for 2,500 periods). Conceptually, it shows that the mean-risk problem is time consistent in the set-valued sense without computing the moving scalarization in advance.
The paper proves Theorem 5.1; no machine-checked version exists. Formalizing it produces a Lean development of dynamic convex risk measures on finite filtrations, of conditional vector optimization in , and of upper images, none of which is currently on the platform beyond the static conditional convex risk measure reused here.
The equality has two halves of different character. Replacing the image by the upper image enlarges the feasible set of the one-period problem, and the new points must be shown to be limits of points already attained: this needs monotonicity of together with its continuity, which holds only because is finite. Removing the cone from the right-hand side needs translation invariance of with an -measurable shift and the monotonicity of with respect to the larger cone . Both closures matter: without them the identity fails in general, since the image of a closed set under need not be closed. The natural first idea, to define recursively, proves nothing: the content of the theorem is that the upper image built from whole multi-period strategies agrees with the recursion.
Fintype with an ambient σ-algebra ; the filtration is a Mathlib Filtration ℕ with and ; is a probability measure with for every nonempty measurable .CondConvexRisk.Representation.IsCondConvexRiskMeasure with respect to (axioms a.s. on ); time consistency is stated pointwise for measurable arguments. On a finite space with positive probabilities, a.s. equality of measurable functions is equality, so all of the mission's own statements are pointwise.condExp.A complete development needs: conditional expectation on finite filtrations (tower property, pull-out of -measurable factors), continuity of convex functions on finite-dimensional spaces, and elementary closure arguments in . The results on dynamic risk measures (Lemma 2.1) and on (Lemma B.1) are reusable beyond this mission. Proofs of any milestone are welcome independently.
A biclique in a graph is a pair of disjoint vertex sets in which every vertex of is adjacent to every vertex of . Maximum-edge bicliques model problems in product manufacturing lines and formal concept analysis; balanced bicliques arise in VLSI design and in the analysis of biological data; and the maximum product over cross-intersecting set families, an extension of the Erdős–Ko–Rado theorem studied by Pyber and by Suda and Tanaka, is an instance of the same parameter. Deciding whether a bipartite graph has a biclique with at least edges is NP-complete (Peeters, 2003), so polynomial-time upper bounds are of interest. The ratio parameter was introduced by Vallentin (2020) to bound product-free sets in finite groups.
In the complement of a bipartite graph a biclique becomes a biindependent pair: no edge between and . Laurent, Polak and Vargas (arXiv:2302.08886, Mathematics of Operations Research, 2025) study the product parameter and the ratio parameter of biindependent pairs in bipartite graphs, and bound them by semidefinite programs from the Lasserre hierarchy, by analogy with Lovász's theta number for the stability number. Their Proposition 1.2 orders these bounds in a single chain; it is the result this mission formalizes.
A bipartite graph has finite vertex sets and edges only between them; . A bipartite biindependent pair is a pair with , and no edge with , . Over all such pairs define
where the trivial pair contributes to . The parameter is the stability number of . The balanced versions , , take the same maxima over pairs with .
Let be the all-ones matrix and , indexed by , so that . For a matrix indexed by write . The first-order semidefinite bounds are
For an arbitrary graph, replacing the objective by in the first program gives the Lasserre bound , and by in the second gives the theta number . With the symmetric matrices supported on the edges of (zero diagonal), the dual of is .
Milestones 1, 5, 7 and 8–9 together give the goal.
The chain says that the semidefinite bound , designed for the ratio parameter , also bounds , and is never weaker than , the bound one obtains from the semidefinite relaxation of itself; the inequality can be strict (for minus a perfect matching, ). Since , the program gives a polynomial-time bound on the maximum product that is at least as good as . The paper builds on this its eigenvalue bounds for regular bipartite graphs (Proposition 1.3) and a sharpened Gowers bound on product-free sets in groups.
The result is proved in the paper. It has not been formalized; nor, to the knowledge of the mission, has Lovász's theta number, its identity with the first Lasserre bound, or its value on bipartite graphs. A completed mission adds a machine-checked theta number with these two classical facts, and the first formal treatment of semidefinite bounds for bicliques.
The two outer inequalities are elementary counting (Lemma 1.1). The inequality needs the dual program (32), hence strong duality for (32)–(33), which is not automatic for semidefinite programs. The inequality is the hard step: an optimal solution of is not feasible for , since the bordered constraint of ties the diagonal of to a border row, and simple scalings do not preserve the value. The paper calls its argument "a bit technical" and compares it with the classical proof of . The last two inequalities need for bipartite , a perfect-graph fact the paper cites rather than proves, and the identity of two formulations of the theta number, also cited.
E : V1 → V2 → Prop between two finite types; the vertex type is V1 ⊕ V2 and bipGraph E is the associated SimpleGraph, with no edges inside a side. Either side may be empty; no further hypothesis is assumed.Finset.sup' maxima, as real numbers, over the finite nonempty set of biindependent pairs; at is the paper's convention that trivial pairs have value .Matrix.PosSemidef (which includes symmetry); the bordered matrix is indexed by Unit ⊕ V. SDP maxima are sSup and the minimum (32) is sInf over real numbers. All feasible sets are bounded, so these are the paper's values (all are when is empty).SimpleGraph.sSup) is not this theorem; the definitions above rule these out.Needed infrastructure: positive semidefinite matrices, principal submatrices and Schur complements (in Mathlib), Gram factorisations, a strong duality theorem for semidefinite programs, and the stability number of bipartite graphs. The theta number, its two formulations and on bipartite graphs are reusable well beyond this mission. Contributions are welcome on any milestone, and on intermediate lemmas such as weak duality for (32)–(33).
Repeated games model long-run relationships: the same players meet stage after stage, observe what was played, and can condition today's behavior on the past. The folk theorem describes what such relationships can sustain. When players are patient, every payoff vector that is feasible and gives each player at least what the others can force on them is the payoff of an equilibrium, and the equilibrium can be chosen subgame perfect, so that every threatened punishment is itself credible. Economics, operations research and computer science use the result to explain cooperation and collusion and to reason about long-term contracts and repeated auctions.
The classical statement assumes stationary discounting: a payoff at stage is worth of a payoff today, and "patient" means . Experimental and behavioral evidence points instead to discount rates that change over time (hyperbolic and quasi-hyperbolic discounting), and planning problems with a finite or decaying horizon have weights that are not geometric at all. X. Li (later with D. Kim) asks whether the perfect folk theorem survives when the weight of stage is an arbitrary decreasing sequence, and gives a patience condition under which it does.
Timeline.
A finite set of players plays a stage game repeatedly. Player has a finite action set , , and gives the stage payoffs. At each stage every player observes the past actions and chooses an action, possibly at random. A behavior strategy assigns a mixed action to every finite history, and a profile determines a distribution over infinite plays.
An evaluation is a sequence in that is decreasing and sums to one; the payoff of is
Stationary discounting is . After a history of stages the remaining game is evaluated by the continuation evaluation ; unlike the stationary case, depends on . A profile is a subgame perfect equilibrium of if, after every history , the induced profile is a Nash equilibrium of the subgame . is the set of subgame perfect equilibrium payoffs.
The minmax level of player is
the lowest payoff the others can hold to by mixing independently. is the set of feasible payoffs and the set of feasible and individually rational payoffs.
A sequence of evaluations is patient if as , uniformly in .
If and is patient, then
The goal fixes no rate and no constants; it asserts only the limit.
The result. The theorem says that the set of credible long-run outcomes is the same under any patient time-dependent discounting as under stationary discounting with . Quasi-hyperbolic preferences with and discount factors that vary by stage are special cases. Patience is stated through ratios of consecutive weights. The paper notes that this condition does not cover -stage averages with , where the folk theorem is known to need extra assumptions. The equilibria use pure paths, with no public randomization.
Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission builds a reusable Lean model of discounted repeated games with perfect monitoring: behavior strategies, the induced distribution over finite histories, continuation games, subgame perfection, minmax levels and the feasible and individually rational set. It then states the theorem and the lemmas of its proof. The one-shot deviation principle under general discounting and the pure-path decomposition (Proposition 4.3) are standard tools that the literature usually cites without proof, and both are useful well beyond this paper.
The stationary proof relies on the fact that every subgame looks like the original game: . Under time-dependent discounting the continuation evaluation changes with the starting stage. A punishment phase of fixed length therefore carries a different weight depending on when it starts, and the number of stages needed to deter a deviation depends on the stage. Two consequences make the obvious adaptation fail. First, a deviation during a punishment starts a new punishment whose length differs from the remaining length of the old one, so the incentive check splits into cases (Lemma 5.2). Second, the pure paths that deliver the reward payoffs have to work for every continuation evaluation at once, which needs the uniformity statements of Lemma 4.2 and the perturbed decomposition of Lemma 4.4. Replacing each continuation evaluation by a geometric one does not work, because nothing forces the weights of a patient sequence to be close to geometric.
All declarations live in the namespace TimeDepFolk.Asymptotic. Stages are 0-based: Lean stage is the paper's , a history of played stages is Fin n → (∀ i, A i), and cont θ n is the paper's , which is when the tail sum vanishes. Mixed actions are lotteries (AGT.IsLottery) and the minmax level uses AGT.expectedPayoff from the published definition agt_games, with independent mixing by the others. Action sets are finite, so expectations are finite sums over histories and the payoff is the series ; no measure theory is needed. Payoff vectors live in I → ℝ with the sup norm. Subgame perfection quantifies over all histories, the empty history included, and over all behavior-strategy deviations; the one-shot reduction is a milestone to prove, not part of the definition. The player set and every action set are finite and nonempty. " nonempty and fully dimensional" is (interior (F g)).Nonempty.
The goal uses the extended-valued Hausdorff distance Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is when one set is empty, so a goal stated with it would hold vacuously for every at which no equilibrium is known; the extended version makes nonemptiness of part of the claim. Stating the goal for a single payoff, with Nash instead of subgame perfect equilibrium, or with Theorem 3.2's discount factors in place of evaluations would each prove a different and weaker theorem.
A complete development needs the probability of finite histories under behavior strategies, the decomposition of the payoff into the first stage and the continuation, the one-shot deviation principle, Carathéodory's theorem (in Mathlib), and the barycentric sensitivity of Claim 7.1. The repeated-game layer and the one-shot deviation principle can be reused for any discounted repeated game with perfect monitoring. Contributions to any milestone, and alternative proofs of the decomposition results, are welcome.
A knockout tournament for players is played in rounds: players are placed at the leaves of a complete binary tree, adjacent players meet in round 1, winners of adjacent matches meet in round 2, and the winner of round , the final, wins the tournament. Who can meet whom, and in which round, is fixed entirely by the seeding, the order in which the players are placed at the leaves.
A serial knockout competition (SKC) runs knockout tournaments with the same players and different seedings. The format is used in practice: since 2022 the Professional Darts Corporation's Premier League of Darts, with 8 players, consists of knockout tournaments, two blocks of seven of which have seedings fixed in advance by the organiser. For such a competition to be fair, no pair of players should be favoured or disadvantaged by the seedings: every pair of players should be able to meet equally often in each round. Lambers, Pendavingh and Spieksma call such a competition stable and ask whether stable SKCs exist for every number of players (arXiv:2211.02513, published in Mathematics of Operations Research, 2025). For they give a stable SKC derived from the Fano plane; for general they give an explicit construction from the finite field . This mission formalizes the general construction.
Fix and a set of players. A knockout tournament on is a seeding: a bijection from the leaf positions , read left to right, to .
For players and a round write if and can meet in round of , that is, they meet there if both win all their earlier matches (Definition 1.1). For leaf positions this means that and lie in the same block of consecutive leaves but in different blocks of leaves.
A finite family of tournaments on is stable in round if there is a number with
for all pairs of distinct players , and stable if it is stable in every round (Definition 1.2). An SKC is a family of knockout tournaments (Definition 1.3). Since a player can meet opponents in round of each tournament and has opponents, a stable SKC necessarily has .
The construction uses the field , for an irreducible of degree with root . Every is uniquely , and its degree is . For a tournament whose players are the elements of and a nonzero , the tournament is obtained from by replacing each player with .
Let be a knockout tournament on the elements of with for all distinct . Then
is a stable SKC, and for all distinct players and every round ,
The theorem settles the existence question for every , with an explicit family: the multiplicative group of acting on one degree-ordered seeding. A stable SKC gives every pair of players the same number of potential encounters in every round, so a tournament organiser can schedule a series of knockout tournaments without favouring any pair. The paper uses the construction to tabulate stable SKCs for 16 and 32 players.
The result is proved in the paper; none of it is formalized. The mission produces a machine-checked definition of balanced knockout tournaments and of their meeting rounds, a reusable notion of stability for families of tournaments, and a formal proof of the construction. The counting identity for elements of of given degree with respect to a power basis is reusable on its own.
The combinatorics is elementary once the right tournament is in hand; the difficulty is in connecting three descriptions of the same object. The meeting round is a property of leaf positions in a binary tree; the degree is a property of coordinates in a power basis of a field; and the relabelling is a multiplicative operation, which does not preserve coordinates. The obvious attempt, a seeding that orders the field elements by their coordinates, gives the identity for one tournament only. The step that needs care is the passage from this single tournament to the whole family: multiplication by differ from those of is distributed as $ ranges over the nonzero elements.
P is a seeding Seeding k P := Fin (2 ^ k) ≃ P. The meeting round is the predicate CanMeetIn T x x' i (leaf blocks of size and , with ), not a function, so it has no junk value at .𝒯 : ι → Seeding k P with [Fintype ι]; IsStableSKC requires Fintype.card ι = 2 ^ k - 1 and stability in every round . The goal's family is indexed by the units Fˣ.F with a power basis pb : PowerBasis (ZMod 2) F; is pb.dim, is pb.gen, and the coordinates are pb.basis.repr x i. deg pb 0 = 0 is a junk value; every statement uses only at nonzero arguments, and the hypothesis on is required only for distinct players, since the page leaves undefined.scale T z of the seeding by , not by the formula ; the formula is milestone 3.The goal states the explicit count and the family size , so it cannot be satisfied by a degenerate meeting predicate or by an empty family; Lemma 3.1 shows that its hypothesis on is satisfiable for every power basis, so it is not vacuous.
Contributions welcome: the coordinate lemmas for power bases over ZMod 2 (the bijection with binary expansions of leaf positions), the milestones in any order, and the goal.
The construction from the Fano plane (Theorem 2.1, Lemma 2.1) and the tables of §4 are not part of this mission.
Retailers that sell many products set prices against one another, and the demand for each product depends on the prices of all of them. Affine demand models, , are the standard starting point for this kind of multi-product price competition in operations management and industrial organization. Two questions follow once an equilibrium is known to exist. Can the firms reach it, and does it matter where they start? A Nash equilibrium that the firms cannot find by adjusting their prices tells little about what prices will actually be observed.
Federgruen and Hu (Operations Research 69(1), 2021; submitted manuscript at SSRN 3010503) answer this for a general multi-firm, multi-product model with an arbitrary number of firms and arbitrary product assortments. The game has features that defeat the usual tools. Once the affine demands are extended so that no demand turns negative, the game is in general not supermodular. Example 1 of the paper, after McGuire and Staelin (1983/2008), is a duopoly that is not supermodular and has a continuum of equilibria. Earlier work (Federgruen and Hu, Operations Research 63(3), 2015) characterized the equilibria. One of them, the special equilibrium , has a closed form. The 2021 paper shows that this equilibrium is reached from any starting price vector when every firm repeatedly plays a robust best response.
A finite set of products is partitioned among firms. Firm sells the products . The foundational demands are
where is an price-sensitivity matrix subject to three assumptions:
Each firm has a cost vector, . Let be the block-diagonal matrix of the transposed firm blocks , and let and . The cost projection solves the linear complementarity problem
and the special equilibrium is
Given the other firms' prices , firm sees the residual intercept . Its robust best response maximizes
Prices are restricted to keep the firm's own affine demands nonnegative, so the firm needs only its own demand and cost data. Collecting all firms gives the map , and is its -fold iterate. Finally, .
There exist a norm on and a constant such that
Neither the norm nor is fixed, because the paper asserts only that they exist.
The milestones follow the paper's own proof:
Theorem 3 makes the special equilibrium an operational prediction. Firms that adjust prices myopically, each using only its own demand and cost information, converge to from any start. The convergence is geometric, so the number of rounds needed to come within grows only logarithmically in the initial distance. This holds although the game is not supermodular and can have infinitely many equilibria, so the lattice-theoretic stability results that cover supermodular games do not apply. Theorem 2 also identifies which of the possibly many equilibria the dynamics select.
The result is proved in the paper, but it has not been formalized. A machine-checked version has two parts: a model layer (affine multi-product demand, the cost projection, robust best responses), and an M-matrix layer (Lemma B.1: inverse-positivity, Schur complements of inverse M-matrices, spectral radius bounds). Mathlib has neither. The proof also rests on results that the paper cites without proof: Propositions 2 and 3 of Federgruen and Hu (2015), and Theorem 4(b) and Lemma B.2(d) of Federgruen and Hu (2016). A formalization has to supply them. In one place the proof cites Horn and Johnson (1985, Lemma 5.6.10) for an absolute norm close to the spectral radius. As stated there, that lemma does not give absoluteness for general matrices: has spectral radius , but every absolute norm gives it induced norm at least . The claim holds for the nonnegative matrix , and the corresponding milestone is stated for that matrix only.
The obvious route is to show that is a contraction in the sup norm and invoke Banach's fixed-point theorem. This fails: can exceed even though , and the bound is all the structure gives. The norm must be adapted to and must also be absolute, so that the componentwise bound transfers. The per-firm estimate behind that bound (Lemma 2) is itself not a Lipschitz estimate for an explicit formula. The robust best response is the solution of a constrained quadratic program whose active set changes with the competitors' prices, and the comparison goes through a componentwise minimum and monotonicity in the intercept. Separately, the fixed-point property needs the cost projection , an LCP whose unique solvability and nonnegativity depend on (IS).
Products form a finite type ι and firms a type F, with firm : ι → F assigning each product to its firm. Vectors are ι → ℝ with the pointwise order. Matrices are Matrix ι ι ℝ, and every matrix inequality is entrywise. The commitments are:
∀ x ≠ 0, 0 < x ⬝ᵥ R *ᵥ x, not Mathlib's Matrix.PosDef, which would add global symmetry.⁻¹. Every inverted matrix is invertible under the hypotheses.No trivializing reading is available. The norm must be definite, the robust best response keeps its feasibility constraint and is never defined by a closed form, and the convergence statement holds for every iterate. A sorry-free sanity check confirms that the standing assumptions, the cost projection and the fixed-point relation are all satisfiable on a two-firm example.
The following results are not formalized here:
Contributions that would be reusable beyond this mission include:
Congestion pricing charges road users for the delay they impose on others. The classical theory, going back to Beckmann, McGuire and Winsten (1956), assumes a single benevolent authority that sets every toll: charging each link its marginal toll makes the selfish (Wardrop) traffic pattern socially optimal. Many real networks are different. Roads, bridges and tunnels built under build-operate-transfer schemes are run by private operators who set their own prices to maximize their own revenue. When operators compete, an equilibrium of the pricing game need not exist, need not be unique, and can be far from optimal (Acemoglu and Ozdaglar 2007; Hayrapetyan, Tardos and Wexler 2007).
Correa, Guzmán, Lianeas, Nikolova and Schröder (2021) ask whether a regulator who can only impose price caps — an upper bound on the toll of each link — can steer competing operators to the optimal flow. Their main result, Theorem 1, answers yes: optimal tolls bounded by the marginal tolls, used as caps, are the unique equilibrium of the capped game, even against coalitions of operators. This mission formalizes that theorem and the two monotonicity lemmas it rests on.
A network has links and commodities ; each commodity has a finite set of routes, each route being a set of links. Commodity has a maximum demand and a nonincreasing, continuous, nonnegative utility function on ; its aggregate utility is . Each link has a latency function on , nonnegative, nondecreasing, convex and smooth.
A flow assigns to each route so that ; is the set of flows and is the flow on link . Under a toll vector , users settle in a Wardrop equilibrium, which is a maximizer over of the potential
The paper restricts to instances where this maximizer is unique (linkwise) for every , and writes for it.
The social welfare of a flow is ; an optimal flow maximizes it over . The marginal tolls are , and a toll vector is optimal if is the optimal flow.
Each link is run by a separate operator, whose profit is . Given caps , operator chooses . A profile is a Nash equilibrium of the capped game if no operator gains by a unilateral change within its cap, and a strong Nash equilibrium if no nonempty coalition has a joint change, within the caps and confined to , that strictly raises the profit of every member. By Definition 1, is a (strong) cap equilibrium if itself is the unique (strong) Nash equilibrium of the game with caps .
If is an optimal toll vector with
then is both a cap equilibrium and a strong cap equilibrium.
Theorem 1 resolves, for capped games, the problems of existence, uniqueness and inefficiency that the literature on competing link operators identified: the regulator needs only to know the optimal flow and its marginal tolls, and then no operator, and no coalition of operators, has a reason to move away from the optimal tolls. The paper's consumer-surplus comparison (Theorem 2) is a comparison among such great tolls, and its extensions with operating costs, multi-link operators and complementary links (Theorems 3–6) follow the same pattern. The two lemmas are general facts about Wardrop flows under elastic demand — monotonicity in the tolls and a first-order bound at a profit maximum — that are reusable for any toll-setting or pricing question in nonatomic routing.
The result is proved in the paper; none of it is formalized. The mission produces a machine-checked version of the full argument, including the steps the paper states without proof.
The equilibrium flow is defined only implicitly, as the maximizer of a concave potential that depends on the tolls, so every statement about operators' profits is a statement about a parametric optimization problem. Lemma 1 needs first-order optimality conditions of (1) on a polytope of route flows with elastic demand, and continuity needs a maximum-theorem argument in which only the link flows, not the route flows, are unique. Lemma 2 cannot simply differentiate : need not be differentiable in , so the argument must work with one-sided difference quotients. The coalition part of Theorem 1 cannot be reduced to unilateral deviations; a deviation by many operators at once moves the flow on every link of the network simultaneously.
All declarations live in the namespace NetworkPricing.Caps. Links, routes and commodities are Fin J, Fin R, Fin Sd; link flows are KellyStochasticNetworks.linkFlow of the published definition KellyStochasticNetworks_Wardrop. The model commits to the following conventions:
flow with flow t a maximizer of (1) for each , together with the paper's uniqueness assumption on link flows.Formalizations that make the goal trivial are ruled out: must maximize the potential (1), not be an arbitrary function of ; uniqueness of the equilibrium is part of the conclusion, not just that is an equilibrium; and the strong notion quantifies over all coalition deviations, not single-player ones.
A complete development needs first-order optimality conditions for concave maximization over polytopes, a version of Berge's maximum theorem, and convexity facts about differentiable functions. All of these are reusable well beyond this mission. Contributions are welcome on each milestone independently, and on general lemmas about parametric Wardrop flows.
In a multiplayer multi-armed bandit, several agents repeatedly choose among the same finite set of arms, and two agents that choose the same arm collide and receive nothing. The model comes from cognitive radio and wireless networks: users share channels, a channel used by two users at once carries neither transmission, and the quality of a channel differs from user to user. Each user must learn the channel qualities from her own rewards while avoiding the others, and in a large network the users can neither exchange messages nor observe each other's choices.
When all players share the same arm means, the problem reduces to finding the best arms and spreading the players over them; algorithms such as Musical Chairs (Rosenski, Shamir and Szlak, 2016) do this. When each player has her own means , the target is an optimal solution of an assignment problem, which couples the players. Bistritz and Leshem (arXiv:1810.11162, NeurIPS 2018; a journal version appeared in Mathematics of Operations Research) gave the first algorithm for this heterogeneous case that uses no communication at all and has near-logarithmic expected regret. This mission formalizes the main theorem of the preprint arXiv:1810.11162v7.
There are players and arms. At every turn each player picks an arm . The non-collision indicator is if more than one player chose arm in the profile and otherwise. Player receives : the reward of her arm, or after a collision.
The rewards satisfy Definition II.1: for each the sequence is i.i.d. with a continuous law, mean , variance and Bernstein's moment condition with parameter , and the sequences are independent. Because the law is continuous, a zero reward reveals a collision almost surely; this is the only feedback a player gets. The horizon is unknown to the players.
Write . The benchmark is an optimal assignment , assumed unique, and the total regret is
The Game of Thrones (GoT) algorithm (Algorithm 1) runs in epochs , each with three phases: an exploration phase of turns, where players sample arms uniformly and average their collision-free rewards into estimates ; a GoT phase of turns, where players run a perturbed content/discontent dynamic with perturbation and exponent on the game ; and an exploitation phase of turns, where each player plays the arm with which she was most often content during the last GoT phases. The GoT dynamics form a Markov chain on the states (baseline arm and mood of every player), with optimal state .
With , , integers , and , there is such that for all large enough
The theorem shows that full decentralization costs at most a factor in regret: the lower bound of Proposition II.3 holds already with full information, and GoT reaches with no messages, no knowledge of , and no observation of the other players. It is a learning-in-games result as much as a bandit result: the players reach the welfare-maximizing assignment of a game that is not interdependent, which the content/discontent dynamics of Marden, Young and Pao (2014) require, and the requirement on the exponent is instead of .
The result is proved on paper and has no machine-checked proof; nothing in this mission is formalized yet. A formal proof would also settle points the paper leaves implicit, recorded in the formalization notes: one must serve every epoch although the stationary threshold of Theorem V.6 depends on the epoch's estimated utilities, and the GoT chain has transient states, so the tree formula of Lemma V.5 and the norm must be applied to its closed class.
Each phase is analysed separately, and the work lies in the parts that are not standard. The exploration bound needs a concentration inequality for averages over a random number of collision-free samples. The GoT phase needs a lower bound on a stationary probability of a perturbed chain on states, obtained by comparing the resistances of trees in the sense of Freidlin and Wentzell (Appendix A, pp. 15–18). It then needs a Chernoff bound for Markov chains (Chung, Lam, Liu and Mitzenmacher, 2012) in terms of the mixing time. Finally, the epochs interact: the estimates of epoch determine the chain of epoch , the GoT phase starts from the end of an earlier GoT phase, and the exploitation phase votes over dependent phases.
The natural first idea, to treat each epoch's GoT run as a fixed ergodic chain and apply a stationary-mass bound, fails twice. The chain is random through the estimates, so the threshold on must hold uniformly over a neighbourhood of the true means. The chain is also not irreducible: a state where a colliding player is content can never be entered.
Players, arms and turns are 0-based (Fin N, Fin M, t : ℕ), and epochs are 1-based. The collision indicator is noColl, because also names the slack in Theorem V.6 and Lemmas V.7–V.8. The rewards live on a probability space as r n i t. The players' randomization is a family of private uniform seeds, jointly independent of the rewards, and every random choice of Algorithm 1 is realized from a seed with exactly the prescribed law. Each player's action and update read only her own memory, her own seeds and her own received reward; the means, , and the other players' actions never enter a rule. Collisions are read off a zero reward, as in Algorithm 1. The regret is Eq. (3) with the realized comparison rewards. The GoT chain is an explicit matrix on Fin N → Fin M × Mood. Stationarity and the mixing time (worst start, total variation) come from the published MarkovMixing definitions.
Conventions and disclosed additions:
A formalization in which a player's rule sees the instance would make the goal trivial (play from the start), and a policy class in place of Algorithm 1 would change the theorem. Neither is used. Irreducibility of the GoT chain is false, and no statement assumes it.
Needed infrastructure that Mathlib lacks: Bernstein's inequality for sums over random index sets, the Markov-chain tree theorem (already posed on the platform as YoungConventions.Perturbed.markov_chain_tree_formula), and a Chernoff bound for finite Markov chains. The last two are reusable well beyond this mission, and contributions of them as separate theorems are welcome.
The incremental knapsack problem is a multi-period extension of the binary knapsack problem. Items are inserted over a planning horizon whose capacity grows over time, and an item, once inserted, stays. Sharp (2007) and Hartline (2008) introduced it in their theses on incremental optimization. It models resource allocation in which the available budget grows predictably, such as investing a growing income or selecting bonds (Faenza–Malinovic 2018), and is related to assortment optimization over time.
Timeline.
An instance has items, item with profit and weight . It also has periods, period with a coefficient and a capacity , where and . A solution is a nested sequence of item sets with for every . The item is introduced in period . The objective is
and .
The algorithm of Section 3 of the paper fixes an accuracy and proceeds in four steps.
The subroutine is the λ⁺-bounded scheme of Section 2 (Theorem 3). Section 3 uses only two properties of it: the returned weight is at most the optimum (super-optimality, equation (8)), and the returned profit is at least .
The statement holds for every admissible profit grid, every subroutine with the two properties above, and every traceback. depends on alone.
The result. Theorem 1 settles the approximability of incremental knapsack up to the PTAS barrier. Strong NP-hardness excludes an FPTAS, so a PTAS is the best possible guarantee unless P = NP. It answers the open question of Bienstock et al. (2013, §5) in the strongest form. Its reduction to sub-problems with bounded ratios of values is a template for related multi-period problems; compare the generalized incremental knapsack problem of Faenza, Segev and Zhang (arXiv:2009.07248).
Formalizing it. The theorem is proved on paper; no machine-checked proof exists. A formalization checks a chain of eleven quantitative steps with explicit constants (, , , ). It also records the corrections the printed argument needs, listed under Formalization scope: the printed profit grid (7) is too short for Lemma 11 (with , one period and 20 unit items, the algorithm with grid (7) returns at most 3 items against ), and the single-cluster profit has to be read with the full-horizon . The model layer (nested solutions, item contributions, clusters) is reusable for other incremental optimization problems.
The obvious argument fails in two places.
First, a single dynamic program over all periods cannot use the Section-2 subroutine, whose running time depends polynomially on the ratio between extreme values. That ratio is unbounded in general. Clustering bounds within a cluster, but items introduced in the dropped bad intervals are lost. The loss is controlled only on average over the shift (Lemma 7), not for each shift.
Second, a near-optimal solution can spread one profit class over several clusters, which would couple the single-cluster sub-problems. Lemma 8 shows that after filtering negligible items, the classes form stars ordered across clusters. Its proof uses the gap of a factor that a bad interval creates between clusters.
The remaining steps are discretization arguments. Claim 3 is an induction comparing with . It works only because the profit requirement absorbs the grid rounding, and because super-optimality lets a smaller carry over. Claim 2 telescopes the resulting losses.
All declarations live in the namespace IncrKnapsack.PTAS, and one definitions file holds the whole model.
Representation.
Fin T, 0-based: the paper's period is t - 1.Fin n → Option (Fin T), the introduction period of each item; nestedness is built in.⊤ : WithTop ℝ, and minima over finite sets are Finset.inf.j = ℓ + 1.Additions and corrections, all disclosed in the items.
IsProfitGrid. It requires property (15) of p. 35 on , the range p. 22 gives , guarded by so that it is satisfiable on every instance.IsSubroutine, the guarantee of Theorem 3, met by the exact single-cluster optimum. The traceback may choose any minimizer.Everything else is constructed, not assumed: rounding, intervals, clusters, , and the glued output .
Ruled out. A trivializing formalization would assert that some feasible solution has , which the optimum itself satisfies. The goal is instead about the constructed output , and nothing about it is assumed.
Not formalized.
Contributions welcome. Proofs of any milestone, and a general existence lemma for admissible grids and tracebacks.
A scheduler in a computing system may know how to allocate a fixed collection of jobs efficiently while having no reliable forecast of future arrivals. A guarantee for jobs available at the outset does not immediately answer whether decisions remain effective when new work appears during execution. Unknown release dates capture this distinction: a job becomes available and visible only at its release time. Shmoys, Wein and Williamson separate this information restriction from uncertainty about processing requirements and give a general conversion between the two arrival models. The present target is their Theorem 2.1, rather than the independent unknown-size conversion later in the paper. Source, §2.
The question concerns both efficient computation and execution on physical resources. A short schedule selected with knowledge of future jobs is not an online algorithm. Conversely, an online rule can make legitimate decisions yet produce schedules much longer than the best off-line schedule. The target retains both requirements and asks how much a scheduler's makespan guarantee deteriorates when advance knowledge of arrivals is removed.
A job is a finite processing task using some of a fixed finite collection of exclusive resources. An instance has a finite set of job identities, job data , and real release dates . Jobs cannot receive processing before release. Each execution specifies resource allocations over time and must satisfy the job's processing rules. Two jobs cannot occupy the same resource simultaneously. The completion time is the time at which job has finished, and the makespan is
The empty instance therefore has makespan zero. The off-line optimum is the least makespan among feasible schedules for the original released instance , with the same resources and processing rules as the online scheduler.
For parallel machines, a job of size runs at speed on machine . Identical machines have all speeds equal to one; uniformly related machines have ; unrelated machines allow job-dependent speeds. Nonpreemptive execution completes a job in one uninterrupted interval. A restart discards a canceled attempt's work. Preemption permits work to accumulate across interruptions and migration. These are separate choices of the environment, not extra powers granted to the transformed scheduler. Source, §1, p. 1314.
The base scheduler receives a finite admitted batch whose local release dates are all zero. Its admission information may include job sizes, or sizes may remain hidden until processing reveals completion. The transformation preserves that choice. In particular, removing advance knowledge of release dates does not remove information about sizes that the base scheduler needs.
The goal is the complete algorithm transformation of Theorem 2.1. Let and suppose one uniform polynomial-time scheduler always produces feasible zero-release schedules satisfying
Then the paper's batching controller supplies one causal polynomial-time scheduler for unknown release dates such that, for every finite valid released instance,
Both guarantees are pure multiplicative inequalities, without an unspecified additive constant. The constant is fixed by the published theorem. Source, Theorem 2.1, pp. 1316–1317.
The formal target also requires an execution of the controller, feasibility of its assembled schedule, disjoint batches covering every job, and at most nonempty base invocations. If the base computation costs at most , the stated metered bound for the wrapper is
Here counts encoded data cells, including release-date cells for analysis, and the constants and the base code are independent of both the instance and the resource configuration. The Lean statement indexes configurations explicitly, allowing their approximation factor while retaining exactly in each configuration. The coefficient 10 is a bookkeeping allowance, not an approximation factor. There are no numbered milestone dependencies in the source proof; the only theorem target is Theorem 2.1.
The result allows zero-release scheduling guarantees to be used in settings with unpredictable arrivals while controlling their loss. Its scope is broader than one machine class. The source explicitly includes shop scheduling and allocation of submeshes, reflecting the independence of the conversion from particular speed formulas or off-line optimization methods. Source, p. 1317.
The mathematical theorem was proved in 1995. The task here is to formalize its statement and eventually its known guarantee. The local draft provides resource-use schedules, processing observations, an interpreted base program, and a controller whose execution is tied to the resulting schedule. Its theorem remains an open Lean proof obligation. These definitions also expose precisely what future formal proofs may assume about release information, processing information, and computation.
A makespan inequality alone cannot certify the result. A construction may accidentally inspect future job data, use an unattainable off-line value as an action, or count physical processing time as computational effort. Each produces a different statement from a polynomial-time online transformation.
Boundary events require equally careful treatment. Arrivals at a completion time must belong to the next batch; an arrival after an idle interval must not be lost; simultaneous arrivals must be collected together in a fixed job-ID order. Empty input and a single batch must remain meaningful without referring to nonexistent preceding batches. The source's compact stage notation is not itself an implementation specification for these cases. None of these concerns permits dropping the computational or information clauses from the target.
The development uses nonnegative real time, natural-number job identities, finite profiles of half-open resource-use intervals, and a static job-local legality relation. It includes concrete parallel, shop, and mesh environment definitions. Whole-job restriction, time translation, release relaxation, and joining disjoint schedules preserve the intended static semantics. Time-dependent resource availability, external deadlines, and cross-job setup requirements are outside that interface.
The optimum inequality is written against every feasible off-line comparator. Valid jobs each have a finite legal execution; sequential execution after all releases supplies a finite feasible comparator, and makespans are bounded below by zero. Universal comparison is consequently equivalent to comparison with their infimum, including empty input.
The computational convention is an explicit finite-cell real RAM, with a finite program, a costed interpreter, and a processing port restricted to requested allocations and completion feedback. It permits arbitrary real times and does not assert a bit-complexity bound for arbitrary reals. Known and hidden sizes have separate admission encodings. Waiting for completion is a physical operation, whereas arithmetic, queue copying and message handling contribute to computation. No future job count or terminal-arrival notification is given to the controller.
The goal expressly rules out scalar-trace and vacuous-algorithm formalizations: it requires actual feasible resource schedules generated by the fixed controller using the interpreted base program, together with the computational bound. No variant theorem is posed. The recorded two-unit-job example demonstrates sharpness of this batching construction's factor 2, without claiming optimality among all possible online schedulers.
Risk measures enter optimization models as objectives or constraints, and the models that use them most, multi-stage stochastic programs, are solved as large linear programs. A risk functional is only usable there if it can itself be written as the value of a linear program. Eichhorn and Römisch introduced polyhedral risk measures for this purpose (doi:10.1137/040605217). They are risk functionals defined as the optimal value of a linear stochastic program whose right-hand side is the random income being evaluated. The average value-at-risk of Rockafellar and Uryasev (doi:10.21314/JOR.2000.038) is the basic example. Sums and nestings of average values-at-risk over several periods are further examples.
Sections 2.4.4 and 3.3.5 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific, 2007, doi:10.1142/6478) develop this class in the book's profit convention (larger is better). They prove that, under two finite-dimensional conditions on the program's data, the functional is finite, concave and continuous, and that it has a dual representation over an explicitly polyhedral set of densities. The book then reads off from that dual set which axioms of multi-period acceptability functionals the functional satisfies. This mission formalizes those results.
Let be a probability space, , and a filtration in with trivial . Fix and with . Income processes live in , densities in . Random variables equal almost surely are identified.
A set is polyhedral if it is a finite intersection of closed half-spaces, and a polyhedral cone if all of those half-spaces pass through the origin. Its polar cone is , which is the negative of the usual dual cone.
The data of a polyhedral functional are dimensions , vectors and non-empty polyhedral sets for , together with coefficients . The functional is
The first decision is deterministic. The functional depends on the filtration only through the measurability of the decisions. The two standing conditions are:
The dual set is
The single-period case with is the book's Definition 2.66.
Under (i) and (ii), is finite, positively homogeneous, concave and continuous on . It is information monotone (MA0): enlarging the filtration does not decrease it. For every ,
Theorem 3.38 turns a linear multi-stage program into a risk functional with known structure. The functional is concave and continuous, and it is the lower envelope of linear functionals over a dual set cut out by finitely many linear conditions on conditional expectations. Theorem 3.39 makes that dual set into a design tool. Which translation equivariance a polyhedral functional has can be read off from finitely many vector conditions, without evaluating the functional. The multi-period average value-at-risk and sums of single-period average values-at-risk are obtained this way. These are the risk functionals that can be embedded in large-scale stochastic programming models without leaving linear programming.
The results are proved in the book and in Eichhorn–Römisch (2005). As far as is known, no part of them has a machine-checked proof. The platform has no polyhedral risk functional. It has finite-dimensional linear programming duality and a loss-side, upper-tail average value-at-risk on , which uses a different convention and so is not a substitute.
The theorem is linear programming duality, but in an infinite-dimensional space of adapted processes. Finite-dimensional LP duality does not apply directly, for three reasons:
Finiteness needs feasible decisions with a uniform bound, which is a measurable-selection question for a polyhedral set-valued map. The duality step needs conjugacy on a product of spaces. It also needs to exchange an infimum over random decisions with an expectation, and that exchange is a theorem about normal integrands, not a formality. Little of this exists in Mathlib.
The two inclusions of Theorem 3.39 that use complete recourse alone cannot simply be combined with the goal: a non-empty dual set is an extra hypothesis there (see below).
Lean namespace RiskFunctionals.Polyhedral.
Fin k → ℝ with the dot product ⬝ᵥ. Polyhedral sets and cones
are explicit finite systems of inequalities, never general closed convex cones. The polar cone
uses the book's sign.MemLp hypotheses and an -measurable
representative. Constraints hold almost surely, and conditional expectations are Mathlib's.W t (t-τ), indexed by the period of the decision it multiplies, so that its type matches.EReal, so empty
or unbounded programs give instead of a junk value. Finiteness is always a conclusion
and never a hypothesis. The other properties are stated for the real value only alongside
finiteness. The dual set is the printed polyhedral set, not an existential family.sSup over the feasible set, or a dual set given
only by its existence, would make the goal trivially true. Both are ruled out by the EReal
values and by the explicit dual set.Beyond the paper. There are two corrected variants, each stated next to the faithful item.
Two sign slips in Example 2.70 (a printed and ) are corrected in the faithful item itself.
The development needs measurable selections of polyhedral multifunctions, Fenchel–Moreau conjugacy on products, and interchange of infimum and integral. All three are reusable well beyond risk measures. Contributions of any of them, of the single-period case, or of the multi-period average value-at-risk as an instance are welcome.
Multi-stage stochastic optimization models a decision maker who acts at times while a random scenario unfolds, and who may use at each time only the information revealed so far. This nonanticipativity constraint is what separates a genuine multi-stage problem from a collection of deterministic ones. A standard way of measuring its cost, the expected value of perfect information of decision analysis and stochastic programming (Birge & Louveaux 2011, Ch. 4), is to compare the decision maker's optimal value with that of a clairvoyant who sees the whole scenario before deciding.
Pflug and Römisch (Modeling, Measuring and Managing Risk, World Scientific 2007, §5.2) carry out this comparison not only at the root of a scenario tree but at every node, with the expectation replaced by a general acceptability functional . This produces three stochastic processes on the tree: the optimality process, the clairvoyant process, and their difference, the value-of-information process. The book shows that, for functionals that behave linearly under mixing of distributions, the value of information is a supermartingale: the expected remaining value of perfect information decreases as the scenario is revealed, and vanishes at the horizon.
Let be a probability space and . A tree process is a process , taking values in a finite set of nodes, with for every : the current node determines the whole path that led to it. The root stage consists of one node. The standard filtration is with , and the clairvoyant's filtration is .
Scenario variables are , . A profit function , written , depends on a decision sequence lying in a decision space . A decision rule is a random sequence; it is non-anticipative, , if each is -measurable, and clairvoyant, , if each is -measurable.
A version-independent probability functional assigns a real number to each distribution in its domain of distributions on . For a Markov kernel on and a distribution on , the compound distribution is . is compound linear, compound convex or compound concave if
respectively, for all , with for -almost every and , for which the right-hand integral exists ("compound linear on "; the book's Example 2.13 uses exactly this domain-relative form for expected utility).
Fix such a functional (an acceptability functional; larger is better), whose domain contains the law of every feasible profit under the conditional probabilities below. For a node of with let and let be applied to the law of under it. The conditional problems are
At the root these are the multi-stage problem and the clairvoyant's problem . The optimality process is , the clairvoyant process , and the value-of-information process .
If is compound linear on its domain, then
is a supermartingale under with respect to .
The goal is the weakest statement of the chain: it fixes no constants and asserts only the direction of drift of .
is the value of perfect information of the multi-stage problem, which the book interprets as a multi-period deviation-type risk functional (the multi-period average value-at-risk deviation of its Chapter 3 is an instance). The supermartingale property gives this risk a dynamic meaning: as the scenario is revealed, the remaining value of information decreases in conditional mean, and it is zero at the horizon. The two lemmas separate the effect of information into its two sources: the clairvoyant's value is a fair game for compound linear functionals, while the non-anticipative decision maker's value can only improve in conditional mean, because a decision fixed at time remains feasible after more is revealed.
The results are proved in the book. No formal version is known: the platform has no item on value-of-information processes, clairvoyant problems or compounding properties of functionals; the closest related items are a complete-information bound in partially observed Markov decision processes and a submartingale property of stable multi-period risk processes, both in other settings. A formalization adds a precise setting (finite scenario trees, conditioning on nodes, attained maxima) in which the chain from Definition 2.11 to Corollary 5.3 is checked.
The supermartingale inequality is a statement about conditional expectations on a tree, while compound convexity is a statement about functionals of mixtures of distributions; the work is to identify the law of the profit under as a compound distribution of the laws under the children's conditional probabilities, with the children encoded as a real mixing parameter. The book's proof of Lemma 5.1 interchanges the maximum and the functional, a step it justifies elsewhere only for monotone functionals, which Lemma 5.1 does not assume; its proof of Lemma 5.2 applies an inequality stated for nonrandom decisions to random ones. A solver should not rely on either step as printed. The martingale half of Lemma 5.1 needs the reverse inequality, for which the optimizers of the child problems must be combined into one feasible clairvoyant decision; the same combination is not available for non-anticipative decisions, which is why the optimality process is only a submartingale. Proposition 2.12 additionally needs regular conditional distributions.
Lean 4 with Mathlib. Time is Fin (T + 1), stage being the single root node ([Unique (N 0)]), so is trivial. Node types are finite with measurable singletons; this is what makes meaningful at every node of positive probability (Mathlib's ProbabilityTheory.cond) and every process integrable. The filtration is a Mathlib Filtration assumed equal to at each stage, and sub-, super- and martingales are Mathlib's Submartingale, Supermartingale, Martingale. Decisions take values in a measurable space with measurable singletons, holds for every , and is jointly measurable. The functional is 𝒜 : Measure ℝ → ℝ, version-independent by construction, evaluated only at probability measures; it is real-valued (the book allows ) with a domain 𝒟 : Set (Measure ℝ), and each compounding (in)equality is required only when the mixed and the mixing distributions lie in and is integrable. The tree theorems assume that contains the law of every feasible profit under every conditional probability of a positive-probability node; Proposition 2.12 assumes and that the conditional distributions are in almost surely. Mixing is over Markov kernels from to (K ∘ₘ G). Proposition 2.12 uses Mathlib's condExpKernel on a standard Borel space and assumes exists.
The maxima , are not defined through sSup: the theorems take them as given numbers and assume each is the greatest element of its value set at every node of positive probability. This rules out the trivializing formalization in which a junk supremum of an empty or unbounded set makes the processes constant and the claim empty. The book's remark "in particular if is the expectation" is covered as an instance and not stated separately: the expectation is compound linear on the distributions with a finite mean, and on a finite tree every feasible profit has finitely many values. Taking to be all distributions instead would exclude the expectation, because Lean's Bochner integral of a non-integrable function is .
Needed infrastructure: finite partitions and conditional expectation on atoms, mixtures of conditional laws, measurable selection of child optimizers on a finite tree, and the disintegration property of condExpKernel. The definitions CompoundLinear/CompoundConvex/CompoundConcave, IsTreeProcess, and the decision-problem sets are reusable for other results of the book on conditional acceptability and multi-stage problems. Proofs of any milestone, and sorry-free instances showing the hypotheses are satisfiable (e.g. a bounded expected utility on a two-stage tree), are welcome.
Risk that unfolds over several periods is measured in two common ways. One adds up one-period measurements of each payment, each made with the information available one step earlier. The other composes one-period conditional measurements backwards in time, the way dynamic programming evaluates a policy. The second way is the one used in multistage stochastic programming with risk-averse objectives, because it is time-consistent by construction: a plan that is optimal today stays optimal when re-evaluated tomorrow. Ruszczyński and Shapiro (Conditional risk mappings, Math. Oper. Res. 2006) built the general theory of such compositions. Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) studied the matching dynamic-programming (Bellman) principle for coherent multiperiod risk-adjusted values.
The most widely used one-period building block is the average value-at-risk. When it is applied conditionally at every stage, the composition is the nested average value-at-risk. Section 3.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007), treats both constructions. It builds the nested functional, shows that it depends only on the total payoff, gives its dual representation as an infimum over bounded-growth martingale densities, and compares it with the additive (multi-period) average value-at-risk. This mission formalizes that section's statements.
Let be a probability space with a filtration . Random variables that agree almost surely are identified, and all (in)equalities between them hold almost surely. The book uses profit variables, where larger is better. Fix and put . An income process is with .
A conditional acceptability mapping has three properties:
A family defines the nested functional and the compositions
Since is trivial, both are constants.
For and a sub--field , the conditional average value-at-risk of is defined implicitly by
With trivial this is the lower-tail average of the quantile function. The nested average value-at-risk is
The multi-period average value-at-risk is . Below it is used with all and .
For and , the nested average value-at-risk is well defined, and
Here is -measurable. The feasible are nonnegative martingales whose one-step growth is at most .
The representation (3.49) shows that the nested average value-at-risk is a coherent functional of the total payoff. Its dual set consists of martingale densities with a multiplicative growth bound. Proposition 3.36 builds on this description to compare the nested and additive constructions. The same description underlies cutting-plane methods for risk-averse multistage programs: there the nested value is evaluated stage by stage, and each stage contributes one factor . Proposition 3.33 is the general mechanism behind this: predictable translation-equivariance collapses a nested definition into a cumulative one.
All of these results are proved in the book, some only in outline. None is machine-checked. The platform has loss-side, upper-tail conditional value-at-risk results in other conventions and a nested risk-adjusted cost in an SDDP setting. It has no statement of the nested average value-at-risk or of (3.49). Formalizing this section yields a reusable treatment of conditional average values-at-risk defined by duality, together with their compositions along a filtration.
The conditional average value-at-risk is not given by a formula. It is defined through a family of infima indexed by the sets , so composing two of them requires knowing what the first one does when paired with a general bounded weight rather than an indicator. Merging the infima of successive stages into one infimum over processes needs measurable selection of near-optimal densities, conditional on the earlier stages, and the martingale constraint must be preserved. The printed proof treats in a few lines and asserts that the general case "follows by induction". Its last display also carries a misprint, for (FINDINGS F5).
Random variables are functions Ω → ℝ. The filtration is Mathlib's Filtration ℕ, and only indices matter. IsStandardFiltration records that is trivial and . The conditional average value-at-risk is the predicate IsConditionalAVaR, a literal transcription of the defining relation, with the infimum computed in EReal. The nested and multi-period values are predicates that are existential over versions of the conditional average values-at-risk. The goal therefore asserts existence and the identity separately. A version of the goal that only assumed some value exists, or that took a bare real infimum, would be vacuous or junk-valued, and the formal statement rules out both. The expectation of the -measurable output is the functional's real value. The dual set requires to be -measurable, which the page leaves implicit.
Beyond the paper. Two corrected variants are posed beside the faithful statements:
The faithful statements stay as printed and are expected to be disproved.
Contributions that would be reused beyond this mission:
An investor who splits a budget across risky assets faces a trade-off between expected return and risk. Markowitz proposed measuring risk by the variance of the portfolio return and selecting, for each required expected return, the portfolio of least variance (Markowitz 1952). Tobin added a risk-free asset (Tobin 1958), and Sharpe, Lintner and Mossin turned the resulting one-fund structure into the capital asset pricing model (CAPM), whose beta equation is still the standard first model of expected returns in finance (Sharpe 1964).
This mission formalizes the closed-form part of that theory as presented in §4.2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), pp. 189–195: the explicit efficient portfolio without a risk-free asset (Proposition 4.8), the solution with a risk-free asset (Proposition 4.9), and the CAPM equation with its variance bound (Proposition 4.10).
Let be a probability space and a random vector of returns, each coordinate with a finite second moment. Returns are profits: larger is better. The vector of expected returns is and the covariance matrix is the matrix with ; it is symmetric and positive semidefinite. A portfolio is a weight vector (negative weights, i.e. short positions, are allowed) with return , so that and . Write for the all-ones vector.
The CAPM problem without a risk-free asset fixes a required return and asks for
With a risk-free asset of constant return , a portfolio is a pair , where is the holding of the risk-free asset and the holdings of the risky assets , with mean and covariance . Its return is , and the problem is
A portfolio is efficient if it solves the respective problem for some . The market portfolio holds nothing in the risk-free asset and in the risky ones; is its return, and .
Assume is invertible and is not a multiple of . With
the unique solution of (4.20) is
any two efficient portfolios for different returns span all efficient portfolios by affine combinations (the Two Fund Theorem in this model), and
The efficient frontier is therefore a parabola in the (variance, mean) plane.
Propositions 4.10 (i) and (ii) are milestones; Proposition 4.9 is a further item of the mission on which they stand.
and, when , every efficient portfolio is an affine combination of and . 2. Proposition 4.10 (i), the CAPM equation (4.25). For every portfolio with ,
with equality if and only if the portfolio is efficient, and, as printed, if and only if .
Proposition 4.8 is the explicit description of the mean-variance efficient set: the efficient portfolios form a line in weight space, and the minimal variance is a quadratic function of the required return. Proposition 4.9 shows that a risk-free asset turns this line into one through the risk-free portfolio (the one-fund, or separation, property), and Proposition 4.10 derives from it the CAPM relation between a portfolio's expected excess return and its beta, together with the capital-market-line bound. These are the statements on which the later sections of the chapter, and most textbook treatments of portfolio theory, build: risk-return diagrams, the market portfolio, beta as a risk measure.
The results are classical and their proofs are elementary, but they are not in Mathlib, and no Prove2Me item states them; the closest platform item is the multi-period mean-variance mutual fund theorem of Bäuerle and Rieder (MDPFinance.MeanVariance.mutual_fund_theorem), a different, dynamic statement. A formalization makes the hypotheses explicit that the printed proofs leave implicit (invertibility and nondegeneracy conditions, the budget constraint behind "any portfolio") and checks the printed equality conditions, one of which is false as stated.
The Lagrange conditions of the printed proof are necessary conditions only. Turning them into the statement requires showing that the stationary point is the global minimizer and the only one, which uses positive definiteness of ; the hypothesis gives only invertibility, and positive definiteness has to come from being a covariance matrix. Dividing by needs , which is not among the hypotheses and must be derived from " is not a multiple of " together with the structure of . The variance identities require computing variances and covariances of linear combinations of square-integrable random variables. In Proposition 4.10 (ii) the equality case is where the printed statement goes wrong: a portfolio short in the market portfolio attains equality with correlation .
All statements live in the namespace RiskFunctionals.Frontier. Assets are indexed by Fin M; vectors are Fin M → ℝ, matrices Matrix (Fin M) (Fin M) ℝ, and is Mathlib's matrix inverse. The mean vector and covariance matrix are computed from a random vector with MemLp 2 coordinates on a probability space using Mathlib's covariance and variance, so " invertible" is the printed hypothesis and positive definiteness is a consequence, not an assumption. "The solution" is stated as existence and uniqueness of a global minimizer on the feasible set (IsSolution420, IsSolution423). The divisions by , by and by are guarded by the printed or implicit nondegeneracy hypotheses; a statement in which or were allowed would make the closed forms the zero vector, so these guards are part of the statement rather than conveniences. The correlation is used only where the portfolio variance is positive, since it is undefined otherwise.
Beyond the paper. One variant item is posed beside the faithful statements: capm_variance_bound_corrected (corrected, finding F4) replaces the equality condition of Proposition 4.10 (ii) by ; with one risky asset of mean 2 and variance 1, and , equality holds while the correlation is . The faithful Proposition 4.10 (ii) is therefore expected to be disproved.
A complete development needs the variance and covariance of finite linear combinations of random variables, positive semidefiniteness of covariance matrices, and the minimization of a positive definite quadratic form under linear equality constraints. These are reusable well beyond this mission; proofs of them as separate lemmas are welcome.
Risk management in finance, insurance and energy rarely concerns one payoff at one date. A pension fund, a hydro-power producer or a bank holds an income process , observed together with an increasing flow of information, a filtration . Chapter 3 of G. Ch. Pflug and W. Römisch, Modeling, Measuring and Managing Risk (World Scientific, 2007, doi:10.1142/6478), argues that risk can only be measured for the pair (process, filtration). It axiomatizes multi-period acceptability functionals, the profit-side counterpart of the dynamic risk measures of Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 152 (2007)), Riedel (Stoch. Proc. Appl. 112 (2004)) and Ruszczyński and Shapiro (Math. Oper. Res. 31 (2006)).
In one period, dual representations of acceptability functionals as infima over probability densities are what make them usable in stochastic optimization: they turn a risk-averse objective into a min–max problem with an explicit dual set. Section 3.2.1 of the book proves the multi-period analogue. Each version of translation-equivariance corresponds to an explicit set of dual processes.
Let be a probability space and a filtration in with . Fix and with . The process space is , normed by . Its dual is , with the pairing . Functionals take values in . The conjugate of is (3.19).
A family is a multi-period acceptability functional (Definition 3.14) if every member is proper ( everywhere, somewhere) and:
The weaker forms are (MA1′), the same identity for constants only, and (MA1″), the identity for constants in the first period only. A multi-period probability functional is any functional that does not take both values (p. 27).
Section 3.1.3.2 adds information to a single-period functional (3.7) through its dual extension (3.8).
If is an upper semicontinuous multi-period acceptability functional, then for every
Conversely, if can be represented in the form (3.21) for some proper , then is proper, upper semicontinuous and satisfies (MA0)–(MA3).
Theorem 3.20 identifies the dual variables of a multi-period acceptability functional. They are nonnegative processes with , so their running products are, when integrable, density processes: changes of measure built period by period along the filtration. The three theorems 3.20–3.22 together show how the strength of translation-equivariance, (MA1), (MA1′) or (MA1″), shrinks or enlarges the dual set. This is the basis on which the book later represents the nested and the multi-period average value-at-risk (§3.3) and polyhedral functionals as linear programs. It also underlies the min–max reformulations of multi-stage risk-averse stochastic programs.
The results are proved in the book. None of them, and none of the axioms (MA0)–(MA3), has a machine-checked statement on the platform or in Mathlib. The related platform items, MultiperiodRisk.Bellman.stable_tfae (stability and the Bellman principle for sets of probabilities) and ConvexRiskFn.Dual.theorem_2_2 (single-period, loss-side, measures as duals), are different statements. Formalizing the chapter fixes the encoding of a filtration-dependent functional, which later chapters on nested functionals need.
The forward directions rest on Fenchel–Moreau duality on a product of spaces, which Mathlib does not provide in this form: the dual of the subspace of -measurable classes must be identified with for every simultaneously, including , . The functionals are extended-real-valued, so every step must handle , and the constraint involves conditional expectations of elements.
Read literally, the statements are not all true:
The faithful statements are kept as printed; a solver should expect to disprove those parts.
The filtration is a Mathlib Filtration indexed by Fin (T+1). A process is a function on Fin T whose component lies in lpMeas ℝ ℝ (𝔽 t.succ) p P, the subspace of of classes with an -measurable version. Lean's index is therefore the book's . The product topology on this type is the norm topology of . In Proposition 3.10, is the supergradient set of , as the book defines it on p. 43, not an independent set. Values are in EReal, and every infimum is taken in EReal over an explicit constraint set, so an empty set gives , the book's value. Constraints hold almost surely, and conditional expectations are Mathlib's condExp. Concavity is the EReal inequality .
Because (MA0) compares filtrations, in Theorem 3.20 is a family indexed by all filtrations with trivial . Part 1 assumes Definition 3.14 for the family, and part 2 assumes a representation at every filtration. Theorems 3.21 and 3.22 concern one filtration and keep the probability-functional convention as a hypothesis.
A trivializing formalization is ruled out: the infima in (3.21)–(3.23) are over the printed constraint sets, never all of (which would collapse them into (3.20)), and in part 1 is the conjugate (3.19), not an arbitrary witness.
Not stated: Propositions 3.8 and 3.9 (expected conditional functionals, which need the conditional acceptability mappings of §2.3) and Theorem 3.23 (local Lipschitz continuity and Hadamard directional differentiability).
Beyond the paper. One corrected variant is posed beside the faithful items. multiperiod_representation_corrected drops (MA0) and properness from the converse of Theorem 3.20. A two-filtration family built from and the expected conditional violates (MA0), and off gives .
Reusable beyond this mission: Fenchel–Moreau duality on products of lpMeas spaces, and the identification of -measurable duals. Contributions of either, or of proofs and disproofs of the printed converses, are welcome.
A distortion functional values an uncertain profit by integrating its quantiles against a reweighting of the probability scale: small (bad) quantiles receive more weight, large ones less. The construction appears in actuarial pricing (the distortion premium principles of Denneberg and Wang), in decision theory (Yaari's dual theory of choice), and in finance as spectral risk measures (Acerbi) or weighted values-at-risk (Cherny). Its central structural fact is that every concave distortion is a mixture of average values-at-risk, the lower-tail averages : this Choquet representation reduces properties of the whole class (concavity, monotonicity with respect to second-order dominance, comonotone additivity) to those of one family. The representation was proved by Acerbi (2002), Jones and Zitikis (2003) and Pflug (2006). This mission formalizes it as Proposition 2.64 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, §2.4.2), together with the lemmas of that section.
All random variables are profit variables (larger is better) on a probability space . For a random variable with distribution function and left limit , the quantile function is the left-continuous inverse
and the average value-at-risk at level is
A distortion function is a bounded, right continuous, increasing function on , the distribution function of a non-negative measure on (not necessarily a probability measure). Writing for the distributions for which is integrable, the distortion acceptability functional is
also written . gives the expectation, the value-at-risk , and the average value-at-risk. is concave when with a nonincreasing density , which may be unbounded near .
Two orders on random variables enter: (convex order) when for every convex for which both expectations exist; and are comonotone when their joint distribution function is . A functional is comonotone additive when it is additive on comonotone pairs.
If is concave, there is an increasing function on with and such that, for every ,
Conversely, every comonotone additive functional having such a Choquet representation is a distortion functional. The goal leaves otherwise unspecified; one serves every .
The Choquet representation identifies the concave distortion functionals with the closed convex cone generated by the average values-at-risk. Downstream, this gives the coherence properties of spectral risk measures, their consistency with second-order stochastic dominance, and, through Proposition 2.65, a dual description by rearrangements of the distortion density that is used to optimize portfolios under such criteria. It also separates the class from the larger family of law-invariant coherent functionals, which are infima of such mixtures over a family of mixing measures (Kusuoka) rather than single mixtures.
The results are classical and proved in the literature; none is machine-checked in this form. A related loss-side layer exists on the platform (MultistageStochastic.distortion_avar_mixture, proved, for a spectrum on with the upper-tail AV@R), but its sign, tail and integrability conventions differ, so it does not state this book's theorem. The formalization adds a quantile calculus with atoms (the left-continuous , , the generalized quantile transform) and Lebesgue–Stieltjes integration against distortion measures, both reusable for the rest of the series.
The forward direction is not a finite-dimensional extreme-point argument: may be unbounded at , so the mixing measure must be obtained as a limit and the exchange of integrals justified for quantile functions that are only -integrable, with unbounded at both ends. Distributions with atoms make on flat stretches, which is exactly where Lemma 2.62 and (2.69) need care.
Proposition 2.65 is false as printed (finding F1): for the differentiable convex and uniform on , , while gives . Its printed proof uses that is nonincreasing. The faithful milestone is therefore expected to be disproved; a corrected variant is posed beside it.
Distributions are probability measures on ; for a random variable, is the image measure of under . is computed by sInf; its junk value (at when everywhere, and at ) is never charged. and are Mathlib StieltjesFunctions; integrates over against . Membership in contains -integrability of , (the mass puts on , where ), and finiteness of when charges . vanishes on , so has no atom at , and the representation integrates over ; -integrability of is part of the conclusion, and the converse is stated on integrable for which that integrability holds. Infima in Proposition 2.65 are greatest lower bounds of value sets restricted to integrable products, with attainment stated separately. Uniform variables are measurable with law Lebesgue measure on , and is independent of in (2.68)–(2.69), as Proposition 1.3 requires. The book's has a sign typo and is used as .
A trivializing formalization would integrate a quantile function that is not - or -integrable, where Lean's integral returns , or take an infimum of an empty set; every such integral is guarded by an integrability hypothesis or an asserted integrability, and every infimum is an IsGLB of a set shown nonempty by the attainment clause.
Beyond the paper. One variant: [Corrected] Proposition 2.65 adds the hypothesis " concave" and changes nothing else (finding F1, the counterexample above). A further finding (F2) records that the converse half of Proposition 2.64 does not use comonotone additivity; no variant is posed for it.
Contributions welcome: proofs of the milestones, a disproof of the printed Proposition 2.65, and reusable lemmas on quantile functions with atoms and on Stieltjes integration on .
A deviation functional measures how far a random profit spreads around its mean: the variance, the standard deviation, the mean absolute deviation from the median, and the average value-at-risk deviation are the standard examples in portfolio selection and in risk-averse stochastic programming. Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), §2.5, organize many of them under one construction, the minimal loss functional: the smallest expected loss incurred when is predicted by a constant under a convex loss . Optimization over portfolios with such a functional as the risk term relies on writing it as a supremum of linear functionals of — a dual representation — because a supremum of linear functions can be handled by linear and conic programming and by subgradient methods.
The best known instance is the representation of the average value-at-risk as a minimum over a scalar , due to Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002), stated in the loss convention. The general convex-analytic tool behind such representations is Rockafellar's conjugacy theorem for integral functionals (Pacific J. Math. 1968). This mission formalizes the book's Theorem 2.75, which combines the two for every minimal loss functional, together with the results its special cases rest on.
Let be a probability space, , and the conjugate exponent, . Random variables are profits (larger is better) in ; dual variables are in , so that is finite.
Let be non-negative, convex, with . The minimal loss functional of is
defined for such that exists. The Fenchel conjugate of is
For example gives and ; gives the mean absolute deviation from the median and equal to on and outside.
The distribution function of is , its quantile function the left-continuous inverse , . For the average value-at-risk is the lower-tail average
and the average value-at-risk deviation is . Write and .
For every as above and every with finite,
and, for every and ,
The constants , and are exactly the book's; the last minimum is attained.
Two further items state Eq. (2.89) (p. 97), , and Eq. (2.101) (p. 102) as printed, .
The result. Theorem 2.75 gives every minimal loss functional an explicit dual set: the centered , penalized by . For piecewise linear the penalty is the indicator of a box, so is a supremum of linear functionals over a polyhedral set, and the acceptability functional is an infimum over mean-one dual variables; (2.114) and the last display recover the dual representation (2.20) of the average value-at-risk from this general principle. For quadratic the theorem returns the variance representation (2.89). The same dual sets feed the book's later results on the monotonicity of with respect to stochastic orders and on conditional versions (2.116)–(2.117).
Formalizing it. No platform item states Theorem 2.75, the integral conjugacy of Proposition B.3, or the dual representations of the variance and standard deviation. Related platform results use other conventions — the loss-side, upper-tail CVaR minimization formula (RUCVaR.MinFormula), a minimal weighted mean absolute deviation in Ogryczak–Ruszczyński normalization (DualSSD.MeanRisk.hDiam_eq_min), finite-dimensional Fenchel–Young and biconjugation (ConvexOptimization.fenchel_young, ConvexOptimization.fenchel_biconjugate_eq_self). The mission produces the profit-side, statements of the book.
The weak inequality in (2.113) is the Fenchel–Young inequality integrated; equality is the content. The printed proof treats piecewise linear by choosing, from alone, a partition on which one affine piece of is maximal, and claims for every ; that identity holds only at , and the conclusion does not follow (for and uniform on the chosen is ). The statement itself is correct in that example, but a complete argument has to choose the dual variable at a minimizing , which need not exist, and has to pass from piecewise linear to general by a limiting argument the book does not give. On the side, an optimal such as need not lie in when grows faster than , so the supremum is in general not attained and must be approached. Proposition B.3 requires a measurable selection of subgradients and handles the case .
Lean represents random variables as measurable functions with MemLp hypotheses (, , p.HolderConjugate q, ) on a probability space; constraints on hold almost surely. is an extended-real supremum (EReal), so it is where the book's supremum is unbounded. The suprema and infima of the dual representations are taken in EReal over the for which (resp. ) is finite — almost surely finite and integrable — which does not change the book's value. is defined as the infimum in of : the book's "min" presupposes attainment, which fails for and unbounded above, and attainment is not claimed. The standing assumption of §2.5.5 that exists is a hypothesis of the parts on general . is the book's lower-tail average of the left-continuous quantile function, not the loss-side upper-tail CVaR; variance is Mathlib's ProbabilityTheory.variance and .
A trivializing formalization is ruled out: no supremum or infimum is a bare real sSup/sInf whose junk value on an empty or unbounded set could make an identity hold, the dual sets are nonempty ( resp. is admissible), is an infimum in rather than a real sInf, and the minimum for is stated with attainment (IsLeast).
Beyond the paper. Two variants are posed beside the faithful items. A corrected Proposition 2.74 adds the hypothesis that is finite: at and exponentially distributed, for every while , so the printed minimum does not exist. A corrected (2.101) replaces the constraint by : for the left side is but every with gives ; the book's own rule (2.79) gives mean-one dual variables.
Definitions needed: the quantile function and , the Fenchel conjugate, the expectation of and the minimal loss functional; all are reusable by any formalization of law-invariant deviation measures. Welcome contributions include a measurable-selection lemma for subgradients of a convex function of one variable, Rockafellar's integral conjugacy on (of which Proposition B.3 is a case), and the variant statements.