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?
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.
Round-Robin is the simplest allocation rule for indivisible goods: agents take turns, in a fixed order, picking their favourite remaining good. When agents have additive valuations and report them truthfully, the outcome is envy-free up to one good (EF1) — every agent values its own bundle at least as much as any other bundle with one good removed, a notion going back to Lipton et al., 2004 and Budish (2011) — which makes Round-Robin a standard baseline in fair division (Markakis, 2017). The mechanism, however, only sees reported rankings, and agents can gain by misreporting; without monetary transfers no truthful mechanism has a meaningful fairness guarantee even for two additive agents. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) therefore study equilibrium fairness of Round-Robin when valuations go beyond additive. This mission concerns their fairness result for submodular valuations: strategic play does not destroy fairness, it only degrades it by a constant factor.
Timeline. Aziz, Goldberg and Walsh (ADT 2017) proved that Round-Robin always has a pure Nash equilibrium for additive valuations. Amanatidis et al. (WINE 2021) initiated the study of equilibrium fairness and showed that, for additive valuations, Round-Robin has equilibria and each of them yields an EF1 allocation with respect to the true valuations. The 2023 paper extends equilibrium existence to cancelable valuations (exact PNE) and submodular valuations (1/2-approximate PNE, with 1/2 tight), and proves that approximate equilibria are approximately EF1: factor for submodular and for subadditive cancelable valuations.
There are agents and a set of goods. Agent has a valuation that is normalized () and non-decreasing. The marginal value of a good with respect to a set is , and is submodular if whenever and .
Each agent reports a ranking , a total order on . Round-Robin runs steps; in step (counted from ) agent receives its -top good among those still unallocated. The result is an allocation . An allocation is -EF1 if for all agents with some satisfies . A profile is an -approximate pure Nash equilibrium (PNE) if no agent can, by reporting any other ranking , obtain a bundle worth more than times its current one:
In Lean the objects are marginal, IsValuation, IsSubmodular, IsRanking, roundRobin, IsApproxEF1 and IsApproxPNE in RoundRobinEq.SubmodularEF1.Setting; the step-to-agent map agentAt n t = t % n comes from the shared module RoundRobinEq.CancelableBluff.Setting.
For and submodular valuations, every -approximate PNE of Round-Robin yields an allocation that is -EF1 with respect to the true valuations:
Companions (not milestones): Lemma 4.1 (the greedy response is 1/2-EF1 from the deviator's perspective) and Theorem 4.2 (two agents: ).
The theorem says that fairness of Round-Robin is robust to strategic misreporting for a class far beyond additive valuations: whatever approximate equilibrium agents settle in, each agent's envy up to one good is bounded by . Combined with the existence of a 1/2-approximate PNE (Theorem 3.7 of the same paper), it gives an equilibrium that is 1/6-EF1. Lemmas 4.6 and 4.7 are statements about two runs of Round-Robin that differ in one agent's report; they involve no valuations and are reused verbatim for subadditive cancelable valuations (Theorem 4.5).
The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The mission builds a finite fair-division layer (Round-Robin as a step-by-step process, rankings, α-EF1, approximate PNE) that does not exist in Mathlib, and checks the combinatorial coupling of two runs, which is where the paper's argument carries its weight.
The obvious argument compares agent 's equilibrium bundle with its bundle after a good deviation (Algorithm 4's greedy response) and then compares that with agent 's bundle. With two agents everything not in or goes to , and this closes the argument. With agents the deviation reshuffles goods among all other agents, and there is no direct control on what ends up holding relative to the deviation run. The proof needs a global statement (Lemma 4.6) about how much two Round-Robin runs that differ in one report can diverge before each of 's turns, and then a careful indexing of by allocation time in the other run, so that a counting bound turns into the good-by-good inequality (2). The bookkeeping of steps, rounds and two simultaneous runs is the main work.
Fin n with , 0-based; goods a finite type M. The paper's standing simplification (p. 7) is a hypothesis Fintype.card M = k * n of every theorem; the paper's reduction to this case (dummy goods) is not formalized.allocBefore σ (r*n + i), and the paper's bounds for , , appear as for .Trivializing formalizations are excluded: deviations over arbitrary lists (which would strengthen the hypothesis), , EF1 computed on reported rankings instead of the true valuations, or the EF1 witness fixed in the goal statement would each change the theorem, and none is used.
Contributions welcome: proofs of Lemma 4.6 by induction on rounds (the reusable core), basic API for allocBefore/roundRobin (every good is allocated once, ), and Theorem 2.1.
Service providers such as hospitals or retail stores each fit a predictive model on their own data, and many of them have few observations. The models of different providers are usually similar but not identical: most coefficients agree, while each provider deviates from the common model in a few features of its own. Multitask learning asks how data from all providers can be pooled to estimate every provider's model better than it could estimate alone, without being misled by the providers that differ.
Xu and Bastani (arXiv:2112.14233v5) model this with sparse heterogeneity: every task parameter is a shared vector plus a sparse deviation. They propose the robust multitask estimator (RMEstimator), which combines per-task least-squares estimates by a coordinatewise trimmed mean and then corrects each task by a LASSO regression centred at that shared estimate. Their main fixed-design guarantee, Proposition 5, is a high-probability bound on the estimation error of each task. The same estimator drives the paper's multitask contextual bandit algorithm (§5), whose regret analysis rests on this bound. The approach builds on transfer learning with a single proxy model (Bastani 2021) and on the robustness of the trimmed mean to corrupted samples (Lugosi and Mendelson 2021).
There are tasks. Task has observations, a fixed design matrix whose columns satisfy the normalization (equation (1)), and responses
The noise terms are mutually independent across all tasks and observations, and each is -subgaussian with mean zero: for all . Assumption 1 asks that the sample covariance matrices satisfy .
Given a trimming level and regularization levels , Algorithm 1 computes:
A coordinate is -poorly-aligned, , if fewer than a fraction of the tasks satisfy ; otherwise it is -well-aligned (Definition 2).
For every constant , every , every , every task and every , every output of Algorithm 1 with satisfies
with probability at least .
The printed Proposition 5 (p. 17) has where this statement has . The proof on pp. 41–43 ends with and combines it with (16), whose coefficient is , so it establishes the bound with . The goal is the bound the proof supports.
Proposition 5 separates two error sources: a LASSO term of order , which depends only on the task's own sample size, and a trimmed-mean term that shrinks with the number of tasks through . With the hyperparameters of Appendix A.2 it yields Theorem 1, an error of order up to logarithmic factors, against for a single task alone. The same decomposition underlies the paper's data-poor guarantee (Proposition 8) and the regret bounds of its multitask bandit algorithm.
The result is proved on paper; none of it has been machine-checked. A formal development checks the constant bookkeeping, including the factor 4 that the printed statement omits, and the use of the trimmed mean for samples that are independent but not identically distributed, which is where this paper departs from the classical i.i.d. robust-statistics results. Proposition 4 and Lemma 1 are reusable on their own: a corruption-robust concentration bound for the trimmed mean and a noise bound for fixed-design LASSO.
The obvious estimator of the shared parameter, the average of the per-task estimates, converges to the average of the , which differs from in up to coordinates, so the LASSO correction would have to undo a dense bias. The trimmed mean avoids this only on poorly-aligned coordinates, and only with high probability. The proof of Proposition 4 must control the samples that survive trimming even though they are not identically distributed and trimming biases the conditional means; that step needs a moment bound for subgaussian variables and a Hoeffding argument on a random index set. The LASSO step needs the cone inequality with a support that is not the support of , and the counting bound (6) to control its size.
Fin N, Fin d, Fin (n j); paper index is Lean i − 1. Designs are deterministic matrices; only the noise is random.HasSubgaussianMGF with variance proxy , . Independence of all noise terms is iIndepFun over the pairs .A formalization that drops Assumption 1 (making the OLS inverse a junk zero), lets the corrupted samples of Proposition 4 be independent or well-behaved, fixes a single existentially, or reads a junk minimizer from Classical.choose, does not state the paper's result.
The development needs least-squares algebra for fixed designs, a Hoeffding bound for independent bounded variables, moment bounds for subgaussian variables, and the LASSO basic inequality. Proofs of any milestone are welcome, and so are alternative arguments for Proposition 4 with better constants.
Firms that hold purchase-history data can treat past customers and a rival's customers differently. The economics of behavior-based pricing (BBP), charging different prices to the two groups, is well developed: in a symmetric duopoly, poaching the rival's customers with discounts intensifies competition and usually lowers profits (Fudenberg and Tirole 2000; Villas-Boas 1999). The same data can also target information. A firm launching a new product of uncertain quality can disclose that quality (free samples, demonstrations, trials) at a cost per customer reached, and it may disclose to one segment and not the other. This is behavior-based quality disclosure (BBD).
Zhang and Li (Management Science 71(10), 2025) combine costly voluntary disclosure in the style of Jovanovic (1982) with BBP in a two-period Hotelling duopoly. Their Proposition 1 answers two questions about the second period: to which segment should a firm disclose more readily, and does the option to target disclosure help or hurt profits? This mission formalizes that proposition and the displayed formulas from which it is derived.
Two firms, A at and B at , face a unit mass of consumers spread uniformly over , with unit transportation cost and a base value high enough that every consumer buys in every period. The first-period purchase splits the line at a share : A's turf consists of A's old customers, B's turf of B's.
In period 2 firm launches a product of quality ; and are independent and uniform on , and consumers do not observe them. Disclosing to the consumers in an interval of length costs , where is the unit disclosure cost. A firm discloses to a segment exactly when its quality exceeds a disclosure threshold ; consumers who see no disclosure infer and hold the belief . The updated belief is therefore if and otherwise.
In both regimes firms then set four prices: on A's turf and on B's turf. On A's turf, with beliefs , the consumers who stay with A are with , clamped to the turf; B's turf is symmetric. A second-period equilibrium is a profile of thresholds and turf price strategies such that, for every belief pair, the turf prices are a Nash equilibrium among nonnegative prices, and every threshold is a best response: disclosing is optimal above it and withholding below it. The ex ante second-period profit is A's expected revenue minus expected disclosure cost, over .
For , at the symmetric first-period share : equilibria exist under both regimes; in every BBD equilibrium
in every BBD equilibrium and for every realization , at the induced beliefs, each firm charges the rival's customers less than its own,
and for every BBD equilibrium and every uniform-disclosure equilibrium, each firm's ex ante second-period profit is strictly higher under BBD:
The goal asserts the shape of the result (an order of thresholds, of prices and of profits) and no closed form.
The result. Part (a) says that disclosure should be retention focused: a firm reveals quality to its own customers over a wider range of qualities than to the rival's. This is the opposite of the acquisition focus BBP prescribes for prices, so the two instruments built on the same data pull in different directions. Part (b) records that prices stay acquisition focused: the rival's customers get the lower price. Part (c) says that targeted disclosure raises second-period profits, in contrast with the classical finding that targeted pricing lowers them. Under uniform disclosure a single threshold over-discloses to the rival's customers and under-discloses to one's own; BBD separates the two, and the paper locates the gain in the expected disclosure cost in (5) against in (14).
Formalizing it. The paper's proofs are in an Online Appendix; the main text shows the displayed formulas only. A formal proof checks the whole chain from the clamped price games, through the best-response conditions, to the closed forms of Table 1 and the final comparison. The comparison in (c) is delicate: the profit difference is positive on all of but tends to as (about at ), so a numerical check does not settle it. The mission also gives the platform its first Hotelling duopoly, its first behavior-based pricing model and its first costly-disclosure model.
There are three nested equilibrium notions: Nash prices in each turf for every belief pair, best-response thresholds given those prices, and expectations of piecewise-defined profits over the belief support. Lemma 2's prices solve first-order conditions only in the interior; uniqueness among nonnegative prices requires ruling out the corners where one firm sells nothing on a turf. Each threshold is characterized by a best-response condition rather than an equation, so obtaining (4) or (13) requires showing that the disclosure gain is monotone in quality and crosses the cost exactly once inside . The expected profits integrate squares of linear functions of beliefs that switch at the thresholds. Finally, (c) is a sign statement about a difference of algebraic functions of with three different square roots that vanishes at ; plugging in endpoints or bounding term by term loses the sign near .
The Lean development lives in the namespace BBDisclosure.Stage2. Conventions:
A formalization in which thresholds or prices are pinned to their closed forms, or in which the equilibrium predicate is unsatisfiable, would make the goal trivial; the goal therefore quantifies over equilibria of the game itself and includes existence of an equilibrium in both regimes. "Firms'" is stated for both A and B rather than assumed by symmetry.
Needed infrastructure: piecewise-quadratic optimization on a half-line (the clamped turf games), interval integrals of piecewise polynomials, and sign analysis of algebraic expressions in , , . The turf-game analysis is reusable for any Hotelling model with behavior-based pricing. Contributions to any milestone, or to intermediate statements such as the conditional profits (3) and (12), are welcome.
In a Bayesian multi-armed bandit a decision maker pulls one of arms in each of periods, observes the reward, and updates a prior belief about each arm's unknown parameter. The best achievable expected total reward, , is the value of a dynamic program over beliefs, and for all but the smallest instances it cannot be computed. Upper bounds on are therefore the yardsticks against which heuristics such as Thompson sampling (TS) are measured: the gap between a policy's performance and an upper bound certifies how far the policy can be from optimal.
The conventional benchmark is the expected total reward of a clairvoyant who knows the arms' parameters, , the quantity behind every Bayesian regret bound. Min, Maglaras and Moallemi (arXiv:1902.04251v2, Management Science 2025) apply the information relaxation duality of Brown, Smith and Sun (Operations Research 2010) to the bandit: a clairvoyant who sees the whole future but pays a penalty for using it. Each penalty yields a performance bound and a randomized policy (IRS, "information relaxation sampling"); the zero-information penalty recovers TS and , the ideal penalty recovers . The paper's Theorem 2 shows that its intermediate penalties give bounds that are provably tighter than . This mission formalizes that theorem.
Let , . Arm has an unknown parameter ; given , its rewards are i.i.d. with law . The parameter has a prior from a conjugate family indexed by a belief , and the Bayesian update is the belief after a reward : if then . The outcome has law , under which arms are independent. Throughout, for every belief.
The conditional and predictive mean rewards are and , and the posterior predictive mean after rewards of arm is . With and , the four bounds compared are
In the last one the clairvoyant chooses a whole action sequence knowing , and at time receives the conditional expected reward under the current belief , minus , plus the expectation of given the history . A supersolution is a function with and for all , , (Definition 2).
for every horizon and every belief vector of every conjugate model satisfying the standing assumptions.
The result. Theorem 2 says that the penalties IRS.FH and IRS.V-Zero, which only require sampling a future and solving a deterministic allocation problem, produce upper bounds on that are never looser than the regret benchmark , and that IRS.V-EMax is too. A bound below gives a sharper certificate of suboptimality for any policy, and the paper's experiments (§5) report these bounds next to the policies' performance. The ordering also organises the paper's family of policies: the bounds move monotonically from the TS benchmark towards the optimal value.
Formalizing it. The theorem is proved in the paper (Appendix D.3); it has no machine-checked proof. A formal development checks three different mechanisms: conditional Jensen for (124); a one-arm-at-a-time interpolation through , driven by a non-standard Jensen-type inequality (Lemma 1, Corollaries 1–2), for (57); and the supersolution argument of Desai et al. for (58). The paper's own remark (pp. 59–60) shows that the middle inequality does not follow from the general "finer information gives a weaker bound" principle of Brown et al.; formalization fixes exactly which properties of the bandit (conjugacy, independence of arms, the martingale property of ) carry the argument.
The obvious route to is to observe that IRS.FH conditions on more information ( rewards of every arm) than IRS.V-Zero (only the history so far) and invoke monotonicity of dual bounds in the relaxation. That argument fails: the two penalties are not generated by a common function, and the paper exhibits a modified bandit (163)–(165) in which the inequality reverses. The interpolation must instead trade one arm's realized cumulative payoff for a constant per-pull payoff one pull at a time, and each step needs Corollary 2, where conditioning acts inside a maximum of affine functions; ordinary Jensen points the wrong way there.
For (58), the difficulty is that the payoff of the penalised inner problem depends on the whole outcome along an adaptively chosen action sequence; the bound must hold uniformly over all sequences, which is why it is proved pathwise by backward induction rather than in expectation.
Arms are Fin K (0-based) with [NeZero K]. All arms share one parameter type (standard Borel, nonempty) and one belief type , the disjoint unions of the per-arm ones. Rewards are a Kernel Θ ℝ per arm, priors a Kernel Y Θ per arm, both Markov. The outcome is Fin K → Θ × (ℕ → ℝ) with law the product over arms of followed by an i.i.d. reward sequence. The standing assumptions are one predicate: conjugacy (the update agrees a.e. with Mathlib's posterior of the reward kernel), joint measurability of each , and for every belief, (3). is the conjugate (pathwise) version of the conditional expectation (10). is defined by its closed form (33). In the penalties (26) and (168) the conditional expectations given are replaced by their conjugate closed forms: , and the expectation of is the integral over the predictive law of the next reward. The supersolution predicate requires the expectation in (166) to exist. Lemma 1 and Corollary 1 compare lower Lebesgue integrals in ; Corollary 1 adds joint measurability of ; Corollary 2 assumes the integrable; Lemma 2's integral form assumes the pathwise maximum integrable.
Trivializations ruled out. No expectation in a goal can silently be a junk : the standing integrability makes every bound an honest integral, and Lemma 1 and Corollary 1 are stated with lower integrals. is the penalised clairvoyant value of the penalty generated by , not itself or the closed form (41) substituted into it. The standing assumptions are satisfiable (a sorry-free check with a one-point parameter space is in the development).
A complete development needs: conjugate updating along reward sequences and the martingale property of (Remark 1); measurability of ; independence of arms under ; conditional Jensen for finite maxima. Lemma 1, Corollaries 1–2 and Lemma 2 are reusable beyond this mission. Contributions of any milestone, or of the infrastructure lemmas above, are welcome.
Many operational risk questions ask for a small probability : the chance that the cost of a decision, evaluated at a random scenario , exceeds a large threshold . Examples are large delays in project networks or vehicle routing, large portfolio credit losses, and failures in engineered systems. Plain Monte Carlo needs on the order of samples to estimate to fixed relative accuracy, which is prohibitive when is or smaller. Importance sampling (IS) draws samples from a different distribution and reweights them by a likelihood ratio, but classical efficient IS schemes are built for one model at a time: they need the distribution of and the structure of (e.g. linearity or convexity) to solve for a good sampling distribution.
Deo and Murthy (arXiv:2102.07060v3, published in Operations Research, 2025) propose a self-structuring sampler that needs neither: it applies a fixed multiplicative stretching to ordinary samples of and uses only black-box evaluations of . Their main result is that this sampler is asymptotically optimal in the standard sense of logarithmic efficiency (Asmussen and Glynn 2007, Ch. 6) over a nonparametric class of light- and Weibull-type-tailed distributions and nonconvex losses.
Write and (componentwise), and . The random vector has density . Its marginal cumulative hazards are , , and is the standardized vector. Let be the left-continuous inverse, , and .
The standing assumptions are:
The sampler (Algorithm 1) fixes a hyper-parameter and maps a sample to , with either exponent
With the closed-form Jacobian of Table 1 and , the single-sample estimator is
Under Assumptions 2.1, 3.1, 3.2, 5.1, existence of , for some , and any slowly varying , for either exponent,
The goal fixes neither the exponent, nor the hyper-parameter , nor the loss or the distribution beyond the stated assumptions.
The milestones follow the paper's proof chain (Appendix A.3 for , Appendix E for ):
Theorem 4.1 gives the exponential decay rate of for a broad class of nonconvex losses (piecewise affine and quadratic functions, values of mixed integer programs, neural-network feature maps) under nonparametric, copula-style dependence. Previously such asymptotics were known only for specific losses and distribution families. Theorem 5.1 shows that one simple, model-oblivious transformation attains the best possible exponential rate for the second moment, so the relative error grows more slowly than any power . This supports using the sampler for value-at-risk, conditional value-at-risk and chance-constrained optimization.
The results are proved in the paper's appendices (Appendices A, D.1 and E). None of them has a machine-checked proof. Formalizing them would require regular variation and Potter bounds, a tail large deviations principle in , and a Varadhan-type integral lemma along a real speed. These are general tools that are missing from Mathlib and are reusable well beyond this paper.
The obvious argument is to bound by computing the likelihood ratio on the rare set. This fails because the rare set, after standardization, is described only asymptotically: converges to only continuously on , not uniformly. The exponent of the likelihood ratio involves the density of at two different scales ( and ) and the hazard rates at points pulled back by . A lower bound on it must hold uniformly enough to apply a Varadhan-type lemma with a varying family of functions, while the transformed sample stays inside a region where the asymptotic density assumptions apply. The upper and lower large-deviations bounds also rely on homogeneity of and , which hold only for the heaviest-tailed coordinates of .
Points of are Fin d → ℝ with the sup norm, and components are 0-based. is modelled by its law together with a density . is a lower Lebesgue integral and ; both are extended nonnegative reals, so neither nor is collapsed to a junk value. Logarithms of probabilities in large-deviations statements are taken in EReal, where . is an EReal infimum, equal to over an empty set. Regular variation is the real-variable limit with an eventually positive denominator, and reuses the published definition HeavyTailNV.Tail.IsRegularlyVarying. The Jacobian is Table 1's closed form. Statements that evaluate at take .
The following hypotheses are added relative to the printed statements, each disclosed on its item:
The following printed statements are corrected:
Lemmas A.8 and A.10 and Corollary A.1 are not posed. Their uniform claims over all of depend on pointwise versions of the hazard rates and on the values of off the support and off , which the hypotheses do not control; Corollary A.1 fails as printed when has negative components.
A trivializing formalization is ruled out explicitly. The goal is the limit (23) for the estimator of §5.2 with Table 1's Jacobian, for every admissible and both exponents. It is not the bound , not a statement about an unspecified IS density, and not a statement for one fixed . The finiteness conjunct prevents Lean's convention from satisfying it.
Contributions are welcome at every level. The general tools (Potter bounds, the tail LDP, a Varadhan lemma for continuously converging functions) are useful as separate developments.
Large retail platforms both host independent sellers and sell their own products, and they control the order in which products appear in search results. When the platform ranks its own product first regardless of relevance, it engages in self-preferencing. Regulators have treated this as a competition problem: the European Commission opened a second antitrust investigation into Amazon's treatment of its own retail offers in 2020 (CNBC, 2020), and search neutrality, the requirement that results be ranked by relevance alone, is the remedy most often proposed.
Zou and Zhou ask whether such a rule helps consumers once prices respond to it. Their model builds on the economics of prominence in consumer search (Armstrong, Vickers and Zhou, 2009), in which the product shown first is searched first and so enjoys a demand advantage. The answer they obtain is negative in an identifiable region: when the two competing products are similarly popular, search neutrality strictly lowers consumer surplus. This mission formalizes that result and the equilibrium analysis on which it rests.
A platform sells its own product and hosts a third-party seller of a competing product ; marginal costs are zero. A unit mass of consumers has unit demand. A product either matches a consumer (value ) or not (value ).
Under Condition 1 there are thresholds , depending only on , with
such that for every , consumer surplus in every equilibrium with search neutrality is strictly smaller than in every equilibrium without it:
The equilibria without neutrality: the price order when is prominent for all (Appendix, p. 42); the closed-form equilibrium of that pricing game (cases (A)–(B), pp. 42–43); the statement of Lemma A1 (p. 42); Proposition 1 (p. 16) and the uniqueness claim before it. The equilibria with neutrality: the price order by (pp. 44–45); cases (A2), (A3)/(B3) and (B2) (pp. 45–46); Proposition 2 (pp. 17–18). The two consumer-surplus displays (pp. 43–44 and 46). Proposition 3(2) and Corollary 1 are included as companion statements.
The result. Proposition 3(1) shows that a relevance-based ranking rule can backfire. Under self-preferencing the third-party product is never prominent, so its seller prices low to invite search, and this disciplines the platform's own price. Under neutrality each seller is prominent for the consumers who like its product best, and for similarly popular products both sellers charge the maximal price ; on consumer surplus with neutrality is exactly zero. The goal makes this precise and shows that the harmful region strictly contains that interval. It is the paper's central short-term finding and the basis of its policy discussion.
Formalizing it. No part of this analysis is machine-checked anywhere, and the platform has no model of consumer search with prominence. The source file contains the equilibrium derivations of §4.1 in its Appendix, but the proofs of Propositions 1–3 and of Lemma A1 are in an online appendix that is not part of the source; a formal proof would supply them. Several of the Appendix's closed forms are misprinted (the interior prices of cases (A1) and (B1), the thresholds and ), and the threshold misclassifies the boundary when ; the formal statements fix what is actually true.
The profits are piecewise quadratic with a kink at , so first-order conditions do not characterize equilibria: every candidate must be checked against global deviations across the kink. Without neutrality, a deviation can also change the platform's ranking, so the deviating seller faces a different demand system; this is the content of Lemma A1 and the reason Condition 1 is needed. The obvious argument for the goal, "consumer surplus with neutrality is zero on and positive without it", proves only the closed interval. The strict extension to requires controlling the neutral equilibrium just outside that interval, in the regions (A2) and (B2), where it is no longer at the corner.
A complete development needs elementary real analysis only: piecewise quadratic optimization on , the integral , and continuity of the neutral equilibrium in . The model definitions are shared, with the same names, with the companion mission on equal popularity and the commission rate. Proofs of any milestone are welcome, as are proofs of Lemma A1 and of uniqueness, whose arguments are not in the source.
Heavy-traffic analysis is the standard tool for scheduling queues whose servers are almost always busy: after diffusion scaling, a multiclass queue is approximated by a reflected Brownian motion, and asymptotically optimal policies are read off a limiting control problem. Classical results of this kind, such as the asymptotic optimality of the cµ rule (serve the class with the largest holding cost times service rate first; van Mieghem, 1995), assume that the job-size distributions are known.
In practice the first moments of service times are usually estimated well, while their variability is not. Atar, Castiel and Shadmi study a high-uncertainty regime: the means of the job-size distributions are pinned down to within , but their variances are uncertain at order one, and an adversary chooses them job by job with full knowledge of the past. The scheduler wants to minimize, and the adversary to maximize, a discounted holding cost. The paper solves this game asymptotically: the nonpreemptive cµ policy is asymptotically optimal against every adversary, and the value of the game converges to the value at of a one-dimensional Hamilton–Jacobi–Bellman (HJB) equation.
There are job types and one server. In the -th system one job of each type arrives at each time , , and the server works at rate , so that a job of size occupies it for time units. The system starts empty.
Adversary. For each and type an uncertainty class , a nonempty closed set of probability distributions on , is given. At each epoch the adversary chooses for every , based on the past job sizes, and the job sizes are then drawn independently across types from these distributions. The set of such controls is .
Scheduler. The scheduler chooses the cumulative effort devoted to each type, an -dimensional Lipschitz path whose increments over lie in . An admissible strategy is a measurable, non-anticipating, work-conserving map from the adversary's control path to such an effort path that never serves more work than has arrived.
Cost and value. With , the workload is , the queue length is the number of arrived type- jobs not yet completed, and hats denote scaling by . For holding costs ,
Assumptions. With the mean and half the variance of , and , the sets converge in the Hausdorff distance to compact sets ; fourth moments are uniformly bounded; (heavy traffic); and types are labelled so that , with .
HJB equation. With ,
for the classical solution of the HJB equation. The paper states with the value of a martingale control problem; the goal uses the form, which leaves the martingale problem out of the statement.
The result gives the first-order asymptotics of a scheduling game with model uncertainty: the scheduler loses nothing by ignoring the adversary and using the cµ rule, and the adversary's best response is a state-feedback choice of drift and variance determined by and . Theorem 1 is a robustness statement for one of the most widely used scheduling rules; Theorem 2 reduces a game on path space to a scalar nonlinear ODE.
The paper's proofs are complete, so the remaining work is formalization. No part of this result, and none of its objects (heavy-traffic queues with adversarial service distributions, the nonpreemptive cµ policy as a map on path space, the HJB equation of a reflected controlled diffusion), has a known machine-checked statement or proof.
The statement is a limit of a real sequence, but each term is an infimum over measurable, causal, work-conserving maps on path space of a supremum over feedback choices of distributions. The proofs (§§4–7 and the appendix) use uniform C-tightness of prelimit processes, weak convergence in , the existence theory for fully nonlinear uniformly elliptic equations (Gilbarg–Trudinger, Thm 17.18), martingale characterizations of limits (Jacod–Shiryaev, Cor. VI.6.30; Karatzas–Shreve, Thm 5.5.15), measurable selection (Budhiraja–Dupuis, Lemma 8.10), and Taylor expansion of along the prelimit workload. The obvious route through the uncontrolled diffusion limit fails because the adversary's variance choice is state dependent, so no single limiting Brownian motion describes all adversaries; the limit is a control problem, not a process.
The Lean development lives in the namespace HighUncertHT.Game. Types are Fin L, 0-based (the paper's type 1 is index 0). Distributions are ProbabilityMeasure ℝ with no mass on , with the weak topology. Systems are indexed by ; the class at is required to satisfy the same conditions so that control sequences indexed by exist. Costs and values are in (lower Lebesgue integrals), sup norms are in , the Hausdorff distance is the extended one, and derivatives of are one-sided on .
An adversary control is encoded by its feedback map from past job sizes to distributions and the measurable Markov kernel it induces; its law is the Ionescu–Tulcea trajectory measure. By (5), the Doob–Dynkin lemma and (7), this has the same laws, hence the same costs, as the paper's . Strategies are measurable for the product σ-algebras. The cµ strategy is defined explicitly by an event recursion over service decisions.
The standing assumptions (Assumptions 1–2, labelling (14), ) are fields of the Setting and hold in every statement. Corrected printed slips: the priority rule serves the highest index (p. 9 prints "lowest", contradicting the cµ rule and Lemma 5); the departure count is capped at the number of arrived jobs (p. 6); "→ 0 in probability" for processes is read as convergence of the sup norm on compact intervals (Lemma 5); (55) is stated for the control (61), not (15).
Trivializing formalizations are ruled out: is nonempty because is a milestone; the HJB has a classical solution (Proposition 1.1), so the goal is not vacuous; no expectation is a Bochner integral that could vanish for non-integrable integrands; is not a junk deriv; and (55) asserts that its feedback control exists.
Needed infrastructure: diffusion-scaled processes and their tightness in , the one-dimensional Skorokhod map and its Lipschitz property, martingale estimates for sums of conditionally centred job sizes, and the existence theory for the HJB equation. The Skorokhod map, the queue primitives and the cµ policy are reusable for other heavy-traffic missions. Contributions on any milestone, or on general lemmas they need, are welcome. Not included: Lemmas 1, 6, 7, 8, Proposition 1.2, Proposition 2, Theorem 2.3 and the martingale control problem.