Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A seller with one item faces buyers whose valuations she does not know, not even in distribution. Prior-independent mechanism design asks which selling mechanism performs well against every distribution in a given class, rather than against one known prior. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) measure performance by regret: the expected gap between the highest valuation, which a seller who knew the valuations could extract, and the revenue actually collected. They solve the resulting minimax problem for several classes of joint distributions: i.i.d., exchangeable and affiliated, mixtures of i.i.d., exchangeable, and arbitrary.
This mission formalizes the last two cases. The answer is that the minimax regret against exchangeable or arbitrary joint valuations is for every number of buyers , so competition among buyers does not help the seller unless Nature's power is restricted.
Timeline. Bergemann and Schlag (2008) solved the one-buyer regret problem: the optimal mechanism is a randomized posted price and the minimax regret is . Koçyiğit, Kuhn and Rujeerapaiboon (2020; doi:10.1287/ijoc.2022.0275) showed, for several bidders and several items, that with arbitrary joint distributions the minimax regret problem reduces to the one-bidder case, so the value does not improve with . Anunrojwong, Balseiro and Besbes (2022–2024, Proposition 4) recover this within their framework, show that the worst case can be taken exchangeable, and identify the optimal mechanism as a second-price auction with a random reserve.
There are buyers with valuations in the type cube . A mechanism maps reported valuations to allocation probabilities and payments . The class of DSIC mechanisms consists of those satisfying, on : individual rationality (IR) ; dominant-strategy incentive compatibility (IC), truthful reporting is optimal for each buyer whatever the others report; and the allocation constraint (AC) .
Write and for the highest and second-highest valuation. The regret of against a joint law on is
and the minimax regret over a class is . Here is the class of all distributions on , and the exchangeable ones, invariant under every permutation of the buyers.
A second-price auction with random reserve draws a reserve , gives the item to a highest bidder if her bid is at least , and charges her . Proposition 4 uses the reserve CDF on ( below ), and the isorevenue law on , with CDF on and an atom of mass at . Nature's candidate picks a buyer uniformly at random, gives her an isorevenue value and gives everyone else value .
With and , for every and ,
is exchangeable, and
The result. Proposition 4 gives the exact minimax regret and an explicit saddle point for the two largest distribution classes of the paper. The value is independent of , in contrast with the i.i.d. class, where the minimax regret decreases in (Theorem 1 of the same paper). Together with the other propositions it shows precisely how much structure Nature must be denied before additional buyers reduce the seller's regret. The worst case being exchangeable shows that symmetry alone does not help.
Formalizing it. The result is proved on paper; it is not formalized anywhere to our knowledge. A formalization produces machine-checked versions of: dominant-strategy incentive compatibility of the second-price auction with random reserve; the pointwise regret identity for that auction; a revenue identity for arbitrary DSIC mechanisms under a mixture of one-buyer laws, which rests on Myerson's payment characterization; and a minimax value computed over all DSIC mechanisms and all distributions. Each of these is reusable by the sister missions on i.i.d., affiliated and fixed-reserve settings.
The minimax problem ranges over all DSIC mechanisms, an infinite-dimensional and unstructured class, and over all joint distributions. The upper bound needs only one mechanism, but the lower bound must hold against every DSIC mechanism, including randomized ones whose allocation is not of auction form; the step from incentive compatibility to an explicit revenue formula along the line is where the work lies. Myerson's payment characterization is quoted by the paper without proof and must be established here for mechanisms that are incentive compatible only on . A second obstacle is measure-theoretic: the regret is an integral of an arbitrary mechanism's payments against an arbitrary law, so its finiteness and the interchange of expectation with the reserve randomization must be justified. The tempting shortcut of restricting Nature to i.i.d. laws gives a different, smaller value.
Lean represents valuations as Fin n → ℝ and laws as measures on that space; is the set of probability measures giving the complement of measure zero, and those also invariant under for every permutation . (IR), (IC), (AC) are imposed on , with misreports in . Two hypotheses are added to the class and disclosed in every statement: allocation and payment functions are measurable, and payments are bounded on , so that the regret is a genuine expectation. Ties for the highest bid are broken towards the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule). is when . The minimax regret is a real infimum of real suprema; for DSIC mechanisms the regrets lie in a bounded interval and both index sets are nonempty, so these are not junk values. The reserve law and the isorevenue law are given through their CDFs, and as the push-forward of the isorevenue law under ; is not a product measure. The page prints ; the formalization uses .
Trivializing formalizations are ruled out: carries the support condition (without it the regret is unbounded), the regret at is that of the stated reserve law , and both classes are nonempty.
A complete development needs: Lebesgue–Stieltjes integration by parts for CDFs, Myerson's envelope characterization of DSIC payments, push-forwards and mixtures of measures on , and conditionally complete lattice reasoning for the minimax value. The DSIC property of and the payment characterization are reusable throughout auction theory. Proofs of any milestone, and lemmas towards Myerson's characterization, are welcome.
Data-protection laws such as the European Union's General Data Protection Regulation (GDPR) shift control over personal data from firms to consumers: data may be collected and used only with the consumer's consent and only for the purposes she allows. The usual expectation is that such a rule helps consumers and costs firms. Xu, Wang and Zhang (Management Science, forthcoming) examine this expectation in an online retail market where consumer data has two uses. Upside utilization (saved carts, location sharing, recommendations) lowers the consumer's shopping inconvenience. Downside exploitation (monetizing the data) earns the retailer money at the consumer's expense.
For a single retailer the paper finds that the GDPR raises the firm's profit and social welfare (Theorem 1). This mission formalizes the second main result, Theorem 2: once the retailer buys from an upstream supplier, the GDPR can make consumers, the retailer and the supplier all strictly worse off at once. Supply chains are the common structure of online retail, so this matters for anyone assessing a privacy rule by its effect on a single firm.
A unit mass of consumers values one product at . Shopping without the website's data-driven functions costs a consumer an inconvenience , uniform on . The data quality is . A consumer who buys at retail price and hides her data gets ; one who buys and discloses gets
where is the retailer's monetization intensity. Monetizing at intensity costs the retailer () and earns per disclosed record, so her data profit is when consumers disclose. A consumer buys iff her best buying utility is non-negative. The demand is the measure of buyers, and the consumer surplus is , where is the consumer's best buying utility.
The game has four stages. The retailer decides whether to collect data (). The supplier, whose production cost is zero, sets a wholesale price . The retailer sets . Then consumers buy and disclose or hide. The retailer earns and the supplier . Two data policies are compared:
Without collection both modes give the hiding utility . The paper's constants are
Outcomes are those of a subgame-perfect equilibrium (SPE): an REE at every , a retailer price that is a best response at every , a supplier price that is a best response after each , and a profit-maximizing .
With , , , and , SPE exist under both policies, and for every pair of SPE the GDPR's effect on (consumer surplus, retailer profit, supplier profit) is:
Every sign is strict.
Lemma 1 (the hide / disclose / no-buy partition of the market), display (5) (the retailer's pricing reaction ), Propositions 3 and 4 (the equilibria of the two modes), Corollary EC.1 (who collects data under which policy), and Propositions EC.11, EC.12, EC.13 (one column of the theorem each: consumer surplus, retailer profit, supplier profit).
The result. Theorem 2 is a counterexample to the view that consumer data protection is a transfer from firms to consumers. In the triple-lose interval the GDPR makes the retailer stop collecting data. That removes the inconvenience reduction consumers valued and shrinks the market, so the supplier loses too. Corollary EC.1 shows that the GDPR shrinks the range of valuations in which data is collected at all. The comparison with the single-firm case (Theorem 1) isolates the supplier's wholesale pricing as the source of the harm.
Formalizing it. The paper's arguments are algebraic and piecewise: an REE fixed point with a kink at full market coverage, global maximization of piecewise-quadratic profits, a nested maximization for the supplier, and comparisons of thresholds involving square roots. Several printed statements hold only on part of their stated range. Display (5) fails when the market saturates. The "otherwise" clauses of Propositions EC.11 and EC.13 fail at the points where the retailer is indifferent about collecting. Several proof displays carry typos. A machine-checked development pins the exact ranges and gives a reusable, fully specified model of consumer-data policies in a vertical chain. No machine-checked proof of these results is known.
The obvious argument plugs the printed closed forms into each other and compares them. That argument does not reach the theorem as stated. The theorem is about every subgame-perfect equilibrium of the game, defined from the utilities, not about the closed forms. So the work is to show that the equilibrium is pinned down at every node, including off the path. The REE must be shown unique at every price. The retailer's best response must be derived globally over , including the saturated branch, where demand equals 1 and the printed formula (5) is wrong. The supplier's profit must be maximized across the kink. After that, the five sign patterns rest on a chain of strict inequalities among and among the equilibrium profits, which must hold for all and .
All statements live in the namespace RetailPrivacy.SupplyChain and use one definition file, RetailPrivacy.SupplyChain.Model. That file holds the policy (Policy.R, Policy.C), the constants , the hide and disclose utilities, demand and disclosing quantity as Lebesgue measures of sets of , consumer surplus as an interval integral, the REE predicate, strategy profiles with actions at every node, and the SPE predicate. Collection is a Bool. Prices range over all of and the intensity over . The standing assumptions are , and the added : the paper leaves implicit, and at nothing is sold and every strict claim fails. The consumer-stage definitions are textually identical, up to the namespace, to those of the single-firm mission of this series.
Departures from the print, each disclosed in the item: display (5) is stated on its valid range; Propositions 3(iii) and 4(iii) are stated as comparisons of the retailer's subgame profits; Corollary EC.1 is stated with strict inequalities; and the "otherwise" clauses of EC.11 and EC.13 are stated without the indifference points.
Four formalizations would trivialize the goal, and none is acceptable: comparing the printed closed forms instead of equilibrium outcomes; an "every equilibrium" claim that might be vacuous (the goal asserts existence); profiles that omit off-path actions, which would make the supplier's or the retailer's optimality checks vacuous; and price domains restricted to or to unsaturated markets.
The paper's proofs are in its e-companion, Appendix C (pp. ec21–ec38). Useful contributions include the consumer-stage lemmas (REE uniqueness and its closed form), the global best-response computations, and the threshold inequalities, each a self-contained lemma.
Social-media influencers earn money by endorsing products to their followers. An endorsement of a product that does not fit the audience brings in money today but costs followers, and followers are also what spreads awareness of the influencer to new people. Nistor, Selove and Villas-Boas (Influencer Authenticity: To Grow or to Monetize, Management Science, 2024) model this trade-off as a deterministic, infinite-horizon, discounted optimal-control problem with a single binary control. In their base model (§3) the optimal policy is to grow first and monetize later: authentic while awareness is small, permanently inauthentic once awareness passes a threshold.
Section 4.2 of the paper asks how this changes when the audience is not permanent: users join and leave the platform, or the influencer covers a topic that interests people only for a while. With follower turnover the influencer never reaches full awareness, and Proposition 3 says that if turnover is fast enough she never monetizes at all. The model gives a testable prediction: influencers on platforms with rapid user turnover, or in product categories with short-lived interest, should stay authentic.
Time is . There is a unit mass of potential followers, and is the share of them who are aware of the influencer, starting from . At each time she is either authentic or inauthentic. Following Table 1 of the paper:
with and . These are the reduced-form parameters of §3.1: a fraction of aware people follow an inauthentic influencer, who earns per follower, and authentic profit per follower is normalized to . The paper assumes "for the remainder of the paper", so that being inauthentic pays more today.
Potential followers leave and are replaced at a turnover rate , and awareness follows equation (6):
where is the word-of-mouth rate. Under the always-authentic policy this is the logistic equation , with steady state . The influencer maximizes the discounted profit (2), , with discount rate .
In the Lean development (namespace InfluencerAuth.Turnover) a policy is a measurable set of the times at which she is inauthentic, so is "always authentic". IsPath β γ x A₀ S A says is an admissible awareness path, discountedProfit γ φ r S A is (2) at time , and IsOptimalFrom β γ φ r x A₀ S A says that earns at least as much as every measurable policy with any admissible path from the same . authValue β x r is the closed form of Lemma 5, and Condition2 γ φ β r x is
Under the standing assumptions , , , , , with and Condition 2,
The range of is the paper's set of "all feasible levels of awareness". The statement fixes no constant beyond those of Condition 2.
For and every admissible always-authentic path from ,
Proposition 3 is the paper's result on when the grow-then-monetize pattern of the base model breaks down. Without turnover the influencer always monetizes once she is large enough (Proposition 1, §3). With turnover there is a whole parameter region, given by Condition 2, where monetizing is never optimal. The condition compares the extra current profit from being inauthentic, , with the awareness lost by being inauthentic, , valued at the marginal value of awareness at the steady state, from (7).
The proofs are in an online appendix that is not part of the published article, and this result has no machine-checked proof. The mission provides a precise statement of the control problem: optimality over every measurable switching pattern, with the dynamics in integral form. It also gives the closed-form always-authentic value and its derivative as separate targets. A complete development would be one of the first formal optimality proofs for an infinite-horizon, discounted, continuous-time deterministic control problem.
Optimality is claimed against every measurable policy, not only against constant or threshold policies. The natural argument is a verification theorem: show that satisfies the Hamilton–Jacobi–Bellman inequality on the feasible range, then integrate along an arbitrary competitor path. Condition 2 is stated only at the steady state , where (7) gives the marginal value of awareness. At a lower awareness level the inequality comparing the two actions involves at that level, so it does not follow from Condition 2 alone; it needs control of on the whole interval. A competitor path may also switch infinitely often, so its awareness is only absolutely continuous, and the comparison must work almost everywhere. Above the steady state the always-authentic policy is in general not optimal, so any argument must use the restriction .
Set ℝ. An admissible path is continuous on , starts at , stays in , and satisfies for , with on and off . This is the Carathéodory form of (6). A derivative everywhere is not required, because that would exclude every switching policy. The clause follows from the equation and is stated to make integrability explicit.discountedProfit is with on and off ; the paper's value from time is the same object after the shift . No optimal value is defined as a real supremum; optimality is a comparison with every competitor.Fake follower accounts are sold openly to social media influencers, who buy them because advertisers and new followers read a large follower count as a sign of quality. Platforms respond with antifake effort: detection, removal and registration hurdles that make fake accounts more expensive to operate, but that also impose a nuisance cost on legitimate users (more CAPTCHAs, more false flags). Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game and ask how fake-account purchases respond to the platform's effort and to contextual factors such as social media literacy and antifake technology.
A finding of the paper that runs against intuition concerns the high-quality influencer. In a costly separating equilibrium the high type buys fake accounts defensively, so that a low-quality influencer cannot afford to mimic its follower count. This contrasts with Chen and Papanastasiou (2021), where only the low type manipulates. Proposition 3 of the paper describes how this defensive purchase moves with every parameter, and in particular that raising the antifake effort can increase it. This mission formalizes Proposition 3 and the steps the paper uses to explain it.
An influencer is of high type or low type , with content qualities . A unit mass of consumers has valuation and follows when . A fraction of consumers, the social media literacy, know the type; the rest infer it from the early follower count, which the influencer can inflate with fake accounts. Advertising yields revenue per real follower, of which the influencer keeps a share .
The platform chooses an antifake effort . With antifake technology level , base price , opportunity cost and nuisance coefficient , the unit price of fake accounts and the cost of following are
A type of quality has informed followers, and, when its type is revealed, uninformed ones. With and , Lemma 2 of the paper gives the costly separating equilibrium for , in which the H-type's early-follower count is
and its defensive purchase is . In the pooling equilibrium the low type's offensive purchase is . In Lean the parameters are fields mu lamI lamP rho l qH qL c0 c1 tau p0 gamma of a structure Params, and the quantities above are price, cost, nIn, nUnSep, eta2, d2, nCsep2, xCsepH, xPoolL.
Assume , and Assumption 3 (). Let (22) be the condition
If (22) holds, is strictly decreasing on . Otherwise there is with strictly increasing on and strictly decreasing on .
A companion theorem, not a milestone, states Proposition 2(a)–(b) for the offensive purchase .
Proposition 3(c) says that the platform's main instrument against fake accounts can backfire: below a threshold on the technology level, a moderate increase in antifake effort makes high-quality influencers buy more fake accounts, because the higher nuisance cost widens the follower gap the low type would have to close. Proposition 3(a) identifies the levers that reduce defensive purchases unambiguously: literacy, the base price, and antifake technology. Together with Proposition 2, these results underlie the paper's policy discussion of when an antifake campaign reduces the number of fake accounts at all.
The results are proved in the paper's Online Appendix; none of them is machine-checked. The formalization makes every hypothesis explicit: positivity of and , the exact domain on which each monotonicity claim is strict, and the reading of the informal remark "", which is false as and true at the edge of the costly separating range. It also yields a reusable closed form for the equilibrium purchase that other statements about this model can cite.
The closed form and the derivative are algebra and calculus over rational functions of , with care about . The content is the dichotomy in (c). On the two marginal effects have opposite signs, , and both depend on through and through . The paper's informal argument (", so dominates eventually") settles only the right end of the range. What the goal requires is the sign of on the whole interval: that it changes sign at most once, that (22) is exactly the condition for it to be nonpositive at , and that in the other case the change of sign happens strictly inside . Strictness of the parameter comparative statics also fails at the edges ( for , for ), so each domain has to be chosen exactly.
All quantities are real-valued closed forms; no probability spaces are introduced, since the paper's expectations over are already the closed forms (8)–(9). The parameter bundle carries the standing ranges of §3 and Table 1: , , , , , , , , . The readings of the paper fixed by the formalization are:
is defined as through (17), not by the right side of (20); a definition by (20) would make the closed-form milestone trivial. The goal must be proved about this function on , not about a sign condition on an abstract derivative. The proofs are in the paper's Online Appendix, which is not used here; every milestone is a statement or display of the main text. Contributions of proofs of any milestone are welcome, as are lemmas on single-crossing of the derivative.
In many sequential decision problems, playing one action reveals the outcome of other actions too. A bidder in a first-price auction who bids and sees the winning price learns whether every bid at or above that price would have won. A recommender that shows one item learns something about related items. Two kinds of side information recur. Graph feedback across actions: playing action also reveals the rewards of the out-neighbours of in a directed graph (Mannor and Shamir 2011; Alon, Cesa-Bianchi, Dekel and Koren 2015). Cross learning across contexts: the reward of the chosen action is revealed under every context, not only the current one (Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider 2019).
Han, Zhou and Weissman (arXiv:2003.09795v7) reduce learning to bid in repeated first-price auctions to a contextual bandit with both structures. Their §3 starts from a simple arm-elimination algorithm that exploits graph feedback (Algorithm 1) and extends it to contexts with cross learning (Algorithm 2). This mission formalizes that layer: the algorithms, their concentration lemma, and their high-probability regret bounds (Theorems 3 and 4).
Timeline:
A stochastic contextual bandit with graph feedback and cross learning (Definition 2) has a horizon , contexts , actions , a joint reward law supported on with mean rewards , and a directed graph without self-loops. In round a context is revealed, the learner picks , nature draws iid from , and the learner observes for every and every . The regret (5) is
Definition 1 is the case , with regret (4). The independence number of is the largest size of a set of actions with no edge between any two of them.
Algorithm 2 keeps for each context an active set and a minimum count , and for each action a count shared by all contexts. In each round it plays an action of , either of largest out-degree in the graph restricted to (Option I) or of in-degree zero there (Option II, for DAGs). When every active action of context has been observed more than times, the active set drops the actions whose empirical reward falls below the best by more than . Algorithm 1 is the case .
With probability at least , writing ,
for every context sequence and every tie-breaking rule.
Theorem 4 shows that one algorithm attains, up to logarithmic factors, the better of two regret rates: , available from cross learning alone, and , available from graph feedback alone. The paper then shows (Theorem 6) that with adversarial contexts nothing better than is possible, while with stochastic contexts and a partial order a variant reaches for first-price auctions. Algorithm 2 is the building block of that variant.
The results are proved in the paper; none is formalized. A formal development produces machine-checked versions of a concentration inequality with a random number of observations, of a domination bound for directed graphs, and of an elimination analysis with shared counts across contexts. Four printed statements need correction, and the formal statements record the corrected forms: the constant in Theorem 4's second bound (the printed proof gives ); Lemma 10, which is false for and for edgeless graphs as worded; Lemma 1, which fails for and close to (excluded by ); and the pseudocode of Algorithms 1–2, whose update can leave empty after an elimination (the formalization keeps the text's invariant , and coincides with the printed algorithm wherever the latter is defined).
The observations of an action are not a fixed sample: how often and when action is revealed depends on earlier rewards through the algorithm's choices. A union bound with Hoeffding's inequality at a fixed sample size does not apply directly, and Lemma 1 needs a self-normalized martingale inequality.
For Option I, the obvious bound on how long it takes to observe every least-pulled action once more is rounds, which gives only . Getting instead of requires that a vertex of largest out-degree covers a fraction of the remaining vertices; this is the content of Lemma 10, a probabilistic-method bound that is not in Mathlib. For contexts, the per-context analyses must be combined while counts are shared, and the bound in needs a per-action rather than a per-context accounting.
Fin K, contexts Fin M, rounds Fin T; paper round is Lean index . The feedback graph is a relation E with no self-loops; "independence number " is the hypothesis that every independent set has at most elements (all bounds increase in ).Fin M → Fin K → ℝ carried by ; rewards are iid across rounds (Measure.pi). The regret is the pseudo-regret with means .Welcome contributions: the self-normalized inequality of de la Peña, Klass and Lai (Lemma 11), Lemma 10, invariants of Algorithm 2 (the active sets stay nonempty and contain an optimal action on the good event), and the deterministic regret accounting given the concentration event.
Large online retailers such as Amazon sell their own products and, on the same storefront, host third-party sellers who pay a commission on their sales. The owner of such a retailer-led marketplace sets the commission, competes with the sellers it hosts, and can direct inattentive consumers to the offer of its choice. How these levers interact is a central question in the economics of digital platforms and in the current policy debate on platform fees and self-preferencing.
Hervas-Drane and Shelegia (2025) build a model of a monopoly retailer with a marketplace and an assortment capacity constraint, and derive the platform's entry pattern, its fee and the effect of policy interventions. A basic question about the fee is whether a retailer that can sell products itself would ever choose to run its marketplace for free, collecting nothing from the sellers it hosts. This mission formalizes the paper's answer, Lemma 2: it never does.
There is a unit mass of products, indexed by their consumer valuation . Valuations are distributed according to a probability measure (the CDF of the paper) on , where is the marginal cost every firm incurs per unit. Each product is an independent market with a unit mass of consumers who each buy one unit at any price .
The monopolist owns the storefront. For each product there is one third-party seller who can sell only through the marketplace. The game has three stages.
The pricing stage (Proposition 1 of the paper) gives per-market payoffs. If sells alone (SBM) he earns . If sells alone (SBT) she charges and collects . If both sell (SBMT), charges
and earns . Seller enters exactly the marketplace products (Lemma 1). Given an allocation , 's profit is
and his profit as a function of the fee is the value of his allocation problem,
The paper maintains Assumption 1, : the monopolist steers over half of the consumers.
For every with for all ,
The statement is about every maximising fee. It does not assert that a maximiser exists, which the paper does not claim in Lemma 2.
The map has a right derivative at , and it is strictly positive:
Lemma 2 is the first result of the paper's fee analysis. It says that the fee is an active instrument in every configuration of capacity and steering: even a monopolist who can sell every product himself extracts revenue from the sellers he hosts, because at a zero fee the first-order effect of raising it is positive. The paper's subsequent characterisation of the optimal fee (Proposition 3) and its policy results on fee caps and on banning the retailer from its own marketplace (Propositions 4–6) all take place in the region that this lemma secures.
The paper proves Lemma 2 in two sentences, by "inspection of ". None of the results is formalized elsewhere. The formal development has to make the inspection precise: is the value of an infinite-dimensional allocation problem whose optimal allocation changes with , so its one-sided differentiability at is an envelope-type statement rather than a calculus exercise. The model layer (the marketplace set, the Proposition 1 payoffs, the allocation problem and its value) is shared, in identical form, with the two companion missions of this series.
is a supremum over measurable sets, not a closed-form function of , so its derivative cannot be read off a formula. Two effects change as grows from zero: fee revenue rises on every marketplace product, while the products with leave the marketplace and their sellers stop paying fees. At these products pay no fee, so their loss is of second order. Making this precise requires control of the optimal allocation uniformly near and of the mass of the exiting products, using only that has a density.
The naive argument "keep the allocation optimal at and raise the fee slightly" shows that some positive fee beats , but it does not compute the derivative. The claim also fails in one corner: with and the SBMT payoff equals the SBM payoff, the monopolist supplies every product at every fee, and does not depend on .
The Lean development lives in the namespace RetailerMarketplace.PositiveFee. Valuations are a measure μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0 (support in ) and μ ≪ volume (the density ). Allocations are arbitrary measurable sets of mass at most , never intervals. is defined as the supremum of profitM over them (PiM); by the paper's Proposition 2 it coincides with the closed form (4), which this mission cannot use because its thresholds are the conclusion of Proposition 2. The marketplace set is {v | c ≤ v * (1 - f)}, correct also at , where it is empty.
Standing and added hypotheses, all disclosed in the item statements:
No full-support hypothesis and no existence of an optimal fee are assumed.
Trivializing formalizations are ruled out: the supremum is over a nonempty family that is bounded above under integrability, so PiM is not a junk sSup; and the goal quantifies over every maximiser rather than asserting that some positive fee beats .
A complete development needs set integrals over , a bathtub-type comparison of allocations, and one-sided derivatives of a value function. The value-function and allocation lemmas are reusable for the companion missions on entry modes and on per-unit fees. Contributions of intermediate lemmas, such as attainment of by a top- allocation, are welcome.
The Lightning Network (LN) is a second-layer payment system for Bitcoin. Instead of recording every payment on the blockchain, two parties lock funds in a payment channel and settle many payments off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it carries. Which channel topology supports a given pattern of payments at least total cost is therefore an economic design question for the network's participants.
Guasoni, Huberman and Shikhelman (SSRN 4439190, 2023; published in Management Science, 2024) study this question for a general cost function, assuming only a few qualitative properties derived in their earlier work on channel economics ([GHS22], Lightning Network Economics: Channels). This mission covers §3.1 of the paper, local channel reconfiguration: a relaying node can be bypassed at lower cost, odd cycles are never optimal, and a cost-minimizing network is bipartite with every net flow going from one side to the other. Three companion missions (II–IV of this series) cover hermetization by a routing hub (§3.2) and bounds on the global minimal cost (§3.3).
Let be a finite set of nodes. A payment flow is a vector of net flows with . A Lightning Network on is an anti-symmetric real matrix , , where is the net flow from to in the channel between them and means there is no channel. The network supports if
A channel cost function is with
The cost of a network is , the sum of over its channels. A network is cost-minimizing for if it supports and no Lightning Network on the same node set that supports has smaller cost.
The paper's channel notation: is a channel with net flow from to , and is a channel in which sends and sends , so the net flow from to is .
If is cost-minimizing for , there is a set with such that the channel graph ( iff ) is bipartite with parts , and
The statement is conditional and does not assert that a minimizer exists.
Corollary 3.3 says that in an optimal Lightning Network every node is a pure sender or a pure receiver, and that no node relays payments. This sits in tension with the observed LN, which is organized around large routing hubs; the paper reconciles the two in §3.2 by allowing new nodes. Corollary 3.11 shows that the star, the intuitive candidate for a cheapest topology, is optimal only with a single net payer or a single net payee.
The results are proved in the paper, with short arguments in its Appendix A, and they have no machine-checked proof. This mission adds a precise version of the model, in which the meaning of "cost-minimizing", the sign conventions and the corrected cost axioms are fixed, and a formal proof of the chain Theorem 3.1 → odd cycles → bipartite structure for an arbitrary cost function satisfying the axioms.
Theorem 3.1 on its own is a two-line computation. The difficulty is in applying it inside an arbitrary network. When and already share a channel, adding or to it requires for reals of either sign. That inequality is not among the axioms and has to be derived from them. The odd-cycle step needs a pigeonhole argument on channel orientations around a cycle. The bipartite step needs either König's characterization of bipartite graphs or a direct construction of the parts from the flow directions. The naive formalization that re-states Theorem 3.1 only for a network with exactly two channels does not reach the corollaries.
V, not . The matrix is Λ : V → V → ℝ, because λ is a Lean keyword.Supports, which is independent of the sign.Fin k → V, odd, with cyclic successor finRotate k. A channel is a nonzero entry in either direction.SimpleGraph.IsBipartiteWith A Aᶜ on the channel graph, with the flow-direction clause stated separately as the stronger content.Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (no or linear cost); cost-minimization ranges over all networks on , not over a fixed edge set; is not fixed to three nodes; the in-and-out claim is stated for arbitrary networks; and and are complementary, so they cannot overlap.
König's theorem is in Mathlib (SimpleGraph.two_colorable_iff_forall_loop_even) and proved on the platform (FamousTheorems.two_colorable_iff_no_odd_cycle_6b), so it is not posed here. The derived two-sided subadditivity of , and a lemma rerouting a relayed flow inside an arbitrary network, are reusable in the other missions of the series. Contributions of such auxiliary lemmas are welcome.
Industries in which capacity can be built but not sold back (energy generation, manufacturing, mining) are studied through irreversible investment models: a firm controls a nondecreasing investment process and trades the cost of capacity against uncertain future revenues. When many small firms compete, each firm's revenue depends on aggregate production through the market price, and the natural equilibrium notion is a mean-field equilibrium: every firm optimizes against a given aggregate, and the aggregate generated by the optimal behaviour is the one that was assumed.
Aïd, Basei and Ferrari (arXiv:2305.00541; Operations Research, 2025) add a macroeconomic regime to this picture. The economy switches between two states according to a continuous-time Markov chain, and volatilities and prices depend on the state. They prove that a stationary mean-field equilibrium exists and is unique, and that the equilibrium firm invests at regime-dependent barriers. Related stationary mean-field games with singular controls include Cao and Guo (Stochastic Processes and their Applications, 2022) and Cao, Dianetti and Ferrari (doi:10.1287/moor.2022.1323); the stability of the reflected regime-switching diffusions that appear in the equilibrium is due to Budhiraja and Liu (Mathematics of Operations Research, 2012).
A real Brownian motion and an independent two-state Markov chain with generator
live on a complete probability space; is their augmented natural filtration. A control is an adapted, nonnegative, nondecreasing càdlàg process with . The production capacity is
and investment costs , the integral (2.3) that charges a jump the amount . Given aggregate productions , the price in regime is , and a firm starting from maximizes, over the admissible set of (2.5),
A stationary mean-field equilibrium (Definition 2.2) is a pair such that maximizes over , and the controlled pair has a stationary distribution with
The barrier control at levels is
the minimal investment keeping . Finally and , whose negative roots are .
Under Assumption 2.1, , and : for every there are barriers and with
The theorem gives a fully explicit equilibrium in a model with common noise in the form of regime switching: the barriers solve a finite system of algebraic equations, and the stationary distribution of capacities is known in closed form, with a Pareto tail of exponent . This makes comparative statics of market concentration and of the industry's response to regime persistence computable, which is what Section 3 of the paper does numerically.
The result is proved on paper; none of it is formalized. A complete development would yield a machine-checked verification theorem for regime-switching singular control, a checked link between singular control and optimal stopping, and a checked stationary law for a reflected regime-switching geometric Brownian motion. The printed text contains slips the formalization corrects in the open: the continuation and stopping regions of Proposition 4.2 are printed swapped, a term of (4.18) carries a spurious factor , and an integration by parts in the proof drops .
The obvious route, solving the variational inequality (4.8) by guessing a smooth-fit solution, fails here: the two regimes couple the ordinary differential equations, and the smooth-fit and smooth-pasting equations become nonlinear in both barriers at once, so existence and uniqueness of their solution cannot be read off. The regularity a verification argument needs ( value, a threshold structure of the investment region) is therefore the hard part, and with regime switching it is not covered by the one-dimensional theory. The stationary law requires positive recurrence of a reflected diffusion with switching and the identification of its limit law. The fixed point , where is built from the stationary law under the barrier control optimal for , needs continuity and a priori bounds of for existence, and a monotonicity argument for uniqueness; the printed uniqueness argument treats ordered pairs of fixed points explicitly, and uniqueness of the optimal control itself is not argued on the page but is part of the goal.
Lean represents regimes as Fin 2 (index 0 is regime 1) and time as . The model consists of: the chain, pinned by its closed-form transition function ; Mathlib's IsBrownianReal for ; independence of and ; the augmented filtration; through the platform relation EthierKurtz.HasBrownianItoIntegral, with continuous paths; the state (2.4); the integral (2.3), computed as ; the admissible set (2.5) with -valued expectations; of (2.6); Definition 2.2; and the barrier control (4.11). is the expectation conditioned on .
Standing constants: , , , , and Assumption 2.1. The root condition is stated as " has no root in ". Pinned hypotheses, each disclosed in the item that carries it: the stationary distribution is the weak limit of the time- laws; ; wherever (4.11) is used; for the §4.2 statements; on the goal; and "" in Theorem 2.4(ii) as a ratio tending to a positive constant.
The equilibrium is defined from the model: optimality against every admissible control, including those with an initial jump, and the limit law of the actually controlled process. It is never defined through the paper's closed forms (4.23) or (4.32), which would make the goal a statement about formulas. The barrier control is the printed formula, not an arbitrary control keeping .
Not formalized: Section 3 (numerics), Proposition 4.4 and Corollary 4.5 (semi-explicit value functions), the continuity part of Step 1, and Steps 2–4 of the proof as separate items. Contributions toward a general verification theorem for regime-switching singular control, regularity of regime-switching stopping problems, and stationary laws of reflected switching diffusions are reusable beyond this mission.
In budget-feasible procurement an auctioneer with a budget wants to buy services from strategic sellers. Each seller has a private cost , the auctioneer has a public valuation over sets of sellers, and the mechanism must choose whom to pay and how much, so that sellers have no reason to misreport and the total payment never exceeds . The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a buyer with a fixed budget faces sellers whose costs it cannot observe.
Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239v2, Operations Research 2025) show that deterministic clock auctions, which repeatedly lower personalized prices and let sellers drop out, achieve constant approximations for monotone submodular valuations. Their Appendix B asks whether an even simpler family suffices: posted-price mechanisms, which approach each seller once with a take-it-or-leave-it offer. This mission formalizes their answer for additive valuations, Theorem 13 (p. 25): no deterministic posted-price mechanism achieves an approximation better than .
There are sellers , a budget , private costs , and a valuation . The valuation is additive if there are values with for every .
A deterministic posted-price mechanism knows , and , but not . It approaches sellers one at a time. At each step it looks at the history of earlier offers (the seller, the price, and whether the seller accepted) and either stops or names a seller not yet approached and a price . The seller accepts if and rejects otherwise, and is never approached again. The output is the set of sellers who accepted; each of them is paid its price. The mechanism is budget feasible if for every additive and every cost profile the accepted prices sum to at most .
For an instance, is the largest value of a set with . A mechanism is a -approximation on a class if on every instance of the class.
In Lean the sellers are Fin n, a mechanism is M : (Finset (Fin n) → ℝ) → PostedPrice n with PostedPrice n a rule next : List (Fin n × ℝ × Bool) → Option (Fin n × ℝ) on histories, run (M v) c is its history on the costs c, and accepted and payment read off the output and the total payment.
For every , every and every budget-feasible deterministic posted-price mechanism , there are an additive , costs and a set with
This is on some instance, written without division.
All three concern one valuation : a high-value seller worth and small sellers worth each, with .
The theorem separates two families of simple mechanisms. Deterministic clock auctions achieve a constant approximation for monotone submodular valuations (Theorem 1 of the same paper, a -approximation), while deterministic posted prices cannot achieve better than even for additive valuations, the simplest class. Clock auctions are therefore not merely sufficient but needed among these simple formats: the ability to lower a price after a refusal is what the constant approximation rests on. The bound also explains why the paper's positive result for posted prices (Theorem 15, symmetric submodular valuations) must give up a logarithmic factor.
The result is proved in the paper; it has not been formalized. A formal version fixes what "deterministic posted-price mechanism" means, an adaptive rule on histories that never sees costs, and makes the adversary argument checkable: the hard instance depends on the mechanism, and the case analysis must be exhaustive over all such rules. The mission also provides a reusable model of sequential take-it-or-leave-it mechanisms with budget constraints.
The statement is a lower bound over all mechanisms, so the instance must be chosen after the mechanism. The mechanism is adaptive: which seller it approaches next and at what price can depend on every earlier answer. The proof handles this by noting that, on the hard family, every seller rejects a non-positive offer, so all instances share the run up to the first positive offer or the offer to . Making that "common prefix" precise for an arbitrary history-dependent rule, and covering the mechanisms that fall outside the three printed cases (those that never approach , or offer more than ), is the work of the formal proof. A naive attempt that fixes one instance for all mechanisms fails: a mechanism tailored to that instance is optimal on it.
Fin n; valuations are functions Finset (Fin n) → ℝ, and additivity carries nonnegative weights. Costs are real and nonnegative.Contributions welcome: proofs of the three cases, the "common prefix" lemma for runs on cost profiles that agree on every seller approached, and the assembly of the goal.
Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.
Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in , which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.
Let , , be open, bounded and of class S: there are and such that for all and . Let be compact, let , and set (Assumption 1.1, eq. (3)). The solution operator maps to the unique weak solution of in , on .
For a control , a cost and a threshold , the robust problem (63) is
The state is , , and . The cone is and its polar cone is . The linear part of the state is . The active set is .
Let be convex and continuously Fréchet differentiable, and assume the constraint qualification . Then is a solution of (63) if and only if there is a nonnegative finite Borel measure on with, for ,
The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in by integration. Both directions are part of the goal.
The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.
All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of and does not treat . Condition (68) is printed per direction , while (67a) needs one measure for all .
The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone has nonempty interior. The multiplier is a priori only an element of , and the Riesz–Markov–Kakutani theorem on the compact space turns it into a measure. The state must also be shown to lie in . Continuity of each slice in is the regularity of Lemma 1.2 (continuity of solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in . Working pointwise in does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.
and are subtypes of Euclidean spaces with CompactSpace instances, so carries its sup norm. Measures on are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map such that is, for every , the weak solution in , encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's " in " is encoded on , the same condition for continuous functions. "Solution" means global minimizer over the feasible set. is identified with through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.
Added hypotheses: and nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion in , where represents . The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.
Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into . The multiplier carries its sign (a nonnegative measure, or ) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.
A complete development needs elliptic regularity in for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on ), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them are welcome.
Retail chains increasingly let a customer who visits one store buy a product that only another store carries, delivered from that store or picked up later. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) study how a seller operating several stores should choose assortments when customers can substitute across stores at a utility cost, and compare two ways of presenting the other stores' products: simultaneous recommendation (SMR), where they are shown together with the visited store's assortment, and sequential recommendation (SQR), where they are shown only after the customer declines everything in the visited store.
For fixed prices, the paper shows that under SMR the best a chain can do is to offer the single-store optimal assortment everywhere (its Theorem 1). Section 8 asks whether this survives when the seller also sets prices, store by store. This mission formalizes the answer, Theorem 6: under SMR with joint pricing, offering every product in every store at the classical single-store constant adjusted markup prices is optimal. It also formalizes the paper's Proposition 9, which transfers this solution to SQR with a factor-½ revenue guarantee.
The single-store ingredient is older. For the multinomial logit (MNL) model with product-specific price sensitivities, the optimal prices share a common markup adjusted by the reciprocal sensitivity; this goes back to work on MNL multi-product pricing such as Li and Huh (2011) and is stated in this form by Wang (2012), whom the paper cites.
There are stores and products . A fraction of customers visits store , with . The seller chooses an assortment profile with , writes , and chooses real prices , the price of product in store ; production costs are zero.
A customer visiting store who buys product in store at that store's price has utility plus an independent standard Gumbel term, where is the intrinsic utility, the price sensitivity, and the utility discount for buying from another store, with . Write . For , the customer buys from a store that offers and maximizes over the stores offering ; then and . The no-purchase option has weight .
The SMR joint problem (13) maximizes
and the SQR joint problem (15) maximizes
The single-store problem (14) maximizes over and real . Finally is the unique solution of
No uniqueness is claimed.
Theorem 6 says that, under simultaneous recommendation, cross-store substitution creates no value that a coordinated price-and-assortment policy can extract: the multistore problem decouples into independent single-store pricing problems, each solved by offering everything at a constant adjusted markup. Together with Theorem 1 it places SMR as a clean benchmark against which SQR is compared, and Proposition 9 turns the benchmark into a guaranteed policy for SQR, where the joint problem has no known closed-form solution.
None of these results has a machine-checked proof. The mission's main new formal content is the single-store MNL pricing theorem with heterogeneous price sensitivities (milestone 2), which is cited, not proved, in the paper and is not on the platform; it is reusable for any MNL pricing model. Formalizing the store-wise reduction also makes explicit what the printed argument leaves implicit: the bound holds for every tie-breaking in the best-store rule, and for arbitrary real prices.
The multistore objective (13) is not a sum of independent store problems: store 's prices enter store 's revenue through and , and the selection is itself an that changes with the prices, so the objective is discontinuous in . Direct first-order analysis of (13) is therefore not available. The single-store problem (14) is not concave in the prices either, so its optimum cannot be read off from a stationarity condition alone: one needs a global bound valid for every real price vector and every assortment, including negative prices and empty assortments.
Stores are Fin m, products Fin n (the paper's product is index ), assortments Finset (Fin n), prices real-valued functions. is the finite union of the . The best-store rule is a function Fin m → Fin n → Fin m constrained by a predicate (it must offer and maximize the customer's utility among the stores offering ); every statement holds for every such , and the right-hand side at the full profile, where , does not depend on its rule. enters as a hypothesis "θ solves the markup equation", never as a chosen term; its existence and uniqueness is milestone 1.
Standing assumptions carried as explicit hypotheses: , , and (the page's ), , . Prices range over all of . Optimality is a universal upper bound over all profiles, prices and tie-breaking rules, never a supremum or an . Proposition 9's "optimal solution to problem (13)" is the solution constructed in Theorem 6.
The choice model (13)–(15) is taken as given; the derivation of the MNL probabilities from Gumbel utilities is not formalized. A formalization in which the selection is unconstrained, in which uses store 's price sensitivity instead of the customer's, or in which the optimum is a supremum of a possibly unbounded set would change the theorem and is ruled out by the definitions.
A complete development needs only Mathlib's real analysis (exponential, logarithm, finite sums); no new library is required. The single-store pricing optimum (milestone 2) is reusable for any MNL pricing model, and contributions of a general MNL pricing library are welcome.
A retailer with several physical stores often carries a different selection in each one. A customer who walks into a store and finds nothing she likes may still buy a product stocked elsewhere in the chain, paying in delivery cost or waiting time for it. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing those other products. Under simultaneous recommendation (SMR) the customer sees the store's own assortment and the rest of the chain's products at once. Under sequential recommendation (SQR) she first sees only the store's assortment and is shown the other stores' products only after declining all of them.
The paper shows that sequential recommendation earns more than simultaneous recommendation, but that choosing the best SQR assortments is NP-hard. A natural first heuristic ignores the cross-store interaction: each store simply carries the assortment that would be optimal if it were alone. This mission formalizes the paper's guarantee for that heuristic: it earns at least half the optimal sequential revenue, and half is the best possible constant. The guarantee is proved in the heterogeneous case of the paper's §7.1, where a product may be valued differently in different stores (a flagship store downtown and an outlet store, for example).
There are stores and products. A fraction of the customers first visits store , with . Product earns revenue , and the products are numbered so that . In store , product has attraction value , where is its mean utility; not buying has attraction value . A customer who first visits store but buys product from store suffers a utility discount , with .
A decision is a profile of assortments ; write . A product reaches a store- customer through the cheapest store that offers it, with discount . Under the multinomial logit model with sequential recommendation, a customer who first visits store buys product with probability
and the seller's expected revenue is
Its maximum over all profiles is .
The single-store problem of store is
An assortment is revenue-ordered if it is for some . Some revenue-ordered assortment is optimal for the single-store problem; denotes the smallest such one. The heuristic offers in store for every , and its revenue is , cross-selling between stores included.
and the factor is tight: for every there is an instance with two stores and two products on which .
The guarantee says that the simplest decentralized policy, in which every store optimizes as if alone, cannot lose more than half of what the best sequential recommendation earns, whatever the store-specific valuations and the cross-store discounts. Read from the other side, the same bound with its tight instance says that sequential cross-selling can at most double the revenue of operating the stores separately, and that a doubling is approached. Since the exact SQR problem is NP-hard (the paper's Proposition 3), a constant-factor guarantee for a policy computable store by store is the kind of statement a practitioner can act on; the paper's numerical study (its Appendix G) finds the heuristic much closer to optimal on synthetic data than the worst case.
Proposition 7 is proved in the paper; nothing in it has been machine-checked. The mission formalizes the model, the proposition with both parts, and the three steps of its proof. Lemma D.1, the monotonicity of the optimal MNL revenue in the attraction values, is a standard fact of assortment optimization that is stated here for a single MNL model and is reusable beyond this mission.
The heuristic profile and the optimal profile are unrelated: the optimal one may stock in store products that store 's own optimum omits, precisely to sell them to other stores' customers in the second stage. A comparison store by store therefore fails, because the optimum's revenue in store depends on every other store's assortment through and the discounts . The second-stage revenue is a product of two MNL fractions over different assortments with discounted attraction values, and it has to be bounded by the single-store optimum with undiscounted values; this is where Lemma D.1 is needed, and the lemma itself does not follow from comparing a fixed assortment, since the optimal assortment changes with the attraction values. For the tightness part, the answer depends on the tie rule that defines : in the instance, store 2 has two optimal single-store assortments, and only the smallest one makes the bound tight.
Lean 4 with Mathlib. Products are Fin n (the paper's product is index ) and stores are Fin m; assortments are Finset (Fin n) and profiles are Fin m → Finset (Fin n). Attraction values are the primitive data, not utilities. The discount factor is the largest over the offering stores, and when no store offers (the paper's ). The single-store revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1 S. The model is the choice probabilities (10) and the objective (SQR-heter), taken as given; the paper's derivation of (10) from Gumbel utilities is not formalized.
The standing assumptions , , , , and are explicit hypotheses of every theorem. One hypothesis is pinned beyond the page: . The paper's revenues are prices and its proof drops a second-stage revenue term that is nonnegative only for nonnegative revenues, but the sign is never stated. The paper's tightness claim ("an instance where the equality holds") is realized only in the limit , so the goal states it in the form "for every , some instance has ".
"Optimal" means a maximizer over all assortments or profiles, ties allowed, and is never formed as a term: the bound is stated as for every profile . is a predicate (revenue-ordered, optimal, and of least cardinality among the revenue-ordered optima). An encoding in which can never exist would make the bound vacuous, so the tightness part asserts that exists on its instance. The tightness part also must use the paper's tie rule, not an arbitrary single-store optimum, since with the other optimum the instance is not tight.
Welcome contributions: proofs of Lemma D.1 and of the two halves of the bound, the exact evaluation of the tightness instance, and a general Lean library for single-store MNL assortment optimization (existence of revenue-ordered optima, monotonicity in attraction values) that the other missions of this series can reuse.
Lambda Value-at-Risk (VaR), introduced by Frittelli, Maggis and Peri (Mathematical Finance 24(3), 2014), generalizes the Value-at-Risk used in banking and insurance regulation: instead of one fixed confidence level, the level may depend on the size of the loss. It has since been studied for its properties, representation and characterization (Bellini and Peri, SIAM J. Financial Math. 13(1), 2022; Han et al. 2025; see the references of arXiv:2511.00717v1).
Regulators and risk managers rarely know the loss distribution exactly. A standard way to account for this ambiguity is to evaluate the risk measure under every model in a neighbourhood of a reference model and report the worst case. Neighbourhoods defined by a -divergence (Kullback–Leibler, chi-squared, -divergences) are the most common choice in distributionally robust optimization (Ben-Tal et al. 2013). P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv:2511.00717v1 (2025), define VaR with respect to a capacity. They show that for increasing the worst case over a -divergence ball is again a VaR, under an explicitly distorted reference probability. This mission formalizes that result.
Let be a measurable space. A capacity is a set function that is increasing () with and ; every probability measure is one. Let be the set of increasing functions . For a capacity and a random variable ,
with and . A constant gives the Choquet quantile . For a class of capacities, and are its setwise envelopes; for a class of probability measures they are written and .
Fix a probability measure and a convex with and . For a probability measure , , and for the -divergence ball is . The distortion is , and
For , , and every random variable ,
If moreover is finite, strictly convex and , then
The theorem reduces a supremum over an infinite-dimensional set of models to a single VaR under the reference model with a transformed level function . Robust VaR therefore inherits the computational and statistical tools available for VaR, and the worst-case VaR at level is the ordinary VaR at the explicit level . The limit statement shows an asymmetry: as the ambiguity vanishes, the robust value converges to the upper version , not to ; the two differ when the distribution function of has a flat piece where it meets .
The result is proved in the paper (2025) and, to our knowledge, nothing of it is machine-checked. The platform has no capacity, no Choquet quantile, no VaR, and no -divergence over general (non-discrete) probability spaces; the mission supplies all of these, and the formula for the upper probability of a -divergence ball (Proposition 5) is a reusable fact about divergence balls in its own right.
Proposition 2 is an order-theoretic exchange of a supremum with an infimum; it fails for decreasing (Example 1 of the paper), so monotonicity of must be used at the right place, and the values have to be handled. Proposition 5 asks for the exact value of a supremum over an infinite-dimensional ball of measures, for a that may take the value and may be negative; the upper bound must hold for every density in the ball, not only for the simple ones, and the integrability conventions of matter. The second part of Proposition 5 is real analysis of the perspective function , and continuity of at the endpoints and does not follow from continuity of alone. In the limit the natural guess is wrong: the limit is , so any argument that treats the robust value as a perturbation of fails at flat pieces of the distribution function.
All definitions live in the namespace LambdaVaRAmb.Robust. A random variable is a measurable function ; statements quantify over all of them, which covers every domain the paper allows. Set functions are Set Ω → ℝ and the capacity axioms are imposed on measurable sets. VaR, VaR, the suprema over the ball and the limits as are taken in EReal, so are genuine values. is ℝ → EReal (only its values on matter); convexity uses . is the integral of the positive part of minus that of the negative part; members of the ball are probability measures. is defined as , which is the inverse of on under the hypotheses where the paper uses it.
Implicit hypotheses made explicit: the classes and in Proposition 2 and Corollary 1 are nonempty; "" in the second parts is the hypothesis that is finite on ; " being the solution" is posed as existence and uniqueness.
The trivializing readings are ruled out: suprema over the ball and VaR values are never real sSup/sInf (which would collapse to on empty or unbounded sets); the envelopes are real suprema only over nonempty classes of values in ; the ball always contains , so it is not empty; is the paper's supremum, not a closed form for a particular .
Needed infrastructure, all reusable beyond this mission: capacities and Choquet-type quantiles; -divergences for general measures via Radon–Nikodym derivatives; conditional Jensen for extended-valued convex functions; perspective functions. Contributions of any of these, and proofs of the milestones in any order, 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.
Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price below the reference is perceived as a gain and raises demand; a price above it is perceived as a loss and lowers demand. Because today's price moves tomorrow's reference price, a seller who maximises the revenue of each period separately ignores how it erodes or builds future demand. This makes pricing a dynamic program, studied for a single product with linear demand by Popescu and Wu (Operations Research 2007) and Chen, Hu and Hu (Management Science 2017), among others.
Guo, Jiang and Shen (SSRN 4189049, published in Manufacturing & Service Operations Management, 2025) treat several substitutable products under multinomial-logit (MNL) demand. The dynamic program then has a continuous state of dimension , and computing the optimal policy is impractical even for moderate . The myopic policy, which maximises the current period's revenue only, is easy to compute. This mission formalizes the paper's bound on how much revenue the myopic policy can lose (Proposition 2).
There are products . Product has intrinsic utility , price sensitivity , and reference-price sensitivities (to gains) and (to losses). At price vector and reference vector , the utility of product is
the market share is , and the single-period revenue is .
Prices and reference prices lie in the admissible box with a price ceiling . The reference price follows exponential smoothing with memory : . Revenue is discounted by .
With , for every and every myopic policy,
The bound is uniform in the initial reference price and has an explicit constant. It vanishes in three regimes: (the reference price never moves), (only the present counts) and (no reference effect). It quantifies how much the intertemporal structure costs a seller who ignores it. The myopic policy is computable by a one-dimensional root search (Theorem 1 of the paper), while the optimal policy suffers from the curse of dimensionality, so the bound is what makes the myopic policy a usable benchmark.
The paper proves Proposition 2 in its online supplement (Appendix C.1), which is not part of the source file used for this mission. To our knowledge, none of these results has a machine-checked proof. Formalizing them yields a verified Bellman equation for a deterministic dynamic program with a continuous multidimensional state and a nonsmooth, nonconcave reward.
The left inequality only uses the fact that the myopic price sequence is admissible. The right inequality is the content. Comparing the two value functions period by period fails: in a given period the optimal policy may earn less than the myopic one, and its later advantage comes from having moved the reference price. The two policies also generate different reference paths, so their revenues are evaluated at different states, and the sensitivity of the revenue to the reference price enters only through the constant . The revenue is not concave in prices or in reference prices, and the kinks at make it nonsmooth. The Bellman equation itself needs the optimal value to be well behaved enough in for the one-step maximum to be attained.
Products are indexed by Fin n (product is Lean index ), and vectors are Fin n → ℝ. The shares are defined directly by the logit formula; the Gumbel random-utility derivation is motivation only. The standing assumptions , , , and are hypotheses of every theorem. The goal also assumes the ceiling condition , as a standing assumption of §2.4. That condition is stated as the existence of a root of (9) at most . The Bellman equation omits the ceiling condition (it holds without it). Proposition 1.1 varies , so it does not take the condition.
optValue, the supremum over all admissible price sequences, built as an instance of the published deterministic dynamic program KarlinDP.Deterministic.optimalReturn (Karlin 1955). The paper writes as a maximum over stationary policies and uses it through (6); milestone 1 is the theorem that connects the two.⨆ i, which is when (then ).Lean's real supremum is on an unbounded family and its tsum is on a non-summable series. Neither default is reached here: with and the family is nonempty and bounded by , and every series is summable. So the goal cannot hold vacuously through a junk value. In particular, may not be replaced by an arbitrary solution of (6), and the constant may not be weakened, for example by replacing with .
Needed infrastructure: continuity of the MNL revenue, the Bellman equation for a discounted deterministic program on a compact action set, and bounds on the myopic value as a function of . The first two are reusable beyond this mission. Contributions toward any milestone are welcome.
Financial networks are webs of liabilities: firm owes firm an amount , and every firm holds some external assets. When firms cannot pay in full, how much money actually moves through the network depends on how each firm splits its available funds among its creditors. The classical clearing model of Eisenberg and Noe (2001) fixes this split by a proportional rule. Flow allocation games, introduced by Bertschinger, Hoefer and Schmand (arXiv:1908.01714, Mathematics of Operations Research, 2025), make it strategic: every firm chooses how to allocate whatever it receives, and the resulting payments are the clearing state of the chosen strategies.
Because money that circulates comes back, the total amount of flow in such a network is driven by cycles, and cycles require several firms to cooperate. The natural solution concept is therefore the strong equilibrium, which is stable against joint deviations of coalitions. The paper shows that in unit-ranking games a strong equilibrium maximizing total flow always exists (Theorem 9, price of stability ). This mission concerns the other side: how much total flow can the worst strong equilibrium lose, and which structural parameter of the network controls the loss.
A flow allocation game consists of a finite directed graph (parallel edges allowed), a fixed supply at each node and a capacity on each edge. Every node is a player. and denote the outgoing and incoming edges of , and .
In a unit-ranking game, player chooses for each edge a non-decreasing function with and : given a total supply , it forwards all of it until its outgoing edges are full, one unit at a time according to a ranking of unit capacities. A flow is feasible for a profile if with . The clearing state is the coordinatewise largest feasible flow; player 's utility is , and the total flow is
A profile is a strong equilibrium if no non-empty coalition can jointly switch to other unit-ranking strategies so that every member of strictly gains.
The circulation network adds an auxiliary node with edges of unbounded capacity and of capacity for every . An optimal circulation of maximizes . A decomposition of into cycles of unit flow is a list of simple directed cycles of that uses each edge exactly as often as has units on it. The parameter of this mission is
the smallest possible size of the longest cycle, over all decompositions of all optimal circulations; sizes count auxiliary edges.
In unit-ranking games, the price of anarchy for strong equilibria in terms of Flow is at most : for every strong equilibrium and every unit-ranking profile ,
The statement fixes no constant beyond the structural parameter and holds for all capacities and supplies.
The bound identifies the length of the circulating cycles as the quantity that governs the efficiency of coalition-stable payment behaviour. In networks whose optimal circulation decomposes into short cycles, such as bilateral or triangular netting of liabilities, every strong equilibrium clears at least a fraction of the optimal total payments; Proposition 17 shows that long cycles genuinely cost efficiency, so the bound is tight up to one. For pure Nash equilibria no such bound exists (Proposition 15, the price of anarchy is unbounded), so the result separates coalitional from unilateral stability.
The results are proved on paper; none of them is machine-checked. A formalization adds a precise account of the model (clearing state as a supremum of feasible flows, unit-ranking strategies as functions on , cycle decompositions of the circulation network) and checks a proof whose last step, as printed, needs repair. The printed last display, , does not hold for cycles passing through the auxiliary node : with a single node , and no outgoing edges, but . The theorem itself is not contradicted by this example, and the printed argument is complete for games without fixed supplies. The cycles through the auxiliary node need a separate count, which is part of the work this mission asks for.
The upper bound compares an arbitrary strong equilibrium with an optimum that may look nothing like it. The obvious approach, counting the units of each optimal cycle that also carry equilibrium flow, fails: the clearing state is a fixed point of all strategies at once, so whether a unit reaches an edge depends on decisions all around the network, and the equilibrium may route its flow along entirely different cycles. A single player cannot complete a cycle on its own, which is why the Nash price of anarchy is unbounded; any argument has to use coalitional deviations, and a deviation changes the clearing state globally, so its effect on each member's utility must be controlled through the fixed point.
The second difficulty is the auxiliary node. A cycle of the optimal decomposition that passes through contains a node that is not a player, so no coalition of players can claim it, and the unit of flow it represents may sit on an auxiliary edge that does not count. These cycles are exactly where the printed argument stops short.
Supplies, capacities, strategies and flows are natural numbers, as the paper prescribes for unit-ranking games. The graph is a finite type of nodes and a finite type of edges with tail and head maps, so parallel edges and loops are allowed. The clearing state is the coordinatewise sSup of the feasible flows. Coalitions are non-empty, and deviations range over unit-ranking profiles. Optimal circulations are optimal among integral circulations. Cycles of are lists of edges with pairwise distinct start nodes, and decompositions are lists of cycles counted with multiplicity. Nodes of are Option V, with none the node .
The price of anarchy is stated multiplicatively, , with no division, so a zero-flow equilibrium cannot satisfy the goal vacuously through a junk quotient. The parameter enters as a hypothesis, "some decomposition of some optimal circulation has all cycles of size at most ", which is equivalent to the bound for the min-max and avoids an infimum that would be on an empty set. In Proposition 17 the strong equilibrium is required to have positive flow, since otherwise the lower bound would hold trivially.
Not formalized: the complexity results of the paper, the bounds for other quality measures (Proposition 18) and for Nash equilibria (Proposition 15). A complete development needs the integral version of the lattice theorem for feasible flows (Theorem 2), the existence of a Flow-optimal profile from the proof of Theorem 9, and integral cycle decomposition of circulations; the last two are reusable beyond this mission. Contributions are welcome on each milestone, on a separate count for cycles through , and on the explicit construction of Proposition 17.
Global sensitivity analysis asks how much the uncertainty in an output of a model or a data set is explained by an input . A large family of indices has the form "expected discrepancy between the marginal law of and its conditional law given ": the variance-based index of Sobol' and Wagner, the density-based index, Kuiper and Cramér–von Mises indices. Borgonovo, Figalli, Plischke and Savaré (Management Science 2025, doi:10.1287/mnsc.2023.01796) take the discrepancy to be an optimal-transport cost. The resulting indices apply to multivariate outputs, need no density, and include as special cases the numerator of Wiesel's Wasserstein correlation coefficient (Wiesel 2022, arXiv:2207.14079).
A sensitivity index is meant to measure information: how much knowing , or a coarsening of , tells about . Two properties make this reading legitimate. Coarser information must never be worth more than finer information, and an index computed from increasingly fine observations of must approach the value for the limiting information. This mission formalizes both properties for the optimal-transport indices, Theorems 8 and 9 of the paper. Theorem 9 is also the last step of the paper's consistency proof for its partition estimator (Theorem 21).
Let be a probability space, and Polish spaces with Borel σ-algebras , , and , measurable maps. Write and for the laws of and .
A cost is a continuous function with exactly when . The optimal-transport cost between probability measures on is
where is the set of probability measures on with marginals and .
For a σ-algebra , representing partial information on , a version of the conditional distribution of given is a family of probability measures on with -measurable and
The OT-based sensitivity measure (Definition 1) is
written when . For a Borel map into a Polish space, is a new random variable and is defined in the same way on ; is the σ-algebra generated by .
For an increasing sequence of sub-σ-algebras of with join ,
The results. Theorem 8 is the formal statement that the OT indices value information monotonically: a transformation of an input, such as a discretization or an aggregation of features, can only lose explanatory power, and loses none when is injective. Theorem 9 makes the indices continuous in the information: refining a partition of the input space, as an estimator does when the sample grows, recovers the index of the limiting σ-algebra. The paper relies on Theorem 9 to prove that its given-data estimator is consistent, and on Theorem 8 to justify its interpretation of the indices as values of information.
The formalization. The proofs are on pp. 35–36 of the authors' manuscript. As far as we know, none of these statements has been machine-checked. Formalizing them requires conditional distributions relative to arbitrary sub-σ-algebras, the convexity of optimal-transport costs under mixtures, and their lower semicontinuity under weak convergence, which are general facts of optimal transport that the platform does not yet have.
The monotonicity in Theorem 8 is a Jensen inequality, but it is applied to a function of a measure, , along a mixture indexed by a disintegration, so the step needs a measurable choice of near-optimal couplings. Without such a choice the averaged coupling is not defined.
For Theorem 9, the inequality follows from monotonicity, and is the substance. The natural first idea, Lévy's upward theorem applied to , gives convergence for one test function at a time and outside a null set that depends on . Weak convergence of the conditional laws for almost every is a statement about all test functions at once. Even with it, is only lower semicontinuous, not continuous, and the cost may be unbounded and take the value . No integrability hypothesis is available: the theorem holds without assuming , including when the limit is .
ℝ≥0∞); integrals are lower Lebesgue integrals.RWPI.SqrtLasso.transportCost. Its first argument is the marginal and its second the conditional law.IsCondDistrib), never constructed. Every statement holds for every version, and versions for different need not be compatible.⨆ n, Fs n), and the sequence is indexed from .The goal is a Tendsto in , not a one-sided bound. In particular, a proof of only (monotonicity) or of the statement under a finiteness hypothesis on does not close it. uses the conditional distribution of given the random variable on , not that given ; their equality is part of (24).
Two readings are disclosed corrections. Theorem 9's "sub-σ-algebras in " is read as sub-σ-algebras of . The comparison of two sub-σ-algebras , used in the proof of Theorem 9 but stated in Theorem 8 only for , is posed as its own milestone.
Reusable infrastructure includes the following, and contributions of any of them are welcome:
Optimal auction theory in the tradition of Myerson (1981) assumes that the seller knows the distribution of the buyers' valuations. In practice that distribution is estimated, misspecified, or simply unknown. Prior-independent mechanism design asks for a mechanism that performs well across a whole class of distributions, without being tuned to any one of them. A natural yardstick is regret: the gap between the revenue the seller would extract if she knew the valuations, namely the highest valuation, and the revenue her mechanism actually collects. The seller chooses a mechanism to minimize the worst case of this gap over all distributions Nature may pick.
For a single buyer, Bergemann and Schlag (2008) showed that the minimax regret over valuations supported on is , attained by a posted price drawn at random with CDF on . Whether a comparably explicit answer exists for buyers, and whether the familiar second-price auction remains optimal among all dominant-strategy mechanisms, was open. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) answer both questions for i.i.d. valuations. This mission formalizes that answer: their Theorem 1.
A seller has one indivisible item and buyers with valuations . A mechanism assigns to every valuation profile allocation probabilities and expected payments . It is dominant-strategy incentive compatible (DSIC), written , if for all , all and every misreport :
For a joint distribution of , the regret is
and the minimax regret over a class of distributions is . Here is the class of product laws whose marginal is supported on .
A second-price auction with random reserve draws a reserve price from a distribution . The highest bidder wins if her bid is at least and pays , where are the two highest valuations. Otherwise nothing is sold.
Two explicit functions enter the answer. For , let
and, for ,
with below and above . The isorevenue marginal on , , is the law under which every posted price in earns the same revenue .
Let be the root of in ; it is the only root in . A reserve distribution on with CDF exists. The auction is DSIC and minimax-regret optimal, and
The Lean goal states the location and uniqueness of the root, the existence of the reserve law, the DSIC property, the upper bound for against every i.i.d. law, the matching lower bound for every DSIC mechanism, and the literal identity for .
A companion item states Corollary 1 (p. 14): for , , on , and the minimax regret is .
The theorem gives, for every number of buyers, a closed-form description of the minimax-regret optimal mechanism among all DSIC mechanisms, together with its value. The optimum is a familiar format, a second-price auction, but its reserve price must be randomized. The same saddle point is the starting point for the paper's results on affiliated and arbitrary joint valuations, which are separate missions of this series.
The result is proved on paper. To our knowledge none of it has been formalized. A complete development would supply machine-checked versions of several tools that recur in robust mechanism design: DSIC mechanisms with randomized allocations, the regret functional, order-statistic CDFs of product measures, Myerson-type revenue characterizations under distributions with atoms, and saddle-point arguments for inf–sup problems over mechanisms and distributions.
The upper bound (Step 1) is a pointwise optimization once the regret of is written through the CDFs of the order statistics. Writing it that way already requires integration by parts against arbitrary distributions on , which may have atoms.
The lower bound (Step 2) is the hard direction. One must show that no DSIC mechanism beats against the isorevenue law. The standard route through Myerson's virtual values does not apply directly: the isorevenue law is a mixture of a density and a point mass at , so the revenue of a general DSIC mechanism has to be characterized from first principles. That characterization starts from the payment identity for dominant-strategy mechanisms. The closed forms also involve a transcendental root and a logarithmic ODE solution, so the monotonicity and boundary facts about (it is a CDF, ) need real analysis rather than numerics.
Buyers are indexed by Fin n, valuations are functions Fin n → ℝ, and distributions are measures on that space. (IR), (IC) and (AC) are imposed for valuations in , which is all the seller considers. Two conditions are added to DSIC so that the expectation in the regret is meaningful: the allocation and payment rules are measurable, and payments are bounded on the cube. The second-price auction breaks ties in favour of the lowest index; the revenue does not depend on the rule. A reserve law or an isorevenue law is described by a hypothesis on its CDF. is defined piecewise, so its closed form is never evaluated at the singular point , and "" is stated as a one-sided limit. The minimax regret is a real infimum over the nonempty class of DSIC mechanisms of real suprema of bounded families. Uniqueness of is stated on , which is what the paper's proof establishes.
Trivializing formalizations are ruled out explicitly. The regret is not a Bochner integral of a possibly non-integrable payment, which Lean would set to . The mechanism class is not restricted to second-price auctions. The value is the explicit integral, not a sSup. The root's location in is part of the claim.
Contributions are welcome at every level. These include the DSIC property of , order-statistic CDFs of product measures, Lemma B-1 and Proposition 1, the analytic facts about and , the payment identity for DSIC mechanisms with randomized allocations, and the revenue bound of Step 2. The analytic and mechanism-design infrastructure is reusable beyond this paper.
Appointment systems, airport runways, outpatient clinics and container terminals do not receive customers at random: each customer is scheduled at a fixed slot and arrives near it, early or late by a random amount. Queues fed by such scheduled traffic have been studied since Winsten (1959) and Mercer (1960). Kingman (1962) showed that, below critical load and for perturbations that are positive with finite mean, the heavy-traffic limit of the equilibrium waiting time of an S/G/1 queue ("S" for scheduled) is the same as for the D/G/1 queue with perfectly punctual arrivals. Araman and Glynn (2012) proved a functional central limit theorem for scheduled traffic when the perturbations have infinite mean, where fractional Brownian motion appears, and Araman, Chen, Glynn and Xia (2022) established properties of scheduled traffic, among them the decomposition and exponential moments used below, and showed that with Pareto-like perturbations the critically loaded S/D/1 workload grows without bound.
Araman and Glynn (arXiv:2212.04164, published as a technical note in Operations Research, 2025) settle the critically loaded case. This mission formalizes their diffusion limit (Corollary 1): when the mean service time equals the slot length, the workload grows like with an explicit reflected-Brownian limit, exactly as if arrivals were punctual. A companion mission formalizes their Theorem 1, the stability criterion for deterministic service times.
Fix . Customer is scheduled at time and arrives at
where the perturbations are i.i.d. real random variables with , and the uniform shift is uniform on and independent of ; the shift makes the arrival point process time-stationary. The counting function is for , so .
Customers arriving after time are numbered in order of arrival and bring service times , i.i.d., with , independent of . A single server works at unit rate and is empty at time , so the workload is
The queue is critically loaded when . The proof works with the counts of early and late customers, and . Finally, reflected Brownian motion with mean , unit volatility and is for a standard Brownian motion .
If , and , then
The case is included; the limit is then .
The result. At critical loading a queue fed by a renewal process with non-degenerate interarrival or service times is null-recurrent at best, and its workload grows like . Corollary 1 shows that scheduled traffic behaves the same way as soon as service times vary, however heavy the (finite-mean) tail of the perturbations: the arrival process contributes nothing on the diffusion scale, and the limit depends only on and . In particular, whenever , which is why the paper's stability question (Theorem 1, the companion mission) is posed for deterministic service. Proposition 1, that scheduled traffic deviates from its fluid path by only over , is of independent use for any functional of scheduled arrivals.
Formalizing it. The result is proved on paper in a short note that cites two ingredients (the decomposition of and the exponential moments of ) from Araman et al. (2022) and leaves the time reversal implicit. A formalization makes those steps explicit and checks the constant: the proof's final display prints , which matches (1.1) only when its is . No part of the argument has been machine-checked so far.
The arrival-process part (Proposition 1) is elementary in each step but long: independent-indicator moment generating functions, stationarity of a perturbed lattice under shifts, and a union bound over slots. The obstacle is the last step. The obvious route, "apply Donsker's theorem", does not apply directly: the random walk is evaluated at the random times , which are not independent stopping times of the walk but come from an independent process, and the target is the law of a Brownian maximum, identified with through Lévy's reflection identity. Mathlib has the central limit theorem and Brownian motion but no invariance principle and no reflection principle. A second trap is the time reversal: the proof's starting expression uses the counting function of the reversed process (perturbations ), and replacing it by the forward count gives a statement that is false in law for asymmetric perturbations.
Lean conventions: the perturbations are a sequence ξ : ℤ → Ω → ℝ; the standing assumptions are bundled in ScheduledInput (measurable, iIndepFun, identically distributed, Integrable (ξ 0), U with the uniform law on , U independent of the whole sequence) and ServiceInput (i.i.d. V : ℕ → Ω → ℝ, MemLp (V 1) 2, V independent of the pair (U, ξ); V 0 is unused). is an ncard in ℕ; , and slot increments are encard in ℕ∞, and every statement that converts them to numbers carries an almost-sure finiteness conjunct. Suprema are real suprema over or . Convergence in distribution is TendstoInDistribution (which includes almost-everywhere measurability), convergence in probability is TendstoInMeasure. The Brownian motion is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an arbitrary probability space, and is B 1 − ⨅ u ∈ [0,1], B u. is written out.
Corrections to the printed text, each recorded in the item notes: the workload index range is (the page's gives ); counts arrivals in instead of the page's non-additive closed intervals; the constant is for the proof's ""; the counting function in the reversed representation is that of the reversed input; "as " on p. 5 means ; and the misprinted intermediate lines of the bound on are not used.
Trivializing formalizations are ruled out as follows: counts that are infinite on a set of positive probability cannot make a bound easier, since finiteness is asserted; the limit is a probability law on , not on an extended line; the limit is reflected Brownian motion at time , not a substituted half-normal formula; and is not excluded.
Needed infrastructure: a Donsker-type invariance principle (or at least the convergence of the maximum of a random walk, which is an open platform goal of its own), a random time-change lemma, Lévy's identity , and stationarity of perturbed lattices. These are reusable well beyond this paper. Contributions to any milestone, or to these supporting results, are welcome.
Social media influencers earn money by endorsing products to their followers. An influencer who endorses only products that fit her organic content keeps her audience; one who accepts every sponsorship offer earns more per follower today but loses part of her audience and grows more slowly. Practitioners describe this as the choice between growing and monetizing, and the marketing literature documents both sides of it: followers unsubscribe after poorly fitting sponsored posts (Cheng and Zhang 2022), and small influencers have deeper engagement than large ones (Bentley et al., J. Global Marketing 34(3), 2021, cited in the paper).
Nistor, Selove and Villas-Boas (Management Science, Articles in Advance 2024) turn this trade-off into a deterministic continuous-time control problem. Awareness of the influencer spreads by word of mouth as in the Bass (1969) diffusion model, and the influencer's authenticity is the control. The paper's first main result, Proposition 1, characterizes the optimal policy completely: depending on two explicit conditions, the influencer is always authentic, always inauthentic, or authentic until her awareness reaches a threshold and inauthentic forever after. This mission formalizes Proposition 1 and the lemmas of §3.3 that lead to it.
Time is and the mass of potential followers is one. The influencer's awareness is the fraction of potential followers who know her, starting from . At each time she is authentic or inauthentic. Following Table 1 of the paper, with parameters and (the reduced-form parameters of §3.1, which aggregate the offer arrival rate, the share of good-fit offers and the followers' tolerance of bad-fit posts):
Awareness grows according to the equation of motion (1),
so it grows at rate when she is authentic and when she is inauthentic. With discount rate the influencer maximizes the discounted profit (2),
and is the value of starting at awareness and following the optimal policy.
Two closed-form objects enter the main result. The value of always being inauthentic from awareness is (Lemma 3)
and its derivative is (3)
Condition 1 (with footnote 4) holds if or .
For , , , :
and for all sufficiently small the policy "authentic while , inauthentic once " is optimal.
In the paper's order: Lemma 1 (corrected) bounds the growth of above awareness ; Lemma 2 (corrected) shows that permanent inauthenticity is optimal at large awareness; Lemma 3 gives in closed form; (3) identifies as its derivative; (4) computes the limit of at zero awareness,
which is where Condition 1 comes from.
Proposition 1 is the benchmark of the paper: each of the six model extensions of §4 (celebrities, follower turnover, partial authenticity, viral content, two segments, commitment) is read against it. Its third clause explains an observed pattern in influencer marketing, that small influencers post fitting content and large ones accept most sponsorships, as an optimal policy rather than a change in preferences, and Condition 1 makes explicit when growth potential outweighs current profits; the paper notes it always holds when . The numerical example of §3.5 (Table 2) places the switch at about 73% awareness.
The proofs are in an online appendix and have not been machine-checked. Formalizing them requires an optimality argument against every measurable switching pattern, not only threshold policies. The mission also records two corrections: Lemma 1 and Lemma 2 are false as printed when (explicit counterexamples are in the milestone statements), and they are stated here with the constant that the paper's own argument gives.
The natural argument compares, at each instant, the extra profit from inauthenticity, , with the value of the extra growth from authenticity, . This requires knowing the value function , its differentiability, and the Bellman equation it satisfies, none of which is given; replacing by is only justified along the part of the trajectory after the switch. The comparison must also hold against every measurable switching pattern, under which awareness solves (1) only almost everywhere. Clause 3 additionally needs the threshold equation to have a single crossing and the optimal trajectory to cross it exactly once. Optimality of a constant policy cannot be read off from instantaneous profits alone when : the instantaneously better choice (inauthenticity) can be the wrong one for a small influencer.
A trivializing formalization is ruled out: optimality is never assumed, the competitor class contains the constant policies' logistic paths, the threshold must solve the equation of (3) inside , and measurability of policies keeps every profit integral meaningful. The microfoundations of §3.1 (, , , , ) do not enter any statement.
The development needs Carathéodory solutions of a scalar ODE with a measurable switching coefficient, comparison and uniqueness for such solutions, differentiation under an improper integral, and a verification argument for a one-dimensional deterministic control problem with bang-bang control. The last two are reusable for other continuous-time marketing and diffusion models. Proofs of any milestone are welcome, as are proofs of the logistic closed form underlying Lemma 3.
A portfolio manager who observes today's value of a covariate (a market signal, a macroeconomic indicator) wants to choose a portfolio that performs well conditionally on that observation: the relevant risk is of the asset return , not its unconditional mean. With finitely many historical pairs , the empirical conditional distribution at a new is usually empty or rests on one or two samples, so estimating it directly is unreliable. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research 2025) hedge it with distributionally robust optimization: they take the worst case of the conditional expectation over all joint laws of within an optimal-transport ball around the empirical measure that still put a prescribed amount of mass on the conditioning event.
The objective is a ratio of two linear functionals of the law, so the standard strong-duality theorems for Wasserstein distributionally robust optimization (Mohajerin Esfahani and Kuhn, 2018; Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) do not apply directly. This mission formalizes the paper's answer in the singular case where the conditioning event is the single point and the event must keep mass at least .
Let (covariates) and (returns) be spaces with ground costs , , combined into the separable cost . The data are samples , , with empirical measure .
For a loss at a fixed decision, the object of study is the worst-case conditional expected loss
For and ,
The loss is arbitrary (measurable, real-valued), and both sides may be .
Theorem 3.2 reduces an infinite-dimensional, fractional worst-case problem to a two-multiplier convex program whose only infinite-dimensional pieces are suprema over . For piecewise-linear losses and norm costs the paper turns this into the conic programs of Propositions 3.3–3.4, which are what make the robust conditional portfolio model solvable in practice. It also compares the formulation with the trimming approach of Esteban-Pérez and Morales (Mathematical Programming, 2022), whose adversary may only pick laws with fiber mass exactly ; Proposition A.5 shows that, at , the more powerful adversary allowed attains the same value.
The result is proved in the paper; nothing here is open mathematics. None of it is formalized. A complete development would add to the platform a first conditional (fractional) distributionally robust duality, a decomposition of optimal-transport balls around empirical measures (milestone 1, reusable by every finite-sample Wasserstein result), and a moment-problem duality with one budget constraint (milestone 5).
The ratio objective is the obstacle: neither the numerator nor the denominator alone determines the worst case, and a law that is optimal for the numerator may violate the mass constraint. The step "fix the fiber mass at " (Proposition A.5) is where the obvious argument fails: an optimal law may put more than on , and reducing that mass requires moving sample points off at vanishing transport cost, which needs points of arbitrarily close to . Milestone 1 needs the existence of optimal couplings, which Mathlib lacks. Milestone 5 is an infinite-dimensional Lagrangian duality whose Slater point degenerates on the boundary of the weight set, so the final interchange of supremum and infimum must avoid that boundary.
and are Polish spaces with their Borel σ-algebras; samples are indexed by Fin N with , repeats allowed. The optimal transport cost is the published RWPI.SqrtLasso.transportCost (an infimum of lower integrals of the -valued cost; attainment is not built in), and every expectation of the loss is the published ModelRiskOT.Duality.extIntegral, in . Worst-case values and duals are EReal suprema and infima. The loss is a measurable L : Y → ℝ standing for at an arbitrary decision.
Hypotheses beyond the page, all disclosed in the statements:
NotIsolated: for every there is with . This is Assumption 2.4(iii) at read with the ambient boundary of , as the paper's remark on p. 11 does; with the topological frontier in , (iii) is vacuous at an isolated , and Theorem 3.2 is then false.Trivializing formalizations are ruled out: conditional expectations are only taken at laws with fiber mass at least (never at mass , where a real division would return ); expectations are never Bochner integrals, which would be for a non-integrable loss; the radius enters through ENNReal.ofReal ρ only where or forces ; and every supremum ranges over exactly the paper's feasible set.
Needed infrastructure: existence of optimal couplings on Polish spaces (Villani, Theorem 4.1), a Lagrangian duality for moment problems, and Mathlib's Sion minimax theorem for the interchange. Contributions to any of these, and proofs of the milestones in any order, are welcome.
Banks lend to each other. When one bank's investments fail, it may be unable to repay its interbank debt, and its creditors then receive less. Since Eisenberg and Noe (2001), the standard way to compute who pays whom after such losses has been a clearing vector: a fixed point of a system in which every bank pays the smaller of what it owes and what it has. Much of the later literature on systemic risk takes the banks' assets as given and asks how losses spread through this fixed point, for example Acemoglu, Ozdaglar and Tahbaz-Salehi (2015).
Chong Shu's paper Endogenous Risk Exposure and Systemic Instability (Management Science, doi:10.1287/mnsc.2022.01519) reverses the question: when banks know they are connected, how much risk do they choose? A successful bank pays its interbank debt in full while its failed counterparties do not, so success is partly taxed by the network. This cross-subsidy shrinks the reward for choosing a safe project. The paper's first main result, Proposition 1, says that in every network the banks' risk choices are strategic complements: when one bank takes more risk, every other bank wants to take more risk too. This mission formalizes Proposition 1.
A finite set of banks is given. For banks , is the face value of the debt that bank owes bank . Bank 's total interbank liability is , assumed positive, and is bank 's share of it. Bank also owes a deposit , which must be paid before its interbank debt.
Every bank picks a project from an interval . The project pays with probability and otherwise, independently across banks. Assumption 1: , is decreasing, and is concave. A standing assumption rules out systemic default: for every , so a bank whose project succeeds can always pay in full.
A state records which projects succeeded; bank 's cash flow is if and otherwise. A payment equilibrium solves
Bank 's profit is , and its expected profit is the sum over states weighted by . The best-response set is the set of maximizers of over , with the other banks' choices held fixed. The cross-subsidy is
bank 's expected net payment to the network when its own project succeeds.
For banks , profiles , and equal to except that :
This is the strong-set-order form of " is nondecreasing in ". It does not require the network to be regular or path-connected.
The regular-network step (I.3) (IA p. 7), that the maximizer of is increasing in , is also posed, as a theorem outside the milestone list.
Proposition 1 makes the risk-taking game supermodular. That property is what the rest of the paper relies on. It gives existence of equilibrium (Proposition 2) through Tarski's fixed-point theorem, it identifies least and greatest equilibria, and it lets the later comparative statics compare networks: complete against ring, size, central clearing, bailouts. Each of these results argues "the cross-subsidy rises, so equilibrium risk rises", and that step is Proposition 1 applied through Topkis's monotonicity theorem.
On the formal side, no clearing model is currently on the platform. This mission supplies one: the Eisenberg–Noe clearing system with a stochastic state, the greatest clearing vector, expected profits, and best responses. It also checks the paper's proof in the non-regular case. That proof splits on the states in which a bank survives its own failure, and one inequality in it is asserted without proof. The result is proved on paper; none of it has been machine-checked.
In a regular network a failed bank always defaults, and the argument reduces to two monotonicity facts: (I.3) and (I.4). In a non-regular network a failed bank can still earn a profit when enough of its debtors succeed. A riskier counterparty then has two opposite effects. It raises the cross-subsidy, which pushes toward risk, and it lowers the chance of being bailed out after one's own failure, which pushes away from risk. The proof must show that the first effect dominates in every network. It does so by partitioning the states according to whether bank survives its own failure, , and by showing that the states in that set contribute nothing to the cross-partial. This requires the clearing vector to be monotone in every bank's success and stable when a surviving bank's own state flips. It also needs an inequality, whenever , which the paper asserts without proof.
The naive route is to differentiate the first-order condition, as the paper does in (I.3). That route is not available: Assumption 1 gives neither differentiability of nor a unique maximizer.
Banks form a finite type, and states are Boolean vectors (true = success). All probabilities are finite products and all expectations are finite sums: no measure theory is involved. Sums over are written as sums over full states with fixed, weighted by the product over .
Conventions the Lean statements commit to:
AntitoneOn), which is the more general hypothesis.The goal is vacuous when a best-response set is empty. This is faithful, since presupposes a maximizer, and best responses exist whenever is continuous. A formalization that takes as an arbitrary solution under a uniqueness hypothesis, or as an sSup that could be junk, would trivialize the mission. The definition used here is shown, in a sorry-free check, to solve the clearing system.
Not posed: Lemma 1 (cited from Eisenberg–Noe), Proposition 2 and Corollary 1 (consequences of Proposition 1), and the later comparative statics (Propositions 3–9). Proposition 4, the comparison of complete and ring networks, is a separate mission of this series. Reusable contributions are welcome: monotonicity of greatest fixed points in a parameter, and a general Topkis-style argmax monotonicity on chains.
Reward-based crowdfunding and venture capital are two of the main sources of early-stage finance, and the empirical record on how they interact points both ways: some studies find that more crowdfunding activity is followed by more VC investment, others find the opposite. Hu, Jin and Keppo (SSRN 3512638; Management Science, 2024, doi:10.1287/mnsc.2022.00994) explain both signs with one firm-level model. A crowdfunding campaign has two roles: it raises a modest amount of money, and its outcome is a public signal about whether the product will succeed. Two VC firms with different priors compete for the deal, and the more optimistic one may prefer to wait for the campaign's outcome rather than invest at once.
The paper builds on earlier work on the informational value of crowdfunding for professional investors (Roma, Gal-Or and Chen, 2018; Babich, Marinesi and Tsoukalas, 2021) and on crowdfunding as a mechanism (Strausz, 2017). Its main result, Proposition 6, says exactly when the mere option of crowdfunding lowers the expected VC investment and when it raises it.
A startup needs at least to launch a project whose revenue is if it succeeds and if it fails, with ; each state has probability . It offers an investing VC firm an equity share . VC and VC believe the startup succeeds with probabilities , the startup itself with probability ; under a belief the expected revenue is , giving . A VC's valuation of the share is .
The investment level at which VC acquires the share is
where is the startup's negotiation power. VC never invests; it matters only as the startup's outside option.
Timeline. At VC may invest. If it does not, the startup runs a crowdfunding campaign with target , which produces a signal (success, collected) or (failure) with , where is the signal's accuracy. All parties update by Bayes' rule, with posteriors , and expected revenues , . At VC reconsiders: after the requirement is and the share is scaled to ; after both stay as they were. Assumption (I) requires .
VC compares its surplus from investing now, , with its expected surplus from waiting, ; the value of waiting is , and VC invests at when and . The paper shows that this happens exactly when , for an explicit threshold (Proposition 2). The startup chooses to maximize its expected payoff. Without crowdfunding it offers . With crowdfunding it offers or , according to the sign of its own value of waiting (Proposition 4). The expected VC investment level or is the level along VC's decisions, averaged over the signal under the unconditional belief .
Under the standing assumptions,
and if no share in draws an investment without crowdfunding, while .
Proposition 6 separates two populations of startups. For a startup that VC would fund anyway () and that prefers to induce a delay (), crowdfunding lowers expected investment: after success the requirement drops to , and after failure nobody invests. For a startup that VC would not fund on its prior (), crowdfunding creates investment that would otherwise not exist. If the startup prefers to keep the investment before the campaign (), the mere option of crowdfunding raises the level even though no campaign is run. Together these account for both signs of the empirical crowdfunding–VC relationship.
The paper's proofs are case analyses on closed forms. No part of this model has been machine-checked, and nothing on the platform models crowdfunding, VC competition or this signal structure. A formalization checks the seven-subcase comparison behind Proposition 2. It also pins down hypotheses the paper uses without stating them: nonnegative revenue, , , and . Each is needed, and each has an explicit counterexample without it.
The hard step is Proposition 2(i). Both and are piecewise linear in , with breakpoints where , , and cross their requirements. The claim that is a single up-ray needs the relative order of these breakpoints. Which closed form ( or ) is the threshold depends on where VC's post-signal valuation sits. The threshold is therefore not read off a single formula: each ordering of the breakpoints is a separate case, and the paper's proof runs through seven of them. Everything downstream, including the startup's optimum and the comparison of investment levels, needs the threshold to be exact.
Everything is elementary real arithmetic, with no measure theory. The parameters are a record of nine reals. "Expected" means the two-term average over and , with , the mixture implied by the signal accuracies (the paper does not print it). The posteriors, , , , , , and are the printed closed forms. VC's decisions, the startup's payoffs and the investment levels are defined from the surpluses and from . A VC that cannot meet the requirement after a signal gets surplus , as in the paper's proof (the printed would give it its valuation). VC's ties go to investing now and the startup's ties to . "Optimal" means a global maximizer over . "Raises" is weak where equality can occur (, ), and comparative statics in are weak.
Standing assumptions on every statement: , , , , , , . Added hypotheses:
Proposition 3(i)'s bound is stated as , because is allowed.
The goal compares investment levels computed from VC's decisions, not the paper's closed forms , , whose comparison is three lines of algebra. The threshold is not defined as the infimum of the shares at which VC invests, which would make Proposition 2(i) a tautology. The goal is stated at the paper's selected share , not at every maximizer.
Not formalized: Online Appendix A (the startup re-optimizes after the campaign), Appendix B (profitability for the startup and VC), and Appendix C (comparative statics in and ). Proofs of any milestone are welcome. The case analysis of Proposition 2(i), stated as lemmas about the piecewise-linear surpluses, would be reusable by every downstream item.
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.
Risk-sensitive decisions are often judged by a quantile of an outcome rather than by its mean: the 95th percentile of waiting time in a service system, the value-at-risk of a portfolio, the tail of a project's completion time. When the outcome is produced by a stochastic simulation or another black box, its distribution is unknown and only samples are available, so neither the quantile nor its gradient can be evaluated. Hu, Song and Fu (arXiv:2308.07607, Operations Research, 2025) propose a local search method for this problem that uses three samples per iteration in any dimension, and they prove that its iterates converge almost surely and at an explicit rate.
Earlier approaches estimate the quantile gradient by finite differences of order statistics, which requires sample sizes growing to infinity (Kibzun and Matveev 2012), or run a multi-timescale stochastic approximation driven by direct gradient estimators such as perturbation analysis or likelihood ratios (Hu, Peng, Zhang and Zhang 2022), which a black box does not provide. The present paper estimates the gradient from indicator differences along a simultaneous perturbation in the spirit of Spall's SPSA (1992), using a coordinate-wise variant (SDQO) as a baseline whose cost grows with the dimension , and, by its own account (p. 5), gives the first convergence rate for a three-timescale stochastic approximation scheme.
For every input a black box returns a random output with c.d.f. and density . For a fixed level the quantile function solves , and the problem is
where the parameter set is compact and convex, with each continuously differentiable and on . Under smoothness, .
Algorithm SPQO keeps a quantile estimate , a gradient estimate and the decision . With step sizes , perturbation sizes , the adaptive perturbation and a random direction with independent uniform signs,
with division by taken componentwise and the Euclidean projection onto . The timescales are separated by and .
The analysis rests on assumptions A1–A3 (local smoothness of and a lower bound on near the iterates; Rademacher directions; step-size conditions) and, for rates, B1–B3 (two-sided bounds on between and ; Lipschitz continuity of and in ; a lower bound on the smallest eigenvalue of the Hessian along the segments ). Section 4 uses step sizes , , , with exponents in .
Under A1–A3 and B1–B3, with the Section 4 step sizes, twice continuously differentiable and the unique equilibrium of the projected gradient ODE (25), lying in the interior of ,
The constants are left unspecified: the goal asserts the shape of the rate, which is what the paper proves.
The rate (27) makes the trade-off among the three timescales explicit: is the cost of tracking a moving quantile, the bias of the perturbation, and its noise. Balancing them selects the step-size exponents, and the special cases recover the rate of recursive quantile estimation and Spall's SPSA rate. The intermediate results (moment bounds for a gradient tracker with adaptive perturbation, an bias bound for an indicator-based SPSA estimator, and the weighted-sum estimate of Lemma 3) apply to other multi-timescale stochastic approximation schemes.
The theorem is proved in the paper; no machine-checked version exists. A formalization would check a rate argument for three coupled recursions, a setting in which hypotheses are easily lost: the paper's own proofs use a bound on that A1 does not list, and one step of the proof of Theorem 3 (display (29)) treats a conditional mean as an unconditional one. The statement survives both, as recorded in the formalization notes.
The three recursions are coupled in both directions. The gradient tracker is driven by indicator differences whose perturbation is itself scaled by , so the bias holds only once is known to be bounded, and boundedness must be shown with the adaptive . The natural first idea, analyzing each recursion with the slower ones frozen, gives convergence but not rates: the targets and move, and the error of each tracker must be bounded in mean square while the tracker it depends on is still converging. The rate also needs the almost-sure convergence of Theorem 1, which is an ODE-method argument for a projected, coupled scheme.
is EuclideanSpace ℝ (Fin d) with . The black box is a family of laws on , defined for every because SPQO samples outside . A run lives on a probability space with a general filtration; initial values are deterministic with ; the sampling model fixes the conditional law of each output given the past (and ), which covers independent sampling and common random numbers. Expectations are Lebesgue integrals in , and the bias of Lemma 2 is an explicit average over the sign vectors. is the paper's one-sided notion: a constant, depending on the instance and the run but not on , times the rate, for all large .
The following departures from the page are disclosed in every affected statement:
B3 is stated as the quadratic-form bound , equivalent to the eigenvalue bound for the symmetric Hessian. Theorem 1 is formalized only in its strictly convex clause.
Several trivializing formalizations are ruled out. Without the truncation of D1 no run satisfies A1(b) or B1, so the untruncated statement would be vacuous. No statement takes a Bochner expectation or conditional expectation of a possibly non-integrable quantity. Gradients and Hessians of are read only where is . No -constant may depend on .
A complete development needs stochastic approximation tools that Mathlib lacks: Robbins–Siegmund-type supermartingale convergence, the ODE method for projected recursions, and second-moment recursions for coupled trackers. These are reusable beyond this mission. Contributions are welcome for any milestone, and Lemma 3 is pure real analysis.