Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A financial transaction tax (FTT) charges a fixed fraction of the value of each securities trade. The idea goes back to Keynes (1936) and to Tobin's proposal of 1972, and it became policy after 2008: France (August 2012) and Italy (March 2013) introduced taxes on equity purchases, and the European Commission has proposed a common FTT (see the introduction of the paper below, pp. 2–3). The standard objection is that such a tax reduces trading volume and market liquidity, and therefore welfare.
Dieler, Biswas, Calzolari and Castiglionesi (Management Science 69(4), 2023; accepted manuscript of January 24, 2022, SSRN 2739357) identify a channel through which a transaction tax can raise welfare. Stock prices are read by firm managers when they decide on real investment. A market can be liquid but uninformative: trade then takes place at a price that does not reveal what informed traders know, and investment is inefficient. A tax that makes this liquid equilibrium impossible can move ("tilt") the market to an equilibrium in which prices are informative. The paper's headline result, Proposition 6, says when such a tilt is optimal and identifies the optimal tax.
There are two states, , with . A single informed trader with discount factor observes and buys a quantity of the firm's stock from a unit mass of competitive uninformed traders with discount factor , where . The buyer pays a tax proportional to the purchase value . After observing the trade, the uninformed traders set the price, and the firm's manager observes the price and invests.
Firm values are when the manager invests knowing , when she invests on the prior, and when she invests as if the state were the other one. They satisfy (1), and (3), and . Write . In §5 the paper specifies , , with (23); the parameter is the value of information.
A separating equilibrium is a pair of trades that reveals the state, so the price is and the firm is worth . A pooling equilibrium is a common trade at the price , and the firm is worth . Both must satisfy the informed trader's participation and incentive constraints, including deviations to any other quantity , which the paper's off-path beliefs price as the -state. Welfare is the expected sum of traders' payoffs and tax revenue, (8). In the Pareto-optimal pooling equilibrium () it is . In the Pareto-optimal separating equilibrium (, ) it is , where .
Suppose that without a tax both a pooling and a separating equilibrium exist (Proposition 4 (ii) at , with strict participation of the low type), that , and that
where is the tax at which . Then . Moreover:
Together these say that the smallest tilting tax is the optimal FTT and that it is strictly positive.
Proposition 2 (separating equilibria and the bounds ); the monotonicity ; Proposition 3 (pooling equilibria exist iff (22)); Proposition 4 (which equilibria coexist); the welfare formulas (24)–(25); Corollary 1 (ii) (a high enough tax rules out pooling); the step and the step of the proof of Proposition 6; and the existence of parameters satisfying all hypotheses of the goal.
The result turns a qualitative policy argument into a formula. When information is valuable relative to the liquidity gains from trade, the welfare-maximizing tax is the threshold . This threshold is determined only by the discount-factor ratio and the information gap , and it is strictly positive. It does not depend on the level of pooling trade. A tax larger than only destroys more trade in the separating equilibrium. A tax at or below changes nothing.
The paper's proofs are explicit algebra. A formal development checks them, and the drafting already found several places where the printed statements are wrong at a boundary:
The mission states the corrected versions. None of these results has a machine-checked proof.
Each step is elementary real algebra, but there are many of them, and they all depend on the deviation constraint. The informed trader may deviate to any quantity , so every equilibrium condition quantifies over a continuum. In the pooling case the binding deviation is , which is excluded when . Characterizing the equilibria therefore needs a supremum argument over a punctured interval, not a finite check. The goal combines both characterizations with a sign analysis of the linear-fractional function and the order of , and . A tempting shortcut is to identify equilibria with the closed-form conditions (17) and (22). That assumes Propositions 2 and 3, which are themselves milestones.
All objects are real numbers. There is no probability space: expectations over the two states are written out as . The parameters form a structure Firm. The hypotheses are named predicates: Standing for (1), (3), , , , together with the disclosed readings and ; Spec23 for (23); and Coexist for Proposition 4 (ii). Every ratio condition is cross-multiplied, so division by zero never decides a statement. The bounds , , and the taxes , , are the printed closed forms. They are used only where their denominators are positive.
The equilibrium predicates IsSeparatingEq and IsPoolingEq encode the paper's participation and incentive constraints (14), (16), (31) and (20), (21) directly, with the deviation ranging over all of except the equilibrium trades. They are not defined through the existence conditions (17) or (22). Welfare is the bracket of (8), evaluated at the realized firm values, not the closed forms (24)–(25). These choices rule out the trivializing formalization in which the propositions hold by definition.
Not formalized:
Only Mathlib's ordered-field and calculus libraries are needed. Proofs of any milestone are welcome. The supremum lemma for punctured intervals is reusable in other signaling models with a continuum of deviations.
Dividing indivisible goods fairly is a central problem of fair division, with applications from inheritance and course allocation to the division of computing resources. Since envy-free allocations of indivisible goods need not exist (one good, two agents), the field studies relaxations. The most prominent is envy-freeness up to any good (EFX): no agent prefers another agent's bundle after removing any single good from it. Whether EFX allocations always exist for additive valuations is one of the main open questions of the area; Plaut and Roughgarden (arXiv:1707.04769) suspected that they may not exist for general valuations.
Two lines of relaxation have been pursued: weakening the envy condition by a factor , and leaving some goods unallocated ("charity").
There are agents and a finite set of goods. Agent has an additive valuation: with . A partial allocation consists of pairwise disjoint bundles ; the goods in none of them form the pool of unallocated goods.
For , is -EFX if
Fix . Agent heavily envies a set if and strongly envies if it heavily envies a proper subset of . The envy graph has an edge when ; a source is an agent nobody envies.
The rainbow cycle number (Definition 2) is the largest for which there is a directed graph whose vertex set is split into parts, each of size at most , such that every vertex has an incoming edge from every other part, but no directed cycle visits each part at most once. In the paper the parts of such a graph are indexed by low-demand unallocated goods, and the graph records which agents are "champions" for which bundles (the group champion graph).
For all , all additive valuations and all there is a partial allocation that is -EFX and leaves a pool with
For every , is finite and
equivalently, every digraph with more than parts of size at most in which every vertex has an incoming edge from every other part contains a cycle visiting each part at most once.
The milestones follow the paper's proof: the update rules U1, U2, U3 (Lemmas 8–10) and envy-cycle elimination (Lemma 6); the high-demand bound under the standing assumption (*) (Observation 12); the in-edge property of the group champion graph (Observation 13); the conversion of a rainbow cycle into a strictly Pareto-improving allocation (Lemma 14, Lemma 16); and the final count with .
The result. Theorem 1 is the first guarantee for EFX-type allocations in which the number of unallocated goods grows sublinearly in the number of agents. It shows that the relaxation by a factor can be traded for a large reduction in charity, and it isolates a purely graph-theoretic quantity, , whose improvement directly improves the bound: would give unallocated goods. For (about at ) the goal already follows from the bound of Chaudhury et al. 2020, which is posed on the platform but unproved; the content of the goal is the sublinear regime of large .
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization produces a reusable account of approximate EFX, most envious agents and the update rules, and a standalone combinatorial theorem on cycles in multipartite digraphs that can be reused independently of fair division. Sharper bounds on , or the paper's existence bound in terms of , are natural follow-ups.
The fair-division part is a potential argument: as long as one of the update rules applies, the allocation strictly improves, and the work is to show that a rule applies whenever too many goods are unallocated. The high-demand goods are counted directly. The low-demand goods are the hard part: a rule applies to them only if the group champion graph has a cycle that uses each good at most once, and nothing about a single good or a single pair of goods forces such a cycle. A Ramsey argument on the configurations between pairs of parts shows that is finite, but only with a bound exponential in , which does not give a sublinear count. The polynomial bound requires a different construction.
Agents are Fin n and goods Fin m, with all of Fin m as the set of goods; valuations are Fin n → Finset (Fin m) → ℝ with the published predicate LittleCharity.MMS.IsAdditive. Allocations, the pool, the envy graph, sources and reachability come from the published LittleCharity.EFX.Setting. The mission's own definitions are in RainbowEFX.Sublinear.Setting.
Conventions committed to:
rainbowCycleNumber d ≤ d^4 + d would hold vacuously for an unbounded set.A formalization in which the pool is an independent variable, the factor is replaced by a weaker one, or is computed as a junk supremum would trivialize the targets; the statements rule these out. The development needs basic finite combinatorics of digraphs and finite sets, and finite sums of real valuations; no measure theory or probability. Proofs of the update rules, of Theorem 3, and of any milestone independently are welcome.
Firms increasingly record what they learn about a customer in one transaction and use it to price the next one. Regulators treat this data tracking as a privacy problem; the consumer-protection question is whether consumers, as a group, lose from it. In a monopoly the answer is typically yes: the seller who learns a consumer's valuation extracts it. Bimpikis, Morgenstern and Saban (Data Tracking under Competition, Operations Research, 2024) show that competition in the market where the data are collected can reverse this. A firm that wants a consumer's data must first win her business, and the competition for that first sale passes the value of the data back to consumers.
The paper builds on the literature on behaviour-based price discrimination (Fudenberg and Villas-Boas, Behavior-based price discrimination and customer recognition, Handbook on Economics and Information Systems, vol. 1, 2006, pp. 377–436) and on the economics of privacy (Acquisti, Taylor and Wagman, The economics of privacy, J. Econ. Literature 54(2), 442–492, 2016). Its distinctive feature is a two-dimensional private type, so that the purchase decision reveals information that matters in a different market.
A single consumer has a type drawn from the uniform distribution on . In period 1 two firms sell product 1 on a Hotelling line: firm A at and firm B at . They set prices and . The consumer must buy product 1 from exactly one of them, and her utility is from A or from B (2.1), with baseline utility .
In period 2 firm B alone sells product 2, which the consumer values at ; the parameter is the value of consumer data. If she bought product 1 from B, firm B has tracked her: it observes and can charge a personalized price. Otherwise it knows only the product-1 prices, and it prices product 2 against its belief about the types that bought from A.
The paper compares three settings:
The equilibrium notion is perfect Bayesian equilibrium (Appendix A). It requires sequential rationality of the consumer and of firm B after every pair of product-1 prices, beliefs given by Bayes' rule where it applies, and mutual best responses in product-1 prices. The aggregate consumer surplus , , is the -expectation of the consumer's total utility along the equilibrium path.
The forward-looking equilibria correspond to the pure-strategy Nash equilibria of a reduced two-player game (Definition 1, Lemma 2). The interior regime is , where is the supremum of the such that has an interior equilibrium for every (B.32). Numerically .
For every and , equilibria exist in all three settings, and every equilibrium triple satisfies
The goal fixes no numerical value of . It asserts only the two comparisons with the restricted benchmark, which is what the theorem claims.
The proof runs through the following chain:
The strict chain is stronger than the goal.
Theorem 2 is the paper's headline. With competition in the market where data are collected, tracking raises aggregate consumer surplus, and this holds even when consumers ignore the consequences of their purchases. Firm B pays for the data in advance with lower product-1 prices, and firm A must respond. The policy content is that blanket restrictions on tracking can hurt consumers when the data-collecting market is competitive. The paper's Proposition 3 contrasts this with a monopoly in both markets (for ). There, tracking lowers consumer surplus for myopic consumers, and also for forward-looking ones when . That contrast is outside this mission.
The paper proves Theorem 2 with pen and paper and a computer-algebra step. The step solving (C.8) uses a Gröbner basis computed in Mathematica, and rests on a numerical evaluation. None of it is machine-checked. A formal proof would certify the following:
The polynomial facts (C.7) and (C.8) are self-contained and can be attacked independently of the game theory.
The obvious argument would compute the forward-looking equilibrium in closed form and compare surpluses. That argument fails, because no closed form exists. Firm B's profit in is not quasiconcave in its own price, so existence and uniqueness of the equilibrium hold only on an interval whose endpoint is known only numerically. The equilibrium dispersion is defined implicitly as the root of , which contains a square root.
Comparing with therefore requires showing that a continuous function of , defined through that implicit root, has no zero on . Doing this by hand is not feasible. The paper eliminates variables algebraically and then evaluates the sign at one point.
On the game-theoretic side, the dynamic game has a continuum of information sets. Lemma 1 must pin down beliefs and prices after every off-path price pair. Without that, firm deviations cannot be evaluated, and Lemma 2 fails.
The formalization commits to the following conventions:
Consumer surplus is the integral of realized utility under equilibrium play. It is not defined by the closed forms (C.1) or (C.3), and the goal never substitutes the paper's equilibrium prices; doing either would make the comparison definitional. The goal also asserts existence in each setting, so it cannot hold vacuously.
The development is self-contained apart from the platform's generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash. Solvers will need a few pieces of infrastructure:
Proofs of individual milestones are welcome independently. The polynomial items (C.7) and (C.8) and the restricted-setting Proposition 1 are natural first targets.
Hawkes processes are point processes in which every event raises the rate of future events. They are used to model contagion in financial markets, earthquake aftershocks, the spread of posts on social networks and arrivals to service systems (Hawkes 1971; Hawkes and Oakes 1974). Hawkes and Oakes showed that a stationary Hawkes process is a Poisson stream of immigrants, each of which starts an independent cluster of descendants. Many questions about a Hawkes process therefore reduce to questions about a single cluster: how many events it contains, when they occur, and how long it lasts.
For a homogeneous Poisson process, the classical conditional uniformity property says that, given the number of points in an interval, the points are distributed as sorted i.i.d. uniforms. A. Daw, Conditional Uniformity and Hawkes Processes (arXiv:2202.05335; Mathematics of Operations Research, 2024), establishes the analogue for a Hawkes cluster. After the random time change by the compensator, the event times of a cluster of known size are uniform on a polytope. Sampling from that polytope is organized by a combinatorial object, a uniformly random parking function. This mission formalizes that result.
Let be the excitation kernel, with
A cluster starts with an event at . Each event at time adds to the intensity, so the intensity is (eq. (3) of the paper). Since , the cluster is almost surely finite. Its events are , and is the cluster size.
The compensator points are
the values of the compensator at the event times (eq. (6)). For , the polytope is
and the unit polytope is with .
A parking function of length is a vector whose increasing rearrangement satisfies for every (Definition 2). denotes the set of parking functions of length . A -step Dyck path is recorded as a non-decreasing integer vector with ; denotes the set of them. Each determines the region
(eq. (10)), and counts the coordinates of equal to .
In the Lean development these are rho, bigG, compensator, polytope, unitPolytope, parkingFunctions, dyckPaths, dyckRegion and kappa, all in the namespace HawkesParking.Spine.
Given , with uniform on and uniform on independent of ,
The law of the compensator points does not depend on beyond . Their spine is a uniformly random parking function.
The result. Theorem 1 gives an exact description of a Hawkes cluster of known size. Combined with the Borel law of , it yields an exact simulation algorithm: draw , draw a uniform parking function and independent uniforms, and invert the compensator. In the paper this is Algorithm 1 and Proposition 4. For the exponential kernel it also yields a representation of the cluster duration as a sum of conditionally independent exponentials (Theorem 2). The result links self-exciting point processes to the combinatorics of parking functions and Dyck paths, which count labelled trees and are enumerated by Cayley-type formulas.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The mission formalizes the proof chain of Theorem 1: Pollak's count of parking functions, the Dyck decomposition of the polytope, the volume of each region, the identification of region probabilities with sorted-parking-function probabilities, and the change of variables behind Lemma 2. None of these objects, and no result about them, has a machine-checked proof on Prove2Me or in Mathlib. Mathlib has neither parking functions nor this encoding of Dyck paths.
Every step is elementary on paper; the difficulty is in the formal measure theory and combinatorics. The change of variables of Lemma 2 maps the ordered epochs to the polytope by a triangular, non-linear map whose Jacobian is the product of the pre-event intensities. This is exactly the factor in the cluster's likelihood. For a general integrable kernel, is only absolutely continuous and may be flat on intervals, so the multivariate change-of-variables theorem for diffeomorphisms does not apply directly.
Proposition 3 needs the number of parking functions sorting to a given Dyck path, , and their total count , whose standard proof is Pollak's circular argument. Proposition 2 needs the law of order statistics of shifted uniforms with repeated shifts. The goal then assembles four measure identities, including a mixture over a finite set and a disjoint decomposition up to null sets.
clusterLaw g k is the measure on with densityon ordered epochs , with . This is the Janossy density of the point process with intensity (3) on , and the proof of Lemma 2 (p. 11) works from the same quantity. Mathlib has no point processes with compensators, and the step from the intensity to the likelihood is classical, not part of this paper. No intensity-based definition is formalized. The model is checked by milestone 7: its total masses are the Borel probabilities.
IsKernel g bundles on , integrability on and from the page. It adds two hypotheses: is measurable, and . The latter is needed because for the event is null and is undefined.i : Fin k with value . . Order statistics are v ∘ Tuple.sort v. "Given " is the cluster law normalized by its total mass. The law of is written as the uniform mixture over . Theorem 1 is stated for the joint law, which implies the coordinatewise eq. (8). Eq. (4) is indexed by .A merger can give a firm access to data generated in a different market. Its effect on consumers depends on what the data do and whether firms could buy them before the merger. In Data-Driven Mergers, Alexandre de Cornière and Greg Taylor study a firm A whose customers generate data useful to two firms in a second market. Their product-improvement example has a sharp reversal: when data cannot be traded, the merger benefits consumers in both markets; when independent firms can already trade data, the merger harms consumers in both markets. This mission formalizes the latter claim, Proposition 2 of the TSE working paper.
The question matters for evaluating mergers across data-connected markets. A merger between A and one downstream firm changes who receives the returns from collecting data. The relevant comparison is therefore between two ownership structures operating under the same possibility of data trade, rather than a comparison that silently gives trade to only one side. The published article treats both the product-improvement example and a broader model of data use; the present target is the paper's explicit quality example.
Firm A is a monopolist in market A. At price it serves consumers, where . Serving consumers also produces a data set of size . A can sell this data set to one or both firms in market B, a Hotelling duopoly on the unit interval. Firm B1 is at one end and B2 at the other; transport cost per unit distance is one. Data held by firm improve its product quality to , while a firm without A's data has quality .
For data quantities held by one B firm and its rival, denotes that firm's equilibrium price and its equilibrium profit. For prices , its interior demand is
The paper's equilibrium formulas are and . Quality-adjusted price means : the price after accounting for the quality the buyer receives. Market-B consumer surplus integrates each consumer's quality less price and travel cost over the two firms' market shares. Market-A consumer surplus is .
At the first stage, A chooses its market-A price. At the second stage it can supply its data exclusively to one independent B firm or supply both. The price of one exclusive licence is ; the per-firm price of nonexclusive licences is . Under a merger, A and B1 maximize their combined returns and may still license B2. After the data allocation, B1 and B2 compete for consumers. These formulas and timing follow Sections 3–4 of the working paper.
The central target is Proposition 2. Let maximize the independent A's objective and maximize the merged A–B1 objective, each including the choice of one or two data licences. Label the independent exclusive buyer first so corresponding B firms can be compared across regimes. The claim is
The six milestones follow the paper's stated steps. Lemma 2 says a B firm's profit rises with its own data, falls with its rival's data, and consumer surplus rises with either firm's data. Lemma 1 gives the ownership-independent criterion for an exclusive allocation. Section 4.3 then says exclusive supply is optimal in the quality model and that the merged firm collects less data than independent A. The goal collects the price and welfare consequences of these comparisons. The target and milestone statements are from printed pages 6–9 of the working paper.
Under trade, independent A can earn more by collecting data that a B firm values partly because its rival lacks them. After merging with B1, A–B1 internalizes the quality benefit to B1 but faces a different return from serving an additional A customer. Proposition 2 records the outcome at optimal prices: fewer A customers are served, quality-adjusted B prices rise, and consumers lose surplus in both markets. This is a concrete merger comparison for an economy where data can already be sold, as the authors emphasize in their abstract and Section 4.3.
The result is proved in the paper but has no machine-checked proof in this mission. A completed development would certify the two-stage objective, the data-allocation decision, the comparative statics, and the two welfare calculations together. Its definitions of data prices, Hotelling demand, equilibrium price and profit, and consumer surplus can also support later work on the paper's no-trade result, Proposition 1. The more general model of Section 5 and the strategic-consumer appendix are outside this mission.
The first-stage objective is not a single smooth expression: it takes the better of an exclusive sale and a sale to both B firms. An argument that starts directly with the exclusive-sale formula skips the allocation decision that Lemma 1 and Section 4.3 establish. The comparison must also connect different optimal A prices to data quantities, then carry that change through two B-firm prices and an integral of consumer utility. The B firms' prices rise with own quality, but consumer welfare depends on quality net of those prices, so the direction of the price effect alone does not settle the welfare effect. The paper's Lemmas 1–2 and Section 4.3 state the claims used at these stages.
All prices and quantities are real; A's price ranges over all of , and the relevant data quantities satisfy . The formalized is the paper's interior linear-demand formula. The standing assumptions make the verbal requirements that market B is covered and both firms are active explicit: and for . The model assumes is differentiable everywhere and . It strengthens the paper's non-decreasing to for , because the paper states strict inequalities in Lemma 2 and Proposition 2, which fail for a constant . Footnote 11's second-derivative concavity condition is omitted; the target quantifies over any maximizers and does not require that condition.
The licence prices are the paper's equilibrium formulas. Bidding strategies and the equilibrium-selection detail in footnote 9 are not encoded. Both first-stage objectives retain the maximum over the one- and two-licence branches, so exclusive supply is a result to establish. Equality in the exclusivity test takes the nonexclusive branch; at both allocations coincide. Market-B surplus uses the paper's two integrals, and the B-firm comparison matches the data holder to the data holder. These conventions exclude an encoding in which the conclusion is true simply because exclusivity was inserted into A's objective. The reusable work includes the model definitions, the generic ownership-independent Lemma 1, and the derivative and welfare lemmas. Proofs of these statements and of the goal are welcome.
When a leveraged financial institution suffers a loss, a leverage constraint can force it to sell assets. If several institutions hold the same assets, their simultaneous sales depress prices and impose losses on everyone holding those assets. These fire-sale spillovers were a central amplification channel in the 2007–2009 financial crisis (Greenwood, Landier and Thesmar, 2015, doi:10.1016/j.jfineco.2014.11.006; Cont and Schaanning, 2017, SSRN 2541114). Regulators who monitor systemic risk care about two different quantities: how likely it is that some institution is forced to sell, and how likely it is that several are forced to sell at once.
A. Capponi and M. Weber ask how banks choose portfolios when they anticipate fire sales by others (SSRN 3345399, published in Operations Research, doi:10.1287/opre.2022.0290). In their model, banks with different leverage choose deliberately different portfolios in equilibrium. They call this systemic diversification. Its effect on the two quantities above goes in opposite directions.
There are banks and assets, each with price one at date 1. Bank has total assets , leverage ratio (debt over equity, so ) and a leverage threshold . At date 1 the bank chooses portfolio weights in the simplex .
At date 2 the asset prices change by the random vector , and bank 's return is . Its new leverage is . If , the bank sells the amount that restores the threshold:
Sales are proportional to holdings. Asset trades at a discount proportional to the total amount sold, with illiquidity parameter . The realized liquidation cost of bank is
and bank minimizes given the others' portfolios. The distance to liquidation is the smallest loss that forces a sale: bank sells exactly when , and then .
The expected cost splits as . Here is the cost bank would bear alone, and is the cost bank 's sales add. The single-bank benchmark minimizes on ; a Nash equilibrium is a profile from which no bank gains by deviating alone. The game has the potential .
The shock satisfies Assumption 3.3: is spherically symmetric, and each has a continuous density that is increasing on . Assumption 3.6 asks that be strictly convex on . Assumption 3.7 asks that every be at most a sufficiently small .
For two banks and two assets with and , the equilibrium raises the probability that at least one bank liquidates and lowers the probability that both do:
Proposition 4.4 says that heterogeneous banks move apart in equilibrium: the more leveraged bank tilts further toward the liquid asset, the other toward the illiquid one. Proposition 4.5 turns this into probabilities of distress. Lower portfolio overlap makes joint liquidation rarer, but each bank holds a less diversified portfolio, so liquidation by some bank becomes more frequent. The trade-off between individual and systemic diversification underlies the paper's welfare comparison (§5) and its discussion of Pigovian taxes (§6). It is a statement about the shape of the equilibrium, not about any particular constant.
The results are proved on paper, with arguments that are partly informal ("by continuity", "sufficiently close"). They have not been formalized anywhere. A formalization would make those steps precise: it fixes the order in which and the closeness of are chosen, and it checks the measure-theoretic interchange of derivatives and expectations. Along the way it builds a reusable model of leverage-driven fire sales and of spherically symmetric shocks in Lean.
The equilibrium has no closed form, so nothing can be computed directly. The comparison with the benchmark rests on the sign of a cross-partial of the potential, which is an expectation over the intersection of two half-planes. This sign is positive at , through an explicit integral in polar coordinates, and stays positive for small only by a uniform continuity argument. The probability comparison of Proposition 4.5 then needs the equilibrium weights to stay on the correct side of , which is where the closeness of and enters. One might try to compare equilibrium and benchmark through first-order conditions alone. That fails: both banks' conditions move together, and their joint movement is controlled only through the monotone best responses that Lemma A.2 provides.
The shock law is a probability measure on EuclideanSpace ℝ (Fin K). Spherical symmetry is invariance under every linear isometry, which is stronger than exchangeability. Each marginal has a continuous density, weakly increasing on . Portfolios are functions Fin N → Fin K → ℝ, the action set is stdSimplex ℝ (Fin K), and for two assets is written two t. Bank 1 and asset 1 are index 0.
Liquidation is the model's leverage rule, written cross-multiplied, and the amount sold solves (2.1). The closed form of Lemma A.1 is a theorem, not a definition. Every theorem that integrates a cost assumes ; without it Lean's integral of a non-integrable cost is .
The following hypotheses are added, each disclosed in its statement:
In Assumption 3.7, is chosen after the law, the illiquidities, total assets and thresholds, and before the leverages.
Results are quantified over every Nash equilibrium and every benchmark optimum. A formalization that fixes a particular equilibrium, replaces the probabilities by expected costs, or assumes the ordering of portfolio weights would be trivializing, and is ruled out.
Needed infrastructure: differentiation under the integral sign for piecewise-quadratic integrands, polar coordinates for rotation-invariant laws on , and convex-analytic facts about potential games. The first two are reusable well beyond this mission. Proofs of any milestone, and sanity lemmas showing the hypotheses are satisfiable (for instance by the standard Gaussian), are welcome.
In the principal–agent model a single agent takes a costly action on behalf of a principal who sees only the action's stochastic outcome, and pays the agent according to that outcome. Many practical relationships have one agent and several principals: a manager and the shareholders, a freelancer and several employers, a marketing agency that bids for ad space on behalf of several advertisers. Bernheim and Whinston introduced this common agency model in 1986 (Econometrica 54(4), 923–942). With several principals there are two problems at once: coordinating principals who act noncooperatively and have private valuations, and the hidden-action problem of contract design.
Lavi and Shamash (EC 2019) proposed VCG contracts for common agency when the agent's action is observable. Alon, Lavi, Shamash and Talgam-Cohen (arXiv:2105.14998, Operations Research 2024, Technical Note) extend the approach to hidden actions. They define the family of incomplete information VCG (IIVCG) contracts and show that it is the unique family that makes truthful reporting dominant for the principals and makes the agent maximize declared welfare. They also show (their Theorem 3) that an IIVCG contract need not be both limited-liability and individually rational, even with one principal. This mission formalizes their main positive result: whenever some IIVCG contract has both properties, an explicit, algorithmically defined contract ALG1 has them too.
A common agency setting has a finite set of actions with pairwise distinct costs , a finite set of outcomes, and for every action a probability distribution on . There are principals. Principal has a valuation taken from a nonempty convex domain . Write .
The principals report bids , and denotes with principal 's bid replaced by . The declared welfare of action is
and denotes the welfare-maximizing action, ties broken towards the highest cost.
A contract specifies the payment from principal to the agent when the bids are and the outcome is . The agent chooses an action maximizing . Among maximizers he takes the one of highest declared welfare, and among those the costliest. The properties studied are:
The algorithm uses four derived quantities:
Contract ALG1 (Definition 4, Algorithm 1) takes an optimal solution of the linear program defining and weights summing to one with . It then pays
and such choices exist. The polynomial-time half of Theorem 5 is not part of the target.
Theorem 5 turns an existence question into a construction. Once the setting admits any IIVCG contract with both participation guarantees, ALG1 is one, computed from three linear programs per bid profile. Combined with Proposition 1 (every IIVCG contract is truthful), ALG1 is a truthful, welfare-maximizing contract under which the agent never pays out of pocket and no truthful principal loses in expectation. Lemma 2 shows that the obstruction found in Theorem 3 is the only one: it is exactly the failure of .
The results are proved in the paper. No machine-checked version of the IIVCG theory exists. Mathlib has no contract-theory or principal–agent library, and the platform's published VCG developments concern allocation mechanisms with an observable outcome and no agent action. A complete development yields a reusable formal model of hidden-action contracts with several principals, including the agent's tie-breaking rule. It also needs a linear-programming attainment fact that is useful beyond this mission.
Definition 2 constrains only expected payments under one action, while limited liability is an outcome-by-outcome condition and the agent's incentive constraint involves every action. A first attempt adjusts the expected-payment formula outcome by outcome. That fails because the payments must also make the agent's choice under the tie-breaking rule, and this couples all principals through (Lemma 1). The two bounds then point in opposite directions. IR caps each principal's expected payment by (Claim 1), and LL with incentive compatibility forces the total to be at least (Claim 2). The contract must split the cheapest implementing payment among the principals inside both bounds at once. Two further points need care: the minima defining and range over sets that need not be compact, and the agent's choice must be pinned down through the tie-breaking rule.
Principals are Fin n, a bid profile is Fin n → O → ℝ, a contract is t b ℓ o, and is Function.update b ℓ w. Expectations are finite sums. The standing assumptions are those of §2: finite nonempty action set, finite outcome set, distinct costs, probability vectors , and nonempty convex domains of non-negative valuations. is added; with no principals the weights cannot sum to one. Convexity is kept although unused. The polynomial description of the domains and every polynomial-time claim are dropped. is the welfare maximizer of highest cost, the reading under which footnote 9 says it is unique, and the same is used in IIVCG, , and ALG1. The paper's minima are real infima over nonempty sets bounded below. ALG1 is parametrized by the choice of optimal LP solutions, and the goal quantifies over all admissible choices and asserts that one exists.
The goal must not take as its hypothesis (that is Claim 3). It must also not quantify over arbitrary contracts "with Algorithm 1's properties": ALG1 is the explicit formula of Algorithm 1, line 8. A sorry-free sanity file exhibits a setting satisfying the standing assumptions with an IIVCG contract that is LL and IR, so the goal's hypothesis is satisfiable.
Contributions are welcome on the milestones in the listed order. The LP-attainment step (Proposition 4) and the infimum bookkeeping for and are reusable.
Cake cutting is the standard model of fair division for a divisible, heterogeneous resource: the cake stands for time on a shared machine, a stretch of coastline, or bandwidth over a time window, and agents value its parts differently. The central fairness notion is envy-freeness: every agent weakly prefers its own piece to every other agent's piece. When pieces must be contiguous intervals, as with time slots or land, envy-free allocations exist under mild assumptions (Stromquist, 1980; Su, 1999), but no finite protocol finds one when the valuations are accessed through queries (Stromquist, 2008), and finding one is PPAD-hard under ordinal valuations (Deng, Qi and Saberi, 2012).
Barman and Rathi (arXiv:2006.00481, Mathematics of Operations Research, 2022) identify a structural condition from statistics and economics under which the problem becomes tractable: the monotone likelihood ratio property (MLRP). Agents' value densities can be ordered so that each consecutive ratio is nondecreasing. MLRP holds, for instance, when all densities are Gaussian with a common variance, Poisson, binomial, single-parameter exponential, or linear, and for linear translations of any log-concave density (Barman and Rathi, §1).
A cake-division instance consists of agents, and agent has a value density , bounded and integrable, normalized so that . Agent values an interval at . A contiguous allocation is given by cut points , and agent receives . It is envy-free up to if for all agents .
Access to the densities is through Robertson–Webb queries. returns a value. returns the leftmost with , or if there is none. The queries are -Lipschitz () when both functions are -Lipschitz in the -norm. Running times are measured in , and .
Under MLRP, the densities are strictly positive and, after reindexing, is nondecreasing on for every . Fixing the first cut point and requiring for determines all later cut points. The resulting last cut point is the ripple map , which is a composition of queries (recursion (1)). A -ripple division is such a chain of cut points with and positive values. BinSearch (Algorithm 1) bisects on the first cut point until of the midpoint lands in .
There is a universal such that, for every MLRP instance with -Lipschitz queries and every , BinSearch with first returns at an iteration with
and giving the leftover to agent turns its output into a contiguous allocation of that is envy-free up to . The goal fixes neither the degree nor the constant of the polynomial.
Theorem 1 marks a boundary in the complexity of contiguous envy-free division. In general there is no finite protocol and no efficient approximation is expected. Under MLRP the problem admits an algorithm that is polynomial in , and , so the precision can be made exponentially small at polynomial cost. The same ripple structure underlies the paper's further results: every envy-free allocation is Pareto optimal under MLRP, and social, egalitarian and Nash welfare can be optimized efficiently. Theorem 6 is also a structural fact in its own right. Under MLRP, envy-freeness reduces to the local equalities between neighbouring agents.
The result is proved in the paper. To our knowledge none of it is formalized: neither the cake-cutting query model nor monotone likelihood ratios of densities exist in Mathlib or on the platform. This mission produces a machine-checked model of contiguous cake division with Robertson–Webb queries and a verified complexity statement for a cake-cutting algorithm.
The algorithm is short, but its analysis combines three ingredients that do not reduce to one another. Envy-freeness of a ripple division (Theorem 6) is not a local statement. Agent is only constrained to be indifferent between its own interval and its right neighbour's, yet it must not envy any interval, far to the left or right. Bridging that gap is exactly where MLRP enters, through the interval-ratio inequalities of Lemma 1. The running-time bound needs a quantitative continuity statement for a -fold composition of queries (Proposition 1). In Lean this composition passes through the truncating Cut query, whose value is defined by an infimum and a convention. Finally, positivity of the ripple values is not assumed. It has to be extracted from the Lipschitz continuity of Cut, because the existence and complexity lemmas do not assume MLRP.
The model is one definitions file, MLRPCake.EnvyFree.Model.
Fin n; agent i is the paper's agent ). Cut points are a sequence x : ℕ → ℝ, and agent i receives [x i, x (i+1)].eval integrates over Set.Icc ℓ r and is for . cut returns the infimum of the solution set and 1 when it is empty, never Lean's sInf ∅ = 0.The goal cannot be met by an existence statement. It bounds the first stopping iteration of the algorithm as defined, with a polynomial whose constant is chosen before the instance. It certifies both that the coalesced output is an allocation of the whole cake and that it is envy-free up to . Stating only that some -envy-free allocation exists, or bounding the iterations by an instance-dependent constant, is not Theorem 1.
A complete development needs basic interval-integral calculus for densities (continuity of , attainment of the Cut infimum), the intermediate value theorem, and a binary-search invariant argument. The query model and Lemma 1 are reusable for the paper's later results (Pareto optimality, welfare maximization) and for other cake-cutting formalizations. Proofs of any milestone and of auxiliary facts about cut and rd are welcome.
Online retailers and platforms summarize the experience of past buyers for future buyers. Some show only an average rating, a single number; others show full reviews, from which a reader can tell who the reviewer was and how well the product suited them. Sellers of new products, in turn, decide whom to advertise to in the launch period, and digital advertising lets them target narrowly. These two decisions interact: the people reached by the launch campaign are the people who later write the ratings.
Fainmesser, Lauga and Ofek (Management Science, 2021) study a monopolist that launches a product of unknown quality, chooses how broadly to advertise it and how to price it, and faces a second generation of consumers who learn from the first generation's user-generated content. Their first result, Proposition 1, compares three information structures and finds that an average rating, unlike full reviews or no information at all, makes the firm advertise to fewer consumers and charge a higher launch price. The mechanism is that later consumers cannot see whom the firm targeted, so a broader campaign, which brings in buyers who like the product less, lowers the average rating and with it the quality later consumers infer.
There are two periods and two generations of consumers, each a unit mass spread uniformly on a circle of length 4 (a Salop circle). The product sits at a location known to the firm, and has quality drawn uniformly from . A consumer's utility from buying is , where is the value of quality, the cost of a unit of distance between the consumer's location and the product, and the price.
In period 1 the firm chooses a price and an advertising interval of length , , centred at , at cost . Only consumers inside the interval learn of the product; they do not see and hold a belief . First-period demand is
The mean net utility of first-generation buyers, the average rating, is
In period 2 all second-generation consumers learn of the product and the firm sets . What they learn about quality depends on the information structure:
The firm maximizes total expected profit . The solution concept is a pure-strategy perfect Bayesian equilibrium (PBE): consumers' belief equals the firm's choice ; the second-period price is optimal at every information value; and no deviation raises when consumers keep the belief .
The paper's standing assumptions are and, for the cost, , , and .
Each of the three cases has a PBE, and for any equilibria (Benchmark), (Reviews), (AR),
the second-period pricing rules of the Reviews and AR cases coincide and are strictly increasing in quality, and .
and every root of (7) in is a PBE. 4. The AR term: the expected optimal second-period profit has derivative in at . 5. Unique roots: (7) and the AR condition
each have exactly one root in , and it is interior. 6. Lemma 2 (AR, necessity): every AR PBE solves (8) with , and , . 7. Lemma 2, sufficiency: the root of (8) with these prices is an AR PBE. 8. Lemma 3 (Reviews): every Reviews PBE solves (7), coincides with the Benchmark in period 1, and every root of (7) is a Reviews PBE.
Proposition 1 is the paper's base result: Proposition 2 (average-rating dynamics), Corollary 1 (the AR/Reviews rating reversal) and Proposition 3 (welfare) are all read against the equilibria it characterizes. It gives a testable prediction, that a seller facing an average-rating system targets more narrowly and prices its launch higher than one facing full reviews, and it isolates the channel: consumers' inability to observe the firm's targeting makes the rating manipulable through the advertising decision, the classic signal-jamming structure in a marketing setting.
The result is proved in the paper, with the derivations of the demand functions in a Technical Appendix. No machine-checked proof of any part of it is known. The mission produces a checked version of the equilibrium characterization, including the existence half, which the paper establishes only in the sufficiency part of the proof of Lemma 2, and an exact statement of the interiority assumption the paper leaves qualitative.
The Benchmark and Reviews cases are routine: the second-period profit does not depend on , the first-period problem is concave, and the first-order conditions characterize the equilibrium. The AR case is not. The inferred quality is clamped to , so the expected second-period profit is only piecewise smooth in the firm's deviation , and it is convex, not concave, for upward deviations. The first-order condition (8) is therefore necessary but does not by itself show that the candidate survives large deviations; that needs the curvature bound against the convexity of the expected profit on each side of . The derivative at also has to be taken through an expectation whose integrand has a moving kink.
Everything lives in the namespace RatingsAdvert.AdInterval, built on one definition file Model.
Params with fields tau, beta and A : ℝ → ℝ. Standing bundles , , of class , , and , on , . Positivity of and the requirement are added; the page divides by and uses , .Interior: and , exactly the statement that the roots of (7) and (8) lie in . It is the quantified form of the paper's "sufficiently convex … to guarantee that the solution is interior"; without it a corner can be an equilibrium.The infrastructure needed is elementary real analysis: concavity of the first-period problem, differentiation of an interval integral with a clamped integrand, and the intermediate value theorem. Contributions of proofs of any milestone are welcome; the AR sufficiency and derivative milestones carry the main work.
A system of linear inequalities may have either a feasible point or a short witness that no feasible point exists. An algorithm that returns the witness is useful when a solver must explain an infeasibility decision rather than merely announce one. The standard ellipsoid method can test feasibility under suitable geometric bounds, but its ordinary output does not supply the type of algebraic certificate considered here. Lamperski, Freund, and Todd's oblivious ellipsoid algorithm (OEA) is designed to return the appropriate kind of object without knowing in advance whether the system is feasible. Its infeasible-case iteration guarantee is Theorem 7.1 of the source preprint.
The source combines a constraint-based ellipsoid representation with continually updated certificates of lower bounds. This mission targets its infeasible case. The feasible-case result, Theorem 7.2, uses a different volume estimate and lies outside this mission.
Let have columns , and let . The primal system (P) seeks such that . A type-L certificate of infeasibility is a vector satisfying , , and . Such a vector rules out a feasible : multiplying the inequalities by its nonnegative components would give , a contradiction.
The paper assumes throughout that the nonnegative cone generated by the columns of equals , and that each column has Euclidean norm one. A certified lower-bound pair consists of and a matrix whose columns certify lower bounds for the individual constraints: , entrywise, and . These are the initial data, alongside positive weights , for OEA. The mission starts at , the all-ones vector.
OEA represents an ellipsoid by the same lower-bound vector and a positive weight vector. With , its Burrell–Todd ellipsoid is
Its centre is , its scale is , and is its radius in the direction of . These quantities determine a new certified lower bound . The condition measure is the absolute value of the greatest possible minimum slack, . On an infeasible system it measures a violation that must be present at every point. The paper defines a potential from the normalized weights and to state the quantitative progress made by an update. These definitions and their source locations appear in Sections 3–7 of the preprint.
For every certified pair and every permitted run of Algorithm 4 starting from , if (P) is infeasible, OEA returns a type-L certificate. The source's displayed bound is
The formal goal records all possible choices left open by the algorithm and bounds the number of completed updates, the quantity called in the proof of Theorem 7.1. It also asserts that every reached state has a next admissible outcome and that every terminal outcome on an infeasible input is a valid type-L certificate.
The milestone list contains the paper's certificate results, the exact form of its weight update, the slab-radius bound, and the potential decrease. In particular, Lemma 7.1 states under its specified update relation. Each milestone retains the paper's own index and hypotheses.
The target strengthens an infeasibility decision with a checkable vector whose entries can be substituted directly into the original inequalities. Its finite bound is expressed using the supplied certified lower bounds and the problem's condition measure, so it quantifies how the algorithm behaves on a particular input rather than only asserting eventual termination. The published paper proves this result; the open work here is a machine-checked development of its definitions, supporting theorems, and run-level guarantee.
The development would also provide reusable finite-dimensional matrix and certificate interfaces. In particular, certified lower bounds and the conversion of a strengthened bound into a type-L witness can be used outside this algorithm. The potential and update relations remain specific to the paper's parameterization.
The main obstacle is maintaining the link between an ellipsoid update and a valid algebraic certificate. A small slab radius alone does not describe a certificate, while an algebraic lower bound alone does not control the number of updates. The algorithm can also stop at several different tests, and Procedure 2 permits choices of indices and positive step sizes. A convergence statement about an arbitrary sequence of weights satisfying a convenient update inequality would leave these algorithmic obligations unresolved.
The representation uses Fin n and Fin m for the paper's finite index sets, real matrices for and , and real-valued functions for vectors. The standing conic-spanning and unit-column conditions are explicit in every theorem. The norm in the bound is the Euclidean norm, written as a square root of a sum of squares because Lean's plain finite function space carries a sup norm. The maximin slack is represented by a real supremum, whose boundedness and attainment follow from the standing assumption; the formal statements do not assume those consequences separately.
Algorithm 4, Procedure 2, and Procedure 3 are relations over states and outcomes. The relations retain the order of each test, the normalization of at Step 3, the replacement of one column of at Steps 5–8, and all allowed choices. A completed iteration means a pass that reaches Step 12. The paper's printed wording counts an eventual stopping pass, while its proof bounds completed updates . A first-pass stop can occur with a negative value of the printed logarithmic expression, so the formal bound applies to reached states with and the first-pass case is covered by the outcome clauses. This is the interpretation used by the proof, not a new assumption on the input.
The definitions use Lean's total matrix inverse, square root, real power, logarithm, and supremum. Positive weights and positive scale guard the ellipsoid formulas in the results that use them; the algorithm tests the scale before using the radius. Needed infrastructure includes finite matrix identities, positivity of , certified lower-bound algebra, and the inequalities underlying the potential bound. Contributions that prove the listed statements or their faithful intermediate lemmas are within scope. The goal must remain about actual OEA runs; assuming its potential decrease as a property of an arbitrary input sequence would trivialize the target.
Loss aversion, the tendency to weigh a loss more heavily than a gain of the same size, is the central ingredient of reference-dependent preferences. Measured degrees of loss aversion vary widely across experiments and markets. One explanation is that the reference point is not fixed. People form it partly from their own expectations about what they will choose, and partly from an external benchmark. He and Strub (SSRN 3318295; Operations Research, 2022, doi:10.1287/opre.2022.2309) ask how this endogenization changes the loss aversion an outside observer would infer from portfolio choices in a complete market.
The relevant models have a short history. Kőszegi and Rabin (QJE 2006; AER 2007) introduced personal equilibrium: a plan that remains optimal when it serves as its own reference point. De Giorgi and Post (Management Science 2011) introduced a state-dependent version together with a partially endogenous variant, in which deviating from an exogenous benchmark carries a mental cost. They applied it to a choice among four strategies. He and Strub solve the partially endogenous model for a general portfolio problem.
An agent with initial wealth buys a prospect, a nonnegative random variable on a probability space . The market is complete with pricing kernel , integrable, so costs . The affordable prospects form .
Given a reference point (itself a prospect), the agent values by
Here is the weight of gain-loss utility and is the intrinsic degree of loss aversion. The utility satisfies Assumption 1: it is strictly increasing, strictly concave and on , with , the Inada conditions, and integrability of and for every . Reference points satisfy , and an expectation is whenever .
With an exogenous reference point , problem (4) maximizes over . Its optimum is denoted . A threshold , given by an explicit formula (6) in terms of and of , marks where stops depending on .
A mental cost , with strictly decreasing and continuous, is charged for choosing . An agent who tolerates cost at most chooses from . A partially endogenous PE is an with for all . The partially endogenous PPE maximizes among these.
Let and . Then
Here is the unique solution of . It is strictly decreasing and continuous, with limits as and as . In each case the partially endogenous PPE exists and is unique up to almost sure equality.
Theorem 3 says that partial endogenization is observationally a reduction of loss aversion. An agent with intrinsic degree and mental-cost tolerance chooses exactly what a standard agent with exogenous reference point and the lower degree would choose. The exhibited degree interpolates monotonically between the intrinsic level (capped at ) and , so empirical estimates of loss aversion confound the intrinsic parameter with the flexibility of the reference point. Theorem 2 is the other extreme: with a fully endogenous reference point and state-dependent evaluation, loss aversion has no effect at all.
The results are proved in the paper; none of them has a machine-checked proof. The mission adds a formal model of reference-dependent preferences in a complete market, with the paper's convention for expectations and utilities with . It also provides formal versions of the exogenous-reference optimum, the personal-equilibrium notions of Kőszegi–Rabin and De Giorgi–Post, and Theorem 3 itself. Three printed slips are corrected along the way: the second limit of Theorem 3 (iii), the constant in the rewrite of (18), and the budget condition in Theorem 2.
Given its inputs, the proof of Theorem 3 is short: a Lagrangian rewrite, the intermediate value theorem and a duality step. The inputs carry the weight. Theorem 1 is an existence and uniqueness result for an infinite-dimensional concave problem whose objective is not differentiable where . The optimal multiplier is defined implicitly, through continuity and monotone limits of a budget map. Proposition 1 needs essential suprema and infima that can be or . Continuity of needs dominated convergence under Assumption 1. Strict monotonicity uses Proposition 1's injectivity, and it fails to be strict at .
A first idea is to maximize directly over . This identifies the PPE only after the reduction (10) ⇔ (16) is proved, and that reduction uses through .
Everything is defined in the namespace EndoRefLA.PartialPPE, in one definitions file. Conventions:
is the optimum of (4), not formula (5), and the PPE is the De Giorgi–Post equilibrium object, not the maximizer of (16). Defining either one by the formula that a milestone proves would make the goal tautological.
A complete development needs the following, all reusable beyond this mission: pointwise maximization of concave integrands under a budget constraint; continuity and monotonicity of budget maps in a Lagrange multiplier; and properties of under the Inada conditions. Proofs of any milestone are welcome. The paper's other two models (§3.2–§3.3) are outside this mission.
In many services the customer, not the provider, decides how long to stay: a gym session, a car-wash bay, an electric-vehicle charger, a call to a help line, a slot on a shared computing resource. Such services are called discretionary. Their congestion depends on how many customers join and on how long each of them stays. Providers manage them with per-use fees, with price rates per unit of time, and with time limits, caps on the time any one customer may spend in service. Time limits are common in practice (charging stations, library computers, public parking), and the operations literature on discretionary services (Hopp, Iravani and Yuen 2007; Tong and Rajagopalan 2014; Debo and Li 2020) studies how such systems should be priced and operated.
Feldman and Segev (SSRN 3424317) ask whether a time limit is merely convenient or actually optimal. Their answer for a single-server queue is that a revenue-maximising provider who may use any incentive-compatible price and time schedule chooses to impose a time limit when congestion is high, and that this mechanism attains the first-best social welfare.
Service needs arise as a Poisson process of rate at a single server that serves in first-come-first-served order. A customer's type is her ideal time in service, uniformly distributed on with . Time in service is worth to a customer of type . Customers pay a waiting cost per unit of expected waiting time.
An allocation consists of a measurable admitted set and a measurable time function with on . Its expected waiting time is the Pollaczek–Khinchine mean wait of the resulting M/G/1 queue, which for uniform types reads
and the allocation is feasible when the queue is stable, . Its social welfare is
and an allocation is first-best if it is feasible and maximises among all feasible allocations.
A direct mechanism adds a non-negative price for . It is incentive compatible (IC) if for all , and individually rational (IR) if on . Its revenue is .
The thresholds of the paper are
For each congestion regime, take the first-best allocation of Theorem 1:
and the full-extraction price . Then is first-best, is a feasible IC and IR mechanism with , a non-admitted type gains nothing by claiming an admitted type, no IC and IR mechanism earns more revenue, and
The result. Theorem 1 shows that the welfare-optimal schedule in a discretionary M/G/1 service is an admission threshold followed, at high congestion, by a time limit. The reason is that the waiting time depends on the second moment of service times, and a time limit is the cheapest way to cut that second moment for a given total service. Theorem 8 then shows that a monopolist with unrestricted pricing loses nothing relative to the planner: the optimal mechanism reproduces the first best, time limit included, and extracts all surplus. Together they justify time limits as an optimal instrument rather than a heuristic, and they supply the benchmark () against which the paper's simpler schemes, per-use fees and price rates with or without limits, are compared in its Theorem 10.
The formalization. The results are proved in the paper, partly by "standard arguments" (the reduction to admitted intervals) and by first-order conditions whose global optimality is argued informally; two displays in the proof of Theorem 1 are misprinted. No part of the paper has been machine-checked, and the platform has no development of discretionary services, endogenous service times or mechanism design with congestion. A complete formal proof would verify the case analysis of Theorem 1, including uniqueness in its first two cases, and the full-extraction argument, which the paper does not check for the non-negativity of prices.
The hard step is Theorem 1. The first-best program is a non-convex optimisation over measurable sets and functions, in which welfare involves the ratio of the second moment to the slack . The natural approach, pointwise optimisation of the integrand, fails because every customer's time enters every other customer's waiting cost through two integrals. The paper's route goes through a reduction to intervals, a water-filling sub-problem and a three-parameter calculus problem with implicit first-order conditions, and a formal proof must justify each reduction globally, not only at stationary points. Theorem 8 on top of Theorem 1 is short, but it needs the first-best time function to leave , which follows from the optimality of the lower threshold.
Everything is real-valued, in the namespace ServTimeLimit.OptMech. Parameters are a structure with fields Lam (), c and θbar (), and every statement assumes ; is made explicit. Allocations are pairs of a set Φ : Set ℝ and a function t : ℝ → ℝ of which only the values on matter; integrals are Lebesgue integrals over .
No queueing process is modelled: the waiting time is defined by the Pollaczek–Khinchine display above, which is the paper's own formula with . The program's condition "" is read as stability, , and is part of feasibility. Welfare integrates over the admitted set, as in the proof of Theorem 1 and the program of Theorem 8; §4's display over would charge the waiting cost to customers who are not admitted. IC is stated on , as printed, and the goal adds the proof's check for excluded types. Prices must be measurable, integrable and non-negative. Uniqueness in Theorem 1 is of the threshold (and time limit) within the displayed shape; for the first best is not unique and no uniqueness is stated. The milestone for adds the stability range at .
The goal is not Theorem 8 for an arbitrary first-best allocation: that version would drop "according to Theorem 1" and reduce to milestones 7 and 8. The goal names Theorem 1's admitted sets and time functions in each regime, so a proof must establish the first-best characterisation.
A complete development needs Lebesgue integrals over intervals, a water-filling (or convexity) argument for sub-problem (4), and one-variable calculus for the first-order conditions. The sub-problem lemma, minimising under a mean and a pointwise upper constraint, is reusable beyond this paper. Contributions of any of the milestones, or of intermediate lemmas such as the reduction to admitted intervals, are welcome.
Many decision problems have set-valued outcomes rather than single numbers. Typical cases are a portfolio whose risk is a set of capital vectors, a vector optimization problem whose image is upper-bounded by an ordering cone, or a robust model whose value is the set of all achievable outcomes. Set optimization minimizes such a map . The first difficulty is how to compare two sets. In the complete lattice approach of Heyde and Löhne (2011) and of the survey by Hamel, Heyde, Löhne, Rudloff and Schrage (2015), the values are taken in a complete lattice of sets, so that infima exist. A solution is then a set of arguments that attains the infimum and consists of minimal points.
Crespi, Hamel, Rocca and Schrage (arXiv:1812.03300v1, published in Mathematics of Operations Research, 2021) generate both the set relation and the lattice from an arbitrary family of monotone scalar functions on a preordered set. The construction needs no linear structure on the image space. It covers vector orders, scalarizations by linear functionals and orders given by indicator functions. On top of it they define approximate solutions with tolerance , and prove a Weierstrass-type existence theorem: compactness of approximate minimizer sets yields exact solutions, and the approximate sets converge to the exact ones in the Hausdorff sense.
Let be a preordered set and . Let be a family of monotone functions , so that implies .
For a map on a non-empty set , the problem is
and for . For and , let if and , with .
In §4, is a separated (Hausdorff) topological linear space over .
Let and , and suppose is compact for all . Then is non-empty and compact, and for every neighbourhood of and all sufficiently small
If, additionally, every is lower semicontinuous, then is non-empty and a -solution of (P).
The theorem is the existence result of the paper's framework. It turns a compactness condition on approximate minimizer sets into an exact solution in the sense of Definition 3.7: a set of arguments that attains the lattice infimum and consists of minimizers. The Hausdorff convergence statement is a well-posedness result: approximate minimizers computed with a tolerance lie close to exact -minimizers when is small. The framework applies to vector optimization with a cone order, to set-valued risk measures and to orders given by indicator functions, all as instances of the same .
The results are proved in the paper. None of them is formalized on the platform or in Mathlib, which has neither set relations nor lattice-valued solution concepts. This mission produces machine-checked statements of the lattice of Ψ-closed sets, inf-stability, approximate solution concepts with their conventions, and the existence theorem. Later set optimization missions can build on these definitions.
The individual arguments are short. The work lies in the extended-real bookkeeping and in using the lattice structure correctly:
EReal, and the empty infimum is . carries [Preorder Z], and is a Set (Z → EReal) with every member monotone. A map into is f : X → Set Z together with the hypothesis that every value is Ψ-closed. The lattice structure is therefore Proposition 2.3, not a built-in instance.The development needs extended-real infima, lower semicontinuity into EReal, and Cantor's intersection theorem for nested compact sets in Hausdorff spaces, all available in Mathlib. The definitions of inf-extension, Ψ-hull, set relation and approximate solutions are reusable beyond this paper. Proofs of any milestone, and of alternative routes to the goal, are welcome.
Classical utility maximization fixes a utility function at a terminal horizon and optimizes backwards. Forward investment performance processes (FIPPs), introduced by Musiela and Zariphopoulou (2008; 2010), drop the fixed horizon: the investor's preferences are a random field specified today and updated forward in time, in such a way that every past optimal decision remains optimal. Constructing FIPPs in incomplete markets with jumps is the central technical question of this literature.
Power FIPPs, , are the forward analogue of constant relative risk aversion utility. Choulli and Ma (2017, Theory Probab. Appl. 61) characterized them for locally bounded price processes without constraints, using minimal Hellinger martingale densities. Bo, Capponi and Zhou (arXiv:1811.11899, Mathematics of Operations Research, 2023) remove local boundedness and add convex compact portfolio constraints. They characterize exactly which scalar semimartingales make a FIPP, through an equation (3.7) between the characteristics of and an optimization problem over the constraint set. This mission formalizes that characterization, Theorem 3.3 of the paper.
Fix a filtered probability space with the usual conditions and trivial. Time is .
Let , assume (A_C), (A_D) and , and let . Then is a -FIPP with optimal strategy if and only if the following three conditions hold:
The result reduces a question about a family of supermartingales indexed by all admissible strategies to a pointwise condition. Equation (3.7) links the drift, diffusion and jump rates of to the value of a concave maximization over the constraint set, and the maximizer is the optimal strategy. The paper uses this to build power FIPPs in factor models, by an integral representation (Theorem 4.5), and through a forward HJB equation (Theorem 5.2). Its examples cover Lévy markets with constraints, where the optimal strategy is constant.
None of this is formalized anywhere. Mathlib has martingales, stopping times, the predictable -algebra and localizing sequences, but it has no predictable characteristics, compensated jump integrals, continuous martingale parts, Doléans-Dade exponential or class (DL). The mission's first two definitions build a relational version of that layer. Each object in it is pinned down by a characterization theorem from Jacod and Shiryaev. The layer can be reused by any formalization of jump-semimartingale finance or of limit theorems for semimartingales.
The obvious route is a verification argument for each strategy: write as a stochastic exponential (3.10) and read off its drift . This route breaks in three places.
Without local boundedness, can take the value (for ) or (for ), and first-order conditions are unavailable.
Time is ℝ≥0, and processes are ℝ≥0 → Ω → (Fin n → ℝ). Local martingales are the published EthierKurtz.IsSourceLocalMartingale.
Welcome contributions:
In a cap-and-trade scheme such as the EU Emissions Trading System, a regulator issues a limited number of emission allowances, firms trade them, and at each compliance date every firm must surrender one allowance per unit emitted or pay a penalty. The allowance price is the quantity regulators and firms care about: it is the marginal cost of emitting. Reduced-form and equilibrium models of this price go back to Carmona, Fehr, Hinz and Porchet (SIAM Review, 2010). In the one-period setting, Carmona, Delarue, Espinosa and Touzi (Ann. Appl. Probab., 2013) showed that the price solves a singular forward-backward SDE (FBSDE): a forward equation for cumulative emissions, a backward equation for the price, and a terminal condition that jumps when emissions reach the cap. Carmona and Delarue (Probab. Theory Relat. Fields, 2013) developed the well-posedness theory for such equations.
Real schemes run over several periods, and the cap of a period may depend on what was emitted before: banking of unused allowances, withdrawal of allowances, and the EU market stability reserve all make the next cap a function of past emissions. Chassagneux, Chotai and Crisan (arXiv:2008.09044, Mathematics of Operations Research, 2023) model this as a chain of singular FBSDEs linked at the compliance dates, and prove that the chain is well posed. This mission formalizes that result, Theorem 2.3 of the paper, and the chain of one-period results its proof rests on.
Fix a horizon , a number of periods and compliance dates . On a complete probability space with a -dimensional Brownian motion and its complete filtration, three processes are coupled:
Assumption 1 requires , and to be -Lipschitz, and the emissions rate to be strictly decreasing in the price with , where and .
The cap of period is . The cap class consists of with non-increasing and as . With penalty , the price must satisfy the compliance conditions
and . A decoupling field is a deterministic with on .
The one-period building block is the system on with a terminal function in the class : -valued, Lipschitz in , non-decreasing in , with limits and in . Its relaxed terminal condition is , with and the left- and right-continuous versions of in . The class adds the cap parameter .
For every restart (period , time , state , cap parameter ):
and there is a decoupling field , continuous on each , with , unique on .
Theorem 2.3 says that the multi-period market with emission-dependent caps has a well-defined allowance price, and that the price is a deterministic function of the current factors, current cumulative emissions and the emissions at the start of the period. That function is what a regulator would evaluate to compare cap rules, such as the reserve mechanism of the paper's Example 1, and it is the starting point of the paper's infinite-period model (Theorem 2.6, not part of this mission).
The result is proved in the paper; one ingredient (Proposition 3.2, with Proposition A.1) is stated there with its proof deferred to Carmona–Delarue and to Chotai's thesis. No part of it is machine-checked. A complete formalization would supply the first machine-checked treatment of a singular FBSDE with a discontinuous terminal condition, and of a multi-period linkage of such equations. Proofs of the one-period milestones in particular, which follow Carmona–Delarue, would be reusable for any degenerate FBSDE with monotone coupling.
The terminal condition is discontinuous in and the forward equation for carries no noise, so the standard Lipschitz FBSDE theory does not apply: the price is not determined by , which in general has no solution, but only by the relaxed condition between and . Solutions must be controlled near the horizon, where the value function can be discontinuous in , and estimates that rely on non-degenerate noise or on a Lipschitz terminal condition are unavailable.
Gluing periods is the second obstacle. The terminal condition of period is built from the price function of period evaluated on the diagonal , cut off at the penalty above the cap. Iterating requires that this cut-off function is again in , uniformly Lipschitz in with constants controlled across periods; solving the periods one after another with fixed terminal values does not close the induction.
Times are in . , , take values in EuclideanSpace ℝ (Fin d) and in EuclideanSpace ℝ (Fin d × Fin d), so the norm in (2.9) is the Frobenius norm. The Brownian motion, its completed filtration and the coordinatewise Itô integrals reuse the published EthierKurtz definitions; each stochastic integral is tied to its integrand. Every Lebesgue time integral carries its integrability, and the , norms are integrals in . Left limits are asserted to exist. Liminf/limsup statements are written in -form. Solutions agree when are indistinguishable and agrees -a.e.
The formalization commits to four labelled readings:
The compliance conditions (2.12) and the relaxed terminal condition (3.5) are part of the solution predicates; a formalization that drops them, writes into the solution predicate, or leaves the stochastic integrals unrelated to would be a different and trivial theorem. The dimension is allowed and gives the deterministic special case.
A complete development needs strong existence and uniqueness for Lipschitz SDEs, the martingale representation theorem for the Brownian filtration, Itô's formula, and BSDE a priori estimates. These are reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of individual milestones.
Hiring decisions often rest on a recommendation from someone who knows the candidate: a thesis adviser, a former supervisor, a colleague. Referrals are a common channel of labor market matching, and their value depends on whether the recommender can be trusted. An adviser who cares about his candidate has a reason to overstate the candidate's quality, and the main check on this is the adviser's reputation: a recommendation that turns out badly costs the adviser future credibility.
Câmara, Jia and Raffiee (2023) study this trade-off in a one-period recommendation game in which reputation enters as a state variable, and ask a question about matching between advisers and firms: which firms are more likely to hire the candidates of strong-reputation advisers? Their answer is that it depends on the shape of the firm's outside market, not only on its average quality. This mission formalizes that result, together with the equilibrium characterization it rests on.
A focal candidate has skill , , high with probability ; the average skill is . An adviser with reputation privately observes and a personal bias , distributed on with a continuous CDF of full support. He sends a message (recommend or not). A firm privately observes the value of an outside candidate, distributed on with a continuously differentiable CDF , density and full support, and hires either the focal candidate (payoff equal to the candidate's skill) or the outside one (payoff ).
If the adviser recommends a high-skilled candidate who is hired, his reputation rises to ; if he recommends a low-skilled candidate who is hired, it falls to , with ; otherwise it stays at . He receives the reputation payoff of his final reputation, plus if his candidate is hired. The payoff loss from an unsuccessful hire is
and the paper's standing Assumption (A1) is : an adviser with a higher reputation has more to lose. The solution concept is perfect Bayesian equilibrium with two tie-breaks: an indifferent firm hires the focal candidate, and an indifferent adviser does not recommend a low-skilled candidate.
In equilibrium a low-skilled adviser lies (recommends) exactly when his bias exceeds a threshold , and the firm's belief after a recommendation is
The largest possible benefit from lying is . A market is top-heavy if is strictly increasing, and bottom-heavy if is strictly decreasing.
Let be the ex-ante probability that the firm hires the focal candidate in an equilibrium at reputation . For all and all equilibria at and :
and both inequalities are strict when and . Part (iii) of the proposition, assortative matching, is (i)–(ii) restated.
The result separates two notions of a firm's "strength" that are often conflated: the average quality of its outside options and the shape of their distribution. Two firms with the same average outside candidate can respond in opposite ways to an adviser's reputation. Firms with access to many strong outside candidates (top-heavy) favor candidates of high-reputation advisers; firms whose outside options are concentrated at the bottom favor candidates of low-reputation advisers. The paper uses this to explain assortative matching between strong advisers and strong firms without assuming it, and connects it to the persuasion literature, where the convexity of the sender's payoff in the receiver's posterior determines how much information the sender wants to reveal (Kamenica and Gentzkow 2011).
All results here are proved in the paper, in Appendix A. None of them has a machine-checked proof. A formal development makes precise several points the prose leaves implicit: what "increasing" means where the adviser's behavior stops responding to reputation, that the comparison holds for every equilibrium and not only for a constructed profile, and which regularity of the shape definitions need.
The obvious argument treats the threshold as a known function of and differentiates. Two steps break this. First, is defined implicitly by a fixed-point condition that couples the adviser's incentive with the firm's Bayesian belief, which itself depends on ; existence and uniqueness of the equilibrium, and the threshold form of every equilibrium (not merely of one candidate profile), have to be established before any comparative static makes sense. Second, the hiring probability is not monotone in for every : a higher threshold makes a recommendation more persuasive but rarer, and the two effects cancel exactly for linear . The sign is decided only by the curvature of , which enters through its density, so the definition of top- and bottom-heavy markets has to be related to convexity of the CDF on the support. A further subtlety is that the hiring probability is constant for reputations at which the adviser never lies, so the monotonicity is strict only from reputations with .
All quantities are real numbers. The laws of the bias and of the outside option are probability measures , on with mass one on , no atoms and strictly increasing CDFs on ; and are their CDFs, is on (not on all of , which would force and rule out top-heavy markets), and is the derivative of on . The functions , , are differentiable on , and (A1) is stated as there.
Strategies are pure and Boolean-valued: for the adviser and for the firm, as in the paper's footnotes 15–16. They are required to be measurable, which the paper leaves implicit; message and hiring probabilities are measures of the corresponding sets. Best responses are imposed for every bias in and every outside value in , so uniqueness in Proposition 1 is on those supports. Beliefs lie in and follow Bayes' rule after every message sent with positive probability. The adviser's expected utilities are eqs. (6)–(8), with in (7); the sentence leading into (7) misprints it as .
"Increasing in " in Propositions 2 and 3 is formalized as weakly monotone on together with strict monotonicity from every with ; strict monotonicity on all of is false. The goal quantifies over arbitrary equilibrium profiles at both reputations: a statement about the threshold or about a profile the theorem itself constructs would reduce the goal to milestones 1, 5 and 8 and is ruled out. The standing assumptions are satisfiable together with a top-heavy market (for instance on with uniform bias).
The development needs only Mathlib's measure theory (CDFs from measures), one-variable calculus (monotonicity from the sign of a derivative, convexity from a monotone derivative) and slope inequalities for convex functions. The general facts in milestones 7 and 8 are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Proposition 1.
Not formalized here: the second sentence of Proposition 2 (the firm's ex-ante payoff increases in ), Proposition 4 (the low-reputation trap), Propositions 5 and 6, and the extensions of §5.
Load balancing is the problem of routing a single stream of jobs to several parallel servers so that no server sits idle while another has a long queue. The classical rule, join the shortest queue (JSQ), needs the current length of every queue at every arrival. In large server farms and distributed systems this information arrives late: the dispatcher learns the state of queue only up to some earlier time. Routing to the shortest delayed queue causes herding: every job is sent to the queue that looked shortest a while ago, and the queue lengths oscillate (Mitzenmacher, How useful is old information?, IEEE Transactions on Parallel and Distributed Systems 11, 2000, pp. 6–20).
R. Atar and D. Lipshutz, Heavy traffic limits for join-the-shortest-estimated-queue policy using delayed information, Mathematics of Operations Research 46(3), 2021, propose to estimate the current queue lengths from the delayed ones and from the routing decisions the dispatcher has itself made, and to join the shortest estimate. They identify the heavy-traffic diffusion limit of this policy for a very general class of estimators. This mission formalizes that limit theorem, following the authors' manuscript of January 12, 2020.
There are servers . A sequence of networks is indexed by . Interarrival times and service times are independent IID sequences of positive variables with mean and variances , . With renewal counts and , the -th network sees exogenous arrivals and potential services. Heavy traffic means and with .
A delay function is componentwise non-decreasing with : at time the dispatcher knows queue up to time . Writing for the queue lengths and for the arrivals routed to each queue, the estimated queue length is
the delayed queue length, plus the jobs sent since, minus the service capacity of the delay interval, plus an estimated idleness . The estimator is arbitrary, subject to measurability and to depending only on up to the delayed times and on up to now. Each arriving job joins the queue with the smallest left limit of , with ties broken toward the smaller index. The queues are non-idling single-server queues: with busy time .
The diffusion-scaled processes are , and the scaled estimator . The limiting objects are a Brownian motion with drift and variance , an independent driftless -dimensional Brownian motion with covariance , and a limiting estimator with .
The diffusion model (Definition 4.1) asks for continuous adapted processes such that with non-decreasing and increasing only when ; ; and
Here is adapted to and to .
Assume is continuous with a sequence such that on (Assumption 3.1). Assume uniformly on compacts along convergent inputs (Assumption 3.5). Assume the moduli of continuity satisfy, for some ,
(Assumption 3.8). Assume is a contraction in its second argument with constant (Assumption 3.9). Then the diffusion model has a unique solution , and
In attack order:
The theorem shows that, in heavy traffic, the state space collapses for the estimated queue lengths: all estimates agree in the limit, while the actual queue lengths need not. The limit is a reflected diffusion with delay. It covers the delayed-queue-length estimator, which oscillates in simulation, and estimators that use routing history, which do not. The diffusion model gives a common object on which estimators can be compared (the paper's Problems 1–2, p. 35).
The result is proved in the paper. This mission formalizes the statement and the lemma structure of the proof. The paper has gaps that a machine-checked development has to resolve:
None of the results is formalized elsewhere. The platform poses the special case of the Skorokhod problem (BellWilliams2001.ThresholdPolicy.skorokhod_problem_1d) as an open item.
The obvious route, tightness of followed by identification of the limit, fails at the first step. Routing is driven by the estimates, which depend on delayed information. Nothing controls the oscillation of the routed arrivals until the estimates are known to stay close together, and closeness of the estimates is what is being proved. The paper breaks the circle with stopping times at which the gap between the largest estimate and the average first exceeds a vanishing threshold. It proves tightness up to and then shows in probability, by induction over the delay intervals . Uniqueness needs a separate contraction argument on the same intervals. The probabilistic infrastructure (Prohorov's theorem on the Skorokhod space, the Skorokhod representation, the renewal functional central limit theorem) is not in Mathlib.
Fin K with , and the lexicographic tie-break picks the smallest index. Time is real, paths are ℝ → Fin K → ℝ, and only matters.CouplingConverges. C-tightness is the published IsCTight. Moduli and sup-distances use the norm, which is equivalent to the paper's Euclidean norm.Reusable parts:
Contributions are welcome on the renewal functional central limit theorem and on the Skorokhod lemmas. These are self-contained.
Not formalized:
Many problems in machine learning, optimal control and data-driven engineering design take the form of minimizing an expected loss subject to deterministic nonlinear equality constraints . When is an expectation over a large or unknown distribution, only stochastic gradient estimates are affordable, while the constraint function and its Jacobian can be evaluated exactly. Sequential quadratic optimization (SQP) methods are the standard deterministic tool for such problems, and a line of work beginning with Berahas, Curtis, Robinson and Zhou (SIAM J. Optim. 2021) adapted them to stochastic objective gradients. That first stochastic SQP method assumed that the constraint Jacobians have full row rank, which fails in practice for redundant or degenerate constraints, and fails at infeasible problems.
Berahas, Curtis, O'Neill and Robinson (arXiv:2106.13015, Mathematics of Operations Research, 2024) proposed a stochastic SQP algorithm that drops the full-rank assumption. Its search direction is split into a normal step, which reduces linearized infeasibility, and a tangential step, which reduces a quadratic model of the objective in the null space of the Jacobian. Steps are accepted with a merit function whose merit parameter is adjusted adaptively. A central question for such a method is what happens when the merit parameter is driven to zero, which occurs in particular when the Jacobians tend to rank deficiency or when the problem is infeasible.
Let , and . The problem is
Write for the constraint Jacobian, and . The merit function is with merit parameter , and the model reduction is
The algorithm (Algorithm 1 of the paper) produces, at iteration :
The direction is tangentially dominated if and normally dominated otherwise; the step-size interval differs between the two cases. The algorithm stops only at an infeasible stationary point, where but ; a run is assumed never to stop. The quantity is the norm of the gradient of the infeasibility measure .
Suppose the merit parameters vanish, , and the gradient errors are bounded, (Assumption 5). Suppose the sequence satisfies the step-size condition (28) and either (a) for all , or (b) , , and either infinitely many directions are normally dominated or . Then
The milestones are the results the paper uses on the way to Theorem 3, in order: the model-reduction inequality (14); Lemma 1 (Cauchy-decrease constants for the normal step); Lemmas 2 and 3 (the adaptive constants , , are eventually constant and bounded uniformly over runs); Lemma 7 (bounded gradient errors give bounded tangential steps); the claim in the proof of Lemma 9 that under (28) the projection never increases the step beyond its trial value; Lemma 13 (a one-step decrease inequality for ); Lemma 14 (a bound on the gradient-error term); Lemma 15 (lower bounds on for both kinds of direction, with the stated dependence).
Theorem 3 is the paper's guarantee for the regime in which the merit parameter vanishes: along a subsequence, the iterates become stationary for the constraint violation. Together with the paper's results for an eventually constant merit parameter, it shows that the stochastic method retains the qualitative behaviour of deterministic SQP methods for rank-deficient or infeasible problems, which is what makes the algorithm usable without a constraint qualification.
The statement is pathwise: it holds in every run satisfying its hypotheses, with no averaging over the randomness of the gradient estimates. Its proof chains the milestones above, each of which is reusable for other adaptive stochastic SQP variants built on the same normal/tangential decomposition and merit-parameter rule. The result is proved in the paper; to our knowledge none of it has been machine-checked. This mission formalizes the statements, so that the proof can be checked against the exact algorithmic rules, including their tie-breaking conventions and the indices at which adaptive quantities are updated.
The obvious argument would sum the decrease of the merit function , as in deterministic SQP. That fails here because the merit function changes with , the step uses a stochastic gradient, and when the objective part of the merit function carries no weight. The analysis instead tracks directly, where the objective and the gradient errors enter as perturbations of size and . These perturbations are controlled only because the adaptive constants , , stabilize at values bounded uniformly over runs, and because the step size of a normally dominated direction does not shrink with . The case analysis between tangentially and normally dominated directions, and between constant and diminishing , is where the bookkeeping concentrates.
All objects live in the namespace StochSQP.Vanishing. The spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is gradient, is fderiv ℝ c x, and is its adjoint. Matrix norms are operator norms.
The run predicate is exactly the algorithm: it neither forces to stay bounded away from zero (which would make Theorem 3 vacuous) nor assumes a lower bound on . A sorry-free check shows the run predicate and the standing assumptions are jointly satisfiable.
Contributions welcome: proofs of the milestones and the goal, and general lemmas on Cauchy decrease for linear least squares and on the descent inequality (19) for with a Lipschitz Jacobian, which are reusable for other SQP formalizations.
Many goods are sold to the same buyer repeatedly: advertising impressions, cloud capacity, seasonal tickets. The buyer's value for each sale is learned only shortly before it, and a seller who knows the distribution of future values can extract more revenue with a dynamic mechanism, one whose terms on later days depend on what the buyer reported earlier. Without further constraints the seller can extract almost the full expected surplus by charging an up-front fee for access to future sales, which leaves the buyer with negative utility on some days and some histories. Buyers in these markets often cannot or will not commit to such losses. Ex-post individual rationality, non-negative utility on every day and every history, rules them out.
Ashlagi, Daskalakis and Haghpanah (arXiv:1603.07229, 2016; Operations Research, 2023) characterize the revenue-optimal mechanism for selling items to one buyer over days under periodic incentive compatibility and ex-post individual rationality. The characterization reduces the dynamic problem to one-dimensional problems solved by backward induction, with a single scalar state passed forward. Mirrokni, Paes Leme, Tang and Zuo (arXiv:1605.08840, 2016) studied the same problem at the same time through bank account mechanisms.
A seller sells items, one per day. On day the buyer learns his value , with , drawn from a probability law , independently across days. Write .
A sequential mechanism consists of allocation probabilities and payments . With
the expected utility from later days, the mechanism is periodic incentive compatible (PIC) if on every day, for every history and every misreport , truthful reporting today, followed by truthful reporting afterwards, gives at least the utility of reporting today and truthfully afterwards:
It is ex-post individually rational (IR) if for every and . The seller maximizes the expected revenue over PIC, IR mechanisms; this is the original problem.
The paper's main tool is a single-day problem. For a law on , a tradeoff function and a utility bound , the surplus-utility-tradeoff problem maximizes over incentive compatible static mechanisms with expected utility at most ; the tight variant requires equality. The general problem does not require non-negative utility. In the cumulative problems, for and otherwise, which enforces non-negative utility. The cumulative tradeoff functions are defined backwards: is the value of day 's tight problem with for , and with for . An optimal mechanism of day 's problem at level is written .
In Lean, days are Fin k (Lean day is the paper's day ), the model is the structure Instance, mechanisms are SeqMech, the cumulative tradeoff function of Lean day is gHat I i, and the optimizers are families X P : Fin k → ℝ → ℝ → ℝ with X i c v .
Let maximize , and run the optimizers forward: on day , with state ,
Then this mechanism is PIC and IR, and its revenue is at least that of every PIC, IR mechanism. The theorem fixes no distribution and no closed form for the optimizers; it states the shape of the optimum.
The theorem shows that under ex-post participation constraints the optimal dynamic mechanism has a one-dimensional state and is computed by nested one-dimensional optimizations. It implies that charging the full surplus before the last day is without loss of generality. The paper's later results reuse its pieces: the 2-approximation of §3.2 works in the adjusted formulation of Lemma 3 and invokes Lemma 6, and the multi-buyer characterization of §3.3 extends the analysis of §3.1.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires conditional expectations over histories, a careful treatment of the value of the tradeoff functions at negative utility, and a backward induction over value functions defined as suprema over infinite-dimensional sets of mechanisms. The paper handles these informally. The mission produces a checked statement of the model, which can be reused for the paper's other results and for related dynamic mechanism design questions, and a checked proof of the characterization.
Under PIC a report on day changes every later allocation and payment, so the constraints couple all days. Lemma 3 decouples them, but only after the change of variables, and the equivalence needs a tower-property computation under the product law for every history. The main difficulty is Lemma 5. It asserts that a value function defined as a supremum, , is the continuation value of the dynamic program. The induction must pass from the one-day problem to the conditional problem given every history, and keep track of the non-negativity of utilities on every type profile; the page treats these steps in a few lines. The obvious argument, "optimize each day separately", fails: the day- mechanism that maximizes day- revenue leaves the wrong utility for later days, and the tradeoff function is exactly the correction.
Measure.pi of the daily laws μ i, each a probability measure carried by [lo i, hi i] with 0 ≤ lo i. General laws replace the paper's densities; the paper says its results also apply to discrete support.Admissible). Conditional expectations are integrals of splice i v w, which keeps for and takes for .sSup and is used only at , where the feasible set is nonempty and bounded above; WithBot definitions record the negative branch.A complete development needs Fubini-type identities for splice under Measure.pi, measurability and concavity of the tradeoff functions, and the backward induction of Lemma 5. The splice calculus and the static tradeoff problem are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are auxiliary lemmas such as monotonicity and boundedness of gTail.
A seller of a good with network externalities (a social app, a telecom plan, a game console) gains from knowing how strongly each consumer's demand depends on the consumption of others. Candogan, Bimpikis and Ozdaglar (Operations Research, 2012) showed that, on a known network, the optimal price vector of a monopolist and the resulting revenue have closed forms built from the matrix . In practice the network is estimated from data and is never known exactly. A seller who commits to prices on the basis of a forecast then faces revenue that moves with the true network .
Baron, Hu and Malekian (SSRN 3561270, 2020; published as a Technical Note in Operations Research, 2022, doi:10.1287/opre.2022.2302) ask how large that movement can be in the worst case, when the forecast error is bounded in spectral norm. Their Theorem 1 gives an exact answer depending on the network only through its largest eigenvalue. This mission formalizes that theorem, read in the SSRN version of 2020-03-25.
There are agents on a network with , and, as for any network without self-loops, . A parameter scales the peer effect, collects the agents' primary values, and is the seller's marginal cost.
The game has two stages. In the first, the seller chooses a price vector . In the second, each agent chooses a quantity , with utility
A consumption equilibrium is a profile in which each maximizes over . The seller's revenue is , and the optimal revenue is its supremum over all prices and their equilibria. Assumption 1 asks for every ; Assumption 2 asks .
The forecast error is measured by the uncertainty set
with the spectral norm. The seller fixes the price that is optimal for the forecast ; consumers then play the equilibrium on the realized , producing revenue . The revenue volatility is the supremum of the relative change over and . Finally, is the largest absolute value of an eigenvalue of .
Under Assumptions 1 and 2, for every with , every admits an interior consumption equilibrium at the seller's ex-ante price, and
The theorem turns a robustness question about an equilibrium of a game into a single spectral quantity. A seller can read off the worst-case relative revenue change from , and , and compare networks by their largest eigenvalue: denser, more central networks are more exposed to estimation error. The paper uses it to compare chains and complete networks (Proposition 3) and as the deterministic benchmark for its stochastic analysis (Theorem 2).
The result is proved on paper; no machine-checked proof exists. A formalization adds three pieces that are absent from the platform: the network pricing game stated as an equilibrium (not as a closed-form demand), the optimality of the price over all of , and the Neumann series for real matrices under .
The obvious argument substitutes Proposition 2's closed form and bounds a difference of resolvents. Two steps resist this. First, the realized network need not satisfy Assumption 1, so the existence, uniqueness and positivity of the equilibrium on must come from the spectral bound alone. Second, the bound is a supremum of a generalized Rayleigh quotient over , which must be related to the spectral norm of through a constrained-optimization argument. Tightness needs the top eigenvector, which is only non-negative in general, so the supremum is generally not attained in the open set .
The game-theoretic layer is not a formality: Proposition 2 asserts optimality over every price vector, including those at which some agents consume nothing.
Agents are Fin n; vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The norm is Mathlib's scoped spectral norm (Matrix.Norms.L2Operator). is the supremum of over the real spectrum (used only for symmetric matrices), and is computed from the complex spectrum. Condition (1) is written , equivalent to the printed form when , and avoiding Lean's convention .
Conventions added to the page, each disclosed in the items:
The optimal revenue and the revenue on are defined from the game (suprema over prices and equilibria), never by Proposition 2's closed form; a formalization that substitutes the closed form would make Propositions 1–2 vacuous and reduce the goal to a matrix inequality, and is ruled out.
A complete development needs: potential games with concave potentials on , linear complementarity for diagonally dominant matrices, the Neumann series and Perron–Frobenius for non-negative matrices, the spectral theorem for real symmetric matrices, and a Lagrange multiplier rule for a quadratic constraint. The Neumann series criterion and the norm–radius equality for symmetric matrices are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Part 3.
Models of naive social learning ask whether agents who update by simple averaging rules, rather than by Bayes' rule, can still aggregate dispersed information. In the classic DeGroot model every agent repeatedly replaces her belief by a weighted average of her neighbours' beliefs. Golub and Jackson (2010) showed that when agents communicate real-valued beliefs, the consensus belief converges to the truth along a sequence of growing networks if and only if no agent keeps a non-vanishing share of influence.
In many settings agents observe only each other's actions, and actions are coarse: a binary choice reveals much less than a probability. Mossel, Sly and Tamuz (2015) showed that even Bayesian agents can fail to learn from binary actions. Leshem and Scaglione (2018) analysed agents who play action with probability equal to their belief (probability matching) and showed that such agents reach agreement, but that the agreed action equals the true state with a probability bounded away from one, whatever the network size.
Arieli, Babichenko and Mueller-Frank (SSRN 3338015, 2020; Operations Research, 2021) show that a slight over-matching of beliefs restores learning: if agents play action with a probability pushed slightly away from the prior, and update with enough inertia, then in large networks without dominant agents all agents eventually play the true state with probability tending to one. This mission formalizes that result.
A finite set of agents carries a weight matrix : row-stochastic, irreducible (the graph with an edge whenever is strongly connected), with for every . Its centrality measure is the probability vector with .
A state is drawn with prior . Given , each agent receives an independent private signal with law ; the triple is the information structure. Agent 's first belief is the Bayesian posterior .
In every period each agent plays a binary action: with probability , independently across agents and periods, where is the decision rule. Beliefs then follow the -DeGroot rule (1):
Probability matching is . An extremization rule , , is Lipschitz with on , on , and as ; one example is . The resulting process is the -extremization DeGroot process.
The process satisfies -naive learning if, with probability at least , there is a time after which every agent plays . A sequence of networks satisfies vanishing influence if .
For every sequence of weight matrices with vanishing influence there are and such that, for every , the -extremization DeGroot process on the -th network satisfies -naive learning:
The goal fixes no rate and no explicit .
The theorem separates two properties that probability matching conflates. Agreement is generic (Theorem 1 covers a broad class of decision rules), but agreement on the truth requires the actions to carry the information of the initial consensus , and probability matching loses it. A slight extremization, combined with inertia, makes the eventual action a threshold function of the initial consensus, and the Golub–Jackson weighted law of large numbers then puts that consensus on the correct side of the prior. The result gives a non-Bayesian, action-based counterpart of the Golub–Jackson wisdom-of-crowds theorem; the paper also uses it to show that every sequence of networks admits weights under which learning holds (Proposition 1, not formalized here).
To our knowledge, none of these results has a machine-checked proof. The platform has deterministic DeGroot averaging of real beliefs but no random action process. A complete formalization would make the following machine-checked: a stochastic approximation theorem with constant step size, an absorption argument for a bounded martingale, and a weighted law of large numbers for posteriors. The paper cites the stochastic approximation step (Proposition 2) from Benaim (1998) and Roth and Sandholm (2013) and does not prove it, so formalizing it is part of the work.
The proof combines three limits that must be taken in the right order: for the ODE approximation, for the comparison of the extremization ODE with linear consensus, and network size to infinity for the law of large numbers. The ODE approximation controls the process only on bounded time windows of length . The obvious next step, letting , fails: Proposition 2 is not uniform in , and the random process need not stay near the ODE forever. Long-run behaviour therefore needs a separate argument near the corners and . The paper uses the martingale of Lemma 2 for that, together with a comparison between the extremization process and probability matching that it states only for conditional expectations. Turning that comparison into a bound on event probabilities needs a coupling the paper does not write out.
All declarations sit in the namespace NaiveLearn.OverMatch, with one definitions file NaiveLearn.OverMatch.Model. These conventions are fixed:
Measure.infinitePi; agent plays iff . The belief process is recursion (1) driven by the coins, never a closed form. The full model lives on (Bool × (Fin m → S)) × Coins m, with state as true.Fin m → ℝ with the sup norm.Matrix.IsIrreducible, and has positive diagonal. The centrality is carried as data with , , .Several hypotheses are added to, or strengthened from, the page:
The extremization family is a hypothesis of the goal, fixed before are chosen. A formalization in which the goal picks , assumes convergence of beliefs, or replaces the random process by its mean field would trivialize the theorem, and is ruled out.
A complete development needs the following infrastructure:
The first, second and last items are reusable well beyond this mission. Contributions of any of the milestones, and of the measurability of the learning event, are welcome.
Scheduling jobs on a single machine under precedence constraints ("job must be completed before job may be started") is one of the oldest problems of operations research, and with random service times and discounted rewards it is a family of alternative bandit processes that is not simple: the set of jobs that may be served changes as jobs are completed. The Gittins index theorem for a simple family therefore does not apply as it stands. Section 4.6 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011), shows that an index theorem survives for ordinary jobs served non-preemptively, provided the index is taken over the whole family rather than over single jobs.
Timeline. For deterministic jobs and undiscounted weighted completion time, Sidney (1975) showed that an optimal sequence can be built from initial sets of maximal ratio of weight to processing time, the "Sidney decomposition"; Lawler (1978) gave the algorithm for series–parallel constraints. Kadane and Simon (1977) and Glazebrook and Gittins (1981) obtained partial results for stochastic jobs. The book's Theorem 4.9 states the result for stochastic, discounted, non-preemptive ordinary jobs under arbitrary acyclic precedence constraints, as a three-way identity of policy classes.
This mission continues Multi-armed Bandit Allocation Indices I–VI, whose goals are all proved, and is part VIII of the series.
There are jobs on a single machine. Job yields the reward at its completion time , where and , and no other reward. Its service time is random with a given law and ; the service times of different jobs are independent. A relation without circuits gives the precedence constraints. There are no arrivals, and service is non-preemptive: once started, a job is served until it is completed.
A policy starts from a set of already completed jobs and, each time the machine becomes free, chooses the next job as a function of the jobs completed so far and their observed service times. It is feasible if every job it starts is uncompleted and has all its predecessors completed. Its payoff is
and it is optimal if no feasible policy has a larger payoff.
A stage is a policy together with a positive stopping time, checked after each completion. With the time at which the stage ends, is the expected discounted reward collected before and the expected discounted time. The index of the family is
A stage attaining the supremum is the first stage of a modified forwards induction (FI*) policy; an FI* policy repeats such stages for the family that remains. A forwards induction (FI) policy starts, at every decision time, a job with which such a stage begins. An ε-FI* policy uses stages whose ratio is only within of the index.
For every family as above and every initial set of completed jobs, the classes of index policies (read as FI* policies), forwards induction policies, and optimal policies are identical:
the optimal payoff.
The result. Theorem 4.9 reduces the optimal non-preemptive schedule of a stochastic precedence-constrained job family to a sequence of ratio maximizations over initial portions of the family, the stochastic and discounted counterpart of the Sidney decomposition. It also marks the limit of the index approach: Section 4.7 shows that the same identity fails when preemption is allowed (Example 4.1), and the conditions E and F of §4.6 are the book's attempt to say what survives. Corollary 4.17 turns the theorem into a robustness statement: a schedule whose stages are only ε-close to the index loses at most , the total discounted time.
Formalizing it. None of these statements has a machine-checked proof, and the platform holds no model of stochastic scheduling under precedence constraints. The related platform items LawlerWCT.SeriesPar.theorem_1 and theorem_2 (open) concern deterministic, undiscounted, series–parallel constraints, a different statement. A formal proof would make precise the "promotion" and "freezing" rearrangements of §4.5–4.6 in a setting where the family is not simple.
The obvious approach is an interchange argument on job sequences, as for the simple family. It fails because a single job is not the right unit: a low-reward job may precede a high-reward one, so the index must be taken over initial portions of the whole family, and the competing policy may interleave the jobs of the first FI* stage with other jobs, adaptively, in an order the stage does not prescribe. Showing that collecting those rewards later cannot raise their rate above is the content of (4.16). The printed proof argues the inclusion "FI* policies are optimal" only; the converse inclusion, and the identification of FI with FI* policies, are not argued on the page. The printed proof also treats only first stages that serve a fixed set in a fixed order, while first stages attaining (4.15) may be adaptive when there are ties.
Jobs are Fin n. The service-time law of job is a ProbabilityMeasure ℝ with no mass on , and realizations have the product law. A policy is a deterministic function from histories (completed jobs with their observed service times) to the next job, measurable in the service times for each history length; it never idles and never chooses a completed job. Feasibility is required for every realization. A stage's stopping rule is checked after each completion, and a stage serves at least one job. The index is a real supremum over feasible stages; for a family with an uncompleted job the set of ratios is nonempty and bounded above. Payoffs and indices are in the book's continuous-time units (): no unit conversion is made anywhere in this mission, and the bound of Corollary 4.17 is exactly as printed. The book does not define index policies for a family that is not simple; the goal reads them as FI* policies built from (4.15), which the book identifies with modified index policies (p. 33). The FI, FI* and ε-FI* properties are required with probability one over the service times, since changing an optimal policy on a null set of realizations leaves it optimal.
The goal must not be weakened to its proved half ("FI* policies are optimal"), and the competing policies must not be restricted to static job orders: a competitor may choose its next job from the completion times observed so far.
Beyond the paper: no variant items are posed.
A complete development needs product measures and integrals of finitely many functions of the service times, conditioning on the history at a decision time, and the freezing-rule inequality of Lemma 4.5 (drafted in mission VII of this series), here for a stream of several jobs. The model (histories, non-preemptive policies, stages, the family index) is reusable for the out-forest results of §4.7.
We establish a quantum version of the classical isoperimetric inequality relating the Fisher information and the entropy power of a quantum state. The key tool is a Fisher information inequality for a state which results from a certain convolution operation: the latter maps a classical probability distribution on phase space and a quantum state to a quantum state. We show that this inequality also gives rise to several related inequalities whose counterparts are well-known in the classical setting: in particular, it implies an entropy power inequality for the mentioned convolution operation as well as the isoperimetric inequality, and establishes concavity of the entropy power along trajectories of the quantum heat diffusion semigroup. As an application, we derive a Log-Sobolev inequality for the quantum Ornstein-Uhlenbeck semigroup, and argue that it implies fast convergence towards the fixed point for a large class of initial states.
This mission is the statement-level formalization of Geometric inequalities from phase space translations (arXiv:1606.08603v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: convolution data processing (Lemma 1, (30), PDF p. 11). 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.
14 results of the paper are not stated yet, because the library lacks an interface they need:
Let {\rho} the density matrix of a mixed Gaussian state. Assuming that one of the Robertson--Schr"odinger uncertainty inequalities is saturated by {\rho}, e.g. ({\Delta}^{{\rho}}X_1)^2({\Delta}^{{\rho}}P_1)^2={\Delta}^{{\rho}}(X_1,P_1)^2+(1/4)\hbar^2, we show that there exists a unique pure Gaussian state whose Wigner distribution is dominated by that of {\rho} and having the same variances and covariance {\Delta}^{{\rho}}X_1,{\Delta}^{{\rho}}P_1, and {\Delta}^{{\rho}}(X_1,P_1) as {\rho}. This property can be viewed as an analytic version of Gromov's non-squeezing theorem in the linear case, which implies that the intersection of a symplectic ball by a single plane of conjugate coordinates determines the radius of this ball.
This mission is the statement-level formalization of The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State (arXiv:1205.5222v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Saturation of one Robertson–Schrödinger inequality gives minimal symplectic capacity (Section 4, First step (continued on p.8), PDF p. 7). 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We show that Araki and Masuda's weighted non-commutative vector valued -spaces [Araki & Masuda, Publ. Res. Inst. Math. Sci., 18:339 (1982)] correspond to an algebraic generalization of the sandwiched R'enyi divergences with parameter . Using complex interpolation theory, we prove various fundamental properties of these divergences in the setup of von Neumann algebras, including a data-processing inequality and monotonicity in . We thereby also give new proofs for the corresponding finite-dimensional properties. We discuss the limiting cases leading to minus the logarithm of Uhlmann's fidelity, Umegaki's relative entropy, and the max-relative entropy, respectively. As a contribution that might be of independent interest, we derive a Riesz-Thorin theorem for Araki-Masuda -spaces and an Araki-Lieb-Thirring inequality for states on von Neumann algebras.
This mission is the statement-level formalization of R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces (arXiv:1608.05317v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-dimensional identification of Araki–Masuda and sandwiched Rényi divergences (§4.1 Eq.(39); Definition 2 and Eq.(10), p.5; Definition 7, p.8, PDF p. 9). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need: