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?
Consumers judge a price against a reference price formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand beyond the plain price effect; a price below it is perceived as a gain and lifts demand. Because today's price moves tomorrow's reference price, a seller who prices many products over time faces a dynamic problem: a discount today raises demand now but lowers the reference price and so weakens demand later.
Whether such a seller should eventually settle on constant prices or keep the prices cycling matters in practice. Stable prices mean stable demand, which simplifies production and inventory planning; cycling prices mean recurring promotions. For a single product with additive demand, Popescu and Wu (2007) showed that loss aversion favours constant prices and gain-seeking favours cycles. Guo, Jiang and Shen (2025) study the multi-product version with multinomial logit (MNL) demand, where products compete for the same customers and each product can have its own type of reference effect. This mission formalizes their characterization of the optimal constant prices.
There are products, . Product has an intrinsic utility , a price sensitivity , a gain sensitivity and a loss sensitivity . Given a price vector and a reference price vector , the utility of product is
A customer buys product with the MNL probability and buys nothing otherwise. The single-period revenue is .
Product is loss-averse if , loss-neutral if and gain-seeking if ; , , denote the three classes.
Prices and reference prices lie in the box . The reference price evolves by exponential smoothing with memory parameter :
With discount factor , the optimal value from an initial reference price is
An optimal steady state is a price vector that the optimal policy keeps fixed: starting from reference price , charging forever is optimal. The constant path keeps and earns , so the condition reads .
Finally, set
If no product is gain-seeking (), every optimal steady state satisfies
The theorem does not assert that an optimal steady state exists; it describes every one that does.
In the same scenario, the equations
have unique solutions and , and every optimal steady state satisfies and .
If every product is loss-neutral, , an optimal steady state, if it exists, is unique, satisfies , and is the unique solution of (24).
Theorem 5 is the paper's only structural description of the optimal policy's long-run behaviour when it is stable. Computing the optimal policy requires solving a Bellman equation on an -dimensional continuous state space, which is intractable for many products; the theorem replaces that with an explicit per-product markup interval around a single scalar, the steady-state revenue. Corollary 3 turns it into explicit price bounds computable from two one-dimensional equations, so candidate constant prices outside those bounds can be discarded without solving the dynamic program. Corollary 4 shows that pure loss-neutrality pins down the steady state completely, and the comparison with the myopic steady state (markup ) shows how forward-looking pricing shrinks the reference-effect term by the factor . The same paper shows (Theorem 4) that a single gain-seeking product rules out optimal steady states altogether, which is why the hypothesis is essential.
The results are proved in the paper's online supplement (Appendix C.4); that supplement is not part of the source file used for this mission, and none of these results has a machine-checked proof. This mission produces formal statements of Theorem 5 and Corollaries 3–4 over a formal definition of the optimal value; a complete development would also produce a Lean theory of the deterministic infinite-horizon pricing problem with reference effects.
An optimal steady state is defined through the value function , which has no closed form, and the revenue is not differentiable exactly where every steady state sits: the utility has a kink at , with loss sensitivity on one side and gain sensitivity on the other. The obvious approach, writing first-order conditions of the Bellman equation at the fixed point, therefore does not apply directly. A change in today's price also moves every future reference price, so the comparison between a steady state and its alternatives involves the whole discounted future revenue stream rather than a single period, and the factor in (20) reflects this intertemporal coupling. The myopic analysis of the same paper does not transfer, because the myopic problem is a single-period optimisation over while here optimality is a property of an infinite-horizon value.
Products are indexed by Fin n (0-based). All vectors are Fin n → ℝ. The shares are defined directly by the MNL formula; the Gumbel random-utility derivation is motivation only. The theorems carry the paper's standing hypotheses explicitly: , , , , , and the standing ceiling assumption of §2.4, , where solves equation (9) (CeilingOK: some root of (9) is at most ).
Conventions committed to:
IsOptSteadyState x means and . The reverse inequality always holds (the constant path is admissible), so this is the equality above.∃!) or "solves (E), and every solution equals it"; no solution is chosen with Classical.choose.The hypothesis must not be dropped: with a gain-seeking product no optimal steady state exists (Theorem 4), so a statement without it would be vacuously true there. A formalization in which IsOptSteadyState is unsatisfiable by construction (for example a junk value of above every constant path) would make every statement here empty; the supremum is over a nonempty family bounded by .
Needed infrastructure: summability and bounds for discounted revenue streams, one-sided perturbation estimates for the kinked MNL revenue, and comparison arguments for the value function. Contributions of reusable lemmas about the MNL revenue and about reference-price dynamics are welcome.
In a budget-feasible procurement auction an auctioneer with a budget buys services from strategic sellers. Each seller knows privately what providing the service costs, and the auctioneer wants a set of services of maximum value without paying more than in total. The model was introduced by Singer (FOCS 2010) and is used to study crowdsourcing, data acquisition from individuals, and influence maximization in networks, where the value of a set of sellers typically shows diminishing returns: it is submodular.
Most of the mechanisms known for this problem are randomized, or are deterministic only when the auctioneer's valuation is monotone, i.e. adding a seller never lowers the value. Amanatidis, Kleer and Schäfer named the existence of deterministic budget-feasible constant-factor mechanisms for submodular valuations the most intriguing open problem of the area. Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) give deterministic clock auctions for these settings. In a clock auction each bidder only ever sees a sequence of decreasing take-it-or-leave-it prices, which makes truthful behaviour obvious to the bidders. This mission covers §4 of that paper: the first deterministic budget-feasible mechanism with a constant approximation ratio for general, not necessarily monotone, submodular valuations.
Timeline. Singer (2010) gave the first budget-feasible mechanisms for monotone submodular valuations. Chen, Gravin and Lu (SODA 2011) improved the constants. Amanatidis, Kleer and Schäfer (EC 2019) gave a randomized 505-approximate mechanism for non-monotone submodular valuations and introduced the idea of building two disjoint tentative sets simultaneously. Balkanski et al. (2021) give a deterministic clock auction for this class with approximation ratio 64.
There are bidders . Bidder has a private cost , the least payment it accepts. The auctioneer has a budget and a valuation that is submodular: for all . The marginal contribution of to is . A set is budget feasible if , and is the largest value of a budget-feasible set.
Simultaneous-Iterative-Pruning (Mechanism 3) works in phases with a target that starts at and doubles in each phase. In phase it grows two disjoint tentative sets and . At each step it picks a bidder and an index maximizing , offers the price , and adds to if it accepts. A bidder who rejects leaves the auction for good. A phase ends when one of the two sets reaches the target or no bidder remains to be offered a price. The two sets of the previous phase are set aside during a phase. After the last phase , an unconstrained submodular maximization subroutine is applied to the four sets of the last two phases, giving . The mechanism returns the best of the six sets , minus its last added bidder if the prices of its bidders exceed . The subroutine is required to be a 2-approximation: and for all .
For every non-negative submodular , costs , budget and 2-approximate subroutine , the set and prices returned by Simultaneous-Iterative-Pruning satisfy
Theorem 5 shows that, for budget-feasible procurement with submodular valuations, determinism costs only a constant factor even without monotonicity. Before this paper no deterministic mechanism, polynomial-time or not, achieved a constant ratio for non-monotone submodular valuations. The mechanism is also a clock auction, whose interface to the bidders is a sequence of decreasing prices. The constant 64 is not claimed to be tight, and better constants are open.
No part of this paper is formalized anywhere that we know of. A machine-checked proof would verify an argument whose bookkeeping is easy to get wrong: two simultaneous tentative sets, sets of the previous phase put aside and later returned to the pool, prices that are lowered across phases, and a pruning step whose case analysis depends on the phase a candidate comes from. The formalization already surfaced two issues in the printed text. Lemma 6 states the wrong inequality. And for it needs , a normalization the paper never assumes.
The approach of the monotone case does not carry over. There, the value of the active optimal bidders is bounded by the value of all active bidders, and that fails once adding a bidder can lower the value. The proof therefore has to account separately for the optimal bidders the auction rejects (Lemma 6, which uses both tentative sets of a phase to absorb the rejected bidders) and for those it keeps, whose value is recovered only through the unconstrained maximization step applied to the four tentative sets of the last two phases (Lemma 7). Budget feasibility needs the fact that every accepted bidder's marginal contribution was non-negative when it was added. Otherwise its offered price would have been negative and it would have rejected. The final pruning step must not lose more than half the value. This holds because a removed bidder's marginal contribution is at most the initial target, while the best candidate exceeds twice that whenever a removal happens.
Bidders are Fin n and sets of bidders are Finset (Fin n). The tentative sets are lists in insertion order, so that "the last bidder added" is defined; the candidate is the sublist of of the bidders that lie in . Valuations, costs and prices are real. The model's standing assumptions appear as hypotheses: , submodular (the published definition NonmonotoneSubmod.Shared.Submodular), and . A bidder offered the price accepts iff . Every argmax breaks ties by the least bidder index (in line 5, least bidder first, then before ; in line 12, the first maximizer in the printed order). The paper fixes no tie rule, and its claims hold for any.
Added hypotheses: everywhere (the paper says only "a budget "), and, in Lemma 6 only, " or ", which excludes the one-bidder instances where the printed lemma fails. The theorems quantify over every subroutine with the 2-approximation guarantee. The paper's example of such a subroutine (Buchbinder et al.) is randomized, and a deterministic 2-approximation exists (Buchbinder and Feldman 2018). The phase loop runs with fuel . For non-negative submodular this is enough unless , in which case and every statement is trivial.
Out of scope: running time (Lemma 12 and the "polynomial-time" clause) and the incentive properties. The clock-auction property is built into the definition, as every price update is a minimum with the old price. A Lean function is deterministic.
The goal cannot be satisfied trivially. It is stated about the mechanism's actual output for every non-negative submodular and every admissible subroutine, and the approximation compares with every budget-feasible set rather than a supremum. Requiring to be an exact maximizer would weaken the theorem and is not done. Contributions of general lemmas on submodular functions (subadditivity of non-negative submodular functions, telescoping marginal sums along a list) are reusable well beyond this mission.
A portfolio manager who observes side information, the covariate (a market state, a set of signals), wants to choose a portfolio for the asset returns given the current value of that covariate. Estimating the conditional law of given from joint samples is fragile: typically no sample has exactly, and a nearest-neighbour or kernel estimate inherits all the noise of the few samples near . Nguyen, Zhang, Wang, Blanchet, Delage and Ye robustify this decision with optimal transport: they let an adversary perturb the empirical joint distribution within a transport budget and evaluate the portfolio by its worst conditional expected loss over the perturbed distributions. This mission formalizes their main reformulation result for the general case, a fiber of positive radius with a positive mass requirement.
Let and be Polish spaces. The data are samples , , with empirical distribution . Ground costs and give the joint cost , and the optimal transport cost is the least expected cost over couplings of and . The ambiguity set is the ball
The neighbourhood of the observed covariate is , and is the fiber set. For a fixed portfolio the loss is a function , and the quantity of interest is the worst-case conditional expected loss
where is a minimum mass the adversary must leave on the fiber, so that the conditional expectation is well defined.
Three more data enter the result. The minimum radius is the least over with fiber mass at least . The index sets are and . The boundary distances are . The dual set (display (16)) consists of the tuples with , , , , subject to
For , and ,
The theorem turns an infinite-dimensional problem, a supremum over probability measures on of a ratio of integrals, into a program in real variables whose only infinite part is the per-sample supremum . For the losses used in portfolio selection (mean–variance, CVaR) this supremum has a closed form or a conic representation, and the outer minimization over portfolios becomes a single convex program; this is how the paper computes its conditional robust portfolios. It is the most general of the paper's four cases (Figure 1, p. 12); the companion missions of this series treat a singleton fiber () and a zero mass requirement ().
The result is proved in the paper, not formalized anywhere. A machine-checked version requires, and would leave behind, an optimal-transport representation of Wasserstein balls around empirical measures, a Dirac-nominal conic duality for moment problems, and finite-dimensional linear programming duality, none of which is in Mathlib.
The conditional expectation is a ratio, so the problem is not a linear program in and the standard Wasserstein DRO duality does not apply directly. Passing to finitely many sample weights requires that leaving the fiber from a sample inside it costs exactly , which depends on the geometry of the neighbourhood and not only on Assumption 2.4. The two duality steps are of different kinds: an infinite-dimensional one over laws on , where the loss is only measurable, and a finite-dimensional linear program whose strong duality must be certified from . The representation of the ball needs an optimal coupling, which is an existence theorem on Polish spaces.
Fin N with ; samples may repeat.RWPI.SqrtLasso.transportCost, an infimum over couplings of a lower integral of the -valued cost; the ball compares it with ENNReal.ofReal ρ.ModelRiskOT.Duality.extIntegral, in the extended reals. Both sides of the goal are extended reals; the infimum over an empty set is .ofReal never collapses a negative radius; and the supremum ranges exactly over intersected with the mass constraint, not over all measures.A portfolio manager who observes side information, such as a vector of market covariates today, wants a decision that performs well conditionally on that information: the relevant risk is the expected loss of the portfolio given that the covariate equals, or is close to, . Estimating this conditional loss from historical pairs of covariates and returns is fragile, since few or no samples may lie near . Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451, Operations Research 2025) robustify the conditional decision with an optimal-transport ambiguity set: the worst case of the conditional expected loss is taken over all distributions within transport budget of the empirical distribution.
Conditioning makes this worst case delicate. The adversary may move mass away from the conditioning set, and a conditional expectation on a set of probability zero is undefined. Section 4.1 of the paper treats a neighbourhood of positive radius around and requires only that the conditioning set have positive probability. This mission formalizes the result showing that, when the budget is below an explicit threshold , the requirement "positive probability" is automatically "probability at least ", with the value of a small linear program.
Let and be Polish spaces carrying their Borel -algebras, with ground costs and and the separable joint cost . The data are samples , , and the empirical distribution is .
The optimal transport cost is the infimum of over couplings of and , and the ambiguity set is the ball of probability measures on .
The covariate neighbourhood is , and is the fiber set. For a loss (the loss of a fixed portfolio decision), the worst-case conditional loss under a mass requirement is
and problem (12) replaces "" by "".
Two derived quantities organize §4.1. The maximal budget is the least transport cost of a distribution that puts no mass on the fiber. Write and for its complement, and let be the cost from to the boundary . Assumption 2.4 asks that the costs be symmetric, non-negative and continuous, with exactly on the diagonal, that each have a unique projection onto , and that every boundary point be approached from outside the neighbourhood.
For and , let
Then , and for every loss
Proposition 4.3 removes the degenerate constraint "positive probability" from the conditional robust problem whenever the budget is below . The degenerate constraint defines a feasible set that is not closed, and conditional expectations along it can involve divisions by arbitrarily small masses; after the reduction, the problem has a positive, explicitly computable mass requirement , and the finite-dimensional dual reformulation of Theorem 4.4 (which needs a positive mass requirement) applies. Together with Proposition 4.2, which shows that above the worst case degenerates to , it gives a complete picture of the regime , . The LP defining is a fractional knapsack problem, solvable greedily.
The paper proves these results; none of them has a machine-checked proof. The mission produces a formal account of the transport-ball representation (24) on Polish spaces, the closed form of , and the reduction itself. It also records, with explicit counterexamples, where the printed arguments need additional hypotheses (see Formalization scope).
The obvious argument fixes , splits it as , and bounds the cost of the mass that each moves out of the fiber. Two steps resist. The splitting with the exact budget requires an optimal coupling, so attainment of the transport infimum on Polish spaces is needed. And the bound "moving a fraction of sample out of the fiber costs at least " needs the cost of leaving from to equal the boundary cost , which is not implied by continuity of . Identifying the infimal fiber mass with the LP value also requires approximating boundary points from outside the neighbourhood, so the LP minimum is approached but not attained by measures in the ball.
Spaces are Polish with Borel -algebras; is Fin N with ; repeated samples are allowed. The transport cost is the published RWPI.SqrtLasso.transportCost (an infimum over couplings with first marginal and second marginal , lower Lebesgue integrals of a -valued cost); the paper's "min" is not built into it. Expectations of the loss are in the extended reals (published ModelRiskOT.Duality.extIntegral). Worst-case values are suprema in EReal over probability measures. The loss is an arbitrary function , which covers every decision . and are infima (sInf), and is the topological frontier in .
Hypotheses beyond the page, all disclosed in the statements:
BoundaryRegular: the boundary of is nonempty, for the infimum of over is , and for , . It holds for norm distances; without it Proposition 4.1 fails for some continuous costs.The formalization excludes the trivializing readings: no conditional expectation is evaluated at a distribution with zero fiber mass, no Bochner integral of a possibly non-integrable loss is used, a negative cannot enter through ENNReal.ofReal, and the suprema range exactly over the probability measures of satisfying the stated mass constraint. "Equivalent" is formalized as equality of the inner suprema for every loss, which is stronger than equality of the min–max values.
A complete development needs couplings and gluing for finitely supported marginals, existence of optimal couplings for continuous costs on Polish spaces, and finite LP facts (attainment, positivity). The transport-ball representation and the optimal-coupling existence are reusable beyond this mission. Proofs of any milestone, and of the representation (24) in particular, are welcome.
A forecaster who issues a probability distribution for a multivariate quantity, such as the joint demand at several locations or the joint returns of several assets, is often judged not on the whole distribution but on a region it implies: the set of outcomes whose cumulative probability, or smoothed density, exceeds a threshold. Such level sets are the multivariate counterpart of quantiles, and they are used as risk regions and as summaries of joint distributions in management science (Abbas, Budescu and Gu 2010) and in density level set estimation (Cadre 2006). To compare competing level set forecasts against realized data, one needs a consistent scoring function: a loss of a candidate set and an outcome whose expectation under the true distribution is smallest at the true level set. For univariate quantiles the answer is classical (the quantile or pinball loss, Gneiting 2011); for general multivariate level sets, the paper notes, scores had not been studied beyond density level sets and univariate quantiles.
Meng, Taylor, Ben Taieb and Li (Operations Research, 2025) obtain such scores by decomposing their scoring rule for multivariate distributions into an integral, over the threshold , of scores for the level sets of a smoothed density. This mission formalizes that construction: Theorem 2 of the paper.
Write for -dimensional space with Lebesgue measure and the componentwise order ( means for all ). The unknown distribution of the observation is a probability measure on ; the paper writes for its generalized density. Fix a kernel and a nonnegative integrable weight . The smoothed density is the convolution
For (the Heaviside function) it is the multivariate CDF .
The level set of a function is (display (9), p. 12)
A function of a Borel set and a realization is a consistent scoring function for if is minimized at , and strictly consistent if that set is the only minimizer (p. 12). The level set score is (display (11), p. 13)
and the scoring rule of the paper is (display (3), p. 8)
In Lean these are smooth, levelSet, scoreΓ, S', cdf and heaviside in the definition item MultivarScores.LevelSet.Setting.
The paper's Theorem 2 (p. 13) reads:
Let , , and satisfy Assumption 1 in the appendix, and is nonnegative. Let , and let be an arbitrary Borel set. Suppose is finite -a.e. and is integrable. Then the following expression defines a consistent scoring function for the level set : . (11) If is nonzero -a.e. and equals the closure of , it is strictly consistent. Moreover, with , the integral of (11) with respect to is precisely half of the score in (3), i.e., .
For every Borel and every ,
This is the part of Theorem 2 that holds exactly as printed, and it is the goal.
If moreover a.e., , and , the inequality is strict. The null-set condition replaces the printed closure condition (see Formalization scope).
The other milestones are the steps of the paper's proof (pp. 33–34): the per-realization difference (p. 33), the expected difference (19) (p. 34), and two companions: the CDF level set score (13) is consistent for (p. 16), and in dimension one it equals the quantile score up to a term depending only on (Remark 2, p. 17).
Theorem 2 supplies consistent scoring functions for a whole family of multivariate level sets at once, one for each kernel : CDF level sets (from ), density level sets (from ) and lower-partial-moment level sets. It thereby gives a way to rank and compare multivariate region forecasts, and in one dimension recovers the full class of quantile scores (Remark 2). The layer-cake identity explains the relation between a distribution score and its level set scores, generalizing the classical identity (display (10)); the paper relates its CDF level set score to the Vorob'ev quantile scores of Fissler, Frongillo, Hlavinová and Rudloff (2021).
The result is proved in the paper's appendix (pp. 33–34). It has no machine-checked proof that this mission is aware of. Formalizing it fixes the exact integrability conditions under which the expectations exist (the paper states them loosely in Assumption 1), and it repairs the strict consistency clause, whose printed sufficient condition does not imply what the proof uses.
The core of consistency is a sign argument, but every quantity in it is an integral over against or against , and none of them is a priori finite: need not be bounded or integrable, and must be integrable in for the true level set as well as for the candidate , although the paper assumes it only for . Exchanging the - and -integrals therefore needs a product-integrability condition, not pointwise finiteness. The layer-cake milestone requires the layer cake formula for two different measures ( and ), with powers and , followed by an exchange that keeps the sign of the second term; a nonnegative (lower) integral cannot express the difference. The strict clause needs a measure-theoretic condition on the boundary ; a topological condition on closures, as printed, is not enough.
Fin d → ℝ with volume and the Pi order; is any natural number. A distribution is a probability measure P : Measure (E d); every integral is a Bochner integral.MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and relatives in Mathlib/MeasureTheory/Integral/Layercake.lean) and Fubini–Tonelli (integral_prod). A reusable lemma for is welcome; it also serves the companion mission on the scoring rules.Quantile-based risk measures are the regulatory standard in banking and insurance, and Lambda Value-at-Risk (ΛVaR), introduced by Frittelli, Maggis and Peri (2014), generalises Value-at-Risk by letting the confidence level vary with the loss: large losses can be judged at a stricter level than small ones. When several agents (desks of a bank, members of a reinsurance pool, insurer and reinsurer) share one aggregate risk, each measuring their part with their own ΛVaR, the natural question is how the risk should be split to minimise the total measured risk. This is the risk-sharing problem, studied for VaR and Expected Shortfall by Embrechts, Liu and Wang (2018) and for ΛVaR under a common probability by Xia and Hu (2025).
Liu and Schied (2025) treat the same question when the agents disagree about, or are uncertain of, the probability model. Each agent's beliefs are encoded by a capacity, a monotone set function that need not be additive, which covers worst-case and best-case evaluations over a set of probability measures. This mission concerns their Section 6, where allocations are required to be comonotonic: every agent's share increases with the aggregate loss. Comonotonic sharing rules out arrangements in which one agent gains when another loses.
Timeline of the relevant results:
Let be a measurable space and a set of real random variables containing all bounded ones (the paper's examples are the bounded random variables and all random variables). A capacity is a set function that is increasing, with and . It is continuous if whenever . It is atomless if some bounded random variable makes continuous. A probability measure is a continuous capacity.
Let be the set of increasing functions . For and a capacity ,
For constant this is the Choquet quantile .
There are agents. An allocation of is with . It is comonotonic if there are increasing with , and its components have the same sign if no two of them take strictly opposite signs in any state. Write for these allocations and
for the comonotonic inf-convolution. A minimiser is an optimal allocation.
Let and let be continuous capacities.
and , () is optimal for every . 2. If every is constant on , then (11) holds for all . 3. If , the capacities are equal and atomless and the are equal, then (11) holds for all if and only if is constant on .
All three parts are posed as one theorem.
Theorem 4 says that, among comonotonic arrangements, nothing beats handing the whole risk to the agent with the smallest ΛVaR, for any heterogeneous beliefs given by continuous capacities. It extends the single-probability result of Xia and Hu (2025, Theorem 11). The characterisation in part 3 marks the boundary of that conclusion: for risks with negative ΛVaR the one-agent arrangement remains optimal exactly when the confidence level does not vary on the negative half-line. For applications this separates the reinsurance-style problems, where losses are nonnegative and the answer is extreme, from the general case, where it is not.
The result is proved in the preprint and has no machine-checked counterpart. A formal development provides a first Lean treatment of ΛVaR under non-additive set functions and of comonotonic allocations defined through increasing functions of the aggregate, and checks a proof whose printed version has a gap (see Difficulty). The definitions are reusable by the companion missions on the same paper (robust ΛVaR, inf-convolution of ΛVaRs).
The upper bound in (11) is immediate from the one-agent allocation. The lower bound needs the reduction of comonotonic same-sign allocations to splits of the identity, which uses that a family of increasing functions summing to the identity on the range of extends to continuous, -Lipschitz functions on vanishing at . ΛVaR does not commute with , so the second step is a change of variables that moves into the level function. The comparison then holds only where , which depends on the sign of the argument.
For part 2 the printed proof asserts whenever is constant on . That fails when jumps at and vanishes on part of the negative half-line, so the printed step does not prove the claim. The claim itself survives, and a correct argument must handle that case separately. Part 3 needs an explicit risk built from an atomless capacity at which the inf-convolution falls strictly below the minimum, and capacities are not additive, so the usual distributional constructions are unavailable.
Lean namespace LambdaVaRAmb.Comono; one definition file and six theorem files. Conventions:
Set Ω → ℝ with the axioms imposed on measurable sets. ΛVaR, the inf-convolution, sums and minima live in EReal, so and an unbounded-below set gives , as in the paper. "Increasing" is Monotone. Agents are Fin n with , and sums of random variables are pointwise.Trivialising encodings are excluded. Infima are taken in EReal, never as a real sInf that collapses to . No sum in the statements can meet . The admissible set is constrained rather than arbitrary. The hypotheses are satisfiable, since a probability measure is a continuous capacity and constant levels lie in .
Welcome contributions include the reduction to (a reusable fact about comonotonic decompositions), the ΛVaR change-of-variables identity, and the atomless-capacity construction of part 3.
A bidder in repeated first-price auctions faces a learning problem with two kinds of side information. Their private value is a context that changes every round, and the outcome of one bid reveals something about other bids (graph feedback across actions) and about other values (cross learning across contexts). Han, Zhou and Weissman (arXiv:2003.09795v7) abstract this structure into partially ordered contextual bandits and show that, when contexts are iid, an arm-elimination policy has regret (Theorem 5), with no polynomial dependence on the number of contexts or actions.
Theorem 6 of the same paper asks whether this survives when contexts are chosen by an adversary. It does not: with adversarial contexts every policy suffers regret polynomial in . This separation is what forces the paper to look beyond the partially ordered structure for its adversarial-value result (Theorem 2). The lower bound is also of independent interest for contextual bandits with cross learning (Balseiro et al., NeurIPS 2019) and with feedback graphs (Alon et al., COLT 2015).
A stochastic contextual bandit with graph feedback and cross learning (Definition 2, p. 14) has a horizon , contexts , actions , a joint reward law on with means , and a directed graph without self-loops. In round the learner sees a context , picks , nature draws a fresh reward vector , and the learner observes for every context and every . The regret (5) is
The independence number of is the size of a largest set of actions with no edge between any two of them; for a partial order, is the size of a largest set of pairwise incomparable elements.
The instance is a partially ordered contextual bandit (Definition 3, pp. 16–17) if is a DAG equal to its own transitive closure, so that iff or is a partial order, and there is a partial order on contexts with for optimal actions .
A policy chooses from its internal randomness, the contexts and the earlier observations. The context sequence is oblivious: fixed in advance, possibly depending on but not on its random draws.
For integers , , with , and : there is a feedback graph on actions with independence number such that for every policy there are a reward law (making partially ordered with the total order on contexts, ) and contexts with
Because , this is at least , the printed form of Theorem 6, in this regime.
Along the proof (pp. 22–24): the construction is a partially ordered contextual bandit with and independence number ; properties 1–4 of the mean rewards; property 5, the KL divergence of the observed rewards; the regret decomposition (7); the testing lemma (Lemma 13, p. 36)
the self-referential inequality (8)
and the final step .
The theorem separates stochastic from adversarial contexts. Under iid contexts, Theorem 5 gives ; with adversarial contexts, even when , regret must grow like , matching the upper bound of Theorem 4 up to logarithms. For first-price auctions with adversarial values (Remark 2), the bound shows that the partially ordered structure alone cannot give ; the paper's algorithm must use the extra correlation of auction rewards.
The paper proves the theorem in full. As far as we know, none of it has been formalized; in particular, no machine-checked version of a Bayesian multi-hypothesis lower bound for bandits with graph feedback and cross learning exists. A formal proof will produce reusable pieces: Lemma 13 is a general testing inequality; the KL chain rule for adaptively collected bandit observations, with feedback revealed on a graph, is needed for any information-theoretic bandit lower bound; and the interaction model is shared with the paper's upper bounds.
The standard minimax argument for -armed bandits compares two instances that differ in one arm, and the regret follows directly from a testing error. Here that argument fails: feedback graphs and cross learning mean that pulling one arm can reveal everything, and a policy may pay to explore. The proof instead plays a uniform prior over instances and obtains an inequality in which the maximal regret appears on both sides, (8). If the regret is small, the policy has not explored enough to tell the instances apart, which in turn forces large regret. Making this rigorous requires the chain rule of KL divergence over the adaptively chosen observations, the specific ordering of contexts (decreasing over blocks, so early observations say nothing about late optimal actions), and the regime to close the self-referential bound.
Fin M, rounds Fin T (paper index = Lean index + 1). The goal uses actions Fin K; the construction uses Fin M × Fin (α + 1), with the action .Fin M → A → ℝ. Definition 2 requires a probability measure carried by and a graph without self-loops. Means are integrals, and is a supremum over the finite action set.klDiv. In Lemma 13, is read as , so an infinite divergence cannot be truncated to and inflate the right side.Needed infrastructure: Bernoulli product measures and their KL divergence, the KL chain rule for the law of an adaptive interaction, and a Bretagnolle–Huber-type inequality. Contributions of these general lemmas, and of the measurability facts for the interaction, are welcome.
Online marketplaces such as Amazon, Alibaba and JD.com host millions of third-party sellers, many of them small firms without the working capital to pay their suppliers upfront. Two sources of credit compete for them. In trade credit the supplier ships the goods and is paid at the end of the season, bearing the risk that the seller cannot repay. In platform financing the marketplace itself lends the purchase cost to the seller at an interest rate of its choosing, the supplier is paid immediately, and the platform bears the default risk. Platform lending programmes (the Amazon Lending Program, launched in 2011; the financial affiliates of Alibaba and JD.com) put the marketplace in the lender's seat. Supply-chain finance research, from Buzacott and Zhang (2004) to Kouvelis and Zhao (2012), studies who should finance a capital-constrained firm; the platform adds a lender that also earns a commission on the borrower's sales, and the question becomes when lending benefits the platform, its sellers and their suppliers.
Huang, Lai, Wang and Xiao study this question in a stylized supply chain with a random market-clearing price and a limited-liability seller. They obtain closed-form equilibria for both schemes and compare the three parties' profits. This mission concerns the platform's side of that comparison: for which loan rates the platform itself earns more by lending than by leaving credit to the supplier.
The version formalized here is the authors' manuscript posted on SSRN (abstract 4014045), titled Lending to Third-party Sellers with Platform Loan. The paper was published in Management Science in 2024 under the title Platform Financing vs. Trade Credit for Lending to Third-Party Sellers. All page and label references are to the SSRN manuscript.
A supplier produces at unit cost . A seller with no capital orders units and sells all of them at the market-clearing price , where the market size is uniform on with . The platform keeps the share of the revenue and passes to the seller. The supplier's and the platform's capital cost is the risk-free rate , and . The seller has limited liability: if her revenue does not cover what she owes, she hands over all of it.
Each scheme is a two-stage Stackelberg game solved by backward induction: a profile is a price and an order rule , and a subgame-perfect equilibrium has the seller best-responding at every price and the supplier choosing the price that maximizes his profit given that rule. and denote the platform's profits along the equilibrium paths.
Let
For :
Proposition 7 identifies two distinct reasons a platform lends. When production is cheap () the platform gains by charging slightly more than its capital cost, earning interest while sales barely fall. When production is expensive () it gains by subsidizing the loan below : the lower rate raises the seller's order enough that the larger commission outweighs the interest forgone. Combined with the paper's Proposition 6, which shows that rates below can make both seller and supplier better off at low uncertainty, the second case is a regime in which platform financing benefits all three parties. The paper's §5 uses the same comparison to derive the platform's optimal rate.
The result is proved in the manuscript; it has not been machine-checked. A formalization adds three things. It certifies the closed-form equilibria of both games under limited liability, including uniqueness up to the paper's tie-breaking conventions. It verifies the radical algebra behind and the sign of on each side of . And it records the model precisely enough for the companion missions of this paper (seller and supplier comparisons; the endogenous rate) to be checked against the same objects.
The comparison itself is algebra once (9) and (10) are known, and an obvious approach would start from those formulas. The difficulty is that they are statements about equilibria of games, not definitions. Each requires maximizing an expectation of a positive part (the seller) or of a minimum (the supplier, the platform) over an interval in which default can or cannot occur. The seller's objective is piecewise polynomial in with a kink where default first becomes possible, and global optimality, not just stationarity, must be shown. The supplier's problem then compares two local optima whose ordering changes at (trade credit) or (platform financing). On top of this the goal requires the threshold facts and the positivity of a quadratic in on the stated intervals, as well as checking that every rate in the intervals keeps the platform-financing equilibrium in its no-default branch ().
The expectation over is the normalized interval integral ; all integrands are continuous. Payoffs are stated with the literal revenue , and is the expectation , not the page's closed form (the two agree). A profile is a price together with the seller's whole order rule. Equilibria carry two tie-breaks, both the paper's own conventions: an indifferent seller with no profitable order orders zero (proofs of Propositions 1–2), and the supplier's equilibrium price is the least optimal one, which places and in the low-price branch as the propositions do. The goal quantifies over a trade-credit equilibrium and over a family of platform-financing equilibria, one for each rate satisfying conditions (ii)–(iii) of the Appendix (, ).
Standing assumptions and pins: reads the page's assumption that the price is always positive; is forced by ; and read "production cost" and "risk-free rate". Lemmas 1–2 add , outside which every order earns zero. Corrected slips: the branch of Proposition 1 on p. 11 omits a factor under the root, and the formalization uses the proof's form (p. 31). The proof of Proposition 7 writes where the statement has ; the statement's form is used.
The page says only "there exist two thresholds and ", which an empty interval satisfies trivially. The goal therefore names the proof's thresholds and includes and in the two cases. Stating the goal about the closed forms (9)–(10) instead of equilibrium profits would also trivialize it; these appear only as milestones.
A complete development needs: optimization of piecewise-polynomial expectations on an interval (reusable for any newsvendor-type problem with a uniform demand), the backward-induction equilibria of both games, and real-radical inequalities. Proofs of any milestone, and of the sanity facts , are welcome.
In a first-price auction the highest bidder wins and pays her own bid. Display advertising moved to first-price auctions around 2019, and a bidder who participates in millions of them faces a learning problem: at each round she sees a private value for the item, bids , and wins when is at least the highest other bid (HOB) , earning . Since the HOB is unknown, she must learn how much to shade her bid.
Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research, 2025) show that when the HOBs are iid draws from an unknown distribution, a bidder can achieve regret against the oracle that knows the distribution, whether the values are iid or chosen by an oblivious adversary, and with only censored feedback. Their §2.2 justifies the iid assumption by the size of the bidder population, and notes that learning "could become impossible even when the iid assumption is only slightly violated". Section 5.2 makes this precise. This mission formalizes that impossibility result, Theorem 8.
Fix a horizon . Values form an oblivious sequence, fixed in advance. Fix two probability laws on and a threshold . The HOBs are independent across rounds with
Feedback is full information: is revealed at the end of round . The laws are known to the bidder; only is not.
The payoff of bid against HOB at value is (ties are won). For a law of the HOB with CDF , the expected reward is , and the oracle reward is .
A policy draws internal randomness once and bids . Its expected regret is
with if and otherwise: the oracle knows and bids optimally at every round.
There are an absolute constant and laws on such that for every and every policy there are a threshold and values with
The constant is existential, which is the paper's ; the value obtained in the paper's argument is not hard-coded.
The paper's argument consists of a hard family indexed by signs , with thresholds and values , , and four displayed claims:
and the Bayesian bound: averaged over uniform , every policy has expected regret at least .
The result. The upper bounds of the paper rely on the HOBs being iid and independent of the bidder's value. Theorem 8 shows that this cannot be relaxed to a mild form of dependence: one threshold, two known laws and full-information feedback already force linear regret against the per-round oracle. The paper concludes that a weaker benchmark is needed once HOBs may depend on values, and leaves that benchmark open.
Formalizing it. The theorem is proved in the paper, on one page; it is not known to be machine-checked. A formal proof pins down the quantifier order (the constant and the laws chosen before the policy, the threshold and values after it), the policy class (randomized, full information) and the treatment of ties, and it provides a reusable model of non-anticipating randomized bidding policies with full-information feedback.
The obvious attempt is to fix a threshold and values and argue that the bidder cannot know on which side of each falls. For any fixed instance this fails: a policy can be tuned to that instance and bid optimally, with zero regret. The lower bound must therefore pass through an average over a family of instances. The family has to make the side of the threshold at round independent of everything the bidder has seen up to round , including the past HOBs, which in full information reveal the past sides exactly. The dyadic construction does this. The formal difficulty is the bookkeeping: expressing the expected regret of an arbitrary randomized policy as an integral over its internal randomness and the HOBs, and exchanging the average over with that integral so that the conditional uniformity of can be used.
Fin T; Lean round is the paper's round .Measure ℝ, with probability and support in required of the existential witnesses . The CDF is . Atoms are allowed, as in the paper; the construction uses point masses.A formalization in which the threshold or the values are chosen before the policy, the bid reads , the expected payoff is not integrable, or the oracle bids a fixed price, is a different and easier statement; all four are excluded by the definitions above.
Contributions welcome: proofs of the four displayed claims (elementary real analysis on dyadic sums and on point masses), the Bayesian bound (the measure-theoretic core), and the step from the Bayesian bound to the goal. The policy and regret definitions are reusable for other full-information lower bounds in this series.
The Lightning Network is a payment layer built on top of Bitcoin. Two parties lock funds in a payment channel and then exchange payments off the blockchain, settling on-chain only when the channel closes. Payments between parties without a direct channel are routed along paths of channels. Locked funds are idle capital, and the amount a channel needs grows with the flow it carries, so the topology of the network (which channels exist and what each carries) determines what it costs to support a given pattern of payments.
Guasoni, Huberman and Shikhelman (SSRN 4439190) study this cost under a general channel cost function, building on their earlier analysis of the cost of a single bilateral channel ([GHS22]). Their §3.3 asks how much the globally cheapest network can cost, and how far a simple design is from it. A natural design is the star: every participant opens one channel to a common hub. Corollary 3.11 of the paper shows that a star is in general not cost-minimizing; Corollary 3.12, the goal of this mission, shows that it is never worse than the optimum by more than a factor of two. For symmetric channels (zero net flows) the factor-two bound was known from Sali and Zohar ([SZ20]); the present result covers arbitrary net flows and any cost function satisfying four axioms.
Let be a finite set of nodes. A payment flow is a vector of reals with
since every payment is sent by one node and received by another.
A Lightning Network (LN) on is an anti-symmetric real matrix : is the net flow from to in the channel between them, , and means that there is no channel. The LN supports if for every node .
A channel cost function is a map with
The cost of an LN is , the sum of its channel costs. The minimal cost of supporting is
For a hub , the star is the LN in which each node has a single channel, to , carrying its flow: , , and all other entries are .
In Lean these are IsLN, Supports, IsChannelCost, cost, cmin and star in the namespace LNTopology.StarBound.
For every channel cost function , every flow with , and every hub ,
For nonempty ,
The result. Computing a cost-minimizing network for a general concave-type channel cost is a combinatorial optimization problem with no known closed form; Theorem 3.10 brackets its value by two explicit sums, and Corollary 3.12 turns that bracket into a guarantee for a design that needs no optimization at all. A hub-and-spoke network, the structure that large Lightning Network routing nodes tend to create in practice, thus pays at most twice the optimal locked-capital cost, whatever the flow pattern and whatever the cost function within the axioms. The lower bound of Theorem 3.10 is also a certificate: any supporting network whose cost is within a given factor of is within that factor of optimal.
Formalizing it. The paper's argument is short, but it assumes that a cost-minimizing network exists and uses its bipartite structure (Theorem 3.1). For a cost function that is not continuous, the minimum need not be attained. The formal development replaces the minimizer by an infimum and proves the lower bound for every supporting network, which removes that gap. It also fixes the hub choice in the proof of the upper bound (see the Formalization scope). To our knowledge, no part of this paper has a machine-checked proof.
The upper bound and the inequality (16) are bookkeeping. The substantive step is the lower bound: every supporting network costs at least the total cost of the payers' flows. The obvious argument applies subadditivity at each payer to the channels incident to it, but those channels carry flows of both signs, and channels between two payers are incident to both of them, so summing over payers can count the same channel twice. Working only with a cost-minimizing network avoids the double count by structure, but a minimizer may not exist. The lower bound must therefore be proved for an arbitrary anti-symmetric supporting matrix, using only (MO), (SY), (CI) and (SA).
V with decidable equality, instead of . V nonempty where a maximum over nodes appears (Theorem 3.10, (16)).V is needed.sInf) over LNs on the same node set V, not a minimum, because is not assumed continuous. Every statement involving it assumes ; without that hypothesis no network supports and is Lean's junk value .Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (not or a power), flows are arbitrary (not the symmetric case of [SZ20]), ranges over all LNs on V (not over stars, trees or bipartite networks), the bound holds for every hub (not one chosen hub), and is kept so that is never a junk value.
The development needs only finite sums and sInf on from Mathlib. A reusable by-product is the many-term subadditivity for a symmetric, monotone, subadditive with , which applies to any concave-type cost on signed quantities. Contributions are welcome on each milestone independently, in particular on the lower bound (14)–(15).
Retail prices are not judged in isolation. Consumers compare a posted price with a reference price formed from the prices they have seen before, and they react to a price below the reference (a perceived gain) differently from a price above it (a perceived loss). Empirical marketing studies of such reference effects include Briesch et al. (1997), and the dynamic-pricing literature asks what a seller facing them should do over time: keep prices constant, or alternate between high and low prices.
For a single product with demand linear in price this question has a classical answer. Popescu and Wu (2007, Operations Research) showed that loss aversion leads optimal prices to settle at a constant, and that sensitivity to gains favours cyclic, "high–low" pricing; Hu, Chen and Hu (2016) characterised optimal cyclic policies in a special gain-seeking case. Guo, Jiang and Shen (2025, Manufacturing & Service Operations Management) revisit the question for several substitutable products under multinomial-logit (MNL) demand, the standard discrete-choice model of retail, where earlier techniques no longer apply. This mission formalizes one of their structural results: a single gain-seeking product rules out a constant optimal price.
A seller offers products over periods . Product has an intrinsic utility , a price sensitivity , and reference-price sensitivities (to gains) and (to losses). Given prices and reference prices , the utility of product is
and the MNL purchase probability and the single-period revenue are
Product is loss-averse if , loss-neutral if , and gain-seeking if ; denotes the set of gain-seeking products.
Prices and reference prices lie in the box , with a price ceiling . Reference prices follow exponential smoothing with memory :
With discount factor , the optimal value from an initial reference price is
Throughout, the paper assumes , where is the unique root of its equation (9); this keeps the single-period problem unconstrained by the ceiling. A price vector is an optimal steady state when the optimal policy maps the reference price to the price ; equivalently, the constant path started from is optimal, which reads
If , the optimal pricing policy admits no steady state:
Only one product needs to be gain-seeking; the others are unrestricted. No condition on or beyond , is imposed.
If , and , then, whatever the types of the products, there is such that for every ceiling the optimal policy admits no steady state in .
Theorem 4 separates two regimes of reference-dependent pricing. Without gain-seeking products the paper shows elsewhere (Theorems 5–6) that optimal steady states can exist and describes where they lie; Theorem 4 shows that one gain-seeking product anywhere in the assortment destroys every steady state, so the optimal prices of the whole assortment keep moving. Together with the corresponding statement for the myopic policy (Theorem 3), it says that with gain-seeking consumers both the myopic and the optimal policies are cyclic in the long run, the multi-product logit analogue of Popescu and Wu's single-product finding. Proposition 3 explains the role of the price ceiling: without one, cyclic pricing becomes optimal for any product with positive gain sensitivity.
Both results are proved in the paper's online supplement (Appendices C.2, C.3), which is not part of the source file used for this mission; neither has a machine-checked proof. Formalizing them requires the value function of an infinite-horizon problem with a continuous vector state, and a formal handle on how responds to perturbations of a price path, infrastructure that other reference-price missions can reuse.
The obvious attempt is local: at a candidate steady state , perturb the constant path and show the revenue increases. The difficulty is that is not differentiable at : the kink in is exactly at the steady state, and the one-sided derivatives of involve on one side and on the other. A first-order argument in one direction is therefore not available, and the comparison has to be made against , a supremum over infinite price sequences, not against the myopic revenue. The MNL coupling adds a further layer: changing the price of the gain-seeking product moves the market shares of every other product, whose own reference effects may be of any type. Single-product arguments for linear demand (Popescu and Wu 2007) rely on assumptions that the logit model violates, as the paper notes on p. 20–21.
Products are indexed by Fin n (the paper's product is index ). The parameters are functions a b cp cm : Fin n → ℝ; the standing assumptions , , , , are hypotheses of each theorem. The market shares are defined directly by the MNL formula; the Gumbel random-utility derivation is not formalized. is optValue, the real supremum over all sequences in of the discounted revenue (a tsum); the family is nonempty and bounded by , so this is a genuine supremum. The paper writes the problem over stationary policies and uses the Bellman equation (6); for this deterministic problem with continuous revenue on a compact box the two values coincide.
The ceiling assumption is CeilingOK: some root of (9) lies below . The goal carries it; Proposition 3 does not, because it holds automatically for large and is absorbed into the threshold.
An optimal steady state is IsOptSteadyState x: and . Optimal stationary policies need not be unique and the paper fixes none, so this sequence form, under which the theorem holds for every optimal policy, is used instead of a fixed point of a chosen policy. Stating the goal about the myopic policy, about one particular policy, or for outside the box would trivialize it; the formal statement quantifies over every and compares with , the supremum over all admissible sequences.
A complete development needs the value function, its finiteness and the Bellman equation (6), and a perturbation argument along the kink. Contributions welcome: the Bellman equation for optValue, monotonicity and continuity of , and either goal.
Networks observed over time, such as communication graphs, contact networks and financial exposure graphs, often change structure abruptly. Change-point detection asks whether the law of the network changed during the observation window. In practice not every pair of nodes is observed at every time: links are missing because of sampling, privacy or measurement failure. Enikeeva and Klopp (arXiv:2106.14470, published in Operations Research, 2025) give the minimax detection boundary for this problem in a sparse inhomogeneous random graph model with missing links, for a change at a known time and at an unknown time.
This mission formalizes the upper bound at a known time (their Theorem 1): a test based on the spectral norm of a matrix-valued CUSUM statistic has level and type II error at most as soon as the change is a constant multiple of plus a logarithmic term. The companion missions of this series formalize the matching lower bound (Theorem 2) and the unknown-time test (Theorem 3).
There are vertices and snapshots. At time the network has a symmetric, zero-diagonal connection-probability matrix , and each pair is sampled independently with probability , where the sampling matrix is symmetric with . What is observed is , symmetric with zero diagonal, whose entries , , are independent Bernoulli variables with success probability , independent over ; is the entrywise product.
The column-wise norm measures the largest expected observed degree. The null class is
A change at time replaces by after time . With and the spectral norm , the change-point energy is , and the alternative class collects the pairs in whose energy is at least .
A test maps the data to . Its type I error is the supremum over the null class of the probability of rejecting, and its type II error is the supremum over of the probability of accepting.
The Matrix CUSUM is
and the test at the known time is
with and a constant depending only on .
For every there are constants and , depending only on , such that for all , , and : if
then and . The constants are existential and are not pinned to particular values; the statement asserts the shape of the boundary.
Theorem 1 is the upper half of the minimax detection boundary for a change at a known time. Together with Theorem 2 of the same paper (a lower bound of order ) it shows that, up to the logarithmic term, the CUSUM test in spectral norm is rate-optimal, and that missing links enter only through the observed degree bound . The same noise bound (Lemma 12) drives the unknown-time test of Theorem 3.
The result is proved in the paper; no machine-checked version exists. Formalizing it produces a checked finite-sample statement with explicit leading constant , a reusable formal Bernoulli network model with missing links, and, through Proposition 11, a formal statement of the Bandeira–van Handel tail bound, which is used well beyond change-point problems. The printed proof of Lemma 12 applies Proposition 11 after conditioning on the event , which destroys centring and independence; a complete proof needs a truncation argument that the paper does not give.
Under the null the CUSUM is pure noise, so both errors reduce to a high-probability bound on whose leading term is exactly after rescaling. Matrix Bernstein inequalities give a bound with an extra factor on the leading term, which is too weak for the stated threshold; the sharp constant requires the Bandeira–van Handel inequality, whose proof goes through moment comparisons for random matrices with non-identically distributed entries. The entries of are themselves sums over time with coefficients up to order in aggregate, so the boundedness hypothesis of Proposition 11 does not hold directly and must be recovered with probability bounds. Finally, the level and the power must hold for the same threshold constant , uniformly in , , and the parameters.
An observation is a function from the snapshots and the pairs to Booleans; time is 0-based in Lean (snapshot is the paper's ). The latent adjacency and sampling matrices are integrated out: only is modelled, by its exact product-Bernoulli law, and probabilities are finite sums over the finite observation space, so every test is measurable. Tests are Boolean-valued (true rejects). The sampling class carries the paper's standing assumptions and . Errors are real suprema over sets contained in ; an empty alternative class has type II error . The spectral norm is the published HighDimProb.RandomMatrices.matrixOpNorm. Proposition 11 alone uses measure theory, with independence of the entries on and above the diagonal and an added (implicit) .
Disclosed readings: (24) prints , which is read as as in the proof; Lemma 12's matrices are the symmetric, zero-diagonal centred observations of the model; Lemmas 3 and 4 take " is a constant of Lemma 12" (with ) as a hypothesis, stated as a predicate. The goal does not assume that predicate: it asserts the existence of and , both chosen before , , , , , and , so neither constant can be tuned to the instance, and tests range over all functions of the data. Choosing huge constants does not trivialize the goal, since for large the energy condition is met by nonempty alternatives that the test must detect.
The development needs: the product-Bernoulli law of the network, the Matrix CUSUM algebra, the Bandeira–van Handel inequality, and a truncation argument for Lemma 12. The Setting and Proposition 11 are reusable for the unknown-time test and for spectral methods on random graphs. Proofs of any milestone, and alternative routes to Lemma 12, are welcome.
Linear opinion models describe each individual's opinion as a weighted average of the opinions of the people they listen to, of an outside signal, and of their own previous opinion. The model goes back to DeGroot (DeGroot 1974) and Friedkin–Johnsen, and its basic questions are when a population reaches consensus and when it polarizes. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) study it on large directed random graphs with vertex attributes, where each vertex also receives a stream of media signals. Their Theorem 2 shows that the opinion of a typical vertex converges, as the graph grows, to a random variable defined on the graph's local limit. When that local limit is a marked Galton–Watson tree, becomes explicit enough that its mean and variance can be written in closed form, and the variance formula is what the paper uses to say when consensus happens.
This mission formalizes those closed-form moments in the no-memory case, where an individual's new opinion does not depend on their own previous opinion.
The tree. Nodes carry Ulam–Harris labels: the root is , and the children of a node are (in the tree, the children of are its inbound neighbours). Each node has a mark , which determines its in-degree , the weights it puts on its inbound neighbours, and an internal opinion . Two parameters , with fix the proportions: if , then . The tree is a delayed marked Galton–Watson tree: the marks are independent, and all marks except the root's are identically distributed.
Signals. Each node receives media signals , , conditionally i.i.d. given its mark and conditionally independent across nodes. The external signal is
so a vertex with inbound neighbours gives weight to the media and to its neighbours, and a vertex without them falls back on its internal opinion.
Dynamics. Opinions evolve by
With the operator , the stationary root opinion is
The no-memory case is . In that case , where the subtree opinions are i.i.d. copies of the endogenous solution of the smoothing transform . The moments are expressed through (a non-root node) and (the root).
If and , then
The result. The variance formula identifies consensus with small media variance: the weights enter only through the second moments , so consensus is possible for any network structure as long as has small variance. The conditional formulas of Proposition 5 separate the part of the opinion explained by the vertex's own attributes from the part contributed by the network, which is how the paper describes polarization: individuals with similar attributes end with similar opinions when is small. The no-memory formulas are also the comparison point for the general case (Proposition 6 of the paper, a separate mission of this series).
The formalization. The results are proved in the paper; none is machine-checked. A formal development produces a reusable encoding of marked Galton–Watson trees with i.i.d. marks and signals, the expansion of powers of the averaging operator over the generations of a tree, and the moment computation for the endogenous solution of the linear smoothing transform, a fixed-point equation that recurs in the study of branching processes and of ranking algorithms such as PageRank on random graphs.
The moment identities are short once Remark 6 is available. The work is in making Remark 6 precise: the subtree opinions are infinite series over random subtrees, and the proof needs them to be measurable, mutually independent, identically distributed, and independent of the root's mark and signal. That independence comes from the disjointness of the label sets they read, together with the independence of all marks and all uniform variables, and it must be carried through a random in-degree and random weights. The conditional variance step then requires conditional independence given of a random number of summands. Simply invoking the law of total variance is not enough: computing from the fixed-point equation needs , which here follows from boundedness, .
Labels are List ℕ with 0-based children: the paper's node is [0] and its -th child of is i ++ [j-1]. Marks live in an arbitrary measurable space and are read through measurable maps giving , , . The signals are written with i.i.d. uniform independent of the marks; this produces exactly the paper's conditional i.i.d. structure (take the quantile function), and every statement concerns laws. Signals are indexed by time ; and are taken at , as their laws do not depend on . The relative path weights are products along the path, never quotients, which removes the paper's convention for .
The paper states Propositions 3–5 under "the assumptions of Theorem 2" with a tree as local limit. Those assumptions only serve to identify with the typical opinion of a large graph; the statements and proofs concern on the limit tree. The Lean statements are therefore made on the tree, under the Section 5 standing assumptions above, without a graph sequence. is the series .
Conditional expectations and variances given are Mathlib's condExp and condVar with respect to the σ-algebra generated by the root's mark, and the conditional statements are equalities almost everywhere, not pointwise. No trivializing reading is available: every series is absolutely summable for every outcome under the standing assumptions, every variable is bounded by , so Lean's junk values for a non-summable tsum, a non-integrable integral or a non- variance never apply, and , so the division is genuine. The standing assumptions are satisfiable together with and (a path tree with uniform signals). The hypotheses are used: without them the term enters at vertices with no inbound neighbours and the formulas change.
Needed infrastructure: independence of functions of disjoint blocks of an independent family, measurability of series over random finite generations, conditional variance of conditionally independent sums. Contributions on each milestone, on general lemmas for marked Galton–Watson trees, and alternative proofs are welcome.
Tele-driving separates a ride-hailing driver from the vehicle: a remote driver operates a car over a wireless link, and on finishing a trip can immediately take control of another car anywhere in the service region. Several companies have run pilots of this model; Benjaafar, Wang and Yang cite Vay's car-sharing service operated by tele-drivers and Halo's remotely operated robo-taxi pilot with T-Mobile. A platform with remote drivers can therefore hold more vehicles than drivers. The practical question is how many drivers such a platform needs.
Benjaafar, Wang and Yang (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687) model the system as a loss system with a state-dependent service rate and compare a fleet with remote drivers to one with a driver in every vehicle (). This mission formalizes their answer for large markets that have many vehicles relative to demand (the supply-rich regime): asymptotically, a fraction of the fleet size suffices, where measures how much the fleet exceeds the offered load. All page numbers refer to the SSRN working paper, version of 1 June 2023, which is the source of this mission.
Customers arrive as a Poisson process of rate . The platform has vehicles and remote drivers. When customers are being served, trips are completed at total rate , where the service rate accounts for the pick-up time (which shrinks as more idle vehicles are available) and the trip time. A customer arriving while all drivers are busy is lost. With
the number of customers in service is a birth–death process on with stationary distribution
The service level, the long-run fraction of demand served, is .
For the asymptotic analysis the paper uses the service rate of Besbes et al.,
where is the mean trip time and the mean pick-up time with idle vehicles. The fleet grows with demand as for a constant ; the offered load is , so is the ratio of fleet size to offered load. The supply-rich regime is .
For the rate (4) and , the equation has a unique root in ; to its left (the chain drifts upward), to its right . For a tolerance the paper defines
the smallest number of remote drivers whose service level is within of that of a fleet with one driver per vehicle.
For and every ,
The bound does not depend on , and since it says that a large supply-rich system can be run with at most about half as many drivers as vehicles.
The result. Theorem 2.C quantifies the labour saving of tele-driving in markets where vehicles are plentiful. A conventional platform needs one driver per vehicle; a remote-driver platform with vehicles needs only about drivers, essentially the offered load, while losing at most of service level. Together with Theorems 2.A and 2.B of the same paper (the supply-limited and intermediate regimes), it gives a complete asymptotic picture of when pooling drivers across vehicles pays off: in the supply-rich regime, the gain appears as fewer drivers rather than as a higher service level. Footnote 14 strengthens this: the service level with drivers matches the full-staffing service level in the limit.
Formalizing it. The result is proved on paper in Appendix D.3; it has no machine-checked proof. The formalization adds a precise reading of the limit statements (the range of the minimum defining , the meaning of "small ") and a verified account of the concentration of a birth–death distribution with a state-dependent rate, in the form of Lemma 5. The same model underlies four sibling missions on this paper.
The obvious first idea, comparing with the Erlang loss formula for a constant service rate, does not apply: under (4) the service rate depends on the state through the pick-up time, so the stationary weights are not Poisson probabilities and their tails have no closed form. The quantities that govern the answer are defined only implicitly: the critical point solves , and its explicit expression (17) involves the arccosine of a cubic's coefficients, which is unusable for estimates. The statements also take a limit in which the number of states, the root and the floors all move together, so any bound on the stationary distribution must hold uniformly along this family rather than for a fixed chain. Finally, is a minimum over integers of a difference of service levels, and the goal concerns its growth rate relative to , not a single system.
The Lean development lives in the namespace TeleDriving.AsymRich.
rho mu lam m q is (1) with real; piMN mu lam m n q and SL mu lam m n are (2)–(3) and the service level, with natural; muBesbes s is the rate (4); mLam alpha s lam is as a natural-number floor. The shared Model file also contains the paper's Assumptions 1–2, its size restriction, the regime predicates and the maximal service-level ratio, which this mission does not use.nStar) is the minimum over , a set that contains when and ; the paper leaves this range implicit.Filter.Tendsto along atTop on .The goal carries no hypothesis on , , or : its only assumptions are , and , so it cannot be discharged by an assumption that makes the minimum small by fiat. A complete development needs elementary real analysis of the rate (4) (concavity of ), estimates for products of along integer ranges, and asymptotics with floors; the concentration estimate for birth–death chains with state-dependent rates is reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.
In a conventional ride-hailing system every vehicle needs its own driver. Tele-driving, in which a vehicle is driven by a remote operator over a network, separates the two: a pool of remote drivers can serve a fleet of vehicles, each driver taking control of an idle vehicle near the next customer. Fewer drivers mean lower labor cost, but also fewer simultaneous trips; more vehicles mean shorter pick-up legs. Benjaafar, Wang and Yang (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687) model this trade-off as a loss system with a state-dependent service rate and ask when it pays to have fewer drivers than vehicles. This mission takes its asymptotic answer for markets that are neither short of vehicles nor flush with them.
Customers arrive as a Poisson process of rate . With vehicles and customers in service, each customer is served at rate : the more vehicles are busy, the farther the nearest idle vehicle, and the slower a trip completes. A customer who finds all drivers busy is lost. The number of customers in service is then a birth–death process on with birth rate and death rate . With the load (equation (1) of the paper), its stationary distribution is
(equations (2)–(3)), and the service level, the long-run fraction of demand served, is .
The asymptotic results use the service rate of Besbes, Castro and Lobel, equation (4):
where is the expected trip time between two uniformly drawn points of the service region and the pick-up time with idle vehicles. The fleet grows in proportion to demand, for a fixed . For this rate the equation has, in the intermediate regime (equation (14)), exactly two roots in , and strictly between them. For this regime is for large .
For ,
Theorem 2.B is the middle of the paper's three asymptotic results. In the supply-limited regime , Theorem 2.A says that choosing the number of drivers optimally improves the service level by a factor of at least ; in the supply-rich regime , Theorem 2.C bounds the fraction of drivers needed to keep the full service level. Theorem 2.B closes the gap: in a large intermediate market the system with one driver per vehicle is already asymptotically as good as the best system with fewer drivers, so the benefit of tele-driving there is cost, not service. The mechanism is that the stationary distribution with is bimodal, and the mass of the congested mode at becomes negligible compared with the mode at .
The result is proved in the paper (App. D.2). It has no machine-checked proof; this mission formalizes the statement and the steps of the published proof, with the root characterization of App. D made explicit.
The ratio of service levels is at least one (take ) and at most , so everything rests on showing that the loss probability of the full system vanishes. The obvious bound fails: the loads exceed one both below and above , so the stationary distribution is not monotone, and the product of loads from the lower mode to mixes factors above and below one. What is needed is quantitative control of both roots as : stays within a bounded distance of , while grows linearly in with loads bounded away from one in between. The roots have no simple closed form; the paper's expressions (17)–(18) involve a cubic and an arccosine.
All objects are defined in one definitions module, TeleDriving.AsymIntermediate.Model, shared verbatim (up to the namespace) with the other four missions of the series. The service rate is a function ; is evaluated at real ; and are the closed forms (2)–(3) rather than a stationary-distribution predicate. is the natural-number floor , and along the reals. The maximum over is a supremum over a finite index set; its value at is and irrelevant because . Limits superior below infinity are stated as "bounded for all large "; divergence to infinity as Tendsto … atTop atTop.
Standing hypotheses: and . The roots in Steps (i)–(ii) and the reduction are functions of characterized only for all sufficiently large by and ; by milestone 1 they then coincide with the paper's . A characterization required for every would be unsatisfiable for small and make those items vacuous; it is ruled out. The goal theorem does not mention the roots and assumes nothing about or . Milestone 1 adds the hypothesis , which the paper's derivation uses tacitly (it places the maximizer of its auxiliary function inside ) and without which the claim fails for small .
The development needs elementary real analysis: concavity of , asymptotics of , and estimates on finite products. No probability theory beyond the closed forms is required. The root analysis of milestone 1 is reusable for the supply-limited and supply-rich missions of the series. Proofs of the milestones, alternative arguments for the goal, and a formal treatment of the closed forms (17)–(18) are welcome. The source is the 2023 SSRN working paper; theorem numbers are those of that version.
A seller with one item faces buyers whose valuations she does not know, not even in distribution. Prior-independent mechanism design asks which selling mechanism performs well against every distribution in a given class, rather than against one known prior. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) measure performance by regret: the expected gap between the highest valuation, which a seller who knew the valuations could extract, and the revenue actually collected. They solve the resulting minimax problem for several classes of joint distributions: i.i.d., exchangeable and affiliated, mixtures of i.i.d., exchangeable, and arbitrary.
This mission formalizes the last two cases. The answer is that the minimax regret against exchangeable or arbitrary joint valuations is for every number of buyers , so competition among buyers does not help the seller unless Nature's power is restricted.
Timeline. Bergemann and Schlag (2008) solved the one-buyer regret problem: the optimal mechanism is a randomized posted price and the minimax regret is . Koçyiğit, Kuhn and Rujeerapaiboon (2020; doi:10.1287/ijoc.2022.0275) showed, for several bidders and several items, that with arbitrary joint distributions the minimax regret problem reduces to the one-bidder case, so the value does not improve with . Anunrojwong, Balseiro and Besbes (2022–2024, Proposition 4) recover this within their framework, show that the worst case can be taken exchangeable, and identify the optimal mechanism as a second-price auction with a random reserve.
There are buyers with valuations in the type cube . A mechanism maps reported valuations to allocation probabilities and payments . The class of DSIC mechanisms consists of those satisfying, on : individual rationality (IR) ; dominant-strategy incentive compatibility (IC), truthful reporting is optimal for each buyer whatever the others report; and the allocation constraint (AC) .
Write and for the highest and second-highest valuation. The regret of against a joint law on is
and the minimax regret over a class is . Here is the class of all distributions on , and the exchangeable ones, invariant under every permutation of the buyers.
A second-price auction with random reserve draws a reserve , gives the item to a highest bidder if her bid is at least , and charges her . Proposition 4 uses the reserve CDF on ( below ), and the isorevenue law on , with CDF on and an atom of mass at . Nature's candidate picks a buyer uniformly at random, gives her an isorevenue value and gives everyone else value .
With and , for every and ,
is exchangeable, and
The result. Proposition 4 gives the exact minimax regret and an explicit saddle point for the two largest distribution classes of the paper. The value is independent of , in contrast with the i.i.d. class, where the minimax regret decreases in (Theorem 1 of the same paper). Together with the other propositions it shows precisely how much structure Nature must be denied before additional buyers reduce the seller's regret. The worst case being exchangeable shows that symmetry alone does not help.
Formalizing it. The result is proved on paper; it is not formalized anywhere to our knowledge. A formalization produces machine-checked versions of: dominant-strategy incentive compatibility of the second-price auction with random reserve; the pointwise regret identity for that auction; a revenue identity for arbitrary DSIC mechanisms under a mixture of one-buyer laws, which rests on Myerson's payment characterization; and a minimax value computed over all DSIC mechanisms and all distributions. Each of these is reusable by the sister missions on i.i.d., affiliated and fixed-reserve settings.
The minimax problem ranges over all DSIC mechanisms, an infinite-dimensional and unstructured class, and over all joint distributions. The upper bound needs only one mechanism, but the lower bound must hold against every DSIC mechanism, including randomized ones whose allocation is not of auction form; the step from incentive compatibility to an explicit revenue formula along the line is where the work lies. Myerson's payment characterization is quoted by the paper without proof and must be established here for mechanisms that are incentive compatible only on . A second obstacle is measure-theoretic: the regret is an integral of an arbitrary mechanism's payments against an arbitrary law, so its finiteness and the interchange of expectation with the reserve randomization must be justified. The tempting shortcut of restricting Nature to i.i.d. laws gives a different, smaller value.
Lean represents valuations as Fin n → ℝ and laws as measures on that space; is the set of probability measures giving the complement of measure zero, and those also invariant under for every permutation . (IR), (IC), (AC) are imposed on , with misreports in . Two hypotheses are added to the class and disclosed in every statement: allocation and payment functions are measurable, and payments are bounded on , so that the regret is a genuine expectation. Ties for the highest bid are broken towards the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule). is when . The minimax regret is a real infimum of real suprema; for DSIC mechanisms the regrets lie in a bounded interval and both index sets are nonempty, so these are not junk values. The reserve law and the isorevenue law are given through their CDFs, and as the push-forward of the isorevenue law under ; is not a product measure. The page prints ; the formalization uses .
Trivializing formalizations are ruled out: carries the support condition (without it the regret is unbounded), the regret at is that of the stated reserve law , and both classes are nonempty.
A complete development needs: Lebesgue–Stieltjes integration by parts for CDFs, Myerson's envelope characterization of DSIC payments, push-forwards and mixtures of measures on , and conditionally complete lattice reasoning for the minimax value. The DSIC property of and the payment characterization are reusable throughout auction theory. Proofs of any milestone, and lemmas towards Myerson's characterization, are welcome.
Data-protection laws such as the European Union's General Data Protection Regulation (GDPR) shift control over personal data from firms to consumers: data may be collected and used only with the consumer's consent and only for the purposes she allows. The usual expectation is that such a rule helps consumers and costs firms. Xu, Wang and Zhang (Management Science, forthcoming) examine this expectation in an online retail market where consumer data has two uses. Upside utilization (saved carts, location sharing, recommendations) lowers the consumer's shopping inconvenience. Downside exploitation (monetizing the data) earns the retailer money at the consumer's expense.
For a single retailer the paper finds that the GDPR raises the firm's profit and social welfare (Theorem 1). This mission formalizes the second main result, Theorem 2: once the retailer buys from an upstream supplier, the GDPR can make consumers, the retailer and the supplier all strictly worse off at once. Supply chains are the common structure of online retail, so this matters for anyone assessing a privacy rule by its effect on a single firm.
A unit mass of consumers values one product at . Shopping without the website's data-driven functions costs a consumer an inconvenience , uniform on . The data quality is . A consumer who buys at retail price and hides her data gets ; one who buys and discloses gets
where is the retailer's monetization intensity. Monetizing at intensity costs the retailer () and earns per disclosed record, so her data profit is when consumers disclose. A consumer buys iff her best buying utility is non-negative. The demand is the measure of buyers, and the consumer surplus is , where is the consumer's best buying utility.
The game has four stages. The retailer decides whether to collect data (). The supplier, whose production cost is zero, sets a wholesale price . The retailer sets . Then consumers buy and disclose or hide. The retailer earns and the supplier . Two data policies are compared:
Without collection both modes give the hiding utility . The paper's constants are
Outcomes are those of a subgame-perfect equilibrium (SPE): an REE at every , a retailer price that is a best response at every , a supplier price that is a best response after each , and a profit-maximizing .
With , , , and , SPE exist under both policies, and for every pair of SPE the GDPR's effect on (consumer surplus, retailer profit, supplier profit) is:
Every sign is strict.
Lemma 1 (the hide / disclose / no-buy partition of the market), display (5) (the retailer's pricing reaction ), Propositions 3 and 4 (the equilibria of the two modes), Corollary EC.1 (who collects data under which policy), and Propositions EC.11, EC.12, EC.13 (one column of the theorem each: consumer surplus, retailer profit, supplier profit).
The result. Theorem 2 is a counterexample to the view that consumer data protection is a transfer from firms to consumers. In the triple-lose interval the GDPR makes the retailer stop collecting data. That removes the inconvenience reduction consumers valued and shrinks the market, so the supplier loses too. Corollary EC.1 shows that the GDPR shrinks the range of valuations in which data is collected at all. The comparison with the single-firm case (Theorem 1) isolates the supplier's wholesale pricing as the source of the harm.
Formalizing it. The paper's arguments are algebraic and piecewise: an REE fixed point with a kink at full market coverage, global maximization of piecewise-quadratic profits, a nested maximization for the supplier, and comparisons of thresholds involving square roots. Several printed statements hold only on part of their stated range. Display (5) fails when the market saturates. The "otherwise" clauses of Propositions EC.11 and EC.13 fail at the points where the retailer is indifferent about collecting. Several proof displays carry typos. A machine-checked development pins the exact ranges and gives a reusable, fully specified model of consumer-data policies in a vertical chain. No machine-checked proof of these results is known.
The obvious argument plugs the printed closed forms into each other and compares them. That argument does not reach the theorem as stated. The theorem is about every subgame-perfect equilibrium of the game, defined from the utilities, not about the closed forms. So the work is to show that the equilibrium is pinned down at every node, including off the path. The REE must be shown unique at every price. The retailer's best response must be derived globally over , including the saturated branch, where demand equals 1 and the printed formula (5) is wrong. The supplier's profit must be maximized across the kink. After that, the five sign patterns rest on a chain of strict inequalities among and among the equilibrium profits, which must hold for all and .
All statements live in the namespace RetailPrivacy.SupplyChain and use one definition file, RetailPrivacy.SupplyChain.Model. That file holds the policy (Policy.R, Policy.C), the constants , the hide and disclose utilities, demand and disclosing quantity as Lebesgue measures of sets of , consumer surplus as an interval integral, the REE predicate, strategy profiles with actions at every node, and the SPE predicate. Collection is a Bool. Prices range over all of and the intensity over . The standing assumptions are , and the added : the paper leaves implicit, and at nothing is sold and every strict claim fails. The consumer-stage definitions are textually identical, up to the namespace, to those of the single-firm mission of this series.
Departures from the print, each disclosed in the item: display (5) is stated on its valid range; Propositions 3(iii) and 4(iii) are stated as comparisons of the retailer's subgame profits; Corollary EC.1 is stated with strict inequalities; and the "otherwise" clauses of EC.11 and EC.13 are stated without the indifference points.
Four formalizations would trivialize the goal, and none is acceptable: comparing the printed closed forms instead of equilibrium outcomes; an "every equilibrium" claim that might be vacuous (the goal asserts existence); profiles that omit off-path actions, which would make the supplier's or the retailer's optimality checks vacuous; and price domains restricted to or to unsaturated markets.
The paper's proofs are in its e-companion, Appendix C (pp. ec21–ec38). Useful contributions include the consumer-stage lemmas (REE uniqueness and its closed form), the global best-response computations, and the threshold inequalities, each a self-contained lemma.
Social-media influencers earn money by endorsing products to their followers. An endorsement of a product that does not fit the audience brings in money today but costs followers, and followers are also what spreads awareness of the influencer to new people. Nistor, Selove and Villas-Boas (Influencer Authenticity: To Grow or to Monetize, Management Science, 2024) model this trade-off as a deterministic, infinite-horizon, discounted optimal-control problem with a single binary control. In their base model (§3) the optimal policy is to grow first and monetize later: authentic while awareness is small, permanently inauthentic once awareness passes a threshold.
Section 4.2 of the paper asks how this changes when the audience is not permanent: users join and leave the platform, or the influencer covers a topic that interests people only for a while. With follower turnover the influencer never reaches full awareness, and Proposition 3 says that if turnover is fast enough she never monetizes at all. The model gives a testable prediction: influencers on platforms with rapid user turnover, or in product categories with short-lived interest, should stay authentic.
Time is . There is a unit mass of potential followers, and is the share of them who are aware of the influencer, starting from . At each time she is either authentic or inauthentic. Following Table 1 of the paper:
with and . These are the reduced-form parameters of §3.1: a fraction of aware people follow an inauthentic influencer, who earns per follower, and authentic profit per follower is normalized to . The paper assumes "for the remainder of the paper", so that being inauthentic pays more today.
Potential followers leave and are replaced at a turnover rate , and awareness follows equation (6):
where is the word-of-mouth rate. Under the always-authentic policy this is the logistic equation , with steady state . The influencer maximizes the discounted profit (2), , with discount rate .
In the Lean development (namespace InfluencerAuth.Turnover) a policy is a measurable set of the times at which she is inauthentic, so is "always authentic". IsPath β γ x A₀ S A says is an admissible awareness path, discountedProfit γ φ r S A is (2) at time , and IsOptimalFrom β γ φ r x A₀ S A says that earns at least as much as every measurable policy with any admissible path from the same . authValue β x r is the closed form of Lemma 5, and Condition2 γ φ β r x is
Under the standing assumptions , , , , , with and Condition 2,
The range of is the paper's set of "all feasible levels of awareness". The statement fixes no constant beyond those of Condition 2.
For and every admissible always-authentic path from ,
Proposition 3 is the paper's result on when the grow-then-monetize pattern of the base model breaks down. Without turnover the influencer always monetizes once she is large enough (Proposition 1, §3). With turnover there is a whole parameter region, given by Condition 2, where monetizing is never optimal. The condition compares the extra current profit from being inauthentic, , with the awareness lost by being inauthentic, , valued at the marginal value of awareness at the steady state, from (7).
The proofs are in an online appendix that is not part of the published article, and this result has no machine-checked proof. The mission provides a precise statement of the control problem: optimality over every measurable switching pattern, with the dynamics in integral form. It also gives the closed-form always-authentic value and its derivative as separate targets. A complete development would be one of the first formal optimality proofs for an infinite-horizon, discounted, continuous-time deterministic control problem.
Optimality is claimed against every measurable policy, not only against constant or threshold policies. The natural argument is a verification theorem: show that satisfies the Hamilton–Jacobi–Bellman inequality on the feasible range, then integrate along an arbitrary competitor path. Condition 2 is stated only at the steady state , where (7) gives the marginal value of awareness. At a lower awareness level the inequality comparing the two actions involves at that level, so it does not follow from Condition 2 alone; it needs control of on the whole interval. A competitor path may also switch infinitely often, so its awareness is only absolutely continuous, and the comparison must work almost everywhere. Above the steady state the always-authentic policy is in general not optimal, so any argument must use the restriction .
Set ℝ. An admissible path is continuous on , starts at , stays in , and satisfies for , with on and off . This is the Carathéodory form of (6). A derivative everywhere is not required, because that would exclude every switching policy. The clause follows from the equation and is stated to make integrability explicit.discountedProfit is with on and off ; the paper's value from time is the same object after the shift . No optimal value is defined as a real supremum; optimality is a comparison with every competitor.Fake follower accounts are sold openly to social media influencers, who buy them because advertisers and new followers read a large follower count as a sign of quality. Platforms respond with antifake effort: detection, removal and registration hurdles that make fake accounts more expensive to operate, but that also impose a nuisance cost on legitimate users (more CAPTCHAs, more false flags). Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game and ask how fake-account purchases respond to the platform's effort and to contextual factors such as social media literacy and antifake technology.
A finding of the paper that runs against intuition concerns the high-quality influencer. In a costly separating equilibrium the high type buys fake accounts defensively, so that a low-quality influencer cannot afford to mimic its follower count. This contrasts with Chen and Papanastasiou (2021), where only the low type manipulates. Proposition 3 of the paper describes how this defensive purchase moves with every parameter, and in particular that raising the antifake effort can increase it. This mission formalizes Proposition 3 and the steps the paper uses to explain it.
An influencer is of high type or low type , with content qualities . A unit mass of consumers has valuation and follows when . A fraction of consumers, the social media literacy, know the type; the rest infer it from the early follower count, which the influencer can inflate with fake accounts. Advertising yields revenue per real follower, of which the influencer keeps a share .
The platform chooses an antifake effort . With antifake technology level , base price , opportunity cost and nuisance coefficient , the unit price of fake accounts and the cost of following are
A type of quality has informed followers, and, when its type is revealed, uninformed ones. With and , Lemma 2 of the paper gives the costly separating equilibrium for , in which the H-type's early-follower count is
and its defensive purchase is . In the pooling equilibrium the low type's offensive purchase is . In Lean the parameters are fields mu lamI lamP rho l qH qL c0 c1 tau p0 gamma of a structure Params, and the quantities above are price, cost, nIn, nUnSep, eta2, d2, nCsep2, xCsepH, xPoolL.
Assume , and Assumption 3 (). Let (22) be the condition
If (22) holds, is strictly decreasing on . Otherwise there is with strictly increasing on and strictly decreasing on .
A companion theorem, not a milestone, states Proposition 2(a)–(b) for the offensive purchase .
Proposition 3(c) says that the platform's main instrument against fake accounts can backfire: below a threshold on the technology level, a moderate increase in antifake effort makes high-quality influencers buy more fake accounts, because the higher nuisance cost widens the follower gap the low type would have to close. Proposition 3(a) identifies the levers that reduce defensive purchases unambiguously: literacy, the base price, and antifake technology. Together with Proposition 2, these results underlie the paper's policy discussion of when an antifake campaign reduces the number of fake accounts at all.
The results are proved in the paper's Online Appendix; none of them is machine-checked. The formalization makes every hypothesis explicit: positivity of and , the exact domain on which each monotonicity claim is strict, and the reading of the informal remark "", which is false as and true at the edge of the costly separating range. It also yields a reusable closed form for the equilibrium purchase that other statements about this model can cite.
The closed form and the derivative are algebra and calculus over rational functions of , with care about . The content is the dichotomy in (c). On the two marginal effects have opposite signs, , and both depend on through and through . The paper's informal argument (", so dominates eventually") settles only the right end of the range. What the goal requires is the sign of on the whole interval: that it changes sign at most once, that (22) is exactly the condition for it to be nonpositive at , and that in the other case the change of sign happens strictly inside . Strictness of the parameter comparative statics also fails at the edges ( for , for ), so each domain has to be chosen exactly.
All quantities are real-valued closed forms; no probability spaces are introduced, since the paper's expectations over are already the closed forms (8)–(9). The parameter bundle carries the standing ranges of §3 and Table 1: , , , , , , , , . The readings of the paper fixed by the formalization are:
is defined as through (17), not by the right side of (20); a definition by (20) would make the closed-form milestone trivial. The goal must be proved about this function on , not about a sign condition on an abstract derivative. The proofs are in the paper's Online Appendix, which is not used here; every milestone is a statement or display of the main text. Contributions of proofs of any milestone are welcome, as are lemmas on single-crossing of the derivative.
In many sequential decision problems, playing one action reveals the outcome of other actions too. A bidder in a first-price auction who bids and sees the winning price learns whether every bid at or above that price would have won. A recommender that shows one item learns something about related items. Two kinds of side information recur. Graph feedback across actions: playing action also reveals the rewards of the out-neighbours of in a directed graph (Mannor and Shamir 2011; Alon, Cesa-Bianchi, Dekel and Koren 2015). Cross learning across contexts: the reward of the chosen action is revealed under every context, not only the current one (Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider 2019).
Han, Zhou and Weissman (arXiv:2003.09795v7) reduce learning to bid in repeated first-price auctions to a contextual bandit with both structures. Their §3 starts from a simple arm-elimination algorithm that exploits graph feedback (Algorithm 1) and extends it to contexts with cross learning (Algorithm 2). This mission formalizes that layer: the algorithms, their concentration lemma, and their high-probability regret bounds (Theorems 3 and 4).
Timeline:
A stochastic contextual bandit with graph feedback and cross learning (Definition 2) has a horizon , contexts , actions , a joint reward law supported on with mean rewards , and a directed graph without self-loops. In round a context is revealed, the learner picks , nature draws iid from , and the learner observes for every and every . The regret (5) is
Definition 1 is the case , with regret (4). The independence number of is the largest size of a set of actions with no edge between any two of them.
Algorithm 2 keeps for each context an active set and a minimum count , and for each action a count shared by all contexts. In each round it plays an action of , either of largest out-degree in the graph restricted to (Option I) or of in-degree zero there (Option II, for DAGs). When every active action of context has been observed more than times, the active set drops the actions whose empirical reward falls below the best by more than . Algorithm 1 is the case .
With probability at least , writing ,
for every context sequence and every tie-breaking rule.
Theorem 4 shows that one algorithm attains, up to logarithmic factors, the better of two regret rates: , available from cross learning alone, and , available from graph feedback alone. The paper then shows (Theorem 6) that with adversarial contexts nothing better than is possible, while with stochastic contexts and a partial order a variant reaches for first-price auctions. Algorithm 2 is the building block of that variant.
The results are proved in the paper; none is formalized. A formal development produces machine-checked versions of a concentration inequality with a random number of observations, of a domination bound for directed graphs, and of an elimination analysis with shared counts across contexts. Four printed statements need correction, and the formal statements record the corrected forms: the constant in Theorem 4's second bound (the printed proof gives ); Lemma 10, which is false for and for edgeless graphs as worded; Lemma 1, which fails for and close to (excluded by ); and the pseudocode of Algorithms 1–2, whose update can leave empty after an elimination (the formalization keeps the text's invariant , and coincides with the printed algorithm wherever the latter is defined).
The observations of an action are not a fixed sample: how often and when action is revealed depends on earlier rewards through the algorithm's choices. A union bound with Hoeffding's inequality at a fixed sample size does not apply directly, and Lemma 1 needs a self-normalized martingale inequality.
For Option I, the obvious bound on how long it takes to observe every least-pulled action once more is rounds, which gives only . Getting instead of requires that a vertex of largest out-degree covers a fraction of the remaining vertices; this is the content of Lemma 10, a probabilistic-method bound that is not in Mathlib. For contexts, the per-context analyses must be combined while counts are shared, and the bound in needs a per-action rather than a per-context accounting.
Fin K, contexts Fin M, rounds Fin T; paper round is Lean index . The feedback graph is a relation E with no self-loops; "independence number " is the hypothesis that every independent set has at most elements (all bounds increase in ).Fin M → Fin K → ℝ carried by ; rewards are iid across rounds (Measure.pi). The regret is the pseudo-regret with means .Welcome contributions: the self-normalized inequality of de la Peña, Klass and Lai (Lemma 11), Lemma 10, invariants of Algorithm 2 (the active sets stay nonempty and contain an optimal action on the good event), and the deterministic regret accounting given the concentration event.
Large online retailers such as Amazon sell their own products and, on the same storefront, host third-party sellers who pay a commission on their sales. The owner of such a retailer-led marketplace sets the commission, competes with the sellers it hosts, and can direct inattentive consumers to the offer of its choice. How these levers interact is a central question in the economics of digital platforms and in the current policy debate on platform fees and self-preferencing.
Hervas-Drane and Shelegia (2025) build a model of a monopoly retailer with a marketplace and an assortment capacity constraint, and derive the platform's entry pattern, its fee and the effect of policy interventions. A basic question about the fee is whether a retailer that can sell products itself would ever choose to run its marketplace for free, collecting nothing from the sellers it hosts. This mission formalizes the paper's answer, Lemma 2: it never does.
There is a unit mass of products, indexed by their consumer valuation . Valuations are distributed according to a probability measure (the CDF of the paper) on , where is the marginal cost every firm incurs per unit. Each product is an independent market with a unit mass of consumers who each buy one unit at any price .
The monopolist owns the storefront. For each product there is one third-party seller who can sell only through the marketplace. The game has three stages.
The pricing stage (Proposition 1 of the paper) gives per-market payoffs. If sells alone (SBM) he earns . If sells alone (SBT) she charges and collects . If both sell (SBMT), charges
and earns . Seller enters exactly the marketplace products (Lemma 1). Given an allocation , 's profit is
and his profit as a function of the fee is the value of his allocation problem,
The paper maintains Assumption 1, : the monopolist steers over half of the consumers.
For every with for all ,
The statement is about every maximising fee. It does not assert that a maximiser exists, which the paper does not claim in Lemma 2.
The map has a right derivative at , and it is strictly positive:
Lemma 2 is the first result of the paper's fee analysis. It says that the fee is an active instrument in every configuration of capacity and steering: even a monopolist who can sell every product himself extracts revenue from the sellers he hosts, because at a zero fee the first-order effect of raising it is positive. The paper's subsequent characterisation of the optimal fee (Proposition 3) and its policy results on fee caps and on banning the retailer from its own marketplace (Propositions 4–6) all take place in the region that this lemma secures.
The paper proves Lemma 2 in two sentences, by "inspection of ". None of the results is formalized elsewhere. The formal development has to make the inspection precise: is the value of an infinite-dimensional allocation problem whose optimal allocation changes with , so its one-sided differentiability at is an envelope-type statement rather than a calculus exercise. The model layer (the marketplace set, the Proposition 1 payoffs, the allocation problem and its value) is shared, in identical form, with the two companion missions of this series.
is a supremum over measurable sets, not a closed-form function of , so its derivative cannot be read off a formula. Two effects change as grows from zero: fee revenue rises on every marketplace product, while the products with leave the marketplace and their sellers stop paying fees. At these products pay no fee, so their loss is of second order. Making this precise requires control of the optimal allocation uniformly near and of the mass of the exiting products, using only that has a density.
The naive argument "keep the allocation optimal at and raise the fee slightly" shows that some positive fee beats , but it does not compute the derivative. The claim also fails in one corner: with and the SBMT payoff equals the SBM payoff, the monopolist supplies every product at every fee, and does not depend on .
The Lean development lives in the namespace RetailerMarketplace.PositiveFee. Valuations are a measure μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0 (support in ) and μ ≪ volume (the density ). Allocations are arbitrary measurable sets of mass at most , never intervals. is defined as the supremum of profitM over them (PiM); by the paper's Proposition 2 it coincides with the closed form (4), which this mission cannot use because its thresholds are the conclusion of Proposition 2. The marketplace set is {v | c ≤ v * (1 - f)}, correct also at , where it is empty.
Standing and added hypotheses, all disclosed in the item statements:
No full-support hypothesis and no existence of an optimal fee are assumed.
Trivializing formalizations are ruled out: the supremum is over a nonempty family that is bounded above under integrability, so PiM is not a junk sSup; and the goal quantifies over every maximiser rather than asserting that some positive fee beats .
A complete development needs set integrals over , a bathtub-type comparison of allocations, and one-sided derivatives of a value function. The value-function and allocation lemmas are reusable for the companion missions on entry modes and on per-unit fees. Contributions of intermediate lemmas, such as attainment of by a top- allocation, are welcome.
The Lightning Network (LN) is a second-layer payment system for Bitcoin. Instead of recording every payment on the blockchain, two parties lock funds in a payment channel and settle many payments off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it carries. Which channel topology supports a given pattern of payments at least total cost is therefore an economic design question for the network's participants.
Guasoni, Huberman and Shikhelman (SSRN 4439190, 2023; published in Management Science, 2024) study this question for a general cost function, assuming only a few qualitative properties derived in their earlier work on channel economics ([GHS22], Lightning Network Economics: Channels). This mission covers §3.1 of the paper, local channel reconfiguration: a relaying node can be bypassed at lower cost, odd cycles are never optimal, and a cost-minimizing network is bipartite with every net flow going from one side to the other. Three companion missions (II–IV of this series) cover hermetization by a routing hub (§3.2) and bounds on the global minimal cost (§3.3).
Let be a finite set of nodes. A payment flow is a vector of net flows with . A Lightning Network on is an anti-symmetric real matrix , , where is the net flow from to in the channel between them and means there is no channel. The network supports if
A channel cost function is with
The cost of a network is , the sum of over its channels. A network is cost-minimizing for if it supports and no Lightning Network on the same node set that supports has smaller cost.
The paper's channel notation: is a channel with net flow from to , and is a channel in which sends and sends , so the net flow from to is .
If is cost-minimizing for , there is a set with such that the channel graph ( iff ) is bipartite with parts , and
The statement is conditional and does not assert that a minimizer exists.
Corollary 3.3 says that in an optimal Lightning Network every node is a pure sender or a pure receiver, and that no node relays payments. This sits in tension with the observed LN, which is organized around large routing hubs; the paper reconciles the two in §3.2 by allowing new nodes. Corollary 3.11 shows that the star, the intuitive candidate for a cheapest topology, is optimal only with a single net payer or a single net payee.
The results are proved in the paper, with short arguments in its Appendix A, and they have no machine-checked proof. This mission adds a precise version of the model, in which the meaning of "cost-minimizing", the sign conventions and the corrected cost axioms are fixed, and a formal proof of the chain Theorem 3.1 → odd cycles → bipartite structure for an arbitrary cost function satisfying the axioms.
Theorem 3.1 on its own is a two-line computation. The difficulty is in applying it inside an arbitrary network. When and already share a channel, adding or to it requires for reals of either sign. That inequality is not among the axioms and has to be derived from them. The odd-cycle step needs a pigeonhole argument on channel orientations around a cycle. The bipartite step needs either König's characterization of bipartite graphs or a direct construction of the parts from the flow directions. The naive formalization that re-states Theorem 3.1 only for a network with exactly two channels does not reach the corollaries.
V, not . The matrix is Λ : V → V → ℝ, because λ is a Lean keyword.Supports, which is independent of the sign.Fin k → V, odd, with cyclic successor finRotate k. A channel is a nonzero entry in either direction.SimpleGraph.IsBipartiteWith A Aᶜ on the channel graph, with the flow-direction clause stated separately as the stronger content.Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (no or linear cost); cost-minimization ranges over all networks on , not over a fixed edge set; is not fixed to three nodes; the in-and-out claim is stated for arbitrary networks; and and are complementary, so they cannot overlap.
König's theorem is in Mathlib (SimpleGraph.two_colorable_iff_forall_loop_even) and proved on the platform (FamousTheorems.two_colorable_iff_no_odd_cycle_6b), so it is not posed here. The derived two-sided subadditivity of , and a lemma rerouting a relayed flow inside an arbitrary network, are reusable in the other missions of the series. Contributions of such auxiliary lemmas are welcome.
Industries in which capacity can be built but not sold back (energy generation, manufacturing, mining) are studied through irreversible investment models: a firm controls a nondecreasing investment process and trades the cost of capacity against uncertain future revenues. When many small firms compete, each firm's revenue depends on aggregate production through the market price, and the natural equilibrium notion is a mean-field equilibrium: every firm optimizes against a given aggregate, and the aggregate generated by the optimal behaviour is the one that was assumed.
Aïd, Basei and Ferrari (arXiv:2305.00541; Operations Research, 2025) add a macroeconomic regime to this picture. The economy switches between two states according to a continuous-time Markov chain, and volatilities and prices depend on the state. They prove that a stationary mean-field equilibrium exists and is unique, and that the equilibrium firm invests at regime-dependent barriers. Related stationary mean-field games with singular controls include Cao and Guo (Stochastic Processes and their Applications, 2022) and Cao, Dianetti and Ferrari (doi:10.1287/moor.2022.1323); the stability of the reflected regime-switching diffusions that appear in the equilibrium is due to Budhiraja and Liu (Mathematics of Operations Research, 2012).
A real Brownian motion and an independent two-state Markov chain with generator
live on a complete probability space; is their augmented natural filtration. A control is an adapted, nonnegative, nondecreasing càdlàg process with . The production capacity is
and investment costs , the integral (2.3) that charges a jump the amount . Given aggregate productions , the price in regime is , and a firm starting from maximizes, over the admissible set of (2.5),
A stationary mean-field equilibrium (Definition 2.2) is a pair such that maximizes over , and the controlled pair has a stationary distribution with
The barrier control at levels is
the minimal investment keeping . Finally and , whose negative roots are .
Under Assumption 2.1, , and : for every there are barriers and with
The theorem gives a fully explicit equilibrium in a model with common noise in the form of regime switching: the barriers solve a finite system of algebraic equations, and the stationary distribution of capacities is known in closed form, with a Pareto tail of exponent . This makes comparative statics of market concentration and of the industry's response to regime persistence computable, which is what Section 3 of the paper does numerically.
The result is proved on paper; none of it is formalized. A complete development would yield a machine-checked verification theorem for regime-switching singular control, a checked link between singular control and optimal stopping, and a checked stationary law for a reflected regime-switching geometric Brownian motion. The printed text contains slips the formalization corrects in the open: the continuation and stopping regions of Proposition 4.2 are printed swapped, a term of (4.18) carries a spurious factor , and an integration by parts in the proof drops .
The obvious route, solving the variational inequality (4.8) by guessing a smooth-fit solution, fails here: the two regimes couple the ordinary differential equations, and the smooth-fit and smooth-pasting equations become nonlinear in both barriers at once, so existence and uniqueness of their solution cannot be read off. The regularity a verification argument needs ( value, a threshold structure of the investment region) is therefore the hard part, and with regime switching it is not covered by the one-dimensional theory. The stationary law requires positive recurrence of a reflected diffusion with switching and the identification of its limit law. The fixed point , where is built from the stationary law under the barrier control optimal for , needs continuity and a priori bounds of for existence, and a monotonicity argument for uniqueness; the printed uniqueness argument treats ordered pairs of fixed points explicitly, and uniqueness of the optimal control itself is not argued on the page but is part of the goal.
Lean represents regimes as Fin 2 (index 0 is regime 1) and time as . The model consists of: the chain, pinned by its closed-form transition function ; Mathlib's IsBrownianReal for ; independence of and ; the augmented filtration; through the platform relation EthierKurtz.HasBrownianItoIntegral, with continuous paths; the state (2.4); the integral (2.3), computed as ; the admissible set (2.5) with -valued expectations; of (2.6); Definition 2.2; and the barrier control (4.11). is the expectation conditioned on .
Standing constants: , , , , and Assumption 2.1. The root condition is stated as " has no root in ". Pinned hypotheses, each disclosed in the item that carries it: the stationary distribution is the weak limit of the time- laws; ; wherever (4.11) is used; for the §4.2 statements; on the goal; and "" in Theorem 2.4(ii) as a ratio tending to a positive constant.
The equilibrium is defined from the model: optimality against every admissible control, including those with an initial jump, and the limit law of the actually controlled process. It is never defined through the paper's closed forms (4.23) or (4.32), which would make the goal a statement about formulas. The barrier control is the printed formula, not an arbitrary control keeping .
Not formalized: Section 3 (numerics), Proposition 4.4 and Corollary 4.5 (semi-explicit value functions), the continuity part of Step 1, and Steps 2–4 of the proof as separate items. Contributions toward a general verification theorem for regime-switching singular control, regularity of regime-switching stopping problems, and stationary laws of reflected switching diffusions are reusable beyond this mission.
In budget-feasible procurement an auctioneer with a budget wants to buy services from strategic sellers. Each seller has a private cost , the auctioneer has a public valuation over sets of sellers, and the mechanism must choose whom to pay and how much, so that sellers have no reason to misreport and the total payment never exceeds . The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a buyer with a fixed budget faces sellers whose costs it cannot observe.
Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239v2, Operations Research 2025) show that deterministic clock auctions, which repeatedly lower personalized prices and let sellers drop out, achieve constant approximations for monotone submodular valuations. Their Appendix B asks whether an even simpler family suffices: posted-price mechanisms, which approach each seller once with a take-it-or-leave-it offer. This mission formalizes their answer for additive valuations, Theorem 13 (p. 25): no deterministic posted-price mechanism achieves an approximation better than .
There are sellers , a budget , private costs , and a valuation . The valuation is additive if there are values with for every .
A deterministic posted-price mechanism knows , and , but not . It approaches sellers one at a time. At each step it looks at the history of earlier offers (the seller, the price, and whether the seller accepted) and either stops or names a seller not yet approached and a price . The seller accepts if and rejects otherwise, and is never approached again. The output is the set of sellers who accepted; each of them is paid its price. The mechanism is budget feasible if for every additive and every cost profile the accepted prices sum to at most .
For an instance, is the largest value of a set with . A mechanism is a -approximation on a class if on every instance of the class.
In Lean the sellers are Fin n, a mechanism is M : (Finset (Fin n) → ℝ) → PostedPrice n with PostedPrice n a rule next : List (Fin n × ℝ × Bool) → Option (Fin n × ℝ) on histories, run (M v) c is its history on the costs c, and accepted and payment read off the output and the total payment.
For every , every and every budget-feasible deterministic posted-price mechanism , there are an additive , costs and a set with
This is on some instance, written without division.
All three concern one valuation : a high-value seller worth and small sellers worth each, with .
The theorem separates two families of simple mechanisms. Deterministic clock auctions achieve a constant approximation for monotone submodular valuations (Theorem 1 of the same paper, a -approximation), while deterministic posted prices cannot achieve better than even for additive valuations, the simplest class. Clock auctions are therefore not merely sufficient but needed among these simple formats: the ability to lower a price after a refusal is what the constant approximation rests on. The bound also explains why the paper's positive result for posted prices (Theorem 15, symmetric submodular valuations) must give up a logarithmic factor.
The result is proved in the paper; it has not been formalized. A formal version fixes what "deterministic posted-price mechanism" means, an adaptive rule on histories that never sees costs, and makes the adversary argument checkable: the hard instance depends on the mechanism, and the case analysis must be exhaustive over all such rules. The mission also provides a reusable model of sequential take-it-or-leave-it mechanisms with budget constraints.
The statement is a lower bound over all mechanisms, so the instance must be chosen after the mechanism. The mechanism is adaptive: which seller it approaches next and at what price can depend on every earlier answer. The proof handles this by noting that, on the hard family, every seller rejects a non-positive offer, so all instances share the run up to the first positive offer or the offer to . Making that "common prefix" precise for an arbitrary history-dependent rule, and covering the mechanisms that fall outside the three printed cases (those that never approach , or offer more than ), is the work of the formal proof. A naive attempt that fixes one instance for all mechanisms fails: a mechanism tailored to that instance is optimal on it.
Fin n; valuations are functions Finset (Fin n) → ℝ, and additivity carries nonnegative weights. Costs are real and nonnegative.Contributions welcome: proofs of the three cases, the "common prefix" lemma for runs on cost profiles that agree on every seller approached, and the assembly of the goal.
Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.
Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in , which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.
Let , , be open, bounded and of class S: there are and such that for all and . Let be compact, let , and set (Assumption 1.1, eq. (3)). The solution operator maps to the unique weak solution of in , on .
For a control , a cost and a threshold , the robust problem (63) is
The state is , , and . The cone is and its polar cone is . The linear part of the state is . The active set is .
Let be convex and continuously Fréchet differentiable, and assume the constraint qualification . Then is a solution of (63) if and only if there is a nonnegative finite Borel measure on with, for ,
The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in by integration. Both directions are part of the goal.
The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.
All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of and does not treat . Condition (68) is printed per direction , while (67a) needs one measure for all .
The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone has nonempty interior. The multiplier is a priori only an element of , and the Riesz–Markov–Kakutani theorem on the compact space turns it into a measure. The state must also be shown to lie in . Continuity of each slice in is the regularity of Lemma 1.2 (continuity of solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in . Working pointwise in does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.
and are subtypes of Euclidean spaces with CompactSpace instances, so carries its sup norm. Measures on are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map such that is, for every , the weak solution in , encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's " in " is encoded on , the same condition for continuous functions. "Solution" means global minimizer over the feasible set. is identified with through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.
Added hypotheses: and nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion in , where represents . The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.
Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into . The multiplier carries its sign (a nonnegative measure, or ) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.
A complete development needs elliptic regularity in for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on ), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them are welcome.