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?
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.
Shared bike and scooter systems (micromobility) must decide, every period, how to move vehicles between stations, which depleted vehicles to recharge, and how many vehicles to source from or return to a central warehouse. Customer trips redistribute the fleet in the meantime, and some vehicles come back with a depleted battery. For a realistic network, the exact Markov decision process has a state space that grows exponentially in the number of stations, so its optimal policy cannot be computed.
Akturk, Candogan and Gupta (Management Science, 2022; preprint SSRN 4155841) group stations into finitely many types and replace the stochastic network by a deterministic mean-field model that tracks, for each type, the fraction of stations holding each number of charged vehicles and the scaled stock of depleted vehicles. They show that the mean-field model is asymptotically exact as the number of stations grows (their Theorem 3.4), and they propose a control algorithm for it whose optimality gap they bound explicitly (their Theorem 4.2). This mission formalizes the second result.
There are station types, with stations of type and in total. A customer leaving a type- station returns the vehicle at a type- station with probability . Demand at a type- station has a law on with finite mean and variance; a returned vehicle is still charged with probability , and costs are discounted by .
The extended types are (the warehouse), (charged vehicles of each type) and (the depleted stock of each type). Moving one vehicle from extended type to costs , with .
An action is a post-rebalancing distribution: fractions of stations of type holding vehicles, supported on and summing to , and a scaled depleted stock . A state records the fractions for , the depleted stock , and two aggregates of the vehicles above , within the bounds of the paper's Appendix F.
The next state depends on the action only, through the transitions (F.1)–(F.5): demand removes vehicles from a station holding , and an independent Poisson number of charged vehicles arrives, with a rate (3.2) that is linear in the action's expected trips. Each period costs , where
The value function is the infimum over action sequences in of , where and .
The algorithm. Given and a transient horizon , solve the finite program (4.1): choose to minimize
then play and repeat forever ((4.2)–(4.3)). Call this policy and its discounted cost .
For every , every and every minimizer of (4.1),
where
Theorem 4.2 makes the algorithm a certified approximation scheme. It turns an infinite-horizon problem into a finite program of actions, and the loss from doing so decays geometrically in , uniformly over the initial state, with a constant that depends only on the rebalancing costs and the action bounds. For the transitions are affine, the program (4.1) becomes a linear program (the paper's Appendix G), and the sharper bound applies.
The result is proved in the paper (Appendix H), but not formalized anywhere. A formal proof combines a triangle inequality for an LP-valued cost, a dynamic-programming principle with attainment on a compact action set, and a fixed-point argument for a convex deterministic dynamic program. The paper has several small printed slips on this path (for example, Proposition H.10 states the constant without the factor that its proof produces); the formal statements fix the corrected reading.
The bound is not a truncation estimate. Cutting the discounted sum at gives a gap proportional to the per-period cost, not to . The comparison has to be made against an optimal action sequence, whose first actions are feasible for (4.1). After period , the optimal sequence and diverge, and the cost of that divergence must be controlled by the cost of moving between two actions, which requires:
The bound needs, in addition, a steady state of the controlled system (Proposition H.3), which rests on a fixed-point theorem for convex deterministic dynamic programs (Flynn 1979). The Bellman equation itself is not free: with defined as an infimum over sequences, attainment of the minimum needs continuity of , , the transition and on the compact action set.
Types are Fin ê (0-based) and the extended types are Fin (2ê+1) with chg e and dep e for the paper's and . Level vectors are functions that vanish outside their support. is the convolution of the demand law with the Poisson law, so and are independent, as the paper presupposes. is the infimum over the subtype of -valued sequences (p. 18 and Proposition F.3), and (3.6) is posed as a milestone rather than used as a definition. is formalized as printed on p. A-22. The policy cost is the discounted cost of , where is a hypothesis-given minimizer of (4.1). Everything is time-homogeneous and stated at .
Standing assumptions, as one predicate on the model: , , , with positive normalizers, , , finite second moments of , the cost assumption , , . Two additions are disclosed: , and , without which Lemma H.9 and the goal fail (the right-hand side could be negative).
Trivializing formalizations are excluded: ranges only over -valued sequences, the policy is tied to a minimizer of (4.1) and to no other objective, the flow value is an infimum over a nonempty set bounded below (warehouse routing is always feasible), and uses , , , with the paper's indexing and the factor .
Two general objects are separate definitions on which the model is built: a discounted deterministic dynamic program (trajectory, discounted cost, value as an infimum over admissible action sequences) and the uncapacitated transshipment LP on a complete digraph with free nodes. Both are reusable beyond this mission. A complete development further needs Poisson tail sums, subadditivity of the flow value, compactness of , a dynamic-programming principle and a fixed-point theorem for convex deterministic programs. Proofs of any milestone, and alternative arguments for the fixed point, are welcome.
Antitrust authorities review horizontal mergers by asking whether the merged firm will raise prices. A prior question is which mergers firms will choose to form at all. When several firms can merge, the identity of the partner matters: a large firm may absorb a small rival, or two small rivals may combine to face the large one. Wang, Wu, Tang and Dai (Management Science, 2024) study this partner-selection question in a price-competition model with two frictions common in retail and service markets: limited capacity of the small firms, and loyal segments, buyers who only buy from their own firm. Their main result says exactly which merger, if any, arises in equilibrium. Every step of its proof is an explicit comparison of closed-form profits, which makes the result a natural target for complete machine verification.
Three firms , , sell a homogeneous product at zero marginal cost. A unit mass of buyers each demand one unit and value it at the reservation price . Each firm has loyal buyers, ; the remaining buyers are switchers who buy from the cheapest firm. Firm is unconstrained; the small firms and each have capacity , with . Unserved buyers are rationed at random and spill over to the next cheapest firm.
The firms may stay independent, ; firm may merge with one small firm, the mixed merger ; or the two small firms may merge, the small merger . A merged entity pools capacities and loyal buyers. In each structure the firms play a price game whose equilibrium is in mixed strategies. The paper's Table A1 lists, for each structure, the lower bound of price support , , and the equilibrium profits , , , , , , as piecewise functions of built from
the numbers of spilled-over switchers. In the small merger each small firm receives half: .
A structure is an equilibrium structure when no firm or coalition gains by deviating. For this is
for it is
and the status quo is the equilibrium structure when neither condition (1) nor condition (2) holds.
With ,
The statement is an exact characterization: in the interval the mixed merger is an equilibrium structure and the small merger is not; outside it neither merger is.
The result separates the two forces of the model. Loyal buyers make a merged entity less aggressive in price, which is why no merger is profitable when capacity is ample. Limited capacity creates spillover demand, which a large firm captures by merging with a small rival but which two small firms do not capture by merging with each other. Proposition 3 says the second force wins exactly on and that the small merger never forms. This answers one of the paper's opening questions, whether two capacity-constrained small firms merge to compete with a large one: in this model they do not.
The paper proves the result by hand, over eight regions of the parameter plane (its Figure A1). The comparisons involve rational functions whose denominators are positive only under the region's constraints, and threshold curves with square roots. A machine-checked proof certifies the region bookkeeping. No formalization of this result exists.
Each single comparison is elementary algebra; the difficulty is the case structure. Table A1 has four rows in whose boundaries (, , ) differ per column, and three of its cells are maxima whose active branch changes along the curves , , . Root-location facts such as and are needed to know which row a region lies in. One inclusion the proof uses is only shown in the paper's figure: on , where condition (2a) holds, one needs in order to conclude that (2b) fails. At the region boundaries and several of the proof's strict inequalities are equalities.
Everything is stated over the reals in the namespace EndogMerger.SymLoyal. All definitions take explicit parameters (α k r : ℝ). The standing assumptions , , , and or as each statement requires, are hypotheses of each theorem. Relative to the paper, replaces (every region of the analysis has ), and is made explicit. Firm 's capacity does not enter Table A1 and is not modelled. The split of between and is left unspecified, as in the paper.
Table A1 is the definition. The profits and lower bounds are defined by Table A1's piecewise expressions, row by row, with max where the table has a maximum. The paper's derivation of these values as equilibrium outcomes of a mixed-strategy price game with random rationing is not formalized; Section 6 of the paper itself obtains Proposition 3 from the Table A1 profits. The paper's PDF page numbers are cited throughout; the appendix restarts its printed numbering, so printed page numbers are not used.
Three trivializing formalizations are ruled out. The profits are not defined by the closed forms of Lemmas 3–5, which would make those lemmas definitional. The equilibrium predicate for requires that neither condition (1) nor condition (2) holds, so the goal includes the claim that the small merger is never an equilibrium. The thresholds and are not defined by the paper's equation , which Real.sqrt satisfies for every with a negative radicand. Instead , and is a parameter pinned as the root in of .
Where the paper's proof claims a strict inequality on a closed region whose boundary gives equality, the milestone states it on the open region, and its Formalization Note says so.
No library beyond Mathlib's real arithmetic and Real.sqrt is needed. Lemmas about the threshold curves, for example that lies in , are reusable across milestones. Contributions of intermediate lemmas, including the region inclusion , are welcome.
Ride-hailing platforms are expected to add autonomous vehicles (AVs) to fleets of human-driven vehicles (HVs). A common expectation is that AVs, by removing the driver's wage, will make rides cheaper. Lian and van Ryzin (SSRN 3716491; published in Management Science, 2025, DOI 10.1287/mnsc.2020.03112) show that the answer depends on the market configuration. Two forces act on the price. A labor-cost effect: AVs displace human drivers, and the remaining drivers need lower pay. A density effect: pickup times fall as more idle cars are close to riders, so a larger fleet on one dispatch platform is more efficient per ride. When AVs and HVs are dispatched by independent platforms, the HV platform becomes thinner and loses density, and the price can rise.
This mission formalizes Proposition 4 of the paper, the result that makes this precise: under an explicit upper bound on the slope of the HV labor supply curve, coexistence of AVs and HVs on independent platforms strictly raises the price above the pure human-driver market. The version used is the authors' SSRN working paper of 23 August 2023; all numbering refers to it.
A market has six parameters. Riders wait for a pickup for an expected time , where is the number of open cars (idle vehicles), , and is the ETA elasticity; means there is a density effect. A ride lasts . Rider values for a ride-hour are uniform on . In a demand scenario with potential demand mass , the inverse demand at a demand rate (ride-hours per hour) is
A fleet of human drivers participates only if each earns its reservation earnings per hour, with and ; means HV supply is finitely elastic.
By Little's law and an optimization over the number of open cars, the minimal fleet that can serve a demand rate is
and the fleet's on-trip utilization is .
Pure-HV market. Revenue is and the minimal labor cost is . A demand rate is an equilibrium when they are equal; it is stable when no small perturbation has cost above revenue below and revenue above cost above . The maximal stable equilibrium is the largest stable equilibrium. At the price equals , the labor cost per ride-hour.
Independent platform market. AVs serve on their own platform; HVs serve on theirs, with their own minimal fleet . The market price is , and HVs are in equilibrium when
Assume , and
Then every coexistence equilibrium of the independent platform market satisfies
Proposition 4 is the step that separates the two dispatch designs in the paper's main comparison (Proposition 3). On a common platform AVs always lower prices; on independent platforms, under (19), every scenario in which AVs and HVs coexist has a strictly higher price, for a monopoly AV supplier and for perfectly competitive AVs alike. The condition (19) is explicit in the primitives, so it says when fragmentation of dispatch harms riders: when the HV supply is elastic (small ) or the pure-HV demand is low.
The result is proved in the paper, in Appendix D.3. It has no machine-checked proof. The mission produces one, together with reusable facts about the square-root-law-type fleet function : its log-derivative bounds and the sign of the derivative of the labor cost per ride-hour.
The two steps are of different kinds. The comparison rests on the defining property of the maximal stable equilibrium: that revenue falls short of cost at every demand above . That property is not part of the definition of the maximal stable equilibrium. A first idea, comparing revenues pointwise at and , fails without it, because revenue minus cost need not be monotone.
The second step is a sign computation of the derivative of , involving real powers and . The paper's condition is pointwise, while Item 1 needs monotonicity on a whole interval.
All quantities are real numbers; fleet sizes and demand rates are continuous, as in the paper. Real powers are Mathlib's Real.rpow. Statements about the ratio are made only at , where it is differentiable; Lean's value at is a junk . Derivatives are Mathlib's deriv.
Standing assumptions: , (and where the page assumes a density effect), , , , (and where the page assumes finite elasticity). Pinned choices:
A coexistence equilibrium with , or a vacuous one with , is excluded explicitly; with the goal would be false, and dropping positivity of would make (48) trivially satisfiable.
Everything is defined locally in one definition file (the shared market model, repeated in each mission of this series, plus the ratio, the bound and coexistence). Contributions of general lemmas on derivatives of and on largest stable roots of continuous functions are reusable.
Data brokers sell two kinds of products to marketers. A marketing list supplies the contacts a marketer needs in order to act at all; a data append enriches a list the marketer already holds. In both cases the broker can also choose how informative its accompanying analytics are, and it can price a menu of plans of different informativeness to marketers whose costs of acting it cannot observe. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how such a seller should design this menu, and in particular when it should sell more or less information than would be efficient.
The paper first works with a two-point value distribution (Sections 2–3) and then, in Section 4, with a general information structure in which informativeness is ordered by the rotation order of the distribution of the posterior mean (Johnson and Myatt 2006). This mission formalizes the marketing-list result of Section 4.1: Proposition 4 (comparative statics of the efficient informativeness) and Proposition 5 (the optimal screening menu). It is the third mission of a four-mission series on the paper; the first two treat the two-point model, the fourth treats data appends under the rotation order.
A marketer's value from targeting a consumer is unknown. The seller supplies a signal of informativeness . The marketer's posterior mean has cumulative distribution function on a support , with a strictly positive density . Bayesian updating keeps the mean fixed: for every , where is the prior mean. The rotation order (9) requires a point such that
Raising moves probability mass from the middle of the distribution to its tails.
The seller incurs a selling cost , increasing, with . A marketer's targeting cost is with probability and with probability , with . A marketer with cost targets exactly when , so informativeness is worth
With observable costs (the benchmark), the seller sells to type the informativeness maximizing (12), ; a maximizer is an efficient level . With private costs, the seller offers a menu of plans , , with fees . A type- marketer choosing plan gets (13). The seller maximizes subject to individual rationality and incentive compatibility (problem (6)). Its solutions are written .
In general , and if (resp. ), then
The first identity says that the low-cost marketer, the "high type" of the screening problem, receives the efficient informativeness. The second says that the high-cost marketer's informativeness is distorted, upward when both costs lie below the rotation point and downward when both lie above it. Both are stated for every optimal menu and every efficient level.
Proposition 4 states that the value of information to a marketer is non-monotone in the cost of acting: it is largest for costs near the rotation point , where the targeting decision is hardest. Proposition 5 turns this into a pricing rule. In the two-point model the direction of the distortion depends only on the prior (Proposition 2, or ). Under the rotation order it depends on where the costs lie relative to , so a seller facing marketers with low costs over-supplies information to its less profitable segment, and one facing high costs under-supplies it. The comparison with the two-point model (pp. 17–18 of the manuscript) connects the two settings through the single-crossing point of the posterior-mean distributions.
The results are proved in the paper, through integration by parts, signs of derivatives and Topkis's monotonicity theorem. None of them is formalized. Formalizing them checks the reduction of the screening problem, which the paper performs by analogy with the two-point model, including the constraints it drops without comment. It also produces a reusable treatment of rotation-ordered distribution families on an interval. Topkis's Theorem 2.8.4 is already proved on the platform and is part of this mission as a reference.
The obvious argument has two gaps. The first is the reduction (14). The paper substitutes the binding and constraints and drops , and . That the dropped constraints hold at a solution of (14) is not shown in the paper. The second gap is strictness: Topkis's theorem compares maximizers weakly. The strict inequalities require showing that efficient levels are interior and that the first-order conditions differ there. This uses the footnote-5 behaviour of at the endpoints and the mean-preserving property (10), which follows from (9) and the constancy of the mean.
The model is one Lean structure, SellingData.ListsRotation.Model, with real parameters and its standing assumptions as fields. The committed conventions are:
Two further hypotheses are pinned, and only on the statements that need strictness or differentiation under the integral sign:
Optimal menus and efficient levels are sets of maximizers, not chosen maximizers, because need not be convex. "" is the equality of the set of low-cost plans of optimal menus with the set of efficient levels. The goal is stated for the screening problem (6) itself, with all four constraints and nonnegative fees. Defining the optimal menu through (14), or efficient levels through a first-order condition, would make half of the goal a restatement of a milestone, and is ruled out. As on the page, is stated with no condition on the position of the costs relative to ; only the comparison of with carries the two cost ranges. A sorry-free instance shows that the model's hypotheses are jointly satisfiable: , , .
Contributions are welcome on the integration-by-parts and differentiation-under-the-integral lemmas for families of distributions on an interval, which are reusable beyond this paper, and on any milestone in any order.
Optimal control of partial differential equations under uncertainty asks for a single deterministic control that performs well when the data of the PDE are random. When a constraint on the state must hold, the modeller has to decide how strictly: with high probability (a probabilistic constraint), for almost every realization (an almost-sure constraint), or for every realization in a support set (a robust constraint). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for all three forms on a common model problem. This mission covers §3.1 of that paper, the almost-sure case.
Almost-sure state constraints are the natural model when a bound (a temperature, a stress, a concentration) must never be violated, and they appear throughout risk-averse PDE-constrained optimization (Geiersbach and Wollner, SIAM J. Optim. 2021; Geiersbach and Hintermüller, ESAIM:COCV 2022). Their difficulty is functional-analytic: the constraint lives in , a space whose dual is not a function space, so Lagrange multipliers are a priori only finitely additive objects.
Let , , be open, bounded and of class S: there are and with for all and . For the Dirichlet problem in , on has a unique weak solution ; the solution map is a continuous linear operator .
Let be a probability space and a random source. For a control the random state solves , on . With the embedding of into constant elements of and , the control-to-state operator is and the constraint map is , where is the constant function . The problem is
with the cone and its polar . The cost is convex and continuously Fréchet differentiable.
For a separable Banach space , a functional is absolutely continuous if for a weakly measurable with (the set of such ), and singular if it vanishes on every that vanishes on some , for a decreasing sequence of events with (the set ).
Under the constraint qualification , solves (51) if and only if there are , and a state with
The result. Lemma 3.7 gives a multiplier in the dual of , which cannot be evaluated scenario by scenario. Theorem 3.10 shows that, for this problem, the multiplier consists of an honest random variable (a random signed measure on ) satisfying sign and complementarity conditions for almost every realization, plus a singular remainder. This is the form needed to write adjoint equations and to design discretizations and algorithms (Proposition 3.12 of the paper). As Remark 3.11 notes, the derivation does not require reflexivity of the state space, unlike earlier work on -constraints.
Formalizing it. The paper's argument is complete, but it rests on two cited results: the regularity theory behind Lemma 1.2/3.6 (Stampacchia-type continuity of weak solutions on class-S domains, Kinderlehrer–Stampacchia) and the Ioffe–Levin decomposition of (Ioffe–Levin, Appendix 1, Theorem 3, and Levin 1974). Neither is in Mathlib. A formal development produces machine-checked versions of both, of a Robinson-type KKT theorem in Banach spaces, and of the multiplier refinement itself. None of these results has a machine-checked proof as far as the platform's catalog shows.
The obvious route is to apply the Riesz representation pointwise in . It fails: contains purely finitely additive functionals that are not given by any integrand, so has no density in general. The decomposition theorem isolates them, and the proof of Theorem 3.10 must then show that the sign condition and the complementarity condition pass to each part separately. The step from for all to " for almost every , simultaneously for all nonnegative test functions" requires the separability of ; a version with a null set depending on the test function is weaker and is not the statement. Lemma 3.6 needs -regularity of weak solutions, which is where class S and enter.
is EuclideanSpace ℝ (Fin d). is Lp ℝ 2 (volume.restrict D) and is Lp X ⊤ P; their elements are a.e. classes, so every pointwise statement in is stated -a.s. is C(closure D, ℝ) with [CompactSpace (closure D)] as an instance argument (implied by boundedness). Weak derivatives use the published HunterPDE.Shared.HasWeakDeriv; a weak solution in is encoded as continuity on , zero boundary values, weak gradient and the weak form. is a hypothesis: a continuous linear map whose values are weak solutions. " a.e. in " for a function continuous on is read as " on "; "" as positivity of the functional. "Solution of (51)" is a global minimizer. (56a) is stated applied to every direction .
Trivializing formalizations are ruled out: the state operator is tied to the PDE, not an arbitrary bounded operator; the multipliers carry their sign and complementarity conditions; absolutely continuous functionals require a weakly measurable, integrable density; singular functionals are concentrated on a decreasing sequence of events of vanishing probability, not merely "not absolutely continuous"; optimality is global.
Needed infrastructure: Lax–Milgram on and continuity of weak solutions (Lemma 3.6); a KKT theorem under Robinson's constraint qualification (Lemma 3.7); the Yosida–Hewitt decomposition for finitely additive measures and a weak*-measurable representation of (Theorem 3.9). The decomposition theorem is reusable far beyond this mission; contributions toward any of these are welcome.
Many service systems do not receive random, memoryless traffic: customers are given appointments. Outpatient clinics, airport runways, container terminals and delivery slots all schedule arrivals on a regular grid, and the actual arrival deviates from the appointment by a random lateness or earliness. A queue fed by such scheduled traffic is a basic model for these systems, going back to Winsten (1959) and Mercer (1960, 1973), and Chen and Zhao (1997) used it with deterministic service times to model aircraft landings, proving stability under bounded perturbations.
Classical queueing theory says that a single-server queue fed by stationary traffic is stable when the mean work brought per unit time is below the service rate, and unstable when it is above (Loynes 1962). The boundary case, critical loading, is unstable for renewal traffic with non-degenerate interarrival times: the workload grows like . Araman and Glynn ask what happens at critical loading when the traffic is scheduled and every customer brings the same amount of work, and show that the answer depends only on the right tail of the arrival perturbations.
Timeline. Winsten (1959) and Mercer (1960, 1973) analysed queues with scheduled arrivals and obtained waiting-time distributions in implicit form. Loynes (1962) proved the stability dichotomy for stationary input. Kingman (1962) showed that the heavy-traffic limit of the S/G/1 queue coincides with that of D/G/1 when perturbations are positive with finite mean. Chen and Zhao (1997) studied the S/D/1 queue with bounded perturbations. Araman and Glynn (2012) obtained a fractional-Brownian functional limit for scheduled traffic with infinite-mean perturbations, and Araman, Chen, Glynn and Xia (2022) showed that S/D/1 queues with Pareto-like perturbations behave unlike D/D/1 and G/D/1 queues. The present note (arXiv 2022; Operations Research technical note, 2025) settles stability at critical loading.
Fix a probability space and a scheduling interval . Customer is scheduled at time . Its perturbation is a real random variable, and the are independent and identically distributed with . A uniform shift , uniform on and independent of , makes the arrival process stationary. Customer arrives at
and for the arrival count is , so .
A single server works at unit rate and every customer brings exactly units of work (the S/D/1 queue; "D" for deterministic service ). Since one customer is scheduled per time units, the queue is critically loaded. The system is empty at time , and the workload at time is
The proof runs in reversed time. With reversed arrival times , let
Write . " is a bounded random variable" means that almost surely for some constant .
The statement makes no assumption beyond the standing model. In particular the left tail of is arbitrary (only ).
Here count reversed arrivals in of customers and ; are the counts , , and .
The result. Theorem 1 shows that, unlike renewal traffic, scheduled traffic can keep a critically loaded queue stable, and it identifies exactly when: only late arrivals (the right tail of ) can destabilise the queue, while arbitrarily early arrivals cannot. For appointment systems this says that a server whose capacity exactly matches the schedule has a finite stationary backlog precisely when lateness is bounded, so tardiness, not earliness, determines whether waiting times stay bounded. It complements Corollary 1 of the same note, a diffusion limit for random service times at critical loading.
Formalizing it. The theorem is proved in the paper, but its proof contains several misprints: an identity that omits a term and has an infinite summand, a bound with a wrong constant, a sign error in , a false inequality , and a conditional Borel–Cantelli step applied to non-adapted events. The milestones of this mission state the corrected inequalities, each checked by hand on small instances. A machine-checked proof would settle the argument. No part of it is formalized anywhere at present.
The forward workload is not monotone in , so its convergence cannot be read off from its paths; the proof needs the time reversal to a monotone running maximum , and the reversal of a perturbed lattice requires its stationarity under the uniform shift. In the unstable direction the obvious first idea is to show that is large for a fixed large . That fails: for each fixed the overshoot is a tight random variable. Large values occur only along random times at which many customers just after are very late while few customers just before are very early, and producing infinitely many such times needs an ergodic or Borel–Cantelli argument over a dependent stationary sequence. Mathlib has no pointwise ergodic theorem and no conditional Borel–Cantelli lemma, so this step needs new infrastructure.
All declarations live in the namespace ScheduledQueue.Stability. The standing model is a bundle ScheduledInput P ξ U (measurable, i.i.d. via iIndepFun and IdentDistrib, Integrable (ξ 0), HasLaw U uniform on , and independence of U from the whole sequence). Customers are indexed by ℤ, time by ℝ, and is the atTop filter on ℝ. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is a probability measure on .
Conventions that differ from the printed page:
Every count used inside a pointwise inequality is an extended natural number (Set.encard), so that statements such as " a.s." are not satisfied by the junk value of an infinite Set.ncard. The goal's limit is a probability measure on , not on the extended reals, because there "" would also count as convergence. "Bounded" means bounded almost surely, not pointwise. Measurability of is part of the conclusion of the "if" direction, not a hypothesis.
A complete development needs the stationarity and time reversal of the perturbed lattice point process, tail-sum bounds , a pointwise ergodic theorem for i.i.d. shifts (or a Lévy-type Borel–Cantelli argument), and measurability of suprema over intervals. The ergodic theorem and the reversal lemma are reusable well beyond this mission. Proofs of individual milestones, in any order, are welcome.
Financial firms owe each other money. When some firms cannot meet their obligations, the payments that actually clear in the network are a fixed point: what a firm can pay depends on what it receives, which depends on what others can pay. Eisenberg and Noe (Management Science, 2001) introduced this clearing model under a fixed pro-rata payment rule. Later work asked what happens when firms choose how to pay their creditors, which turns the clearing problem into a game.
Bertschinger, Hoefer and Schmand (arXiv:1908.01714v3; Mathematics of Operations Research, 2025) study this game in an abstract form, the flow allocation game. Each node of a directed network receives a fixed external supply plus whatever flows in, and decides how to split its total supply among its outgoing edges, subject to edge capacities. Each node wants to maximize its own total outflow (its payments, which in the financial reading is what keeps it solvent). The paper's first main result is that, when strategies rank single units of flow, there is always a strong equilibrium, stable against every coalition, which is at the same time socially optimal for the total flow.
Timeline:
A flow allocation game consists of a finite directed multigraph , a fixed supply at each node and a capacity on each edge. and are the outgoing and incoming edges of , and .
Every node is a player. A strategy profile assigns to each edge an allocation function : when the tail of has total supply , it forwards units on . The profile is unit-ranking if for all , , : (1); (2); (no fraud, (3)); and each is non-decreasing (5). Equivalently, every node ranks the single units of its outgoing capacity.
A flow gives node the total supply , and is feasible for if on every edge (4). The clearing state of is the coordinatewise supremum of the feasible flows. Player 's utility is , and the total flow is .
A unit-ranking profile is a strong equilibrium if no non-empty coalition has a joint deviation such that is unit-ranking and for all .
The circulation network adds a node , an uncapacitated edge and an edge of capacity for every . An optimal circulation maximizes the total flow over all edges of .
For every flow-monotone (if then ) there is a strong equilibrium maximizing over all unit-ranking profiles.
Strong equilibria rarely exist in network games, and when they do they are usually not efficient. Theorem 9 gives both at once: every unit-ranking game has a strong equilibrium, and one of them maximizes the total flow, so the price of stability for is . Corollary 12 extends this to every flow-monotone welfare function, including egalitarian welfare, Nash social welfare and the number of solvent firms. In the financial reading, a coalition of firms cannot jointly reorder its payments to make every member better off, and the stable payment pattern can be chosen to clear the largest possible volume of debt.
The results are proved in the paper and, to our knowledge, have no machine-checked proof. Formalizing them yields a reusable Lean development of clearing states (the Knaster–Tarski structure of feasible flows), the circulation representation of feasible flows, and integral maximum circulations with a cycle-augmentation argument. The second mission of this series (strong price of anarchy, Theorem 16) builds on the same model.
The obvious argument fails at the deviation step. After a coalition deviates, the clearing state of the new profile is an implicit object: the greatest fixed point of a map that mixes the deviators' new strategies with everyone else's old ones. Nothing ties it pointwise to the optimal circulation, and comparing utilities alone gives no contradiction, because a deviator's gain can be paid for by flow that appears elsewhere in the network. The increase of flow has to be traced through deviators and non-deviators alike, and the two kinds of node obey different constraints.
A second difficulty is that the threshold profile built from an optimal circulation has clearing state exactly . The clearing state is a supremum over all feasible flows, so it is not enough that is feasible. The claim depends on optimality: for a circulation that is not optimal it is false, as a two-node cycle carrying one unit on edges of capacity two already shows.
All data are natural numbers: supplies, capacities, strategies and flows, as the paper prescribes for unit-ranking games (p. 13). The graph is a finite type of edges with tail and head maps, so multi-edges and self-loops are allowed. A profile is one function on edges. The clearing state is the coordinatewise sSup in ; the definition does not assume that the supremum is a feasible flow, which is milestone 1. Optimal circulations are optimal among integral circulations, which the paper justifies by integrality of capacities (p. 23). Natural-number subtraction is used only where it is the page's .
Coalitions are non-empty. With the condition "every member strictly gains" holds vacuously and no profile would be a strong equilibrium; the paper reads it the same way (Proposition 4, Proposition 17). Deviations must again be unit-ranking profiles; the broader deviations of Remark 10 are not formalized. The maximization in the goal ranges over all unit-ranking profiles, not over threshold-ranking ones. A goal maximizing only over threshold profiles, or one that drops the optimality conjunct, is a strictly weaker theorem and is ruled out.
Out of scope: the second sentence of Theorem 9 (polynomial-time computation and polynomial-space representation) and the polynomial-space sentence of Corollary 12. Both need a model of computation. The threshold representation behind them is milestone 4.
A complete development needs: Knaster–Tarski on a finite product of intervals (Mathlib's OrderHom fixed-point lattice), flow conservation bookkeeping on finite multigraphs, existence of integral optimal circulations, and extraction of a cycle from an infinite backward walk in a finite graph. The last two are reusable beyond this mission. Proofs of any milestone, and sorry-free lemmas about clearing states, are welcome.
Two-sided platforms (ride hailing, delivery, freelancing, logistics) collect demand and supply requests over a matching cycle and then clear them with an optimization problem. When such a platform runs an experiment, treated and control units compete for the same supply, so the outcome of one unit depends on the treatment of others. Interference bias of this kind is the subject of Bright, Delarue and Lobel, Reducing Marketplace Interference Bias Via Shadow Prices (arXiv:2205.02274v4; Management Science, 2025). Their analysis of estimators, including the shadow-price estimator built from linear-programming duals, is carried out in a deterministic fluid limit. Theorem 1 of the paper justifies that step: as the market becomes dense, the expected matching value per unit of density converges to the optimal value of a deterministic linear program with the arrival rates as inputs.
The same kind of statement, the expected value of a random linear program converging to the value of the program at the mean data, is also used in network revenue management and in stochastic matching, where fluid linear programs serve as benchmarks.
Network. There are demand types and supply types. A directed network has one demand node per demand type (a sink), one supply node per supply type (a source) and a finite set of intermediate nodes. Every arc carries a value and a capacity .
Matching program. For a density , demand vector and supply vector , is the maximum of over flows with inflow at most at , outflow at most at , flow balance at every intermediate node and (display (2), p. 7). Write . Without intermediate nodes this is a capacitated bipartite transportation problem.
Random counts. Demand units of type arrive at rate and supply units of type at rate . At density the numbers of units collected in one cycle are independent Poisson counts
Treatment effect. If a treatment changes the demand rates from to (with ), the global treatment effect at density is (Definition 1, p. 8).
for every network, every and every , along integer densities . No rate of convergence and no constant is fixed.
Theorem 1 is the bridge between the paper's stochastic model and its deterministic analysis. Corollary 1 follows from it and identifies the estimand . Every fluid-limit result of the paper is stated about this deterministic quantity: that the RCT estimator overestimates the treatment effect (Theorem 2), and that in a symmetric experiment the shadow-price estimator is no more biased than the RCT estimator (Theorem 4). Without Theorem 1 those results describe a linear program, not the experiment.
The result is proved in the paper (Appendix C.1, pp. 37–39). As far as a search of the Prove2Me catalogue shows, it has not been formalized: the catalogue has fluid limits of queueing networks and several Poisson concentration bounds, but no law of large numbers for the value of a random network-flow program. A formal development would provide a reusable definition of the capacitated network-flow program with supply and demand bounds, its scaling identity, and an integrability tool for suprema of scaled Poisson counts. The two other missions of this series, on the shadow-price estimator in the fluid limit and in finite samples, use the same network program.
The obvious argument is: and , is continuous, so the expectations converge. Each step needs care.
Representation.
Fin nd and supply types Fin ns; Lean index is the paper's type .E and intermediate-node type I. Each arc's tail is a supply or intermediate node and its head is a demand or intermediate node, which builds in the source/sink structure. Values are real and capacities nonnegative.Probability.
Ruled out. A trivializing formalization is excluded: the expectation is taken against the Poisson laws with means and , with the factor inside the expectation, not against point masses at the rates or in the rescaled form . No hypothesis beyond is imposed.
Not stated.
The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed in each item's Formalization Note.
Infrastructure needed.
The network-program definition and the Poisson tail bound are reusable beyond this mission. Contributions toward any of these are welcome.
Global sensitivity analysis asks how much of the uncertainty in the output of a model, a simulator or a learned predictor is attributable to an input . A standard way to answer is to compare the law of with its law after is revealed, and to average that discrepancy over . Variance-based indices (Sobol' 1993; Wagner 1995) compare conditional and unconditional means. Density-based and distribution-based indices compare whole distributions. Rényi's postulates for measures of dependence ask, among other things, that such an index vanish exactly under independence (zero-independence) and reach its maximum exactly when is a function of (max-functionality, Postulate E). Variance-based indices fail the first postulate, because the conditional mean can be constant while the conditional law moves.
Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose indices in which the discrepancy is an optimal transport cost. The squared 2-Wasserstein case is the numerator of the Wasserstein correlation coefficient of Wiesel (2022), whose Theorem 2.2 gives max-functionality for that coefficient. The paper extends max-functionality to general continuous costs, through a strict-convexity property of the transport cost on Dirac masses (Lemma 4). This mission formalizes that result, Theorem 5, together with the zero-independence property, Proposition 3.
Let be a probability space and , Polish spaces with their Borel -algebras. The input and the output are measurable, with laws and .
A cost is a continuous function with if and only if . It need not be symmetric, a metric, or finite. For probability measures on , a coupling is a probability measure on with marginals and , and the optimal transport cost is
For a sub--algebra of the Borel sets of , a version of the conditional distribution of given is a Markov kernel that is -measurable in and satisfies for and Borel . The OT-based sensitivity measure of Definition 1 is
written when is the full Borel -algebra. The candidate maximum is
with an independent copy of ; for it equals twice the total variance of .
If , then for every sub--algebra and every version of the conditional distribution,
and
The steps of the paper's proof, in order:
The result. Together, Proposition 3 and Theorem 5 place on a scale from (no information about in ) to (complete information), so the ratio is a normalized measure of association. This normalization is what lets practitioners rank inputs of a simulator or features of a model on a common scale. The result covers all continuous costs vanishing exactly on the diagonal, including the powers of a metric that give the Wasserstein indices, and arbitrary sub--algebras , which model partial information about (for example the information carried by a function ).
Formalizing it. The theorem is proved in the paper; the work here is to formalize the known proof. As far as is known, no machine-checked version of this result or of Wiesel's Wasserstein-correlation theorem exists. Along the way the development needs facts about optimal transport with extended-real costs that are not in Mathlib: the product-coupling bound, the transport cost to a Dirac mass, convexity and lower semicontinuity of , and cyclical monotonicity of optimal plans.
The inequality and the "functional dependence ⇒ equality" direction are direct computations with the product coupling and with Dirac conditional laws. The converse is the hard direction. Equality of the integrals gives only the pointwise equality (63) almost everywhere, and the step from there to " is a Dirac mass" needs strict convexity of . Strict convexity fails for general measures: is affine along many segments. It holds only between Dirac masses at distinct points of (Lemma 4), and even there it fails when the costs involved are infinite. A non-Dirac conditional law is not a two-point mixture, so the strict inequality must be carried over to general measures with an integrand that takes values in . The last step, building an -measurable from the conditional laws, is measure-theoretic bookkeeping that is easy to get wrong.
ℝ≥0∞), so is allowed as on the page, and integrals are lower Lebesgue integrals.RWPI.SqrtLasso.transportCost. Its first argument is the marginal , and the cost is evaluated as with .IsCondDistrib is admissible, and every theorem quantifies over all versions and over all sub--algebras .Firms that sell to the same customers over time learn who bought from whom. Behavior-based pricing (BBP) — charging a firm's own past customers one price and the rival's past customers another — has been studied since Fudenberg and Tirole (2000) and Villas-Boas (1999). A second instrument is the disclosure of product quality: free samples, demonstrations and trial versions reveal the quality of a new product, at a cost per customer reached. With purchase histories, a firm can disclose differently to its own customers and to the rival's: behavior-based disclosure (BBD). The classical disclosure model is Jovanovic (1982), in which costly disclosure leads a firm to reveal quality only above a threshold.
Zhang and Li (2025) combine the two instruments in a two-period Hotelling duopoly and compare BBD with uniform disclosure. Their Proposition 1 shows that BBD always raises second-period profits; this mission is about the whole game, where the answer depends on the disclosure cost.
A unit mass of customers is uniformly distributed on ; firm A is at , firm B at , the transportation cost is , marginal costs are and the market is fully covered.
Period 1. The firms charge prices . The first-period purchase splits the line at : A's old customers are (A's turf), B's are (B's turf).
Period 2. Each firm launches a new product of quality , with independent and uniform on . A firm discloses its quality to a segment iff it exceeds a disclosure threshold ; disclosing costs per customer reached. A segment that sees no disclosure believes the quality is . Under uniform disclosure each firm has one threshold for the whole line; under BBD it has for its own customers and for the rival's. On each turf the two firms then play a price game (A charges and B charges on A's turf; and on B's turf), and customers stay or switch according to their beliefs and prices.
Forward-looking customers. The share is the location of the marginal consumer, who compares the two first-period options including the expected second-period surplus of staying or switching ((6) for uniform disclosure, (15) for BBD):
Two-period profits (8) are and , with the ex ante second-period profit at share . A symmetric subgame-perfect equilibrium is a common first-period price together with a second-period equilibrium at every share and a consistent share at every price pair, such that neither firm gains from any other nonnegative first-period price. Its total profits are .
The standing assumption is (p. 8515).
There is a cutoff such that for every , symmetric subgame-perfect equilibria exist under both regimes and, for any two of them,
The value of is left unfixed, as in the paper.
with share . 4. Table 1, total profits, both regimes, in closed form. 5. Proposition 2: a cutoff across which the comparison of first-period prices and profits reverses.
Proposition 3(a) is the paper's answer to the managerial question in its title. BBD lets a firm disclose to its own customers more often than to the rival's (retention-focused disclosure), which improves the efficiency of disclosure and raises second-period profits. In the first period, however, BBD changes how hard firms compete for customers, and when disclosure is cheap the first-period loss dominates. The result locates the sign change of the total effect at a single cutoff, and together with Proposition 2 () it separates three regimes of : total profits fall, total profits rise despite lower first-period profits, and both rise.
None of these results is formalized anywhere. The paper's proofs are in an Online Appendix and its displayed formulas are the end points of long computations. A complete development would produce:
The model nests three equilibrium notions: a clamped price game on each turf, threshold disclosure as a best response to the rival and to the induced beliefs, and first-period pricing with forward-looking customers. The first-order condition behind (9) and (17) involves the derivative of in , and every threshold, including the rival's, moves with ; treating the rival's thresholds as fixed gives a wrong price.
The symmetric first-order condition alone does not settle the equilibrium. A deviation in first-period price can push the share outside the region where all second-period prices are interior, into the corner regions 2 and 3 of Lemma 1/2, where the second-period profit has a different form. The paper checks these deviations only in its Online Appendix.
The final comparison is a sign analysis of an expression with three different square roots on . The difference of total profits is small throughout: for example, about at and at .
A multiclass queueing network routes jobs of several classes through shared stations. Whether such a network is stable depends on the scheduling policy and not only on the load: the Lu–Kumar and Rybko–Stolyar examples are unstable under a static-priority policy with every station loaded below capacity (Bramson, Stability of Queueing Networks, 2008). A network operator who does not control, or does not know, the policy in use therefore wants robust stability: stability under every policy of a given family.
Zhao, Gurvich and Hasenbein (arXiv:2303.17746v3) study robust stability over the family of queue-ratio policies, which steer each station's workload towards fixed proportions across its classes and contain the static-priority and quadratic max-weight policies as special cases. Their analysis is hierarchical. Under a queue-ratio policy the fluid model first reaches state-space collapse and then follows a linear Skorohod problem. This mission formalizes the second layer: a purely algebraic sufficient condition for stability of that Skorohod problem holds for every queue-ratio policy as soon as it holds at the finitely many static-priority "corners".
Timeline. Dai (1995) reduced stability of the queueing network to stability of its fluid model. Delgado (2010) related fluid stability under state-space collapse to stability of a Skorohod problem. Chen (1996) gave the Chen- sufficient condition for stability of a linear Skorohod problem. Zhao, Gurvich and Hasenbein (preprint 2023, Operations Research 2025) proved that Chen- is inherited from the static-priority corners (their Theorem 4).
Fix an open network with stations and classes. Class is served at station , and the constituency matrix has if and otherwise. holds the mean service times . is the substochastic routing matrix, and the vector of exogenous arrival rates. The network is open: converges and is invertible. Then , and the traffic intensities are .
A ratio matrix is a matrix with if and otherwise, normalized by
It is static-priority if at each station exactly one class with has and all others have . For a ratio matrix with invertible, the reflection matrix and drift are
A square matrix is an S-matrix if for some , and completely- if every principal sub-matrix is an S-matrix. The pair is Chen- if is completely- and some satisfies for every partition of the stations with and every with . Ratio matrices are neighbors if they differ in at most one column.
If for every static-priority the matrix is invertible and is Chen-, and all over static-priority have one sign, then
The network is arbitrary: any , , routing and service times.
For neighbors and with :
By Chen's theorem, Chen- of makes the Skorohod problem of the policy stable. Theorem 4 reduces this requirement over a continuum of policies to a finite check, one per static-priority policy, and the paper combines it with a state-space-collapse result to certify robust queue-ratio stability of the DHV, push-started Lu–Kumar and Lu–Kumar networks. The orthogonal convexity of Theorem 5 is of independent interest: the Chen- region of ratio matrices is in general not convex, yet it is convex along every axis-parallel segment.
The results are proved on paper and nothing in this mission has been machine-checked. A formal development checks the matrix algebra (adjugate and Sherman–Morrison identities, determinant-sign arguments) and settles the details the paper leaves out. The proof of Theorem 5(ii) is given there only as "an identical argument" to that of part (i). Theorem 6's claim needs a same-sign hypothesis that the page omits (see below).
The obvious argument fails because the convexity is only orthogonal. The set of ratio matrices is a product of simplices. A convex combination of two arbitrary Chen- ratio matrices need not be Chen-, and the inverse is not affine in . Two pieces of structure must be found and exploited instead. Moving one column of changes in one column, which makes move along a line in a reparametrized coordinate . Then completely- and Chen-, whose definitions quantify over all partitions and over the solution sets , must be shown to survive that line. The latter sets move with in a way that does not follow from convexity of either endpoint's set. Passing from neighbors to all ratio matrices needs a column-by-column descent through faces of the product of simplices. Invertibility must be maintained along the way, which is where the common determinant sign at the corners enters.
Fin J, classes Fin K; the paper's index is Lean's . The network is a structure Network J K with fields , , , and the hypotheses , , row sums of at most one, , summability of , and invertibility of . The remark and the renewal arrivals are not used.a : Finset (Fin J) with ; sub-matrices are indexed by the subtypes. Chen- quantifies over (for the condition reads and would make Chen- unsatisfiable and the goal vacuous); is allowed. Principal sub-matrices in completely- are those of nonempty index sets.A complete development needs the adjugate and determinant identities for matrices differing in one column, a Sherman–Morrison formula for rank-one updates, and a decomposition of ratio matrices along faces of a product of simplices. The definitions of S-matrices, completely- and Chen- are reusable for other work on reflected processes. Proofs of the milestones, alternative proofs of Theorem 5 that avoid linear-programming duality, and counterexamples showing a hypothesis cannot be dropped are all welcome.
Thompson sampling (TS) is the standard randomized heuristic for the Bayesian multi-armed bandit: at each decision it samples a parameter vector from the current posterior and pulls the arm that would be best if the sample were true. It ignores the remaining horizon. Min, Maglaras and Moallemi (arXiv:1902.04251, Management Science, 2025) obtain horizon-aware generalizations of TS from the information relaxation duality of Brown, Smith and Sun (Oper. Res. 2010). Each penalty function yields an upper bound on the Bayes-optimal value and an IRS policy. Such a policy samples a whole future outcome and plays the first action of the penalized clairvoyant optimum. With the zero-information penalty it is exactly TS.
Two of these policies, IRS.FH and IRS.V-Zero, are designed to interpolate between TS and the myopic rule. When one period remains they pull the arm with the highest predictive mean (Remark 5 of the paper). This mission formalizes the other end, Proposition 1: when many periods remain, they randomize exactly as Thompson sampling does. The paper presents this as the sense in which IRS policies "behave like TS during the initial decision epochs" and shift smoothly from exploration to exploitation without a tuning parameter.
There are arms . Arm has an unknown parameter . Given , its rewards are i.i.d. with law . The prior of is , a member of a conjugate family indexed by a belief . A Bayesian update maps to the posterior belief after a reward . The arms are independent. Throughout, rewards are integrable: for every belief (display (3)).
At remaining horizon and belief , the three policies act as follows:
It then plays the arm to which the optimal allocation assigns the most pulls.
Each action is a random variable driven by the policy's own sample.
Assume almost surely under , for all . Then for every arm ,
This holds for every choice of the tie-breaking rules in the argmaxes and in the allocation problem.
Proposition 1 identifies the long-horizon behaviour of the two IRS policies with that of Thompson sampling. Together with Remark 5 it pins down both ends of the horizon. It explains why their simulated regret curves track TS early and the myopic policy late (§5 of the paper). It also shows that the design choice "play the arm with the largest allocation" in IRS.V-Zero is the one that recovers TS. Other selection rules, such as any arm with a positive allocation, need not.
The paper gives a complete proof in Appendix D.1–D.2. A machine-checked version adds three things. It fixes the probabilistic model of a conjugate Bayesian bandit with infinite reward sequences in Lean, which the companion missions on the same paper also need. It makes the role of tie-breaking explicit. And it repairs a step of the printed proof: the bound in §D.2 holds only for two arms, and the general case needs and a threshold growing with . No formalization of this result is known on Prove2Me or in Mathlib.
The IRS.FH half reduces to almost-sure convergence of posterior means, which is a martingale argument (Lévy's upward theorem). That argument needs to be measurable with respect to the limit -algebra of the reward sequence, a fact supplied by the strong law of large numbers. Building the outcome law, a mixture over of infinite product measures, and identifying the conjugate update with conditional expectation are where the measure theory lies.
The IRS.V-Zero half does not follow from convergence of the posterior means alone. The selected arm is a function of an optimal allocation of a combinatorial problem whose size grows with . The naive expectation that the arm with the best limit receives "most" pulls has to be proved by an exchange argument that handles the finitely many early terms, where the posterior means can still be badly ordered. The printed version of this argument is correct only for .
Fin K with NeZero K; the reward sequence of an arm is ℕ → ℝ, 0-based.The development needs Lévy's upward theorem (MeasureTheory.tendsto_ae_condExp in Mathlib) and the strong law of large numbers (ProbabilityTheory.strong_law_ae). It also needs a lemma identifying iterated conjugate updates with the posterior given finitely many rewards, and the measurability of . These last two are reusable for any Bayesian bandit or sequential-estimation development. Contributions of the two deterministic milestones are self-contained and welcome first.
Many demand, traffic and click-through series are seasonal: their mean repeats after a fixed number of periods (a week of days, a year of months), while the length of that cycle is not known in advance. A retailer choosing among promotions, or a platform choosing among recommendations, then faces a multi-armed bandit whose arms have time-varying but periodic mean rewards. Standard stochastic bandit algorithms assume stationary means and fail here, and fully adversarial or arbitrarily drifting models give up the structure that periodicity offers.
N. Chen, C. Wang and L. Wang (arXiv:2005.08088, Operations Research, 2025) propose a two-stage policy for this problem: a spectral first stage that estimates every arm's period from a short exploration phase, and a confidence-bound second stage that learns and exploits the resulting "effective arms". Their main upper bound, Theorem 1, shows that the policy's regret grows like up to logarithmic factors. This mission formalizes that theorem and the chain of lemmas behind it. The matching lower bound (Theorem 3 of the paper) is the subject of a separate mission of this series.
At each epoch a decision maker pulls one of arms. Pulling arm at epoch yields the reward . The mean has a minimum period : for all , and no smaller positive shift has this property. The standing assumptions are:
The pseudo-regret of an arm sequence is , and the number of effective arms is : arm at phase is one effective arm.
Stage one (Algorithm 1). Each arm is pulled times in a row. From its rewards the policy computes the periodogram , the modulus of the discrete Fourier transform , on . A data-driven threshold is computed from the constants (sums of sinc-type maxima), and . The algorithm repeatedly takes the highest peak above in , snaps it to the nearest fraction with , and removes a -neighbourhood. The period estimate is the least common multiple of the selected reciprocals.
Stage two (Algorithm 2). At every later epoch an -round screening tournament, , compares the arms at their current phases modulo . It uses estimated means and widths pooled from the stage-one samples and from round-specific index sets . The weak oracle runs the same policy with the true periods in place of .
The parameters are fixed by (7): , , . Assumption 3 asks , and . Assumption 4 asks the smallest present Fourier coefficient of each arm to dominate a combination of and the largest coefficient .
Under Assumptions 1–4 and (7), the two-stage policy satisfies
with depending only on and , and with Algorithm 2 run at .
The theorem shows that unknown seasonality costs only the factor that would be paid if every phase of every arm were a separate stationary arm. Up to logarithmic factors this matches the rate of the classical stationary bandit with arms in place of . Together with the paper's lower bound it locates the minimax regret of periodic bandits within a factor . Stage one is a non-asymptotic, finite-sample period-identification guarantee for a thresholded periodogram, which is of independent use in spectral estimation.
The paper proves these results; none of them is machine-checked. A complete development yields a verified finite-sample periodogram theory (noise bounds for random trigonometric polynomials, Dirichlet-kernel leakage estimates), a verified anytime sub-Gaussian inequality, and a verified analysis of a nested elimination algorithm with data reuse. The formalization also pins down several points the printed text leaves open: the constant of Lemma 6 and the exponent of Lemma 7 and Theorem 2 are slightly stronger than what the proofs give, and the printed claim that Theorem 1's constant is independent of is not established by the printed argument.
Two steps resist the obvious approach. In stage one, the periodogram has to be controlled at uncountably many frequencies at once. A union bound over is unavailable, and the leakage of each present frequency spreads over the whole spectrum, so both the noise and the signal must be bounded uniformly in with explicit constants. In stage two, the samples used to estimate an effective arm are selected with the estimated periods, which were computed from the same stage-one data, so the usual independence behind confidence bounds fails. Lemmas 9–11 are therefore stated for the weak oracle, whose sample selection does not depend on the data; on the event the definitions make the oracle's run and the policy's run the same function of the noise path.
Epochs are natural numbers ; arms are Fin K (the paper's arm is index ), and . The noise is a sequence on a probability space, independent, with Mathlib's HasSubgaussianMGF at variance proxy , plus the printed tail clause. Both algorithms are defined in full, as deterministic functions of the noise path, with canonical tie-breaking: smallest maximizer, smallest closest candidate, smallest arm index. Algorithm 1's loop runs at most passes, and is the least common multiple of the reduced denominators of the selected frequencies. Algorithm 2 takes its period vector as an argument; the two-stage policy and the oracle are its two instances. Expected regret is an outer expectation: an integrable majorant of the regret whose integral obeys the bound. Probability bounds bound the outer measure of the bad event. Every DFT uses the absolute stage-one epochs, as in Step 8 of Algorithm 1.
Disclosed deviations: Theorem 1's constant depends on and (the printed proof does not give uniformity in ), and is fixed as in the proof of Lemma 11. Lemma 6 uses for the printed ; Lemma 7 and Theorem 2 use for the printed . Lemma 7 covers the nonzero present frequencies. Lemma 11 states the standing Assumption 3 and the parameters (7) as hypotheses, as its proof uses them.
The algorithm is the object of the theorem. Replacing Algorithm 1 by "any estimator that is correct with high probability", or Algorithm 2 by "any policy with the oracle's regret", would make the goal a different and much weaker statement. So would placing the constant after the horizon or the instance, since the regret is at most , or using a bare Lebesgue integral of a possibly non-measurable regret.
A complete development needs discrete Fourier analysis of finite sequences, Bernstein's inequality for complex polynomials on the unit disc (Lemma 14 of the paper, from Nagy and Totik), sinc-function estimates, anytime concentration for sub-Gaussian sums, and a bookkeeping layer for the nested index sets of Algorithm 2. The concentration and polynomial-inequality parts are reusable beyond this mission. Proofs of individual lemmas, helper lemmas such as the closed form (6) of the frequency components, and alternative arguments are welcome.
Optimal control of partial differential equations under uncertainty arises whenever a physical system is steered by a control while its sources, coefficients or loads are only known in distribution. A typical requirement is a state constraint: the state (a temperature, a concentration, a displacement) must stay below a threshold everywhere in the domain. When the source term is random, demanding this for every realization is often impossible or too conservative, and the natural relaxation is a probabilistic (chance) constraint: the state must stay below the threshold uniformly on the domain with probability at least .
Probabilistic constraints are classical in operations research (Prékopa, Stochastic Programming, 1995), but in a PDE setting the constraint is an infinite family of random inequalities, one per point of the domain, and the probability function is not differentiable in general. C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for such problems in terms of the Clarke subdifferential, building on the spherical-radial decomposition of Gaussian vectors developed by Hantoute, Henrion and Pérez-Aros (Math. Program. 2019) and van Ackooij and Henrion. This mission formalizes the PDE half of §2 of that paper: explicit formulas for the subdifferential of the probability function and the resulting optimality conditions.
Let , , be a nonempty, open, bounded set of class S: there are and with for all and . For the Dirichlet problem in , on has a unique weak solution in ; the solution operator is linear and continuous.
Fix and a threshold . The control-to-state operator is
The random vector on a probability space is Gaussian with positive definite, and is the random state. With and the probability function , the problem is
with convex and Fréchet differentiable and .
The analysis uses the spherical-radial decomposition. Let be the uniform distribution on the unit sphere , the chi distribution with degrees of freedom and density , the square root of . The radial probability function is and the radius function is the supremum of that set. For , is defined by , and
is the Clarke subdifferential, with identified with , and integrals of set-valued maps are Aumann integrals.
Assume a control with (41), and let be feasible with expected state satisfying on (42). If solves (24), there is with
and these conditions are sufficient when is a singleton for -a.e. with , or the set is bounded. The goal has no hard-coded constants; it asserts the form of the optimality system.
In attack order: well-posedness of the state equation with the bound (Lemma 1.2); measurability of the random state (Lemma 1.4); convexity and global Lipschitz continuity of (Lemma 2.9); moderate growth (Lemma 2.10); the Lipschitz and subdifferential conclusions of the general theory under (26) (Corollary 2.11); the optimality conditions (21), (22) for (24) (Corollary 2.12); when (Lemma 2.13); the explicit formula when (Lemma 2.14); and the upper estimate (40) of with its equality cases (Theorem 2.15).
The result turns an abstract statement — lies in a multiple of the Clarke subdifferential of a probability function that has no closed form — into a condition written in the problem data: Green-type functions , the expected state, and the radius function along each direction of the sphere. This is what makes the conditions usable for checking candidate controls and for designing algorithms, and Example 2.18 of the paper computes a solution this way. The sufficiency half identifies when the nonconvex chance-constrained problem behaves like a convex one.
The paper's proofs are on paper only; to our knowledge none of these results, nor the spherical-radial decomposition, Clarke calculus in Hilbert spaces, or Aumann integrals in , has a machine-checked proof. Formalizing Theorem 2.16 requires connecting elliptic regularity, Gaussian measure theory and nonsmooth analysis, and the milestones are reusable on their own: Lemma 1.2 is a regularity statement for the Poisson equation, and Lemmas 2.13 and 2.14 are max-function subdifferential formulas in an infinite-dimensional space.
The obvious route — differentiate and use a Lagrange multiplier — fails because is generally not differentiable even for smooth data (Example 2.17 of the paper), and because is only Lipschitz, being a maximum over . The general subdifferential estimate (Theorem 2.2, from Hantoute–Henrion–Pérez-Aros) needs a growth condition and only gives an inclusion, since the radial probability function is not Clarke regular; the radius function is an infimum over the open set where , which is neither compact nor independent of , so standard max-function formulas do not apply directly. Directions with require a separate limiting argument through the Mordukhovich subdifferential (Lemma 2.13). The regularity input, continuity of solutions on for class-S domains (Kinderlehrer–Stampacchia 1980), is not in Mathlib.
All declarations are in the namespace ChanceStateCtrl.PDE. and are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m), indices are Fin m, is Lp ℝ 2 (volume.restrict D). Weak derivatives are the published HunterPDE.Shared.HasWeakDeriv; a weak solution is a function continuous on , zero on , in with weak first derivatives in , satisfying the weak form against .
Standing hypotheses on every theorem: open, bounded and nonempty, , class S, and CompactSpace (closure D) (a consequence of boundedness). Nonemptiness of is the one added hypothesis: Lean's supremum over an empty domain is , not , and Lemma 2.9's identification of events fails for . is a continuous linear map to together with the hypothesis that it returns the weak solution; it is never an arbitrary operator. , as the uniform distribution on requires. is the positive semidefinite root; is its operator norm. The Clarke directional derivative is (the page's denominator is a misprint). takes values in . clco is the norm closure of the convex hull. The integral in (40)/(43) is over the restriction of to , not a renormalization. A solution is a global minimizer over ; the page's "solution to (9)" refers to this instance of the abstract problem (9).
Trivializing formalizations are ruled out: every Clarke subdifferential is taken at a point where the function is locally Lipschitz (proved in Corollary 2.11 and Theorem 2.15), the state operator is tied to the PDE, the multiplier carries its sign and complementarity, Aumann selections must be scalarly integrable, and optimality is global.
Needed infrastructure: elliptic regularity in for class-S domains; the spherical-radial decomposition of ; Clarke calculus (chain rule, max functions) on Hilbert spaces; Clarke's theorem on subdifferentials of integral functionals. Contributions of any of these as stand-alone theorems are welcome.
Dividing indivisible goods among agents without money is a basic problem of fair division. The most widely used procedure is Round-Robin: the agents take turns, in a fixed order, picking their favourite remaining good. For agents with additive valuations, Round-Robin run on the agents' true preferences produces an allocation that is envy-free up to one good (EF1, Lipton et al. 2004). The agents, however, report their preferences, and a strategic agent may misreport. This raises the question of which allocations arise at the mechanism's equilibria, and whether equilibria exist at all.
For additive valuations, the existence of an exact pure Nash equilibrium was established in pieces over three papers (Bouveret–Lemaître 2016, Aziz–Goldberg–Walsh 2017, Amanatidis et al. 2021), through the bluff profile, in which every agent reports the order in which the truthful run hands out the goods. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research 2025) carry this programme beyond additive agents. For cancelable valuations the bluff profile is still an exact equilibrium (Theorem 3.2). For submodular valuations exact equilibria may fail to exist (Proposition 3.4), and the right generalization of the bluff profile is not obvious. This mission formalizes their answer for submodular agents: a greedy bluff profile that is always a -approximate equilibrium, with best possible.
There are agents and a finite set of goods. Agent has a valuation that is normalized, , and non-decreasing. The marginal value of with respect to is . The valuation is submodular if whenever and .
Each agent reports a ranking , a total order on . Mechanism 1 (Round-Robin) runs rounds. In each round agents act in turn, and the acting agent receives the first good of that is still available. denotes agent 's true value for the bundle she receives under the reported profile . A profile of rankings is an -approximate pure Nash equilibrium (PNE) if no agent can multiply her value by more than through reporting another ranking:
The submodular bluff profile comes from Algorithm 2 (p. 10), a hypothetical truthfully greedy run. Agents act in round-robin order, and the active agent takes a good of largest marginal value with respect to her current goods . Listing the goods in the order this run hands them out gives , and the bluff profile is the profile in which every agent reports .
When all valuations are submodular, the bluff profile is a -approximate PNE:
Moreover, for every there is an instance in which the bluff profile is not a -approximate PNE. Both parts form the goal; the bound without the tightness is a weaker statement.
Companion statements: Theorem 3.8 (p. 14: the bluff allocation is -EF1, tight) and Proposition 3.4 (p. 10: an instance with no -approximate PNE).
The theorem settles existence for a class where exact existence fails. Proposition 3.4 shows that submodular agents can make every profile unstable, so an approximate equilibrium is the most one can ask for, and Theorem 3.7 exhibits one with the explicit factor by a polynomial-time construction. Theorem 3.8 turns the equilibrium bound into a fairness bound, -EF1 for the bluff allocation. The paper's §4 then shows that every approximate equilibrium of Round-Robin is approximately EF1 for submodular agents, so the existence result here is what makes those fairness guarantees non-vacuous.
The result is proved in the paper; none of it, nor Round-Robin as a mechanism, has a machine-checked proof that we know of. Formalizing it adds a reusable layer for discrete fair division: valuation classes, Round-Robin with step-level bookkeeping, approximate PNE and approximate EF1. On top of that layer come a rigorous proof of the coupling argument and a checked tight instance. The other three missions of this series reuse the same model.
The obvious approach compares agent 's bundle under the bluff profile with her bundle after a deviation, one good at a time. In the cancelable case this works by a swapping argument. For submodular valuations the value of a good depends on what the agent already holds, so a good-wise comparison is only meaningful relative to a carefully chosen ordering of the deviation bundle. That ordering is Algorithm 3, which renames the goods backwards by minimum marginal value against prefixes of the bluff bundle.
Even with that ordering, the good-wise inequality of Lemma 3.5 does not by itself bound by ; the analogue of the cancelable lemma that would do so is missing. The bound comes from an interleaving of prefixes of with suffixes of , and that is where the factor is lost. The proof of Lemma 3.5 must also follow how a single deviation shifts which goods every other agent receives, step by step, in two coupled runs of the mechanism. This counting is the bulk of the work in Lean.
Agents are Fin n with [NeZero n]; goods are a Fintype with decidable equality. Valuations are real-valued and carry normalization and monotonicity. Submodularity is the paper's marginal form, not the lattice form. Rankings are lists that contain every good exactly once, and deviations in the PNE definition range over rankings only. Round-Robin is computed step by step: step (0-based) belongs to agent .
Committed conventions:
IsGreedyOrder v h admits every tie-breaking of Algorithm 2, and the theorems quantify over all of them, so they include the paper's lexicographic bluff profile. The tightness parts hold for every greedy order of the instance, and the instance must admit one.Trivializing formalizations are ruled out by four requirements. Deviations range over rankings, not arbitrary lists. The approximation factors are the paper's and with . The bluff profile is Algorithm 2's output, not an arbitrary profile. The goal contains the tightness part.
Reusable beyond this mission: the Round-Robin model, valuation classes, approximate PNE and EF1. Welcome contributions include API lemmas about allocBefore and roundRobin (bundle sizes, the bluff run allocating in order, the effect of a single deviation) and the submodularity of OXS valuations.
The European Union's General Data Protection Regulation (GDPR, 2018) requires a firm to obtain a consumer's explicit consent before it collects personal data. The common expectation, in policy debate and in much of the empirical literature, is that consent requirements cost firms money: they shrink the pool of consumer data that can be monetized through advertising, personalization or resale. Choe, Matsushima and Shekhar (ISER Discussion Paper No. 1246, 2024; published as Management Science, 2025) build a monopoly pricing model in which consent creates a new purchase option. A consumer who would not have bought the service under compulsory data sharing can now buy it without sharing. They then ask how the firm's equilibrium price, profit and consumer surplus change.
This mission formalizes the paper's analytic profit result. If the firm's revenue is mostly usage based, meaning its revenue per unit of collected data is small, then the firm earns strictly more in equilibrium after the GDPR than before. The result is the source of the paper's title. Regulation that is usually read as a cost to firms raises the profit of one well-defined class of firms.
A monopolist sells an online service at zero marginal cost and sets a price . Negative prices are allowed: they pay consumers to use the service. A consumer type is a pair , where is the valuation of the service and the privacy cost of sharing data. Types are independent and uniform on the unit square, so the mass of a set of consumers is its area. A consumer who shares data receives an opt-in benefit . The utilities of opt-in purchase (buy and share) and opt-out purchase (buy without sharing) are
The firm earns data revenue per unit of collected data. Its profit is , where is total demand and the mass of consumers who share data.
An equilibrium price is a global maximizer of the profit over : the firm moves first and consumers respond. The paper's thresholds are
"Case 1a" (before) and "case 2a" (after) are the equilibria with , in which low-valuation consumers stay out of the market.
If , both profit functions attain their maxima over , and
that is, . The hypothesis forces , because .
The result. Proposition A3 separates firms by revenue model. A firm whose revenue is mostly usage based gains from the GDPR. The opt-out option brings in consumers with high privacy costs who did not buy before, and this extra demand lets the firm both raise its price and sell to more consumers. Together these outweigh the lost data revenue. The other two bullets of Proposition A3 treat firms with larger , for which the comparison can go either way. Their thresholds and are defined only as "the value of that solves" an equation, with existence and uniqueness shown in plots, so they are not posed here. The paper's Propositions 1–4 are its main-text results at . The price comparison (Proposition 1) is the instance of the general Proposition A1, the subject of the sibling mission in this series. Propositions 2–4, A2, A3 (bullets 2–3) and A4 rest on numerically located thresholds and are not posed.
Formalizing it. The paper's proof is in print, but no part of it has been machine-checked. The model is fully explicit (a uniform distribution, two areas, two profit functions on ), so a complete formal proof would certify every link from the primitives to the inequality. That covers the computation of the polygon areas, the global maximization of a piecewise polynomial over all real prices, and the final polynomial inequality. The printed proof of the last step contains a slip: the value it gives for "" is the value of . A formalization fixes such details for good.
The closed forms are easy to verify once the equilibrium is known to be interior to case 1a and case 2a. The work lies elsewhere. Computing the demands requires the Lebesgue area of a family of polygons whose shape changes with . Over all of each demand is piecewise polynomial with several pieces, and the profits are piecewise cubic. Identifying the global maximizer means checking every piece, including negative prices before the GDPR and the corner pieces where demand saturates at or . A first-order condition on one piece gives only a candidate. The comparison of the two maximal values then reduces to a two-variable quartic inequality on a triangle, which holds strictly on the open region but becomes tight at its corner , , where .
GDPRPrivacy.PriceRise.Model, shared with the sibling mission on the equilibrium price. A type is q : ℝ × ℝ with q.1 = v and q.2 = c. Demands are (volume S).toReal for the explicit sets above, with the opt-in and opt-out sets of p. 13 copied literally. Ties are assigned to opt-in, which changes only null sets. The file also defines .p with IsMaxOn (profitBefore x α) Set.univ p (respectively profitAfter). Every statement asserts that a maximizer exists and then quantifies over all maximizers.MeasureTheory.volume (Fubini or regionBetween), maximization of piecewise polynomials on , and polynomial inequalities. Lemmas computing the area of as a function of are reusable for other uniform-type screening and pricing models. Contributions of such lemmas, and of the explicit demand formulas (4)–(6) of the paper, are welcome.A retailer often knows more about her own demand than the supplier who must produce for her. In a decentralized supply chain the supplier sets a production quantity before demand is realized, and an under-informed supplier produces too little or too much. The retailer can shape what the supplier believes by committing in advance to a disclosure policy, a rule that maps what she knows to messages she sends. This is the Bayesian persuasion or information design framework of Kamenica and Gentzkow (2011), applied by Candogan and Gurkan (2024) to a newsvendor supplier.
The natural expectation is that the retailer either tells the supplier everything or nothing. The paper shows the answer depends on the supplier's critical ratio, and that it can be non-monotone. For nested demand supports (the setting of the first missions in this series) partial disclosure appears for low critical ratios. This mission formalizes the paper's §4 extension to supports that overlap without being nested. There, under an explicit condition on the supports, the optimal policy moves from partial disclosure to no disclosure to full disclosure as the critical ratio rises.
The state is with prior . In state the retailer's demand is uniform on . The supports intersect:
Write , , ; all three are positive.
The supplier holds a belief and chooses a quantity that minimizes the newsvendor cost (2),
where is the critical ratio of the shortage cost and the excess cost . A best-response profile assigns an optimal quantity to every belief .
A policy consists of a finite message space and probabilities . After message the supplier's belief is the Bayes posterior (1),
The retailer orders the realized demand and bears only the shortage. Her design problem (3) minimizes, over policies and best-response profiles , the expected shortage
where is the induced posterior. Full disclosure reveals . No disclosure sends one uninformative message. The function
of (B.1) is the retailer's cost when the posterior is , and denotes its lower convex envelope on .
Assume and . Let and . Then:
where has two messages, sends in state with probability 1, and sends in state with probability .
The result. With nested supports, more information can only hurt the retailer at low critical ratios. With overlapping supports, Proposition 3 shows the regimes of full, no and partial disclosure can occur in a different order. It also gives a sufficient condition on the shape of the supports for that pattern. Together with the paper's Theorem 1 (nested) and Theorem 3 (disjoint), it gives the optimal policy for the main configurations of two uniform supports. The explicit thresholds tell a practitioner which disclosure regime applies from four interval endpoints and a cost ratio.
Formalizing it. The paper's argument is in its Online Appendix (C.1, pp. 30–35). It cites Kamenica–Gentzkow for the value of the design problem and proves the envelope lemma through second-derivative sign computations. None of this is machine-checked. A complete development yields a formal concavification theorem for a finite-state persuasion problem over all finite message spaces, which is reusable well beyond this paper. It also yields a checked closed form for the newsvendor quantile under a two-uniform mixture. The goal and every milestone are open on the platform; only the published convex-envelope definition is reused.
The obvious argument compares full disclosure, no disclosure and one candidate partial policy, and picks the best of the three. That proves nothing, because optimality is claimed against every policy on every finite message space. The reduction to the convex envelope (milestone 2) is what makes the comparison finite, and it is itself a theorem about splitting a prior into posteriors.
The envelope of is the second obstacle. is piecewise rational in , with two regime boundaries that move with . Its curvature changes sign across the boundaries, and the sign of its second derivative depends on relative to . Verifying that the claimed is convex at the kink requires a one-sided slope inequality whose sign rests on the hypotheses on . The equivalence of milestone 3 is where those hypotheses enter.
All objects live in the namespace SCInfoDesign.Intersecting. States are Fin 2; is the state with demand on , and beliefs are always . The uniform expectation is . Policies are stochastic maps from Fin 2 to any finite type; the paper does not bound the message space, and finite spaces are the standard Kamenica–Gentzkow setting. The supplier's cost is normalized by , which leaves its minimizers unchanged, so is the only cost parameter. A message of probability zero carries the default posterior and weight . No disclosure is the one-message policy. uses the largest optimal quantity, which is the unique one here. The envelope is the published BiconvexProg.BranchBound.convexEnvelope on .
Standing assumptions, added and disclosed because the paper uses them implicitly: ; (nonnegative demand, so the constraint never binds); . Nondegeneracy follows from the support ordering. Two printed slips are corrected in the statements and quoted as printed in the milestones: for in the display, and the label for on p. 32. The overlapping indicators of (C.2) at are read piecewise.
Trivializing encodings are excluded. Optimality is over all finite policies and all best-response profiles, not over the three named policies. The supplier's response is an argmin of (2), never the closed form (6), which is a milestone. Each named policy is also asserted to be a policy.
Contributions are welcome on any milestone. The concavification theorem (milestone 2) and the uniform-mixture newsvendor quantile (milestone 1) are the reusable pieces. Proposition 5 (shift case) and the second-derivative display (C.3) are not posed here.