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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
This paper introduces the notion of calibrated representations for affine Hecke algebras and classifies and constructs all finite dimensional irreducible calibrated representations. The main results are that (1) irreducible calibrated representations are indexed by placed skew shapes, (2) the dimension of an irreducible calibrated representation is the number of standard Young tableaux corresponding to the placed skew shape and (3) each irreducible calibrated representation is constructed explicitly by formulas which describe the action of each generator of the affine Hecke algebra on a specific basis in the representation space. This construction is a generalization of A. Young's seminormal construction of the irreducible representations of the symmetric group. In this sense Young's construction has been generalized to arbitrary Lie type.
This mission is the statement-level formalization of Calibrated representations of affine Hecke algebras (arXiv:math/0401323v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Explicit construction, dimension, and classification (Abstract; Theorems 3.1 and 4.5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We define the notion of {\em classifying space} of a topological stack and show that every topological stack \X has a classifying space X which is a topological space well-defined up to weak homotopy equivalence. Under a certain paracompactness condition on \X, we show that X is actually well-defined up to homotopy equivalence. These results are formulated in terms of functors from the category of topological stacks to the (weak) homotopy category of topological spaces. We prove similar results for (small) diagrams of topological stacks.
This mission is the statement-level formalization of Homotopy types of topological stacks (arXiv:0808.3799v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Restriction of an adjunction to full subcategories (Lemma 7.4, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
59 results of the paper are not stated yet, because the library lacks an interface they need:
Bike-sharing systems such as New York's Citi Bike place bikes in docks at fixed stations. Over a day, demand pushes bikes away from some stations and toward others, and customers who find no bike, or no empty dock to return one, leave dissatisfied. Operators rebalance bikes by truck overnight, but the number of docks at each station is a strategic decision that can be changed only rarely and at a cost. Freund, Henderson and Shmoys (arXiv:1611.09304, Operations Research 2022) model this decision as a discrete optimization problem over the allocation of docks and bikes, show that the station costs have a discrete-convexity property called multimodularity, and give a discrete gradient-descent algorithm that solves the problem exactly, also under a limit on the number of docks that may be moved. The analysis was used with data from Citi Bike to recommend dock reallocations.
The model is general: the algorithm and its proof use only multimodularity of the station costs, so the result is a statement about minimizing separable multimodular functions under budget and movement constraints.
There is a finite set of stations. An allocation puts empty docks and bikes at station , so station has docks. A customer arriving at a station either rents a bike () or returns one (); a renter at an empty station, or a returner at a full one, is dissatisfied. For an arrival sequence , the user dissatisfaction function counts the dissatisfied customers when the station starts with empty docks and bikes. A demand profile is a probability distribution over arrival sequences, and the station cost is .
A function is multimodular if, wherever the arguments are nonnegative,
Station must hold between and docks. With a bike budget and docks in total, an allocation is feasible for problem (P3) if every station is within its bounds, , and . The objective is . The dock-move distance between two allocations is , the number of docks to be moved, irrespective of bikes. Problem (P2) adds the operational constraint that the solution be within dock-move distance of the current allocation .
A dock-move from to moves one empty dock (), one full dock (), one dock from to together with a bike from a third station to (), or one dock from to while a bike moves from to (). The neighborhood consists of all results of one dock-move. An allocation is bike-optimal if no reallocation of bikes with the same docks at every station is better.
Algorithm 3 first places bikes optimally for the current docks with a greedy routine (Algorithm 1), giving , and then repeatedly moves to the best allocation in the neighborhood (Algorithm 2), stopping when no neighbor is better. Its iterates are .
For every finite set of stations with multimodular costs, every feasible start and every run of Algorithm 3 (any tie-breaking), and every :
and moreover a stationary iterate is optimal for (P3), is optimal for (P3), and the run is constant from iteration on. With this solves (P2) for every movement budget with a single run.
The milestones follow the paper's proof: multimodularity of the station UDF (Lemma 2.1) and of the depot cost; the implied inequalities (4)–(6); convexity in the number of bikes (Fact 1) and the exchange property of separable convex functions (Fact 2); correctness of Algorithm 1; preservation of bike-optimality by a best dock-move (Lemma 3.1) and along the run; the station inequalities used in Lemma 3.3; the exchange Lemma 3.3; Lemma 3.2 and the optimality of local optima for (P3); Lemma 3.4 (local optimality in the next ball); and Lemma C.1.
Theorem 1 says that one greedy run answers every movement budget at once: the -th iterate is the best allocation reachable by moving docks. This makes the trade-off between reallocation effort and customer dissatisfaction computable as a whole curve, which is how the paper's case studies use it. The theorem also underlies the paper's faster scaling algorithms (Theorems 2 and 3), whose proofs build on it.
The result is proved in the paper; it has no machine-checked proof. The proof history is instructive: the authors' earlier version derived Theorem 1 from the claim that local optima inside the ball are optimal in the ball, which is false (Remark, p.20, citing a counterexample of Shioura 2018, who also gives an alternative correctness proof through M-convexity). A formal proof would settle the corrected argument. The formalization also repairs two printed statements: Definition 1's convention , under which Lemma 2.1 fails, and the gloss of "next choice of the gradient-descent algorithm" in Lemma 3.4.
The obvious argument is: each step is a best local improvement, a local optimum is globally optimal (Lemma 3.2), hence each iterate is optimal in its ball. This fails, because a neighbor of a ball optimum that improves may leave the ball, and local optimality inside a ball does not imply optimality in the ball. The paper's proof instead takes a better allocation closest to and applies the exchange Lemma 3.3 to rather than to , then rules out both places the exchanged allocation can lie. Lemma 3.4 alone runs five pages: a dock-move out of can interact with the up to three stations changed in the previous step in many ways, each handled by a chain of the multimodular inequalities.
Stations form a Fintype S with decidable equality. Costs are real functions g i : ℤ → ℤ → ℝ, multimodular on the quadrant; the paper's value off the band is replaced by requiring feasibility (Feasible) of every allocation compared. Allocations are integer vectors with explicit nonnegativity. "Dock-move distance at most " is dockGap a a₀ ≤ 2 * r, where dockGap sums the absolute differences of dock counts. Algorithms 1–3 are relations, so every tie-breaking is covered, and a stopped run is a constant sequence. Neighbors move a dock between two distinct stations. The ball is centered at the initial allocation.
The goal is stated for any family of multimodular costs; it specializes to the paper's problem through Lemma 2.1 and the depot lemma. It cannot be trivialized: the verification file shows a run of Algorithm 3 that moves, under multimodular costs and a feasible start, and the multimodularity hypothesis is on the whole quadrant, not only on the band (the band reading makes Theorem 1 false).
Everything is built on Finset.sum, Relation.ReflTransGen and PMF; no discrete-convex-analysis library is required. Contributions are welcome on any milestone: the inequality lemmas (Fact 1, the implied inequalities, the station inequalities) are short and reusable for other multimodular-cost models, Fact 2 is a general lemma on separable convex resource allocation, and Lemmas 3.3 and 3.4 carry the combinatorial core.
Most real-options models of capacity investment assume that the firm finances the outlay at the risk-free rate, or that capital comes from a competitive market. Many firms, in particular young and small ones, have no equity and borrow from a lender with market power. Huberts, Wen, Dawid, Huisman and Kort (Management Science, 2025) model this as a dynamic game. The lender announces a coupon scheme, the coupon rate it will charge as a function of the demand level at which the firm invests. The firm then chooses when to invest and how much capacity to install. Without a bankruptcy option, the paper solves the game in closed form (Proposition 1). The timing is the same as under internal financing (Huisman and Kort, 2015), but the capacity is halved. This is a dynamic, financial counterpart of the static double marginalization of successive monopolies (Spengler, 1950).
The paper connects two literatures. One is real options with capacity choice (Dixit and Pindyck, 1994; Huisman and Kort, 2015). The other is debt financing of investment, with endogenous default following Leland (1994). Earlier models in which the input supplier has market power (de Villemeur, Ruble and Versaevel, 2014) fix the size of the investment. In this model the size is a choice as well.
The demand level is a geometric Brownian motion , where is a standard Brownian motion and . The inverse demand is . After installing capacity at unit cost , with the outlay borrowed from the lender, the firm earns the profit flow , where is the coupon rate. Payoffs are discounted at the risk-free rate . The parameters satisfy , , , and .
In the no-bankruptcy scenario the firm pays the coupon forever. At an investment level and a finite coupon :
A coupon scheme takes values in , where means that financing is refused. The firm uses an investment threshold : starting from it waits until demand first reaches , at the time , and otherwise it invests at once. Its payoff is or , and the lender's payoff is defined in the same way with . Finally, is the larger root of .
With , the lender's optimal coupon scheme is
from every initial demand level, against every optimal response of the firm. Under this scheme the firm waits until demand reaches (the unique optimal threshold) and invests immediately above it, with capacity . At the trigger,
These are steps of the proof, each anchored to the body text that defines or asserts the object.
Proposition 1 makes the cost of external financing with a market-powered lender explicit. The coupon rate exceeds the risk-free rate, the capacity is half of what an internally financed monopolist installs, and the timing does not change. Two effects cancel exactly: a higher coupon delays investment, while the coupon's dependence on the investment level accelerates it. As a result, welfare is lower than under internal financing (Table 1 of the paper). The no-bankruptcy case is also the benchmark for the bankruptcy-option analysis of §3.2 and §4, which the paper carries out numerically.
The proposition is proved in the paper's Online Appendix. This mission formalizes the statement and the proof steps named in the body. None of it has a machine-checked proof yet. Milestone 1, the first-passage Laplace transform of a geometric Brownian motion, is a standard fact that is used throughout real-options theory and is reusable beyond this mission.
The calculus is elementary once milestones 1 and 2 are available. The difficulty is in the probability and in the game. Milestone 1 needs optional stopping for the martingale in continuous time, including on paths that never reach the level when . Mathlib's optional stopping theorem is stated for discrete time. Milestone 2 needs Fubini–Tonelli and the moment .
The game has a second source of difficulty. The lender's optimality ranges over every coupon scheme, including schemes for which the firm's best threshold is not where the lender wants it. A first attempt maximizes the lender's value pointwise in the coupon. That fails, because the pointwise maximizer need not induce the firm to invest at the lender's preferred level. The proof has to show that, without bankruptcy, the firm's and the lender's preferred thresholds under coincide.
All objects are in the namespace DebtDoubleMarg. The Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal (time ) on an arbitrary probability space. The geometric Brownian motion is its explicit exponential. The hitting time is a pathwise infimum in , and its discount factor is when the level is never reached. Coupons live in WithTop ℝ, and an infinite coupon gives both players zero. The firm's strategies are thresholds, as in the paper (p.6, endnote 6). is a chosen maximizer, whose existence and uniqueness are milestone 3. Only the paper's no-bankruptcy scenario (Proposition 1) is formalized. Propositions 2–5 and the numerical Results concern the bankruptcy option and are out of scope.
None of the payoffs (, , , , , firm-optimality) is defined by its closed form. Each is defined by its expectation or its optimization problem, so the goal cannot be reduced to algebra by unfolding definitions. Only , , the scheme (6) and are transcribed, because the statements name them. The goal also asserts that is optimal for the firm and that the sizes are unique maximizers, so its universal clauses are not vacuous.
Welcome contributions include a continuous-time optional stopping theorem for Brownian functionals, the expectation of a discounted geometric Brownian motion, and proofs of the milestones in order.
A non-parametric choice model describes customers by a probability distribution over rankings of products: a customer offered a subset of products buys the one ranked highest among them. Revenue management and assortment planning use such models because they impose no functional form on substitution behaviour (Farias, Jagabathula and Shah, 2013; van Ryzin and Vulcano, 2015). Estimating one from sales data means finding a distribution over the rankings whose induced purchase probabilities are close to the observed frequencies. Two features make this hard in practice: the set of rankings is exponentially large, and the observed frequencies are themselves only estimates, refined as more transactions arrive.
Ho-Nguyen and Kılınç-Karzan (arXiv:1702.05702v5) treat the estimation problem as a convex-concave saddle-point problem whose data are revealed through a sequence of estimates , a joint estimation and optimization (JEO) setting. Their framework bounds the error of an aggregated primal-dual iterate on the true data by quantities computable from the estimated data, and their primal-oracle algorithms produce sparse ranking distributions whose sparsity is controlled by the iteration count. This mission formalizes the core certificate of that framework, Corollary 1, together with the steps leading to it.
Let and be convex compact sets and let be a real function, defined for every data value in a parameter space, that is convex in and concave in . Define the primal and dual objectives
and the primal problem . The SP gap of a pair is
An algorithm runs for rounds. In round it uses the current data estimate to produce . Nonnegative weights with aggregate the iterates into the weighted averages and . Three error terms appear:
A primal-oracle algorithm picks first and then . In the choice-model application and is the convex hull of the ranking vectors, so this step is a linear program over with a vertex solution.
For arbitrary , data , weights with and primal-oracle steps ,
No rate, constant or special form of is fixed: the statement holds for every convex-concave , every horizon and every nonnegative weight sequence with .
Corollary 1 turns any no-regret algorithm for the dual player into an estimator for the primal problem on the true data. With standard online convex optimization methods , and under a Lipschitz condition on in the data the terms vanish as (Theorem 2 of the paper). In the choice-model application each primal step adds at most one ranking to the support of the estimated distribution, so the corollary gives an explicit trade-off between accuracy and sparsity of the fitted model.
The paper proves the result on paper; no machine-checked version exists. The mission produces a formal statement of the saddle-point certificate in the general convex-concave setting, independent of the choice-model application, so that later formalizations of specific regret bounds (online gradient descent, mirror descent, follow-the-leader) can be combined with it to give end-to-end convergence guarantees for primal-oracle schemes.
The algebra of the argument is short. The work is in the analysis that the paper leaves implicit: every "max" and "min" must be shown finite, and the paper assumes no continuity of . A convex function on a compact convex set need not attain its minimum and need not be continuous at the boundary, so compactness alone does not give attained extrema. Finiteness of , , and follows from the existence of affine minorants (subgradients at relative-interior points) of convex functions on compact convex subsets of , a fact that is not a one-line Mathlib lemma. The data-error terms are suprema of differences of concave (resp. convex) functions and can genuinely be infinite; these are excluded explicitly. The natural shortcut through Sion's minimax theorem is unavailable: its semicontinuity hypotheses are not among the paper's assumptions.
are Fin N → ℝ, Fin k → ℝ; the data space is an arbitrary type P; the horizon is Fin T. Every max/min is the real sSup/sInf of an image set. The goal assumes 0 < ∑ t, θ t and that the two images defining and are bounded above; when either is unbounded the paper's right side is and the bound is empty. No continuity, differentiability or special form of is assumed. The SP gap is defined by the second expression of the paper's (9), , which dominates the first expression by weak duality and so gives the stronger bounds without any minimax theorem. The primal-oracle condition is encoded as together with minimality of over , so the statement cannot be satisfied by points outside .
A complete development needs: Jensen's inequality for convex and concave functions on finite convex combinations (ConvexOn.map_sum_le), lower boundedness of convex functions on compact convex sets in finite dimension, and elementary lemmas on sSup/sInf of sums. The boundedness lemma is reusable well beyond this mission. Proofs of the milestones, and of auxiliary finiteness lemmas, are welcome.
Electricity is traded in two stages. In a day-ahead market generators commit quantities for a delivery period; at delivery, deviations between committed and actual production are settled in a real-time imbalance market at an imbalance price. As the share of wind and solar grows, the generators with the lowest marginal cost are also those with the largest forecast errors, and in several markets they already supply most of the demand in many hours. A generator of this kind can raise the day-ahead price by committing less than it expects to produce and selling the rest in real time. Whether it gains from doing so depends on how the imbalance price is set. European regulation asks that imbalance prices support competitive behaviour (Article 52 of the EU electricity balancing guideline), but the two families of rules in use, single pricing and dual pricing, were compared mostly by simulation before this paper.
Ghiassi-Farrokhfal, Belo, Hesamzadeh and Bunn (MSOM 2023) model this market with strategic low-cost generators and one nonstrategic expensive generator, show that the usual single price leads to under-commitment (their Theorem 1), compare it with two dual-pricing rules, and then propose an optimal pricing rule under which under-commitment disappears (Theorem 5). This mission formalizes Theorem 5 together with the model it rests on.
There are low-cost generators (LCGs) with zero marginal cost, indexed by , and one high-cost generator (HCG). Expected demand is normalized to ; the realized demand is . LCG expects to produce and actually produces . The market share of the LCGs is . The forecast errors are random variables on a probability space with mean and finite variance; they may be correlated in any way.
In Stage 1 each LCG chooses an offer adjustment and commits . The HCG schedules the rest, with , and the Stage-1 price is its marginal cost . In Stage 2 LCG trades the difference and the HCG adjusts by , where . Its marginal cost at delivery is with , so its total cost, the area under the marginal-cost curves, is
Since demand is inelastic, the efficient outcome minimizes cost, and the deadweight loss is , the extra cost of producing the same total partly as a real-time adjustment.
The optimal pricing (OP) rule charges LCG the imbalance price
and LCG chooses to maximize its expected profit .
Under the OP rule:
The statement covers every , every share vector and every joint law of the errors with finite second moments.
Theorem 5 says that the market power of renewable generators in the day-ahead market can be removed by the imbalance rule alone, without caps or monitoring: subtracting from the single price exactly offsets the gain an LCG makes on its Stage-1 sales by under-committing. The remaining deadweight loss is then the part caused by forecast errors, which no offer strategy can remove, so the rule attains the efficiency bound of Eq. (6). The paper's simulations (§7) show the effect against single pricing and two dual-pricing rules.
The proof is in an online appendix that is not part of the source used here, and no machine-checked version exists. Formalizing it checks a mechanism-design claim end to end, from the cost model through the expectations. The faithfulness work already found two places where the printed statement is stronger than what holds: "any LCG … choosing " cannot mean that is the unique equilibrium (other equilibria exist, one with positive deadweight loss), and the expected-loss formula of Lemma 1 and Theorem 5 needs to be uncorrelated with the aggregate error (a two-point counterexample gives against the printed ). The goal states the corrected theorem; the counterexamples are recorded in the item statements.
The algebra is short once the expected profit is written as a quadratic in the offers. The work is in the expectations. Every product of forecast errors must be shown integrable from square integrability, and the cross terms such as and vanish only because of the zero means. Moving between Bochner integrals and Mathlib's variance and covariance needs the means to be zero. The natural first attempt, expanding into , silently drops , and that is false without the covariance condition. The equilibrium clauses need the deviation to be unilateral and to range over the offer box, whose upper end depends on all the shares.
All declarations are in the namespace ImbalPricing. The market is a structure Market Ω N with fields μ, γ, α₁, α₂, ε, ν. The predicate Market.Standing collects exactly the standing assumptions: , , , , IsProbabilityMeasure μ, MemLp · 2 μ for and every , and zero means. The covariance condition is not part of it and appears only where it is needed. LCGs are indexed by Fin N. Expectations are Bochner integrals; Var and Cov are ProbabilityTheory.variance and ProbabilityTheory.covariance. The HCG cost is the oriented interval integral of Eq. (3), so the closed forms of Eqs. (3)–(4) are theorems, not definitions. The OP profit is defined as an expectation, not by its closed form. Equilibrium is the general predicate IsPureNash on strategy sets offerBox with payoffs profitOP. Prices and costs are linear as printed (no floor at zero on the marginal cost), and the paper's bounds , which only keep quantities nonnegative, are replaced by square integrability.
Without MemLp the integrals of non-integrable products would be and the identities would hold vacuously; the standing assumptions rule this out, and an explicit market satisfying them is checked. The goal contains no uniqueness clause, because uniqueness is false.
Reusable pieces: the IsPureNash predicate, and the expectation lemmas for quadratic forms in square-integrable random variables with zero mean. Contributions of proofs of any milestone are welcome; Lemma 1 and the closed-form profit are the natural first steps.
Many risk measures used in stochastic optimization are not expectations of a single function but composite functionals: expectations nested inside one another. The mean–semideviation of order , , and higher-order inverse risk measures are of this form. When the law of the data is known only through a sample, every nested expectation has to be estimated, and the plain sample average is not the only choice: replacing the empirical measure by a smoothed version (a kernel estimator, for instance) can reduce bias. Dentcheva, Lin and Penev (arXiv:2201.01338v1, later in Operations Research, 2023) prove that optimization problems built from such estimators are strongly consistent, whichever levels are smoothed. This mission formalizes that result and the stability theory it rests on.
Earlier work established the central limit theorem for empirical composite estimators (Dentcheva, Penev, Ruszczyński 2017); the consistency of smoothed and mixed estimators of optimal values and solutions is the contribution of the present paper.
Decisions are vectors and data are random vectors in with law and . Fix dimensions and functions
jointly continuous in and -integrable in . The composite functional is
and the problem is over a closed set , with solution set , assumed nonempty and bounded. A compact with and compact are fixed so that each inner expectation maps into the interior of .
Replacing at level by a measure gives the perturbed objective , its optimal value and its solution set over . Given an i.i.d. sample with empirical measure and smoothing measures , the mixed estimator uses for the levels in an index set and for the others:
Its optimal value is and its solution set . Distances between sets are the excess and the Pompeiu–Hausdorff distance .
Suppose the smoothed levels have components admitting moduli of continuity on , uniformly over , the unsmoothed levels have a -integrable envelope , and satisfies Assumption 6 (weak convergence to with uniformly integrable first moments). If, almost surely, is nonempty and contained in for large, then almost surely
and when is a singleton. No rate and no constant is fixed; the statement covers every , including (the empirical estimator) and the fully smoothed case.
The theorem justifies using kernel and other convolution estimators inside composite risk-averse optimization: the optimal value and every optimal solution of the smoothed problem are strongly consistent, with no boundedness of the integrands at the smoothed levels. Theorems 3 and 4 are general stability results for nested expectations under perturbation of each level's measure, and apply to any estimation scheme that converges in those metrics. The paper's bias comparisons between smoothed and empirical estimators (§4) presuppose this consistency.
The results are proved on paper; none of them has a machine-checked proof. A formalization produces checked statements of the stability theorems with every hypothesis explicit. Writing them out exposed four places where the printed statements need a correction (nonempty perturbed solution sets, continuity of the limit level maps in Theorem 3, the first-moment claim on p.11, and monotonicity of a subadditive modulus), each recorded with a counterexample in the item it affects.
The obvious argument, "each level converges, so the composition converges", fails twice. First, convergence at each fixed does not pass through the nesting: the inner level's output moves, so uniform convergence on , together with continuity of the limit maps and the interior conditions keeping the inner values inside , is required. Second, at the smoothed levels the integrands are unbounded and only uniformly continuous, so neither the Glivenko–Cantelli argument nor bounded weak convergence applies; uniform convergence over the class needs weak convergence plus convergence of first moments, and for these hold only almost surely and only because the tails of are uniformly integrable. Convergence of optimal values and solution sets over the possibly unbounded further needs the estimated solution sets to be nonempty and to stay in .
is EuclideanSpace ℝ (Fin d). The dimension family is m : ℕ → ℕ with m 0 = 1; levels are 1-based, f j for and a separate fLast for . The composite is a recursion nestStage over stages, shared by the true functional, the perturbed objective, the empirical estimator and the mixed estimator. Optimal values are infima over and solution sets are sets of minimizers; every theorem assumes them attained (nonempty solution sets), so the infimum is never a junk value. and take values in , so can only make a conclusion easier when the solution set is nonempty, which the hypotheses guarantee. Convergence in and is written as "for every , eventually, uniformly over the class". Weak convergence is tested against bounded continuous functions. The sample is X : ℕ → Ω → ℝ^m with iIndepFun and HasLaw, indexed from 0; is deterministic, and the inner limit of Assumption 6 is a limsup.
A trivializing formalization would drop nonemptiness of the estimated solution sets, under which the assumption is vacuous and the statement false; the formal statements assume it explicitly.
A complete development needs a uniform strong law of large numbers over a compact parameter set with an integrable envelope, weak convergence of empirical measures (Varadarajan), uniformity over equicontinuous classes with uniformly integrable growth, and Berge-type continuity of parametric minima. These are reusable well beyond this mission, and contributions of any of them are welcome, as are proofs of the individual milestones.
Display advertising is sold in two ways. Reservation contracts guarantee an advertiser a volume of impressions at a fixed price, negotiated in advance. Programmatic auctions (ad exchanges) sell impressions one at a time, efficiently, but at a price and with an allocation that the advertiser does not know in advance. Advertisers with fixed campaign budgets are risk-averse about both. Cohen, Désir, Korula and Sivan (SSRN 3088600; Management Science, doi:10.1287/mnsc.2022.4542) propose a Market-Maker contract that combines the two. A buyer pays a fixed price now, and the seller procures the unit inside the same auction. They then ask whether such a contract can help the seller without hurting anyone. This mission formalizes their main answer, Theorem 3, together with the chain of results it rests on.
A seller sells identical units. On a probability space , an outcome is a random list of nonnegative unit values. The number of units demanded is random and the values may be correlated. A buyer with demand and value contributes copies of , the paper's per-unit reduction (Assumption 2). Without a contract, the highest units win the -th price auction and each pays the clearing price , the -th highest unit value ( if at most units are demanded). Every buyer knows the law of .
Buyers are risk-averse with a common model, either mean-variance with parameter or CARA with parameter . A buyer with value who joins the auction gets
Buying the contract at price gives , resp. . A buyer opts for the contract if and ; ties go to the contract. With and the mean and variance of , the Market-Maker price is
With the contract at , the contract units are served first. The other units compete in the -th price auction for the remaining units. The seller's revenue is the sum of prices paid, the efficiency is the sum of allocated values, and the welfare is the buyers' utilities plus the revenue. denotes the top of the support of .
Assume almost surely, for every , and . Then at :
The three hypotheses of clause 3 correct the printed statement, which is false without them (counterexamples are in the goal's statement). The hypothesis includes the case where and are independent, which is the case the paper's proof treats.
Theorem 3 says the seller can add a guaranteed-price product to an efficient auction and strictly gain revenue. No buyer loses utility and the allocation stays efficient: the high-value buyers pay a risk premium that equals the value they place on removing price uncertainty. Theorem 1 is independently useful. It shows that the uniform-price multi-unit auction stays truthful for mean-variance bidders, whose preferences violate the von Neumann–Morgenstern axioms, so truthfulness in expectation does not follow from truthfulness outcome by outcome.
The paper's proofs are informal and treat and as uncorrelated, although the model allows correlated values and a random number of buyers. A formal proof establishes the theorem in the corrected form above, under no density assumption, for every market given as a random list of unit values. No part of the paper has been formalized before.
The obvious argument for Theorem 1 is that misreporting lowers the payoff in every outcome. That suffices for CARA but not for mean-variance: a misreport lowers the mean but can also lower the variance, and the utility subtracts times the variance. The proof needs the inequality between the relative drops of variance and mean (Step 2), for every law of the clearing price and both directions of misreporting.
For Theorem 3, the obvious argument "the contract buyers pay instead of the clearing price" fails in expectation when the number of contract buyers is correlated with the clearing price. The market side also needs care. One must show that the contract buyers are almost surely strictly above the clearing price, which uses Corollary 2 and the absence of an atom at . One must then show that removing them leaves the -th price unchanged, a statement about order statistics of lists with ties.
The Lean development (namespace MarketMakerAds) represents:
riskUtility, the variance written as an integral;is natural-number subtraction; the theorem proves almost surely. Theorems 1 and 2 hold for every law whose negative part has a finite second moment, and for both tie rules at the reported value.
The revenue is computed from the two-stage outcome, not defined as . The purchase rule is the utility comparison, not a threshold on . Without these two choices, clauses 1 and 3 of the goal would hold by unfolding definitions.
A complete development needs:
The list lemmas and the truthfulness results for mean-variance bidders can be reused outside this paper. Proofs of any milestone are welcome, as are alternative proofs of Theorem 1 that avoid the case split on the direction of misreporting.
A partially observable Markov decision process (POMDP) models a controller that acts on a system whose state it cannot see: it observes only signals correlated with the state. POMDPs are the standard model for planning under uncertainty in robotics, machine maintenance, medical decision-making and verification of probabilistic systems. When the controller is evaluated over an infinite horizon by its long-run average reward, the natural question is how much memory a good controller needs. A controller that must remember the whole history cannot be implemented; a controller with finitely many internal states can.
For fully observable Markov decision processes, stationary strategies are optimal for the long-run average reward (Blackwell 1962). For POMDPs, ε-optimality of finite-memory strategies was known only in special cases: belief-stationary strategies suffice in blind or ergodic POMDPs, and in general the controller's belief ranges over an infinite set. Chatterjee, Saona and Ziliotto (arXiv:1904.13360, published in Mathematics of Operations Research, 2022) prove that for every finite POMDP with the liminf-average objective and every ε > 0, some finite-memory strategy is ε-optimal.
Timeline of the inputs used here:
A POMDP is with finite state space , finite action set , finite signal set , transition function and reward function . Given an initial belief , the initial state is drawn from . At each stage the decision-maker plays an action , receives the unobserved reward , and the pair is drawn from ; only the signal is observed.
A history before stage is , and a (pure) strategy is a map . The strategy and the initial belief induce a law on plays. The long-run payoff and the value are
A strategy is ε-optimal if . It has finite memory if it is generated by a finite-state transducer: a finite set , an initial memory , an action map and an update map , with and .
For every finite POMDP , every initial belief and every ,
No bound on the memory size is part of the statement; by Remark 2.10 of the paper, none exists in terms of the data of .
The theorem shows that long-run average POMDPs, unlike their limsup counterparts (Proposition 3.4 of the paper), can be approximately solved by finite controllers. Two consequences are drawn in the paper: approximating the long-run value is recursively enumerable (Corollary 3.2), and the value is lower semicontinuous in the transition function (Corollary 3.10), so ε-optimal finite-memory controllers are robust to small model errors (Lemma 3.9).
The result is proved, in a published paper. No machine-checked proof of it, or of its inputs from Venel and Ziliotto, is known. A formalization adds a Lean development of POMDPs with history-dependent strategies built on Mathlib's Ionescu-Tulcea construction, of beliefs and Bayes updating, of invariant measures on the belief simplex, and of the super-support construction.
The obvious approach is to play an optimal strategy and remember only the current belief, or a finite approximation of it. This fails: the belief takes infinitely many values, an optimal strategy need not be a function of the belief, and finite-recall strategies are not enough in general (Proposition 2.12). Remembering the support of the belief is not enough either (Example 4.5): the controller must remember from which value class of initial states the current mass came, which is what the super-support records.
The second difficulty is the passage from almost-sure ergodic behaviour of a strategy that is not finite-memory to an expected-payoff bound for a block strategy, which needs a uniform block length over the finitely many reachable super-supports and an exact accounting of mass through the blocks (Lemmas 6.8 and 6.9). The input Lemma 5.3 rests on the uniform convergence of and on the invariant-measure lemma of Venel and Ziliotto, which are proved in another paper and are milestones here.
PMF (K × S), a joint law of next state and signal with no positivity assumption; takes values in . Beliefs are stdSimplex ℝ K.Kernel.trajMeasure on ℕ → PlayStep A S K, where coordinate is and coordinate carries . Histories are chronological lists; strategies are functions List (A × S) → A on histories of every length; Lean stages are indexed from .∫ or ⨆.rep of representative histories.Reusable parts: the POMDP play law, beliefs and Bayes updates, and the theorem that a finite-memory strategy's expected averages converge (a finite Markov chain ergodic argument). Proofs of any milestone are welcome, as are proofs of the Venel–Ziliotto inputs from their own source.
Stochastic first-order methods minimize a smooth, strongly convex function on using only noisy gradients . Most analyses of accelerated stochastic methods assume an oracle with uniformly bounded variance, . Least-squares regression violates this outside a compact domain: its noise grows with . A weaker and more realistic assumption is the growth condition , with a multiplicative part and an additive part .
Chen, Na and Kolar (arXiv:2006.06782v4; Mathematics of Operations Research, 2024) analyze four accelerated methods under this condition. Nesterov's method, the robust momentum method and implicit DAM+ keep the accelerated rate only for small (for instance ). The accelerated dual averaging method DAM+ keeps it for every , and with a two-phase tail-averaging schedule nearly attains the lower bound , where .
means: is continuously differentiable and for all
with ; is the unique minimizer. On a probability space with filtration , the gradient queried at is -measurable and the noise satisfies and .
Given positive weights with , step sizes , and the regularizer with conjugate , DAM+ is
The first equation is implicit, since contains . The schedule fixes , and a parameter : while and afterwards, , and the output is the tail average , where puts all mass on in the first phase and averages the second-phase iterates uniformly.
Write , and .
Three clauses, for every , and :
depends only on ; also on ; on the instance. Clause (C) is the printed (5.12).
Lemmas 2.1 and 2.2; the unique minimizer; the closed form (4.7) of ; Lemmas 4.1 and 4.2; the inequalities (4.13)–(4.16); two moment-bound statements; the error recursion of Theorem 4.1,
for the duality-gap potential ; its specialization in the proof of Theorem 5.1; Proposition 5.1 for the abstract recursion ; and the Jensen step.
Theorem 5.1 shows that, with a schedule that does not depend on a horizon, acceleration survives arbitrarily large multiplicative noise: in the first phase the bias decays at rate , with of order for fixed ; in the second phase the bias tail is and the variance term is within a factor of the statistical rate . This separates DAM+ from Nesterov's method, whose rate degrades as , and justifies its use for least-squares-type problems.
The result is proved in the paper and is not formalized anywhere. The mission adds a machine-checked version and pins down the statement. Two printed details are false: the weight condition cannot hold at , and the printed fails at (for , and noiseless gradients, ). The goal states what does hold. The definitions (the class , the conditional growth condition, DAM+ runs, the tail-averaging schedule) are reusable for other stochastic accelerated methods.
The obvious route is to cast DAM+ as the recursion (5.2) and solve it, as the paper does. That fails in three places. At the weight ratio is , so the recursion starts at from a bound on . When , the second-phase rate exceeds on finitely many steps, where (5.2) is not available; those steps need separate moment bounds, uniform over the instance. And the expectations require integrability of , and , which must be derived from the implicit update and the conditional noise model. The stochastic part also needs , which uses that depends on only through a -measurable quantity.
The space is EuclideanSpace ℝ (Fin d) for every . Sequences are indexed by with index 0 unused. is a real supremum; it is finite for and evaluated at only at . A DAM+ run is a family of sequences satisfying the equations at every outcome, not a recursive definition. The noise model is the conditional form (2.5) with integrable ; the initial point may be random with finite second moment. The weight ratio is imposed for ; need not be an integer; is allowed. Expectations are Bochner integrals, made genuine by the integrability milestone. is replaced by explicit constants valid for all , with chosen before and the instance, so the statement cannot be met by an instance-dependent constant in the first phase.
Welcome contributions: the closed form of the quadratic conjugate, the measurability of the implicit update, the conditional-expectation steps of Theorem 4.1, and the deterministic recursion bounds of Proposition 5.1, which are reusable for other two-phase schedules.
Newspapers, magazines, newsletters and data feeds sell information goods whose value decays with time. A publisher that releases often sells fresher content but pays a fixed publication cost for every issue; a publisher that releases rarely saves on costs but sells staler content. For a monopolist this is an EOQ-type trade-off. With competition, the frequency of publication becomes a strategic variable: a daily and a weekly covering the same events are imperfect substitutes, and customers may buy both.
L. Chen and G. Roels (SSRN 3986163, INSEAD Working Paper 2021/74/TOM, 2021; published in Manufacturing & Service Operations Management, 2024, doi:10.1287/msom.2023.0024) model two ex-ante identical publishers that first choose publication cycles and then compete on price. Their headline result, Theorem 2, is that identical firms choose different frequencies in equilibrium, and that the faster one earns more. This mission formalizes that theorem. All theorem, equation and page numbers refer to the 2021 SSRN working paper, not to the MSOM version of record.
Information arrives at rate and decays linearly at rate . The undecayed information accumulated over periods is
where is the per-period value of a publication with cycle of which a fraction is new to the reader. Each issue costs , and throughout .
Pricing game. Firm 1 is the fast publisher with cycle , and the slow cycle is with . At prices , homogeneous customers buy a fraction of the fast firm's issues and of the slow firm's, with utility
They choose by exact maximization over , except in one region where the paper uses a first-order approximation (its eq. (7)). The weekly choice is , with ties going to the weekly. Profits are and . A mixed equilibrium of this game is a pair of price distributions under which every price in a firm's support earns the same expected profit and no price earns more.
Publishing game (10). Each firm chooses a cycle , either equal to its rival's or differing from it by a factor of at least , to maximize its anticipated pricing-equilibrium profit . These payoffs are the paper's closed-form equilibrium profits: Lemma EC.5 when both cycles satisfy , (EC.3) when , (EC.48) when , and on equal cycles.
There are cycles solving
such that the equilibria of (10) are exactly and , and .
The theorem shows that frequency differentiation arises without any ex-ante asymmetry between the firms. Identical firms that published at the same frequency would face Bertrand competition on undifferentiated content and earn . Separating their cycles gives each firm a market segment. The equilibrium cycles are strategic substitutes, and both are longer than the monopoly cycle (Proposition 1). Because the fast firm earns more, there is a first-mover advantage to committing to frequent publication. The paper's comparative statics in and (Propositions 2–4) and its extensions with differentiated content (Theorem 3) all build on this characterization.
The result is proved on paper, but the proof is not complete. The paper derives Theorem 2 as the case of Theorem 3, whose proof checks five classes of deviations over eight pages. It states that uniqueness "can be shown by a similar logic" and omits the details (p. ec28). A formal proof would supply the uniqueness argument and would check the many regime boundaries of the piecewise payoffs. To our knowledge no part of this paper has been machine-checked.
The payoffs are piecewise: three regimes for each firm (both cycles short; fast short and slow long; both long), and inside the middle regime two further branches with boundaries that depend on both cycles. Checking that the equilibrium is an equilibrium means checking every feasible deviation. These include deviations that switch roles, such as the slow firm undercutting to a cycle at most half the fast firm's, or the fast firm jumping to at least twice the slow firm's. Uniqueness requires excluding every other profile, including symmetric ones, in every regime.
The obvious first step, solving the first-order conditions of each firm's payoff, gives (11) but proves neither part. A first-order point is not a best response once the deviation crosses a regime boundary, and the feasible set is not an interval: it is . The milestone lemmas on the pricing game need expected profits against price distributions with an atom, that is, integrals of piecewise rational functions. They also need an argument that no pure equilibrium exists in a game whose demand function is discontinuous.
All declarations live in the namespace PubFrequency. The parameters are real numbers with , and on every theorem. Choices that the formalization fixes:
deriv. The approximation (7) is , with the largest minimizer over the real interval (footnote 9). Ties: the weekly first, then more dailies.Defining the equilibrium of (10) by (11), or the equilibrium payoffs by (EC.6), would make the goal an identity. Neither the game nor its payoffs mention (11). Lemma EC.1 of the paper (the exact customer choice when ) is false as printed; a counterexample is , , . It is not used: the pricing game is defined from (3), (4), (7) and (8) directly.
Contributions are welcome on the existence half of the goal (the deviation cases (i)–(v) of pp. ec22–ec28 at ), on uniqueness, on the one-variable inequalities behind Lemma EC.6 and , and on the mixed-equilibrium computations of Lemmas EC.2 and EC.5. A reusable library for expected payoffs of price distributions with atoms would also serve other price-dispersion models.
In a two-tier supply chain a retailer orders from a supplier, and the supplier must forecast those orders. If the retailer shares its demand data, the supplier forecasts with full information. If not, the supplier sees only the order stream. A large literature (Lee, So and Tang 2000; Gavirneni, Kapuscinski and Tayur 1999; Giloni, Hurvich and Seshadri 2014) asks when sharing has value and how large that value is. Caldentey, Giloni, Hurvich and Zhang (SSRN 4319721, version of January 20, 2024; published in Mathematics of Operations Research, 2024) answer this for an i.i.d. Gaussian demand and arbitrary linear ordering policies. They compute the entire efficient frontier between the retailer's inventory variance and the supplier's forecast error, both with and without sharing.
Timeline of the problem as the paper presents it:
Demand is , where is Gaussian white noise with variance . The retailer orders . The policy is a real sequence in the set
Its z-transform is on the unit disk. The boundary value is the radial limit .
Let , with Taylor coefficients . Assumption 2 requires .
The two efficient frontiers are the infima
for every and . The goal is stated on the explicit problem (26). It is not stated through any factorization.
Theorem 2 gives the exact price of withholding demand information. For the two frontiers coincide, so sharing has no value there. For the ratio tends to infinity as . Combined with linear cost weights, this yields the paper's thresholds for when a retailer should share (§7.3). Proposition 6 measures the value of sharing for any single policy: it is the squared modulus of the inner factor at the origin.
The results are proved in the paper. None of them, and none of the Hardy-space theory they use, has a machine-checked proof on the platform. Mathlib has Fourier series on the circle, Parseval's identity and Abel's limit theorem, but no Hardy spaces, outer functions, Blaschke products, singular inner functions or Smirnov–Beurling factorization. A formalization of the goal therefore checks an optimization result whose proof combines time-series modelling, complex analysis and convex optimization. It also leaves reusable Hardy-space infrastructure behind.
The obvious approach optimizes over the coefficients directly. It fails because is not continuous in (p.20): Kolmogorov's integral sees only on the circle and ignores the zeros inside the disk. The problem must instead be decomposed by the inner–outer factorization. The inventory variance then depends on the Blaschke and singular factors through a boundary integral with a pole at , which the residue theorem does not handle directly (§9.7 Step 1). Finally, the infimum is not attained for . The limiting policy carries a singular inner factor and violates the forecast constraint. The upper bound therefore needs an approximating family (Proposition 3) and a continuity argument in .
limUnder along ). The integrand of (26) is written , which equals for real coefficients.sInfs of sets of attained values. These sets are nonempty and bounded below by . The goal is not a statement about a minimizer.A trivializing encoding would be an empty feasible set, for which sInf ∅ = 0. It is ruled out because the policy satisfies Assumption 2 and is feasible for every .
The infrastructure is reusable well beyond this mission:
Contributions to any of these are welcome, as are self-contained proofs of the milestones (Theorem 1 and Lemma 8 need no Hardy-space theory).
Contingent convertible bonds (CoCos) are bank debt that converts into equity when the issuing bank is in distress, so that the bank is recapitalised without a default (Avdjiev, Kartasheva & Bogdanova 2013). A trigger based on the bank's own stock price is transparent and fast, but circular: the stock price depends on whether the debt converts, and whether it converts depends on the stock price. Sundaresan & Wang (2015) observed that with such a trigger neither existence nor uniqueness of an equilibrium stock price is guaranteed, and this concern is cited as the main reason stock price triggers have not been used in practice. For a single bank, Glasserman & Nouri (2016) and Pennacchi & Tchistyi (2019) gave sufficient conditions for existence and uniqueness.
Balter, Schweizer and Vera (arXiv:2011.06474, later in Mathematics of Operations Research, 2023) ask the same question when banks hold each other's CoCos, so that one bank's conversion changes the assets of the others. This mission formalizes their existence theorem for the case where every bank sets a fair or super-fair threshold.
There are banks . Bank has assets net of liabilities and convertible debt . If its stock price is at most its conversion threshold , the debt is not paid back but converted into new shares (the original number of shares is ). The fraction of bank 's convertible debt held by bank is , with and ; such a pair is called admissible.
Each price vector determines a partition of the banks into bankrupt , converting and healthy . The pair is a -equilibrium when the partition is the one read off and
Writing for with the entries outside set to zero, these equations say with
where is the partition read off . Thresholds are fair if , super-fair if , and sub-fair if . Assumption 1 is that is invertible.
For every admissible with invertible, thresholds and credit amounts with for all ,
No constant is fixed; the statement covers every , every network and every fair or super-fair choice of thresholds.
The result. With interbank holdings, the map from prices to assets is piecewise affine with pieces, and the paper shows that existence of equilibrium is decided by the thresholds alone: with sub-fair thresholds there are asset vectors with no equilibrium at all (Proposition 1, not part of this mission), while with fair or super-fair thresholds an equilibrium always exists, although it may not be unique. For a regulator this is a design rule: a CoCo with a stock price trigger set below the fair level can leave the market without any consistent price. The fair case is also formally close to the Eisenberg–Noe clearing model, so tools transfer between the two.
Formalizing it. The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified existence theorem for a nonsmooth, discontinuous equilibrium map, a Lean statement of the Poincaré–Miranda theorem on , and sign results for inverse M-matrices of the kind that recur in network and Leontief models.
In the fair case is continuous, monotone in the right directions and tends to along the diagonal, so a Poincaré–Miranda argument gives surjectivity. In the super-fair case ( for some ) this route fails: the map jumps by when bank 's price crosses its threshold upwards, so it is neither continuous nor injective, and degree or fixed-point arguments do not apply directly. The paper instead views the super-fair map as the fair map shifted by vectors depending on which banks are healthy, and reduces existence to a fixed point of a set map on subsets of banks. That is not monotone, so Tarski's theorem does not apply. Its iterates only oscillate between bounds that tighten, and the proof that the oscillation stops rests on Lemmas 3 and 4. These in turn need the inverse of the fair map along a segment, its piecewise-linear structure, and the sign pattern of .
Banks are Fin n; vectors are Fin n → ℝ; W : Matrix (Fin n) (Fin n) ℝ with W i j (holder , issuer ), so the admissibility condition bounds column sums. is restrictTo F v. The partition is read off with strict inequalities for bankrupt and healthy and closed bounds for converting. Phi m W l c is for credit amounts c: the fair map is Phi m W l (m * l), the super-fair map is Phi m W l c with c i / m i ≤ l i. is Hfair, built from Function.invFun of the fair map. It is meaningful because that map is bijective (Proposition 4), and every statement using it assumes an admissible network and 0 ≤ l. Assumption 1 is IsUnit (1 - W).
All statements assume . The paper uses this tacitly when it states that the price regions partition ; without it the regions overlap and the fair map is discontinuous. Credit amounts in the goal and in Lemma 1 may have any sign. Lemma 5(b) and the diagonal-dominance milestone are stated for arbitrary, possibly overlapping , . Assumption 1 is carried by Lemmas 2, 4, 5(a), Corollary 1 and Theorem 1. The paper imposes it throughout its §3.3, but Lemma 3, the p.19 identity and Lemma 5(b) are stated here without it, which is more general; their proofs do not use it. The goal cannot be satisfied trivially: the admissibility hypotheses are satisfied by concrete networks, and both conclusions are nontrivial for with super-fair thresholds, where is discontinuous.
A complete development needs Poincaré–Miranda (from Brouwer's theorem on the cube, which is proved on the platform as Plasticity.Ext.Brouwer), continuity and invertibility of piecewise-affine maps, and M-matrix sign results. The Poincaré–Miranda theorem and Proposition 2 are reusable beyond this mission. Proofs of any milestone, and alternative routes to Lemma 2 such as a direct combinatorial argument on , are welcome.
A clutter is a family of subsets of a finite ground set none of which contains another. A clutter is ideal if its set covering polyhedron has only integral vertices. It packs if the largest number of pairwise disjoint members equals the smallest number of elements meeting every member. Ideal clutters and clutters with the packing property are central objects in combinatorial optimization. The Replication Conjecture of Conforti and Cornuéjols (1993) and the question of which ideal clutters are minimally non-packing are both long open in general.
Abdi, Cornuéjols, Guričanová and Lee (Cuboids, a class of clutters) attached to every set a clutter, its cuboid, and translated idealness and packing of cuboids into geometric properties of . The paper formalized in this mission, Resistant sets in the unit hypercube (LSE Research Online 102397, accepted manuscript of October 28, 2019; published in Math. Oper. Res. 46(1), 2021), studies one large class of such sets, the resistant sets. Their cuboids are ideal. The paper proves the Replication Conjecture for these cuboids and classifies the resistant sets whose cuboids are ideal minimally non-packing and have the largest possible number of members.
In the cuboids paper, 745 strictly non-polar sets of dimension at most 7 were enumerated, 74 of them half-dense. The infinite family and the sporadic set stood out among them. Theorem 1.17 of the paper shows that, among resistant sets, these are the only half-dense examples.
A point of the cube is a string , and is coordinate-wise addition modulo 2. Fix . Its points are feasible and the other points infeasible. Twisting by a point gives . A minimal point of a set is a point of inclusion-minimal support.
The sets of the classification use the reflective product :
where . For example .
In the Lean development a point is Fin n → Bool, a set is a Finset (Fin n → Bool), and the predicates are IsResistant, IsPolar, IsStrictlyNonPolar, IsHalfDense, IsIso and HasRestriction; the sets are Rk1 k and R5.
For every and every ,
The paper states this as " are, up to isomorphism, the only half-dense strictly non-polar sets that are resistant". Both directions are part of the goal.
Theorem 1.17 answers Question 7.4 of the cuboids paper for cuboids of resistant sets. By Theorem 1.15 of the paper, a resistant set is strictly non-polar exactly when its cuboid is an ideal minimally non-packing clutter. So the theorem lists every ideal minimally non-packing cuboid of a resistant set that has the maximum number of members. The paper also uses it to decide when a reflective product of resistant sets is strictly polar (Theorem 1.18).
The intermediate results are reusable on their own:
The paper's proofs are complete and refereed. No part of them has a machine-checked proof that this mission knows of. The mission asks for proofs of the published statements, not for new results.
The "if" direction is a finite statement for each . It is uniform in , however, and strict non-polarity of quantifies over every proper restriction of a cube of dimension . So it cannot be settled by enumeration.
In the "only if" direction, half-density and non-polarity bound the straight infeasible paths. The difficulty is to turn that local information into a global description of . The obvious approach, induction on through restrictions, does not work directly: strict non-polarity is not inherited by restrictions, and resistance alone allows many configurations. The paper instead fixes a longest straight infeasible path, closes it into a circuit of length by Path Propagation, and analyses the feasible points next to the circuit coordinate by coordinate. The rerouting argument of Lemma 5.2 and the five-case induction of Lemma 5.4 are long case analyses on 3- and 4-dimensional subcubes, and they are the bulk of the work.
Conventions:
Fin n → Bool with false for . The paper's coordinate is the index , and coordinate is lastCoord n _.Finset. Half-density is written .ι : Fin m ↪ Fin n of kept coordinates and the values of the others. The kept dimension satisfies , and a proper restriction has . The restriction that fixes nothing (the set itself) counts, as in the paper.Allowing -dimensional restrictions would trivialize the goal: the empty set in dimension is non-polar, so no set with an infeasible point would be strictly non-polar. The dimension bound rules this out.
Everything is built on Mathlib's Finset and finite function types; no external library is needed. The definitions (twisting, restrictions, minors, isomorphism, polarity) are reusable for other results of the cuboids paper and of this paper, such as Theorems 1.13–1.15 and 1.18. Contributions are welcome at every level: proofs of the milestones, decidability instances and lemmas that reduce small-dimensional cases to computation, and lemmas on twisting and restriction that the proofs use repeatedly.
Ride-sharing platforms match passengers who request rides at different times and places. Three features of that problem are hard to separate: two passengers far apart yield a poor match, two requests far apart in time cannot be matched at all, and the platform does not know future demand. Ashlagi, Burq, Dutta, Jaillet, Saberi and Sholley (arXiv:1808.03526v1, published in Mathematics of Operations Research, 2023, as Edge-Weighted Online Windowed Matching) reduce these features to a graph matching problem on an arbitrary, not necessarily bipartite, graph.
The classical online bipartite matching literature takes : a vertex must be matched on arrival. Emek, Kutten and Wattenhofer (STOC 2016) and Huang et al. (STOC 2018) study delayed decisions in other models. The present model fixes a uniform deadline, and the weights are arbitrary.
A weighted graph has vertices and weights on undirected pairs. Vertices arrive one per period, vertex in period , and the Adversarial Order setting assumes . The weight of a pair is observed only when its later vertex arrives.
For a deadline , the online graph keeps the edge exactly when . Vertex becomes critical at period : the algorithm must match it then or let it depart. The benchmark is the maximum weight of a matching of . A randomized online algorithm is -competitive if its expected total weight is at least .
Postponed Greedy (PG, Algorithm 3) gives each vertex a virtual seller with price and a virtual buyer . On arrival, bids once on the seller of largest margin . If the margin is positive, becomes the tentative match , displacing any earlier buyer, and rises to . The maximal margin is . When becomes critical with , a fair coin decides 's status if it is still undetermined. A seller finalizes and collects , and in either case receives the opposite status.
The theorem is stated for every , every , all and every tie-breaking rule for the , as four clauses. Every finalized pair is an edge of , for every outcome of the coins. The finalized pairs are vertex-disjoint, for every . The expected reward satisfies
And the state after periods depends only on the weights among vertices arrived by then and on the coins of vertices already critical.
The proof of Theorem 3.3 uses no numbered result, so the milestones are its unnumbered claims, in proof order.
The result. Theorem 3.3 gives a constant competitive ratio for matching on arbitrary graphs with arbitrary non-negative weights and an adversarial arrival order. The paper's Figure 1 shows that no deterministic algorithm achieves a constant ratio, and the paper shows that no algorithm exceeds . The same algorithm underlies the paper's extension to stochastic departures.
The formalization. The theorem is proved in the paper, and at the time of writing no machine-checked proof exists on this platform. The mission produces an executable-style specification of a randomized online algorithm, with the word "online" as a theorem clause, not a comment. It also produces a primal-dual argument for general-graph matching in the shape used by auction-style online algorithms. Weak duality for vertex potentials (milestone 10) is stated for every finite simple graph.
The obvious approach, assigning each vertex a seller or buyer role by an independent coin, loses a factor on each edge and gives only (Corollary 3.2). Postponed Greedy gains the factor by correlating the roles along paths of the virtual -matching.
That correlation is the central difficulty. Whether is a seller is not one coin: it is the coin at the head of 's path, flipped once per step along the path, and which vertices form that path depends on prices set after arrived. The claim "with probability exactly " (milestone 4) needs the path structure to be independent of the coins (milestone 1), and it fails for a vertex with no final match. A vertex with no match is never a seller, which the proof's sentence leaves implicit, so milestone 4 is stated only for matched vertices.
Two further points are easy to get wrong. A buyer displaced from a seller never bids again, so the tentative matching need not be a maximum-weight matching of the virtual graph. The price of a seller rises while the seller is present, and the dual constraint for reads the price at the moment arrives, so the constraint at the final prices needs monotonicity (milestone 8).
Vertices are Fin n, 0-based: vertex arrives in period and becomes critical in period . Weights are v : Sym2 (Fin n) → ℝ. The run is a fold over the periods , with the arrival processed before the criticality within a period. Both choices are forced: processing criticality first makes the theorem false on , , and stopping at period collects nothing on , . Margins read onlineWeight, which is off the edges of the online graph, so the seller has margin for . Coins are ω : Fin n → Bool, uniform, and the expectation is . The benchmark reuses the published ProphetMatchingEFGT.optWeight, a finite maximum over matchings of a SimpleGraph.
The tie-breaking rule is a free parameter of the theorem, restricted to choose a maximizer and to see the arriving vertex, the seller set and the margins, but no coin. The reward is a sum over the finalized pairs, not the quantity , and the benchmark is on and on no other graph. Each of these excludes a trivializing reading.
A complete development needs invariants of the state machine and no theory beyond Mathlib: finite sums, Finset and Sym2 manipulation, and counting on Fin n → Bool. Milestone 10 is reusable beyond this mission. Contributions to any milestone are welcome, in any order.
In a coordination game on a graph, every player is a node and chooses a colour, and a node is rewarded for agreeing with its neighbours. These games model the adoption of a common standard, clustering, and the stabilisation of distributed protocols. When the graph is directed, the dynamics change sharply. A node is paid only by its in-neighbours and pays nothing back. Nash equilibria may fail to exist, and even on a single directed cycle, improvement dynamics can cycle forever. Apt, Simon and Wojtczak (arXiv:1910.02693v2, published in Mathematics of Operations Research, 2022) study when, from every starting configuration, some short sequence of profitable unilateral moves reaches a Nash equilibrium. Their two main graph classes come from networking. Simple cycles model token rings. Open chains of cycles model Ethernet ring protection (ITU-T G.8032), in which rings are joined in a sequence and consecutive rings share a single node.
Timeline:
Fix a finite set of colours. A coordination game is given by a directed graph on a finite vertex set without self-loops, a positive weight on each edge, a colour assignment giving every node a non-empty set , and bonuses . A joint strategy picks for every node, and the payoff of node is
where is the set of in-neighbours of . Unless stated otherwise, graphs are unweighted () and there are no bonuses ().
A node plays a best response if no colour in gives it a higher payoff. A Nash equilibrium is a joint strategy in which every node plays a best response. An improvement step changes the colour of a single node to one that strictly increases that node's payoff. A game ensures improvement paths of length at most if from every joint strategy there are , , all improvement steps, with a Nash equilibrium.
A simple cycle is . An open chain of cycles , each with nodes, has cycles . For the node coincides with the node of the next cycle, for some . No other nodes coincide, so the chain has nodes.
For every open chain of cycles with nodes each, every choice of the attachment positions , every colour set and every colour assignment with non-empty colour sets, the unweighted coordination game without bonuses on the chain satisfies
The result shows that on open chains of directed cycles, which lack the finite improvement property, short improvement paths always exist. Their length is polynomial in both the ring size and the number of rings. In particular a Nash equilibrium always exists and can be reached by local, one-node-at-a-time improvements, which is the kind of guarantee a distributed protocol needs. The same construction underlies the paper's polynomial-time algorithm for finding a Nash equilibrium on open chains and its bound for coalitional improvement paths (Theorem 23).
Formalizing it adds to the platform coordination games on directed graphs, improvement paths with a length bound, and the open-chain graph class. None of these are on the platform today. The results are proved in the paper. None of them has a machine-checked proof.
Status of the printed proof. A check of Lemmas 12 and 14 (pp.17–20, Appendix pp.35–39) found that both fail for some attachment positions. Lemma 12 claims that one round of Algorithm 1 on changes only the grades of , and Lemma 14 claims that increases in every round. When , the node is the link node , so recolouring can change the grade of . A concrete chain with , , , has a round of Algorithm 1 in which drops from to . These two lemmas are therefore not milestones. Theorem 15 itself is not contradicted: exhaustive search on small chains found improvement paths well within . A complete proof needs a repaired progress argument or a different one.
The obvious argument fails at the start. Scheduling the nodes round-robin does not terminate on a directed cycle, since a colour can chase itself around the ring forever (Example 2, p.10). Even the cycle bounds need a specific schedule and a specific choice among best responses. On an open chain, repairing one cycle recolours its link nodes and can destroy the equilibrium of the neighbouring cycles. The index of the lowest broken cycle can therefore move down by an arbitrary amount (Figure 9, p.19). Termination needs a progress measure that increases at every round despite this back-and-forth, and the attachment positions and let a single repair reach two cycles away.
A joint strategy is a function with . Payoffs are real. An improvement path of length at most is a list , , of joint strategies in which each step changes exactly one node's colour to a colour in its set and strictly raises that node's payoff, and whose last element is a Nash equilibrium. Length counts steps. Simple cycles live on Fin n with edges and . An open chain is a structure with , , a surjective naming map from Fin m × Fin v onto , attachment positions with , the link identifications, and nothing else identified. Its edges are exactly the cycle edges. The game on an open chain is unweighted and has no bonuses, as in the paper. Weighted open chains are outside this paper (p.34).
Non-empty colour sets are hypotheses everywhere. Without them there is no joint strategy and every statement would be vacuous. Improvement steps require a strict gain, so constant paths do not count.
The development needs the general strategic-game notions (best response, Nash equilibrium, improvement steps and paths, schedules), coordination games, simple cycles and open chains, and, for the milestones about Algorithm 1, the link bonuses , grades, , , , the measure and one round of the algorithm. The strategic-game layer is reusable for any finite game. Contributions are welcome on the cycle theorems, on a repaired progress measure for open chains, or on any other proof of Theorem 15.
Spare parts, slow-moving retail items and humanitarian relief stock share a demand pattern: most periods see no demand, and a demand arrives only now and then. Planners of such long-tail or intermittent-demand items estimate the inter-arrival distribution from a finite observed history and feed it into an inventory policy. Bi, He and Teo (MSOM 2023) observe that this estimate is biased in a precise, computable way, for the same reason as the "hot hand" selection bias of Miller and Sanjurjo (Econometrica 2018): in a finite sequence of independent trials, the expected proportion of successes that immediately follow a success is strictly smaller than the success probability.
Timeline:
Time positions are . A demand arrival occurs at position by assumption, and at each of the positions independently with probability ; write and for the arrival indicator, so .
For a gap length , the empirical proportion is the number of positions with , , and , divided by the number of arrivals at positions . The denominator is at least because of the arrival at . The biased estimate is
and the relative bias of the estimate of is
In Lean, a sample path is ω : Fin n → Bool, the arrival indicator is arrival ω t, is empiricalGap n j ω, and is biasedEstimate n j p, the weighted sum of over the paths with weights .
For every , the map is strictly decreasing on ; and for every , the map is strictly decreasing on :
The printed proposition says "for all ". At the estimate is unbiased (, so ) and the relative bias is for every , which is not strictly decreasing in and is smaller than its value at (so part (ii) fails at under any reading). The goal is therefore stated for , the range in which the proof (which divides by ) works. "Decreasing" is read as strict, which is what the proof gives.
The printed theorem lacks the last term; without it the formula fails at (for , , : , while the printed sum is empty). 2. EC.2.2 (i), derivative. With and ,
The printed chain asserts a strict "" in (EC.2); the two sides are in fact equal (both are at , ), and the milestone states the equality. 5. Last inequality of EC.2.2 (ii). , strictly when .
Proposition 2 explains why the finite-horizon effect matters most for long-tail items: the relative under-estimation of the arrival probability is largest when is small and the observation window is short. In the paper this drives the inventory results of §4: the delay of the delay-ordering policy chosen with the biased estimates, and the staggered base stock policy. Theorem 2 makes the bias computable exactly rather than by simulation.
On the formalization side, nothing in this mission has a machine-checked proof yet. The work is to formalize the paper's argument: the path-counting identity behind Theorem 2 (summing over Bernoulli paths), a derivative computation, and two strict Cauchy–Schwarz type bounds for binomial weights. The definitions of the empirical proportion and the expected estimate are reusable for other results on streaks and the hot-hand selection bias.
The main step is Theorem 2: converting an expectation of a ratio of two random counts into a binomial sum. The obvious route, linearity of expectation, fails because the denominator (the number of arrivals) is random and correlated with the numerator. The paper conditions on the number of arrivals among periods and counts the positions where a gap of length can sit, including the gap that closes exactly at the horizon. That case split is where the printed formula loses the term.
The monotonicity steps are elementary but require strictness throughout: both (EC.1) and the last inequality are of the form , and they are strict only because the binomial variable is non-degenerate for and .
Fin n → Bool for the periods ; the arrival at position is built into arrival, so the denominator of is at least for by construction, not by hypothesis.StrictAntiOn, on Set.Ioo 0 1 in and on {n | 2 ≤ n} in .Welcome contributions: a proof of Theorem 2 by induction on or by conditioning on the number of arrivals; general lemmas on sums over Fin n → Bool against product Bernoulli weights; and the strict inequality for non-degenerate binomial .
Electric utilities run demand-response programs to cut peak load during supply shortages: when an event is called, a participating customer is paid a rebate for every unit by which its consumption falls below a baseline. The utility sees consumption, not demand, so the baseline is its estimate of what the customer would have consumed without the event. In practice the baseline is the customer's average historical consumption in non-event periods (the "normal-use" baseline used by PEPCO and BG&E). This creates a measurement problem. A customer whose demand happens to be low is paid for reductions it never made, and a customer whose demand is high has to cut a lot before it is paid anything.
Agrawal and Yücel (Management Science, 2022, doi:10.1287/mnsc.2021.4278) model this as a game between a utility and its customers. They ask how the utility should set the baseline and the rebate, and whether moving the baseline away from normal use helps or hurts the environment. Their headline finding is that the cost-optimal baseline can reduce the actual demand reduction and raise emissions, against the intuition that paying more effectively must buy more reduction. This mission formalizes that finding, Proposition 4 of the authors' manuscript of May 26, 2021, together with the chain of results it rests on.
Peak demand in an event (probability ) is , uniform on . Without an event it is , uniform on with . Off-peak demand is uniform on . The utility buys power at marginal cost in an event and otherwise, and .
Given a baseline and a rebate , a customer with demand shifts units to the off-peak period. Its consumption is , the estimated reduction is , and the customer maximizes
A best-response selection picks a maximizer for every . The utility's expected net cost savings are
and its total cost is with independent of . The expected actual demand reduction is . Total expected emissions are , with emission intensities and . Two regimes are compared:
The firm inflates the baseline if and deflates it if .
For and there are thresholds , depending only on , such that
and the same with total emissions in place of , with the inequalities reversed. The goal pins the thresholds down: with the root of in , and when , or the root of an explicit equation in otherwise.
The result separates two things a regulator might expect to move together. Optimizing the baseline always raises the utility's savings. Proposition 4 says exactly when it also lowers the actual reduction of peak demand, and with it the environmental benefit that motivates these programs. For a large cost gap the inflated baseline comes with a lower rebate, and the lower rebate dominates. For a small cost gap the deflated baseline comes with a higher rebate, and the reduction rises. The thresholds are explicit functions of the model's primitives, so the regions can be located for any calibration, such as the Maryland one of the paper's Figure 3.
The paper proves the result by hand through a case analysis over the quadrant. Machine-checking it fixes several printed details that the formal statements had to correct. The emissions clause compares the emissions reduction where total emissions are meant. The proof's switches form at instead of . One display of Case 3 has the wrong sign. Three clauses of Proposition 1 fail at boundary cases. Each correction is recorded on its item with a counterexample. None of these results has a machine-checked proof yet.
The customer's objective is the maximum of two parabolas. It is not concave, so the best response jumps with , and ties occur at isolated demand levels. The firm's objective therefore has different closed forms on several regions of the quadrant, separated by curves such as , and . The maximum has to be global over all of them. The natural approach, setting the gradient to zero on the region that contains the paper's optimum, does not certify a global maximum. For the savings are constant along the ridge , so the maximizer is a curve rather than a point. The comparison of with then needs single-crossing arguments between a polynomial and a square-root expression, and the threshold changes form with .
All quantities are real numbers. Expectations are interval integrals with the uniform densities written out, and the two-period expectations are iterated integrals. The customer's best response is an arbitrary selection s : ℝ → ℝ → ℝ → ℝ with IsBestResponse, never a closed formula. Selections differ only on null sets, so every expectation is the paper's. The firm's domain is , , and the customer's feasible set is . Optimality of and of is defined by maximizing . The closed forms are milestones, not definitions. integrates the density only up to , and is a set integral over , so both make sense for .
Defining , or by their closed forms would make the goal a statement about formulas rather than about optimization, and placing the threshold quantifiers after would make the equivalences empty. The statements do neither.
Mathlib's interval integrals, Real.sqrt and max are the only infrastructure needed. Proofs of any milestone are welcome, as are alternative proofs of the firm's global optimum that avoid the full case analysis.
Many combinatorial optimization problems ask for a maximum-weight set that is "independent" in two different senses at once: a bipartite matching is a set of edges that uses each left node at most once and each right node at most once; a branching in a digraph is a forest that enters each node at most once. Each of these is a common independent set of two matroids. Edmonds (1970) showed that the weighted version of this problem has a clean linear description: the convex hull of the common independent sets is cut out by the rank inequalities of the two matroids. The result is one of the central examples in polyhedral combinatorics, and Chapter 8 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), proves it in §8.5 with the tools of Chapter 6 (integral polytopes and total dual integrality).
Timeline:
A matroid is a finite set with a family of subsets, the independent sets, such that , subsets of independent sets are independent, and for every all maximal independent subsets of have the same size. That size is the rank . For the characteristic vector has on and elsewhere, and .
Given two matroids , with rank functions , the matroid intersection system is
Its linear-programming dual for an objective is
A rational system is totally dual integral (TDI) if for every integral for which has optima, the minimum is attained by an integral . A rational polyhedron is integral if every nonempty face contains an integral vector.
The theorem turns the weighted matroid intersection problem into a linear program with an explicit constraint system, and its dual gives a certificate of optimality: a weight splitting under which is optimal in each matroid separately. Specializations include the bipartite matching polytope (two partition matroids), the arborescence and branching polytopes (a graphic and a partition matroid), and König–Egerváry-type min-max theorems. Total dual integrality of (8.7) also yields an integral min-max formula for every integral weight vector.
All results here are classical and fully proved in the book. As far as a search of the platform shows, none of them is formalized there: no matroid polytope, matroid intersection polytope, TDI or Hoffman-type integrality statement exists on Prove2Me. Mathlib has matroids but no matroid polytopes. The mission therefore produces a first machine-checked path from LP duality to an integral polytope theorem for matroids, with Hoffman's criterion and the Edmonds–Giles implication as standalone, reusable results.
The inclusion of the convex hull in (8.7) is immediate: . The content is the reverse inclusion, i.e. that every vertex of (8.7) is integral. The obvious idea, intersecting two integral polytopes, fails: the intersection of two integral polytopes generally has fractional vertices, so the integrality of each single matroid polytope (Theorem 8.5) says nothing about (8.7) on its own. What makes the two rank systems compatible is a property of the pair, and stating and using it requires linear-programming duality, faces and vertices of polytopes, and integrality criteria (Theorems 6.22 and 6.29) that are not in Mathlib in this form.
S, with subsets as Finset S (structure FinMatroid), not Mathlib's Matroid. The rank r(A) is the largest size of an independent subset of A, a natural number.S → ℝ; the dual variables of (8.2) and (8.8) are functions on Finset S.A, b and rows and columns indexed by finite types; a polytope is a polyhedron with on it; faces follow §6.2 (supporting hyperplanes, plus and ).Useful infrastructure, reusable beyond this mission: LP duality and complementary slackness for finite systems (Prove2Me has MatousekLP.Duality.duality_theorem), vertices of polytopes and the representation of a polytope as the convex hull of its vertices, totally unimodular matrices, and the dual Greedy Algorithm. Contributions to any milestone are welcome, as is a direct proof of Theorem 8.20 by another route.
A stochastic linear program evaluates a decision through a random outcome, typically the linear-affine random variable , where is a random vector and a random variable. Chapter 2 of Kall and Mayer's Stochastic Linear Programming (Springer, 2005) builds its single-stage models in two steps: a functional assigns a number to each random variable, and the evaluation function enters the objective or a constraint . If quantifies risk, it is called a risk measure. Whether the resulting optimization problem is convex, and so numerically tractable, depends on structural properties of .
The same question was asked independently in mathematical finance. Artzner, Delbaen, Eber and Heath (Math. Finance 9, 1999) proposed four axioms for coherent risk measures; Föllmer and Schied (Finance Stoch. 6, 2002) weakened two of them to convexity, giving convex risk measures; Rockafellar, Uryasev and Zabarankin (Finance Stoch. 10, 2006) introduced deviation measures, which measure spread rather than loss. Section 7 of Chapter 2 places the risk functionals used earlier in the book (expectation, the worst case, CVaR, integrated chance constraints, quadratic and absolute deviations, standard deviation and semideviations) into these axiom systems.
Let be a probability space. A random variable is interpreted as a loss. is the linear space of -dimensional random vectors with finite -th moment, and the space of random vectors with bounded support (the book's (1.6)). A function on a linear space is positive homogeneous if for and subadditive if .
A function on a linear space of random variables is
The three risk measures of the goal are the expectation on ; the worst case on , where is the support of the distribution of ; and, for , the conditional value-at-risk
For every probability space, on , on and on (every ) are coherent risk measures and convex risk measures:
Proposition 7.3, combined with Propositions 7.1 and 7.2, gives convexity of every SLP model built on expectation, worst-case or CVaR evaluation, for any distribution of the data: the CVaR-constrained and CVaR-minimizing portfolio models of §7.3 and the robust ("fat solution") models of §1 are convex programs. Propositions 7.4–7.7 do the same for the integrated chance constraints of §4.1 and the deviation models of §5, and they separate the families: the deviation measures fail the axioms of coherence and conversely, so the classes (7.1)/(7.4) and (7.2)/(7.3) are disjoint.
None of these statements is new mathematics; all are proved in the book, and coherence of CVaR is classical (Pflug 2000; Rockafellar and Uryasev 2002). The platform holds related formal results in other settings: coherence of expected shortfall and worst case on a finite state space with the payoff sign convention (CoherentRisk.es_coherent, CoherentRisk.worstCase_coherent), convexity of a sublinear functional on (CoherentSDDP.Inner.convexity_of_coherent), and the Rockafellar–Uryasev minimization formula for laws on (RUCVaR.MinFormula.theorem_10). This mission states the results for general probability spaces, losses, and the domains of the book, which is what a stochastic-programming library needs.
Most clauses are routine once the right integrability facts are available; the work is concentrated in three places. Subadditivity of CVaR needs the attainment of the minimum in its definition (or an -argument) and convexity of under the expectation, with integrability of for each . The worst case is defined through the support of a distribution; its subadditivity rests on the fact that the support of lies in the closure of , which in Lean is most easily reached by identifying the maximum of the support with the essential supremum. The deviation-measure clause (D3) requires showing that a random variable that is not almost surely constant has positive (semi)deviation, a statement about null sets rather than an inequality. The naive pointwise reading of "constant" makes (D3) false, which is why the formalization reads it almost surely.
Random variables are functions (or , as Fin s → ℝ), not equivalence classes, and is the submodule Lspace of functions with MemLp · p P. A risk measure is a function on all functions whose axioms are imposed on a submodule . The monotonicity hypothesis is taken almost surely, which is weaker than the pointwise order of the book's proofs and therefore yields stronger statements. The worst case is the supremum of the topological support of the law; CVaR is the real infimum over ; both are attained on the relevant spaces, and attainment is not built into the definitions. Expectations are Bochner integrals, used only where integrability holds.
On the printed domain the one-sided quadratic deviations of Proposition 7.5 (H) and the semideviations of Proposition 7.6 (K) can be ; these functionals are therefore valued in , which contains the real-valued statement on . A trivializing encoding is ruled out: the coherence predicate fails for the zero functional, expectation is not a deviation measure, and and CVaR evaluate a constant to itself (checked in the mission's verification file).
Reusable beyond this mission: the axiom predicates (coherent, convex, deviation), Lspace, and the named risk functionals. Contributions of general lemmas (essential supremum versus support of the law, integrability of , subadditivity of seminorms of positive parts) are welcome.
The joint distribution function of a random vector is the quantity that a joint probability constraint asks for. In dimension it is an -dimensional integral, and for most distributions no exact formula is available. The one- and two-dimensional marginals are usually much easier to compute, so stochastic programming algorithms want bounds on which use only those marginals and hold for every distribution.
The bounds of this mission provide that. They come from Chapter 4, §3.4 of P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation (Kluwer/Springer, 2005), where they serve as computable bounds on the distribution function.
Timeline of the results used here:
Let be a probability space, and let , , be events. The counting variable is the number of events among them that contain . So .
The binomial moments are and, for ,
They satisfy .
Keeping only of this linear system gives the linear program (3.14): minimize, or maximize, over with
Its optimal values are and .
For a random vector and , take and . Then the distribution function is , where counts the events .
For all events, with when ,
and for every random vector and every ,
The milestones follow the section in order:
The bounds turn the two lowest binomial moments into two-sided bounds on valid for every distribution of . Since and depend only on the one- and two-dimensional marginals, the bounds can be evaluated where itself cannot. The spanning tree bound uses the same pairwise data and reduces its best case to a maximum spanning tree problem.
All these results are classical and proved. Mathlib has inclusion–exclusion for measures (measureReal_biUnion_eq_sum_powerset) but no binomial moments, no Bonferroni inequalities and no Boole–Bonferroni bounds, so the value of this mission is a machine-checked development of the binomial moment calculus for finite families of events. The book cites the closed forms (3.15) to Kall and Wallace rather than proving them, so a formal proof also makes that step self-contained. No machine-checked proof of these bounds was found on the platform; the closest item is a counting form of inclusion–exclusion.
The obvious route to (3.15) is to solve the linear program (3.14) directly for general . It requires identifying the optimal basis and showing that the formula is correct at the boundary of the floor function, including the case , where and the pair of adjacent columns no longer exists. Both directions also need , which holds for binomial moments and fails for arbitrary data.
For the spanning tree bound, the difficulty is that (3.16) is stated for a fixed numbering of the events, in which every has an earlier parent . An arbitrary spanning tree need not have this form in the given numbering, so it requires a renumbering of the events.
Events are indexed by Fin r, so the book's indices become , and is a hypothesis everywhere. Probabilities are real numbers, through μ.real, under IsProbabilityMeasure μ; events are measurable sets and is a measurable map into Fin r → ℝ. The sets are Finset.powersetCard k univ. The binomial coefficient of is Nat.choose, which is zero for .
The index is a natural number and is used only under , because the book's formula divides by . At every event is null. Division by zero therefore never enters a statement. is not capped at : capping it would change the book's bound. The real infimum and supremum defining the optimal values are safe, because the feasible set is shown to be nonempty and bounded, and optima are attained.
A spanning tree is a SimpleGraph (Fin r) with IsTree, and every edge is counted once as a pair . The printed middle term of the display for on p.289 is corrected from to , as (3.10) requires.
A complete development needs a calculus of the finite distribution of and of finite linear programs in two equality constraints. The binomial moment calculus is reusable beyond this mission. Contributions welcome: proofs of any milestone, and Bonferroni-type bounds with higher binomial moments stated on top of the same definitions.
Value iteration computes the optimal cost-to-go vector of a Markov decision problem as the fixed point of the Bellman operator , by iterating . In reinforcement learning is rarely available exactly. It is replaced by an approximate Bellman operator (a regression model or a neural network fitted to ), which is biased, and it is evaluated from simulated transitions, which are noisy. The resulting scheme, approximate value iteration (AVI), is a stochastic approximation whose errors do not vanish: the approximation error stays of the order of the fitting accuracy forever.
Ramaswamy and Bhatnagar (arXiv:1709.04673v5; Mathematics of Operations Research, 2022) ask what AVI does under these conditions: whether the iterates stay bounded, and where they end up, when the error is only asymptotically bounded by a fixed in a weighted max-norm and the sampling noise is a martingale difference sequence whose conditional variance may grow with the iterate. Classical stochastic-approximation results (Tsitsiklis, Machine Learning 1994; Borkar and Meyn, SIAM J. Control Optim. 2000) assume errors that vanish asymptotically, so they do not cover this regime.
Fix states, a weight vector with , and the weighted max-norm
Write for the Euclidean norm. AVI is the recursion (5) of the paper,
where are step sizes, is the approximation error at stage and is sampling noise, on a probability space with a filtration . The assumptions are:
(AV2), which asks that be the globally asymptotically stable equilibrium of , follows from (AV1). The paper's analysis passes through the perturbed Bellman operator , with , a set-valued map, and the differential inclusion .
Almost surely,
The first conclusion, stability, is the paper's. The second replaces the printed convergence clause, which states that converges to some point of . That clause is false. Take two states with swapped deterministic transitions, discount (so , , ), , , , and errors that switch between and on the clock . Every assumption holds, yet infinitely often. The bound is what the paper's proof actually reaches (convergence to the global attractor of ), and it is sharp: for and constant errors with , .
Stability is the precondition for any statement about the limit of a stochastic approximation, and for AVI it is not automatic: with errors that never vanish and noise variance that grows with , a single large excursion can feed itself. The goal says that a fixed fitting accuracy cannot make AVI diverge, and that the asymptotic loss is at most , the same amplification factor as in the deterministic error analysis of approximate dynamic programming. It thereby gives a sample-path guarantee for value iteration with function approximation and simulation noise.
The paper's result has not been machine-checked. The mission also documents that the printed convergence clause is false and states a corrected, sharp version. The milestones build reusable substrate: weighted max-norms, Marchaud maps, Hausdorff distances of set-valued maps, and the interpolation and noise-control lemmas of the ODE method for stochastic approximation.
The obvious argument writes as a contracting part plus a weighted sum of errors and noise, and bounds the sum. It fails because the noise is controlled only relative to : without first knowing that is bounded, need not converge. Stability must therefore be established first, without any a priori bound on the noise sum. The limit bound is then a statement about the differential inclusion measured in the weighted max-norm. The paper's sharpening to convergence into is exactly the step that fails: the limit sets of a stochastic approximation of a differential inclusion are internally chain transitive sets, and these need not consist of equilibria.
is Fin d → ℝ with states indexed from . Mathlib's norm on that type is the max-norm, so the Euclidean norm is a separate definition euclNorm; wNorm ν x is . Probability is Mathlib's: a probability measure μ, a Filtration ℕ, conditional expectation μ[·|ℱ n], square integrability as MemLp _ 2 μ. is any map satisfying (AV1); the Bellman operator (3) is an instance. The filtration is arbitrary, with and -measurable and -measurable. Each is stated as "for every , eventually ", which avoids the junk value of a real limsup on an unbounded sequence. Hausdorff distances take values in .
No hypothesis of the goal is vacuous: the deterministic instance , , satisfies all of them (checked in a verification file). The goal assumes nothing about beyond the limsup bound (no uniform bound), nothing about the noise beyond (AV5) (no bounded noise), and nothing about the step sizes beyond (AV4) (no ).
Contributions welcome: proofs of the milestones; a stability proof by either route; the Lyapunov bound for the limsup clause; and general lemmas on almost-sure convergence of under (AV5)-type conditional variance bounds, which are reusable across stochastic approximation.
In a two-stage stochastic linear program, a simple recourse constraint penalizes the gap between a first-stage quantity (for example a production level ) and a random demand at constant unit costs: a surplus costs per unit and a shortage costs per unit. Its expected cost has a closed form in the distribution function of . Because of this, simple recourse is the most tractable class of recourse models, and it is used both as a model in its own right and as an approximation tool inside general recourse algorithms (Kall and Mayer 2005, Ch. 3 §2.2).
Constant marginal costs are often unrealistic. Overtime, outsourcing or emergency purchases usually become more expensive the larger the shortfall. Klein Haneveld (1986) extended the simple recourse function to the multiple simple recourse function, in which the marginal surplus and shortage costs increase at fixed breakpoints (Kall and Mayer, p.235). Van der Vlerk (2002) showed that a multiple simple recourse problem is an ordinary simple recourse problem with a modified distribution, based on a statement proved in Klein Haneveld, Stougie and van der Vlerk (1995) (Kall and Mayer, p.241). That reduction is the goal of this mission, in the form given by Kall and Mayer (Theorem 2.8, p.242).
Let be a real random variable with law , distribution function and finite mean . Write and .
For real with , the SRT function is and the expected SRT function is (srt, expectedSRT). For an interval with , and are the conditional mean and conditional expected SRT function given .
Multiple simple recourse. Constants , , are admissible (IsMSRTData) if , for , , and . The MSRT function and its expectation are
(msrt, expectedMSRT). The mixture distribution function and the constant are
(mixtureCdf, mixtureConst). The optimization problem is (2.59): (IsOptimal259).
is the distribution function of a probability measure, and for every
Consequently equals the right-hand side minus , and (2.59) with has the same optimal solutions as (2.59) with the expected SRT function of .
Theorem 2.8 means that every algorithm, bound and closed-form formula for simple recourse applies to multiple simple recourse unchanged, after the distribution of is replaced by the mixture . In particular, (2.64)–(2.65) show that a finite discrete yields a finite discrete , so the multiple simple recourse problem becomes a linear program of the special simple-recourse form (2.52). Lemmas 2.10–2.16 are the approximation theory of the expected SRT function: convexity, exactness outside the support, and the partition bounds with a distribution-free error estimate. Via Theorem 2.8 they transfer to the multiple case.
All results are proved in the book, and Theorem 2.8 also in van der Vlerk (2002). No machine-checked version of any of them is known. On the platform, only finite-scenario simple recourse formulas from other sources exist (for example NumStochOpt.Bounds.eq_2_51_simple_recourse_expected_cost, MulticutLShaped.SimpleRecourse). This mission formalizes the general-distribution statements.
The identity of Theorem 2.8 is elementary once the right objects are in place, and the obstacle is measure-theoretic bookkeeping. is defined as a function. To integrate against one needs the probability measure with distribution function , and must show that it is the mixture . The obvious formula is not a measure, because or may be negative. Only the combined term is nonnegative, which needs .
For the partition lemmas, the conditional laws on (closed) and (half-open) must be handled separately at the boundary points. The error bound of Lemma 2.15 is uniform over all conditional distributions on the interval, so it cannot be read off any single distribution.
The random variable is represented by its law , a probability measure on , and is Mathlib's cdf P. "Finite mean" is Integrable (fun ξ => ξ) P. is the integral against P.map (· - u k), whose distribution function is (stated in eq_2_57_2_58). is the integral against any probability measure with cdf ν = G; the goal asserts that such a exists. Conditional quantities use P[|I]. Supports use Measure.support. Index base is , as in the book. The sums printed as in (2.61) are read as .
is defined by formula (2.62), not as "a distribution making (2.61) hold". Defining it that way would make the goal trivial.
Needed infrastructure: distribution functions of pushforwards under translations, finite mixtures of probability measures and their distribution functions, uniqueness of a measure given its distribution function (MeasureTheory.Measure.ext_of_Iic), and integrals of under conditional laws. The mixture and translation lemmas are reusable for any recourse model with shifted distributions. Contributions of proofs of any milestone, and of general lemmas on mixtures of laws on , are welcome.
A linear program whose technology matrix and right-hand side are random cannot simply require its constraints to hold: for most realizations of the data, no decision satisfies them all. A joint probability constraint (also called a chance constraint) asks instead that the random system hold with probability at least a prescribed level . Models of this kind, introduced by Charnes and Cooper (1959) and by Miller and Wagner (1965) and developed systematically by Prékopa, are used in reservoir management, power system planning, finance and production planning, wherever a reliability level is the natural way to state a requirement.
The basic question about such a model is whether its feasible set is closed and convex, since that decides whether the optimization problem is a convex program that standard methods can solve. This mission formalizes the first answers in Kall and Mayer's textbook Stochastic Linear Programming: Models, Theory, and Computation (2005), Chapter 2, §2.1–§2.2: closedness for every distribution, convexity at the extreme levels, and, for finite discrete distributions, the results of Marti (1971) and Kall (1976) that guarantee convexity once the level is high enough.
Let be a random vector in with distribution on the Borel sets . The data are a random matrix and a random vector ; in the book they are affine in . For a decision let
be the event that the random system holds (componentwise), and let the probability function be . For a level , the feasible set of the probability constraint is
Let be the family of events of probability at least .
A finite discrete distribution is given by a realization tableau : with probability , where and . Write and
for the decisions feasible for the -th realization.
The milestones, in order:
If the smallest probability is attained at a unique index and is the second smallest, then
The statement fixes no constant: the threshold is expressed through the tableau.
By (2.18), a chance-constrained linear program with a finite discrete distribution maximizes a linear function over a finite union of polyhedra, a disjunctive program that is in general non-convex and is solved as a mixed-integer program with one binary variable per realization (the big- formulation (2.19)). Theorems 2.3 and 2.4 identify levels at which the union collapses to a single polyhedron, so that the problem is a plain linear program: under Theorem 2.3 it is the system of all realized constraints (2.20); under Theorem 2.4 it is either that system or the system without the least likely realization. Theorem 2.1 gives existence of optimal solutions over bounded deterministic constraint sets for every distribution, and Theorem 2.2 shows which levels are safe with no knowledge of the distribution.
The book cites the proofs of Theorems 2.1, 2.3 and 2.4 (to Kall and Wallace and to Kall's 1976 monograph) and proves Theorem 2.2 in a few lines. The platform has no statement or proof of these results, and no prior formalization of joint probability constraints with general distributions. The definitions of this mission (the probability function, the feasible set and the realization tableau) are the base for the later chapters of the book on separate chance constraints and generalized concave measures.
Closedness for a general distribution is a semicontinuity statement: the probability function is upper semicontinuous, but not continuous, because probability mass can sit on the boundary of . An argument through continuity of fails already for a single atom. Convexity is not inherited from the convexity of the sets : a union of convex sets is generally not convex, and Figure 2.1 shows a non-convex with three realizations. The content of Theorems 2.3 and 2.4 is a counting argument over the index sets in (2.18) that are admissible at a high level, and Theorem 2.4 must handle the case that the least likely realization may be dropped.
Vectors in are Fin k → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; is the pointwise order h ξ ≤ T ξ *ᵥ x. The distribution of is a probability measure on Fin r → ℝ with its Borel -algebra, and is the real number (μ (S x)).toReal. The level is any real number, as in the book; the one exception is the remark after Theorem 2.3, which is false as printed for and is stated with . The data , are general: measurable functions of for the general-distribution results, arbitrary functions for the discrete ones. The book's affine data are a special case, so each statement contains the book's.
A finite discrete distribution is a structure holding the probabilities with and the realizations , indexed by Fin N; its law is . is defined through , never through the union (2.18), so the representation theorems are not definitional. In Theorem 2.4, uniqueness of the minimizer is for all , and the existence of forces .
A complete development needs: the measurability of ; upper semicontinuity of through Fatou's lemma for indicators; the evaluation of a finite sum of Dirac measures; and the combinatorics of admissible index sets. Proofs of any milestone, and alternative statements of the polyhedral representation (2.19), are welcome.
A joint probability constraint with random right-hand side asks that a decision satisfy , where is an -dimensional random vector and a fixed matrix (Kall & Mayer 2005, Chapter 2, (2.61)). Writing for the distribution function of , the constraint reads , and the feasible set is convex as soon as is quasi-concave. Whether a chance-constrained program is a convex program therefore reduces to a concavity property of a multivariate distribution function. Distribution functions are rarely available in closed form, while densities usually are, so the practical question is which properties of a density imply generalized concavity of the measure it generates.
Timeline. Prékopa proved in 1971 that a log-concave density generates a log-concave measure, with Leindler (1972) and Prékopa (1973) completing the integral inequality behind it. Dinghas (1957) had treated the case . Borell (1975) proved the full statement for every (Borell 1975), and Brascamp and Lieb (1976) gave the functional form of the inequality (Brascamp–Lieb 1976). Kall and Mayer present the result as Theorem 2.8 of their textbook, together with the transfer to distribution functions, composite probability functions and affine images.
For , and the generalized mean is if , and otherwise for finite , for , for and for (eq. (2.63)). In Lean this is genMean γ lam a b with γ : EReal.
A nonnegative function on is -concave if for all and (Definition 2.3, IsGammaConcaveFun). For this is log-concavity, for quasi-concavity.
With and , a probability measure on the Borel sets of is -concave if for all convex Borel sets and for which is Borel (Definition 2.4, IsGammaConcaveMeasure).
The concavity exponent of a dimension is for , extended by at and at (concavityExponent r γ).
If has a -concave probability density on , , and , then
for all admissible : the law of is -concave.
Theorem 2.8 is the standard criterion for convexity of joint chance constraints. Combined with Proposition 2.2 it shows that the uniform distribution on a convex body, the non-degenerate normal, Dirichlet, Wishart and gamma (shape ) distributions have log-concave distribution functions, and that densities with convex give quasi-concave ones. With Theorem 2.11 it extends to degenerate normal laws, and with Theorem 2.10 to log-normal distribution functions. Each of these makes a chance-constrained program with such data a convex program. The integral inequality used in the proof contains the Brunn–Minkowski inequality as the special case of indicator functions.
All results in this mission are classical and proved in the literature. On the platform, the Prékopa–Leindler inequality (the case of the integral inequality) and a version of Prékopa's marginal theorem with Borel-measurable functions and integrable sections have been formalized in the ConvexOptimization namespace. No statement for general , no -concave measure and no generalized mean with the book's conventions is formalized there or in Mathlib. Mathlib has no Brunn–Minkowski inequality in .
The first idea is to combine the pointwise hypothesis on with the formula . This does not work directly: the hypothesis compares at three points, while the conclusion compares integrals over three different sets. Bridging the two is the Borell–Brascamp–Lieb inequality, a dimension-dependent statement whose exponent records how volume scales under Minkowski combinations in . The usual argument proves the one-dimensional case through a transport map between the normalized distribution functions and then inducts on the dimension. The induction does not preserve the exponent in an obvious way, and the boundary cases (, , , functions with zero integral) need separate treatment.
A second difficulty is measure-theoretic. Minkowski combinations of Borel sets need not be Borel, which is why Definition 2.4 restricts to admissible . Theorem 2.11 pulls sets back through an affine map, and the combination of the preimages need not be Borel. Theorem 2.10 combines closed sets. In both cases the proof has to supply a Borel set sitting between the two sides.
Fin k → ℝ with Lebesgue measure volume and its Borel σ-algebra. Laws of random vectors are measures on this space; Definition 2.4 requires a probability measure. Pointwise set operations (open Pointwise) are the book's (2.64).EReal). The generalized mean is whenever , for every , as in the book; Mathlib's weighted power mean has a different convention and is not used.Infrastructure that would help beyond this mission: the generalized mean and its monotonicity, the Brunn–Minkowski and Borell–Brascamp–Lieb inequalities in , and Borel measurability of sums of closed sets. Proofs of any milestone are welcome, as are alternative routes to the goal, such as the one-dimensional case followed by induction on the dimension, or a transport argument.