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?
Autonomous vehicles that cannot yet drive every trip on their own can be supervised or driven by remote (tele-)drivers who sit in a control center and take over a vehicle only while it serves a customer. Because a remote driver is not tied to one vehicle, a platform may operate more vehicles than drivers. Benjaafar, Wang and Yang ask when this decoupling pays off: given a fleet of vehicles, how many remote drivers should a ride-hailing operator staff, and how much better is the best choice than the conventional one driver per vehicle ()?
The question is sharpened by a feature of ride-hailing that classical loss systems lack. A trip consists of a pick-up leg and a delivery leg, and the pick-up leg is long when few vehicles are idle. Following Besbes, Castro and Lobel (2022), the paper models this through a state-dependent service rate: with customers in service, each trip ends at rate , which falls as approaches . Withholding drivers keeps idle vehicles available, shortens pick-ups and can raise throughput. This mission formalizes the asymptotic size of that gain in the supply-limited regime, where vehicles are scarce relative to demand.
The source is the authors' SSRN working paper (abstract 4130757, version of 1 June 2023); all numbering in this mission is that version's. The paper was published in Management Science in 2024.
Customers arrive as a Poisson process of rate . A customer who arrives when all remote drivers are busy is lost. The number of customers in service is a birth–death process with birth rate and death rate . Its load is
and its stationary distribution is
The service level is the long-run fraction of demand served, .
The mission uses the service rate
where is the expected trip time and is the expected pick-up time when vehicles are idle. Demand and fleet scale together: for a fixed the fleet has
vehicles. The load at full occupancy is . The case is the supply-limited regime: there at every occupancy .
In Lean the namespace is TeleDriving.AsymLimited; the functions are rho, piMN, SL, muBesbes (the rate (4)), mLam () and maxSLRatio (the maximum below).
For ,
The theorem asserts a lower bound on the limiting gain only; it does not assert that is attained or that the limit exists.
With :
Theorem 2.A quantifies the value of decoupling drivers from vehicles when vehicles are scarce. A platform that staffs only enough remote drivers to keep some vehicles idle serves, asymptotically, at least times the fraction of demand it would serve with one driver per vehicle. The bound decreases in and reaches at , where the companion Theorem 2.B (intermediate regime, ) shows the gain vanishes. Theorems 2.A–2.C together describe how the benefit of remote driving changes from supply-limited to supply-rich markets.
The result is proved in the paper, by explicit comparison distributions. As far as is known it has not been machine-checked; no ride-hailing or state-dependent loss-system result of this kind is formalized in Mathlib or on the platform. A formal proof would establish the asymptotics of a birth–death loss system whose rates depend on the system size in a non-classical way, using only elementary real analysis: geometric series, floors and limits of explicit expressions. The intermediate statements, such as the vanishing of the low-occupancy mass, are reusable for the sibling missions on Theorems 2.B and 2.C.
The obvious argument compares the two blocking probabilities with an Erlang loss system, but the load is not constant: it depends on , on and on simultaneously, and all three grow together. Neither the stationary distribution with drivers nor the one with the optimal number of drivers converges to a fixed geometric law. The goal concerns a ratio of two quantities that both tend to explicit nonzero limits only after the distribution has been localized near a moving maximizer of . That maximizer has a closed form only through cube roots, and the localization has to hold uniformly as . The two bounds also use different comparison distributions, and the floors , and must be controlled at the same time.
ℕ → ℝ → ℝ; the rate (4) is muBesbes s. takes a real occupancy, while and take natural arguments. is written as one quotient of products; it equals (2)–(3). The objects carry the page's meaning only on the page's domains ( for , for ), because Lean's division by returns and Real.sqrt of a negative number returns . Every statement stays inside these domains.Fin m with index . It ranges over only, and for large .Filter.Tendsto along atTop on . The of the liminf is not the of D.1's cut-off , which is named eps.Real.rpow does not represent. The unimodality milestone is stated for every and ; the page states it for .No external library is needed beyond Mathlib. Proofs of any milestone are welcome, and so are alternative proofs of the goal that bypass them.
A seller offers one indivisible item to buyers but does not know the joint distribution of their valuations. The seller knows only that every valuation lies in . Prior-independent mechanism design asks for a selling mechanism that performs well against every distribution in a class. One measure of performance is the regret: the expected gap between the full surplus , which a seller who knew the valuations could extract, and the revenue actually collected. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) solve the minimax-regret problem over dominant-strategy incentive compatible (DSIC) mechanisms. For i.i.d. valuations the optimum is a second-price auction with a random reserve price (their Theorem 1).
I.i.d. valuations are a strong assumption in auction practice. In common-value and interdependent settings, bidders' values are positively dependent. The standard model of positive dependence in auction theory is affiliation, introduced by Milgrom and Weber (Econometrica 1982). §4.1 of the paper asks whether letting Nature choose an exchangeable affiliated distribution, rather than an i.i.d. one, changes the answer. It does not: the same auction and the same worst-case distribution form a saddle point, and the minimax regret is unchanged.
There are buyers with valuation profile . A mechanism assigns to each profile allocation probabilities and payments . It is DSIC, , if it satisfies ex post individual rationality (IR), dominant-strategy incentive compatibility (IC), and the allocation constraint (AC). The regret of against a joint law on is
and the minimax regret of a class is .
Two classes of laws on appear:
The candidate saddle point comes from Theorem 1. Let solve . The mechanism draws a reserve from the CDF of Theorem 1, sells to the highest bidder if the highest bid is at least , and charges , where is the second-highest bid. The distribution makes the valuations i.i.d. with the isorevenue CDF: on , with an atom of mass at . Order statistics enter through and .
For every and every ,
The second inequality is Step 2 of Theorem 1 and is restated here. The first is new to §4.1.
The result. Proposition 2 shows that positive dependence of the affiliated kind gives Nature no advantage against the optimal second-price auction. The minimax regret over is the explicit i.i.d. value , and the same randomized-reserve auction remains optimal. This contrasts with arbitrary or merely exchangeable dependence, where §4.3 of the paper shows the minimax regret jumps to for every . Affiliation is therefore the dividing line between the dependence structures that the i.i.d. analysis covers and those it does not. Lemma 1, a comparison between the maximum of and of affiliated variables, is a self-contained inequality about order statistics under positive dependence.
Formalizing it. The result is proved in the paper. No machine-checked version of any part of it exists. The mission produces: a formal definition of affiliation in the measure-theoretic form of Milgrom and Weber's appendix; the order-statistic identity for exchangeable laws; Lemma 1; and the saddle-point statement. The proof of Lemma 1 quotes Milgrom–Weber Theorem 23 (monotone functions of affiliated variables are affiliated), and the identity is quoted from David and Nagaraja. Neither is proved in the paper, so formalizing them is part of the work.
The obvious route to the first inequality is to show that regret is monotone in dependence. That route fails, because the benchmark moves with dependence as well. With the marginals fixed, stronger positive dependence raises the auction's revenue, since moves toward , but it also lowers . Neither effect dominates uniformly, and the comparison must come out exactly at the isorevenue law. Nature's class is also not parametrized by marginals: an affiliated law need not have the marginals of , so no coupling argument with a fixed i.i.d. law is available.
The second difficulty is in Lemma 1. It needs affiliation conditional on sublattices, not merely positive correlation of increasing events. The Harris-type inequality for alone (association) is a strictly weaker property, and a formalization that keeps only it states a different class. Both the definition and the inequality must be handled for general laws without densities, since Definition 4 does not assume one.
Valuation profiles are functions Fin n → ℝ, and laws are measures on that space giving full mass to . (IR), (IC), (AC) and are imposed on the cube. Mechanisms are additionally required to have measurable allocation and payment rules and bounded payments on the cube, so that (2) is a genuine expectation. is an over DSIC mechanisms of a over the class; both are bounded, so the real-valued / are not default values. Affiliation is stated for measurable , , in the cross-multiplied form . Ties in the auction go to the lowest index, which does not affect revenue. The reserve law and are given by CDF hypotheses ("CDF equals ", "CDF equals the isorevenue CDF"), and by the hypothesis that it solves the -equation in . These restate Theorem 1, which belongs to mission I of this series.
Trivializing encodings are ruled out explicitly. Affiliation quantifies over every measurable sublattice , not only . requires exchangeability; without it Nature can set all but one valuation to zero and the statement is false. The CDF hypotheses are satisfiable, and the sanity file constructs the isorevenue law.
Needed infrastructure: the regret representation of Proposition 1 for a joint law; Myerson-type payment identities for DSIC mechanisms (for the second inequality); Milgrom–Weber Theorem 23 or a direct proof of the pmf inequalities for the indicator vector ; the order-statistic identity. Affiliation and the order-statistic identity are reusable beyond auctions. Contributions to any milestone, or to these supporting results stated as separate theorems, are welcome.
Decision makers facing uncertainty treat different sources of uncertainty differently. The Ellsberg paradox, home bias in investment, and the competence effect all show people preferring bets on one source (a known urn, domestic stocks, a familiar domain) over equally likely bets on another. Ambiguity theories try to describe these differences. Most of them are hard to apply empirically because they work with sets of priors or nonadditive measures on the whole state space.
Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) propose source theory. Within a source, the agent behaves as if she has a probability measure (probabilistic sophistication). Across sources, she may weight those probabilities differently, through a source function . Two attitude components measure the difference between sources: source preference (ambiguity aversion) and insensitivity (a-insensitivity, the tendency to treat all intermediate likelihoods alike). Their Theorem 4 answers a basic question for this framework. When are two sources at exactly the same level on both components?
A state space carries an algebra of events. An act is a finite-valued map into an outcome set whose level sets are events. A weak order on acts is represented by biseparable utility: a utility on outcomes and a weighting function on events (, , monotone) evaluate a binary act with by . Structural Assumption 1 adds three nonindifferent outcomes, convex rangedness of , strong monotonicity, cumulative dominance and an Archimedean axiom. Events are ranked by : iff .
A source is a subalgebra on which is convex ranged. It is uniform if a finitely additive probability measure on satisfies stochastic dominance for all acts from . Then on for a continuous, strictly increasing , the source function.
For two sources and :
Under Assumption 1, sources and are equally preferred and equally insensitive with a regular insensitivity region if and only if both are uniform and
Moreover, and are then equally insensitive with the maximal region .
In the order of the proof (p. 8780):
The theorem says that a comparison of ambiguity attitudes "at the same level" is only possible between uniform sources. Equal preference and equal insensitivity, both observable through bets, already force probabilistic sophistication within each source and identical source functions. With risk as the second source, it characterizes ambiguity neutrality of a source behaviorally (Corollary 1 of the paper). It also shows that both attitude components are needed: the paper's Example 1 exhibits sources that are equally preferred but differ in insensitivity.
The result is proved in the paper, partly by reference. The linearity step defers to an Online Appendix, and Theorem 1's proof relies on a representation theorem of Krantz, Luce, Suppes and Tversky (1971). As far as known, none of the paper's results has a machine-checked proof. A formalization would check the paper's proof, including the deferred functional-equation step and the boundary bookkeeping of insensitivity regions. It would also provide a reusable Lean layer for Savage-style acts, biseparable utility and comparative ambiguity attitudes.
The forward direction is the hard one. The obvious route is to compare the two sources directly through the pmatcher . But exists only once both sources are known to be uniform, and nothing in the hypotheses says so. The proof first collapses the cross-source conditions into conditions of each source with itself, by transitivity, and then invokes Theorem 1. Theorem 1 in turn needs a qualitative-probability representation theorem.
Once exists, the insensitivity conditions give only one-sided inequalities: and are sub-additive on . Sub-additivity of gives super-additivity of only where . The symmetry , which comes from source preference, is what closes the gap. Regularity is used twice: it brings Theorem 1 into play, and it guarantees that the region's upper bound lies above probability .
The Lean development works in the sub-namespace SourceTheory.EqualSources, with one definition module holding the whole model:
Assumption1 bundles Structural Assumption 1.IsSource is a subalgebra on which is convex ranged.IsUniformWith and IsSourceFunction encode uniformity and (5).IsPreferredTo, IsMoreInsensitive and IsRegularRegion encode Definition 2, Definition 4 and regularity.Conventions committed to:
Function.invFun;The goal deliberately has no Assumption 2: the paper says it is implied by the other conditions, and adding it would weaken the theorem. Neither regularity hypothesis may be dropped either. Without regularity, a degenerate region such as makes the insensitivity conditions nearly empty, and the left-hand side holds for sources that are not uniform.
A complete development needs:
The last two are reusable beyond this mission. Contributions to any milestone, and to the shared model layer, are welcome.
Decision makers facing uncertainty do not treat all events alike. Beyond liking or disliking ambiguity (the Ellsberg paradox, the home bias, the competence effect), people show insensitivity: a lack of discriminatory power that makes them overweight unlikely and underweight likely events, more so when they understand the uncertainty less. For risk this is the empirically prevalent inverse-S shape of probability weighting; for uncertainty it is linked to ambiguity perception and cognitive ability. Trautmann and van de Kuilen (2015) and many empirical studies stress its importance, yet most theoretical work on ambiguity models only the preference component.
Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) propose source theory: within each source of uncertainty (a family of events generated by one mechanism, such as a stock index or an urn) the agent is probabilistically sophisticated, and differences in attitude appear across sources. Their third main result, Theorem 3, characterises comparative insensitivity between two sources through a single function of probabilities, the pmatcher. This mission formalizes that theorem.
A state space carries an algebra of events, and is a set of outcomes. An act is a finite-valued map whose level sets are events; a preference ranks acts. Structural Assumption 1 requires a utility on outcomes and a weighting function on events (, , monotone) such that binary acts are ranked by biseparable utility, for , together with convex rangedness of , strong monotonicity, cumulative dominance, an Archimedean axiom, and three outcomes of distinct utility. Events are ranked by : means .
A source is a subalgebra on which is convex ranged. It is uniform if a finitely additive probability on (the a-neutral probability) satisfies stochastic dominance for acts from . Then on for a continuous, strictly increasing source function . Assumption 2 says that two sources and are uniform, with and . The pmatcher from to is the transformation with
More insensitivity (Definition 4): is more insensitive than with insensitivity region if, for all threefold partitions from and from ,
A function on is insensitive with region if for all summing to 1, whenever , and whenever .
Under Assumptions 1 and 2, for boundary events :
Theorem 3 shows that comparative insensitivity, a condition on preferences over events of two sources, is equivalent to a shape condition (sub-additivity bounded away from the extremes) on one real function. With the risky source, is the matching-probability function measured in experiments (Dimmock et al. 2016), so the theorem justifies reading inverse-S matching probabilities as ambiguity-generated insensitivity, and it identifies the probability interval on which the shape condition applies. Together with Theorem 2 (source preference iff a disliked pmatcher), it lets a single function capture both components of uncertainty attitudes.
The result is proved in the paper, in a short argument relying on a range property whose general finitely additive proof is in an online appendix. No part of the paper is formalized anywhere to our knowledge. A formal development fixes the model precisely (Assumption 1 has many components), checks the region correspondence, and provides a reusable layer of decision-theoretic definitions (acts, biseparable utility, sources, source functions) for the rest of the paper's results.
The pmatcher translates events into probabilities, but Definition 4 quantifies over partitions while (13)–(14) quantify over real triples. The direction from preferences to needs every triple to be realised by a partition of and a matching partition of , with nested events. This rests on convex rangedness and on the fact that a finitely additive a-neutral probability of a convex-ranged source takes every value in , which is elementary only for countably additive measures. Matching must also respect the boundary condition in both sources at once, so the region has to be carried exactly to , not merely to some interval.
Lean represents events as an algebra of Set S (MeasureTheory.IsSetAlgebra), allowed by the paper's endnote 1; the paper's own case is all subsets. , , , are real-valued; is total on Set S and every event in a statement is required to belong to or to a named source. Structural Assumption 1 is one structure with a field per axiom; "W is convex ranged for every source" is read as convex rangedness on and on each source a theorem names, since the trivial algebra is never convex ranged. Event preference is -order. Probabilities are finitely additive. Partitions are ordered and may have empty cells. A "transformation" is read as a continuous probability weighting function, the properties (18) gives the pmatcher. The pmatcher is asserted to exist, never defined through an inverse function. The function region is not constrained to , because can happen for .
The goal is stated in the theorem's "Furthermore" form with both regions pinned. The bare equivalence with both regions existentially quantified would be trivialized: a function region with and satisfies (13)–(14) vacuously, which would reduce condition (ii) to the existence of a pmatcher.
A complete development needs the range lemma for finitely additive probabilities on convex-ranged algebras, the construction of nested events of prescribed probability, and the inverse of a continuous strictly increasing map of onto itself. The model layer is shared with the other missions of this paper series and is reusable for any result on biseparable preferences and sources of uncertainty. Proofs of the milestones and of the range lemma are welcome individually.
Decisions under uncertainty rarely come with known probabilities. Since Ellsberg's (1961) urn experiments it has been documented that people prefer betting on events whose likelihood they understand — a known urn, a familiar domestic stock, a domain they feel competent in — over events of an unfamiliar source of uncertainty, even when they judge the events equally likely. This phenomenon, ambiguity aversion, together with the competence effect and home bias, is central to behavioural economics, finance and decision analysis, and its measurement requires a way to compare attitudes across sources.
Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) develop source theory, in which every source of uncertainty carries its own probability-weighting function, and comparisons between sources are carried by a single function, the pmatcher. Their Theorem 2 characterises when one source is preferred to another: exactly when the pmatcher between them is disliked. With risk as the reference source, the pmatcher is the matching-probability function measured in experiments (Dimmock, Kouwenberg and Wakker 2016, Theorem 3.1), so the theorem connects a preference axiom with an observable function.
is a state space and a set of outcomes. Events are the members of an algebra of subsets of . An act is a map with finitely many values whose level sets are events; is the bet paying on and on . A preference over acts is represented by biseparable utility: a utility and a weighting function on events with , , monotone, such that bets with are ranked by . Structural Assumption 1 adds three outcomes of distinct utility, convex rangedness of (between two nested events every intermediate weight is attained by an event in between), strong monotonicity, cumulative dominance and an Archimedean axiom. Events are compared by : means .
A source is a subalgebra on which is convex ranged. It is uniform if some finitely additive probability measure on makes the agent respect first-order stochastic dominance for acts measurable with respect to . Then on for a continuous, strictly increasing source function with , ; is the a-neutral probability. Assumption 2 says that two sources and are uniform, with .
Source preference (Definition 2): is preferred to if for all and ,
A function on is disliked if for all . The pmatcher from to is , so that .
Under Assumptions 1 and 2,
The theorem turns a qualitative axiom on preferences between bets into a single inequality on one real function. Ambiguity aversion (take to be risk, Corollary 1 of the paper) becomes dislike of the matching-probability function, which can be estimated from choice data without specifying any parametric ambiguity model. The pmatcher also carries the companion insensitivity result (Theorem 3), so source preference and insensitivity are both read off the same function.
The result is proved in the paper, in one paragraph that relies on (18), Observation 4 and a range property of uniform sources whose general (finitely additive) proof is deferred to an online appendix. No part of source theory has been formalized before. A machine-checked proof makes explicit what the short argument uses: that convex rangedness forces the a-neutral probabilities to fill , that the pmatcher is well defined from the source functions alone, and that the twofold partitions of the definition can be realised for every probability level.
Source preference speaks only about pairs of events, while dislike is a condition on every probability . Passing between them requires every probability level to be realised by events of both sources. The familiar route to such a range statement uses countable additivity or a measure-theoretic continuity argument, which is not available here: the a-neutral probabilities are only finitely additive, and the paper defers the general case to an online appendix. The range has to come from convex rangedness of and the properties of the source function. A second point is that the pmatcher is only meaningful on , so it cannot be handled as a total inverse function.
All objects are in the namespace SourceTheory.PrefMatch, defined in one module Model.
𝓔 : Set (Set S) (MeasureTheory.IsSetAlgebra), as the paper's endnote 1 permits. Preference is a relation pref on acts; W : Set S → ℝ and U : Γ → ℝ are total functions whose values off events are never used.Assumption1 bundles Structural Assumption 1: weak order, normalised monotone W, utility on constant acts, three outcomes, biseparable utility, convex rangedness on 𝓔, strong monotonicity, cumulative dominance with event preference read as W-order, and the Archimedean axiom.IsSource) is a subalgebra of 𝓔 on which W is convex ranged; the paper's "W is convex ranged for every source" is read this way because the trivial algebra is never convex ranged.IsProbOn); uniformity is stochastic dominance with that probability (IsUniformWith); source functions and transformations are continuous strictly increasing self-maps of fixing and .Function.invFun, which would return junk off the range.A formalization in which Assumption 2 or the source hypotheses were contradictory would make the goal vacuous; the statements use exactly the paper's assumptions, and a sanity file checks that the identity and are disliked transformations while is a transformation that is not.
Proofs of the milestones, and of a full model of Assumption 1 (for example expected utility with Lebesgue measure on the Borel sets of ), are welcome contributions; the model layer is shared verbatim with the other missions of this series.
A probabilistic forecast issues a whole distribution for an uncertain quantity rather than a single number: wind and wave heights at several sites, demand for several products, the joint returns of several assets. Forecasts of this kind are compared and estimated with a scoring rule , a number assigned to the forecast once the realization is observed. A scoring rule is proper if a forecaster who knows the true distribution minimizes the expected score by reporting it, and strictly proper if is the only minimizer (Gneiting and Raftery 2007). Properness is what makes a score usable for model ranking and for M-estimation: an improper score rewards systematic misreporting.
For univariate distributions the continuous ranked probability score (CRPS) and the quadratic score are standard. In several dimensions the choices are thinner: the quadratic score needs a density and is sensitive to its spikes, and the energy score and the multivariate CRPS (MCRPS) were treated as separate constructions. Meng, Taylor, Ben Taieb and Li (arXiv:2002.09578v6, Operations Research, 2025) give one family, the L² scoring rules, which contains the quadratic score, the CRPS and the MCRPS as special cases and produces new ones, such as a score based on lower partial moments. Their Theorem 1 says these rules are proper. This mission formalizes that theorem.
Work on with Lebesgue measure and the componentwise order. A distribution is a probability measure on ; the paper writes it through a generalized density (a PDF, a PMF or a mixture), and every integral below is . The forecasts range over a class of distributions.
Fix a kernel and a weight that is integrable. The smoothed density of is the convolution
For the Heaviside kernel it is the CDF .
The two L² scoring rules are, for a forecast and a realization ,
The realization is treated as a point mass, whose convolution with is . The divergence of a score is , and the paper's candidate is the weighted L² distance between smoothed densities,
Assumption 1 (p. 32) collects the integrability under which all these integrals are finite.
Under Assumption 1, for all ,
so both rules are proper. If in addition -a.e. and determines within , both are strictly proper. The goal fixes no kernel and no weight: it holds for every pair meeting the assumption.
Theorem 1 is the paper's justification for its whole family of scores. With it shows that the MCRPS is proper; with the kernel of lower partial moments it shows that a new LPM score is proper; and in Section 4 of the paper the same smoothed densities define the level sets whose scoring functions are the subject of the companion mission (Mission II of this series). Strict properness reduces to one question about the kernel: whether determines . Milestones 5 and 6 answer it for the CDF and for lower partial moments.
The result is proved in the paper (appendix, pp. 32 and 34). To our knowledge none of it is formalized: Mathlib has no scoring rules, and the platform has no proper scoring rule for distributions, no multivariate CRPS and no lower partial moment. The formalization adds the integrability bookkeeping the paper leaves implicit, a machine-checked uniqueness theorem for the multivariate CDF (Mathlib's ext_of_Iic covers linear orders only, i.e. ), and the same for lower partial moments.
The algebraic core of Theorem 1 is the expansion of a square, and the obvious argument is the paper's. The cost lies elsewhere. Every expectation is an iterated integral of a function of , and exchanging the order (Fubini) and splitting an integral of a difference require the integrability that Assumption 1 states only as "then (2) is well-defined and finite". The proof also uses when it integrates the -free terms against .
For the companions the obstacle is measure-theoretic. An a.e. equality of multivariate CDFs must first be upgraded to equality everywhere, by right-continuity in each coordinate, and then measures that agree on lower orthants must be shown equal, a π-system argument in . For lower partial moments the paper differentiates times under the integral; a rigorous version has to control the finiteness of the lower-order moments.
Fin d → ℝ with its product Lebesgue measure volume and the Pi order, so is componentwise and lower orthants are Set.Iic z. is any natural number; at the strict clauses are vacuous, as in the paper.IsProbabilityMeasure; the class is a set of such measures. Its convexity (§2) is never used and is not imposed.integral_integral_swap), integrability of products and squares, and uniqueness of measures from a generating π-system. A general lemma "a multivariate CDF determines its measure" would be reusable well beyond this mission and is welcome as a separate contribution.Risk sharing asks how a total loss should be split among agents, each of whom evaluates its share with its own risk measure, so that the sum of their assessments is as small as possible. The smallest achievable sum is the inf-convolution of the agents' risk measures, and an allocation that attains it is an optimal allocation. For Value-at-Risk, the risk measure of the Basel framework, this problem was solved by Embrechts, Liu and Wang (2018) and extended to agents with heterogeneous beliefs by Embrechts, Liu, Mao and Wang (2020).
Lambda Value-at-Risk (), introduced by Frittelli, Maggis and Peri (2014), replaces the fixed confidence level of VaR by a function of the loss threshold, so that the tolerated exceedance probability may depend on the size of the loss. Liu and Schied (2025) study when probabilities are replaced by capacities, which model ambiguity about the underlying distribution: a capacity can be the upper envelope of a family of probability measures. Their Section 5.1 answers the question of what the inf-convolution of such risk measures is, which earlier work had settled for constant under capacities (Choquet quantiles, Liu, Mao and Wang 2024) and for under probability measures (Liu 2025; Liu, Tsanakas and Wei 2025).
is a measurable space and a set of random variables containing every bounded one. A capacity is a map that is increasing for inclusion with and ; it is continuous if whenever . For a function (the class ; increasing members form ) and a capacity ,
a value in . () denotes the increasing (decreasing) functions .
The allocations of are , and the inf-convolution of is
A downset is a collection containing and closed under taking measurable subsets. A family of downsets induces the risk measure . For and the paper defines
and denotes the measurable partitions of into (possibly empty) parts.
For with and continuous capacities :
if this infimum is attained at , then is optimal for every with and with (and such data exist); and if all are increasing, the inf-convolution equals for some and capacity .
Proposition 8 shows that risk measures of type, under possibly different capacities for different agents, are closed under inf-convolution when all increase, and it gives explicit optimal allocations: each agent pays a fixed amount and carries the excess on one cell of a partition. It contains as special cases the inf-convolution of VaR (Embrechts et al. 2018), of VaR with heterogeneous beliefs (Embrechts et al. 2020) and of Choquet quantiles (Liu, Mao and Wang 2024). Via the paper's Corollary 4 it yields risk sharing for robust over sets of probability measures.
The result is proved in the preprint; it has no machine-checked proof. A formalization adds a verified account of the extended-real bookkeeping that the paper leaves implicit, and it pins down which printed claims hold: two claims in the preprint are false (see Formalization scope), which a formal development has to avoid.
The individual risk measures are not real-valued: can be , and without the finiteness of Remark 1 it can be , in which case a sum over agents is meaningless. Every step of (9) therefore has to be carried out in the extended reals, and the identity has to hold in the degenerate cases (an empty or unbounded threshold set) as well as the generic one. Capacities are neither additive nor continuous from above in general, so the familiar quantile arguments for probability measures do not transfer.
The last claim of the goal is not a consequence of (9) alone: it needs the representation Theorem 1 (i), whose converse direction must produce a and a capacity from an abstract increasing family of downsets, including degenerate families in which itself is eventually admissible or no nonempty event ever is. The natural first idea, that the decreasing case is symmetric, fails: the convolved family of downsets need not be left-continuous, and the decreasing analogue of the claim is false.
Lean namespace LambdaVaRAmb.InfConv. Random variables are measurable maps ; the domain is any set of functions that contains all bounded measurable functions, consists of measurable functions, and is closed under and under for increasing 1-Lipschitz with . This is the disclosed reading of the paper's "good enough properties"; bounded and all measurable functions both qualify. Capacities are real set functions whose axioms are imposed on measurable sets. , induced risk measures and the inf-convolution are valued in EReal, with . Agents are indexed by Fin n with (implicit in the paper). "Increasing" is Monotone; left-continuity of is continuity within ; "admits a minimizer" is attainment of the infimum (IsLeast).
Not posed, because false: the claim of Theorem 3 that is left-continuous when all input families decrease, and the decreasing branch of Proposition 8. With Lebesgue measure on , equal to on and on , and , the convolved family is not left-continuous and the inf-convolution is not a with decreasing . The goal states the increasing branch only.
Trivializing encodings are ruled out: infima are taken in EReal (a real sInf would collapse unbounded sets to ); the finiteness hypothesis of Theorem 3 keeps and out of the sums; the domain is constrained so that the tail allocations lie in it; downsets consist of events; the allocation clause comes with an existence clause so that it cannot hold vacuously; and the representing pair is chosen uniformly in . Sanity checks (not part of the mission) confirm that the hypotheses of Proposition 8 are satisfiable and that of a constant is that constant.
Contributions welcome: Remark 1 and the monotonicity milestone are short and independent; Theorem 3 is reusable for any risk measure induced by downsets; Theorem 1 is a general representation result for under capacities.
Ranking and selection (R&S) asks which of simulated systems has the largest mean performance when every observation is costly. It is a basic tool of simulation optimization: choosing a staffing level, an inventory policy or a network design from a large catalogue of candidates that can only be evaluated by noisy simulation. In the fixed-budget formulation a total of observations is spent sequentially and one alternative is selected at the end; procedures are compared by their probability of correct selection (PCS).
Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and the relevant question is how the budget must grow with . A procedure is sample optimal if a budget , linear in , keeps its PCS bounded away from zero as ; a total budget of order is clearly necessary. Li, Fan and Hong (arXiv:2303.02951) show that the simplest procedure of all, the greedy procedure, which always samples the alternative with the largest current sample mean, is sample optimal. They also show that its PCS limit is strictly below one under the slippage configuration, however large is: the greedy procedure is not consistent. This mission formalizes the remedy: an exploration phase of observations per alternative before the greedy phase makes the procedure consistent.
There are alternatives. Alternative produces independent observations , independent across alternatives, and alternative 1 is the unique best. The running average after observations is .
Assumption 1 (p. 12). There are constants and such that and , regardless of how large is.
The explore-first greedy (EFG) procedure (Procedure 2, p. 21) with exploration size and budget :
With the exploration phase uses observations and the greedy phase , where . The greedy procedure is the case .
Crossing times. Let be iid standard normal, , and
with . is finite exactly on , where it is strictly decreasing and continuous.
Consistency (Definition 2, p. 21): A sample-optimal fixed-budget R&S procedure is consistent if the PCS of the procedure satisfies that, for any , there exists a constant such that , for .
Suppose Assumption 1 holds. Let and . Let satisfy
and let . If , then the PCS of the EFG procedure satisfies
The result. Theorem 4 shows that a one-line change to the greedy procedure, a fixed number of initial observations per alternative, turns a sample-optimal but inconsistent procedure into one that is both sample optimal and consistent. Any PCS target is reached with a budget that grows only linearly in the number of alternatives, without variance estimates, elimination rules or pairwise comparisons. Together with (5.4) (p. 24) it also gives a recipe for choosing and when and are known, which converts the fixed-budget procedure into a fixed-precision one.
Formalizing it. The results are proved in the paper, but Lemma 4 and Theorem 4 have their proofs omitted ("straightforward"), and Theorem 3's proof refers to "almost the same analysis" as Theorem 1. A machine-checked development makes these steps explicit. It also corrects the scaling in (5.1), which is misprinted in the source. No part of it is formalized on the platform. The boundary-crossing inequality (5.2) and the crossing-time lemmas for the Gaussian running average are reusable in the companion missions of this series and for other greedy procedures.
The obvious approach is to bound each inferior alternative's sample size by the number of observations it needs to fall below alternative 1, and to sum. It fails because alternative 1's running average is itself random, may drop below its mean, and can lose the lead at any time before it reaches its minimum. The boundary must be the random minimum , and the crossing times of the other alternatives are then dependent through it. The step from (5.2) to Theorem 3 needs crossing times dominated by iid copies of on the event that the minimum is high, a strong law over the growing array, and the continuity of (Lemma 7) to pass to the limit in the level. Lemma 4 needs fluctuation facts for the Gaussian random walk (finite expected crossing time for , infinite mean at ) that are not in Mathlib.
Model. Observations form an array indexed by on a probability space, mutually independent, with and . Problem uses alternatives ; Lean's alternative is the paper's alternative 1. One array serves every , which does not change any PCS.
Procedure. The EFG procedure is a deterministic map from the observation array to the selected index. Ties in every arg max go to the smallest index, which is a null event under the model. The greedy loop runs times (none if ).
Budget. is read as . Conditions involving are written additively in .
Crossing times, argmins and . These take values in and . A path that never crosses has crossing time , and is literal. "" means that the path is bounded below from on and its infimum exceeds . The minimum is attained a.s. (Lemma 3).
Probabilities and limits. These are extended nonnegative reals. The liminf is taken in .
(5.1) correction. The paper derives from " statistically". In fact , so the milestone states the bound with . The printed form is false for and .
Theorem 3. The existence of , implicit in the paper, is a conclusion of the statement, so the lower bound cannot hold vacuously. The slippage-configuration limit in its second sentence is not stated.
Ruled out. None of the following can make the statements trivial, because the encodings above exclude them:
Infrastructure needed. A complete development needs the following, all reusable beyond this mission:
Contributions to any milestone are welcome.
Source. The source is the authors' arXiv preprint, version 3 (11 Dec 2023), and all numbering follows it.
Most display advertising is sold in first-price auctions: the highest bidder wins and pays its own bid. Since the industry's move away from second-price formats around 2019, a bidder can no longer bid its value and must instead learn how much to shade its bid, from data about how the other bidders behave. A demand-side platform faces this problem millions of times a day with very little information. When it wins it pays its bid and learns nothing about the competition beyond the fact that it won; when it loses it sees only the winning price.
Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research 2025) cast this as an online learning problem and gave the first bidding policies with regret against an arbitrary unknown distribution of competing bids. This mission is the first of a series of six on that paper. It covers the case of stochastic private values, and the route to it through a general class of contextual bandits.
A single bidder takes part in rounds. In round she observes a private value , bids , and the highest other bid (HOB) is . She wins iff , so her payoff is . The HOBs are iid with an unknown CDF on ; no continuity or shape assumption is made, and atoms are allowed. The values are iid with an unknown distribution on , independent of the HOBs.
Feedback is censored: at the end of round only the winning bid is revealed. A policy chooses from its own internal randomness, and . With the expected reward , the regret is
the gap to an oracle that knows .
The paper reaches its bound through partially ordered contextual bandits. These are contextual bandits with contexts and actions, rewards in , and a feedback graph on the actions. Playing reveals the rewards of and its out-neighbours under every context (cross learning). The graph is a transitively closed DAG, so it induces a partial order on actions. There is also a partial order on contexts along which some choice of optimal action is monotone (Definitions 2 and 3). Algorithm 3 is an arm-elimination algorithm for this class. The auction becomes such a bandit when values are clipped to the grid and bids are restricted to : a bid reveals for every .
The policy may depend on but not on or , and is absolute. The goal leaves the policy unspecified. That makes it the weakest stable form of the paper's result: any later policy with a better logarithmic factor still proves it.
The result. Theorem 1 shows that a bidder facing an arbitrary unknown competition distribution can learn to bid as well as the oracle up to . That rate is optimal up to logarithms: mission 3 of the series formalizes the lower bound. Theorem 5 is of independent interest. For partially ordered contextual bandits with iid contexts, the regret depends on the widths of the two orders and not on the numbers of contexts and actions. Mission 5 of the series shows that this fails for adversarial contexts.
Formalizing it. The results are proved in the paper, with full proofs in its Appendix C; none of them has a machine-checked proof. Beyond the theorems, the mission produces a reusable model of repeated auctions with censored feedback, with policies that are non-anticipating by construction. It also produces a definition of contextual bandits with graph feedback and cross learning, and an executable definition of an elimination algorithm with randomized exploration. Lemmas 3, 4 and 5 are self-contained and need no bandit machinery.
The obvious approach discretizes and runs one bandit algorithm per context. That gives regret and, after balancing against the quantization error of Lemma 4, only . Reaching requires information to flow across contexts. Lemma 2 says that a round with a small context feeds the minimum counts of every larger context. Lemma 3 turns this into a bound on the sum of confidence widths that depends on the width of the context order and not on . Lemma 2 is a statement about a randomized algorithm whose active sets depend on the whole past, and its proof uses the uniform choice among the sources of the active set together with the extra elimination rule (). The step from a high-probability bound to an expectation over iid contexts must keep the contexts independent of the rewards and of the algorithm's randomness.
Fin T: paper round is index . The grids (6) are finite sets of reals. Context and action of Fin M, Fin K stand for and . The paper's are .Fin (t+1) → ℝ and the feedback as Fin t → ℝ. It never sees , or . The expectation is an integral against .Not stated here: the adversarial parts of Theorem 5 and Corollary 1, Lemma 3.2, and the contextual form of Lemma 1. Proof contributions are welcome at every level. Useful infrastructure includes an anytime concentration bound for running means under adaptive sampling (the contextual Lemma 1) and Dilworth's theorem for finite posets (the step from to general in Lemma 3). Lemmas 3, 4 and 5 can be attacked first and independently.
Ranking and selection (R&S) asks which of simulated alternatives has the largest mean when each observation is noisy and the simulation budget is fixed. Large-scale problems, with thousands or millions of alternatives, arise in simulation optimization run on parallel computers, and for them the relevant question is how the total budget must grow with . A procedure is sample optimal when a budget linear in keeps its probability of correct selection (PCS) bounded away from zero as .
Li, Fan and Hong (arXiv:2303.02951, Management Science 2025) show that the simplest adaptive procedure, the greedy procedure, which always samples the alternative with the largest current sample mean, is sample optimal, and that an explore-first greedy (EFG) procedure, which first takes observations from every alternative and then runs the greedy procedure, is in addition consistent: its asymptotic PCS can be pushed to any level with a budget linear in .
The EFG procedure splits the budget per alternative, , into an exploration part and a greedy part . A natural guess is that most of the budget should go to the greedy phase, since the exploration phase alone is equal allocation, which is not sample optimal. Lemma 6 of the paper (§5.5, p. 25) shows the opposite: the greedy-phase budget needed for the paper's guarantee decays exponentially in . This mission formalizes Lemma 6.
Let be independent standard normal random variables and
their running average. For a level and a positive integer , the boundary-crossing time is
with , and its expectation is
For the running average eventually drops below and is finite; for it is infinite. Write for the standard normal cdf and .
In the R&S model, alternative has normal observations with mean and variance . Assumption 1 (p. 12) gives constants and such that the best mean exceeds every other by at least and every variance is at most . The paper's Theorem 3 (p. 23) shows that EFG with exploration budget keeps the PCS above a positive bound when the greedy phase receives at least
observations per alternative, for a fixed . In Lean the objects are GreedyRS.Budget.zbar, crossTime, Cn0 and Phi.
For , and , set
Then , , and
The result. Lemma 6 explains the budget-allocation behaviour of EFG: as the budget per alternative grows, almost all of it can go to exploration, and an exponentially small greedy phase still turns equal allocation into a sample-optimal and consistent procedure. The paper uses it to justify a simple proportional rule (a fixed fraction of the budget to exploration) when and are unknown, and it suggests that a short greedy phase may repair other non-sample-optimal procedures. The bound also gives an explicit, computable upper estimate of , for which no closed form is known when (p. 22).
Formalizing it. The result is proved in the paper; no machine-checked proof exists. The mission produces a formal model of the expected boundary-crossing time of a Gaussian running average, with values in , a tail-sum bound for it, and the standard Gaussian tail bound in the form . The companion missions of this series (Theorems 1, 2 and 4 of the same paper) use the same crossing-time objects.
The closing algebra is elementary; the difficulty is measure-theoretic. The crossing time is an extended-natural-valued random variable defined through the whole infinite path, and before its finiteness is known it may be infinite with positive probability, so its expectation must be handled in rather than as a real number. Relating it to normal tail probabilities requires the exact law of the running average under the infinite product measure, that is, the distribution of a sum of independent Gaussian coordinates, which is not a one-line consequence of the available library.
Measure.infinitePi (fun _ => gaussianReal 0 1) on ; entry of a path is .ℕ∞), and is a lower Lebesgue integral with values in . A crossing time typed in , where the infimum of the empty set is , would make finite for every and the goal easier than the paper's; this encoding is excluded.1 - Phi t with Phi the cdf of gaussianReal 0 1.Contributions welcome: the tail-sum formula for ℕ∞-valued expectations, the law of under the product measure, and the three milestones.
Networks observed over time — contact networks, communication graphs, brain connectivity recorded in sessions, trade networks — often change their structure abruptly at an unknown or suspected moment. Detecting such a change point from a sequence of snapshots is a basic statistical task, and in practice the snapshots are incomplete: some pairs of nodes are never queried, or their interaction is not recorded. Enikeeva and Klopp (arXiv:2106.14470, Operations Research, 2025) study this problem for inhomogeneous random graphs with missing links in the framework of minimax hypothesis testing (Ingster and Suslina, 2003). They give a test based on the spectral norm of a matrix CUSUM statistic that detects every change above a threshold (their Theorem 1), and a lower bound showing that changes of smaller order cannot be detected by any test (their Theorem 2). This mission formalizes the lower bound for a change at a known time.
There are vertices and time points. At time one observes a symmetric matrix with zero diagonal, whose entries , , are independent over pairs and over time with
Here is the matrix of connection probabilities (symmetric, entries in , zero diagonal) and the sampling matrix: pair is observed with probability , and . The product is entrywise. Sparsity is measured by the column norm , and the null class is
so bounds the expected observed degree.
Under the null hypothesis every snapshot has the same . Under the alternative with a change at time , snapshots have and snapshots have . With , the energy of the change is , the spectral norm of the observed jump weighted by the position of the change. The alternative class is the set of pairs in with energy at least .
A test is any -valued function of the observations. Its type I error is the supremum of over the null class, and its type II error the supremum of over the alternative class (Definition 1). Fix levels , , and put and .
With , and
if , ,
then every test with has . For this covers every with depending only on , so the minimax detection boundary is at least of order . The statement fixes no asymptotic regime: it holds for every , , and in range.
The lower bound is the half of the minimax result that cannot be obtained by exhibiting a procedure: it says that no test, however computed, separates the hypotheses below energy of order . Combined with the matrix CUSUM test of Theorem 1, which succeeds above plus a logarithmic term, it identifies the detection rate for a known change point. It also shows that missing links enter only through , the bound on observed degrees.
The result is proved in the paper; nothing in it is machine-checked. A formalization adds a checked statement of the minimax testing framework for a finite random-graph model (tests, type I and II errors over composite classes, the lower bound condition), a checked version of the second moment method for mixtures, and a checked Rademacher-chaos moment bound. While preparing the statements, two displays of the printed proof were found to be false as printed (see Formalization scope); the formal goal records the bound the corrected argument gives.
The minimax type II error is a supremum over a composite alternative class and an infimum over all level- tests, and neither can be handled directly. The lower bound requires choosing priors that sit inside both classes, reducing to a -divergence between two mixtures of product Bernoulli laws over sign vectors, and bounding the resulting exponential moment of a quadratic form in Rademacher signs. The last step is where the naive argument fails: a Gaussian-type bound on that ignores is false when , whose spectral norm is ; the exponential moment is finite only when stays below a constant.
The observation space is finite: one Boolean per time point and pair , with 0-based time in Lean. Probabilities are finite sums of products of Bernoulli weights; no measure theory is used, and a test is any Boolean function of the observation. The type I and II errors are real suprema of sets of probabilities in ; the level condition ranges over the whole null class, every sampling matrix included. Sampling matrices carry the standing assumptions , of §2. The spectral norm is the published HighDimProb.RandomMatrices.matrixOpNorm; sign vectors are Boolean vectors mapped to , and Rademacher expectations are averages over vectors.
Departures from the printed text, all disclosed in the statements:
Trivializing encodings are ruled out: the tests are unrestricted, the alternative class is nonempty for every admissible (milestone 3), and a lower bound on a supremum cannot hold vacuously on an empty class. When the hypotheses cannot hold for , matching the paper, where is the trivial boundary.
The development needs elementary finite probability over product spaces, Cauchy–Schwarz for the step, and a Rademacher-chaos exponential moment bound; the last is reusable well beyond this mission. Proofs of any milestone, and of the goal from the milestones, are welcome.
Linear models of opinion formation go back to DeGroot (DeGroot 1974), in which every individual repeatedly replaces their opinion by a weighted average of the opinions of the people they listen to, and to Friedkin and Johnsen (Friedkin–Johnsen 1990), who added a persistent internal opinion. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) add a random external (media) signal whose law may depend on the individual's attributes, which models selective exposure, and ask what the opinions look like on a large random social network. The answer is the behaviour of a typical individual, a uniformly chosen vertex: its stationary opinion converges in law to the opinion of the root of the network's local weak limit, and the empirical distribution of all stationary opinions converges to the same law. Questions such as consensus or polarization are then questions about one limiting random variable, independent of the particular realization of the network.
This mission formalizes that main result (Theorem 2) together with the fixed-graph stationarity theorem it rests on (Theorem 1).
A vertex-weighted directed graph on a vertex set gives each vertex an in-degree , an ordered list of inbound neighbours and weights with whenever . The parameters satisfy , , . The opinions evolve by recursion (1),
where the external signals are independent, i.i.d. in time given the vertex mark, and bounded by . With the operator this reads . The stationary vector is .
The full mark of a vertex is : a generic attribute, an internal opinion, a stubbornness label, the in-degree and the weights. Marks are compared by the metric
A random graph sequence has vertex set and attributes ; edges and weights are random given the attributes. The conditional expectation conditions on the attributes only. The in-component of depth of a vertex is the set of vertices with a directed path of length at most to . The sequence admits a strong coupling (Definition 4) with a rooted marked graph if, for two independent uniform vertices , every depth and every , there are two independent copies of whose depth- root in-components are, with conditional probability tending to one in probability, isomorphic to those of and , with all marks -close in and the two in-components of and disjoint. The Wasserstein distance is .
Assume a strong coupling, , and a signal kernel with . Then there are laws of and of , not depending on , with
for every continuous on , and geometrically fast:
A supporting statement of the proposal, not a milestone, is the tail bound for (proof of Theorem 2, p. 28).
Theorem 2 reduces the stationary opinion distribution of a large network to a single random variable attached to the local limit. When the limit is a marked Galton–Watson tree, has an explicit series representation whose mean and variance are computed in closed form later in the paper (the other two missions of this series), and these formulas are what explain consensus and polarization. Strong couplings exist ([Olvera-Cravioto 2022], cited on p. 8 of the paper) for Erdős–Rényi graphs, the Chung–Lu and Norros–Reittu models, the configuration model, stochastic block models and preferential attachment graphs, so the theorem applies to most random graph models used for social networks.
The result is proved in the paper; nothing in it has been formalized. On Prove2Me this is the first statement of a strong coupling, a form of local weak convergence for directed marked graphs, and of a stochastic recursion on a random graph. The definitions of in-components, the coupling event and the strong coupling are reusable for any local-limit statement about directed random graphs, and the contraction and time-reversal milestones are reusable for linear stochastic recursions.
The fixed-graph part is a contraction argument, but the coupled object is not the opinion process itself: does not converge almost surely, and only its time reversal does. The main difficulty is Theorem 2. A local limit controls one neighbourhood at a time, while the empirical averages need two uniformly chosen vertices to be asymptotically independent, which a one-vertex limit statement does not give. The errors in weights, signals and initial opinions enter at every vertex of a depth- neighbourhood, and the statements condition only on the attributes, with edges and weights integrated out. The stationary statement then requires an interchange of and that is uniform in .
All random objects of the -th model live on one probability space, and the -th graph has vertices (the paper's ), so a uniform vertex always exists. Signals are written and initial opinions with i.i.d. uniforms independent of the graph: this quantile representation is equivalent in law to the paper's conditionally i.i.d. signals. Neighbour indices are 0-based. The conditional quantities given are regular conditional distributions given the attribute vector, and "random variables whose distribution does not depend on " are encoded by fixed limit laws, with the paper's read as convergence in probability of the conditional laws, which is equivalent. Theorem 1 is stated on countably many vertices, with its geometric rate given as an explicit bound for 1-Lipschitz test functions of finitely many coordinates.
Disclosed choices: the strong coupling is stated on the given space with measurable events inside the coupling events (the event "an isomorphism exists" need not be measurable), with isomorphisms that preserve the order of inbound neighbours (which the proof uses), and through its second bullet, which implies the first. The paper's conditional independence of weight vectors given is not imposed. The strong coupling also requires the depth- in-components of and to be disjoint on the coupling event: the proof of Theorem 7 uses this, and without it Definition 4 admits a graph whose vertices all listen to a single hub, whose shared signals keep random. The page puts no condition on beyond conditional independence of the signals, but Theorem 2(1) at time is false then (take ); the statement assumes a -Lipschitz initial kernel with the same , which covers the paper's own simulations. The geometric rate uses the constant of the proof.
Trivializing readings are excluded: every tsum is absolutely summable under the hypotheses, conditional laws are regular conditional distributions of measurable random variables, the averages have no division by zero, and the limit laws are forced onto by the convergence, so no integral defaults to . Theorem 7 of the paper (the two-vertex coupling) is not a milestone. Contributions of proofs of any milestone, and of general lemmas on regular conditional distributions and Wasserstein couplings, are welcome.
Inverse optimization asks for the objective of an optimization problem when only its optimal decisions are observed. It was formalized for linear programs by Ahuja and Orlin (Operations Research 2001) and has since been used to infer costs, preferences and utilities from observed choices, for instance in routing, pricing and the imitation of expert planners (see the survey discussion in Chan, Lee and Terekhov, Management Science 2019, and the noisy-data setting of Aswani, Shen and Siddiq, Operations Research 2018).
Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) study a contextual version: the problems a decision-maker faces change from instance to instance, and the observed expert decisions constrain a fixed but unknown cost vector. Their question is not how to estimate the cost, but which decisions to take so that the loss against the expert is as small as possible in the worst case. This mission formalizes the answer in the offline setting, where a finite data set is given in advance. The text used is the arXiv preprint v3 (1 July 2023); all theorem numbers refer to it.
Actions live in and costs in , both with the Euclidean norm, and . The unknown cost lies on the unit sphere .
An instance is a pair : a feasible set , i.e. a nonempty compact subset of with diameter at most , and a context function , i.e. a -Lipschitz map . Given a cost , the forward problem is
a set of minimizers.
The offline data are with . The costs compatible with them form the knowledge set
A policy maps the data and a new instance to an action , and its regret on the instance is with . The worst-case regret is the supremum of the regret over , and .
The angle between two vectors is , with . The uncertainty angle of a set is
and a circumcenter is a point of attaining the infimum. Geometrically, is the aperture of the narrowest revolution cone containing and is its axis. The circumcenter policy answers an instance with any . Write .
For every realizable data set,
for the circumcenter policy , whatever circumcenter and whatever minimizer it picks. Conversely, for every there is an information set with on which every policy suffers regret at least on some instance. The upper bound and the lower bound are one statement.
Theorem 1 identifies the minimax offline regret of contextual inverse optimization with a single geometric number of the knowledge set, (or ), and shows that one explicit policy, acting as if the cost were the circumcenter, attains it uniformly over all instances. It reduces the design of offline policies to computing a circumcenter, and it is the benchmark that the paper's online analysis (§4–§5) compares against: the online policies are judged by how fast they shrink the uncertainty angle.
The results are proved in the paper (App-3–App-9). To our knowledge none of them has a machine-checked proof. Formalizing them yields a verified statement of the minimax value, a reusable notion of uncertainty angle and circumcenter for arbitrary subsets of , and the exact tightness of the bound, including the regime where nature can force the maximal regret.
The upper bound is not a direct consequence of the definitions: the regret involves an arbitrary compact action set and an arbitrary -Lipschitz context, and the only link between the circumcenter's choice and is that is optimal for the wrong cost. Lemma 1 is where this link is turned into an angle, and its value must be matched exactly, not up to constants. Lemma 2 requires care because the objective is a supremum over an arbitrary, possibly non-closed, set and the angle convention at breaks continuity. The lower bound must hold for every policy, including ones that exploit tie-breaking, so the hard instance must be chosen after the policy.
Vectors are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin d). The angle vecAngle is defined directly with value when either argument is ; Mathlib's InnerProductGeometry.angle (which is there) is not used. is a real infimum over the sphere of a real supremum over ; the angles lie in , so both are genuine when is nonempty. Action sets are nonempty compact sets of diameter at most (nonemptiness is added: an empty feasible set has no action), contexts are -Lipschitz, and data are indexed by Fin N.
Committed conventions and pins:
IsGreatest, and the lower bound of Theorem 1 in attained form, which implies the paper's statement about the supremum.A formalization that bounds the regret only for one selected minimizer of the forward problem, or that chooses the hard instance before the policy, proves a different and weaker theorem and is excluded.
The development needs: compactness and lower semicontinuity on the sphere (existence of a circumcenter), elementary spherical geometry for the uniqueness and for as the value of a two-point instance, and monotonicity of on . The angle, uncertainty angle and circumcenter definitions are reusable for the online missions of this series. Proofs of the two lemmas are the natural first contributions.
A budget-feasible procurement auction buys services from strategic sellers under a hard budget. Each of bidders can provide a service at a private cost; the auctioneer values each set of acquired services through a set function and must keep total payments within a budget . The question, introduced by Singer (FOCS 2010), is how much of the optimal value a truthful mechanism can secure when it does not know the costs. The model covers crowdsourcing, influence maximization with paid seeds, and experimental design with paid participants.
For subadditive valuations, the most general class with non-trivial guarantees, the timeline is short:
Clock auctions are prized beyond truthfulness: they are obviously strategy-proof, they protect the privacy of the winners' costs, and a bidder only ever decides whether to accept a price that keeps falling.
There are bidders . Bidder has a private cost , the least payment for which it provides its service, and it accepts an offered price exactly when . The auctioneer has a budget and a valuation . The valuation is subadditive:
It is not assumed monotone, nor normalized.
A set is budget feasible at true costs if ; the optimum is the largest value of such a set. A mechanism outputs a set and payments for ; it is budget feasible if , and it is a -approximation if on every instance.
Mechanism 4 runs in phases and keeps a set of active bidders and two solutions and , all starting from , . While some active bidder lies outside , a phase
At price a set of candidates is affordable exactly when it has at most members, so the oracle returns a subset of with at most members whose value is at least half that of every such subset. The paper uses the demand-query algorithm of Badanidiyuru, Dobzinski and Oren for this step. The mechanism returns the more valuable of the two solutions, , and pays each of its members its current price.
There is an absolute constant such that for every , every instance as above, every oracle with the 2-approximation guarantee and every run of Mechanism 4 of at least phases,
The constant is left unspecified, as in the paper's ; the proof gives roughly for large .
Theorem 8 shows that randomization buys nothing asymptotically for budget-feasible procurement with subadditive valuations: the best known approximation factor is achieved by a deterministic mechanism, and moreover by a clock auction, which adds obvious strategy-proofness and transparency. It improves the previous best deterministic factor from to . The same template, two maintained solutions and a gradually refined benchmark, drives the paper's constant-factor auctions for submodular valuations (the companion missions of this series).
Nothing in this paper is formalized yet, and no budget-feasible mechanism exists on the platform. The mission produces a machine-checked model of a clock auction with an abstract demand oracle, a monotonicity lemma for two-solution auctions, and the counting argument behind the factor, which is a self-contained real inequality.
The obvious argument looks only at the phase whose size bound matches a large block of the optimal set and invokes the oracle there. It fails because part of may already sit in , which is never offered to the oracle again, and because the output is decided in the last phase, when the bidders of may have been priced out. Both gaps have to be closed with properties of the run (what the oracle guaranteed when was formed, and that the value of the output never decreases), not of a single phase.
The second case of the analysis, where every block is small, is a counting argument whose final contradiction is asymptotic and involves terms that are only meaningful for large . A statement with a single uniform constant must also cover small , which the printed argument leaves implicit.
Fin n, sets are Finset (Fin n), values and costs are real. Non-negativity of and are hypotheses; subadditivity is IsSubadditive v. No monotonicity or normalization is assumed.alg : ℕ → Finset (Fin n) → Finset (Fin n) satisfying IsTwoApproxOracle v alg; feasibility at price is encoded as cardinality at most .Contributions welcome: proofs of the milestones and the goal; a concrete demand-oracle implementation satisfying IsTwoApproxOracle; and a definition of the block decomposition with the cost chain of p. 16, which this mission does not state.
In budget-feasible procurement an auctioneer with a fixed budget wants to buy services from strategic sellers whose costs are private. The auctioneer values sets of services through a valuation function , and wants a mechanism that pays the sellers at most in total while acquiring a set of nearly maximal value. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a platform recruits workers or data owners under a fixed spending cap.
Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) study deterministic clock auctions for this problem: mechanisms that offer each seller a sequence of non-increasing prices, where a seller who rejects an offer leaves for good. Clock auctions are obviously strategyproof and robust to collusion, which makes them attractive in practice. A posted-price mechanism is the most restrictive kind: every seller receives a single take-it-or-leave-it offer.
Appendix B of the paper asks how much is lost by restricting to posted prices. For additive valuations no deterministic posted-price mechanism beats (Theorem 13). For symmetric submodular valuations, where the value of a set depends only on how many sellers it contains, no such mechanism achieves a factor better than (Theorem 14), and Theorem 15, the subject of this mission, shows that a simple posted-price mechanism achieves a logarithmic factor.
There are sellers (bidders) . Seller has a private cost and accepts an offered price exactly when . The auctioneer has a budget , and throughout this mission every cost satisfies , as the paper assumes for Mechanism 5.
A valuation is symmetric submodular if there are numbers such that
The case counts the sellers bought.
A set is budget feasible at true costs if ; the optimum is the largest value over such sets.
Mechanism 5 (p. 27) sets aside an arbitrary seller and keeps a counter of accepted offers, initially , and a winning set , initially empty. It visits every other seller once, offering
a seller who accepts joins and increments . If nobody accepted, is offered the whole budget . Winners are paid their offered price. In Lean the mechanism is BudgetClock.PostedSym.mech5 n B c j, the loop is scan n B c j, and the valuation class is IsSymmetricSubmodular n v.
There is an absolute constant such that for every , every symmetric submodular , every budget , every cost vector with and every choice of the set-aside seller , the winning set of Mechanism 5 and its prices satisfy
The constant is left unspecified, as in the paper's ; the goal survives any improvement of it.
Theorem 15 locates the price of posting prices for symmetric submodular valuations: together with Theorem 14 (no deterministic posted-price mechanism beats ) it shows that the best such mechanism loses a factor of order exactly , while the clock auctions of the main body of the paper achieve constant factors for all monotone submodular valuations. The gap between one-shot offers and descending clocks is therefore a genuine separation, not an artefact of the analysis.
The result is proved in the paper. Its formal value lies in pinning down the mechanism and the constants. Checking the printed argument against a precise model exposes three slips: the pseudocode never adds the set-aside seller to , the printed payment bound fails for , and the constant of Case 2 ignores the set-aside seller and is false (see the milestone notes). None of them affects the claim, and the formal statements record the corrected forms. To our knowledge no machine-checked proof of any result of this paper exists.
The mechanism decides each offer without knowing the remaining costs, and the optimum is defined at the true costs, which the mechanism never learns for rejected sellers. The only information available is a lower bound on each rejected seller's cost, and these lower bounds shrink as the counter grows. The difficulty is to convert the history of offers into an upper bound on how many sellers any budget-feasible set can hold, uniformly in the order of the scan and the choice of , while keeping the total payment, a harmonic-type sum, below the budget for every . The set-aside seller is the subtle point: it receives no offer when , so nothing is known about its cost, and a count that forgets it is wrong.
Fin n; costs are a real vector with ; the budget is a real (the paper says only "a budget "; is an added hypothesis, since a zero budget makes every offer zero).r 0 is ).A complete development needs elementary facts about finite sums, the harmonic numbers (, available in Mathlib) and a reasoning principle for the left fold that defines the scan; the latter is reusable for any sequential posted-price mechanism. Proofs of the three milestones, and of the goal from them, are all welcome.
A portfolio manager who observes a covariate today, say a vector of macroeconomic indicators , wants an allocation that performs well on the returns that follow such a covariate. With finitely many historical pairs the conditional law of given is poorly estimated: usually no sample has covariate exactly , and few have covariates near it. Distributionally robust optimization hedges against this estimation error by optimizing against the worst distribution in a ball around the empirical one. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research, 2025) study this problem with an optimal transport ball and a conditional objective. Before giving tractable reformulations they identify the regimes in which the robust problem is degenerate. This mission covers one of those regimes, a transport budget large enough to empty a fiber of positive radius.
Let and be Polish spaces (covariates and returns) and let , , be the data, with empirical distribution . Ground costs and combine into the separable cost . The optimal transport cost is the least expected cost over couplings of and , and the ambiguity set is the ball
The conditioning event is the fiber , with and fiber radius . For a loss (the loss of a fixed portfolio at return ) the worst-case conditional expected loss is
problem (12) of the paper, where the strict inequality avoids conditioning on null sets. The threshold
is the least budget that empties the fiber. With and the cost from to the boundary , the paper computes it in closed form. Throughout, the paper's Assumption 2.4 holds: the costs are symmetric, nonnegative and continuous, and vanishes exactly on the diagonal; projections onto are unique; and every boundary point of has points outside it at arbitrarily small cost.
For and , and every loss ,
Proposition 4.2 is a negative result with a practical consequence: when the budget exceeds , the robust conditional loss equals the worst loss over the whole return space and ignores the data. The modeler must therefore keep , and Proposition 4.1 makes that threshold computable from the samples. In that regime the paper replaces the strict constraint by a positive mass requirement (Proposition 4.3) and derives a finite-dimensional dual (Theorem 4.4); those results are separate missions of this series.
The results are proved in the paper; none is formalized. The mission formalizes them in Lean 4 on top of Mathlib, using a published optimal transport cost and a published extended-real integral. The decomposition (24) is reusable for every argument about empirical optimal transport balls with finitely many atoms. The formal statement of Proposition 4.1 makes explicit a regularity condition on the boundary that the paper's proof uses but does not state.
The upper bound is elementary. The lower bound needs, for each , a feasible distribution whose conditional law on the fiber is concentrated at . The construction printed on p. 46 keeps a positive mass of a sample inside the fiber, so its conditional expectation mixes with a sample loss; that construction has to be corrected. Proposition 4.1 needs a matching lower bound on the cost of every fiber-emptying coupling, and an exit cost from the fiber that equals the boundary distance . For a general continuous this fails. The decomposition (24) needs an optimal coupling to exist, which on Polish spaces with a lower semicontinuous cost is Villani's existence theorem. Mathlib does not have that theorem.
Fin N with ; repeated samples are allowed.RWPI.SqrtLasso.transportCost, an infimum over couplings with a -valued cost; the paper's "min" is not built into the definition.EReal (ModelRiskOT.Duality.extIntegral), never a Bochner integral, which would assign to a non-integrable loss. Both sides of the goal are extended reals; may be .ENNReal.ofReal ρ; the hypothesis forces , and (24) carries .BoundaryRegular, which is not in the paper: the boundary is nonempty, the exit cost of a sample inside the fiber equals , and for samples outside. It mentions only and the samples and holds when is a norm distance. The goal does not carry it.Trivializing formalizations are ruled out: no conditional expectation is evaluated at fiber mass zero, the expectation is not a Bochner integral, cannot enter through ofReal, and the supremum is over the ball with positive fiber mass, not over all measures.
Needed infrastructure: finitely supported measures and their couplings, convexity of , and for (24) the existence of optimal couplings on Polish spaces. These are reusable well beyond this paper, and contributions toward them are welcome.
A retailer that operates several physical stores can show a customer who finds nothing she likes in her store the products that other stores carry, for example on an in-store screen or a magic mirror, and ship the chosen product from the other store. The customer then buys at a utility discount: shipping takes time and the product cannot be tried on. Liu, Chen, Liu and Wan (2025) compare two ways of making such recommendations. Under simultaneous recommendation (SMR) all products of all stores are shown at once; under sequential recommendation (SQR) the customer first sees the products of her own store and is shown the other stores' products only if she buys nothing. The SQR choice model is the impatient-customer multinomial logit (MNL) model of Gao et al. (2021) applied store by store.
Under SMR the seller can do no better than letting every store offer the single-store optimal assortment (Theorem 1 of the paper, the subject of mission I of this series). Under SQR the seller can do better: the assortment of one store becomes a second-chance offer to the customers of every other store. The SQR problem with general discounts is NP-hard (Proposition 3 of the paper). This mission formalizes the structural result that makes the problem tractable when the discounts depend only on the store a customer visits.
A seller runs stores and sells products. A fraction of the customers visits store , with . Product has revenue , with , and attraction value ; not buying has attraction . A profile lists the assortment of each store, and . A customer of store who buys product from store pays a utility discount , with , and is the smallest such discount over the stores that offer . Under SQR the probability that a customer of store buys product is
and otherwise, where and . The seller maximizes the expected revenue
The discounts are universally homogeneous if for all , and store-wise homogeneous if for all : the discount depends only on the store the customer visits. The single-store problem is (3). An assortment is revenue-ordered if it equals for some , and denotes the smallest revenue-ordered optimal solution of (3).
If the discounts are store-wise homogeneous, and , then some optimal solution of (SQR) satisfies
with every revenue-ordered.
Theorem 4 reduces the SQR problem with store-wise homogeneous discounts from a search over profiles to a search over nested chains of prefixes, of which there are polynomially many for fixed . It also gives an operational rule: the store with the lowest demand and the largest discount for its customers carries the widest assortment, wider than the single-store optimum , and every other store carries a prefix that fits inside . Example 2 of the paper (p. 18) shows that when the two orderings point in opposite directions an optimal solution need not be revenue-ordered, so both hypotheses carry weight.
The result is proved in the paper's Online and Additional Supplements. None of it is machine-checked. A formal development would also settle two places where the printed proof is incomplete: the proof of Proposition B.2 ends with "If we continue the analysis, one can show…", and it applies Lemma B.4 with some coefficients and a reordered index, outside the lemma's stated hypotheses.
The revenue of one store depends on the assortments of all others through , and the objective is a sum of ratios of ratios. The classical argument for MNL assortment problems, that a product with revenue above the current optimum should be added, does not transfer: adding a product to store raises store 's first-step revenue but also changes the second-step offer to every other store's customers, and removing it from store moves it into the second step. A local exchange that improves one store can hurt another, so revenue-ordering has to be established jointly with the nesting, and the order of the stores (by and by ) determines which exchanges are safe.
Products are Fin n and the paper's product is index ; stores are Fin (M + 2), so and stores , are the last two indices. Assortments are Finset (Fin n). The attraction values are the primitive data. The factor is the largest over the stores offering , and when none does. The choice probabilities (2) and the objective (SQR) are the model; the Gumbel derivation of (2) (Proposition 1, from Gao et al. 2021) is not formalized. Store-wise homogeneity is a predicate on a general discount array, not a separate model.
The standing assumptions of §3 are explicit hypotheses everywhere: , , , , . Two hypotheses are pinned and disclosed: (revenues are prices; Lemma B.3 is false with a negative revenue), and wherever revenue-ordered sets appear, since with is nonempty. Lemma B.3 takes nonnegative revenues and attraction values, because the proof of Proposition B.1 applies it to proxy products that may be empty.
"Optimal" means a global maximizer of (SQR) over all profiles, ties allowed. enters as the hypothesis that a given set is the smallest revenue-ordered optimum of (3); the first milestone shows the hypothesis can be met, so the goal is not vacuous. A formalization in which is an arbitrary optimum, the discount factor ignores which store offers a product, or is fixed to would be a different theorem and is ruled out. The inequalities (B.4), (B.5) and those of Step 3 are stated for every profile of the stated shape rather than only for an optimal one, since for an optimal profile they would hold trivially.
A complete development needs finite-sum manipulations of MNL ratios, a reusable lemma that the single-store MNL problem has a revenue-ordered optimum, and quasi-convexity of sums of linear-fractional functions (Lemma B.4, a pure real-analysis statement of independent use). Contributions of any milestone, of alternative proofs of Theorem 4, and of proofs of the companion Theorems 2 and 3 are welcome.
Small third-party sellers on e-commerce marketplaces (Amazon, JD.com, Alibaba) typically have little capital and limited credit history, so they finance procurement through short-term credit. The traditional source is trade credit: the supplier ships the goods and is paid after the sales. Since about 2011 the platforms themselves lend to their sellers (the Amazon Lending Program, Ant Group's micro-loans, JD Small Loan), a form of finance called platform financing. The usual argument for platform loans is that platforms have cheap capital and rich data. Huang, Lai, Wang and Xiao (SSRN 4014045; published in Management Science, 2024, doi:10.1287/mnsc.2022.00201) remove both advantages: supplier and platform have the same capital cost and the same information. They ask whether a platform loan can still help the seller and the supplier, and at which interest rates.
The paper builds on the literature comparing supply-chain finance with bank finance, for example Buzacott and Zhang (2004) on asset-based financing and Kouvelis and Zhao (2012) on supplier versus bank financing of a newsvendor. The new feature is a third lender, the platform, which also collects a share of the revenue.
A supplier produces at unit cost . A seller with no capital procures units and sells all of them on a platform at the market-clearing price . The market size is uniform on , where measures uncertainty. The platform keeps the share of revenue, and the seller receives . Supplier and platform both have capital cost equal to the risk-free rate . The paper assumes , so selling is profitable in expectation, and that the smallest market size keeps the price positive.
The seller has limited liability: if her revenue falls short of what she owes, she hands over all of it. If she owes per unit, her expected profit is
Each scheme is a two-stage Stackelberg game: the supplier chooses , then the seller, having observed , chooses . Its subgame-perfect equilibrium gives the profits (seller and supplier under trade credit) and (under platform financing).
The paper defines two piecewise threshold functions of . They are built from the thresholds and the rates , all explicit in :
The goal states that and that, for every pair of equilibria of the two games,
The theorem says that a platform loan never benefits the seller while hurting the supplier. The outcome "win for the seller, loss for the supplier" does not occur. Whenever the platform's rate is low enough to help the seller, it also helps the supplier. Combined with Proposition 3, it identifies the mechanisms that make a platform loan attractive even without a cost-of-capital or information advantage: an interest subsidy at low uncertainty, risk mitigation at moderate uncertainty, and risk isolation at high uncertainty, where exceeds . The thresholds are explicit, so the result tells a platform the range of rates at which its lending creates value for both supply-chain parties.
The paper's proofs are long case analyses on closed-form radicals. Several displayed formulas in the manuscript contain printing errors (listed below), and some comparisons are justified as "it can be verified". A machine-checked development would certify the closed forms and the threshold algebra and settle the boundary cases. None of these results is formalized in Mathlib or in the Prove2Me library as of October 2026.
The equilibrium is not given by first-order conditions alone. Under limited liability the seller's objective is not concave in : it has a no-default regime and a default regime, and the maximizer jumps between them at . The supplier's problem under trade credit is therefore a comparison of two local optima: one quadratic, one a cubic in with a radical maximizer. The winner switches at , which involves . The comparisons of Propositions 3–6 then require sign analyses of differences of nested radicals across up to five regimes, ordered by and over .
Equating first-order conditions is not enough: equilibrium uniqueness requires excluding the off-path behaviour of the seller and handling the supplier's indifference at and .
Expectation. over is the normalized interval integral . All integrands are continuous.
Equilibrium. A strategy profile is a price together with an order rule defined at every price. A subgame-perfect equilibrium requires two things:
Two tie-breaks are part of the definition, both the paper's own conventions:
Goals quantify over equilibria. The closed forms enter only through the milestones. A statement taking the closed forms as hypotheses, or proving only , is not this theorem.
Standing assumptions.
Corrected slips, each disclosed in its item:
Boundary. Propositions 3–4 exclude the rate from their "otherwise" clause only for , where makes and the paper's statement and proof disagree; for other the boundary rate is kept, as on the page.
A complete development needs the following:
The best-response analysis under limited liability is reusable for other newsvendor-type financing models. Contributions of any milestone, of lemmas on the threshold order, and of alternative proofs are welcome.
Music streaming platforms collect a subscription fee from each user and pass a large share of the revenue to the artists. How that money is divided has become a policy question. Most platforms use the pro-rata rule: all fees are pooled and each artist is paid in proportion to their share of all streams. The main alternative is the user-centric rule: each user's fee is divided only among the artists that user played, in proportion to that user's own streams. The choice decides whether a heavy listener's tastes count for more than a light listener's, and it has been debated by platforms, rights holders and regulators.
G. Bergantiños and J. D. Moreno-Ternero, Revenue Sharing at Music Streaming Platforms (arXiv:2310.11861, Management Science, 2025), study the question axiomatically and through cooperative game theory. This mission formalizes their Theorem 3: once one asks that no group of artists can be paid less than the money of the users who only listened to that group, the user-centric rule is the only homogeneous and additive option. Two sibling missions treat Theorem 1 (axiomatic characterizations of pro-rata and user-centric) and Theorem 2 (the core of the streaming game).
There are artists . A streaming problem consists of a finite set of users and the numbers of times user played artist ; every user has played at least one artist. For a user let
the user's total streams and the list of artists the user played. Each user pays , so the amount to be shared is .
A popularity index assigns to each problem a nonnegative vector with positive total. Artist is then paid
Indices that are positive multiples of each other pay the same, and are identified. The user-centric index is .
The streaming game of a problem is the cooperative game on the artists with worth , the money of the users who only played artists in . Its core is
The axioms are:
The domain consists of the problems in which no user has played every artist, for all .
On , an index satisfies homogeneity, additivity and core selection if and only if there is with
The theorem singles out the user-centric rule by a stability property rather than by a fairness postulate about users. Core selection says that no coalition of artists receives less than the payments of the users who listen exclusively to that coalition; the pro-rata rule violates it already in a two-user example (p. 14). Together with Theorem 1 of the same paper, it gives two independent routes to the user-centric rule, which is the form in which the result enters the policy discussion.
The paper proves the theorem in its appendix (pp. 23–25). Nothing about streaming problems, popularity indices or this characterization has been formalized before; the mission produces a machine-checked version of the model, of the user-centric index's membership in the core, and of the characterization. The model layer (problems as finitely supported stream tables, rewards, the streaming game) is shared in shape with the two sibling missions.
Each axiom is easy to verify for the user-centric index; the content is the converse. Homogeneity and additivity alone allow every weighted index, where each user's streams are weighted by an arbitrary positive function of the user and the profile, and pro-rata is one of them. The difficulty is to extract from core selection, which only constrains ratios of index values through the reward normalization, that every user carries exactly the same total weight. Core selection on a single user only fixes the shape of the index on that user's list; comparing two users requires problems with several users, and the comparison of two users whose lists overlap cannot be made directly.
Artists are Fin n (0-based). Users are natural numbers, and a problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) whose support is the user set . This builds in three standing assumptions of the paper: every user of a problem has played some artist (), streams are natural numbers, and an index can depend only on the columns of the users of the problem. The core is the published Supermodularity.Cooperative.Core on Finset.univ. Rewards use ; at the empty problem the reward vector is and the core of the zero game is .
Two readings are committed to and disclosed:
The index requirements (nonnegativity, positive total) are imposed on nonempty problems of only; demanding a positive total at the empty problem would make every index impossible and the theorem vacuous. "Is the user-centric index" is one global , not a constant depending on the problem: a problem-dependent constant would turn the conclusion into a much weaker statement. With one artist holds only the empty problem and the theorem is vacuous, as on the page; no hypothesis on is added. The milestones on one-user problems are stated for arbitrary nonzero profiles of a user, which is the same as the page's columns of a problem in .
A complete development needs finite-sum manipulation over Finsupp supports and the decomposition of a problem into its one-user problems. Proofs of any milestone are welcome, as are proofs of Theorem 2's inclusion , which milestone 1 needs.
Decision theory under uncertainty distinguishes risk, where probabilities are known, from ambiguity, where they are not. Ellsberg's (1961) urn experiments showed that people's choices between bets on the same kind of event depend on where the uncertainty comes from: a bet on a known urn is preferred to the matching bet on an unknown urn. Tversky and Fox (1995) found that basketball fans prefer bets on basketball games to bets with matched objective chances. Models of ambiguity therefore have to let attitudes depend on the source of uncertainty.
Baillon, Bleichrodt, Li and Wakker (Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10), 2025) take sources to be algebras of events and propose source theory: within each source the agent behaves as if events carry probabilities, transformed by a source-dependent weighting function, while different sources may be weighted differently. The behavior within one source is probabilistic sophistication in the sense of Machina and Schmeidler (1992), restricted to that source. This mission formalizes the paper's first main result, Theorem 1: a characterization of when a single source admits such a probability, entirely in terms of two ambiguity attitudes that are measured in experiments.
A state space carries an algebra of events, and is a set of outcomes. An act is a finite-valued map whose level sets are events; it is from an algebra if its level sets lie in . The binary act pays on and on . The agent has a preference on acts.
Structural Assumption 1 (p. 8771) requires that is a weak order represented on binary acts by biseparable utility: there are a utility and a weighting function on events (, , monotone) such that for the act is valued . It further requires three nonindifferent outcomes, convex rangedness of (between two nested events every intermediate weight is attained by a nested event), strong monotonicity, cumulative dominance and the Archimedean axiom. Events are ranked by : means .
A source is a subalgebra of on which is convex ranged. It is uniform (source theory holds for it, Definition 1) if there is a finitely additive probability measure on such that for all acts from
Two attitudes compare sources and . is preferred to (Definition 2) if for all , ,
is more insensitive than with insensitivity region (Definition 4) if for all ordered threefold partitions of from and from ,
The region is regular for if every fourfold partition of from has a cell with and .
For a source under Assumption 1,
Theorem 1 gives source theory a behavioral foundation: whether a source admits an a-neutral probability measure can be read off from comparisons of bets on its own events, without assuming expected utility for risk. Uniformity is what makes the paper's quantitative tools available. Once a source is uniform, its weighting function factors as , and Theorems 2–4 of the paper compare sources through the pmatcher between their source functions; Theorem 4 uses Theorem 1 as a step. The uniqueness of (milestone 8) is what makes the source function well defined.
The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The proof relies on a classical representation theorem for qualitative probability (Krantz, Luce, Suppes and Tversky, 1971, Theorem 5.2.2), which is not in Mathlib either. A complete development would give Lean a first framework of Savage-style acts, biseparable utility and comparative probability, which other decision-theory missions could reuse.
The necessity half rests on the probability of a uniform source representing event preference strictly, which needs strong monotonicity and the range of on a convex-ranged source. The sufficiency half is the hard one. From the two attitude conditions alone one has to derive de Finetti's additivity (Lemma B.1). Its proof is a case analysis that uses regularity of the region to guarantee that one of the cells is a genuine middle event. One then needs a representation theorem for qualitative probabilities on an algebra, with uniqueness, in the finitely additive setting. Dropping regularity is not an option: without it the region , makes insensitivity nearly empty, and source preference alone does not imply uniformity (the paper's Example 1). The obvious route through countably additive measure theory is not available either, because the probabilities are only finitely additive.
All statements share one module, SourceTheory.Uniform.Model. It holds acts (IsActFrom), binary acts (bet), null events, convex rangedness, Assumption1 (a structure with one field per clause of Assumption 1), sources (IsSource), finitely additive probabilities (IsProbOn), uniformity (IsUniformWith, IsUniform), IsPreferredTo (Definition 2), IsMoreInsensitive (Definition 4) and IsRegularRegion. Its text is shared verbatim by the four missions on this paper. The conventions are:
Assumption1, and each source carries its own via IsSource. Reading it over every subalgebra would make Assumption 1 unsatisfiable, because has no event of weight .Statement (ii) carries an existential region, and it must be regular. A version without regularity, or with uniformity replaced by " for some ", would be a different and weaker theorem.
Needed infrastructure: comparative-probability representation (Krantz et al. 1971, Theorem 5.2.2, or a direct construction via convex rangedness), finitely additive measures on set algebras, and the range of a finitely additive probability that represents a convex-ranged weighting. Proofs of the milestones, of the representation theorem as a reusable lemma, and sanity models of Assumption 1 (for instance an expected-utility agent on with Lebesgue measure) are all welcome.
A seller who must auction one item without knowing how buyers value it needs a mechanism that performs acceptably against every plausible value distribution. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478, Operations Research 2025) measure performance by regret: the expected revenue lost relative to a seller who knows the realized valuations and extracts the highest one. Their main result (Theorem 1, the subject of mission I of this series) shows that against independent and identically distributed valuations the minimax-regret mechanism is a second-price auction whose reserve price is random, drawn from an explicit distribution.
Practitioners rarely randomize reserves. The natural benchmark is the familiar second-price auction with a fixed deterministic reserve , and the question this mission addresses is how much is lost by insisting on a deterministic reserve: what is the worst-case regret of that auction, and which reserve minimizes it? The paper answers this exactly in Proposition 5 (§5.2.1, p. 24, proof in Appendix D, pp. App-10–11). For a single buyer, regret-optimal posted pricing was studied by Bergemann and Schlag (2008), where a deterministic price has worst-case regret ; Proposition 5 is the -buyer version of that benchmark.
There are buyers with valuations in the type cube , drawn from a joint distribution unknown to the seller. Write and for the second-highest valuation. A direct mechanism charges buyer a payment , and its regret under is
The second-price auction with reserve , , gives the item to the highest bidder if the highest bid is at least , at price , and otherwise does not sell. Its revenue is .
Three classes of distributions on are considered:
The worst-case regret of over a class is . The closed form found by the paper is
called wcFixed n r in the Lean development.
For every , every class and every ,
the no-reserve auction has for and for , and
with the unique minimizer.
The result. Proposition 5 gives the exact price of determinism. The optimal fixed reserve has worst-case regret : for one buyer, for two. The minimax regret of the optimal randomized auction is about and for the same cases, so the benchmark shows how much of the paper's improvement comes from randomizing the reserve. Both values converge to as . Proposition 5 also shows that the worst case does not change when valuations are positively dependent (affiliated, or mixtures of i.i.d.), the same robustness the paper establishes for its optimal mechanism.
Formalizing it. The result is proved on paper in the paper's Appendix D, and no machine-checked version is known. A formal proof needs an expression of the expected revenue of a second-price auction through the order-statistic CDFs, a careful treatment of atoms at the reserve, two elementary but fiddly one-variable optimizations, and, for and , the reduction to the i.i.d. case.
The supremum over is not attained. The auction's revenue jumps at the reserve: a buyer valued exactly at buys, while one valued just below does not. Nature exploits this with two-point laws placing mass just below and the rest at , and the regret approaches only in the limit. So the first idea, exhibiting a maximizing distribution, fails, and any formalization must treat the worst case as a least upper bound. The upper bound over is the real difficulty: it rests on an order-statistic identity and on an inequality between the CDFs of the maxima of and affiliated valuations, which in turn needs properties of affiliation that are quoted from Milgrom and Weber (1982) rather than proved in the paper. For the bound needs the regret to be linear in the mixing measure, i.e. a disintegration of the mixture law through its joint CDF.
Fin n; valuations are vectors Fin n → ℝ; a distribution is a probability measure on Fin n → ℝ whose complement of the cube is null. is the set of products Measure.pi (fun _ => G) of a probability law G on . uses a probability measure on Measure ℝ with the Giry σ-algebra and states the CDF identity of Definition 6 for every .SPA ρ at ρ = Measure.dirac r; the winner pays when its bid is at least . Ties go to the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule).IsLUB of the set of regrets, not a maximum and not sSup. "The optimal reserve" is IsLeast of on , its value at , and uniqueness of the minimizer.IsGreatest would be false (the supremum is not attained); sSup of the regret image would be a junk value if the image were unbounded; classes without the support condition, or unconstrained, change the theorem.Ranking and selection (R&S) is the problem of identifying, by simulation, the alternative with the largest mean performance among candidates, when each alternative can only be observed with noise. It is a basic tool of simulation optimization, with roots in Bechhofer's indifference-zone formulation (Bechhofer 1954). Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and for such large-scale problems the relevant question is how the total sampling budget must grow with to keep the probability of correct selection (PCS) from collapsing.
Li, Fan and Hong (arXiv:2303.02951, Management Science 2025) call a procedure sample optimal if a budget linear in , , keeps . Order is the least any procedure can use, since every alternative needs at least one observation. As the paper recalls, Zhong & Hong (2022) and Hong et al. (2022) show that well-known procedures such as KN (Kim & Nelson 2001) and OCBA (Chen et al. 2000) need a budget of order ; the procedures previously proved sample optimal, median elimination (Even-Dar et al. 2006) and the knockout-tournament procedures, rely on a rigid halving structure with carefully planned allocations in each round. The paper's surprising observation is that the simplest procedure of all, the greedy procedure, which always samples the alternative that currently looks best, is already sample optimal.
There are alternatives. Alternative yields independent observations , independent across alternatives, and alternative is the unique best: for . Write for the running average of alternative .
The greedy procedure (Procedure 1) with total budget :
The PCS is the probability that alternative is selected. The asymptotic regime is fixed by Assumption 1: there are constants and with and , however large is.
For an i.i.d. sequence with running average , the crossing time of a level is . With the standard normal distribution function, the paper's key function is
which equals (Lemma 2). Finally, is the boundary, the first time it is attained, and the boundary-crossing time of alternative .
Under Assumption 1, if with , then there is with , and
The constant and the gap are free; the bound depends only on the shape of .
The result. Theorem 1 shows that a procedure with no tuning parameters, no elimination and no knowledge of or achieves the optimal order of budget growth for large-scale R&S. It gives an explicit, computable lower bound on the limiting PCS. The companion Theorem 2 of the paper shows that this bound is the exact limit under the slippage configuration with a common variance, so the constant cannot be improved in general. The same boundary-crossing analysis underlies the paper's explore-first variant, which turns the positive limit into an arbitrarily high one.
Formalizing it. The result is proved in the paper; nothing here is claimed open. As far as is known, no part of it has a machine-checked proof. A formalization adds:
The obvious argument fails at its first step. The greedy procedure's sample sizes depend on all past observations of all alternatives, so the PCS has no tractable expression, and the classical route through pairwise comparisons at fixed sample sizes does not apply. The boundary-crossing perspective sidesteps this, at three costs. First, (3.2) requires a careful pathwise argument: before the best alternative's running average reaches its minimum, it can lead, be sampled, and lose the lead, so "once best, always best" is false until . Second, Lemma 2 is a fluctuation-theory identity (Spitzer's formula for the mean ladder epoch of a Gaussian walk), not an elementary computation. Third, the limit combines a strong law over i.i.d. crossing times with a continuity argument in , which needs the continuity and strict monotonicity of .
tsum ( for ), an unbounded infimum read as , and a "for every with " statement that holds vacuously: the goal asserts the existence of .Sampling from a Gibbs distribution on , or computing integrals against it, is a basic task in Bayesian statistics and machine learning. A standard approach simulates an ergodic diffusion whose invariant distribution is , such as the overdamped Langevin diffusion , discretizes it with an Euler scheme of step , and averages along one long trajectory. Two errors compete: a bias of order , because the scheme's invariant distribution differs from , and a variance of order for a time horizon . With a single step, balancing them requires of the order of Euler iterations for an -approximation when the bias is of order (Egéa–Panloup, p. 3).
Multilevel Monte Carlo (Giles 2008, doi:10.1287/opre.1070.0496) removes this extra factor in finite-horizon problems by combining coarse and fine discretizations whose differences have small variance. Pagès and Panloup (arXiv:1609.00412) and Giles, Majka, Szpruch, Vollmer and Zygalakis (arXiv:1805.10974) adapted the idea to invariant distributions. Egéa and Panloup (arXiv:2109.07753, Math. Oper. Res. 2025) build a multilevel pathwise average, a combination of occupation measures of Euler schemes, and prove an -error of order at cost , or in a borderline case, under four abstract assumptions. This mission formalizes that general result (their Theorem 2.1 (ii)) and the bias and variance estimates behind it.
Let and be Lipschitz. For a step , a starting point and a -dimensional standard Brownian motion , the Euler scheme is and
Write and for the Lipschitz constant of .
Fix , a number of levels , steps , horizons , a warm start , and independent Brownian motions . The multilevel occupation measure is
Inside level both schemes use the same Brownian motion and are read at the coarse times. The cost is , the number of Euler iterations.
The assumptions involve , , , the invariant distributions of the diffusion and of the scheme, and . For every :
With , , , , , , , () or (), and :
with a universal constant. The cost constant is explicit; the error constant is left existential, which is how the paper states it.
With the same steps and horizons but , arbitrary and for a fixed , the same two bounds hold with an error constant that depends on the parameters but not on , or . It is a separate theorem item, not a milestone.
Lemma 3.1 (long-time bias of one average), Proposition 3.2 (bias of ), the variance decomposition (32), Lemma 3.2 (variance of one correcting level), Proposition 3.3 (variance of ), the cost bound (28), and Proposition 3.1, the non-asymptotic squared-error bound for given steps and horizons.
Theorem 2.1 separates the analysis of the multilevel estimator from the analysis of any particular diffusion. Once a diffusion satisfies –, the complexity follows with explicit parameters. The paper then checks the assumptions for Langevin diffusions with strongly convex potentials and obtains dimension-explicit costs and . Those are the companion missions II and III of this series; they rest on the same estimator and cost.
The paper's proofs are on paper only. No machine-checked proof of a multilevel ergodic estimator is known to us. This mission produces a statement-level formalization of the estimator, its cost, the four assumptions and the bias–variance bounds. A complete development would add discrete-time Markov-property arguments for Euler schemes driven by a Brownian motion, covariance bounds for ergodic averages, and the elementary but delicate parameter calculus of §4.
The bias step is close to routine once and are given. The variance of a correcting level is not. Bounding it by the second moment alone gives , which does not decay with . The proof must also use mixing: covariances between times and far apart are controlled by through the Markov property, which needs the conditional law of each scheme given its past and a moment bound on along the path . The two regimes are matched at a separation of order , and this is where the factor comes from. At the level of the theorem, the parameters (8) and the warm start must make three error terms simultaneously with a constant independent of , , the diffusion and every assumption constant. Getting the uniformity right is what the explicit thresholds , , are for.
EthierKurtz.SDEState d, and a Brownian motion is the published EthierKurtz.IsStandardBrownian. The levels' Brownian motions form one family B : ℕ → ℝ≥0 → Ω → ℝ^d, mutually independent as path-valued variables. is a continuous linear map .eLpNorm · 2 P and variances are evariance, both valued in , so an infinite moment is never read as . Expectations that are concluded come with an integrability conjunct.Contributions are welcome on any milestone, on Markov-property and moment lemmas for Euler schemes driven by IsStandardBrownian, and on the Theorem 2.1 (i) companion with non-explicit constants.
Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand; a price below it is perceived as a gain and stimulates it. Because today's prices shape tomorrow's reference prices, a seller facing reference effects solves a dynamic problem even when demand is otherwise stationary. The single-product theory is classical: Popescu and Wu (2007) showed, for a broad class of demand models, that loss-averse consumers make optimal and myopic price paths converge monotonically, and Hu, Chen and Hu (2016) studied the cyclic behaviour that gain-seeking consumers can induce under linear demand.
Retailers sell many substitutable products, and the standard model of substitution is the multinomial logit (MNL). Guo, Jiang and Shen (2025) combine the two: each product has its own reference price and its own asymmetric sensitivities to gains and losses, and consumers choose among the products by MNL. This mission formalizes the paper's first set of results, on the myopic pricing policy, which maximises the current period's revenue at the current reference prices and ignores the effect on the future. Myopic pricing is both a widely used heuristic and the benchmark against which the optimal policy is measured later in the paper.
There are products . Product has an intrinsic utility , a price sensitivity , and reference sensitivities (to gains) and (to losses). At price vector and reference price vector the deterministic utility of product is
the market share of product is , and the single-period revenue is . Product is loss-averse if , loss-neutral if , and gain-seeking if ; the three sets are .
Prices and reference prices lie in the box with ceiling . A myopic policy assigns to each a maximiser of over ; the maximum value is the optimal single-period revenue . Reference prices follow exponential smoothing with memory :
and is the myopic price path. A policy has a steady state if for some .
The paper assumes throughout that , where is the unique root of the scalar equation (9), with . This ceiling assumption makes the ceiling non-binding for the myopic problem.
For every myopic policy and every :
Theorem 3 separates two regimes by consumer type alone. With loss-averse and loss-neutral consumers a seller who reprices myopically settles at a stable price vector; with even one gain-seeking product no price vector is self-reproducing, and myopic prices keep oscillating. Theorems 1 and 2 are the structural results behind this: they reduce a non-concave, non-smooth -dimensional optimisation to one scalar equation with a monotone right-hand side, which is also how the myopic policy is computed in practice. The same structure is used later in the paper to bound the gap between myopic and optimal revenue.
All results are proved in the paper; the proofs are in its online supplement (Appendices B.1–B.5), which is not part of the source file used here. None of the results is formalized. The work in this mission is the first machine-checked treatment of MNL pricing with reference effects: global optimality of a candidate maximiser for a non-concave revenue, the analysis of a scalar root equation with piecewise definitions, and the dynamics of a map that is continuous without gain-seeking products and discontinuous with them.
The obvious route to Theorem 2, setting the gradient of to zero, fails twice. The revenue has kinks at , so a maximiser may sit at a kink where no gradient exists; this is the middle branch for loss-averse products. And the revenue is not concave in prices: for a gain-seeking product the first-order conditions have several solutions, and a global maximiser must be singled out among them. The usual reformulation of MNL pricing in market-share variables, which restores concavity without reference effects, does not survive the kinks.
For Theorem 3 the difficulty is dynamic. Without gain-seeking products the myopic map is continuous, but the flat middle branch of (14) makes it non-contracting, so the standard contraction arguments do not apply, and the limit depends on the starting point. With a gain-seeking product the map jumps at the threshold , so continuity-based arguments about the limit of the path are unavailable.
Products are indexed by Fin n (0-based); vectors are Fin n → ℝ with the product topology and the coordinatewise order. The standing hypotheses , , , and the ceiling assumption (as "some root of (9) is at most ") appear as hypotheses of every theorem that needs them; Corollary 1 needs only , . The market shares (3) are defined directly, without the Gumbel derivation. is an indexed supremum over Fin n (zero when ). The three sums of (13) are written as one sum whose term is chosen by product type.
Maximisers need not be unique, so a myopic policy is any selection of maximisers, and every statement holds for all selections; is the revenue of an arbitrary maximiser. "The unique solution" is split into "is a solution" and "every solution equals it". The following deviations are disclosed in the items: at the threshold of (16) both prices are maximisers, so only "one of the two" is claimed there; the fixed-point property of the limit in Theorem 3, and every limit claim of Corollary 2, require , since at the price path is the constant ; the non-convergence clause in Theorem 3.2 is an addition to the literal "no steady state". "Monotone decreasing" (Corollary 1) and "monotone increasing" (Corollary 2, §3.1) are read non-strictly.
A trivializing formalization is ruled out: Theorem 3.2 quantifies over every reference price in the box and every myopic selection, Theorem 3.1 asserts convergence from every initial reference price rather than the existence of some fixed point, and Theorems 1–3 keep the ceiling assumption, without which the maximiser can sit on the boundary and (14)–(16) fail.
A complete development needs: continuity and compactness facts for the MNL revenue on a box; optimality conditions for the kinked, non-concave revenue; one-variable analysis of the piecewise-exponential right-hand side of (13); and convergence results for monotone or continuous recursions in . The MNL and reference-price infrastructure is reusable by the five other missions of this series. Contributions to any milestone, and alternative proofs, are welcome.
Online platforms run controlled experiments in which subjects (users, sessions, sellers) arrive one at a time and must be assigned to control or treatment on arrival, before later subjects are seen. A good design makes the two groups look alike in their observed covariates, because covariate imbalance inflates the variance of treatment-effect estimates. Classical offline remedies such as matched-pair designs need all covariates in advance, and the simplest online design, complete randomization, ignores covariates altogether.
Zhao and Zhou (arXiv:2201.12936, Management Science 2025) measure imbalance by the cost of the best one-to-one matching between the treated and the control subjects, which links sequential experimental design to online matching. They propose the pigeonhole design: partition the covariate space into cells and, inside each cell, assign each arrival to the group that is currently short there. This mission formalizes their main upper bound for one continuous covariate.
A horizon , assumed even, of subjects arrives sequentially. Subject carries a covariate , and the whole sequence is fixed in advance by an adversary who does not see the randomization (an oblivious adversary). Each subject is assigned, at arrival and irrevocably, to the control group or the treated group , and in the end .
The discrepancy of a split is the cost of a minimum-weight perfect matching between the two groups (display (1) of the paper):
The completely randomized design chooses uniformly among the subsets of size ; its expected discrepancy is written .
A pigeonhole design takes a partition of into cells. When subject arrives: (1) if one group already holds subjects, joins the other; (2) otherwise, if the cell of currently holds fewer control than treated subjects, joins control, if fewer treated, joins treatment, and on a tie a fair coin decides. Its expected discrepancy is the average of over the coins.
The uniform pigeonholes with parameter are the cells .
For every fixed there are and such that, for every even and every , the pigeonhole design with uniform pigeonholes satisfies
The constant may depend on but on nothing else. Corollary 1, the case giving , is included as a separate statement.
In attack order:
Lemma 3 shows that a simple, time-invariant, covariate-aware online rule beats complete randomization by a polynomial factor: with the expected discrepancy is , against for complete randomization (Lemma 2). A companion result of the paper (Lemma 4) shows that no pigeonhole design does better than , so the bound is tight up to the logarithm. The same two-component argument underlies the paper's multi-dimensional result.
The paper proves these statements in an e-companion; none is machine-checked. A formalization adds the following. It fixes the exact model behind each expectation, namely an average over coin vectors with the balancing rule included. It repairs the places where the printed argument does not close as written. The printed constant of Lemma EC.4 is wrong, and the stated value here is the corrected one. Lemma EC.7 is false as printed in its strict form and trivial in its weak form, and the stated version is the one the proof actually establishes. The printed proof of Lemma 2 passes through a lemma (EC.6) that is false. Component 2 relies on a conditional binomial law that does not hold literally. A complete development would certify Lemma 3 independently of these slips.
The natural first idea is to bound each cell separately and add the results. This handles subjects that are paired inside their own cell, but it leaves out the balancing rule. Once one group is full, every later subject is forced into the other group regardless of its covariate. These forced subjects can be far from everything they are matched to. The number of forced subjects, , equals the imbalance among the cells' leftover subjects, which is random and read at a random time. Bounding its expectation requires a concentration argument that is uniform over time.
A second difficulty is the per-cell bound itself. Inside one cell the design pairs consecutive arrivals with random orientation, but the number of pairs in a cell is random and depends on the stopping time. A bound of the form for a cell of length holding subjects must therefore survive a coin-dependent truncation. Finally, the discrepancy is a minimum over matchings, so every upper bound must exhibit a matching, and every comparison between instances (Lemma EC.7) is an exchange argument over all coin outcomes.
All statements live in the namespace PigeonholeDesign.Upper, and the conventions are fixed as follows:
Fin T, from , so the paper's subject is index , and its odd index is an even 0-based position. An assignment is Fin T → Bool, with true meaning treated.Several formalizations would make the statements easy for the wrong reason, and the statements rule them out. The junk value of an unbalanced split never applies, because the designs are balanced. A bound on a single run, or on the best run, in place of the average over all coin vectors is not the claim. Constants may not depend on or . The partition is fixed, and the statements do not range over arbitrary partitions.
A complete development needs:
The design definitions and the balance lemma are reusable by the paper's lower-bound and multi-dimensional missions. Contributions of any milestone, of alternative proofs that bypass the faulty printed steps, and of sharper constants are welcome.